awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
hs_compact : IsCompact s
hs_closed : IsClosed s
⊢ IsClosed (X := (a : (↑S : Type u_1)) → α (↑a : ι))
    (Set.image (α := (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
      Prod.snd
      (Set.image (α := (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)))
        (⇑(Homeomorph.preimageImageRestrict α S s) :
          (a : (↑(Sᶜ.restrict ⁻¹' Sᶜ.restrict '' s) : Type (max u_1 u_2))) →
            (↑(Sᶜ.restrict '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
        ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))) ↦
            (↑x : (a : ι) → α a)) ⁻¹'
          s)))
have this : CompactSpace (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))
Tactic: have : CompactSpace (Sᶜ.restrict '' s) :=
    isCompact_iff_compactSpace.mp (hs_compact.image (Pi.continuous_restrict _))
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this : CompactSpace (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))
⊢ IsClosed (X := (a : (↑S : Type u_1)) → α (↑a : ι))
    (Set.image (α := (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
      Prod.snd
      (Set.image (α := (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)))
        (⇑(Homeomorph.preimageImageRestrict α S s) :
          (a : (↑(Sᶜ.restrict ⁻¹' Sᶜ.restrict '' s) : Type (max u_1 u_2))) →
            (↑(Sᶜ.restrict '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
        ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))) ↦
            (↑x : (a : ι) → α a)) ⁻¹'
          s)))
have refine : IsClosed (X := (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((a : (↑S : Type u_1)) → α (↑a : ι)))
  (Set.image (α := (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)))
    (⇑(Homeomorph.preimageImageRestrict α S s) :
      (a : (↑(Sᶜ.restrict ⁻¹' Sᶜ.restrict '' s) : Type (max u_1 u_2))) →
        (↑(Sᶜ.restrict '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
    ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))) ↦ (↑x : (a : ι) → α a)) ⁻¹'
      s))
Tactic: refine isClosedMap_snd_of_compactSpace _ ?_
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this : CompactSpace (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))
⊢ IsClosed (X := (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((a : (↑S : Type u_1)) → α (↑a : ι)))
    (Set.image (α := (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)))
      (⇑(Homeomorph.preimageImageRestrict α S s) :
        (a : (↑(Sᶜ.restrict ⁻¹' Sᶜ.restrict '' s) : Type (max u_1 u_2))) →
          (↑(Sᶜ.restrict '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
      ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))) ↦
          (↑x : (a : ι) → α a)) ⁻¹'
        s))
have rw : IsClosed (X := (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)))
  ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))) ↦ (↑x : (a : ι) → α a)) ⁻¹'
    s)
Tactic: rw [Homeomorph.isClosed_image]
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
inst_1 : ∀ (i : ι), CompactSpace.{u_2} (α i)
s : Set ((a : ι) → α a)
hs : IsClosed s
⊢ IsClosed (S.restrict (π := α) '' s)
have this : Eq (α := (f : (a : ι) → α a) → (a : (↑S : Type u_1)) → α (↑a : ι)) (S.restrict (π := α))
  (Function.comp (β := ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) Prod.fst
    (⇑(Homeomorph.piEquivPiSubtypeProd (fun (x : ι) ↦ x ∈ S) α) :
      (a : (i : ι) → α i) → ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))))
Tactic: have : S.restrict (π := α) = Prod.fst ∘ (Homeomorph.piEquivPiSubtypeProd (· ∈ S) α) := rfl
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
inst_1 : ∀ (i : ι), CompactSpace.{u_2} (α i)
s : Set ((a : ι) → α a)
hs : IsClosed s
this :
  Eq (α := (f : (a : ι) → α a) → (a : (↑S : Type u_1)) → α (↑a : ι)) (S.restrict (π := α))
    (Function.comp (β := ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) Prod.fst
      (⇑(Homeomorph.piEquivPiSubtypeProd (fun (x : ι) ↦ x ∈ S) α) :
        (a : (i : ι) → α i) → ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))))
⊢ IsClosed (S.restrict (π := α) '' s)
have rw : IsClosed (X := (a : (↑S : Type u_1)) → α (↑a : ι))
  (image (α := ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) Prod.fst
    ((⇑(Homeomorph.piEquivPiSubtypeProd (fun (x : ι) ↦ x ∈ S) α) :
        (a : (i : ι) → α i) → ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) ''
      s))
Tactic: rw [this, image_comp]
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
inst_1 : ∀ (i : ι), CompactSpace.{u_2} (α i)
s : Set ((a : ι) → α a)
hs : IsClosed s
⊢ IsClosed (S.restrict (π := α) '' s)
have have : ∀
  (this :
    Eq (α := (f : (a : ι) → α a) → (a : (↑S : Type u_1)) → α (↑a : ι)) (S.restrict (π := α))
      (Function.comp (β := ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) Prod.fst
        (⇑(Homeomorph.piEquivPiSubtypeProd (fun (x : ι) ↦ x ∈ S) α) :
          (a : (i : ι) → α i) → ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))))),
  IsClosed (S.restrict (π := α) '' s)
Tactic: classical
  have : S.restrict (π := α) = Prod.fst ∘ (Homeomorph.piEquivPiSubtypeProd (· ∈ S) α) := rfl
  rw [this, image_comp]
  exact isClosedMap_fst_of_compactSpace _ <| (Homeomorph.isClosed_image _).mpr hs
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
inst_1 : ∀ (i : ι), CompactSpace.{u_2} (α i)
s : Set ((a : ι) → α a)
hs : IsClosed s
have have₁ have₂ :
  ∀
    (this :
      Eq (α := (f : (a : ι) → α a) → (a : (↑S : Type u_1)) → α (↑a : ι)) (S.restrict (π := α))
        (Function.comp (β := ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) Prod.fst
          (⇑(Homeomorph.piEquivPiSubtypeProd (fun (x : ι) ↦ x ∈ S) α) :
            (a : (i : ι) → α i) → ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))))),
    IsClosed (S.restrict (π := α) '' s)
⊢ IsClosed (S.restrict (π := α) '' s)
have have₃ : ∀
  (this :
    Eq (α := (f : (a : ι) → α a) → (a : (↑S : Type u_1)) → α (↑a : ι)) (S.restrict (π := α))
      (Function.comp (β := ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) Prod.fst
        (⇑(Homeomorph.piEquivPiSubtypeProd (fun (x : ι) ↦ x ∈ S) α) :
          (a : (i : ι) → α i) → ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))))),
  IsClosed (X := (a : (↑S : Type u_1)) → α (↑a : ι))
    (image (α := ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) Prod.fst
      ((⇑(Homeomorph.piEquivPiSubtypeProd (fun (x : ι) ↦ x ∈ S) α) :
          (a : (i : ι) → α i) → ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) ''
        s))
Tactic: classical
  have : S.restrict (π := α) = Prod.fst ∘ (Homeomorph.piEquivPiSubtypeProd (· ∈ S) α) := rfl
  rw [this, image_comp]
  exact isClosedMap_fst_of_compactSpace _ <| (Homeomorph.isClosed_image _).mpr hs
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
i : ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this : IsClosed (X := (a : (↑{i} : Type u_1)) → α (↑a : ι)) (restrict (π := α) {i} '' s)
⊢ IsClosed.{u_2} (X := α i) ((fun (x : (i : ι) → α i) ↦ x i) '' s)
have this₁ : Eq (α := ((a : ι) → α a) → α (↑default : ι))
  (Function.comp (β := (t : (↑{i} : Type u_1)) → α (↑t : ι))
    (⇑(Homeomorph.piUnique fun (t : (↑{i} : Type u_1)) ↦ α (↑t : ι)) :
      (a : (t : (↑{i} : Type u_1)) → α (↑t : ι)) → α (↑default : ι))
    (restrict (π := α) {i}))
  fun (x : (j : ι) → α j) ↦ x i
Tactic: have : Homeomorph.piUnique _ ∘ Set.restrict {i} = fun (x : Π j, α j) ↦ x i := rfl
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
i : ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this_1 : IsClosed (X := (a : (↑{i} : Type u_1)) → α (↑a : ι)) (restrict (π := α) {i} '' s)
this :
  Eq (α := ((a : ι) → α a) → α (↑default : ι))
    (Function.comp (β := (t : (↑{i} : Type u_1)) → α (↑t : ι))
      (⇑(Homeomorph.piUnique fun (t : (↑{i} : Type u_1)) ↦ α (↑t : ι)) :
        (a : (t : (↑{i} : Type u_1)) → α (↑t : ι)) → α (↑default : ι))
      (restrict (π := α) {i}))
    fun (x : (j : ι) → α j) ↦ x i
⊢ IsClosed.{u_2} (X := α i) ((fun (x : (i : ι) → α i) ↦ x i) '' s)
have rwa : IsClosed.{u_2} (X := α i)
  (Function.comp (β := (t : (↑{i} : Type u_1)) → α (↑t : ι))
      (⇑(Homeomorph.piUnique fun (t : (↑{i} : Type u_1)) ↦ α (↑t : ι)) :
        (a : (t : (↑{i} : Type u_1)) → α (↑t : ι)) → α (↑default : ι))
      (restrict (π := α) {i}) ''
    s)
Tactic: rwa [← this, image_comp, Homeomorph.isClosed_image (Homeomorph.piUnique _)]
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
i : ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this_1 : IsClosed (X := (a : (↑{i} : Type u_1)) → α (↑a : ι)) (restrict (π := α) {i} '' s)
this :
  Eq (α := ((a : ι) → α a) → α (↑default : ι))
    (Function.comp (β := (t : (↑{i} : Type u_1)) → α (↑t : ι))
      (⇑(Homeomorph.piUnique fun (t : (↑{i} : Type u_1)) ↦ α (↑t : ι)) :
        (a : (t : (↑{i} : Type u_1)) → α (↑t : ι)) → α (↑default : ι))
      (restrict (π := α) {i}))
    fun (x : (j : ι) → α j) ↦ x i
rwa :
  IsClosed.{u_2} (X := α i)
    (Function.comp (β := (t : (↑{i} : Type u_1)) → α (↑t : ι))
        (⇑(Homeomorph.piUnique fun (t : (↑{i} : Type u_1)) ↦ α (↑t : ι)) :
          (a : (t : (↑{i} : Type u_1)) → α (↑t : ι)) → α (↑default : ι))
        (restrict (π := α) {i}) ''
      s)
⊢ IsClosed.{u_2} (X := α i) ((fun (x : (i : ι) → α i) ↦ x i) '' s)
have rwa₁ : IsClosed.{u_2} (X := α i)
  (image (α := (t : (↑{i} : Type u_1)) → α (↑t : ι))
    (⇑(Homeomorph.piUnique fun (t : (↑{i} : Type u_1)) ↦ α (↑t : ι)) :
      (a : (t : (↑{i} : Type u_1)) → α (↑t : ι)) → α (↑default : ι))
    (restrict (π := α) {i} '' s))
Tactic: rwa [← this, image_comp, Homeomorph.isClosed_image (Homeomorph.piUnique _)]
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
i : ι
hs_compact : IsCompact s
hs_closed : IsClosed s
⊢ IsClosed.{u_2} (X := α i) ((fun (x : (i : ι) → α i) ↦ x i) '' s)
have suffices : IsClosed (X := (a : (↑{i} : Type u_1)) → α (↑a : ι)) (restrict (π := α) {i} '' s)
Tactic: suffices IsClosed (Set.restrict {i} '' s) by
    have : Homeomorph.piUnique _ ∘ Set.restrict {i} = fun (x : Π j, α j) ↦ x i := rfl
    rwa [← this, image_comp, Homeomorph.isClosed_image (Homeomorph.piUnique _)]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
⊢ IsLocalHomeomorphOn f s ↔ ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
have refine_1 : ∀ (h : IsLocalHomeomorphOn f s) (x : X) (hx : x ∈ s), ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
Tactic: refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
refine_1 :
  ∀ (h : IsLocalHomeomorphOn f s) (x : X) (hx : x ∈ s), ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
⊢ IsLocalHomeomorphOn f s ↔ ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
have refine_2 : ∀ (h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)) (x : X) (hx : x ∈ s),
  ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = (↑e : X → Y)
Tactic: refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : IsLocalHomeomorphOn f s
x : X
hx : x ∈ s
⊢ ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
have refine_1 : ∀ (e : OpenPartialHomeomorph X Y) (hxe : x ∈ e.source) (h : IsLocalHomeomorphOn (↑e : X → Y) s),
  ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) (↑e : X → Y))
Tactic: obtain ⟨e, hxe, rfl⟩ := h x hx
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = (↑e : X → Y)
have refine_2 : ∀ (U : Set X) (hU : U ∈ 𝓝 x) (emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)),
  ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = (↑e : X → Y)
Tactic: obtain ⟨U, hU, emb⟩ := h x hx
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
⊢ IsOpenEmbedding ((interior U).restrict (π := fun (a : X) ↦ Y) f)
have refine : IsOpen[instTopologicalSpaceSubtype]
  (Set.range (ι := (↑(interior U) : Type u_1)) (Set.inclusion (s := interior U) (t := U) sorry))
Tactic: refine emb.comp ⟨.inclusion interior_subset, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
⊢ IsOpen[instTopologicalSpaceSubtype]
    (Set.range (ι := (↑(interior U) : Type u_1)) (Set.inclusion (s := interior U) (t := U) ⋯))
have rw : IsOpen[instTopologicalSpaceSubtype] {x : (↑U : Type u_1) | (↑x : X) ∈ interior U}
Tactic: rw [Set.range_inclusion]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = (↑e : X → Y)
have this : IsOpenEmbedding ((interior U).restrict (π := fun (a : X) ↦ Y) f)
Tactic: have : IsOpenEmbedding ((interior U).restrict f) := by
      refine emb.comp ⟨.inclusion interior_subset, ?_⟩
      rw [Set.range_inclusion]; exact isOpen_induced isOpen_interior
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
this : IsOpenEmbedding ((interior U).restrict (π := fun (a : X) ↦ Y) f)
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = (↑e : X → Y)
have cont : Continuous[instTopologicalSpaceSubtype, inst_1] ((interior U).restrict (π := fun (a : X) ↦ Y) f)
Tactic: obtain ⟨cont, inj, openMap⟩ := isOpenEmbedding_iff_continuous_injective_isOpenMap.mp this
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
this : IsOpenEmbedding ((interior U).restrict (π := fun (a : X) ↦ Y) f)
cont : Continuous[instTopologicalSpaceSubtype, inst_1] ((interior U).restrict (π := fun (a : X) ↦ Y) f)
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = (↑e : X → Y)
have inj : Function.Injective ((interior U).restrict (π := fun (a : X) ↦ Y) f)
Tactic: obtain ⟨cont, inj, openMap⟩ := isOpenEmbedding_iff_continuous_injective_isOpenMap.mp this
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
this : IsOpenEmbedding ((interior U).restrict (π := fun (a : X) ↦ Y) f)
cont : Continuous[instTopologicalSpaceSubtype, inst_1] ((interior U).restrict (π := fun (a : X) ↦ Y) f)
inj : Function.Injective ((interior U).restrict (π := fun (a : X) ↦ Y) f)
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = (↑e : X → Y)
have openMap : IsOpenMap ((interior U).restrict (π := fun (a : X) ↦ Y) f)
Tactic: obtain ⟨cont, inj, openMap⟩ := isOpenEmbedding_iff_continuous_injective_isOpenMap.mp this
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
this : IsOpenEmbedding ((interior U).restrict (π := fun (a : X) ↦ Y) f)
cont : Continuous[instTopologicalSpaceSubtype, inst_1] ((interior U).restrict (π := fun (a : X) ↦ Y) f)
inj : Function.Injective ((interior U).restrict (π := fun (a : X) ↦ Y) f)
openMap : IsOpenMap ((interior U).restrict (π := fun (a : X) ↦ Y) f)
⊢ ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = (↑e : X → Y)
have this₁ : Nonempty X
Tactic: haveI : Nonempty X := ⟨x⟩
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : IsLocalHomeomorphOn f s
inst_2 : DiscreteTopology.{u_2} (↑(f '' s) : Type u_2)
x : (↑s : Type u_1)
⊢ IsOpen[instTopologicalSpaceSubtype] {x}
have obtain : ∀ (e : OpenPartialHomeomorph X Y) (hx : (↑x : X) ∈ e.source) (h : IsLocalHomeomorphOn (↑e : X → Y) s)
  [DiscreteTopology.{u_2} (↑((↑e : X → Y) '' s) : Type u_2)], IsOpen[instTopologicalSpaceSubtype] {x}
Tactic: obtain ⟨e, hx, rfl⟩ := h x x.2
Cleared hypotheses: f, h, inst_2
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
x : (↑s : Type u_1)
e : OpenPartialHomeomorph X Y
hx : (↑x : X) ∈ e.source
h : IsLocalHomeomorphOn (↑e : X → Y) s
inst_2 : DiscreteTopology.{u_2} (↑((↑e : X → Y) '' s) : Type u_2)
⊢ IsOpen[instTopologicalSpaceSubtype] {x}
have have : ∀ (U : Set Y) (hU : IsOpen[inst_1] U)
  (eq :
    Eq (α := Set { x : Y // x ∈ (↑e : X → Y) '' s }) (Subtype.val (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ⁻¹' U)
      {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) (↑x : X)) sorry}),
  IsOpen[instTopologicalSpaceSubtype] {x}
Tactic: have ⟨U, hU, eq⟩ := isOpen_discrete {(⟨_, _, x.2, rfl⟩ : e '' s)}
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
x : (↑s : Type u_1)
e : OpenPartialHomeomorph X Y
hx : (↑x : X) ∈ e.source
h : IsLocalHomeomorphOn (↑e : X → Y) s
inst_2 : DiscreteTopology.{u_2} (↑((↑e : X → Y) '' s) : Type u_2)
U : Set Y
hU : IsOpen[inst_1] U
eq :
  Eq (α := Set { x : Y // x ∈ (↑e : X → Y) '' s }) (Subtype.val (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ⁻¹' U)
    {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) (↑x : X)) ⋯}
⊢ IsOpen[instTopologicalSpaceSubtype] {x}
have refine_1 : ∀ (x' : { x : X // x ∈ s })
  (mem :
    Membership.mem (γ := Set { x : X // x ∈ s })
      (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' (e.source ∩ (↑e : X → Y) ⁻¹' U)) x'),
  (↑e : X → Y) (↑x' : X) = (↑e : X → Y) (↑x : X)
Tactic: refine ⟨e.source ∩ e ⁻¹' U, e.continuousOn_toFun.isOpen_inter_preimage e.open_source hU,
      subset_antisymm (fun x' mem ↦ Subtype.ext <| e.injOn mem.1 hx ?_) ?_⟩
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
x : (↑s : Type u_1)
e : OpenPartialHomeomorph X Y
hx : (↑x : X) ∈ e.source
h : IsLocalHomeomorphOn (↑e : X → Y) s
inst_2 : DiscreteTopology.{u_2} (↑((↑e : X → Y) '' s) : Type u_2)
U : Set Y
hU : IsOpen[inst_1] U
eq :
  Eq (α := Set { x : Y // x ∈ (↑e : X → Y) '' s }) (Subtype.val (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ⁻¹' U)
    {Subtype.mk (p := fun (x : Y) ↦ x ∈ (↑e : X → Y) '' s) ((↑e : X → Y) (↑x : X)) ⋯}
refine_1 :
  ∀ (x' : { x : X // x ∈ s })
    (mem :
      Membership.mem (γ := Set { x : X // x ∈ s })
        (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' (e.source ∩ (↑e : X → Y) ⁻¹' U)) x'),
    (↑e : X → Y) (↑x' : X) = (↑e : X → Y) (↑x : X)
⊢ IsOpen[instTopologicalSpaceSubtype] {x}
have refine_2 : Subset (α := Set { x : X // x ∈ s }) {x} (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' (e.source ∩ (↑e : X → Y) ⁻¹' U))
Tactic: refine ⟨e.source ∩ e ⁻¹' U, e.continuousOn_toFun.isOpen_inter_preimage e.open_source hU,
      subset_antisymm (fun x' mem ↦ Subtype.ext <| e.injOn mem.1 hx ?_) ?_⟩
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : IsLocalHomeomorphOn f s
hs : IsOpen[inst] s
⊢ DiscreteTopology.{u_2} (↑(f '' s) : Type u_2) ↔ DiscreteTopology.{u_1} (↑s : Type u_1)
have refine : DiscreteTopology.{u_1} (↑s : Type u_1) → DiscreteTopology.{u_2} (↑(f '' s) : Type u_2)
Tactic: refine ⟨fun _ ↦ h.discreteTopology_of_image, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : IsLocalHomeomorphOn f s
hs : IsOpen[inst] s
⊢ DiscreteTopology.{u_1} (↑s : Type u_1) → DiscreteTopology.{u_2} (↑(f '' s) : Type u_2)
have simp_rw : (∀ (a : (↑s : Type u_1)), IsOpen[instTopologicalSpaceSubtype] {a}) →
  ∀ (a : (↑(f '' s) : Type u_2)), IsOpen[instTopologicalSpaceSubtype] {a}
Tactic: simp_rw [discreteTopology_iff_isOpen_singleton]