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
f : X → Y
h : IsOpenEmbedding f
inst_2 : Nonempty X
x : X
h₁ : x ∈ (toOpenPartialHomeomorph f h).source
⊢ (↑(toOpenPartialHomeomorph f h).symm : Y → X) (f x) = x

Tactic:
rw [← congr_fun (h.toOpenPartialHomeomorph_apply f), OpenPartialHomeomorph.left_inv]

Premises used: Topology.IsOpenEmbedding.toOpenPartialHomeomorph_apply, OpenPartialHomeomorph.left_inv, congr_fun
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst_2 : Nonempty X
x : X
⊢ x ∈ (toOpenPartialHomeomorph f h).source

Tactic:
Set.mem_univ _

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst_2 : Nonempty X
x : X
⊢ x ∈ (toOpenPartialHomeomorph f h).source

Tactic:
exact Set.mem_univ _

Premises used: Set.mem_univ
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst_2 : Nonempty X
x : Y
hx : x ∈ range f
h₁ : x ∈ (toOpenPartialHomeomorph f h).target
⊢ f ((↑(toOpenPartialHomeomorph f h).symm : Y → X) x) = x

Tactic:
rw [← congr_fun (h.toOpenPartialHomeomorph_apply f), OpenPartialHomeomorph.right_inv]

Premises used: Topology.IsOpenEmbedding.toOpenPartialHomeomorph_apply, congr_fun, OpenPartialHomeomorph.right_inv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst_2 : Nonempty X
x : Y
hx h₁ h₂ h₃ h₄ : x ∈ range f
⊢ x ∈ (toOpenPartialHomeomorph f h).target

Tactic:
rwa [toOpenPartialHomeomorph_target]

Premises used: Topology.IsOpenEmbedding.toOpenPartialHomeomorph_target
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
⊢ (↑(s.openPartialHomeomorphSubtypeCoe hs) : ↥s → X) = Subtype.val (p := fun (x : X) ↦ x ∈ s)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
⊢ (s.openPartialHomeomorphSubtypeCoe hs).source = univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
simp : {x : X | x ∈ s.carrier} = (↑s : Set X)
⊢ (s.openPartialHomeomorphSubtypeCoe hs).target = (↑s : Set X)

Tactic:
simp only [openPartialHomeomorphSubtypeCoe, Subtype.range_coe_subtype, mfld_simps]

Premises used: TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe, Subtype.range_coe_subtype
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
⊢ {x : X | x ∈ s.carrier} = (↑s : Set X)

Tactic:
rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
a : X
b : Y
ha : IsOpen[inst] {a}
hb : IsOpen[inst_2] {b}
⊢ ContinuousOn (↑(PartialEquiv.single a b) : X → Y) (PartialEquiv.single a b).source

Tactic:
simp
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
a : X
b : Y
ha : IsOpen[inst] {a}
hb : IsOpen[inst_2] {b}
⊢ ContinuousOn (PartialEquiv.single a b).invFun (PartialEquiv.single a b).target

Tactic:
simp
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
a : X
b : Y
ha : IsOpen[inst] {a}
hb : IsOpen[inst_1] {b}
x : X
⊢ (↑(const ha hb) : X → Y) x = b

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
a : X
b : Y
ha : IsOpen[inst] {a}
hb : IsOpen[inst_1] {b}
⊢ (const ha hb).source = {a}

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
a : X
b : Y
ha : IsOpen[inst] {a}
hb : IsOpen[inst_1] {b}
⊢ (const ha hb).target = {b}

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
eX : OpenPartialHomeomorph X X'
eY : OpenPartialHomeomorph Y Y'
⊢ (eX.prod eY).symm = eX.symm.prod eY.symm

Tactic:
rfl

Premises used: PartialEquiv.prod, PartialEquiv.symm, OpenPartialHomeomorph.prod, rfl, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Eq (α := OpenPartialHomeomorph (X × Y) (X × Y)) (prod (OpenPartialHomeomorph.refl X) (OpenPartialHomeomorph.refl Y))
    (OpenPartialHomeomorph.refl (X × Y))

Tactic:
OpenPartialHomeomorph.ext _ _ (fun _ => rfl) (fun _ => rfl) univ_prod_univ

Premises used: Set.univ_prod_univ, OpenPartialHomeomorph.ext, rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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
f : OpenPartialHomeomorph Y Z
e' : OpenPartialHomeomorph X' Y'
f' : OpenPartialHomeomorph Y' Z'
⊢ (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')

Tactic:
toPartialEquiv_injective <| e.1.prod_trans ..

Premises used: OpenPartialHomeomorph.toPartialEquiv_injective, PartialEquiv.prod_trans, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
obtain : ∀ (x : X) (y : Y), eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Tactic:
obtain ⟨⟨x, y⟩, -⟩ := id h

Premises used: id
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
⊢ Nonempty X

Tactic:
haveI : Nonempty X := ⟨x⟩
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this : Nonempty X
⊢ Nonempty X'

Tactic:
haveI : Nonempty X' := ⟨eX x⟩
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this_1 : Nonempty X
this : Nonempty X'
⊢ Nonempty Y

Tactic:
haveI : Nonempty Y := ⟨y⟩
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this_1 : Nonempty X
this_2 : Nonempty X'
this : Nonempty Y
⊢ Nonempty Y'

Tactic:
haveI : Nonempty Y' := ⟨eY y⟩
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX'.prod eY').source.Nonempty
rw : eX'.prod eY' = eX.prod eY ↔ eX = eX' ∧ eY = eY'
rw₁ : eX' = eX ∧ eY' = eY ↔ eX = eX' ∧ eY = eY'
rw₂ : eX = eX' ∧ eY' = eY ↔ eX = eX' ∧ eY = eY'
rw₃ rw₄ : eX = eX' ∧ eY = eY' ↔ eX = eX' ∧ eY = eY'
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Tactic:
rw [eq_comm, prod_eq_prod_of_nonempty h, eq_comm, @eq_comm _ eY']

Premises used: OpenPartialHomeomorph.prod_eq_prod_of_nonempty, eq_comm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
e f : OpenPartialHomeomorph X Y
e' f' : OpenPartialHomeomorph X' Y'
⊢ (e.prod e').symm.trans (f.prod f') = (e.symm.trans f).prod (e'.symm.trans f')

Tactic:
simp
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
inst_2 : (x : X) → Decidable (x ∈ s)
inst_3 : (y : Y) → Decidable (y ∈ t)
H : e.IsImage s t
H' : e'.IsImage s t
Hs : e.source ∩ frontier s = e'.source ∩ frontier s
Heq : EqOn (↑e : X → Y) (↑e' : X → Y) (e.source ∩ frontier s)
⊢ (e.piecewise e' s t H H' Hs Heq).symm = e.symm.piecewise e'.symm t s ⋯ ⋯ ⋯ ⋯

Tactic:
rfl

Premises used: Set.ite, PartialEquiv.symm, OpenPartialHomeomorph.piecewise, Set.piecewise, PartialEquiv.piecewise, rfl, OpenPartialHomeomorph.symm, ite
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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 e e' : OpenPartialHomeomorph X Y
inst_6 : (x : X) → Decidable (x ∈ e.source)
inst_7 : (y : Y) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
rw : ∅ = e'.source ∩ frontier e.source
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set X) ∅ ∅
⊢ e.source ∩ frontier e.source = e'.source ∩ frontier e.source

Tactic:
rw [e.open_source.inter_frontier_eq, (Hs.symm.frontier_right e'.open_source).inter_eq]

Premises used: OpenPartialHomeomorph.open_source, IsOpen.inter_frontier_eq, Disjoint.symm, Disjoint.inter_eq, Disjoint.frontier_right
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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 e e' : OpenPartialHomeomorph X Y
inst_6 : (x : X) → Decidable (x ∈ e.source)
inst_7 : (y : Y) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
rw : EqOn (↑e : X → Y) (↑e' : X → Y) ∅
⊢ EqOn (↑e : X → Y) (↑e' : X → Y) (e.source ∩ frontier e.source)

Tactic:
rw [e.open_source.inter_frontier_eq]

Premises used: OpenPartialHomeomorph.open_source, IsOpen.inter_frontier_eq
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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 e e' : OpenPartialHomeomorph X Y
inst_6 : (x : X) → Decidable (x ∈ e.source)
inst_7 : (y : Y) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
⊢ EqOn (↑e : X → Y) (↑e' : X → Y) ∅

Tactic:
eqOn_empty _ _

Premises used: Set.eqOn_empty
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
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 e e' : OpenPartialHomeomorph X Y
inst_6 : (x : X) → Decidable (x ∈ e.source)
inst_7 : (y : Y) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
⊢ EqOn (↑e : X → Y) (↑e' : X → Y) ∅

Tactic:
exact eqOn_empty _ _

Premises used: Set.eqOn_empty
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f' : Y ≃ₜ Z
⊢ e.transHomeomorph f' = e.trans f'.toOpenPartialHomeomorph

Tactic:
toPartialEquiv_injective <| PartialEquiv.transEquiv_eq_trans _ _

Premises used: OpenPartialHomeomorph.toPartialEquiv_injective, PartialEquiv.transEquiv_eq_trans
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
e : OpenPartialHomeomorph X Y
f' : Y ≃ₜ Z
f'' : Z ≃ₜ Z'
⊢ (e.transHomeomorph f').transHomeomorph f'' = e.transHomeomorph (f'.trans f'')

Tactic:
simp only [transHomeomorph_eq_trans, trans_assoc, Homeomorph.trans_toOpenPartialHomeomorph]

Premises used: OpenPartialHomeomorph.trans_assoc, Homeomorph.trans_toOpenPartialHomeomorph, OpenPartialHomeomorph.transHomeomorph_eq_trans
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace Z'
e : OpenPartialHomeomorph X Y
e' : OpenPartialHomeomorph Y Z
f'' : Z ≃ₜ Z'
⊢ (e.trans e').transHomeomorph f'' = e.trans (e'.transHomeomorph f'')

Tactic:
simp only [transHomeomorph_eq_trans, trans_assoc]

Premises used: OpenPartialHomeomorph.trans_assoc, OpenPartialHomeomorph.transHomeomorph_eq_trans
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
⊢ e.subtypeRestr hs = (s.openPartialHomeomorphSubtypeCoe hs).trans e

Tactic:
rfl

Premises used: OpenPartialHomeomorph.subtypeRestr, rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
⊢ (↑(e.subtypeRestr hs) : ↥s → Y) = (↑s : Set X).restrict (π := fun (a : X) ↦ Y) (↑e : X → Y)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.subtypeRestr, OpenPartialHomeomorph.trans, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.trans', Set.restrict, rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
⊢ (e.subtypeRestr hs).source = Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' e.source

Tactic:
simp only [subtypeRestr_def, mfld_simps]

Premises used: OpenPartialHomeomorph.subtypeRestr_def
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
x : ↥s
hxe : (↑x : X) ∈ e.source
⊢ (↑e : X → Y) (↑x : X) ∈ (e.subtypeRestr hs).target

Tactic:
⟨e.map_source hxe, ?_⟩

Premises used: Set.Mem, setOf, Set.inter, OpenPartialHomeomorph.map_source, And.intro
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
x : ↥s
hxe : (↑x : X) ∈ e.source
refine : (↑e : X → Y) (↑x : X) ∈ (↑e.symm : Y → X) ⁻¹' (s.openPartialHomeomorphSubtypeCoe hs).target
⊢ (↑e : X → Y) (↑x : X) ∈ (e.subtypeRestr hs).target

Tactic:
refine ⟨e.map_source hxe, ?_⟩
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
x : ↥s
hxe : (↑x : X) ∈ e.source
rw : (↑x : X) ∈ (↑s : Set X)
⊢ (↑e : X → Y) (↑x : X) ∈ (↑e.symm : Y → X) ⁻¹' (s.openPartialHomeomorphSubtypeCoe hs).target

Tactic:
rw [s.openPartialHomeomorphSubtypeCoe_target, mem_preimage, e.leftInvOn hxe]

Premises used: OpenPartialHomeomorph.leftInvOn, TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_target, Set.mem_preimage
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
x : ↥s
hxe : (↑x : X) ∈ e.source
⊢ (↑x : X) ∈ (↑s : Set X)

Tactic:
x.prop

Premises used: Subtype.prop
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
x : ↥s
hxe : (↑x : X) ∈ e.source
⊢ (↑x : X) ∈ (↑s : Set X)

Tactic:
exact x.prop

Premises used: Subtype.prop
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
rw : (↑(e.subtypeRestr hs) : ↥s → Y) '' Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' e.source ⊆ (↑e : X → Y) '' e.source
⊢ (e.subtypeRestr hs).target ⊆ e.target

Tactic:
rw [← e.image_source_eq_target, ← OpenPartialHomeomorph.image_source_eq_target,
    e.subtypeRestr_source]

Premises used: OpenPartialHomeomorph.image_source_eq_target, OpenPartialHomeomorph.subtypeRestr_source
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
z₀ : ↥s
hz₀ : Membership.mem (γ := Set ↥s) (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' e.source) z₀
h : (↑z₀ : X) ∈ e.source ∧ (↑e : X → Y) (↑z₀ : X) = (↑(e.subtypeRestr hs) : ↥s → Y) z₀
⊢ (↑(e.subtypeRestr hs) : ↥s → Y) z₀ ∈ (↑e : X → Y) '' e.source

Tactic:
use z₀.val

Premises used: Subtype.val
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
z₀ : ↥s
hz₀ : Membership.mem (γ := Set ↥s) (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' e.source) z₀
⊢ (↑z₀ : X) ∈ e.source ∧ (↑e : X → Y) (↑z₀ : X) = (↑(e.subtypeRestr hs) : ↥s → Y) z₀

Tactic:
simpa
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
f f' : OpenPartialHomeomorph X Y
simp :
  (f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans ((s.openPartialHomeomorphSubtypeCoe hs).trans f') ≈
    (f.symm.trans f').restr (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
⊢ (f.subtypeRestr hs).symm.trans (f'.subtypeRestr hs) ≈
    (f.symm.trans f').restr (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))

Tactic:
simp only [subtypeRestr_def, trans_symm_eq_symm_trans_symm]

Premises used: OpenPartialHomeomorph.trans_symm_eq_symm_trans_symm, OpenPartialHomeomorph.subtypeRestr_def
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
f f' : OpenPartialHomeomorph X Y
⊢ IsOpen[inst_1] (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))

Tactic:
have openness₁ : IsOpen (f.target ∩ f.symm ⁻¹' s) := f.isOpen_inter_preimage_symm s.2
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst_1] (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
rw :
  ((f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans (s.openPartialHomeomorphSubtypeCoe hs)).trans f' ≈
    ((ofSet (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) openness₁).trans f.symm).trans f'
⊢ (f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans ((s.openPartialHomeomorphSubtypeCoe hs).trans f') ≈
    (f.symm.trans f').restr (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))

Tactic:
rw [← ofSet_trans _ openness₁, ← trans_assoc, ← trans_assoc]

Premises used: OpenPartialHomeomorph.trans_assoc, OpenPartialHomeomorph.ofSet_trans
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst_1] (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
⊢ ((f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans (s.openPartialHomeomorphSubtypeCoe hs)).trans f' ≈
    ((ofSet (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) openness₁).trans f.symm).trans f'

Tactic:
EqOnSource.trans' ?_ (eqOnSource_refl _)

Premises used: OpenPartialHomeomorph.EqOnSource.trans', OpenPartialHomeomorph.eqOnSource_refl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst_1] (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
refine :
  (f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans (s.openPartialHomeomorphSubtypeCoe hs) ≈
    (ofSet (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) openness₁).trans f.symm
⊢ ((f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans (s.openPartialHomeomorphSubtypeCoe hs)).trans f' ≈
    ((ofSet (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) openness₁).trans f.symm).trans f'

Tactic:
refine EqOnSource.trans' ?_ (eqOnSource_refl _)

Premises used: OpenPartialHomeomorph.EqOnSource.trans', OpenPartialHomeomorph.eqOnSource_refl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst_1] (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X))
h h₁ h₂ h₃ :
  ∀ (my_y : Y),
    my_y ∈ f.symm.source ∩ (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) ↔
      my_y ∈ f.symm.source ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)
⊢ f.symm.source ∩ (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) = f.symm.source ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)

Tactic:
mfld_set_tac