awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
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
trans₁ : s' ∩ f ⁻¹' hf.codChart (P := P).source ⊆ g ⁻¹' hf.codChart (P := P).source
⊢ (hf.domChart (P := P).restr s).source ⊆ g ⁻¹' hf.codChart (P := P).source

Tactic:
trans s' ∩ f ⁻¹' hf.codChart.source

Premises used: Manifold.LiftSourceTargetPropertyAt.codChart, PartialEquiv.source, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
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'
rt : (hf.domChart (P := P).restr s).source ⊆ f ⁻¹' hf.codChart (P := P).source
⊢ (hf.domChart (P := P).restr s).source ⊆ s' ∩ f ⁻¹' hf.codChart (P := P).source

Tactic:
apply subset_inter

Premises used: Set.subset_inter
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
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

Tactic:
simp [interior_eq_iff_isOpen.mpr hs]

Premises used: Iff.mpr, interior_eq_iff_isOpen
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
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'

Tactic:
exact Subset.trans (by simp [interior_eq_iff_isOpen.mpr hs]) hss'

Premises used: Set.Subset.trans
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
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 ⊆ hf.domChart (P := P).source

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
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 ⊆ f ⁻¹' hf.codChart (P := P).source

Tactic:
exact Subset.trans (by simp) hf.source_subset_preimage_source

Premises used: Set.Subset.trans, Manifold.LiftSourceTargetPropertyAt.source_subset_preimage_source
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
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
rw : s' ∩ g ⁻¹' hf.codChart (P := P).source ⊆ g ⁻¹' hf.codChart (P := P).source
⊢ s' ∩ f ⁻¹' hf.codChart (P := P).source ⊆ g ⁻¹' hf.codChart (P := P).source

Tactic:
rw [hfg.inter_preimage_eq]

Premises used: Set.EqOn.inter_preimage_eq
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
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' ∩ g ⁻¹' hf.codChart (P := P).source ⊆ g ⁻¹' hf.codChart (P := P).source

Tactic:
inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
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' ∩ g ⁻¹' hf.codChart (P := P).source ⊆ g ⁻¹' hf.codChart (P := P).source

Tactic:
exact inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
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

Tactic:
grind
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
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
⊢ P g (hf.domChart (P := P).restr s) (hf.codChart (P := P))

Tactic:
exact hP.congr (hfg.mono hss' |>.mono (by grind)) <| hP.mono_source hs hf.property

Premises used: Manifold.LiftSourceTargetPropertyAt.property, Manifold.IsLocalSourceTargetProperty.congr, Manifold.IsLocalSourceTargetProperty.mono_source, Set.EqOn.mono
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
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
h' : f =ᶠ[𝓝 x] g
⊢ LiftSourceTargetPropertyAt I J n f x P ↔ LiftSourceTargetPropertyAt I J n g x P

Tactic:
⟨fun hf ↦ hf.congr_of_eventuallyEq hP h', fun hg ↦ hg.congr_of_eventuallyEq hP h'.symm⟩

Premises used: Manifold.LiftSourceTargetPropertyAt.congr_of_eventuallyEq, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
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
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
⊢ IsOpen[inst_7] {x : M | LiftSourceTargetPropertyAt I J n g x P}

Tactic:
rw [isOpen_iff_forall_mem_open]

Premises used: isOpen_iff_forall_mem_open
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
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

Tactic:
⟨hx.domChart.source, fun y hy ↦ ?_, hx.domChart.open_source, hx.mem_domChart_source⟩

Premises used: Manifold.LiftSourceTargetPropertyAt.mem_domChart_source, OpenPartialHomeomorph.open_source, And.intro, Exists.intro, Manifold.LiftSourceTargetPropertyAt.domChart, PartialEquiv.source, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
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
refine :
  ∀ (y : M) (hy : y ∈ (domChart (P := P) hx).source),
    Membership.mem (γ := Set M) {x : M | LiftSourceTargetPropertyAt I J n g x P} y
⊢ ∃ t ⊆ {x : M | LiftSourceTargetPropertyAt I J n g x P}, IsOpen[inst_7] t ∧ x ∈ t

Tactic:
refine ⟨hx.domChart.source, fun y hy ↦ ?_, hx.domChart.open_source, hx.mem_domChart_source⟩
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
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
y : M
hy : y ∈ (domChart (P := P) hx).source
⊢ Membership.mem (γ := Set M) {x : M | LiftSourceTargetPropertyAt I J n g x P} y

Tactic:
⟨hx.domChart, hx.codChart, hy, hx.source_subset_preimage_source hy,
    hx.domChart_mem_maximalAtlas, hx.codChart_mem_maximalAtlas, hx.source_subset_preimage_source,
    hx.property⟩

Premises used: Manifold.LocalPresentationAt.mk, Manifold.LiftSourceTargetPropertyAt.codChart, Set.Mem, setOf, Nonempty.intro, Manifold.LiftSourceTargetPropertyAt, Manifold.LiftSourceTargetPropertyAt.property, Manifold.LiftSourceTargetPropertyAt.domChart_mem_maximalAtlas, Manifold.LiftSourceTargetPropertyAt.domChart, Manifold.LiftSourceTargetPropertyAt.codChart_mem_maximalAtlas, Manifold.LiftSourceTargetPropertyAt.source_subset_preimage_source
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
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
y : M
hy : y ∈ (domChart (P := P) hx).source
⊢ Membership.mem (γ := Set M) {x : M | LiftSourceTargetPropertyAt I J n g x P} y

Tactic:
exact ⟨hx.domChart, hx.codChart, hy, hx.source_subset_preimage_source hy,
    hx.domChart_mem_maximalAtlas, hx.codChart_mem_maximalAtlas, hx.source_subset_preimage_source,
    hx.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 ψ₂)
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
property :
  R (Prod.map f g) (hf.domChart (P := P).prod (hg.domChart (P := Q))) (hf.codChart (P := P).prod (hg.codChart (P := Q)))
⊢ LiftSourceTargetPropertyAt (I.prod I') (J.prod J') n (Prod.map f g) (x, x') R

Tactic:
use hf.domChart.prod hg.domChart, hf.codChart.prod hg.codChart

Premises used: Manifold.LiftSourceTargetPropertyAt.codChart, Manifold.LiftSourceTargetPropertyAt.domChart, OpenPartialHomeomorph.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 ψ₂)
⊢ (x, x') ∈ (hf.domChart (P := P).prod (hg.domChart (P := Q))).source

Tactic:
simp [hf.mem_domChart_source, hg.mem_domChart_source]

Premises used: Manifold.LiftSourceTargetPropertyAt.mem_domChart_source