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

Tactic:
(hf x hx).mdifferentiableAt (hs.mem_nhds hx) |>.mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, MDifferentiableWithinAt.mdifferentiableAt, 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'
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
⊢ MDifferentiableWithinAt I I' f (s ∪ t) x

Tactic:
exact (hf x hx).mdifferentiableAt (hs.mem_nhds hx) |>.mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, MDifferentiableWithinAt.mdifferentiableAt, 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'
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 ∈ t
⊢ MDifferentiableWithinAt I I' f (s ∪ t) x

Tactic:
(hf' x hx).mdifferentiableAt (ht.mem_nhds hx) |>.mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, MDifferentiableWithinAt.mdifferentiableAt, 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'
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 ∈ t
⊢ MDifferentiableWithinAt I I' f (s ∪ t) x

Tactic:
exact (hf' x hx).mdifferentiableAt (ht.mem_nhds hx) |>.mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, MDifferentiableWithinAt.mdifferentiableAt, 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'
s t : Set M
hs : IsOpen[inst_4] s
ht : IsOpen[inst_4] t
⊢ MDifferentiableOn I I' f (s ∪ t) ↔ MDifferentiableOn I I' f s ∧ MDifferentiableOn I I' f t

Tactic:
⟨fun h ↦ ⟨h.mono subset_union_left, h.mono subset_union_right⟩,
    fun ⟨hfs, hft⟩ ↦ MDifferentiableOn.union_of_isOpen hfs hft hs ht⟩

Premises used: MDifferentiableOn.mono, Set.subset_union_right, _private.0.mdifferentiableOn_union_iff_of_isOpen.match_1, MDifferentiableOn, Set.subset_union_left, And.intro, Iff.intro, MDifferentiableOn.union_of_isOpen, Union.union
-- 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
hst : s ∪ t = univ
hs : IsOpen[inst_4] s
ht : IsOpen[inst_4] t
rw : MDifferentiableOn I I' f (s ∪ t)
⊢ MDifferentiable I I' f

Tactic:
rw [← mdifferentiableOn_univ, ← hst]

Premises used: 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 t : Set M
hf : MDifferentiableOn I I' f s
hf' : MDifferentiableOn I I' f t
hst : s ∪ t = univ
hs : IsOpen[inst_4] s
ht : IsOpen[inst_4] t
⊢ MDifferentiableOn I I' f (s ∪ t)

Tactic:
hf.union_of_isOpen hf' hs ht

Premises used: MDifferentiableOn.union_of_isOpen
-- 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
hst : s ∪ t = univ
hs : IsOpen[inst_4] s
ht : IsOpen[inst_4] t
⊢ MDifferentiableOn I I' f (s ∪ t)

Tactic:
exact hf.union_of_isOpen hf' hs ht

Premises used: MDifferentiableOn.union_of_isOpen
-- 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'
ι : Type u_11
s : ι → Set M
hf : ∀ (i : ι), MDifferentiableOn I I' f (s i)
hs : ∀ (i : ι), IsOpen[inst_4] (s i)
x : M
i : ι
hxsi : Membership.mem (γ := Set M) ((fun (i : ι) ↦ s i) i) x
⊢ MDifferentiableWithinAt I I' f (⋃ (i : ι), s i) x

Tactic:
(hf i).mdifferentiableAt ((hs i).mem_nhds hxsi) |>.mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, MDifferentiableOn.mdifferentiableAt, 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'
ι : Type u_11
s : ι → Set M
hf : ∀ (i : ι), MDifferentiableOn I I' f (s i)
hs : ∀ (i : ι), IsOpen[inst_4] (s i)
x : M
i : ι
hxsi : Membership.mem (γ := Set M) ((fun (i : ι) ↦ s i) i) x
⊢ MDifferentiableWithinAt I I' f (⋃ (i : ι), s i) x

Tactic:
exact (hf i).mdifferentiableAt ((hs i).mem_nhds hxsi) |>.mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, MDifferentiableOn.mdifferentiableAt, 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'
ι : Type u_11
s : ι → Set M
hs : ∀ (i : ι), IsOpen[inst_4] (s i)
⊢ MDifferentiableOn I I' f (⋃ (i : ι), s i) ↔ ∀ (i : ι), MDifferentiableOn I I' f (s i)

Tactic:
⟨fun h i ↦ h.mono <| subset_iUnion_of_subset i fun _ a ↦ a,
   fun h ↦ MDifferentiableOn.iUnion_of_isOpen h hs⟩

Premises used: Set.subset_iUnion_of_subset, MDifferentiableOn.mono, MDifferentiableOn.iUnion_of_isOpen, Iff.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'
ι : Type u_11
s : ι → Set M
hf : ∀ (i : ι), MDifferentiableOn I I' f (s i)
hs : ∀ (i : ι), IsOpen[inst_4] (s i)
hs' : Eq.{u_4 + 1} (α := Set M) (⋃ (i : ι), s i) univ
rw : MDifferentiableOn I I' f (⋃ (i : ι), s i)
⊢ MDifferentiable I I' f

Tactic:
rw [← mdifferentiableOn_univ, ← hs']

Premises used: 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'
ι : Type u_11
s : ι → Set M
hf : ∀ (i : ι), MDifferentiableOn I I' f (s i)
hs : ∀ (i : ι), IsOpen[inst_4] (s i)
hs' : Eq.{u_4 + 1} (α := Set M) (⋃ (i : ι), s i) univ
⊢ MDifferentiableOn I I' f (⋃ (i : ι), s i)

Tactic:
MDifferentiableOn.iUnion_of_isOpen hf hs

Premises used: MDifferentiableOn.iUnion_of_isOpen
-- 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'
ι : Type u_11
s : ι → Set M
hf : ∀ (i : ι), MDifferentiableOn I I' f (s i)
hs : ∀ (i : ι), IsOpen[inst_4] (s i)
hs' : Eq.{u_4 + 1} (α := Set M) (⋃ (i : ι), s i) univ
⊢ MDifferentiableOn I I' f (⋃ (i : ι), s i)

Tactic:
exact MDifferentiableOn.iUnion_of_isOpen hf hs

Premises used: MDifferentiableOn.iUnion_of_isOpen
-- 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'
⊢ ContinuousWithinAt f s x

Tactic:
h.1

Premises used: And.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' : 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'
⊢ ContinuousAt f x

Tactic:
h.1

Premises used: And.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'
s t : Set M
p : TangentBundle I M
st : s ⊆ t
hs : UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))
h : MDifferentiableWithinAt I I' f t (p.proj (E := TangentSpace I))
simp :
  Eq.{u_5 + 1} (α := TangentSpace I' (f (p.proj (E := TangentSpace I))))
    (((mfderivWithin I I' f s (p.proj (E := TangentSpace I)) :
            ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
              (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
          (a : TangentSpace I p.proj) → TangentSpace I' (f p.proj))
        (p.snd (E := TangentSpace I)) :
      TangentSpace I' (f (p.proj (E := TangentSpace I))))
    (((mfderivWithin I I' f t (p.proj (E := TangentSpace I)) :
            ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
              (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
          (a : TangentSpace I p.proj) → TangentSpace I' (f p.proj))
        (p.snd (E := TangentSpace I)) :
      TangentSpace I' (f (p.proj (E := TangentSpace I))))
⊢ Eq (α := TangentBundle I' M') (tangentMapWithin I I' f s p) (tangentMapWithin I I' f t p)

Tactic:
simp only [tangentMapWithin, mfld_simps]

Premises used: tangentMapWithin
-- 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
p : TangentBundle I M
st : s ⊆ t
hs : UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))
h : MDifferentiableWithinAt I I' f t (p.proj (E := TangentSpace I))
rw rw₁ :
  Eq.{u_5 + 1} (α := TangentSpace I' (f (p.proj (E := TangentSpace I))))
    (((mfderivWithin I I' f t (p.proj (E := TangentSpace I)) :
            ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
              (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
          (a : TangentSpace I p.proj) → TangentSpace I' (f p.proj))
        (p.snd (E := TangentSpace I)) :
      TangentSpace I' (f (p.proj (E := TangentSpace I))))
    (((mfderivWithin I I' f t (p.proj (E := TangentSpace I)) :
            ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
              (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
          (a : TangentSpace I p.proj) → TangentSpace I' (f p.proj))
        (p.snd (E := TangentSpace I)) :
      TangentSpace I' (f (p.proj (E := TangentSpace I))))
⊢ Eq.{u_5 + 1} (α := TangentSpace I' (f (p.proj (E := TangentSpace I))))
    (((mfderivWithin I I' f s (p.proj (E := TangentSpace I)) :
            ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
              (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
          (a : TangentSpace I p.proj) → TangentSpace I' (f p.proj))
        (p.snd (E := TangentSpace I)) :
      TangentSpace I' (f (p.proj (E := TangentSpace I))))
    (((mfderivWithin I I' f t (p.proj (E := TangentSpace I)) :
            ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
              (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
          (a : TangentSpace I p.proj) → TangentSpace I' (f p.proj))
        (p.snd (E := TangentSpace I)) :
      TangentSpace I' (f (p.proj (E := TangentSpace I))))

Tactic:
rw [mfderivWithin_subset st hs h]

Premises used: 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'
h : ∀ (p : TangentBundle I M), Eq (α := TangentBundle I' M') (tangentMapWithin I I' f univ p) (tangentMap I I' f p)
⊢ Eq (α := TangentBundle I M → TangentBundle I' M') (tangentMapWithin I I' f univ) (tangentMap I I' f)

Tactic:
ext p : 1
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
p : TangentBundle I M
⊢ Eq (α := TangentBundle I' M') (tangentMapWithin I I' f univ p) (tangentMap I I' f p)

Tactic:
simp only [tangentMapWithin, tangentMap, mfld_simps]

Premises used: tangentMapWithin, tangentMap
-- 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
p : TangentBundle I M
hs : UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))
h : MDifferentiableAt I I' f (p.proj (E := TangentSpace I))
⊢ MDifferentiableWithinAt I I' f univ (p.proj (E := TangentSpace I))

Tactic:
rw [← mdifferentiableWithinAt_univ] at h

Premises used: mdifferentiableWithinAt_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
p : TangentBundle I M
hs : UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))
h : MDifferentiableWithinAt I I' f univ (p.proj (E := TangentSpace I))
rw : Eq (α := TangentBundle I' M') (tangentMapWithin I I' f s p) (tangentMapWithin I I' f univ p)
⊢ Eq (α := TangentBundle I' M') (tangentMapWithin I I' f s p) (tangentMap I I' f p)

Tactic:
rw [← tangentMapWithin_univ]

Premises used: tangentMapWithin_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
p : TangentBundle I M
hs : UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))
h : MDifferentiableWithinAt I I' f univ (p.proj (E := TangentSpace I))
⊢ Eq (α := TangentBundle I' M') (tangentMapWithin I I' f s p) (tangentMapWithin I I' f univ p)

Tactic:
tangentMapWithin_subset (subset_univ _) hs h

Premises used: tangentMapWithin_subset, Set.subset_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
p : TangentBundle I M
hs : UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))
h : MDifferentiableWithinAt I I' f univ (p.proj (E := TangentSpace I))
⊢ Eq (α := TangentBundle I' M') (tangentMapWithin I I' f s p) (tangentMapWithin I I' f univ p)

Tactic:
exact tangentMapWithin_subset (subset_univ _) hs h

Premises used: tangentMapWithin_subset, Set.subset_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
p : TangentBundle I M
⊢ TotalSpace.proj (E := TangentSpace I') (tangentMapWithin I I' f s p) = f (p.proj (E := TangentSpace I))

Tactic:
rfl

Premises used: rfl