-- 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:
case h.H.h.e_6.h.h.inr
𝕜 : 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
j : Fin c.length
hij : j ≠ i
⊢ (p (update c.partSize i (c.partSize i + 1) j))
      (cons e v ∘
        if h : j = i then (fun i_1 => cases 0 (succ ∘ c.emb i) i_1) ∘ Fin.cast ⋯ else succ ∘ c.emb j ∘ Fin.cast ⋯) =
    (update (fun i => p (c.partSize i)) i ((p (c.partSize i + 1)).curryLeft e) j) (v ∘ c.emb j)

Tactic:
simp only [hij, ↓reduceDIte, ne_eq, not_false_eq_true, update_of_ne]

Result:
case h.H.h.e_6.h.h.inr
𝕜 : 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
j : Fin c.length
hij : j ≠ i
⊢ (p (update c.partSize i (c.partSize i + 1) j)) (cons e v ∘ succ ∘ c.emb j ∘ Fin.cast ⋯) =
    (p (c.partSize j)) (v ∘ c.emb j)

Proof state:
case h.H.h.e_6.h.h.inl
𝕜 : 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
⊢ ∀ (i : ℕ) (him : i < update c.partSize j (c.partSize j + 1) j) (hin : i < c.partSize j + 1),
    (cons e v ∘ (fun i => cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯) ⟨i, him⟩ = cons e (v ∘ c.emb j) ⟨i, hin⟩

Tactic:
intro a ha h'a

Result:
case h.H.h.e_6.h.h.inl
𝕜 : 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 : ℕ
ha : a < update c.partSize j (c.partSize j + 1) j
h'a : a < c.partSize j + 1
⊢ (cons e v ∘ (fun i => cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯) ⟨a, ha⟩ = cons e (v ∘ c.emb j) ⟨a, h'a⟩

Proof state:
case h.H.h.e_6.h.h.inl
𝕜 : 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
⊢ (p (update c.partSize j (c.partSize j + 1) j)) (cons e v ∘ (fun i => cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯) =
    (p (c.partSize j + 1)) (cons e (v ∘ c.emb j))

Tactic:
apply FormalMultilinearSeries.congr _ (by simp)

Result:
case h.H.h.e_6.h.h.inl
𝕜 : 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
⊢ ∀ (i : ℕ) (him : i < update c.partSize j (c.partSize j + 1) j) (hin : i < c.partSize j + 1),
    (cons e v ∘ (fun i => cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯) ⟨i, him⟩ = cons e (v ∘ c.emb j) ⟨i, hin⟩

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
i : Fin c.length
e : E
v : Fin m → E
j : Fin c.length
⊢ (p (update c.partSize i (c.partSize i + 1) j))
      (cons e v ∘
        if h : j = i then (fun i_1 => cases 0 (succ ∘ c.emb i) i_1) ∘ Fin.cast ⋯ else succ ∘ c.emb j ∘ Fin.cast ⋯) =
    (update (fun i => p (c.partSize i)) i ((p (c.partSize i + 1)).curryLeft e) j) (v ∘ c.emb j)

Tactic:
rcases eq_or_ne j i with rfl | hij

Result:
case h.H.h.e_6.h.h.inl
𝕜 : 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
⊢ (p (update c.partSize j (c.partSize j + 1) j))
      (cons e v ∘
        if h : j = j then (fun i => cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯ else succ ∘ c.emb j ∘ Fin.cast ⋯) =
    (update (fun i => p (c.partSize i)) j ((p (c.partSize j + 1)).curryLeft e) j) (v ∘ c.emb j)

case h.H.h.e_6.h.h.inr
𝕜 : 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
j : Fin c.length
hij : j ≠ i
⊢ (p (update c.partSize i (c.partSize i + 1) j))
      (cons e v ∘
        if h : j = i then (fun i_1 => cases 0 (succ ∘ c.emb i) i_1) ∘ Fin.cast ⋯ else succ ∘ c.emb j ∘ Fin.cast ⋯) =
    (update (fun i => p (c.partSize i)) i ((p (c.partSize i + 1)).curryLeft e) j) (v ∘ c.emb j)

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
i : Fin c.length
e : E
v : Fin m → E
j : Fin c.length
hij : j ≠ i
⊢ update c.partSize i (c.partSize i + 1) j = c.partSize j

Tactic:
simp [hij]

Result:
no goals