awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
s : Set M
f : M → M'
g : M → M''
hf : MDiff[s] f
hg : MDiff[s] g
⊢ MDiff[s] fun (x : M) ↦ (f x, g x)

Tactic:
fun x hx ↦ (hf x hx).prodMk (hg x hx)

Premises used: MDifferentiableWithinAt.prodMk, MDifferentiableOn
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
g : M → M''
hf : MDiff f
hg : MDiff g
⊢ MDiff fun (x : M) ↦ (f x, g x)

Tactic:
fun x ↦ (hf x).prodMk (hg x)

Premises used: MDifferentiableAt.prodMk, MDifferentiable
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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'
E'' : Type u_8
inst_8 : NormedAddCommGroup E''
inst_9 : NormedSpace 𝕜 E''
s : Set M
f : M → E'
g : M → E''
hf : MDiff[s] f
hg : MDiff[s] g
⊢ MDiff[s] fun (x : M) ↦ (f x, g x)

Tactic:
fun x hx ↦ (hf x hx).prodMk_space (hg x hx)

Premises used: MDifferentiableWithinAt.prodMk_space, MDifferentiableOn
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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'
E'' : Type u_8
inst_8 : NormedAddCommGroup E''
inst_9 : NormedSpace 𝕜 E''
f : M → E'
g : M → E''
hf : MDiff f
hg : MDiff g
⊢ MDiff fun (x : M) ↦ (f x, g x)

Tactic:
fun x ↦ (hf x).prodMk_space (hg x)

Premises used: MDifferentiableAt.prodMk_space, MDifferentiable
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M'
⊢ HasMFDerivAt (I.prod I') I Prod.fst x (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))

Tactic:
⟨continuous_fst.continuousAt, ?_⟩

Premises used: HasMFDerivAt, continuous_fst, Continuous.continuousAt, And.intro
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M'
refine :
  HasFDerivWithinAt (𝕜 := 𝕜) (writtenInExtChartAt (I.prod I') I x Prod.fst)
    (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
    (range (↑(I.prod I') : ModelProd H H' → E × E')) ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x)
⊢ HasMFDerivAt (I.prod I') I Prod.fst x (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))

Tactic:
refine ⟨continuous_fst.continuousAt, ?_⟩
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M'
h :
  ∀ (y : E × E') (hy : y ∈ (extChartAt (I.prod I') x).target),
    ((↑(extChartAt I x.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.1
⊢ ∀ᶠ (y : E × E') in
    𝓝[range (↑(I.prod I') : ModelProd H H' → E × E')] (↑(extChartAt (I.prod I') x) : M × M' → E × E') x,
    ((↑(extChartAt I x.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.1

Tactic:
filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy

Premises used: extChartAt_target_mem_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M'
y : E × E'
hy : y ∈ (extChartAt (I.prod I') x).target
⊢ y ∈ ((extChartAt I x.1).prod (extChartAt I' x.2)).target

Tactic:
rw [extChartAt_prod] at hy

Premises used: extChartAt_prod
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M'
y : E × E'
hy : y ∈ ((extChartAt I x.1).prod (extChartAt I' x.2)).target
⊢ ((↑(extChartAt I x.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.1

Tactic:
(extChartAt I x.1).right_inv hy.1

Premises used: extChartAt, PartialEquiv.right_inv, Prod.fst, And.left
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M'
y : E × E'
hy : y ∈ ((extChartAt I x.1).prod (extChartAt I' x.2)).target
⊢ ((↑(extChartAt I x.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.1

Tactic:
exact (extChartAt I x.1).right_inv hy.1

Premises used: extChartAt, PartialEquiv.right_inv, Prod.fst, And.left
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M'
⊢ ∀ᶠ (y : E × E') in
    𝓝[range (↑(I.prod I') : ModelProd H H' → E × E')] (↑(extChartAt (I.prod I') x) : M × M' → E × E') x,
    ((↑(extChartAt I x.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.1

Tactic:
have :
    ∀ᶠ y in 𝓝[range (I.prod I')] extChartAt (I.prod I') x x,
      (extChartAt I x.1 ∘ Prod.fst ∘ (extChartAt (I.prod I') x).symm) y = y.1 := by
    /- porting note: was
    apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin (I.prod I') x)
    mfld_set_tac
    -/
    filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy
    rw [extChartAt_prod] at hy
    exact (extChartAt I x.1).right_inv hy.1
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M'
this :
  ∀ᶠ (y : E × E') in
    𝓝[range (↑(I.prod I') : ModelProd H H' → E × E')] (↑(extChartAt (I.prod I') x) : M × M' → E × E') x,
    ((↑(extChartAt I x.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.1
apply :
  ((↑(extChartAt I x.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M'))
      ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x) =
    ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x).1
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (writtenInExtChartAt (I.prod I') I x Prod.fst)
    (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
    (range (↑(I.prod I') : ModelProd H H' → E × E')) ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x)

Tactic:
apply HasFDerivWithinAt.congr_of_eventuallyEq hasFDerivWithinAt_fst this

Premises used: HasFDerivWithinAt.congr_of_eventuallyEq, hasFDerivWithinAt_fst
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M'
this :
  ∀ᶠ (y : E × E') in
    𝓝[range (↑(I.prod I') : ModelProd H H' → E × E')] (↑(extChartAt (I.prod I') x) : M × M' → E × E') x,
    ((↑(extChartAt I x.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.1
⊢ ((↑(extChartAt I x.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M'))
      ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x) =
    ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x).1

Tactic:
(extChartAt I x.1).right_inv <| (extChartAt I x.1).map_source (mem_extChartAt_source _)

Premises used: extChartAt, PartialEquiv.map_source, mem_extChartAt_source, PartialEquiv.right_inv, Prod.fst
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M'
this :
  ∀ᶠ (y : E × E') in
    𝓝[range (↑(I.prod I') : ModelProd H H' → E × E')] (↑(extChartAt (I.prod I') x) : M × M' → E × E') x,
    ((↑(extChartAt I x.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.1
⊢ ((↑(extChartAt I x.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M'))
      ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x) =
    ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x).1

Tactic:
exact (extChartAt I x.1).right_inv <| (extChartAt I x.1).map_source (mem_extChartAt_source _)

Premises used: extChartAt, PartialEquiv.map_source, mem_extChartAt_source, PartialEquiv.right_inv, Prod.fst
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M')
x : M × M'
⊢ HasMFDerivWithinAt (I.prod I') I Prod.fst s x (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))

Tactic:
(hasMFDerivAt_fst x).hasMFDerivWithinAt

Premises used: hasMFDerivAt_fst, HasMFDerivAt.hasMFDerivWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M'
⊢ MDiffAt Prod.fst x

Tactic:
(hasMFDerivAt_fst x).mdifferentiableAt

Premises used: hasMFDerivAt_fst, HasMFDerivAt.mdifferentiableAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M')
x : M × M'
⊢ MDiffAt[s] Prod.fst x

Tactic:
mdifferentiableAt_fst.mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, mdifferentiableAt_fst
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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'
⊢ MDiff Prod.fst

Tactic:
fun _ ↦ mdifferentiableAt_fst

Premises used: mdifferentiableAt_fst, MDifferentiable
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M')
⊢ MDiff[s] Prod.fst

Tactic:
mdifferentiable_fst.mdifferentiableOn

Premises used: mdifferentiable_fst, MDifferentiable.mdifferentiableOn
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M'
⊢ Eq (α := TangentSpace (I.prod I') x →L[𝕜] TangentSpace I x.1) (mfderiv% Prod.fst x)
    (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))

Tactic:
(hasMFDerivAt_fst x).mfderiv

Premises used: hasMFDerivAt_fst, HasMFDerivAt.mfderiv, TangentSpace
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M')
x : M × M'
hxs : UniqueMDiffWithinAt (I.prod I') s x
rw :
  Eq (α := TangentSpace (I.prod I') x →L[𝕜] TangentSpace I x.1) (mfderiv% Prod.fst x)
    (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
⊢ Eq (α := TangentSpace (I.prod I') x →L[𝕜] TangentSpace I x.1) (mfderivWithin (I.prod I') I Prod.fst s x)
    (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))

Tactic:
rw [MDifferentiable.mfderivWithin mdifferentiableAt_fst hxs]

Premises used: mdifferentiableAt_fst, MDifferentiable.mfderivWithin
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M')
x : M × M'
hxs : UniqueMDiffWithinAt (I.prod I') s x
⊢ Eq (α := TangentSpace (I.prod I') x →L[𝕜] TangentSpace I x.1) (mfderiv% Prod.fst x)
    (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))

Tactic:
mfderiv_fst

Premises used: mfderiv_fst
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 × M')
x : M × M'
hxs : UniqueMDiffWithinAt (I.prod I') s x
⊢ Eq (α := TangentSpace (I.prod I') x →L[𝕜] TangentSpace I x.1) (mfderiv% Prod.fst x)
    (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))

Tactic:
exact mfderiv_fst

Premises used: mfderiv_fst
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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'
p : TangentBundle (I.prod I') (M × M')
simp :
  ((ContinuousLinearMap.fst 𝕜 (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
            (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) :
          Prod.{u_2, u_5} (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
              (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) →L[𝕜]
            TangentSpace I p.proj (E := TangentSpace (I.prod I')).1) :
        (a : TangentSpace (I.prod I') p.proj) → TangentSpace I p.proj.1)
      (p.snd (E := TangentSpace (I.prod I'))) =
    p.snd (E := TangentSpace (I.prod I')).1
⊢ Eq (α := TangentBundle I M) (tangentMap (I.prod I') I Prod.fst p)
    ⟨p.proj (E := TangentSpace (I.prod I')).1, p.snd (E := TangentSpace (I.prod I')).1⟩

Tactic:
simp [tangentMap]

Premises used: tangentMap
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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'
p : TangentBundle (I.prod I') (M × M')
⊢ ((ContinuousLinearMap.fst 𝕜 (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
            (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) :
          Prod.{u_2, u_5} (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
              (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) →L[𝕜]
            TangentSpace I p.proj (E := TangentSpace (I.prod I')).1) :
        (a : TangentSpace (I.prod I') p.proj) → TangentSpace I p.proj.1)
      (p.snd (E := TangentSpace (I.prod I'))) =
    p.snd (E := TangentSpace (I.prod I')).1

Tactic:
rfl