-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem exp_mem_exp [RCLike 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : A)
    {z : 𝕜} (hz : z ∈ spectrum 𝕜 a) : exp 𝕜 z ∈ spectrum 𝕜 (exp 𝕜 a)

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n => (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)
⊢ exp 𝕜 (a - ↑ₐ z) = 1 + (a - ↑ₐ z) * b

Tactic:
rw [exp_eq_tsum]

Result:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n => (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)
⊢ (fun x => ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n) (a - ↑ₐ z) = 1 + (a - ↑ₐ z) * b

Proof state:
case h
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
n : ℕ
hn : n ≠ 0
⊢ ‖(↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n‖ ≤ ‖a - ↑ₐ z‖ ^ n / ↑n.factorial

Tactic:
rw [norm_smul, mul_comm, norm_inv, RCLike.norm_natCast, ← div_eq_mul_inv]

Result:
case h
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
n : ℕ
hn : n ≠ 0
⊢ ‖(a - ↑ₐ z) ^ n‖ / ↑(n + 1).factorial ≤ ‖a - ↑ₐ z‖ ^ n / ↑n.factorial

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n => (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)
⊢ (fun x => ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n) (a - ↑ₐ z) = 1 + (a - ↑ₐ z) * b

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

Result:
case h.e'_3.h.e'_5
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n => (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)
⊢ 1 = (↑(Nat.factorial 0))⁻¹ • (a - ↑ₐ z) ^ 0

case h.e'_3.h.e'_6
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n => (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)
⊢ (a - ↑ₐ z) * b = ∑' (b : ℕ), (↑(b + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (b + 1)

Proof state:
case h.e'_3.h.e'_6
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n => (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)
⊢ (a - ↑ₐ z) * b = ∑' (b : ℕ), (↑(b + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (b + 1)

Tactic:
exact h₀.symm

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
⊢ exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)

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

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
⊢ exp 𝕜 z ∈ spectrum 𝕜 (exp 𝕜 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]

Result:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)
⊢ exp 𝕜 z ∈ spectrum 𝕜 (exp 𝕜 a)

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
⊢ exp 𝕜 z ∈ spectrum 𝕜 (exp 𝕜 a)

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]
  exact div_le_div₀ (pow_nonneg (norm_nonneg _) n) (norm_pow_le' (a - ↑ₐ z) (zero_lt_iff.mpr hn))
    (mod_cast Nat.factorial_pos n) (mod_cast Nat.factorial_le (lt_add_one n).le)

Result:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n => (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
⊢ exp 𝕜 z ∈ spectrum 𝕜 (exp 𝕜 a)

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n => (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)
h₃ : exp 𝕜 (a - ↑ₐ z) = 1 + (a - ↑ₐ z) * b
⊢ ¬((IsUnit (a - ↑ₐ z) ∧ IsUnit b) ∧ IsUnit (↑ₐ (exp 𝕜 z)))

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

Result:
no goals