-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
/-- Composing two formal multilinear series `q` and `p` along an ordered partition extended by a
new atom to the left corresponds to applying `p 1` on the first coordinates, and the initial
ordered partition on the other coordinates.
This is one of the terms that appears when differentiating in the Faa di Bruno
formula, going from step `m` to step `m + 1`. -/
private lemma faaDiBruno_aux1 {m : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
    (p : FormalMultilinearSeries 𝕜 E F) (c : OrderedFinpartition m) :
    (q.compAlongOrderedFinpartition p (c.extend none)).curryLeft =
    ((c.compAlongOrderedFinpartitionL 𝕜 E F G).flipMultilinear fun i ↦ p (c.partSize i)).comp
      ((q (c.length + 1)).curryLeft.comp ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)))

Proof state:
case h.H
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : Fin m → E
⊢ ((q.compAlongOrderedFinpartition p (c.extend none)).curryLeft e) v =
    ((((compAlongOrderedFinpartitionL 𝕜 E F G c).flipMultilinear fun i => p (c.partSize i)).comp
          ((q (c.length + 1)).curryLeft.comp ((continuousMultilinearCurryFin1 𝕜 E F) (p 1))))
        e)
      v

Tactic:
simp only [Nat.succ_eq_add_one, OrderedFinpartition.extend, extendLeft,
  ContinuousMultilinearMap.curryLeft_apply,
  FormalMultilinearSeries.compAlongOrderedFinpartition_apply, applyOrderedFinpartition_apply,
  ContinuousLinearMap.coe_comp', comp_apply, continuousMultilinearCurryFin1_apply,
  Matrix.zero_empty, ContinuousLinearMap.flipMultilinear_apply_apply,
  compAlongOrderedFinpartitionL_apply, compAlongOrderFinpartition_apply]

Result:
case h.H
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : Fin m → E
⊢ ((q (c.length + 1)) fun m_1 =>
      (p (cons 1 c.partSize m_1))
        (cons e v ∘
          cases (motive := fun x => Fin (cons 1 c.partSize x) → Fin (m + 1)) (fun x => 0) (fun m_2 => succ ∘ c.emb m_2)
            m_1)) =
    (q (c.length + 1)) (cons ((p 1) (snoc ![] e)) fun m_1 => (p (c.partSize m_1)) (v ∘ c.emb m_1))

Proof state:
case h.H.h.e_6.h.h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : Fin m → E
j : Fin (c.length + 1)
⊢ (p (cons 1 c.partSize j))
      (cons e v ∘
        cases (motive := fun x => Fin (cons 1 c.partSize x) → Fin (m + 1)) (fun x => 0) (fun m_1 => succ ∘ c.emb m_1)
          j) =
    cons ((p 1) (snoc ![] e)) (fun m_1 => (p (c.partSize m_1)) (v ∘ c.emb m_1)) j

Tactic:
exact Fin.cases rfl (fun i ↦ rfl) j

Result:
no goals

Proof state:
case h.H
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : Fin m → E
⊢ ((q (c.length + 1)) fun m_1 =>
      (p (cons 1 c.partSize m_1))
        (cons e v ∘
          cases (motive := fun x => Fin (cons 1 c.partSize x) → Fin (m + 1)) (fun x => 0) (fun m_2 => succ ∘ c.emb m_2)
            m_1)) =
    (q (c.length + 1)) (cons ((p 1) (snoc ![] e)) fun m_1 => (p (c.partSize m_1)) (v ∘ c.emb m_1))

Tactic:
congr

Result:
case h.H.h.e_6.h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : Fin m → E
⊢ (fun m_1 =>
      (p (cons 1 c.partSize m_1))
        (cons e v ∘
          cases (motive := fun x => Fin (cons 1 c.partSize x) → Fin (m + 1)) (fun x => 0) (fun m_2 => succ ∘ c.emb m_2)
            m_1)) =
    cons ((p 1) (snoc ![] e)) fun m_1 => (p (c.partSize m_1)) (v ∘ c.emb m_1)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
⊢ (q.compAlongOrderedFinpartition p (c.extend none)).curryLeft =
    ((compAlongOrderedFinpartitionL 𝕜 E F G c).flipMultilinear fun i => p (c.partSize i)).comp
      ((q (c.length + 1)).curryLeft.comp ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)))

Tactic:
ext e v

Result:
case h.H
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : Fin m → E
⊢ ((q.compAlongOrderedFinpartition p (c.extend none)).curryLeft e) v =
    ((((compAlongOrderedFinpartitionL 𝕜 E F G c).flipMultilinear fun i => p (c.partSize i)).comp
          ((q (c.length + 1)).curryLeft.comp ((continuousMultilinearCurryFin1 𝕜 E F) (p 1))))
        e)
      v

Proof state:
case h.H.h.e_6.h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : Fin m → E
⊢ (fun m_1 =>
      (p (cons 1 c.partSize m_1))
        (cons e v ∘
          cases (motive := fun x => Fin (cons 1 c.partSize x) → Fin (m + 1)) (fun x => 0) (fun m_2 => succ ∘ c.emb m_2)
            m_1)) =
    cons ((p 1) (snoc ![] e)) fun m_1 => (p (c.partSize m_1)) (v ∘ c.emb m_1)

Tactic:
ext j

Result:
case h.H.h.e_6.h.h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : Fin m → E
j : Fin (c.length + 1)
⊢ (p (cons 1 c.partSize j))
      (cons e v ∘
        cases (motive := fun x => Fin (cons 1 c.partSize x) → Fin (m + 1)) (fun x => 0) (fun m_1 => succ ∘ c.emb m_1)
          j) =
    cons ((p 1) (snoc ![] e)) (fun m_1 => (p (c.partSize m_1)) (v ∘ c.emb m_1)) j