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
H : Type u_5
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
n : ℕ
p : FormalMultilinearSeries 𝕜 E F
c_1 : Composition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c_1.length) ↦ F) G
v : (i : Fin n) → E
i : Fin n
c : 𝕜
x : E
⊢ (fun (v : (i : Fin n) → E) ↦ ((f : (a : (i : Fin c_1.length) → F) → G) (p.applyComposition c_1 v) : G))
      (Function.update (β := fun (i : Fin n) ↦ E) v i (c • x)) =
    HSMul.hSMul (β := G) c
      ((fun (v : (i : Fin n) → E) ↦ ((f : (a : (i : Fin c_1.length) → F) → G) (p.applyComposition c_1 v) : G))
        (Function.update (β := fun (i : Fin n) ↦ E) v i x))

Tactic:
simp only [applyComposition_update, map_update_smul]

Premises used: ContinuousMultilinearMap.map_update_smul, FormalMultilinearSeries.applyComposition_update
-- Module: Mathlib.Analysis.Analytic.Composition
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
n : ℕ
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
v : Fin n → E
⊢ Eq.{u_4 + 1} (α := G) ((compAlongComposition p c f : (a : (i : Fin n) → E) → G) v : G)
    ((f : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Analytic.Composition
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 : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
v : Fin n → E
⊢ Eq.{u_4 + 1} (α := G) ((q.compAlongComposition p c : (a : (i : Fin n) → E) → G) v : G)
    ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Analytic.Composition
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
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)
⊢ 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)

Tactic:
dsimp [FormalMultilinearSeries.comp]

Premises used: FormalMultilinearSeries.comp
-- Module: Mathlib.Analysis.Analytic.Composition
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
h₂ : Finset.card (α := Composition 0) Finset.univ ≤ Finset.card (α := Composition 0) {c}
⊢ Eq (α := Finset (Composition 0)) {c} Finset.univ

Tactic:
apply Finset.eq_of_subset_of_card_le

Premises used: Finset.eq_of_subset_of_card_le
-- Module: Mathlib.Analysis.Analytic.Composition
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
⊢ Subset (α := Finset (Composition 0)) {c} Finset.univ

Tactic:
simp [Finset.card_univ, composition_card 0]

Premises used: Finset.card_univ, composition_card, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.Composition
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
⊢ Finset.card (α := Composition 0) Finset.univ ≤ Finset.card (α := Composition 0) {c}

Tactic:
simp [Finset.card_univ, composition_card 0]

Premises used: Finset.card_univ, composition_card, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.Composition
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

Tactic:
have : {c} = (Finset.univ : Finset (Composition 0)) := by
    apply Finset.eq_of_subset_of_card_le <;> simp [Finset.card_univ, composition_card 0]
-- Module: Mathlib.Analysis.Analytic.Composition
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
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)
⊢ 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:
rw [← this, Finset.sum_singleton, compAlongComposition_apply]

Premises used: Finset.sum_singleton, FormalMultilinearSeries.compAlongComposition_apply
-- Module: Mathlib.Analysis.Analytic.Composition
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
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)
⊢ 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:
symm
-- Module: Mathlib.Analysis.Analytic.Composition
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 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:
congr!
-- Module: Mathlib.Analysis.Analytic.Composition
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
⊢ 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) fun (_i : Fin 0) ↦ 0 : G)

Tactic:
q.comp_coeff_zero p v _

Premises used: FormalMultilinearSeries.comp_coeff_zero
-- Module: Mathlib.Analysis.Analytic.Composition
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
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)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (q.comp p 0) (q 0)

Tactic:
ext v
-- Module: Mathlib.Analysis.Analytic.Composition
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
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:
q.comp_coeff_zero p _ _

Premises used: FormalMultilinearSeries.comp_coeff_zero
-- Module: Mathlib.Analysis.Analytic.Composition
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
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:
exact q.comp_coeff_zero p _ _

Premises used: FormalMultilinearSeries.comp_coeff_zero
-- Module: Mathlib.Analysis.Analytic.Composition
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
⊢ Finset.card (α := Composition 1) {Composition.ones 1} = Fintype.card (Composition 1)

Tactic:
simp [composition_card]

Premises used: composition_card
-- Module: Mathlib.Analysis.Analytic.Composition
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 (α := 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])
-- Module: Mathlib.Analysis.Analytic.Composition
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
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)
⊢ 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)

Tactic:
simp only [FormalMultilinearSeries.comp, compAlongComposition_apply, ← this,
    Finset.sum_singleton]

Premises used: Finset.sum_singleton, FormalMultilinearSeries.compAlongComposition_apply, FormalMultilinearSeries.comp
-- Module: Mathlib.Analysis.Analytic.Composition
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
⊢ Composition.length (n := 1) (Composition.ones 1) = 1

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Composition
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
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
⊢ 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:
refine q.congr (by simp) fun i hi1 hi2 => ?_

Premises used: FormalMultilinearSeries.congr
-- Module: Mathlib.Analysis.Analytic.Composition
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
simp :
  Eq.{u_3 + 1} (α := F)
    ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦
        v (Fin.castLE ⋯ (⟨i, hi1⟩ : Fin (Composition.length (n := 1) (Composition.ones 1)))) :
      F)
    ((p 1 : (a : (i : Fin 1) → E) → F) v : F)
⊢ 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:
simp only [applyComposition_ones]

Premises used: FormalMultilinearSeries.applyComposition_ones
-- Module: Mathlib.Analysis.Analytic.Composition
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
j : ℕ
_hj1 hj2 : j < 1
⊢ v (Fin.castLE ⋯ (⟨i, hi1⟩ : Fin (Composition.length (n := 1) (Composition.ones 1)))) = v ⟨j, hj2⟩

Tactic:
congr!
-- Module: Mathlib.Analysis.Analytic.Composition
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
⊢ Eq.{u_3 + 1} (α := F)
    ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦
        v (Fin.castLE ⋯ (⟨i, hi1⟩ : Fin (Composition.length (n := 1) (Composition.ones 1)))) :
      F)
    ((p 1 : (a : (i : Fin 1) → E) → F) v : F)

Tactic:
exact p.congr rfl fun j _hj1 hj2 => by congr!

Premises used: FormalMultilinearSeries.congr, rfl
-- Module: Mathlib.Analysis.Analytic.Composition
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
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)
⊢ q.removeZero.comp p n = q.comp p n

Tactic:
ext v
-- Module: Mathlib.Analysis.Analytic.Composition
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
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))
⊢ 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:
simp only [FormalMultilinearSeries.comp, compAlongComposition,
    ContinuousMultilinearMap.compAlongComposition_apply, ContinuousMultilinearMap.sum_apply]

Premises used: FormalMultilinearSeries.compAlongComposition, ContinuousMultilinearMap.sum_apply, ContinuousMultilinearMap.compAlongComposition_apply, FormalMultilinearSeries.comp