-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
theorem applyOrderedFinpartition_update_left (p : ∀ (i : Fin c.length), E[×c.partSize i]→L[𝕜] F)
    (m : Fin c.length) (v : Fin n → E) (q : E[×c.partSize m]→L[𝕜] F) :
    c.applyOrderedFinpartition (update p m q) v
      = update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m))

Proof state:
case 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
m : Fin c.length
v : Fin n → E
q : ContinuousMultilinearMap 𝕜 (fun i => E) F
d : Fin c.length
⊢ c.applyOrderedFinpartition (update p m q) v d = update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m)) d

Tactic:
by_cases h : d = m

Result:
case pos
𝕜 : 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
m : Fin c.length
v : Fin n → E
q : ContinuousMultilinearMap 𝕜 (fun i => E) F
d : Fin c.length
h : d = m
⊢ c.applyOrderedFinpartition (update p m q) v d = update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m)) d

case neg
𝕜 : 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
m : Fin c.length
v : Fin n → E
q : ContinuousMultilinearMap 𝕜 (fun i => E) F
d : Fin c.length
h : ¬d = m
⊢ c.applyOrderedFinpartition (update p m q) v d = update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m)) d

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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
m : Fin c.length
v : Fin n → E
q : ContinuousMultilinearMap 𝕜 (fun i => E) F
⊢ c.applyOrderedFinpartition (update p m q) v = update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m))

Tactic:
ext d

Result:
case 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
m : Fin c.length
v : Fin n → E
q : ContinuousMultilinearMap 𝕜 (fun i => E) F
d : Fin c.length
⊢ c.applyOrderedFinpartition (update p m q) v d = update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m)) d

Proof state:
case neg
𝕜 : 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
m : Fin c.length
v : Fin n → E
q : ContinuousMultilinearMap 𝕜 (fun i => E) F
d : Fin c.length
h : ¬d = m
⊢ c.applyOrderedFinpartition (update p m q) v d = update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m)) d

Tactic:
simp [h, applyOrderedFinpartition]

Result:
no goals

Proof state:
case pos
𝕜 : 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
m : Fin c.length
v : Fin n → E
q : ContinuousMultilinearMap 𝕜 (fun i => E) F
d : Fin c.length
h : d = m
⊢ c.applyOrderedFinpartition (update p m q) v m = update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m)) m

Tactic:
simp [applyOrderedFinpartition]

Result:
no goals

Proof state:
case pos
𝕜 : 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
m : Fin c.length
v : Fin n → E
q : ContinuousMultilinearMap 𝕜 (fun i => E) F
d : Fin c.length
h : d = m
⊢ c.applyOrderedFinpartition (update p m q) v d = update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m)) d

Tactic:
rw [h]

Result:
case pos
𝕜 : 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
m : Fin c.length
v : Fin n → E
q : ContinuousMultilinearMap 𝕜 (fun i => E) F
d : Fin c.length
h : d = m
⊢ c.applyOrderedFinpartition (update p m q) v m = update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m)) m