awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A :
  Tendsto (fun (n : ℕ) ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y)) atTop
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
B :
  Tendsto (fun (n : ℕ) ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (g (f (x + y))))
C :
  Tendsto
    (fun (n : ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n n,
        (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)
    atTop (𝓝 (g (f (x + y))))
⊢ 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
have 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))‖₊ *
          r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)) :
      ℝ)
Tactic: apply cauchySeq_finset_of_norm_bounded (NNReal.summable_coe.2 hr) _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A :
  Tendsto (fun (n : ℕ) ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y)) atTop
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
B :
  Tendsto (fun (n : ℕ) ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (g (f (x + y))))
C :
  Tendsto
    (fun (n : ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n n,
        (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)
    atTop (𝓝 (g (f (x + y))))
n : ℕ
c : Composition n
⊢ ‖q.compAlongComposition p c‖ * ∏ _j : Fin n, ‖y‖ ≤ ‖q.compAlongComposition p c‖ * (↑r : ℝ) ^ n
have rw : ‖q.compAlongComposition p c‖ * ‖y‖ ^ n ≤ ‖q.compAlongComposition p c‖ * (↑r : ℝ) ^ n
Tactic: rw [Finset.prod_const, Finset.card_fin]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A :
  Tendsto (fun (n : ℕ) ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y)) atTop
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
B :
  Tendsto (fun (n : ℕ) ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (g (f (x + y))))
C :
  Tendsto
    (fun (n : ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n n,
        (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)
    atTop (𝓝 (g (f (x + y))))
n : ℕ
c : Composition n
⊢ ‖q.compAlongComposition p c‖ * ‖y‖ ^ n ≤ ‖q.compAlongComposition p c‖ * (↑r : ℝ) ^ n
have hbc : ‖y‖ ≤ (↑r : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A :
  Tendsto (fun (n : ℕ) ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y)) atTop
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
B :
  Tendsto (fun (n : ℕ) ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (g (f (x + y))))
C :
  Tendsto
    (fun (n : ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n n,
        (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)
    atTop (𝓝 (g (f (x + y))))
n : ℕ
c : Composition n
⊢ ‖y‖ ≤ (↑r : ℝ)
have hbc : ∀ (hy : ‖y‖ₑ < min rf' (↑r : ℝ≥0∞)) (y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y)
  (fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg)
  (A :
    Tendsto (fun (n : ℕ) ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y)) atTop
      (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x))))
  (B :
    Tendsto
      (fun (n : ℕ) ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
      atTop (𝓝 (g (f (x + y)))))
  (C :
    Tendsto
      (fun (n : ℕ) ↦
        ∑ i ∈ compPartialSumTarget 0 n n,
          (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)
      atTop (𝓝 (g (f (x + y)))))
  (n : ℕ) (c : Composition n), ‖y‖ ≤ (↑r : ℝ)
Tactic: rw [Metric.mem_eball, edist_zero_right] at hy
Cleared hypotheses: hy, y_mem, fy_mem, A, B, C, n, c
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : ‖y‖ₑ < min rf' (↑r : ℝ≥0∞)
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A :
  Tendsto (fun (n : ℕ) ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y)) atTop
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
B :
  Tendsto (fun (n : ℕ) ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (g (f (x + y))))
C :
  Tendsto
    (fun (n : ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n n,
        (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)
    atTop (𝓝 (g (f (x + y))))
n : ℕ
c : Composition n
⊢ ‖y‖ ≤ (↑r : ℝ)
have this : ‖y‖ₑ ≤ (↑r : ℝ≥0∞)
Tactic: have := le_trans (le_of_lt hy) (min_le_right _ _)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : ‖y‖ₑ < min rf' (↑r : ℝ≥0∞)
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A :
  Tendsto (fun (n : ℕ) ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y)) atTop
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
B :
  Tendsto (fun (n : ℕ) ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (g (f (x + y))))
C :
  Tendsto
    (fun (n : ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n n,
        (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)
    atTop (𝓝 (g (f (x + y))))
n : ℕ
c : Composition n
this : ‖y‖ₑ ≤ (↑r : ℝ≥0∞)
⊢ ‖y‖ ≤ (↑r : ℝ)
have hbc : ∀ (this : ‖y‖₊ ≤ r), ‖y‖ ≤ (↑r : ℝ)
Tactic: rwa [enorm_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : ‖y‖ₑ < min rf' (↑r : ℝ≥0∞)
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A :
  Tendsto (fun (n : ℕ) ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y)) atTop
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
B :
  Tendsto (fun (n : ℕ) ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (g (f (x + y))))
C :
  Tendsto
    (fun (n : ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n n,
        (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)
    atTop (𝓝 (g (f (x + y))))
n : ℕ
c : Composition n
this : ‖y‖ₑ ≤ (↑r : ℝ≥0∞)
hbc : ∀ (this : ‖y‖₊ ≤ r), ‖y‖ ≤ (↑r : ℝ)
⊢ ‖y‖ ≤ (↑r : ℝ)
have hbc₁ : ∀ (this : (↑‖y‖₊ : ℝ) ≤ (↑r : ℝ)), ‖y‖ ≤ (↑r : ℝ)
Tactic: rwa [enorm_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : ‖y‖ₑ < min rf' (↑r : ℝ≥0∞)
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A :
  Tendsto (fun (n : ℕ) ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y)) atTop
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
B :
  Tendsto (fun (n : ℕ) ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (g (f (x + y))))
C :
  Tendsto
    (fun (n : ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n n,
        (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)
    atTop (𝓝 (g (f (x + y))))
n : ℕ
c : Composition n
this : ‖y‖ₑ ≤ (↑r : ℝ≥0∞)
hbc : ∀ (this : ‖y‖₊ ≤ r), ‖y‖ ≤ (↑r : ℝ)
hbc₁ : ∀ (this : (↑‖y‖₊ : ℝ) ≤ (↑r : ℝ)), ‖y‖ ≤ (↑r : ℝ)
⊢ ‖y‖ ≤ (↑r : ℝ)
have hbc₂ : ∀ (this : ‖y‖ ≤ (↑r : ℝ)), ‖y‖ ≤ (↑r : ℝ)
Tactic: rwa [enorm_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A :
  Tendsto (fun (n : ℕ) ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y)) atTop
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
B :
  Tendsto (fun (n : ℕ) ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (g (f (x + y))))
C :
  Tendsto
    (fun (n : ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n n,
        (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)
    atTop (𝓝 (g (f (x + y))))
n : ℕ
c : Composition n
⊢ norm.{u_4} (E := G)
      ((q.compAlongComposition p
              ((Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n)) :
            (a : (i : Fin ⟨n, c⟩.fst) → E) → G)
          fun (_j : Fin ((Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).fst (β := fun (n : ℕ) ↦ Composition n))) ↦
          y :
        G) ≤
    ‖q.compAlongComposition p
          ((Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n))‖ *
      (↑r : ℝ) ^ (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).fst (β := fun (n : ℕ) ↦ Composition n)
have q₁ : 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: calc
        ‖(compAlongComposition q p c) fun _j : Fin n => y‖ ≤
            ‖compAlongComposition q p c‖ * ∏ _j : Fin n, ‖y‖ := by
          apply ContinuousMultilinearMap.le_opNorm
        _ ≤ ‖compAlongComposition q p c‖ * (r : ℝ) ^ n := by
          rw [Finset.prod_const, Finset.card_fin]
          gcongr
          rw [Metric.mem_eball, edist_zero_right] at hy
          have := le_trans (le_of_lt hy) (min_le_right _ _)
          rwa [enorm_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' (↑r : ℝ≥0∞)
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min rf' (↑r : ℝ≥0∞))) y
y_mem : Membership.mem (γ := Set E) (Metric.eball 0 rf) y
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A :
  Tendsto (fun (n : ℕ) ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (x : Fin a) ↦ y)) atTop
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 (f (x + y) - f x)))
B :
  Tendsto (fun (n : ℕ) ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a : (a : (i : Fin a) → E) → F) fun (_b : Fin a) ↦ y))
    atTop (𝓝 (g (f (x + y))))
C :
  Tendsto
    (fun (n : ℕ) ↦
      ∑ i ∈ compPartialSumTarget 0 n n,
        (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)
    atTop (𝓝 (g (f (x + y))))
⊢ HasSum (fun (n : ℕ) ↦ (q.comp p n : (a : (i : Fin n) → E) → G) fun (x : Fin n) ↦ y) ((g ∘ f) (x + y))
have D : HasSum
  (fun (i : (n : ℕ) × Composition n) ↦
    (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 (f (x + y)))
Tactic: have D :
    HasSum (fun i : Σ n, Composition n => q.compAlongComposition p i.2 fun _j => y)
      (g (f (x + y))) :=
    haveI cau :
      CauchySeq fun s : Finset (Σ n, Composition n) =>
        ∑ i ∈ s, q.compAlongComposition p i.2 fun _j => y := by
      apply cauchySeq_finset_of_norm_bounded (NNReal.summable_coe.2 hr) _
      simp only [coe_nnnorm, NNReal.coe_mul, NNReal.coe_pow]
      rintro ⟨n, c⟩
      calc
        ‖(compAlongComposition q p c) fun _j : Fin n => y‖ ≤
            ‖compAlongComposition q p c‖ * ∏ _j : Fin n, ‖y‖ := by
          apply ContinuousMultilinearMap.le_opNorm
        _ ≤ ‖compAlongComposition q p c‖ * (r : ℝ) ^ n := by
          rw [Finset.prod_const, Finset.card_fin]
          gcongr
          rw [Metric.mem_eball, edist_zero_right] at hy
          have := le_trans (le_of_lt hy) (min_le_right _ _)
          rwa [enorm_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this
    tendsto_nhds_of_cauchySeq_of_subseq cau compPartialSumTarget_tendsto_atTop C