awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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 ⋯
⊢ ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y
have refine : (fun (x1 x2 : α) ↦ x1 ⤳ x2) (↑a : α) x
Tactic: refine ⟨a, ?_, congr(($heq).val)⟩
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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 ⋯
⊢ (fun (x1 x2 : α) ↦ x1 ⤳ x2) (↑a : α) x
have 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 sorry), (↑a : α) ⤳ x
Tactic: rwa [subtype_specializes_iff] at ha
Cleared hypotheses: ha, heq
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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))
have refine : ∀ (hf : ∀ (i : ι), IsOpenMap (X := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))), IsOpenMap f
Tactic: refine ⟨fun hf ↦ fun i ↦ hf.comp (U i).isOpenEmbedding'.isOpenMap, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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] (f '' V)
have 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)
Tactic: convert! isOpen_iUnion (fun i ↦ hf i _ <| isOpen_induced hV)
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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
⊢ f '' V =
    ⋃ (i : ι),
      image (α := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))
        (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' V)
have 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)
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]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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)
⊢ f '' V =
    ⋃ (i : ι),
      image (α := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))
        (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' V)
have h₁ : f '' V = ⋃ (i : ι), f '' (V ∩ range (ι := ↥(U i)) (Subtype.val (p := fun (x : α) ↦ x ∈ U i)))
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]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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)))
⊢ f '' V =
    ⋃ (i : ι),
      image (α := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))
        (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' V)
have h₂ : f '' V = f '' ⋃ (i : ι), V ∩ range (ι := ↥(U i)) (Subtype.val (p := fun (x : α) ↦ x ∈ U i))
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]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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))
⊢ f '' V =
    ⋃ (i : ι),
      image (α := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))
        (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' V)
have h₃ : f '' V = f '' ⋃ (i : ι), V ∩ {x : α | x ∈ U i}
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]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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}
⊢ f '' V =
    ⋃ (i : ι),
      image (α := ↥(U i)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i))
        (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' V)
have h₄ : f '' V = f '' ⋃ (i : ι), V ∩ (↑(U i) : Set α)
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]
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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))
have 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
Tactic: refine ⟨fun hf ↦ fun i ↦
      ((U i).isOpenEmbedding'.generalizingMap
        (U i).isOpenEmbedding'.isOpen_range.stableUnderGeneralization).comp hf,
    fun hf ↦ fun x y h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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)
⊢ ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y
have obtain : ∀ (i : ι) (hi : x ∈ U i), ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y
Tactic: obtain ⟨i, hi⟩ := hU.exists_mem x
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (hypothesis)
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
⊢ ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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)
⊢ ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = y
have 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
Tactic: obtain ⟨a, ha, rfl⟩ := hf i h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Topology.LocalAtTarget (goal)
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)
⊢ ∃ (a' : α), (fun (x1 x2 : α) ↦ x1 ⤳ x2) a' x ∧ f a' = (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) a
have h₁ : (fun (x1 x2 : α) ↦ x1 ⤳ x2) (↑a : α) x ∧ f (↑a : α) = (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) a
Tactic: use a.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)
⊢ IsEmbedding f
have 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
Tactic: wlog hU' : iSup U = ⊤
-- 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)
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
⊢ IsEmbedding f
have 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
Tactic: wlog hU' : iSup U = ⊤
Cleared hypotheses: X, Y, inst, inst_1, f, h, ι, U, hU, V, inst_2, iV, hiV, hV, hV'
-- 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) ⋯
⊢ IsEmbedding f
have inr : IsEmbedding f₀
Tactic: suffices IsEmbedding f₀ from IsEmbedding.subtypeVal.comp this
-- 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) ⋯
⊢ 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))
    ⊤
have 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 := sorry } :
        (a : Opens Y) → Opens { x : Y // x ∈ range f })
      (U i))
Tactic: rw [← top_le_iff]
-- 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)
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) ⋯
⊢ IsEmbedding f₀
have 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 := sorry } :
        (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
-- 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))
    ⊤
⊢ IsEmbedding f₀
have inr : Continuous[inst, instTopologicalSpaceSubtype] f₀
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))
    ⊤
inr : Continuous[inst, instTopologicalSpaceSubtype] f₀
⊢ IsEmbedding f₀
have inr₁ : range f₀ ⊆
  (↑(⨆ (i : ι),
        (Opens.comap { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ range f), continuous_toFun := sorry } :
            (a : Opens Y) → Opens { x : Y // x ∈ range f })
          (U i)) :
    Set (↑(range f) : Type u_7))
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))
    ⊤
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))
⊢ IsEmbedding f₀
have inr₂ : ∀ (i : ι),
  f₀ ⁻¹'
      (↑((Opens.comap
                  { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ range f), continuous_toFun := sorry :
                    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: refine this _ ?_ _ ?_ V iV hiV ?_ ?_ hU''