awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
inst_2 : TopologicalSpace α
inst_3 : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set (↑T : Type u_1)
ha : ∃ (a : Set α), a.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure a) : Set α))ᶜ = R
h :
  ∀ (F : Set α) (hF : F.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure F) : Set α))ᶜ = R),
    ∃ (a : α), (hull T a)ᶜ = R
⊢ ∃ (a : α), (hull T a)ᶜ = R

Tactic:
obtain ⟨F, hF⟩ := ha
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
inst_2 : TopologicalSpace α
inst_3 : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set (↑T : Type u_1)
F : Set α
hF : F.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure F) : Set α))ᶜ = R
⊢ F.Finite

Tactic:
hF.1

Premises used: And.left
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
inst_2 : TopologicalSpace α
inst_3 : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set (↑T : Type u_1)
F : Set α
hF : F.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure F) : Set α))ᶜ = R
h :
  ∀ (F : Finset α)
    (hF :
      (↑F : Set α).Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure (↑F : Set α)) : Set α))ᶜ = R),
    ∃ (a : α), (hull T a)ᶜ = R
⊢ ∃ (a : α), (hull T a)ᶜ = R

Tactic:
lift F to Finset α using hF.1

Premises used: Finset, And.left
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
inst_2 : TopologicalSpace α
inst_3 : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set (↑T : Type u_1)
F : Finset α
hF : (↑F : Set α).Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure (↑F : Set α)) : Set α))ᶜ = R
h : (hull T (F.inf id))ᶜ = R
⊢ ∃ (a : α), (hull T a)ᶜ = R

Tactic:
use Finset.inf F id

Premises used: id, Finset.inf
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
inst_2 : TopologicalSpace α
inst_3 : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set (↑T : Type u_1)
F : Finset α
hF : (↑F : Set α).Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure (↑F : Set α)) : Set α))ᶜ = R
h : ∀ (x : (↑T : Type u_1)), x ∈ (hull T (F.inf id))ᶜ ↔ x ∈ R
⊢ (hull T (F.inf id))ᶜ = R

Tactic:
ext
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
inst_2 : TopologicalSpace α
inst_3 : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set (↑T : Type u_1)
F : Finset α
hF : (↑F : Set α).Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure (↑F : Set α)) : Set α))ᶜ = R
x : (↑T : Type u_1)
⊢ x ∈ (hull T (F.inf id))ᶜ ↔ x ∈ R

Tactic:
simp [hull_finsetInf hT, ← hF.2]

Premises used: PrimitiveSpectrum.hull_finsetInf, And.right
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
ι : Sort v
s : ι → α
⊢ hull T (iSup s) = ⋂ (i : ι), hull T (s i)

Tactic:
aesop
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T S : Set α
⊢ hull T (sSup S) = ⋂₀ {x : Set (↑T : Type u_1) | ∃ a ∈ S, hull T a = x}

Tactic:
aesop
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
S : Set (↑T : Type u_1)
mp : IsOpen[instTopologicalSpaceSubtype] S → ∃ (a : α), S = (hull T a)ᶜ
mpr : (∃ (a : α), S = (hull T a)ᶜ) → IsOpen[instTopologicalSpaceSubtype] S
⊢ IsOpen[instTopologicalSpaceSubtype] S ↔ ∃ (a : α), S = (hull T a)ᶜ

Tactic:
constructor
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
S : Set (↑T : Type u_1)
h : IsOpen[instTopologicalSpaceSubtype] S
R : Set α := {a : α | (hull T a)ᶜ ⊆ S}
h₁ : S = (hull T (sSup R))ᶜ
⊢ ∃ (a : α), S = (hull T a)ᶜ

Tactic:
use sSup R

Premises used: SupSet.sSup
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
S : Set (↑T : Type u_1)
h : IsOpen[instTopologicalSpaceSubtype] S
R : Set α := {a : α | (hull T a)ᶜ ⊆ S}
h₁ :
  ⋃₀
      {s : Set (↑T : Type u_1) |
        Membership.mem (γ := Set (Set (↑T : Type u_1))) {S : Set (↑T : Type u_1) | ∃ (a : α), (hull T a)ᶜ = S} s ∧
          s ⊆ S} =
    (hull T (sSup R))ᶜ
⊢ S = (hull T (sSup R))ᶜ

Tactic:
rw [IsTopologicalBasis.open_eq_sUnion' (isTopologicalBasis_relativeLower hT) h]

Premises used: PrimitiveSpectrum.isTopologicalBasis_relativeLower, TopologicalSpace.IsTopologicalBasis.open_eq_sUnion'
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
S : Set (↑T : Type u_1)
h : IsOpen[instTopologicalSpaceSubtype] S
R : Set α := {a : α | (hull T a)ᶜ ⊆ S}
⊢ ⋃₀
      {s : Set (↑T : Type u_1) |
        Membership.mem (γ := Set (Set (↑T : Type u_1))) {S : Set (↑T : Type u_1) | ∃ (a : α), (hull T a)ᶜ = S} s ∧
          s ⊆ S} =
    (hull T (sSup R))ᶜ

Tactic:
aesop
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
S : Set (↑T : Type u_1)
h : ∃ (a : α), S = (hull T a)ᶜ
mpr : ∀ (a : α) (ha : S = (hull T a)ᶜ), IsOpen[instTopologicalSpaceSubtype] S
⊢ IsOpen[instTopologicalSpaceSubtype] S

Tactic:
obtain ⟨a, ha⟩ := h
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
S : Set (↑T : Type u_1)
a : α
ha : S = (hull T a)ᶜ
⊢ IsOpen[instTopologicalSpaceSubtype] S

Tactic:
⟨(Ici a)ᶜ, isClosed_Ici.isOpen_compl, ha.symm⟩

Premises used: Set.Ici, IsClosed.isOpen_compl, Compl.compl, And.intro, Exists.intro, IsOpen, Eq.symm
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
S : Set (↑T : Type u_1)
a : α
ha : S = (hull T a)ᶜ
⊢ IsOpen[instTopologicalSpaceSubtype] S

Tactic:
exact ⟨(Ici a)ᶜ, isClosed_Ici.isOpen_compl, ha.symm⟩
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
S : Set (↑T : Type u_1)
⊢ IsClosed[instTopologicalSpaceSubtype] S ↔ ∃ (a : α), S = hull T a

Tactic:
simp only [← isOpen_compl_iff, isOpen_iff hT, compl_inj_iff]

Premises used: PrimitiveSpectrum.isOpen_iff, compl_inj_iff, isOpen_compl_iff
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
S : Set (↑T : Type u_1)
a : αᵒᵈ
⊢ (fun (S : Set (↑T : Type u_1)) ↦ ((toDual : (a : α) → αᵒᵈ) (kernel (T := T) S) : αᵒᵈ)) S ≤ a ↔
    S ≤ (fun (a : αᵒᵈ) ↦ hull T ((ofDual : (a : αᵒᵈ) → α) a)) a

Tactic:
simp [Set.subset_def]

Premises used: Set.subset_def
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
S : Set (↑T : Type u_1)
simp :
  hull T
      (sInf
        (preimage (β := αᵒᵈ) (⇑OrderDual.toDual : (a : α) → αᵒᵈ)
          ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S))) =
    hull T (kernel (T := T) S)
⊢ (GaloisConnection.closureOperator (u := fun (a : αᵒᵈ) ↦ hull T ((OrderDual.ofDual : (a : αᵒᵈ) → α) a)) ⋯ :
        (a : Set (↑T : Type u_1)) → Set (↑T : Type u_1))
      S =
    hull T (kernel (T := T) S)

Tactic:
simp only [toDual_sInf, GaloisConnection.closureOperator_apply, ofDual_sSup]

Premises used: toDual_sInf, GaloisConnection.closureOperator_apply, ofDual_sSup
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
S : Set (↑T : Type u_1)
rw :
  hull T
      (sInf
        (Function.comp (β := αᵒᵈ) (⇑OrderDual.ofDual : (a : αᵒᵈ) → α) (⇑OrderDual.toDual : (a : α) → αᵒᵈ) ⁻¹'
          Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S)) =
    hull T (kernel (T := T) S)
rw₁ :
  hull T
      (sInf
        (Function.comp (β := αᵒᵈ) (⇑(Equiv.symm OrderDual.toDual) : (a : αᵒᵈ) → α)
            (⇑OrderDual.toDual : (a : α) → αᵒᵈ) ⁻¹'
          Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S)) =
    hull T (kernel (T := T) S)
rw₂ : hull T (sInf (id ⁻¹' Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S)) = hull T (kernel (T := T) S)
rw₃ : hull T (sInf (id (Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S))) = hull T (kernel (T := T) S)
rw₄ rw₅ : hull T (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S)) = hull T (kernel (T := T) S)
⊢ hull T
      (sInf
        (preimage (β := αᵒᵈ) (⇑OrderDual.toDual : (a : α) → αᵒᵈ)
          ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S))) =
    hull T (kernel (T := T) S)

Tactic:
rw [← preimage_comp, ← OrderDual.toDual_symm_eq, Equiv.symm_comp_self, preimage_id_eq, id_eq]

Premises used: OrderDual.toDual_symm_eq, Equiv.symm_comp_self, Set.preimage_comp, Set.preimage_id_eq, id_eq
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
hG : OrderGenerates T
a : αᵒᵈ
obtain :
  ∀ (S : Set (↑T : Type u_1)),
    kernel (T := T) S ≤
      (OrderDual.toDual : (a : α) → αᵒᵈ)
        (kernel (T := T) (hull T ((OrderDual.ofDual : (a : αᵒᵈ) → α) (kernel (T := T) S))))
⊢ a ≤ (OrderDual.toDual : (a : α) → αᵒᵈ) (kernel (T := T) (hull T ((OrderDual.ofDual : (a : αᵒᵈ) → α) a)))

Tactic:
obtain ⟨S, rfl⟩ := hG a

Premises used: rfl
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
hG : OrderGenerates T
S : Set (↑T : Type u_1)
rw :
  sInf
      (Subtype.val (p := fun (x : α) ↦ x ∈ T) ''
        hull T ((OrderDual.ofDual : (a : αᵒᵈ) → α) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S)))) ≤
    (OrderDual.ofDual : (a : αᵒᵈ) → α) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S))
⊢ kernel (T := T) S ≤
    (OrderDual.toDual : (a : α) → αᵒᵈ)
      (kernel (T := T) (hull T ((OrderDual.ofDual : (a : αᵒᵈ) → α) (kernel (T := T) S))))

Tactic:
rw [OrderDual.le_toDual, kernel, kernel]

Premises used: PrimitiveSpectrum.kernel, OrderDual.le_toDual
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
hG : OrderGenerates T
S : Set (↑T : Type u_1)
c : (↑T : Type u_1)
hcS : c ∈ S
rw : (OrderDual.ofDual : (a : αᵒᵈ) → α) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S)) ≤ (↑c : α)
⊢ c ∈ hull T ((OrderDual.ofDual : (a : αᵒᵈ) → α) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S)))

Tactic:
rw [hull, mem_preimage, mem_Ici]

Premises used: PrimitiveSpectrum.hull, Set.mem_Ici, Set.mem_preimage
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
hG : OrderGenerates T
S : Set (↑T : Type u_1)
c : (↑T : Type u_1)
hcS : c ∈ S
⊢ (OrderDual.ofDual : (a : αᵒᵈ) → α) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S)) ≤ (↑c : α)

Tactic:
sInf_le (mem_image_of_mem Subtype.val hcS)

Premises used: Set.mem_image_of_mem, sInf_le, Subtype.val
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
hG : OrderGenerates T
S : Set (↑T : Type u_1)
c : (↑T : Type u_1)
hcS : c ∈ S
⊢ (OrderDual.ofDual : (a : αᵒᵈ) → α) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S)) ≤ (↑c : α)

Tactic:
exact sInf_le (mem_image_of_mem Subtype.val hcS)

Premises used: Set.mem_image_of_mem, sInf_le, Subtype.val
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
hG : OrderGenerates T
S : Set (↑T : Type u_1)
⊢ sInf
      (Subtype.val (p := fun (x : α) ↦ x ∈ T) ''
        hull T ((OrderDual.ofDual : (a : αᵒᵈ) → α) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S)))) ≤
    (OrderDual.ofDual : (a : αᵒᵈ) → α) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S))

Tactic:
exact sInf_le_sInf <| image_val_mono fun c hcS => by
      rw [hull, mem_preimage, mem_Ici]
      exact sInf_le (mem_image_of_mem Subtype.val hcS)

Premises used: sInf_le_sInf, Set.image_val_mono
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
hG : OrderGenerates T
a : α
rw :
  ((OrderDual.ofDual : (a : αᵒᵈ) → α)
      ((OrderDual.toDual : (a : α) → αᵒᵈ)
          (((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ kernel (T := T)) ((hull T ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α)) a)) :
        αᵒᵈ) :
    α)
| a

Tactic:
rw [← OrderDual.ofDual_toDual a, ← (gi hG).l_u_eq a]

Premises used: PrimitiveSpectrum.gi, OrderDual.ofDual_toDual, GaloisInsertion.l_u_eq
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
hG : OrderGenerates T
a : α
conv_rhs :
  kernel (T := T) (hull T a) =
    (OrderDual.ofDual : (a : αᵒᵈ) → α)
      ((OrderDual.toDual : (a : α) → αᵒᵈ)
          (((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ kernel (T := T)) ((hull T ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α)) a)) :
        αᵒᵈ)
⊢ kernel (T := T) (hull T a) = a

Tactic:
conv_rhs => rw [← OrderDual.ofDual_toDual a, ← (gi hG).l_u_eq a]

Premises used: PrimitiveSpectrum.gi, OrderDual.ofDual_toDual, GaloisInsertion.l_u_eq
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
hG : OrderGenerates T
a : α
⊢ kernel (T := T) (hull T a) =
    (OrderDual.ofDual : (a : αᵒᵈ) → α)
      ((OrderDual.toDual : (a : α) → αᵒᵈ)
          (((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ kernel (T := T)) ((hull T ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α)) a)) :
        αᵒᵈ)

Tactic:
rfl
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
C : Set (↑T : Type u_1)
h : IsClosed[instTopologicalSpaceSubtype] C
obtain : ∀ (a : α) (ha : C = hull T a), hull T (kernel (T := T) C) = C
⊢ hull T (kernel (T := T) C) = C

Tactic:
obtain ⟨a, ha⟩ := (isClosed_iff hT).mp h

Premises used: PrimitiveSpectrum.isClosed_iff, Iff.mp
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
C : Set (↑T : Type u_1)
h : IsClosed[instTopologicalSpaceSubtype] C
a : α
ha : C = hull T a
rw : hull T (kernel (T := T) (hull T a)) = hull T a
rw₁ rw₂ : hull T a = hull T a
⊢ hull T (kernel (T := T) C) = C

Tactic:
rw [ha, kernel_hull hG]

Premises used: PrimitiveSpectrum.kernel_hull
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set (↑T : Type u_1)
simp :
  ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} ≤ hull T (kernel (T := T) S) ∧
    hull T (kernel (T := T) S) ≤ ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}
⊢ (GaloisConnection.closureOperator (u := SetLike.coe) ⋯ : (a : Set (↑T : Type u_1)) → Set (↑T : Type u_1)) S =
    hull T (kernel (T := T) S)

Tactic:
simp only [GaloisConnection.closureOperator_apply, Closeds.coe_closure, closure, le_antisymm_iff]

Premises used: closure, le_antisymm_iff, TopologicalSpace.Closeds.coe_closure, GaloisConnection.closureOperator_apply
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set (↑T : Type u_1)
left : ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} ≤ hull T (kernel (T := T) S)
right : hull T (kernel (T := T) S) ≤ ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}
⊢ ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} ≤ hull T (kernel (T := T) S) ∧
    hull T (kernel (T := T) S) ≤ ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}

Tactic:
constructor
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set (↑T : Type u_1)
⊢ ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} ≤ hull T (kernel (T := T) S)

Tactic:
fun ⦃a⦄ a ↦ a (hull T (kernel S)) ⟨(isClosed_iff hT).mpr ⟨kernel S, rfl⟩,
      image_subset_iff.mp (fun _ hbS => sInf_le hbS)⟩

Premises used: Iff.mpr, PrimitiveSpectrum.hull, Set.Subset, sInf_le, And.intro, PrimitiveSpectrum.kernel, Exists.intro, PrimitiveSpectrum.isClosed_iff, Iff.mp, Set.image_subset_iff, rfl
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set (↑T : Type u_1)
⊢ ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} ≤ hull T (kernel (T := T) S)

Tactic:
exact fun ⦃a⦄ a ↦ a (hull T (kernel S)) ⟨(isClosed_iff hT).mpr ⟨kernel S, rfl⟩,
      image_subset_iff.mp (fun _ hbS => sInf_le hbS)⟩
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set (↑T : Type u_1)
right :
  ∀ (t' : Set (↑T : Type u_1)),
    Membership.mem (γ := Set (Set (↑T : Type u_1)))
        {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} t' →
      hull T (kernel (T := T) S) ⊆ t'
⊢ hull T (kernel (T := T) S) ≤ ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}

Tactic:
simp_rw [le_eq_subset, subset_sInter_iff]

Premises used: Set.le_eq_subset, Set.subset_sInter_iff
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S R : Set (↑T : Type u_1)
hR :
  Membership.mem (γ := Set (Set (↑T : Type u_1)))
    {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} R
right :
  (GaloisConnection.closureOperator (u := fun (a : αᵒᵈ) ↦ hull T ((OrderDual.ofDual : (a : αᵒᵈ) → α) a)) ⋯ :
        (a : Set (↑T : Type u_1)) → Set (↑T : Type u_1))
      S ⊆
    hull T (kernel (T := T) R)
⊢ hull T (kernel (T := T) S) ⊆ R

Tactic:
rw [← (hull_kernel_of_isClosed hT hG hR.1), ← gc_closureOperator]

Premises used: PrimitiveSpectrum.hull_kernel_of_isClosed, PrimitiveSpectrum.gc_closureOperator, And.left
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S R : Set (↑T : Type u_1)
hR :
  Membership.mem (γ := Set (Set (↑T : Type u_1)))
    {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} R
⊢ (GaloisConnection.closureOperator (u := fun (a : αᵒᵈ) ↦ hull T ((OrderDual.ofDual : (a : αᵒᵈ) → α) a)) ⋯ :
        (a : Set (↑T : Type u_1)) → Set (↑T : Type u_1))
      S ⊆
    hull T (kernel (T := T) R)

Tactic:
ClosureOperator.monotone _ hR.2

Premises used: Set.Ici, Set.Mem, setOf, And.right, Set.preimage, ClosureOperator.monotone
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S R : Set (↑T : Type u_1)
hR :
  Membership.mem (γ := Set (Set (↑T : Type u_1)))
    {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} R
⊢ (GaloisConnection.closureOperator (u := fun (a : αᵒᵈ) ↦ hull T ((OrderDual.ofDual : (a : αᵒᵈ) → α) a)) ⋯ :
        (a : Set (↑T : Type u_1)) → Set (↑T : Type u_1))
      S ⊆
    hull T (kernel (T := T) R)

Tactic:
exact ClosureOperator.monotone _ hR.2

Premises used: And.right, ClosureOperator.monotone
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : PreconnectedSpace X
a b : X
f g : X → α
hf : Continuous[inst, inst_2] f
hg : Continuous[inst, inst_2] g
ha : f a ≤ g a
hb : g b ≤ f b
⊢ Set.Nonempty.{u} (α := X) (univ ∩ {x : X | f x ≤ g x ∧ g x ≤ f x})

Tactic:
isPreconnected_closed_iff.1 PreconnectedSpace.isPreconnected_univ _ _ (isClosed_le hf hg)
      (isClosed_le hg hf) (fun _ _ => le_total _ _) ⟨a, trivial, ha⟩ ⟨b, trivial, hb⟩

Premises used: trivial, Set.Mem, setOf, isClosed_le, Set.inter, le_total, And.intro, Exists.intro, Iff.mp, PreconnectedSpace.isPreconnected_univ, isPreconnected_closed_iff
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : PreconnectedSpace X
a b : X
f g : X → α
hf : Continuous[inst, inst_2] f
hg : Continuous[inst, inst_2] g
ha : f a ≤ g a
hb : g b ≤ f b
obtain : ∀ (x : X), Membership.mem (γ := Set X) univ x → ∀ (hfg : f x ≤ g x) (hgf : g x ≤ f x), ∃ (x : X), f x = g x
⊢ ∃ (x : X), f x = g x

Tactic:
obtain ⟨x, _, hfg, hgf⟩ : (univ ∩ { x | f x ≤ g x ∧ g x ≤ f x }).Nonempty :=
    isPreconnected_closed_iff.1 PreconnectedSpace.isPreconnected_univ _ _ (isClosed_le hf hg)
      (isClosed_le hg hf) (fun _ _ => le_total _ _) ⟨a, trivial, ha⟩ ⟨b, trivial, hb⟩

Premises used: trivial, Set.univ, setOf, isClosed_le, le_total, LE.le, Inter.inter, And, Set.Nonempty, And.intro, Exists.intro, Iff.mp, PreconnectedSpace.isPreconnected_univ, isPreconnected_closed_iff
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : PreconnectedSpace X
a b : X
f g : X → α
hf : Continuous[inst, inst_2] f
hg : Continuous[inst, inst_2] g
ha : f a ≤ g a
hb : g b ≤ f b
x : X
left : Membership.mem (γ := Set X) univ x
hfg : f x ≤ g x
hgf : g x ≤ f x
⊢ ∃ (x : X), f x = g x

Tactic:
⟨x, le_antisymm hfg hgf⟩

Premises used: le_antisymm, Exists.intro
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : PreconnectedSpace X
a b : X
f g : X → α
hf : Continuous[inst, inst_2] f
hg : Continuous[inst, inst_2] g
ha : f a ≤ g a
hb : g b ≤ f b
x : X
left : Membership.mem (γ := Set X) univ x
hfg : f x ≤ g x
hgf : g x ≤ f x
⊢ ∃ (x : X), f x = g x

Tactic:
exact ⟨x, le_antisymm hfg hgf⟩
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : PreconnectedSpace X
a : X
l : Filter X
inst_5 : l.NeBot
f g : X → α
hf : Continuous[inst, inst_2] f
hg : Continuous[inst, inst_2] g
ha : f a ≤ g a
he : g ≤ᶠ[l] f
⊢ ∃ (x : X), f x = g x

Tactic:
let ⟨_, h⟩ := he.exists; intermediate_value_univ₂ hf hg ha h

Premises used: _private.0.intermediate_value_univ₂_eventually₁.match_1, Exists, intermediate_value_univ₂, Filter.Eventually.exists, Eq
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : PreconnectedSpace X
l₁ l₂ : Filter X
inst_5 : l₁.NeBot
inst_6 : l₂.NeBot
f g : X → α
hf : Continuous[inst, inst_2] f
hg : Continuous[inst, inst_2] g
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
⊢ ∃ (x : X), f x = g x

Tactic:
let ⟨_, h₁⟩ := he₁.exists
  let ⟨_, h₂⟩ := he₂.exists
  intermediate_value_univ₂ hf hg h₁ h₂

Premises used: _private.0.intermediate_value_univ₂_eventually₁.match_1, Exists, intermediate_value_univ₂, Filter.Eventually.exists, _private.0.intermediate_value_univ₂_eventually₂.match_1, Eq