awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiffOn I s
x₀ : TangentBundle I M
hx₀ : Membership.mem (γ := Set (TangentBundle I M)) (TotalSpace.proj (E := TangentSpace I) ⁻¹' s) x₀
s' : Set (TangentBundle I M) := TotalSpace.proj (E := TangentSpace I) ⁻¹' s
b₁ : TangentBundle I M → M := fun (p : TangentBundle I M) ↦ p.proj (E := TangentSpace I)
v : (y : TangentBundle I M) → TangentSpace I (b₁ y) := fun (y : TangentBundle I M) ↦ y.snd (E := TangentSpace I)
hv :
  ContMDiffWithinAt I.tangent I.tangent (M' := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) m
    (fun (y : TangentBundle I M) ↦ ⟨b₁ y, v y⟩) s' x₀
b₂ : TangentBundle I M → M' := f ∘ b₁
hb₂ : ContMDiffWithinAt I.tangent I' m b₂ s' x₀
ϕ : (y : TangentBundle I M) →
  ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (b₁ y)) (TangentSpace I' (b₂ y)) :=
  fun (y : TangentBundle I M) ↦ mfderivWithin I I' f s (b₁ y)
hϕ :
  ContMDiffWithinAt I.tangent (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (y : TangentBundle I M) ↦
      ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') (b₁ x₀) (b₁ y) (b₂ x₀) (b₂ y) (ϕ y))
    s' x₀
⊢ ContMDiffWithinAt I.tangent I'.tangent (M' := TangentBundle I' M') m (tangentMapWithin I I' f s)
    (TotalSpace.proj (E := TangentSpace I) ⁻¹' s) x₀

Tactic:
ContMDiffWithinAt.clm_apply_of_inCoordinates hϕ hv hb₂

Premises used: ContMDiffWithinAt.clm_apply_of_inCoordinates, tangentMapWithin
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiffOn I s
x₀ : TangentBundle I M
hx₀ : Membership.mem (γ := Set (TangentBundle I M)) (TotalSpace.proj (E := TangentSpace I) ⁻¹' s) x₀
s' : Set (TangentBundle I M) := TotalSpace.proj (E := TangentSpace I) ⁻¹' s
b₁ : TangentBundle I M → M := fun (p : TangentBundle I M) ↦ p.proj (E := TangentSpace I)
v : (y : TangentBundle I M) → TangentSpace I (b₁ y) := fun (y : TangentBundle I M) ↦ y.snd (E := TangentSpace I)
hv :
  ContMDiffWithinAt I.tangent I.tangent (M' := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) m
    (fun (y : TangentBundle I M) ↦ ⟨b₁ y, v y⟩) s' x₀
b₂ : TangentBundle I M → M' := f ∘ b₁
hb₂ : ContMDiffWithinAt I.tangent I' m b₂ s' x₀
ϕ : (y : TangentBundle I M) →
  ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (b₁ y)) (TangentSpace I' (b₂ y)) :=
  fun (y : TangentBundle I M) ↦ mfderivWithin I I' f s (b₁ y)
hϕ :
  ContMDiffWithinAt I.tangent (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (y : TangentBundle I M) ↦
      ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') (b₁ x₀) (b₁ y) (b₂ x₀) (b₂ y) (ϕ y))
    s' x₀
⊢ ContMDiffWithinAt I.tangent I'.tangent (M' := TangentBundle I' M') m (tangentMapWithin I I' f s)
    (TotalSpace.proj (E := TangentSpace I) ⁻¹' s) x₀

Tactic:
exact ContMDiffWithinAt.clm_apply_of_inCoordinates hϕ hv hb₂

Premises used: ContMDiffWithinAt.clm_apply_of_inCoordinates
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : 1 ≤ n
hs : UniqueMDiffOn I s
⊢ ContMDiffOn I.tangent (M := TangentBundle I M) I'.tangent (M' := TangentBundle I' M') 0 (tangentMapWithin I I' f s)
    (TotalSpace.proj (E := TangentSpace I) ⁻¹' s)

Tactic:
have : CMDiff[π E (TangentSpace I) ⁻¹' s] 0 (tangentMapWithin I I' f s) :=
    hf.contMDiffOn_tangentMapWithin hmn hs
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : 1 ≤ n
hs : UniqueMDiffOn I s
this :
  ContMDiffOn I.tangent (M := TangentBundle I M) I'.tangent (M' := TangentBundle I' M') 0 (tangentMapWithin I I' f s)
    (TotalSpace.proj (E := TangentSpace I) ⁻¹' s)
⊢ ContinuousOn (X := TangentBundle I M) (Y := TangentBundle I' M') (tangentMapWithin I I' f s)
    (TotalSpace.proj (E := TangentSpace I) ⁻¹' s)

Tactic:
this.continuousOn

Premises used: ContMDiffOn.continuousOn
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : 1 ≤ n
hs : UniqueMDiffOn I s
this :
  ContMDiffOn I.tangent (M := TangentBundle I M) I'.tangent (M' := TangentBundle I' M') 0 (tangentMapWithin I I' f s)
    (TotalSpace.proj (E := TangentSpace I) ⁻¹' s)
⊢ ContinuousOn (X := TangentBundle I M) (Y := TangentBundle I' M') (tangentMapWithin I I' f s)
    (TotalSpace.proj (E := TangentSpace I) ⁻¹' s)

Tactic:
exact this.continuousOn

Premises used: ContMDiffOn.continuousOn
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiff I I' n f
hmn : m + 1 ≤ n
rw :
  ∀ (hf : ContMDiffOn I I' n f univ) (hmn : m + 1 ≤ n),
    ContMDiffOn I.tangent (M := TangentBundle I M) I'.tangent (M' := TangentBundle I' M') m (tangentMap I I' f) univ
⊢ ContMDiff I.tangent (M := TangentBundle I M) I'.tangent (M' := TangentBundle I' M') m (tangentMap I I' f)

Tactic:
rw [← contMDiffOn_univ] at hf ⊢

Premises used: contMDiffOn_univ
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f univ
hmn : m + 1 ≤ n
⊢ ContMDiffOn I.tangent (M := TangentBundle I M) I'.tangent (M' := TangentBundle I' M') m (tangentMapWithin I I' f univ)
    (TotalSpace.proj (E := TangentSpace I) ⁻¹' univ)

Tactic:
hf.contMDiffOn_tangentMapWithin hmn uniqueMDiffOn_univ

Premises used: uniqueMDiffOn_univ, ContMDiffOn.contMDiffOn_tangentMapWithin
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f univ
hmn : m + 1 ≤ n
h : Eq (α := TangentBundle I M → TangentBundle I' M') (tangentMap I I' f) (tangentMapWithin I I' f univ)
⊢ ContMDiffOn I.tangent (M := TangentBundle I M) I'.tangent (M' := TangentBundle I' M') m (tangentMap I I' f) univ

Tactic:
convert! hf.contMDiffOn_tangentMapWithin hmn uniqueMDiffOn_univ

Premises used: uniqueMDiffOn_univ, ContMDiffOn.contMDiffOn_tangentMapWithin
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f univ
hmn : m + 1 ≤ n
h h₁ : Eq (α := TangentBundle I M → TangentBundle I' M') (tangentMap I I' f) (tangentMap I I' f)
⊢ Eq (α := TangentBundle I M → TangentBundle I' M') (tangentMap I I' f) (tangentMapWithin I I' f univ)

Tactic:
rw [tangentMapWithin_univ]

Premises used: tangentMapWithin_univ
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiff I I' n f
hmn : 1 ≤ n
⊢ ContMDiffOn I I' n f univ

Tactic:
rw [← contMDiffOn_univ] at hf

Premises used: contMDiffOn_univ
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiff I I' n f
hmn : 1 ≤ n
hf₁ : ContMDiffOn I I' n f univ
⊢ 1 ≤ n

Tactic:
rw [← contMDiffOn_univ] at hf

Premises used: contMDiffOn_univ
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f univ
hmn : 1 ≤ n
rw : ContinuousOn (X := TangentBundle I M) (Y := TangentBundle I' M') (tangentMap I I' f) univ
⊢ Continuous[instTopologicalSpaceTangentBundle, instTopologicalSpaceTangentBundle] (tangentMap I I' f)

Tactic:
rw [← continuousOn_univ]

Premises used: continuousOn_univ
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f univ
hmn : 1 ≤ n
⊢ ContinuousOn (X := TangentBundle I M) (Y := TangentBundle I' M') (tangentMapWithin I I' f univ)
    (TotalSpace.proj (E := TangentSpace I) ⁻¹' univ)

Tactic:
hf.continuousOn_tangentMapWithin hmn uniqueMDiffOn_univ

Premises used: uniqueMDiffOn_univ, ContMDiffOn.continuousOn_tangentMapWithin
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f univ
hmn : 1 ≤ n
h : Eq (α := TangentBundle I M → TangentBundle I' M') (tangentMap I I' f) (tangentMapWithin I I' f univ)
⊢ ContinuousOn (X := TangentBundle I M) (Y := TangentBundle I' M') (tangentMap I I' f) univ

Tactic:
convert! hf.continuousOn_tangentMapWithin hmn uniqueMDiffOn_univ

Premises used: uniqueMDiffOn_univ, ContMDiffOn.continuousOn_tangentMapWithin
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f univ
hmn : 1 ≤ n
h h₁ : Eq (α := TangentBundle I M → TangentBundle I' M') (tangentMap I I' f) (tangentMap I I' f)
⊢ Eq (α := TangentBundle I M → TangentBundle I' M') (tangentMap I I' f) (tangentMapWithin I I' f univ)

Tactic:
rw [tangentMapWithin_univ]

Premises used: tangentMapWithin_univ
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
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
Is : IsManifold I 1 M
p : TangentBundle I M
rcases :
  ∀ (x : M) (v : TangentSpace I x),
    Eq (α := TangentBundle I.tangent (TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)))
      (tangentMap I I.tangent (zeroSection E (TangentSpace I)) ⟨x, v⟩)
      ⟨⟨TotalSpace.proj (F := E) (E := TangentSpace I) ⟨x, v⟩, 0⟩, (TotalSpace.snd (E := TangentSpace I) ⟨x, v⟩, 0)⟩
⊢ Eq (α := TangentBundle I.tangent (TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)))
    (tangentMap I I.tangent (zeroSection E (TangentSpace I)) p)
    ⟨⟨p.proj (E := TangentSpace I), 0⟩, (p.snd (E := TangentSpace I), 0)⟩

Tactic:
rcases p with ⟨x, v⟩
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
hs :
  IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
hx :
  (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈
    (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target
⊢ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))

Tactic:
apply IsOpen.mem_nhds

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)

Tactic:
apply (OpenPartialHomeomorph.open_target _).preimage I.continuous_invFun

Premises used: ModelWithCorners.continuous_invFun, OpenPartialHomeomorph.open_target, IsOpen.preimage
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
⊢ (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈
    (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
⊢ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))

Tactic:
have N : I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (I ((chartAt H x) x)) := by
    apply IsOpen.mem_nhds
    · apply (OpenPartialHomeomorph.open_target _).preimage I.continuous_invFun
    · simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
⊢ (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x

Tactic:
have A : MDiffAt (fun x ↦ TotalSpace.mk' E (x : M) (0 : TangentSpace I x)) x :=
    haveI : CMDiff 1 (zeroSection E (TangentSpace I : M → Type _)) :=
      Bundle.contMDiff_zeroSection 𝕜 (TangentSpace I : M → Type _)
    this.mdifferentiableAt one_ne_zero
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
rw :
  Eq (α := E × E)
    ((ContinuousLinearMap.prod (fderiv 𝕜 (fun (x' : E) ↦ x') ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
            (fderiv 𝕜 (fun (x' : E) ↦ 0) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
hf₁ : DifferentiableAt 𝕜 (F := E) (fun (x' : E) ↦ x') ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
hf₂ : DifferentiableAt 𝕜 (F := E) (fun (x' : E) ↦ 0) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
hs : UniqueDiffWithinAt 𝕜 (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
h : DifferentiableAt 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
⊢ Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0)) (range (↑I : H → E))
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)

Tactic:
rw [fderivWithin_eq_fderiv, DifferentiableAt.fderiv_prodMk]

Premises used: DifferentiableAt.fderiv_prodMk, fderivWithin_eq_fderiv
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
⊢ Eq (α := E × E)
    ((ContinuousLinearMap.prod (fderiv 𝕜 (fun (x' : E) ↦ x') ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
            (fderiv 𝕜 (fun (x' : E) ↦ 0) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
⊢ DifferentiableAt 𝕜 (F := E) (fun (x' : E) ↦ x') ((↑I : H → E) ((↑(chartAt H x) : M → H) x))

Tactic:
differentiableAt_fun_id

Premises used: differentiableAt_fun_id