-- 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
feq : ∀ᶠ (y : A) in 𝓝 ↑z, (f1 ∘ f2 ∘ f3) y = Ring.inverse y
⊢ AnalyticAt 𝕜 Ring.inverse ↑z

Tactic:
apply AnalyticAt.congr _ feq

Result:
𝕜 : 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 𝕜 (f1 ∘ f2 ∘ f3) ↑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
⊢ AnalyticAt 𝕜 Ring.inverse ↑z

Tactic:
let f1 : A → A := fun a ↦ a * z.inv

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
⊢ 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
⊢ ∀ᶠ (y : A) in 𝓝 ↑z, (f1 ∘ f2 ∘ f3) y = Ring.inverse y

Tactic:
have : Metric.ball (z : A) (‖(↑z⁻¹ : A)‖⁻¹) ∈ 𝓝 (z : A) := by
  apply Metric.ball_mem_nhds
  simp

Result:
𝕜 : 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

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⁻¹‖⁻¹
⊢ (f1 ∘ f2 ∘ f3) y = Ring.inverse y

Tactic:
have : y = Units.ofNearby z y hy := rfl

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)
⊢ (f1 ∘ f2 ∘ f3) y = Ring.inverse y

Proof state:
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

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

Tactic:
rw [← Ring.inverse_unit]

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 ↑(Units.oneSub (1 - ↑z⁻¹ * y) ⋯) = Ring.inverse (↑z⁻¹ * 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 𝕜 (fun b => Ring.inverse (1 - b)) 0

Tactic:
exact analyticAt_inverse_one_sub 𝕜 A

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
feq : ∀ᶠ (y : A) in 𝓝 ↑z, (f1 ∘ f2 ∘ f3) y = Ring.inverse y
⊢ AnalyticAt 𝕜 (f1 ∘ f2 ∘ f3) ↑z

Tactic:
apply (analyticAt_id.mul analyticAt_const).comp

Result:
𝕜 : 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

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

Tactic:
simp [Units.ofNearby, f1, f2, f3, Units.add, _root_.mul_sub]

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

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

Tactic:
rcases subsingleton_or_nontrivial A with hA|hA

Result:
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

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