awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
h₀ :
  ∑' (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
⊢ ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    b * HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)

Tactic:
simpa only [pow_succ, Algebra.smul_mul_assoc] using hb.tsum_mul_right (a - ↑ₐ z)

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

Tactic:
have h₁ : (∑' n : ℕ, ((n + 1).factorial⁻¹ : 𝕜) • (a - ↑ₐ z) ^ (n + 1)) = b * (a - ↑ₐ z) := by
    simpa only [pow_succ, Algebra.smul_mul_assoc] using hb.tsum_mul_right (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)
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)
h₀ :
  ∑' (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
h₁ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    b * HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)
rw :
  (fun (x : A) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x ^ n) : A))
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) =
    1 + HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b
⊢ exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) = 1 + HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b

Tactic:
rw [exp_eq_tsum 𝕜]

Premises used: NormedSpace.exp_eq_tsum
-- 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)
h₀ :
  ∑' (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
h₁ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    b * HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)
⊢ ∑' (b : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑b.factorial : 𝕜)⁻¹ (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ b) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(Nat.factorial 0) : 𝕜)⁻¹
        (HPow.hPow (β := ℕ) (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) 0) +
      ∑' (b : ℕ),
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(b + 1).factorial : 𝕜)⁻¹
          (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (b + 1))

Tactic:
(expSeries_summable' (𝕂 := 𝕜) (a - ↑ₐ z)).tsum_eq_zero_add

Premises used: Algebra.algebraMap, Summable.tsum_eq_zero_add, HSub.hSub, NormedSpace.expSeries_summable', 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)
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)
h₀ :
  ∑' (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
h₁ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    b * HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)
h :
  1 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(Nat.factorial 0) : 𝕜)⁻¹
      (HPow.hPow (β := ℕ) (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) 0)
h₂ :
  HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b =
    ∑' (b : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(b + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (b + 1))
⊢ (fun (x : A) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x ^ n) : A))
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) =
    1 + HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b

Tactic:
convert! (expSeries_summable' (𝕂 := 𝕜) (a - ↑ₐ z)).tsum_eq_zero_add
-- 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)
h₀ :
  ∑' (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
h₁ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    b * HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)
⊢ 1 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(Nat.factorial 0) : 𝕜)⁻¹
      (HPow.hPow (β := ℕ) (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) 0)

Tactic:
simp only [Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero, one_smul]

Premises used: inv_one, pow_zero, one_smul, Nat.factorial_zero, Nat.cast_one
-- 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)
h₀ :
  ∑' (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
h₁ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    b * HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)
⊢ HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b =
    ∑' (b : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(b + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (b + 1))

Tactic:
h₀.symm

Premises used: 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
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)
h₀ :
  ∑' (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
h₁ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    b * HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)
⊢ HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b =
    ∑' (b : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(b + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (b + 1))

Tactic:
exact h₀.symm

Premises used: 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
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)
h₀ :
  ∑' (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
h₁ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    b * HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)
⊢ exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) = 1 + HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b

Tactic:
have h₃ : exp (a - ↑ₐ z) = 1 + (a - ↑ₐ z) * b := by
    rw [exp_eq_tsum 𝕜]
    convert! (expSeries_summable' (𝕂 := 𝕜) (a - ↑ₐ z)).tsum_eq_zero_add
    · simp only [Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero, one_smul]
    · exact h₀.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
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)
h₀ :
  ∑' (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
h₁ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    b * HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)
h₃ : exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) = 1 + HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b
rw :
  ¬((IsUnit (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) ∧ IsUnit b) ∧
      IsUnit.{u_2} (M := A) ((↑ₐ : (a : 𝕜) → A) (exp z) : A))
⊢ exp z ∈ spectrum 𝕜 (exp a)

Tactic:
rw [spectrum.mem_iff, IsUnit.sub_iff, ← one_mul (↑ₐ (exp z)), hexpmul, ← _root_.sub_mul,
    Commute.isUnit_mul_iff (Algebra.commutes (exp z) (exp (a - ↑ₐ z) - 1)).symm,
    sub_eq_iff_eq_add'.mpr h₃, Commute.isUnit_mul_iff (h₀ ▸ h₁ : (a - ↑ₐ z) * b = b * (a - ↑ₐ z))]

Premises used: Iff.mpr, IsUnit.sub_iff, sub_mul, spectrum.mem_iff, sub_eq_iff_eq_add'
-- 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)
h₀ :
  ∑' (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
h₁ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    b * HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)
h₃ : exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) = 1 + HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b
⊢ ¬((IsUnit (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) ∧ IsUnit b) ∧
      IsUnit.{u_2} (M := A) ((↑ₐ : (a : 𝕜) → A) (exp z) : A))

Tactic:
not_and_of_not_left _ (not_and_of_not_left _ ((not_iff_not.mpr IsUnit.sub_iff).mp hz))

Premises used: not_iff_not, Iff.mpr, not_and_of_not_left, IsUnit.sub_iff, Iff.mp
-- 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)
h₀ :
  ∑' (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
h₁ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    b * HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)
h₃ : exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) = 1 + HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b
⊢ ¬((IsUnit (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) ∧ IsUnit b) ∧
      IsUnit.{u_2} (M := A) ((↑ₐ : (a : 𝕜) → A) (exp z) : A))

Tactic:
exact not_and_of_not_left _ (not_and_of_not_left _ ((not_iff_not.mpr IsUnit.sub_iff).mp hz))

Premises used: not_iff_not, Iff.mpr, not_and_of_not_left, IsUnit.sub_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
F : Type u_3
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : FunLike F A 𝕜
inst_5 : AlgHomClass F 𝕜 A 𝕜
⊢ ContinuousLinearMapClass F 𝕜 A 𝕜

Tactic:
{ AlgHomClass.linearMapClass with
    map_continuous := fun φ =>
      AddMonoidHomClass.continuous_of_bound φ ‖(1 : A)‖ fun a =>
        mul_comm ‖a‖ ‖(1 : A)‖ ▸ spectrum.norm_le_norm_mul_of_mem (apply_mem_spectrum φ _) }

Premises used: AlgHomClass.linearMapClass, ContinuousSemilinearMapClass.mk
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
φ : A →ₐ[𝕜] 𝕜
⊢ Eq (α := (a : A) → 𝕜) (⇑φ.toContinuousLinearMap : (a : A) → 𝕜) (⇑φ : (a : A) → 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
F : Type u_3
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : FunLike F A 𝕜
inst_5 : AlgHomClass F 𝕜 A 𝕜
f : F
a : A
⊢ norm.{u_1} (E := 𝕜) ((f : (a : A) → 𝕜) a : 𝕜) ≤ ‖a‖ * norm.{u_2} (E := A) 1

Tactic:
spectrum.norm_le_norm_mul_of_mem (apply_mem_spectrum f _)

Premises used: AlgHom.apply_mem_spectrum, spectrum.norm_le_norm_mul_of_mem
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
F : Type u_3
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : NormOneClass A
inst_5 : FunLike F A 𝕜
inst_6 : AlgHomClass F 𝕜 A 𝕜
f : F
a : A
⊢ norm.{u_1} (E := 𝕜) ((f : (a : A) → 𝕜) a : 𝕜) ≤ ‖a‖

Tactic:
spectrum.norm_le_norm_of_mem (apply_mem_spectrum f _)

Premises used: spectrum.norm_le_norm_of_mem, AlgHom.apply_mem_spectrum
-- 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 : CompleteSpace A
inst_4 : NormOneClass A
φ : A →ₐ[𝕜] 𝕜
x : ℝ
h_1 : x ≥ 0
h : ∀ (x_1 : A), norm.{u_1} (E := 𝕜) ((φ.toContinuousLinearMap : (a : A) → 𝕜) x_1 : 𝕜) ≤ x * ‖x_1‖
⊢ 1 ≤ x

Tactic:
simpa only [coe_toContinuousLinearMap, map_one, norm_one, mul_one] using h 1

Premises used: NormOneClass.norm_one, map_one, AlgHom.coe_toContinuousLinearMap, mul_one, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : CompleteSpace A
inst_3 : NormedAlgebra 𝕜 A
f : A →ₐ[𝕜] 𝕜
rw :
  Membership.mem (γ := Set (WeakDual 𝕜 A))
    {φ : WeakDual 𝕜 A |
      Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜) ∧
        ∀ (x y : A),
          (φ : (a : A) → 𝕜) (x * y) = HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((φ : (a : A) → 𝕜) y : 𝕜)}
    f.toContinuousLinearMap
⊢ Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) f.toContinuousLinearMap

Tactic:
rw [eq_set_map_one_map_mul]

Premises used: WeakDual.CharacterSpace.eq_set_map_one_map_mul
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : CompleteSpace A
inst_3 : NormedAlgebra 𝕜 A
f : A →ₐ[𝕜] 𝕜
⊢ Membership.mem (γ := Set (WeakDual 𝕜 A))
    {φ : WeakDual 𝕜 A |
      Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜) ∧
        ∀ (x y : A),
          (φ : (a : A) → 𝕜) (x * y) = HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((φ : (a : A) → 𝕜) y : 𝕜)}
    f.toContinuousLinearMap

Tactic:
⟨map_one f, map_mul f⟩

Premises used: Set.Mem, setOf, map_mul, map_one, And.intro
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : CompleteSpace A
inst_3 : NormedAlgebra 𝕜 A
f : A →ₐ[𝕜] 𝕜
⊢ Membership.mem (γ := Set (WeakDual 𝕜 A))
    {φ : WeakDual 𝕜 A |
      Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜) ∧
        ∀ (x y : A),
          (φ : (a : A) → 𝕜) (x * y) = HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((φ : (a : A) → 𝕜) y : 𝕜)}
    f.toContinuousLinearMap

Tactic:
exact ⟨map_one f, map_mul f⟩
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : CompleteSpace A
inst_3 : NormedAlgebra 𝕜 A
f : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
⊢ Eq (α := (a : A) → 𝕜)
    (⇑((equivAlgHom : (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → A →ₐ[𝕜] 𝕜) f : A →ₐ[𝕜] 𝕜) : (a : A) → 𝕜)
    (⇑f : (a : A) → 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : CompleteSpace A
inst_3 : NormedAlgebra 𝕜 A
f : A →ₐ[𝕜] 𝕜
⊢ Eq (α := (a : A) → 𝕜)
    (⇑((Equiv.symm equivAlgHom : (a : A →ₐ[𝕜] 𝕜) → (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) f :
          (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) :
      (a : A) → 𝕜)
    (⇑f : (a : A) → 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
l : Filter ↥S
a : ↥S
ha : IsUnit (↑a : A)
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
rw : Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (Ring.inverse (↑ha.unit : A)))
⊢ Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (↑ha.unit⁻¹ : A))

Tactic:
rw [← Ring.inverse_unit]

Premises used: Ring.inverse_unit