-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem HasMFDerivWithinAt.mfderivWithin_eq_zero (h : HasMFDerivWithinAt I I' f s x 0) :
    mfderivWithin I I' f s x = 0

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : HasMFDerivWithinAt I I' f s x 0
⊢ fderivWithin 𝕜 ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm)
      (↑(chartAt H x).symm ∘ ↑I.symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x)) =
    0

Tactic:
simp only [HasMFDerivWithinAt, mfld_simps] at h

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) 0
      (↑(chartAt H x).symm ∘ ↑I.symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x))
⊢ fderivWithin 𝕜 ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm)
      (↑(chartAt H x).symm ∘ ↑I.symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x)) =
    0

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) 0
      (↑(chartAt H x).symm ∘ ↑I.symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x))
⊢ fderivWithin 𝕜 ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm)
      (↑(chartAt H x).symm ∘ ↑I.symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x)) =
    0

Tactic:
rw [fderivWithin, if_pos]

Result:
case hc
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) 0
      (↑(chartAt H x).symm ∘ ↑I.symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x))
⊢ HasFDerivWithinAt ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) 0
    (↑(chartAt H x).symm ∘ ↑I.symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x))

Proof state:
case hc
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) 0
      (↑(chartAt H x).symm ∘ ↑I.symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x))
⊢ HasFDerivWithinAt ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) 0
    (↑(chartAt H x).symm ∘ ↑I.symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x))

Tactic:
exact h.2

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : HasMFDerivWithinAt I I' f s x 0
⊢ mfderivWithin I I' f s x = 0

Tactic:
simp only [mfld_simps, mfderivWithin, h.mdifferentiableWithinAt, ↓reduceIte]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : HasMFDerivWithinAt I I' f s x 0
⊢ fderivWithin 𝕜 ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm)
      (↑(chartAt H x).symm ∘ ↑I.symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x)) =
    0