awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
j : ℕ
h : j ∈ Ico 2 (n + 1)
i_1 : Composition j
h_1 : Membership.mem (γ := Finset (Composition j)) (Set.toFinset {c : Composition j | 1 < c.length}) i_1
⊢ ‖p.compAlongComposition (p.rightInv i x) i_1‖ ≤
    C * r ^ i_1.length *
      ∏ j_1 : Fin i_1.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (i_1.blocksFun j_1)) ↦ F) E)
          (p.rightInv i x (i_1.blocksFun j_1))
have bc : norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i_1.length) ↦ E) F) (p i_1.length) *
    ∏ i_2 : Fin i_1.length,
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (i_1.blocksFun i_2)) ↦ F) E)
        (p.rightInv i x (i_1.blocksFun i_2)) ≤
  C * r ^ i_1.length *
    ∏ j_1 : Fin i_1.length,
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (i_1.blocksFun j_1)) ↦ F) E)
        (p.rightInv i x (i_1.blocksFun j_1))
Tactic: apply (compAlongComposition_norm _ _ _).trans
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
j : ℕ
h : j ∈ Ico 2 (n + 1)
i_1 : Composition j
h_1 : Membership.mem (γ := Finset (Composition j)) (Set.toFinset {c : Composition j | 1 < c.length}) i_1
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i_1.length) ↦ E) F) (p i_1.length) *
      ∏ i_2 : Fin i_1.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (i_1.blocksFun i_2)) ↦ F) E)
          (p.rightInv i x (i_1.blocksFun i_2)) ≤
    C * r ^ i_1.length *
      ∏ j_1 : Fin i_1.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (i_1.blocksFun j_1)) ↦ F) E)
          (p.rightInv i x (i_1.blocksFun j_1))
have bc : norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i_1.length) ↦ E) F) (p i_1.length) ≤
  C * r ^ i_1.length
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
⊢ a * ‖(↑i.symm : F →L[𝕜] E)‖ +
      ∑ k ∈ Ico 2 (n + 1),
        a ^ k *
          (I *
            ∑ c ∈ Set.toFinset {c : Composition k | 1 < c.length},
              C * r ^ c.length *
                ∏ j : Fin c.length,
                  norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (c.blocksFun j)) ↦ F) E)
                    (p.rightInv i x (c.blocksFun j))) =
    I * a +
      I * C *
        ∑ k ∈ Ico 2 (n + 1),
          a ^ k *
            ∑ c ∈ Set.toFinset {c : Composition k | 1 < c.length},
              r ^ c.length *
                ∏ j : Fin c.length,
                  norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (c.blocksFun j)) ↦ F) E)
                    (p.rightInv i x (c.blocksFun j))
have simp_rw : ‖(↑i.symm : F →L[𝕜] E)‖ * a +
    ‖(↑i.symm : F →L[𝕜] E)‖ *
      (C *
        ∑ i_1 ∈ Ico 2 (n + 1),
          a ^ i_1 *
            ∑ i_2 ∈ Set.toFinset {c : Composition i_1 | 1 < c.length},
              r ^ i_2.length *
                ∏ j : Fin i_2.length,
                  norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (i_2.blocksFun j)) ↦ F) E)
                    (p.rightInv i x (i_2.blocksFun j))) =
  ‖(↑i.symm : F →L[𝕜] E)‖ * a +
    C *
      (‖(↑i.symm : F →L[𝕜] E)‖ *
        ∑ k ∈ Ico 2 (n + 1),
          a ^ k *
            ∑ c ∈ Set.toFinset {c : Composition k | 1 < c.length},
              r ^ c.length *
                ∏ j : Fin c.length,
                  norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (c.blocksFun j)) ↦ F) E)
                    (p.rightInv i x (c.blocksFun j)))
Tactic: simp_rw [I, mul_assoc C, ← mul_sum, ← mul_assoc, mul_comm _ ‖(i.symm : F →L[𝕜] E)‖,
        mul_assoc, ← mul_sum, ← mul_assoc, mul_comm _ C, mul_assoc, ← mul_sum]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
⊢ I * a +
      I * C *
        ∑ k ∈ Ico 2 (n + 1),
          a ^ k *
            ∑ c ∈ Set.toFinset {c : Composition k | 1 < c.length},
              r ^ c.length *
                ∏ j : Fin c.length,
                  norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (c.blocksFun j)) ↦ F) E)
                    (p.rightInv i x (c.blocksFun j)) ≤
    I * a + I * C * ∑ k ∈ Ico 2 (n + 1), (r * ∑ j ∈ Ico 1 n, a ^ j * ‖p.rightInv i x j‖) ^ k
have bc : LE.le (α := ℝ)
  (∑ k ∈ Ico 2 (n + 1),
    a ^ k *
      ∑ c ∈ Set.toFinset {c : Composition k | 1 < c.length},
        r ^ c.length *
          ∏ j : Fin c.length,
            norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (c.blocksFun j)) ↦ F) E)
              (p.rightInv i x (c.blocksFun j)))
  (∑ k ∈ Ico 2 (n + 1), (r * ∑ j ∈ Ico 1 n, a ^ j * ‖p.rightInv i x j‖) ^ k)
Tactic: gcongr _ + _ * _ * ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
⊢ LE.le (α := ℝ)
    (∑ k ∈ Ico 2 (n + 1),
      a ^ k *
        ∑ c ∈ Set.toFinset {c : Composition k | 1 < c.length},
          r ^ c.length *
            ∏ j : Fin c.length,
              norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (c.blocksFun j)) ↦ F) E)
                (p.rightInv i x (c.blocksFun j)))
    (∑ k ∈ Ico 2 (n + 1), (r * ∑ j ∈ Ico 1 n, a ^ j * ‖p.rightInv i x j‖) ^ k)
have bc : LE.le (α := ℝ)
  (∑ k ∈ Ico 2 (n + 1),
    a ^ k *
      ∑ c ∈ Set.toFinset {c : Composition k | 1 < c.length},
        r ^ c.length *
          ∏ j : Fin c.length,
            norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (c.blocksFun j)) ↦ F) E)
              (p.rightInv i x (c.blocksFun j)))
  (∑ x_1 ∈ Ico 2 (n + 1), r ^ x_1 * HPow.hPow (α := ℝ) (∑ j ∈ Ico 1 n, a ^ j * ‖p.rightInv i x j‖) x_1)
Tactic: simp_rw [mul_pow]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
⊢ 0 < (p.rightInv i x).radius
have obtain : ∀ (C r : ℝ) (Cpos : 0 < C) (rpos : 0 < r) (ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n), 0 < (p.rightInv i x).radius
Tactic: obtain ⟨C, r, Cpos, rpos, ple⟩ :
    ∃ (C r : _) (_ : 0 < C) (_ : 0 < r), ∀ n : ℕ, ‖p n‖ ≤ C * r ^ n :=
    le_mul_pow_of_radius_pos p hp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
⊢ ∃ (a : ℝ) (_ : 0 < a),
    2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a ≤ 1 ∧ r * (I + 1) * a ≤ 1 / 2
have this : Tendsto (fun (a : ℝ) ↦ 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a) (𝓝 0)
  (𝓝 (2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * 0))
Tactic: have :
      Tendsto (fun a => 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a) (𝓝 0)
        (𝓝 (2 * I * C * r ^ 2 * (I + 1) ^ 2 * 0)) :=
      tendsto_const_nhds.mul tendsto_id
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
this :
  Tendsto (fun (a : ℝ) ↦ 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a) (𝓝 0)
    (𝓝 (2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * 0))
⊢ ∀ᶠ (a : ℝ) in 𝓝 0, 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a < 1
have a : 1 > 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * 0
Tactic: apply (tendsto_order.1 this).2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
this :
  Tendsto (fun (a : ℝ) ↦ 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a) (𝓝 0)
    (𝓝 (2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * 0))
⊢ ∃ (a : ℝ) (_ : 0 < a),
    2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a ≤ 1 ∧ r * (I + 1) * a ≤ 1 / 2
have A : ∀ᶠ (a : ℝ) in 𝓝 0, 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a < 1
Tactic: have A : ∀ᶠ a in 𝓝 0, 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a < 1 := by
      apply (tendsto_order.1 this).2; simp [zero_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
this :
  Tendsto (fun (a : ℝ) ↦ 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a) (𝓝 0)
    (𝓝 (2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * 0))
A : ∀ᶠ (a : ℝ) in 𝓝 0, 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a < 1
⊢ ∃ (a : ℝ) (_ : 0 < a),
    2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a ≤ 1 ∧ r * (I + 1) * a ≤ 1 / 2
have this₁ : Tendsto (fun (a : ℝ) ↦ r * (I + 1) * a) (𝓝 0) (𝓝 (r * (I + 1) * 0))
Tactic: have : Tendsto (fun a => r * (I + 1) * a) (𝓝 0) (𝓝 (r * (I + 1) * 0)) :=
      tendsto_const_nhds.mul tendsto_id
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
this_1 :
  Tendsto (fun (a : ℝ) ↦ 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a) (𝓝 0)
    (𝓝 (2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * 0))
A : ∀ᶠ (a : ℝ) in 𝓝 0, 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a < 1
this : Tendsto (fun (a : ℝ) ↦ r * (I + 1) * a) (𝓝 0) (𝓝 (r * (I + 1) * 0))
⊢ ∀ᶠ (a : ℝ) in 𝓝 0, r * (I + 1) * a < 1 / 2
have a : 1 / 2 > r * (I + 1) * 0
Tactic: apply (tendsto_order.1 this).2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
this_1 :
  Tendsto (fun (a : ℝ) ↦ 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a) (𝓝 0)
    (𝓝 (2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * 0))
A : ∀ᶠ (a : ℝ) in 𝓝 0, 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a < 1
this : Tendsto (fun (a : ℝ) ↦ r * (I + 1) * a) (𝓝 0) (𝓝 (r * (I + 1) * 0))
⊢ ∃ (a : ℝ) (_ : 0 < a),
    2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a ≤ 1 ∧ r * (I + 1) * a ≤ 1 / 2
have B : ∀ᶠ (a : ℝ) in 𝓝 0, r * (I + 1) * a < 1 / 2
Tactic: have B : ∀ᶠ a in 𝓝 0, r * (I + 1) * a < 1 / 2 := by
      apply (tendsto_order.1 this).2; simp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
this_1 :
  Tendsto (fun (a : ℝ) ↦ 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a) (𝓝 0)
    (𝓝 (2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * 0))
A : ∀ᶠ (a : ℝ) in 𝓝 0, 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a < 1
this : Tendsto (fun (a : ℝ) ↦ r * (I + 1) * a) (𝓝 0) (𝓝 (r * (I + 1) * 0))
B : ∀ᶠ (a : ℝ) in 𝓝 0, r * (I + 1) * a < 1 / 2
⊢ ∀ᶠ (a : ℝ) in 𝓝[>] 0, 0 < a
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) (Set.Ioi 0) x → Membership.mem (γ := Set ℝ) {x : ℝ | (fun (a : ℝ) ↦ 0 < a) x} x}
    a
Tactic: filter_upwards [self_mem_nhdsWithin] with _ ha using ha
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
this_1 :
  Tendsto (fun (a : ℝ) ↦ 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a) (𝓝 0)
    (𝓝 (2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * 0))
A : ∀ᶠ (a : ℝ) in 𝓝 0, 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a < 1
this : Tendsto (fun (a : ℝ) ↦ r * (I + 1) * a) (𝓝 0) (𝓝 (r * (I + 1) * 0))
B : ∀ᶠ (a : ℝ) in 𝓝 0, r * (I + 1) * a < 1 / 2
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) (Set.Ioi 0) x → Membership.mem (γ := Set ℝ) {x : ℝ | (fun (a : ℝ) ↦ 0 < a) x} x}
      a
⊢ ∀ᶠ (a : ℝ) in 𝓝[>] 0, 0 < a
have h₁ : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioi 0) a → 0 < a
Tactic: filter_upwards [self_mem_nhdsWithin] with _ ha using ha
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
this_1 :
  Tendsto (fun (a : ℝ) ↦ 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a) (𝓝 0)
    (𝓝 (2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * 0))
A : ∀ᶠ (a : ℝ) in 𝓝 0, 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a < 1
this : Tendsto (fun (a : ℝ) ↦ r * (I + 1) * a) (𝓝 0) (𝓝 (r * (I + 1) * 0))
B : ∀ᶠ (a : ℝ) in 𝓝 0, r * (I + 1) * a < 1 / 2
⊢ ∃ (a : ℝ) (_ : 0 < a),
    2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a ≤ 1 ∧ r * (I + 1) * a ≤ 1 / 2
have C₁ : ∀ᶠ (a : ℝ) in 𝓝[>] 0, 0 < a
Tactic: have C : ∀ᶠ a in 𝓝[>] (0 : ℝ), (0 : ℝ) < a := by
      filter_upwards [self_mem_nhdsWithin] with _ ha using ha
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C_1 r : ℝ
Cpos : 0 < C_1
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C_1 * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
this_1 :
  Tendsto (fun (a : ℝ) ↦ 2 * I * C_1 * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a) (𝓝 0)
    (𝓝 (2 * I * C_1 * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * 0))
A : ∀ᶠ (a : ℝ) in 𝓝 0, 2 * I * C_1 * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a < 1
this : Tendsto (fun (a : ℝ) ↦ r * (I + 1) * a) (𝓝 0) (𝓝 (r * (I + 1) * 0))
B : ∀ᶠ (a : ℝ) in 𝓝 0, r * (I + 1) * a < 1 / 2
C : ∀ᶠ (a : ℝ) in 𝓝[>] 0, 0 < a
⊢ ∃ (a : ℝ) (_ : 0 < a),
    2 * I * C_1 * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a ≤ 1 ∧ r * (I + 1) * a ≤ 1 / 2
have rcases : ∀ (a : ℝ)
  (ha : 0 < a ∧ 2 * I * C_1 * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a < 1 ∧ r * (I + 1) * a < 1 / 2),
  ∃ (a : ℝ) (_ : 0 < a),
    2 * I * C_1 * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a ≤ 1 ∧ r * (I + 1) * a ≤ 1 / 2
Tactic: rcases (C.and ((A.and B).filter_mono inf_le_left)).exists with ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
⊢ 0 < (p.rightInv i x).radius
have obtain : ∀ (a : ℝ) (apos : 0 < a) (ha1 : 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a ≤ 1)
  (ha2 : r * (I + 1) * a ≤ 1 / 2), 0 < (p.rightInv i x).radius
Tactic: obtain ⟨a, apos, ha1, ha2⟩ :
    ∃ (a : _) (apos : 0 < a),
      2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1 ∧ r * (I + 1) * a ≤ 1 / 2 := by
    have :
      Tendsto (fun a => 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a) (𝓝 0)
        (𝓝 (2 * I * C * r ^ 2 * (I + 1) ^ 2 * 0)) :=
      tendsto_const_nhds.mul tendsto_id
    have A : ∀ᶠ a in 𝓝 0, 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a < 1 := by
      apply (tendsto_order.1 this).2; simp [zero_lt_one]
    have : Tendsto (fun a => r * (I + 1) * a) (𝓝 0) (𝓝 (r * (I + 1) * 0)) :=
      tendsto_const_nhds.mul tendsto_id
    have B : ∀ᶠ a in 𝓝 0, r * (I + 1) * a < 1 / 2 := by
      apply (tendsto_order.1 this).2; simp
    have C : ∀ᶠ a in 𝓝[>] (0 : ℝ), (0 : ℝ) < a := by
      filter_upwards [self_mem_nhdsWithin] with _ ha using ha
    rcases (C.and ((A.and B).filter_mono inf_le_left)).exists with ⟨a, ha⟩
    exact ⟨a, ha.1, ha.2.1.le, ha.2.2.le⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : (n : ℕ) → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
⊢ ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a
have base : S 1 ≤ (I + 1) * a
Tactic: apply Nat.le_induction
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : (n : ℕ) → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
base : S 1 ≤ (I + 1) * a
⊢ ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a
have succ : ∀ (n : ℕ) (hmn : 1 ≤ n), S n ≤ (I + 1) * a → S (n + 1) ≤ (I + 1) * a
Tactic: apply Nat.le_induction
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : (n : ℕ) → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
n : ℕ
one_le_n : 1 ≤ n
hn : S n ≤ (I + 1) * a
⊢ S (n + 1) ≤ (I + 1) * a
have In : 2 ≤ n + 1
Tactic: have In : 2 ≤ n + 1 := by lia
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : (n : ℕ) → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
n : ℕ
one_le_n : 1 ≤ n
hn : S n ≤ (I + 1) * a
In : 2 ≤ n + 1
⊢ r * S n ≤ r * ((I + 1) * a)
have ha : 0 ≤ r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : (n : ℕ) → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
n : ℕ
one_le_n : 1 ≤ n
hn : S n ≤ (I + 1) * a
In : 2 ≤ n + 1
⊢ S (n + 1) ≤ (I + 1) * a
have rSn : r * S n ≤ 1 / 2
Tactic: have rSn : r * S n ≤ 1 / 2 :=
        calc
          r * S n ≤ r * ((I + 1) * a) := by gcongr
          _ ≤ 1 / 2 := by rwa [← mul_assoc]