-- Mathlib/Analysis/Analytic/IteratedFDeriv.lean
theorem ContDiffWithinAt.iteratedFDerivWithin_comp_perm
    (h : ContDiffWithinAt 𝕜 ω f s x) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ} (v : Fin n → E)
    (σ : Perm (Fin n)) :
    iteratedFDerivWithin 𝕜 n f s x (v ∘ σ) = iteratedFDerivWithin 𝕜 n f s x v

Proof state:
case intro.intro.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
f : E → F
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 ω f (s ∩ u)
this : iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x
⊢ (iteratedFDerivWithin 𝕜 n f (s ∩ u) x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f (s ∩ u) x) v

Tactic:
exact AnalyticOn.iteratedFDerivWithin_comp_perm hu.analyticOn (hs.inter u_open) ⟨hx, xu⟩ _ _

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
f : E → F
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ ω = ∞ → ω = ω

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.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
f : E → F
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 ω f (s ∩ u)
⊢ (iteratedFDerivWithin 𝕜 n f s x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f s x) v

Tactic:
have : iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x :=
  iteratedFDerivWithin_inter_open u_open xu

Result:
case intro.intro.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
f : E → F
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 ω f (s ∩ u)
this : iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x
⊢ (iteratedFDerivWithin 𝕜 n f s x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f s x) v

Proof state:
case intro.intro.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
f : E → F
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 ω f (s ∩ u)
this : iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x
⊢ (iteratedFDerivWithin 𝕜 n f s x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f s x) v

Tactic:
rw [← this]

Result:
case intro.intro.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
f : E → F
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 ω f (s ∩ u)
this : iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x
⊢ (iteratedFDerivWithin 𝕜 n f (s ∩ u) x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f (s ∩ u) x) v

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
f : E → F
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ (iteratedFDerivWithin 𝕜 n f s x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f s x) v

Tactic:
rcases h.contDiffOn' le_rfl (by simp) with ⟨u, u_open, xu, hu⟩

Result:
case intro.intro.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
f : E → F
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 ω f (insert x s ∩ u)
⊢ (iteratedFDerivWithin 𝕜 n f s x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f s x) v

Proof state:
case intro.intro.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
f : E → F
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 ω f (insert x s ∩ u)
⊢ (iteratedFDerivWithin 𝕜 n f s x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f s x) v

Tactic:
rw [insert_eq_of_mem hx] at hu

Result:
case intro.intro.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
f : E → F
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 ω f (s ∩ u)
⊢ (iteratedFDerivWithin 𝕜 n f s x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f s x) v