awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this_1 : IsManifold I ω M
z_1 : H
hz_1 : M
z : E
hz :
  z ∈
    (extChartAt I z_1).target ∩
      (↑(extChartAt I z_1).symm : E → H) ⁻¹'
        (range e ∩ (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ⁻¹' (extChartAt I hz_1).source)
this : (↑I.symm : E → H) z ∈ range e
⊢ z ∈ range (↑I : H → E)

Tactic:
mem_of_subset_of_mem (extChartAt_target_subset_range _) hz.1

Premises used: Set.mem_of_subset_of_mem, extChartAt_target_subset_range, And.left
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this_1 : IsManifold I ω M
z_1 : H
hz_1 : M
z : E
hz :
  z ∈
    (extChartAt I z_1).target ∩
      (↑(extChartAt I z_1).symm : E → H) ⁻¹'
        (range e ∩ (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ⁻¹' (extChartAt I hz_1).source)
this : (↑I.symm : E → H) z ∈ range e
⊢ z ∈ range (↑I : H → E)

Tactic:
exact mem_of_subset_of_mem (extChartAt_target_subset_range _) hz.1

Premises used: Set.mem_of_subset_of_mem, extChartAt_target_subset_range, And.left
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
n : ℕ∞ω
inst_9 : ChartedSpace H M
inst_10 : Nonempty M'
e' : M' → H'
h' : IsOpenEmbedding e'
f : M → M'
hf : ContMDiff I I' n (e' ∘ f)
h : ∀ (x : M), f x = ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f) x
⊢ f = (↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f

Tactic:
ext
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
n : ℕ∞ω
inst_9 : ChartedSpace H M
inst_10 : Nonempty M'
e' : M' → H'
h' : IsOpenEmbedding e'
f : M → M'
hf : ContMDiff I I' n (e' ∘ f)
x : M
h : f x = (↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ((e' ∘ f) x)
h₁ : f x = (↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') (e' (f x))
h₂ h₃ : f x = f x
⊢ f x = ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f) x

Tactic:
rw [Function.comp_apply, Function.comp_apply, IsOpenEmbedding.toOpenPartialHomeomorph_left_inv]

Premises used: Function.comp_apply, Topology.IsOpenEmbedding.toOpenPartialHomeomorph_left_inv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
n : ℕ∞ω
inst_9 : ChartedSpace H M
inst_10 : Nonempty M'
e' : M' → H'
h' : IsOpenEmbedding e'
f : M → M'
hf : ContMDiff I I' n (e' ∘ f)
⊢ f = (↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f

Tactic:
have : f = (h'.toOpenPartialHomeomorph e').symm ∘ e' ∘ f := by
    ext
    rw [Function.comp_apply, Function.comp_apply, IsOpenEmbedding.toOpenPartialHomeomorph_left_inv]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
n : ℕ∞ω
inst_9 : ChartedSpace H M
inst_10 : Nonempty M'
e' : M' → H'
h' : IsOpenEmbedding e'
f : M → M'
hf : ContMDiff I I' n (e' ∘ f)
this : f = (↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f
rw : ContMDiff I I' n ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f)
⊢ ContMDiff I I' n f

Tactic:
rw [this]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
n : ℕ∞ω
inst_9 : ChartedSpace H M
inst_10 : Nonempty M'
e' : M' → H'
h' : IsOpenEmbedding e'
f : M → M'
hf : ContMDiff I I' n (e' ∘ f)
this : f = (↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f
apply : ∀ (x : M), (e' ∘ f) x ∈ range e'
⊢ ContMDiff I I' n ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f)

Tactic:
apply @ContMDiffOn.comp_contMDiff _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
    h'.singletonChartedSpace _ _ (range e') _ (contMDiffOn_isOpenEmbedding_symm h') hf

Premises used: contMDiffOn_isOpenEmbedding_symm, ContMDiffOn.comp_contMDiff
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
n : ℕ∞ω
inst_9 : ChartedSpace H M
inst_10 : Nonempty M'
e' : M' → H'
h' : IsOpenEmbedding e'
f : M → M'
hf : ContMDiff I I' n (e' ∘ f)
this : f = (↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f
⊢ ∀ (x : M), (e' ∘ f) x ∈ range e'

Tactic:
simp
-- 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
x : M
n : WithTop ℕ∞
f : M → M'
g : M → N'
hf : ContMDiffWithinAt I I' n f s x
hg : ContMDiffWithinAt I J' n g s x
rw :
  ∀
    (hf :
      ContinuousWithinAt f s x ∧
        ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
    (hg :
      ContinuousWithinAt g s x ∧
        ContDiffWithinAt 𝕜 n ((↑(extChartAt J' (g x)) : N' → F') ∘ g ∘ (↑(extChartAt I x).symm : E → M))
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)),
    ContinuousWithinAt (Y := M' × N') (fun (x : M) ↦ (f x, g x)) s x ∧
      ContDiffWithinAt 𝕜 n
        ((↑(extChartAt (I'.prod J') (f x, g x)) : M' × N' → E' × F') ∘
          (fun (x : M) ↦ (f x, g x)) ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ ContMDiffWithinAt I (I'.prod J') (M' := M' × N') n (fun (x : M) ↦ (f x, g x)) s x

Tactic:
rw [contMDiffWithinAt_iff] at *

Premises used: contMDiffWithinAt_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
x : M
n : WithTop ℕ∞
f : M → M'
g : M → N'
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
hg :
  ContinuousWithinAt g s x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt J' (g x)) : N' → F') ∘ g ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ ContinuousWithinAt (Y := M' × N') (fun (x : M) ↦ (f x, g x)) s x ∧
    ContDiffWithinAt 𝕜 n
      ((↑(extChartAt (I'.prod J') (f x, g x)) : M' × N' → E' × F') ∘
        (fun (x : M) ↦ (f x, g x)) ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩

Premises used: And.right, And.left, And.intro, ContDiffWithinAt.prodMk, ContinuousWithinAt.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'
s : Set M
x : M
n : WithTop ℕ∞
f : M → M'
g : M → N'
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
hg :
  ContinuousWithinAt g s x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt J' (g x)) : N' → F') ∘ g ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ ContinuousWithinAt (Y := M' × N') (fun (x : M) ↦ (f x, g x)) s x ∧
    ContDiffWithinAt 𝕜 n
      ((↑(extChartAt (I'.prod J') (f x, g x)) : M' × N' → E' × F') ∘
        (fun (x : M) ↦ (f x, g x)) ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
exact ⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩
-- 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'
F' : Type u_11
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
s : Set M
x : M
n : WithTop ℕ∞
f : M → E'
g : M → F'
hf : ContMDiffWithinAt I 𝓘(𝕜, E') n f s x
hg : ContMDiffWithinAt I 𝓘(𝕜, F') n g s x
rw :
  ∀
    (hf :
      ContinuousWithinAt f s x ∧
        ContDiffWithinAt 𝕜 n ((↑(extChartAt 𝓘(𝕜, E') (f x)) : E' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
    (hg :
      ContinuousWithinAt g s x ∧
        ContDiffWithinAt 𝕜 n ((↑(extChartAt 𝓘(𝕜, F') (g x)) : F' → F') ∘ g ∘ (↑(extChartAt I x).symm : E → M))
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)),
    ContinuousWithinAt (Y := E' × F') (fun (x : M) ↦ (f x, g x)) s x ∧
      ContDiffWithinAt 𝕜 (F := E' × F') n
        ((↑(extChartAt 𝓘(𝕜, E' × F') (f x, g x)) : E' × F' → E' × F') ∘
          (fun (x : M) ↦ (f x, g x)) ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ ContMDiffWithinAt I (E' := E' × F') 𝓘(𝕜, E' × F') (M' := E' × F') n (fun (x : M) ↦ (f x, g x)) s x

Tactic:
rw [contMDiffWithinAt_iff] at *

Premises used: contMDiffWithinAt_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'
F' : Type u_11
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
s : Set M
x : M
n : WithTop ℕ∞
f : M → E'
g : M → F'
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt 𝓘(𝕜, E') (f x)) : E' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
hg :
  ContinuousWithinAt g s x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt 𝓘(𝕜, F') (g x)) : F' → F') ∘ g ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ ContinuousWithinAt (Y := E' × F') (fun (x : M) ↦ (f x, g x)) s x ∧
    ContDiffWithinAt 𝕜 (F := E' × F') n
      ((↑(extChartAt 𝓘(𝕜, E' × F') (f x, g x)) : E' × F' → E' × F') ∘
        (fun (x : M) ↦ (f x, g x)) ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩

Premises used: And.right, And.left, And.intro, ContDiffWithinAt.prodMk, ContinuousWithinAt.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'
F' : Type u_11
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
s : Set M
x : M
n : WithTop ℕ∞
f : M → E'
g : M → F'
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt 𝓘(𝕜, E') (f x)) : E' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
hg :
  ContinuousWithinAt g s x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt 𝓘(𝕜, F') (g x)) : F' → F') ∘ g ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ ContinuousWithinAt (Y := E' × F') (fun (x : M) ↦ (f x, g x)) s x ∧
    ContDiffWithinAt 𝕜 (F := E' × F') n
      ((↑(extChartAt 𝓘(𝕜, E' × F') (f x, g x)) : E' × F' → E' × F') ∘
        (fun (x : M) ↦ (f x, g x)) ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
exact ⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩
-- 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'
g : M → N'
hf : ContMDiffAt I I' n f x
hg : ContMDiffAt I J' n g x
⊢ ContMDiffAt I (I'.prod J') (M' := M' × N') n (fun (x : M) ↦ (f x, g x)) x

Tactic:
hf.prodMk hg

Premises used: ContMDiffWithinAt.prodMk, ContMDiffAt
-- 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'
F' : Type u_11
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
x : M
n : WithTop ℕ∞
f : M → E'
g : M → F'
hf : ContMDiffAt I 𝓘(𝕜, E') n f x
hg : ContMDiffAt I 𝓘(𝕜, F') n g x
⊢ ContMDiffAt I (E' := E' × F') 𝓘(𝕜, E' × F') (M' := E' × F') n (fun (x : M) ↦ (f x, g x)) x

Tactic:
hf.prodMk_space hg

Premises used: ContMDiffWithinAt.prodMk_space, ContMDiffAt
-- 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'
g : M → N'
hf : ContMDiffOn I I' n f s
hg : ContMDiffOn I J' n g s
⊢ ContMDiffOn I (I'.prod J') (M' := M' × N') n (fun (x : M) ↦ (f x, g x)) s

Tactic:
fun x hx => (hf x hx).prodMk (hg x hx)

Premises used: ContMDiffWithinAt.prodMk, 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'
F' : Type u_11
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
s : Set M
n : WithTop ℕ∞
f : M → E'
g : M → F'
hf : ContMDiffOn I 𝓘(𝕜, E') n f s
hg : ContMDiffOn I 𝓘(𝕜, F') n g s
⊢ ContMDiffOn I (E' := E' × F') 𝓘(𝕜, E' × F') (M' := E' × F') n (fun (x : M) ↦ (f x, g x)) s

Tactic:
fun x hx => (hf x hx).prodMk_space (hg x hx)

Premises used: ContMDiffWithinAt.prodMk_space, 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_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'
g : M → N'
hf : ContMDiff I I' n f
hg : ContMDiff I J' n g
⊢ ContMDiff I (I'.prod J') (M' := M' × N') n fun (x : M) ↦ (f x, g x)

Tactic:
fun x =>
  (hf x).prodMk (hg x)

Premises used: ContMDiff, ContMDiffAt.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'
F' : Type u_11
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
n : WithTop ℕ∞
f : M → E'
g : M → F'
hf : ContMDiff I 𝓘(𝕜, E') n f
hg : ContMDiff I 𝓘(𝕜, F') n g
⊢ ContMDiff I (E' := E' × F') 𝓘(𝕜, E' × F') (M' := E' × F') n fun (x : M) ↦ (f x, g x)

Tactic:
fun x =>
  (hf x).prodMk_space (hg x)

Premises used: ContMDiff, ContMDiffAt.prodMk_space
-- 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_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_9
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
rw :
  ContinuousWithinAt Prod.fst s p ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I p.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N))
      ((extChartAt (I.prod J) p).target ∩
        (↑(extChartAt (I.prod J) p).symm : E × F → M × N) ⁻¹' (s ∩ Prod.fst ⁻¹' (extChartAt I p.1).source))
      ((↑(extChartAt (I.prod J) p) : M × N → E × F) p)
⊢ ContMDiffWithinAt (I.prod J) I n Prod.fst s p

Tactic:
rw [contMDiffWithinAt_iff']

Premises used: contMDiffWithinAt_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_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_9
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
⊢ ContinuousWithinAt Prod.fst s p ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I p.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N))
      ((extChartAt (I.prod J) p).target ∩
        (↑(extChartAt (I.prod J) p).symm : E × F → M × N) ⁻¹' (s ∩ Prod.fst ⁻¹' (extChartAt I p.1).source))
      ((↑(extChartAt (I.prod J) p) : M × N → E × F) p)

Tactic:
⟨continuousWithinAt_fst, contDiffWithinAt_fst.congr (fun y hy => ?_) ?_⟩

Premises used: contDiffWithinAt_fst, ContDiffWithinAt.congr, And.intro, continuousWithinAt_fst