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
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousConstSMul 𝕜 E
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
h : k = c.index j
r : Fin (c.blocksFun (c.index j)) → Fin n := (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n)
j' : Fin (c.blocksFun (c.index j)) := c.invEmbedding j
⊢ Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r =
    Function.update (β := fun (a : Fin (c.blocksFun (c.index j))) ↦ E) (v ∘ r) j' z
have pos : Function.update (β := fun (a : Fin n) ↦ E) v (r j') z ∘ r =
  Function.update (β := fun (a : Fin (c.blocksFun (c.index j))) ↦ E) (v ∘ r) j' z
Tactic: suffices C : Function.update v (r j') z ∘ r = Function.update (v ∘ r) j' z by
      convert! C; exact (c.embedding_comp_inv j).symm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousConstSMul 𝕜 E
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
h : ¬k = c.index j
⊢ p.applyComposition c (Function.update (β := fun (a : Fin n) ↦ E) v j z) k =
    Function.update (β := fun (a : Fin c.length) ↦ F) (p.applyComposition c v) (c.index j)
      ((p (c.blocksFun (c.index j)) : (a : (i : Fin (c.blocksFun (c.index j))) → E) → F)
        (Function.update (β := fun (i : Fin (c.blocksFun (c.index j))) ↦ E)
          (v ∘ (⇑(c.embedding (c.index j)) : (a : Fin (c.blocksFun (c.index j))) → Fin n)) (c.invEmbedding j) z))
      k
have neg : p.applyComposition c (Function.update (β := fun (a : Fin n) ↦ E) v j z) k = p.applyComposition c v k
Tactic: simp only [h, Function.update_of_ne, Ne, not_false_iff]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousConstSMul 𝕜 E
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
h : ¬k = c.index j
r : Fin (c.blocksFun k) → Fin n := (⇑(c.embedding k) : (a : Fin (c.blocksFun k)) → Fin n)
⊢ p.applyComposition c (Function.update (β := fun (a : Fin n) ↦ E) v j z) k = p.applyComposition c v k
have neg : Eq.{u_3 + 1} (α := F)
  ((p (c.blocksFun k) : (a : (i : Fin (c.blocksFun k)) → E) → F)
      (Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r) :
    F)
  ((p (c.blocksFun k) : (a : (i : Fin (c.blocksFun k)) → E) → F) (v ∘ r) : F)
Tactic: change p (c.blocksFun k) (Function.update v j z ∘ r) = p (c.blocksFun k) (v ∘ r)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousConstSMul 𝕜 E
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
h : ¬k = c.index j
r : Fin (c.blocksFun k) → Fin n := (⇑(c.embedding k) : (a : Fin (c.blocksFun k)) → Fin n)
B : Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r = v ∘ r
⊢ Eq.{u_3 + 1} (α := F)
    ((p (c.blocksFun k) : (a : (i : Fin (c.blocksFun k)) → E) → F)
        (Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r) :
      F)
    ((p (c.blocksFun k) : (a : (i : Fin (c.blocksFun k)) → E) → F) (v ∘ r) : F)
have rw : Eq.{u_3 + 1} (α := F) ((p (c.blocksFun k) : (a : (i : Fin (c.blocksFun k)) → E) → F) (v ∘ r) : F)
  ((p (c.blocksFun k) : (a : (i : Fin (c.blocksFun k)) → E) → F) (v ∘ r) : F)
Tactic: rw [B]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousConstSMul 𝕜 E
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
h : ¬k = c.index j
r : Fin (c.blocksFun k) → Fin n := (⇑(c.embedding k) : (a : Fin (c.blocksFun k)) → Fin n)
⊢ Eq.{u_3 + 1} (α := F)
    ((p (c.blocksFun k) : (a : (i : Fin (c.blocksFun k)) → E) → F)
        (Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r) :
      F)
    ((p (c.blocksFun k) : (a : (i : Fin (c.blocksFun k)) → E) → F) (v ∘ r) : F)
have neg : Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r = v ∘ r
Tactic: suffices B : Function.update v j z ∘ r = v ∘ r by rw [B]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousConstSMul 𝕜 E
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
h : ¬k = c.index j
r : Fin (c.blocksFun k) → Fin n := (⇑(c.embedding k) : (a : Fin (c.blocksFun k)) → Fin n)
⊢ Function.update (β := fun (a : Fin n) ↦ E) v j z ∘ r = v ∘ r
have neg : j ∉ Set.range r
Tactic: apply Function.update_comp_eq_of_notMem_range
-- 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 : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
n : ℕ
p : FormalMultilinearSeries 𝕜 F G
f : E →L[𝕜] F
c : Composition n
v : Fin n → E
⊢ applyComposition (p.compContinuousLinearMap f) c v = p.applyComposition c ((⇑f : (a : E) → F) ∘ v)
have h : ∀ (x : Fin c.length),
  applyComposition (p.compContinuousLinearMap f) c v x = p.applyComposition c ((⇑f : (a : E) → F) ∘ v) x
Tactic: ext
-- 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 : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 0 → E
v' : Fin 0 → F
c : Composition 0 := Composition.ones 0
⊢ Eq.{u_4 + 1} (α := G) ((q.comp p 0 : (a : (i : Fin 0) → E) → G) v : G) ((q 0 : (a : (i : Fin 0) → F) → G) v' : G)
have dsimp : Eq.{u_4 + 1} (α := G) ((∑ c : Composition 0, q.compAlongComposition p c : (a : (i : Fin 0) → E) → G) v : G)
  ((q 0 : (a : (i : Fin 0) → F) → G) v' : G)
Tactic: dsimp [FormalMultilinearSeries.comp]
-- 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 : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 0 → E
v' : Fin 0 → F
c : Composition 0 := Composition.ones 0
⊢ Eq (α := Finset (Composition 0)) {c} Finset.univ
have h : Subset (α := Finset (Composition 0)) {c} Finset.univ
Tactic: apply Finset.eq_of_subset_of_card_le
-- 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 : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 0 → E
v' : Fin 0 → F
c : Composition 0 := Composition.ones 0
h : Subset (α := Finset (Composition 0)) {c} Finset.univ
⊢ Eq (α := Finset (Composition 0)) {c} Finset.univ
have h₂ : Finset.card (α := Composition 0) Finset.univ ≤ Finset.card (α := Composition 0) {c}
Tactic: apply Finset.eq_of_subset_of_card_le
-- 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 : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 0 → E
v' : Fin 0 → F
c : Composition 0 := Composition.ones 0
⊢ Eq.{u_4 + 1} (α := G) ((∑ c : Composition 0, q.compAlongComposition p c : (a : (i : Fin 0) → E) → G) v : G)
    ((q 0 : (a : (i : Fin 0) → F) → G) v' : G)
have this : Eq (α := Finset (Composition 0)) {c} Finset.univ
Tactic: have : {c} = (Finset.univ : Finset (Composition 0)) := by
    apply Finset.eq_of_subset_of_card_le <;> simp [Finset.card_univ, composition_card 0]
-- 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 : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 0 → E
v' : Fin 0 → F
c : Composition 0 := Composition.ones 0
this : Eq (α := Finset (Composition 0)) {c} Finset.univ
⊢ Eq.{u_4 + 1} (α := G) ((∑ c : Composition 0, q.compAlongComposition p c : (a : (i : Fin 0) → E) → G) v : G)
    ((q 0 : (a : (i : Fin 0) → F) → G) v' : G)
have rw : Eq.{u_4 + 1} (α := G) ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G)
  ((q 0 : (a : (i : Fin 0) → F) → G) v' : G)
Tactic: rw [← this, Finset.sum_singleton, compAlongComposition_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 : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 0 → E
v' : Fin 0 → F
c : Composition 0 := Composition.ones 0
this : Eq (α := Finset (Composition 0)) {c} Finset.univ
⊢ Eq.{u_4 + 1} (α := G) ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G)
    ((q 0 : (a : (i : Fin 0) → F) → G) v' : G)
have symm : Eq.{u_4 + 1} (α := G) ((q 0 : (a : (i : Fin 0) → F) → G) v' : G)
  ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G)
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousConstSMul 𝕜 E
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousConstSMul 𝕜 F
q : FormalMultilinearSeries 𝕜 E F
p : FormalMultilinearSeries 𝕜 E E
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (q.comp p 0) (q 0)
have H : ∀ (v : (i : Fin 0) → E),
  Eq.{u_3 + 1} (α := F) ((q.comp p 0 : (a : (i : Fin 0) → E) → F) v : F) ((q 0 : (a : (i : Fin 0) → E) → F) v : F)
Tactic: ext v
-- 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 : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 1 → E
⊢ Eq.{u_4 + 1} (α := G) ((q.comp p 1 : (a : (i : Fin 1) → E) → G) v : G)
    ((q 1 : (a : (i : Fin 1) → F) → G) fun (_i : Fin 1) ↦ (p 1 : (a : (i : Fin 1) → E) → F) v : G)
have this : Eq (α := Finset (Composition 1)) {Composition.ones 1} Finset.univ
Tactic: have : {Composition.ones 1} = (Finset.univ : Finset (Composition 1)) :=
    Finset.eq_univ_of_card _ (by simp [composition_card])
-- 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 : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 1 → E
this : Eq (α := Finset (Composition 1)) {Composition.ones 1} Finset.univ
⊢ Eq.{u_4 + 1} (α := G) ((q.comp p 1 : (a : (i : Fin 1) → E) → G) v : G)
    ((q 1 : (a : (i : Fin 1) → F) → G) fun (_i : Fin 1) ↦ (p 1 : (a : (i : Fin 1) → E) → F) v : G)
have simp : Eq.{u_4 + 1} (α := G)
  ((q (Composition.length (n := 1) (Composition.ones 1)) : (a : (i : Fin (Composition.ones 1).length) → F) → G)
      (p.applyComposition (Composition.ones 1) v) :
    G)
  ((q 1 : (a : (i : Fin 1) → F) → G) fun (_i : Fin 1) ↦ (p 1 : (a : (i : Fin 1) → E) → F) v : G)
Tactic: simp only [FormalMultilinearSeries.comp, compAlongComposition_apply, ← this,
    Finset.sum_singleton]
-- 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 : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 1 → E
this : Eq (α := Finset (Composition 1)) {Composition.ones 1} Finset.univ
⊢ Eq.{u_4 + 1} (α := G)
    ((q (Composition.length (n := 1) (Composition.ones 1)) : (a : (i : Fin (Composition.ones 1).length) → F) → G)
        (p.applyComposition (Composition.ones 1) v) :
      G)
    ((q 1 : (a : (i : Fin 1) → F) → G) fun (_i : Fin 1) ↦ (p 1 : (a : (i : Fin 1) → E) → F) v : G)
have refine : ∀ (i : ℕ) (hi1 : i < Composition.length (n := 1) (Composition.ones 1)) (hi2 : i < 1),
  p.applyComposition (Composition.ones 1) v (⟨i, hi1⟩ : Fin (Composition.length (n := 1) (Composition.ones 1))) =
    (p 1 : (a : (i : Fin 1) → E) → F) v
Tactic: refine q.congr (by simp) fun i hi1 hi2 => ?_
-- 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 : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 1 → E
this : Eq (α := Finset (Composition 1)) {Composition.ones 1} Finset.univ
i : ℕ
hi1 : i < Composition.length (n := 1) (Composition.ones 1)
hi2 : i < 1
⊢ p.applyComposition (Composition.ones 1) v (⟨i, hi1⟩ : Fin (Composition.length (n := 1) (Composition.ones 1))) =
    (p 1 : (a : (i : Fin 1) → E) → F) v
have simp : Eq.{u_3 + 1} (α := F)
  ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦
      v (Fin.castLE sorry (⟨i, hi1⟩ : Fin (Composition.length (n := 1) (Composition.ones 1)))) :
    F)
  ((p 1 : (a : (i : Fin 1) → E) → F) v : F)
Tactic: simp only [applyComposition_ones]
-- 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 : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : 0 < n
⊢ q.removeZero.comp p n = q.comp p n
have H : ∀ (v : (i : Fin n) → E),
  Eq.{u_4 + 1} (α := G) ((q.removeZero.comp p n : (a : (i : Fin n) → E) → G) v : G)
    ((q.comp p n : (a : (i : Fin n) → 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 : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : 0 < n
v : (i : Fin n) → E
⊢ Eq.{u_4 + 1} (α := G) ((q.removeZero.comp p n : (a : (i : Fin n) → E) → G) v : G)
    ((q.comp p n : (a : (i : Fin n) → E) → G) v : G)
have H : Eq.{u_4 + 1} (α := G)
  (∑ x : Composition n, (q.removeZero x.length : (a : (i : Fin x.length) → F) → G) (p.applyComposition x v))
  (∑ x : Composition n, (q x.length : (a : (i : Fin x.length) → F) → G) (p.applyComposition x v))
Tactic: simp only [FormalMultilinearSeries.comp, compAlongComposition,
    ContinuousMultilinearMap.compAlongComposition_apply, ContinuousMultilinearMap.sum_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 : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : 0 < n
v : (i : Fin n) → E
⊢ Eq.{u_4 + 1} (α := G)
    (∑ x : Composition n, (q.removeZero x.length : (a : (i : Fin x.length) → F) → G) (p.applyComposition x v))
    (∑ x : Composition n, (q x.length : (a : (i : Fin x.length) → F) → G) (p.applyComposition x v))
have H : ∀ (c : Composition n) (_hc : Membership.mem (γ := Finset (Composition n)) Finset.univ c),
  Eq.{u_4 + 1} (α := G) ((q.removeZero c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G)
    ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G)
Tactic: refine Finset.sum_congr rfl fun c _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 : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : 0 < n
v : (i : Fin n) → E
c : Composition n
_hc : Membership.mem (γ := Finset (Composition n)) Finset.univ c
⊢ Eq.{u_4 + 1} (α := G) ((q.removeZero c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G)
    ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G)
have H : Eq.{u_4 + 1} (α := G) ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G)
  ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G)
Tactic: rw [removeZero_of_pos _ (c.length_pos_of_pos hn)]