awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Goal:
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
H : Type u_6
H' : Type u_7
G : Type u_8
G' : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
inst_9 : TopologicalSpace H
inst_10 : TopologicalSpace H'
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
M : Type u_10
M' : Type u_11
N : Type u_12
N' : Type u_13
inst_13 : TopologicalSpace M
inst_14 : ChartedSpace H M
inst_15 : TopologicalSpace M'
inst_16 : ChartedSpace H' M'
inst_17 : TopologicalSpace N
inst_18 : ChartedSpace G N
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
inst_21 : IsManifold I n M
inst_22 : IsManifold I' n M'
inst_23 : IsManifold J n N
inst_24 : IsManifold J' n N'
Q : (M' → N') → OpenPartialHomeomorph M' H' → OpenPartialHomeomorph N' G' → Prop
R : (M × M' → N × N') → OpenPartialHomeomorph (M × M') (H × H') → OpenPartialHomeomorph (N × N') (G × G') → Prop
hf : LiftSourceTargetPropertyAt I J n f x P
g : M' → N'
x' : M'
hg : LiftSourceTargetPropertyAt I' J' n g x' Q
h :
  ∀ {f : M → N} {φ₁ : OpenPartialHomeomorph M H} {ψ₁ : OpenPartialHomeomorph N G} {g : M' → N'}
    {φ₂ : OpenPartialHomeomorph M' H'} {ψ₂ : OpenPartialHomeomorph N' G'},
    P f φ₁ ψ₁ → Q g φ₂ ψ₂ → R (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂)
⊢ Prod.map f g (x, x') ∈ (hf.codChart (P := P).prod (hg.codChart (P := Q))).source

Tactic:
simp [mem_codChart_source hf, mem_codChart_source hg]

Premises used: Manifold.LiftSourceTargetPropertyAt.mem_codChart_source
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Goal:
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
H : Type u_6
H' : Type u_7
G : Type u_8
G' : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
inst_9 : TopologicalSpace H
inst_10 : TopologicalSpace H'
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
M : Type u_10
M' : Type u_11
N : Type u_12
N' : Type u_13
inst_13 : TopologicalSpace M
inst_14 : ChartedSpace H M
inst_15 : TopologicalSpace M'
inst_16 : ChartedSpace H' M'
inst_17 : TopologicalSpace N
inst_18 : ChartedSpace G N
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
inst_21 : IsManifold I n M
inst_22 : IsManifold I' n M'
inst_23 : IsManifold J n N
inst_24 : IsManifold J' n N'
Q : (M' → N') → OpenPartialHomeomorph M' H' → OpenPartialHomeomorph N' G' → Prop
R : (M × M' → N × N') → OpenPartialHomeomorph (M × M') (H × H') → OpenPartialHomeomorph (N × N') (G × G') → Prop
hf : LiftSourceTargetPropertyAt I J n f x P
g : M' → N'
x' : M'
hg : LiftSourceTargetPropertyAt I' J' n g x' Q
h :
  ∀ {f : M → N} {φ₁ : OpenPartialHomeomorph M H} {ψ₁ : OpenPartialHomeomorph N G} {g : M' → N'}
    {φ₂ : OpenPartialHomeomorph M' H'} {ψ₂ : OpenPartialHomeomorph N' G'},
    P f φ₁ ψ₁ → Q g φ₂ ψ₂ → R (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (M × M') (ModelProd H H')))
    (IsManifold.maximalAtlas (I.prod I') n (M × M')) (hf.domChart (P := P).prod (hg.domChart (P := Q)))

Tactic:
IsManifold.mem_maximalAtlas_prod
      (domChart_mem_maximalAtlas hf) (domChart_mem_maximalAtlas hg)

Premises used: Set.Mem, Manifold.LiftSourceTargetPropertyAt.domChart_mem_maximalAtlas, IsManifold.mem_maximalAtlas_prod
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Goal:
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
H : Type u_6
H' : Type u_7
G : Type u_8
G' : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
inst_9 : TopologicalSpace H
inst_10 : TopologicalSpace H'
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
M : Type u_10
M' : Type u_11
N : Type u_12
N' : Type u_13
inst_13 : TopologicalSpace M
inst_14 : ChartedSpace H M
inst_15 : TopologicalSpace M'
inst_16 : ChartedSpace H' M'
inst_17 : TopologicalSpace N
inst_18 : ChartedSpace G N
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
inst_21 : IsManifold I n M
inst_22 : IsManifold I' n M'
inst_23 : IsManifold J n N
inst_24 : IsManifold J' n N'
Q : (M' → N') → OpenPartialHomeomorph M' H' → OpenPartialHomeomorph N' G' → Prop
R : (M × M' → N × N') → OpenPartialHomeomorph (M × M') (H × H') → OpenPartialHomeomorph (N × N') (G × G') → Prop
hf : LiftSourceTargetPropertyAt I J n f x P
g : M' → N'
x' : M'
hg : LiftSourceTargetPropertyAt I' J' n g x' Q
h :
  ∀ {f : M → N} {φ₁ : OpenPartialHomeomorph M H} {ψ₁ : OpenPartialHomeomorph N G} {g : M' → N'}
    {φ₂ : OpenPartialHomeomorph M' H'} {ψ₂ : OpenPartialHomeomorph N' G'},
    P f φ₁ ψ₁ → Q g φ₂ ψ₂ → R (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (M × M') (ModelProd H H')))
    (IsManifold.maximalAtlas (I.prod I') n (M × M')) (hf.domChart (P := P).prod (hg.domChart (P := Q)))

Tactic:
exact IsManifold.mem_maximalAtlas_prod
      (domChart_mem_maximalAtlas hf) (domChart_mem_maximalAtlas hg)

Premises used: Manifold.LiftSourceTargetPropertyAt.domChart_mem_maximalAtlas, IsManifold.mem_maximalAtlas_prod
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Goal:
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
H : Type u_6
H' : Type u_7
G : Type u_8
G' : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
inst_9 : TopologicalSpace H
inst_10 : TopologicalSpace H'
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
M : Type u_10
M' : Type u_11
N : Type u_12
N' : Type u_13
inst_13 : TopologicalSpace M
inst_14 : ChartedSpace H M
inst_15 : TopologicalSpace M'
inst_16 : ChartedSpace H' M'
inst_17 : TopologicalSpace N
inst_18 : ChartedSpace G N
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
inst_21 : IsManifold I n M
inst_22 : IsManifold I' n M'
inst_23 : IsManifold J n N
inst_24 : IsManifold J' n N'
Q : (M' → N') → OpenPartialHomeomorph M' H' → OpenPartialHomeomorph N' G' → Prop
R : (M × M' → N × N') → OpenPartialHomeomorph (M × M') (H × H') → OpenPartialHomeomorph (N × N') (G × G') → Prop
hf : LiftSourceTargetPropertyAt I J n f x P
g : M' → N'
x' : M'
hg : LiftSourceTargetPropertyAt I' J' n g x' Q
h :
  ∀ {f : M → N} {φ₁ : OpenPartialHomeomorph M H} {ψ₁ : OpenPartialHomeomorph N G} {g : M' → N'}
    {φ₂ : OpenPartialHomeomorph M' H'} {ψ₂ : OpenPartialHomeomorph N' G'},
    P f φ₁ ψ₁ → Q g φ₂ ψ₂ → R (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (N × N') (ModelProd G G')))
    (IsManifold.maximalAtlas (J.prod J') n (N × N')) (hf.codChart (P := P).prod (hg.codChart (P := Q)))

Tactic:
apply IsManifold.mem_maximalAtlas_prod
      (codChart_mem_maximalAtlas hf) (codChart_mem_maximalAtlas hg)

Premises used: IsManifold.mem_maximalAtlas_prod, Manifold.LiftSourceTargetPropertyAt.codChart_mem_maximalAtlas
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Goal:
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
H : Type u_6
H' : Type u_7
G : Type u_8
G' : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
inst_9 : TopologicalSpace H
inst_10 : TopologicalSpace H'
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
M : Type u_10
M' : Type u_11
N : Type u_12
N' : Type u_13
inst_13 : TopologicalSpace M
inst_14 : ChartedSpace H M
inst_15 : TopologicalSpace M'
inst_16 : ChartedSpace H' M'
inst_17 : TopologicalSpace N
inst_18 : ChartedSpace G N
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
inst_21 : IsManifold I n M
inst_22 : IsManifold I' n M'
inst_23 : IsManifold J n N
inst_24 : IsManifold J' n N'
Q : (M' → N') → OpenPartialHomeomorph M' H' → OpenPartialHomeomorph N' G' → Prop
R : (M × M' → N × N') → OpenPartialHomeomorph (M × M') (H × H') → OpenPartialHomeomorph (N × N') (G × G') → Prop
hf : LiftSourceTargetPropertyAt I J n f x P
g : M' → N'
x' : M'
hg : LiftSourceTargetPropertyAt I' J' n g x' Q
h :
  ∀ {f : M → N} {φ₁ : OpenPartialHomeomorph M H} {ψ₁ : OpenPartialHomeomorph N G} {g : M' → N'}
    {φ₂ : OpenPartialHomeomorph M' H'} {ψ₂ : OpenPartialHomeomorph N' G'},
    P f φ₁ ψ₁ → Q g φ₂ ψ₂ → R (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂)
source_subset_preimage_source :
  hf.domChart (P := P).source ×ˢ hg.domChart (P := Q).source ⊆
    (f ⁻¹' hf.codChart (P := P).source) ×ˢ (g ⁻¹' hg.codChart (P := Q).source)
⊢ (hf.domChart (P := P).prod (hg.domChart (P := Q))).source ⊆
    Prod.map f g ⁻¹' (hf.codChart (P := P).prod (hg.codChart (P := Q))).source

Tactic:
simp only [OpenPartialHomeomorph.prod_toPartialEquiv, PartialEquiv.prod_source,
      preimage_prod_map_prod]

Premises used: PartialEquiv.prod_source, OpenPartialHomeomorph.prod_toPartialEquiv, Set.preimage_prod_map_prod
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Goal:
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
H : Type u_6
H' : Type u_7
G : Type u_8
G' : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
inst_9 : TopologicalSpace H
inst_10 : TopologicalSpace H'
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
M : Type u_10
M' : Type u_11
N : Type u_12
N' : Type u_13
inst_13 : TopologicalSpace M
inst_14 : ChartedSpace H M
inst_15 : TopologicalSpace M'
inst_16 : ChartedSpace H' M'
inst_17 : TopologicalSpace N
inst_18 : ChartedSpace G N
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
inst_21 : IsManifold I n M
inst_22 : IsManifold I' n M'
inst_23 : IsManifold J n N
inst_24 : IsManifold J' n N'
Q : (M' → N') → OpenPartialHomeomorph M' H' → OpenPartialHomeomorph N' G' → Prop
R : (M × M' → N × N') → OpenPartialHomeomorph (M × M') (H × H') → OpenPartialHomeomorph (N × N') (G × G') → Prop
hf : LiftSourceTargetPropertyAt I J n f x P
g : M' → N'
x' : M'
hg : LiftSourceTargetPropertyAt I' J' n g x' Q
h :
  ∀ {f : M → N} {φ₁ : OpenPartialHomeomorph M H} {ψ₁ : OpenPartialHomeomorph N G} {g : M' → N'}
    {φ₂ : OpenPartialHomeomorph M' H'} {ψ₂ : OpenPartialHomeomorph N' G'},
    P f φ₁ ψ₁ → Q g φ₂ ψ₂ → R (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂)
⊢ hf.domChart (P := P).source ×ˢ hg.domChart (P := Q).source ⊆
    (f ⁻¹' hf.codChart (P := P).source) ×ˢ (g ⁻¹' hg.codChart (P := Q).source)

Tactic:
prod_mono hf.source_subset_preimage_source hg.source_subset_preimage_source

Premises used: Set.prod_mono, Manifold.LiftSourceTargetPropertyAt.source_subset_preimage_source
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Goal:
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
H : Type u_6
H' : Type u_7
G : Type u_8
G' : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
inst_9 : TopologicalSpace H
inst_10 : TopologicalSpace H'
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
M : Type u_10
M' : Type u_11
N : Type u_12
N' : Type u_13
inst_13 : TopologicalSpace M
inst_14 : ChartedSpace H M
inst_15 : TopologicalSpace M'
inst_16 : ChartedSpace H' M'
inst_17 : TopologicalSpace N
inst_18 : ChartedSpace G N
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
inst_21 : IsManifold I n M
inst_22 : IsManifold I' n M'
inst_23 : IsManifold J n N
inst_24 : IsManifold J' n N'
Q : (M' → N') → OpenPartialHomeomorph M' H' → OpenPartialHomeomorph N' G' → Prop
R : (M × M' → N × N') → OpenPartialHomeomorph (M × M') (H × H') → OpenPartialHomeomorph (N × N') (G × G') → Prop
hf : LiftSourceTargetPropertyAt I J n f x P
g : M' → N'
x' : M'
hg : LiftSourceTargetPropertyAt I' J' n g x' Q
h :
  ∀ {f : M → N} {φ₁ : OpenPartialHomeomorph M H} {ψ₁ : OpenPartialHomeomorph N G} {g : M' → N'}
    {φ₂ : OpenPartialHomeomorph M' H'} {ψ₂ : OpenPartialHomeomorph N' G'},
    P f φ₁ ψ₁ → Q g φ₂ ψ₂ → R (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂)
⊢ hf.domChart (P := P).source ×ˢ hg.domChart (P := Q).source ⊆
    (f ⁻¹' hf.codChart (P := P).source) ×ˢ (g ⁻¹' hg.codChart (P := Q).source)

Tactic:
exact prod_mono hf.source_subset_preimage_source hg.source_subset_preimage_source

Premises used: Set.prod_mono, Manifold.LiftSourceTargetPropertyAt.source_subset_preimage_source
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Goal:
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
H : Type u_6
H' : Type u_7
G : Type u_8
G' : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
inst_9 : TopologicalSpace H
inst_10 : TopologicalSpace H'
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
M : Type u_10
M' : Type u_11
N : Type u_12
N' : Type u_13
inst_13 : TopologicalSpace M
inst_14 : ChartedSpace H M
inst_15 : TopologicalSpace M'
inst_16 : ChartedSpace H' M'
inst_17 : TopologicalSpace N
inst_18 : ChartedSpace G N
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
inst_21 : IsManifold I n M
inst_22 : IsManifold I' n M'
inst_23 : IsManifold J n N
inst_24 : IsManifold J' n N'
Q : (M' → N') → OpenPartialHomeomorph M' H' → OpenPartialHomeomorph N' G' → Prop
R : (M × M' → N × N') → OpenPartialHomeomorph (M × M') (H × H') → OpenPartialHomeomorph (N × N') (G × G') → Prop
hf : LiftSourceTargetPropertyAt I J n f x P
g : M' → N'
x' : M'
hg : LiftSourceTargetPropertyAt I' J' n g x' Q
h :
  ∀ {f : M → N} {φ₁ : OpenPartialHomeomorph M H} {ψ₁ : OpenPartialHomeomorph N G} {g : M' → N'}
    {φ₂ : OpenPartialHomeomorph M' H'} {ψ₂ : OpenPartialHomeomorph N' G'},
    P f φ₁ ψ₁ → Q g φ₂ ψ₂ → R (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂)
⊢ R (Prod.map f g) (hf.domChart (P := P).prod (hg.domChart (P := Q))) (hf.codChart (P := P).prod (hg.codChart (P := Q)))

Tactic:
h hf.property hg.property

Premises used: Manifold.LiftSourceTargetPropertyAt.property
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Goal:
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
H : Type u_6
H' : Type u_7
G : Type u_8
G' : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
inst_9 : TopologicalSpace H
inst_10 : TopologicalSpace H'
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
M : Type u_10
M' : Type u_11
N : Type u_12
N' : Type u_13
inst_13 : TopologicalSpace M
inst_14 : ChartedSpace H M
inst_15 : TopologicalSpace M'
inst_16 : ChartedSpace H' M'
inst_17 : TopologicalSpace N
inst_18 : ChartedSpace G N
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
inst_21 : IsManifold I n M
inst_22 : IsManifold I' n M'
inst_23 : IsManifold J n N
inst_24 : IsManifold J' n N'
Q : (M' → N') → OpenPartialHomeomorph M' H' → OpenPartialHomeomorph N' G' → Prop
R : (M × M' → N × N') → OpenPartialHomeomorph (M × M') (H × H') → OpenPartialHomeomorph (N × N') (G × G') → Prop
hf : LiftSourceTargetPropertyAt I J n f x P
g : M' → N'
x' : M'
hg : LiftSourceTargetPropertyAt I' J' n g x' Q
h :
  ∀ {f : M → N} {φ₁ : OpenPartialHomeomorph M H} {ψ₁ : OpenPartialHomeomorph N G} {g : M' → N'}
    {φ₂ : OpenPartialHomeomorph M' H'} {ψ₂ : OpenPartialHomeomorph N' G'},
    P f φ₁ ψ₁ → Q g φ₂ ψ₂ → R (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂)
⊢ R (Prod.map f g) (hf.domChart (P := P).prod (hg.domChart (P := Q))) (hf.codChart (P := P).prod (hg.codChart (P := Q)))

Tactic:
exact h hf.property hg.property

Premises used: Manifold.LiftSourceTargetPropertyAt.property
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
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
x : H
⊢ HasMFDerivAt I 𝓘(𝕜, E) (↑I : H → E) x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))

Tactic:
⟨I.continuousAt, (hasFDerivWithinAt_id _ _).congr' I.rightInvOn (mem_range_self _)⟩

Premises used: Set.mem_range_self, HasMFDerivAt, ModelWithCorners.continuousAt, And.intro, HasFDerivWithinAt.congr', ModelWithCorners.rightInvOn, hasFDerivWithinAt_id
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
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
s : Set H
x : H
⊢ HasMFDerivWithinAt I 𝓘(𝕜, E) (↑I : H → E) s x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))

Tactic:
I.hasMFDerivAt.hasMFDerivWithinAt

Premises used: ModelWithCorners.hasMFDerivAt, HasMFDerivAt.hasMFDerivWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
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
s : Set H
x : H
⊢ MDiffAt[s] (↑I : H → E) x

Tactic:
I.hasMFDerivWithinAt.mdifferentiableWithinAt

Premises used: HasMFDerivWithinAt.mdifferentiableWithinAt, ModelWithCorners.hasMFDerivWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
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
x : H
⊢ MDiffAt (↑I : H → E) x

Tactic:
I.hasMFDerivAt.mdifferentiableAt

Premises used: ModelWithCorners.hasMFDerivAt, HasMFDerivAt.mdifferentiableAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
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
s : Set H
⊢ MDiff[s] (↑I : H → E)

Tactic:
fun _ _ =>
  I.mdifferentiableWithinAt

Premises used: MDifferentiableOn, ModelWithCorners.mdifferentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
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
⊢ MDiff (↑I : H → E)

Tactic:
fun _ => I.mdifferentiableAt

Premises used: ModelWithCorners.mdifferentiableAt, MDifferentiable
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
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
x : E
hx : x ∈ range (↑I : H → E)
⊢ HasMFDerivWithinAt 𝓘(𝕜, E) I (↑I.symm : E → H) (range (↑I : H → E)) x
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) x))

Tactic:
⟨I.continuousWithinAt_symm,
    (hasFDerivWithinAt_id _ _).congr' (fun _y hy => I.rightInvOn hy.1) ⟨hx, mem_range_self _⟩⟩

Premises used: Set.mem_range_self, ModelWithCorners.continuousWithinAt_symm, And.left, And.intro, HasFDerivWithinAt.congr', ModelWithCorners.rightInvOn, HasMFDerivWithinAt, hasFDerivWithinAt_id
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
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
⊢ MDiff[range (↑I : H → E)] (↑I.symm : E → H)

Tactic:
fun _x hx =>
  (I.hasMFDerivWithinAt_symm hx).mdifferentiableWithinAt

Premises used: HasMFDerivWithinAt.mdifferentiableWithinAt, MDifferentiableOn, ModelWithCorners.hasMFDerivWithinAt_symm
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
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
z : E
hz : z ∈ range (↑I : H → E)
⊢ MDiffAt[range (↑I : H → E)] (↑I.symm : E → H) z

Tactic:
I.mdifferentiableOn_symm z hz

Premises used: ModelWithCorners.mdifferentiableOn_symm
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : M
hx : x ∈ e.source
rw :
  ContinuousAt (↑e : M → H) x ∧
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e : M → H)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
⊢ MDiffAt (↑e : M → H) x

Tactic:
rw [mdifferentiableAt_iff]

Premises used: mdifferentiableAt_iff