awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.LocalAtTarget
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₀ ⊆ (↑⊤ : Set (↑(range f) : Type u_7))

Tactic:
simp
-- Module: Mathlib.Topology.LocalAtTarget
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))
    ⊤
⊢ ∀ (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)

Tactic:
hV

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.LocalAtTarget
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))
    ⊤
⊢ ∀ (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)

Tactic:
exact hV
-- Module: Mathlib.Topology.LocalAtTarget
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))
    ⊤
i : ι
⊢ Continuous[inst_2 i, instTopologicalSpaceSubtype] (f₀ ∘ iV i)

Tactic:
fun_prop
-- Module: Mathlib.Topology.LocalAtTarget
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))
    ⊤
⊢ ∀ (i : ι), IsEmbedding (f₀ ∘ iV i)

Tactic:
exact fun i ↦ IsEmbedding.of_comp (by fun_prop) continuous_subtype_val (hV' i)
-- Module: Mathlib.Topology.LocalAtTarget
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 = ⊤
rw : ∀ (i : ι), IsEmbedding ((U i).carrier.restrictPreimage f)
⊢ IsEmbedding f

Tactic:
rw [(IsOpenCover.mk hU').isEmbedding_iff_restrictPreimage h]

Premises used: TopologicalSpace.IsOpenCover.mk, TopologicalSpace.IsOpenCover.isEmbedding_iff_restrictPreimage
-- Module: Mathlib.Topology.LocalAtTarget
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 f'

Tactic:
have : IsEmbedding f' :=
    IsEmbedding.subtypeVal.comp ((IsEmbedding.of_comp (hiV i) h (hV' _)).restrictPreimage _)
-- Module: Mathlib.Topology.LocalAtTarget
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'
⊢ range f' = f ⁻¹' (↑(U i) : Set Y)

Tactic:
simpa [f', Set.range_comp, Set.range_restrictPreimage] using hV i

Premises used: Set.range_comp, Set.range_restrictPreimage
-- Module: Mathlib.Topology.LocalAtTarget
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'
⊢ 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
-- Module: Mathlib.Topology.LocalAtTarget
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')
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] ((U i).carrier.restrictPreimage f)

Tactic:
fun_prop
-- Module: Mathlib.Topology.LocalAtTarget
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')
refine : IsEmbedding (Subtype.val (p := fun (x : Y) ↦ x ∈ (U i).carrier) ∘ (U i).carrier.restrictPreimage f)
⊢ IsEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
refine IsEmbedding.of_comp (by fun_prop) continuous_subtype_val ?_

Premises used: continuous_subtype_val, Topology.IsEmbedding.of_comp
-- Module: Mathlib.Topology.LocalAtTarget
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_6, u_7} (X := (↑(f ⁻¹' (↑(U i) : Set Y)) : Type u_6))
    (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:
((hV' i).comp IsEmbedding.subtypeVal).comp e.symm.isEmbedding

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.comp, Homeomorph.symm, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.LocalAtTarget
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')
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))
⊢ IsEmbedding (Subtype.val (p := fun (x : Y) ↦ x ∈ (U i).carrier) ∘ (U i).carrier.restrictPreimage f)

Tactic:
convert! ((hV' i).comp IsEmbedding.subtypeVal).comp e.symm.isEmbedding

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.comp, Homeomorph.symm, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.LocalAtTarget
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)
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
⊢ 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:
ext x
-- Module: Mathlib.Topology.LocalAtTarget
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)
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))
⊢ (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:
obtain ⟨x, rfl⟩ := e.surjective x

Premises used: Homeomorph.surjective, rfl
-- Module: Mathlib.Topology.LocalAtTarget
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)
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))
⊢ (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:
simp
-- Module: Mathlib.Topology.LocalAtTarget
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)
⊢ 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:
rfl
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : Disjoint s (closure[inst] s \ s)
⊢ s ⊆ coborder s

Tactic:
rw [coborder, subset_compl_iff_disjoint_right]

Premises used: Set.subset_compl_iff_disjoint_right, coborder
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ Disjoint s (closure[inst] s \ s)

Tactic:
disjoint_sdiff_self_right

Premises used: disjoint_sdiff_self_right