awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜' E F
hp : HasFPowerSeriesAt f p x
⊢ AnalyticAt 𝕜 f x

Tactic:
exact ⟨p.restrictScalars 𝕜, hp.restrictScalars⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
s : Set E
hf : AnalyticOn 𝕜' f s
⊢ AnalyticOn 𝕜 f s

Tactic:
fun x hx ↦ (hf x hx).restrictScalars

Premises used: AnalyticOn, AnalyticWithinAt.restrictScalars
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_9
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
s : Set E
hf : AnalyticOnNhd 𝕜' f s
⊢ AnalyticOnNhd 𝕜 f s

Tactic:
fun x hx ↦ (hf x hx).restrictScalars

Premises used: AnalyticOnNhd, AnalyticAt.restrictScalars
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
simp_rw :
  ∀ (n : ℕ),
    Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ A) A) (formalMultilinearSeries_geometric 𝕜 A n)
      (FormalMultilinearSeries.ofScalars A (fun (x : ℕ) ↦ 1) n)
simp_rw₁ :
  ∀ (n : ℕ),
    formalMultilinearSeries_geometric 𝕜 A n =
      HSMul.hSMul.{u_2, u_7, u_7} (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ A) A) 1
        (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A)
simp_rw₂ :
  ∀ (n : ℕ),
    ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A =
      HSMul.hSMul.{u_2, u_7, u_7} (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ A) A) 1
        (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A)
simp_rw₃ : ∀ (n : ℕ), True
⊢ Eq (α := FormalMultilinearSeries 𝕜 A A) (formalMultilinearSeries_geometric 𝕜 A)
    (FormalMultilinearSeries.ofScalars A fun (x : ℕ) ↦ 1)

Tactic:
simp_rw [FormalMultilinearSeries.ext_iff, FormalMultilinearSeries.ofScalars,
    formalMultilinearSeries_geometric, one_smul, implies_true]

Premises used: FormalMultilinearSeries.ext_iff, one_smul, implies_true, formalMultilinearSeries_geometric, FormalMultilinearSeries.ofScalars
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
n : ℕ
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ A) A) (formalMultilinearSeries_geometric 𝕜 A n) ≤
    max 1 (norm.{u_7} (E := A) 1)

Tactic:
ContinuousMultilinearMap.norm_mkPiAlgebraFin_le

Premises used: ContinuousMultilinearMap.norm_mkPiAlgebraFin_le, formalMultilinearSeries_geometric
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : NormOneClass A
n : ℕ
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ A) A) (formalMultilinearSeries_geometric 𝕜 A n) = 1

Tactic:
ContinuousMultilinearMap.norm_mkPiAlgebraFin

Premises used: formalMultilinearSeries_geometric, ContinuousMultilinearMap.norm_mkPiAlgebraFin
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
⊢ Tendsto (fun (n : ℕ) ↦ norm.{u_2} (E := 𝕜) 1 / norm.{u_2} (E := 𝕜) 1) atTop (𝓝 (↑1 : ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
h : 1 = (↑1⁻¹ : ℝ≥0∞)
⊢ 1 ≤ FormalMultilinearSeries.radius.{u_2, u_7, u_7} (𝕜 := 𝕜) (E := A) (F := A) (formalMultilinearSeries_geometric 𝕜 A)

Tactic:
convert!
    formalMultilinearSeries_geometric_eq_ofScalars 𝕜 A ▸
      FormalMultilinearSeries.inv_le_ofScalars_radius_of_tendsto A _ one_ne_zero (by simp)
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
⊢ 1 = (↑1⁻¹ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : NormOneClass A
⊢ Tendsto (fun (n : ℕ) ↦ norm.{u_2} (E := 𝕜) 1 / norm.{u_2} (E := 𝕜) 1) atTop (𝓝 (↑1 : ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
r_le :
  1 ≤ FormalMultilinearSeries.radius.{u_2, u_7, u_7} (𝕜 := 𝕜) (E := A) (F := A) (formalMultilinearSeries_geometric 𝕜 A)
r_pos : LT.lt (α := ℝ≥0∞) 0 1
hasSum :
  ∀ {y : A},
    Membership.mem (γ := Set A) (Metric.eball 0 1) y →
      HasSum (fun (n : ℕ) ↦ (formalMultilinearSeries_geometric 𝕜 A n : (a : (i : Fin n) → A) → A) fun (x : Fin n) ↦ y)
        (1 - (0 + y))⁻¹ʳ
⊢ HasFPowerSeriesOnBall.{u_2, u_7, u_7} (𝕜 := 𝕜) (F := A) (fun (x : A) ↦ (1 - x)⁻¹ʳ)
    (formalMultilinearSeries_geometric 𝕜 A) 0 1

Tactic:
constructor
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
⊢ 1 ≤ FormalMultilinearSeries.radius.{u_2, u_7, u_7} (𝕜 := 𝕜) (E := A) (F := A) (formalMultilinearSeries_geometric 𝕜 A)

Tactic:
one_le_formalMultilinearSeries_geometric_radius 𝕜 A

Premises used: one_le_formalMultilinearSeries_geometric_radius
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
⊢ 1 ≤ FormalMultilinearSeries.radius.{u_2, u_7, u_7} (𝕜 := 𝕜) (E := A) (F := A) (formalMultilinearSeries_geometric 𝕜 A)

Tactic:
exact one_le_formalMultilinearSeries_geometric_radius 𝕜 A

Premises used: one_le_formalMultilinearSeries_geometric_radius
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
⊢ LT.lt (α := ℝ≥0∞) 0 1

Tactic:
one_pos

Premises used: one_pos
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
⊢ LT.lt (α := ℝ≥0∞) 0 1

Tactic:
exact one_pos

Premises used: one_pos
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
y : A
hy : Membership.mem (γ := Set A) (Metric.eball 0 1) y
⊢ ‖y‖ < 1

Tactic:
simp only [Metric.mem_eball, edist_dist, dist_zero_right, ofReal_lt_one] at hy

Premises used: edist_dist, ENNReal.ofReal_lt_one, dist_zero_right, Metric.mem_eball
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
y : A
hy : ‖y‖ < 1
hasSum : HasSum.{u_7, 0} (α := A) (fun (n : ℕ) ↦ y ^ n) (∑' (n : ℕ), y ^ n)
⊢ HasSum (fun (n : ℕ) ↦ (formalMultilinearSeries_geometric 𝕜 A n : (a : (i : Fin n) → A) → A) fun (x : Fin n) ↦ y)
    (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]

Premises used: ContinuousMultilinearMap.mkPiAlgebraFin_apply, Units.inv_mk, Units.oneSub, zero_add, NormedRing.inverse_one_sub, List.ofFn_const, formalMultilinearSeries_geometric, List.prod_replicate
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
y : A
hy : ‖y‖ < 1
⊢ HasSum.{u_7, 0} (α := A) (fun (n : ℕ) ↦ y ^ n) (∑' (n : ℕ), y ^ n)

Tactic:
(summable_geometric_of_norm_lt_one hy).hasSum

Premises used: Summable.hasSum, summable_geometric_of_norm_lt_one
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
y : A
hy : ‖y‖ < 1
⊢ HasSum.{u_7, 0} (α := A) (fun (n : ℕ) ↦ y ^ n) (∑' (n : ℕ), y ^ n)

Tactic:
exact (summable_geometric_of_norm_lt_one hy).hasSum

Premises used: Summable.hasSum, summable_geometric_of_norm_lt_one
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
⊢ AnalyticAt 𝕜 (F := A) (fun (x : A) ↦ (1 - x)⁻¹ʳ) 0

Tactic:
⟨_, ⟨_, hasFPowerSeriesOnBall_inverse_one_sub 𝕜 A⟩⟩

Premises used: hasFPowerSeriesOnBall_inverse_one_sub, AnalyticAt, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
inl : ∀ (hA : Subsingleton A), AnalyticAt 𝕜 Ring.inverse (↑z : A)
inr : ∀ (hA : Nontrivial A), AnalyticAt 𝕜 Ring.inverse (↑z : A)
⊢ AnalyticAt 𝕜 Ring.inverse (↑z : A)

Tactic:
rcases subsingleton_or_nontrivial A with hA | hA

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Subsingleton A
⊢ AnalyticAt 𝕜 (F := A) (fun (x : A) ↦ 0) (↑z : A)

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

Premises used: analyticAt_const
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Subsingleton A
⊢ AnalyticAt 𝕜 Ring.inverse (↑z : A)

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

Premises used: analyticAt_const
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
ε0 : 0 < ‖(↑z⁻¹ : A)‖⁻¹
⊢ Metric.ball (↑z : A) ‖(↑z⁻¹ : A)‖⁻¹ ∈ 𝓝 (↑z : A)

Tactic:
apply Metric.ball_mem_nhds

Premises used: Metric.ball_mem_nhds
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
⊢ 0 < ‖(↑z⁻¹ : A)‖⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
⊢ Metric.ball (↑z : A) ‖(↑z⁻¹ : A)‖⁻¹ ∈ 𝓝 (↑z : A)

Tactic:
have : Metric.ball (z : A) (‖(↑z⁻¹ : A)‖⁻¹) ∈ 𝓝 (z : A) := by
        apply Metric.ball_mem_nhds
        simp
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
this : Metric.ball (↑z : A) ‖(↑z⁻¹ : A)‖⁻¹ ∈ 𝓝 (↑z : A)
h : ∀ (y : A) (hy : y ∈ Metric.ball (↑z : A) ‖(↑z⁻¹ : A)‖⁻¹), (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ
⊢ ∀ᶠ (y : A) in 𝓝 (↑z : A), (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ

Tactic:
filter_upwards [this] with y hy
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
this : Metric.ball (↑z : A) ‖(↑z⁻¹ : A)‖⁻¹ ∈ 𝓝 (↑z : A)
y : A
hy : y ∈ Metric.ball (↑z : A) ‖(↑z⁻¹ : A)‖⁻¹
⊢ ‖y - (↑z : A)‖ < ‖(↑z⁻¹ : A)‖⁻¹

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

Premises used: dist_eq_norm, Metric.mem_ball
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
this : Metric.ball (↑z : A) ‖(↑z⁻¹ : A)‖⁻¹ ∈ 𝓝 (↑z : A)
y : A
hy : ‖y - (↑z : A)‖ < ‖(↑z⁻¹ : A)‖⁻¹
⊢ y = (↑(z.ofNearby y hy) : A)

Tactic:
have : y = Units.ofNearby z y hy := rfl
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
this_1 : Metric.ball (↑z : A) ‖(↑z⁻¹ : A)‖⁻¹ ∈ 𝓝 (↑z : A)
y : A
hy : ‖y - (↑z : A)‖ < ‖(↑z⁻¹ : A)‖⁻¹
this : y = (↑(z.ofNearby y hy) : A)
h : (↑(z.ofNearby y hy) : A)⁻¹ʳ = (f1 ∘ f2 ∘ f3) (↑(z.ofNearby y hy) : A)
⊢ (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ

Tactic:
rw [this, Eq.comm]

Premises used: Eq.comm
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
this_1 : Metric.ball (↑z : A) ‖(↑z⁻¹ : A)‖⁻¹ ∈ 𝓝 (↑z : A)
y : A
hy : ‖y - (↑z : A)‖ < ‖(↑z⁻¹ : A)‖⁻¹
this : y = (↑(z.ofNearby y hy) : A)
h : (↑(z.ofNearby y hy)⁻¹ : A) = f1 (f2 (f3 (↑(z.ofNearby y hy) : A)))
⊢ (↑(z.ofNearby y hy) : A)⁻¹ʳ = (f1 ∘ f2 ∘ f3) (↑(z.ofNearby y hy) : A)

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

Premises used: Ring.inverse_unit, Function.comp_apply
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
this_1 : Metric.ball (↑z : A) ‖(↑z⁻¹ : A)‖⁻¹ ∈ 𝓝 (↑z : A)
y : A
hy : ‖y - (↑z : A)‖ < ‖(↑z⁻¹ : A)‖⁻¹
this : y = (↑(z.ofNearby y hy) : A)
h : (↑(Units.oneSub (1 - (↑z⁻¹ : A) * y) ⋯)⁻¹ : A) = ((↑z⁻¹ : A) * y)⁻¹ʳ
⊢ (↑(z.ofNearby y hy)⁻¹ : A) = f1 (f2 (f3 (↑(z.ofNearby y hy) : A)))

Tactic:
simp only [Units.ofNearby, Units.add, mul_sub, Units.inv_mul, neg_sub, add_sub_cancel,
        mul_inv_rev, Units.val_mul, Units.val_inv_copy, Units.inv_eq_val_inv, Units.val_copy,
        _root_.sub_sub_cancel, Units.mul_left_inj, f1, f2, f3]

Premises used: neg_sub, Units.ofNearby, mul_sub, Units.val_inv_copy, Units.inv_eq_val_inv, Units.val_copy, Units.inv_mul, sub_sub_cancel, add_sub_cancel, mul_inv_rev, Units.add, Units.mul_left_inj, Units.val_mul
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
this_1 : Metric.ball (↑z : A) ‖(↑z⁻¹ : A)‖⁻¹ ∈ 𝓝 (↑z : A)
y : A
hy : ‖y - (↑z : A)‖ < ‖(↑z⁻¹ : A)‖⁻¹
this : y = (↑(z.ofNearby y hy) : A)
h : (↑(Units.oneSub (1 - (↑z⁻¹ : A) * y) ⋯) : A)⁻¹ʳ = ((↑z⁻¹ : A) * y)⁻¹ʳ
⊢ (↑(Units.oneSub (1 - (↑z⁻¹ : A) * y) ⋯)⁻¹ : A) = ((↑z⁻¹ : A) * y)⁻¹ʳ

Tactic:
rw [← Ring.inverse_unit]

Premises used: Ring.inverse_unit
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
this_1 : Metric.ball (↑z : A) ‖(↑z⁻¹ : A)‖⁻¹ ∈ 𝓝 (↑z : A)
y : A
hy : ‖y - (↑z : A)‖ < ‖(↑z⁻¹ : A)‖⁻¹
this : y = (↑(z.ofNearby y hy) : A)
h : (↑(Units.oneSub (1 - (↑z⁻¹ : A) * y) ⋯) : A) = (↑z⁻¹ : A) * y
⊢ (↑(Units.oneSub (1 - (↑z⁻¹ : A) * y) ⋯) : A)⁻¹ʳ = ((↑z⁻¹ : A) * y)⁻¹ʳ

Tactic:
congr
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
this_1 : Metric.ball (↑z : A) ‖(↑z⁻¹ : A)‖⁻¹ ∈ 𝓝 (↑z : A)
y : A
hy : ‖y - (↑z : A)‖ < ‖(↑z⁻¹ : A)‖⁻¹
this : y = (↑(z.ofNearby y hy) : A)
⊢ (↑(Units.oneSub (1 - (↑z⁻¹ : A) * y) ⋯) : A) = (↑z⁻¹ : A) * y

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
⊢ ∀ᶠ (y : A) in 𝓝 (↑z : A), (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ

Tactic:
have feq : ∀ᶠ y in 𝓝 (z : A), (f1 ∘ f2 ∘ f3) y = 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 only [Units.ofNearby, Units.add, mul_sub, Units.inv_mul, neg_sub, add_sub_cancel,
        mul_inv_rev, Units.val_mul, Units.val_inv_copy, Units.inv_eq_val_inv, Units.val_copy,
        _root_.sub_sub_cancel, Units.mul_left_inj, f1, f2, f3]
      rw [← Ring.inverse_unit]
      congr
      simp
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
feq : ∀ᶠ (y : A) in 𝓝 (↑z : A), (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ
apply : AnalyticAt 𝕜 (f1 ∘ f2 ∘ f3) (↑z : A)
⊢ AnalyticAt 𝕜 Ring.inverse (↑z : A)

Tactic:
apply AnalyticAt.congr _ feq

Premises used: AnalyticAt.congr
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
feq : ∀ᶠ (y : A) in 𝓝 (↑z : A), (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ
apply : AnalyticAt 𝕜 (f2 ∘ f3) (↑z : A)
⊢ AnalyticAt 𝕜 (f1 ∘ f2 ∘ f3) (↑z : A)

Tactic:
apply (analyticAt_id.mul analyticAt_const).comp

Premises used: analyticAt_const, analyticAt_id, AnalyticAt.mul, AnalyticAt.comp
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
feq : ∀ᶠ (y : A) in 𝓝 (↑z : A), (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ
hg : AnalyticAt 𝕜 f2 (f3 (↑z : A))
hf : AnalyticAt 𝕜 f3 (↑z : A)
⊢ AnalyticAt 𝕜 (f2 ∘ f3) (↑z : A)

Tactic:
apply AnalyticAt.comp

Premises used: AnalyticAt.comp
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
feq : ∀ᶠ (y : A) in 𝓝 (↑z : A), (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ
hg : AnalyticAt 𝕜 (F := A) (fun (b : A) ↦ (1 - b)⁻¹ʳ) 0
⊢ AnalyticAt 𝕜 f2 (f3 (↑z : A))

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

Premises used: sub_self, Units.inv_eq_val_inv, Units.inv_mul
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
feq : ∀ᶠ (y : A) in 𝓝 (↑z : A), (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ
⊢ AnalyticAt 𝕜 (F := A) (fun (b : A) ↦ (1 - b)⁻¹ʳ) 0

Tactic:
analyticAt_inverse_one_sub 𝕜 A

Premises used: analyticAt_inverse_one_sub
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
feq : ∀ᶠ (y : A) in 𝓝 (↑z : A), (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ
⊢ AnalyticAt 𝕜 (F := A) (fun (b : A) ↦ (1 - b)⁻¹ʳ) 0

Tactic:
exact analyticAt_inverse_one_sub 𝕜 A

Premises used: analyticAt_inverse_one_sub
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
feq : ∀ᶠ (y : A) in 𝓝 (↑z : A), (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ
⊢ AnalyticAt 𝕜 f3 (↑z : A)

Tactic:
analyticAt_const.sub (analyticAt_const.mul analyticAt_id)

Premises used: analyticAt_const, AnalyticAt.sub, analyticAt_id, AnalyticAt.mul
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun (a : A) ↦ a * z.inv
f2 : A → A := fun (b : A) ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun (c : A) ↦ 1 - z.inv * c
feq : ∀ᶠ (y : A) in 𝓝 (↑z : A), (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ
⊢ AnalyticAt 𝕜 f3 (↑z : A)

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

Premises used: analyticAt_const, AnalyticAt.sub, analyticAt_id, AnalyticAt.mul