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'
x : M
y : M'
s : Set M
t : Set M'
hs : UniqueMDiffWithinAt I s x
ht : UniqueMDiffWithinAt I' t y
rw :
  ((↑(extChartAt I x).symm : E → M) ⁻¹' s) ×ˢ ((↑(extChartAt I' y).symm : E' → M') ⁻¹' t) ∩
      range (↑I : H → E) ×ˢ range (↑I' : H' → E') ⊆
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s) ×ˢ ((↑(extChartAt I' y).symm : E' → M') ⁻¹' t) ∩
      range (↑I : H → E) ×ˢ range (↑I' : H' → E')
⊢ ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ×ˢ
      ((↑(extChartAt I' y).symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) ⊆
    (↑(extChartAt (I.prod I') (x, y)).symm : E × E' → M × M') ⁻¹' s ×ˢ t ∩
      range (↑(I.prod I') : ModelProd H H' → E × E')

Tactic:
rw [ModelWithCorners.range_prod, ← prod_inter_prod]

Premises used: ModelWithCorners.range_prod, Set.prod_inter_prod
-- 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'
x : M
y : M'
s : Set M
t : Set M'
hs : UniqueMDiffWithinAt I s x
ht : UniqueMDiffWithinAt I' t y
⊢ ((↑(extChartAt I x).symm : E → M) ⁻¹' s) ×ˢ ((↑(extChartAt I' y).symm : E' → M') ⁻¹' t) ∩
      range (↑I : H → E) ×ˢ range (↑I' : H' → E') ⊆
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s) ×ˢ ((↑(extChartAt I' y).symm : E' → M') ⁻¹' t) ∩
      range (↑I : H → E) ×ˢ range (↑I' : H' → E')

Tactic:
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'
s : Set M
t : Set M'
hs : UniqueMDiffOn I s
ht : UniqueMDiffOn I' t
⊢ UniqueMDiffOn (I.prod I') (s ×ˢ t)

Tactic:
fun x h ↦
  (hs x.1 h.1).prod (ht x.2 h.2)

Premises used: UniqueMDiffOn, Prod.fst, And.right, And.left, UniqueMDiffWithinAt.prod, Prod.snd
-- 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 ⊆ t
h : MDifferentiableWithinAt I I' f t x
⊢ MDifferentiableWithinAt I I' f s x

Tactic:
⟨ContinuousWithinAt.mono h.1 hst, DifferentiableWithinAt.mono
    h.differentiableWithinAt_writtenInExtChartAt
    (inter_subset_inter_left _ (preimage_mono hst))⟩

Premises used: ChartedSpace.LiftPropWithinAt.continuousWithinAt, MDifferentiableWithinAt.differentiableWithinAt_writtenInExtChartAt, Set.inter_subset_inter_left, DifferentiableWithinAt.mono, Set.preimage_mono, ContinuousWithinAt.mono, MDifferentiableWithinAt, ChartedSpace.LiftPropWithinAt.mk
-- 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
simp_rw : LiftPropWithinAt (DifferentiableWithinAtProp I I') f univ x ↔ MDifferentiableAt I I' f x
simp_rw₁ :
  LiftPropWithinAt (DifferentiableWithinAtProp I I') f univ x ↔ LiftPropAt (DifferentiableWithinAtProp I I') f x
⊢ MDifferentiableWithinAt I I' f univ x ↔ MDifferentiableAt I I' f x

Tactic:
simp_rw [MDifferentiableWithinAt, MDifferentiableAt, ChartedSpace.LiftPropAt]

Premises used: MDifferentiableAt, ChartedSpace.LiftPropAt, 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
ht : t ∈ 𝓝 x
rw : LiftPropWithinAt (DifferentiableWithinAtProp I I') f (s ∩ t) x ↔ MDifferentiableWithinAt I I' f s x
rw₁ :
  LiftPropWithinAt (DifferentiableWithinAtProp I I') f (s ∩ t) x ↔
    LiftPropWithinAt (DifferentiableWithinAtProp I I') f s x
rw₂ rw₃ :
  LiftPropWithinAt (DifferentiableWithinAtProp I I') f s x ↔ LiftPropWithinAt (DifferentiableWithinAtProp I I') f s x
⊢ MDifferentiableWithinAt I I' f (s ∩ t) x ↔ MDifferentiableWithinAt I I' f s x

Tactic:
rw [MDifferentiableWithinAt, MDifferentiableWithinAt,
    differentiableWithinAt_localInvariantProp.liftPropWithinAt_inter ht]

Premises used: StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter, differentiableWithinAt_localInvariantProp, 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
ht : t ∈ 𝓝[s] x
rw : LiftPropWithinAt (DifferentiableWithinAtProp I I') f (s ∩ t) x ↔ MDifferentiableWithinAt I I' f s x
rw₁ :
  LiftPropWithinAt (DifferentiableWithinAtProp I I') f (s ∩ t) x ↔
    LiftPropWithinAt (DifferentiableWithinAtProp I I') f s x
rw₂ rw₃ :
  LiftPropWithinAt (DifferentiableWithinAtProp I I') f s x ↔ LiftPropWithinAt (DifferentiableWithinAtProp I I') f s x
⊢ MDifferentiableWithinAt I I' f (s ∩ t) x ↔ MDifferentiableWithinAt I I' f s x

Tactic:
rw [MDifferentiableWithinAt, MDifferentiableWithinAt,
    differentiableWithinAt_localInvariantProp.liftPropWithinAt_inter' ht]

Premises used: differentiableWithinAt_localInvariantProp, MDifferentiableWithinAt, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_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 : MDifferentiableAt I I' f x
⊢ MDifferentiableWithinAt I I' f s x

Tactic:
MDifferentiableWithinAt.mono (subset_univ _) (mdifferentiableWithinAt_univ.2 h)

Premises used: Iff.mpr, mdifferentiableWithinAt_univ, Set.subset_univ, MDifferentiableWithinAt.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 : MDifferentiableWithinAt I I' f s x
hs : s ∈ 𝓝 x
rw rw₁ : s = s
⊢ s = univ ∩ s

Tactic:
rw [univ_inter]

Premises used: Set.univ_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
hs : s ∈ 𝓝 x
⊢ s = univ ∩ s

Tactic:
have : s = univ ∩ s := by rw [univ_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
hs : s ∈ 𝓝 x
this : s = univ ∩ s
rwa :
  ∀ (h : MDifferentiableWithinAt I I' f (univ ∩ s) x) (hs : s ∈ 𝓝 x) (this : s = univ ∩ s), MDifferentiableAt I I' f x
rwa₁ : ∀ (h : MDifferentiableWithinAt I I' f univ x) (hs : s ∈ 𝓝 x) (this : s = univ ∩ s), MDifferentiableAt I I' f x
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (h : MDifferentiableAt I I' f x) (hs : s ∈ 𝓝 x) (this : s = univ ∩ s), MDifferentiableAt I I' f x
⊢ MDifferentiableAt I I' f x

Tactic:
rwa [this, mdifferentiableWithinAt_inter hs, mdifferentiableWithinAt_univ] at h

Premises used: mdifferentiableWithinAt_univ, mdifferentiableWithinAt_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'
s t : Set M
h : MDifferentiableOn I I' f t
st : s ⊆ t
⊢ MDifferentiableOn I I' f s

Tactic:
fun x hx => (h x (st hx)).mono st

Premises used: MDifferentiableWithinAt.mono, MDifferentiableOn
-- 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'
⊢ MDifferentiableOn I I' f ∅

Tactic:
fun _x hx ↦ hx.elim

Premises used: False.elim, MDifferentiableOn
-- 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'
simp : (∀ (x : M), MDifferentiableAt I I' f x) ↔ MDifferentiable I I' f
⊢ MDifferentiableOn I I' f univ ↔ MDifferentiable I I' f

Tactic:
simp only [MDifferentiableOn, mdifferentiableWithinAt_univ, mfld_simps]

Premises used: mdifferentiableWithinAt_univ, MDifferentiableOn
-- 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), MDifferentiableAt I I' f x) ↔ MDifferentiable I I' f

Tactic:
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
h : MDifferentiableOn I I' f s
hx : s ∈ 𝓝 x
⊢ MDifferentiableAt I I' f x

Tactic:
(h x (mem_of_mem_nhds hx)).mdifferentiableAt hx

Premises used: mem_of_mem_nhds, MDifferentiableWithinAt.mdifferentiableAt
-- 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 : Set M
h : MDifferentiable I I' f
⊢ MDifferentiableOn I I' f s

Tactic:
(mdifferentiableOn_univ.2 h).mono (subset_univ _)

Premises used: Iff.mpr, MDifferentiableOn.mono, Set.subset_univ, mdifferentiableOn_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'
s : Set M
h : ∀ x ∈ s, ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ MDifferentiableOn I I' f (s ∩ u)
x : M
xs : x ∈ s
rcases :
  ∀ (t : Set M) (t_open : IsOpen[inst_4] t) (xt : x ∈ t) (ht : MDifferentiableOn I I' f (s ∩ t)),
    MDifferentiableWithinAt I I' f s x
⊢ MDifferentiableWithinAt I I' f s x

Tactic:
rcases h x xs with ⟨t, t_open, xt, ht⟩
-- 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 : Set M
h : ∀ x ∈ s, ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ MDifferentiableOn I I' f (s ∩ u)
x : M
xs : x ∈ s
t : Set M
t_open : IsOpen[inst_4] t
xt : x ∈ t
ht : MDifferentiableOn I I' f (s ∩ t)
⊢ MDifferentiableWithinAt I I' f s x

Tactic:
(mdifferentiableWithinAt_inter (t_open.mem_nhds xt)).1 (ht x ⟨xs, xt⟩)

Premises used: mdifferentiableWithinAt_inter, And.intro, IsOpen.mem_nhds, Iff.mp
-- 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 : Set M
h : ∀ x ∈ s, ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ MDifferentiableOn I I' f (s ∩ u)
x : M
xs : x ∈ s
t : Set M
t_open : IsOpen[inst_4] t
xt : x ∈ t
ht : MDifferentiableOn I I' f (s ∩ t)
⊢ MDifferentiableWithinAt I I' f s x

Tactic:
exact (mdifferentiableWithinAt_inter (t_open.mem_nhds xt)).1 (ht x ⟨xs, xt⟩)

Premises used: mdifferentiableWithinAt_inter, And.intro, IsOpen.mem_nhds, Iff.mp
-- 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
hf : MDifferentiable I I' f
⊢ MDifferentiableAt I I' f x

Tactic:
hf 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'
s : Set M
x : M
rw :
  ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f)
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f)
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) x)
⊢ MDifferentiableWithinAt I I' f s x ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f)
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) x)

Tactic:
rw [mdifferentiableWithinAt_iff']

Premises used: mdifferentiableWithinAt_iff'
-- 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 : Set M
x : M
⊢ ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f)
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f)
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) x)

Tactic:
and_congr Iff.rfl (exists_congr fun f' => ?_)

Premises used: Iff.rfl, exists_congr, 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'
s : Set M
x : M
refine :
  ∀ (f' : E →L[𝕜] 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).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) x)
⊢ ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f)
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f)
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) x)

Tactic:
refine and_congr Iff.rfl (exists_congr fun f' => ?_)

Premises used: Iff.rfl, exists_congr, 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'
s : Set M
x : M
f' : E →L[𝕜] E'
rw :
  HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' (range (↑I : H → E) ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)
      ((↑(extChartAt I x) : M → E) x) ↔
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) 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) ↔
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) x)

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm