awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
succ : ∀ (n : ℕ), ‖a ^ (n + 1)‖₊ * r ^ (n + 1) ≤ max 1 (nnnorm.{u_2} (E := A) 1)
⊢ ‖a ^ n‖₊ * r ^ n ≤ max 1 (nnnorm.{u_2} (E := A) 1)

Tactic:
rcases n with - | n
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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∞)⁻¹
⊢ ‖HPow.hPow (β := ℕ) a 0‖₊ * HPow.hPow (β := ℕ) r 0 ≤ max 1 (nnnorm.{u_2} (E := A) 1)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : ℕ
succ : ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1
⊢ ‖a ^ (n + 1)‖₊ * r ^ (n + 1) ≤ max 1 (nnnorm.{u_2} (E := A) 1)

Tactic:
grw [nnnorm_pow_le' a n.succ_pos, ← le_max_left]

Premises used: nnnorm_pow_le', Nat.succ_pos, le_max_left
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
neg : ∀ (h : ¬‖a‖₊ = 0), ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1
⊢ ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1

Tactic:
by_cases h : ‖a‖₊ = 0
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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

Tactic:
simp [h, pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
neg : ∀ (hr : r * ‖a‖₊ < 1) (n : ℕ) (h : ¬‖a‖₊ = 0), ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1
⊢ ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1

Tactic:
rw [← coe_inv h, coe_lt_coe, NNReal.lt_inv_iff_mul_lt h] at hr

Premises used: ENNReal.coe_inv, ENNReal.coe_lt_coe, NNReal.lt_inv_iff_mul_lt
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 * ‖a‖₊ < 1
n : ℕ
h : ¬‖a‖₊ = 0
⊢ ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1

Tactic:
simpa only [← mul_pow, mul_comm] using pow_le_one' hr.le n.succ

Premises used: pow_le_one', LT.lt.le, mul_comm, mul_pow, Nat.succ
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
neg : ∀ (h : ¬‖a‖₊ = 0), ‖y • a‖ < 1
⊢ ‖y • a‖ < 1

Tactic:
by_cases h : ‖a‖₊ = 0
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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

Tactic:
simp only [nnnorm_eq_zero.mp h, norm_zero, zero_lt_one, smul_zero]

Premises used: norm_zero, smul_zero, zero_lt_one, nnnorm_eq_zero, Iff.mp
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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‖₊⁻¹

Tactic:
simpa only [← coe_inv h, mem_ball_zero_iff, Metric.eball_coe] using hy

Premises used: ENNReal.coe_inv, Metric.eball_coe, mem_ball_zero_iff
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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‖₊⁻¹

Tactic:
have nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹ := by
            simpa only [← coe_inv h, mem_ball_zero_iff, Metric.eball_coe] using hy
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
neg₃ : ‖y‖₊ * ‖a‖₊ < 1
neg₄ neg₅ neg₆ neg₇ : ‖y‖₊ < ‖a‖₊⁻¹
⊢ ‖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]

Premises used: nnnorm_smul, Real.toNNReal_one, NNReal.lt_inv_iff_mul_lt, coe_nnnorm, Real.lt_toNNReal_iff_coe_lt
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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

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]
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
norm_lt : ‖y • a‖ < 1
⊢ 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))

Tactic:
simpa [← smul_pow, (summable_geometric_of_norm_lt_one norm_lt).hasSum_iff] using
        (NormedRing.inverse_one_sub _ norm_lt).symm

Premises used: NormedRing.inverse_one_sub, smul_pow, Summable.hasSum_iff, summable_geometric_of_norm_lt_one, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
neg : ∀ (hz : ¬z = 0), IsUnit (1 - z • a)
⊢ IsUnit (1 - z • a)

Tactic:
by_cases hz : z = 0
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
⊢ IsUnit (1 - z • a)

Tactic:
simp only [hz, isUnit_one, sub_zero, zero_smul]

Premises used: sub_zero, zero_smul, isUnit_one
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hu : IsUnit (1 - u • a)), IsUnit (1 - z • a)
⊢ IsUnit (1 - z • a)

Tactic:
rwa [IsUnit.smul_sub_iff_sub_inv_smul, inv_inv u] at hu

Premises used: IsUnit.smul_sub_iff_sub_inv_smul, inv_inv
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : IsUnit (HSMul.hSMul (β := A) u⁻¹ 1 - a)
⊢ IsUnit (1 - z • a)

Tactic:
suffices hu : IsUnit (u⁻¹ • (1 : A) - a) by
      rwa [IsUnit.smul_sub_iff_sub_inv_smul, inv_inv u] at hu
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : (↑u⁻¹ : 𝕜) ∈ resolventSet 𝕜 a
⊢ IsUnit (HSMul.hSMul (β := A) u⁻¹ 1 - a)

Tactic:
rw [Units.smul_def, ← Algebra.algebraMap_eq_smul_one, ← mem_resolventSet_iff]

Premises used: spectrum.mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, Units.smul_def
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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

Tactic:
mem_resolventSet_of_spectralRadius_lt ?_

Premises used: spectrum.mem_resolventSet_of_spectralRadius_lt
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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∞)
⊢ (↑u⁻¹ : 𝕜) ∈ resolventSet 𝕜 a

Tactic:
refine mem_resolventSet_of_spectralRadius_lt ?_

Premises used: spectrum.mem_resolventSet_of_spectralRadius_lt
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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∞)⁻¹
neg₃ neg₄ neg₅ neg₆ : (↑‖(↑(Units.mk0 z hz) : 𝕜)‖₊ : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹
⊢ 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]

Premises used: nnnorm_inv, Iff.mpr, ENNReal.coe_inv, Units.val_inv_eq_inv_val, nnnorm_ne_zero_iff, Eq.rec, ENNReal.lt_inv_iff_lt_inv, Units.val_mk0, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
let : ∀ (this : NormedAlgebra ℚ A), exp z ∈ spectrum 𝕜 (exp a)
⊢ exp z ∈ spectrum 𝕜 (exp a)

Tactic:
let +nondep : NormedAlgebra ℚ A := .restrictScalars ℚ 𝕜 A
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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))
rw₂ rw₃ : exp a = exp a
⊢ exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)

Tactic:
rw [algebraMap_exp_comm z, ← exp_add_of_commute (Algebra.commutes z (a - ↑ₐ z)).symm,
      sub_add_cancel]

Premises used: NormedSpace.algebraMap_exp_comm, sub_add_cancel
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)

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]
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)

Tactic:
.of_norm_bounded_eventually (Real.summable_pow_div_factorial ‖a - ↑ₐ z‖) ?_

Premises used: Norm.norm, Algebra.algebraMap, HSub.hSub, Real.summable_pow_div_factorial, Summable.of_norm_bounded_eventually, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
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 : ℝ)
⊢ 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)

Tactic:
refine .of_norm_bounded_eventually (Real.summable_pow_div_factorial ‖a - ↑ₐ z‖) ?_
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
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 : ℝ)
⊢ ∀ᶠ (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:
filter_upwards [Filter.eventually_cofinite_ne 0] with n hn

Premises used: Filter.eventually_cofinite_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
h :
  ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n‖ / (↑(n + 1).factorial : ℝ) ≤
    ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)‖ ^ n / (↑n.factorial : ℝ)
⊢ ‖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:
rw [norm_smul, mul_comm, norm_inv, RCLike.norm_natCast, ← div_eq_mul_inv]

Premises used: norm_smul, div_eq_mul_inv, norm_inv, RCLike.norm_natCast, mul_comm
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
h : ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n‖ ≤ ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)‖ ^ n
h₁ : n ≤ n + 1
⊢ ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n‖ / (↑(n + 1).factorial : ℝ) ≤
    ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)‖ ^ n / (↑n.factorial : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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‖ ≤ ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)‖ ^ n

Tactic:
norm_pow_le' _ (pos_iff_ne_zero.mpr hn)

Premises used: Iff.mpr, norm_pow_le', pos_iff_ne_zero
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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‖ ≤ ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)‖ ^ n

Tactic:
exact norm_pow_le' _ (pos_iff_ne_zero.mpr hn)

Premises used: Iff.mpr, norm_pow_le', pos_iff_ne_zero
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
⊢ n ≤ n + 1

Tactic:
n.le_succ

Premises used: Nat.le_succ
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
⊢ n ≤ n + 1

Tactic:
exact n.le_succ

Premises used: Nat.le_succ
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)

Tactic:
have hb : Summable fun n : ℕ => ((n + 1).factorial⁻¹ : 𝕜) • (a - ↑ₐ z) ^ n := by
    refine .of_norm_bounded_eventually (Real.summable_pow_div_factorial ‖a - ↑ₐ z‖) ?_
    filter_upwards [Filter.eventually_cofinite_ne 0] with n hn
    rw [norm_smul, mul_comm, norm_inv, RCLike.norm_natCast, ← div_eq_mul_inv]
    gcongr
    · exact norm_pow_le' _ (pos_iff_ne_zero.mpr hn)
    · exact n.le_succ
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
hb :
  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)
⊢ ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b

Tactic:
simpa only [mul_smul_comm, pow_succ'] using hb.tsum_mul_left (a - ↑ₐ z)

Premises used: mul_smul_comm, pow_succ'
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
hb :
  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)
⊢ ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b

Tactic:
have h₀ : (∑' n : ℕ, ((n + 1).factorial⁻¹ : 𝕜) • (a - ↑ₐ z) ^ (n + 1)) = (a - ↑ₐ z) * b := by
    simpa only [mul_smul_comm, pow_succ'] using hb.tsum_mul_left (a - ↑ₐ z)