awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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 (F := A)
    (fun (x : A) ↦ resolvent (R := A) x (((↑(↑(algebraMap 𝕜 A) : 𝕜 →* A) : OneHom 𝕜 A) : OneHom 𝕜 A).1 k))
    ((((((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 :
      A)
    a

Tactic:
hasFDerivAt_resolvent (𝕜 := A) hk |>.hasDerivAt

Premises used: spectrum.hasFDerivAt_resolvent, HasFDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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
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
⊢ HasDerivAt (fun (x : A) ↦ resolvent x k) (HPow.hPow (β := ℕ) (resolvent a k) 2) a

Tactic:
convert! hasFDerivAt_resolvent (𝕜 := A) hk |>.hasDerivAt

Premises used: spectrum.hasFDerivAt_resolvent, HasFDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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
⊢ 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:
simp [resolvent, pow_two]

Premises used: pow_two, resolvent
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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
h : DifferentiableAt.{u_1, u_1, u_2} 𝕜 (F := A) (fun (z : 𝕜) ↦ (1 - z • a)⁻¹ʳ) z
⊢ DifferentiableWithinAt.{u_1, u_1, u_2} 𝕜 (F := A) (fun (z : 𝕜) ↦ (1 - z • a)⁻¹ʳ) (Metric.closedBall 0 (↑r : ℝ)) z

Tactic:
apply DifferentiableAt.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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)

Tactic:
isUnit_one_sub_smul_of_lt_inv_radius (lt_of_le_of_lt (coe_mono ?_) hr)

Premises used: lt_of_le_of_lt, spectrum.isUnit_one_sub_smul_of_lt_inv_radius, ENNReal.coe_mono
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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
refine : ‖z‖₊ ≤ r
⊢ IsUnit (1 - z • a)

Tactic:
refine isUnit_one_sub_smul_of_lt_inv_radius (lt_of_le_of_lt (coe_mono ?_) hr)

Premises used: lt_of_le_of_lt, spectrum.isUnit_one_sub_smul_of_lt_inv_radius, ENNReal.coe_mono
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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
⊢ ‖z‖₊ ≤ r

Tactic:
simpa only [norm_toNNReal, Real.toNNReal_coe] using
      Real.toNNReal_mono (mem_closedBall_zero_iff.mp z_mem)

Premises used: Real.toNNReal_mono, Iff.mp, Real.toNNReal_coe, mem_closedBall_zero_iff, norm_toNNReal
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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)

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)
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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)
⊢ 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
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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)
H₁ : Differentiable.{u_1, u_1, u_2} 𝕜 (F := A) fun (w : 𝕜) ↦ 1 - w • a
⊢ DifferentiableAt.{u_1, u_1, u_2} 𝕜 (F := A) (fun (z : 𝕜) ↦ (1 - z • a)⁻¹ʳ) z

Tactic:
DifferentiableAt.comp z (differentiableAt_inverse hu) H₁.differentiableAt

Premises used: Differentiable.differentiableAt, Ring.inverse, dite, DifferentiableAt.comp
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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)
H₁ : Differentiable.{u_1, u_1, u_2} 𝕜 (F := A) fun (w : 𝕜) ↦ 1 - w • a
⊢ DifferentiableAt.{u_1, u_1, u_2} 𝕜 (F := A) (fun (z : 𝕜) ↦ (1 - z • a)⁻¹ʳ) z

Tactic:
exact DifferentiableAt.comp z (differentiableAt_inverse hu) H₁.differentiableAt

Premises used: Differentiable.differentiableAt, DifferentiableAt.comp
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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

Tactic:
ENNReal.inv_le_inv.mp (le_of_forall_pos_nnreal_lt fun r r_pos r_lt => ?_)

Premises used: ENNReal.le_of_forall_pos_nnreal_lt, ENNReal.inv_le_inv, Iff.mp
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
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)⁻¹
⊢ limsup (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop ≤ spectralRadius ℂ a

Tactic:
refine ENNReal.inv_le_inv.mp (le_of_forall_pos_nnreal_lt fun r r_pos r_lt => ?_)

Premises used: ENNReal.le_of_forall_pos_nnreal_lt, ENNReal.inv_le_inv, Iff.mp
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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)⁻¹
simp_rw : (↑r : ℝ≥0∞) ≤ liminf (fun (i : ℕ) ↦ 1 / (↑‖a ^ i‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ)) atTop
⊢ (↑r : ℝ≥0∞) ≤ (limsup (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop)⁻¹

Tactic:
simp_rw [inv_limsup, ← one_div]

Premises used: one_div, ENNReal.inv_limsup
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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∞) ≤ FormalMultilinearSeries.radius.{0, 0, u_2} (𝕜 := ℂ) (E := ℂ) (F := A) p

Tactic:
h
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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
h₁ :
  liminf (fun (i : ℕ) ↦ 1 / (↑‖a ^ i‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ)) atTop =
    FormalMultilinearSeries.radius.{0, 0, u_2} (𝕜 := ℂ) (E := ℂ) (F := A) p
⊢ (↑r : ℝ≥0∞) ≤ liminf (fun (i : ℕ) ↦ 1 / (↑‖a ^ i‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ)) atTop

Tactic:
convert! h
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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
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)
⊢ liminf (fun (i : ℕ) ↦ 1 / (↑‖a ^ i‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ)) atTop =
    FormalMultilinearSeries.radius.{0, 0, u_2} (𝕜 := ℂ) (E := ℂ) (F := A) p

Tactic:
simp only [p, p.radius_eq_liminf, ← norm_toNNReal, norm_mkPiRing]

Premises used: ContinuousMultilinearMap.norm_mkPiRing, norm_toNNReal, FormalMultilinearSeries.radius_eq_liminf
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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
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∞)
⊢ 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:
congr
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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
h₁ :
  ∀ (n : ℕ),
    1 / (↑‖a ^ n‖.toNNReal : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
      1 / (↑(‖a ^ n‖.toNNReal ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)
⊢ 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:
ext n
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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 : ℕ
h₁ : ¬(‖a ^ n‖₊ = 0 ∧ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) < 0)
⊢ 1 / (↑‖a ^ n‖.toNNReal : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    1 / (↑(‖a ^ n‖.toNNReal ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)

Tactic:
rw [norm_toNNReal, ENNReal.coe_rpow_def ‖a ^ n‖₊ (1 / n : ℝ), if_neg]

Premises used: NNNorm.nnnorm, HDiv.hDiv, Nat.cast, HPow.hPow, ENNReal.coe_rpow_def, OfNat.ofNat, norm_toNNReal, if_neg
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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 : ℕ
⊢ ¬(‖a ^ n‖₊ = 0 ∧ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) < 0)

Tactic:
fun ha => (lt_self_iff_false _).mp
      (ha.2.trans_le (one_div_nonneg.mpr n.cast_nonneg : 0 ≤ (1 / n : ℝ)))

Premises used: Iff.mpr, Nat.cast_nonneg, one_div_nonneg, HDiv.hDiv, Nat.cast, And.right, LT.lt.trans_le, lt_self_iff_false, Iff.mp, OfNat.ofNat, Not
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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 : ℕ
⊢ ¬(‖a ^ n‖₊ = 0 ∧ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) < 0)

Tactic:
exact fun ha => (lt_self_iff_false _).mp
      (ha.2.trans_le (one_div_nonneg.mpr n.cast_nonneg : 0 ≤ (1 / n : ℝ)))

Premises used: lt_self_iff_false, Iff.mp
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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)
suffices : (↑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

Tactic:
suffices h : (r : ℝ≥0∞) ≤ p.radius by
    convert! h
    simp only [p, p.radius_eq_liminf, ← norm_toNNReal, norm_mkPiRing]
    congr
    ext n
    rw [norm_toNNReal, ENNReal.coe_rpow_def ‖a ^ n‖₊ (1 / n : ℝ), if_neg]
    exact fun ha => (lt_self_iff_false _).mp
      (ha.2.trans_le (one_div_nonneg.mpr n.cast_nonneg : 0 ≤ (1 / n : ℝ)))
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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)
⊢ HasFPowerSeriesOnBall.{0, 0, u_2} (F := A) (fun (z : ℂ) ↦ (1 - z • a)⁻¹ʳ)
    (cauchyPowerSeries (fun (z : ℂ) ↦ (1 - z • a)⁻¹ʳ) 0 (↑r : ℝ)) 0 (↑r : ℝ≥0∞)

Tactic:
have H₁ := (differentiableOn_inverse_one_sub_smul r_lt).hasFPowerSeriesOnBall r_pos
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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₁ :
  HasFPowerSeriesOnBall.{0, 0, u_2} (F := A) (fun (z : ℂ) ↦ (1 - z • a)⁻¹ʳ)
    (cauchyPowerSeries (fun (z : ℂ) ↦ (1 - z • a)⁻¹ʳ) 0 (↑r : ℝ)) 0 (↑r : ℝ≥0∞)
⊢ (↑r : ℝ≥0∞) ≤ FormalMultilinearSeries.radius.{0, 0, u_2} (𝕜 := ℂ) (E := ℂ) (F := A) p

Tactic:
((hasFPowerSeriesOnBall_inverse_one_sub_smul ℂ a).exchange_radius H₁).r_le

Premises used: spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul, HasFPowerSeriesOnBall.r_le, Complex, HasFPowerSeriesOnBall.exchange_radius
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
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₁ :
  HasFPowerSeriesOnBall.{0, 0, u_2} (F := A) (fun (z : ℂ) ↦ (1 - z • a)⁻¹ʳ)
    (cauchyPowerSeries (fun (z : ℂ) ↦ (1 - z • a)⁻¹ʳ) 0 (↑r : ℝ)) 0 (↑r : ℝ≥0∞)
⊢ (↑r : ℝ≥0∞) ≤ FormalMultilinearSeries.radius.{0, 0, u_2} (𝕜 := ℂ) (E := ℂ) (F := A) p

Tactic:
exact ((hasFPowerSeriesOnBall_inverse_one_sub_smul ℂ a).exchange_radius H₁).r_le

Premises used: spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul, HasFPowerSeriesOnBall.r_le, Complex, HasFPowerSeriesOnBall.exchange_radius
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
⊢ Tendsto (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop (𝓝 (spectralRadius ℂ a))

Tactic:
tendsto_of_le_liminf_of_limsup_le (spectralRadius_le_liminf_pow_nnnorm_pow_one_div ℂ a)
    (limsup_pow_nnnorm_pow_one_div_le_spectralRadius a)

Premises used: spectrum.spectralRadius_le_liminf_pow_nnnorm_pow_one_div, spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius, Complex, tendsto_of_le_liminf_of_limsup_le
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
⊢ Tendsto (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop (𝓝 (spectralRadius ℂ a))

Tactic:
pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius a

Premises used: spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
h :
  Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (‖a ^ n‖ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))) fun (n : ℕ) ↦
    (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
⊢ Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal (‖a ^ n‖ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))) atTop (𝓝 (spectralRadius ℂ a))

Tactic:
convert! pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius a using 1

Premises used: spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
h :
  ∀ (x : ℕ),
    ENNReal.ofReal (‖a ^ x‖ ^ HDiv.hDiv (α := ℝ) 1 (↑x : ℝ)) = (↑‖a ^ x‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑x : ℝ)
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (‖a ^ n‖ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))) fun (n : ℕ) ↦
    (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
ext1
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
x : ℕ
rw : 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑x : ℝ)
⊢ ENNReal.ofReal (‖a ^ x‖ ^ HDiv.hDiv (α := ℝ) 1 (↑x : ℝ)) = (↑‖a ^ x‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑x : ℝ)

Tactic:
rw [← ofReal_rpow_of_nonneg (norm_nonneg _) _, ← coe_nnnorm, coe_nnreal_eq]

Premises used: ENNReal.ofReal_rpow_of_nonneg, coe_nnnorm, ENNReal.coe_nnreal_eq, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
x : ℕ
⊢ 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑x : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
by_contra! : ∀ (h : spectrum ℂ a = ∅), False
⊢ (spectrum ℂ a).Nonempty

Tactic:
by_contra! h
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
h : spectrum ℂ a = ∅
rwa : ∀ (h : (resolventSet ℂ a)ᶜ = ∅), resolventSet ℂ a = Set.univ
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : resolventSet ℂ a = Set.univ), resolventSet ℂ a = Set.univ
⊢ resolventSet ℂ a = Set.univ

Tactic:
rwa [spectrum, Set.compl_empty_iff] at h

Premises used: spectrum, Set.compl_empty_iff
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
h : spectrum ℂ a = ∅
⊢ resolventSet ℂ a = Set.univ

Tactic:
have H₀ : resolventSet ℂ a = Set.univ := by rwa [spectrum, Set.compl_empty_iff] at h
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
⊢ Differentiable.{0, 0, u_2} ℂ (F := A) fun (z : ℂ) ↦ resolvent a z

Tactic:
have H₁ : Differentiable ℂ fun z : ℂ => resolvent a z := fun z =>
    hasDerivAt_resolvent_const_left (H₀.symm ▸ Set.mem_univ z : z ∈ resolventSet ℂ a)
      |>.differentiableAt
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
H₁ : Differentiable.{0, 0, u_2} ℂ (F := A) fun (z : ℂ) ↦ resolvent a z
⊢ Tendsto.{0, u_2} (β := A) (fun (z : ℂ) ↦ resolvent a z) (cocompact ℂ) (𝓝 0)

Tactic:
simpa [Metric.cobounded_eq_cocompact] using resolvent_tendsto_cobounded a (𝕜 := ℂ)

Premises used: Metric.cobounded_eq_cocompact, spectrum.resolvent_tendsto_cobounded
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
H₁ : Differentiable.{0, 0, u_2} ℂ (F := A) fun (z : ℂ) ↦ resolvent a z
⊢ resolvent (R := ℂ) a 0 = 0

Tactic:
have H₃ := H₁.apply_eq_of_tendsto_cocompact 0 <| by
    simpa [Metric.cobounded_eq_cocompact] using resolvent_tendsto_cobounded a (𝕜 := ℂ)
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
H₁ : Differentiable.{0, 0, u_2} ℂ (F := A) fun (z : ℂ) ↦ resolvent a z
H₃ : resolvent (R := ℂ) a 0 = 0
⊢ False

Tactic:
not_isUnit_zero <| H₃ ▸ (isUnit_resolvent.mp <| H₀.symm ▸ Set.mem_univ 0)

Premises used: not_isUnit_zero
-- Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
inst_3 : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
H₁ : Differentiable.{0, 0, u_2} ℂ (F := A) fun (z : ℂ) ↦ resolvent a z
H₃ : resolvent (R := ℂ) a 0 = 0
⊢ False

Tactic:
exact not_isUnit_zero <| H₃ ▸ (isUnit_resolvent.mp <| H₀.symm ▸ Set.mem_univ 0)

Premises used: not_isUnit_zero