-- Mathlib/Analysis/Analytic/Constructions.lean
/-- If `A` is a normed algebra over `𝕜` with summable geometric series, then inversion on `A` is
analytic at any unit. -/
@[fun_prop]
lemma analyticAt_inverse {𝕜 : Type*} [NontriviallyNormedField 𝕜]
    {A : Type*} [NormedRing A] [NormedAlgebra 𝕜 A] [HasSummableGeomSeries A] (z : Aˣ) :
    AnalyticAt 𝕜 Ring.inverse (z : A)

Proof state:
case inr
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun a => a * z.inv
f2 : A → A := fun b => Ring.inverse (1 - b)
f3 : A → A := fun c => 1 - z.inv * c
⊢ AnalyticAt 𝕜 Ring.inverse ↑z

Tactic:
have feq : ∀ᶠ y in 𝓝 (z : A), (f1 ∘ f2 ∘ f3) y = Ring.inverse y := by
  have : Metric.ball (z : A) (‖(↑z⁻¹ : A)‖⁻¹) ∈ 𝓝 (z : A) := by
    apply Metric.ball_mem_nhds
    simp
  filter_upwards [this] with y hy
  simp only [Metric.mem_ball, dist_eq_norm] at hy
  have : y = Units.ofNearby z y hy := rfl
  rw [this, Eq.comm]
  simp only [Ring.inverse_unit, Function.comp_apply]
  simp [Units.ofNearby, f1, f2, f3, Units.add, _root_.mul_sub]
  rw [← Ring.inverse_unit]
  congr
  simp

Result:
case inr
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun a => a * z.inv
f2 : A → A := fun b => Ring.inverse (1 - b)
f3 : A → A := fun c => 1 - z.inv * c
feq : ∀ᶠ (y : A) in 𝓝 ↑z, (f1 ∘ f2 ∘ f3) y = Ring.inverse y
⊢ AnalyticAt 𝕜 Ring.inverse ↑z

Proof state:
case inr
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun a => a * z.inv
⊢ AnalyticAt 𝕜 Ring.inverse ↑z

Tactic:
let f2 : A → A := fun b ↦ Ring.inverse (1 - b)

Result:
case inr
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun a => a * z.inv
f2 : A → A := fun b => Ring.inverse (1 - b)
⊢ AnalyticAt 𝕜 Ring.inverse ↑z

Proof state:
case h
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun a => a * z.inv
f2 : A → A := fun b => Ring.inverse (1 - b)
f3 : A → A := fun c => 1 - z.inv * c
this : Metric.ball ↑z ‖↑z⁻¹‖⁻¹ ∈ 𝓝 ↑z
y : A
hy : y ∈ Metric.ball ↑z ‖↑z⁻¹‖⁻¹
⊢ (f1 ∘ f2 ∘ f3) y = Ring.inverse y

Tactic:
simp only [Metric.mem_ball, dist_eq_norm] at hy

Result:
case h
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun a => a * z.inv
f2 : A → A := fun b => Ring.inverse (1 - b)
f3 : A → A := fun c => 1 - z.inv * c
this : Metric.ball ↑z ‖↑z⁻¹‖⁻¹ ∈ 𝓝 ↑z
y : A
hy : ‖y - ↑z‖ < ‖↑z⁻¹‖⁻¹
⊢ (f1 ∘ f2 ∘ f3) y = Ring.inverse y

Proof state:
case hg
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun a => a * z.inv
f2 : A → A := fun b => Ring.inverse (1 - b)
f3 : A → A := fun c => 1 - z.inv * c
feq : ∀ᶠ (y : A) in 𝓝 ↑z, (f1 ∘ f2 ∘ f3) y = Ring.inverse y
⊢ AnalyticAt 𝕜 f2 (f3 ↑z)

Tactic:
simp only [Units.inv_eq_val_inv, Units.inv_mul, sub_self, f2, f3]

Result:
case hg
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun a => a * z.inv
f2 : A → A := fun b => Ring.inverse (1 - b)
f3 : A → A := fun c => 1 - z.inv * c
feq : ∀ᶠ (y : A) in 𝓝 ↑z, (f1 ∘ f2 ∘ f3) y = Ring.inverse y
⊢ AnalyticAt 𝕜 (fun b => Ring.inverse (1 - b)) 0