awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
s : Set M
n : WithTop ℕ∞
h : M' × N' → N
f : M → M'
g : M → N'
x : M
y : M' × N'
t : Set (M' × N')
ha : ContMDiffWithinAt (I'.prod J') J n h t (f x, g x)
fa : ContMDiffWithinAt I I' n f s x
ga : ContMDiffWithinAt I J' n g s x
e : (f x, g x) = y
st : MapsTo (fun (x : M) ↦ (f x, g x)) s t
⊢ ContMDiffWithinAt.{u_1, u_2, u_3, u_4, u_8, u_9, u_10} I J (M' := N) n (fun (x : M) ↦ h (f x, g x)) s x

Tactic:
ha.comp₂ fa ga st

Premises used: ContMDiffWithinAt.comp₂
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
s : Set M
n : WithTop ℕ∞
h : M' × N' → N
f : M → M'
g : M → N'
x : M
y : M' × N'
t : Set (M' × N')
ha : ContMDiffWithinAt (I'.prod J') J n h t (f x, g x)
fa : ContMDiffWithinAt I I' n f s x
ga : ContMDiffWithinAt I J' n g s x
e : (f x, g x) = y
st : MapsTo (fun (x : M) ↦ (f x, g x)) s t
⊢ ContMDiffWithinAt.{u_1, u_2, u_3, u_4, u_8, u_9, u_10} I J (M' := N) n (fun (x : M) ↦ h (f x, g x)) s x

Tactic:
exact ha.comp₂ fa ga st

Premises used: ContMDiffWithinAt.comp₂
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : WithTop ℕ∞
h : M' × N' → N
f : M → M'
g : M → N'
x : M
ha : ContMDiffAt (I'.prod J') J n h (f x, g x)
fa : ContMDiffAt I I' n f x
ga : ContMDiffAt I J' n g x
⊢ ContMDiffAt.{u_1, u_2, u_3, u_4, u_8, u_9, u_10} I J (M' := N) n (fun (x : M) ↦ h (f x, g x)) x

Tactic:
ha.comp (f := fun x ↦ (f x, g x)) _ (fa.prodMk ga)

Premises used: ContMDiffAt.prodMk, ContMDiffAt.comp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : WithTop ℕ∞
h : M' × N' → N
f : M → M'
g : M → N'
x : M
y : M' × N'
ha : ContMDiffAt (I'.prod J') J n h y
fa : ContMDiffAt I I' n f x
ga : ContMDiffAt I J' n g x
e : (f x, g x) = y
⊢ ContMDiffAt (I'.prod J') J n h (f x, g x)

Tactic:
rw [← e] at ha
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : WithTop ℕ∞
h : M' × N' → N
f : M → M'
g : M → N'
x : M
y : M' × N'
ha : ContMDiffAt (I'.prod J') J n h y
fa : ContMDiffAt I I' n f x
ga : ContMDiffAt I J' n g x
e : (f x, g x) = y
ha₁ : ContMDiffAt (I'.prod J') J n h (f x, g x)
⊢ ContMDiffAt I I' n f x

Tactic:
rw [← e] at ha
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : WithTop ℕ∞
h : M' × N' → N
f : M → M'
g : M → N'
x : M
y : M' × N'
ha : ContMDiffAt (I'.prod J') J n h y
fa : ContMDiffAt I I' n f x
ga : ContMDiffAt I J' n g x
e : (f x, g x) = y
ha₁ : ContMDiffAt (I'.prod J') J n h (f x, g x)
fa₁ : ContMDiffAt I I' n f x
⊢ ContMDiffAt I J' n g x

Tactic:
rw [← e] at ha
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : WithTop ℕ∞
h : M' × N' → N
f : M → M'
g : M → N'
x : M
y : M' × N'
ha : ContMDiffAt (I'.prod J') J n h y
fa : ContMDiffAt I I' n f x
ga : ContMDiffAt I J' n g x
e : (f x, g x) = y
ha₁ : ContMDiffAt (I'.prod J') J n h (f x, g x)
fa₁ : ContMDiffAt I I' n f x
ga₁ : ContMDiffAt I J' n g x
⊢ (f x, g x) = y

Tactic:
rw [← e] at ha
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : WithTop ℕ∞
h : M' × N' → N
f : M → M'
g : M → N'
x : M
y : M' × N'
ha : ContMDiffAt (I'.prod J') J n h (f x, g x)
fa : ContMDiffAt I I' n f x
ga : ContMDiffAt I J' n g x
e : (f x, g x) = y
⊢ ContMDiffAt.{u_1, u_2, u_3, u_4, u_8, u_9, u_10} I J (M' := N) n (fun (x : M) ↦ h (f x, g x)) x

Tactic:
ha.comp₂ fa ga

Premises used: ContMDiffAt.comp₂
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : WithTop ℕ∞
h : M' × N' → N
f : M → M'
g : M → N'
x : M
y : M' × N'
ha : ContMDiffAt (I'.prod J') J n h (f x, g x)
fa : ContMDiffAt I I' n f x
ga : ContMDiffAt I J' n g x
e : (f x, g x) = y
⊢ ContMDiffAt.{u_1, u_2, u_3, u_4, u_8, u_9, u_10} I J (M' := N) n (fun (x : M) ↦ h (f x, g x)) x

Tactic:
exact ha.comp₂ fa ga

Premises used: ContMDiffAt.comp₂
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n : WithTop ℕ∞
f : M → M' → N
x : M
y : M'
s : Set (M × M')
fa : ContMDiffWithinAt (I.prod I') J n (uncurry f) s (x, y)
⊢ ContMDiffWithinAt.{u_1, u_2, u_3, u_4, u_8, u_9, u_10} I J (M' := N) n (fun (x : M) ↦ f x y) {x : M | (x, y) ∈ s} x

Tactic:
fa.comp₂ contMDiffWithinAt_id contMDiffWithinAt_const (fun _ h ↦ h)

Premises used: Set.Mem, setOf, contMDiffWithinAt_const, ContMDiffWithinAt.comp₂, contMDiffWithinAt_id
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n : WithTop ℕ∞
f : M → M' → N
x : M
y : M'
s : Set (M × M')
fa : ContMDiffWithinAt (I.prod I') J n (uncurry f) s (x, y)
⊢ ContMDiffWithinAt.{u_1, u_5, u_6, u_7, u_8, u_9, u_10} I' J (M' := N) n (fun (y : M') ↦ f x y) {y : M' | (x, y) ∈ s} y

Tactic:
fa.comp₂ contMDiffWithinAt_const contMDiffWithinAt_id (fun _ h ↦ h)

Premises used: Set.Mem, setOf, contMDiffWithinAt_const, ContMDiffWithinAt.comp₂, contMDiffWithinAt_id
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n : WithTop ℕ∞
f : M → M' → N
x : M
y : M'
fa : ContMDiffAt (I.prod I') J n (uncurry f) (x, y)
⊢ ContMDiffAt.{u_1, u_2, u_3, u_4, u_8, u_9, u_10} I J (M' := N) n (fun (x : M) ↦ f x y) x

Tactic:
fa.comp₂ contMDiffAt_id contMDiffAt_const

Premises used: ContMDiffAt.comp₂, contMDiffAt_const, contMDiffAt_id
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n : WithTop ℕ∞
f : M → M' → N
x : M
y : M'
fa : ContMDiffAt (I.prod I') J n (uncurry f) (x, y)
⊢ ContMDiffAt.{u_1, u_5, u_6, u_7, u_8, u_9, u_10} I' J (M' := N) n (fun (y : M') ↦ f x y) y

Tactic:
fa.comp₂ contMDiffAt_const contMDiffAt_id

Premises used: ContMDiffAt.comp₂, contMDiffAt_const, contMDiffAt_id
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n : WithTop ℕ∞
f : M → M' → N
s : Set (M × M')
fa : ContMDiffOn (I.prod I') J n (uncurry f) s
y : M'
⊢ ContMDiffOn.{u_1, u_2, u_3, u_4, u_8, u_9, u_10} I J (M' := N) n (fun (x : M) ↦ f x y) {x : M | (x, y) ∈ s}

Tactic:
fun x m ↦ (fa (x, y) m).along_fst

Premises used: Prod.mk, ContMDiffWithinAt.along_fst, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n : WithTop ℕ∞
f : M → M' → N
x : M
s : Set (M × M')
fa : ContMDiffOn (I.prod I') J n (uncurry f) s
⊢ ContMDiffOn.{u_1, u_5, u_6, u_7, u_8, u_9, u_10} I' J (M' := N) n (fun (y : M') ↦ f x y) {y : M' | (x, y) ∈ s}

Tactic:
fun y m ↦ (fa (x, y) m).along_snd

Premises used: Prod.mk, ContMDiffWithinAt.along_snd, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n : WithTop ℕ∞
f : M → M' → N
fa : ContMDiff (I.prod I') J n (uncurry f)
y : M'
⊢ ContMDiff.{u_1, u_2, u_3, u_4, u_8, u_9, u_10} I J (M' := N) n fun (x : M) ↦ f x y

Tactic:
fun _ ↦ (fa _).along_fst

Premises used: ContMDiff, Prod.mk, ContMDiffAt.along_fst
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n : WithTop ℕ∞
f : M → M' → N
x : M
fa : ContMDiff (I.prod I') J n (uncurry f)
⊢ ContMDiff.{u_1, u_5, u_6, u_7, u_8, u_9, u_10} I' J (M' := N) n fun (y : M') ↦ f x y

Tactic:
fun _ ↦ (fa _).along_snd

Premises used: ContMDiff, Prod.mk, ContMDiffAt.along_snd
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
f : M → M'
s : Set M
n : WithTop ℕ∞
g : N → N'
r : Set N
p : M × N
hf : ContMDiffWithinAt I I' n f s p.1
hg : ContMDiffWithinAt J J' n g r p.2
⊢ ContMDiffWithinAt (I.prod J) (I'.prod J') n (Prod.map f g) (s ×ˢ r) p

Tactic:
(hf.comp p contMDiffWithinAt_fst mapsTo_fst_prod).prodMk <|
    hg.comp p contMDiffWithinAt_snd mapsTo_snd_prod

Premises used: contMDiffWithinAt_snd, Prod.map, contMDiffWithinAt_fst, ContMDiffWithinAt.prodMk, Set.mapsTo_fst_prod, Set.mapsTo_snd_prod, ContMDiffWithinAt.comp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions
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 : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
f : M → M'
s : Set M
x : M
n : WithTop ℕ∞
g : N → N'
r : Set N
y : N
hf : ContMDiffWithinAt I I' n f s x
hg : ContMDiffWithinAt J J' n g r y
⊢ ContMDiffWithinAt (I.prod J) (I'.prod J') n (Prod.map f g) (s ×ˢ r) (x, y)

Tactic:
ContMDiffWithinAt.prodMap' hf hg

Premises used: ContMDiffWithinAt.prodMap'