-- 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
⊢ (∑ x_1 : Fin n ↪ Fin n, f fun j => if h : ∃ y, x_1 y = j then g (v (x_1.toEquivRange.symm ⟨j, ⋯⟩)) j else g x j) =
    ∑ i : Perm (Fin n), f fun i_1 => v (((Equiv.inv (Perm (Fin n))) i) i_1)

Tactic:
rw [← sum_comp (Equiv.embeddingEquivOfFinite (Fin n))]

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
⊢ (∑ x_1 : Fin n ↪ Fin n, f fun j => if h : ∃ y, x_1 y = j then g (v (x_1.toEquivRange.symm ⟨j, ⋯⟩)) j else g x j) =
    ∑ i : Fin n ↪ Fin n, f fun i_1 => v (((Equiv.inv (Perm (Fin n))) ((embeddingEquivOfFinite (Fin n)) i)) i_1)

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
⊢ (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:
have A : ∃ y, σ y = i := by
  have : Function.Bijective σ := (Fintype.bijective_iff_injective_and_card _).2 ⟨σ.injective, rfl⟩
  exact this.surjective i

Result:
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)

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
⊢ (∑ x_1 : Fin n ↪ Fin n, f fun j => if h : ∃ y, x_1 y = j then g (v (x_1.toEquivRange.symm ⟨j, ⋯⟩)) j else g x j) =
    ∑ i : Fin n ↪ Fin n, f fun i_1 => v (((Equiv.inv (Perm (Fin n))) ((embeddingEquivOfFinite (Fin n)) i)) i_1)

Tactic:
congr with σ

Result:
case e_f.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
⊢ (f fun j => if h : ∃ y, σ y = j then g (v (σ.toEquivRange.symm ⟨j, ⋯⟩)) j else g x j) =
    f fun i => v (((Equiv.inv (Perm (Fin n))) ((embeddingEquivOfFinite (Fin n)) σ)) i)

Proof state:
case e_f.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
⊢ (f fun j => if h : ∃ y, σ y = j then g (v (σ.toEquivRange.symm ⟨j, ⋯⟩)) j else g x j) =
    f fun i => v (((Equiv.inv (Perm (Fin n))) ((embeddingEquivOfFinite (Fin n)) σ)) i)

Tactic:
congr with i

Result:
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
⊢ (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)

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
⊢ ((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)

Tactic:
simp only [ContinuousMultilinearMap.iteratedFDeriv,
  ContinuousMultilinearMap.compContinuousLinearMap_apply, ContinuousMultilinearMap.sum_apply,
  ContinuousMultilinearMap.iteratedFDerivComponent_apply, Set.mem_range, Pi.compRightL_apply]

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
⊢ (∑ x_1 : Fin n ↪ Fin n, f fun j => if h : ∃ y, x_1 y = j then g (v (x_1.toEquivRange.symm ⟨j, ⋯⟩)) j else g x j) =
    ∑ i : Perm (Fin n), f fun i_1 => v (((Equiv.inv (Perm (Fin n))) i) i_1)

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
⊢ ((Equiv.inv (Perm (Fin n))) ((embeddingEquivOfFinite (Fin n)) σ)) (σ y) = y

Tactic:
simp [coe_fn_mk, inv_apply, Perm.inv_def,
  ofBijective_symm_apply_apply, Function.Embedding.equivOfFiniteSelfEmbedding]

Result:
no goals

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
⊢ v y = v (((Equiv.inv (Perm (Fin n))) ((embeddingEquivOfFinite (Fin n)) σ)) (σ y))

Tactic:
congr 1

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
⊢ y = ((Equiv.inv (Perm (Fin n))) ((embeddingEquivOfFinite (Fin n)) σ)) (σ y)