awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set (↑(ofOpenSubsets U).glued : Type u)
hs :
  ∀ (i : (ofOpenSubsets U).J),
    IsOpen (X := (↑((ofOpenSubsets U).U i) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i)) :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u)) ⁻¹'
        s)
i : (ofOpenSubsets U).J
x : (↑(of α) : Type u)
hx' : x ∈ U i
hx :
  Membership.mem (α := (↑(ofOpenSubsets U).glued : Type u)) s
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
        (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx') :
      (↑(ofOpenSubsets U).glued : Type u))
⊢ Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(of α) : Type u))
    (Set.range (ι := (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            Functor.obj (Opens.toTopCat (of α)) (U i)) (U i).inclusion') :
        (a : (↑((Opens.toTopCat (of α)).obj (U i)) : Type u)) → (↑(of α) : Type u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
              (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
            (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx') :
          (↑(ofOpenSubsets U).glued : Type u)) :
      (↑(of α) : Type u))
have right : Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(of α) : Type u))
  (Set.range (ι := (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          Functor.obj (Opens.toTopCat (of α)) (U i)) (U i).inclusion') :
      (a : (↑((Opens.toTopCat (of α)).obj (U i)) : Type u)) → (↑(of α) : Type u)))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          (ofOpenSubsets U).U i) (U i).inclusion' :
        (a : (↑((ofOpenSubsets U).U i) : Type u)) → α)
      (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx') :
    α)
Tactic: rw [ι_fromOpenSubsetsGlue_apply]
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
⊢ Eq (α := Set (↑(of α) : Type u))
    (Set.range (ι := (↑(ofOpenSubsets U).glued : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U)) :
        (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)))
    (⋃ (i : J), (↑(U i) : Set α))
have h : ∀ (x : (↑(of α) : Type u)),
  Membership.mem (γ := Set (↑(of α) : Type u))
      (Set.range (ι := (↑(ofOpenSubsets U).glued : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (fromOpenSubsetsGlue U)) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)))
      x ↔
    Membership.mem (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
x : (↑(of α) : Type u)
⊢ Membership.mem (γ := Set (↑(of α) : Type u))
      (Set.range (ι := (↑(ofOpenSubsets U).glued : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (fromOpenSubsetsGlue U)) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)))
      x ↔
    Membership.mem (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α)) x
have h : Membership.mem (γ := Set (↑(of α) : Type u))
    (Set.range (ι := (↑(ofOpenSubsets U).glued : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U)) :
        (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)))
    x →
  Membership.mem (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
x : (↑(of α) : Type u)
h :
  Membership.mem (γ := Set (↑(of α) : Type u))
      (Set.range (ι := (↑(ofOpenSubsets U).glued : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (fromOpenSubsetsGlue U)) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)))
      x →
    Membership.mem (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α)) x
⊢ Membership.mem (γ := Set (↑(of α) : Type u))
      (Set.range (ι := (↑(ofOpenSubsets U).glued : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (fromOpenSubsetsGlue U)) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)))
      x ↔
    Membership.mem (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α)) x
have h₁ : Membership.mem (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α)) x →
  Membership.mem (γ := Set (↑(of α) : Type u))
    (Set.range (ι := (↑(ofOpenSubsets U).glued : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U)) :
        (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)))
    x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
x : (↑(ofOpenSubsets U).glued : Type u)
⊢ Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
        x :
      (↑(of α) : Type u))
have h : ∀ (i : (ofOpenSubsets U).J) (x : (↑(of α) : Type u)) (hx' : x ∈ U i),
  Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
              (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
            (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx') :
          (↑(ofOpenSubsets U).glued : Type u)) :
      (↑(of α) : Type u))
Tactic: obtain ⟨i, ⟨x, hx'⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : (↑(of α) : Type u)
hx' : x ∈ U i
⊢ Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
              (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
            (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx') :
          (↑(ofOpenSubsets U).glued : Type u)) :
      (↑(of α) : Type u))
have h : Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          (ofOpenSubsets U).U i) (U i).inclusion' :
        (a : (↑((ofOpenSubsets U).U i) : Type u)) → α)
      (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx') :
    α)
Tactic: rw [ι_fromOpenSubsetsGlue_apply]
-- Lean 4 proof step from Mathlib.Topology.Hom.Open (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f g : α →CO β
h : Eq (α := (a : α) → β) ((fun (f : α →CO β) ↦ f.toFun) f) ((fun (f : α →CO β) ↦ f.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : α → β) (continuous_toFun : Continuous toFun)
  (map_open' : IsOpenMap { toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : α →CO β) ↦ f.toFun) { toFun := toFun, continuous_toFun := continuous_toFun, map_open' := map_open' })
      ((fun (f : α →CO β) ↦ f.toFun) g)),
  { toFun := toFun, continuous_toFun := continuous_toFun, map_open' := map_open' : α →CO β } = g
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.Hom.Open (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
g : α →CO β
toFun : α → β
continuous_toFun : Continuous toFun
map_open' : IsOpenMap { toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →CO β) ↦ f.toFun) { toFun := toFun, continuous_toFun := continuous_toFun, map_open' := map_open' })
    ((fun (f : α →CO β) ↦ f.toFun) g)
⊢ { toFun := toFun, continuous_toFun := continuous_toFun, map_open' := map_open' : α →CO β } = g
have obtain : ∀ (toFun_1 : α → β) (continuous_toFun_1 : Continuous toFun_1)
  (map_open'_1 : IsOpenMap { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : C(α, β) }.toFun)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : α →CO β) ↦ f.toFun) { toFun := toFun, continuous_toFun := continuous_toFun, map_open' := map_open' })
      ((fun (f : α →CO β) ↦ f.toFun)
        { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_open' := map_open'_1 })),
  { toFun := toFun, continuous_toFun := continuous_toFun, map_open' := map_open' : α →CO β } =
    { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_open' := map_open'_1 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Topology.Hom.Open (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : β →CO γ
f₁ f₂ : α →CO β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Hom.Open (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : β →CO γ
f₁ f₂ : α →CO β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Hom.Open (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : β →CO γ
f₁ f₂ : α →CO β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ h.trans h.symm = Homeomorph.refl X
have H : ∀ (x : X), Eq (α := X) ((h.trans h.symm : (a : X) → X) x : X) ((Homeomorph.refl X : (a : X) → X) x : X)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ h.symm.trans h = Homeomorph.refl Y
have H : ∀ (x : Y), Eq (α := Y) ((h.symm.trans h : (a : Y) → Y) x : Y) ((Homeomorph.refl Y : (a : Y) → Y) x : Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ IsOpen[inst_1] ((⇑h : (a : X) → Y) '' s) ↔ IsOpen[inst] s
have rw : IsOpen[inst_1] ((⇑h.symm : (a : Y) → X) ⁻¹' s) ↔ IsOpen[inst] s
Tactic: rw [← preimage_symm, isOpen_preimage]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
rw : IsOpen[inst_1] ((⇑h.symm : (a : Y) → X) ⁻¹' s) ↔ IsOpen[inst] s
⊢ IsOpen[inst_1] ((⇑h : (a : X) → Y) '' s) ↔ IsOpen[inst] s
have rw₁ : IsOpen[inst] s ↔ IsOpen[inst] s
Tactic: rw [← preimage_symm, isOpen_preimage]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ IsClosed[inst_1] ((⇑h : (a : X) → Y) '' s) ↔ IsClosed[inst] s
have rw : IsClosed[inst_1] ((⇑h.symm : (a : Y) → X) ⁻¹' s) ↔ IsClosed[inst] s
Tactic: rw [← preimage_symm, isClosed_preimage]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
rw : IsClosed[inst_1] ((⇑h.symm : (a : Y) → X) ⁻¹' s) ↔ IsClosed[inst] s
⊢ IsClosed[inst_1] ((⇑h : (a : X) → Y) '' s) ↔ IsClosed[inst] s
have rw₁ : IsClosed[inst] s ↔ IsClosed[inst] s
Tactic: rw [← preimage_symm, isClosed_preimage]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ Eq.{u_2 + 1} (α := Set Y) ((⇑h : (a : X) → Y) '' closure[inst] s) (closure[inst_1] ((⇑h : (a : X) → Y) '' s))
have rw : Eq.{u_2 + 1} (α := Set Y) ((⇑h.symm : (a : Y) → X) ⁻¹' closure[inst] s)
  (closure[inst_1] ((⇑h.symm : (a : Y) → X) ⁻¹' s))
Tactic: rw [← preimage_symm, preimage_closure]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
rw :
  Eq.{u_2 + 1} (α := Set Y) ((⇑h.symm : (a : Y) → X) ⁻¹' closure[inst] s)
    (closure[inst_1] ((⇑h.symm : (a : Y) → X) ⁻¹' s))
⊢ Eq.{u_2 + 1} (α := Set Y) ((⇑h : (a : X) → Y) '' closure[inst] s) (closure[inst_1] ((⇑h : (a : X) → Y) '' s))
have rw₁ : Eq.{u_2 + 1} (α := Set Y) (closure[inst_1] ((⇑h.symm : (a : Y) → X) ⁻¹' s))
  (closure[inst_1] ((⇑h.symm : (a : Y) → X) ⁻¹' s))
Tactic: rw [← preimage_symm, preimage_closure]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ Eq.{u_2 + 1} (α := Set Y) ((⇑h : (a : X) → Y) '' interior s) (interior ((⇑h : (a : X) → Y) '' s))
have rw : Eq.{u_2 + 1} (α := Set Y) ((⇑h.symm : (a : Y) → X) ⁻¹' interior s) (interior ((⇑h.symm : (a : Y) → X) ⁻¹' s))
Tactic: rw [← preimage_symm, preimage_interior]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
rw : Eq.{u_2 + 1} (α := Set Y) ((⇑h.symm : (a : Y) → X) ⁻¹' interior s) (interior ((⇑h.symm : (a : Y) → X) ⁻¹' s))
⊢ Eq.{u_2 + 1} (α := Set Y) ((⇑h : (a : X) → Y) '' interior s) (interior ((⇑h : (a : X) → Y) '' s))
have rw₁ : Eq.{u_2 + 1} (α := Set Y) (interior ((⇑h.symm : (a : Y) → X) ⁻¹' s)) (interior ((⇑h.symm : (a : Y) → X) ⁻¹' s))
Tactic: rw [← preimage_symm, preimage_interior]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ Eq.{u_2 + 1} (α := Set Y) ((⇑h : (a : X) → Y) '' frontier s) (frontier ((⇑h : (a : X) → Y) '' s))
have rw : Eq.{u_2 + 1} (α := Set Y) ((⇑h.symm : (a : Y) → X) ⁻¹' frontier s) (frontier ((⇑h.symm : (a : Y) → X) ⁻¹' s))
Tactic: rw [← preimage_symm, preimage_frontier]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
rw : Eq.{u_2 + 1} (α := Set Y) ((⇑h.symm : (a : Y) → X) ⁻¹' frontier s) (frontier ((⇑h.symm : (a : Y) → X) ⁻¹' s))
⊢ Eq.{u_2 + 1} (α := Set Y) ((⇑h : (a : X) → Y) '' frontier s) (frontier ((⇑h : (a : X) → Y) '' s))
have rw₁ : Eq.{u_2 + 1} (α := Set Y) (frontier ((⇑h.symm : (a : Y) → X) ⁻¹' s)) (frontier ((⇑h.symm : (a : Y) → X) ⁻¹' s))
Tactic: rw [← preimage_symm, preimage_frontier]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
⊢ IsOpenMap.{u_4, u_2} (Y := Y) ((⇑h : (a : X) → Y) ∘ f) ↔ IsOpenMap f
have refine : IsOpenMap.{u_4, u_2} (Y := Y) ((⇑h : (a : X) → Y) ∘ f) → IsOpenMap f
Tactic: refine ⟨?_, fun hf => h.isOpenMap.comp hf⟩
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
hf : IsOpenMap.{u_4, u_2} (Y := Y) ((⇑h : (a : X) → Y) ∘ f)
⊢ IsOpenMap f
have rw : IsOpenMap.{u_4, u_1} (Y := X)
  (Function.comp.{u_4 + 1, u_2 + 1, u_1 + 1} (β := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) ∘ f))
Tactic: rw [← Function.id_comp f, ← h.symm_comp_self, Function.comp_assoc]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
⊢ IsOpenMap.{u_1, u_4} (X := X) (f ∘ (⇑h : (a : X) → Y)) ↔ IsOpenMap f
have refine : IsOpenMap.{u_1, u_4} (X := X) (f ∘ (⇑h : (a : X) → Y)) → IsOpenMap f
Tactic: refine ⟨?_, fun hf => hf.comp h.isOpenMap⟩
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
hf : IsOpenMap.{u_1, u_4} (X := X) (f ∘ (⇑h : (a : X) → Y))
⊢ IsOpenMap f
have rw : IsOpenMap.{u_2, u_4} (X := Y)
  (Function.comp.{u_2 + 1, u_1 + 1, u_4 + 1} (β := X) (f ∘ (⇑h : (a : X) → Y)) (⇑h.symm : (a : Y) → X))
Tactic: rw [← Function.comp_id f, ← h.self_comp_symm, ← Function.comp_assoc]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ map.{u_2, u_1} (α := Y) ((⇑h.symm : (a : Y) → X) : (a : Y) → X) (𝓝 ((h : (a : X) → Y) x) : Filter Y) = 𝓝 x
have rw : 𝓝 ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) = 𝓝 x
Tactic: rw [h.symm.map_nhds_eq, h.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
x : X
rw : 𝓝 ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) = 𝓝 x
⊢ map.{u_2, u_1} (α := Y) ((⇑h.symm : (a : Y) → X) : (a : Y) → X) (𝓝 ((h : (a : X) → Y) x) : Filter Y) = 𝓝 x
have rw₁ : 𝓝 x = 𝓝 x
Tactic: rw [h.symm.map_nhds_eq, h.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
y : Y
⊢ Eq.{u_1 + 1} (α := Filter X) (comap (⇑h : (a : X) → Y) (𝓝 y) : Filter X) (𝓝 ((h.symm : (a : Y) → X) y) : Filter X)
have rw : Eq.{u_1 + 1} (α := Filter X) (comap (⇑h : (a : X) → Y) (𝓝 y))
  (comap.{u_1, u_2} (β := Y) ((⇑h : (a : X) → Y) : (a : X) → Y)
    (𝓝 ((h : (a : X) → Y) ((h.symm : (a : Y) → X) y : X)) : Filter Y))
Tactic: rw [h.nhds_eq_comap, h.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
y : Y
rw :
  Eq.{u_1 + 1} (α := Filter X) (comap (⇑h : (a : X) → Y) (𝓝 y))
    (comap.{u_1, u_2} (β := Y) ((⇑h : (a : X) → Y) : (a : X) → Y)
      (𝓝 ((h : (a : X) → Y) ((h.symm : (a : Y) → X) y : X)) : Filter Y))
⊢ Eq.{u_1 + 1} (α := Filter X) (comap (⇑h : (a : X) → Y) (𝓝 y) : Filter X) (𝓝 ((h.symm : (a : Y) → X) y) : Filter X)
have rw₁ : Eq.{u_1 + 1} (α := Filter X) (comap (⇑h : (a : X) → Y) (𝓝 y)) (comap (⇑h : (a : X) → Y) (𝓝 y))
Tactic: rw [h.nhds_eq_comap, h.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_2
W : Type u_3
Z_1 : Type u_4
Z : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
e : X ≃ Y
he : ∀ (s : Set Y), IsOpen[inst] ((⇑e : (a : X) → Y) ⁻¹' s) ↔ IsOpen[inst_1] s
s : Set X
⊢ IsOpen[inst_1] ((⇑e.symm : (a : Y) → X) ⁻¹' s) ↔ IsOpen[inst] s
have h : s = preimage.{u_1, u_2} (β := Y) (⇑e : (a : X) → Y) ((⇑e.symm : (a : Y) → X) ⁻¹' s)
Tactic: convert! (he _).symm
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsCompact.{u_1} (X := X) ((⇑h : (a : X) → Y) ⁻¹' s) ↔ IsCompact s
have rw : IsCompact.{u_1} (X := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsCompact s
Tactic: rw [← image_symm]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsSigmaCompact.{u_1} (X := X) ((⇑h : (a : X) → Y) ⁻¹' s) ↔ IsSigmaCompact s
have rw : IsSigmaCompact.{u_1} (X := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsSigmaCompact s
Tactic: rw [← image_symm]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsPreconnected.{u_1} (α := X) ((⇑h : (a : X) → Y) ⁻¹' s) ↔ IsPreconnected s
have rw : IsPreconnected.{u_1} (α := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsPreconnected s
Tactic: rw [← image_symm, isPreconnected_image]