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
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
s : Set M
x : M
n : WithTop ℕ∞
f : M → F₁ × F₂
rw :
  ContMDiffWithinAt I (ModelWithCorners.prod 𝓘(𝕜, F₁) 𝓘(𝕜, F₂)) n f s x ↔
    ContMDiffWithinAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s x ∧ ContMDiffWithinAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s x
⊢ ContMDiffWithinAt I (E' := F₁ × F₂) 𝓘(𝕜, F₁ × F₂) n f s x ↔
    ContMDiffWithinAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s x ∧ ContMDiffWithinAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s x

Tactic:
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]

Premises used: chartedSpaceSelf_prod, modelWithCornersSelf_prod
-- 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
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
s : Set M
x : M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffWithinAt I (ModelWithCorners.prod 𝓘(𝕜, F₁) 𝓘(𝕜, F₂)) n f s x ↔
    ContMDiffWithinAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s x ∧ ContMDiffWithinAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s x

Tactic:
contMDiffWithinAt_prod_iff f

Premises used: contMDiffWithinAt_prod_iff, setOf, instTopologicalSpaceModelProd._aux_1, ModelProd
-- 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
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
s : Set M
x : M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffWithinAt I (ModelWithCorners.prod 𝓘(𝕜, F₁) 𝓘(𝕜, F₂)) n f s x ↔
    ContMDiffWithinAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s x ∧ ContMDiffWithinAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s x

Tactic:
exact contMDiffWithinAt_prod_iff f

Premises used: contMDiffWithinAt_prod_iff
-- 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_11
inst_11 : NormedAddCommGroup F'
inst_12 : NormedSpace 𝕜 F'
G' : Type u_12
inst_13 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_14 : TopologicalSpace N'
inst_15 : ChartedSpace G' N'
x : M
n : WithTop ℕ∞
f : M → M' × N'
⊢ ContMDiffWithinAt I (I'.prod J') n f univ x ↔
    ContMDiffWithinAt I I' n (Prod.fst ∘ f) univ x ∧ ContMDiffWithinAt I J' n (Prod.snd ∘ f) univ x

Tactic:
contMDiffWithinAt_prod_iff f

Premises used: contMDiffWithinAt_prod_iff
-- 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_11
inst_11 : NormedAddCommGroup F'
inst_12 : NormedSpace 𝕜 F'
G' : Type u_12
inst_13 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_14 : TopologicalSpace N'
inst_15 : ChartedSpace G' N'
x : M
n : WithTop ℕ∞
f : M → M' × N'
⊢ ContMDiffWithinAt I (I'.prod J') n f univ x ↔
    ContMDiffWithinAt I I' n (Prod.fst ∘ f) univ x ∧ ContMDiffWithinAt I J' n (Prod.snd ∘ f) univ x

Tactic:
exact contMDiffWithinAt_prod_iff f

Premises used: contMDiffWithinAt_prod_iff
-- 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
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
x : M
n : WithTop ℕ∞
f : M → F₁ × F₂
rw :
  ContMDiffAt I (ModelWithCorners.prod 𝓘(𝕜, F₁) 𝓘(𝕜, F₂)) n f x ↔
    ContMDiffAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) x ∧ ContMDiffAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) x
⊢ ContMDiffAt I (E' := F₁ × F₂) 𝓘(𝕜, F₁ × F₂) n f x ↔
    ContMDiffAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) x ∧ ContMDiffAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) x

Tactic:
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]

Premises used: chartedSpaceSelf_prod, modelWithCornersSelf_prod
-- 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
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
x : M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffAt I (ModelWithCorners.prod 𝓘(𝕜, F₁) 𝓘(𝕜, F₂)) n f x ↔
    ContMDiffAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) x ∧ ContMDiffAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) x

Tactic:
contMDiffAt_prod_iff f

Premises used: setOf, contMDiffAt_prod_iff, instTopologicalSpaceModelProd._aux_1, ModelProd
-- 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
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
x : M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffAt I (ModelWithCorners.prod 𝓘(𝕜, F₁) 𝓘(𝕜, F₂)) n f x ↔
    ContMDiffAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) x ∧ ContMDiffAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) x

Tactic:
exact contMDiffAt_prod_iff f

Premises used: contMDiffAt_prod_iff
-- 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_11
inst_11 : NormedAddCommGroup F'
inst_12 : NormedSpace 𝕜 F'
G' : Type u_12
inst_13 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_14 : TopologicalSpace N'
inst_15 : ChartedSpace G' N'
s : Set M
n : WithTop ℕ∞
f : M → M' × N'
⊢ ContMDiffOn I (I'.prod J') n f s ↔ ContMDiffOn I I' n (Prod.fst ∘ f) s ∧ ContMDiffOn I J' n (Prod.snd ∘ f) s

Tactic:
⟨fun h ↦ ⟨fun x hx ↦ ((contMDiffWithinAt_prod_iff f).1 (h x hx)).1,
      fun x hx ↦ ((contMDiffWithinAt_prod_iff f).1 (h x hx)).2⟩,
    fun h x hx ↦ (contMDiffWithinAt_prod_iff f).2 ⟨h.1 x hx, h.2 x hx⟩⟩

Premises used: Iff.mpr, contMDiffWithinAt_prod_iff, And.right, And.left, And.intro, Iff.intro, Iff.mp
-- 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
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
s : Set M
n : WithTop ℕ∞
f : M → F₁ × F₂
rw :
  ContMDiffOn I (ModelWithCorners.prod 𝓘(𝕜, F₁) 𝓘(𝕜, F₂)) n f s ↔
    ContMDiffOn I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s ∧ ContMDiffOn I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s
⊢ ContMDiffOn I (E' := F₁ × F₂) 𝓘(𝕜, F₁ × F₂) n f s ↔
    ContMDiffOn I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s ∧ ContMDiffOn I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s

Tactic:
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]

Premises used: chartedSpaceSelf_prod, modelWithCornersSelf_prod
-- 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
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
s : Set M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffOn I (ModelWithCorners.prod 𝓘(𝕜, F₁) 𝓘(𝕜, F₂)) n f s ↔
    ContMDiffOn I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s ∧ ContMDiffOn I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s

Tactic:
exact contMDiffOn_prod_iff f

Premises used: contMDiffOn_prod_iff
-- 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_11
inst_11 : NormedAddCommGroup F'
inst_12 : NormedSpace 𝕜 F'
G' : Type u_12
inst_13 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_14 : TopologicalSpace N'
inst_15 : ChartedSpace G' N'
n : WithTop ℕ∞
f : M → M' × N'
h : ContMDiff I I' n (Prod.fst ∘ f) ∧ ContMDiff I J' n (Prod.snd ∘ f)
⊢ ContMDiff I (I'.prod J') (M' := M' × N') n fun (x : M) ↦ ((Prod.fst ∘ f) x, (Prod.snd ∘ f) x)

Tactic:
h.1.prodMk h.2

Premises used: And.right, And.left, ContMDiff.prodMk
-- 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_11
inst_11 : NormedAddCommGroup F'
inst_12 : NormedSpace 𝕜 F'
G' : Type u_12
inst_13 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_14 : TopologicalSpace N'
inst_15 : ChartedSpace G' N'
n : WithTop ℕ∞
f : M → M' × N'
h : ContMDiff I I' n (Prod.fst ∘ f) ∧ ContMDiff I J' n (Prod.snd ∘ f)
⊢ ContMDiff I (I'.prod J') n f

Tactic:
convert! h.1.prodMk h.2

Premises used: And.right, And.left, ContMDiff.prodMk
-- 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
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
f : M → F₁ × F₂
rw :
  ContMDiff I (ModelWithCorners.prod 𝓘(𝕜, F₁) 𝓘(𝕜, F₂)) n f ↔
    ContMDiff I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) ∧ ContMDiff I 𝓘(𝕜, F₂) n (Prod.snd ∘ f)
⊢ ContMDiff I (E' := F₁ × F₂) 𝓘(𝕜, F₁ × F₂) n f ↔
    ContMDiff I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) ∧ ContMDiff I 𝓘(𝕜, F₂) n (Prod.snd ∘ f)

Tactic:
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]

Premises used: chartedSpaceSelf_prod, modelWithCornersSelf_prod
-- 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
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiff I (ModelWithCorners.prod 𝓘(𝕜, F₁) 𝓘(𝕜, F₂)) n f ↔
    ContMDiff I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) ∧ ContMDiff I 𝓘(𝕜, F₂) n (Prod.snd ∘ f)

Tactic:
contMDiff_prod_iff f

Premises used: setOf, contMDiff_prod_iff, instTopologicalSpaceModelProd._aux_1, ModelProd
-- 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
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiff I (ModelWithCorners.prod 𝓘(𝕜, F₁) 𝓘(𝕜, F₂)) n f ↔
    ContMDiff I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) ∧ ContMDiff I 𝓘(𝕜, F₂) n (Prod.snd ∘ f)

Tactic:
exact contMDiff_prod_iff f

Premises used: contMDiff_prod_iff
-- 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 ℕ∞
⊢ ContMDiff ((I.prod I').prod J) (I.prod (I'.prod J)) (M' := M × M' × N) n fun (x : (M × M') × N) ↦ (x.1.1, x.1.2, x.2)

Tactic:
contMDiff_fst.fst.prodMk <| contMDiff_fst.snd.prodMk contMDiff_snd

Premises used: contMDiff_snd, ContMDiff.fst, ContMDiff.snd, contMDiff_fst, ContMDiff.prodMk
-- 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
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
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 (f := fun x ↦ (f x, g x)) _ (fa.prodMk ga) st

Premises used: ContMDiffWithinAt.prodMk, 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 y
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 (I'.prod J') J n h t (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'
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 y
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
ha₁ : ContMDiffWithinAt (I'.prod J') J n h t (f x, g x)
⊢ ContMDiffWithinAt I I' n f s 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'
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 y
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
ha₁ : ContMDiffWithinAt (I'.prod J') J n h t (f x, g x)
fa₁ : ContMDiffWithinAt I I' n f s x
⊢ ContMDiffWithinAt I J' n g s 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'
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 y
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
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
⊢ (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'
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 y
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
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
⊢ MapsTo (fun (x : M) ↦ (f x, g x)) s t

Tactic:
rw [← e] at ha