awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hs : IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
refine_2 refine_2₁ refine_2₂ :
  ∀ ⦃my_y : H₁⦄,
    my_y ∈ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source →
      my_y ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source
refine_2₃ refine_2₄ :
  ∀ ⦃my_y : H₁⦄,
    (my_y ∈ f.target ∧
          (↑f.symm : H₁ → H₂) my_y ∈ e.target ∧
            (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) my_y) ∈ e'.source ∧
              (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) my_y)) ∈ f'.source) ∧
        my_y ∈ φ.source →
      my_y ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source
⊢ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source ⊆ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source

Tactic:
mfld_set_tac
-- 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 : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
h : LiftSourceTargetPropertyAt I J n f x P
⊢ x ∈ h.domChart (P := P).source

Tactic:
h.localPresentationAt.mem_domChart_source

Premises used: Set.Mem, Manifold.LocalPresentationAt.mem_domChart_source, Manifold.LiftSourceTargetPropertyAt.localPresentationAt
-- 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 : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
h : LiftSourceTargetPropertyAt I J n f x P
⊢ f x ∈ h.codChart (P := P).source

Tactic:
h.localPresentationAt.mem_codChart_source

Premises used: Manifold.LocalPresentationAt.mem_codChart_source, Set.Mem, Manifold.LiftSourceTargetPropertyAt.localPresentationAt
-- 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 : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
h : LiftSourceTargetPropertyAt I J n f x P
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) (h.domChart (P := P))

Tactic:
h.localPresentationAt.domChart_mem_maximalAtlas

Premises used: Set.Mem, Manifold.LocalPresentationAt.domChart_mem_maximalAtlas, Manifold.LiftSourceTargetPropertyAt.domChart, Manifold.LiftSourceTargetPropertyAt.localPresentationAt
-- 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 : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
h : LiftSourceTargetPropertyAt I J n f x P
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (IsManifold.maximalAtlas J n N) (h.codChart (P := P))

Tactic:
h.localPresentationAt.codChart_mem_maximalAtlas

Premises used: Manifold.LiftSourceTargetPropertyAt.codChart, Set.Mem, Manifold.LiftSourceTargetPropertyAt.localPresentationAt, Manifold.LocalPresentationAt.codChart_mem_maximalAtlas
-- 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 : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
h : LiftSourceTargetPropertyAt I J n f x P
⊢ h.domChart (P := P).source ⊆ f ⁻¹' h.codChart (P := P).source

Tactic:
h.localPresentationAt.source_subset_preimage_source

Premises used: Manifold.LocalPresentationAt.source_subset_preimage_source, Manifold.LiftSourceTargetPropertyAt.localPresentationAt
-- 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 : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
h : LiftSourceTargetPropertyAt I J n f x P
⊢ P f (h.domChart (P := P)) (h.codChart (P := P))

Tactic:
h.localPresentationAt.property

Premises used: Manifold.LiftSourceTargetPropertyAt.codChart, Manifold.LocalPresentationAt.property, Manifold.LiftSourceTargetPropertyAt.domChart, Manifold.LiftSourceTargetPropertyAt.localPresentationAt
-- Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Goal:
H : Type u_6
G : Type u_8
inst : TopologicalSpace H
inst_1 : TopologicalSpace G
M : Type u_10
N : Type u_12
inst_2 : TopologicalSpace M
inst_3 : TopologicalSpace N
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
f g : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hfg : EqOn f g φ.source
⊢ P f φ ψ ↔ P g φ ψ

Tactic:
⟨hP.congr hfg, hP.congr hfg.symm⟩

Premises used: Manifold.IsLocalSourceTargetProperty.congr, Iff.intro, Set.EqOn.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 : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hf : ContinuousAt f x
hP : IsLocalSourceTargetProperty P
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) domChart
hcodChart : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (IsManifold.maximalAtlas J n N) codChart
hfP : P f domChart codChart
obtain :
  ∀ (s : Set M) (hs : s ⊆ f ⁻¹' codChart.source) (hsopen : IsOpen[inst_7] s) (hxs : x ∈ s),
    LiftSourceTargetPropertyAt I J n f x P
⊢ LiftSourceTargetPropertyAt I J n f x P

Tactic:
obtain ⟨s, hs, hsopen, hxs⟩ := mem_nhds_iff.mp <|
    hf.preimage_mem_nhds (codChart.open_source.mem_nhds hfx)

Premises used: OpenPartialHomeomorph.open_source, mem_nhds_iff, ContinuousAt.preimage_mem_nhds, IsOpen.mem_nhds, Iff.mp
-- 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 : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hf : ContinuousAt f x
hP : IsLocalSourceTargetProperty P
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) domChart
hcodChart : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (IsManifold.maximalAtlas J n N) codChart
hfP : P f domChart codChart
s : Set M
hs : s ⊆ f ⁻¹' codChart.source
hsopen : IsOpen[inst_7] s
hxs : x ∈ s
⊢ x ∈ (domChart.restr s).source

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 : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hf : ContinuousAt f x
hP : IsLocalSourceTargetProperty P
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) domChart
hcodChart : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (IsManifold.maximalAtlas J n N) codChart
hfP : P f domChart codChart
s : Set M
hs : s ⊆ f ⁻¹' codChart.source
hsopen : IsOpen[inst_7] s
hxs : x ∈ s
⊢ (domChart.restr s).source ⊆ f ⁻¹' codChart.source

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 : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hf : ContinuousAt f x
hP : IsLocalSourceTargetProperty P
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) domChart
hcodChart : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (IsManifold.maximalAtlas J n N) codChart
hfP : P f domChart codChart
s : Set M
hs : s ⊆ f ⁻¹' codChart.source
hsopen : IsOpen[inst_7] s
hxs : x ∈ s
⊢ LiftSourceTargetPropertyAt I J n f x P

Tactic:
exact ⟨domChart.restr s, codChart, by grind, hfx,
    restr_mem_maximalAtlas (contDiffGroupoid n I) hdomChart hsopen, hcodChart, by grind,
    hP.mono_source hsopen hfP⟩
-- 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
obtain : ∀ (s' : Set M) (hxs' : s' ∈ 𝓝 x) (hfg : EqOn f g s'), LiftSourceTargetPropertyAt I J n g x P
⊢ LiftSourceTargetPropertyAt I J n g x P

Tactic:
obtain ⟨s', hxs', hfg⟩ := h'.exists_mem

Premises used: Filter.EventuallyEq.exists_mem
-- 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'
obtain : ∀ (s : Set M) (hss' : s ⊆ s') (hs : IsOpen[inst_7] s) (hxs : x ∈ s), LiftSourceTargetPropertyAt I J n g x P
⊢ LiftSourceTargetPropertyAt I J n g x P

Tactic:
obtain ⟨s, hss', hs, hxs⟩ := mem_nhds_iff.mp hxs'

Premises used: mem_nhds_iff, Iff.mp
-- 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
⊢ LiftSourceTargetPropertyAt I J n g x P

Tactic:
⟨hf.domChart.restr s, hf.codChart, ?_, ?_, ?_, hf.codChart_mem_maximalAtlas, ?_, ?_⟩

Premises used: Manifold.LocalPresentationAt.mk, Manifold.LiftSourceTargetPropertyAt.codChart, Nonempty.intro, Manifold.LiftSourceTargetPropertyAt, Manifold.LiftSourceTargetPropertyAt.domChart, Manifold.LiftSourceTargetPropertyAt.codChart_mem_maximalAtlas, OpenPartialHomeomorph.restr
-- 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
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
refine_5 : P g (hf.domChart (P := P).restr s) (hf.codChart (P := P))
⊢ LiftSourceTargetPropertyAt I J n g x P

Tactic:
refine ⟨hf.domChart.restr s, hf.codChart, ?_, ?_, ?_, hf.codChart_mem_maximalAtlas, ?_, ?_⟩
-- 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 rwa rwa₁ rwa₂ rwa₃ : x ∈ s
⊢ x ∈ interior s

Tactic:
rwa [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
⊢ x ∈ (hf.domChart (P := P).restr s).source

Tactic:
simpa using ⟨mem_domChart_source hf, by rwa [interior_eq_iff_isOpen.mpr hs]⟩
-- 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
⊢ g x ∈ hf.codChart (P := P).source

Tactic:
hfg (mem_of_mem_nhds hxs') ▸ mem_codChart_source hf

Premises used: Eq.rec, mem_of_mem_nhds, Manifold.LiftSourceTargetPropertyAt.mem_codChart_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
⊢ g x ∈ hf.codChart (P := P).source

Tactic:
exact hfg (mem_of_mem_nhds hxs') ▸ mem_codChart_source hf
-- 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
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) (hf.domChart (P := P).restr s)

Tactic:
restr_mem_maximalAtlas _ hf.domChart_mem_maximalAtlas hs

Premises used: restr_mem_maximalAtlas, Set.Mem, IsManifold.maximalAtlas, Manifold.LiftSourceTargetPropertyAt.domChart_mem_maximalAtlas
-- 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
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) (hf.domChart (P := P).restr s)

Tactic:
exact restr_mem_maximalAtlas _ hf.domChart_mem_maximalAtlas hs

Premises used: restr_mem_maximalAtlas, Manifold.LiftSourceTargetPropertyAt.domChart_mem_maximalAtlas