awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
⊢ (↑e : X → Y) '' (e.source ∩ s) = e.target ∩ (↑e.symm : Y → X) ⁻¹' (e.source ∩ s)

Tactic:
e.toPartialEquiv.image_source_inter_eq s

Premises used: OpenPartialHomeomorph.toFun', PartialEquiv.image_source_inter_eq, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set Y
h : s ⊆ e.target
⊢ (↑e.symm : Y → X) '' s = e.source ∩ (↑e : X → Y) ⁻¹' s

Tactic:
e.symm.image_eq_target_inter_inv_preimage h

Premises used: OpenPartialHomeomorph.image_eq_target_inter_inv_preimage, PartialEquiv.symm, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set Y
⊢ (↑e.symm : Y → X) '' (e.target ∩ s) = e.source ∩ (↑e : X → Y) ⁻¹' (e.target ∩ s)

Tactic:
e.symm.image_source_inter_eq _

Premises used: PartialEquiv.symm, OpenPartialHomeomorph.image_source_inter_eq, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
⊢ e.source ∩ (↑e : X → Y) ⁻¹' (↑e.symm : Y → X) ⁻¹' s = e.source ∩ s

Tactic:
e.toPartialEquiv.source_inter_preimage_inv_preimage s

Premises used: OpenPartialHomeomorph.toFun', PartialEquiv.source_inter_preimage_inv_preimage, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set Y
⊢ e.target ∩ (↑e.symm : Y → X) ⁻¹' (↑e : X → Y) ⁻¹' s = e.target ∩ s

Tactic:
e.symm.source_inter_preimage_inv_preimage _

Premises used: OpenPartialHomeomorph.source_inter_preimage_inv_preimage, PartialEquiv.symm, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set Y
⊢ e.source ∩ (↑e : X → Y) ⁻¹' (e.target ∩ s) = e.source ∩ (↑e : X → Y) ⁻¹' s

Tactic:
e.toPartialEquiv.source_inter_preimage_target_inter s

Premises used: OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.toPartialEquiv, PartialEquiv.source_inter_preimage_target_inter
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ (↑e : X → Y) '' e.source = e.target

Tactic:
e.toPartialEquiv.image_source_eq_target

Premises used: PartialEquiv.image_source_eq_target, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ (↑e.symm : Y → X) '' e.target = e.source

Tactic:
e.symm.image_source_eq_target

Premises used: OpenPartialHomeomorph.image_source_eq_target, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set Y
hs : IsOpen[inst_1] s
⊢ IsOpen[inst] (e.source ∩ (↑e : X → Y) ⁻¹' s)

Tactic:
e.continuousOn.isOpen_inter_preimage e.open_source hs

Premises used: OpenPartialHomeomorph.open_source, ContinuousOn.isOpen_inter_preimage, OpenPartialHomeomorph.continuousOn
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : IsOpen[inst] s
⊢ IsOpen[inst_1] (e.target ∩ (↑e.symm : Y → X) ⁻¹' s)

Tactic:
e.symm.continuousOn.isOpen_inter_preimage e.open_target hs

Premises used: ContinuousOn.isOpen_inter_preimage, OpenPartialHomeomorph.continuousOn, OpenPartialHomeomorph.open_target, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : IsOpen[inst] s
hse : s ⊆ e.source
rw : IsOpen[inst_1] (e.target ∩ (↑e.symm : Y → X) ⁻¹' s)
⊢ IsOpen[inst_1] ((↑e : X → Y) '' s)

Tactic:
rw [(image_eq_target_inter_inv_preimage (e := e) hse)]

Premises used: OpenPartialHomeomorph.image_eq_target_inter_inv_preimage
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : IsOpen[inst] s
hse : s ⊆ e.source
⊢ IsOpen[inst_1] (e.target ∩ (↑e.symm : Y → X) ⁻¹' s)

Tactic:
e.continuousOn_invFun.isOpen_inter_preimage e.open_target hs

Premises used: ContinuousOn.isOpen_inter_preimage, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.continuousOn_invFun, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : IsOpen[inst] s
hse : s ⊆ e.source
⊢ IsOpen[inst_1] (e.target ∩ (↑e.symm : Y → X) ⁻¹' s)

Tactic:
exact e.continuousOn_invFun.isOpen_inter_preimage e.open_target hs

Premises used: ContinuousOn.isOpen_inter_preimage, OpenPartialHomeomorph.continuousOn_invFun, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : IsOpen[inst] s
⊢ IsOpen[inst_1] ((↑e : X → Y) '' (e.source ∩ s))

Tactic:
e.isOpen_image_of_subset_source (e.open_source.inter hs) inter_subset_left

Premises used: OpenPartialHomeomorph.open_source, OpenPartialHomeomorph.isOpen_image_of_subset_source, Set.inter_subset_left, IsOpen.inter
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
ht : IsOpen[inst_1] t
hte : t ⊆ e.target
⊢ IsOpen[inst] ((↑e.symm : Y → X) '' t)

Tactic:
isOpen_image_of_subset_source e.symm ht (e.symm_source ▸ hte)

Premises used: Eq.rec, OpenPartialHomeomorph.isOpen_image_of_subset_source, OpenPartialHomeomorph.symm_source, Eq.symm, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
⊢ IsOpen[inst] ((↑e.symm : Y → X) '' t) ↔ IsOpen[inst_1] t

Tactic:
⟨fun h ↦ ?_, fun h ↦ e.symm.isOpen_image_of_subset_source h hs⟩

Premises used: OpenPartialHomeomorph.isOpen_image_of_subset_source, Iff.intro, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
refine : ∀ (h : IsOpen[inst] ((↑e.symm : Y → X) '' t)), IsOpen[inst_1] t
⊢ IsOpen[inst] ((↑e.symm : Y → X) '' t) ↔ IsOpen[inst_1] t

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ e.symm.isOpen_image_of_subset_source h hs⟩
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen[inst] ((↑e.symm : Y → X) '' t)
rw : e.source ∩ (↑e : X → Y) ⁻¹' t ⊆ e.source
⊢ (↑e.symm : Y → X) '' t ⊆ e.source

Tactic:
rw [e.symm_image_eq_source_inter_preimage hs]

Premises used: OpenPartialHomeomorph.symm_image_eq_source_inter_preimage
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen[inst] ((↑e.symm : Y → X) '' t)
⊢ e.source ∩ (↑e : X → Y) ⁻¹' t ⊆ e.source

Tactic:
apply Set.inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen[inst] ((↑e.symm : Y → X) '' t)
⊢ (↑e.symm : Y → X) '' t ⊆ e.source

Tactic:
have hs' : e.symm '' t ⊆ e.source := by
    rw [e.symm_image_eq_source_inter_preimage hs]
    apply Set.inter_subset_left
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen[inst] ((↑e.symm : Y → X) '' t)
hs' : (↑e.symm : Y → X) '' t ⊆ e.source
rw : IsOpen[inst_1] ((↑e.toPartialEquiv : X → Y) '' (↑e.symm : Y → X) '' t)
⊢ IsOpen[inst_1] t

Tactic:
rw [← e.image_symm_image_of_subset_target hs]

Premises used: PartialEquiv.image_symm_image_of_subset_target, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen[inst] ((↑e.symm : Y → X) '' t)
hs' : (↑e.symm : Y → X) '' t ⊆ e.source
⊢ IsOpen[inst_1] ((↑e.toPartialEquiv : X → Y) '' (↑e.symm : Y → X) '' t)

Tactic:
e.isOpen_image_of_subset_source h hs'

Premises used: OpenPartialHomeomorph.isOpen_image_of_subset_source, OpenPartialHomeomorph.toFun'
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen[inst] ((↑e.symm : Y → X) '' t)
hs' : (↑e.symm : Y → X) '' t ⊆ e.source
⊢ IsOpen[inst_1] ((↑e.toPartialEquiv : X → Y) '' (↑e.symm : Y → X) '' t)

Tactic:
exact e.isOpen_image_of_subset_source h hs'

Premises used: OpenPartialHomeomorph.isOpen_image_of_subset_source
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : s ⊆ e.source
rw : IsOpen[inst_1] ((↑e : X → Y) '' s) ↔ IsOpen[inst_1] ((↑e.symm.symm : X → Y) '' s)
rw₁ rw₂ : IsOpen[inst_1] ((↑e : X → Y) '' s) ↔ IsOpen[inst_1] ((↑e : X → Y) '' s)
⊢ IsOpen[inst_1] ((↑e : X → Y) '' s) ↔ IsOpen[inst] s

Tactic:
rw [← e.symm.isOpen_symm_image_iff_of_subset_target hs, e.symm_symm]

Premises used: OpenPartialHomeomorph.isOpen_symm_image_iff_of_subset_target, OpenPartialHomeomorph.symm_symm, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X Y
e : PartialEquiv X Y
hc : ContinuousOn (↑e : X → Y) e.source
ho : IsOpenMap (e.source.restrict (π := fun (a : X) ↦ Y) (↑e : X → Y))
hs : IsOpen[inst] e.source
⊢ IsOpen[inst_2] e.target

Tactic:
simpa only [range_restrict, e.image_source_eq_target] using ho.isOpen_range

Premises used: PartialEquiv.image_source_eq_target, Set.range_restrict, IsOpenMap.isOpen_range
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : PartialEquiv X Y
hc : ContinuousOn (↑e : X → Y) e.source
ho : IsOpenMap (e.source.restrict (π := fun (a : X) ↦ Y) (↑e : X → Y))
hs : IsOpen[inst] e.source
⊢ (↑(ofContinuousOpenRestrict e hc ho hs) : X → Y) = (↑e : X → Y)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : PartialEquiv X Y
hc : ContinuousOn (↑e : X → Y) e.source
ho : IsOpenMap (e.source.restrict (π := fun (a : X) ↦ Y) (↑e : X → Y))
hs : IsOpen[inst] e.source
⊢ (↑(ofContinuousOpenRestrict e hc ho hs).symm : Y → X) = (↑e.symm : Y → X)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : PartialEquiv X Y
hc : ContinuousOn (↑e : X → Y) e.source
ho : IsOpenMap (↑e : X → Y)
hs : IsOpen[inst] e.source
⊢ (↑(ofContinuousOpen e hc ho hs) : X → Y) = (↑e : X → Y)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : PartialEquiv X Y
hc : ContinuousOn (↑e : X → Y) e.source
ho : IsOpenMap (↑e : X → Y)
hs : IsOpen[inst] e.source
⊢ (↑(ofContinuousOpen e hc ho hs).symm : Y → X) = (↑e.symm : Y → X)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
inst_2 : SecondCountableTopology Y
⊢ SecondCountableTopology.{u_1} (↑e.source : Type u_1)

Tactic:
e.toHomeomorphSourceTarget.secondCountableTopology

Premises used: Homeomorph.secondCountableTopology, OpenPartialHomeomorph.toHomeomorphSourceTarget
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
⊢ x ∈ e.source

Tactic:
hx
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
lift : ∀ (x : { x : X // x ∈ e.source }), 𝓝 (↑x : X) = comap (↑e : X → Y) (𝓝 ((↑e : X → Y) (↑x : X))) ⊓ 𝓟 e.source
⊢ 𝓝 x = comap (↑e : X → Y) (𝓝 ((↑e : X → Y) x)) ⊓ 𝓟 e.source

Tactic:
lift x to e.source using hx

Premises used: PartialEquiv.source, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : { x : X // x ∈ e.source }
rw :
  map (α := { x : X // x ∈ e.source }) (Subtype.val (p := fun (x : X) ↦ x ∈ e.source))
      (comap.{u_1, u_3} (β := (↑e.target : Type u_3))
        (⇑e.toHomeomorphSourceTarget : (a : (↑e.source : Type u_1)) → (↑e.target : Type u_3))
        (comap (Subtype.val (p := fun (x : Y) ↦ x ∈ e.target))
          (𝓝 (↑((e.toHomeomorphSourceTarget : (a : (↑e.source : Type u_1)) → (↑e.target : Type u_3)) x) : Y)))) =
    map (α := { x : X // x ∈ e.source }) (Subtype.val (p := fun (x : X) ↦ x ∈ e.source))
      (comap (Subtype.val (p := fun (x : X) ↦ x ∈ e.source)) (comap (↑e : X → Y) (𝓝 ((↑e : X → Y) (↑x : X)))))
⊢ 𝓝 (↑x : X) = comap (↑e : X → Y) (𝓝 ((↑e : X → Y) (↑x : X))) ⊓ 𝓟 e.source

Tactic:
rw [← e.open_source.nhdsWithin_eq x.2, ← map_nhds_subtype_val, ← map_comap_setCoe_val,
    e.toHomeomorphSourceTarget.nhds_eq_comap, nhds_subtype_eq_comap]

Premises used: IsOpen.nhdsWithin_eq, OpenPartialHomeomorph.open_source, Filter.map_comap_setCoe_val, nhds_subtype_eq_comap, Homeomorph.nhds_eq_comap, OpenPartialHomeomorph.toHomeomorphSourceTarget, Subtype.property, map_nhds_subtype_val
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : { x : X // x ∈ e.source }
⊢ map (α := { x : X // x ∈ e.source }) (Subtype.val (p := fun (x : X) ↦ x ∈ e.source))
      (comap.{u_1, u_3} (β := (↑e.target : Type u_3))
        (⇑e.toHomeomorphSourceTarget : (a : (↑e.source : Type u_1)) → (↑e.target : Type u_3))
        (comap (Subtype.val (p := fun (x : Y) ↦ x ∈ e.target))
          (𝓝 (↑((e.toHomeomorphSourceTarget : (a : (↑e.source : Type u_1)) → (↑e.target : Type u_3)) x) : Y)))) =
    map (α := { x : X // x ∈ e.source }) (Subtype.val (p := fun (x : X) ↦ x ∈ e.source))
      (comap (Subtype.val (p := fun (x : X) ↦ x ∈ e.source)) (comap (↑e : X → Y) (𝓝 ((↑e : X → Y) (↑x : X)))))

Tactic:
simp only [Function.comp_def, toHomeomorphSourceTarget_apply_coe, comap_comap]

Premises used: OpenPartialHomeomorph.toHomeomorphSourceTarget_apply_coe, Function.comp_def, Filter.comap_comap
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z
inst_5 : TopologicalSpace Z'
e : OpenPartialHomeomorph X Y
h : e.source = univ
h' : e.target = univ
x : X
rw : Membership.mem (γ := Set X) univ x
⊢ x ∈ e.source

Tactic:
rw [h]
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z
inst_5 : TopologicalSpace Z'
e : OpenPartialHomeomorph X Y
h : e.source = univ
h' : e.target = univ
x : X
⊢ Membership.mem (γ := Set X) univ x

Tactic:
mem_univ _

Premises used: Set.mem_univ
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z
inst_5 : TopologicalSpace Z'
e : OpenPartialHomeomorph X Y
h : e.source = univ
h' : e.target = univ
x : X
⊢ Membership.mem (γ := Set X) univ x

Tactic:
exact mem_univ _

Premises used: Set.mem_univ
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z
inst_5 : TopologicalSpace Z'
e : OpenPartialHomeomorph X Y
h : e.source = univ
h' : e.target = univ
x : Y
rw : Membership.mem (γ := Set Y) univ x
⊢ x ∈ e.target

Tactic:
rw [h']
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z
inst_5 : TopologicalSpace Z'
e : OpenPartialHomeomorph X Y
h : e.source = univ
h' : e.target = univ
x : Y
⊢ Membership.mem (γ := Set Y) univ x

Tactic:
mem_univ _

Premises used: Set.mem_univ
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z
inst_5 : TopologicalSpace Z'
e : OpenPartialHomeomorph X Y
h : e.source = univ
h' : e.target = univ
x : Y
⊢ Membership.mem (γ := Set Y) univ x

Tactic:
exact mem_univ _

Premises used: Set.mem_univ
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z
inst_5 : TopologicalSpace Z'
e : OpenPartialHomeomorph X Y
h : e.source = univ
h' : e.target = univ
⊢ Continuous[inst, inst_2] (↑e : X → Y)

Tactic:
simpa only [continuousOn_univ, h] using e.continuousOn

Premises used: OpenPartialHomeomorph.continuousOn, continuousOn_univ
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z
inst_5 : TopologicalSpace Z'
e : OpenPartialHomeomorph X Y
h : e.source = univ
h' : e.target = univ
⊢ Continuous[inst_2, inst] (↑e.symm : Y → X)

Tactic:
simpa only [continuousOn_univ, h'] using e.continuousOn_symm

Premises used: OpenPartialHomeomorph.continuousOn_symm, continuousOn_univ
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ IsOpenEmbedding (e.source.restrict (π := fun (a : X) ↦ Y) (↑e : X → Y))

Tactic:
.of_continuous_injective_isOpenMap (e.continuousOn.comp_continuous
    continuous_subtype_val Subtype.prop) e.injOn.injective fun V hV ↦ ?_

Premises used: continuous_subtype_val, ContinuousOn.comp_continuous, Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap, Set.InjOn.injective, OpenPartialHomeomorph.continuousOn, Subtype.prop, OpenPartialHomeomorph.injOn
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
refine :
  ∀ (V : Set (↑e.source : Type u_1)) (hV : IsOpen[instTopologicalSpaceSubtype] V),
    IsOpen[inst_1] (e.source.restrict (π := fun (a : X) ↦ Y) (↑e : X → Y) '' V)
⊢ IsOpenEmbedding (e.source.restrict (π := fun (a : X) ↦ Y) (↑e : X → Y))

Tactic:
refine .of_continuous_injective_isOpenMap (e.continuousOn.comp_continuous
    continuous_subtype_val Subtype.prop) e.injOn.injective fun V hV ↦ ?_
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
V : Set (↑e.source : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
rw : IsOpen[inst_1] ((↑e : X → Y) '' Subtype.val (p := fun (x : X) ↦ x ∈ e.source) '' V)
⊢ IsOpen[inst_1] (e.source.restrict (π := fun (a : X) ↦ Y) (↑e : X → Y) '' V)

Tactic:
rw [Set.restrict_eq, Set.image_comp]

Premises used: Set.restrict_eq, Set.image_comp
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
V : Set (↑e.source : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
⊢ IsOpen[inst_1] ((↑e : X → Y) '' Subtype.val (p := fun (x : X) ↦ x ∈ e.source) '' V)

Tactic:
e.isOpen_image_of_subset_source (e.open_source.isOpenMap_subtype_val V hV)
    fun _ ⟨x, _, h⟩ ↦ h ▸ x.2

Premises used: OpenPartialHomeomorph.open_source, Membership.mem, Eq.rec, OpenPartialHomeomorph.isOpen_image_of_subset_source, PartialEquiv.source, OpenPartialHomeomorph.toPartialEquiv, IsOpen.isOpenMap_subtype_val, _private.0.OpenPartialHomeomorph.isOpenEmbedding_restrict.match_1, Subtype.property
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
V : Set (↑e.source : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
⊢ IsOpen[inst_1] ((↑e : X → Y) '' Subtype.val (p := fun (x : X) ↦ x ∈ e.source) '' V)

Tactic:
exact e.isOpen_image_of_subset_source (e.open_source.isOpenMap_subtype_val V hV)
    fun _ ⟨x, _, h⟩ ↦ h ▸ x.2

Premises used: OpenPartialHomeomorph.open_source, Membership.mem, Eq.rec, OpenPartialHomeomorph.isOpen_image_of_subset_source, _private.0.match_1, PartialEquiv.source, OpenPartialHomeomorph.toPartialEquiv, IsOpen.isOpenMap_subtype_val, Subtype.property
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
h : e.source = univ
⊢ IsOpenEmbedding (↑e : X → Y)

Tactic:
e.isOpenEmbedding_restrict.comp
    ((Homeomorph.setCongr h).trans <| Homeomorph.Set.univ X).symm.isOpenEmbedding

Premises used: Homeomorph.Set.univ, OpenPartialHomeomorph.isOpenEmbedding_restrict, OpenPartialHomeomorph.toFun', Homeomorph.symm, Homeomorph.trans, Homeomorph.setCongr, Homeomorph.isOpenEmbedding, Set.restrict, Topology.IsOpenEmbedding.comp