awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace H
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
s : Set M
hss' : s ⊆ s'
hs : IsOpen[inst_7] s
hxs : x ∈ s
refine_1 : x ∈ (hf.domChart (P := P).restr s).source
refine_2 : g x ∈ hf.codChart (P := P).source
refine_3 :
  Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) (hf.domChart (P := P).restr s)
⊢ LiftSourceTargetPropertyAt I J n g x P
have refine_4 : (hf.domChart (P := P).restr s).source ⊆ g ⁻¹' hf.codChart (P := P).source
Tactic: refine ⟨hf.domChart.restr s, hf.codChart, ?_, ?_, ?_, hf.codChart_mem_maximalAtlas, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace H
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
s : Set M
hss' : s ⊆ s'
hs : IsOpen[inst_7] s
hxs : x ∈ s
refine_1 : x ∈ (hf.domChart (P := P).restr s).source
refine_2 : g x ∈ hf.codChart (P := P).source
refine_3 :
  Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) (hf.domChart (P := P).restr s)
refine_4 : (hf.domChart (P := P).restr s).source ⊆ g ⁻¹' hf.codChart (P := P).source
⊢ LiftSourceTargetPropertyAt I J n g x P
have refine_5 : P g (hf.domChart (P := P).restr s) (hf.codChart (P := P))
Tactic: refine ⟨hf.domChart.restr s, hf.codChart, ?_, ?_, ?_, hf.codChart_mem_maximalAtlas, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace H
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
s : Set M
hss' : s ⊆ s'
hs : IsOpen[inst_7] s
hxs : x ∈ s
⊢ (hf.domChart (P := P).restr s).source ⊆ g ⁻¹' hf.codChart (P := P).source
have trans : (hf.domChart (P := P).restr s).source ⊆ s' ∩ f ⁻¹' hf.codChart (P := P).source
Tactic: trans s' ∩ f ⁻¹' hf.codChart.source
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace H
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
s : Set M
hss' : s ⊆ s'
hs : IsOpen[inst_7] s
hxs : x ∈ s
trans : (hf.domChart (P := P).restr s).source ⊆ s' ∩ f ⁻¹' hf.codChart (P := P).source
⊢ (hf.domChart (P := P).restr s).source ⊆ g ⁻¹' hf.codChart (P := P).source
have trans₁ : s' ∩ f ⁻¹' hf.codChart (P := P).source ⊆ g ⁻¹' hf.codChart (P := P).source
Tactic: trans s' ∩ f ⁻¹' hf.codChart.source
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace H
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
s : Set M
hss' : s ⊆ s'
hs : IsOpen[inst_7] s
hxs : x ∈ s
⊢ (hf.domChart (P := P).restr s).source ⊆ s' ∩ f ⁻¹' hf.codChart (P := P).source
have rs : (hf.domChart (P := P).restr s).source ⊆ s'
Tactic: apply subset_inter
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace H
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
s : Set M
hss' : s ⊆ s'
hs : IsOpen[inst_7] s
hxs : x ∈ s
rs : (hf.domChart (P := P).restr s).source ⊆ s'
⊢ (hf.domChart (P := P).restr s).source ⊆ s' ∩ f ⁻¹' hf.codChart (P := P).source
have rt : (hf.domChart (P := P).restr s).source ⊆ f ⁻¹' hf.codChart (P := P).source
Tactic: apply subset_inter
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace H
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
s : Set M
hss' : s ⊆ s'
hs : IsOpen[inst_7] s
hxs : x ∈ s
⊢ s' ∩ f ⁻¹' hf.codChart (P := P).source ⊆ g ⁻¹' hf.codChart (P := P).source
have rw : s' ∩ g ⁻¹' hf.codChart (P := P).source ⊆ g ⁻¹' hf.codChart (P := P).source
Tactic: rw [hfg.inter_preimage_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace H
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
g : M → N
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
⊢ IsOpen[inst_7] {x : M | LiftSourceTargetPropertyAt I J n g x P}
have rw : ∀ (x : M),
  Membership.mem (γ := Set M) {x : M | LiftSourceTargetPropertyAt I J n g x P} x →
    ∃ t ⊆ {x : M | LiftSourceTargetPropertyAt I J n g x P}, IsOpen[inst_7] t ∧ x ∈ t
Tactic: rw [isOpen_iff_forall_mem_open]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace H
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
g : M → N
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
x : M
hx : Membership.mem (γ := Set M) {x : M | LiftSourceTargetPropertyAt I J n g x P} x
⊢ ∃ t ⊆ {x : M | LiftSourceTargetPropertyAt I J n g x P}, IsOpen[inst_7] t ∧ x ∈ t
have refine : ∀ (y : M) (hy : y ∈ (domChart (P := P) hx).source),
  Membership.mem (γ := Set M) {x : M | LiftSourceTargetPropertyAt I J n g x P} y
Tactic: refine ⟨hx.domChart.source, fun y hy ↦ ?_, hx.domChart.open_source, hx.mem_domChart_source⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
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 ψ₂)
⊢ LiftSourceTargetPropertyAt (I.prod I') (J.prod J') n (Prod.map f g) (x, x') R
have mem_domChart_source : (x, x') ∈ (hf.domChart (P := P).prod (hg.domChart (P := Q))).source
Tactic: use hf.domChart.prod hg.domChart, hf.codChart.prod hg.codChart
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
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 ψ₂)
mem_domChart_source : (x, x') ∈ (hf.domChart (P := P).prod (hg.domChart (P := Q))).source
⊢ LiftSourceTargetPropertyAt (I.prod I') (J.prod J') n (Prod.map f g) (x, x') R
have mem_codChart_source : Prod.map f g (x, x') ∈ (hf.codChart (P := P).prod (hg.codChart (P := Q))).source
Tactic: use hf.domChart.prod hg.domChart, hf.codChart.prod hg.codChart
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
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 ψ₂)
mem_domChart_source : (x, x') ∈ (hf.domChart (P := P).prod (hg.domChart (P := Q))).source
mem_codChart_source : Prod.map f g (x, x') ∈ (hf.codChart (P := P).prod (hg.codChart (P := Q))).source
⊢ LiftSourceTargetPropertyAt (I.prod I') (J.prod J') n (Prod.map f g) (x, x') R
have domChart_mem_maximalAtlas : 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: use hf.domChart.prod hg.domChart, hf.codChart.prod hg.codChart
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
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 ψ₂)
mem_domChart_source : (x, x') ∈ (hf.domChart (P := P).prod (hg.domChart (P := Q))).source
mem_codChart_source : Prod.map f g (x, x') ∈ (hf.codChart (P := P).prod (hg.codChart (P := Q))).source
domChart_mem_maximalAtlas :
  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)))
⊢ LiftSourceTargetPropertyAt (I.prod I') (J.prod J') n (Prod.map f g) (x, x') R
have codChart_mem_maximalAtlas : 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: use hf.domChart.prod hg.domChart, hf.codChart.prod hg.codChart
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
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 ψ₂)
mem_domChart_source : (x, x') ∈ (hf.domChart (P := P).prod (hg.domChart (P := Q))).source
mem_codChart_source : Prod.map f g (x, x') ∈ (hf.codChart (P := P).prod (hg.codChart (P := Q))).source
domChart_mem_maximalAtlas :
  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)))
codChart_mem_maximalAtlas :
  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)))
⊢ LiftSourceTargetPropertyAt (I.prod I') (J.prod J') n (Prod.map f g) (x, x') R
have source_subset_preimage_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: use hf.domChart.prod hg.domChart, hf.codChart.prod hg.codChart
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
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 ψ₂)
mem_domChart_source : (x, x') ∈ (hf.domChart (P := P).prod (hg.domChart (P := Q))).source
mem_codChart_source : Prod.map f g (x, x') ∈ (hf.codChart (P := P).prod (hg.codChart (P := Q))).source
domChart_mem_maximalAtlas :
  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)))
codChart_mem_maximalAtlas :
  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)))
source_subset_preimage_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
⊢ LiftSourceTargetPropertyAt (I.prod I') (J.prod J') n (Prod.map f g) (x, x') R
have property : R (Prod.map f g) (hf.domChart (P := P).prod (hg.domChart (P := Q))) (hf.codChart (P := P).prod (hg.codChart (P := Q)))
Tactic: use hf.domChart.prod hg.domChart, hf.codChart.prod hg.codChart