-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
lemma fderivWithin_fderivWithin_eq_of_mem_nhdsWithin (h : t ∈ 𝓝[s] x)
    (hf : ContDiffWithinAt 𝕜 2 f t x) (hs : UniqueDiffOn 𝕜 s) (ht : UniqueDiffOn 𝕜 t) (hx : x ∈ s) :
    fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
this : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜 2 f t y
⊢ ∀ᶠ (y : E) in 𝓝[s] x, fderivWithin 𝕜 f s y = fderivWithin 𝕜 f t y

Tactic:
filter_upwards [self_mem_nhdsWithin, this, eventually_eventually_nhdsWithin.2 h]
  with y hy h'y h''y

Result:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
this : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜 2 f t y
y : E
hy : y ∈ s
h'y : ContDiffWithinAt 𝕜 2 f t y
h''y : ∀ᶠ (x : E) in 𝓝[s] y, t x
⊢ fderivWithin 𝕜 f s y = fderivWithin 𝕜 f t y

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
⊢ ∀ᶠ (y : E) in 𝓝[s] x, fderivWithin 𝕜 f s y = fderivWithin 𝕜 f t y

Tactic:
have : ∀ᶠ y in 𝓝[s] x, ContDiffWithinAt 𝕜 2 f t y :=
  nhdsWithin_le_iff.2 h (nhdsWithin_mono _ (subset_insert x t) (hf.eventually (by simp)))

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
this : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜 2 f t y
⊢ ∀ᶠ (y : E) in 𝓝[s] x, fderivWithin 𝕜 f s y = fderivWithin 𝕜 f t y

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
A : ∀ᶠ (y : E) in 𝓝[s] x, fderivWithin 𝕜 f s y = fderivWithin 𝕜 f t y
this : fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x
⊢ fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x

Tactic:
apply fderivWithin_of_mem_nhdsWithin h (hs x hx)

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
A : ∀ᶠ (y : E) in 𝓝[s] x, fderivWithin 𝕜 f s y = fderivWithin 𝕜 f t y
this : fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x
⊢ DifferentiableWithinAt 𝕜 (fderivWithin 𝕜 f t) t x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
A : ∀ᶠ (y : E) in 𝓝[s] x, fderivWithin 𝕜 f s y = fderivWithin 𝕜 f t y
⊢ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x

Tactic:
have : fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x := by
  apply Filter.EventuallyEq.fderivWithin_eq A
  exact fderivWithin_of_mem_nhdsWithin h (hs x hx) (hf.differentiableWithinAt one_le_two)

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
A : ∀ᶠ (y : E) in 𝓝[s] x, fderivWithin 𝕜 f s y = fderivWithin 𝕜 f t y
this : fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x
⊢ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
A : ∀ᶠ (y : E) in 𝓝[s] x, fderivWithin 𝕜 f s y = fderivWithin 𝕜 f t y
this : fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x
⊢ DifferentiableWithinAt 𝕜 (fderivWithin 𝕜 f t) t x

Tactic:
exact (hf.fderivWithin_right (m := 1) ht le_rfl
  (mem_of_mem_nhdsWithin hx h)).differentiableWithinAt le_rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
⊢ 2 ≠ ∞

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
⊢ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x

Tactic:
have A : ∀ᶠ y in 𝓝[s] x, fderivWithin 𝕜 f s y = fderivWithin 𝕜 f t y := by
  have : ∀ᶠ y in 𝓝[s] x, ContDiffWithinAt 𝕜 2 f t y :=
    nhdsWithin_le_iff.2 h (nhdsWithin_mono _ (subset_insert x t) (hf.eventually (by simp)))
  filter_upwards [self_mem_nhdsWithin, this, eventually_eventually_nhdsWithin.2 h]
    with y hy h'y h''y
  exact fderivWithin_of_mem_nhdsWithin h''y (hs y hy) (h'y.differentiableWithinAt one_le_two)

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
A : ∀ᶠ (y : E) in 𝓝[s] x, fderivWithin 𝕜 f s y = fderivWithin 𝕜 f t y
⊢ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x