awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
inst_6 : TopologicalSpace δ
inst_7 : Preorder δ
toFun : α → β
monotone' : Monotone toFun
continuous_toFun : Continuous { toFun := toFun, monotone' := monotone' : α →o β }.toFun
exists_map_eq_of_map_le' :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun : α →Co β }.toFun a ≤ b →
      ∃ (c : α),
        a ≤ c ∧ { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun : α →Co β }.toFun c = b
toFun_1 : α → β
monotone'_1 : Monotone toFun_1
continuous_toFun_1 : Continuous { toFun := toFun_1, monotone' := monotone'_1 : α →o β }.toFun
exists_map_eq_of_map_le'_1 :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    { toFun := toFun_1, monotone' := monotone'_1, continuous_toFun := continuous_toFun_1 : α →Co β }.toFun a ≤ b →
      ∃ (c : α),
        a ≤ c ∧
          { toFun := toFun_1, monotone' := monotone'_1, continuous_toFun := continuous_toFun_1 : α →Co β }.toFun c = b
h :
  Eq (α := (a : α) → β)
    ((fun (f : EsakiaHom α β) ↦ f.toFun)
      { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun,
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le' })
    ((fun (f : EsakiaHom α β) ↦ f.toFun)
      { toFun := toFun_1, monotone' := monotone'_1, continuous_toFun := continuous_toFun_1,
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le'_1 })
⊢ { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun,
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le' : EsakiaHom α β } =
    { toFun := toFun_1, monotone' := monotone'_1, continuous_toFun := continuous_toFun_1,
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le'_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
f : EsakiaHom α β
⊢ Eq (α := (a : α) → β) (⇑f.toContinuousOrderHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
f : EsakiaHom α β
⊢ f.toFun = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
f g : EsakiaHom α β
h : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
inst_6 : TopologicalSpace δ
inst_7 : Preorder δ
f : EsakiaHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ ∀ ⦃a : α⦄ ⦃b : β⦄, (f.copy f' h).toFun a ≤ b → ∃ (c : α), a ≤ c ∧ (f.copy f' h).toFun c = b

Tactic:
simpa only [h.symm, toFun_eq_coe] using f.exists_map_eq_of_map_le'

Premises used: EsakiaHom.exists_map_eq_of_map_le', Eq.symm, EsakiaHom.toFun_eq_coe
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
f : EsakiaHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
f : EsakiaHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
⊢ Eq (α := (a : α) → α) (⇑(EsakiaHom.id α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
⊢ Eq (α := PseudoEpimorphism α α) { toOrderHom := (↑(EsakiaHom.id α) : α →o α), exists_map_eq_of_map_le' := ⋯ }
    (PseudoEpimorphism.id α)

Tactic:
rfl

Premises used: OrderHom.id, PseudoEpimorphism.id, OrderHomClass.toOrderHom, rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
a : α
⊢ (EsakiaHom.id α : (a : α) → α) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
⊢ Eq (α := α →Co α) (↑(EsakiaHom.id α) : α →Co α) (ContinuousOrderHom.id α)

Tactic:
rfl

Premises used: OrderHom.id, ContinuousOrderHom.id, ContinuousOrderHomClass.toContinuousOrderHom, rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
inst_6 : TopologicalSpace δ
inst_7 : Preorder δ
g : EsakiaHom β γ
f : EsakiaHom α β
a : α
b : γ
h₀ : (g.comp f.toContinuousOrderHom).toFun a ≤ b
obtain :
  ∀ (b : β) (h₁ : (f.toOrderHom : (a : α) → β) a ≤ b) (h₀ : (g.comp f.toContinuousOrderHom).toFun a ≤ g.toFun b),
    ∃ (c : α), a ≤ c ∧ (g.comp f.toContinuousOrderHom).toFun c = g.toFun b
⊢ ∃ (c : α), a ≤ c ∧ (g.comp f.toContinuousOrderHom).toFun c = b

Tactic:
obtain ⟨b, h₁, rfl⟩ := g.exists_map_eq_of_map_le' h₀

Premises used: EsakiaHom.exists_map_eq_of_map_le', rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
inst_6 : TopologicalSpace δ
inst_7 : Preorder δ
g : EsakiaHom β γ
f : EsakiaHom α β
a : α
b : β
h₁ : (f.toOrderHom : (a : α) → β) a ≤ b
h₀ : (g.comp f.toContinuousOrderHom).toFun a ≤ g.toFun b
obtain :
  ∀ (b : α) (h₂ : a ≤ b) (h₁ : (f.toOrderHom : (a : α) → β) a ≤ f.toFun b)
    (h₀ : (g.comp f.toContinuousOrderHom).toFun a ≤ g.toFun (f.toFun b)),
    ∃ (c : α), a ≤ c ∧ (g.comp f.toContinuousOrderHom).toFun c = g.toFun (f.toFun b)
⊢ ∃ (c : α), a ≤ c ∧ (g.comp f.toContinuousOrderHom).toFun c = g.toFun b

Tactic:
obtain ⟨b, h₂, rfl⟩ := f.exists_map_eq_of_map_le' h₁

Premises used: EsakiaHom.exists_map_eq_of_map_le', rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
inst_6 : TopologicalSpace δ
inst_7 : Preorder δ
g : EsakiaHom β γ
f : EsakiaHom α β
a b : α
h₂ : a ≤ b
h₁ : (f.toOrderHom : (a : α) → β) a ≤ f.toFun b
h₀ : (g.comp f.toContinuousOrderHom).toFun a ≤ g.toFun (f.toFun b)
⊢ ∃ (c : α), a ≤ c ∧ (g.comp f.toContinuousOrderHom).toFun c = g.toFun (f.toFun b)

Tactic:
⟨b, h₂, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
inst_6 : TopologicalSpace δ
inst_7 : Preorder δ
g : EsakiaHom β γ
f : EsakiaHom α β
a b : α
h₂ : a ≤ b
h₁ : (f.toOrderHom : (a : α) → β) a ≤ f.toFun b
h₀ : (g.comp f.toContinuousOrderHom).toFun a ≤ g.toFun (f.toFun b)
⊢ ∃ (c : α), a ≤ c ∧ (g.comp f.toContinuousOrderHom).toFun c = g.toFun (f.toFun b)

Tactic:
exact ⟨b, h₂, rfl⟩
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
g : EsakiaHom β γ
f : EsakiaHom α β
⊢ Eq (α := α →Co γ) (↑(g.comp f) : α →Co γ) (ContinuousOrderHom.comp (↑g : β →Co γ) (↑f : α →Co β))

Tactic:
rfl

Premises used: OrderHom.comp, ContinuousOrderHom.comp, ContinuousOrderHomClass.toContinuousOrderHom, rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
g : EsakiaHom β γ
f : EsakiaHom α β
⊢ { toOrderHom := (↑(g.comp f) : α →o γ), exists_map_eq_of_map_le' := ⋯ } =
    { toOrderHom := (↑g : β →o γ), exists_map_eq_of_map_le' := ⋯ : PseudoEpimorphism β γ }.comp
      { toOrderHom := (↑f : α →o β), exists_map_eq_of_map_le' := ⋯ : PseudoEpimorphism α β }

Tactic:
rfl

Premises used: PseudoEpimorphism.comp, OrderHom.comp, OrderHomClass.toOrderHom, rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
g : EsakiaHom β γ
f : EsakiaHom α β
⊢ Eq (α := (a : α) → γ) (⇑(g.comp f) : (a : α) → γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
g : EsakiaHom β γ
f : EsakiaHom α β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((g.comp f : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
inst_6 : TopologicalSpace δ
inst_7 : Preorder δ
h : EsakiaHom γ δ
g : EsakiaHom β γ
f : EsakiaHom α β
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
rfl

Premises used: EsakiaHom.comp, OrderHom.comp, ContinuousOrderHom.comp, rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
f : EsakiaHom α β
⊢ f.comp (EsakiaHom.id α) = f

Tactic:
ext fun _ => rfl

Premises used: EsakiaHom.ext, rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
f : EsakiaHom α β
⊢ comp (EsakiaHom.id β) f = f

Tactic:
ext fun _ => rfl

Premises used: EsakiaHom.ext, rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
g₁ g₂ : EsakiaHom β γ
f : EsakiaHom α β
hf : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, congr_arg (comp · f)⟩

Premises used: Iff.mpr, Function.Surjective.forall, EsakiaHom.comp, DFunLike.ext_iff, congr_arg, EsakiaHom.ext, Iff.intro, Iff.mp
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
g : EsakiaHom β γ
f₁ f₂ : EsakiaHom α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)

Tactic:
rw [← comp_apply, h, comp_apply]

Premises used: EsakiaHom.comp_apply
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
hT : ∀ p ∈ T, InfPrime p
a b : α
⊢ hull T (a ⊓ b) = hull T a ∪ hull T b

Tactic:
grind [InfPrime.inf_le]

Premises used: InfPrime.inf_le
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
hT : ∀ p ∈ T, InfPrime p
F : Finset α
rw : hull T (F.inf id) = T ↓∩ ⋃ a ∈ (↑F : Set α), Set.Ici a
⊢ hull T (F.inf id) = T ↓∩ (↑(upperClosure (↑F : Set α)) : Set α)

Tactic:
rw [coe_upperClosure]

Premises used: coe_upperClosure
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
hT : ∀ p ∈ T, InfPrime p
empty : hull T ⊤ = ∅
⊢ hull T (inf ∅ id) = T ↓∩ ⋃ a ∈ (↑∅ : Set α), Set.Ici a

Tactic:
simp only [coe_empty, mem_empty_iff_false, iUnion_of_empty, iUnion_empty, Set.preimage_empty,
      inf_empty]

Premises used: Finset.coe_empty, Set.preimage_empty, Set.iUnion_of_empty, Finset.inf_empty, Set.mem_empty_iff_false, Set.iUnion_empty
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
hT : ∀ p ∈ T, InfPrime p
empty : ∀ (hf : ¬hull T ⊤ = ∅), False
⊢ hull T ⊤ = ∅

Tactic:
by_contra hf
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
hT : ∀ p ∈ T, InfPrime p
hf : ¬hull T ⊤ = ∅
⊢ (hull T ⊤).Nonempty

Tactic:
rw [← Set.not_nonempty_iff_eq_empty, not_not] at hf

Premises used: Classical.not_not, Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
hT : ∀ p ∈ T, InfPrime p
hf : (hull T ⊤).Nonempty
empty : ∀ (x : (↑T : Type u_1)) (hx : x ∈ hull T ⊤), False
⊢ False

Tactic:
obtain ⟨x, hx⟩ := hf
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
hT : ∀ p ∈ T, InfPrime p
x : (↑T : Type u_1)
hx : x ∈ hull T ⊤
⊢ False

Tactic:
(hT x (Subtype.coe_prop x)).1 (isMax_iff_eq_top.mpr (eq_top_iff.mpr hx))

Premises used: isMax_iff_eq_top, Iff.mpr, Subtype.coe_prop, eq_top_iff, And.left, Subtype.val
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
hT : ∀ p ∈ T, InfPrime p
x : (↑T : Type u_1)
hx : x ∈ hull T ⊤
⊢ False

Tactic:
exact (hT x (Subtype.coe_prop x)).1 (isMax_iff_eq_top.mpr (eq_top_iff.mpr hx))

Premises used: isMax_iff_eq_top, Iff.mpr, Subtype.coe_prop, eq_top_iff, And.left, Subtype.val
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
hT : ∀ p ∈ T, InfPrime p
a : α
F' : Finset α
h : a ∉ F'
I4 : hull T (F'.inf id) = T ↓∩ ⋃ a ∈ (↑F' : Set α), Set.Ici a
⊢ hull T ((cons a F' h).inf id) = T ↓∩ ⋃ a_1 ∈ (↑(cons a F' h) : Set α), Set.Ici a_1

Tactic:
simp [hull_inf hT, I4]

Premises used: PrimitiveSpectrum.hull_inf
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
hT : ∀ p ∈ T, InfPrime p
F : Finset α
empty : hull T (inf ∅ id) = T ↓∩ ⋃ a ∈ (↑∅ : Set α), Set.Ici a
cons :
  ∀ (a : α) (F' : Finset α) (h : a ∉ F') (I4 : hull T (F'.inf id) = T ↓∩ ⋃ a ∈ (↑F' : Set α), Set.Ici a),
    hull T ((Finset.cons a F' h).inf id) = T ↓∩ ⋃ a_1 ∈ (↑(Finset.cons a F' h) : Set α), Set.Ici a_1
⊢ hull T (F.inf id) = T ↓∩ ⋃ a ∈ (↑F : Set α), Set.Ici a

Tactic:
induction F using Finset.cons_induction with
  | empty =>
    simp only [coe_empty, mem_empty_iff_false, iUnion_of_empty, iUnion_empty, Set.preimage_empty,
      inf_empty]
    by_contra hf
    rw [← Set.not_nonempty_iff_eq_empty, not_not] at hf
    obtain ⟨x, hx⟩ := hf
    exact (hT x (Subtype.coe_prop x)).1 (isMax_iff_eq_top.mpr (eq_top_iff.mpr hx))
  | cons a F' _ I4 => simp [hull_inf hT, I4]

Premises used: Finset.coe_empty, Classical.not_not, Finset.cons, Set.not_nonempty_iff_eq_empty, PrimitiveSpectrum.hull_inf, Set.preimage_empty, Set.iUnion_of_empty, Finset.inf_empty, Set.mem_empty_iff_false, Set.iUnion_empty
-- Module: Mathlib.Topology.Order.HullKernel
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
hT : ∀ p ∈ T, InfPrime p
F : Finset α
rw : (T ↓∩ (↑(upperClosure (↑F : Set α)) : Set α))ᶜ = (hull T (F.inf id))ᶜ
rw₁ rw₂ :
  Eq (α := Set (↑T : Type u_1)) (T ↓∩ (↑(upperClosure (↑F : Set α)) : Set α))ᶜ
    (T ↓∩ (↑(upperClosure (↑F : Set α)) : Set α))ᶜ
⊢ T ↓∩ (↑(upperClosure (↑F : Set α)) : Set α)ᶜ = (hull T (F.inf id))ᶜ

Tactic:
rw [Set.preimage_compl, (hull_finsetInf hT)]

Premises used: PrimitiveSpectrum.hull_finsetInf, Set.preimage_compl
-- 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
⊢ IsTopologicalBasis (α := { x : α // x ∈ T })
    (preimage (Subtype.val (p := fun (x : α) ↦ x ∈ T)) '' IsLower.lowerBasis α)

Tactic:
isTopologicalBasis_subtype Topology.IsLower.isTopologicalBasis (· ∈ T)

Premises used: isTopologicalBasis_subtype, Membership.mem, Topology.IsLower.isTopologicalBasis
-- 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
h :
  Eq (α := Set (Set (↑T : Type u_1))) {S : Set (↑T : Type u_1) | ∃ (a : α), (hull T a)ᶜ = S}
    (preimage (Subtype.val (p := fun (x : α) ↦ x ∈ T)) '' IsLower.lowerBasis α)
⊢ IsTopologicalBasis.{u_1} (α := (↑T : Type u_1)) {S : Set (↑T : Type u_1) | ∃ (a : α), (hull T a)ᶜ = S}

Tactic:
convert! isTopologicalBasis_subtype Topology.IsLower.isTopologicalBasis (· ∈ T)

Premises used: isTopologicalBasis_subtype, Membership.mem, Topology.IsLower.isTopologicalBasis
-- 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
h :
  ∀ (R : Set (↑T : Type u_1)),
    Membership.mem (γ := Set (Set (↑T : Type u_1))) {S : Set (↑T : Type u_1) | ∃ (a : α), (hull T a)ᶜ = S} R ↔
      Membership.mem (γ := Set (Set (↑T : Type u_1)))
        (preimage (Subtype.val (p := fun (x : α) ↦ x ∈ T)) '' IsLower.lowerBasis α) R
⊢ Eq (α := Set (Set (↑T : Type u_1))) {S : Set (↑T : Type u_1) | ∃ (a : α), (hull T a)ᶜ = S}
    (preimage (Subtype.val (p := fun (x : α) ↦ x ∈ T)) '' IsLower.lowerBasis α)

Tactic:
ext R
-- 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)
h :
  (∃ (a : α), (hull T a)ᶜ = R) ↔
    ∃ (a : Set α), a.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure a) : Set α))ᶜ = R
⊢ Membership.mem (γ := Set (Set (↑T : Type u_1))) {S : Set (↑T : Type u_1) | ∃ (a : α), (hull T a)ᶜ = S} R ↔
    Membership.mem (γ := Set (Set (↑T : Type u_1)))
      (preimage (Subtype.val (p := fun (x : α) ↦ x ∈ T)) '' IsLower.lowerBasis α) R

Tactic:
simp only [preimage_compl, mem_setOf_eq, IsLower.lowerBasis, mem_image, exists_exists_and_eq_and]

Premises used: Topology.IsLower.lowerBasis, Set.mem_image, Set.mem_setOf_eq, exists_exists_and_eq_and, Set.preimage_compl
-- 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)
h :
  (∃ (a : α), (hull T a)ᶜ = R) →
    ∃ (a : Set α), a.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure a) : Set α))ᶜ = R
h₁ :
  (∃ (a : Set α), a.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure a) : Set α))ᶜ = R) →
    ∃ (a : α), (hull T a)ᶜ = R
⊢ (∃ (a : α), (hull T a)ᶜ = R) ↔
    ∃ (a : Set α), a.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure a) : Set α))ᶜ = R

Tactic:
constructor
-- 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 : α), (hull T a)ᶜ = R
h :
  ∀ (a : α) (ha' : (hull T a)ᶜ = R),
    ∃ (a : Set α), a.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure a) : Set α))ᶜ = R
⊢ ∃ (a : Set α), a.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure a) : Set α))ᶜ = R

Tactic:
obtain ⟨a, ha'⟩ := 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)
a : α
ha' : (hull T a)ᶜ = R
h : Set.Finite (α := α) {a} ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure {a}) : Set α))ᶜ = R
⊢ ∃ (a : Set α), a.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure a) : Set α))ᶜ = R

Tactic:
use {a}
-- 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)
a : α
ha' : (hull T a)ᶜ = R
h :
  Set.Finite (α := α) {a} ∧
    Eq (α := Set (↑T : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure {a}) : Set α))ᶜ
      (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' Subtype.val (p := fun (x : α) ↦ x ∈ T) '' (hull T a)ᶜ)
⊢ Set.Finite (α := α) {a} ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure {a}) : Set α))ᶜ = R

Tactic:
rw [← (Function.Injective.preimage_image Subtype.val_injective R), ← ha']

Premises used: Subtype.val_injective, Function.Injective.preimage_image
-- 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)
a : α
ha' : (hull T a)ᶜ = R
h :
  Eq (α := Set (↑T : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' Ici a)ᶜ
    (univ \ Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' Ici a)
⊢ Set.Finite (α := α) {a} ∧
    Eq (α := Set (↑T : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure {a}) : Set α))ᶜ
      (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' Subtype.val (p := fun (x : α) ↦ x ∈ T) '' (hull T a)ᶜ)

Tactic:
simp only [finite_singleton, upperClosure_singleton, UpperSet.coe_Ici, image_val_compl,
      Subtype.image_preimage_coe, diff_self_inter, preimage_diff, Subtype.coe_preimage_self,
      true_and]

Premises used: UpperSet.coe_Ici, Set.diff_self_inter, upperClosure_singleton, Subtype.image_preimage_coe, Subtype.coe_preimage_self, Set.image_val_compl, Set.finite_singleton, Set.preimage_diff, true_and
-- 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)
a : α
ha' : (hull T a)ᶜ = R
⊢ Eq (α := Set (↑T : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' Ici a)ᶜ
    (univ \ Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' Ici a)

Tactic:
compl_eq_univ_diff (Subtype.val ⁻¹' Ici a)

Premises used: Set.Ici, Set.preimage, Set.compl_eq_univ_diff, Subtype.val
-- 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)
a : α
ha' : (hull T a)ᶜ = R
⊢ Eq (α := Set (↑T : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' Ici a)ᶜ
    (univ \ Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' Ici a)

Tactic:
exact compl_eq_univ_diff (Subtype.val ⁻¹' Ici a)

Premises used: Set.Ici, Set.preimage, Set.compl_eq_univ_diff, Subtype.val