awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
U : Opens (↑Y : Type u)
x : (↑Y : Type u)
h : x ∈ (↑(hf.functor.obj ((map f).obj U)) : Set (↑Y : Type u)) → x ∈ (↑(hf.functor.obj ⊤ ⊓ U) : Set (↑Y : Type u))
h₁ : x ∈ (↑(hf.functor.obj ⊤ ⊓ U) : Set (↑Y : Type u)) → x ∈ (↑(hf.functor.obj ((map f).obj U)) : Set (↑Y : Type u))
⊢ x ∈ (↑(hf.functor.obj ((map f).obj U)) : Set (↑Y : Type u)) ↔ x ∈ (↑(hf.functor.obj ⊤ ⊓ U) : Set (↑Y : Type u))

Tactic:
constructor
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
U : Opens (↑Y : Type u)
x : (↑X : Type u)
hx : x ∈ (↑((map f).obj U) : Set (↑X : Type u))
⊢ Membership.mem (α := (↑Y : Type u)) (↑(hf.functor.obj ⊤ ⊓ U) : Set (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))

Tactic:
⟨⟨x, trivial, rfl⟩, hx⟩

Premises used: trivial, Set.Mem, setOf, Set.inter, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
U : Opens (↑Y : Type u)
x : (↑X : Type u)
hx : x ∈ (↑((map f).obj U) : Set (↑X : Type u))
⊢ Membership.mem (α := (↑Y : Type u)) (↑(hf.functor.obj ⊤ ⊓ U) : Set (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))

Tactic:
exact ⟨⟨x, trivial, rfl⟩, hx⟩
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
U : Opens (↑Y : Type u)
x : (↑X : Type u)
hx :
  Membership.mem (α := (↑Y : Type u)) (↑U : Set (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
⊢ Membership.mem (α := (↑Y : Type u)) (↑(hf.functor.obj ((map f).obj U)) : Set (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))

Tactic:
⟨x, hx, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
U : Opens (↑Y : Type u)
x : (↑X : Type u)
hx :
  Membership.mem (α := (↑Y : Type u)) (↑U : Set (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
⊢ Membership.mem (α := (↑Y : Type u)) (↑(hf.functor.obj ((map f).obj U)) : Set (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))

Tactic:
exact ⟨x, hx, rfl⟩
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
h :
  ∀ (x : (↑X : Type u)),
    Membership.mem (γ := Set (↑X : Type u))
        (Set.range (ι := (↑((toTopCat X).obj U) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier) U.inclusion') :
            (a : (↑((toTopCat X).obj U) : Type u)) → (↑X : Type u)))
        x ↔
      x ∈ (↑U : Set (↑X : Type u))
⊢ Set.range (ι := (↑((toTopCat X).obj U) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            U.inclusion') :
        (a : (↑((toTopCat X).obj U) : Type u)) → (↑X : Type u)) =
    (↑U : Set (↑X : Type u))

Tactic:
ext x
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
x : (↑X : Type u)
h :
  Membership.mem (γ := Set (↑X : Type u))
      (Set.range (ι := (↑((toTopCat X).obj U) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              U.inclusion') :
          (a : (↑((toTopCat X).obj U) : Type u)) → (↑X : Type u)))
      x →
    x ∈ (↑U : Set (↑X : Type u))
h₁ :
  x ∈ (↑U : Set (↑X : Type u)) →
    Membership.mem (γ := Set (↑X : Type u))
      (Set.range (ι := (↑((toTopCat X).obj U) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              U.inclusion') :
          (a : (↑((toTopCat X).obj U) : Type u)) → (↑X : Type u)))
      x
⊢ Membership.mem (γ := Set (↑X : Type u))
      (Set.range (ι := (↑((toTopCat X).obj U) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              U.inclusion') :
          (a : (↑((toTopCat X).obj U) : Type u)) → (↑X : Type u)))
      x ↔
    x ∈ (↑U : Set (↑X : Type u))

Tactic:
constructor
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
x : (↑((toTopCat X).obj U) : Type u)
⊢ Membership.mem (α := (↑X : Type u)) (↑U : Set (↑X : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            U.inclusion' :
          (a : (↑((toTopCat X).obj U) : Type u)) → (↑X : Type u))
        x :
      (↑X : Type u))

Tactic:
x.2

Premises used: Set.Mem, Subtype.property
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
x : (↑((toTopCat X).obj U) : Type u)
⊢ Membership.mem (α := (↑X : Type u)) (↑U : Set (↑X : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            U.inclusion' :
          (a : (↑((toTopCat X).obj U) : Type u)) → (↑X : Type u))
        x :
      (↑X : Type u))

Tactic:
exact x.2

Premises used: Subtype.property
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
x : (↑X : Type u)
h : x ∈ (↑U : Set (↑X : Type u))
⊢ Membership.mem (γ := Set (↑X : Type u))
    (Set.range (ι := (↑((toTopCat X).obj U) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            U.inclusion') :
        (a : (↑((toTopCat X).obj U) : Type u)) → (↑X : Type u)))
    x

Tactic:
⟨⟨x, h⟩, rfl⟩

Premises used: Set.Mem, setOf, Subtype.mk, Exists.intro, Set.range, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
x : (↑X : Type u)
h : x ∈ (↑U : Set (↑X : Type u))
⊢ Membership.mem (γ := Set (↑X : Type u))
    (Set.range (ι := (↑((toTopCat X).obj U) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            U.inclusion') :
        (a : (↑((toTopCat X).obj U) : Type u)) → (↑X : Type u)))
    x

Tactic:
exact ⟨⟨x, h⟩, rfl⟩
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X U : TopCat
f : U ⟶ X
hf :
  IsOpenEmbedding (X := (↑U : Type u)) (Y := (↑X : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑U : Type u)) → (↑X : Type u))
V : Opens (↑U : Type u)
⊢ (map f).obj (hf.functor.obj V) = V

Tactic:
Opens.ext <| Set.preimage_image_eq _ hf.injective

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, TopologicalSpace.Opens.ext, Topology.IsEmbedding.injective, Set.preimage_image_eq
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
V : Opens ↥U
⊢ (map U.inclusion').obj (⋯.functor.obj V) = V

Tactic:
TopologicalSpace.Opens.map_functor_eq' _ U.isOpenEmbedding V

Premises used: TopologicalSpace.Opens.map_functor_eq', TopologicalSpace.Opens.isOpenEmbedding
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
V : Opens ↥U
rw rw₁ : ⋯.functor.obj V = ⋯.functor.obj V
⊢ ⋯.functor.obj ((map U.inclusion').obj (⋯.functor.obj V)) = ⋯.functor.obj V

Tactic:
rw [map_functor_eq V]

Premises used: TopologicalSpace.Opens.map_functor_eq
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
V : Opens ↥U
⊢ ⋯.adjunction.counit.app (⋯.functor.obj V) = eqToHom ⋯

Tactic:
subsingleton
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
e' : OpenPartialHomeomorph Y Z
⊢ (e.symm.restrOpen e'.source ⋯).symm.target = (e'.restrOpen e.target ⋯).source

Tactic:
simp [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
e' : OpenPartialHomeomorph Y Z
⊢ (e.trans e').toPartialEquiv = e.trans e'.toPartialEquiv

Tactic:
rfl

Premises used: PartialEquiv.restr, PartialEquiv.trans, PartialEquiv.symm, OpenPartialHomeomorph.toFun', PartialEquiv.IsImage.restr, PartialEquiv.trans', rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
e' : OpenPartialHomeomorph Y Z
⊢ (↑(e.trans e') : X → Z) = (↑e' : Y → Z) ∘ (↑e : X → Y)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
e' : OpenPartialHomeomorph Y Z
⊢ (↑(e.trans e').symm : Z → X) = (↑e.symm : Y → X) ∘ (↑e'.symm : Z → Y)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
e' : OpenPartialHomeomorph Y Z
x : X
⊢ (↑(e.trans e') : X → Z) x = (↑e' : Y → Z) ((↑e : X → Y) x)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.trans, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.trans', rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
e' : OpenPartialHomeomorph Y Z
⊢ (e.trans e').symm = e'.symm.trans e.symm

Tactic:
rfl

Premises used: OpenPartialHomeomorph.trans, PartialEquiv.symm, OpenPartialHomeomorph.trans', PartialEquiv.trans', rfl, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
e' : OpenPartialHomeomorph Y Z
⊢ (e.trans e').source = e.source ∩ (↑e : X → Y) ⁻¹' e'.source

Tactic:
PartialEquiv.trans_source e.toPartialEquiv e'.toPartialEquiv

Premises used: PartialEquiv.trans_source, PartialEquiv.restr, PartialEquiv.symm, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.toPartialEquiv, PartialEquiv.IsImage.restr
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
e' : OpenPartialHomeomorph Y Z
⊢ (e.trans e').source = e.source ∩ (↑e : X → Y) ⁻¹' (e.target ∩ e'.source)

Tactic:
PartialEquiv.trans_source' e.toPartialEquiv e'.toPartialEquiv

Premises used: PartialEquiv.restr, PartialEquiv.symm, PartialEquiv.trans_source', OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.toPartialEquiv, PartialEquiv.IsImage.restr
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
e' : OpenPartialHomeomorph Y Z
⊢ (e.trans e').source = (↑e.symm : Y → X) '' (e.target ∩ e'.source)

Tactic:
PartialEquiv.trans_source'' e.toPartialEquiv e'.toPartialEquiv

Premises used: PartialEquiv.restr, PartialEquiv.trans_source'', PartialEquiv.symm, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.toPartialEquiv, PartialEquiv.IsImage.restr
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
e' : OpenPartialHomeomorph Y Z
⊢ (↑e : X → Y) '' (e.trans e').source = e.target ∩ e'.source

Tactic:
PartialEquiv.image_trans_source e.toPartialEquiv e'.toPartialEquiv

Premises used: PartialEquiv.restr, PartialEquiv.image_trans_source, PartialEquiv.symm, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.toPartialEquiv, PartialEquiv.IsImage.restr
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
e' : OpenPartialHomeomorph Y Z
⊢ (e.trans e').target = e'.target ∩ (↑e'.symm : Z → Y) ⁻¹' e.target

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
e' : OpenPartialHomeomorph Y Z
⊢ (e.trans e').target = e'.target ∩ (↑e'.symm : Z → Y) ⁻¹' (e'.source ∩ e.target)

Tactic:
trans_source' e'.symm e.symm

Premises used: OpenPartialHomeomorph.trans_source', PartialEquiv.symm, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
e' : OpenPartialHomeomorph Y Z
⊢ (e.trans e').target = (↑e' : Y → Z) '' (e'.source ∩ e.target)

Tactic:
trans_source'' e'.symm e.symm

Premises used: OpenPartialHomeomorph.trans_source'', PartialEquiv.symm, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
e' : OpenPartialHomeomorph Y Z
⊢ (↑e'.symm : Z → Y) '' (e.trans e').target = e'.source ∩ e.target

Tactic:
image_trans_source e'.symm e.symm

Premises used: OpenPartialHomeomorph.image_trans_source, PartialEquiv.symm, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
e'' : OpenPartialHomeomorph Z Z'
⊢ (e.trans e').trans e'' = e.trans (e'.trans e'')

Tactic:
toPartialEquiv_injective <| e.1.trans_assoc _ _

Premises used: OpenPartialHomeomorph.toPartialEquiv_injective, OpenPartialHomeomorph.toPartialEquiv, PartialEquiv.trans_assoc
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ e.trans (OpenPartialHomeomorph.refl Y) = e

Tactic:
toPartialEquiv_injective e.1.trans_refl

Premises used: OpenPartialHomeomorph.toPartialEquiv_injective, PartialEquiv.trans_refl, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ OpenPartialHomeomorph.trans (OpenPartialHomeomorph.refl X) e = e

Tactic:
toPartialEquiv_injective e.1.refl_trans

Premises used: OpenPartialHomeomorph.toPartialEquiv_injective, OpenPartialHomeomorph.toPartialEquiv, PartialEquiv.refl_trans
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
rw : e.source ∩ (↑e : X → Y) ⁻¹' (ofSet s hs).source = (e.restr ((↑e : X → Y) ⁻¹' s)).source
rw₁ : e.source ∩ (↑e : X → Y) ⁻¹' (ofSet s hs).source = e.source ∩ interior ((↑e : X → Y) ⁻¹' s)
rw₂ : e.source ∩ (↑e : X → Y) ⁻¹' s = e.source ∩ interior ((↑e : X → Y) ⁻¹' s)
rw₃ : e.source ∩ (↑e : X → Y) ⁻¹' s = e.source ∩ (↑e : X → Y) ⁻¹' interior s
rw₄ rw₅ : e.source ∩ (↑e : X → Y) ⁻¹' s = e.source ∩ (↑e : X → Y) ⁻¹' s
⊢ (e.trans (ofSet s hs)).source = (e.restr ((↑e : X → Y) ⁻¹' s)).source

Tactic:
rw [trans_source, restr_source, ofSet_source, ← preimage_interior, hs.interior_eq]

Premises used: OpenPartialHomeomorph.ofSet_source, OpenPartialHomeomorph.preimage_interior, OpenPartialHomeomorph.trans_source, OpenPartialHomeomorph.restr_source, IsOpen.interior_eq
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
rw : e.restr ((↑e : X → Y) ⁻¹' s) = e.restr (e.source ∩ (↑e : X → Y) ⁻¹' s)
rw₁ rw₂ : e.restr ((↑e : X → Y) ⁻¹' s) = e.restr ((↑e : X → Y) ⁻¹' s)
⊢ e.trans (ofSet s hs) = e.restr (e.source ∩ (↑e : X → Y) ⁻¹' s)

Tactic:
rw [trans_ofSet, restr_source_inter]

Premises used: OpenPartialHomeomorph.restr_source_inter, OpenPartialHomeomorph.trans_ofSet
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
⊢ ((ofSet s hs).trans e).source = (e.restr s).source

Tactic:
simp [hs.interior_eq, inter_comm]

Premises used: Set.inter_comm, IsOpen.interior_eq
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
rw : e.restr s = e.restr (e.source ∩ s)
rw₁ rw₂ : e.restr s = e.restr s
⊢ (ofSet s hs).trans e = e.restr (e.source ∩ s)

Tactic:
rw [ofSet_trans, restr_source_inter]

Premises used: OpenPartialHomeomorph.restr_source_inter, OpenPartialHomeomorph.ofSet_trans
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
s' : Set X
hs' : IsOpen[inst] s'
rw : (ofSet s hs).restr ((↑(ofSet s hs) : X → X) ⁻¹' s') = ofSet (s ∩ s') ⋯
⊢ (ofSet s hs).trans (ofSet s' hs') = ofSet (s ∩ s') ⋯

Tactic:
rw [(ofSet s hs).trans_ofSet hs']

Premises used: OpenPartialHomeomorph.ofSet, OpenPartialHomeomorph.trans_ofSet
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
s' : Set X
hs' : IsOpen[inst] s'
h : ∀ (x : X), (↑((ofSet s hs).restr ((↑(ofSet s hs) : X → X) ⁻¹' s')) : X → X) x = (↑(ofSet (s ∩ s') ⋯) : X → X) x
hinv :
  ∀ (x : X),
    (↑((ofSet s hs).restr ((↑(ofSet s hs) : X → X) ⁻¹' s')).symm : X → X) x = (↑(ofSet (s ∩ s') ⋯).symm : X → X) x
hs₁ : ∀ (x : X), x ∈ ((ofSet s hs).restr ((↑(ofSet s hs) : X → X) ⁻¹' s')).source ↔ x ∈ (ofSet (s ∩ s') ⋯).source
⊢ (ofSet s hs).restr ((↑(ofSet s hs) : X → X) ⁻¹' s') = ofSet (s ∩ s') ⋯

Tactic:
ext
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
s' : Set X
hs' : IsOpen[inst] s'
x : X
⊢ (↑((ofSet s hs).restr ((↑(ofSet s hs) : X → X) ⁻¹' s')) : X → X) x = (↑(ofSet (s ∩ s') ⋯) : X → X) x

Tactic:
simp [hs'.interior_eq]

Premises used: IsOpen.interior_eq
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
s' : Set X
hs' : IsOpen[inst] s'
x : X
⊢ (↑((ofSet s hs).restr ((↑(ofSet s hs) : X → X) ⁻¹' s')).symm : X → X) x = (↑(ofSet (s ∩ s') ⋯).symm : X → X) x

Tactic:
simp [hs'.interior_eq]

Premises used: IsOpen.interior_eq
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
s' : Set X
hs' : IsOpen[inst] s'
x : X
⊢ x ∈ ((ofSet s hs).restr ((↑(ofSet s hs) : X → X) ⁻¹' s')).source ↔ x ∈ (ofSet (s ∩ s') ⋯).source

Tactic:
simp [hs'.interior_eq]

Premises used: IsOpen.interior_eq
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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
e' : OpenPartialHomeomorph Y Z
s : Set X
⊢ (e.restr s).trans e' = (e.trans e').restr s

Tactic:
toPartialEquiv_injective <|
    PartialEquiv.restr_trans e.toPartialEquiv e'.toPartialEquiv (interior s)

Premises used: OpenPartialHomeomorph.toPartialEquiv_injective, interior, OpenPartialHomeomorph.toPartialEquiv, PartialEquiv.restr_trans
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
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 e' : OpenPartialHomeomorph X Y
f f' : OpenPartialHomeomorph Y Z
he : e ≈ e'
hf : f ≈ f'
⊢ e.trans f ≈ e'.trans f'

Tactic:
PartialEquiv.EqOnSource.trans' he hf

Premises used: PartialEquiv.restr, PartialEquiv.symm, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.EqOnSource, PartialEquiv.EqOnSource.trans', PartialEquiv.IsImage.restr
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ e.trans e.symm ≈ ofSet e.source ⋯

Tactic:
PartialEquiv.self_trans_symm _

Premises used: PartialEquiv.restr, PartialEquiv.symm, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.EqOnSource, PartialEquiv.IsImage.restr, PartialEquiv.self_trans_symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ e.symm.trans e ≈ ofSet e.target ⋯

Tactic:
e.symm.self_trans_symm

Premises used: OpenPartialHomeomorph.self_trans_symm, PartialEquiv.symm, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Composition
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
hs' : IsOpen[inst_1] ((↑e : X → Y) '' s)
hs'' : s ⊆ e.source
⊢ (e.restr s).symm.trans e' ≈ (e.symm.trans e').restr ((↑e : X → Y) '' s)

Tactic:
⟨?_, ?_⟩

Premises used: OpenPartialHomeomorph.EqOnSource, And.intro