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 t : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
refine_1 : ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x
refine_2 :
  HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x) ↔
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
⊢ ContinuousWithinAt f s x ∧
      HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x) ↔
    ContinuousWithinAt f t x ∧
      HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x)

Tactic:
refine and_congr ?_ ?_

Premises used: and_congr
-- 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
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x

Tactic:
continuousWithinAt_congr_set' _ h

Premises used: continuousWithinAt_congr_set'
-- 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
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x

Tactic:
exact continuousWithinAt_congr_set' _ h

Premises used: continuousWithinAt_congr_set'
-- 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
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
refine_2 :
  (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝[≠] (↑(extChartAt I x) : M → E) x]
    (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x) ↔
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)

Tactic:
apply hasFDerivWithinAt_congr_set' (extChartAt I x x)

Premises used: extChartAt, hasFDerivWithinAt_congr_set', PartialEquiv.toFun
-- 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
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝[≠] (↑(extChartAt I x) : M → E) x]
    (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)

Tactic:
preimage_extChartAt_eventuallyEq_compl_singleton y h

Premises used: preimage_extChartAt_eventuallyEq_compl_singleton
-- 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
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝[≠] (↑(extChartAt I x) : M → E) x]
    (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)

Tactic:
exact preimage_extChartAt_eventuallyEq_compl_singleton y h

Premises used: preimage_extChartAt_eventuallyEq_compl_singleton
-- 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
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h : s =ᶠ[𝓝 x] t
⊢ HasMFDerivWithinAt I I' f s x f' ↔ HasMFDerivWithinAt I I' f t x f'

Tactic:
hasMFDerivWithinAt_congr_set' x <| h.filter_mono inf_le_left

Premises used: Filter.EventuallyEq.filter_mono, inf_le_left, hasMFDerivWithinAt_congr_set'
-- 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
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
simp :
  (∃ (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') ↔
    ∃ (f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))),
      HasMFDerivWithinAt I I' f t x f'
⊢ MDifferentiableWithinAt I I' f s x ↔ MDifferentiableWithinAt I I' f t x

Tactic:
simp only [mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt]

Premises used: mdifferentiableWithinAt_iff_exists_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 t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ (∃ (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') ↔
    ∃ (f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))),
      HasMFDerivWithinAt I I' f t x f'

Tactic:
exists_congr fun _ => hasMFDerivWithinAt_congr_set' _ h

Premises used: exists_congr, hasMFDerivWithinAt_congr_set'
-- 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
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ (∃ (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') ↔
    ∃ (f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))),
      HasMFDerivWithinAt I I' f t x f'

Tactic:
exact exists_congr fun _ => hasMFDerivWithinAt_congr_set' _ h

Premises used: exists_congr, hasMFDerivWithinAt_congr_set'
-- 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
h : s =ᶠ[𝓝 x] t
simp :
  (∃ (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') ↔
    ∃ (f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))),
      HasMFDerivWithinAt I I' f t x f'
⊢ MDifferentiableWithinAt I I' f s x ↔ MDifferentiableWithinAt I I' f t x

Tactic:
simp only [mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt]

Premises used: mdifferentiableWithinAt_iff_exists_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 t : Set M
h : s =ᶠ[𝓝 x] t
⊢ (∃ (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') ↔
    ∃ (f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))),
      HasMFDerivWithinAt I I' f t x f'

Tactic:
exists_congr fun _ => hasMFDerivWithinAt_congr_set h

Premises used: exists_congr, hasMFDerivWithinAt_congr_set
-- 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
h : s =ᶠ[𝓝 x] t
⊢ (∃ (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') ↔
    ∃ (f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))),
      HasMFDerivWithinAt I I' f t x f'

Tactic:
exact exists_congr fun _ => hasMFDerivWithinAt_congr_set h

Premises used: exists_congr, hasMFDerivWithinAt_congr_set
-- 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
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
pos :
  ∀ (hx : 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) (mfderivWithin I I' f t x)
neg :
  ∀ (hx : ¬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) (mfderivWithin I I' f t 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) (mfderivWithin I I' f t x)

Tactic:
by_cases hx : MDifferentiableWithinAt I I' f s x

Premises used: 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 t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
hx : MDifferentiableWithinAt I I' f s x
pos :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x))
    (fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) 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) (mfderivWithin I I' f t x)

Tactic:
simp only [mfderivWithin, hx, (mdifferentiableWithinAt_congr_set' y h).1 hx, ↓reduceIte]

Premises used: mfderivWithin, Iff.mp, reduceIte, mdifferentiableWithinAt_congr_set'
-- 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
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
hx : MDifferentiableWithinAt I I' f s x
pos :
  (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝[≠] (↑(extChartAt I x) : M → E) x]
    (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x))
    (fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x))

Tactic:
apply fderivWithin_congr_set' (extChartAt I x x)

Premises used: extChartAt, fderivWithin_congr_set', PartialEquiv.toFun
-- 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
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
hx : MDifferentiableWithinAt I I' f s x
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝[≠] (↑(extChartAt I x) : M → E) x]
    (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)

Tactic:
preimage_extChartAt_eventuallyEq_compl_singleton y h

Premises used: preimage_extChartAt_eventuallyEq_compl_singleton
-- 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
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
hx : MDifferentiableWithinAt I I' f s x
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝[≠] (↑(extChartAt I x) : M → E) x]
    (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)

Tactic:
exact preimage_extChartAt_eventuallyEq_compl_singleton y h

Premises used: preimage_extChartAt_eventuallyEq_compl_singleton
-- 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
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
hx : ¬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) (mfderivWithin I I' f t x)

Tactic:
simp [mfderivWithin, hx, ← mdifferentiableWithinAt_congr_set' y h]

Premises used: mfderivWithin, mdifferentiableWithinAt_congr_set'
-- 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
h : s =ᶠ[𝓝 x] t
⊢ 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) (mfderivWithin I I' f t x)

Tactic:
mfderivWithin_congr_set' x <| h.filter_mono inf_le_left

Premises used: Filter.EventuallyEq.filter_mono, mfderivWithin_congr_set', inf_le_left
-- 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
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ ∀ᶠ (y : M) in 𝓝 x,
    Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I y) (TangentSpace I' (f y)))
      (mfderivWithin I I' f s y) (mfderivWithin I I' f t y)

Tactic:
(eventually_nhds_nhdsWithin.2 h).mono fun _ => mfderivWithin_congr_set' y

Premises used: Iff.mpr, eventually_nhds_nhdsWithin, Filter.Eventually.mono, mfderivWithin_congr_set'
-- 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
h : s =ᶠ[𝓝 x] t
⊢ ∀ᶠ (y : M) in 𝓝 x,
    Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I y) (TangentSpace I' (f y)))
      (mfderivWithin I I' f s y) (mfderivWithin I I' f t y)

Tactic:
mfderivWithin_eventually_congr_set' x <| h.filter_mono inf_le_left

Premises used: Filter.EventuallyEq.filter_mono, mfderivWithin_eventually_congr_set', inf_le_left
-- 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' 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'
h' : f' = f₁'
⊢ HasMFDerivAt I I' f x f₁'

Tactic:
h' ▸ h

Premises used: Eq.rec