awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h : HasMFDerivWithinAt I I' f s x f'
hs : s ∈ 𝓝 x
rwa : ∀ (h : HasMFDerivWithinAt I I' f (univ ∩ s) x f') (hs : s ∈ 𝓝 x), HasMFDerivAt I I' f x f'
rwa₁ : ∀ (h : HasMFDerivWithinAt I I' f univ x f') (hs : s ∈ 𝓝 x), HasMFDerivAt I I' f x f'
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : HasMFDerivAt I I' f x f') (hs : s ∈ 𝓝 x), HasMFDerivAt I I' f x f'
⊢ HasMFDerivAt I I' f x f'

Tactic:
rwa [← univ_inter s, hasMFDerivWithinAt_inter hs, hasMFDerivWithinAt_univ] at h

Premises used: Set.univ_inter, hasMFDerivWithinAt_univ, hasMFDerivWithinAt_inter
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : MDifferentiableWithinAt I I' f s x
⊢ HasMFDerivWithinAt I I' f s x (mfderivWithin I I' f s x)

Tactic:
⟨h.1, ?_⟩

Premises used: ChartedSpace.LiftPropWithinAt.continuousWithinAt, And.intro, HasMFDerivWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : MDifferentiableWithinAt I I' f s x
refine :
  HasFDerivWithinAt (writtenInExtChartAt I I' x f) (mfderivWithin I I' f s x)
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ HasMFDerivWithinAt I I' f s x (mfderivWithin I I' f s x)

Tactic:
refine ⟨h.1, ?_⟩
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : MDifferentiableWithinAt I I' f s x
simp :
  HasFDerivWithinAt
    (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
      f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
    (fderivWithin 𝕜
      (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
        f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x f) (mfderivWithin I I' f s x)
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
simp only [mfderivWithin, h, if_pos, mfld_simps]

Premises used: mfderivWithin, if_pos
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : MDifferentiableWithinAt I I' f s x
⊢ HasFDerivWithinAt
    (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
      f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
    (fderivWithin 𝕜
      (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
        f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x))

Tactic:
DifferentiableWithinAt.hasFDerivWithinAt h.2

Premises used: ChartedSpace.LiftPropWithinAt.prop, instModuleTangentSpace._aux_1, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_1, DifferentiableWithinAt.hasFDerivWithinAt, instAddCommGroupTangentSpace._aux_4
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : MDifferentiableWithinAt I I' f s x
⊢ HasFDerivWithinAt
    (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
      f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
    (fderivWithin 𝕜
      (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
        f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x))

Tactic:
exact DifferentiableWithinAt.hasFDerivWithinAt h.2

Premises used: ChartedSpace.LiftPropWithinAt.prop, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
⊢ MDifferentiableWithinAt I I' f s x ↔
    ∃ (f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))),
      HasMFDerivWithinAt I I' f s x f'

Tactic:
⟨fun h ↦ ⟨mfderivWithin I I' f s x, h.hasMFDerivWithinAt⟩, ?_⟩

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, mfderivWithin, Iff.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
refine :
  (∃ (f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))),
      HasMFDerivWithinAt I I' f s x f') →
    MDifferentiableWithinAt I I' f s x
⊢ MDifferentiableWithinAt I I' f s x ↔
    ∃ (f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))),
      HasMFDerivWithinAt I I' f s x f'

Tactic:
refine ⟨fun h ↦ ⟨mfderivWithin I I' f s x, h.hasMFDerivWithinAt⟩, ?_⟩
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
hf' : HasMFDerivWithinAt I I' f s x f'
⊢ MDifferentiableWithinAt I I' f s x

Tactic:
hf'.mdifferentiableWithinAt

Premises used: HasMFDerivWithinAt.mdifferentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
hf' : HasMFDerivWithinAt I I' f s x f'
⊢ MDifferentiableWithinAt I I' f s x

Tactic:
exact hf'.mdifferentiableWithinAt

Premises used: HasMFDerivWithinAt.mdifferentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : MDifferentiableWithinAt I I' f s x
t : Set M
hst : s ∈ 𝓝[t] x
⊢ MDifferentiableWithinAt I I' f t x

Tactic:
(h.hasMFDerivWithinAt.mono_of_mem_nhdsWithin hst).mdifferentiableWithinAt

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.mdifferentiableWithinAt, HasMFDerivWithinAt.mono_of_mem_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : MDifferentiableWithinAt I I' f s x
t : Set M
hst : 𝓝[s] x = 𝓝[t] x
⊢ MDifferentiableWithinAt I I' f t x

Tactic:
h.mono_of_mem_nhdsWithin <| hst ▸ self_mem_nhdsWithin

Premises used: Eq.rec, self_mem_nhdsWithin, MDifferentiableWithinAt.mono_of_mem_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
hst : 𝓝[s] x = 𝓝[t] x
⊢ MDifferentiableWithinAt I I' f s x ↔ MDifferentiableWithinAt I I' f t x

Tactic:
⟨fun h => h.congr_nhds hst, fun h => h.congr_nhds hst.symm⟩

Premises used: Iff.intro, Eq.symm, MDifferentiableWithinAt.congr_nhds
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : MDifferentiableWithinAt I I' f s x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderivWithin I I' f s x)
    (fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x))

Tactic:
simp only [mfderivWithin, h, if_pos]

Premises used: mfderivWithin, if_pos
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
h : MDifferentiableAt I I' f x
⊢ HasMFDerivAt I I' f x (mfderiv I I' f x)

Tactic:
⟨h.continuousAt, ?_⟩

Premises used: MDifferentiableAt.continuousAt, HasMFDerivAt, And.intro
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
h : MDifferentiableAt I I' f x
refine :
  HasFDerivWithinAt (writtenInExtChartAt I I' x f) (mfderiv I I' f x) (range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)
⊢ HasMFDerivAt I I' f x (mfderiv I I' f x)

Tactic:
refine ⟨h.continuousAt, ?_⟩
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
h : MDifferentiableAt I I' f x
simp :
  HasFDerivWithinAt
    (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
      f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
    (fderivWithin 𝕜
      (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
        f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
      (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
    (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x f) (mfderiv I I' f x) (range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)

Tactic:
simp only [mfderiv, h, if_pos, mfld_simps]

Premises used: mfderiv, if_pos
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
h : MDifferentiableAt I I' f x
⊢ HasFDerivWithinAt
    (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
      f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
    (fderivWithin 𝕜
      (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
        f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
      (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
    (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))

Tactic:
DifferentiableWithinAt.hasFDerivWithinAt h.differentiableWithinAt_writtenInExtChartAt

Premises used: MDifferentiableAt.differentiableWithinAt_writtenInExtChartAt, instModuleTangentSpace._aux_1, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_1, DifferentiableWithinAt.hasFDerivWithinAt, instAddCommGroupTangentSpace._aux_4
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
h : MDifferentiableAt I I' f x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderiv I I' f x)
    (fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))

Tactic:
simp only [mfderiv, h, if_pos]

Premises used: mfderiv, if_pos
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h : HasMFDerivAt I I' f x f'
⊢ mfderiv I I' f x = f'

Tactic:
(hasMFDerivAt_unique h h.mdifferentiableAt.hasMFDerivAt).symm

Premises used: MDifferentiableAt.hasMFDerivAt, HasMFDerivAt.mdifferentiableAt, hasMFDerivAt_unique, Eq.symm
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h : HasMFDerivWithinAt I I' f s x f'
hxs : UniqueMDiffWithinAt I s x
h₁ :
  ∀ (x_1 : TangentSpace I x),
    Eq.{u_5 + 1} (α := TangentSpace I' (f x))
      (((mfderivWithin I I' f s x :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))) :
            (a : TangentSpace I x) → TangentSpace I' (f x))
          x_1 :
        TangentSpace I' (f x))
      ((f' : (a : TangentSpace I x) → TangentSpace I' (f x)) x_1 : TangentSpace I' (f x))
⊢ mfderivWithin I I' f s x = f'

Tactic:
ext
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h : HasMFDerivWithinAt I I' f s x f'
hxs : UniqueMDiffWithinAt I s x
x_1 : TangentSpace I x
h₁ h₂ :
  Eq.{u_5 + 1} (α := TangentSpace I' (f x))
    (((mfderivWithin I I' f s x :
            ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))) :
          (a : TangentSpace I x) → TangentSpace I' (f x))
        x_1 :
      TangentSpace I' (f x))
    (((mfderivWithin I I' f s x :
            ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))) :
          (a : TangentSpace I x) → TangentSpace I' (f x))
        x_1 :
      TangentSpace I' (f x))
⊢ Eq.{u_5 + 1} (α := TangentSpace I' (f x))
    (((mfderivWithin I I' f s x :
            ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))) :
          (a : TangentSpace I x) → TangentSpace I' (f x))
        x_1 :
      TangentSpace I' (f x))
    ((f' : (a : TangentSpace I x) → TangentSpace I' (f x)) x_1 : TangentSpace I' (f x))

Tactic:
rw [hxs.eq h h.mdifferentiableWithinAt.hasMFDerivWithinAt]

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, UniqueMDiffWithinAt.eq, HasMFDerivWithinAt.mdifferentiableWithinAt