awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Inverse
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)‖
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
⊢ 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⟩

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.Inverse
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
succ : ∀ (n : ℕ) (hmn : 1 ≤ n), S n ≤ (I + 1) * a → S (n + 1) ≤ (I + 1) * a
⊢ ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a

Tactic:
apply Nat.le_induction
-- Module: Mathlib.Analysis.Analytic.Inverse
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 : ∑ k ∈ Ico 1 1, a ^ k * ‖p.rightInv i x k‖ ≤ (I + 1) * a
⊢ S 1 ≤ (I + 1) * a

Tactic:
simp only [S]
-- Module: Mathlib.Analysis.Analytic.Inverse
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‖
⊢ 0 ≤ (I + 1) * a

Tactic:
positivity
-- Module: Mathlib.Analysis.Analytic.Inverse
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
⊢ 2 ≤ n + 1

Tactic:
lia
-- Module: Mathlib.Analysis.Analytic.Inverse
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
⊢ 2 ≤ n + 1

Tactic:
have In : 2 ≤ n + 1 := by lia
-- Module: Mathlib.Analysis.Analytic.Inverse
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
ha : 0 ≤ r
⊢ r * S n ≤ r * ((I + 1) * a)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Analytic.Inverse
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
rwa rwa₁ rwa₂ rwa₃ : r * (I + 1) * a ≤ 1 / 2
⊢ r * ((I + 1) * a) ≤ 1 / 2

Tactic:
rwa [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Analytic.Inverse
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 ≤ 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]
-- Module: Mathlib.Analysis.Analytic.Inverse
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
rSn : r * S n ≤ 1 / 2
⊢ S (n + 1) ≤ I * a + I * C * ∑ k ∈ Ico 2 (n + 1), (r * S n) ^ k

Tactic:
radius_rightInv_pos_of_radius_pos_aux2 In p i rpos.le apos.le Cpos.le ple

Premises used: LT.lt.le, FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2
-- Module: Mathlib.Analysis.Analytic.Inverse
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
rSn : r * S n ≤ 1 / 2
rw : r * S n ≠ 1
⊢ I * a + I * C * ∑ k ∈ Ico 2 (n + 1), (r * S n) ^ k =
    I * a + I * C * ((HPow.hPow (β := ℕ) (r * S n) 2 - (r * S n) ^ (n + 1)) / (1 - r * S n))

Tactic:
rw [geom_sum_Ico' _ In]

Premises used: geom_sum_Ico'
-- Module: Mathlib.Analysis.Analytic.Inverse
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
rSn : r * S n ≤ 1 / 2
⊢ 1 / 2 < 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Analytic.Inverse
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
rSn : r * S n ≤ 1 / 2
⊢ r * S n ≠ 1

Tactic:
exact ne_of_lt (rSn.trans_lt (by norm_num))

Premises used: LE.le.trans_lt, ne_of_lt
-- Module: Mathlib.Analysis.Analytic.Inverse
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
rSn : r * S n ≤ 1 / 2
bc : HPow.hPow (β := ℕ) (r * S n) 2 - (r * S n) ^ (n + 1) ≤ HPow.hPow (β := ℕ) (r * S n) 2
bc₁ : 1 / 2 ≤ 1 - r * S n
⊢ I * a + I * C * ((HPow.hPow (β := ℕ) (r * S n) 2 - (r * S n) ^ (n + 1)) / (1 - r * S n)) ≤
    I * a + I * C * (HPow.hPow (β := ℕ) (r * S n) 2 / (1 / 2))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Analytic.Inverse
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
rSn : r * S n ≤ 1 / 2
bc : 0 ≤ (r * S n) ^ (n + 1)
⊢ HPow.hPow (β := ℕ) (r * S n) 2 - (r * S n) ^ (n + 1) ≤ HPow.hPow (β := ℕ) (r * S n) 2

Tactic:
simp only [sub_le_self_iff]

Premises used: sub_le_self_iff
-- Module: Mathlib.Analysis.Analytic.Inverse
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
rSn : r * S n ≤ 1 / 2
⊢ 0 ≤ (r * S n) ^ (n + 1)

Tactic:
positivity
-- Module: Mathlib.Analysis.Analytic.Inverse
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
rSn : r * S n ≤ 1 / 2
linarith : 1 - r * S n < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁ : 1 - r * S n < 1 / 2 → 2 / 2 = 1
linarith₂ : 1 - r * S n < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₃ : 1 - r * S n < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₄ : 1 - r * S n < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 1 - r * S n < 1 / 2 → 2 / 2 = 1
linarith₆ : 1 - r * S n < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : 1 - r * S n < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₈ :
  1 - r * S n < 1 / 2 →
    HMul.hMul (α := ℝ) 2 1 - 1 * r * (2 * S n) - HMul.hMul (α := ℝ) 1 1 + (1 * r * (2 * S n) - HMul.hMul (α := ℝ) 1 1) =
      0
⊢ 1 / 2 ≤ 1 - r * S n

Tactic:
linarith only [rSn]
-- Module: Mathlib.Analysis.Analytic.Inverse
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
rSn : r * S n ≤ 1 / 2
⊢ I * a + I * C * (HPow.hPow (β := ℕ) (r * S n) 2 / (1 / 2)) = I * a + 2 * I * C * HPow.hPow (β := ℕ) (r * S n) 2

Tactic:
ring
-- Module: Mathlib.Analysis.Analytic.Inverse
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
rSn : r * S n ≤ 1 / 2
bc : 0 ≤ 2 * I * C
bc₁ : 0 ≤ r * S n
bc₂ : 0 ≤ r
⊢ I * a + 2 * I * C * HPow.hPow (β := ℕ) (r * S n) 2 ≤ I * a + 2 * I * C * HPow.hPow (β := ℕ) (r * ((I + 1) * a)) 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.Analytic.Inverse
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
rSn : r * S n ≤ 1 / 2
⊢ I * a + 2 * I * C * HPow.hPow (β := ℕ) (r * ((I + 1) * a)) 2 =
    (I + 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a) * a

Tactic:
ring
-- Module: Mathlib.Analysis.Analytic.Inverse
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
rSn : r * S n ≤ 1 / 2
ha : 0 ≤ a
⊢ (I + 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a) * a ≤ (I + 1) * a

Tactic:
gcongr
-- Module: Mathlib.Analysis.Analytic.Inverse
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
rSn : r * S n ≤ 1 / 2
S₁ :
  I * a + I * C * ∑ k ∈ Ico 2 (n + 1), (r * S n) ^ k =
    I * a + I * C * ((HPow.hPow (β := ℕ) (r * S n) 2 - (r * S n) ^ (n + 1)) / (1 - r * S n))
S₂ :
  I * a + I * C * ((HPow.hPow (β := ℕ) (r * S n) 2 - (r * S n) ^ (n + 1)) / (1 - r * S n)) ≤
    I * a + I * C * (HPow.hPow (β := ℕ) (r * S n) 2 / (1 / 2))
S₃ : I * a + I * C * (HPow.hPow (β := ℕ) (r * S n) 2 / (1 / 2)) = I * a + 2 * I * C * HPow.hPow (β := ℕ) (r * S n) 2
S₄ : I * a + 2 * I * C * HPow.hPow (β := ℕ) (r * S n) 2 ≤ I * a + 2 * I * C * HPow.hPow (β := ℕ) (r * ((I + 1) * a)) 2
S₅ :
  I * a + 2 * I * C * HPow.hPow (β := ℕ) (r * ((I + 1) * a)) 2 =
    (I + 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a) * a
S₆ : (I + 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * a) * a ≤ (I + 1) * a
⊢ S (n + 1) ≤ (I + 1) * a

Tactic:
calc
        S (n + 1) ≤ I * a + I * C * ∑ k ∈ Ico 2 (n + 1), (r * S n) ^ k :=
          radius_rightInv_pos_of_radius_pos_aux2 In p i rpos.le apos.le Cpos.le ple
        _ = I * a + I * C * (((r * S n) ^ 2 - (r * S n) ^ (n + 1)) / (1 - r * S n)) := by
          rw [geom_sum_Ico' _ In]; exact ne_of_lt (rSn.trans_lt (by norm_num))
        _ ≤ I * a + I * C * ((r * S n) ^ 2 / (1 / 2)) := by
          gcongr
          · simp only [sub_le_self_iff]
            positivity
          · linarith only [rSn]
        _ = I * a + 2 * I * C * (r * S n) ^ 2 := by ring
        _ ≤ I * a + 2 * I * C * (r * ((I + 1) * a)) ^ 2 := by gcongr
        _ = (I + 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a) * a := by ring
        _ ≤ (I + 1) * a := by gcongr

Premises used: HMul.hMul, HSub.hSub, Finset.Ico, HDiv.hDiv, LT.lt.le, HPow.hPow, HAdd.hAdd, FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.Inverse
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

Tactic:
have IRec : ∀ n, 1 ≤ n → S n ≤ (I + 1) * a := by
    apply Nat.le_induction
    · simp only [S]
      rw [Ico_eq_empty_of_le (le_refl 1), sum_empty]
      positivity
    · intro n one_le_n hn
      have In : 2 ≤ n + 1 := by lia
      have rSn : r * S n ≤ 1 / 2 :=
        calc
          r * S n ≤ r * ((I + 1) * a) := by gcongr
          _ ≤ 1 / 2 := by rwa [← mul_assoc]
      calc
        S (n + 1) ≤ I * a + I * C * ∑ k ∈ Ico 2 (n + 1), (r * S n) ^ k :=
          radius_rightInv_pos_of_radius_pos_aux2 In p i rpos.le apos.le Cpos.le ple
        _ = I * a + I * C * (((r * S n) ^ 2 - (r * S n) ^ (n + 1)) / (1 - r * S n)) := by
          rw [geom_sum_Ico' _ In]; exact ne_of_lt (rSn.trans_lt (by norm_num))
        _ ≤ I * a + I * C * ((r * S n) ^ 2 / (1 / 2)) := by
          gcongr
          · simp only [sub_le_self_iff]
            positivity
          · linarith only [rSn]
        _ = I * a + 2 * I * C * (r * S n) ^ 2 := by ring
        _ ≤ I * a + 2 * I * C * (r * ((I + 1) * a)) ^ 2 := by gcongr
        _ = (I + 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a) * a := by ring
        _ ≤ (I + 1) * a := by gcongr
-- Module: Mathlib.Analysis.Analytic.Inverse
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‖
IRec : ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a
a' : NNReal := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) a ⋯
H : (↑a' : ℝ≥0∞) ≤ (p.rightInv i x).radius
apply : 0 < (↑a' : ℝ≥0∞)
⊢ 0 < (p.rightInv i x).radius

Tactic:
apply lt_of_lt_of_le _ H

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Analysis.Analytic.Inverse
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‖
IRec : ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a
a' : NNReal := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) a ⋯
H : (↑a' : ℝ≥0∞) ≤ (p.rightInv i x).radius
⊢ 0 < (↑a' : ℝ≥0∞)

Tactic:
simpa only [ENNReal.coe_pos]

Premises used: ENNReal.coe_pos