awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
n : ℕ
⊢ AnalyticWithinAt 𝕜 (f ^ n) s z
have zero : AnalyticWithinAt 𝕜 (HPow.hPow (β := ℕ) f 0) s z
Tactic: induction n with
  | zero =>
    simp only [pow_zero]
    apply analyticWithinAt_const
  | succ m hm =>
    simp only [pow_succ]
    exact hm.mul hf
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
n : ℕ
zero : AnalyticWithinAt 𝕜 (HPow.hPow (β := ℕ) f 0) s z
⊢ AnalyticWithinAt 𝕜 (f ^ n) s z
have succ : ∀ (m : ℕ) (hm : AnalyticWithinAt 𝕜 (f ^ m) s z), AnalyticWithinAt 𝕜 (f ^ (m + 1)) s z
Tactic: induction n with
  | zero =>
    simp only [pow_zero]
    apply analyticWithinAt_const
  | succ m hm =>
    simp only [pow_succ]
    exact hm.mul hf
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_7
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f : E → A
z : E
hf : AnalyticAt 𝕜 f z
n : ℕ
⊢ AnalyticAt 𝕜 (f ^ n) z
have rw : ∀ (hf : AnalyticWithinAt 𝕜 f Set.univ z) (n : ℕ), AnalyticWithinAt 𝕜 (f ^ n) Set.univ z
Tactic: rw [← analyticWithinAt_univ] at hf ⊢
Cleared hypotheses: hf, n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕝 : Type u_8
inst_3 : NormedDivisionRing 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
s : Set E
n : ℤ
hf : AnalyticOnNhd 𝕜 f s
hn : 0 ≤ n
⊢ AnalyticOnNhd 𝕜 (f ^ n) s
have simp_rw : AnalyticOnNhd 𝕜 (HPow.hPow (β := ℕ) f (OfNat.ofNat n.toNat)) s
Tactic: simp_rw [(Eq.symm (Int.toNat_of_nonneg hn) : n = OfNat.ofNat n.toNat), zpow_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
p : FormalMultilinearSeries 𝕜' E F
x : E
s : Set E
hf : HasFPowerSeriesWithinAt f p s x
⊢ HasFPowerSeriesWithinAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) s x
have rcases : ∀ (r : ℝ≥0∞) (hr : HasFPowerSeriesWithinOnBall f p s x r),
  HasFPowerSeriesWithinAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) s x
Tactic: rcases hf with ⟨r, hr⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
p : FormalMultilinearSeries 𝕜' E F
x : E
hf : HasFPowerSeriesAt f p x
⊢ HasFPowerSeriesAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) x
have rcases : ∀ (r : ℝ≥0∞) (hr : HasFPowerSeriesOnBall f p x r), HasFPowerSeriesAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) x
Tactic: rcases hf with ⟨r, hr⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
s : Set E
hf : AnalyticWithinAt 𝕜' f s x
⊢ AnalyticWithinAt 𝕜 f s x
have rcases : ∀ (p : FormalMultilinearSeries 𝕜' E F) (hp : HasFPowerSeriesWithinAt f p s x), AnalyticWithinAt 𝕜 f s x
Tactic: rcases hf with ⟨p, hp⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
hf : AnalyticAt 𝕜' f x
⊢ AnalyticAt 𝕜 f x
have rcases : ∀ (p : FormalMultilinearSeries 𝕜' E F) (hp : HasFPowerSeriesAt f p x), AnalyticAt 𝕜 f x
Tactic: rcases hf with ⟨p, hp⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
⊢ Eq (α := FormalMultilinearSeries 𝕜 A A) (formalMultilinearSeries_geometric 𝕜 A)
    (FormalMultilinearSeries.ofScalars A fun (x : ℕ) ↦ 1)
have simp_rw : ∀ (n : ℕ),
  Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ A) A) (formalMultilinearSeries_geometric 𝕜 A n)
    (FormalMultilinearSeries.ofScalars A (fun (x : ℕ) ↦ 1) n)
Tactic: simp_rw [FormalMultilinearSeries.ext_iff, FormalMultilinearSeries.ofScalars,
    formalMultilinearSeries_geometric, one_smul, implies_true]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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)
⊢ Eq (α := FormalMultilinearSeries 𝕜 A A) (formalMultilinearSeries_geometric 𝕜 A)
    (FormalMultilinearSeries.ofScalars A fun (x : ℕ) ↦ 1)
have 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)
Tactic: simp_rw [FormalMultilinearSeries.ext_iff, FormalMultilinearSeries.ofScalars,
    formalMultilinearSeries_geometric, one_smul, implies_true]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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)
⊢ Eq (α := FormalMultilinearSeries 𝕜 A A) (formalMultilinearSeries_geometric 𝕜 A)
    (FormalMultilinearSeries.ofScalars A fun (x : ℕ) ↦ 1)
have 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)
Tactic: simp_rw [FormalMultilinearSeries.ext_iff, FormalMultilinearSeries.ofScalars,
    formalMultilinearSeries_geometric, one_smul, implies_true]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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)
⊢ Eq (α := FormalMultilinearSeries 𝕜 A A) (formalMultilinearSeries_geometric 𝕜 A)
    (FormalMultilinearSeries.ofScalars A fun (x : ℕ) ↦ 1)
have simp_rw₃ : ∀ (n : ℕ), True
Tactic: simp_rw [FormalMultilinearSeries.ext_iff, FormalMultilinearSeries.ofScalars,
    formalMultilinearSeries_geometric, one_smul, implies_true]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
⊢ 1 ≤ FormalMultilinearSeries.radius.{u_2, u_7, u_7} (𝕜 := 𝕜) (E := A) (F := A) (formalMultilinearSeries_geometric 𝕜 A)
have h : 1 = (↑1⁻¹ : ℝ≥0∞)
Tactic: convert!
    formalMultilinearSeries_geometric_eq_ofScalars 𝕜 A ▸
      FormalMultilinearSeries.inv_le_ofScalars_radius_of_tendsto A _ one_ne_zero (by simp)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
⊢ HasFPowerSeriesOnBall.{u_2, u_7, u_7} (𝕜 := 𝕜) (F := A) (fun (x : A) ↦ (1 - x)⁻¹ʳ)
    (formalMultilinearSeries_geometric 𝕜 A) 0 1
have r_le : 1 ≤ FormalMultilinearSeries.radius.{u_2, u_7, u_7} (𝕜 := 𝕜) (E := A) (F := A) (formalMultilinearSeries_geometric 𝕜 A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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)
⊢ HasFPowerSeriesOnBall.{u_2, u_7, u_7} (𝕜 := 𝕜) (F := A) (fun (x : A) ↦ (1 - x)⁻¹ʳ)
    (formalMultilinearSeries_geometric 𝕜 A) 0 1
have r_pos : LT.lt (α := ℝ≥0∞) 0 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ HasFPowerSeriesOnBall.{u_2, u_7, u_7} (𝕜 := 𝕜) (F := A) (fun (x : A) ↦ (1 - x)⁻¹ʳ)
    (formalMultilinearSeries_geometric 𝕜 A) 0 1
have 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))⁻¹ʳ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (hypothesis)
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
⊢ HasSum (fun (n : ℕ) ↦ (formalMultilinearSeries_geometric 𝕜 A n : (a : (i : Fin n) → A) → A) fun (x : Fin n) ↦ y)
    (1 - (0 + y))⁻¹ʳ
have hy₁ : ‖y‖ < 1
Tactic: simp only [Metric.mem_eball, edist_dist, dist_zero_right, ofReal_lt_one] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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 (fun (n : ℕ) ↦ (formalMultilinearSeries_geometric 𝕜 A n : (a : (i : Fin n) → A) → A) fun (x : Fin n) ↦ y)
    (1 - (0 + y))⁻¹ʳ
have hasSum : HasSum.{u_7, 0} (α := A) (fun (n : ℕ) ↦ y ^ n) (∑' (n : ℕ), y ^ n)
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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
A : Type u_7
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
z : Aˣ
⊢ AnalyticAt 𝕜 Ring.inverse (↑z : A)
have inl : ∀ (hA : Subsingleton A), AnalyticAt 𝕜 Ring.inverse (↑z : A)
Tactic: rcases subsingleton_or_nontrivial A with hA | hA
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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)
⊢ AnalyticAt 𝕜 Ring.inverse (↑z : A)
have inr : ∀ (hA : Nontrivial A), AnalyticAt 𝕜 Ring.inverse (↑z : A)
Tactic: rcases subsingleton_or_nontrivial A with hA | hA
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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)
have ε0 : 0 < ‖(↑z⁻¹ : A)‖⁻¹
Tactic: apply Metric.ball_mem_nhds
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (hypothesis)
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⁻¹ʳ
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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) in 𝓝 (↑z : A), (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ
have h : ∀ (y : A) (hy : y ∈ Metric.ball (↑z : A) ‖(↑z⁻¹ : A)‖⁻¹), (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ
Tactic: filter_upwards [this] with y hy
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (hypothesis)
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)‖⁻¹
⊢ (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ
have hy₁ : ‖y - (↑z : A)‖ < ‖(↑z⁻¹ : A)‖⁻¹
Tactic: simp only [Metric.mem_ball, dist_eq_norm] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (hypothesis)
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)‖⁻¹
⊢ (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ
have this₁ : y = (↑(z.ofNearby y hy) : A)
Tactic: have : y = Units.ofNearby z y hy := rfl
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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)
⊢ (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ
have h : (↑(z.ofNearby y hy) : A)⁻¹ʳ = (f1 ∘ f2 ∘ f3) (↑(z.ofNearby y hy) : A)
Tactic: rw [this, Eq.comm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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)
⊢ (↑(z.ofNearby y hy) : A)⁻¹ʳ = (f1 ∘ f2 ∘ f3) (↑(z.ofNearby y hy) : A)
have h : (↑(z.ofNearby y hy)⁻¹ : A) = f1 (f2 (f3 (↑(z.ofNearby y hy) : A)))
Tactic: simp only [Ring.inverse_unit, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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)
⊢ (↑(z.ofNearby y hy)⁻¹ : A) = f1 (f2 (f3 (↑(z.ofNearby y hy) : A)))
have h : (↑(Units.oneSub (1 - (↑z⁻¹ : A) * y) sorry)⁻¹ : A) = ((↑z⁻¹ : A) * y)⁻¹ʳ
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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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)⁻¹ʳ
have h : (↑(Units.oneSub (1 - (↑z⁻¹ : A) * y) sorry) : A)⁻¹ʳ = ((↑z⁻¹ : A) * y)⁻¹ʳ
Tactic: rw [← Ring.inverse_unit]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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)⁻¹ʳ
have h : (↑(Units.oneSub (1 - (↑z⁻¹ : A) * y) sorry) : A) = (↑z⁻¹ : A) * y
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (hypothesis)
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
⊢ AnalyticAt 𝕜 Ring.inverse (↑z : A)
have feq : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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 𝕜 Ring.inverse (↑z : A)
have apply : AnalyticAt 𝕜 (f1 ∘ f2 ∘ f3) (↑z : A)
Tactic: apply AnalyticAt.congr _ feq
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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 𝕜 (f1 ∘ f2 ∘ f3) (↑z : A)
have apply : AnalyticAt 𝕜 (f2 ∘ f3) (↑z : A)
Tactic: apply (analyticAt_id.mul analyticAt_const).comp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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 𝕜 (f2 ∘ f3) (↑z : A)
have hg : AnalyticAt 𝕜 f2 (f3 (↑z : A))
Tactic: apply AnalyticAt.comp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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))
⊢ AnalyticAt 𝕜 (f2 ∘ f3) (↑z : A)
have hf : AnalyticAt 𝕜 f3 (↑z : A)
Tactic: apply AnalyticAt.comp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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 𝕜 f2 (f3 (↑z : A))
have hg : AnalyticAt 𝕜 (F := A) (fun (b : A) ↦ (1 - b)⁻¹ʳ) 0
Tactic: simp only [Units.inv_eq_val_inv, Units.inv_mul, sub_self, f2, f3]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst_1 : NormedDivisionRing 𝕝
inst_2 : NormedAlgebra 𝕜 𝕝
⊢ HasFPowerSeriesOnBall.{u_2, u_8, u_8} (𝕜 := 𝕜) (F := 𝕝) (fun (x : 𝕝) ↦ (1 - x)⁻¹)
    (formalMultilinearSeries_geometric 𝕜 𝕝) 0 1
have h : ∀ (x : 𝕝), Eq.{u_8 + 1} (α := 𝕝 → 𝕝) Inv.inv Ring.inverse
Tactic: convert! hasFPowerSeriesOnBall_inverse_one_sub 𝕜 𝕝