-- Mathlib/Analysis/Analytic/Constructions.lean
lemma hasFPowerSeriesOnBall_inverse_one_sub
    (𝕜 : Type*) [NontriviallyNormedField 𝕜]
    (A : Type*) [NormedRing A] [NormedAlgebra 𝕜 A] [HasSummableGeomSeries A] :
    HasFPowerSeriesOnBall (fun x : A ↦ Ring.inverse (1 - x))
      (formalMultilinearSeries_geometric 𝕜 A) 0 1

Proof state:
case r_le
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
⊢ 1 ≤ (formalMultilinearSeries_geometric 𝕜 A).radius

Tactic:
exact one_le_formalMultilinearSeries_geometric_radius 𝕜 A

Result:
no goals

Proof state:
case hasSum
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
y : A
hy : ‖y‖ < 1
⊢ HasSum (fun n => y ^ n) (∑' (n : ℕ), y ^ n)

Tactic:
exact (summable_geometric_of_norm_lt_one hy).hasSum

Result:
no goals

Proof state:
case r_pos
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
⊢ 0 < 1

Tactic:
exact one_pos

Result:
no goals

Proof state:
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
⊢ HasFPowerSeriesOnBall (fun x => Ring.inverse (1 - x)) (formalMultilinearSeries_geometric 𝕜 A) 0 1

Tactic:
constructor

Result:
case r_le
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
⊢ 1 ≤ (formalMultilinearSeries_geometric 𝕜 A).radius

case r_pos
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
⊢ 0 < 1

case hasSum
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
⊢ ∀ {y : A},
    y ∈ EMetric.ball 0 1 →
      HasSum (fun n => (formalMultilinearSeries_geometric 𝕜 A n) fun x => y) (Ring.inverse (1 - (0 + y)))

Proof state:
case hasSum
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
⊢ ∀ {y : A},
    y ∈ EMetric.ball 0 1 →
      HasSum (fun n => (formalMultilinearSeries_geometric 𝕜 A n) fun x => y) (Ring.inverse (1 - (0 + y)))

Tactic:
intro y hy

Result:
case hasSum
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
y : A
hy : y ∈ EMetric.ball 0 1
⊢ HasSum (fun n => (formalMultilinearSeries_geometric 𝕜 A n) fun x => y) (Ring.inverse (1 - (0 + y)))

Proof state:
case hasSum
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
y : A
hy : ‖y‖ < 1
⊢ HasSum (fun n => (formalMultilinearSeries_geometric 𝕜 A n) fun x => y) (Ring.inverse (1 - (0 + y)))

Tactic:
simp only [zero_add, NormedRing.inverse_one_sub _ hy, Units.oneSub, Units.inv_mk,
  formalMultilinearSeries_geometric, ContinuousMultilinearMap.mkPiAlgebraFin_apply,
  List.ofFn_const, List.prod_replicate]

Result:
case hasSum
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
y : A
hy : ‖y‖ < 1
⊢ HasSum (fun n => y ^ n) (∑' (n : ℕ), y ^ n)

Proof state:
case hasSum
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
y : A
hy : y ∈ EMetric.ball 0 1
⊢ HasSum (fun n => (formalMultilinearSeries_geometric 𝕜 A n) fun x => y) (Ring.inverse (1 - (0 + y)))

Tactic:
simp only [EMetric.mem_ball, edist_dist, dist_zero_right, ofReal_lt_one] at hy

Result:
case hasSum
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
y : A
hy : ‖y‖ < 1
⊢ HasSum (fun n => (formalMultilinearSeries_geometric 𝕜 A n) fun x => y) (Ring.inverse (1 - (0 + y)))