awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
X : Type u_6
Y : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : Continuous[inst, inst_1] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ (↑(iSup U) : Set Y)
V : ι → Type u_5
inst_2 : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst_2 i, inst] (iV i)
hV : ∀ (i : ι), f ⁻¹' (↑(U i) : Set Y) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_3 : TopologicalSpace Y] (f : X → Y)
    (h : Continuous f) {ι : Type u_4} (U : ι → Opens Y) (hU : range f ⊆ (↑(iSup U) : Set Y)) (V : ι → Type u_5)
    [inst_4 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X) (hiV : ∀ (i : ι), Continuous (iV i))
    (hV : ∀ (i : ι), f ⁻¹' (↑(U i) : Set Y) ⊆ range (iV i)) (hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i))
    (hU' : iSup U = ⊤), IsEmbedding f
hU' : ¬iSup U = ⊤
f₀ : X → (↑(range f) : Type u_7) := fun (x : X) ↦ Subtype.mk (p := fun (x : Y) ↦ x ∈ range f) (f x) ⋯
hU'' :
  Eq.{u_7 + 1} (α := Opens (↑(range f) : Type u_7))
    (⨆ (i : ι),
      (Opens.comap { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ range f), continuous_toFun := ⋯ } :
          (a : Opens Y) → Opens { x : Y // x ∈ range f })
        (U i))
    ⊤
inr : Continuous[inst, instTopologicalSpaceSubtype] f₀
inr₁ :
  range f₀ ⊆
    (↑(⨆ (i : ι),
          (Opens.comap { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ range f), continuous_toFun := ⋯ } :
              (a : Opens Y) → Opens { x : Y // x ∈ range f })
            (U i)) :
      Set (↑(range f) : Type u_7))
inr₂ :
  ∀ (i : ι),
    f₀ ⁻¹'
        (↑((Opens.comap
                    { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ range f), continuous_toFun := ⋯ :
                      C({ x : Y // x ∈ range f }, Y) } :
                  (a : Opens Y) → Opens { x : Y // x ∈ range f })
                (U i) :
              Opens { x : Y // x ∈ range f }) :
          Set (↑(range f) : Type u_7)) ⊆
      range (iV i)
⊢ IsEmbedding f₀
have inr₃ : ∀ (i : ι), IsEmbedding (f₀ ∘ iV i)
Tactic: refine this _ ?_ _ ?_ V iV hiV ?_ ?_ hU''
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
X : Type u_6
Y : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : Continuous[inst, inst_1] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ (↑(iSup U) : Set Y)
V : ι → Type u_5
inst_2 : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst_2 i, inst] (iV i)
hV : ∀ (i : ι), f ⁻¹' (↑(U i) : Set Y) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_3 : TopologicalSpace Y] (f : X → Y)
    (h : Continuous f) {ι : Type u_4} (U : ι → Opens Y) (hU : range f ⊆ (↑(iSup U) : Set Y)) (V : ι → Type u_5)
    [inst_4 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X) (hiV : ∀ (i : ι), Continuous (iV i))
    (hV : ∀ (i : ι), f ⁻¹' (↑(U i) : Set Y) ⊆ range (iV i)) (hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i))
    (hU' : iSup U = ⊤), IsEmbedding f
hU' : ¬iSup U = ⊤
f₀ : X → (↑(range f) : Type u_7) := fun (x : X) ↦ Subtype.mk (p := fun (x : Y) ↦ x ∈ range f) (f x) ⋯
hU'' :
  Eq.{u_7 + 1} (α := Opens (↑(range f) : Type u_7))
    (⨆ (i : ι),
      (Opens.comap { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ range f), continuous_toFun := ⋯ } :
          (a : Opens Y) → Opens { x : Y // x ∈ range f })
        (U i))
    ⊤
⊢ range f₀ ⊆
    (↑(⨆ (i : ι),
          (Opens.comap { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ range f), continuous_toFun := ⋯ } :
              (a : Opens Y) → Opens { x : Y // x ∈ range f })
            (U i)) :
      Set (↑(range f) : Type u_7))
have inr : range f₀ ⊆ (↑⊤ : Set (↑(range f) : Type u_7))
Tactic: rw [hU'']
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
X : Type u_6
Y : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : Continuous[inst, inst_1] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ (↑(iSup U) : Set Y)
V : ι → Type u_5
inst_2 : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst_2 i, inst] (iV i)
hV : ∀ (i : ι), f ⁻¹' (↑(U i) : Set Y) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
hU' : iSup U = ⊤
⊢ IsEmbedding f
have rw : ∀ (i : ι), IsEmbedding ((U i).carrier.restrictPreimage f)
Tactic: rw [(IsOpenCover.mk hU').isEmbedding_iff_restrictPreimage h]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (hypothesis)
Goal:
X : Type u_6
Y : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : Continuous[inst, inst_1] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ (↑(iSup U) : Set Y)
V : ι → Type u_5
inst_2 : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst_2 i, inst] (iV i)
hV : ∀ (i : ι), f ⁻¹' (↑(U i) : Set Y) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
hU' : iSup U = ⊤
i : ι
f' : (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5) → X :=
  Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' (↑(U i) : Set Y)) ∘ (f ⁻¹' (↑(U i) : Set Y)).restrictPreimage (iV i)
⊢ IsEmbedding ((U i).carrier.restrictPreimage f)
have this : IsEmbedding f'
Tactic: have : IsEmbedding f' :=
    IsEmbedding.subtypeVal.comp ((IsEmbedding.of_comp (hiV i) h (hV' _)).restrictPreimage _)
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (hypothesis)
Goal:
X : Type u_6
Y : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : Continuous[inst, inst_1] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ (↑(iSup U) : Set Y)
V : ι → Type u_5
inst_2 : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst_2 i, inst] (iV i)
hV : ∀ (i : ι), f ⁻¹' (↑(U i) : Set Y) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
hU' : iSup U = ⊤
i : ι
f' : (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5) → X :=
  Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' (↑(U i) : Set Y)) ∘ (f ⁻¹' (↑(U i) : Set Y)).restrictPreimage (iV i)
this : IsEmbedding f'
⊢ IsEmbedding ((U i).carrier.restrictPreimage f)
have hf' : range f' = f ⁻¹' (↑(U i) : Set Y)
Tactic: have hf' : Set.range f' = f ⁻¹' U i := by
    simpa [f', Set.range_comp, Set.range_restrictPreimage] using hV i
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
X : Type u_6
Y : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : Continuous[inst, inst_1] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ (↑(iSup U) : Set Y)
V : ι → Type u_5
inst_2 : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst_2 i, inst] (iV i)
hV : ∀ (i : ι), f ⁻¹' (↑(U i) : Set Y) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
hU' : iSup U = ⊤
i : ι
f' : (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5) → X :=
  Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' (↑(U i) : Set Y)) ∘ (f ⁻¹' (↑(U i) : Set Y)).restrictPreimage (iV i)
this : IsEmbedding f'
hf' : range f' = f ⁻¹' (↑(U i) : Set Y)
e : Homeomorph.{u_5, u_6} (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5) (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6) :=
  this.toHomeomorph.trans (Homeomorph.setCongr (s := range f') (t := f ⁻¹' (↑(U i) : Set Y)) hf')
⊢ IsEmbedding ((U i).carrier.restrictPreimage f)
have refine : IsEmbedding (Subtype.val (p := fun (x : Y) ↦ x ∈ (U i).carrier) ∘ (U i).carrier.restrictPreimage f)
Tactic: refine IsEmbedding.of_comp (by fun_prop) continuous_subtype_val ?_
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
X : Type u_6
Y : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : Continuous[inst, inst_1] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ (↑(iSup U) : Set Y)
V : ι → Type u_5
inst_2 : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst_2 i, inst] (iV i)
hV : ∀ (i : ι), f ⁻¹' (↑(U i) : Set Y) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
hU' : iSup U = ⊤
i : ι
f' : (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5) → X :=
  Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' (↑(U i) : Set Y)) ∘ (f ⁻¹' (↑(U i) : Set Y)).restrictPreimage (iV i)
this : IsEmbedding f'
hf' : range f' = f ⁻¹' (↑(U i) : Set Y)
e : Homeomorph.{u_5, u_6} (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5) (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6) :=
  this.toHomeomorph.trans (Homeomorph.setCongr (s := range f') (t := f ⁻¹' (↑(U i) : Set Y)) hf')
⊢ IsEmbedding (Subtype.val (p := fun (x : Y) ↦ x ∈ (U i).carrier) ∘ (U i).carrier.restrictPreimage f)
have h₁ : (↑(f ⁻¹' (U i).carrier) : Type u_6) = (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6) →
  Subtype.val (p := fun (x : Y) ↦ x ∈ (U i).carrier) ∘ (U i).carrier.restrictPreimage f =
    Function.comp (β := { x : V i // x ∈ iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y) })
      ((f ∘ iV i) ∘ Subtype.val (p := fun (x : V i) ↦ x ∈ iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)))
      (⇑e.symm : (a : (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)) → (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5))
Tactic: convert! ((hV' i).comp IsEmbedding.subtypeVal).comp e.symm.isEmbedding
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
X : Type u_6
Y : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : Continuous[inst, inst_1] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ (↑(iSup U) : Set Y)
V : ι → Type u_5
inst_2 : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst_2 i, inst] (iV i)
hV : ∀ (i : ι), f ⁻¹' (↑(U i) : Set Y) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
hU' : iSup U = ⊤
i : ι
f' : (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5) → X :=
  Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' (↑(U i) : Set Y)) ∘ (f ⁻¹' (↑(U i) : Set Y)).restrictPreimage (iV i)
this : IsEmbedding f'
hf' : range f' = f ⁻¹' (↑(U i) : Set Y)
e : Homeomorph.{u_5, u_6} (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5) (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6) :=
  this.toHomeomorph.trans (Homeomorph.setCongr (s := range f') (t := f ⁻¹' (↑(U i) : Set Y)) hf')
e_1 : (↑(f ⁻¹' (U i).carrier) : Type u_6) = (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)
⊢ Subtype.val (p := fun (x : Y) ↦ x ∈ (U i).carrier) ∘ (U i).carrier.restrictPreimage f =
    Function.comp (β := { x : V i // x ∈ iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y) })
      ((f ∘ iV i) ∘ Subtype.val (p := fun (x : V i) ↦ x ∈ iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)))
      (⇑e.symm : (a : (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)) → (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5))
have h₁ : ∀ (x : (↑(f ⁻¹' (U i).carrier) : Type u_6)),
  (Subtype.val (p := fun (x : Y) ↦ x ∈ (U i).carrier) ∘ (U i).carrier.restrictPreimage f) x =
    Function.comp (β := { x : V i // x ∈ iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y) })
      ((f ∘ iV i) ∘ Subtype.val (p := fun (x : V i) ↦ x ∈ iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)))
      (⇑e.symm : (a : (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)) → (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
X : Type u_6
Y : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : Continuous[inst, inst_1] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ (↑(iSup U) : Set Y)
V : ι → Type u_5
inst_2 : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst_2 i, inst] (iV i)
hV : ∀ (i : ι), f ⁻¹' (↑(U i) : Set Y) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
hU' : iSup U = ⊤
i : ι
f' : (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5) → X :=
  Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' (↑(U i) : Set Y)) ∘ (f ⁻¹' (↑(U i) : Set Y)).restrictPreimage (iV i)
this : IsEmbedding f'
hf' : range f' = f ⁻¹' (↑(U i) : Set Y)
e : Homeomorph.{u_5, u_6} (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5) (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6) :=
  this.toHomeomorph.trans (Homeomorph.setCongr (s := range f') (t := f ⁻¹' (↑(U i) : Set Y)) hf')
e_1 : (↑(f ⁻¹' (U i).carrier) : Type u_6) = (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)
x : (↑(f ⁻¹' (U i).carrier) : Type u_6)
⊢ (Subtype.val (p := fun (x : Y) ↦ x ∈ (U i).carrier) ∘ (U i).carrier.restrictPreimage f) x =
    Function.comp (β := { x : V i // x ∈ iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y) })
      ((f ∘ iV i) ∘ Subtype.val (p := fun (x : V i) ↦ x ∈ iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)))
      (⇑e.symm : (a : (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)) → (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5)) x
have h₁ : ∀ (x : (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5)),
  (Subtype.val (p := fun (x : Y) ↦ x ∈ (U i).carrier) ∘ (U i).carrier.restrictPreimage f)
      ((e : (a : (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5)) → (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)) x) =
    Function.comp.{u_6 + 1, u_5 + 1, u_7 + 1} (α := (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)) (β :=
      { x : V i // x ∈ iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y) })
      ((f ∘ iV i) ∘ Subtype.val (p := fun (x : V i) ↦ x ∈ iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)))
      ((⇑e.symm : (a : (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)) → (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5)) :
        (a : (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)) → (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5))
      ((e : (a : (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5)) → (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)) x :
        (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6))
Tactic: obtain ⟨x, rfl⟩ := e.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
Goal:
X : Type u_6
Y : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : Continuous[inst, inst_1] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ (↑(iSup U) : Set Y)
V : ι → Type u_5
inst_2 : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst_2 i, inst] (iV i)
hV : ∀ (i : ι), f ⁻¹' (↑(U i) : Set Y) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
hU' : iSup U = ⊤
i : ι
f' : (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5) → X :=
  Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' (↑(U i) : Set Y)) ∘ (f ⁻¹' (↑(U i) : Set Y)).restrictPreimage (iV i)
this : IsEmbedding f'
hf' : range f' = f ⁻¹' (↑(U i) : Set Y)
e : Homeomorph.{u_5, u_6} (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5) (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6) :=
  this.toHomeomorph.trans (Homeomorph.setCongr (s := range f') (t := f ⁻¹' (↑(U i) : Set Y)) hf')
e_1 : (↑(f ⁻¹' (U i).carrier) : Type u_6) = (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)
x : (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5)
⊢ (Subtype.val (p := fun (x : Y) ↦ x ∈ (U i).carrier) ∘ (U i).carrier.restrictPreimage f)
      ((e : (a : (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5)) → (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)) x) =
    Function.comp.{u_6 + 1, u_5 + 1, u_7 + 1} (α := (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)) (β :=
      { x : V i // x ∈ iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y) })
      ((f ∘ iV i) ∘ Subtype.val (p := fun (x : V i) ↦ x ∈ iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)))
      ((⇑e.symm : (a : (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)) → (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5)) :
        (a : (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)) → (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5))
      ((e : (a : (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5)) → (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)) x :
        (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6))
have h₁ : f (↑((e : (a : (↑(iV i ⁻¹' f ⁻¹' (↑(U i) : Set Y)) : Type u_5)) → (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6)) x) : X) =
  f (iV i (↑x : V i))
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ s ⊆ coborder s
have rw : Disjoint s (closure[inst] s \ s)
Tactic: rw [coborder, subset_compl_iff_disjoint_right]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ coborder s ∩ closure[inst] s = s
have rw : s ⊆ closure[inst] s
Tactic: rw [coborder, ← diff_eq_compl_inter, diff_diff_right_self, inter_eq_right]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ closure[inst] s ∩ coborder s = s
have rw : coborder s ∩ closure[inst] s = s
Tactic: rw [inter_comm, coborder_inter_closure]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : coborder s ∩ closure[inst] s = s
⊢ closure[inst] s ∩ coborder s = s
have rw₁ : s = s
Tactic: rw [inter_comm, coborder_inter_closure]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ coborder s = s ∪ (frontier s)ᶜ
have rw : (closure[inst] s \ s)ᶜ = s ∪ (frontier s)ᶜ
Tactic: rw [coborder, compl_eq_comm, compl_union, compl_compl, ← diff_eq_compl_inter,
    ← union_diff_right, union_comm, ← closure_eq_self_union_frontier]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : (closure[inst] s \ s)ᶜ = s ∪ (frontier s)ᶜ
⊢ coborder s = s ∪ (frontier s)ᶜ
have rw₁ : (s ∪ (frontier s)ᶜ)ᶜ = closure[inst] s \ s
Tactic: rw [coborder, compl_eq_comm, compl_union, compl_compl, ← diff_eq_compl_inter,
    ← union_diff_right, union_comm, ← closure_eq_self_union_frontier]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : (closure[inst] s \ s)ᶜ = s ∪ (frontier s)ᶜ
rw₁ : (s ∪ (frontier s)ᶜ)ᶜ = closure[inst] s \ s
⊢ coborder s = s ∪ (frontier s)ᶜ
have rw₂ : sᶜ ∩ (frontier s)ᶜᶜ = closure[inst] s \ s
Tactic: rw [coborder, compl_eq_comm, compl_union, compl_compl, ← diff_eq_compl_inter,
    ← union_diff_right, union_comm, ← closure_eq_self_union_frontier]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : (closure[inst] s \ s)ᶜ = s ∪ (frontier s)ᶜ
rw₁ : (s ∪ (frontier s)ᶜ)ᶜ = closure[inst] s \ s
rw₂ : sᶜ ∩ (frontier s)ᶜᶜ = closure[inst] s \ s
⊢ coborder s = s ∪ (frontier s)ᶜ
have rw₃ : sᶜ ∩ frontier s = closure[inst] s \ s
Tactic: rw [coborder, compl_eq_comm, compl_union, compl_compl, ← diff_eq_compl_inter,
    ← union_diff_right, union_comm, ← closure_eq_self_union_frontier]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : (closure[inst] s \ s)ᶜ = s ∪ (frontier s)ᶜ
rw₁ : (s ∪ (frontier s)ᶜ)ᶜ = closure[inst] s \ s
rw₂ : sᶜ ∩ (frontier s)ᶜᶜ = closure[inst] s \ s
rw₃ : sᶜ ∩ frontier s = closure[inst] s \ s
⊢ coborder s = s ∪ (frontier s)ᶜ
have rw₄ : frontier s \ s = closure[inst] s \ s
Tactic: rw [coborder, compl_eq_comm, compl_union, compl_compl, ← diff_eq_compl_inter,
    ← union_diff_right, union_comm, ← closure_eq_self_union_frontier]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : (closure[inst] s \ s)ᶜ = s ∪ (frontier s)ᶜ
rw₁ : (s ∪ (frontier s)ᶜ)ᶜ = closure[inst] s \ s
rw₂ : sᶜ ∩ (frontier s)ᶜᶜ = closure[inst] s \ s
rw₃ : sᶜ ∩ frontier s = closure[inst] s \ s
rw₄ : frontier s \ s = closure[inst] s \ s
⊢ coborder s = s ∪ (frontier s)ᶜ
have rw₅ : (frontier s ∪ s) \ s = closure[inst] s \ s
Tactic: rw [coborder, compl_eq_comm, compl_union, compl_compl, ← diff_eq_compl_inter,
    ← union_diff_right, union_comm, ← closure_eq_self_union_frontier]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : (closure[inst] s \ s)ᶜ = s ∪ (frontier s)ᶜ
rw₁ : (s ∪ (frontier s)ᶜ)ᶜ = closure[inst] s \ s
rw₂ : sᶜ ∩ (frontier s)ᶜᶜ = closure[inst] s \ s
rw₃ : sᶜ ∩ frontier s = closure[inst] s \ s
rw₄ : frontier s \ s = closure[inst] s \ s
rw₅ : (frontier s ∪ s) \ s = closure[inst] s \ s
⊢ coborder s = s ∪ (frontier s)ᶜ
have rw₆ : (s ∪ frontier s) \ s = closure[inst] s \ s
Tactic: rw [coborder, compl_eq_comm, compl_union, compl_compl, ← diff_eq_compl_inter,
    ← union_diff_right, union_comm, ← closure_eq_self_union_frontier]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : (closure[inst] s \ s)ᶜ = s ∪ (frontier s)ᶜ
rw₁ : (s ∪ (frontier s)ᶜ)ᶜ = closure[inst] s \ s
rw₂ : sᶜ ∩ (frontier s)ᶜᶜ = closure[inst] s \ s
rw₃ : sᶜ ∩ frontier s = closure[inst] s \ s
rw₄ : frontier s \ s = closure[inst] s \ s
rw₅ : (frontier s ∪ s) \ s = closure[inst] s \ s
rw₆ : (s ∪ frontier s) \ s = closure[inst] s \ s
⊢ coborder s = s ∪ (frontier s)ᶜ
have rw₇ : closure[inst] s \ s = closure[inst] s \ s
Tactic: rw [coborder, compl_eq_comm, compl_union, compl_compl, ← diff_eq_compl_inter,
    ← union_diff_right, union_comm, ← closure_eq_self_union_frontier]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ coborder s = (frontier s)ᶜ ↔ IsOpen[inst] s
have simp_rw : s ∪ (frontier s)ᶜ = (frontier s)ᶜ ↔ IsOpen[inst] s
Tactic: simp_rw [coborder_eq_union_frontier_compl, union_eq_right, subset_compl_iff_disjoint_left,
    disjoint_frontier_iff_isOpen]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
simp_rw : s ∪ (frontier s)ᶜ = (frontier s)ᶜ ↔ IsOpen[inst] s
⊢ coborder s = (frontier s)ᶜ ↔ IsOpen[inst] s
have simp_rw₁ : s ⊆ (frontier s)ᶜ ↔ IsOpen[inst] s
Tactic: simp_rw [coborder_eq_union_frontier_compl, union_eq_right, subset_compl_iff_disjoint_left,
    disjoint_frontier_iff_isOpen]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
simp_rw : s ∪ (frontier s)ᶜ = (frontier s)ᶜ ↔ IsOpen[inst] s
simp_rw₁ : s ⊆ (frontier s)ᶜ ↔ IsOpen[inst] s
⊢ coborder s = (frontier s)ᶜ ↔ IsOpen[inst] s
have simp_rw₂ : Disjoint (frontier s) s ↔ IsOpen[inst] s
Tactic: simp_rw [coborder_eq_union_frontier_compl, union_eq_right, subset_compl_iff_disjoint_left,
    disjoint_frontier_iff_isOpen]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ coborder s = s ∪ (closure[inst] s)ᶜ
have rw : closure[inst] s ∩ sᶜ = closure[inst] s \ s
Tactic: rw [coborder, compl_eq_comm, compl_union, compl_compl, inter_comm]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ Dense (coborder s)
have rw : univ ⊆ closure[inst] s ∪ closure[inst] (closure[inst] s)ᶜ
Tactic: rw [dense_iff_closure_eq, coborder_eq_union_closure_compl, closure_union, ← univ_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ univ ⊆ closure[inst] s ∪ closure[inst] (closure[inst] s)ᶜ
have refine : univ ⊆ closure[inst] s ∪ (closure[inst] s)ᶜ
Tactic: refine _root_.subset_trans ?_ (union_subset_union_right _ (subset_closure))
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenMap f
s : Set Y
⊢ coborder (f ⁻¹' s) ⊆ f ⁻¹' coborder s
have rw : f ⁻¹' closure[inst_1] s \ f ⁻¹' s ⊆ closure[inst] (f ⁻¹' s) \ f ⁻¹' s
Tactic: rw [coborder, coborder, preimage_compl, preimage_diff, compl_subset_compl]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenMap f
s : Set Y
⊢ f ⁻¹' closure[inst_1] s \ f ⁻¹' s ⊆ closure[inst] (f ⁻¹' s) \ f ⁻¹' s
have h : f ⁻¹' closure[inst_1] s ⊆ closure[inst] (f ⁻¹' s)
Tactic: apply diff_subset_diff_left
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
s : Set Y
⊢ f ⁻¹' coborder s ⊆ coborder (f ⁻¹' s)
have rw : closure[inst] (f ⁻¹' s) \ f ⁻¹' s ⊆ f ⁻¹' closure[inst_1] s \ f ⁻¹' s
Tactic: rw [coborder, coborder, preimage_compl, preimage_diff, compl_subset_compl]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
s : Set Y
⊢ closure[inst] (f ⁻¹' s) \ f ⁻¹' s ⊆ f ⁻¹' closure[inst_1] s \ f ⁻¹' s
have h : closure[inst] (f ⁻¹' s) ⊆ f ⁻¹' closure[inst_1] s
Tactic: apply diff_subset_diff_left