[GOAL]
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
⊢ spectrum 𝕜 ↑u ⊆ Metric.sphere 0 1
[PROOFSTEP]
nontriviality E
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
✝ : Nontrivial E
⊢ spectrum 𝕜 ↑u ⊆ Metric.sphere 0 1
[PROOFSTEP]
refine' fun k hk => mem_sphere_zero_iff_norm.mpr (le_antisymm _ _)
[GOAL]
case refine'_1
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
✝ : Nontrivial E
k : 𝕜
hk : k ∈ spectrum 𝕜 ↑u
⊢ ‖k‖ ≤ 1
[PROOFSTEP]
simpa only [CstarRing.norm_coe_unitary u] using norm_le_norm_of_mem hk
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
✝ : Nontrivial E
k : 𝕜
hk : k ∈ spectrum 𝕜 ↑u
⊢ 1 ≤ ‖k‖
[PROOFSTEP]
rw [← unitary.toUnits_apply_val u] at hk
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
✝ : Nontrivial E
k : 𝕜
hk : k ∈ spectrum 𝕜 ↑(↑toUnits u)
⊢ 1 ≤ ‖k‖
[PROOFSTEP]
have hnk := ne_zero_of_mem_of_unit hk
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
✝ : Nontrivial E
k : 𝕜
hk : k ∈ spectrum 𝕜 ↑(↑toUnits u)
hnk : k ≠ 0
⊢ 1 ≤ ‖k‖
[PROOFSTEP]
rw [← inv_inv (unitary.toUnits u), ← spectrum.map_inv, Set.mem_inv] at hk
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
✝ : Nontrivial E
k : 𝕜
hk : k⁻¹ ∈ spectrum 𝕜 ↑(↑toUnits u)⁻¹
hnk : k ≠ 0
⊢ 1 ≤ ‖k‖
[PROOFSTEP]
have : ‖k‖⁻¹ ≤ ‖(↑(unitary.toUnits u)⁻¹ : E)‖ := by simpa only [norm_inv] using norm_le_norm_of_mem hk
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
✝ : Nontrivial E
k : 𝕜
hk : k⁻¹ ∈ spectrum 𝕜 ↑(↑toUnits u)⁻¹
hnk : k ≠ 0
⊢ ‖k‖⁻¹ ≤ ‖↑(↑toUnits u)⁻¹‖
[PROOFSTEP]
simpa only [norm_inv] using norm_le_norm_of_mem hk
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
✝ : Nontrivial E
k : 𝕜
hk : k⁻¹ ∈ spectrum 𝕜 ↑(↑toUnits u)⁻¹
hnk : k ≠ 0
this : ‖k‖⁻¹ ≤ ‖↑(↑toUnits u)⁻¹‖
⊢ 1 ≤ ‖k‖
[PROOFSTEP]
simpa [← Units.inv_eq_val_inv] using inv_le_of_inv_le (norm_pos_iff.mpr hnk) this
[GOAL]
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra ℂ A
inst✝² : CompleteSpace A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : A
ha : IsSelfAdjoint a
⊢ spectralRadius ℂ a = ↑‖a‖₊
[PROOFSTEP]
have hconst : Tendsto (fun _n : ℕ => (‖a‖₊ : ℝ≥0∞)) atTop _ := tendsto_const_nhds
[GOAL]
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra ℂ A
inst✝² : CompleteSpace A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
⊢ spectralRadius ℂ a = ↑‖a‖₊
[PROOFSTEP]
refine' tendsto_nhds_unique _ hconst
[GOAL]
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra ℂ A
inst✝² : CompleteSpace A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
⊢ Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 (spectralRadius ℂ a))
[PROOFSTEP]
convert
  (spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a : A)).comp
    (Nat.tendsto_pow_atTop_atTop_of_one_lt one_lt_two) using
  1
[GOAL]
case h.e'_3
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra ℂ A
inst✝² : CompleteSpace A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
⊢ (fun _n => ↑‖a‖₊) = (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) ∘ fun n => 2 ^ n
[PROOFSTEP]
refine' funext fun n => _
[GOAL]
case h.e'_3
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra ℂ A
inst✝² : CompleteSpace A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
n : ℕ
⊢ ↑‖a‖₊ = ((fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) ∘ fun n => 2 ^ n) n
[PROOFSTEP]
rw [Function.comp_apply, ha.nnnorm_pow_two_pow, ENNReal.coe_pow, ← rpow_nat_cast, ← rpow_mul]
[GOAL]
case h.e'_3
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra ℂ A
inst✝² : CompleteSpace A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
n : ℕ
⊢ ↑‖a‖₊ = ↑‖a‖₊ ^ (↑(2 ^ n) * (1 / ↑(2 ^ n)))
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
a : A
inst✝ : IsStarNormal a
⊢ spectralRadius ℂ a = ↑‖a‖₊
[PROOFSTEP]
refine' (ENNReal.pow_strictMono two_ne_zero).injective _
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
a : A
inst✝ : IsStarNormal a
⊢ spectralRadius ℂ a ^ 2 = ↑‖a‖₊ ^ 2
[PROOFSTEP]
have heq :
  (fun n : ℕ => (‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ)) =
    (fun x => x ^ 2) ∘ fun n : ℕ => (‖a ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ) :=
  by
  funext n
  rw [Function.comp_apply, ← rpow_nat_cast, ← rpow_mul, mul_comm, rpow_mul, rpow_nat_cast, ← coe_pow, sq, ←
    nnnorm_star_mul_self, Commute.mul_pow (star_comm_self' a), star_pow]
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
a : A
inst✝ : IsStarNormal a
⊢ (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x => x ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)
[PROOFSTEP]
funext n
[GOAL]
case h
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
a : A
inst✝ : IsStarNormal a
n : ℕ
⊢ ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n) = ((fun x => x ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) n
[PROOFSTEP]
rw [Function.comp_apply, ← rpow_nat_cast, ← rpow_mul, mul_comm, rpow_mul, rpow_nat_cast, ← coe_pow, sq, ←
  nnnorm_star_mul_self, Commute.mul_pow (star_comm_self' a), star_pow]
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
a : A
inst✝ : IsStarNormal a
heq : (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x => x ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)
⊢ spectralRadius ℂ a ^ 2 = ↑‖a‖₊ ^ 2
[PROOFSTEP]
have h₂ :=
  ((ENNReal.continuous_pow 2).tendsto (spectralRadius ℂ a)).comp
    (spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius a)
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
a : A
inst✝ : IsStarNormal a
heq : (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x => x ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)
h₂ : Tendsto ((fun a => a ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) atTop (𝓝 (spectralRadius ℂ a ^ 2))
⊢ spectralRadius ℂ a ^ 2 = ↑‖a‖₊ ^ 2
[PROOFSTEP]
rw [← heq] at h₂
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
a : A
inst✝ : IsStarNormal a
heq : (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x => x ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)
h₂ : Tendsto (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) atTop (𝓝 (spectralRadius ℂ a ^ 2))
⊢ spectralRadius ℂ a ^ 2 = ↑‖a‖₊ ^ 2
[PROOFSTEP]
convert tendsto_nhds_unique h₂ (pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a⋆ * a))
[GOAL]
case h.e'_3
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
a : A
inst✝ : IsStarNormal a
heq : (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x => x ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)
h₂ : Tendsto (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) atTop (𝓝 (spectralRadius ℂ a ^ 2))
⊢ ↑‖a‖₊ ^ 2 = spectralRadius ℂ (a⋆ * a)
[PROOFSTEP]
rw [(IsSelfAdjoint.star_mul_self a).spectralRadius_eq_nnnorm, sq, nnnorm_star_mul_self, coe_mul]
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ spectrum ℂ a
⊢ z = ↑z.re
[PROOFSTEP]
have hu := exp_mem_unitary_of_mem_skewAdjoint ℂ (ha.smul_mem_skewAdjoint conj_I)
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ spectrum ℂ a
hu : _root_.exp ℂ (I • a) ∈ unitary A
⊢ z = ↑z.re
[PROOFSTEP]
let Iu := Units.mk0 I I_ne_zero
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ spectrum ℂ a
hu : _root_.exp ℂ (I • a) ∈ unitary A
Iu : ℂˣ := Units.mk0 I I_ne_zero
⊢ z = ↑z.re
[PROOFSTEP]
have : _root_.exp ℂ (I • z) ∈ spectrum ℂ (_root_.exp ℂ (I • a)) := by
  simpa only [Units.smul_def, Units.val_mk0] using spectrum.exp_mem_exp (Iu • a) (smul_mem_smul_iff.mpr hz)
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ spectrum ℂ a
hu : _root_.exp ℂ (I • a) ∈ unitary A
Iu : ℂˣ := Units.mk0 I I_ne_zero
⊢ _root_.exp ℂ (I • z) ∈ spectrum ℂ (_root_.exp ℂ (I • a))
[PROOFSTEP]
simpa only [Units.smul_def, Units.val_mk0] using spectrum.exp_mem_exp (Iu • a) (smul_mem_smul_iff.mpr hz)
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ spectrum ℂ a
hu : _root_.exp ℂ (I • a) ∈ unitary A
Iu : ℂˣ := Units.mk0 I I_ne_zero
this : _root_.exp ℂ (I • z) ∈ spectrum ℂ (_root_.exp ℂ (I • a))
⊢ z = ↑z.re
[PROOFSTEP]
exact
  Complex.ext (ofReal_re _) <| by
    simpa only [← Complex.exp_eq_exp_ℂ, mem_sphere_zero_iff_norm, norm_eq_abs, abs_exp, Real.exp_eq_one_iff,
      smul_eq_mul, I_mul, neg_eq_zero] using spectrum.subset_circle_of_unitary hu this
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ spectrum ℂ a
hu : _root_.exp ℂ (I • a) ∈ unitary A
Iu : ℂˣ := Units.mk0 I I_ne_zero
this : _root_.exp ℂ (I • z) ∈ spectrum ℂ (_root_.exp ℂ (I • a))
⊢ z.im = (↑z.re).im
[PROOFSTEP]
simpa only [← Complex.exp_eq_exp_ℂ, mem_sphere_zero_iff_norm, norm_eq_abs, abs_exp, Real.exp_eq_one_iff, smul_eq_mul,
  I_mul, neg_eq_zero] using spectrum.subset_circle_of_unitary hu this
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
⊢ z ∈ ofReal' ∘ re '' spectrum ℂ a → z ∈ spectrum ℂ a
[PROOFSTEP]
rintro ⟨z, hz, rfl⟩
[GOAL]
case intro.intro
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ spectrum ℂ a
⊢ (ofReal' ∘ re) z ∈ spectrum ℂ a
[PROOFSTEP]
simpa only [(ha.mem_spectrum_eq_re hz).symm, Function.comp_apply] using hz
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : NormedRing A
inst✝⁸ : NormedAlgebra ℂ A
inst✝⁷ : CompleteSpace A
inst✝⁶ : StarRing A
inst✝⁵ : CstarRing A
inst✝⁴ : NormedRing B
inst✝³ : NormedAlgebra ℂ B
inst✝² : CompleteSpace B
inst✝¹ : StarRing B
inst✝ : CstarRing B
hF : StarAlgHomClass F ℂ A B
φ : F
a : A
⊢ ‖↑φ a‖₊ ≤ ‖a‖₊
[PROOFSTEP]
suffices ∀ s : A, IsSelfAdjoint s → ‖φ s‖₊ ≤ ‖s‖₊ by
  exact
    nonneg_le_nonneg_of_sq_le_sq zero_le' <| by
      simpa only [nnnorm_star_mul_self, map_star, map_mul] using this _ (IsSelfAdjoint.star_mul_self a)
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : NormedRing A
inst✝⁸ : NormedAlgebra ℂ A
inst✝⁷ : CompleteSpace A
inst✝⁶ : StarRing A
inst✝⁵ : CstarRing A
inst✝⁴ : NormedRing B
inst✝³ : NormedAlgebra ℂ B
inst✝² : CompleteSpace B
inst✝¹ : StarRing B
inst✝ : CstarRing B
hF : StarAlgHomClass F ℂ A B
φ : F
a : A
this : ∀ (s : A), IsSelfAdjoint s → ‖↑φ s‖₊ ≤ ‖s‖₊
⊢ ‖↑φ a‖₊ ≤ ‖a‖₊
[PROOFSTEP]
exact
  nonneg_le_nonneg_of_sq_le_sq zero_le' <| by
    simpa only [nnnorm_star_mul_self, map_star, map_mul] using this _ (IsSelfAdjoint.star_mul_self a)
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : NormedRing A
inst✝⁸ : NormedAlgebra ℂ A
inst✝⁷ : CompleteSpace A
inst✝⁶ : StarRing A
inst✝⁵ : CstarRing A
inst✝⁴ : NormedRing B
inst✝³ : NormedAlgebra ℂ B
inst✝² : CompleteSpace B
inst✝¹ : StarRing B
inst✝ : CstarRing B
hF : StarAlgHomClass F ℂ A B
φ : F
a : A
this : ∀ (s : A), IsSelfAdjoint s → ‖↑φ s‖₊ ≤ ‖s‖₊
⊢ ‖↑φ a‖₊ * ‖↑φ a‖₊ ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
simpa only [nnnorm_star_mul_self, map_star, map_mul] using this _ (IsSelfAdjoint.star_mul_self a)
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : NormedRing A
inst✝⁸ : NormedAlgebra ℂ A
inst✝⁷ : CompleteSpace A
inst✝⁶ : StarRing A
inst✝⁵ : CstarRing A
inst✝⁴ : NormedRing B
inst✝³ : NormedAlgebra ℂ B
inst✝² : CompleteSpace B
inst✝¹ : StarRing B
inst✝ : CstarRing B
hF : StarAlgHomClass F ℂ A B
φ : F
a : A
⊢ ∀ (s : A), IsSelfAdjoint s → ‖↑φ s‖₊ ≤ ‖s‖₊
[PROOFSTEP]
intro s hs
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : NormedRing A
inst✝⁸ : NormedAlgebra ℂ A
inst✝⁷ : CompleteSpace A
inst✝⁶ : StarRing A
inst✝⁵ : CstarRing A
inst✝⁴ : NormedRing B
inst✝³ : NormedAlgebra ℂ B
inst✝² : CompleteSpace B
inst✝¹ : StarRing B
inst✝ : CstarRing B
hF : StarAlgHomClass F ℂ A B
φ : F
a s : A
hs : IsSelfAdjoint s
⊢ ‖↑φ s‖₊ ≤ ‖s‖₊
[PROOFSTEP]
simpa only [hs.spectralRadius_eq_nnnorm, (hs.starHom_apply φ).spectralRadius_eq_nnnorm, coe_le_coe] using
  show spectralRadius ℂ (φ s) ≤ spectralRadius ℂ s from iSup_le_iSup_of_subset (AlgHom.spectrum_apply_subset φ s)
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : NormedRing A
inst✝⁸ : NormedAlgebra ℂ A
inst✝⁷ : CompleteSpace A
inst✝⁶ : StarRing A
inst✝⁵ : CstarRing A
inst✝⁴ : NormedRing B
inst✝³ : NormedAlgebra ℂ B
inst✝² : CompleteSpace B
inst✝¹ : StarRing B
inst✝ : CstarRing B
hF : StarAlgHomClass F ℂ A B
φ✝ : F
src✝ : LinearMapClass F ℂ A B := AlgHomClass.linearMapClass
φ : F
⊢ ∀ (x : A), ‖↑φ x‖ ≤ 1 * ‖x‖
[PROOFSTEP]
simpa only [one_mul] using nnnorm_apply_le φ
[GOAL]
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
⊢ ↑φ a⋆ = (↑φ a)⋆
[PROOFSTEP]
suffices hsa : ∀ s : selfAdjoint A, (φ s)⋆ = φ s
[GOAL]
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
hsa : ∀ (s : { x // x ∈ selfAdjoint A }), (↑φ ↑s)⋆ = ↑φ ↑s
⊢ ↑φ a⋆ = (↑φ a)⋆
[PROOFSTEP]
rw [← realPart_add_I_smul_imaginaryPart a]
[GOAL]
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
hsa : ∀ (s : { x // x ∈ selfAdjoint A }), (↑φ ↑s)⋆ = ↑φ ↑s
⊢ ↑φ (↑(↑ℜ a) + I • ↑(↑ℑ a))⋆ = (↑φ (↑(↑ℜ a) + I • ↑(↑ℑ a)))⋆
[PROOFSTEP]
simp only [map_add, map_smul, star_add, star_smul, hsa, selfAdjoint.star_val_eq]
[GOAL]
case hsa
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
⊢ ∀ (s : { x // x ∈ selfAdjoint A }), (↑φ ↑s)⋆ = ↑φ ↑s
[PROOFSTEP]
intro s
[GOAL]
case hsa
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
s : { x // x ∈ selfAdjoint A }
⊢ (↑φ ↑s)⋆ = ↑φ ↑s
[PROOFSTEP]
have := AlgHom.apply_mem_spectrum φ (s : A)
[GOAL]
case hsa
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
s : { x // x ∈ selfAdjoint A }
this : ↑φ ↑s ∈ spectrum ℂ ↑s
⊢ (↑φ ↑s)⋆ = ↑φ ↑s
[PROOFSTEP]
rw [selfAdjoint.val_re_map_spectrum s] at this
[GOAL]
case hsa
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
s : { x // x ∈ selfAdjoint A }
this : ↑φ ↑s ∈ ofReal' ∘ re '' spectrum ℂ ↑s
⊢ (↑φ ↑s)⋆ = ↑φ ↑s
[PROOFSTEP]
rcases this with ⟨⟨_, _⟩, _, heq⟩
[GOAL]
case hsa.intro.mk.intro
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
s : { x // x ∈ selfAdjoint A }
re✝ im✝ : ℝ
left✝ : { re := re✝, im := im✝ } ∈ spectrum ℂ ↑s
heq : (ofReal' ∘ re) { re := re✝, im := im✝ } = ↑φ ↑s
⊢ (↑φ ↑s)⋆ = ↑φ ↑s
[PROOFSTEP]
simp only [Function.comp_apply] at heq
[GOAL]
case hsa.intro.mk.intro
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
s : { x // x ∈ selfAdjoint A }
re✝ im✝ : ℝ
left✝ : { re := re✝, im := im✝ } ∈ spectrum ℂ ↑s
heq : ↑re✝ = ↑φ ↑s
⊢ (↑φ ↑s)⋆ = ↑φ ↑s
[PROOFSTEP]
rw [← heq, IsROrC.star_def]
[GOAL]
case hsa.intro.mk.intro
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
s : { x // x ∈ selfAdjoint A }
re✝ im✝ : ℝ
left✝ : { re := re✝, im := im✝ } ∈ spectrum ℂ ↑s
heq : ↑re✝ = ↑φ ↑s
⊢ ↑(starRingEnd ((fun x => ℂ) ↑s)) ↑re✝ = ↑re✝
[PROOFSTEP]
exact IsROrC.conj_ofReal _


[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
⊢ (fun x => ‖f' x‖) =Θ[l] g ↔ f' =Θ[l] g
[PROOFSTEP]
simp [IsTheta]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
⊢ (f =Θ[l] fun x => ‖g' x‖) ↔ f =Θ[l] g'
[PROOFSTEP]
simp [IsTheta]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
h : (fun x => ‖f x‖) =ᶠ[l] fun x => ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ 1 * ‖g x‖
[PROOFSTEP]
simpa only [one_mul] using h.le
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
h : (fun x => ‖f x‖) =ᶠ[l] fun x => ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖g x‖ ≤ 1 * ‖f x‖
[PROOFSTEP]
simpa only [one_mul] using h.symm.le
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g✝ : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
g : α → ℝ
h : (fun x => ‖f' x‖) =ᶠ[l] g
x : α
hx : (fun x => ‖f' x‖) x = g x
⊢ (fun x => ‖f' x‖) x = (fun x => ‖g x‖) x
[PROOFSTEP]
simp only [← hx, norm_norm]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
h : f'' =Θ[l] g''
⊢ Tendsto f'' l (𝓝 0) ↔ Tendsto g'' l (𝓝 0)
[PROOFSTEP]
simp only [← isLittleO_one_iff ℝ, h.isLittleO_congr_left]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
h : f' =Θ[l] g'
⊢ Tendsto (norm ∘ f') l atTop ↔ Tendsto (norm ∘ g') l atTop
[PROOFSTEP]
simp only [Function.comp, ← isLittleO_const_left_of_ne (one_ne_zero' ℝ), h.isLittleO_congr_right]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
h : f' =Θ[l] g'
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f') ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ g')
[PROOFSTEP]
simp only [← isBigO_const_of_ne (one_ne_zero' ℝ), h.isBigO_congr_left]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f✝ : α → E
g✝ : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
f : α → 𝕜
g : α → 𝕜'
h : (fun x => (f x)⁻¹) =Θ[l] fun x => (g x)⁻¹
⊢ f =Θ[l] g
[PROOFSTEP]
simpa only [inv_inv] using h.inv
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
f₁ f₂ : α → 𝕜
g₁ g₂ : α → 𝕜'
h₁ : f₁ =Θ[l] g₁
h₂ : f₂ =Θ[l] g₂
⊢ (fun x => f₁ x / f₂ x) =Θ[l] fun x => g₁ x / g₂ x
[PROOFSTEP]
simpa only [div_eq_mul_inv] using h₁.mul h₂.inv
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f✝ : α → E
g✝ : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
n : ℤ
⊢ (fun x => f x ^ n) =Θ[l] fun x => g x ^ n
[PROOFSTEP]
cases n
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f✝ : α → E
g✝ : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x => f x ^ Int.ofNat a✝) =Θ[l] fun x => g x ^ Int.ofNat a✝
[PROOFSTEP]
simpa only [Int.ofNat_eq_coe, zpow_coe_nat] using h.pow _
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f✝ : α → E
g✝ : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x => f x ^ Int.negSucc a✝) =Θ[l] fun x => g x ^ Int.negSucc a✝
[PROOFSTEP]
simpa only [zpow_negSucc] using (h.pow _).inv
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹³ : Norm E
inst✝¹² : Norm F
inst✝¹¹ : Norm G
inst✝¹⁰ : SeminormedAddCommGroup E'
inst✝⁹ : SeminormedAddCommGroup F'
inst✝⁸ : SeminormedAddCommGroup G'
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedAddCommGroup F''
inst✝⁵ : NormedAddCommGroup G''
inst✝⁴ : SeminormedRing R
inst✝³ : SeminormedRing R'
inst✝² : NormedField 𝕜
inst✝¹ : NormedField 𝕜'
c c' c₁✝ c₂✝ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
inst✝ : NeBot l
c₁ : E''
c₂ : F''
⊢ ((fun x => c₁) =Θ[l] fun x => c₂) ↔ (c₁ = 0 ↔ c₂ = 0)
[PROOFSTEP]
simpa only [IsTheta, isBigO_const_const_iff, ← iff_def] using Iff.comm
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
⊢ (fun x => 0) =Θ[l] g'' ↔ g'' =ᶠ[l] 0
[PROOFSTEP]
simp only [IsTheta, isBigO_zero, isBigO_zero_right_iff, true_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f✝ : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
c : 𝕜
f : α → 𝕜
hc : c ≠ 0
⊢ (fun x => c * f x) =Θ[l] g ↔ f =Θ[l] g
[PROOFSTEP]
simpa only [← smul_eq_mul] using isTheta_const_smul_left hc
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c✝ c' c₁ c₂ : ℝ
f : α → E
g✝ : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
c : 𝕜
g : α → 𝕜
hc : c ≠ 0
⊢ (f =Θ[l] fun x => c * g x) ↔ f =Θ[l] g
[PROOFSTEP]
simpa only [← smul_eq_mul] using isTheta_const_smul_right hc
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
f₁ f₂ : α → E'
h : f₂ =o[l] f₁
⊢ f₁ =O[l] (f₁ + f₂)
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
E' : Type u_6
F' : Type u_7
G' : Type u_8
E'' : Type u_9
F'' : Type u_10
G'' : Type u_11
R : Type u_12
R' : Type u_13
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
l l' : Filter α
f₁ f₂ : α → E'
h : f₂ =o[l] f₁
⊢ f₁ =O[l] (f₂ + f₁)
[PROOFSTEP]
exact h.right_isBigO_add


[GOAL]
E : Type u_1
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : Module ℝ E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
x : E
hx : x ≠ 0
⊢ ∃ f, ↑f x ≠ 0
[PROOFSTEP]
rcases geometric_hahn_banach_point_point hx.symm with ⟨f, hf⟩
[GOAL]
case intro
E : Type u_1
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : Module ℝ E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
x : E
hx : x ≠ 0
f : E →L[ℝ] ℝ
hf : ↑f 0 < ↑f x
⊢ ∃ f, ↑f x ≠ 0
[PROOFSTEP]
simp only [map_zero] at hf
[GOAL]
case intro
E : Type u_1
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : Module ℝ E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
x : E
hx : x ≠ 0
f : E →L[ℝ] ℝ
hf : 0 < ↑f x
⊢ ∃ f, ↑f x ≠ 0
[PROOFSTEP]
exact ⟨f, hf.ne'⟩
[GOAL]
E : Type u_1
𝕜 : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
⊢ ∃ f, ↑f x ≠ 0
[PROOFSTEP]
rcases exists_dual_vector 𝕜 x hx with ⟨f, -, hf⟩
[GOAL]
case intro.intro
E : Type u_1
𝕜 : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
f : E →L[𝕜] 𝕜
hf : ↑f x = ↑‖x‖
⊢ ∃ f, ↑f x ≠ 0
[PROOFSTEP]
refine ⟨f, ?_⟩
[GOAL]
case intro.intro
E : Type u_1
𝕜 : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
f : E →L[𝕜] 𝕜
hf : ↑f x = ↑‖x‖
⊢ ↑f x ≠ 0
[PROOFSTEP]
simpa [hf] using hx
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace V
inst✝² : TopologicalSpace R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
h : x ≠ y
⊢ ∃ f, ↑f x ≠ ↑f y
[PROOFSTEP]
rcases exists_ne_zero (R := R) (sub_ne_zero_of_ne h) with ⟨f, hf⟩
[GOAL]
case intro
R : Type u_1
V : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace V
inst✝² : TopologicalSpace R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
h : x ≠ y
f : V →L[R] R
hf : ↑f (x - y) ≠ 0
⊢ ∃ f, ↑f x ≠ ↑f y
[PROOFSTEP]
exact ⟨f, by simpa [sub_ne_zero] using hf⟩
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace V
inst✝² : TopologicalSpace R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
h : x ≠ y
f : V →L[R] R
hf : ↑f (x - y) ≠ 0
⊢ ↑f x ≠ ↑f y
[PROOFSTEP]
simpa [sub_ne_zero] using hf
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T1Space R
⊢ T1Space V
[PROOFSTEP]
apply t1Space_iff_exists_open.2 (fun x y hxy ↦ ?_)
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T1Space R
x y : V
hxy : x ≠ y
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
[PROOFSTEP]
rcases exists_separating_of_ne (R := R) hxy with ⟨f, hf⟩
[GOAL]
case intro
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T1Space R
x y : V
hxy : x ≠ y
f : V →L[R] R
hf : ↑f x ≠ ↑f y
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
[PROOFSTEP]
exact ⟨f ⁻¹' {f y}ᶜ, isOpen_compl_singleton.preimage f.continuous, hf, by simp⟩
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T1Space R
x y : V
hxy : x ≠ y
f : V →L[R] R
hf : ↑f x ≠ ↑f y
⊢ ¬y ∈ ↑f ⁻¹' {↑f y}ᶜ
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T2Space R
⊢ T2Space V
[PROOFSTEP]
apply (t2Space_iff _).2 (fun {x} {y} hxy ↦ ?_)
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T2Space R
x y : V
hxy : x ≠ y
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
[PROOFSTEP]
rcases exists_separating_of_ne (R := R) hxy with ⟨f, hf⟩
[GOAL]
case intro
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T2Space R
x y : V
hxy : x ≠ y
f : V →L[R] R
hf : ↑f x ≠ ↑f y
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
[PROOFSTEP]
exact separated_by_continuous f.continuous hf
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁷ : Field R
inst✝⁶ : AddCommGroup V
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup V
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x : V
hx : x ≠ 0
⊢ ∃ f, ↑f x = 1
[PROOFSTEP]
rcases exists_ne_zero (R := R) hx with ⟨f, hf⟩
[GOAL]
case intro
R : Type u_1
V : Type u_2
inst✝⁷ : Field R
inst✝⁶ : AddCommGroup V
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup V
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x : V
hx : x ≠ 0
f : V →L[R] R
hf : ↑f x ≠ 0
⊢ ∃ f, ↑f x = 1
[PROOFSTEP]
exact ⟨(f x)⁻¹ • f, inv_mul_cancel hf⟩
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁷ : Field R
inst✝⁶ : AddCommGroup V
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup V
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ f, ↑f x = 1 ∧ ↑f y ≠ 0
[PROOFSTEP]
obtain ⟨u, ux⟩ : ∃ u : V →L[R] R, u x = 1 := exists_eq_one hx
[GOAL]
case intro
R : Type u_1
V : Type u_2
inst✝⁷ : Field R
inst✝⁶ : AddCommGroup V
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup V
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : V →L[R] R
ux : ↑u x = 1
⊢ ∃ f, ↑f x = 1 ∧ ↑f y ≠ 0
[PROOFSTEP]
rcases ne_or_eq (u y) 0 with uy | uy
[GOAL]
case intro.inl
R : Type u_1
V : Type u_2
inst✝⁷ : Field R
inst✝⁶ : AddCommGroup V
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup V
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : V →L[R] R
ux : ↑u x = 1
uy : ↑u y ≠ 0
⊢ ∃ f, ↑f x = 1 ∧ ↑f y ≠ 0
[PROOFSTEP]
exact ⟨u, ux, uy⟩
[GOAL]
case intro.inr
R : Type u_1
V : Type u_2
inst✝⁷ : Field R
inst✝⁶ : AddCommGroup V
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup V
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : V →L[R] R
ux : ↑u x = 1
uy : ↑u y = 0
⊢ ∃ f, ↑f x = 1 ∧ ↑f y ≠ 0
[PROOFSTEP]
obtain ⟨v, vy⟩ : ∃ v : V →L[R] R, v y = 1 := exists_eq_one hy
[GOAL]
case intro.inr.intro
R : Type u_1
V : Type u_2
inst✝⁷ : Field R
inst✝⁶ : AddCommGroup V
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup V
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : V →L[R] R
ux : ↑u x = 1
uy : ↑u y = 0
v : V →L[R] R
vy : ↑v y = 1
⊢ ∃ f, ↑f x = 1 ∧ ↑f y ≠ 0
[PROOFSTEP]
rcases ne_or_eq (v x) 0 with vx | vx
[GOAL]
case intro.inr.intro.inl
R : Type u_1
V : Type u_2
inst✝⁷ : Field R
inst✝⁶ : AddCommGroup V
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup V
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : V →L[R] R
ux : ↑u x = 1
uy : ↑u y = 0
v : V →L[R] R
vy : ↑v y = 1
vx : ↑v x ≠ 0
⊢ ∃ f, ↑f x = 1 ∧ ↑f y ≠ 0
[PROOFSTEP]
exact ⟨(v x)⁻¹ • v, inv_mul_cancel vx, show (v x)⁻¹ * v y ≠ 0 by simp [vx, vy]⟩
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁷ : Field R
inst✝⁶ : AddCommGroup V
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup V
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : V →L[R] R
ux : ↑u x = 1
uy : ↑u y = 0
v : V →L[R] R
vy : ↑v y = 1
vx : ↑v x ≠ 0
⊢ (↑v x)⁻¹ * ↑v y ≠ 0
[PROOFSTEP]
simp [vx, vy]
[GOAL]
case intro.inr.intro.inr
R : Type u_1
V : Type u_2
inst✝⁷ : Field R
inst✝⁶ : AddCommGroup V
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup V
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : V →L[R] R
ux : ↑u x = 1
uy : ↑u y = 0
v : V →L[R] R
vy : ↑v y = 1
vx : ↑v x = 0
⊢ ∃ f, ↑f x = 1 ∧ ↑f y ≠ 0
[PROOFSTEP]
exact ⟨u + v, by simp [ux, vx], by simp [uy, vy]⟩
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁷ : Field R
inst✝⁶ : AddCommGroup V
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup V
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : V →L[R] R
ux : ↑u x = 1
uy : ↑u y = 0
v : V →L[R] R
vy : ↑v y = 1
vx : ↑v x = 0
⊢ ↑(u + v) x = 1
[PROOFSTEP]
simp [ux, vx]
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁷ : Field R
inst✝⁶ : AddCommGroup V
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalRing R
inst✝² : TopologicalAddGroup V
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : V →L[R] R
ux : ↑u x = 1
uy : ↑u y = 0
v : V →L[R] R
vy : ↑v y = 1
vx : ↑v x = 0
⊢ ↑(u + v) y ≠ 0
[PROOFSTEP]
simp [uy, vy]
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ A, ↑A x = y
[PROOFSTEP]
obtain ⟨G, Gx, Gy⟩ : ∃ G : V →L[R] R, G x = 1 ∧ G y ≠ 0 := exists_eq_one_ne_zero_of_ne_zero_pair hx hy
[GOAL]
case intro.intro
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : ↑G x = 1
Gy : ↑G y ≠ 0
⊢ ∃ A, ↑A x = y
[PROOFSTEP]
let A : V ≃L[R] V :=
  { toFun := fun z ↦ z + G z • (y - x)
    invFun := fun z ↦ z + ((G y)⁻¹ * G z) • (x - y)
    map_add' := fun a b ↦ by simp [add_smul]; abel
    map_smul' := by simp [smul_smul]
    left_inv := fun z ↦
      by
      simp only [id_eq, eq_mpr_eq_cast, RingHom.id_apply, smul_eq_mul, AddHom.toFun_eq_coe, AddHom.coe_mk, map_add,
        map_smulₛₗ, map_sub, Gx, mul_sub, mul_one, add_sub_cancel'_right]
      rw [mul_comm (G z), ← mul_assoc, inv_mul_cancel Gy]
      simp only [smul_sub, one_mul]
      abel
    right_inv := fun z ↦
      by
      simp only [map_add, map_smulₛₗ, map_mul, map_inv₀, RingHom.id_apply, map_sub, Gx, smul_eq_mul, mul_sub, mul_one]
      rw [mul_comm _ (G y), ← mul_assoc, mul_inv_cancel Gy]
      simp only [smul_sub, one_mul, add_sub_cancel'_right]
      abel
    continuous_toFun := continuous_id.add (G.continuous.smul continuous_const)
    continuous_invFun := continuous_id.add ((continuous_const.mul G.continuous).smul continuous_const) }
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : ↑G x = 1
Gy : ↑G y ≠ 0
a b : V
⊢ (fun z => z + ↑G z • (y - x)) (a + b) = (fun z => z + ↑G z • (y - x)) a + (fun z => z + ↑G z • (y - x)) b
[PROOFSTEP]
simp [add_smul]
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : ↑G x = 1
Gy : ↑G y ≠ 0
a b : V
⊢ a + b + (↑G a • (y - x) + ↑G b • (y - x)) = a + ↑G a • (y - x) + (b + ↑G b • (y - x))
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : ↑G x = 1
Gy : ↑G y ≠ 0
a b : V
⊢ a + b + (↑G a • (y - x) + ↑G b • (y - x)) = a + ↑G a • (y - x) + (b + ↑G b • (y - x))
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : ↑G x = 1
Gy : ↑G y ≠ 0
⊢ ∀ (r : R) (x_1 : V),
    AddHom.toFun
        { toFun := fun z => z + ↑G z • (y - x),
          map_add' :=
            (_ :
              ∀ (a b : V),
                (fun z => z + ↑G z • (y - x)) (a + b) =
                  (fun z => z + ↑G z • (y - x)) a + (fun z => z + ↑G z • (y - x)) b) }
        (r • x_1) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := fun z => z + ↑G z • (y - x),
            map_add' :=
              (_ :
                ∀ (a b : V),
                  (fun z => z + ↑G z • (y - x)) (a + b) =
                    (fun z => z + ↑G z • (y - x)) a + (fun z => z + ↑G z • (y - x)) b) }
          x_1
[PROOFSTEP]
simp [smul_smul]
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : ↑G x = 1
Gy : ↑G y ≠ 0
z : V
⊢ (fun z => z + ((↑G y)⁻¹ * ↑G z) • (x - y))
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun z => z + ↑G z • (y - x),
                map_add' :=
                  (_ :
                    ∀ (a b : V),
                      (fun z => z + ↑G z • (y - x)) (a + b) =
                        (fun z => z + ↑G z • (y - x)) a + (fun z => z + ↑G z • (y - x)) b) },
            map_smul' :=
              (_ : ∀ (a : R) (a_1 : V), a • a_1 + ↑G (a • a_1) • (y - x) = a • (a_1 + ↑G a_1 • (y - x))) }.toAddHom
        z) =
    z
[PROOFSTEP]
simp only [id_eq, eq_mpr_eq_cast, RingHom.id_apply, smul_eq_mul, AddHom.toFun_eq_coe, AddHom.coe_mk, map_add,
  map_smulₛₗ, map_sub, Gx, mul_sub, mul_one, add_sub_cancel'_right]
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : ↑G x = 1
Gy : ↑G y ≠ 0
z : V
⊢ z + ↑G z • (y - x) + ((↑G y)⁻¹ * (↑G z * ↑G y)) • (x - y) = z
[PROOFSTEP]
rw [mul_comm (G z), ← mul_assoc, inv_mul_cancel Gy]
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : ↑G x = 1
Gy : ↑G y ≠ 0
z : V
⊢ z + ↑G z • (y - x) + (1 * ↑G z) • (x - y) = z
[PROOFSTEP]
simp only [smul_sub, one_mul]
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : ↑G x = 1
Gy : ↑G y ≠ 0
z : V
⊢ z + (↑G z • y - ↑G z • x) + (↑G z • x - ↑G z • y) = z
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : ↑G x = 1
Gy : ↑G y ≠ 0
z : V
⊢ z + (↑G z • y - ↑G z • x) + (↑G z • x - ↑G z • y) = z
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : ↑G x = 1
Gy : ↑G y ≠ 0
z : V
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun z => z + ↑G z • (y - x),
              map_add' :=
                (_ :
                  ∀ (a b : V),
                    (fun z => z + ↑G z • (y - x)) (a + b) =
                      (fun z => z + ↑G z • (y - x)) a + (fun z => z + ↑G z • (y - x)) b) },
          map_smul' :=
            (_ : ∀ (a : R) (a_1 : V), a • a_1 + ↑G (a • a_1) • (y - x) = a • (a_1 + ↑G a_1 • (y - x))) }.toAddHom
      ((fun z => z + ((↑G y)⁻¹ * ↑G z) • (x - y)) z) =
    z
[PROOFSTEP]
simp only [map_add, map_smulₛₗ, map_mul, map_inv₀, RingHom.id_apply, map_sub, Gx, smul_eq_mul, mul_sub, mul_one]
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : ↑G x = 1
Gy : ↑G y ≠ 0
z : V
⊢ z + ((↑G y)⁻¹ * ↑G z) • (x - y) + (↑G z + ((↑G y)⁻¹ * ↑G z - (↑G y)⁻¹ * ↑G z * ↑G y)) • (y - x) = z
[PROOFSTEP]
rw [mul_comm _ (G y), ← mul_assoc, mul_inv_cancel Gy]
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : ↑G x = 1
Gy : ↑G y ≠ 0
z : V
⊢ z + ((↑G y)⁻¹ * ↑G z) • (x - y) + (↑G z + ((↑G y)⁻¹ * ↑G z - 1 * ↑G z)) • (y - x) = z
[PROOFSTEP]
simp only [smul_sub, one_mul, add_sub_cancel'_right]
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : ↑G x = 1
Gy : ↑G y ≠ 0
z : V
⊢ z + (((↑G y)⁻¹ * ↑G z) • x - ((↑G y)⁻¹ * ↑G z) • y) + (((↑G y)⁻¹ * ↑G z) • y - ((↑G y)⁻¹ * ↑G z) • x) = z
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : ↑G x = 1
Gy : ↑G y ≠ 0
z : V
⊢ z + (((↑G y)⁻¹ * ↑G z) • x - ((↑G y)⁻¹ * ↑G z) • y) + (((↑G y)⁻¹ * ↑G z) • y - ((↑G y)⁻¹ * ↑G z) • x) = z
[PROOFSTEP]
abel
[GOAL]
case intro.intro
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : ↑G x = 1
Gy : ↑G y ≠ 0
A : V ≃L[R] V :=
  ContinuousLinearEquiv.mk
    {
      toLinearMap :=
        {
          toAddHom :=
            { toFun := fun z => z + ↑G z • (y - x),
              map_add' :=
                (_ :
                  ∀ (a b : V),
                    (fun z => z + ↑G z • (y - x)) (a + b) =
                      (fun z => z + ↑G z • (y - x)) a + (fun z => z + ↑G z • (y - x)) b) },
          map_smul' := (_ : ∀ (a : R) (a_1 : V), a • a_1 + ↑G (a • a_1) • (y - x) = a • (a_1 + ↑G a_1 • (y - x))) },
      invFun := fun z => z + ((↑G y)⁻¹ * ↑G z) • (x - y),
      left_inv :=
        (_ :
          ∀ (z : V),
            (fun z => z + ((↑G y)⁻¹ * ↑G z) • (x - y))
                (AddHom.toFun
                  {
                      toAddHom :=
                        { toFun := fun z => z + ↑G z • (y - x),
                          map_add' :=
                            (_ :
                              ∀ (a b : V),
                                (fun z => z + ↑G z • (y - x)) (a + b) =
                                  (fun z => z + ↑G z • (y - x)) a + (fun z => z + ↑G z • (y - x)) b) },
                      map_smul' :=
                        (_ :
                          ∀ (a : R) (a_1 : V),
                            a • a_1 + ↑G (a • a_1) • (y - x) = a • (a_1 + ↑G a_1 • (y - x))) }.toAddHom
                  z) =
              z),
      right_inv :=
        (_ :
          ∀ (z : V),
            AddHom.toFun
                {
                    toAddHom :=
                      { toFun := fun z => z + ↑G z • (y - x),
                        map_add' :=
                          (_ :
                            ∀ (a b : V),
                              (fun z => z + ↑G z • (y - x)) (a + b) =
                                (fun z => z + ↑G z • (y - x)) a + (fun z => z + ↑G z • (y - x)) b) },
                    map_smul' :=
                      (_ :
                        ∀ (a : R) (a_1 : V), a • a_1 + ↑G (a • a_1) • (y - x) = a • (a_1 + ↑G a_1 • (y - x))) }.toAddHom
                ((fun z => z + ((↑G y)⁻¹ * ↑G z) • (x - y)) z) =
              z) }
⊢ ∃ A, ↑A x = y
[PROOFSTEP]
exact ⟨A, show x + G x • (y - x) = y by simp [Gx]⟩
[GOAL]
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalRing R
inst✝³ : TopologicalAddGroup V
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : ↑G x = 1
Gy : ↑G y ≠ 0
A : V ≃L[R] V :=
  ContinuousLinearEquiv.mk
    {
      toLinearMap :=
        {
          toAddHom :=
            { toFun := fun z => z + ↑G z • (y - x),
              map_add' :=
                (_ :
                  ∀ (a b : V),
                    (fun z => z + ↑G z • (y - x)) (a + b) =
                      (fun z => z + ↑G z • (y - x)) a + (fun z => z + ↑G z • (y - x)) b) },
          map_smul' := (_ : ∀ (a : R) (a_1 : V), a • a_1 + ↑G (a • a_1) • (y - x) = a • (a_1 + ↑G a_1 • (y - x))) },
      invFun := fun z => z + ((↑G y)⁻¹ * ↑G z) • (x - y),
      left_inv :=
        (_ :
          ∀ (z : V),
            (fun z => z + ((↑G y)⁻¹ * ↑G z) • (x - y))
                (AddHom.toFun
                  {
                      toAddHom :=
                        { toFun := fun z => z + ↑G z • (y - x),
                          map_add' :=
                            (_ :
                              ∀ (a b : V),
                                (fun z => z + ↑G z • (y - x)) (a + b) =
                                  (fun z => z + ↑G z • (y - x)) a + (fun z => z + ↑G z • (y - x)) b) },
                      map_smul' :=
                        (_ :
                          ∀ (a : R) (a_1 : V),
                            a • a_1 + ↑G (a • a_1) • (y - x) = a • (a_1 + ↑G a_1 • (y - x))) }.toAddHom
                  z) =
              z),
      right_inv :=
        (_ :
          ∀ (z : V),
            AddHom.toFun
                {
                    toAddHom :=
                      { toFun := fun z => z + ↑G z • (y - x),
                        map_add' :=
                          (_ :
                            ∀ (a b : V),
                              (fun z => z + ↑G z • (y - x)) (a + b) =
                                (fun z => z + ↑G z • (y - x)) a + (fun z => z + ↑G z • (y - x)) b) },
                    map_smul' :=
                      (_ :
                        ∀ (a : R) (a_1 : V), a • a_1 + ↑G (a • a_1) • (y - x) = a • (a_1 + ↑G a_1 • (y - x))) }.toAddHom
                ((fun z => z + ((↑G y)⁻¹ * ↑G z) • (x - y)) z) =
              z) }
⊢ x + ↑G x • (y - x) = y
[PROOFSTEP]
simp [Gx]