awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
v : (i : Fin n) → E
i : ℕ
him : i < (Composition.ones n).length
hin : i < n
h : (↑(Fin.castLE ⋯ (⟨i, him⟩ : Fin (Composition.ones n).length)) : ℕ) = (↑(⟨i, hin⟩ : Fin n) : ℕ)
h₁ : (↑(⟨i, him⟩ : Fin (Composition.ones n).length) : ℕ) = (↑(⟨i, hin⟩ : Fin n) : ℕ)
h₂ h₃ : i = i
⊢ Fin.castLE ⋯ (⟨i, him⟩ : Fin (Composition.ones n).length) = ⟨i, hin⟩

Tactic:
rw [Fin.ext_iff, Fin.val_castLE, Fin.val_mk]

Premises used: Fin.ext_iff, Fin.val_mk, Fin.val_castLE
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h :
  Membership.mem (γ := Finset (Composition n)) Finset.univ b →
    b ≠ Composition.ones n → p.compAlongComposition (id 𝕜 E x) b = 0
⊢ Membership.mem (γ := Finset (Composition n)) Finset.univ b →
    b ≠ Composition.ones n → p.compAlongComposition (id 𝕜 E x) b = 0

Tactic:
_
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
⊢ ∃ k ∈ b.blocks, 1 < k

Tactic:
Composition.ne_ones_iff.1 hb

Premises used: Composition.ne_ones_iff, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h_1 : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
h : ∀ (k : ℕ) (hk : k ∈ b.blocks) (lt_k : 1 < k), p.compAlongComposition (id 𝕜 E x) b = 0
⊢ p.compAlongComposition (id 𝕜 E x) b = 0

Tactic:
obtain ⟨k, hk, lt_k⟩ : ∃ (k : ℕ), k ∈ Composition.blocks b ∧ 1 < k :=
      Composition.ne_ones_iff.1 hb

Premises used: Composition.blocks, Composition.ne_ones_iff, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
⊢ ∃ (i : Fin b.blocks.length),
    getElem (valid := fun (xs : List ℕ) (i : Fin b.blocks.length) ↦ (↑i : ℕ) < xs.length) b.blocks i ⋯ = k

Tactic:
List.get_of_mem hk

Premises used: List.get_of_mem
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h_1 : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
h :
  ∀ (i : Fin b.blocks.length)
    (hi : getElem (valid := fun (xs : List ℕ) (i : Fin b.blocks.length) ↦ (↑i : ℕ) < xs.length) b.blocks i ⋯ = k),
    p.compAlongComposition (id 𝕜 E x) b = 0
⊢ p.compAlongComposition (id 𝕜 E x) b = 0

Tactic:
obtain ⟨i, hi⟩ : ∃ (i : Fin b.blocks.length), b.blocks[i] = k :=
      List.get_of_mem hk

Premises used: List.get_of_mem, Composition.blocks, Fin, List.length
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : getElem (valid := fun (xs : List ℕ) (i : Fin b.blocks.length) ↦ (↑i : ℕ) < xs.length) b.blocks i ⋯ = k
j : Fin b.length := ⟨(↑i : ℕ), ⋯⟩
⊢ 1 < k

Tactic:
lt_k
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : getElem (valid := fun (xs : List ℕ) (i : Fin b.blocks.length) ↦ (↑i : ℕ) < xs.length) b.blocks i ⋯ = k
j : Fin b.length := ⟨(↑i : ℕ), ⋯⟩
⊢ 1 < b.blocksFun j

Tactic:
convert! lt_k
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : getElem (valid := fun (xs : List ℕ) (i : Fin b.blocks.length) ↦ (↑i : ℕ) < xs.length) b.blocks i ⋯ = k
j : Fin b.length := ⟨(↑i : ℕ), ⋯⟩
⊢ 1 < b.blocksFun j

Tactic:
have A : 1 < b.blocksFun j := by convert! lt_k
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h_1 : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : getElem (valid := fun (xs : List ℕ) (i : Fin b.blocks.length) ↦ (↑i : ℕ) < xs.length) b.blocks i ⋯ = k
j : Fin b.length := ⟨(↑i : ℕ), ⋯⟩
A : 1 < b.blocksFun j
h :
  ∀ (v : (i : Fin n) → E),
    Eq.{u_3 + 1} (α := F) ((p.compAlongComposition (id 𝕜 E x) b : (a : (i : Fin n) → E) → F) v : F)
      ((0 : (a : (i : Fin n) → E) → F) v : F)
⊢ p.compAlongComposition (id 𝕜 E x) b = 0

Tactic:
ext v
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h_1 : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : getElem (valid := fun (xs : List ℕ) (i : Fin b.blocks.length) ↦ (↑i : ℕ) < xs.length) b.blocks i ⋯ = k
j : Fin b.length := ⟨(↑i : ℕ), ⋯⟩
A : 1 < b.blocksFun j
v : (i : Fin n) → E
h :
  Eq.{u_3 + 1} (α := F) ((p b.length : (a : (i : Fin b.length) → E) → F) (applyComposition (id 𝕜 E x) b v) : F) (0 : F)
⊢ Eq.{u_3 + 1} (α := F) ((p.compAlongComposition (id 𝕜 E x) b : (a : (i : Fin n) → E) → F) v : F)
    ((0 : (a : (i : Fin n) → E) → F) v : F)

Tactic:
rw [compAlongComposition_apply, ContinuousMultilinearMap.zero_apply]

Premises used: FormalMultilinearSeries.compAlongComposition_apply, ContinuousMultilinearMap.zero_apply
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h_1 : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : getElem (valid := fun (xs : List ℕ) (i : Fin b.blocks.length) ↦ (↑i : ℕ) < xs.length) b.blocks i ⋯ = k
j : Fin b.length := ⟨(↑i : ℕ), ⋯⟩
A : 1 < b.blocksFun j
v : (i : Fin n) → E
h : applyComposition (id 𝕜 E x) b v j = 0
⊢ Eq.{u_3 + 1} (α := F) ((p b.length : (a : (i : Fin b.length) → E) → F) (applyComposition (id 𝕜 E x) b v) : F) (0 : F)

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
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h_1 : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : getElem (valid := fun (xs : List ℕ) (i : Fin b.blocks.length) ↦ (↑i : ℕ) < xs.length) b.blocks i ⋯ = k
j : Fin b.length := ⟨(↑i : ℕ), ⋯⟩
A : 1 < b.blocksFun j
v : (i : Fin n) → E
h :
  Eq (α := E)
    ((id 𝕜 E x (b.blocksFun j) : (a : (i : Fin (b.blocksFun j)) → E) → E)
        (v ∘ (⇑(b.embedding j) : (a : Fin (b.blocksFun j)) → Fin n)) :
      E)
    (0 : E)
⊢ applyComposition (id 𝕜 E x) b v j = 0

Tactic:
dsimp [applyComposition]

Premises used: FormalMultilinearSeries.applyComposition
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
h_1 : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : getElem (valid := fun (xs : List ℕ) (i : Fin b.blocks.length) ↦ (↑i : ℕ) < xs.length) b.blocks i ⋯ = k
j : Fin b.length := ⟨(↑i : ℕ), ⋯⟩
A : 1 < b.blocksFun j
v : (i : Fin n) → E
h :
  Eq (α := E)
    ((0 : (a : (i : Fin (b.blocksFun j)) → E) → E) (v ∘ (⇑(b.embedding j) : (a : Fin (b.blocksFun j)) → Fin n)) : E)
    (0 : E)
h₁ h₂ : Eq.{u_2 + 1} (α := E) 0 0
⊢ Eq (α := E)
    ((id 𝕜 E x (b.blocksFun j) : (a : (i : Fin (b.blocksFun j)) → E) → E)
        (v ∘ (⇑(b.embedding j) : (a : Fin (b.blocksFun j)) → Fin n)) :
      E)
    (0 : E)

Tactic:
rw [id_apply_of_one_lt _ _ _ A, ContinuousMultilinearMap.zero_apply]

Premises used: FormalMultilinearSeries.id_apply_of_one_lt, ContinuousMultilinearMap.zero_apply
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
⊢ Composition.ones n ∉ Finset.univ → p.compAlongComposition (id 𝕜 E x) (Composition.ones n) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
h : ∀ (n : ℕ), FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p n = p n
⊢ FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p = p

Tactic:
ext1 n
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p 0) (p 0)
h₁ : ∀ (n_pos : n > 0), FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p n = p n
⊢ FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p n = p n

Tactic:
obtain rfl | n_pos := n.eq_zero_or_pos

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
h :
  ∀ (v : (i : Fin 0) → E),
    Eq.{u_3 + 1} (α := F)
      ((FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p 0 : (a : (i : Fin 0) → E) → F)
          v :
        F)
      ((p 0 : (a : (i : Fin 0) → E) → F) v : F)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p 0) (p 0)

Tactic:
ext v
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 v : (i : Fin 0) → E
h : Eq.{u_3 + 1} (α := F) ((p 0 : (a : (i : Fin 0) → E) → F) v0 : F) ((p 0 : (a : (i : Fin 0) → E) → F) v : F)
⊢ Eq.{u_3 + 1} (α := F)
    ((FormalMultilinearSeries.comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p 0 : (a : (i : Fin 0) → E) → F) v :
      F)
    ((p 0 : (a : (i : Fin 0) → E) → F) v : F)

Tactic:
simp only [comp_coeff_zero', id_apply_zero]

Premises used: FormalMultilinearSeries.comp_coeff_zero', FormalMultilinearSeries.id_apply_zero
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 v : (i : Fin 0) → E
h : ∀ (i : Fin 0), v0 i = v i
⊢ Eq.{u_3 + 1} (α := F) ((p 0 : (a : (i : Fin 0) → E) → F) v0 : F) ((p 0 : (a : (i : Fin 0) → E) → F) v : F)

Tactic:
congr with i
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 v : (i : Fin 0) → E
i : Fin 0
⊢ v0 i = v i

Tactic:
i.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 v : (i : Fin 0) → E
i : Fin 0
⊢ v0 i = v i

Tactic:
exact i.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
h : compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p (Composition.single n n_pos) = p n
h₁ :
  ∀ (b : Composition n),
    Membership.mem (γ := Finset (Composition n)) Finset.univ b →
      b ≠ Composition.single n n_pos → compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p b = 0
h₂ :
  Composition.single n n_pos ∉ Finset.univ →
    compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p (Composition.single n n_pos) = 0
⊢ ∑ c : Composition n, compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p c = p n

Tactic:
rw [Finset.sum_eq_single (Composition.single n n_pos)]

Premises used: Composition.single, Finset.sum_eq_single
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
h :
  ∀ (v : (i : Fin n) → E),
    Eq.{u_3 + 1} (α := F)
      ((compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p (Composition.single n n_pos) :
            (a : (i : Fin n) → E) → F)
          v :
        F)
      ((p n : (a : (i : Fin n) → E) → F) v : F)
⊢ compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p (Composition.single n n_pos) = p n

Tactic:
ext v
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
v : (i : Fin n) → E
h :
  p.applyComposition (Composition.single n n_pos) v (⟨0, ⋯⟩ : Fin (Composition.single n n_pos).length) =
    (p n : (a : (i : Fin n) → E) → F) v
⊢ Eq.{u_3 + 1} (α := F)
    ((compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p (Composition.single n n_pos) :
          (a : (i : Fin n) → E) → F)
        v :
      F)
    ((p n : (a : (i : Fin n) → E) → F) v : F)

Tactic:
rw [compAlongComposition_apply, id_apply_one' _ _ _ (Composition.single_length n_pos)]

Premises used: FormalMultilinearSeries.id_apply_one', Composition.single_length, FormalMultilinearSeries.compAlongComposition_apply
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
v : (i : Fin n) → E
h :
  Eq.{u_3 + 1} (α := F)
    ((p ((Composition.single n n_pos).blocksFun 0) : (a : (i : Fin ((Composition.single n n_pos).blocksFun 0)) → E) → F)
        (v ∘
          (⇑((Composition.single n n_pos).embedding 0) :
            (a : Fin ((Composition.single n n_pos).blocksFun 0)) → Fin n)) :
      F)
    ((p n : (a : (i : Fin n) → E) → F) v : F)
⊢ p.applyComposition (Composition.single n n_pos) v (⟨0, ⋯⟩ : Fin (Composition.single n n_pos).length) =
    (p n : (a : (i : Fin n) → E) → F) v

Tactic:
dsimp [applyComposition]

Premises used: FormalMultilinearSeries.applyComposition
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
v : (i : Fin n) → E
⊢ Eq.{u_3 + 1} (α := F)
    ((p ((Composition.single n n_pos).blocksFun 0) : (a : (i : Fin ((Composition.single n n_pos).blocksFun 0)) → E) → F)
        (v ∘
          (⇑((Composition.single n n_pos).embedding 0) :
            (a : Fin ((Composition.single n n_pos).blocksFun 0)) → Fin n)) :
      F)
    ((p n : (a : (i : Fin n) → E) → F) v : F)

Tactic:
p.congr rfl fun i him hin => congr_arg v <| ?_

Premises used: FormalMultilinearSeries.congr, congr_arg, rfl
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
v : (i : Fin n) → E
h :
  ∀ (i : ℕ) (him : i < (Composition.single n n_pos).blocksFun 0) (hin : i < n),
    ((Composition.single n n_pos).embedding 0 : (a : Fin ((Composition.single n n_pos).blocksFun 0)) → Fin n) ⟨i, him⟩ =
      (⟨i, hin⟩ : Fin n)
⊢ Eq.{u_3 + 1} (α := F)
    ((p ((Composition.single n n_pos).blocksFun 0) : (a : (i : Fin ((Composition.single n n_pos).blocksFun 0)) → E) → F)
        (v ∘
          (⇑((Composition.single n n_pos).embedding 0) :
            (a : Fin ((Composition.single n n_pos).blocksFun 0)) → Fin n)) :
      F)
    ((p n : (a : (i : Fin n) → E) → F) v : F)

Tactic:
refine p.congr rfl fun i him hin => congr_arg v <| ?_

Premises used: FormalMultilinearSeries.congr, congr_arg, rfl
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
v : (i : Fin n) → E
i : ℕ
him : i < (Composition.single n n_pos).blocksFun 0
hin : i < n
h :
  (↑(((Composition.single n n_pos).embedding 0 : (a : Fin ((Composition.single n n_pos).blocksFun 0)) → Fin n)
          (⟨i, him⟩ : Fin ((Composition.single n n_pos).blocksFun 0))) :
      ℕ) =
    (↑(⟨i, hin⟩ : Fin n) : ℕ)
⊢ ((Composition.single n n_pos).embedding 0 : (a : Fin ((Composition.single n n_pos).blocksFun 0)) → Fin n) ⟨i, him⟩ =
    (⟨i, hin⟩ : Fin n)

Tactic:
ext
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
v : (i : Fin n) → E
i : ℕ
him : i < (Composition.single n n_pos).blocksFun 0
hin : i < n
⊢ (↑(((Composition.single n n_pos).embedding 0 : (a : Fin ((Composition.single n n_pos).blocksFun 0)) → Fin n)
          (⟨i, him⟩ : Fin ((Composition.single n n_pos).blocksFun 0))) :
      ℕ) =
    (↑(⟨i, hin⟩ : Fin n) : ℕ)

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
h :
  Membership.mem (γ := Finset (Composition n)) Finset.univ b →
    b ≠ Composition.single n n_pos → compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p b = 0
⊢ Membership.mem (γ := Finset (Composition n)) Finset.univ b →
    b ≠ Composition.single n n_pos → compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p b = 0

Tactic:
_
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.single n n_pos
⊢ b.length ≠ 1

Tactic:
simpa [Composition.eq_single_iff_length] using hb

Premises used: Composition.eq_single_iff_length
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.single n n_pos
⊢ b.length ≠ 1

Tactic:
have : b.length ≠ 1 := by simpa [Composition.eq_single_iff_length] using hb
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.single n n_pos
this : b.length ≠ 1
⊢ 0 < b.length

Tactic:
have : 0 < b.length := Composition.length_pos_of_pos b n_pos