-- Mathlib/Analysis/Analytic/IteratedFDeriv.lean
lemma ContinuousMultilinearMap.iteratedFDeriv_comp_diagonal
    {n : ℕ} (f : E [×n]→L[𝕜] F) (x : E) (v : Fin n → E) :
    iteratedFDeriv 𝕜 n (fun x ↦ f (fun _ ↦ x)) x v = ∑ σ : Perm (Fin n), f (fun i ↦ v (σ i))

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 : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i => ContinuousLinearMap.id 𝕜 E
⊢ (iteratedFDeriv 𝕜 n (fun x => f fun x_1 => x) x) v =
    ∑ i : Perm (Fin n), f fun i_1 => v (((Equiv.inv (Perm (Fin n))) i) i_1)

Tactic:
change iteratedFDeriv 𝕜 n (f ∘ g) x v = _

Result:
𝕜 : 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 : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i => ContinuousLinearMap.id 𝕜 E
⊢ (iteratedFDeriv 𝕜 n (⇑f ∘ ⇑g) x) v = ∑ i : Perm (Fin n), f fun i_1 => v (((Equiv.inv (Perm (Fin n))) i) i_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
n : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i => ContinuousLinearMap.id 𝕜 E
⊢ (iteratedFDeriv 𝕜 n (⇑f ∘ ⇑g) x) v = ∑ i : Perm (Fin n), f fun i_1 => v (((Equiv.inv (Perm (Fin n))) i) i_1)

Tactic:
rw [ContinuousLinearMap.iteratedFDeriv_comp_right _ f.contDiff _ le_rfl, f.iteratedFDeriv_eq]

Result:
𝕜 : 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 : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i => ContinuousLinearMap.id 𝕜 E
⊢ ((f.iteratedFDeriv n (g x)).compContinuousLinearMap fun x => g) v =
    ∑ i : Perm (Fin n), f fun i_1 => v (((Equiv.inv (Perm (Fin n))) i) i_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
n : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i => ContinuousLinearMap.id 𝕜 E
σ : Fin n ↪ Fin n
i : Fin n
this : Function.Bijective ⇑σ
⊢ ∃ y, σ y = i

Tactic:
exact this.surjective i

Result:
no goals

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 : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i => ContinuousLinearMap.id 𝕜 E
σ : Fin n ↪ Fin n
i : Fin n
⊢ ∃ y, σ y = i

Tactic:
have : Function.Bijective σ := (Fintype.bijective_iff_injective_and_card _).2 ⟨σ.injective, rfl⟩

Result:
𝕜 : 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 : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i => ContinuousLinearMap.id 𝕜 E
σ : Fin n ↪ Fin n
i : Fin n
this : Function.Bijective ⇑σ
⊢ ∃ y, σ y = i

Proof state:
case e_f.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
n : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i => ContinuousLinearMap.id 𝕜 E
σ : Fin n ↪ Fin n
i : Fin n
A : ∃ y, σ y = i
⊢ (if h : ∃ y, σ y = i then g (v (σ.toEquivRange.symm ⟨i, ⋯⟩)) i else g x i) =
    v (((Equiv.inv (Perm (Fin n))) ((embeddingEquivOfFinite (Fin n)) σ)) i)

Tactic:
rcases A with ⟨y, rfl⟩

Result:
case e_f.h.h.e_6.h.h.intro
𝕜 : 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 : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i => ContinuousLinearMap.id 𝕜 E
σ : Fin n ↪ Fin n
y : Fin n
⊢ (if h : ∃ y_1, σ y_1 = σ y then g (v (σ.toEquivRange.symm ⟨σ y, ⋯⟩)) (σ y) else g x (σ y)) =
    v (((Equiv.inv (Perm (Fin n))) ((embeddingEquivOfFinite (Fin n)) σ)) (σ y))

Proof state:
case e_f.h.h.e_6.h.h.intro.e_a
𝕜 : 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 : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i => ContinuousLinearMap.id 𝕜 E
σ : Fin n ↪ Fin n
y : Fin n
⊢ y = ((Equiv.inv (Perm (Fin n))) ((embeddingEquivOfFinite (Fin n)) σ)) (σ y)

Tactic:
symm

Result:
case e_f.h.h.e_6.h.h.intro.e_a
𝕜 : 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 : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i => ContinuousLinearMap.id 𝕜 E
σ : Fin n ↪ Fin n
y : Fin n
⊢ ((Equiv.inv (Perm (Fin n))) ((embeddingEquivOfFinite (Fin n)) σ)) (σ y) = y

Proof state:
case e_f.h.h.e_6.h.h.intro
𝕜 : 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 : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i => ContinuousLinearMap.id 𝕜 E
σ : Fin n ↪ Fin n
y : Fin n
⊢ (if h : ∃ y_1, σ y_1 = σ y then g (v (σ.toEquivRange.symm ⟨σ y, ⋯⟩)) (σ y) else g x (σ y)) =
    v (((Equiv.inv (Perm (Fin n))) ((embeddingEquivOfFinite (Fin n)) σ)) (σ y))

Tactic:
simp only [EmbeddingLike.apply_eq_iff_eq, exists_eq, ↓reduceDIte,
  Function.Embedding.toEquivRange_symm_apply_self, ContinuousLinearMap.coe_pi',
  ContinuousLinearMap.coe_id', id_eq, g]

Result:
case e_f.h.h.e_6.h.h.intro
𝕜 : 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 : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i => ContinuousLinearMap.id 𝕜 E
σ : Fin n ↪ Fin n
y : Fin n
⊢ v y = v (((Equiv.inv (Perm (Fin n))) ((embeddingEquivOfFinite (Fin n)) σ)) (σ y))