awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.source ∩ (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) = f.symm.source ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)

Tactic:
have set_identity : f.symm.source ∩ (f.target ∩ f.symm ⁻¹' s) = f.symm.source ∩ f.symm ⁻¹' s := by
    mfld_set_tac
-- 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))
set_identity :
  f.symm.source ∩ (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) = f.symm.source ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)
⊢ IsOpen[inst] (↑s : Set X)

Tactic:
have openness₂ : IsOpen (s : Set X) := 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))
set_identity :
  f.symm.source ∩ (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) = f.symm.source ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)
openness₂ : IsOpen[inst] (↑s : Set X)
rw :
  f.symm.trans ((s.openPartialHomeomorphSubtypeCoe hs).symm.trans (s.openPartialHomeomorphSubtypeCoe hs)) ≈
    f.symm.trans (ofSet (↑s : Set X) openness₂)
⊢ (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

Tactic:
rw [ofSet_trans', set_identity, ← trans_of_set' _ openness₂, trans_assoc]

Premises used: OpenPartialHomeomorph.ofSet_trans', OpenPartialHomeomorph.trans_assoc, OpenPartialHomeomorph.trans_of_set'
-- 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))
set_identity :
  f.symm.source ∩ (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) = f.symm.source ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)
openness₂ : IsOpen[inst] (↑s : Set X)
⊢ f.symm.trans ((s.openPartialHomeomorphSubtypeCoe hs).symm.trans (s.openPartialHomeomorphSubtypeCoe hs)) ≈
    f.symm.trans (ofSet (↑s : Set X) openness₂)

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))
set_identity :
  f.symm.source ∩ (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) = f.symm.source ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)
openness₂ : IsOpen[inst] (↑s : Set X)
refine :
  (s.openPartialHomeomorphSubtypeCoe hs).symm.trans (s.openPartialHomeomorphSubtypeCoe hs) ≈
    ofSet (↑s : Set X) openness₂
⊢ f.symm.trans ((s.openPartialHomeomorphSubtypeCoe hs).symm.trans (s.openPartialHomeomorphSubtypeCoe hs)) ≈
    f.symm.trans (ofSet (↑s : Set X) openness₂)

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))
set_identity :
  f.symm.source ∩ (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) = f.symm.source ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)
openness₂ : IsOpen[inst] (↑s : Set X)
⊢ (s.openPartialHomeomorphSubtypeCoe hs).symm.trans (s.openPartialHomeomorphSubtypeCoe hs) ≈
    ofSet (↑s : Set X) openness₂

Tactic:
Setoid.trans (symm_trans_self (s.openPartialHomeomorphSubtypeCoe hs)) ?_

Premises used: TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe, OpenPartialHomeomorph.symm_trans_self, Setoid.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))
set_identity :
  f.symm.source ∩ (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) = f.symm.source ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)
openness₂ : IsOpen[inst] (↑s : Set X)
refine : ofSet (s.openPartialHomeomorphSubtypeCoe hs).target ⋯ ≈ ofSet (↑s : Set X) openness₂
⊢ (s.openPartialHomeomorphSubtypeCoe hs).symm.trans (s.openPartialHomeomorphSubtypeCoe hs) ≈
    ofSet (↑s : Set X) openness₂

Tactic:
refine Setoid.trans (symm_trans_self (s.openPartialHomeomorphSubtypeCoe hs)) ?_

Premises used: TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe, OpenPartialHomeomorph.symm_trans_self, Setoid.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))
set_identity :
  f.symm.source ∩ (f.target ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)) = f.symm.source ∩ (↑f.symm : Y → X) ⁻¹' (↑s : Set X)
openness₂ : IsOpen[inst] (↑s : Set X)
⊢ ofSet (s.openPartialHomeomorphSubtypeCoe hs).target ⋯ ≈ ofSet (↑s : Set X) openness₂

Tactic:
simp only [mfld_simps, Setoid.refl]

Premises used: Setoid.refl
-- 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
U : Opens X
hU : Nonempty.{u_1 + 1} ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
rw : (↑e : X → Y) ((Subtype.val (p := fun (x : X) ↦ x ∈ U) ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) y) = y
rw₁ : (Subtype.val (p := fun (x : X) ↦ x ∈ U) ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) y ∈ e.source
⊢ (Subtype.val (p := fun (x : X) ↦ x ∈ U) ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) y = (↑e.symm : Y → X) y

Tactic:
rw [e.eq_symm_apply _ hy.1]

Premises used: And.left, OpenPartialHomeomorph.eq_symm_apply
-- 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
U : Opens X
hU : Nonempty.{u_1 + 1} ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
change : (↑U : Set X).restrict (π := fun (a : X) ↦ Y) (↑e : X → Y) ((↑(e.subtypeRestr hU).symm : Y → ↥U) y) = y
⊢ (↑e : X → Y) ((Subtype.val (p := fun (x : X) ↦ x ∈ U) ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) y) = y

Tactic:
change restrict _ e _ = _

Premises used: OpenPartialHomeomorph.toFun', Set.restrict
-- 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
U : Opens X
hU : Nonempty.{u_1 + 1} ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
rw : (↑(e.subtypeRestr hU) : ↥U → Y) ((↑(e.subtypeRestr hU).symm : Y → ↥U) y) = y
rw₁ rw₂ : y = y
⊢ (↑U : Set X).restrict (π := fun (a : X) ↦ Y) (↑e : X → Y) ((↑(e.subtypeRestr hU).symm : Y → ↥U) y) = y

Tactic:
rw [← e.subtypeRestr_coe hU, (e.subtypeRestr hU).right_inv hy]

Premises used: OpenPartialHomeomorph.subtypeRestr_coe, OpenPartialHomeomorph.subtypeRestr, OpenPartialHomeomorph.right_inv
-- 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
U : Opens X
hU : Nonempty.{u_1 + 1} ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ (↑(e.subtypeRestr hU).symm : Y → ↥U) y ∈ (e.subtypeRestr hU).source

Tactic:
have := OpenPartialHomeomorph.map_target _ hy
-- 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
U : Opens X
hU : Nonempty.{u_1 + 1} ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
this : (↑(e.subtypeRestr hU).symm : Y → ↥U) y ∈ (e.subtypeRestr hU).source
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      Membership.mem (γ := Set ↥U) (Subtype.val (p := fun (x : X) ↦ x ∈ U) ⁻¹' e.source)
        ((↑(e.subtypeRestr hU).symm : Y → ↥U) y)),
    (Subtype.val (p := fun (x : X) ↦ x ∈ U) ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) y ∈ e.source
⊢ (Subtype.val (p := fun (x : X) ↦ x ∈ U) ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) y ∈ e.source

Tactic:
rwa [e.subtypeRestr_source] at this

Premises used: 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
U : Opens X
hU : Nonempty.{u_1 + 1} ↥U
⊢ EqOn (↑e.symm : Y → X) (Subtype.val (p := fun (x : X) ↦ x ∈ U) ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U))
    (e.subtypeRestr hU).target

Tactic:
fun _y hy ↦ (e.subtypeRestr_symm_apply hU hy).symm

Premises used: Set.EqOn, OpenPartialHomeomorph.subtypeRestr_symm_apply, Eq.symm
-- 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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
set :
  let i := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV;
  EqOn (↑(e.subtypeRestr hV).symm : Y → ↥V) (i ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) (e.subtypeRestr hU).target
⊢ EqOn (↑(e.subtypeRestr hV).symm : Y → ↥V)
    (inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U))
    (e.subtypeRestr hU).target

Tactic:
set i := Set.inclusion hUV

Premises used: Set.inclusion
-- 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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ (e.subtypeRestr hU).target
dsimp :
  (↑(V.openPartialHomeomorphSubtypeCoe hV).symm : X → ↥V) ((↑e.symm : Y → X) y) =
    i ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y))
⊢ (↑(e.subtypeRestr hV).symm : Y → ↥V) y = (i ∘ (↑(e.subtypeRestr hU).symm : Y → ↥U)) y

Tactic:
dsimp [OpenPartialHomeomorph.subtypeRestr_def] at hy ⊢

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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
rw : ∀ (hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (↑U : Set X)), (↑e.symm : Y → X) y ∈ (↑V : Set X)
⊢ (↑e.symm : Y → X) y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target

Tactic:
rw [Opens.openPartialHomeomorphSubtypeCoe_target] at hy ⊢

Premises used: TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_target
-- 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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (↑U : Set X)
⊢ (↑e.symm : Y → X) y ∈ (↑V : Set X)

Tactic:
hUV hy.2

Premises used: And.right
-- 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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (↑U : Set X)
⊢ (↑e.symm : Y → X) y ∈ (↑V : Set X)

Tactic:
exact hUV hy.2

Premises used: And.right
-- 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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
⊢ (↑e.symm : Y → X) y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target

Tactic:
have hyV : e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target := by
    rw [Opens.openPartialHomeomorphSubtypeCoe_target] at hy ⊢
    exact hUV hy.2
-- 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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : (↑e.symm : Y → X) y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ (↑(V.openPartialHomeomorphSubtypeCoe hV).symm : X → ↥V) ((↑e.symm : Y → X) y) =
    i ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y))

Tactic:
(V.openPartialHomeomorphSubtypeCoe hV).injOn ?_ trivial ?_

Premises used: trivial, TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe, OpenPartialHomeomorph.injOn
-- 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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : (↑e.symm : Y → X) y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
refine_1 :
  (↑(V.openPartialHomeomorphSubtypeCoe hV).symm : X → ↥V) ((↑e.symm : Y → X) y) ∈
    (V.openPartialHomeomorphSubtypeCoe hV).source
refine_2 :
  (↑(V.openPartialHomeomorphSubtypeCoe hV) : ↥V → X)
      ((↑(V.openPartialHomeomorphSubtypeCoe hV).symm : X → ↥V) ((↑e.symm : Y → X) y)) =
    (↑(V.openPartialHomeomorphSubtypeCoe hV) : ↥V → X)
      (i ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y)))
⊢ (↑(V.openPartialHomeomorphSubtypeCoe hV).symm : X → ↥V) ((↑e.symm : Y → X) y) =
    i ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y))

Tactic:
refine (V.openPartialHomeomorphSubtypeCoe hV).injOn ?_ trivial ?_

Premises used: trivial, TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe, OpenPartialHomeomorph.injOn
-- 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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : (↑e.symm : Y → X) y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ (↑(V.openPartialHomeomorphSubtypeCoe hV).symm : X → ↥V) ((↑e.symm : Y → X) y) ∈
    (V.openPartialHomeomorphSubtypeCoe hV).source

Tactic:
simp
-- 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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : (↑e.symm : Y → X) y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
refine_2 :
  (↑e.symm : Y → X) y =
    (↑(V.openPartialHomeomorphSubtypeCoe hV) : ↥V → X)
      (i ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y)))
⊢ (↑(V.openPartialHomeomorphSubtypeCoe hV) : ↥V → X)
      ((↑(V.openPartialHomeomorphSubtypeCoe hV).symm : X → ↥V) ((↑e.symm : Y → X) y)) =
    (↑(V.openPartialHomeomorphSubtypeCoe hV) : ↥V → X)
      (i ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y)))

Tactic:
rw [(V.openPartialHomeomorphSubtypeCoe hV).right_inv hyV]

Premises used: TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe, OpenPartialHomeomorph.right_inv
-- 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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : (↑e.symm : Y → X) y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
refine_2 :
  (↑e.symm : Y → X) y =
    (↑(U.openPartialHomeomorphSubtypeCoe hU) : ↥U → X)
      ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y))
⊢ (↑e.symm : Y → X) y =
    (↑(V.openPartialHomeomorphSubtypeCoe hV) : ↥V → X)
      (i ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y)))

Tactic:
change _ = U.openPartialHomeomorphSubtypeCoe hU _

Premises used: TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe, OpenPartialHomeomorph.toFun'
-- 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
U V : Opens X
hU : Nonempty.{u_1 + 1} ↥U
hV : Nonempty.{u_1 + 1} ↥V
hUV : U ≤ V
i : (↑(↑U : Set X) : Type u_1) → (↑(↑V : Set X) : Type u_1) := inclusion (s := (↑U : Set X)) (t := (↑V : Set X)) hUV
y : Y
hy : y ∈ e.target ∩ (↑e.symm : Y → X) ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : (↑e.symm : Y → X) y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
refine_2 refine_2₁ : (↑e.symm : Y → X) y = (↑e.symm : Y → X) y
⊢ (↑e.symm : Y → X) y =
    (↑(U.openPartialHomeomorphSubtypeCoe hU) : ↥U → X)
      ((↑(U.openPartialHomeomorphSubtypeCoe hU).symm : X → ↥U) ((↑e.symm : Y → X) y))

Tactic:
rw [(U.openPartialHomeomorphSubtypeCoe hU).right_inv hy.2]

Premises used: TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe, And.right, OpenPartialHomeomorph.right_inv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
rw : (↑e : X → Z) x₀ ∈ e.target
⊢ extend f (↑e : X → Z) (fun (x : X') ↦ Classical.arbitrary Z) x ∈ e.target

Tactic:
rw [← hxx₀, hf.injective.extend_apply e]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, OpenPartialHomeomorph.toFun', Function.Injective.extend_apply, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ (↑e : X → Z) x₀ ∈ e.target

Tactic:
e.map_source' hx₀

Premises used: PartialEquiv.map_source', Set.Mem, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ (↑e : X → Z) x₀ ∈ e.target

Tactic:
exact e.map_source' hx₀

Premises used: PartialEquiv.map_source', OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
this :
  ∀ (x₀ : X) (hx₀ : x₀ ∈ e.source) (hxx₀ : f x₀ = x),
    (f ∘ e.invFun) (extend f (↑e : X → Z) (fun (x : X') ↦ Classical.arbitrary Z) x) = x
⊢ x ∈ f '' e.source → (f ∘ e.invFun) (extend f (↑e : X → Z) (fun (x : X') ↦ Classical.arbitrary Z) x) = x

Tactic:
⟨x₀, hx₀, hxx₀⟩
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions
Goal:
X_1 : Type u_1
X'_1 : Type u_2
Y : Type u_3
Y' : Type u_4
Z_1 : Type u_5
Z' : Type u_6
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace X'_1
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z_1
inst_5 : TopologicalSpace Z'
e_1 : OpenPartialHomeomorph X_1 Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst_6 : TopologicalSpace X
inst_7 : TopologicalSpace X'
inst_8 : TopologicalSpace Z
inst_9 : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
rw : f (e.invFun ((↑e : X → Z) x₀)) = f x₀
⊢ (f ∘ e.invFun) (extend f (↑e : X → Z) (fun (x : X') ↦ Classical.arbitrary Z) x) = x

Tactic:
rw [← hxx₀, hf.injective.extend_apply e, comp_apply]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, OpenPartialHomeomorph.toFun', Function.Injective.extend_apply, Topology.IsEmbedding.injective, Function.comp_apply