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
h : HasMFDerivWithinAt I I' f s x 0
simp :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (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)))
    0
⊢ 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) 0

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

Premises used: mfderivWithin, HasMFDerivWithinAt.mdifferentiableWithinAt, reduceIte
-- 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 :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt.{u_1, u_2, u_5} (𝕜 := 𝕜)
      (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
        f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
      0 ((↑(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))
hc :
  HasFDerivWithinAt.{u_1, u_2, u_5} (𝕜 := 𝕜)
    (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
      f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
    0 ((↑(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))
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (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)))
    0

Tactic:
rw [fderivWithin, if_pos]

Premises used: if_pos, fderivWithin
-- 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 :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt.{u_1, u_2, u_5} (𝕜 := 𝕜)
      (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
        f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
      0 ((↑(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.{u_1, u_2, u_5} (𝕜 := 𝕜)
    (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
      f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
    0 ((↑(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:
h.2

Premises used: instModuleTangentSpace._aux_1, And.right, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_1, 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 :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt.{u_1, u_2, u_5} (𝕜 := 𝕜)
      (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
        f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
      0 ((↑(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.{u_1, u_2, u_5} (𝕜 := 𝕜)
    (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
      f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
    0 ((↑(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 h.2

Premises used: And.right
-- 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 : MDifferentiableAt I I' f x
hxs : UniqueMDiffWithinAt I s x
apply : HasMFDerivWithinAt I I' f s x (mfderiv I I' f x)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (_root_.mfderivWithin I I' f s x) (mfderiv I I' f x)

Tactic:
apply HasMFDerivWithinAt.mfderivWithin _ hxs

Premises used: HasMFDerivWithinAt.mfderivWithin
-- 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 : MDifferentiableAt I I' f x
hxs : UniqueMDiffWithinAt I s x
⊢ HasMFDerivWithinAt I I' f s x (mfderiv I I' f x)

Tactic:
h.hasMFDerivAt.hasMFDerivWithinAt

Premises used: MDifferentiableAt.hasMFDerivAt, HasMFDerivAt.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 : MDifferentiableAt I I' f x
hxs : UniqueMDiffWithinAt I s x
⊢ HasMFDerivWithinAt I I' f s x (mfderiv I I' f x)

Tactic:
exact h.hasMFDerivAt.hasMFDerivWithinAt

Premises used: MDifferentiableAt.hasMFDerivAt, HasMFDerivAt.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
st : s ⊆ t
hs : UniqueMDiffWithinAt I s x
h : MDifferentiableWithinAt 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:
((MDifferentiableWithinAt.hasMFDerivWithinAt h).mono st).mfderivWithin hs

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.mfderivWithin, HasMFDerivWithinAt.mono
-- 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 : s ∈ 𝓝 x
rw :
  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 univ x)
rw₁ :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderivWithin I I' f (univ ∩ s) x) (mfderivWithin I I' f univ x)
rw₂ rw₃ :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderivWithin I I' f univ x) (mfderivWithin I I' f univ 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) (mfderiv I I' f x)

Tactic:
rw [← mfderivWithin_univ, ← univ_inter s, mfderivWithin_inter h]

Premises used: mfderivWithin_univ, Set.univ_inter, mfderivWithin_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
hs : IsOpen[inst_4] s
hx : x ∈ s
⊢ 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) (mfderiv I I' f x)

Tactic:
mfderivWithin_of_mem_nhds (hs.mem_nhds hx)

Premises used: mfderivWithin_of_mem_nhds, IsOpen.mem_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
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
y : M
⊢ T1Space M

Tactic:
have : T1Space M := I.t1Space M
-- 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))
y : M
this : T1Space M
⊢ HasMFDerivWithinAt I I' f (insert y s) x f' ↔ HasMFDerivWithinAt I I' f s x f'

Tactic:
⟨fun h => h.mono <| subset_insert y s, fun hf ↦ ?_⟩

Premises used: Iff.intro, HasMFDerivWithinAt.mono, Set.subset_insert
-- 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))
y : M
this : T1Space M
refine : ∀ (hf : HasMFDerivWithinAt I I' f s x f'), HasMFDerivWithinAt I I' f (insert y s) x f'
⊢ HasMFDerivWithinAt I I' f (insert y s) x f' ↔ HasMFDerivWithinAt I I' f s x f'

Tactic:
refine ⟨fun h => h.mono <| subset_insert y s, fun hf ↦ ?_⟩
-- 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))
y : M
this : T1Space M
hf : HasMFDerivWithinAt I I' f s x f'
inl : HasMFDerivWithinAt I I' f (insert x s) x f'
inr : ∀ (h : x ≠ y), HasMFDerivWithinAt I I' f (insert y s) x f'
⊢ HasMFDerivWithinAt I I' f (insert y s) x f'

Tactic:
rcases eq_or_ne x y with rfl | h

Premises used: eq_or_ne, rfl
-- 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))
this : T1Space M
hf : HasMFDerivWithinAt I I' f s x f'
⊢ 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)

Tactic:
rw [HasMFDerivWithinAt] at hf ⊢

Premises used: 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))
this : T1Space M
hf :
  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 (insert x s) x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
      ((↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
⟨hf.1.insert, ?_⟩

Premises used: ContinuousWithinAt.insert, And.left, 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
s : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
this : T1Space M
hf :
  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)
inl :
  HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
    ((↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ ContinuousWithinAt f (insert x s) x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
      ((↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
refine ⟨hf.1.insert, ?_⟩
-- 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))
this : T1Space M
hf :
  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)
⊢ (extChartAt I x).target ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
have : (extChartAt I x).target ∈
        𝓝[(extChartAt I x).symm ⁻¹' insert x s ∩ range I] (extChartAt I x) x :=
      nhdsWithin_mono _ inter_subset_right (extChartAt_target_mem_nhdsWithin x)
-- 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))
this_1 : T1Space M
hf :
  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)
this :
  (extChartAt I x).target ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
inl :
  HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
    ((↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E) ∩ (extChartAt I x).target)
    ((↑(extChartAt I x) : M → E) x)
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
    ((↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
rw [← hasFDerivWithinAt_inter' this]

Premises used: hasFDerivWithinAt_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
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
this_1 : T1Space M
hf :
  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)
this :
  (extChartAt I x).target ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
inl :
  (↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E) ∩ (extChartAt I x).target ⊆
    insert ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
    ((↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E) ∩ (extChartAt I x).target)
    ((↑(extChartAt I x) : M → E) x)

Tactic:
apply hf.2.insert.mono

Premises used: HasFDerivWithinAt.insert, And.right, HasFDerivWithinAt.mono
-- 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))
this_1 : T1Space M
hf :
  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)
this :
  (extChartAt I x).target ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
z : E
h'z : z ∈ (extChartAt I x).target
hz : z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' insert x s
h2z : z ∈ range (↑I : H → E)
inl :
  ∀ (hz : (↑(extChartAt I x).symm : E → M) z = x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s)
    (h2z : ∃ (y : H), (↑I : H → E) y = z),
    z = (↑(extChartAt I x) : M → E) x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
⊢ z ∈ insert ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))

Tactic:
simp only [mem_inter_iff, mem_preimage, mem_insert_iff, mem_range] at hz h2z ⊢

Premises used: Set.mem_range, Set.mem_inter_iff, Set.mem_insert_iff, Set.mem_preimage