-- 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 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⁻¹‖⁻¹
this : y = ↑(z.ofNearby y hy)
⊢ Ring.inverse ↑(z.ofNearby y hy) = (f1 ∘ f2 ∘ f3) ↑(z.ofNearby y hy)

Tactic:
simp only [Ring.inverse_unit, Function.comp_apply]

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⁻¹‖⁻¹
this : y = ↑(z.ofNearby y hy)
⊢ ↑(z.ofNearby y hy)⁻¹ = f1 (f2 (f3 ↑(z.ofNearby y hy)))

Proof state:
case inl
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
z : Aˣ
hA : Subsingleton A
⊢ AnalyticAt 𝕜 Ring.inverse ↑z

Tactic:
convert analyticAt_const (v := (0 : A))

Result:
no goals

Proof state:
case hf
𝕜 : 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 𝕜 f3 ↑z

Tactic:
exact analyticAt_const.sub (analyticAt_const.mul analyticAt_id)

Result:
no goals

Proof state:
𝕜 : 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) in 𝓝 ↑z, (f1 ∘ f2 ∘ f3) y = Ring.inverse y

Tactic:
filter_upwards [this] with y 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 ∈ Metric.ball ↑z ‖↑z⁻¹‖⁻¹
⊢ (f1 ∘ f2 ∘ f3) y = Ring.inverse y

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)
⊢ AnalyticAt 𝕜 Ring.inverse ↑z

Tactic:
let f3 : A → A := fun c ↦ 1 - z.inv * c

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
⊢ AnalyticAt 𝕜 Ring.inverse ↑z

Proof state:
𝕜 : 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
⊢ Metric.ball ↑z ‖↑z⁻¹‖⁻¹ ∈ 𝓝 ↑z

Tactic:
apply Metric.ball_mem_nhds

Result:
case ε0
𝕜 : 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
⊢ 0 < ‖↑z⁻¹‖⁻¹

Proof state:
𝕜 : 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:
apply AnalyticAt.comp

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 𝕜 f2 (f3 ↑z)

case hf
𝕜 : 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 𝕜 f3 ↑z

Proof state:
case ε0
𝕜 : 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
⊢ 0 < ‖↑z⁻¹‖⁻¹

Tactic:
simp

Result:
no goals

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 - ↑z‖ < ‖↑z⁻¹‖⁻¹
this : y = ↑(z.ofNearby y hy)
⊢ (f1 ∘ f2 ∘ f3) y = Ring.inverse y

Tactic:
rw [this, Eq.comm]

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⁻¹‖⁻¹
this : y = ↑(z.ofNearby y hy)
⊢ Ring.inverse ↑(z.ofNearby y hy) = (f1 ∘ f2 ∘ f3) ↑(z.ofNearby y hy)

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 - ↑z‖ < ‖↑z⁻¹‖⁻¹
this : y = ↑(z.ofNearby y hy)
⊢ Ring.inverse ↑(Units.oneSub (1 - ↑z⁻¹ * y) ⋯) = Ring.inverse (↑z⁻¹ * y)

Tactic:
congr

Result:
case h.e_a
𝕜 : 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⁻¹‖⁻¹
this : y = ↑(z.ofNearby y hy)
⊢ ↑(Units.oneSub (1 - ↑z⁻¹ * y) ⋯) = ↑z⁻¹ * y