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
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
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
⊢ 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:
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
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) ≤
    C * r ^ i_1.length

Tactic:
apply hp
-- 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
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)‖
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)))
⊢ 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))

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]

Premises used: Norm.norm, Finset.mul_sum, ContinuousLinearEquiv.symm, mul_assoc, mul_comm, ContinuousLinearEquiv.toContinuousLinearMap
-- 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
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.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:
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
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)‖
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)
⊢ 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

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
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)‖
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)
⊢ 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:
simp_rw [mul_pow]

Premises used: mul_pow
-- 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
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)))
    (∑ 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:
apply
        radius_right_inv_pos_of_radius_pos_aux1 n (fun k => ‖p.rightInv i x k‖)
          (fun k => norm_nonneg _) hr ha

Premises used: Norm.norm, FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1, FormalMultilinearSeries.rightInv, norm_nonneg
-- 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 : ℝ) (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n

Tactic:
le_mul_pow_of_radius_pos p hp

Premises used: FormalMultilinearSeries.le_mul_pow_of_radius_pos
-- 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
obtain : ∀ (C r : ℝ) (Cpos : 0 < C) (rpos : 0 < r) (ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n), 0 < (p.rightInv i x).radius
⊢ 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

Premises used: FormalMultilinearSeries.le_mul_pow_of_radius_pos
-- 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)‖
⊢ 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
-- 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)‖
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 : 1 > 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

Tactic:
apply (tendsto_order.1 this).2

Premises used: tendsto_order, And.right, Iff.mp
-- 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)‖
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))
⊢ 1 > 2 * I * C * HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) (I + 1) 2 * 0

Tactic:
simp [zero_lt_one]

Premises used: zero_lt_one
-- 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)‖
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

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]
-- 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)‖
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
⊢ 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
-- 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)‖
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 : 1 / 2 > r * (I + 1) * 0
⊢ ∀ᶠ (a : ℝ) in 𝓝 0, r * (I + 1) * a < 1 / 2

Tactic:
apply (tendsto_order.1 this).2

Premises used: tendsto_order, And.right, Iff.mp
-- 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)‖
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))
⊢ 1 / 2 > r * (I + 1) * 0

Tactic:
simp
-- 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)‖
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

Tactic:
have B : ∀ᶠ a in 𝓝 0, r * (I + 1) * a < 1 / 2 := by
      apply (tendsto_order.1 this).2; simp
-- 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)‖
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 : ℝ
ha : Membership.mem (γ := Set ℝ) (Set.Ioi 0) a
⊢ 0 < a

Tactic:
ha

Premises used: Set.Ioi, Set.Mem
-- 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)‖
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
h₁ h₂ : ∀ (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Set.Ioi 0) a), 0 < a
⊢ ∀ᶠ (a : ℝ) in 𝓝[>] 0, 0 < a

Tactic:
filter_upwards [self_mem_nhdsWithin] with _ ha using ha

Premises used: self_mem_nhdsWithin
-- 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)‖
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

Tactic:
have C : ∀ᶠ a in 𝓝[>] (0 : ℝ), (0 : ℝ) < a := by
      filter_upwards [self_mem_nhdsWithin] with _ ha using ha
-- 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_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
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
⊢ ∃ (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⟩

Premises used: Filter.Eventually.filter_mono, Filter.Eventually.and, Filter.Eventually.exists, inf_le_left
-- 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_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 : ℝ
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:
⟨a, ha.1, ha.2.1.le, ha.2.2.le⟩

Premises used: LT.lt.le, And.right, And.left, And.intro, Exists.intro
-- 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_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 : ℝ
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:
exact ⟨a, ha.1, ha.2.1.le, ha.2.2.le⟩