awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Composition
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
j : Fin c.length
hj : Membership.mem (γ := Finset (Fin c.length)) Finset.univ j
this : (↑j : ℕ) < c.length
⊢ c.blocksFun j = 0

Tactic:
grind
-- Module: Mathlib.Analysis.Analytic.Composition
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

Tactic:
have : ∑ j : Fin c.length, c.blocksFun j = 0 := by
        apply Finset.sum_eq_zero (fun j hj ↦ ?_)
        have := j.2
        grind
-- Module: Mathlib.Analysis.Analytic.Composition
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
this : Eq (α := ℕ) (∑ j : Fin c.length, c.blocksFun j) 0
inl : 0 < m * n
⊢ ∑ i_1 : Fin c.length, c.blocksFun i_1 < m * n

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Analytic.Composition
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
this : Eq (α := ℕ) (∑ j : Fin c.length, c.blocksFun j) 0
⊢ 0 < m

Tactic:
grind
-- Module: Mathlib.Analysis.Analytic.Composition
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
this : Eq (α := ℕ) (∑ j : Fin c.length, c.blocksFun j) 0
⊢ 0 < m * n

Tactic:
exact mul_pos (by grind) hn

Premises used: mul_pos
-- Module: Mathlib.Analysis.Analytic.Composition
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 : 0 < c.length
apply : ∃ (i_1 : Fin c.length), Membership.mem (γ := Finset (Fin c.length)) Finset.univ i_1 ∧ c.blocksFun i_1 < n
⊢ LT.lt (α := ℕ) (∑ j : Fin c.length, c.blocksFun j) (∑ j : Fin c.length, n)

Tactic:
apply Finset.sum_lt_sum (fun j hj ↦ (hi j).le)

Premises used: LT.lt.le, Finset.sum_lt_sum
-- Module: Mathlib.Analysis.Analytic.Composition
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 : 0 < c.length
⊢ ∃ (i_1 : Fin c.length), Membership.mem (γ := Finset (Fin c.length)) Finset.univ i_1 ∧ c.blocksFun i_1 < n

Tactic:
⟨⟨0, h'c⟩, Finset.mem_univ _, hi _⟩

Premises used: Finset.mem_univ, Fin.mk, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.Composition
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 : 0 < c.length
⊢ ∃ (i_1 : Fin c.length), Membership.mem (γ := Finset (Fin c.length)) Finset.univ i_1 ∧ c.blocksFun i_1 < n

Tactic:
exact ⟨⟨0, h'c⟩, Finset.mem_univ _, hi _⟩
-- Module: Mathlib.Analysis.Analytic.Composition
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 : 0 < c.length
⊢ ∑ j : Fin c.length, n = c.length * n

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Composition
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 : 0 < c.length
⊢ c.length * n ≤ m * n

Tactic:
gcongr
-- Module: Mathlib.Analysis.Analytic.Composition
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 : 0 < c.length
calc : LT.lt (α := ℕ) (∑ j : Fin c.length, c.blocksFun j) (∑ j : Fin c.length, n)
calc₁ : ∑ j : Fin c.length, n = c.length * n
calc₂ : c.length * n ≤ m * n
⊢ ∑ i_1 : Fin c.length, c.blocksFun i_1 < m * n

Tactic:
calc ∑ j : Fin c.length, c.blocksFun j
      _ < ∑ j : Fin c.length, n := by
        apply Finset.sum_lt_sum (fun j hj ↦ (hi j).le)
        exact ⟨⟨0, h'c⟩, Finset.mem_univ _, hi _⟩
      _ = c.length * n := by simp
      _ ≤ m * n := by gcongr

Premises used: Composition.length, Fin
-- Module: Mathlib.Analysis.Analytic.Composition
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
h :
  ∀ (j : Fin c.length) (hj : n ≤ c.blocksFun j),
    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)

Tactic:
obtain ⟨j, hj⟩ : ∃ j, n ≤ c.blocksFun j := by
    contrapose! hi
    rw [← c.sum_blocksFun]
    rcases eq_zero_or_pos c.length with h'c | h'c
    · have : ∑ j : Fin c.length, c.blocksFun j = 0 := by
        apply Finset.sum_eq_zero (fun j hj ↦ ?_)
        have := j.2
        grind
      rw [this]
      exact mul_pos (by grind) hn
    · calc ∑ j : Fin c.length, c.blocksFun j
      _ < ∑ j : Fin c.length, n := by
        apply Finset.sum_lt_sum (fun j hj ↦ (hi j).le)
        exact ⟨⟨0, h'c⟩, Finset.mem_univ _, hi _⟩
      _ = c.length * n := by simp
      _ ≤ m * n := by gcongr
-- Module: Mathlib.Analysis.Analytic.Composition
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
hj : n ≤ c.blocksFun j
h : p.applyComposition c v j = 0
⊢ Eq.{u_4 + 1} (α := G) ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G) (0 : G)

Tactic:
apply ContinuousMultilinearMap.map_coord_zero _ j

Premises used: ContinuousMultilinearMap.map_coord_zero
-- Module: Mathlib.Analysis.Analytic.Composition
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
hj : n ≤ c.blocksFun j
⊢ p.applyComposition c v j = 0

Tactic:
simp [applyComposition, hf.finite _ hj]

Premises used: HasFiniteFPowerSeriesAt.finite, FormalMultilinearSeries.applyComposition
-- Module: Mathlib.Analysis.Analytic.Composition
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 : CPolynomialAt 𝕜 g (f x)
hf : CPolynomialAt 𝕜 f x
rcases :
  ∀ (q : FormalMultilinearSeries 𝕜 F G) (m : ℕ) (hm : HasFiniteFPowerSeriesAt g q (f x) m), CPolynomialAt 𝕜 (g ∘ f) x
⊢ CPolynomialAt 𝕜 (g ∘ f) x

Tactic:
rcases hg with ⟨q, m, hm⟩
-- Module: Mathlib.Analysis.Analytic.Composition
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
hf : CPolynomialAt 𝕜 f x
q : FormalMultilinearSeries 𝕜 F G
m : ℕ
hm : HasFiniteFPowerSeriesAt g q (f x) m
rcases : ∀ (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) (hn : HasFiniteFPowerSeriesAt f p x n), CPolynomialAt 𝕜 (g ∘ f) x
⊢ CPolynomialAt 𝕜 (g ∘ f) x

Tactic:
rcases hf with ⟨p, n, hn⟩
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
m : ℕ
hm : HasFiniteFPowerSeriesAt g q (f x) m
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : HasFiniteFPowerSeriesAt f p x n
⊢ CPolynomialAt 𝕜 (g ∘ f) x

Tactic:
⟨q.comp p, m * (n + 1), ?_⟩

Premises used: HMul.hMul, HAdd.hAdd, Exists.intro, CPolynomialAt, FormalMultilinearSeries.comp, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
m : ℕ
hm : HasFiniteFPowerSeriesAt g q (f x) m
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : HasFiniteFPowerSeriesAt f p x n
refine : HasFiniteFPowerSeriesAt (g ∘ f) (q.comp p) x (m * (n + 1))
⊢ CPolynomialAt 𝕜 (g ∘ f) x

Tactic:
refine ⟨q.comp p, m * (n + 1), ?_⟩
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
m : ℕ
hm : HasFiniteFPowerSeriesAt g q (f x) m
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : HasFiniteFPowerSeriesAt f p x n
⊢ HasFiniteFPowerSeriesAt (g ∘ f) (q.comp p) x (m * (n + 1))

Tactic:
hm.comp (hn.of_le (Nat.le_succ n)) (Nat.zero_lt_succ n)

Premises used: HasFiniteFPowerSeriesAt.of_le, Nat.zero_lt_succ, Nat.le_succ, HasFiniteFPowerSeriesAt.comp
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
m : ℕ
hm : HasFiniteFPowerSeriesAt g q (f x) m
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : HasFiniteFPowerSeriesAt f p x n
⊢ HasFiniteFPowerSeriesAt (g ∘ f) (q.comp p) x (m * (n + 1))

Tactic:
exact hm.comp (hn.of_le (Nat.le_succ n)) (Nat.zero_lt_succ n)

Premises used: HasFiniteFPowerSeriesAt.of_le, Nat.zero_lt_succ, Nat.le_succ, HasFiniteFPowerSeriesAt.comp
-- Module: Mathlib.Analysis.Analytic.Composition
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 : CPolynomialAt 𝕜 g (f x)
hf : CPolynomialAt 𝕜 f x
⊢ CPolynomialAt.{u_1, u_2, u_4} 𝕜 (F := G) (fun (z : E) ↦ g (f z)) x

Tactic:
hg.comp hf

Premises used: CPolynomialAt.comp
-- Module: Mathlib.Analysis.Analytic.Composition
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 : CPolynomialAt 𝕜 g y
hf : CPolynomialAt 𝕜 f x
hy : f x = y
⊢ CPolynomialAt 𝕜 g (f x)

Tactic:
rw [← hy] at hg
-- Module: Mathlib.Analysis.Analytic.Composition
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 : CPolynomialAt 𝕜 g y
hf : CPolynomialAt 𝕜 f x
hy : f x = y
hg₁ : CPolynomialAt 𝕜 g (f x)
⊢ CPolynomialAt 𝕜 f x

Tactic:
rw [← hy] at hg
-- Module: Mathlib.Analysis.Analytic.Composition
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 : CPolynomialAt 𝕜 g y
hf : CPolynomialAt 𝕜 f x
hy : f x = y
hg₁ : CPolynomialAt 𝕜 g (f x)
hf₁ : CPolynomialAt 𝕜 f x
⊢ f x = y

Tactic:
rw [← hy] at hg
-- Module: Mathlib.Analysis.Analytic.Composition
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 : CPolynomialAt 𝕜 g (f x)
hf : CPolynomialAt 𝕜 f x
hy : f x = y
⊢ CPolynomialAt 𝕜 (g ∘ f) x

Tactic:
hg.comp hf

Premises used: CPolynomialAt.comp
-- Module: Mathlib.Analysis.Analytic.Composition
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 : CPolynomialAt 𝕜 g (f x)
hf : CPolynomialAt 𝕜 f x
hy : f x = y
⊢ CPolynomialAt 𝕜 (g ∘ f) x

Tactic:
exact hg.comp hf

Premises used: CPolynomialAt.comp
-- Module: Mathlib.Analysis.Analytic.Composition
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 : CPolynomialAt 𝕜 g y
hf : CPolynomialAt 𝕜 f x
hy : f x = y
⊢ CPolynomialAt.{u_1, u_2, u_4} 𝕜 (F := G) (fun (z : E) ↦ g (f z)) x

Tactic:
hg.comp_of_eq hf hy

Premises used: CPolynomialAt.comp_of_eq
-- Module: Mathlib.Analysis.Analytic.Composition
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
s : Set E
g : F → G
f : E → F
hg : CPolynomialOn 𝕜 g (f '' s)
hf : CPolynomialOn 𝕜 f s
⊢ CPolynomialOn 𝕜 (g ∘ f) s

Tactic:
fun z hz => (hg (f z) (Set.mem_image_of_mem f hz)).comp (hf z hz)

Premises used: Set.mem_image_of_mem, CPolynomialAt.comp, CPolynomialOn
-- Module: Mathlib.Analysis.Analytic.Composition
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
s : Set E
t : Set F
g : F → G
f : E → F
hg : CPolynomialOn 𝕜 g t
hf : CPolynomialOn 𝕜 f s
st : Set.MapsTo f s t
⊢ CPolynomialOn 𝕜 (g ∘ f) s

Tactic:
comp' (mono hg (Set.mapsTo_iff_image_subset.mp st)) hf

Premises used: CPolynomialOn.comp', Set.mapsTo_iff_image_subset, Iff.mp, CPolynomialOn.mono
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
i : (a : Composition n) × Composition a.length
⊢ i.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks =
      i.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks ∧
    i.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks =
      i.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks

Tactic:
⟨rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
i : (a : Composition n) × Composition a.length
⊢ i.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks =
      i.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks ∧
    i.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks =
      i.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks

Tactic:
exact ⟨rfl, rfl⟩
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
i j : (a : Composition n) × Composition a.length
refine :
  i.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks =
        j.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks ∧
      i.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks =
        j.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks →
    i = j
⊢ i = j ↔
    i.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks =
        j.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks ∧
      i.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks =
        j.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks

Tactic:
refine ⟨by rintro rfl; exact ⟨rfl, rfl⟩, ?_⟩
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
n : ℕ
i j : (a : Composition n) × Composition a.length
rcases :
  ∀ (a : Composition n) (b : Composition a.length),
    (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
              (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).blocks =
          j.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks ∧
        blocks (n :=
            (Sigma.fst (β := fun (a : Composition n) ↦ Composition a.length)
                (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)).length)
            (Sigma.snd (β := fun (a : Composition n) ↦ Composition a.length)
              (Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b)) =
          j.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks →
      Sigma.mk (β := fun (a : Composition n) ↦ Composition a.length) a b = j
⊢ i.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks =
        j.fst (β := fun (a : Composition n) ↦ Composition a.length).blocks ∧
      i.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks =
        j.snd (β := fun (a : Composition n) ↦ Composition a.length).blocks →
    i = j

Tactic:
rcases i with ⟨a, b⟩