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)‖
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 ⋯
suffices : (↑a' : ℝ≥0∞) ≤ (p.rightInv i x).radius
⊢ 0 < (p.rightInv i x).radius

Tactic:
suffices H : (a' : ENNReal) ≤ (p.rightInv i x).radius by
    apply lt_of_lt_of_le _ H
    -- Prior to https://github.com/leanprover/lean4/pull/2734, this was `exact_mod_cast apos`.
    simpa only [ENNReal.coe_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)‖
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 ⋯
apply : ∀ᶠ (n : ℕ) in atTop, ‖p.rightInv i x n‖ * (↑a' : ℝ) ^ n ≤ (I + 1) * a
⊢ (↑a' : ℝ≥0∞) ≤ (p.rightInv i x).radius

Tactic:
apply le_radius_of_eventually_le _ ((I + 1) * a)

Premises used: HMul.hMul, HAdd.hAdd, FormalMultilinearSeries.le_radius_of_eventually_le, 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‖
IRec : ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a
a' : NNReal := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) a ⋯
n : ℕ
h : ∀ (hn : 1 ≤ n), ‖p.rightInv i x n‖ * (↑a' : ℝ) ^ n ≤ (I + 1) * a
⊢ Membership.mem (γ := Set ℕ) (Set.Ici 1) n → ‖p.rightInv i x n‖ * (↑a' : ℝ) ^ n ≤ (I + 1) * a

Tactic:
(hn : 1 ≤ n)
-- 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 : ∀ (n : ℕ) (hn : 1 ≤ n), ‖p.rightInv i x n‖ * (↑a' : ℝ) ^ n ≤ (I + 1) * a
⊢ ∀ᶠ (n : ℕ) in atTop, ‖p.rightInv i x n‖ * (↑a' : ℝ) ^ n ≤ (I + 1) * a

Tactic:
filter_upwards [Ici_mem_atTop 1] with n (hn : 1 ≤ n)

Premises used: Filter.Ici_mem_atTop, 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‖
IRec : ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a
a' : NNReal := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) a ⋯
n : ℕ
hn : 1 ≤ n
⊢ ‖p.rightInv i x n‖ * (↑a' : ℝ) ^ n = a ^ n * ‖p.rightInv i x n‖

Tactic:
mul_comm _ _

Premises used: mul_comm, NNReal.toReal
-- 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 ⋯
n : ℕ
hn : 1 ≤ n
k : ℕ
h : k ∈ Ico 1 (n + 1)
⊢ 0 ≤ a ^ k * ‖p.rightInv i x k‖

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‖
IRec : ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a
a' : NNReal := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) a ⋯
n : ℕ
hn : 1 ≤ n
this : ∀ k ∈ Ico 1 (n + 1), 0 ≤ a ^ k * ‖p.rightInv i x k‖
⊢ n ∈ Ico 1 (n + 1)

Tactic:
simp [hn]
-- 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 ⋯
n : ℕ
hn : 1 ≤ n
⊢ 1 ≤ n + 1

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)‖
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 ⋯
n : ℕ
hn : 1 ≤ n
⊢ ‖p.rightInv i x n‖ * (↑a' : ℝ) ^ n ≤ (I + 1) * a

Tactic:
calc
    ‖p.rightInv i x n‖ * (a' : ℝ) ^ n = a ^ n * ‖p.rightInv i x n‖ := mul_comm _ _
    _ ≤ ∑ k ∈ Ico 1 (n + 1), a ^ k * ‖p.rightInv i x k‖ :=
      (haveI : ∀ k ∈ Ico 1 (n + 1), 0 ≤ a ^ k * ‖p.rightInv i x k‖ := fun k _ => by positivity
      single_le_sum this (by simp [hn]))
    _ ≤ (I + 1) * a := IRec (n + 1) (by simp)

Premises used: Finset.Ico, HAdd.hAdd, Finset.single_le_sum, mul_comm, FormalMultilinearSeries.rightInv, OfNat.ofNat, NNReal.toReal
-- 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
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
rw : 0 < (p.rightInv i x).radius
⊢ 0 < (p.leftInv i x).radius

Tactic:
rw [leftInv_eq_rightInv _ _ _ h]

Premises used: FormalMultilinearSeries.leftInv_eq_rightInv
-- 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
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
⊢ 0 < (p.rightInv i x).radius

Tactic:
radius_rightInv_pos_of_radius_pos hp

Premises used: FormalMultilinearSeries.radius_rightInv_pos_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
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
⊢ 0 < (p.rightInv i x).radius

Tactic:
exact radius_rightInv_pos_of_radius_pos hp

Premises used: FormalMultilinearSeries.radius_rightInv_pos_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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f (q.comp p) x
hq : 0 < q.radius
hp : 0 < p.radius
rcases :
  ∀ (r0 : ℝ≥0∞) (h0 : HasFPowerSeriesOnBall f (q.comp p) x r0),
    ∀ᶠ (y : E) in 𝓝 0,
      Tendsto
        (fun (a : ℕ × ℕ) ↦
          q.partialSum a.1
            (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)))
        atTop (𝓝 (f (x + y)))
⊢ ∀ᶠ (y : E) in 𝓝 0,
    Tendsto
      (fun (a : ℕ × ℕ) ↦
        q.partialSum a.1
          (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)))
      atTop (𝓝 (f (x + y)))

Tactic:
rcases hf with ⟨r0, h0⟩
-- 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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
rcases :
  ∀ (r1 : NNReal) (r1_pos : 0 < r1)
    (hr1 :
      Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
        ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
          r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)),
    ∀ᶠ (y : E) in 𝓝 0,
      Tendsto
        (fun (a : ℕ × ℕ) ↦
          q.partialSum a.1
            (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)))
        atTop (𝓝 (f (x + y)))
⊢ ∀ᶠ (y : E) in 𝓝 0,
    Tendsto
      (fun (a : ℕ × ℕ) ↦
        q.partialSum a.1
          (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)))
      atTop (𝓝 (f (x + y)))

Tactic:
rcases q.comp_summable_nnreal p hq hp with ⟨r1, r1_pos : 0 < r1, hr1⟩

Premises used: FormalMultilinearSeries.comp_summable_nnreal
-- 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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
⊢ 0 < (↑r1 : ℝ≥0∞)

Tactic:
exact_mod_cast r1_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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
⊢ Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)

Tactic:
have : Metric.eball (0 : E) r ∈ 𝓝 0 :=
    Metric.eball_mem_nhds 0 (lt_min h0.r_pos (by exact_mod_cast r1_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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
h :
  ∀ (y : E) (hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y),
    Tendsto
      (fun (a : ℕ × ℕ) ↦
        q.partialSum a.1
          (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)))
      atTop (𝓝 (f (x + y)))
⊢ ∀ᶠ (y : E) in 𝓝 0,
    Tendsto
      (fun (a : ℕ × ℕ) ↦
        q.partialSum a.1
          (HSub.hSub (β := F) (p.partialSum a.2 y) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)))
      atTop (𝓝 (f (x + y)))

Tactic:
filter_upwards [this] with y hy
-- 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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ Membership.mem (γ := Set E) (Metric.eball 0 r0) y

Tactic:
have hy0 : y ∈ Metric.eball 0 r0 := Metric.eball_subset_eball (min_le_left _ _) hy
-- 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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
apply :
  ∀ (i : (n : ℕ) × Composition n),
    norm.{u_4} (E := G)
        ((q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
            fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y :
          G) ≤
      (↑(‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
            r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)) :
        ℝ)
⊢ CauchySeq.{u_4, 0} (α := G) fun (s : Finset ((n : ℕ) × Composition n)) ↦
    ∑ i ∈ s,
      (q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n)) : (a : (i : Fin i.fst) → E) → G)
        fun (_j : Fin (i.fst (β := fun (n : ℕ) ↦ Composition n))) ↦ y

Tactic:
apply cauchySeq_finset_of_norm_bounded (NNReal.summable_coe.2 hr1) _

Premises used: NNReal.summable_coe, Iff.mpr, cauchySeq_finset_of_norm_bounded
-- 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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
n : ℕ
c : Composition n
⊢ norm.{u_4} (E := G) ((q.compAlongComposition p c : (a : (i : Fin n) → E) → G) fun (_j : Fin n) ↦ y : G) ≤
    ‖q.compAlongComposition p c‖ * ∏ _j : Fin n, ‖y‖

Tactic:
apply ContinuousMultilinearMap.le_opNorm

Premises used: ContinuousMultilinearMap.le_opNorm
-- 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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
n : ℕ
c : Composition n
apply : ∏ _j : Fin n, ‖y‖ ≤ (↑r1 : ℝ) ^ n
⊢ ‖q.compAlongComposition p c‖ * ∏ _j : Fin n, ‖y‖ ≤ ‖q.compAlongComposition p c‖ * (↑r1 : ℝ) ^ n

Tactic:
apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)

Premises used: mul_le_mul_of_nonneg_left, 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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
n : ℕ
c : Composition n
rw : ‖y‖ ^ n ≤ (↑r1 : ℝ) ^ n
⊢ ∏ _j : Fin n, ‖y‖ ≤ (↑r1 : ℝ) ^ n

Tactic:
rw [Finset.prod_const, Finset.card_fin]

Premises used: Finset.prod_const, Finset.card_fin
-- 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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
n : ℕ
c : Composition n
hab : ‖y‖ ≤ (↑r1 : ℝ)
⊢ ‖y‖ ^ n ≤ (↑r1 : ℝ) ^ n

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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 :
  Summable (α := NNReal) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r1 ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
r : ℝ≥0∞ := min r0 (↑r1 : ℝ≥0∞)
this : Membership.mem (γ := Filter E) (𝓝 0) (Metric.eball 0 r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y
n : ℕ
c : Composition n
hab :
  ∀ (hy : ‖y‖ₑ < r) (hy0 : Membership.mem (γ := Set E) (Metric.eball 0 r0) y) (n : ℕ) (c : Composition n),
    ‖y‖ ≤ (↑r1 : ℝ)
⊢ ‖y‖ ≤ (↑r1 : ℝ)

Tactic:
rw [Metric.mem_eball, edist_zero_right] at hy

Premises used: edist_zero_right, Metric.mem_eball