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))
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 : (↑(extChartAt I x).symm : E → M) z = x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s
h2z : ∃ (y : H), (↑I : H → E) y = z
inl :
  ∀ (xz : (↑(extChartAt I x).symm : E → M) z = x),
    z = (↑(extChartAt I x) : M → E) x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
inl₁ :
  ∀ (h'z : (↑(extChartAt I x).symm : E → M) z ∈ s),
    z = (↑(extChartAt I x) : M → E) x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s ∧ ∃ (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

Tactic:
rcases hz with xz | h'z
-- 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
h2z : ∃ (y : H), (↑I : H → E) y = z
xz : (↑(extChartAt I x).symm : E → M) z = x
inl : z = (↑(extChartAt I x) : M → E) x
⊢ z = (↑(extChartAt I x) : M → E) x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z

Tactic:
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 : 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
h2z : ∃ (y : H), (↑I : H → E) y = z
xz : (↑(extChartAt I x).symm : E → M) z = x
⊢ x ∈ (extChartAt I x).source

Tactic:
have : x ∈ (extChartAt I x).source := mem_extChartAt_source 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_2 :
  (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
h2z : ∃ (y : H), (↑I : H → E) y = z
xz : (↑(extChartAt I x).symm : E → M) z = x
this : x ∈ (extChartAt I x).source
⊢ z = (↑(extChartAt I x) : M → E) x

Tactic:
(((extChartAt I x).eq_symm_apply this h'z).1 xz.symm).symm

Premises used: PartialEquiv.eq_symm_apply, extChartAt, Iff.mp, 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))
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_2 :
  (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
h2z : ∃ (y : H), (↑I : H → E) y = z
xz : (↑(extChartAt I x).symm : E → M) z = x
this : x ∈ (extChartAt I x).source
⊢ z = (↑(extChartAt I x) : M → E) x

Tactic:
exact (((extChartAt I x).eq_symm_apply this h'z).1 xz.symm).symm

Premises used: PartialEquiv.eq_symm_apply, extChartAt, Iff.mp, 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))
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_1 : z ∈ (extChartAt I x).target
h2z : ∃ (y : H), (↑I : H → E) y = z
h'z : (↑(extChartAt I x).symm : E → M) z ∈ s
⊢ z = (↑(extChartAt I x) : M → E) x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z

Tactic:
Or.inr ⟨h'z, h2z⟩

Premises used: And.intro, Or.inr
-- 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_1 : z ∈ (extChartAt I x).target
h2z : ∃ (y : H), (↑I : H → E) y = z
h'z : (↑(extChartAt I x).symm : E → M) z ∈ s
⊢ z = (↑(extChartAt I x) : M → E) x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z

Tactic:
exact Or.inr ⟨h'z, h2z⟩

Premises used: Or.inr
-- 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'
h : x ≠ y
apply : s ∈ 𝓝[insert y s] x
⊢ HasMFDerivWithinAt I I' f (insert y s) x f'

Tactic:
apply hf.mono_of_mem_nhdsWithin ?_

Premises used: 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
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'
h : x ≠ y
simp_rw : s ∈ 𝓝[s] x
⊢ s ∈ 𝓝[insert y s] x

Tactic:
simp_rw [nhdsWithin_insert_of_ne h, self_mem_nhdsWithin]

Premises used: self_mem_nhdsWithin, nhdsWithin_insert_of_ne
-- 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'
⊢ HasMFDerivWithinAt I I' f (insert x s) x f'

Tactic:
h.insert'

Premises used: HasMFDerivWithinAt.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
rw : HasMFDerivWithinAt I I' f (insert y (s \ {y})) x f' ↔ HasMFDerivWithinAt I I' f s x f'
rw₁ : M
rw₂ : HasMFDerivWithinAt I I' f (insert y s) x f' ↔ HasMFDerivWithinAt I I' f s x f'
rw₃ rw₄ : HasMFDerivWithinAt I I' f s x f' ↔ HasMFDerivWithinAt I I' f s x f'
⊢ HasMFDerivWithinAt I I' f (s \ {y}) x f' ↔ HasMFDerivWithinAt I I' f s x f'

Tactic:
rw [← hasMFDerivWithinAt_insert, insert_diff_singleton, hasMFDerivWithinAt_insert]

Premises used: hasMFDerivWithinAt_insert, Set.insert_diff_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 : Set M
hs : UniqueMDiffWithinAt I s x
h : MDifferentiableAt I I' f 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)
⊢ 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]

Premises used: mfderivWithin_univ
-- 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 : UniqueMDiffWithinAt I s x
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)))
    (mfderivWithin I I' f s x) (mfderivWithin I I' f univ x)

Tactic:
mfderivWithin_subset (subset_univ _) hs h.mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, Set.subset_univ, mfderivWithin_subset
-- 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 : UniqueMDiffWithinAt I s x
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)))
    (mfderivWithin I I' f s x) (mfderivWithin I I' f univ x)

Tactic:
exact mfderivWithin_subset (subset_univ _) hs h.mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, Set.subset_univ, mfderivWithin_subset
-- 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 (insert x s) x ↔ MDifferentiableWithinAt I I' f s x

Tactic:
⟨fun h ↦ h.mono (subset_insert x s), fun h ↦ h.hasMFDerivWithinAt.insert.mdifferentiableWithinAt⟩

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.insert, HasMFDerivWithinAt.mdifferentiableWithinAt, MDifferentiableWithinAt.mono, Iff.intro, 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
y : M
inl : MDifferentiableWithinAt I I' f (insert x s) x ↔ MDifferentiableWithinAt I I' f s x
inr : ∀ (h : x ≠ y), MDifferentiableWithinAt I I' f (insert y s) x ↔ MDifferentiableWithinAt I I' f s x
⊢ MDifferentiableWithinAt I I' f (insert y s) x ↔ MDifferentiableWithinAt I I' f s x

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
⊢ MDifferentiableWithinAt I I' f (insert x s) x ↔ MDifferentiableWithinAt I I' f s x

Tactic:
mdifferentiableWithinAt_insert_self

Premises used: mdifferentiableWithinAt_insert_self
-- 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 (insert x s) x ↔ MDifferentiableWithinAt I I' f s x

Tactic:
exact mdifferentiableWithinAt_insert_self

Premises used: mdifferentiableWithinAt_insert_self
-- 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
y : M
h : x ≠ y
⊢ 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
y : M
h : x ≠ y
this : T1Space M
inr : 𝓝[insert y s] x = 𝓝[s] x
⊢ MDifferentiableWithinAt I I' f (insert y s) x ↔ MDifferentiableWithinAt I I' f s x

Tactic:
apply mdifferentiableWithinAt_congr_nhds

Premises used: 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
y : M
h : x ≠ y
this : T1Space M
⊢ 𝓝[insert y s] x = 𝓝[s] x

Tactic:
nhdsWithin_insert_of_ne h

Premises used: nhdsWithin_insert_of_ne
-- 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
y : M
h : x ≠ y
this : T1Space M
⊢ 𝓝[insert y s] x = 𝓝[s] x

Tactic:
exact nhdsWithin_insert_of_ne h

Premises used: nhdsWithin_insert_of_ne
-- 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
⊢ MDifferentiableWithinAt I I' f (insert x s) x

Tactic:
h.insert'

Premises used: MDifferentiableWithinAt.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'
s t : Set M
hf : MDifferentiableOn I I' f s
hf' : MDifferentiableOn I I' f t
hs : IsOpen[inst_4] s
ht : IsOpen[inst_4] t
x : M
hx : x ∈ s ∪ t
inl : ∀ (hx : x ∈ s), MDifferentiableWithinAt I I' f (s ∪ t) x
inr : ∀ (hx : x ∈ t), MDifferentiableWithinAt I I' f (s ∪ t) x
⊢ MDifferentiableWithinAt I I' f (s ∪ t) x

Tactic:
obtain (hx | hx) := hx