awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
k' : ℕ
blocks_fun' : Fin k' → ℕ
H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun' ∈ compPartialSumSource m M N
heq :
  compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
    compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun') H'
⊢ k = k'
have this : Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) =
  (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
      Composition n).length
Tactic: have := (compChangeOfVariables_length m M N H).symm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
k' : ℕ
blocks_fun' : Fin k' → ℕ
H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun' ∈ compPartialSumSource m M N
heq :
  compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
    compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun') H'
this :
  Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) =
    (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length
⊢ k = k'
have rwa : ∀
  (this :
    Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) =
      (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun') H').snd (β := fun (n : ℕ) ↦
          Composition n).length),
  k = k'
Tactic: rwa [heq, compChangeOfVariables_length] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
k' : ℕ
blocks_fun' : Fin k' → ℕ
H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun' ∈ compPartialSumSource m M N
heq :
  compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
    compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun') H'
this :
  Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) =
    (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length
rwa :
  ∀
    (this :
      Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) =
        (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun') H').snd (β :=
            fun (n : ℕ) ↦ Composition n).length),
    k = k'
⊢ k = k'
have rwa₁ : ∀
  (this :
    Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) =
      Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun')),
  k = k'
Tactic: rwa [heq, compChangeOfVariables_length] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
k' : ℕ
blocks_fun' : Fin k' → ℕ
H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun' ∈ compPartialSumSource m M N
heq :
  compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
    compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun') H'
⊢ Eq (α := (n : ℕ) × (Fin n → ℕ)) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun)
    (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k' blocks_fun')
have i_inj : ∀ (blocks_fun' : Fin k → ℕ) (H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun' ∈ compPartialSumSource m M N)
  (heq :
    compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
      compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun') H'),
  Eq (α := (n : ℕ) × (Fin n → ℕ)) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun)
    (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun')
Tactic: obtain rfl : k = k' := by
      have := (compChangeOfVariables_length m M N H).symm
      rwa [heq, compChangeOfVariables_length] at this
Cleared hypotheses: k', blocks_fun', H', heq
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
blocks_fun' : Fin k → ℕ
H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun' ∈ compPartialSumSource m M N
heq :
  compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
    compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun') H'
⊢ Eq (α := (n : ℕ) × (Fin n → ℕ)) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun)
    (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun')
have i_inj : blocks_fun = blocks_fun'
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
blocks_fun' : Fin k → ℕ
H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun' ∈ compPartialSumSource m M N
heq :
  compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
    compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun') H'
⊢ blocks_fun = blocks_fun'
have i_inj : ∀ (i : Fin k), blocks_fun i = blocks_fun' i
Tactic: funext i
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
blocks_fun' : Fin k → ℕ
H' : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun' ∈ compPartialSumSource m M N
heq :
  compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H =
    compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun') H'
i : Fin k
⊢ blocks_fun i = blocks_fun' i
have blocks_fun₁ : (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
        Composition n).blocksFun
    (⟨(↑i : ℕ), sorry⟩ :
      Fin
        (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
            Composition n).length) =
  (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun') H').snd (β := fun (n : ℕ) ↦
        Composition n).blocksFun
    ⟨(↑i : ℕ), sorry⟩
Tactic: calc
      blocks_fun i = (compChangeOfVariables m M N _ H).2.blocksFun _ :=
        (compChangeOfVariables_blocksFun m M N H i).symm
      _ = (compChangeOfVariables m M N _ H').2.blocksFun _ := by
        grind
      _ = blocks_fun' i := compChangeOfVariables_blocksFun m M N H' i
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
i : (n : ℕ) × Composition n
hi : i ∈ compPartialSumTarget m M N
⊢ ∃ (a : (n : ℕ) × (Fin n → ℕ)) (ha : a ∈ compPartialSumSource m M N), compChangeOfVariables m M N a ha = i
have i_surj : i ∈ compPartialSumTargetSet m M N
Tactic: apply compPartialSumTargetSet_image_compPartialSumSource m M N i
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
⊢ Tendsto (β := Finset ((n : ℕ) × Composition n)) (fun (p : ℕ × ℕ) ↦ compPartialSumTarget 0 p.1 p.2) atTop atTop
have h : Monotone (β := Finset ((n : ℕ) × Composition n)) fun (p : ℕ × ℕ) ↦ compPartialSumTarget 0 p.1 p.2
Tactic: apply Monotone.tendsto_atTop_finset
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
h : Monotone (β := Finset ((n : ℕ) × Composition n)) fun (p : ℕ × ℕ) ↦ compPartialSumTarget 0 p.1 p.2
⊢ Tendsto (β := Finset ((n : ℕ) × Composition n)) (fun (p : ℕ × ℕ) ↦ compPartialSumTarget 0 p.1 p.2) atTop atTop
have h' : ∀ (x : (n : ℕ) × Composition n), ∃ (n : ℕ × ℕ), x ∈ compPartialSumTarget 0 n.1 n.2
Tactic: apply Monotone.tendsto_atTop_finset
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
m n : ℕ × ℕ
hmn : m ≤ n
a : (n : ℕ) × Composition n
ha : Membership.mem (γ := Finset ((n : ℕ) × Composition n)) ((fun (p : ℕ × ℕ) ↦ compPartialSumTarget 0 p.1 p.2) m) a
⊢ Membership.mem (γ := Finset ((n : ℕ) × Composition n)) ((fun (p : ℕ × ℕ) ↦ compPartialSumTarget 0 p.1 p.2) n) a
have this : ∀ i < m.1, i < n.1
Tactic: have : ∀ i, i < m.1 → i < n.1 := fun i hi => lt_of_lt_of_le hi hmn.1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
m n : ℕ × ℕ
hmn : m ≤ n
a : (n : ℕ) × Composition n
ha : Membership.mem (γ := Finset ((n : ℕ) × Composition n)) ((fun (p : ℕ × ℕ) ↦ compPartialSumTarget 0 p.1 p.2) m) a
this : ∀ i < m.1, i < n.1
⊢ Membership.mem (γ := Finset ((n : ℕ) × Composition n)) ((fun (p : ℕ × ℕ) ↦ compPartialSumTarget 0 p.1 p.2) n) a
have this₁ : ∀ i < m.2, i < n.2
Tactic: have : ∀ i, i < m.2 → i < n.2 := fun i hi => lt_of_lt_of_le hi hmn.2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
c : Composition n
⊢ ∃ (n_1 : ℕ × ℕ), Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c ∈ compPartialSumTarget 0 n_1.1 n_1.2
have h' : ∃ (n_1 : ℕ × ℕ), 0 ≤ c.length ∧ c.length < n_1.1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n_1.2
Tactic: simp only [mem_compPartialSumTarget_iff]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n : ℕ
c : Composition n
⊢ ∃ (n_1 : ℕ × ℕ), 0 ≤ c.length ∧ c.length < n_1.1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n_1.2
have h' : ∀ (n_1 : ℕ) (hn : n_1 ∈ upperBounds (↑(Finset.image (fun (i : Fin c.length) ↦ c.blocksFun i) Finset.univ) : Set ℕ)),
  ∃ (n_2 : ℕ × ℕ), 0 ≤ c.length ∧ c.length < n_2.1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n_2.2
Tactic: obtain ⟨n, hn⟩ : BddAbove ((Finset.univ.image fun i : Fin c.length => c.blocksFun i) : Set ℕ) :=
      Finset.bddAbove _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n_1 : ℕ
c : Composition n_1
n : ℕ
hn : n ∈ upperBounds (↑(Finset.image (fun (i : Fin c.length) ↦ c.blocksFun i) Finset.univ) : Set ℕ)
⊢ ∃ (n : ℕ × ℕ), 0 ≤ c.length ∧ c.length < n.1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n.2
have h' : ∀ (j : Fin c.length), c.blocksFun j ≤ n
Tactic: refine
      ⟨max n c.length + 1, bot_le, lt_of_le_of_lt (le_max_right n c.length) (lt_add_one _), fun j =>
        lt_of_le_of_lt (le_trans ?_ (le_max_left _ _)) (lt_add_one _)⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
n_1 : ℕ
c : Composition n_1
n : ℕ
hn : n ∈ upperBounds (↑(Finset.image (fun (i : Fin c.length) ↦ c.blocksFun i) Finset.univ) : Set ℕ)
j : Fin c.length
⊢ c.blocksFun j ≤ n
have h' : c.blocksFun j ∈ (↑(Finset.image (fun (i : Fin c.length) ↦ c.blocksFun i) Finset.univ) : Set ℕ)
Tactic: apply hn
-- 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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
⊢ q.partialSum M (∑ i ∈ Finset.Ico 1 N, (p i : (a : (i : Fin i) → E) → F) fun (_j : Fin i) ↦ z) =
    ∑ i ∈ compPartialSumTarget 0 M 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))) ↦ z
have suffices : Eq.{u_4 + 1} (α := G)
  (∑ n ∈ Finset.range M,
    ∑ r ∈ Fintype.piFinset (δ := fun (i : Fin n) ↦ ℕ) fun (i : Fin n) ↦ Finset.Ico 1 N,
      (q n : (a : (i : Fin n) → F) → G) fun (i : Fin n) ↦
        (p (r i) : (a : (i : Fin (r i)) → E) → F) fun (_j : Fin (r i)) ↦ z)
  (∑ i ∈ compPartialSumTarget 0 M 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))) ↦ z)
Tactic: suffices H :
    (∑ n ∈ Finset.range M,
        ∑ r ∈ Fintype.piFinset fun i : Fin n => Finset.Ico 1 N,
          q n fun i : Fin n => p (r i) fun _j => z) =
      ∑ i ∈ compPartialSumTarget 0 M N, q.compAlongComposition p i.2 fun _j => z by
    simpa only [FormalMultilinearSeries.partialSum, ContinuousMultilinearMap.map_sum_finset] using 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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
⊢ Eq.{u_4 + 1} (α := G)
    (∑ n ∈ Finset.range M,
      ∑ r ∈ Fintype.piFinset (δ := fun (i : Fin n) ↦ ℕ) fun (i : Fin n) ↦ Finset.Ico 1 N,
        (q n : (a : (i : Fin n) → F) → G) fun (i : Fin n) ↦
          (p (r i) : (a : (i : Fin (r i)) → E) → F) fun (_j : Fin (r i)) ↦ z)
    (∑ i ∈ compPartialSumTarget 0 M 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))) ↦ z)
have rw : Eq.{u_4 + 1} (α := G)
  (∑
    x ∈
      (Finset.Ico 0 M).sigma (α := fun (a : ℕ) ↦ (a : Fin a) → ℕ) fun (n : ℕ) ↦
        Fintype.piFinset (δ := fun (i : Fin n) ↦ ℕ) fun (i : Fin n) ↦ Finset.Ico 1 N,
    (q (x.fst (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ)) : (a : (i : Fin x.fst) → F) → G)
      fun (i : Fin (x.fst (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ))) ↦
      (p (x.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) i) : (a : (i : Fin (x.snd i)) → E) → F)
        fun (_j : Fin (x.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) i)) ↦ z)
  (∑ i ∈ compPartialSumTarget 0 M 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))) ↦ z)
Tactic: rw [Finset.range_eq_Ico, Finset.sum_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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
⊢ Eq.{u_4 + 1} (α := G)
    (∑
      x ∈
        (Finset.Ico 0 M).sigma (α := fun (a : ℕ) ↦ (a : Fin a) → ℕ) fun (n : ℕ) ↦
          Fintype.piFinset (δ := fun (i : Fin n) ↦ ℕ) fun (i : Fin n) ↦ Finset.Ico 1 N,
      (q (x.fst (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ)) : (a : (i : Fin x.fst) → F) → G)
        fun (i : Fin (x.fst (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ))) ↦
        (p (x.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) i) : (a : (i : Fin (x.snd i)) → E) → F)
          fun (_j : Fin (x.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) i)) ↦ z)
    (∑ i ∈ compPartialSumTarget 0 M 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))) ↦ z)
have h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource 0 M N),
  Eq.{u_4 + 1} (α := G)
    ((q (e.fst (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ)) : (a : (i : Fin e.fst) → F) → G)
        fun (i : Fin (e.fst (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ))) ↦
        (p (e.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) i) : (a : (i : Fin (e.snd i)) → E) → F)
          fun (_j : Fin (e.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) i)) ↦ z :
      G)
    ((q.compAlongComposition p ((compChangeOfVariables 0 M N e he).snd (β := fun (n : ℕ) ↦ Composition n)) :
          (a : (i : Fin (compChangeOfVariables 0 M N e he).fst) → E) → G)
        fun (_j : Fin ((compChangeOfVariables 0 M N e he).fst (β := fun (n : ℕ) ↦ Composition n))) ↦ z :
      G)
Tactic: apply compChangeOfVariables_sum 0 M N
-- 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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
k : ℕ
blocks_fun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource 0 M N
⊢ Eq.{u_4 + 1} (α := G)
    ((q (Sigma.fst (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun)) :
          (a : (i : Fin ⟨k, blocks_fun⟩.fst) → F) → G)
        fun
          (i :
            Fin
              (Sigma.fst (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun))) ↦
        (p (Sigma.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) i) :
            (a : (i : Fin (⟨k, blocks_fun⟩.snd i)) → E) → F)
          fun
            (_j :
              Fin
                (Sigma.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun)
                  i)) ↦
          z :
      G)
    ((q.compAlongComposition p
            ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β :=
              fun (n : ℕ) ↦ Composition n)) :
          (a : (i : Fin (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).fst) → E) → G)
        fun
          (_j :
            Fin
              ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).fst (β :=
                fun (n : ℕ) ↦ Composition n))) ↦
        z :
      G)
have h : ∀ (i : ℕ) (him : i < Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun))
  (hin :
    i <
      (compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
          Composition n).length),
  ((p (Sigma.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) ⟨i, him⟩) :
        (a : (i : Fin (⟨k, blocks_fun⟩.snd ⟨i, him⟩)) → E) → F)
      fun
        (_j :
          Fin
            (Sigma.snd (β := fun (i : ℕ) ↦ (a : Fin i) → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun)
              ⟨i, him⟩)) ↦
      z) =
    p.applyComposition
      ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
        Composition n))
      (fun
          (_j :
            Fin
              ((compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).fst (β :=
                fun (n : ℕ) ↦ Composition n))) ↦
        z)
      (⟨i, hin⟩ :
        Fin
          (compChangeOfVariables 0 M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H).snd (β := fun (n : ℕ) ↦
              Composition n).length)
Tactic: apply congr _ (compChangeOfVariables_length 0 M N H).symm
-- 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
hg : HasFPowerSeriesWithinAt g q t (f x)
hf : HasFPowerSeriesWithinAt f p s x
hs : Set.MapsTo f s t
⊢ HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x
have rcases : ∀ (rg : ℝ≥0∞) (Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg), HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x
Tactic: rcases hg with ⟨rg, Hg⟩
Cleared hypotheses: 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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hf : HasFPowerSeriesWithinAt f p s x
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
⊢ HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x
have rcases : ∀ (rf : ℝ≥0∞) (Hf : HasFPowerSeriesWithinOnBall f p s x rf), HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x
Tactic: rcases hf with ⟨rf, Hf⟩
Cleared hypotheses: 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
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
⊢ HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x
have rcases : ∀ (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)),
  HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x
Tactic: rcases q.comp_summable_nnreal p Hg.radius_pos Hf.radius_pos with ⟨r, r_pos : 0 < r, hr⟩