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_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
refine_1 :
  ∀ (y : E × F)
    (hy :
      y ∈
        (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 p.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N)) y = y.1
refine_2 :
  ((↑(extChartAt I p.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N))
      ((↑(extChartAt (I.prod J) p) : M × N → E × F) p) =
    ((↑(extChartAt (I.prod J) p) : M × N → E × F) p).1
⊢ 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:
refine ⟨continuousWithinAt_fst, contDiffWithinAt_fst.congr (fun y hy => ?_) ?_⟩
-- 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
y : E × F
hy :
  y ∈
    (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 p.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N)) y = y.1

Tactic:
(extChartAt I p.1).right_inv ⟨hy.1.1.1, hy.1.2.1⟩

Premises used: extChartAt, PartialEquiv.right_inv, Prod.fst, And.right, And.left, And.intro
-- 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
y : E × F
hy :
  y ∈
    (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 p.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N)) y = y.1

Tactic:
exact (extChartAt I p.1).right_inv ⟨hy.1.1.1, hy.1.2.1⟩

Premises used: extChartAt, PartialEquiv.right_inv, Prod.fst, And.right, And.left, And.intro
-- 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
⊢ ((↑(extChartAt I p.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N))
      ((↑(extChartAt (I.prod J) p) : M × N → E × F) p) =
    ((↑(extChartAt (I.prod J) p) : M × N → E × F) p).1

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

Premises used: extChartAt, PartialEquiv.map_source, mem_extChartAt_source, PartialEquiv.right_inv, Prod.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
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
⊢ ((↑(extChartAt I p.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N))
      ((↑(extChartAt (I.prod J) p) : M × N → E × F) p) =
    ((↑(extChartAt (I.prod J) p) : M × N → E × F) p).1

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

Premises used: extChartAt, PartialEquiv.map_source, mem_extChartAt_source, PartialEquiv.right_inv, Prod.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 : N → M × M'
s : Set N
x : N
hf : ContMDiffWithinAt J (I.prod I') n f s x
⊢ ContMDiffWithinAt.{u_1, u_8, u_9, u_10, u_2, u_3, u_4} J I (M' := M) n (fun (x : N) ↦ (f x).1) s x

Tactic:
contMDiffWithinAt_fst.comp x hf (mapsTo_image f s)

Premises used: Set.mapsTo_image, contMDiffWithinAt_fst, 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
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 ℕ∞
p : M × N
⊢ ContMDiffAt (I.prod J) I n Prod.fst p

Tactic:
contMDiffWithinAt_fst

Premises used: contMDiffWithinAt_fst, 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
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 ℕ∞
⊢ ContMDiff (I.prod J) (M := M × N) I n Prod.fst

Tactic:
fun _ => contMDiffAt_fst

Premises used: ContMDiff, contMDiffAt_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 : N → M × M'
x : N
hf : ContMDiffAt J (I.prod I') n f x
⊢ ContMDiffAt.{u_1, u_8, u_9, u_10, u_2, u_3, u_4} J I (M' := M) n (fun (x : N) ↦ (f x).1) x

Tactic:
contMDiffAt_fst.comp x hf

Premises used: contMDiffAt_fst, 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 : N → M × M'
hf : ContMDiff J (I.prod I') n f
⊢ ContMDiff.{u_1, u_8, u_9, u_10, u_2, u_3, u_4} J I (M' := M) n fun (x : N) ↦ (f x).1

Tactic:
contMDiff_fst.comp hf

Premises used: ContMDiff.comp, contMDiff_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
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.snd s p ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt J p.2) : N → F) ∘ Prod.snd ∘ (↑(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.snd ⁻¹' (extChartAt J p.2).source))
      ((↑(extChartAt (I.prod J) p) : M × N → E × F) p)
⊢ ContMDiffWithinAt (I.prod J) J n Prod.snd 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.snd s p ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt J p.2) : N → F) ∘ Prod.snd ∘ (↑(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.snd ⁻¹' (extChartAt J p.2).source))
      ((↑(extChartAt (I.prod J) p) : M × N → E × F) p)

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

Premises used: ContDiffWithinAt.congr, And.intro, continuousWithinAt_snd, contDiffWithinAt_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
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
refine_1 :
  ∀ (y : E × F)
    (hy :
      y ∈
        (extChartAt (I.prod J) p).target ∩
          (↑(extChartAt (I.prod J) p).symm : E × F → M × N) ⁻¹' (s ∩ Prod.snd ⁻¹' (extChartAt J p.2).source)),
    ((↑(extChartAt J p.2) : N → F) ∘ Prod.snd ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N)) y = y.2
refine_2 :
  ((↑(extChartAt J p.2) : N → F) ∘ Prod.snd ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N))
      ((↑(extChartAt (I.prod J) p) : M × N → E × F) p) =
    ((↑(extChartAt (I.prod J) p) : M × N → E × F) p).2
⊢ ContinuousWithinAt Prod.snd s p ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt J p.2) : N → F) ∘ Prod.snd ∘ (↑(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.snd ⁻¹' (extChartAt J p.2).source))
      ((↑(extChartAt (I.prod J) p) : M × N → E × F) p)

Tactic:
refine ⟨continuousWithinAt_snd, contDiffWithinAt_snd.congr (fun y hy => ?_) ?_⟩
-- 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
y : E × F
hy :
  y ∈
    (extChartAt (I.prod J) p).target ∩
      (↑(extChartAt (I.prod J) p).symm : E × F → M × N) ⁻¹' (s ∩ Prod.snd ⁻¹' (extChartAt J p.2).source)
⊢ ((↑(extChartAt J p.2) : N → F) ∘ Prod.snd ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N)) y = y.2

Tactic:
(extChartAt J p.2).right_inv ⟨hy.1.1.2, hy.1.2.2⟩

Premises used: extChartAt, PartialEquiv.right_inv, And.right, And.left, And.intro, Prod.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
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
y : E × F
hy :
  y ∈
    (extChartAt (I.prod J) p).target ∩
      (↑(extChartAt (I.prod J) p).symm : E × F → M × N) ⁻¹' (s ∩ Prod.snd ⁻¹' (extChartAt J p.2).source)
⊢ ((↑(extChartAt J p.2) : N → F) ∘ Prod.snd ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N)) y = y.2

Tactic:
exact (extChartAt J p.2).right_inv ⟨hy.1.1.2, hy.1.2.2⟩

Premises used: extChartAt, PartialEquiv.right_inv, And.right, And.left, And.intro, Prod.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
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
⊢ ((↑(extChartAt J p.2) : N → F) ∘ Prod.snd ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N))
      ((↑(extChartAt (I.prod J) p) : M × N → E × F) p) =
    ((↑(extChartAt (I.prod J) p) : M × N → E × F) p).2

Tactic:
(extChartAt J p.2).right_inv <| (extChartAt J p.2).map_source (mem_extChartAt_source _)

Premises used: extChartAt, PartialEquiv.map_source, mem_extChartAt_source, PartialEquiv.right_inv, Prod.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
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
⊢ ((↑(extChartAt J p.2) : N → F) ∘ Prod.snd ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N))
      ((↑(extChartAt (I.prod J) p) : M × N → E × F) p) =
    ((↑(extChartAt (I.prod J) p) : M × N → E × F) p).2

Tactic:
exact (extChartAt J p.2).right_inv <| (extChartAt J p.2).map_source (mem_extChartAt_source _)

Premises used: extChartAt, PartialEquiv.map_source, mem_extChartAt_source, PartialEquiv.right_inv, Prod.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
n : WithTop ℕ∞
f : N → M × M'
s : Set N
x : N
hf : ContMDiffWithinAt J (I.prod I') n f s x
⊢ ContMDiffWithinAt.{u_1, u_8, u_9, u_10, u_5, u_6, u_7} J I' (M' := M') n (fun (x : N) ↦ (f x).2) s x

Tactic:
contMDiffWithinAt_snd.comp x hf (mapsTo_image f s)

Premises used: contMDiffWithinAt_snd, Set.mapsTo_image, 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
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 ℕ∞
p : M × N
⊢ ContMDiffAt (I.prod J) J n Prod.snd p

Tactic:
contMDiffWithinAt_snd

Premises used: contMDiffWithinAt_snd, 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
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)
⊢ ContMDiffOn (I.prod J) J n Prod.snd s

Tactic:
fun _ _ =>
  contMDiffWithinAt_snd

Premises used: contMDiffWithinAt_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
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 ℕ∞
⊢ ContMDiff (I.prod J) (M := M × N) J n Prod.snd

Tactic:
fun _ => contMDiffAt_snd

Premises used: ContMDiff, contMDiffAt_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
n : WithTop ℕ∞
f : N → M × M'
x : N
hf : ContMDiffAt J (I.prod I') n f x
⊢ ContMDiffAt.{u_1, u_8, u_9, u_10, u_5, u_6, u_7} J I' (M' := M') n (fun (x : N) ↦ (f x).2) x

Tactic:
contMDiffAt_snd.comp x hf

Premises used: ContMDiffAt.comp, contMDiffAt_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
n : WithTop ℕ∞
f : N → M × M'
hf : ContMDiff J (I.prod I') n f
⊢ ContMDiff.{u_1, u_8, u_9, u_10, u_5, u_6, u_7} J I' (M' := M') n fun (x : N) ↦ (f x).2

Tactic:
contMDiff_snd.comp hf

Premises used: ContMDiff.comp, contMDiff_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_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' × N'
⊢ ContMDiffWithinAt I (I'.prod J') n f s x ↔
    ContMDiffWithinAt I I' n (Prod.fst ∘ f) s x ∧ ContMDiffWithinAt I J' n (Prod.snd ∘ f) s x

Tactic:
⟨fun h => ⟨h.fst, h.snd⟩, fun h => h.1.prodMk h.2⟩

Premises used: ContMDiffWithinAt.snd, ContMDiffWithinAt.fst, ContMDiffWithinAt.prodMk, And.right, And.left, And.intro, Iff.intro