[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
src✝¹ : NormedAddCommGroup PUnit := normedAddCommGroup
src✝ : CommRing PUnit := commRing
x✝¹ x✝ : PUnit
⊢ ‖x✝¹ * x✝‖ ≤ ‖x✝¹‖ * ‖x✝‖
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
α : Type u_5
inst✝² : SeminormedAddCommGroup α
inst✝¹ : One α
inst✝ : NormOneClass α
⊢ ‖0‖ ≠ ‖1‖
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : SeminormedAddCommGroup α
inst✝¹ : One α
inst✝ : NormOneClass α
⊢ ‖1‖ = 1
[PROOFSTEP]
simp [ULift.norm_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁵ : SeminormedAddCommGroup α
inst✝⁴ : One α
inst✝³ : NormOneClass α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : One β
inst✝ : NormOneClass β
⊢ ‖1‖ = 1
[PROOFSTEP]
simp [Prod.norm_def]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
ι : Type u_5
α : ι → Type u_6
inst✝⁴ : Nonempty ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → SeminormedAddCommGroup (α i)
inst✝¹ : (i : ι) → One (α i)
inst✝ : ∀ (i : ι), NormOneClass (α i)
⊢ ‖1‖ = 1
[PROOFSTEP]
simp [Pi.norm_def]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
ι : Type u_5
α : ι → Type u_6
inst✝⁴ : Nonempty ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → SeminormedAddCommGroup (α i)
inst✝¹ : (i : ι) → One (α i)
inst✝ : ∀ (i : ι), NormOneClass (α i)
⊢ (Finset.sup Finset.univ fun b => 1) = 1
[PROOFSTEP]
exact Finset.sup_const Finset.univ_nonempty 1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
a b : α
⊢ ‖a * b‖₊ ≤ ‖a‖₊ * ‖b‖₊
[PROOFSTEP]
simpa only [← norm_toNNReal, ← Real.toNNReal_mul (norm_nonneg _)] using Real.toNNReal_mono (norm_mul_le _ _)
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : NonUnitalSeminormedRing α
β : Type u_5
inst✝¹ : NormedRing β
inst✝ : Nontrivial β
⊢ ‖1‖ ≤ ‖1‖ * ‖1‖
[PROOFSTEP]
simpa only [mul_one] using norm_mul_le (1 : β) 1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x y : α
⊢ ‖↑(AddMonoidHom.mulRight x) y‖ ≤ ‖x‖ * ‖y‖
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x y : α
⊢ ‖↑(AddMonoidHom.mulRight x) y‖ ≤ ‖y‖ * ‖x‖
[PROOFSTEP]
exact norm_mul_le y x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
inst✝ : NonUnitalSeminormedRing β
src✝¹ : SeminormedAddCommGroup (α × β) := seminormedAddCommGroup
src✝ : NonUnitalRing (α × β) := instNonUnitalRing
x y : α × β
⊢ max (‖x.fst‖ * ‖y.fst‖) (‖x.snd‖ * ‖y.snd‖) = max (‖x.fst‖ * ‖y.fst‖) (‖y.snd‖ * ‖x.snd‖)
[PROOFSTEP]
simp [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
inst✝ : NonUnitalSeminormedRing β
src✝¹ : SeminormedAddCommGroup (α × β) := seminormedAddCommGroup
src✝ : NonUnitalRing (α × β) := instNonUnitalRing
x y : α × β
⊢ max (‖x.fst‖ * ‖y.fst‖) (‖y.snd‖ * ‖x.snd‖) ≤ max ‖x.fst‖ ‖x.snd‖ * max ‖y.snd‖ ‖y.fst‖
[PROOFSTEP]
apply max_mul_mul_le_max_mul_max
[GOAL]
case ha
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
inst✝ : NonUnitalSeminormedRing β
src✝¹ : SeminormedAddCommGroup (α × β) := seminormedAddCommGroup
src✝ : NonUnitalRing (α × β) := instNonUnitalRing
x y : α × β
⊢ 0 ≤ ‖x.fst‖
[PROOFSTEP]
simp [norm_nonneg]
[GOAL]
case hd
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
inst✝ : NonUnitalSeminormedRing β
src✝¹ : SeminormedAddCommGroup (α × β) := seminormedAddCommGroup
src✝ : NonUnitalRing (α × β) := instNonUnitalRing
x y : α × β
⊢ 0 ≤ ‖y.snd‖
[PROOFSTEP]
simp [norm_nonneg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
inst✝ : NonUnitalSeminormedRing β
src✝¹ : SeminormedAddCommGroup (α × β) := seminormedAddCommGroup
src✝ : NonUnitalRing (α × β) := instNonUnitalRing
x y : α × β
⊢ max ‖x.fst‖ ‖x.snd‖ * max ‖y.snd‖ ‖y.fst‖ = max ‖x.fst‖ ‖x.snd‖ * max ‖y.fst‖ ‖y.snd‖
[PROOFSTEP]
simp [max_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
⊢ ‖↑0‖ ≤ ↑0 * ‖1‖
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
n : ℕ
⊢ ‖↑(n + 1)‖ ≤ ↑(n + 1) * ‖1‖
[PROOFSTEP]
rw [n.cast_succ, n.cast_succ, add_mul, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
n : ℕ
⊢ ‖↑n + 1‖ ≤ ↑n * ‖1‖ + ‖1‖
[PROOFSTEP]
exact norm_add_le_of_le (Nat.norm_cast_le n) le_rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
a : α
x✝ : [a] ≠ []
⊢ ‖prod [a]‖ ≤ prod (map norm [a])
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖prod (a :: b :: l)‖ ≤ prod (map norm (a :: b :: l))
[PROOFSTEP]
rw [List.map_cons, List.prod_cons, @List.prod_cons _ _ _ ‖a‖]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖a * prod (b :: l)‖ ≤ ‖a‖ * prod (map norm (b :: l))
[PROOFSTEP]
refine' le_trans (norm_mul_le _ _) (mul_le_mul_of_nonneg_left _ (norm_nonneg _))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖prod (b :: l)‖ ≤ prod (map norm (b :: l))
[PROOFSTEP]
exact List.norm_prod_le' (List.cons_ne_nil b l)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
l : List α
hl : l ≠ []
⊢ prod (map norm l) = (fun a => ↑a) (prod (map nnnorm l))
[PROOFSTEP]
simp [NNReal.coe_list_prod, List.map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
⊢ ‖prod []‖ ≤ prod (map norm [])
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
l : List α
⊢ prod (map norm l) = (fun a => ↑a) (prod (map nnnorm l))
[PROOFSTEP]
simp [NNReal.coe_list_prod, List.map_map]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α✝
α : Type u_5
inst✝ : NormedCommRing α
s : Finset ι
hs : Finset.Nonempty s
f : ι → α
⊢ ‖∏ i in s, f i‖ ≤ ∏ i in s, ‖f i‖
[PROOFSTEP]
rcases s with ⟨⟨l⟩, hl⟩
[GOAL]
case mk.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α✝
α : Type u_5
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk Setoid.r l)
hs : Finset.Nonempty { val := Quot.mk Setoid.r l, nodup := hl }
⊢ ‖∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, f i‖ ≤ ∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, ‖f i‖
[PROOFSTEP]
have : l.map f ≠ [] := by simpa using hs
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α✝
α : Type u_5
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk Setoid.r l)
hs : Finset.Nonempty { val := Quot.mk Setoid.r l, nodup := hl }
⊢ List.map f l ≠ []
[PROOFSTEP]
simpa using hs
[GOAL]
case mk.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α✝
α : Type u_5
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk Setoid.r l)
hs : Finset.Nonempty { val := Quot.mk Setoid.r l, nodup := hl }
this : List.map f l ≠ []
⊢ ‖∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, f i‖ ≤ ∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, ‖f i‖
[PROOFSTEP]
simpa using List.norm_prod_le' this
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α✝
α : Type u_5
inst✝ : NormedCommRing α
s : Finset ι
hs : Finset.Nonempty s
f : ι → α
⊢ ∏ i in s, ‖f i‖ = (fun a => ↑a) (∏ i in s, ‖f i‖₊)
[PROOFSTEP]
simp [NNReal.coe_prod]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : SeminormedRing α✝
α : Type u_5
inst✝¹ : NormedCommRing α
inst✝ : NormOneClass α
s : Finset ι
f : ι → α
⊢ ‖∏ i in s, f i‖ ≤ ∏ i in s, ‖f i‖
[PROOFSTEP]
rcases s with ⟨⟨l⟩, hl⟩
[GOAL]
case mk.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : SeminormedRing α✝
α : Type u_5
inst✝¹ : NormedCommRing α
inst✝ : NormOneClass α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk Setoid.r l)
⊢ ‖∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, f i‖ ≤ ∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, ‖f i‖
[PROOFSTEP]
simpa using (l.map f).norm_prod_le
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : SeminormedRing α✝
α : Type u_5
inst✝¹ : NormedCommRing α
inst✝ : NormOneClass α
s : Finset ι
f : ι → α
⊢ ∏ i in s, ‖f i‖ = (fun a => ↑a) (∏ i in s, ‖f i‖₊)
[PROOFSTEP]
simp [NNReal.coe_prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
a : α
x✝ : 0 < 1
⊢ ‖a ^ 1‖₊ ≤ ‖a‖₊ ^ 1
[PROOFSTEP]
simp only [pow_one, le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
a : α
n : ℕ
x✝ : 0 < n + 2
⊢ ‖a ^ (n + 2)‖₊ ≤ ‖a‖₊ ^ (n + 2)
[PROOFSTEP]
simpa only [pow_succ _ (n + 1)] using le_trans (nnnorm_mul_le _ _) (mul_le_mul_left' (nnnorm_pow_le' a n.succ_pos) _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
a : α
n : ℕ
⊢ ‖a ^ Nat.zero‖₊ ≤ ‖a‖₊ ^ Nat.zero
[PROOFSTEP]
simp only [Nat.zero_eq, pow_zero, nnnorm_one, le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
a : α
n : ℕ
h : 0 < n
⊢ ‖a ^ n‖ ≤ ‖a‖ ^ n
[PROOFSTEP]
simpa only [NNReal.coe_pow, coe_nnnorm] using NNReal.coe_mono (nnnorm_pow_le' a h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
a : α
n : ℕ
⊢ ‖a ^ Nat.zero‖ ≤ ‖a‖ ^ Nat.zero
[PROOFSTEP]
simp only [Nat.zero_eq, pow_zero, norm_one, le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
⊢ Tendsto (fun e => ‖e.fst * e.snd - (fun p => p.fst * p.snd) x‖) (𝓝 x) (𝓝 0)
[PROOFSTEP]
have : ∀ e : α × α, ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ :=
  by
  intro e
  calc
    ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖ := by
      rw [_root_.mul_sub, _root_.sub_mul, sub_add_sub_cancel]
        -- porting note: `ENNReal.{mul_sub, sub_mul}` should be protected
    _ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ := norm_add_le_of_le (norm_mul_le _ _) (norm_mul_le _ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
⊢ ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
[PROOFSTEP]
intro e
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x e : α × α
⊢ ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
[PROOFSTEP]
calc
  ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖ := by
    rw [_root_.mul_sub, _root_.sub_mul, sub_add_sub_cancel]
      -- porting note: `ENNReal.{mul_sub, sub_mul}` should be protected
  _ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ := norm_add_le_of_le (norm_mul_le _ _) (norm_mul_le _ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x e : α × α
⊢ ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst * (e.snd - x.snd) + (e.fst - x.fst) * x.snd‖
[PROOFSTEP]
rw [_root_.mul_sub, _root_.sub_mul, sub_add_sub_cancel]
  -- porting note: `ENNReal.{mul_sub, sub_mul}` should be protected
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ Tendsto (fun e => ‖e.fst * e.snd - (fun p => p.fst * p.snd) x‖) (𝓝 x) (𝓝 0)
[PROOFSTEP]
refine squeeze_zero (fun e => norm_nonneg _) this ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ Tendsto (fun t => ‖t.fst‖ * ‖t.snd - x.snd‖ + ‖t.fst - x.fst‖ * ‖x.snd‖) (𝓝 x) (𝓝 0)
[PROOFSTEP]
convert
  ((continuous_fst.tendsto x).norm.mul ((continuous_snd.tendsto x).sub tendsto_const_nhds).norm).add
    (((continuous_fst.tendsto x).sub tendsto_const_nhds).norm.mul _)
      -- Porting note: `show` used to select a goal to work on
[GOAL]
case h.e'_5.h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ 0 = ‖x.fst‖ * ‖x.snd - x.snd‖ + ‖x.fst - x.fst‖ * ?convert_4
case convert_4
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ ℝ
case convert_5
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ Tendsto (fun t => ‖x.snd‖) (𝓝 x) (𝓝 ?convert_4)
[PROOFSTEP]
rotate_right
[GOAL]
case convert_5
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ Tendsto (fun t => ‖x.snd‖) (𝓝 x) (𝓝 ?convert_4)
case h.e'_5.h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ 0 = ‖x.fst‖ * ‖x.snd - x.snd‖ + ‖x.fst - x.fst‖ * ?convert_4
case convert_4
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ ℝ
[PROOFSTEP]
show Tendsto _ _ _
[GOAL]
case convert_5
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ Tendsto (fun t => ‖x.snd‖) (𝓝 x) (𝓝 ?convert_4)
case h.e'_5.h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ 0 = ‖x.fst‖ * ‖x.snd - x.snd‖ + ‖x.fst - x.fst‖ * ?convert_4
case convert_4
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ ℝ
[PROOFSTEP]
exact tendsto_const_nhds
[GOAL]
case h.e'_5.h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ 0 = ‖x.fst‖ * ‖x.snd - x.snd‖ + ‖x.fst - x.fst‖ * ‖x.snd‖
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
⊢ ‖1‖ * ‖1‖ = ‖1‖ * 1
[PROOFSTEP]
rw [← norm_mul, mul_one, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
a : α
⊢ ↑‖a⁻¹‖₊ = ↑‖a‖₊⁻¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)
[PROOFSTEP]
rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹, mul_assoc, dist_eq_norm',
  div_eq_mul_inv, mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ nndist z⁻¹ w⁻¹ = nndist z w / (‖z‖₊ * ‖w‖₊)
[PROOFSTEP]
rw [← NNReal.coe_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ ↑(nndist z⁻¹ w⁻¹) = ↑(nndist z w / (‖z‖₊ * ‖w‖₊))
[PROOFSTEP]
simp [-NNReal.coe_eq, dist_inv_inv₀ hz hw]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
a : α
ha : a ≠ 0
⊢ Tendsto ((fun x x_1 => x * x_1) a) (comap norm atTop) (comap norm atTop)
[PROOFSTEP]
simpa only [tendsto_comap_iff, (· ∘ ·), norm_mul] using tendsto_const_nhds.mul_atTop (norm_pos_iff.2 ha) tendsto_comap
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
a : α
ha : a ≠ 0
⊢ Tendsto (fun x => x * a) (comap norm atTop) (comap norm atTop)
[PROOFSTEP]
simpa only [tendsto_comap_iff, (· ∘ ·), norm_mul] using tendsto_comap.atTop_mul (norm_pos_iff.2 ha) tendsto_const_nhds
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
⊢ HasContinuousInv₀ α
[PROOFSTEP]
refine' ⟨fun r r0 => tendsto_iff_norm_tendsto_zero.2 _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
⊢ Tendsto (fun e => ‖e⁻¹ - r⁻¹‖) (𝓝 r) (𝓝 0)
[PROOFSTEP]
have r0' : 0 < ‖r‖ := norm_pos_iff.2 r0
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
⊢ Tendsto (fun e => ‖e⁻¹ - r⁻¹‖) (𝓝 r) (𝓝 0)
[PROOFSTEP]
rcases exists_between r0' with ⟨ε, ε0, εr⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
⊢ Tendsto (fun e => ‖e⁻¹ - r⁻¹‖) (𝓝 r) (𝓝 0)
[PROOFSTEP]
have : ∀ᶠ e in 𝓝 r, ‖e⁻¹ - r⁻¹‖ ≤ ‖r - e‖ / ‖r‖ / ε :=
  by
  filter_upwards [(isOpen_lt continuous_const continuous_norm).eventually_mem εr] with e he
  have e0 : e ≠ 0 := norm_pos_iff.1 (ε0.trans he)
  calc
    ‖e⁻¹ - r⁻¹‖ = ‖r‖⁻¹ * ‖r - e‖ * ‖e‖⁻¹ := by
      rw [← norm_inv, ← norm_inv, ← norm_mul, ← norm_mul, _root_.mul_sub, _root_.sub_mul, mul_assoc _ e,
        inv_mul_cancel r0, mul_inv_cancel e0, one_mul, mul_one]
        -- porting note: `ENNReal.{mul_sub, sub_mul}` should be `protected`
    _ = ‖r - e‖ / ‖r‖ / ‖e‖ := by field_simp [mul_comm]
    _ ≤ ‖r - e‖ / ‖r‖ / ε := by gcongr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
⊢ ∀ᶠ (e : α) in 𝓝 r, ‖e⁻¹ - r⁻¹‖ ≤ ‖r - e‖ / ‖r‖ / ε
[PROOFSTEP]
filter_upwards [(isOpen_lt continuous_const continuous_norm).eventually_mem εr] with e he
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
e : α
he : ε < ‖e‖
⊢ ‖e⁻¹ - r⁻¹‖ ≤ ‖r - e‖ / ‖r‖ / ε
[PROOFSTEP]
have e0 : e ≠ 0 := norm_pos_iff.1 (ε0.trans he)
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
e : α
he : ε < ‖e‖
e0 : e ≠ 0
⊢ ‖e⁻¹ - r⁻¹‖ ≤ ‖r - e‖ / ‖r‖ / ε
[PROOFSTEP]
calc
  ‖e⁻¹ - r⁻¹‖ = ‖r‖⁻¹ * ‖r - e‖ * ‖e‖⁻¹ := by
    rw [← norm_inv, ← norm_inv, ← norm_mul, ← norm_mul, _root_.mul_sub, _root_.sub_mul, mul_assoc _ e,
      inv_mul_cancel r0, mul_inv_cancel e0, one_mul, mul_one]
      -- porting note: `ENNReal.{mul_sub, sub_mul}` should be `protected`
  _ = ‖r - e‖ / ‖r‖ / ‖e‖ := by field_simp [mul_comm]
  _ ≤ ‖r - e‖ / ‖r‖ / ε := by gcongr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
e : α
he : ε < ‖e‖
e0 : e ≠ 0
⊢ ‖e⁻¹ - r⁻¹‖ = ‖r‖⁻¹ * ‖r - e‖ * ‖e‖⁻¹
[PROOFSTEP]
rw [← norm_inv, ← norm_inv, ← norm_mul, ← norm_mul, _root_.mul_sub, _root_.sub_mul, mul_assoc _ e, inv_mul_cancel r0,
  mul_inv_cancel e0, one_mul, mul_one]
  -- porting note: `ENNReal.{mul_sub, sub_mul}` should be `protected`
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
e : α
he : ε < ‖e‖
e0 : e ≠ 0
⊢ ‖r‖⁻¹ * ‖r - e‖ * ‖e‖⁻¹ = ‖r - e‖ / ‖r‖ / ‖e‖
[PROOFSTEP]
field_simp [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
e : α
he : ε < ‖e‖
e0 : e ≠ 0
⊢ ‖r - e‖ / ‖r‖ / ‖e‖ ≤ ‖r - e‖ / ‖r‖ / ε
[PROOFSTEP]
gcongr
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
this : ∀ᶠ (e : α) in 𝓝 r, ‖e⁻¹ - r⁻¹‖ ≤ ‖r - e‖ / ‖r‖ / ε
⊢ Tendsto (fun e => ‖e⁻¹ - r⁻¹‖) (𝓝 r) (𝓝 0)
[PROOFSTEP]
refine' squeeze_zero' (eventually_of_forall fun _ => norm_nonneg _) this _
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
this : ∀ᶠ (e : α) in 𝓝 r, ‖e⁻¹ - r⁻¹‖ ≤ ‖r - e‖ / ‖r‖ / ε
⊢ Tendsto (fun t => ‖r - t‖ / ‖r‖ / ε) (𝓝 r) (𝓝 0)
[PROOFSTEP]
refine' (((continuous_const.sub continuous_id).norm.div_const _).div_const _).tendsto' _ _ _
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
this : ∀ᶠ (e : α) in 𝓝 r, ‖e⁻¹ - r⁻¹‖ ≤ ‖r - e‖ / ‖r‖ / ε
⊢ ‖r - id r‖ / ‖r‖ / ε = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NormedDivisionRing α
inst✝ : Monoid β
φ : β →* α
x : β
k : ℕ+
h : x ^ ↑k = 1
⊢ ‖↑φ x‖ = 1
[PROOFSTEP]
rw [← pow_left_inj, ← norm_pow, ← map_pow, h, map_one, norm_one, one_pow]
[GOAL]
case Hxpos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NormedDivisionRing α
inst✝ : Monoid β
φ : β →* α
x : β
k : ℕ+
h : x ^ ↑k = 1
⊢ 0 ≤ ‖↑φ x‖
case Hypos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NormedDivisionRing α
inst✝ : Monoid β
φ : β →* α
x : β
k : ℕ+
h : x ^ ↑k = 1
⊢ 0 ≤ 1
case Hnpos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NormedDivisionRing α
inst✝ : Monoid β
φ : β →* α
x : β
k : ℕ+
h : x ^ ↑k = 1
⊢ 0 < ↑k
[PROOFSTEP]
exacts [norm_nonneg _, zero_le_one, k.pos]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NontriviallyNormedField α
r : ℝ
w : α
hw : 1 < ‖w‖
n : ℕ
hn : r < ‖w‖ ^ n
⊢ r < ‖w ^ n‖
[PROOFSTEP]
rwa [norm_pow]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NontriviallyNormedField α
r : ℝ
hr : 0 < r
w : α
hw : r⁻¹ < ‖w‖
⊢ 0 < ‖w⁻¹‖ ∧ ‖w⁻¹‖ < r
[PROOFSTEP]
rwa [← Set.mem_Ioo, norm_inv, ← Set.mem_inv, Set.inv_Ioo_0_left hr]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NontriviallyNormedField α
x : α
⊢ NeBot (𝓝[{x}ᶜ] x)
[PROOFSTEP]
rw [← mem_closure_iff_nhdsWithin_neBot, Metric.mem_closure_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NontriviallyNormedField α
x : α
⊢ ∀ (ε : ℝ), ε > 0 → ∃ b, b ∈ {x}ᶜ ∧ dist x b < ε
[PROOFSTEP]
rintro ε ε0
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
⊢ ∃ b, b ∈ {x}ᶜ ∧ dist x b < ε
[PROOFSTEP]
rcases exists_norm_lt α ε0 with ⟨b, hb0, hbε⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ ∃ b, b ∈ {x}ᶜ ∧ dist x b < ε
[PROOFSTEP]
refine' ⟨x + b, mt (Set.mem_singleton_iff.trans add_right_eq_self).1 <| norm_pos_iff.1 hb0, _⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ dist x (x + b) < ε
[PROOFSTEP]
rwa [dist_comm, dist_eq_norm, add_sub_cancel']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NontriviallyNormedField α
⊢ NeBot (𝓝[{x | IsUnit x}] 0)
[PROOFSTEP]
simpa only [isUnit_iff_ne_zero] using punctured_nhds_neBot (0 : α)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
r₁ r₂ : ℝ≥0
h : r₁ < r₂
⊢ ∃ x, r₁ < ‖x‖₊ ∧ ‖x‖₊ < r₂
[PROOFSTEP]
exact_mod_cast exists_lt_norm_lt α r₁.prop h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
⊢ ∀ (a₁ a₂ : ↑(Set.range norm)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
[PROOFSTEP]
rintro ⟨-, x, rfl⟩ ⟨-, y, rfl⟩ hxy
[GOAL]
case mk.intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
x y : α
hxy : { val := ‖x‖, property := (_ : ∃ y, ‖y‖ = ‖x‖) } < { val := ‖y‖, property := (_ : ∃ y_1, ‖y_1‖ = ‖y‖) }
⊢ ∃ a, { val := ‖x‖, property := (_ : ∃ y, ‖y‖ = ‖x‖) } < a ∧ a < { val := ‖y‖, property := (_ : ∃ y_1, ‖y_1‖ = ‖y‖) }
[PROOFSTEP]
let ⟨z, h⟩ := exists_lt_norm_lt α (norm_nonneg _) hxy
[GOAL]
case mk.intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
x y : α
hxy : { val := ‖x‖, property := (_ : ∃ y, ‖y‖ = ‖x‖) } < { val := ‖y‖, property := (_ : ∃ y_1, ‖y_1‖ = ‖y‖) }
z : α
h : ‖x‖ < ‖z‖ ∧ ‖z‖ < ↑{ val := ‖y‖, property := (_ : ∃ y_1, ‖y_1‖ = ‖y‖) }
⊢ ∃ a, { val := ‖x‖, property := (_ : ∃ y, ‖y‖ = ‖x‖) } < a ∧ a < { val := ‖y‖, property := (_ : ∃ y_1, ‖y_1‖ = ‖y‖) }
[PROOFSTEP]
exact ⟨⟨‖z‖, z, rfl⟩, h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
⊢ ∀ (a₁ a₂ : ↑(Set.range nnnorm)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
[PROOFSTEP]
rintro ⟨-, x, rfl⟩ ⟨-, y, rfl⟩ hxy
[GOAL]
case mk.intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
x y : α
hxy : { val := ‖x‖₊, property := (_ : ∃ y, ‖y‖₊ = ‖x‖₊) } < { val := ‖y‖₊, property := (_ : ∃ y_1, ‖y_1‖₊ = ‖y‖₊) }
⊢ ∃ a,
    { val := ‖x‖₊, property := (_ : ∃ y, ‖y‖₊ = ‖x‖₊) } < a ∧
      a < { val := ‖y‖₊, property := (_ : ∃ y_1, ‖y_1‖₊ = ‖y‖₊) }
[PROOFSTEP]
let ⟨z, h⟩ := exists_lt_nnnorm_lt α hxy
[GOAL]
case mk.intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
x y : α
hxy : { val := ‖x‖₊, property := (_ : ∃ y, ‖y‖₊ = ‖x‖₊) } < { val := ‖y‖₊, property := (_ : ∃ y_1, ‖y_1‖₊ = ‖y‖₊) }
z : α
h :
  ↑{ val := ‖x‖₊, property := (_ : ∃ y, ‖y‖₊ = ‖x‖₊) } < ‖z‖₊ ∧
    ‖z‖₊ < ↑{ val := ‖y‖₊, property := (_ : ∃ y_1, ‖y_1‖₊ = ‖y‖₊) }
⊢ ∃ a,
    { val := ‖x‖₊, property := (_ : ∃ y, ‖y‖₊ = ‖x‖₊) } < a ∧
      a < { val := ‖y‖₊, property := (_ : ∃ y_1, ‖y_1‖₊ = ‖y‖₊) }
[PROOFSTEP]
exact ⟨⟨‖z‖₊, z, rfl⟩, h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
x✝¹ x✝ : ℝ
h₀ : 0 ≤ x✝¹
hr : x✝¹ < x✝
x : ℝ
h : x✝¹ < x ∧ x < x✝
⊢ x✝¹ < ‖x‖ ∧ ‖x‖ < x✝
[PROOFSTEP]
rwa [Real.norm_eq_abs, abs_of_nonneg (h₀.trans h.1.le)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
x y : ℝ
hx : 0 ≤ x
⊢ toNNReal x * ‖y‖₊ = ‖x * y‖₊
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
x y : ℝ
hx : 0 ≤ x
⊢ ↑(toNNReal x * ‖y‖₊) = ↑‖x * y‖₊
[PROOFSTEP]
simp only [NNReal.coe_mul, nnnorm_mul, coe_nnnorm, Real.toNNReal_of_nonneg, norm_of_nonneg, hx, coe_mk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
x y : ℝ
hy : 0 ≤ y
⊢ ‖x‖₊ * toNNReal y = ‖x * y‖₊
[PROOFSTEP]
rw [mul_comm, mul_comm x, toNNReal_mul_nnnorm x hy]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
x : ℝ≥0
⊢ ‖↑x‖ = ↑x
[PROOFSTEP]
rw [Real.norm_eq_abs, x.abs_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedAddCommGroup α
a : α
⊢ ‖‖a‖‖₊ = ‖a‖₊
[PROOFSTEP]
rw [Real.nnnorm_of_nonneg (norm_nonneg a)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedAddCommGroup α
a : α
⊢ { val := ‖a‖, property := (_ : 0 ≤ ‖a‖) } = ‖a‖₊
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : Nonempty α
inst✝¹ : SemilatticeSup α
β : Type u_5
inst✝ : SeminormedAddCommGroup β
f : α → β
b : β
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ (x : α), x ∈ Set.Ici ia → f x ∈ ball b ib) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N ≤ n → ‖f n - b‖ < ε
[PROOFSTEP]
simp [dist_eq_norm]
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝³ : Nonempty α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
β : Type u_5
inst✝ : SeminormedAddCommGroup β
f : α → β
b : β
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ (x : α), x ∈ Set.Ioi ia → f x ∈ ball b ib) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N < n → ‖f n - b‖ < ε
[PROOFSTEP]
simp [dist_eq_norm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
src✝¹ : NormedAddCommGroup ℤ := normedAddCommGroup
src✝ : Ring ℤ := instRingInt
m n : ℤ
⊢ ‖m * n‖ = ‖m‖ * ‖n‖
[PROOFSTEP]
simp only [norm, Int.cast_mul, abs_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
⊢ ‖1‖ = 1
[PROOFSTEP]
simp [← Int.norm_cast_real]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
src✝¹ : NormedAddCommGroup ℚ := normedAddCommGroup
src✝ : Field ℚ := field
r₁ r₂ : ℚ
⊢ ‖r₁ * r₂‖ = ‖r₁‖ * ‖r₂‖
[PROOFSTEP]
simp only [norm, Rat.cast_mul, abs_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r₁ r₂ : ℝ
h₀ : 0 ≤ r₁
hr : r₁ < r₂
q : ℚ
h : r₁ < ↑q ∧ ↑q < r₂
⊢ r₁ < ‖q‖ ∧ ‖q‖ < r₂
[PROOFSTEP]
rwa [← Rat.norm_cast_real, Real.norm_eq_abs, abs_of_pos (h₀.trans_lt h.1)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
F : Type u_5
R : Type u_6
S : Type u_7
inst✝² : NonUnitalRing R
inst✝¹ : NonUnitalSeminormedRing S
inst✝ : NonUnitalRingHomClass F R S
f : F
src✝¹ : SeminormedAddCommGroup R := SeminormedAddCommGroup.induced R S f
src✝ : NonUnitalRing R := inst✝²
x y : R
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖
[PROOFSTEP]
show ‖f (x * y)‖ ≤ ‖f x‖ * ‖f y‖
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
F : Type u_5
R : Type u_6
S : Type u_7
inst✝² : NonUnitalRing R
inst✝¹ : NonUnitalSeminormedRing S
inst✝ : NonUnitalRingHomClass F R S
f : F
src✝¹ : SeminormedAddCommGroup R := SeminormedAddCommGroup.induced R S f
src✝ : NonUnitalRing R := inst✝²
x y : R
⊢ ‖↑f (x * y)‖ ≤ ‖↑f x‖ * ‖↑f y‖
[PROOFSTEP]
exact (map_mul f x y).symm ▸ norm_mul_le (f x) (f y)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
F : Type u_5
R : Type u_6
S : Type u_7
inst✝² : DivisionRing R
inst✝¹ : NormedDivisionRing S
inst✝ : NonUnitalRingHomClass F R S
f : F
hf : Function.Injective ↑f
src✝¹ : NormedAddCommGroup R := NormedAddCommGroup.induced R S f hf
src✝ : DivisionRing R := inst✝²
x y : R
⊢ ‖x * y‖ = ‖x‖ * ‖y‖
[PROOFSTEP]
show ‖f (x * y)‖ = ‖f x‖ * ‖f y‖
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
F : Type u_5
R : Type u_6
S : Type u_7
inst✝² : DivisionRing R
inst✝¹ : NormedDivisionRing S
inst✝ : NonUnitalRingHomClass F R S
f : F
hf : Function.Injective ↑f
src✝¹ : NormedAddCommGroup R := NormedAddCommGroup.induced R S f hf
src✝ : DivisionRing R := inst✝²
x y : R
⊢ ‖↑f (x * y)‖ = ‖↑f x‖ * ‖↑f y‖
[PROOFSTEP]
exact (map_mul f x y).symm ▸ norm_mul (f x) (f y)


[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
⊢ spectrum ℂ (star a * a) ⊆ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
rcases subsingleton_or_nontrivial A with ⟨⟩
[GOAL]
case inl
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h✝ : Subsingleton A
⊢ spectrum ℂ (star a * a) ⊆ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
simp only [spectrum.of_subsingleton, Set.empty_subset]
[GOAL]
case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h✝ : Nontrivial A
⊢ spectrum ℂ (star a * a) ⊆ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
set a' : elementalStarAlgebra ℂ a := ⟨a, self_mem ℂ a⟩
[GOAL]
case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
⊢ spectrum ℂ (star a * a) ⊆ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
refine' (spectrum.subset_starSubalgebra (star a' * a')).trans _
[GOAL]
case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
⊢ spectrum ℂ (star a' * a') ⊆ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
rw [← spectrum.gelfandTransform_eq (star a' * a'), ContinuousMap.spectrum_eq_range]
[GOAL]
case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
⊢ Set.range ↑(↑(gelfandTransform ℂ { x // x ∈ elementalStarAlgebra ℂ a }) (star a' * a')) ⊆ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
rintro - ⟨φ, rfl⟩
[GOAL]
case inr.intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
φ : ↑(characterSpace ℂ { x // x ∈ elementalStarAlgebra ℂ a })
⊢ ↑(↑(gelfandTransform ℂ { x // x ∈ elementalStarAlgebra ℂ a }) (star a' * a')) φ ∈ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
rw [gelfandTransform_apply_apply ℂ _ (star a' * a') φ, map_mul φ, map_star φ]
[GOAL]
case inr.intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
φ : ↑(characterSpace ℂ { x // x ∈ elementalStarAlgebra ℂ a })
⊢ star (↑φ a') * ↑φ a' ∈ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
rw [Complex.eq_coe_norm_of_nonneg (star_mul_self_nonneg _), ← map_star, ← map_mul]
[GOAL]
case inr.intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
φ : ↑(characterSpace ℂ { x // x ∈ elementalStarAlgebra ℂ a })
⊢ ↑‖↑φ (star a' * a')‖ ∈ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
exact ⟨Complex.zero_le_real.2 (norm_nonneg _), Complex.real_le_real.2 (AlgHom.norm_apply_le_self φ (star a' * a'))⟩
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h : IsUnit a
⊢ IsUnit { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
[PROOFSTEP]
nontriviality A
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h : IsUnit a
✝ : Nontrivial A
⊢ IsUnit { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
[PROOFSTEP]
set a' : elementalStarAlgebra ℂ a := ⟨a, self_mem ℂ a⟩
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h : IsUnit a
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
⊢ IsUnit a'
[PROOFSTEP]
suffices : IsUnit (star a' * a')
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h : IsUnit a
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
this : IsUnit (star a' * a')
⊢ IsUnit a'
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h : IsUnit a
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
⊢ IsUnit (star a' * a')
[PROOFSTEP]
exact (IsUnit.mul_iff.1 this).2
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h : IsUnit a
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
⊢ IsUnit (star a' * a')
[PROOFSTEP]
replace h :=
  (show Commute (star a) a from star_comm_self' a).isUnit_mul_iff.2
    ⟨h.star, h⟩
      /- Since `a` is invertible, `‖star a * a‖ ≠ 0`, so `‖star a * a‖ • 1` is invertible in
          `elementalStarAlgebra ℂ a`, and so it suffices to show that the distance between this unit and
          `star a * a` is less than `‖star a * a‖`. -/
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
⊢ IsUnit (star a' * a')
[PROOFSTEP]
have h₁ : (‖star a * a‖ : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (norm_ne_zero_iff.mpr h.ne_zero)
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
⊢ IsUnit (star a' * a')
[PROOFSTEP]
set u : Units (elementalStarAlgebra ℂ a) :=
  Units.map (algebraMap ℂ (elementalStarAlgebra ℂ a)).toMonoidHom (Units.mk0 _ h₁)
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
⊢ IsUnit (star a' * a')
[PROOFSTEP]
refine' ⟨u.ofNearby _ _, rfl⟩
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
⊢ ‖star a' * a' - ↑u‖ < ‖↑u⁻¹‖⁻¹
[PROOFSTEP]
simp only [Units.coe_map, Units.val_inv_eq_inv_val, RingHom.toMonoidHom_eq_coe, Units.val_mk0, Units.coe_map_inv,
  MonoidHom.coe_coe, norm_algebraMap', norm_inv, Complex.norm_eq_abs, Complex.abs_ofReal, abs_norm, inv_inv]
  --RingHom.coe_monoidHom,
      -- Complex.abs_ofReal, map_inv₀,
    --rw [norm_algebraMap', inv_inv, Complex.norm_eq_abs, abs_norm]I-
    /- Since `a` is invertible, by `spectrum_star_mul_self_of_isStarNormal`, the spectrum (in `A`)
      of `star a * a` is contained in the half-open interval `(0, ‖star a * a‖]`. Therefore, by basic
      spectral mapping properties, the spectrum of `‖star a * a‖ • 1 - star a * a` is contained in
      `[0, ‖star a * a‖)`. -/
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
⊢ ‖star { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) } *
          { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) } -
        ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a }) ↑‖star a * a‖‖ <
    ‖star a * a‖
[PROOFSTEP]
have h₂ : ∀ z ∈ spectrum ℂ (algebraMap ℂ A ‖star a * a‖ - star a * a), ‖z‖₊ < ‖star a * a‖₊ :=
  by
  intro z hz
  rw [← spectrum.singleton_sub_eq, Set.singleton_sub] at hz
  have h₃ : z ∈ Set.Icc (0 : ℂ) ‖star a * a‖ :=
    by
    replace hz := Set.image_subset _ (spectrum_star_mul_self_of_isStarNormal a) hz
    rwa [Set.image_const_sub_Icc, sub_self, sub_zero] at hz
  refine' lt_of_le_of_ne (Complex.real_le_real.1 <| Complex.eq_coe_norm_of_nonneg h₃.1 ▸ h₃.2) _
  · intro hz'
    replace hz' := congr_arg (fun x : ℝ≥0 => ((x : ℝ) : ℂ)) hz'
    simp only [coe_nnnorm] at hz'
    rw [← Complex.eq_coe_norm_of_nonneg h₃.1] at hz'
    obtain ⟨w, hw₁, hw₂⟩ := hz
    refine' (spectrum.zero_not_mem_iff ℂ).mpr h _
    rw [hz', sub_eq_self] at hw₂
    rwa [hw₂] at hw₁
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
⊢ ∀ (z : ℂ), z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a) → ‖z‖₊ < ‖star a * a‖₊
[PROOFSTEP]
intro z hz
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a)
⊢ ‖z‖₊ < ‖star a * a‖₊
[PROOFSTEP]
rw [← spectrum.singleton_sub_eq, Set.singleton_sub] at hz
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' spectrum ℂ (star a * a)
⊢ ‖z‖₊ < ‖star a * a‖₊
[PROOFSTEP]
have h₃ : z ∈ Set.Icc (0 : ℂ) ‖star a * a‖ :=
  by
  replace hz := Set.image_subset _ (spectrum_star_mul_self_of_isStarNormal a) hz
  rwa [Set.image_const_sub_Icc, sub_self, sub_zero] at hz
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' spectrum ℂ (star a * a)
⊢ z ∈ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
replace hz := Set.image_subset _ (spectrum_star_mul_self_of_isStarNormal a) hz
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' Set.Icc 0 ↑‖star a * a‖
⊢ z ∈ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
rwa [Set.image_const_sub_Icc, sub_self, sub_zero] at hz
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' spectrum ℂ (star a * a)
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
⊢ ‖z‖₊ < ‖star a * a‖₊
[PROOFSTEP]
refine' lt_of_le_of_ne (Complex.real_le_real.1 <| Complex.eq_coe_norm_of_nonneg h₃.1 ▸ h₃.2) _
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' spectrum ℂ (star a * a)
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
⊢ ‖z‖₊ ≠ ‖star a * a‖₊
[PROOFSTEP]
intro hz'
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' spectrum ℂ (star a * a)
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
hz' : ‖z‖₊ = ‖star a * a‖₊
⊢ False
[PROOFSTEP]
replace hz' := congr_arg (fun x : ℝ≥0 => ((x : ℝ) : ℂ)) hz'
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' spectrum ℂ (star a * a)
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
hz' : (fun x => ↑↑x) ‖z‖₊ = (fun x => ↑↑x) ‖star a * a‖₊
⊢ False
[PROOFSTEP]
simp only [coe_nnnorm] at hz'
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' spectrum ℂ (star a * a)
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
hz' : ↑‖z‖ = ↑‖star a * a‖
⊢ False
[PROOFSTEP]
rw [← Complex.eq_coe_norm_of_nonneg h₃.1] at hz'
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' spectrum ℂ (star a * a)
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
hz' : z = ↑‖star a * a‖
⊢ False
[PROOFSTEP]
obtain ⟨w, hw₁, hw₂⟩ := hz
[GOAL]
case intro.intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
hz' : z = ↑‖star a * a‖
w : ℂ
hw₁ : w ∈ spectrum ℂ (star a * a)
hw₂ : (fun x x_1 => x - x_1) (↑‖star a * a‖) w = z
⊢ False
[PROOFSTEP]
refine' (spectrum.zero_not_mem_iff ℂ).mpr h _
[GOAL]
case intro.intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
hz' : z = ↑‖star a * a‖
w : ℂ
hw₁ : w ∈ spectrum ℂ (star a * a)
hw₂ : (fun x x_1 => x - x_1) (↑‖star a * a‖) w = z
⊢ 0 ∈ spectrum ℂ (star a * a)
[PROOFSTEP]
rw [hz', sub_eq_self] at hw₂
[GOAL]
case intro.intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
hz' : z = ↑‖star a * a‖
w : ℂ
hw₁ : w ∈ spectrum ℂ (star a * a)
hw₂ : w = 0
⊢ 0 ∈ spectrum ℂ (star a * a)
[PROOFSTEP]
rwa [hw₂] at hw₁
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
h₂ : ∀ (z : ℂ), z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a) → ‖z‖₊ < ‖star a * a‖₊
⊢ ‖star { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) } *
          { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) } -
        ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a }) ↑‖star a * a‖‖ <
    ‖star a * a‖
[PROOFSTEP]
exact
  ENNReal.coe_lt_coe.1
    (calc
      (‖star a' * a' - algebraMap ℂ _ ‖star a * a‖‖₊ : ℝ≥0∞) = ‖algebraMap ℂ A ‖star a * a‖ - star a * a‖₊ := by
        rw [← nnnorm_neg, neg_sub]; rfl
      _ = spectralRadius ℂ (algebraMap ℂ A ‖star a * a‖ - star a * a) :=
        by
        refine' (IsSelfAdjoint.spectralRadius_eq_nnnorm _).symm
        rw [IsSelfAdjoint, star_sub, star_mul, star_star, ← algebraMap_star_comm]
        congr!
        exact IsROrC.conj_ofReal _
      _ < ‖star a * a‖₊ := spectrum.spectralRadius_lt_of_forall_lt _ h₂)
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
h₂ : ∀ (z : ℂ), z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a) → ‖z‖₊ < ‖star a * a‖₊
⊢ ↑‖star a' * a' - ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a }) ↑‖star a * a‖‖₊ =
    ↑‖↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a‖₊
[PROOFSTEP]
rw [← nnnorm_neg, neg_sub]
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
h₂ : ∀ (z : ℂ), z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a) → ‖z‖₊ < ‖star a * a‖₊
⊢ ↑‖↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a }) ↑‖star a * a‖ - star a' * a'‖₊ =
    ↑‖↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a‖₊
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
h₂ : ∀ (z : ℂ), z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a) → ‖z‖₊ < ‖star a * a‖₊
⊢ ↑‖↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a‖₊ = spectralRadius ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a)
[PROOFSTEP]
refine' (IsSelfAdjoint.spectralRadius_eq_nnnorm _).symm
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
h₂ : ∀ (z : ℂ), z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a) → ‖z‖₊ < ‖star a * a‖₊
⊢ IsSelfAdjoint (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a)
[PROOFSTEP]
rw [IsSelfAdjoint, star_sub, star_mul, star_star, ← algebraMap_star_comm]
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
h₂ : ∀ (z : ℂ), z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a) → ‖z‖₊ < ‖star a * a‖₊
⊢ ↑(algebraMap ℂ A) (star ↑‖star a * a‖) - star a * a = ↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a
[PROOFSTEP]
congr!
[GOAL]
case h.e'_5.h.e'_6
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
h₂ : ∀ (z : ℂ), z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a) → ‖z‖₊ < ‖star a * a‖₊
⊢ star ↑‖star a * a‖ = ↑‖star a * a‖
[PROOFSTEP]
exact IsROrC.conj_ofReal _
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
⊢ ↑(IsUnit.unit h)⁻¹ ∈ S
[PROOFSTEP]
have hx := h.star.mul h
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
⊢ ↑(IsUnit.unit h)⁻¹ ∈ S
[PROOFSTEP]
suffices this : (↑hx.unit⁻¹ : A) ∈ S
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
this : ↑(IsUnit.unit hx)⁻¹ ∈ S
⊢ ↑(IsUnit.unit h)⁻¹ ∈ S
[PROOFSTEP]
rw [← one_mul (↑h.unit⁻¹ : A), ← hx.unit.inv_mul, mul_assoc, IsUnit.unit_spec, mul_assoc, h.mul_val_inv, mul_one]
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
this : ↑(IsUnit.unit hx)⁻¹ ∈ S
⊢ ↑(IsUnit.unit hx)⁻¹ * star x ∈ S
[PROOFSTEP]
exact mul_mem this (star_mem hxS)
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
⊢ ↑(IsUnit.unit hx)⁻¹ ∈ S
[PROOFSTEP]
refine' le_of_isClosed_of_mem ℂ hS (mul_mem (star_mem hxS) hxS) _
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
⊢ ↑(IsUnit.unit hx)⁻¹ ∈ elementalStarAlgebra ℂ (star x * x)
[PROOFSTEP]
haveI := (IsSelfAdjoint.star_mul_self x).isStarNormal
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
this : IsStarNormal (star x * x)
⊢ ↑(IsUnit.unit hx)⁻¹ ∈ elementalStarAlgebra ℂ (star x * x)
[PROOFSTEP]
have hx' := elementalStarAlgebra.isUnit_of_isUnit_of_isStarNormal hx
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
this : IsStarNormal (star x * x)
hx' : IsUnit { val := star x * x, property := (_ : star x * x ∈ elementalStarAlgebra ℂ (star x * x)) }
⊢ ↑(IsUnit.unit hx)⁻¹ ∈ elementalStarAlgebra ℂ (star x * x)
[PROOFSTEP]
convert (↑hx'.unit⁻¹ : elementalStarAlgebra ℂ (star x * x)).prop using 1
[GOAL]
case h.e'_4
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
this : IsStarNormal (star x * x)
hx' : IsUnit { val := star x * x, property := (_ : star x * x ∈ elementalStarAlgebra ℂ (star x * x)) }
⊢ ↑(IsUnit.unit hx)⁻¹ = ↑↑(IsUnit.unit hx')⁻¹
[PROOFSTEP]
refine left_inv_eq_right_inv hx.unit.inv_mul ?_
[GOAL]
case h.e'_4
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
this : IsStarNormal (star x * x)
hx' : IsUnit { val := star x * x, property := (_ : star x * x ∈ elementalStarAlgebra ℂ (star x * x)) }
⊢ ↑(IsUnit.unit hx) * ↑↑(IsUnit.unit hx')⁻¹ = 1
[PROOFSTEP]
exact (congr_arg ((↑) : _ → A) hx'.unit.mul_inv)
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : { x // x ∈ S }
⊢ IsUnit ↑x ↔ IsUnit x
[PROOFSTEP]
refine'
  ⟨fun hx => ⟨⟨x, ⟨(↑hx.unit⁻¹ : A), StarSubalgebra.isUnit_coe_inv_mem hS hx x.prop⟩, _, _⟩, rfl⟩, fun hx =>
    hx.map S.subtype⟩
[GOAL]
case refine'_1
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : { x // x ∈ S }
hx : IsUnit ↑x
⊢ x * { val := ↑(IsUnit.unit hx)⁻¹, property := (_ : ↑(IsUnit.unit hx)⁻¹ ∈ S) } = 1
case refine'_2
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : { x // x ∈ S }
hx : IsUnit ↑x
⊢ { val := ↑(IsUnit.unit hx)⁻¹, property := (_ : ↑(IsUnit.unit hx)⁻¹ ∈ S) } * x = 1
[PROOFSTEP]
exacts [Subtype.coe_injective hx.mul_val_inv, Subtype.coe_injective hx.val_inv_mul]
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
x : A
φ : ↑(characterSpace ℂ { x_1 // x_1 ∈ elementalStarAlgebra ℂ x })
⊢ ↑φ { val := x, property := (_ : x ∈ elementalStarAlgebra ℂ x) } ∈ spectrum ℂ x
[PROOFSTEP]
simpa only [StarSubalgebra.spectrum_eq (elementalStarAlgebra.isClosed ℂ x) ⟨x, self_mem ℂ x⟩] using
  AlgHom.apply_mem_spectrum φ ⟨x, self_mem ℂ x⟩
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
⊢ Function.Bijective (characterSpaceToSpectrum a)
[PROOFSTEP]
refine' ⟨fun φ ψ h => starAlgHomClass_ext ℂ _ _ _, _⟩
[GOAL]
case refine'_1
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
φ ψ : ↑(characterSpace ℂ { x // x ∈ elementalStarAlgebra ℂ a })
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ Continuous ↑φ
[PROOFSTEP]
exact (map_continuous φ)
[GOAL]
case refine'_2
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
φ ψ : ↑(characterSpace ℂ { x // x ∈ elementalStarAlgebra ℂ a })
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ Continuous ↑ψ
[PROOFSTEP]
exact (map_continuous ψ)
[GOAL]
case refine'_3
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
φ ψ : ↑(characterSpace ℂ { x // x ∈ elementalStarAlgebra ℂ a })
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) } =
    ↑ψ { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
[PROOFSTEP]
simpa only [elementalStarAlgebra.characterSpaceToSpectrum, Subtype.mk_eq_mk, ContinuousMap.coe_mk] using h
[GOAL]
case refine'_4
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
⊢ Function.Surjective (characterSpaceToSpectrum a)
[PROOFSTEP]
rintro ⟨z, hz⟩
[GOAL]
case refine'_4.mk
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
z : ℂ
hz : z ∈ spectrum ℂ a
⊢ ∃ a_1, characterSpaceToSpectrum a a_1 = { val := z, property := hz }
[PROOFSTEP]
have hz' := (StarSubalgebra.spectrum_eq (elementalStarAlgebra.isClosed ℂ a) ⟨a, self_mem ℂ a⟩).symm.subst hz
[GOAL]
case refine'_4.mk
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
z : ℂ
hz : z ∈ spectrum ℂ a
hz' : z ∈ spectrum ℂ { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
⊢ ∃ a_1, characterSpaceToSpectrum a a_1 = { val := z, property := hz }
[PROOFSTEP]
rw [CharacterSpace.mem_spectrum_iff_exists] at hz'
[GOAL]
case refine'_4.mk
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
z : ℂ
hz : z ∈ spectrum ℂ a
hz' : ∃ f, ↑f { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) } = z
⊢ ∃ a_1, characterSpaceToSpectrum a a_1 = { val := z, property := hz }
[PROOFSTEP]
obtain ⟨φ, rfl⟩ := hz'
[GOAL]
case refine'_4.mk.intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
φ : ↑(characterSpace ℂ { x // x ∈ elementalStarAlgebra ℂ a })
hz : ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) } ∈ spectrum ℂ a
⊢ ∃ a_1,
    characterSpaceToSpectrum a a_1 =
      { val := ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }, property := hz }
[PROOFSTEP]
exact ⟨φ, rfl⟩