-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem differentiableOn_inverse_one_sub_smul [CompleteSpace A] {a : A} {r : ℝ≥0}
    (hr : (r : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹) :
    DifferentiableOn 𝕜 (fun z : 𝕜 => Ring.inverse (1 - z • a)) (Metric.closedBall 0 r)

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
hr : ↑r < (spectralRadius 𝕜 a)⁻¹
⊢ DifferentiableOn 𝕜 (fun z => Ring.inverse (1 - z • a)) (Metric.closedBall 0 ↑r)

Tactic:
intro z z_mem

Result:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
hr : ↑r < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : z ∈ Metric.closedBall 0 ↑r
⊢ DifferentiableWithinAt 𝕜 (fun z => Ring.inverse (1 - z • a)) (Metric.closedBall 0 ↑r) z

Proof state:
case h
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
hr : ↑r < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : z ∈ Metric.closedBall 0 ↑r
⊢ DifferentiableAt 𝕜 (fun z => Ring.inverse (1 - z • a)) z

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)

Result:
case h
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
hr : ↑r < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : z ∈ Metric.closedBall 0 ↑r
hu : IsUnit (1 - z • a)
⊢ DifferentiableAt 𝕜 (fun z => Ring.inverse (1 - z • a)) z

Proof state:
case h
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
hr : ↑r < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : z ∈ Metric.closedBall 0 ↑r
hu : IsUnit (1 - z • a)
⊢ DifferentiableAt 𝕜 (fun z => Ring.inverse (1 - z • a)) z

Tactic:
have H₁ : Differentiable 𝕜 fun w : 𝕜 => 1 - w • a := (differentiable_id.smul_const a).const_sub 1

Result:
case h
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
hr : ↑r < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : z ∈ Metric.closedBall 0 ↑r
hu : IsUnit (1 - z • a)
H₁ : Differentiable 𝕜 fun w => 1 - w • a
⊢ DifferentiableAt 𝕜 (fun z => Ring.inverse (1 - z • a)) z

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
hr : ↑r < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : z ∈ Metric.closedBall 0 ↑r
⊢ ‖z‖₊ ≤ r

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

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
hr : ↑r < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : z ∈ Metric.closedBall 0 ↑r
⊢ IsUnit (1 - z • a)

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

Result:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
hr : ↑r < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : z ∈ Metric.closedBall 0 ↑r
⊢ ‖z‖₊ ≤ r

Proof state:
case h
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
hr : ↑r < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : z ∈ Metric.closedBall 0 ↑r
hu : IsUnit (1 - z • a)
H₁ : Differentiable 𝕜 fun w => 1 - w • a
⊢ DifferentiableAt 𝕜 (fun z => Ring.inverse (1 - z • a)) z

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

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
hr : ↑r < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : z ∈ Metric.closedBall 0 ↑r
⊢ DifferentiableWithinAt 𝕜 (fun z => Ring.inverse (1 - z • a)) (Metric.closedBall 0 ↑r) z

Tactic:
apply DifferentiableAt.differentiableWithinAt

Result:
case h
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
hr : ↑r < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : z ∈ Metric.closedBall 0 ↑r
⊢ DifferentiableAt 𝕜 (fun z => Ring.inverse (1 - z • a)) z