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))))
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)))
⊢ HasSum (fun (n : ℕ) ↦ (q.comp p n : (a : (i : Fin n) → E) → G) fun (_j : Fin n) ↦ y) (g (f (x + y)))
have apply : ∀ (b : ℕ),
  HasSum.{u_4, 0} (α := G)
    (fun (c : Composition b) ↦
      ((q.compAlongComposition p
              ((Sigma.mk (β := fun (b : ℕ) ↦ Composition b) b c).snd (β := fun (n : ℕ) ↦ Composition n)) :
            (a : (i : Fin ⟨b, c⟩.fst) → E) → G)
          fun (_j : Fin ((Sigma.mk (β := fun (b : ℕ) ↦ Composition b) b c).fst (β := fun (n : ℕ) ↦ Composition n))) ↦
          y :
        G))
    ((q.comp p b : (a : (i : Fin b) → E) → G) fun (_j : Fin b) ↦ y : G)
Tactic: apply D.sigma
-- 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))))
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)))
n : ℕ
⊢ HasSum.{u_4, 0} (α := G)
    (fun (c : Composition n) ↦
      ((q.compAlongComposition p
              ((Sigma.mk (β := fun (b : ℕ) ↦ Composition b) n c).snd (β := fun (n : ℕ) ↦ Composition n)) :
            (a : (i : Fin ⟨n, c⟩.fst) → E) → G)
          fun (_j : Fin ((Sigma.mk (β := fun (b : ℕ) ↦ Composition b) n c).fst (β := fun (n : ℕ) ↦ Composition n))) ↦
          y :
        G))
    ((q.comp p n : (a : (i : Fin n) → E) → G) fun (_j : Fin n) ↦ y : G)
have simp : HasSum.{u_4, 0} (α := G)
  (fun (c : Composition n) ↦
    (q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c fun (_j : Fin n) ↦ y))
  (∑ c : Composition n, (q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c fun (_j : Fin n) ↦ y))
Tactic: simp only [compAlongComposition_apply, FormalMultilinearSeries.comp,
      ContinuousMultilinearMap.sum_apply]
-- 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))))
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)))
⊢ HasSum (fun (n : ℕ) ↦ (q.comp p n : (a : (i : Fin n) → E) → G) fun (x : Fin n) ↦ y) ((g ∘ f) (x + y))
have E₁ : HasSum (fun (n : ℕ) ↦ (q.comp p n : (a : (i : Fin n) → E) → G) fun (_j : Fin n) ↦ y) (g (f (x + y)))
Tactic: have E : HasSum (fun n => (q.comp p) n fun _j => y) (g (f (x + y))) := by
    apply D.sigma
    intro n
    simp only [compAlongComposition_apply, FormalMultilinearSeries.comp,
      ContinuousMultilinearMap.sum_apply]
    exact hasSum_fintype _
-- 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
hg : HasFPowerSeriesAt g q (f x)
hf : HasFPowerSeriesAt f p x
⊢ HasFPowerSeriesAt (g ∘ f) (q.comp p) x
have rw : ∀ (hg : HasFPowerSeriesWithinAt g q Set.univ (f x)) (hf : HasFPowerSeriesWithinAt f p Set.univ x),
  HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) Set.univ x
Tactic: rw [← hasFPowerSeriesWithinAt_univ] at hf hg ⊢
Cleared hypotheses: hg, hf
-- 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
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x
have let : ∀ (_q : FormalMultilinearSeries 𝕜 F G) (hq : HasFPowerSeriesWithinAt g _q t (f x)), AnalyticWithinAt 𝕜 (g ∘ f) s x
Tactic: let ⟨_q, hq⟩ := hg
-- 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
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
_q : FormalMultilinearSeries 𝕜 F G
hq : HasFPowerSeriesWithinAt g _q t (f x)
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x
have let : ∀ (_p : FormalMultilinearSeries 𝕜 E F) (hp : HasFPowerSeriesWithinAt f _p s x), AnalyticWithinAt 𝕜 (g ∘ f) s x
Tactic: let ⟨_p, hp⟩ := hf
-- 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
y : F
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t y
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
hy : f x = y
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x
have hg₁ : AnalyticWithinAt 𝕜 g t (f x)
Tactic: rw [← hy] at hg
Cleared hypotheses: hg, hf, h, hy
-- 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
x : E
hg : AnalyticAt 𝕜 g (f x)
hf : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 (g ∘ f) x
have rw : ∀ (hg : AnalyticWithinAt 𝕜 g Set.univ (f x)) (hf : AnalyticWithinAt 𝕜 f Set.univ x),
  AnalyticWithinAt 𝕜 (g ∘ f) Set.univ x
Tactic: rw [← analyticWithinAt_univ] at hg hf ⊢
Cleared hypotheses: hg, hf
-- 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
y : F
x : E
hg : AnalyticAt 𝕜 g y
hf : AnalyticAt 𝕜 f x
hy : f x = y
⊢ AnalyticAt 𝕜 (g ∘ f) x
have hg₁ : AnalyticAt 𝕜 g (f x)
Tactic: rw [← hy] at hg
Cleared hypotheses: hg, hf, hy
-- 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
x : E
s : Set E
hg : AnalyticAt 𝕜 g (f x)
hf : AnalyticWithinAt 𝕜 f s x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x
have hg₁ : AnalyticWithinAt 𝕜 g Set.univ (f x)
Tactic: rw [← analyticWithinAt_univ] at hg
Cleared hypotheses: hg, hf
-- 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
x : E
y : F
s : Set E
hg : AnalyticAt 𝕜 g y
hf : AnalyticWithinAt 𝕜 f s x
h : f x = y
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x
have hg₁ : AnalyticAt 𝕜 g (f x)
Tactic: rw [← h] at hg
Cleared hypotheses: hg, hf, h
-- 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
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
⊢ HasFiniteFPowerSeriesAt (g ∘ f) (q.comp p) x (m * n)
have rcases : ∀ (r : ℝ≥0∞) (hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r), HasFiniteFPowerSeriesAt (g ∘ f) (q.comp p) x (m * n)
Tactic: rcases hg.hasFPowerSeriesAt.comp hf.hasFPowerSeriesAt with ⟨r, 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
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
⊢ HasFiniteFPowerSeriesAt (g ∘ f) (q.comp p) x (m * n)
have refine : ∀ (i : ℕ) (hi : m * n ≤ i), q.comp p i = 0
Tactic: refine ⟨r, hr, fun i hi ↦ ?_⟩
-- 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
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
hi : m * n ≤ i
⊢ q.comp p i = 0
have h : ∀ (x : Composition i), Membership.mem (γ := Finset (Composition i)) Finset.univ x → q.compAlongComposition p x = 0
Tactic: apply Finset.sum_eq_zero
-- 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
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
hi : m * n ≤ i
c : Composition i
⊢ q.compAlongComposition p c = 0
have h : ∀ (v : (i : Fin i) → E),
  Eq.{u_4 + 1} (α := G) ((q.compAlongComposition p c : (a : (i : Fin i) → E) → G) v : G)
    ((0 : (a : (i : Fin i) → E) → G) v : G)
Tactic: ext v
-- 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
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
hi : m * n ≤ i
c : Composition i
v : (i : Fin i) → E
⊢ Eq.{u_4 + 1} (α := G) ((q.compAlongComposition p c : (a : (i : Fin i) → E) → G) v : G)
    ((0 : (a : (i : Fin i) → E) → G) v : G)
have h : Eq.{u_4 + 1} (α := G) ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G) (0 : G)
Tactic: simp only [compAlongComposition_apply, ContinuousMultilinearMap.zero_apply]
-- 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
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
hi : m * n ≤ i
c : Composition i
v : (i : Fin i) → E
⊢ Eq.{u_4 + 1} (α := G) ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G) (0 : G)
have h : ∀ (hc : m ≤ c.length),
  Eq.{u_4 + 1} (α := G) ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G) (0 : G)
Tactic: rcases le_or_gt m c.length with hc | hc
-- 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
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
hi : m * n ≤ i
c : Composition i
v : (i : Fin i) → E
h :
  ∀ (hc : m ≤ c.length),
    Eq.{u_4 + 1} (α := G) ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G) (0 : G)
⊢ Eq.{u_4 + 1} (α := G) ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G) (0 : G)
have h₁ : ∀ (hc : c.length < m),
  Eq.{u_4 + 1} (α := G) ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G) (0 : G)
Tactic: rcases le_or_gt m c.length with hc | hc
-- 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
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
hi : m * n ≤ i
c : Composition i
v : (i : Fin i) → E
hc : c.length < m
⊢ ∃ (j : Fin c.length), n ≤ c.blocksFun j
have contrapose! : ∀ (hi : ∀ (j : Fin c.length), c.blocksFun j < n), i < m * n
Tactic: contrapose! hi
Cleared hypotheses: hi
-- 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
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
c : Composition i
v : (i : Fin i) → E
hc : c.length < m
hi : ∀ (j : Fin c.length), c.blocksFun j < n
⊢ i < m * n
have rw : ∑ i_1 : Fin c.length, c.blocksFun i_1 < m * n
Tactic: rw [← c.sum_blocksFun]
-- 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
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
c : Composition i
v : (i : Fin i) → E
hc : c.length < m
hi : ∀ (j : Fin c.length), c.blocksFun j < n
⊢ ∑ i_1 : Fin c.length, c.blocksFun i_1 < m * n
have inl : ∀ (h'c : c.length = 0), ∑ i_1 : Fin c.length, c.blocksFun i_1 < m * n
Tactic: rcases eq_zero_or_pos c.length with h'c | h'c
-- 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
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
c : Composition i
v : (i : Fin i) → E
hc : c.length < m
hi : ∀ (j : Fin c.length), c.blocksFun j < n
inl : ∀ (h'c : c.length = 0), ∑ i_1 : Fin c.length, c.blocksFun i_1 < m * n
⊢ ∑ i_1 : Fin c.length, c.blocksFun i_1 < m * n
have inr : ∀ (h'c : 0 < c.length), ∑ i_1 : Fin c.length, c.blocksFun i_1 < m * n
Tactic: rcases eq_zero_or_pos c.length with h'c | h'c
-- 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
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
c : Composition i
v : (i : Fin i) → E
hc : c.length < m
hi : ∀ (j : Fin c.length), c.blocksFun j < n
h'c : c.length = 0
⊢ Eq (α := ℕ) (∑ j : Fin c.length, c.blocksFun j) 0
have apply : ∀ (j : Fin c.length) (hj : Membership.mem (γ := Finset (Fin c.length)) Finset.univ j), c.blocksFun j = 0
Tactic: apply Finset.sum_eq_zero (fun j hj ↦ ?_)