awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹
n : ℕ
⊢ (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) ≤
    (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) * ε⁻¹
have neg : (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) * ε⁻¹ ≤
  (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) * ε⁻¹
Tactic: grw [hN (n + N + 1) (by lia)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
⊢ ∀ᶠ (z : 𝕜) in cobounded 𝕜, IsUnit (resolvent a z)
have rw : ∃ (i : ℝ), True ∧ ∀ ⦃x : 𝕜⦄, Membership.mem (γ := Set 𝕜) (norm ⁻¹' Set.Ioi i) x → IsUnit (resolvent a x)
Tactic: rw [atTop_basis_Ioi.cobounded_of_norm.eventually_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
h :
  IsBigO.{u_1, u_2, 0} (E := A) (F := ℝ) (cobounded 𝕜) (fun (z : 𝕜) ↦ resolvent.{u_1, u_2} (R := 𝕜) (z⁻¹ • a) 1)
    fun (x : 𝕜) ↦ 1
⊢ resolvent a =ᶠ[cobounded 𝕜] fun (z : 𝕜) ↦ z⁻¹ • resolvent.{u_1, u_2} (R := 𝕜) (z⁻¹ • a) 1
have h₁ : ∀ (z : 𝕜) (hz : Membership.mem (γ := Set 𝕜) {0}ᶜ z), resolvent a z = z⁻¹ • resolvent.{u_1, u_2} (R := 𝕜) (z⁻¹ • a) 1
Tactic: filter_upwards [isBounded_singleton (x := 0)] with z hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
h :
  IsBigO.{u_1, u_2, 0} (E := A) (F := ℝ) (cobounded 𝕜) (fun (z : 𝕜) ↦ resolvent.{u_1, u_2} (R := 𝕜) (z⁻¹ • a) 1)
    fun (x : 𝕜) ↦ 1
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {0}ᶜ z
⊢ resolvent a z = z⁻¹ • resolvent.{u_1, u_2} (R := 𝕜) (z⁻¹ • a) 1
have h₁ : ∀ (z : 𝕜ˣ) (hz : Membership.mem (γ := Set 𝕜) {0}ᶜ (↑z : 𝕜)),
  resolvent a (↑z : 𝕜) = (↑z : 𝕜)⁻¹ • resolvent.{u_1, u_2} (R := 𝕜) ((↑z : 𝕜)⁻¹ • a) 1
Tactic: lift z to 𝕜ˣ using Ne.isUnit hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
⊢ (↑‖a‖₊ : ℝ≥0∞)⁻¹ ≤
    radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := A) fun (n : ℕ) ↦ ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)
have refine : ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < (↑‖a‖₊ : ℝ≥0∞)⁻¹) (n : ℕ),
  nnnorm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) A)
        (ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)) *
      r ^ n ≤
    max 1 (nnnorm.{u_2} (E := A) 1)
Tactic: refine le_of_forall_nnreal_lt fun r hr =>
        le_radius_of_bound_nnreal _ (max 1 ‖(1 : A)‖₊) fun n => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (↑‖a‖₊ : ℝ≥0∞)⁻¹
n : ℕ
⊢ nnnorm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) A)
        (ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)) *
      r ^ n ≤
    max 1 (nnnorm.{u_2} (E := A) 1)
have rw : ‖a ^ n‖₊ * r ^ n ≤ max 1 (nnnorm.{u_2} (E := A) 1)
Tactic: rw [← norm_toNNReal, norm_mkPiRing, norm_toNNReal]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (↑‖a‖₊ : ℝ≥0∞)⁻¹
n : ℕ
⊢ ‖a ^ n‖₊ * r ^ n ≤ max 1 (nnnorm.{u_2} (E := A) 1)
have zero : ‖HPow.hPow (β := ℕ) a 0‖₊ * HPow.hPow (β := ℕ) r 0 ≤ max 1 (nnnorm.{u_2} (E := A) 1)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (↑‖a‖₊ : ℝ≥0∞)⁻¹
n : ℕ
zero : ‖HPow.hPow (β := ℕ) a 0‖₊ * HPow.hPow (β := ℕ) r 0 ≤ max 1 (nnnorm.{u_2} (E := A) 1)
⊢ ‖a ^ n‖₊ * r ^ n ≤ max 1 (nnnorm.{u_2} (E := A) 1)
have succ : ∀ (n : ℕ), ‖a ^ (n + 1)‖₊ * r ^ (n + 1) ≤ max 1 (nnnorm.{u_2} (E := A) 1)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (↑‖a‖₊ : ℝ≥0∞)⁻¹
n : ℕ
⊢ ‖a ^ (n + 1)‖₊ * r ^ (n + 1) ≤ max 1 (nnnorm.{u_2} (E := A) 1)
have succ : ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1
Tactic: grw [nnnorm_pow_le' a n.succ_pos, ← le_max_left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (↑‖a‖₊ : ℝ≥0∞)⁻¹
n : ℕ
⊢ ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1
have pos : ∀ (h : ‖a‖₊ = 0), ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1
Tactic: by_cases h : ‖a‖₊ = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (↑‖a‖₊ : ℝ≥0∞)⁻¹
n : ℕ
pos : ∀ (h : ‖a‖₊ = 0), ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1
⊢ ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1
have neg : ∀ (h : ¬‖a‖₊ = 0), ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1
Tactic: by_cases h : ‖a‖₊ = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (↑‖a‖₊ : ℝ≥0∞)⁻¹
n : ℕ
h : ¬‖a‖₊ = 0
⊢ ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1
have neg : ∀ (hr : r * ‖a‖₊ < 1) (n : ℕ) (h : ¬‖a‖₊ = 0), ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1
Tactic: rw [← coe_inv h, coe_lt_coe, NNReal.lt_inv_iff_mul_lt h] at hr
Cleared hypotheses: hr, n, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
y : 𝕜
hy : Membership.mem (γ := Set 𝕜) (Metric.eball 0 (↑‖a‖₊ : ℝ≥0∞)⁻¹) y
⊢ ‖y • a‖ < 1
have pos : ∀ (h : ‖a‖₊ = 0), ‖y • a‖ < 1
Tactic: by_cases h : ‖a‖₊ = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
y : 𝕜
hy : Membership.mem (γ := Set 𝕜) (Metric.eball 0 (↑‖a‖₊ : ℝ≥0∞)⁻¹) y
pos : ∀ (h : ‖a‖₊ = 0), ‖y • a‖ < 1
⊢ ‖y • a‖ < 1
have neg : ∀ (h : ¬‖a‖₊ = 0), ‖y • a‖ < 1
Tactic: by_cases h : ‖a‖₊ = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
y : 𝕜
hy : Membership.mem (γ := Set 𝕜) (Metric.eball 0 (↑‖a‖₊ : ℝ≥0∞)⁻¹) y
h : ¬‖a‖₊ = 0
⊢ ‖y • a‖ < 1
have nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹
Tactic: have nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹ := by
            simpa only [← coe_inv h, mem_ball_zero_iff, Metric.eball_coe] using hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
y : 𝕜
hy : Membership.mem (γ := Set 𝕜) (Metric.eball 0 (↑‖a‖₊ : ℝ≥0∞)⁻¹) y
h : ¬‖a‖₊ = 0
nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹
⊢ ‖y • a‖ < 1
have neg : (↑‖y • a‖₊ : ℝ) < 1
Tactic: rwa [← coe_nnnorm, ← Real.lt_toNNReal_iff_coe_lt, Real.toNNReal_one, nnnorm_smul,
            ← NNReal.lt_inv_iff_mul_lt h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
y : 𝕜
hy : Membership.mem (γ := Set 𝕜) (Metric.eball 0 (↑‖a‖₊ : ℝ≥0∞)⁻¹) y
h : ¬‖a‖₊ = 0
nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹
neg : (↑‖y • a‖₊ : ℝ) < 1
⊢ ‖y • a‖ < 1
have neg₁ : ‖y • a‖₊ < Real.toNNReal 1
Tactic: rwa [← coe_nnnorm, ← Real.lt_toNNReal_iff_coe_lt, Real.toNNReal_one, nnnorm_smul,
            ← NNReal.lt_inv_iff_mul_lt h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
y : 𝕜
hy : Membership.mem (γ := Set 𝕜) (Metric.eball 0 (↑‖a‖₊ : ℝ≥0∞)⁻¹) y
h : ¬‖a‖₊ = 0
nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹
neg : (↑‖y • a‖₊ : ℝ) < 1
neg₁ : ‖y • a‖₊ < Real.toNNReal 1
⊢ ‖y • a‖ < 1
have neg₂ : ‖y • a‖₊ < 1
Tactic: rwa [← coe_nnnorm, ← Real.lt_toNNReal_iff_coe_lt, Real.toNNReal_one, nnnorm_smul,
            ← NNReal.lt_inv_iff_mul_lt h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
y : 𝕜
hy : Membership.mem (γ := Set 𝕜) (Metric.eball 0 (↑‖a‖₊ : ℝ≥0∞)⁻¹) y
h : ¬‖a‖₊ = 0
nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹
neg : (↑‖y • a‖₊ : ℝ) < 1
neg₁ : ‖y • a‖₊ < Real.toNNReal 1
neg₂ : ‖y • a‖₊ < 1
⊢ ‖y • a‖ < 1
have neg₃ : ‖y‖₊ * ‖a‖₊ < 1
Tactic: rwa [← coe_nnnorm, ← Real.lt_toNNReal_iff_coe_lt, Real.toNNReal_one, nnnorm_smul,
            ← NNReal.lt_inv_iff_mul_lt h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
y : 𝕜
hy : Membership.mem (γ := Set 𝕜) (Metric.eball 0 (↑‖a‖₊ : ℝ≥0∞)⁻¹) y
⊢ HasSum
    (fun (n : ℕ) ↦
      (ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n) : (a : (i : Fin n) → 𝕜) → A) fun (x : Fin n) ↦ y)
    (Ring.inverse (1 - (0 + y) • a))
have norm_lt : ‖y • a‖ < 1
Tactic: have norm_lt : ‖y • a‖ < 1 := by
        by_cases h : ‖a‖₊ = 0
        · simp only [nnnorm_eq_zero.mp h, norm_zero, zero_lt_one, smul_zero]
        · have nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹ := by
            simpa only [← coe_inv h, mem_ball_zero_iff, Metric.eball_coe] using hy
          rwa [← coe_nnnorm, ← Real.lt_toNNReal_iff_coe_lt, Real.toNNReal_one, nnnorm_smul,
            ← NNReal.lt_inv_iff_mul_lt h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : (↑‖z‖₊ : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹
⊢ IsUnit (1 - z • a)
have pos : ∀ (hz : z = 0), IsUnit (1 - z • a)
Tactic: by_cases hz : z = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : (↑‖z‖₊ : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹
pos : ∀ (hz : z = 0), IsUnit (1 - z • a)
⊢ IsUnit (1 - z • a)
have neg : ∀ (hz : ¬z = 0), IsUnit (1 - z • a)
Tactic: by_cases hz : z = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : (↑‖z‖₊ : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
hu : IsUnit (HSMul.hSMul (β := A) u⁻¹ 1 - a)
⊢ IsUnit (1 - z • a)
have rwa : ∀ (hu : IsUnit (1 - u⁻¹⁻¹ • a)), IsUnit (1 - z • a)
Tactic: rwa [IsUnit.smul_sub_iff_sub_inv_smul, inv_inv u] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : (↑‖z‖₊ : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
hu : IsUnit (HSMul.hSMul (β := A) u⁻¹ 1 - a)
rwa : ∀ (hu : IsUnit (1 - u⁻¹⁻¹ • a)), IsUnit (1 - z • a)
⊢ IsUnit (1 - z • a)
have rwa₁ : ∀ (hu : IsUnit (1 - u • a)), IsUnit (1 - z • a)
Tactic: rwa [IsUnit.smul_sub_iff_sub_inv_smul, inv_inv u] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : (↑‖z‖₊ : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
⊢ IsUnit (1 - z • a)
have neg : IsUnit (HSMul.hSMul (β := A) u⁻¹ 1 - a)
Tactic: suffices hu : IsUnit (u⁻¹ • (1 : A) - a) by
      rwa [IsUnit.smul_sub_iff_sub_inv_smul, inv_inv u] at hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : (↑‖z‖₊ : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
⊢ IsUnit (HSMul.hSMul (β := A) u⁻¹ 1 - a)
have neg : (↑u⁻¹ : 𝕜) ∈ resolventSet 𝕜 a
Tactic: rw [Units.smul_def, ← Algebra.algebraMap_eq_smul_one, ← mem_resolventSet_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : (↑‖z‖₊ : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
⊢ (↑u⁻¹ : 𝕜) ∈ resolventSet 𝕜 a
have neg : spectralRadius 𝕜 a < (↑‖(↑u⁻¹ : 𝕜)‖₊ : ℝ≥0∞)
Tactic: refine mem_resolventSet_of_spectralRadius_lt ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : (↑‖z‖₊ : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
⊢ spectralRadius 𝕜 a < (↑‖(↑u⁻¹ : 𝕜)‖₊ : ℝ≥0∞)
have neg : spectralRadius 𝕜 a < (↑‖(↑u : 𝕜)⁻¹‖₊ : ℝ≥0∞)
Tactic: rwa [Units.val_inv_eq_inv_val, nnnorm_inv,
      coe_inv (nnnorm_ne_zero_iff.mpr (Units.val_mk0 hz ▸ hz : (u : 𝕜) ≠ 0)), lt_inv_iff_lt_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : (↑‖z‖₊ : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
neg : spectralRadius 𝕜 a < (↑‖(↑u : 𝕜)⁻¹‖₊ : ℝ≥0∞)
⊢ spectralRadius 𝕜 a < (↑‖(↑u⁻¹ : 𝕜)‖₊ : ℝ≥0∞)
have neg₁ : spectralRadius 𝕜 a < (↑‖(↑u : 𝕜)‖₊⁻¹ : ℝ≥0∞)
Tactic: rwa [Units.val_inv_eq_inv_val, nnnorm_inv,
      coe_inv (nnnorm_ne_zero_iff.mpr (Units.val_mk0 hz ▸ hz : (u : 𝕜) ≠ 0)), lt_inv_iff_lt_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : (↑‖z‖₊ : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
neg : spectralRadius 𝕜 a < (↑‖(↑u : 𝕜)⁻¹‖₊ : ℝ≥0∞)
neg₁ : spectralRadius 𝕜 a < (↑‖(↑u : 𝕜)‖₊⁻¹ : ℝ≥0∞)
⊢ spectralRadius 𝕜 a < (↑‖(↑u⁻¹ : 𝕜)‖₊ : ℝ≥0∞)
have neg₂ : spectralRadius 𝕜 a < (↑‖(↑(Units.mk0 z hz) : 𝕜)‖₊ : ℝ≥0∞)⁻¹
Tactic: rwa [Units.val_inv_eq_inv_val, nnnorm_inv,
      coe_inv (nnnorm_ne_zero_iff.mpr (Units.val_mk0 hz ▸ hz : (u : 𝕜) ≠ 0)), lt_inv_iff_lt_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : (↑‖z‖₊ : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
neg : spectralRadius 𝕜 a < (↑‖(↑u : 𝕜)⁻¹‖₊ : ℝ≥0∞)
neg₁ : spectralRadius 𝕜 a < (↑‖(↑u : 𝕜)‖₊⁻¹ : ℝ≥0∞)
neg₂ : spectralRadius 𝕜 a < (↑‖(↑(Units.mk0 z hz) : 𝕜)‖₊ : ℝ≥0∞)⁻¹
⊢ spectralRadius 𝕜 a < (↑‖(↑u⁻¹ : 𝕜)‖₊ : ℝ≥0∞)
have neg₃ : (↑‖(↑(Units.mk0 z hz) : 𝕜)‖₊ : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹
Tactic: rwa [Units.val_inv_eq_inv_val, nnnorm_inv,
      coe_inv (nnnorm_ne_zero_iff.mpr (Units.val_mk0 hz ▸ hz : (u : 𝕜) ≠ 0)), lt_inv_iff_lt_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
⊢ exp z ∈ spectrum 𝕜 (exp a)
have let : ∀ (this : NormedAlgebra ℚ A), exp z ∈ spectrum 𝕜 (exp a)
Tactic: let +nondep : NormedAlgebra ℚ A := .restrictScalars ℚ 𝕜 A
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
⊢ exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)
have rw : exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) (exp ((↑ₐ : (a : 𝕜) → A) z) : A)
Tactic: rw [algebraMap_exp_comm z, ← exp_add_of_commute (Algebra.commutes z (a - ↑ₐ z)).symm,
      sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
rw : exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) (exp ((↑ₐ : (a : 𝕜) → A) z) : A)
⊢ exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)
have rw₁ : exp a = exp (HAdd.hAdd (β := A) (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) ((↑ₐ : (a : 𝕜) → A) z : A))
Tactic: rw [algebraMap_exp_comm z, ← exp_add_of_commute (Algebra.commutes z (a - ↑ₐ z)).symm,
      sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
rw : exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) (exp ((↑ₐ : (a : 𝕜) → A) z) : A)
rw₁ : exp a = exp (HAdd.hAdd (β := A) (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) ((↑ₐ : (a : 𝕜) → A) z : A))
⊢ exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)
have rw₂ : exp a = exp a
Tactic: rw [algebraMap_exp_comm z, ← exp_add_of_commute (Algebra.commutes z (a - ↑ₐ z)).symm,
      sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
⊢ exp z ∈ spectrum 𝕜 (exp a)
have hexpmul : exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)
Tactic: have hexpmul : exp a = exp (a - ↑ₐ z) * ↑ₐ (exp z) := by
    rw [algebraMap_exp_comm z, ← exp_add_of_commute (Algebra.commutes z (a - ↑ₐ z)).symm,
      sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul :
  exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)
b : A :=
  ∑' (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
⊢ Summable.{u_2, 0} (α := A) fun (n : ℕ) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
have refine : ∀ᶠ (i : ℕ) in Filter.cofinite,
  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(i + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ i)‖ ≤
    ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)‖ ^ i / (↑i.factorial : ℝ)
Tactic: refine .of_norm_bounded_eventually (Real.summable_pow_div_factorial ‖a - ↑ₐ z‖) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul :
  exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)
b : A :=
  ∑' (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
⊢ ∀ᶠ (i : ℕ) in Filter.cofinite,
    ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(i + 1).factorial : 𝕜)⁻¹
          (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ i)‖ ≤
      ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)‖ ^ i / (↑i.factorial : ℝ)
have h : ∀ (n : ℕ) (hn : n ≠ 0),
  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)‖ ≤
    ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)‖ ^ n / (↑n.factorial : ℝ)
Tactic: filter_upwards [Filter.eventually_cofinite_ne 0] with n hn
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul :
  exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)
b : A :=
  ∑' (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
n : ℕ
hn : n ≠ 0
⊢ ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)‖ ≤
    ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)‖ ^ n / (↑n.factorial : ℝ)
have h : ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n‖ / (↑(n + 1).factorial : ℝ) ≤
  ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)‖ ^ n / (↑n.factorial : ℝ)
Tactic: rw [norm_smul, mul_comm, norm_inv, RCLike.norm_natCast, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul :
  exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)
b : A :=
  ∑' (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
n : ℕ
hn : n ≠ 0
⊢ ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n‖ / (↑(n + 1).factorial : ℝ) ≤
    ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)‖ ^ n / (↑n.factorial : ℝ)
have h : ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n‖ ≤ ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)‖ ^ n
Tactic: gcongr