awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : ∀ (ht : ∀ i ∈ s, IsRetrocompact (t i)), IsRetrocompact (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact (t i ⊓ s.inf t)

Tactic:
exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht

Premises used: Finset.forall_of_forall_cons, IsRetrocompact.inter
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
empty : ∀ (ht : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsRetrocompact (t i)), IsRetrocompact (Finset.inf ∅ t)
cons :
  ∀ (i : ι) (s : Finset ι) (ih : i ∉ s) (hi : ∀ (ht : ∀ i ∈ s, IsRetrocompact (t i)), IsRetrocompact (s.inf t))
    (ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)), IsRetrocompact ((Finset.cons i s ih).inf t)
⊢ IsRetrocompact (s.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

Premises used: IsRetrocompact.empty, Finset.forall_of_forall_cons, IsRetrocompact.inter, Finset.inf_cons
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
rw : IsRetrocompact (s.inf t)
⊢ IsRetrocompact (s.inf' hs t)

Tactic:
rw [Finset.inf'_eq_inf]

Premises used: Finset.inf'_eq_inf
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.inf t)

Tactic:
.finsetInf ht

Premises used: IsRetrocompact.finsetInf
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.inf t)

Tactic:
exact .finsetInf ht
-- Module: Mathlib.Topology.Constructible
Goal:
ι : Sort u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Finite ι
f : ι → Set X
hf : ∀ (i : ι), IsRetrocompact (f i)
⊢ IsRetrocompact.{u_2} (X := X) (⋂ (i : ι), f i)

Tactic:
infClosed_isRetrocompact.iInf_mem .univ hf

Premises used: Set.Mem, Set.iInter, IsRetrocompact, setOf, InfClosed.iInf_mem, IsRetrocompact.univ, _private.0.infClosed_isRetrocompact
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
S : Set (Set X)
hS : S.Finite
hS' : ∀ s ∈ S, IsRetrocompact s
⊢ IsRetrocompact (⋂₀ S)

Tactic:
infClosed_isRetrocompact.sInf_mem hS .univ hS'

Premises used: Set.Mem, IsRetrocompact, setOf, Set.sInter, InfClosed.sInf_mem, IsRetrocompact.univ, _private.0.infClosed_isRetrocompact
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
ι : Type u_4
f : ι → Set X
t : Set ι
ht : t.Finite
hf : ∀ i ∈ t, IsRetrocompact (f i)
⊢ IsRetrocompact.{u_2} (X := X) (⋂ i ∈ t, f i)

Tactic:
infClosed_isRetrocompact.biInf_mem ht .univ hf

Premises used: Set.Mem, Set.iInter, IsRetrocompact, setOf, InfClosed.biInf_mem, IsRetrocompact.univ, _private.0.infClosed_isRetrocompact
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsRetrocompact s
ht : IsRetrocompact t
htopen : IsOpen[inst] t
⊢ IsRetrocompact (s ∩ t)

Tactic:
fun _U hUcomp hUopen ↦ inter_assoc .. ▸ hs (ht hUcomp hUopen) (htopen.inter hUopen)

Premises used: IsRetrocompact, Eq.rec, IsOpen.inter, Eq.symm, Set.inter_assoc
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsRetrocompact s
ht : IsRetrocompact t
hsopen : IsOpen[inst] s
⊢ IsRetrocompact (s ∩ t)

Tactic:
inter_comm .. ▸ ht.inter_isOpen hs hsopen

Premises used: Eq.rec, Set.inter_comm, IsRetrocompact.inter_isOpen
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
⊢ IsRetrocompact s ↔ IsSpectralMap.{u_2, u_2} (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))

Tactic:
⟨fun hs ↦ ⟨continuous_subtype_val, fun t htopen htcomp ↦ ?_⟩, fun hs t htcomp htopen ↦ ?_⟩

Premises used: continuous_subtype_val, IsSpectralMap.mk, Iff.intro
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
refine_1 :
  ∀ (hs : IsRetrocompact s) (t : Set X) (htopen : IsOpen[inst] t) (htcomp : IsCompact t),
    IsCompact (X := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
refine_2 :
  ∀ (hs : IsSpectralMap.{u_2, u_2} (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))) (t : Set X)
    (htcomp : IsCompact t) (htopen : IsOpen[inst] t), IsCompact (s ∩ t)
⊢ IsRetrocompact s ↔ IsSpectralMap.{u_2, u_2} (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))

Tactic:
refine ⟨fun hs ↦ ⟨continuous_subtype_val, fun t htopen htcomp ↦ ?_⟩, fun hs t htcomp htopen ↦ ?_⟩
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
hs : IsRetrocompact s
t : Set X
htopen : IsOpen[inst] t
htcomp : IsCompact t
refine_1 : IsCompact (s ∩ t)
⊢ IsCompact (X := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)

Tactic:
rw [IsEmbedding.subtypeVal.isCompact_iff, image_preimage_eq_inter_range,
      Subtype.range_coe_subtype, setOf_mem_eq, inter_comm]

Premises used: Topology.IsEmbedding.isCompact_iff, Subtype.range_coe_subtype, Set.image_preimage_eq_inter_range, Set.setOf_mem_eq, Set.inter_comm, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
hs : IsRetrocompact s
t : Set X
htopen : IsOpen[inst] t
htcomp : IsCompact t
⊢ IsCompact (s ∩ t)

Tactic:
hs htcomp htopen
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
hs : IsRetrocompact s
t : Set X
htopen : IsOpen[inst] t
htcomp : IsCompact t
⊢ IsCompact (s ∩ t)

Tactic:
exact hs htcomp htopen
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
hs : IsSpectralMap.{u_2, u_2} (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
t : Set X
htcomp : IsCompact t
htopen : IsOpen[inst] t
⊢ IsCompact (s ∩ t)

Tactic:
simpa using (hs.isCompact_preimage_of_isOpen htopen htcomp).image continuous_subtype_val

Premises used: continuous_subtype_val, IsSpectralMap.isCompact_preimage_of_isOpen, IsCompact.image
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen[inst_1] U
rw : IsCompact (s ∩ f ⁻¹' U)
⊢ IsCompact (f '' s ∩ U)

Tactic:
rw [← image_inter_preimage, ← hfemb.isCompact_iff]

Premises used: Set.image_inter_preimage, Topology.IsEmbedding.isCompact_iff
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen[inst_1] U
⊢ IsCompact (s ∩ f ⁻¹' U)

Tactic:
hs ?_ <| hUopen.preimage hfemb.continuous

Premises used: IsOpen.preimage, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen[inst_1] U
refine : IsCompact (f ⁻¹' U)
⊢ IsCompact (s ∩ f ⁻¹' U)

Tactic:
refine hs ?_ <| hUopen.preimage hfemb.continuous

Premises used: IsOpen.preimage, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen[inst_1] U
rw : IsCompact (range f ∩ U)
⊢ IsCompact (f ⁻¹' U)

Tactic:
rw [hfemb.isCompact_iff, image_preimage_eq_inter_range, inter_comm]

Premises used: Topology.IsEmbedding.isCompact_iff, Set.image_preimage_eq_inter_range, Set.inter_comm
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen[inst_1] U
⊢ IsCompact (range f ∩ U)

Tactic:
hfcomp hUcomp hUopen
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen[inst_1] U
⊢ IsCompact (range f ∩ U)

Tactic:
exact hfcomp hUcomp hUopen
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsOpenEmbedding f
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst] U
rw : IsCompact (s ∩ f '' U)
⊢ IsCompact (f ⁻¹' s ∩ U)

Tactic:
rw [hf.isCompact_iff, image_preimage_inter]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsEmbedding.isCompact_iff, Set.image_preimage_inter
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsOpenEmbedding f
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst] U
⊢ IsCompact (s ∩ f '' U)

Tactic:
hs (hUcomp.image hf.continuous) <| hf.isOpenMap _ hUopen

Premises used: Topology.IsOpenEmbedding.isOpenMap, Topology.IsOpenEmbedding.continuous, IsCompact.image
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsOpenEmbedding f
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst] U
⊢ IsCompact (s ∩ f '' U)

Tactic:
exact hs (hUcomp.image hf.continuous) <| hf.isOpenMap _ hUopen

Premises used: Topology.IsOpenEmbedding.isOpenMap, Topology.IsOpenEmbedding.continuous, IsCompact.image
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst] U
⊢ IsOpen[inst_1] (f '' U ∪ (range f)ᶜ)

Tactic:
simpa [← range_diff_image hf.injective, sdiff_eq, compl_inter, union_comm]
      using (hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl

Premises used: IsClosed.isOpen_compl, Set.range_diff_image, Set.compl_inter, sdiff_eq, Set.union_comm, Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst] U
⊢ IsOpen[inst_1] (f '' U ∪ (range f)ᶜ)

Tactic:
have hfUopen : 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
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst] U
hfUopen : IsOpen[inst_1] (f '' U ∪ (range f)ᶜ)
⊢ IsCompact (f '' U ∪ (range f)ᶜ)

Tactic:
have hfUcomp : IsCompact (f '' U ∪ (range f)ᶜ) := (hUcomp.image hf.continuous).union hf'
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst] U
hfUopen : IsOpen[inst_1] (f '' U ∪ (range f)ᶜ)
hfUcomp : IsCompact (f '' U ∪ (range f)ᶜ)
⊢ IsCompact (f ⁻¹' s ∩ U)

Tactic:
simpa [inter_union_distrib_left, inter_left_comm, inter_eq_right.2 (image_subset_range ..),
    hf.isCompact_iff, image_preimage_inter] using (hs hfUcomp hfUopen).inter_left hf.isClosed_range

Premises used: Iff.mpr, IsCompact.inter_left, Set.inter_left_comm, Topology.IsEmbedding.isCompact_iff, Set.image_preimage_inter, Set.image_subset_range, Set.inter_eq_right, Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsClosedEmbedding.isClosed_range, Set.inter_union_distrib_left
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
⊢ IsConstructible.{u_2} (X := X) ∅

Tactic:
BooleanSubalgebra.bot_mem

Premises used: Set.Mem, Topology.IsConstructible, BooleanSubalgebra.bot_mem
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
⊢ IsConstructible.{u_2} (X := X) univ

Tactic:
BooleanSubalgebra.top_mem

Premises used: BooleanSubalgebra.top_mem, Set.Mem, Topology.IsConstructible
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
⊢ IsConstructible s → IsConstructible t → IsConstructible (s ∪ t)

Tactic:
BooleanSubalgebra.sup_mem

Premises used: Set.Mem, BooleanSubalgebra.sup_mem, Topology.IsConstructible
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
⊢ IsConstructible s → IsConstructible t → IsConstructible (s ∩ t)

Tactic:
BooleanSubalgebra.inf_mem

Premises used: Set.Mem, BooleanSubalgebra.inf_mem, Topology.IsConstructible
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
⊢ IsConstructible s → IsConstructible t → IsConstructible (s \ t)

Tactic:
BooleanSubalgebra.sdiff_mem

Premises used: Set.Mem, BooleanSubalgebra.sdiff_mem, Topology.IsConstructible
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
⊢ IsConstructible s → IsConstructible t → IsConstructible (s ⇨ t)

Tactic:
BooleanSubalgebra.himp_mem

Premises used: Set.Mem, Topology.IsConstructible, BooleanSubalgebra.himp_mem
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
⊢ IsConstructible sᶜ ↔ IsConstructible s

Tactic:
BooleanSubalgebra.compl_mem_iff

Premises used: Set.Mem, BooleanSubalgebra.compl_mem_iff, Topology.IsConstructible
-- Module: Mathlib.Topology.Constructible
Goal:
ι : Sort u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Finite ι
f : ι → Set X
hf : ∀ (i : ι), IsConstructible (f i)
⊢ IsConstructible.{u_2} (X := X) (⋃ (i : ι), f i)

Tactic:
BooleanSubalgebra.iSup_mem hf

Premises used: Set.Mem, Topology.IsConstructible, BooleanSubalgebra.iSup_mem, Set.iUnion
-- Module: Mathlib.Topology.Constructible
Goal:
ι : Sort u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Finite ι
f : ι → Set X
hf : ∀ (i : ι), IsConstructible (f i)
⊢ IsConstructible.{u_2} (X := X) (⋂ (i : ι), f i)

Tactic:
BooleanSubalgebra.iInf_mem hf

Premises used: Set.Mem, Set.iInter, Topology.IsConstructible, BooleanSubalgebra.iInf_mem
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
hS' : ∀ s ∈ S, IsConstructible s
⊢ IsConstructible (⋃₀ S)

Tactic:
BooleanSubalgebra.sSup_mem hS hS'

Premises used: Set.Mem, Set.sUnion, BooleanSubalgebra.sSup_mem, Topology.IsConstructible
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
hS' : ∀ s ∈ S, IsConstructible s
⊢ IsConstructible (⋂₀ S)

Tactic:
BooleanSubalgebra.sInf_mem hS hS'

Premises used: Set.Mem, Topology.IsConstructible, BooleanSubalgebra.sInf_mem, Set.sInter
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
f : ι → Set X
t : Set ι
ht : t.Finite
hf : ∀ i ∈ t, IsConstructible (f i)
⊢ IsConstructible.{u_2} (X := X) (⋃ i ∈ t, f i)

Tactic:
BooleanSubalgebra.biSup_mem ht hf

Premises used: Set.Mem, BooleanSubalgebra.biSup_mem, Topology.IsConstructible, Set.iUnion
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
f : ι → Set X
t : Set ι
ht : t.Finite
hf : ∀ i ∈ t, IsConstructible (f i)
⊢ IsConstructible.{u_2} (X := X) (⋂ i ∈ t, f i)

Tactic:
BooleanSubalgebra.biInf_mem ht hf

Premises used: Set.Mem, Set.iInter, Topology.IsConstructible, BooleanSubalgebra.biInf_mem
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
U : Set X
hUopen : IsOpen[inst] U
hUcomp : IsRetrocompact U
⊢ IsConstructible U

Tactic:
BooleanSubalgebra.subset_closure ⟨hUopen, hUcomp⟩

Premises used: BooleanSubalgebra.subset_closure, And.intro, Topology.IsConstructible
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s U : Set X
hU : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U} U
⊢ p U ⋯

Tactic:
open_retrocompact _ hU.1 hU.2

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s U : Set X
hU : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U} U
⊢ p U ⋯

Tactic:
exact open_retrocompact _ hU.1 hU.2

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s : Set X
⊢ p ⊥ ⋯

Tactic:
open_retrocompact _ isOpen_empty .empty

Premises used: IsRetrocompact.empty, isOpen_empty
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s : Set X
⊢ p ⊥ ⋯

Tactic:
exact open_retrocompact _ isOpen_empty .empty

Premises used: IsRetrocompact.empty, isOpen_empty
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s_1 s : Set X
hs :
  Membership.mem (γ := BooleanSubalgebra (Set X))
    (BooleanSubalgebra.closure {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U}) s
t : Set X
ht :
  Membership.mem (γ := BooleanSubalgebra (Set X))
    (BooleanSubalgebra.closure {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U}) t
hs' : p s hs
ht' : p t ht
⊢ p (s ⊔ t) ⋯

Tactic:
union _ _ _ _ hs' ht'
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s_1 s : Set X
hs :
  Membership.mem (γ := BooleanSubalgebra (Set X))
    (BooleanSubalgebra.closure {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U}) s
t : Set X
ht :
  Membership.mem (γ := BooleanSubalgebra (Set X))
    (BooleanSubalgebra.closure {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U}) t
hs' : p s hs
ht' : p t ht
⊢ p (s ⊔ t) ⋯

Tactic:
exact union _ _ _ _ hs' ht'
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s_1 s : Set X
hs :
  Membership.mem (γ := BooleanSubalgebra (Set X))
    (BooleanSubalgebra.closure {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U}) s
hs' : p s hs
⊢ p sᶜ ⋯

Tactic:
compl _ _ hs'
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s_1 s : Set X
hs :
  Membership.mem (γ := BooleanSubalgebra (Set X))
    (BooleanSubalgebra.closure {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U}) s
hs' : p s hs
⊢ p sᶜ ⋯

Tactic:
exact compl _ _ hs'
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s : Set X
hs : IsConstructible s
mem : ∀ (U : Set X) (hU : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U} U), p U ⋯
bot : p ⊥ ⋯
sup :
  ∀ (s : Set X)
    (hs :
      Membership.mem (γ := BooleanSubalgebra (Set X))
        (BooleanSubalgebra.closure {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U}) s)
    (t : Set X)
    (ht :
      Membership.mem (γ := BooleanSubalgebra (Set X))
        (BooleanSubalgebra.closure {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U}) t)
    (hs' : p s hs) (ht' : p t ht), p (s ⊔ t) ⋯
compl₁ :
  ∀ (s : Set X)
    (hs :
      Membership.mem (γ := BooleanSubalgebra (Set X))
        (BooleanSubalgebra.closure {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U}) s)
    (hs' : p s hs), p sᶜ ⋯
⊢ p s hs

Tactic:
induction hs using BooleanSubalgebra.closure_bot_sup_induction with
  | mem U hU => exact open_retrocompact _ hU.1 hU.2
  | bot => exact open_retrocompact _ isOpen_empty .empty
  | sup s hs t ht hs' ht' => exact union _ _ _ _ hs' ht'
  | compl s hs hs' => exact compl _ _ hs'

Premises used: IsRetrocompact.empty, isOpen_empty
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hfcont : Continuous[inst, inst_1] f
hf : ∀ (s : Set Y), IsOpen[inst_1] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
U : Set Y
hUopen : IsOpen[inst_1] U
hUcomp : IsRetrocompact U
⊢ IsConstructible (f ⁻¹' U)

Tactic:
(hf _ hUopen hUcomp).isConstructible <| hUopen.preimage hfcont

Premises used: IsRetrocompact.isConstructible, IsOpen.preimage