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

Proof state:
case neg.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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
A : Disjoint (range (c.emb m)) (range (c.emb (c.index j)))
this : j ∈ range (c.emb (c.index j))
⊢ j ∉ range (c.emb m)

Tactic:
exact Set.disjoint_right.1 A this

Result:
no goals

Proof state:
case neg.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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
⊢ j ∉ range (c.emb m)

Tactic:
have A : Disjoint (range (c.emb m)) (range (c.emb (c.index j))) :=
  c.disjoint (mem_univ m) (mem_univ (c.index j)) h

Result:
case neg.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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
A : Disjoint (range (c.emb m)) (range (c.emb (c.index j)))
⊢ j ∉ range (c.emb m)

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
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : m = c.index j
⊢ c.applyOrderedFinpartition p (update v j z) (c.index j) =
    update (c.applyOrderedFinpartition p v) (c.index j)
      ((p (c.index j)) (update (v ∘ c.emb (c.index j)) (c.invEmbedding j) z)) (c.index j)

Tactic:
simp only [applyOrderedFinpartition, update_self]

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
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : m = c.index j
⊢ (p (c.index j)) (update v j z ∘ c.emb (c.index j)) =
    (p (c.index j)) (update (v ∘ c.emb (c.index j)) (c.invEmbedding j) z)

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
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : m = c.index j
⊢ c.applyOrderedFinpartition p (update v j z) m =
    update (c.applyOrderedFinpartition p v) (c.index j)
      ((p (c.index j)) (update (v ∘ c.emb (c.index j)) (c.invEmbedding j) z)) m

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
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : m = c.index j
⊢ c.applyOrderedFinpartition p (update v j z) (c.index j) =
    update (c.applyOrderedFinpartition p v) (c.index j)
      ((p (c.index j)) (update (v ∘ c.emb (c.index j)) (c.invEmbedding j) z)) (c.index j)

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

Tactic:
apply Function.update_comp_eq_of_not_mem_range

Result:
case neg.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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
⊢ j ∉ range (c.emb m)

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
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
⊢ (p m) (update v j z ∘ c.emb m) = (p m) (v ∘ c.emb m)

Tactic:
congr

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

Proof state:
case pos.h.e_6.h.hf
𝕜 : 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
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : m = c.index j
⊢ Injective (c.emb (c.index j))

Tactic:
exact (c.emb_strictMono (c.index j)).injective

Result:
no goals

Proof state:
case neg.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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
A : Disjoint (range (c.emb m)) (range (c.emb (c.index j)))
⊢ j ∉ range (c.emb m)

Tactic:
have : j ∈ range (c.emb (c.index j)) := mem_range.2 ⟨c.invEmbedding j, by simp⟩

Result:
case neg.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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
A : Disjoint (range (c.emb m)) (range (c.emb (c.index j)))
this : j ∈ range (c.emb (c.index j))
⊢ j ∉ range (c.emb m)