awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
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 : X ≃ₜ Y
s : Set X
hs : IsOpen[inst] s
t : Set Y
h : (⇑e : (a : X) → Y) '' s = t
⊢ IsOpen[inst_2] (e.toPartialEquivOfImageEq s t h).target

Tactic:
simpa [← h]
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
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 : X ≃ₜ Y
rw : Eq.{u_3 + 1} (α := Set Y) (range.{u_3, u_1 + 1} (ι := X) (⇑e : (a : X) → Y)) univ
rw₁ rw₂ : Eq.{u_3 + 1} (α := Set Y) univ univ
⊢ Eq.{u_3 + 1} (α := Set Y) (image.{u_1, u_3} (α := X) (⇑e : (a : X) → Y) univ) univ

Tactic:
rw [image_univ, e.surjective.range_eq]

Premises used: Set.image_univ, Function.Surjective.range_eq, Homeomorph.surjective
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
e' : PartialEquiv X Y
h : e.toPartialEquiv = e'
mk :
  ∀ (toPartialEquiv : PartialEquiv X Y) (open_source : IsOpen[inst] toPartialEquiv.source)
    (open_target : IsOpen[inst_1] toPartialEquiv.target)
    (continuousOn_toFun : ContinuousOn (↑toPartialEquiv : X → Y) toPartialEquiv.source)
    (continuousOn_invFun : ContinuousOn toPartialEquiv.invFun toPartialEquiv.target)
    (h :
      { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
            continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun :
            OpenPartialHomeomorph X Y }.toPartialEquiv =
        e'),
    { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
            continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun :
            OpenPartialHomeomorph X Y }.replaceEquiv
        e' h =
      { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
        continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun }
⊢ e.replaceEquiv e' h = e

Tactic:
cases e
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e' toPartialEquiv : PartialEquiv X Y
open_source : IsOpen[inst] toPartialEquiv.source
open_target : IsOpen[inst_1] toPartialEquiv.target
continuousOn_toFun : ContinuousOn (↑toPartialEquiv : X → Y) toPartialEquiv.source
continuousOn_invFun : ContinuousOn toPartialEquiv.invFun toPartialEquiv.target
h :
  { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
        continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun :
        OpenPartialHomeomorph X Y }.toPartialEquiv =
    e'
mk :
  { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
          continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun :
          OpenPartialHomeomorph X Y }.replaceEquiv
      { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
          continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun :
          OpenPartialHomeomorph X Y }.toPartialEquiv
      ⋯ =
    { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
      continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun }
⊢ { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
          continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun :
          OpenPartialHomeomorph X Y }.replaceEquiv
      e' h =
    { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
      continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun }

Tactic:
subst e'
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
toPartialEquiv : PartialEquiv X Y
open_source : IsOpen[inst] toPartialEquiv.source
open_target : IsOpen[inst_1] toPartialEquiv.target
continuousOn_toFun : ContinuousOn (↑toPartialEquiv : X → Y) toPartialEquiv.source
continuousOn_invFun : ContinuousOn toPartialEquiv.invFun toPartialEquiv.target
⊢ { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
          continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun :
          OpenPartialHomeomorph X Y }.replaceEquiv
      { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
          continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun :
          OpenPartialHomeomorph X Y }.toPartialEquiv
      ⋯ =
    { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
      continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun }

Tactic:
rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : ∀ (x : X), (↑e : X → Y) x = (↑e' : X → Y) x
hinv : ∀ (x : Y), (↑e.symm : Y → X) x = (↑e'.symm : Y → X) x
hs : e.source = e'.source
⊢ e = e'

Tactic:
toPartialEquiv_injective (PartialEquiv.ext h hinv hs)

Premises used: OpenPartialHomeomorph.toPartialEquiv_injective, PartialEquiv.ext
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ e.symm.toPartialEquiv = e.symm

Tactic:
rfl

Premises used: PartialEquiv.symm, rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ e.symm.source = e.target

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ e.symm.target = e.source

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: PartialEquiv.symm, rfl, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Defs
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Bijective (α := OpenPartialHomeomorph X Y) OpenPartialHomeomorph.symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, Function.bijective_iff_has_inverse, And.intro, Exists.intro, OpenPartialHomeomorph.symm_symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
h : e.IsImage s t
⊢ e.IsImage s t

Tactic:
h

Premises used: Set.Mem, OpenPartialHomeomorph.toFun', PartialEquiv.IsImage
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
x : X
h : e.IsImage s t
hx : x ∈ e.source
⊢ (↑e : X → Y) x ∈ t ↔ x ∈ s

Tactic:
h hx
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
h : e.IsImage s t
⊢ e.symm.IsImage t s

Tactic:
h.toPartialEquiv.symm

Premises used: Set.Mem, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.IsImage, OpenPartialHomeomorph.IsImage.toPartialEquiv, PartialEquiv.IsImage.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
y : Y
h : e.IsImage s t
hy : y ∈ e.target
⊢ (↑e.symm : Y → X) y ∈ s ↔ y ∈ t

Tactic:
h.symm hy

Premises used: OpenPartialHomeomorph.IsImage.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
⊢ e.symm.IsImage t s ↔ e.IsImage s t

Tactic:
⟨fun h => h.symm, fun h => h.symm⟩

Premises used: Iff.intro, OpenPartialHomeomorph.IsImage.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
h : e.IsImage s t
⊢ MapsTo (↑e : X → Y) (e.source ∩ s) (e.target ∩ t)

Tactic:
h.toPartialEquiv.mapsTo

Premises used: PartialEquiv.IsImage.mapsTo, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.IsImage.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
h : e.IsImage s t
⊢ MapsTo (↑e.symm : Y → X) (e.target ∩ t) (e.source ∩ s)

Tactic:
h.symm.mapsTo

Premises used: OpenPartialHomeomorph.IsImage.mapsTo, OpenPartialHomeomorph.IsImage.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
h : e.IsImage s t
⊢ (↑e : X → Y) '' (e.source ∩ s) = e.target ∩ t

Tactic:
h.toPartialEquiv.image_eq

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

Tactic:
h.symm.image_eq

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

Tactic:
PartialEquiv.IsImage.iff_preimage_eq

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

Tactic:
symm_iff.symm.trans iff_preimage_eq

Premises used: Iff.trans, Iff.symm, OpenPartialHomeomorph.IsImage.symm_iff, OpenPartialHomeomorph.IsImage.iff_preimage_eq
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
rw : e.target ∩ (↑e.symm : Y → X) ⁻¹' s = e.target ∩ t ↔ e.target ∩ (↑e.symm : Y → X) ⁻¹' (e.source ∩ s) = e.target ∩ t
rw₁ : e.target ∩ (↑e.symm : Y → X) ⁻¹' s = e.target ∩ t ↔ (↑e : X → Y) '' (e.source ∩ s) = e.target ∩ t
rw₂ rw₃ : (↑e : X → Y) '' (e.source ∩ s) = e.target ∩ t ↔ (↑e : X → Y) '' (e.source ∩ s) = e.target ∩ t
⊢ e.IsImage s t ↔ e.target ∩ (↑e.symm : Y → X) ⁻¹' (e.source ∩ s) = e.target ∩ t

Tactic:
rw [iff_symm_preimage_eq, ← image_source_inter_eq, ← image_source_inter_eq']

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

Tactic:
symm_iff.symm.trans iff_symm_preimage_eq'

Premises used: Iff.trans, OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq', Iff.symm, OpenPartialHomeomorph.IsImage.symm_iff
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
h : (↑e : X → Y) '' (e.source ∩ s) = e.target ∩ t
⊢ e.IsImage s t

Tactic:
PartialEquiv.IsImage.of_image_eq h

Premises used: Set.Mem, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.IsImage, PartialEquiv.IsImage.of_image_eq
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
h : (↑e.symm : Y → X) '' (e.target ∩ t) = e.source ∩ s
⊢ e.IsImage s t

Tactic:
PartialEquiv.IsImage.of_symm_image_eq h

Premises used: Set.Mem, PartialEquiv.IsImage.of_symm_image_eq, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.IsImage
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
h : e.IsImage s t
⊢ e.IsImage sᶜ tᶜ

Tactic:
fun _ hx => (h hx).not

Premises used: Set.Mem, setOf, Iff.not, OpenPartialHomeomorph.IsImage, Not
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
s' : Set X
t' : Set Y
h : e.IsImage s t
h' : e.IsImage s' t'
⊢ e.IsImage (s ∩ s') (t ∩ t')

Tactic:
fun _ hx => (h hx).and (h' hx)

Premises used: Set.Mem, setOf, Set.inter, OpenPartialHomeomorph.IsImage, Iff.and
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
s' : Set X
t' : Set Y
h : e.IsImage s t
h' : e.IsImage s' t'
⊢ e.IsImage (s ∪ s') (t ∪ t')

Tactic:
fun _ hx => (h hx).or (h' hx)

Premises used: Set.union, Set.Mem, setOf, OpenPartialHomeomorph.IsImage, Iff.or
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
s' : Set X
t' : Set Y
h : e.IsImage s t
h' : e.IsImage s' t'
⊢ e.IsImage (s \ s') (t \ t')

Tactic:
h.inter h'.compl

Premises used: Set.Mem, Set.diff, OpenPartialHomeomorph.IsImage.compl, setOf, OpenPartialHomeomorph.IsImage.inter, Not
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
e' : OpenPartialHomeomorph X Y
inst_2 : (i : X) → Decidable (i ∈ s)
inst_3 : (i : Y) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
⊢ LeftInvOn (t.piecewise (β := fun (a : Y) ↦ X) (↑e.symm : Y → X) (↑e'.symm : Y → X))
    (s.piecewise (β := fun (a : X) ↦ Y) (↑e : X → Y) (↑e' : X → Y)) (s.ite e.source e'.source)

Tactic:
h.toPartialEquiv.leftInvOn_piecewise h'

Premises used: PartialEquiv.IsImage.leftInvOn_piecewise, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.IsImage.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
e' : OpenPartialHomeomorph X Y
h : e.IsImage s t
h' : e'.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
Heq : EqOn (↑e : X → Y) (↑e' : X → Y) (e.source ∩ s)
⊢ e.target ∩ t = e'.target ∩ t

Tactic:
h.toPartialEquiv.inter_eq_of_inter_eq_of_eqOn h' hs Heq

Premises used: PartialEquiv.IsImage.inter_eq_of_inter_eq_of_eqOn, OpenPartialHomeomorph.IsImage.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
e' : OpenPartialHomeomorph X Y
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
Heq : EqOn (↑e : X → Y) (↑e' : X → Y) (e.source ∩ s)
⊢ EqOn (↑e.symm : Y → X) (↑e'.symm : Y → X) (e.target ∩ t)

Tactic:
h.toPartialEquiv.symm_eq_on_of_inter_eq_of_eqOn hs Heq

Premises used: OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.IsImage.toPartialEquiv, PartialEquiv.IsImage.symm_eq_on_of_inter_eq_of_eqOn
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
x : X
h : e.IsImage s t
hx : x ∈ e.source
rw : 𝓝[(↑e : X → Y) '' (e.source ∩ s)] (↑e : X → Y) x = 𝓝[t] (↑e : X → Y) x
rw₁ : 𝓝[e.target ∩ t] (↑e : X → Y) x = 𝓝[t] (↑e : X → Y) x
rw₂ rw₃ : 𝓝[t] (↑e : X → Y) x = 𝓝[t] (↑e : X → Y) x
⊢ map (↑e : X → Y) (𝓝[s] x) = 𝓝[t] (↑e : X → Y) x

Tactic:
rw [e.map_nhdsWithin_eq hx, h.image_eq, e.nhdsWithin_target_inter (e.map_source hx)]

Premises used: OpenPartialHomeomorph.map_nhdsWithin_eq, OpenPartialHomeomorph.nhdsWithin_target_inter, OpenPartialHomeomorph.map_source, OpenPartialHomeomorph.IsImage.image_eq
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
h : e.IsImage s t
x : X
hx : x ∈ e.source
⊢ (↑e : X → Y) x ∈ closure[inst_1] t ↔ x ∈ closure[inst] s

Tactic:
simp only [mem_closure_iff_nhdsWithin_neBot, ← h.map_nhdsWithin_eq hx, map_neBot_iff]

Premises used: mem_closure_iff_nhdsWithin_neBot, OpenPartialHomeomorph.IsImage.map_nhdsWithin_eq, Filter.map_neBot_iff
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
h : e.IsImage s t
⊢ e.IsImage (interior s) (interior t)

Tactic:
simpa only [closure_compl, compl_compl] using h.compl.closure.compl

Premises used: OpenPartialHomeomorph.IsImage.closure, compl_compl, OpenPartialHomeomorph.IsImage.compl, closure_compl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
h : e.IsImage s t
⊢ e.IsImage (frontier s) (frontier t)

Tactic:
h.closure.diff h.interior

Premises used: OpenPartialHomeomorph.IsImage.closure, frontier, OpenPartialHomeomorph.IsImage.interior, OpenPartialHomeomorph.IsImage.diff
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
h : e.IsImage s t
⊢ IsOpen[inst] (e.source ∩ s) ↔ IsOpen[inst_1] (e.target ∩ t)

Tactic:
⟨fun hs => h.symm_preimage_eq' ▸ e.symm.isOpen_inter_preimage hs, fun hs =>
    h.preimage_eq' ▸ e.isOpen_inter_preimage hs⟩

Premises used: OpenPartialHomeomorph.IsImage.preimage_eq', Eq.rec, OpenPartialHomeomorph.isOpen_inter_preimage, Iff.intro, OpenPartialHomeomorph.IsImage.symm_preimage_eq', OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ e.IsImage e.source e.target

Tactic:
e.toPartialEquiv.isImage_source_target

Premises used: Set.Mem, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.IsImage, PartialEquiv.isImage_source_target, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
hs : Disjoint e.source e'.source
ht : Disjoint e.target e'.target
⊢ e.IsImage e'.source e'.target

Tactic:
e.toPartialEquiv.isImage_source_target_of_disjoint e'.toPartialEquiv hs ht

Premises used: Set.Mem, PartialEquiv.isImage_source_target_of_disjoint, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.IsImage, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
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) ⁻¹' interior s = e.source ∩ interior ((↑e : X → Y) ⁻¹' s)

Tactic:
(IsImage.of_preimage_eq rfl).interior.preimage_eq

Premises used: OpenPartialHomeomorph.IsImage.of_preimage_eq, OpenPartialHomeomorph.IsImage.interior, OpenPartialHomeomorph.IsImage.preimage_eq, rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
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) ⁻¹' closure[inst_1] s = e.source ∩ closure[inst] ((↑e : X → Y) ⁻¹' s)

Tactic:
(IsImage.of_preimage_eq rfl).closure.preimage_eq

Premises used: OpenPartialHomeomorph.IsImage.closure, OpenPartialHomeomorph.IsImage.of_preimage_eq, OpenPartialHomeomorph.IsImage.preimage_eq, rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
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) ⁻¹' frontier s = e.source ∩ frontier ((↑e : X → Y) ⁻¹' s)

Tactic:
(IsImage.of_preimage_eq rfl).frontier.preimage_eq

Premises used: OpenPartialHomeomorph.IsImage.of_preimage_eq, OpenPartialHomeomorph.IsImage.preimage_eq, OpenPartialHomeomorph.IsImage.frontier, rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
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
⊢ (e.restrOpen s hs).toPartialEquiv = e.restr s

Tactic:
rfl

Premises used: PartialEquiv.restr, OpenPartialHomeomorph.toFun', PartialEquiv.IsImage.restr, rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
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
⊢ (e.restrOpen s hs).source = e.source ∩ s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
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
⊢ (↑(e.restrOpen s hs) : X → Y) = (↑e : X → Y)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.IsImage.restr, setOf, OpenPartialHomeomorph.toFun', Set.inter, OpenPartialHomeomorph.restrOpen, PartialEquiv.IsImage.restr, rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
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
⊢ (↑(e.restrOpen s hs).symm : Y → X) = (↑e.symm : Y → X)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.IsImage.restr, setOf, PartialEquiv.symm, OpenPartialHomeomorph.toFun', Set.inter, OpenPartialHomeomorph.restrOpen, PartialEquiv.IsImage.restr, rfl, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
⊢ (e.restr s).toPartialEquiv = e.restr (interior s)

Tactic:
rfl

Premises used: PartialEquiv.restr, OpenPartialHomeomorph.toFun', PartialEquiv.IsImage.restr, rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
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
⊢ (e.restr s).source = e.source ∩ s

Tactic:
grind