awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
n : ℕ
ih : exp (n • x) = exp x ^ n
succ : exp (n • x + x) = exp x ^ (n + 1)
⊢ exp ((n + 1) • x) = exp x ^ (n + 1)
have succ₁ : exp (n • x + x) = exp x ^ n * exp x
Tactic: rw [succ_nsmul, pow_succ, exp_add_of_commute ((Commute.refl x).smul_left n), ih]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
n : ℕ
ih : exp (n • x) = exp x ^ n
succ : exp (n • x + x) = exp x ^ (n + 1)
succ₁ : exp (n • x + x) = exp x ^ n * exp x
⊢ exp ((n + 1) • x) = exp x ^ (n + 1)
have succ₂ : exp (n • x) * exp x = exp x ^ n * exp x
Tactic: rw [succ_nsmul, pow_succ, exp_add_of_commute ((Commute.refl x).smul_left n), ih]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
n : ℕ
ih : exp (n • x) = exp x ^ n
succ : exp (n • x + x) = exp x ^ (n + 1)
succ₁ : exp (n • x + x) = exp x ^ n * exp x
succ₂ : exp (n • x) * exp x = exp x ^ n * exp x
⊢ exp ((n + 1) • x) = exp x ^ (n + 1)
have succ₃ : exp x ^ n * exp x = exp x ^ n * exp x
Tactic: rw [succ_nsmul, pow_succ, exp_add_of_commute ((Commute.refl x).smul_left n), ih]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
n : ℕ
x : 𝔸
⊢ exp (n • x) = exp x ^ n
have zero : exp (HSMul.hSMul (α := ℕ) 0 x) = HPow.hPow (β := ℕ) (exp x) 0
Tactic: induction n with
  | zero => rw [zero_smul, pow_zero, exp_zero]
  | succ n ih => rw [succ_nsmul, pow_succ, exp_add_of_commute ((Commute.refl x).smul_left n), ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
n : ℕ
x : 𝔸
zero : exp (HSMul.hSMul (α := ℕ) 0 x) = HPow.hPow (β := ℕ) (exp x) 0
⊢ exp (n • x) = exp x ^ n
have succ : ∀ (n : ℕ) (ih : exp (n • x) = exp x ^ n), exp ((n + 1) • x) = exp x ^ (n + 1)
Tactic: induction n with
  | zero => rw [zero_smul, pow_zero, exp_zero]
  | succ n ih => rw [succ_nsmul, pow_succ, exp_add_of_commute ((Commute.refl x).smul_left n), ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
ι : Type u_3
𝔸 : ι → Type u_4
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → NormedRing (𝔸 i)
inst_3 : (i : ι) → NormedAlgebra ℚ (𝔸 i)
inst_4 : ∀ (i : ι), CompleteSpace.{u_4} (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
⊢ Function.update (β := 𝔸) (exp x) j (exp xj) = exp (Function.update (β := 𝔸) x j xj)
have h : ∀ (i : ι), Function.update (β := 𝔸) (exp x) j (exp xj) i = exp (Function.update (β := 𝔸) x j xj) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
ι : Type u_3
𝔸 : ι → Type u_4
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → NormedRing (𝔸 i)
inst_3 : (i : ι) → NormedAlgebra ℚ (𝔸 i)
inst_4 : ∀ (i : ι), CompleteSpace.{u_4} (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
i : ι
⊢ Function.update (β := 𝔸) (exp x) j (exp xj) i = exp (Function.update (β := 𝔸) x j xj) i
have h : Function.update (β := 𝔸) (fun (i : ι) ↦ exp (x i)) j (exp xj) i = exp (Function.update (β := 𝔸) x j xj i)
Tactic: simp_rw [Pi.exp_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
z : ℤ
x : 𝔸
⊢ exp (z • x) = exp x ^ z
have inl : ∀ (n : ℕ), exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) x) = HPow.hPow (β := ℤ) (exp x) (↑n : ℤ)
Tactic: obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
z : ℤ
x : 𝔸
inl : ∀ (n : ℕ), exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) x) = HPow.hPow (β := ℤ) (exp x) (↑n : ℤ)
⊢ exp (z • x) = exp x ^ z
have inr : ∀ (n : ℕ), exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = HPow.hPow (β := ℤ) (exp x) (-(↑n : ℤ))
Tactic: obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
n : ℕ
⊢ exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) x) = HPow.hPow (β := ℤ) (exp x) (↑n : ℤ)
have inl : exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) x) = exp x ^ n
Tactic: rw [zpow_natCast, natCast_zsmul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
n : ℕ
inl : exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) x) = exp x ^ n
⊢ exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) x) = HPow.hPow (β := ℤ) (exp x) (↑n : ℤ)
have inl₁ : exp (n • x) = exp x ^ n
Tactic: rw [zpow_natCast, natCast_zsmul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
n : ℕ
inl : exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) x) = exp x ^ n
inl₁ : exp (n • x) = exp x ^ n
⊢ exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) x) = HPow.hPow (β := ℤ) (exp x) (↑n : ℤ)
have inl₂ : exp x ^ n = exp x ^ n
Tactic: rw [zpow_natCast, natCast_zsmul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
n : ℕ
⊢ exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = HPow.hPow (β := ℤ) (exp x) (-(↑n : ℤ))
have inr : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = (HPow.hPow (β := ℤ) (exp x) (↑n : ℤ))⁻¹
Tactic: rw [zpow_neg, zpow_natCast, neg_smul, exp_neg, natCast_zsmul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
n : ℕ
inr : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = (HPow.hPow (β := ℤ) (exp x) (↑n : ℤ))⁻¹
⊢ exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = HPow.hPow (β := ℤ) (exp x) (-(↑n : ℤ))
have inr₁ : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = (exp x ^ n)⁻¹
Tactic: rw [zpow_neg, zpow_natCast, neg_smul, exp_neg, natCast_zsmul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
n : ℕ
inr : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = (HPow.hPow (β := ℤ) (exp x) (↑n : ℤ))⁻¹
inr₁ : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = (exp x ^ n)⁻¹
⊢ exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = HPow.hPow (β := ℤ) (exp x) (-(↑n : ℤ))
have inr₂ : exp (-HSMul.hSMul (α := ℤ) (↑n : ℤ) x) = (exp x ^ n)⁻¹
Tactic: rw [zpow_neg, zpow_natCast, neg_smul, exp_neg, natCast_zsmul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
n : ℕ
inr : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = (HPow.hPow (β := ℤ) (exp x) (↑n : ℤ))⁻¹
inr₁ : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = (exp x ^ n)⁻¹
inr₂ : exp (-HSMul.hSMul (α := ℤ) (↑n : ℤ) x) = (exp x ^ n)⁻¹
⊢ exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = HPow.hPow (β := ℤ) (exp x) (-(↑n : ℤ))
have inr₃ : (exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) x))⁻¹ = (exp x ^ n)⁻¹
Tactic: rw [zpow_neg, zpow_natCast, neg_smul, exp_neg, natCast_zsmul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
n : ℕ
inr : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = (HPow.hPow (β := ℤ) (exp x) (↑n : ℤ))⁻¹
inr₁ : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = (exp x ^ n)⁻¹
inr₂ : exp (-HSMul.hSMul (α := ℤ) (↑n : ℤ) x) = (exp x ^ n)⁻¹
inr₃ : (exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) x))⁻¹ = (exp x ^ n)⁻¹
⊢ exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = HPow.hPow (β := ℤ) (exp x) (-(↑n : ℤ))
have inr₄ : (exp (n • x))⁻¹ = (exp x ^ n)⁻¹
Tactic: rw [zpow_neg, zpow_natCast, neg_smul, exp_neg, natCast_zsmul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_1
inst : NormedDivisionRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
x : 𝔸
n : ℕ
inr : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = (HPow.hPow (β := ℤ) (exp x) (↑n : ℤ))⁻¹
inr₁ : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = (exp x ^ n)⁻¹
inr₂ : exp (-HSMul.hSMul (α := ℤ) (↑n : ℤ) x) = (exp x ^ n)⁻¹
inr₃ : (exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) x))⁻¹ = (exp x ^ n)⁻¹
inr₄ : (exp (n • x))⁻¹ = (exp x ^ n)⁻¹
⊢ exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) = HPow.hPow (β := ℤ) (exp x) (-(↑n : ℤ))
have inr₅ : (exp x ^ n)⁻¹ = (exp x ^ n)⁻¹
Tactic: rw [zpow_neg, zpow_natCast, neg_smul, exp_neg, natCast_zsmul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : NormedCommRing 𝔸
inst_1 : NormedAlgebra ℚ 𝔸
inst_2 : CompleteSpace 𝔸
ι : Type u_3
s : Finset ι
f : ι → 𝔸
⊢ Eq.{u_2 + 1} (α := 𝔸) (exp (∑ i ∈ s, f i)) (∏ i ∈ s, exp (f i))
have h : (↑s : Set ι).Pairwise (Function.onFun Commute f)
Tactic: rw [exp_sum_of_commute, Finset.noncommProd_eq_prod]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst : Field 𝕂
inst_1 : Field 𝕂'
inst_2 : Ring 𝔸
inst_3 : Algebra 𝕂 𝔸
inst_4 : Algebra 𝕂' 𝔸
inst_5 : TopologicalSpace 𝔸
inst_6 : IsTopologicalRing 𝔸
n : ℕ
x : 𝔸
⊢ Eq (α := 𝔸) ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x : 𝔸)
    ((expSeries 𝕂' 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x : 𝔸)
have rw : HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) =
  (expSeries 𝕂' 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x
Tactic: rw [expSeries_apply_eq, expSeries_apply_eq, inv_natCast_smul_eq 𝕂 𝕂']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst : Field 𝕂
inst_1 : Field 𝕂'
inst_2 : Ring 𝔸
inst_3 : Algebra 𝕂 𝔸
inst_4 : Algebra 𝕂' 𝔸
inst_5 : TopologicalSpace 𝔸
inst_6 : IsTopologicalRing 𝔸
n : ℕ
x : 𝔸
rw :
  HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) =
    (expSeries 𝕂' 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x
⊢ Eq (α := 𝔸) ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x : 𝔸)
    ((expSeries 𝕂' 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x : 𝔸)
have rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) = HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕂') (↑n ! : 𝕂')⁻¹ (x ^ n)
Tactic: rw [expSeries_apply_eq, expSeries_apply_eq, inv_natCast_smul_eq 𝕂 𝕂']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst : Field 𝕂
inst_1 : Field 𝕂'
inst_2 : Ring 𝔸
inst_3 : Algebra 𝕂 𝔸
inst_4 : Algebra 𝕂' 𝔸
inst_5 : TopologicalSpace 𝔸
inst_6 : IsTopologicalRing 𝔸
n : ℕ
x : 𝔸
rw :
  HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) =
    (expSeries 𝕂' 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x
rw₁ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕂') (↑n ! : 𝕂')⁻¹ (x ^ n)
⊢ Eq (α := 𝔸) ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x : 𝔸)
    ((expSeries 𝕂' 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x : 𝔸)
have rw₂ : HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕂') (↑n ! : 𝕂')⁻¹ (x ^ n) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕂') (↑n ! : 𝕂')⁻¹ (x ^ n)
Tactic: rw [expSeries_apply_eq, expSeries_apply_eq, inv_natCast_smul_eq 𝕂 𝕂']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
⊢ HasDerivAt (resolvent a) (-HPow.hPow (β := ℕ) (resolvent a k) 2) k
have H₁ : HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕜) Ring.inverse
  (-(((ContinuousLinearMap.mulLeftRight 𝕜 A : (a : A) → A →L[𝕜] A →L[𝕜] A) (↑(IsUnit.unit hk)⁻¹ : A) :
          A →L[𝕜] A →L[𝕜] A) :
        (a : A) → A →L[𝕜] A)
      (↑(IsUnit.unit hk)⁻¹ : A))
  (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a)
Tactic: have H₁ : HasFDerivAt Ring.inverse _ (algebraMap 𝕜 A k - a) :=
    hasFDerivAt_ringInverse (𝕜 := 𝕜) hk.unit
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
H₁ :
  HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕜) Ring.inverse
    (-(((ContinuousLinearMap.mulLeftRight 𝕜 A : (a : A) → A →L[𝕜] A →L[𝕜] A) (↑(IsUnit.unit hk)⁻¹ : A) :
            A →L[𝕜] A →L[𝕜] A) :
          (a : A) → A →L[𝕜] A)
        (↑(IsUnit.unit hk)⁻¹ : A))
    (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a)
⊢ HasDerivAt (resolvent a) (-HPow.hPow (β := ℕ) (resolvent a k) 2) k
have H₂ : HasDerivAt.{u_1, u_2} (F := A) (fun (k : 𝕜) ↦ HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a) 1 k
Tactic: have H₂ : HasDerivAt (fun k => algebraMap 𝕜 A k - a) 1 k := by
    simpa using (Algebra.linearMap 𝕜 A).hasDerivAt.sub_const a
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
⊢ HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕜) (F := A) (fun (x : A) ↦ resolvent x k)
    ((((ContinuousLinearMap.mulLeftRight 𝕜 A : (a : A) → A →L[𝕜] A →L[𝕜] A) (resolvent a k) : A →L[𝕜] A →L[𝕜] A) :
        (a : A) → A →L[𝕜] A)
      (resolvent a k))
    a
have H₁ : HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕜) Ring.inverse
  (-(((ContinuousLinearMap.mulLeftRight 𝕜 A : (a : A) → A →L[𝕜] A →L[𝕜] A) (↑(IsUnit.unit hk)⁻¹ : A) :
          A →L[𝕜] A →L[𝕜] A) :
        (a : A) → A →L[𝕜] A)
      (↑(IsUnit.unit hk)⁻¹ : A))
  (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a)
Tactic: have H₁ : HasFDerivAt Ring.inverse _ (algebraMap 𝕜 A k - a) :=
    hasFDerivAt_ringInverse (𝕜 := 𝕜) hk.unit
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
H₁ :
  HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕜) Ring.inverse
    (-(((ContinuousLinearMap.mulLeftRight 𝕜 A : (a : A) → A →L[𝕜] A →L[𝕜] A) (↑(IsUnit.unit hk)⁻¹ : A) :
            A →L[𝕜] A →L[𝕜] A) :
          (a : A) → A →L[𝕜] A)
        (↑(IsUnit.unit hk)⁻¹ : A))
    (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a)
⊢ HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕜) (F := A) (fun (x : A) ↦ resolvent x k)
    ((((ContinuousLinearMap.mulLeftRight 𝕜 A : (a : A) → A →L[𝕜] A →L[𝕜] A) (resolvent a k) : A →L[𝕜] A →L[𝕜] A) :
        (a : A) → A →L[𝕜] A)
      (resolvent a k))
    a
have H₂ : HasFDerivAt (fun (a : A) ↦ HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A) a) (-ContinuousLinearMap.id 𝕜 A) a
Tactic: have H₂ : HasFDerivAt (fun a => algebraMap 𝕜 A k - a) (- .id 𝕜 A) a := by
    simpa using (hasFDerivAt_const _ a).sub (hasFDerivAt_id a)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
⊢ HasDerivAt (fun (x : A) ↦ resolvent x k) (HPow.hPow (β := ℕ) (resolvent a k) 2) a
have h : HPow.hPow (β := ℕ) (resolvent a k) 2 =
  (((((ContinuousLinearMap.mulLeftRight A A : (a : A) → A →L[A] A →L[A] A)
                (resolvent (R := A) a (((↑(↑(algebraMap 𝕜 A) : 𝕜 →* A) : OneHom 𝕜 A) : OneHom 𝕜 A).1 k)) :
              A →L[A] A →L[A] A) :
            (a : A) → A →L[A] A)
          (resolvent (R := A) a (((↑(↑(algebraMap 𝕜 A) : 𝕜 →* A) : OneHom 𝕜 A) : OneHom 𝕜 A).1 k)) :
        A →L[A] A) :
      (a : A) → A)
    1
Tactic: convert! hasFDerivAt_resolvent (𝕜 := A) hk |>.hasDerivAt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (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
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 (↑r : ℝ)) z
⊢ DifferentiableWithinAt.{u_1, u_1, u_2} 𝕜 (F := A) (fun (z : 𝕜) ↦ (1 - z • a)⁻¹ʳ) (Metric.closedBall 0 (↑r : ℝ)) z
have h : DifferentiableAt.{u_1, u_1, u_2} 𝕜 (F := A) (fun (z : 𝕜) ↦ (1 - z • a)⁻¹ʳ) z
Tactic: apply DifferentiableAt.differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (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
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 (↑r : ℝ)) z
⊢ IsUnit (1 - z • a)
have refine : ‖z‖₊ ≤ r
Tactic: refine isUnit_one_sub_smul_of_lt_inv_radius (lt_of_le_of_lt (coe_mono ?_) hr)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 (↑r : ℝ)) z
⊢ DifferentiableAt.{u_1, u_1, u_2} 𝕜 (F := A) (fun (z : 𝕜) ↦ (1 - z • a)⁻¹ʳ) z
have hu : IsUnit (1 - z • a)
Tactic: have hu : IsUnit (1 - z • a) := by
    refine isUnit_one_sub_smul_of_lt_inv_radius (lt_of_le_of_lt (coe_mono ?_) hr)
    simpa only [norm_toNNReal, Real.toNNReal_coe] using
      Real.toNNReal_mono (mem_closedBall_zero_iff.mp z_mem)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 (↑r : ℝ)) z
hu : IsUnit (1 - z • a)
⊢ DifferentiableAt.{u_1, u_1, u_2} 𝕜 (F := A) (fun (z : 𝕜) ↦ (1 - z • a)⁻¹ʳ) z
have H₁ : Differentiable.{u_1, u_1, u_2} 𝕜 (F := A) fun (w : 𝕜) ↦ 1 - w • a
Tactic: have H₁ : Differentiable 𝕜 fun w : 𝕜 => 1 - w • a := (differentiable_id.smul_const a).const_sub 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
⊢ limsup (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop ≤ spectralRadius ℂ a
have refine : ∀ (r : ℝ≥0) (r_pos : 0 < r) (r_lt : (↑r : ℝ≥0∞) < (spectralRadius ℂ a)⁻¹),
  (↑r : ℝ≥0∞) ≤ (limsup (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop)⁻¹
Tactic: refine ENNReal.inv_le_inv.mp (le_of_forall_pos_nnreal_lt fun r r_pos r_lt => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : (↑r : ℝ≥0∞) < (spectralRadius ℂ a)⁻¹
⊢ (↑r : ℝ≥0∞) ≤ (limsup (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop)⁻¹
have simp_rw : (↑r : ℝ≥0∞) ≤ liminf (fun (i : ℕ) ↦ 1 / (↑‖a ^ i‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ)) atTop
Tactic: simp_rw [inv_limsup, ← one_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : (↑r : ℝ≥0∞) < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun (n : ℕ) ↦ ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : (↑r : ℝ≥0∞) ≤ FormalMultilinearSeries.radius.{0, 0, u_2} (𝕜 := ℂ) (E := ℂ) (F := A) p
⊢ (↑r : ℝ≥0∞) ≤ liminf (fun (i : ℕ) ↦ 1 / (↑‖a ^ i‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ)) atTop
have h₁ : liminf (fun (i : ℕ) ↦ 1 / (↑‖a ^ i‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ)) atTop =
  FormalMultilinearSeries.radius.{0, 0, u_2} (𝕜 := ℂ) (E := ℂ) (F := A) p
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : (↑r : ℝ≥0∞) < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun (n : ℕ) ↦ ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : (↑r : ℝ≥0∞) ≤ FormalMultilinearSeries.radius.{0, 0, u_2} (𝕜 := ℂ) (E := ℂ) (F := A) p
⊢ liminf (fun (i : ℕ) ↦ 1 / (↑‖a ^ i‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ)) atTop =
    FormalMultilinearSeries.radius.{0, 0, u_2} (𝕜 := ℂ) (E := ℂ) (F := A) p
have h₁ : Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ 1 / (↑‖a ^ i‖.toNNReal : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ)) atTop)
  (liminf (fun (n : ℕ) ↦ 1 / (↑(‖a ^ n‖.toNNReal ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop)
Tactic: simp only [p, p.radius_eq_liminf, ← norm_toNNReal, norm_mkPiRing]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : (↑r : ℝ≥0∞) < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun (n : ℕ) ↦ ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : (↑r : ℝ≥0∞) ≤ FormalMultilinearSeries.radius.{0, 0, u_2} (𝕜 := ℂ) (E := ℂ) (F := A) p
⊢ Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ 1 / (↑‖a ^ i‖.toNNReal : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ)) atTop)
    (liminf (fun (n : ℕ) ↦ 1 / (↑(‖a ^ n‖.toNNReal ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop)
have h₁ : Eq (α := ℕ → ℝ≥0∞) (fun (i : ℕ) ↦ 1 / (↑‖a ^ i‖.toNNReal : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ)) fun (n : ℕ) ↦
  1 / (↑(‖a ^ n‖.toNNReal ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : (↑r : ℝ≥0∞) < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun (n : ℕ) ↦ ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : (↑r : ℝ≥0∞) ≤ FormalMultilinearSeries.radius.{0, 0, u_2} (𝕜 := ℂ) (E := ℂ) (F := A) p
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (i : ℕ) ↦ 1 / (↑‖a ^ i‖.toNNReal : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ)) fun (n : ℕ) ↦
    1 / (↑(‖a ^ n‖.toNNReal ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)
have h₁ : ∀ (n : ℕ),
  1 / (↑‖a ^ n‖.toNNReal : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    1 / (↑(‖a ^ n‖.toNNReal ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandFormula (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : (↑r : ℝ≥0∞) < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun (n : ℕ) ↦ ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : (↑r : ℝ≥0∞) ≤ FormalMultilinearSeries.radius.{0, 0, u_2} (𝕜 := ℂ) (E := ℂ) (F := A) p
n : ℕ
⊢ 1 / (↑‖a ^ n‖.toNNReal : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    1 / (↑(‖a ^ n‖.toNNReal ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)
have h₁ : ¬(‖a ^ n‖₊ = 0 ∧ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) < 0)
Tactic: rw [norm_toNNReal, ENNReal.coe_rpow_def ‖a ^ n‖₊ (1 / n : ℝ), if_neg]