awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
hs : IsConstructible s
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] U) (hUcomp : IsRetrocompact U), IsConstructible (f '' U)
⊢ IsConstructible (f '' s)
have union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t) (hs' : IsConstructible (f '' s))
  (ht' : IsConstructible (f '' t)), IsConstructible (f '' (s ∪ t))
Tactic: induction hs using IsConstructible.empty_union_induction with
  | open_retrocompact U hUopen hUcomp =>
    have hfU : IsOpen (f '' U ∪ (range f)ᶜ) := by
      simpa [← range_diff_image hf.injective, sdiff_eq, compl_inter, union_comm]
        using (hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl
    suffices h : IsRetrocompact (f '' U ∪ (range f)ᶜ) by
      simpa [union_inter_distrib_right, inter_eq_left.2 (image_subset_range ..)]
        using (h.isConstructible hfU).sdiff (hfcomp.isConstructible hf.isClosed_range.isOpen_compl)
    rintro V hVcomp hVopen
    rw [union_inter_distrib_right, ← image_inter_preimage]
    exact ((hUcomp (hf.isCompact_preimage hVcomp) (hVopen.preimage hf.continuous)).image
      hf.continuous).union <| hfcomp hVcomp hVopen
  | union s hs t ht hs' ht' => rw [image_union]; exact hs'.union ht'
  | compl s hs hs' =>
    rw [← range_diff_image hf.injective]
    exact (hfcomp.isConstructible hf.isClosed_range.isOpen_compl).of_compl.sdiff hs'
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
hs : IsConstructible s
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] U) (hUcomp : IsRetrocompact U), IsConstructible (f '' U)
union :
  ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t) (hs' : IsConstructible (f '' s))
    (ht' : IsConstructible (f '' t)), IsConstructible (f '' (s ∪ t))
⊢ IsConstructible (f '' s)
have compl : ∀ (s : Set X) (hs : IsConstructible s) (hs' : IsConstructible (f '' s)), IsConstructible (f '' sᶜ)
Tactic: induction hs using IsConstructible.empty_union_induction with
  | open_retrocompact U hUopen hUcomp =>
    have hfU : IsOpen (f '' U ∪ (range f)ᶜ) := by
      simpa [← range_diff_image hf.injective, sdiff_eq, compl_inter, union_comm]
        using (hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl
    suffices h : IsRetrocompact (f '' U ∪ (range f)ᶜ) by
      simpa [union_inter_distrib_right, inter_eq_left.2 (image_subset_range ..)]
        using (h.isConstructible hfU).sdiff (hfcomp.isConstructible hf.isClosed_range.isOpen_compl)
    rintro V hVcomp hVopen
    rw [union_inter_distrib_right, ← image_inter_preimage]
    exact ((hUcomp (hf.isCompact_preimage hVcomp) (hVopen.preimage hf.continuous)).image
      hf.continuous).union <| hfcomp hVcomp hVopen
  | union s hs t ht hs' ht' => rw [image_union]; exact hs'.union ht'
  | compl s hs hs' =>
    rw [← range_diff_image hf.injective]
    exact (hfcomp.isConstructible hf.isClosed_range.isOpen_compl).of_compl.sdiff hs'
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact (↑(U i) : Set X)
h₂ : ∀ (i : ι), IsQuasiSeparated (↑(U i) : Set X)
V₁ V₂ : Set X
ho₁ : IsOpen[inst] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst] V₂
hc₂ : IsCompact V₂
⊢ IsCompact (V₁ ∩ V₂)
have obtain : ∀ (t : Finset ι) (ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier), IsCompact (V₁ ∩ V₂)
Tactic: obtain ⟨t, ht⟩ := hc₁.elim_finite_subcover _ (fun i ↦ (U i).2) (by simp [hU.iSup_set_eq_univ])
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact (↑(U i) : Set X)
h₂ : ∀ (i : ι), IsQuasiSeparated (↑(U i) : Set X)
V₁ V₂ : Set X
ho₁ : IsOpen[inst] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
⊢ IsCompact (V₁ ∩ V₂)
have h : V₁ ∩ V₂ = ⋃ i ∈ t, (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂)
Tactic: convert!
      t.isCompact_biUnion fun i _ ↦
        h₂ i _ _ Set.inter_subset_left ((U i).2.inter ho₁) (h₁ i hc₁ ho₁) Set.inter_subset_left
          ((U i).2.inter ho₂) (h₁ i hc₂ ho₂)
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact (↑(U i) : Set X)
h₂ : ∀ (i : ι), IsQuasiSeparated (↑(U i) : Set X)
V₁ V₂ : Set X
ho₁ : IsOpen[inst] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
⊢ V₁ ∩ V₂ = ⋃ i ∈ t, (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂)
have h : V₁ ∩ V₂ ⊆ ⋃ i ∈ t, (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂)
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact (↑(U i) : Set X)
h₂ : ∀ (i : ι), IsQuasiSeparated (↑(U i) : Set X)
V₁ V₂ : Set X
ho₁ : IsOpen[inst] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
h : V₁ ∩ V₂ ⊆ ⋃ i ∈ t, (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂)
⊢ V₁ ∩ V₂ = ⋃ i ∈ t, (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂)
have h₃ : ⋃ i ∈ t, (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂) ⊆ V₁ ∩ V₂
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact (↑(U i) : Set X)
h₂ : ∀ (i : ι), IsQuasiSeparated (↑(U i) : Set X)
V₁ V₂ : Set X
ho₁ : IsOpen[inst] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
x : X
hx₁ : x ∈ V₁
hx₂ : x ∈ V₂
⊢ Membership.mem (γ := Set X) (⋃ i ∈ t, (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂)) x
have h : ∀ (i : ι) (hi : i ∈ t) (hxi : x ∈ (U i).carrier),
  Membership.mem (γ := Set X) (⋃ i ∈ t, (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂)) x
Tactic: obtain ⟨i, hi, hxi⟩ := Set.mem_iUnion₂.mp (ht hx₁)
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s ∩ t)
have obtain : ∀ (U : Set X) (hxU : U ∈ 𝓝 x) (hU : IsOpen[inst] U) (hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)),
  ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s ∩ t)
Tactic: obtain ⟨U, hxU, hU, hsU⟩ := hs x
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s ∩ t)
have obtain : ∀ (V : Set X) (hxV : V ∈ 𝓝 x) (hV : IsOpen[inst] V) (htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)),
  ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s ∩ t)
Tactic: obtain ⟨V, hxV, hV, htV⟩ := ht x
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s ∩ t)
have refine : IsConstructible (X := (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ s ∩ t)
Tactic: refine ⟨U ∩ V, Filter.inter_mem hxU hxV, hU.inter hV, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
⊢ IsConstructible (X := (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ s ∩ t)
have change : IsConstructible (X := (↑(U ∩ V) : Type u_2))
  ((inclusion (s := U ∩ V) (t := U) sorry ⁻¹' U ↓∩ s) ∩ inclusion (s := U ∩ V) (t := V) sorry ⁻¹' V ↓∩ t)
Tactic: change IsConstructible
    (inclusion inter_subset_left ⁻¹' (U ↓∩ s) ∩ inclusion inter_subset_right ⁻¹' (V ↓∩ t))
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : ∀ (ht : ∀ i ∈ s, IsLocallyConstructible (t i)), IsLocallyConstructible (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsLocallyConstructible (t i_1)
⊢ IsLocallyConstructible ((Finset.cons i s ih).inf t)
have cons : IsLocallyConstructible (t i ⊓ s.inf t)
Tactic: rw [Finset.inf_cons]
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (s.inf t)
have empty : ∀ (ht : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsLocallyConstructible (t i)),
  IsLocallyConstructible (Finset.inf ∅ t)
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons i s ih hi =>
    rw [Finset.inf_cons]
    exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht
Cleared hypotheses: s, ht
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
empty :
  ∀ (ht : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsLocallyConstructible (t i)),
    IsLocallyConstructible (Finset.inf ∅ t)
⊢ IsLocallyConstructible (s.inf t)
have cons : ∀ (i : ι) (s : Finset ι) (ih : i ∉ s)
  (hi : ∀ (ht : ∀ i ∈ s, IsLocallyConstructible (t i)), IsLocallyConstructible (s.inf t))
  (ht : ∀ i_1 ∈ Finset.cons i s ih, IsLocallyConstructible (t i_1)), IsLocallyConstructible ((Finset.cons i s ih).inf t)
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons i s ih hi =>
    rw [Finset.inf_cons]
    exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht
Cleared hypotheses: s, ht
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (s.inf' hs t)
have rw : IsLocallyConstructible (s.inf t)
Tactic: rw [Finset.inf'_eq_inf]
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ (s ∪ t))
have obtain : ∀ (U : Set X) (hxU : U ∈ 𝓝 x) (hU : IsOpen[inst] U) (hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)),
  ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ (s ∪ t))
Tactic: obtain ⟨U, hxU, hU, hsU⟩ := hs x
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ (s ∪ t))
have obtain : ∀ (V : Set X) (hxV : V ∈ 𝓝 x) (hV : IsOpen[inst] V) (htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)),
  ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ (s ∪ t))
Tactic: obtain ⟨V, hxV, hV, htV⟩ := ht x
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ (s ∪ t))
have refine : IsConstructible (X := (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ (s ∪ t))
Tactic: refine ⟨U ∩ V, Filter.inter_mem hxU hxV, hU.inter hV, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
⊢ Eq (α := Set (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ (s ∪ t))
    (inclusion (s := U ∩ V) (t := U) ⋯ ⁻¹' U ↓∩ s ∪ inclusion (s := U ∩ V) (t := V) ⋯ ⁻¹' V ↓∩ t)
have h : ∀ (x : (↑(U ∩ V) : Type u_2)),
  Membership.mem (γ := Set (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ (s ∪ t)) x ↔
    Membership.mem (γ := Set (↑(U ∩ V) : Type u_2))
      (inclusion (s := U ∩ V) (t := U) sorry ⁻¹' U ↓∩ s ∪ inclusion (s := U ∩ V) (t := V) sorry ⁻¹' V ↓∩ t) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Constructible (hypothesis)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
⊢ IsConstructible (X := (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ (s ∪ t))
have this : Eq (α := Set (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ (s ∪ t))
  (inclusion (s := U ∩ V) (t := U) sorry ⁻¹' U ↓∩ s ∪ inclusion (s := U ∩ V) (t := V) sorry ⁻¹' V ↓∩ t)
Tactic: have : (U ∩ V) ↓∩ (s ∪ t) =
      inclusion inter_subset_left ⁻¹' (U ↓∩ s) ∪ inclusion inter_subset_right ⁻¹' (V ↓∩ t) := by
    ext; simp
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
this :
  Eq (α := Set (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ (s ∪ t))
    (inclusion (s := U ∩ V) (t := U) ⋯ ⁻¹' U ↓∩ s ∪ inclusion (s := U ∩ V) (t := V) ⋯ ⁻¹' V ↓∩ t)
⊢ IsConstructible (X := (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ (s ∪ t))
have rw : IsConstructible (X := (↑(U ∩ V) : Type u_2))
  (inclusion (s := U ∩ V) (t := U) sorry ⁻¹' U ↓∩ s ∪ inclusion (s := U ∩ V) (t := V) sorry ⁻¹' V ↓∩ t)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsLocallyConstructible s
hf : IsOpenEmbedding f
x : X
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ f ⁻¹' s)
have obtain : ∀ (U : Set Y) (hxU : U ∈ 𝓝 (f x)) (hU : IsOpen[inst_1] U) (H : IsConstructible (X := (↑U : Type u_3)) (U ↓∩ s)),
  ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ f ⁻¹' s)
Tactic: obtain ⟨U, hxU, hU, H⟩ := hs (f x)
-- Lean 4 proof step from Mathlib.Topology.Constructible (hypothesis)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hUs : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hV₁ : IsOpen[inst] V
hV₂ : IsCompact V
hxV : x ∈ V
hVU : V ⊆ U
this : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ s)
⊢ IsConstructible (V ∩ s)
have this₁ : IsConstructible (image (α := { x : X // x ∈ V }) (Subtype.val (p := fun (x : X) ↦ x ∈ V)) (V ↓∩ s))
Tactic: have := this.image_of_isOpenEmbedding hV₁.isOpenEmbedding_subtypeVal
        (by simpa using hV₂.isRetrocompact hV₁)
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hUs : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hV₁ : IsOpen[inst] V
hV₂ : IsCompact V
hxV : x ∈ V
hVU : V ⊆ U
this_1 : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ s)
this : IsConstructible (image (α := { x : X // x ∈ V }) (Subtype.val (p := fun (x : X) ↦ x ∈ V)) (V ↓∩ s))
⊢ IsConstructible (V ∩ s)
have rwa : ∀ (this : IsConstructible (V ∩ s)), IsConstructible (V ∩ s)
Tactic: rwa [Subtype.image_preimage_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Constructible (hypothesis)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
⊢ IsConstructible s
have this : ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ IsCompact U ∧ x ∈ U ∧ IsConstructible (U ∩ s)
Tactic: have (x : _) : ∃ U, IsOpen U ∧ IsCompact U ∧ x ∈ U ∧ IsConstructible (U ∩ s) :=
    have ⟨U, hxU, hU, hUs⟩ := hs x
    have ⟨V, ⟨hV₁, hV₂⟩, hxV, hVU⟩ := PrespectralSpace.isTopologicalBasis.mem_nhds_iff.mp hxU
    have : IsConstructible (V ↓∩ s) :=
      (hUs.preimage_of_isOpenEmbedding (IsOpenEmbedding.id.restrict hVU hV₁) :)
    have : IsConstructible (V ∩ s) := by
      have := this.image_of_isOpenEmbedding hV₁.isOpenEmbedding_subtypeVal
        (by simpa using hV₂.isRetrocompact hV₁)
      rwa [Subtype.image_preimage_coe] at this
    ⟨V, hV₁, hV₂, hxV, this⟩
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
this : ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ IsCompact U ∧ x ∈ U ∧ IsConstructible (U ∩ s)
⊢ IsConstructible s
have choose : ∀ (U : (x : X) → Set X) (hU : ∀ (x : X), IsOpen[inst] (U x)) (hU' : ∀ (x : X), IsCompact (U x))
  (hxU : ∀ (x : X), x ∈ U x) (hUs : ∀ (x : X), IsConstructible (U x ∩ s)), IsConstructible s
Tactic: choose U hU hU' hxU hUs using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : (x : X) → Set X
hU : ∀ (x : X), IsOpen[inst] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
⊢ IsConstructible s
have obtain : ∀ (σ : Finset X) (hσ : ∀ x ∈ σ, x ∈ t) (htσ : t ⊆ ⋃ x ∈ σ, U x), IsConstructible s
Tactic: obtain ⟨σ, hσ, htσ⟩ := ht.elim_nhds_subcover U (fun x _ ↦ (hU x).mem_nhds (hxU x))
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : (x : X) → Set X
hU : ∀ (x : X), IsOpen[inst] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
⊢ IsConstructible s
have h : s = ⋃ i ∈ (↑σ : Set X), U i ∩ s
Tactic: convert! IsConstructible.biUnion σ.finite_toSet (fun x _ ↦ hUs x)
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : (x : X) → Set X
hU : ∀ (x : X), IsOpen[inst] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
⊢ s = ⋃ i ∈ (↑σ : Set X), U i ∩ s
have h : s ⊆ ⋃ i ∈ (↑σ : Set X), U i ∩ s
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : (x : X) → Set X
hU : ∀ (x : X), IsOpen[inst] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
h : s ⊆ ⋃ i ∈ (↑σ : Set X), U i ∩ s
⊢ s = ⋃ i ∈ (↑σ : Set X), U i ∩ s
have h₁ : ⋃ i ∈ (↑σ : Set X), U i ∩ s ⊆ s
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : (x : X) → Set X
hU : ∀ (x : X), IsOpen[inst] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
⊢ s ⊆ ⋃ i ∈ (↑σ : Set X), U i ∩ s
have h : s ⊆ ⋃ i ∈ (↑σ : Set X), U i ∧ s ⊆ s
Tactic: rw [← Set.iUnion₂_inter, Set.subset_inter_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2)) ((↑(U i) : Set X) ↓∩ s)
x : X
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
have have : ∀ (i : ι) (hi : x ∈ U i), ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
Tactic: have ⟨i, hi⟩ := hU.exists_mem x
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2)) ((↑(U i) : Set X) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
have have : ∀ (V : Set (↑(↑(U i) : Set X) : Type u_2)) (hVx : V ∈ 𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) x hi))
  (hV : IsOpen[instTopologicalSpaceSubtype] V)
  (hV' : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ (↑(U i) : Set X) ↓∩ s)),
  ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
Tactic: have ⟨V, hVx, hV, hV'⟩ := H i ⟨x, hi⟩
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2)) ((↑(U i) : Set X) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
V : Set (↑(↑(U i) : Set X) : Type u_2)
hVx : V ∈ 𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) x hi)
hV : IsOpen[instTopologicalSpaceSubtype] V
hV' : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ (↑(U i) : Set X) ↓∩ s)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
have refine : IsConstructible (X := (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2)) ((Subtype.val '' V) ↓∩ s)
Tactic: refine ⟨_, (U i).2.isOpenEmbedding_subtypeVal.image_mem_nhds.mpr hVx,
      (U i).2.isOpenMap_subtype_val _ hV, ?_⟩