awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
hf : ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)
x : α
y : β
h_1 : (fun (x1 x2 : β) ↦ x1 ⤳ x2) y (f x)
i : ι
hx : f x ∈ U i
h :
  Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y ⋯ ⤳
    (U i).carrier.restrictPreimage f (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hx)
a : (↑(f ⁻¹' (U i).carrier) : Type u_1)
ha : a ⤳ Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hx
heq : (U i).carrier.restrictPreimage f a = Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y ⋯
refine : (fun (x1 x2 : α) ↦ x1 ⤳ x2) (↑a : α) x
⊢ ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y

Tactic:
refine ⟨a, ?_, congr(($heq).val)⟩
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
hf : ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)
x : α
y : β
h_1 : (fun (x1 x2 : β) ↦ x1 ⤳ x2) y (f x)
i : ι
hx : f x ∈ U i
h :
  Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y ⋯ ⤳
    (U i).carrier.restrictPreimage f (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hx)
a : (↑(f ⁻¹' (U i).carrier) : Type u_1)
ha : a ⤳ Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hx
heq : (U i).carrier.restrictPreimage f a = Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y ⋯
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (ha : (↑a : α) ⤳ (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hx) : α))
    (heq : (U i).carrier.restrictPreimage f a = Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y ⋯), (↑a : α) ⤳ x
⊢ (fun (x1 x2 : α) ↦ x1 ⤳ x2) (↑a : α) x

Tactic:
rwa [subtype_specializes_iff] at ha

Premises used: subtype_specializes_iff
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
⊢ IsOpenMap f ↔ ∀ (i : ι), IsOpenMap (X := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))

Tactic:
⟨fun hf ↦ fun i ↦ hf.comp (U i).isOpenEmbedding'.isOpenMap, fun hf ↦ ?_⟩

Premises used: Topology.IsOpenEmbedding.isOpenMap, IsOpenMap.comp, TopologicalSpace.Opens.isOpenEmbedding', Iff.intro
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
refine : ∀ (hf : ∀ (i : ι), IsOpenMap (X := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))), IsOpenMap f
⊢ IsOpenMap f ↔ ∀ (i : ι), IsOpenMap (X := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))

Tactic:
refine ⟨fun hf ↦ fun i ↦ hf.comp (U i).isOpenEmbedding'.isOpenMap, fun hf ↦ ?_⟩
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), IsOpenMap (X := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))
V : Set α
hV : IsOpen[inst] V
⊢ IsOpen[inst_1]
    (⋃ (i : ι),
      image (α := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))
        (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' V))

Tactic:
isOpen_iUnion (fun i ↦ hf i _ <| isOpen_induced hV)

Premises used: isOpen_induced, isOpen_iUnion, Set.preimage, Subtype.val
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), IsOpenMap (X := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))
V : Set α
hV : IsOpen[inst] V
h :
  f '' V =
    ⋃ (i : ι),
      image (α := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))
        (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' V)
⊢ IsOpen[inst_1] (f '' V)

Tactic:
convert! isOpen_iUnion (fun i ↦ hf i _ <| isOpen_induced hV)

Premises used: isOpen_induced, isOpen_iUnion, Set.preimage, Subtype.val
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), IsOpenMap (X := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))
V : Set α
hV : IsOpen[inst] V
h :
  f '' V =
    ⋃ (i : ι),
      f ''
        image (α := ↥(U i)) (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' V)
h₁ : f '' V = ⋃ (i : ι), f '' (V ∩ range (ι := ↥(U i)) (Subtype.val (p := fun (x : α) ↦ x ∈ U i)))
h₂ : f '' V = f '' ⋃ (i : ι), V ∩ range (ι := ↥(U i)) (Subtype.val (p := fun (x : α) ↦ x ∈ U i))
h₃ : f '' V = f '' ⋃ (i : ι), V ∩ {x : α | x ∈ U i}
h₄ : f '' V = f '' ⋃ (i : ι), V ∩ (↑(U i) : Set α)
⊢ f '' V =
    ⋃ (i : ι),
      image (α := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))
        (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' V)

Tactic:
simp_rw [Set.image_comp, Set.image_preimage_eq_inter_range, ← Set.image_iUnion,
    Subtype.range_coe_subtype, SetLike.setOf_mem_eq, hU.iUnion_inter]

Premises used: SetLike.setOf_mem_eq, Subtype.range_coe_subtype, Set.image_preimage_eq_inter_range, Set.image_iUnion, TopologicalSpace.IsOpenCover.iUnion_inter, Set.image_comp
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
⊢ GeneralizingMap f ↔ ∀ (i : ι), GeneralizingMap (X := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))

Tactic:
⟨fun hf ↦ fun i ↦
      ((U i).isOpenEmbedding'.generalizingMap
        (U i).isOpenEmbedding'.isOpen_range.stableUnderGeneralization).comp hf,
    fun hf ↦ fun x y h ↦ ?_⟩

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, GeneralizingMap.comp, TopologicalSpace.Opens.isOpenEmbedding', Topology.IsInducing.generalizingMap, Topology.IsOpenEmbedding.isOpen_range, Iff.intro, Topology.IsEmbedding.toIsInducing, IsOpen.stableUnderGeneralization
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
refine :
  ∀ (hf : ∀ (i : ι), GeneralizingMap (X := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))) (x : α) (y : β)
    (h : (fun (x1 x2 : β) ↦ x1 ⤳ x2) y (f x)), ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y
⊢ GeneralizingMap f ↔ ∀ (i : ι), GeneralizingMap (X := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))

Tactic:
refine ⟨fun hf ↦ fun i ↦
      ((U i).isOpenEmbedding'.generalizingMap
        (U i).isOpenEmbedding'.isOpen_range.stableUnderGeneralization).comp hf,
    fun hf ↦ fun x y h ↦ ?_⟩
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), GeneralizingMap (X := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))
x : α
y : β
h : (fun (x1 x2 : β) ↦ x1 ⤳ x2) y (f x)
obtain : ∀ (i : ι) (hi : x ∈ U i), ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y
⊢ ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y

Tactic:
obtain ⟨i, hi⟩ := hU.exists_mem x

Premises used: TopologicalSpace.IsOpenCover.exists_mem
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), GeneralizingMap (X := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))
x : α
y : β
h : (fun (x1 x2 : β) ↦ x1 ⤳ x2) y (f x)
i : ι
hi : x ∈ U i
⊢ y ⤳ (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) (Subtype.mk (p := fun (x : α) ↦ x ∈ U i) x hi)

Tactic:
replace h : y ⤳ (f ∘ ((↑) : U i → α)) ⟨x, hi⟩ := h
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), GeneralizingMap (X := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))
x : α
y : β
i : ι
hi : x ∈ U i
h : y ⤳ (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) (Subtype.mk (p := fun (x : α) ↦ x ∈ U i) x hi)
obtain :
  ∀ (a : ↥(U i)) (ha : a ⤳ Subtype.mk (p := fun (x : α) ↦ x ∈ U i) x hi)
    (h :
      (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) a ⤳
        (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) (Subtype.mk (p := fun (x : α) ↦ x ∈ U i) x hi)),
    ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) a
⊢ ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y

Tactic:
obtain ⟨a, ha, rfl⟩ := hf i h

Premises used: rfl
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), GeneralizingMap (X := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))
x : α
i : ι
hi : x ∈ U i
a : ↥(U i)
ha : a ⤳ Subtype.mk (p := fun (x : α) ↦ x ∈ U i) x hi
h :
  (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) a ⤳
    (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) (Subtype.mk (p := fun (x : α) ↦ x ∈ U i) x hi)
h₁ : (fun (x1 x2 : α) ↦ x1 ⤳ x2) (↑a : α) x ∧ f (↑a : α) = (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) a
⊢ ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) a

Tactic:
use a.val

Premises used: Subtype.val
-- Module: Mathlib.Topology.LocalAtTarget
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), GeneralizingMap (X := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))
x : α
i : ι
hi : x ∈ U i
a : ↥(U i)
ha : a ⤳ Subtype.mk (p := fun (x : α) ↦ x ∈ U i) x hi
h :
  (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) a ⤳
    (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) (Subtype.mk (p := fun (x : α) ↦ x ∈ U i) x hi)
⊢ (fun (x1 x2 : α) ↦ x1 ⤳ x2) (↑a : α) x ∧ f (↑a : α) = (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) a

Tactic:
simp [ha.map (U i).isOpenEmbedding'.continuous]

Premises used: TopologicalSpace.Opens.isOpenEmbedding', Topology.IsOpenEmbedding.continuous, Specializes.map
-- 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)
inr :
  ∀
    (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 = ⊤), IsEmbedding f
wlog :
  ∀ {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
⊢ IsEmbedding f

Tactic:
wlog hU' : iSup U = ⊤

Premises used: iSup
-- 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) ⋯
inr : IsEmbedding f₀
⊢ IsEmbedding f

Tactic:
suffices IsEmbedding f₀ from IsEmbedding.subtypeVal.comp this
-- 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) ⋯
rw :
  LE.le.{u_7} (α := 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))
⊢ 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))
    ⊤

Tactic:
rw [← top_le_iff]

Premises used: top_le_iff
-- 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) ⋯
⊢ LE.le.{u_7} (α := 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))

Tactic:
simpa [Set.range_subset_iff, SetLike.le_def] using hU

Premises used: SetLike.le_def, Set.range_subset_iff
-- 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) ⋯
⊢ 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))
    ⊤

Tactic:
have hU'' : (⨆ i, (U i).comap ⟨Subtype.val, continuous_subtype_val⟩ :
        Opens (Set.range f)) = ⊤ := by
      rw [← top_le_iff]
      simpa [Set.range_subset_iff, SetLike.le_def] using hU
-- 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))
    ⊤
⊢ IsEmbedding f₀

Tactic:
this _ ?_ _ ?_ V iV hiV ?_ ?_ hU''
-- 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))
    ⊤
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)
inr₃ : ∀ (i : ι), IsEmbedding (f₀ ∘ iV i)
⊢ IsEmbedding f₀

Tactic:
refine this _ ?_ _ ?_ V iV hiV ?_ ?_ hU''
-- 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))
    ⊤
⊢ Continuous[inst, instTopologicalSpaceSubtype] 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)
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 : range f₀ ⊆ (↑⊤ : Set (↑(range f) : Type u_7))
⊢ 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))

Tactic:
rw [hU'']