-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
/-- Composing a formal multilinear series with an ordered partition extended by adding a left point
to an already existing atom of index `i` corresponds to updating the `i`th block,
using `p (c.partSize i + 1)` instead of `p (c.partSize i)` there.
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_aux2 {m : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
    (p : FormalMultilinearSeries 𝕜 E F) (c : OrderedFinpartition m) (i : Fin c.length) :
    (q.compAlongOrderedFinpartition p (c.extend (some i))).curryLeft =
    ((c.compAlongOrderedFinpartitionL 𝕜 E F G (q c.length)).toContinuousLinearMap
      (fun i ↦ p (c.partSize i)) i).comp (p (c.partSize i + 1)).curryLeft

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
e : E
v : Fin m → E
j : Fin c.length
a✝ a : ℕ
ha : a + 1 < update c.partSize j (c.partSize j + 1) j
h'a : a + 1 < c.partSize j + 1
⊢ (cons e v ∘ (fun i => cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯) ⟨a + 1, ha⟩ = cons e (v ∘ c.emb j) ⟨a + 1, h'a⟩

Tactic:
simp [cons]

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
i : Fin c.length
e : E
v : Fin m → E
⊢ ((q c.length) fun m_1 =>
      (p (update c.partSize i (c.partSize i + 1) m_1))
        (cons e v ∘
          if h : m_1 = i then (fun i_1 => cases 0 (succ ∘ c.emb i) i_1) ∘ Fin.cast ⋯
          else succ ∘ c.emb m_1 ∘ Fin.cast ⋯)) =
    (q c.length) fun m_1 =>
      (update (fun i => p (c.partSize i)) i ((p (c.partSize i + 1)).curryLeft e) 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
i : Fin c.length
e : E
v : Fin m → E
⊢ (fun m_1 =>
      (p (update c.partSize i (c.partSize i + 1) m_1))
        (cons e v ∘
          if h : m_1 = i then (fun i_1 => cases 0 (succ ∘ c.emb i) i_1) ∘ Fin.cast ⋯
          else succ ∘ c.emb m_1 ∘ Fin.cast ⋯)) =
    fun m_1 => (update (fun i => p (c.partSize i)) i ((p (c.partSize i + 1)).curryLeft e) m_1) (v ∘ c.emb m_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
i : Fin c.length
e : E
v : Fin m → E
⊢ ((q.compAlongOrderedFinpartition p (c.extend (some i))).curryLeft e) v =
    (((((compAlongOrderedFinpartitionL 𝕜 E F G c) (q c.length)).toContinuousLinearMap (fun i => p (c.partSize i))
              i).comp
          (p (c.partSize i + 1)).curryLeft)
        e)
      v

Tactic:
simp only [Nat.succ_eq_add_one, OrderedFinpartition.extend, extendMiddle,
  ContinuousMultilinearMap.curryLeft_apply,
  FormalMultilinearSeries.compAlongOrderedFinpartition_apply, applyOrderedFinpartition_apply,
  ContinuousLinearMap.coe_comp', comp_apply,
  ContinuousMultilinearMap.toContinuousLinearMap_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
i : Fin c.length
e : E
v : Fin m → E
⊢ ((q c.length) fun m_1 =>
      (p (update c.partSize i (c.partSize i + 1) m_1))
        (cons e v ∘
          if h : m_1 = i then (fun i_1 => cases 0 (succ ∘ c.emb i) i_1) ∘ Fin.cast ⋯
          else succ ∘ c.emb m_1 ∘ Fin.cast ⋯)) =
    (q c.length) fun m_1 =>
      (update (fun i => p (c.partSize i)) i ((p (c.partSize i + 1)).curryLeft e) m_1) (v ∘ c.emb m_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
i : Fin c.length
e : E
v : Fin m → E
⊢ ((q.compAlongOrderedFinpartition p (c.extend (some i))).curryLeft e) v =
    (((((compAlongOrderedFinpartitionL 𝕜 E F G c) (q c.length)).toContinuousLinearMap (fun i => p (c.partSize i))
              i).comp
          (p (c.partSize i + 1)).curryLeft)
        e)
      v

Tactic:
simp? [OrderedFinpartition.extend, extendMiddle, applyOrderedFinpartition_apply] says
  simp only [Nat.succ_eq_add_one, OrderedFinpartition.extend, extendMiddle,
    ContinuousMultilinearMap.curryLeft_apply,
    FormalMultilinearSeries.compAlongOrderedFinpartition_apply, applyOrderedFinpartition_apply,
    ContinuousLinearMap.coe_comp', comp_apply,
    ContinuousMultilinearMap.toContinuousLinearMap_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
i : Fin c.length
e : E
v : Fin m → E
⊢ ((q c.length) fun m_1 =>
      (p (update c.partSize i (c.partSize i + 1) m_1))
        (cons e v ∘
          if h : m_1 = i then (fun i_1 => cases 0 (succ ∘ c.emb i) i_1) ∘ Fin.cast ⋯
          else succ ∘ c.emb m_1 ∘ Fin.cast ⋯)) =
    (q c.length) fun m_1 =>
      (update (fun i => p (c.partSize i)) i ((p (c.partSize i + 1)).curryLeft e) m_1) (v ∘ c.emb m_1)