[GOAL]
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
P : M
h : IsLprojection X P
x : X
⊢ ‖x‖ = ‖(1 - P) • x‖ + ‖(1 - (1 - P)) • x‖
[PROOFSTEP]
rw [add_comm, sub_sub_cancel]
[GOAL]
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
P : M
h : IsLprojection X P
x : X
⊢ ‖x‖ = ‖P • x‖ + ‖(1 - P) • x‖
[PROOFSTEP]
exact h.Lnorm x
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ Commute P Q
[PROOFSTEP]
have PR_eq_RPR : ∀ R : M, IsLprojection X R → P * R = R * P * R := fun R h₃ => by
  --porting note: Needed to fix function, which changes indent of following linesrefine
    @eq_of_smul_eq_smul _ X _ _ _ _ fun x => by
      rw [← norm_sub_eq_zero_iff]
      have e1 : ‖R • x‖ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ :=
        calc
          ‖R • x‖ =
              ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) :=
            by rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub, mul_smul]
          _ =
              ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
                (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖) :=
            by rw [h₃.proj.eq, sub_smul 1 P, one_smul, smul_sub, mul_smul]
          _ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) := by
            rw [sub_mul, h₃.proj.eq, one_mul, sub_self, zero_smul, zero_sub, norm_neg]
          _ = ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖ := by abel
          _ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ :=
            by
            rw [GE.ge]
            have := add_le_add_right (norm_le_insert' (R • x) (R • P • R • x)) (2 • ‖(1 - R) • P • R • x‖)
            simpa only [mul_smul, sub_smul, one_smul] using this
      rw [GE.ge] at e1
      nth_rewrite 2 [← add_zero ‖R • x‖] at e1
      rw [add_le_add_iff_left, two_smul, ← two_mul] at e1
      rw [le_antisymm_iff]
      refine' ⟨_, norm_nonneg _⟩
      rwa [← mul_zero (2 : ℝ), mul_le_mul_left (show (0 : ℝ) < 2 by norm_num)] at e1
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
⊢ P * R = R * P * R
[PROOFSTEP]
refine
  @eq_of_smul_eq_smul _ X _ _ _ _ fun x => by
    rw [← norm_sub_eq_zero_iff]
    have e1 : ‖R • x‖ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ :=
      calc
        ‖R • x‖ =
            ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) :=
          by rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub, mul_smul]
        _ =
            ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
              (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖) :=
          by rw [h₃.proj.eq, sub_smul 1 P, one_smul, smul_sub, mul_smul]
        _ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) := by
          rw [sub_mul, h₃.proj.eq, one_mul, sub_self, zero_smul, zero_sub, norm_neg]
        _ = ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖ := by abel
        _ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ :=
          by
          rw [GE.ge]
          have := add_le_add_right (norm_le_insert' (R • x) (R • P • R • x)) (2 • ‖(1 - R) • P • R • x‖)
          simpa only [mul_smul, sub_smul, one_smul] using this
    rw [GE.ge] at e1
    nth_rewrite 2 [← add_zero ‖R • x‖] at e1
    rw [add_le_add_iff_left, two_smul, ← two_mul] at e1
    rw [le_antisymm_iff]
    refine' ⟨_, norm_nonneg _⟩
    rwa [← mul_zero (2 : ℝ), mul_le_mul_left (show (0 : ℝ) < 2 by norm_num)] at e1
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ (P * R) • x = (R * P * R) • x
[PROOFSTEP]
rw [← norm_sub_eq_zero_iff]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖(P * R) • x - (R * P * R) • x‖ = 0
[PROOFSTEP]
have e1 : ‖R • x‖ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ :=
  calc
    ‖R • x‖ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) :=
      by rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub, mul_smul]
    _ =
        ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
          (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖) :=
      by rw [h₃.proj.eq, sub_smul 1 P, one_smul, smul_sub, mul_smul]
    _ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) := by
      rw [sub_mul, h₃.proj.eq, one_mul, sub_self, zero_smul, zero_sub, norm_neg]
    _ = ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖ := by abel
    _ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ :=
      by
      rw [GE.ge]
      have := add_le_add_right (norm_le_insert' (R • x) (R • P • R • x)) (2 • ‖(1 - R) • P • R • x‖)
      simpa only [mul_smul, sub_smul, one_smul] using this
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • x‖ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
[PROOFSTEP]
rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub, mul_smul]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖)
[PROOFSTEP]
rw [h₃.proj.eq, sub_smul 1 P, one_smul, smul_sub, mul_smul]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖)
[PROOFSTEP]
rw [sub_mul, h₃.proj.eq, one_mul, sub_self, zero_smul, zero_sub, norm_neg]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖
[PROOFSTEP]
abel
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖
[PROOFSTEP]
abel
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖
[PROOFSTEP]
rw [GE.ge]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖
[PROOFSTEP]
have := add_le_add_right (norm_le_insert' (R • x) (R • P • R • x)) (2 • ‖(1 - R) • P • R • x‖)
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
this : ‖R • x‖ + 2 • ‖(1 - R) • P • R • x‖ ≤ ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖
⊢ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖
[PROOFSTEP]
simpa only [mul_smul, sub_smul, one_smul] using this
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : ‖R • x‖ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖
⊢ ‖(P * R) • x - (R * P * R) • x‖ = 0
[PROOFSTEP]
rw [GE.ge] at e1
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • x‖
⊢ ‖(P * R) • x - (R * P * R) • x‖ = 0
[PROOFSTEP]
nth_rewrite 2 [← add_zero ‖R • x‖] at e1
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • x‖ + 0
⊢ ‖(P * R) • x - (R * P * R) • x‖ = 0
[PROOFSTEP]
rw [add_le_add_iff_left, two_smul, ← two_mul] at e1
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
⊢ ‖(P * R) • x - (R * P * R) • x‖ = 0
[PROOFSTEP]
rw [le_antisymm_iff]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
⊢ ‖(P * R) • x - (R * P * R) • x‖ ≤ 0 ∧ 0 ≤ ‖(P * R) • x - (R * P * R) • x‖
[PROOFSTEP]
refine' ⟨_, norm_nonneg _⟩
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
⊢ ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
[PROOFSTEP]
rwa [← mul_zero (2 : ℝ), mul_le_mul_left (show (0 : ℝ) < 2 by norm_num)] at e1
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ 2 * 0
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
⊢ Commute P Q
[PROOFSTEP]
have QP_eq_QPQ : Q * P = Q * P * Q :=
  by
  have e1 : P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q) :=
    calc
      P * (1 - Q) = (1 - Q) * P * (1 - Q) := by rw [PR_eq_RPR (1 - Q) h₂.Lcomplement]
      _ = P * (1 - Q) - (Q * P - Q * P * Q) := by noncomm_ring
  rwa [eq_sub_iff_add_eq, add_right_eq_self, sub_eq_zero] at e1
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
⊢ Q * P = Q * P * Q
[PROOFSTEP]
have e1 : P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q) :=
  calc
    P * (1 - Q) = (1 - Q) * P * (1 - Q) := by rw [PR_eq_RPR (1 - Q) h₂.Lcomplement]
    _ = P * (1 - Q) - (Q * P - Q * P * Q) := by noncomm_ring
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
⊢ P * (1 - Q) = (1 - Q) * P * (1 - Q)
[PROOFSTEP]
rw [PR_eq_RPR (1 - Q) h₂.Lcomplement]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
⊢ (1 - Q) * P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q)
[PROOFSTEP]
noncomm_ring
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
e1 : P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q)
⊢ Q * P = Q * P * Q
[PROOFSTEP]
rwa [eq_sub_iff_add_eq, add_right_eq_self, sub_eq_zero] at e1
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
QP_eq_QPQ : Q * P = Q * P * Q
⊢ Commute P Q
[PROOFSTEP]
show P * Q = Q * P
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
QP_eq_QPQ : Q * P = Q * P * Q
⊢ P * Q = Q * P
[PROOFSTEP]
rw [QP_eq_QPQ, PR_eq_RPR Q h₂]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ IsLprojection X (P * Q)
[PROOFSTEP]
refine' ⟨IsIdempotentElem.mul_of_commute (h₁.commute h₂) h₁.proj h₂.proj, _⟩
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ ∀ (x : X), ‖x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
[PROOFSTEP]
intro x
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖x‖ ≤ ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
[PROOFSTEP]
calc
  ‖x‖ = ‖(P * Q) • x + (x - (P * Q) • x)‖ := by rw [add_sub_cancel'_right ((P * Q) • x) x]
  _ ≤ ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖ := by apply norm_add_le
  _ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ := by rw [sub_smul, one_smul]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖x‖ = ‖(P * Q) • x + (x - (P * Q) • x)‖
[PROOFSTEP]
rw [add_sub_cancel'_right ((P * Q) • x) x]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖(P * Q) • x + (x - (P * Q) • x)‖ ≤ ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖
[PROOFSTEP]
apply norm_add_le
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
[PROOFSTEP]
rw [sub_smul, one_smul]
[GOAL]
case refine'_2
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ ≤ ‖x‖
[PROOFSTEP]
calc
  ‖x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖) := by
    rw [h₂.Lnorm x, h₁.Lnorm (Q • x), sub_smul, one_smul, sub_smul, one_smul, add_assoc]
  _ ≥ ‖P • Q • x‖ + ‖Q • x - P • Q • x + (x - Q • x)‖ :=
    ((add_le_add_iff_left ‖P • Q • x‖).mpr (norm_add_le (Q • x - P • Q • x) (x - Q • x)))
  _ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ := by rw [sub_add_sub_cancel', sub_smul, one_smul, mul_smul]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
[PROOFSTEP]
rw [h₂.Lnorm x, h₁.Lnorm (Q • x), sub_smul, one_smul, sub_smul, one_smul, add_assoc]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖P • Q • x‖ + ‖Q • x - P • Q • x + (x - Q • x)‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
[PROOFSTEP]
rw [sub_add_sub_cancel', sub_smul, one_smul, mul_smul]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ IsLprojection X (P + Q - P * Q)
[PROOFSTEP]
convert (Lcomplement_iff _).mp (h₁.Lcomplement.mul h₂.Lcomplement) using 1
[GOAL]
case h.e'_6
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ P + Q - P * Q = 1 - (1 - P) * (1 - Q)
[PROOFSTEP]
noncomm_ring
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P : { P // IsLprojection X P }
⊢ P ≤ P
[PROOFSTEP]
simpa only [coe_inf, ← sq] using P.prop.proj.eq.symm
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
h₁ : P ≤ Q
h₂ : Q ≤ R
⊢ P ≤ R
[PROOFSTEP]
simp only [coe_inf] at h₁ h₂ ⊢
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
h₁ : ↑P = ↑P * ↑Q
h₂ : ↑Q = ↑Q * ↑R
⊢ ↑P = ↑P * ↑R
[PROOFSTEP]
rw [h₁, mul_assoc, ← h₂]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
h₁ : P ≤ Q
h₂ : Q ≤ P
⊢ ↑P = ↑Q
[PROOFSTEP]
convert (P.prop.commute Q.prop).eq
[GOAL]
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
⊢ IsIdempotentElem 0
[PROOFSTEP]
rw [IsIdempotentElem, zero_mul]
[GOAL]
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
x : X
⊢ ‖x‖ = ‖0 • x‖ + ‖(1 - 0) • x‖
[PROOFSTEP]
simp only [zero_smul, norm_zero, sub_zero, one_smul, zero_add]
[GOAL]
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
P : { P // IsLprojection X P }
Q : M
⊢ ↑Pᶜ * Q = Q - ↑P * Q
[PROOFSTEP]
rw [coe_compl, sub_mul, one_mul]
[GOAL]
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
P : { P // IsLprojection X P }
⊢ ↑P * ↑Pᶜ = 0
[PROOFSTEP]
rw [coe_compl, mul_sub, mul_one, P.prop.proj.eq, sub_self]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ (↑P + ↑Pᶜ * ↑R) * (↑P + ↑Q * ↑R * ↑Pᶜ) = ↑P + ↑Q * ↑R * ↑Pᶜ
[PROOFSTEP]
rw [add_mul, mul_add, mul_add, (mul_assoc _ (R : M) (↑Q * ↑R * ↑Pᶜ)), ← mul_assoc (R : M) (↑Q * ↑R) _, ← coe_inf Q,
  (Pᶜ.prop.commute R.prop).eq, ((Q ⊓ R).prop.commute Pᶜ.prop).eq, (R.prop.commute (Q ⊓ R).prop).eq, coe_inf Q,
  mul_assoc (Q : M), ← mul_assoc, mul_assoc (R : M), (Pᶜ.prop.commute P.prop).eq, mul_compl_self, zero_mul, mul_zero,
  zero_add, add_zero, ← mul_assoc, P.prop.proj.eq, R.prop.proj.eq, ← coe_inf Q, mul_assoc,
  ((Q ⊓ R).prop.commute Pᶜ.prop).eq, ← mul_assoc, Pᶜ.prop.proj.eq]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ P ≤ P ⊔ Q
[PROOFSTEP]
rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, ← mul_assoc, P.prop.proj.eq, sub_self, add_zero]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ Q ≤ P ⊔ Q
[PROOFSTEP]
rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, (P.prop.commute Q.prop).eq, ← mul_assoc, Q.prop.proj.eq,
  add_sub_cancel'_right]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ P ≤ R → Q ≤ R → P ⊔ Q ≤ R
[PROOFSTEP]
rw [le_def, le_def, le_def, coe_inf, coe_inf, coe_sup, coe_inf, coe_sup, ← add_sub, add_mul, sub_mul, mul_assoc]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P = ↑P * ↑R → ↑Q = ↑Q * ↑R → ↑P + (↑Q - ↑P * ↑Q) = ↑P * ↑R + (↑Q * ↑R - ↑P * (↑Q * ↑R))
[PROOFSTEP]
intro h₁ h₂
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
h₁ : ↑P = ↑P * ↑R
h₂ : ↑Q = ↑Q * ↑R
⊢ ↑P + (↑Q - ↑P * ↑Q) = ↑P * ↑R + (↑Q * ↑R - ↑P * (↑Q * ↑R))
[PROOFSTEP]
rw [← h₂, ← h₁]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ P ⊓ Q ≤ P
[PROOFSTEP]
rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, (Q.prop.commute P.prop).eq, ← mul_assoc, P.prop.proj.eq]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ P ⊓ Q ≤ Q
[PROOFSTEP]
rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, Q.prop.proj.eq]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ P ≤ Q → P ≤ R → P ≤ Q ⊓ R
[PROOFSTEP]
rw [le_def, le_def, le_def, coe_inf, coe_inf, coe_inf, coe_inf, ← mul_assoc]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P = ↑P * ↑Q → ↑P = ↑P * ↑R → ↑P = ↑P * ↑Q * ↑R
[PROOFSTEP]
intro h₁ h₂
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
h₁ : ↑P = ↑P * ↑Q
h₂ : ↑P = ↑P * ↑R
⊢ ↑P = ↑P * ↑Q * ↑R
[PROOFSTEP]
rw [← h₁, ← h₂]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ (P ⊔ Q) ⊓ (P ⊔ R) ≤ P ⊔ Q ⊓ R
[PROOFSTEP]
have e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * (R : M) * ↑Pᶜ := by
  rw [coe_inf, coe_sup, coe_sup, ← add_sub, ← add_sub, ← compl_mul, ← compl_mul, add_mul, mul_add,
    (Pᶜ.prop.commute Q.prop).eq, mul_add, ← mul_assoc, mul_assoc (Q : M), (Pᶜ.prop.commute P.prop).eq, mul_compl_self,
    zero_mul, mul_zero, zero_add, add_zero, ← mul_assoc, mul_assoc (Q : M), P.prop.proj.eq, Pᶜ.prop.proj.eq, mul_assoc,
    (Pᶜ.prop.commute R.prop).eq, ← mul_assoc]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
[PROOFSTEP]
rw [coe_inf, coe_sup, coe_sup, ← add_sub, ← add_sub, ← compl_mul, ← compl_mul, add_mul, mul_add,
  (Pᶜ.prop.commute Q.prop).eq, mul_add, ← mul_assoc, mul_assoc (Q : M), (Pᶜ.prop.commute P.prop).eq, mul_compl_self,
  zero_mul, mul_zero, zero_add, add_zero, ← mul_assoc, mul_assoc (Q : M), P.prop.proj.eq, Pᶜ.prop.proj.eq, mul_assoc,
  (Pᶜ.prop.commute R.prop).eq, ← mul_assoc]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
⊢ (P ⊔ Q) ⊓ (P ⊔ R) ≤ P ⊔ Q ⊓ R
[PROOFSTEP]
have e₂ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) * ↑(P ⊔ Q ⊓ R) = (P : M) + ↑Q * ↑R * ↑Pᶜ := by
  rw [coe_inf, coe_sup, coe_sup, coe_sup, ← add_sub, ← add_sub, ← add_sub, ← compl_mul, ← compl_mul, ← compl_mul,
    (Pᶜ.prop.commute (Q ⊓ R).prop).eq, coe_inf, mul_assoc, distrib_lattice_lemma, (Q.prop.commute R.prop).eq,
    distrib_lattice_lemma]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
⊢ ↑((P ⊔ Q) ⊓ (P ⊔ R)) * ↑(P ⊔ Q ⊓ R) = ↑P + ↑Q * ↑R * ↑Pᶜ
[PROOFSTEP]
rw [coe_inf, coe_sup, coe_sup, coe_sup, ← add_sub, ← add_sub, ← add_sub, ← compl_mul, ← compl_mul, ← compl_mul,
  (Pᶜ.prop.commute (Q ⊓ R).prop).eq, coe_inf, mul_assoc, distrib_lattice_lemma, (Q.prop.commute R.prop).eq,
  distrib_lattice_lemma]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
e₂ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) * ↑(P ⊔ Q ⊓ R) = ↑P + ↑Q * ↑R * ↑Pᶜ
⊢ (P ⊔ Q) ⊓ (P ⊔ R) ≤ P ⊔ Q ⊓ R
[PROOFSTEP]
rw [le_def, e₁, coe_inf, e₂]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
src✝² : HasCompl { f // IsLprojection X f } := hasCompl
src✝¹ : SDiff { P // IsLprojection X P } := sdiff
src✝ : BoundedOrder { P // IsLprojection X P } := boundedOrder
P : { P // IsLprojection X P }
⊢ ↑(P ⊓ Pᶜ) = ↑⊥
[PROOFSTEP]
rw [coe_inf, coe_compl, coe_bot, ← coe_compl, mul_compl_self]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
src✝² : HasCompl { f // IsLprojection X f } := hasCompl
src✝¹ : SDiff { P // IsLprojection X P } := sdiff
src✝ : BoundedOrder { P // IsLprojection X P } := boundedOrder
P : { P // IsLprojection X P }
⊢ ↑⊤ = ↑(P ⊔ Pᶜ)
[PROOFSTEP]
rw [coe_top, coe_sup, coe_compl, add_sub_cancel'_right, ← coe_compl, mul_compl_self, sub_zero]
[GOAL]
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
src✝² : HasCompl { f // IsLprojection X f } := hasCompl
src✝¹ : SDiff { P // IsLprojection X P } := sdiff
src✝ : BoundedOrder { P // IsLprojection X P } := boundedOrder
P Q : { P // IsLprojection X P }
⊢ ↑(P \ Q) = ↑(P ⊓ Qᶜ)
[PROOFSTEP]
rw [coe_sdiff, ← coe_compl, coe_inf]


[GOAL]
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun n => (-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n)!) c
hs : HasSum (fun n => (-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)!) s
⊢ HasSum (fun n => ↑(expSeries ℝ ℍ n) fun x => q) (↑c + (s / ‖q‖) • q)
[PROOFSTEP]
replace hc := hasSum_coe.mpr hc
[GOAL]
q : ℍ
hq : q.re = 0
c s : ℝ
hs : HasSum (fun n => (-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)!) s
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
⊢ HasSum (fun n => ↑(expSeries ℝ ℍ n) fun x => q) (↑c + (s / ‖q‖) • q)
[PROOFSTEP]
replace hs := (hs.div_const ‖q‖).smul_const q
[GOAL]
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
⊢ HasSum (fun n => ↑(expSeries ℝ ℍ n) fun x => q) (↑c + (s / ‖q‖) • q)
[PROOFSTEP]
obtain rfl | hq0 := eq_or_ne q 0
[GOAL]
case inl
c s : ℝ
hq : 0.re = 0
hc : HasSum (fun a => ↑((-1) ^ a * ‖0‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖0‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖0‖) • 0) ((s / ‖0‖) • 0)
⊢ HasSum (fun n => ↑(expSeries ℝ ℍ n) fun x => 0) (↑c + (s / ‖0‖) • 0)
[PROOFSTEP]
simp_rw [expSeries_apply_zero, norm_zero, div_zero, zero_smul, add_zero]
[GOAL]
case inl
c s : ℝ
hq : 0.re = 0
hc : HasSum (fun a => ↑((-1) ^ a * ‖0‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖0‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖0‖) • 0) ((s / ‖0‖) • 0)
⊢ HasSum (fun n => Pi.single 0 1 n) ↑c
[PROOFSTEP]
simp_rw [norm_zero] at hc
[GOAL]
case inl
c s : ℝ
hq : 0.re = 0
hs : HasSum (fun z => ((-1) ^ z * ‖0‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖0‖) • 0) ((s / ‖0‖) • 0)
hc : HasSum (fun a => ↑((-1) ^ a * 0 ^ (2 * a) / ↑(2 * a)!)) ↑c
⊢ HasSum (fun n => Pi.single 0 1 n) ↑c
[PROOFSTEP]
convert hc using 1
[GOAL]
case h.e'_5
c s : ℝ
hq : 0.re = 0
hs : HasSum (fun z => ((-1) ^ z * ‖0‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖0‖) • 0) ((s / ‖0‖) • 0)
hc : HasSum (fun a => ↑((-1) ^ a * 0 ^ (2 * a) / ↑(2 * a)!)) ↑c
⊢ (fun n => Pi.single 0 1 n) = fun a => ↑((-1) ^ a * 0 ^ (2 * a) / ↑(2 * a)!)
[PROOFSTEP]
ext (_ | n) : 1
[GOAL]
case h.e'_5.h.zero
c s : ℝ
hq : 0.re = 0
hs : HasSum (fun z => ((-1) ^ z * ‖0‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖0‖) • 0) ((s / ‖0‖) • 0)
hc : HasSum (fun a => ↑((-1) ^ a * 0 ^ (2 * a) / ↑(2 * a)!)) ↑c
⊢ Pi.single 0 1 Nat.zero = ↑((-1) ^ Nat.zero * 0 ^ (2 * Nat.zero) / ↑(2 * Nat.zero)!)
[PROOFSTEP]
rw [pow_zero, Nat.zero_eq, mul_zero, pow_zero, Nat.factorial_zero, Nat.cast_one, div_one, one_mul, Pi.single_eq_same,
  coe_one]
[GOAL]
case h.e'_5.h.succ
c s : ℝ
hq : 0.re = 0
hs : HasSum (fun z => ((-1) ^ z * ‖0‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖0‖) • 0) ((s / ‖0‖) • 0)
hc : HasSum (fun a => ↑((-1) ^ a * 0 ^ (2 * a) / ↑(2 * a)!)) ↑c
n : ℕ
⊢ Pi.single 0 1 (Nat.succ n) = ↑((-1) ^ Nat.succ n * 0 ^ (2 * Nat.succ n) / ↑(2 * Nat.succ n)!)
[PROOFSTEP]
rw [zero_pow (mul_pos two_pos (Nat.succ_pos _)), mul_zero, zero_div, Pi.single_eq_of_ne n.succ_ne_zero, coe_zero]
[GOAL]
case inr
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
⊢ HasSum (fun n => ↑(expSeries ℝ ℍ n) fun x => q) (↑c + (s / ‖q‖) • q)
[PROOFSTEP]
simp_rw [expSeries_apply_eq]
[GOAL]
case inr
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
⊢ HasSum (fun n => (↑n !)⁻¹ • q ^ n) (↑c + (s / ‖q‖) • q)
[PROOFSTEP]
have hq2 : q ^ 2 = -normSq q := sq_eq_neg_normSq.mpr hq
[GOAL]
case inr
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
⊢ HasSum (fun n => (↑n !)⁻¹ • q ^ n) (↑c + (s / ‖q‖) • q)
[PROOFSTEP]
have hqn := norm_ne_zero_iff.mpr hq0
[GOAL]
case inr
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
⊢ HasSum (fun n => (↑n !)⁻¹ • q ^ n) (↑c + (s / ‖q‖) • q)
[PROOFSTEP]
refine' HasSum.even_add_odd _ _
[GOAL]
case inr.refine'_1
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
⊢ HasSum (fun k => (↑(2 * k)!)⁻¹ • q ^ (2 * k)) ↑c
[PROOFSTEP]
convert hc using 1
[GOAL]
case h.e'_5
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
⊢ (fun k => (↑(2 * k)!)⁻¹ • q ^ (2 * k)) = fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)
[PROOFSTEP]
ext n : 1
[GOAL]
case h.e'_5.h
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
⊢ (↑(2 * n)!)⁻¹ • q ^ (2 * n) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n)!)
[PROOFSTEP]
letI k : ℝ := ↑(2 * n)!
[GOAL]
case h.e'_5.h
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n)!
⊢ (↑(2 * n)!)⁻¹ • q ^ (2 * n) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n)!)
[PROOFSTEP]
calc
  k⁻¹ • q ^ (2 * n) = k⁻¹ • (-normSq q) ^ n := by rw [pow_mul, hq2]; norm_cast
  _ = k⁻¹ • ↑((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n)) := ?_
  _ = ↑((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n) / k) := ?_
[GOAL]
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n)!
⊢ k⁻¹ • q ^ (2 * n) = ↑(k⁻¹ • (-↑normSq q) ^ n)
[PROOFSTEP]
rw [pow_mul, hq2]
[GOAL]
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n)!
⊢ k⁻¹ • (-↑(↑normSq q)) ^ n = ↑(k⁻¹ • (-↑normSq q) ^ n)
[PROOFSTEP]
norm_cast
[GOAL]
case h.e'_5.h.calc_1
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n)!
⊢ ↑(k⁻¹ • (-↑normSq q) ^ n) = k⁻¹ • ↑((-1) ^ n * ‖q‖ ^ (2 * n))
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_5.h.calc_1
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n)!
⊢ ↑(k⁻¹ • (-↑normSq q) ^ n) = k⁻¹ • ↑((-1) ^ n * ‖q‖ ^ (2 * n))
[PROOFSTEP]
rw [neg_pow, normSq_eq_norm_mul_self, pow_mul, sq]
[GOAL]
case h.e'_5.h.calc_1
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n)!
⊢ ↑(k⁻¹ • ((-1) ^ n * (‖q‖ * ‖q‖) ^ n)) = k⁻¹ • ↑((-1) ^ n * (‖q‖ * ‖q‖) ^ n)
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_5.h.calc_1
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n)!
⊢ (↑(2 * n)!)⁻¹ • ((-1) ^ n * (↑‖q‖ * ↑‖q‖) ^ n) = (↑(2 * n)!)⁻¹ • ((-1) ^ n * (↑‖q‖ * ↑‖q‖) ^ n)
[PROOFSTEP]
rfl
[GOAL]
case h.e'_5.h.calc_2
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n)!
⊢ k⁻¹ • ↑((-1) ^ n * ‖q‖ ^ (2 * n)) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / k)
[PROOFSTEP]
rw [← coe_mul_eq_smul, div_eq_mul_inv]
[GOAL]
case h.e'_5.h.calc_2
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n)!
⊢ ↑k⁻¹ * ↑((-1) ^ n * ‖q‖ ^ (2 * n)) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) * k⁻¹)
[PROOFSTEP]
norm_cast
[GOAL]
case h.e'_5.h.calc_2
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n)!
⊢ ↑(k⁻¹ * (↑(Int.negSucc 0 ^ n) * ‖q‖ ^ (2 * n))) = ↑(↑(Int.negSucc 0 ^ n) * ‖q‖ ^ (2 * n) * k⁻¹)
[PROOFSTEP]
ring_nf
[GOAL]
case inr.refine'_2
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
⊢ HasSum (fun k => (↑(2 * k + 1)!)⁻¹ • q ^ (2 * k + 1)) ((s / ‖q‖) • q)
[PROOFSTEP]
convert hs using 1
[GOAL]
case h.e'_5
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
⊢ (fun k => (↑(2 * k + 1)!)⁻¹ • q ^ (2 * k + 1)) = fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q
[PROOFSTEP]
ext n : 1
[GOAL]
case h.e'_5.h
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
⊢ (↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q
[PROOFSTEP]
let k : ℝ := ↑(2 * n + 1)!
[GOAL]
case h.e'_5.h
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n + 1)!
⊢ (↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q
[PROOFSTEP]
calc
  k⁻¹ • q ^ (2 * n + 1) = k⁻¹ • ((-normSq q) ^ n * q) :=
    by
    rw [pow_succ', pow_mul, hq2]
    norm_cast
  _ = k⁻¹ • ((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n)) • q := ?_
  _ = ((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q := ?_
[GOAL]
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ • q ^ (2 * n + 1) = k⁻¹ • (↑((-↑normSq q) ^ n) * q)
[PROOFSTEP]
rw [pow_succ', pow_mul, hq2]
[GOAL]
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ • ((-↑(↑normSq q)) ^ n * q) = k⁻¹ • (↑((-↑normSq q) ^ n) * q)
[PROOFSTEP]
norm_cast
[GOAL]
case h.e'_5.h.calc_1
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ • (↑((-↑normSq q) ^ n) * q) = k⁻¹ • ((-1) ^ n * ‖q‖ ^ (2 * n)) • q
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_5.h.calc_1.e_a
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n + 1)!
⊢ ↑((-↑normSq q) ^ n) * q = ((-1) ^ n * ‖q‖ ^ (2 * n)) • q
[PROOFSTEP]
rw [neg_pow, normSq_eq_norm_mul_self, pow_mul, sq, ← coe_mul_eq_smul]
[GOAL]
case h.e'_5.h.calc_2
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ • ((-1) ^ n * ‖q‖ ^ (2 * n)) • q = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q
[PROOFSTEP]
rw [smul_smul]
[GOAL]
case h.e'_5.h.calc_2
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n + 1)!
⊢ (k⁻¹ * ((-1) ^ n * ‖q‖ ^ (2 * n))) • q = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_5.h.calc_2.e_a
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ * ((-1) ^ n * ‖q‖ ^ (2 * n)) = (-1) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖
[PROOFSTEP]
simp_rw [pow_succ', mul_div_assoc, div_div_cancel_left' hqn]
[GOAL]
case h.e'_5.h.calc_2.e_a
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(↑normSq q)
hqn : ‖q‖ ≠ 0
n : ℕ
k : ℝ := ↑(2 * n + 1)!
⊢ (↑(2 * n + 1)!)⁻¹ * ((-1) ^ n * ‖q‖ ^ (2 * n)) = (-1) ^ n * (‖q‖ ^ (2 * n) * (↑(2 * n + 1)!)⁻¹)
[PROOFSTEP]
ring
[GOAL]
q : ℍ
hq : q.re = 0
⊢ exp ℝ q = ↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q
[PROOFSTEP]
rw [exp_eq_tsum]
[GOAL]
q : ℍ
hq : q.re = 0
⊢ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) q = ↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q
[PROOFSTEP]
refine' HasSum.tsum_eq _
[GOAL]
q : ℍ
hq : q.re = 0
⊢ HasSum (fun n => (↑n !)⁻¹ • q ^ n) (↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q)
[PROOFSTEP]
simp_rw [← expSeries_apply_eq]
[GOAL]
q : ℍ
hq : q.re = 0
⊢ HasSum (fun n => ↑(expSeries ℝ ℍ n) fun x => q) (↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q)
[PROOFSTEP]
exact hasSum_expSeries_of_imaginary hq (Real.hasSum_cos _) (Real.hasSum_sin _)
[GOAL]
q : ℍ
⊢ exp ℝ q = exp ℝ q.re • (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q)
[PROOFSTEP]
rw [← exp_of_re_eq_zero q.im q.im_re, ← coe_mul_eq_smul, ← exp_coe, ← exp_add_of_commute, re_add_im]
[GOAL]
q : ℍ
⊢ Commute (↑q.re) (im q)
[PROOFSTEP]
exact Algebra.commutes q.re (_ : ℍ[ℝ])
[GOAL]
q : ℍ
⊢ (exp ℝ q).re = exp ℝ q.re * Real.cos ‖q - ↑q.re‖
[PROOFSTEP]
simp [exp_eq]
[GOAL]
q : ℍ
⊢ im (exp ℝ q) = (exp ℝ q.re * (Real.sin ‖im q‖ / ‖im q‖)) • im q
[PROOFSTEP]
simp [exp_eq, smul_smul]
[GOAL]
q : ℍ
⊢ ↑normSq (exp ℝ q) = ↑normSq (exp ℝ q.re • (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q))
[PROOFSTEP]
rw [exp_eq]
[GOAL]
q : ℍ
⊢ ↑normSq (exp ℝ q.re • (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q)) =
    exp ℝ q.re ^ 2 * ↑normSq (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q)
[PROOFSTEP]
rw [normSq_smul]
[GOAL]
q : ℍ
⊢ exp ℝ q.re ^ 2 * ↑normSq (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q) =
    exp ℝ q.re ^ 2 * (Real.cos ‖im q‖ ^ 2 + Real.sin ‖im q‖ ^ 2)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
q : ℍ
⊢ ↑normSq (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q) = Real.cos ‖im q‖ ^ 2 + Real.sin ‖im q‖ ^ 2
[PROOFSTEP]
obtain hv | hv := eq_or_ne ‖q.im‖ 0
[GOAL]
case e_a.inl
q : ℍ
hv : ‖im q‖ = 0
⊢ ↑normSq (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q) = Real.cos ‖im q‖ ^ 2 + Real.sin ‖im q‖ ^ 2
[PROOFSTEP]
simp [hv]
[GOAL]
case e_a.inr
q : ℍ
hv : ‖im q‖ ≠ 0
⊢ ↑normSq (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q) = Real.cos ‖im q‖ ^ 2 + Real.sin ‖im q‖ ^ 2
[PROOFSTEP]
rw [normSq_add, normSq_smul, star_smul, coe_mul_eq_smul, smul_re, smul_re, star_re, im_re, smul_zero, smul_zero,
  mul_zero, add_zero, div_pow, normSq_coe, normSq_eq_norm_mul_self, ← sq, div_mul_cancel _ (pow_ne_zero _ hv)]
[GOAL]
q : ℍ
⊢ exp ℝ q.re ^ 2 * (Real.cos ‖im q‖ ^ 2 + Real.sin ‖im q‖ ^ 2) = exp ℝ q.re ^ 2
[PROOFSTEP]
rw [Real.cos_sq_add_sin_sq, mul_one]
[GOAL]
q : ℍ
⊢ ‖exp ℝ q‖ = ‖exp ℝ q.re‖
[PROOFSTEP]
rw [norm_eq_sqrt_real_inner (exp ℝ q), inner_self, normSq_exp, Real.sqrt_sq_eq_abs, Real.norm_eq_abs]


[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
⊢ ‖↑f x‖ ≤ ‖↑f 1‖ * ‖x‖
[PROOFSTEP]
conv_lhs => rw [← mul_one x]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
| ‖↑f x‖
[PROOFSTEP]
rw [← mul_one x]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
| ‖↑f x‖
[PROOFSTEP]
rw [← mul_one x]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
| ‖↑f x‖
[PROOFSTEP]
rw [← mul_one x]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
⊢ ‖↑f (x * 1)‖ ≤ ‖↑f 1‖ * ‖x‖
[PROOFSTEP]
rw [← smul_eq_mul, f.map_smul, mul_comm]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
⊢ ‖x • ↑f 1‖ ≤ ‖x‖ * ‖↑f 1‖
[PROOFSTEP]
exact norm_smul_le _ _
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
f✝ : E →ₛₗ[σ] F
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
⊢ (∀ (x : E), ‖↑f x‖ = a * ‖x‖) → ∀ (y : F), ‖↑(LinearEquiv.symm f) y‖ = a⁻¹ * ‖y‖
[PROOFSTEP]
intro hf y
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
f✝ : E →ₛₗ[σ] F
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖↑f x‖ = a * ‖x‖
y : F
⊢ ‖↑(LinearEquiv.symm f) y‖ = a⁻¹ * ‖y‖
[PROOFSTEP]
calc
  ‖f.symm y‖ = a⁻¹ * (a * ‖f.symm y‖) := by rw [← mul_assoc, inv_mul_cancel (ne_of_lt ha).symm, one_mul]
  _ = a⁻¹ * ‖f (f.symm y)‖ := by rw [hf]
  _ = a⁻¹ * ‖y‖ := by simp
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
f✝ : E →ₛₗ[σ] F
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖↑f x‖ = a * ‖x‖
y : F
⊢ ‖↑(LinearEquiv.symm f) y‖ = a⁻¹ * (a * ‖↑(LinearEquiv.symm f) y‖)
[PROOFSTEP]
rw [← mul_assoc, inv_mul_cancel (ne_of_lt ha).symm, one_mul]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
f✝ : E →ₛₗ[σ] F
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖↑f x‖ = a * ‖x‖
y : F
⊢ a⁻¹ * (a * ‖↑(LinearEquiv.symm f) y‖) = a⁻¹ * ‖↑f (↑(LinearEquiv.symm f) y)‖
[PROOFSTEP]
rw [hf]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
f✝ : E →ₛₗ[σ] F
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖↑f x‖ = a * ‖x‖
y : F
⊢ a⁻¹ * ‖↑f (↑(LinearEquiv.symm f) y)‖ = a⁻¹ * ‖y‖
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
x : E
c : 𝕜
⊢ ‖↑(LinearMap.toSpanSingleton 𝕜 E x) c‖ = ‖x‖ * ‖c‖
[PROOFSTEP]
rw [mul_comm]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
x : E
c : 𝕜
⊢ ‖↑(LinearMap.toSpanSingleton 𝕜 E x) c‖ = ‖c‖ * ‖x‖
[PROOFSTEP]
exact norm_smul _ _


[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
t : R
h : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ ‖-(↑x⁻¹ * t)‖ < 1
[PROOFSTEP]
nontriviality R using zero_lt_one
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
t : R
h : ‖t‖ < ‖↑x⁻¹‖⁻¹
✝ : Nontrivial R
⊢ ‖-(↑x⁻¹ * t)‖ < 1
[PROOFSTEP]
have hpos : 0 < ‖(↑x⁻¹ : R)‖ := Units.norm_pos x⁻¹
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
t : R
h : ‖t‖ < ‖↑x⁻¹‖⁻¹
✝ : Nontrivial R
hpos : 0 < ‖↑x⁻¹‖
⊢ ‖-(↑x⁻¹ * t)‖ < 1
[PROOFSTEP]
calc
  ‖-(↑x⁻¹ * t)‖ = ‖↑x⁻¹ * t‖ := by rw [norm_neg]
  _ ≤ ‖(↑x⁻¹ : R)‖ * ‖t‖ := (norm_mul_le (x⁻¹).1 _)
  _ < ‖(↑x⁻¹ : R)‖ * ‖(↑x⁻¹ : R)‖⁻¹ := by nlinarith only [h, hpos]
  _ = 1 := mul_inv_cancel (ne_of_gt hpos)
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
t : R
h : ‖t‖ < ‖↑x⁻¹‖⁻¹
✝ : Nontrivial R
hpos : 0 < ‖↑x⁻¹‖
⊢ ‖-(↑x⁻¹ * t)‖ = ‖↑x⁻¹ * t‖
[PROOFSTEP]
rw [norm_neg]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
t : R
h : ‖t‖ < ‖↑x⁻¹‖⁻¹
✝ : Nontrivial R
hpos : 0 < ‖↑x⁻¹‖
⊢ ‖↑x⁻¹‖ * ‖t‖ < ‖↑x⁻¹‖ * ‖↑x⁻¹‖⁻¹
[PROOFSTEP]
nlinarith only [h, hpos]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
t : R
h : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ ↑x + t = ↑(x * oneSub (-(↑x⁻¹ * t)) (_ : ‖-(↑x⁻¹ * t)‖ < 1))
[PROOFSTEP]
simp [mul_add]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
y : R
h : ‖y - ↑x‖ < ‖↑x⁻¹‖⁻¹
⊢ y = ↑(add x (y - ↑x) h)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
⊢ IsOpen {x | IsUnit x}
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
⊢ IsOpen {x | IsUnit x}
[PROOFSTEP]
apply Metric.isOpen_iff.mpr
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
⊢ ∀ (x : R), x ∈ {x | IsUnit x} → ∃ ε, ε > 0 ∧ Metric.ball x ε ⊆ {x | IsUnit x}
[PROOFSTEP]
rintro _ ⟨x, rfl⟩
[GOAL]
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
x : Rˣ
⊢ ∃ ε, ε > 0 ∧ Metric.ball (↑x) ε ⊆ {x | IsUnit x}
[PROOFSTEP]
refine' ⟨‖(↑x⁻¹ : R)‖⁻¹, _root_.inv_pos.mpr (Units.norm_pos x⁻¹), fun y hy ↦ _⟩
[GOAL]
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
x : Rˣ
y : R
hy : y ∈ Metric.ball ↑x ‖↑x⁻¹‖⁻¹
⊢ y ∈ {x | IsUnit x}
[PROOFSTEP]
rw [mem_ball_iff_norm] at hy
[GOAL]
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
x : Rˣ
y : R
hy : ‖y - ↑x‖ < ‖↑x⁻¹‖⁻¹
⊢ y ∈ {x | IsUnit x}
[PROOFSTEP]
exact (x.ofNearby y hy).isUnit
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
hx : x ∈ nonunits R
h₁ : x ∈ Metric.ball 1 1
⊢ ‖1 - x‖ < 1
[PROOFSTEP]
rwa [mem_ball_iff_norm'] at h₁
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
h : ‖t‖ < 1
⊢ inverse (1 - t) = ↑(Units.oneSub t h)⁻¹
[PROOFSTEP]
rw [← inverse_unit (Units.oneSub t h), Units.oneSub_val]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
⊢ ∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
⊢ ∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
[PROOFSTEP]
rw [Metric.eventually_nhds_iff]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
⊢ ∃ ε, ε > 0 ∧ ∀ ⦃y : R⦄, dist y 0 < ε → inverse (↑x + y) = inverse (1 + ↑x⁻¹ * y) * ↑x⁻¹
[PROOFSTEP]
refine ⟨‖(↑x⁻¹ : R)‖⁻¹, by cancel_denoms, fun t ht ↦ ?_⟩
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
⊢ ‖↑x⁻¹‖⁻¹ > 0
[PROOFSTEP]
cancel_denoms
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
⊢ ‖↑x⁻¹‖⁻¹ > 0
[PROOFSTEP]
cancel_denoms
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
t : R
ht : dist t 0 < ‖↑x⁻¹‖⁻¹
⊢ inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
[PROOFSTEP]
rw [dist_zero_right] at ht
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
t : R
ht : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
[PROOFSTEP]
rw [← x.add_val t ht, inverse_unit, Units.add, Units.copy_eq, mul_inv_rev, Units.val_mul, ← inverse_unit,
  Units.oneSub_val, sub_neg_eq_add]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
n : ℕ
t : R
ht : ‖t‖ < 1
this : Summable fun n => t ^ n
⊢ ∑ i in range n, t ^ i + ∑' (i : ℕ), t ^ (i + n) = ∑ i in range n, t ^ i + t ^ n * inverse (1 - t)
[PROOFSTEP]
simp only [inverse_one_sub t ht, add_comm _ n, pow_add, this.tsum_mul_left]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
n : ℕ
t : R
ht : ‖t‖ < 1
this : Summable fun n => t ^ n
⊢ ∑ i in range n, t ^ i + t ^ n * ∑' (i : ℕ), t ^ i = ∑ i in range n, t ^ i + t ^ n * ↑(Units.oneSub t ht)⁻¹
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
n : ℕ
t : R
ht : dist t 0 < 1
⊢ ‖t‖ < 1
[PROOFSTEP]
rwa [← dist_zero_right]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ ∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
[PROOFSTEP]
have hzero : Tendsto (-(↑x⁻¹ : R) * ·) (𝓝 0) (𝓝 0) := (mulLeft_continuous _).tendsto' _ _ <| mul_zero _
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
⊢ ∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
[PROOFSTEP]
filter_upwards [inverse_add x, hzero.eventually (inverse_one_sub_nth_order n)] with t ht ht'
[GOAL]
case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 - -↑x⁻¹ * t) = ∑ i in range n, (-↑x⁻¹ * t) ^ i + (-↑x⁻¹ * t) ^ n * inverse (1 - -↑x⁻¹ * t)
⊢ inverse (↑x + t) = (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
[PROOFSTEP]
rw [neg_mul, sub_neg_eq_add] at ht'
[GOAL]
case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 + ↑x⁻¹ * t) = ∑ i in range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
⊢ inverse (↑x + t) = (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
[PROOFSTEP]
conv_lhs => rw [ht, ht', add_mul, ← neg_mul, mul_assoc]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 + ↑x⁻¹ * t) = ∑ i in range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
| inverse (↑x + t)
[PROOFSTEP]
rw [ht, ht', add_mul, ← neg_mul, mul_assoc]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 + ↑x⁻¹ * t) = ∑ i in range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
| inverse (↑x + t)
[PROOFSTEP]
rw [ht, ht', add_mul, ← neg_mul, mul_assoc]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 + ↑x⁻¹ * t) = ∑ i in range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
| inverse (↑x + t)
[PROOFSTEP]
rw [ht, ht', add_mul, ← neg_mul, mul_assoc]
[GOAL]
case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 + ↑x⁻¹ * t) = ∑ i in range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
⊢ (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * (inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹) =
    (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
[PROOFSTEP]
rw [ht]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
⊢ (fun t => inverse (1 - t)) =O[𝓝 0] fun _t => 1
[PROOFSTEP]
simp only [IsBigO, IsBigOWith, Metric.eventually_nhds_iff]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
⊢ ∃ c ε, ε > 0 ∧ ∀ ⦃y : R⦄, dist y 0 < ε → ‖inverse (1 - y)‖ ≤ c * ‖1‖
[PROOFSTEP]
refine ⟨‖(1 : R)‖ + 1, (2 : ℝ)⁻¹, by norm_num, fun t ht ↦ ?_⟩
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
⊢ 2⁻¹ > 0
[PROOFSTEP]
norm_num
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : dist t 0 < 2⁻¹
⊢ ‖inverse (1 - t)‖ ≤ (‖1‖ + 1) * ‖1‖
[PROOFSTEP]
rw [dist_zero_right] at ht
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
⊢ ‖inverse (1 - t)‖ ≤ (‖1‖ + 1) * ‖1‖
[PROOFSTEP]
have ht' : ‖t‖ < 1 := by
  have : (2 : ℝ)⁻¹ < 1 := by cancel_denoms
  linarith
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
⊢ ‖t‖ < 1
[PROOFSTEP]
have : (2 : ℝ)⁻¹ < 1 := by cancel_denoms
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
⊢ 2⁻¹ < 1
[PROOFSTEP]
cancel_denoms
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
⊢ 2⁻¹ < 1
[PROOFSTEP]
cancel_denoms
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
this : 2⁻¹ < 1
⊢ ‖t‖ < 1
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
⊢ ‖inverse (1 - t)‖ ≤ (‖1‖ + 1) * ‖1‖
[PROOFSTEP]
simp only [inverse_one_sub t ht', norm_one, mul_one, Set.mem_setOf_eq]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
⊢ ‖↑(Units.oneSub t ht')⁻¹‖ ≤ ‖1‖ + 1
[PROOFSTEP]
change ‖∑' n : ℕ, t ^ n‖ ≤ _
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
⊢ ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ + 1
[PROOFSTEP]
have := NormedRing.tsum_geometric_of_norm_lt_1 t ht'
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹
⊢ ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ + 1
[PROOFSTEP]
have : (1 - ‖t‖)⁻¹ ≤ 2 := by
  rw [← inv_inv (2 : ℝ)]
  refine' inv_le_inv_of_le (by norm_num) _
  have : (2 : ℝ)⁻¹ + (2 : ℝ)⁻¹ = 1 := by ring
  linarith
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹
⊢ (1 - ‖t‖)⁻¹ ≤ 2
[PROOFSTEP]
rw [← inv_inv (2 : ℝ)]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹
⊢ (1 - ‖t‖)⁻¹ ≤ 2⁻¹⁻¹
[PROOFSTEP]
refine' inv_le_inv_of_le (by norm_num) _
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹
⊢ 0 < 2⁻¹
[PROOFSTEP]
norm_num
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹
⊢ 2⁻¹ ≤ 1 - ‖t‖
[PROOFSTEP]
have : (2 : ℝ)⁻¹ + (2 : ℝ)⁻¹ = 1 := by ring
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹
⊢ 2⁻¹ + 2⁻¹ = 1
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this✝ : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹
this : 2⁻¹ + 2⁻¹ = 1
⊢ 2⁻¹ ≤ 1 - ‖t‖
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this✝ : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹
this : (1 - ‖t‖)⁻¹ ≤ 2
⊢ ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ + 1
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
⊢ (fun t => inverse (↑x + t)) =O[𝓝 0] fun _t => 1
[PROOFSTEP]
refine EventuallyEq.trans_isBigO (inverse_add x) (one_mul (1 : ℝ) ▸ ?_)
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
⊢ (fun x_1 => inverse (1 + ↑x⁻¹ * x_1) * ↑x⁻¹) =O[𝓝 0] fun _t => 1 * 1
[PROOFSTEP]
simp only [← sub_neg_eq_add, ← neg_mul]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
⊢ (fun x_1 => inverse (1 - -↑x⁻¹ * x_1) * ↑x⁻¹) =O[𝓝 0] fun _t => 1 * 1
[PROOFSTEP]
have hzero : Tendsto (-(↑x⁻¹ : R) * ·) (𝓝 0) (𝓝 0) := (mulLeft_continuous _).tendsto' _ _ <| mul_zero _
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
⊢ (fun x_1 => inverse (1 - -↑x⁻¹ * x_1) * ↑x⁻¹) =O[𝓝 0] fun _t => 1 * 1
[PROOFSTEP]
exact (inverse_one_sub_norm.comp_tendsto hzero).mul (isBigO_const_const _ one_ne_zero _)
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun t => inverse (↑x + t) - (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖ ^ n
[PROOFSTEP]
refine EventuallyEq.trans_isBigO (.sub (inverse_add_nth_order x n) (.refl _ _)) ?_
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun x_1 =>
      (∑ i in range n, (-↑x⁻¹ * x_1) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * x_1) ^ n * inverse (↑x + x_1) -
        (∑ i in range n, (-↑x⁻¹ * x_1) ^ i) * ↑x⁻¹) =O[𝓝 0]
    fun t => ‖t‖ ^ n
[PROOFSTEP]
simp only [add_sub_cancel']
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun x_1 => (-↑x⁻¹ * x_1) ^ n * inverse (↑x + x_1)) =O[𝓝 0] fun t => ‖t‖ ^ n
[PROOFSTEP]
refine ((isBigO_refl _ _).norm_right.mul (inverse_add_norm x)).trans ?_
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun x_1 => ‖(-↑x⁻¹ * x_1) ^ n‖ * 1) =O[𝓝 0] fun t => ‖t‖ ^ n
[PROOFSTEP]
simp only [mul_one, isBigO_norm_left]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun x_1 => (-↑x⁻¹ * x_1) ^ n) =O[𝓝 0] fun t => ‖t‖ ^ n
[PROOFSTEP]
exact ((isBigO_refl _ _).norm_right.const_mul_left _).pow _
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
⊢ (fun t => inverse (↑x + t) - ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖
[PROOFSTEP]
simpa using inverse_add_norm_diff_nth_order x 1
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
⊢ (fun t => inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖ ^ 2
[PROOFSTEP]
convert inverse_add_norm_diff_nth_order x 2 using 2
[GOAL]
case h.e'_7.h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
x✝ : R
⊢ inverse (↑x + x✝) - ↑x⁻¹ + ↑x⁻¹ * x✝ * ↑x⁻¹ = inverse (↑x + x✝) - (∑ i in range 2, (-↑x⁻¹ * x✝) ^ i) * ↑x⁻¹
[PROOFSTEP]
simp only [sum_range_succ, sum_range_zero, zero_add, pow_zero, pow_one, add_mul, one_mul, ← sub_sub, neg_mul,
  sub_neg_eq_add]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
⊢ ContinuousAt inverse ↑x
[PROOFSTEP]
have h_is_o : (fun t : R => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] (fun _ => 1 : R → ℝ) :=
  (inverse_add_norm_diff_first_order x).trans_isLittleO (isLittleO_id_const one_ne_zero).norm_left
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
⊢ ContinuousAt inverse ↑x
[PROOFSTEP]
have h_lim : Tendsto (fun y : R => y - x) (𝓝 x) (𝓝 0) :=
  by
  refine' tendsto_zero_iff_norm_tendsto_zero.mpr _
  exact tendsto_iff_norm_tendsto_zero.mp tendsto_id
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
⊢ Tendsto (fun y => y - ↑x) (𝓝 ↑x) (𝓝 0)
[PROOFSTEP]
refine' tendsto_zero_iff_norm_tendsto_zero.mpr _
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
⊢ Tendsto (fun e => ‖e - ↑x‖) (𝓝 ↑x) (𝓝 0)
[PROOFSTEP]
exact tendsto_iff_norm_tendsto_zero.mp tendsto_id
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
h_lim : Tendsto (fun y => y - ↑x) (𝓝 ↑x) (𝓝 0)
⊢ ContinuousAt inverse ↑x
[PROOFSTEP]
rw [ContinuousAt, tendsto_iff_norm_tendsto_zero, inverse_unit]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
h_lim : Tendsto (fun y => y - ↑x) (𝓝 ↑x) (𝓝 0)
⊢ Tendsto (fun e => ‖inverse e - ↑x⁻¹‖) (𝓝 ↑x) (𝓝 0)
[PROOFSTEP]
simpa [(· ∘ ·)] using h_is_o.norm_left.tendsto_div_nhds_zero.comp h_lim
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
I : Ideal R
x : R
hxI : x ∈ I
hx : ‖1 - x‖ < 1
u : Rˣ := Units.oneSub (1 - x) hx
⊢ 1 ∈ I
[PROOFSTEP]
simpa only [show u.inv * x = 1 by simp] using I.mul_mem_left u.inv hxI
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
I : Ideal R
x : R
hxI : x ∈ I
hx : ‖1 - x‖ < 1
u : Rˣ := Units.oneSub (1 - x) hx
⊢ u.inv * x = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
I : Ideal R
hI : I ≠ ⊤
⊢ Ideal.closure I ≠ ⊤
[PROOFSTEP]
have h := closure_minimal (coe_subset_nonunits hI) nonunits.isClosed
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
I : Ideal R
hI : I ≠ ⊤
h : closure ↑I ⊆ nonunits R
⊢ Ideal.closure I ≠ ⊤
[PROOFSTEP]
simpa only [I.closure.eq_top_iff_one, Ne.def] using mt (@h 1) one_not_mem_nonunits


[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
src✝ : Module 𝕜 (Completion E) := instModule
c : 𝕜
x : Completion E
y : E
⊢ ‖c • ↑E y‖ ≤ ‖c‖ * ‖↑E y‖
[PROOFSTEP]
simp only [← coe_smul, norm_coe, norm_smul, le_rfl]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : Completion A
⊢ dist x y = ‖x - y‖
[PROOFSTEP]
refine Completion.induction_on₂ x y ?_ ?_
[GOAL]
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : Completion A
⊢ IsClosed {x | dist x.fst x.snd = ‖x.fst - x.snd‖}
[PROOFSTEP]
clear x y
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : Completion A
⊢ ∀ (a b : A), dist (↑A a) (↑A b) = ‖↑A a - ↑A b‖
[PROOFSTEP]
clear x y
[GOAL]
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
⊢ IsClosed {x | dist x.fst x.snd = ‖x.fst - x.snd‖}
[PROOFSTEP]
refine' isClosed_eq (Completion.uniformContinuous_extension₂ _).continuous _
[GOAL]
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
⊢ Continuous fun x => ‖x.fst - x.snd‖
[PROOFSTEP]
exact Continuous.comp Completion.continuous_extension continuous_sub
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
⊢ ∀ (a b : A), dist (↑A a) (↑A b) = ‖↑A a - ↑A b‖
[PROOFSTEP]
intro x y
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : A
⊢ dist (↑A x) (↑A y) = ‖↑A x - ↑A y‖
[PROOFSTEP]
rw [← Completion.coe_sub, norm_coe, Completion.dist_eq, dist_eq_norm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : Completion A
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖
[PROOFSTEP]
refine Completion.induction_on₂ x y ?_ ?_
[GOAL]
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : Completion A
⊢ IsClosed {x | ‖x.fst * x.snd‖ ≤ ‖x.fst‖ * ‖x.snd‖}
[PROOFSTEP]
clear x y
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : Completion A
⊢ ∀ (a b : A), ‖↑A a * ↑A b‖ ≤ ‖↑A a‖ * ‖↑A b‖
[PROOFSTEP]
clear x y
[GOAL]
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
⊢ IsClosed {x | ‖x.fst * x.snd‖ ≤ ‖x.fst‖ * ‖x.snd‖}
[PROOFSTEP]
exact
  isClosed_le (Continuous.comp continuous_norm continuous_mul)
    (Continuous.comp _root_.continuous_mul (Continuous.prod_map continuous_norm continuous_norm))
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
⊢ ∀ (a b : A), ‖↑A a * ↑A b‖ ≤ ‖↑A a‖ * ‖↑A b‖
[PROOFSTEP]
intro x y
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : A
⊢ ‖↑A x * ↑A y‖ ≤ ‖↑A x‖ * ‖↑A y‖
[PROOFSTEP]
simp only [← coe_mul, norm_coe]
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : A
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖
[PROOFSTEP]
exact norm_mul_le x y
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
A : Type u_3
inst✝² : SeminormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : UniformContinuousConstSMul 𝕜 A
src✝ : Algebra 𝕜 (Completion A) := algebra A 𝕜
r : 𝕜
x : Completion A
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
[PROOFSTEP]
refine Completion.induction_on x ?_ ?_
[GOAL]
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
A : Type u_3
inst✝² : SeminormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : UniformContinuousConstSMul 𝕜 A
src✝ : Algebra 𝕜 (Completion A) := algebra A 𝕜
r : 𝕜
x : Completion A
⊢ IsClosed {a | ‖r • a‖ ≤ ‖r‖ * ‖a‖}
[PROOFSTEP]
clear x
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
A : Type u_3
inst✝² : SeminormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : UniformContinuousConstSMul 𝕜 A
src✝ : Algebra 𝕜 (Completion A) := algebra A 𝕜
r : 𝕜
x : Completion A
⊢ ∀ (a : A), ‖r • ↑A a‖ ≤ ‖r‖ * ‖↑A a‖
[PROOFSTEP]
clear x
[GOAL]
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
A : Type u_3
inst✝² : SeminormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : UniformContinuousConstSMul 𝕜 A
src✝ : Algebra 𝕜 (Completion A) := algebra A 𝕜
r : 𝕜
⊢ IsClosed {a | ‖r • a‖ ≤ ‖r‖ * ‖a‖}
[PROOFSTEP]
exact
  isClosed_le (Continuous.comp continuous_norm (continuous_const_smul r))
    (Continuous.comp (continuous_mul_left _) continuous_norm)
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
A : Type u_3
inst✝² : SeminormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : UniformContinuousConstSMul 𝕜 A
src✝ : Algebra 𝕜 (Completion A) := algebra A 𝕜
r : 𝕜
⊢ ∀ (a : A), ‖r • ↑A a‖ ≤ ‖r‖ * ‖↑A a‖
[PROOFSTEP]
intro x
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
A : Type u_3
inst✝² : SeminormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : UniformContinuousConstSMul 𝕜 A
src✝ : Algebra 𝕜 (Completion A) := algebra A 𝕜
r : 𝕜
x : A
⊢ ‖r • ↑A x‖ ≤ ‖r‖ * ‖↑A x‖
[PROOFSTEP]
simp only [← coe_smul, norm_coe]
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
A : Type u_3
inst✝² : SeminormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : UniformContinuousConstSMul 𝕜 A
src✝ : Algebra 𝕜 (Completion A) := algebra A 𝕜
r : 𝕜
x : A
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
[PROOFSTEP]
exact norm_smul_le r x


[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜' E
r : ℝ
c : ↑(closedBall 0 1)
x : ↑(ball 0 r)
⊢ ‖↑c • ↑x‖ < r
[PROOFSTEP]
simpa only [norm_smul, one_mul] using
  mul_lt_mul' (mem_closedBall_zero_iff.1 c.2) (mem_ball_zero_iff.1 x.2) (norm_nonneg _) one_pos
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜' E
r : ℝ
c : ↑(closedBall 0 1)
x : ↑(closedBall 0 r)
⊢ ‖↑c • ↑x‖ ≤ r
[PROOFSTEP]
simpa only [norm_smul, one_mul] using
  mul_le_mul (mem_closedBall_zero_iff.1 c.2) (mem_closedBall_zero_iff.1 x.2) (norm_nonneg _) zero_le_one
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜' E
r : ℝ
c : ↑(sphere 0 1)
x : ↑(sphere 0 r)
⊢ ‖↑c • ↑x‖ = r
[PROOFSTEP]
rw [norm_smul, mem_sphere_zero_iff_norm.1 c.coe_prop, mem_sphere_zero_iff_norm.1 x.coe_prop, one_mul]
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedField 𝕜'
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' E
r✝ : ℝ
inst✝ : CharZero 𝕜
r : ℝ
hr : r ≠ 0
x : ↑(sphere 0 r)
h : x = -x
⊢ ↑x = -↑x
[PROOFSTEP]
conv_lhs => rw [h]
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedField 𝕜'
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' E
r✝ : ℝ
inst✝ : CharZero 𝕜
r : ℝ
hr : r ≠ 0
x : ↑(sphere 0 r)
h : x = -x
| ↑x
[PROOFSTEP]
rw [h]
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedField 𝕜'
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' E
r✝ : ℝ
inst✝ : CharZero 𝕜
r : ℝ
hr : r ≠ 0
x : ↑(sphere 0 r)
h : x = -x
| ↑x
[PROOFSTEP]
rw [h]
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedField 𝕜'
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' E
r✝ : ℝ
inst✝ : CharZero 𝕜
r : ℝ
hr : r ≠ 0
x : ↑(sphere 0 r)
h : x = -x
| ↑x
[PROOFSTEP]
rw [h]


[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
⊢ F →ₗ[𝕜] 𝕜
[PROOFSTEP]
let fc : F → 𝕜 := fun x => (fr x : 𝕜) - (I : 𝕜) * fr ((I : 𝕜) • x)
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
⊢ F →ₗ[𝕜] 𝕜
[PROOFSTEP]
have add : ∀ x y : F, fc (x + y) = fc x + fc y := by
  intro x y
  simp only [smul_add, LinearMap.map_add, ofReal_add]
  rw [mul_add]
  abel
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
⊢ ∀ (x y : F), fc (x + y) = fc x + fc y
[PROOFSTEP]
intro x y
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
x y : F
⊢ fc (x + y) = fc x + fc y
[PROOFSTEP]
simp only [smul_add, LinearMap.map_add, ofReal_add]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
x y : F
⊢ ↑(↑fr x) + ↑(↑fr y) - I * (↑(↑fr (I • x)) + ↑(↑fr (I • y))) =
    ↑(↑fr x) - I * ↑(↑fr (I • x)) + (↑(↑fr y) - I * ↑(↑fr (I • y)))
[PROOFSTEP]
rw [mul_add]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
x y : F
⊢ ↑(↑fr x) + ↑(↑fr y) - (I * ↑(↑fr (I • x)) + I * ↑(↑fr (I • y))) =
    ↑(↑fr x) - I * ↑(↑fr (I • x)) + (↑(↑fr y) - I * ↑(↑fr (I • y)))
[PROOFSTEP]
abel
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
x y : F
⊢ ↑(↑fr x) + ↑(↑fr y) - (I * ↑(↑fr (I • x)) + I * ↑(↑fr (I • y))) =
    ↑(↑fr x) - I * ↑(↑fr (I • x)) + (↑(↑fr y) - I * ↑(↑fr (I • y)))
[PROOFSTEP]
abel
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
⊢ F →ₗ[𝕜] 𝕜
[PROOFSTEP]
have A : ∀ (c : ℝ) (x : F), (fr ((c : 𝕜) • x) : 𝕜) = (c : 𝕜) * (fr x : 𝕜) :=
  by
  intro c x
  rw [← ofReal_mul]
  congr 1
  rw [IsROrC.ofReal_alg, smul_assoc, fr.map_smul, Algebra.id.smul_eq_mul, one_smul]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
⊢ ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
[PROOFSTEP]
intro c x
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
c : ℝ
x : F
⊢ ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
[PROOFSTEP]
rw [← ofReal_mul]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
c : ℝ
x : F
⊢ ↑(↑fr (↑c • x)) = ↑(c * ↑fr x)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
c : ℝ
x : F
⊢ ↑fr (↑c • x) = c * ↑fr x
[PROOFSTEP]
rw [IsROrC.ofReal_alg, smul_assoc, fr.map_smul, Algebra.id.smul_eq_mul, one_smul]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
⊢ F →ₗ[𝕜] 𝕜
[PROOFSTEP]
have smul_ℝ : ∀ (c : ℝ) (x : F), fc ((c : 𝕜) • x) = (c : 𝕜) * fc x :=
  by
  intro c x
  dsimp only
  rw [A c x, smul_smul, mul_comm I (c : 𝕜), ← smul_smul, A, mul_sub]
  ring
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
⊢ ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
[PROOFSTEP]
intro c x
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
c : ℝ
x : F
⊢ fc (↑c • x) = ↑c * fc x
[PROOFSTEP]
dsimp only
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
c : ℝ
x : F
⊢ ↑(↑fr (↑c • x)) - I * ↑(↑fr (I • ↑c • x)) = ↑c * (↑(↑fr x) - I * ↑(↑fr (I • x)))
[PROOFSTEP]
rw [A c x, smul_smul, mul_comm I (c : 𝕜), ← smul_smul, A, mul_sub]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
c : ℝ
x : F
⊢ ↑c * ↑(↑fr x) - I * (↑c * ↑(↑fr (I • x))) = ↑c * ↑(↑fr x) - ↑c * (I * ↑(↑fr (I • x)))
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
⊢ F →ₗ[𝕜] 𝕜
[PROOFSTEP]
have smul_I : ∀ x : F, fc ((I : 𝕜) • x) = (I : 𝕜) * fc x :=
  by
  intro x
  dsimp only
  cases' @I_mul_I_ax 𝕜 _ with h h
  · simp [h]
  rw [mul_sub, ← mul_assoc, smul_smul, h]
  simp only [neg_mul, LinearMap.map_neg, one_mul, one_smul, mul_neg, ofReal_neg, neg_smul, sub_neg_eq_add, add_comm]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
⊢ ∀ (x : F), fc (I • x) = I * fc x
[PROOFSTEP]
intro x
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
x : F
⊢ fc (I • x) = I * fc x
[PROOFSTEP]
dsimp only
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
x : F
⊢ ↑(↑fr (I • x)) - I * ↑(↑fr (I • I • x)) = I * (↑(↑fr x) - I * ↑(↑fr (I • x)))
[PROOFSTEP]
cases' @I_mul_I_ax 𝕜 _ with h h
[GOAL]
case inl
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
x : F
h : I = 0
⊢ ↑(↑fr (I • x)) - I * ↑(↑fr (I • I • x)) = I * (↑(↑fr x) - I * ↑(↑fr (I • x)))
[PROOFSTEP]
simp [h]
[GOAL]
case inr
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
x : F
h : I * I = -1
⊢ ↑(↑fr (I • x)) - I * ↑(↑fr (I • I • x)) = I * (↑(↑fr x) - I * ↑(↑fr (I • x)))
[PROOFSTEP]
rw [mul_sub, ← mul_assoc, smul_smul, h]
[GOAL]
case inr
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
x : F
h : I * I = -1
⊢ ↑(↑fr (I • x)) - I * ↑(↑fr (-1 • x)) = I * ↑(↑fr x) - -1 * ↑(↑fr (I • x))
[PROOFSTEP]
simp only [neg_mul, LinearMap.map_neg, one_mul, one_smul, mul_neg, ofReal_neg, neg_smul, sub_neg_eq_add, add_comm]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
smul_I : ∀ (x : F), fc (I • x) = I * fc x
⊢ F →ₗ[𝕜] 𝕜
[PROOFSTEP]
have smul_𝕜 : ∀ (c : 𝕜) (x : F), fc (c • x) = c • fc x :=
  by
  intro c x
  rw [← re_add_im c, add_smul, add_smul, add, smul_ℝ, ← smul_smul, smul_ℝ, smul_I, ← mul_assoc]
  rfl
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
smul_I : ∀ (x : F), fc (I • x) = I * fc x
⊢ ∀ (c : 𝕜) (x : F), fc (c • x) = c • fc x
[PROOFSTEP]
intro c x
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
smul_I : ∀ (x : F), fc (I • x) = I * fc x
c : 𝕜
x : F
⊢ fc (c • x) = c • fc x
[PROOFSTEP]
rw [← re_add_im c, add_smul, add_smul, add, smul_ℝ, ← smul_smul, smul_ℝ, smul_I, ← mul_assoc]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
smul_I : ∀ (x : F), fc (I • x) = I * fc x
c : 𝕜
x : F
⊢ ↑(↑re c) * fc x + ↑(↑im c) * I * fc x = ↑(↑re c) • fc x + (↑(↑im c) * I) • fc x
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
smul_I : ∀ (x : F), fc (I • x) = I * fc x
smul_𝕜 : ∀ (c : 𝕜) (x : F), fc (c • x) = c • fc x
⊢ F →ₗ[𝕜] 𝕜
[PROOFSTEP]
exact
  { toFun := fc
    map_add' := add
    map_smul' := smul_𝕜 }
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
x : F
⊢ ↑re (↑(extendTo𝕜' fr) x) = ↑fr x
[PROOFSTEP]
simp only [extendTo𝕜'_apply, map_sub, zero_mul, mul_zero, sub_zero, isROrC_simps]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
x : F
⊢ ‖↑(extendTo𝕜' fr) x‖ ^ 2 = ↑re (↑(starRingEnd ((fun x => 𝕜) x)) (↑(extendTo𝕜' fr) x) * ↑(extendTo𝕜' fr) x)
[PROOFSTEP]
rw [IsROrC.conj_mul, normSq_eq_def', ofReal_re]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
x : F
⊢ ↑re (↑(starRingEnd ((fun x => 𝕜) x)) (↑(extendTo𝕜' fr) x) * ↑(extendTo𝕜' fr) x) =
    ↑fr (↑(starRingEnd ((fun x => 𝕜) x)) (↑(extendTo𝕜' fr) x) • x)
[PROOFSTEP]
rw [← smul_eq_mul, ← map_smul, extendTo𝕜'_apply_re]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
⊢ ‖↑(LinearMap.extendTo𝕜' ↑fr) x‖ ≤ ‖fr‖ * ‖x‖
[PROOFSTEP]
set lm : F →ₗ[𝕜] 𝕜 := fr.toLinearMap.extendTo𝕜'
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
⊢ ‖↑lm x‖ ≤ ‖fr‖ * ‖x‖
[PROOFSTEP]
by_cases h : lm x = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ↑lm x = 0
⊢ ‖↑lm x‖ ≤ ‖fr‖ * ‖x‖
[PROOFSTEP]
rw [h, norm_zero]
[GOAL]
case pos
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ↑lm x = 0
⊢ 0 ≤ ‖fr‖ * ‖x‖
[PROOFSTEP]
apply mul_nonneg
[GOAL]
case pos.ha
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ↑lm x = 0
⊢ 0 ≤ ‖fr‖
[PROOFSTEP]
exact norm_nonneg _
[GOAL]
case pos.hb
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ↑lm x = 0
⊢ 0 ≤ ‖x‖
[PROOFSTEP]
exact norm_nonneg _
[GOAL]
case neg
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ¬↑lm x = 0
⊢ ‖↑lm x‖ ≤ ‖fr‖ * ‖x‖
[PROOFSTEP]
rw [← mul_le_mul_left (norm_pos_iff.2 h), ← sq]
[GOAL]
case neg
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ¬↑lm x = 0
⊢ ‖↑lm x‖ ^ 2 ≤ ‖↑lm x‖ * (‖fr‖ * ‖x‖)
[PROOFSTEP]
calc
  ‖lm x‖ ^ 2 = fr (conj (lm x : 𝕜) • x) := fr.toLinearMap.norm_extendTo𝕜'_apply_sq x
  _ ≤ ‖fr (conj (lm x : 𝕜) • x)‖ := (le_abs_self _)
  _ ≤ ‖fr‖ * ‖conj (lm x : 𝕜) • x‖ := (le_op_norm _ _)
  _ = ‖(lm x : 𝕜)‖ * (‖fr‖ * ‖x‖) := by rw [norm_smul, norm_conj, mul_left_comm]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ¬↑lm x = 0
⊢ ‖fr‖ * ‖↑(starRingEnd ((fun x => 𝕜) x)) (↑lm x) • x‖ = ‖↑lm x‖ * (‖fr‖ * ‖x‖)
[PROOFSTEP]
rw [norm_smul, norm_conj, mul_left_comm]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ NormedSpace 𝕜 (RestrictScalars ℝ 𝕜 F)
[PROOFSTEP]
unfold RestrictScalars
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ NormedSpace 𝕜 F
[PROOFSTEP]
infer_instance