awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Opens (goal)
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (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))
V : Opens (↑Y : Type u)
t : Set (↑Y : Type u)
ht : IsOpen t
hU :
  IsOpen (X := (↑X : 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)) ⁻¹'
      t)
h :
  (Opens.map f).obj V ≤
    {
      carrier :=
        (⇑(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)) ⁻¹'
          t,
      is_open' := hU }
x : (↑Y : Type u)
hx : x ∈ V
⊢ (↑((Opens.map f).obj { carrier := V.carrier ∪ t, is_open' := ⋯ : Opens (↑Y : Type u) }) : Set (↑X : Type u)) =
    (↑{
          carrier :=
            (⇑(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)) ⁻¹'
              t,
          is_open' := hU : Opens (↑X : Type u) } :
      Set (↑X : Type u))
have mpr : Eq (α := Set (↑X : 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)) ⁻¹'
      (↑V : 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)) ⁻¹'
      t)
  ((⇑(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)) ⁻¹'
    t)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Opens (goal)
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (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))
V : Opens (↑Y : Type u)
t : Set (↑Y : Type u)
ht : IsOpen t
hU :
  IsOpen (X := (↑X : 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)) ⁻¹'
      t)
h :
  (Opens.map f).obj V ≤
    {
      carrier :=
        (⇑(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)) ⁻¹'
          t,
      is_open' := hU }
x : (↑Y : Type u)
hx : x ∈ V
⊢ Eq (α := Set (↑X : 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)) ⁻¹'
        (↑V : 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)) ⁻¹'
        t)
    ((⇑(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)) ⁻¹'
      t)
have mpr : Subset (α := Set (↑X : 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)) ⁻¹'
    (↑V : 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)) ⁻¹'
    t)
Tactic: rwa [Set.union_eq_right]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Opens (goal)
Goal:
X : TopCat
U : Opens (↑X : Type u)
⊢ ⋯.functor.obj ⊤ = U
have h : (↑(sorry.functor.obj ⊤) : Set (↑X : Type u)) = (↑U : Set (↑X : Type u))
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Opens (goal)
Goal:
X : TopCat
U : Opens (↑X : Type u)
⊢ (map U.inclusion').obj U = ⊤
have h : (↑((map U.inclusion').obj U) : Set (↑((toTopCat X).obj U) : Type u)) = (↑⊤ : Set (↑((toTopCat X).obj U) : Type u))
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Opens (goal)
Goal:
X : TopCat
⊢ IsOpenEmbedding.functor ⋯ = map (inclusionTopIso X).inv
have refine_1 : ∀ (X_1 : Opens (↑((toTopCat X).obj ⊤) : Type u_1)),
  Functor.obj (IsOpenEmbedding.functor sorry) X_1 = (map (inclusionTopIso X).inv).obj X_1
Tactic: refine CategoryTheory.Functor.ext ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Opens (goal)
Goal:
X : TopCat
refine_1 :
  ∀ (X_1 : Opens (↑((toTopCat X).obj ⊤) : Type u_1)),
    Functor.obj (IsOpenEmbedding.functor ⋯) X_1 = (map (inclusionTopIso X).inv).obj X_1
⊢ IsOpenEmbedding.functor ⋯ = map (inclusionTopIso X).inv
have refine_2 : ∀ (X_1 Y : Opens (↑((toTopCat X).obj ⊤) : Type u_1)) (f : X_1 ⟶ Y),
  Eq (α := Functor.obj (IsOpenEmbedding.functor sorry) X_1 ⟶ Functor.obj (IsOpenEmbedding.functor sorry) Y)
    (CategoryTheory.Functor.map (IsOpenEmbedding.functor sorry) f)
    (eqToHom sorry ≫ (map (inclusionTopIso X).inv).map f ≫ eqToHom sorry)
Tactic: refine CategoryTheory.Functor.ext ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Opens (goal)
Goal:
X : TopCat
U : Opens (↑((toTopCat X).obj ⊤) : Type u_1)
⊢ Functor.obj (IsOpenEmbedding.functor ⋯) U = (map (inclusionTopIso X).inv).obj U
have refine_1 : ∀ (x : (↑X : Type u_1)),
  x ∈ (↑(Functor.obj (IsOpenEmbedding.functor sorry) U) : Set (↑X : Type u_1)) ↔
    x ∈ (↑((map (inclusionTopIso X).inv).obj U) : Set (↑X : Type u_1))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Opens (goal)
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)
⊢ hf.functor.obj ((map f).obj U) = hf.functor.obj ⊤ ⊓ U
have h : ∀ (x : (↑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: ext
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Opens (goal)
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)
⊢ x ∈ (↑(hf.functor.obj ((map f).obj U)) : Set (↑Y : Type u)) ↔ x ∈ (↑(hf.functor.obj ⊤ ⊓ U) : Set (↑Y : Type u))
have h : x ∈ (↑(hf.functor.obj ((map f).obj U)) : Set (↑Y : Type u)) → x ∈ (↑(hf.functor.obj ⊤ ⊓ U) : Set (↑Y : Type u))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Opens (goal)
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))
⊢ x ∈ (↑(hf.functor.obj ((map f).obj U)) : Set (↑Y : Type u)) ↔ x ∈ (↑(hf.functor.obj ⊤ ⊓ U) : Set (↑Y : Type u))
have h₁ : x ∈ (↑(hf.functor.obj ⊤ ⊓ U) : Set (↑Y : Type u)) → x ∈ (↑(hf.functor.obj ((map f).obj U)) : Set (↑Y : Type u))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Opens (goal)
Goal:
X : TopCat
U : Opens (↑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))
have 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))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Opens (goal)
Goal:
X : TopCat
U : Opens (↑X : Type u)
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))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Opens (goal)
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))
⊢ 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))
have 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: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Opens (goal)
Goal:
X : TopCat
U : Opens (↑X : Type u)
V : Opens ↥U
⊢ ⋯.functor.obj ((map U.inclusion').obj (⋯.functor.obj V)) = ⋯.functor.obj V
have rw : sorry.functor.obj V = sorry.functor.obj V
Tactic: rw [map_functor_eq V]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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
⊢ (e.trans (ofSet s hs)).source = (e.restr ((↑e : X → Y) ⁻¹' s)).source
have rw : e.source ∩ (↑e : X → Y) ⁻¹' (ofSet s hs).source = (e.restr ((↑e : X → Y) ⁻¹' s)).source
Tactic: rw [trans_source, restr_source, ofSet_source, ← preimage_interior, hs.interior_eq]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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
⊢ (e.trans (ofSet s hs)).source = (e.restr ((↑e : X → Y) ⁻¹' s)).source
have rw₁ : e.source ∩ (↑e : X → Y) ⁻¹' (ofSet s hs).source = e.source ∩ interior ((↑e : X → Y) ⁻¹' s)
Tactic: rw [trans_source, restr_source, ofSet_source, ← preimage_interior, hs.interior_eq]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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)
⊢ (e.trans (ofSet s hs)).source = (e.restr ((↑e : X → Y) ⁻¹' s)).source
have rw₂ : e.source ∩ (↑e : X → Y) ⁻¹' s = e.source ∩ interior ((↑e : X → Y) ⁻¹' s)
Tactic: rw [trans_source, restr_source, ofSet_source, ← preimage_interior, hs.interior_eq]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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)
⊢ (e.trans (ofSet s hs)).source = (e.restr ((↑e : X → Y) ⁻¹' s)).source
have rw₃ : e.source ∩ (↑e : X → Y) ⁻¹' s = e.source ∩ (↑e : X → Y) ⁻¹' interior s
Tactic: rw [trans_source, restr_source, ofSet_source, ← preimage_interior, hs.interior_eq]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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
⊢ (e.trans (ofSet s hs)).source = (e.restr ((↑e : X → Y) ⁻¹' s)).source
have rw₄ : e.source ∩ (↑e : X → Y) ⁻¹' s = e.source ∩ (↑e : X → Y) ⁻¹' s
Tactic: rw [trans_source, restr_source, ofSet_source, ← preimage_interior, hs.interior_eq]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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
⊢ e.trans (ofSet s hs) = e.restr (e.source ∩ (↑e : X → Y) ⁻¹' s)
have rw : e.restr ((↑e : X → Y) ⁻¹' s) = e.restr (e.source ∩ (↑e : X → Y) ⁻¹' s)
Tactic: rw [trans_ofSet, restr_source_inter]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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)
⊢ e.trans (ofSet s hs) = e.restr (e.source ∩ (↑e : X → Y) ⁻¹' s)
have rw₁ : e.restr ((↑e : X → Y) ⁻¹' s) = e.restr ((↑e : X → Y) ⁻¹' s)
Tactic: rw [trans_ofSet, restr_source_inter]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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 = e.restr (e.source ∩ s)
have rw : e.restr s = e.restr (e.source ∩ s)
Tactic: rw [ofSet_trans, restr_source_inter]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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)
⊢ (ofSet s hs).trans e = e.restr (e.source ∩ s)
have rw₁ : e.restr s = e.restr s
Tactic: rw [ofSet_trans, restr_source_inter]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
s' : Set X
hs' : IsOpen[inst] s'
⊢ (ofSet s hs).trans (ofSet s' hs') = ofSet (s ∩ s') ⋯
have rw : (ofSet s hs).restr ((↑(ofSet s hs) : X → X) ⁻¹' s') = ofSet (s ∩ s') sorry
Tactic: rw [(ofSet s hs).trans_ofSet hs']
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
s' : Set X
hs' : IsOpen[inst] s'
⊢ (ofSet s hs).restr ((↑(ofSet s hs) : X → X) ⁻¹' s') = ofSet (s ∩ s') ⋯
have h : ∀ (x : X), (↑((ofSet s hs).restr ((↑(ofSet s hs) : X → X) ⁻¹' s')) : X → X) x = (↑(ofSet (s ∩ s') sorry) : X → X) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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
⊢ (ofSet s hs).restr ((↑(ofSet s hs) : X → X) ⁻¹' s') = ofSet (s ∩ s') ⋯
have hinv : ∀ (x : X),
  (↑((ofSet s hs).restr ((↑(ofSet s hs) : X → X) ⁻¹' s')).symm : X → X) x = (↑(ofSet (s ∩ s') sorry).symm : X → X) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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
⊢ (ofSet s hs).restr ((↑(ofSet s hs) : X → X) ⁻¹' s') = ofSet (s ∩ s') ⋯
have hs₁ : ∀ (x : X), x ∈ ((ofSet s hs).restr ((↑(ofSet s hs) : X → X) ⁻¹' s')).source ↔ x ∈ (ofSet (s ∩ s') sorry).source
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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)
have refine_1 : ((e.restr s).symm.trans e').source = ((e.symm.trans e').restr ((↑e : X → Y) '' s)).source
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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
refine_1 : ((e.restr s).symm.trans e').source = ((e.symm.trans e').restr ((↑e : X → Y) '' s)).source
⊢ (e.restr s).symm.trans e' ≈ (e.symm.trans e').restr ((↑e : X → Y) '' s)
have refine_2 : EqOn (↑((e.restr s).symm.trans e') : Y → Y) (↑((e.symm.trans e').restr ((↑e : X → Y) '' s)) : Y → Y)
  ((e.restr s).symm.trans e').source
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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').source = ((e.symm.trans e').restr ((↑e : X → Y) '' s)).source
have refine_1 : e.target ∩ (↑e.symm : Y → X) ⁻¹' interior s ∩ (↑e.symm : Y → X) ⁻¹' e'.source =
  e.target ∩ (↑e.symm : Y → X) ⁻¹' e'.source ∩ interior ((↑e : X → Y) '' s)
Tactic: simp only [trans_toPartialEquiv, symm_toPartialEquiv, restr_toPartialEquiv,
      PartialEquiv.trans_source, PartialEquiv.symm_source, PartialEquiv.restr_target, coe_coe_symm,
      PartialEquiv.restr_coe_symm, PartialEquiv.restr_source]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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.target ∩ (↑e.symm : Y → X) ⁻¹' interior s ∩ (↑e.symm : Y → X) ⁻¹' e'.source =
    e.target ∩ (↑e.symm : Y → X) ⁻¹' e'.source ∩ interior ((↑e : X → Y) '' s)
have refine_1 : e.target ∩ (↑e.symm : Y → X) ⁻¹' s ∩ (↑e.symm : Y → X) ⁻¹' e'.source =
  e.target ∩ (↑e.symm : Y → X) ⁻¹' e'.source ∩ (↑e : X → Y) '' s
Tactic: rw [interior_eq_iff_isOpen.mpr hs', interior_eq_iff_isOpen.mpr hs]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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.target ∩ (↑e.symm : Y → X) ⁻¹' s ∩ (↑e.symm : Y → X) ⁻¹' e'.source =
    e.target ∩ (↑e.symm : Y → X) ⁻¹' e'.source ∩ (↑e : X → Y) '' s
have refine_1 : e.target ∩ (↑e.symm : Y → X) ⁻¹' s ∩ (↑e.symm : Y → X) ⁻¹' e'.source =
  e.target ∩ (↑e : X → Y) '' s ∩ (↑e.symm : Y → X) ⁻¹' e'.source
Tactic: rw [inter_assoc, inter_assoc, inter_comm _ (e '' s), ← inter_assoc, ← inter_assoc]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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.target ∩ (↑e.symm : Y → X) ⁻¹' s ∩ (↑e.symm : Y → X) ⁻¹' e'.source =
    e.target ∩ (↑e : X → Y) '' s ∩ (↑e.symm : Y → X) ⁻¹' e'.source
have refine_1 : e.target ∩ (↑e.symm : Y → X) ⁻¹' s = e.target ∩ (↑e : X → Y) '' s
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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.target ∩ (↑e.symm : Y → X) ⁻¹' s = e.target ∩ (↑e : X → Y) '' s
have refine_1 : (↑e : X → Y) '' (e.source ∩ s) = (↑e : X → Y) '' e.source ∩ (↑e : X → Y) '' s
Tactic: rw [← image_source_inter_eq', ← image_source_eq_target]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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 : X → Y) '' (e.source ∩ s) = (↑e : X → Y) '' e.source ∩ (↑e : X → Y) '' s
have refine_1 : ∀ x ∈ s, ∀ y ∈ e.source, (↑e : X → Y) x = (↑e : X → Y) y → x = y
Tactic: refine image_inter_on ?_
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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
x : X
hx : x ∈ s
y : X
hy : y ∈ e.source
h : (↑e : X → Y) x = (↑e : X → Y) y
⊢ x = y
have refine_1 : x = (↑e.symm : Y → X) ((↑e : X → Y) y)
Tactic: rw [← left_inv e hy, ← left_inv e (hs'' hx), h]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
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
x : X
hx : x ∈ s
y : X
hy : y ∈ e.source
h : (↑e : X → Y) x = (↑e : X → Y) y
refine_1 : x = (↑e.symm : Y → X) ((↑e : X → Y) y)
⊢ x = y
have refine_1₁ : (↑e.symm : Y → X) ((↑e : X → Y) x) = (↑e.symm : Y → X) ((↑e : X → Y) y)
Tactic: rw [← left_inv e hy, ← left_inv e (hs'' hx), h]