awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Esakia (goal)
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
⊢ ∃ (c : α), a ≤ c ∧ (g.comp f.toContinuousOrderHom).toFun c = b
have 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
Tactic: obtain ⟨b, h₁, rfl⟩ := g.exists_map_eq_of_map_le' h₀
Cleared hypotheses: b, h₀
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Esakia (goal)
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
⊢ ∃ (c : α), a ≤ c ∧ (g.comp f.toContinuousOrderHom).toFun c = g.toFun b
have 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)
Tactic: obtain ⟨b, h₂, rfl⟩ := f.exists_map_eq_of_map_le' h₁
Cleared hypotheses: b, h₁, h₀
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Esakia (goal)
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 : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Esakia (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Esakia (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
hT : ∀ p ∈ T, InfPrime p
F : Finset α
⊢ hull T (F.inf id) = T ↓∩ (↑(upperClosure (↑F : Set α)) : Set α)
have rw : hull T (F.inf id) = T ↓∩ ⋃ a ∈ (↑F : Set α), Set.Ici a
Tactic: rw [coe_upperClosure]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
hT : ∀ p ∈ T, InfPrime p
⊢ hull T (inf ∅ id) = T ↓∩ ⋃ a ∈ (↑∅ : Set α), Set.Ici a
have empty : hull T ⊤ = ∅
Tactic: simp only [coe_empty, mem_empty_iff_false, iUnion_of_empty, iUnion_empty, Set.preimage_empty,
      inf_empty]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
hT : ∀ p ∈ T, InfPrime p
⊢ hull T ⊤ = ∅
have empty : ∀ (hf : ¬hull T ⊤ = ∅), False
Tactic: by_contra hf
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (hypothesis)
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
hT : ∀ p ∈ T, InfPrime p
hf : ¬hull T ⊤ = ∅
⊢ False
have hf₁ : (hull T ⊤).Nonempty
Tactic: rw [← Set.not_nonempty_iff_eq_empty, not_not] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
hT : ∀ p ∈ T, InfPrime p
hf : (hull T ⊤).Nonempty
⊢ False
have empty : ∀ (x : (↑T : Type u_1)) (hx : x ∈ hull T ⊤), False
Tactic: obtain ⟨x, hx⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
hT : ∀ p ∈ T, InfPrime p
F : Finset α
⊢ hull T (F.inf id) = T ↓∩ ⋃ a ∈ (↑F : Set α), Set.Ici a
have empty : hull T (inf ∅ id) = T ↓∩ ⋃ a ∈ (↑∅ : 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]
Cleared hypotheses: F
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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
⊢ hull T (F.inf id) = T ↓∩ ⋃ a ∈ (↑F : Set α), Set.Ici a
have cons : ∀ (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: 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]
Cleared hypotheses: F
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
hT : ∀ p ∈ T, InfPrime p
F : Finset α
⊢ T ↓∩ (↑(upperClosure (↑F : Set α)) : Set α)ᶜ = (hull T (F.inf id))ᶜ
have rw : (T ↓∩ (↑(upperClosure (↑F : Set α)) : Set α))ᶜ = (hull T (F.inf id))ᶜ
Tactic: rw [Set.preimage_compl, (hull_finsetInf hT)]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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))ᶜ
⊢ T ↓∩ (↑(upperClosure (↑F : Set α)) : Set α)ᶜ = (hull T (F.inf id))ᶜ
have rw₁ : Eq (α := Set (↑T : Type u_1)) (T ↓∩ (↑(upperClosure (↑F : Set α)) : Set α))ᶜ
  (T ↓∩ (↑(upperClosure (↑F : Set α)) : Set α))ᶜ
Tactic: rw [Set.preimage_compl, (hull_finsetInf hT)]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
inst_2 : TopologicalSpace α
inst_3 : IsLower α
hT : ∀ p ∈ T, InfPrime p
⊢ IsTopologicalBasis.{u_1} (α := (↑T : Type u_1)) {S : Set (↑T : Type u_1) | ∃ (a : α), (hull T a)ᶜ = S}
have 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 α)
Tactic: convert! isTopologicalBasis_subtype Topology.IsLower.isTopologicalBasis (· ∈ T)
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
T : Set α
inst_1 : OrderTop α
inst_2 : TopologicalSpace α
inst_3 : IsLower α
hT : ∀ p ∈ T, InfPrime p
⊢ 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 α)
have 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
Tactic: ext R
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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)
⊢ 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
have h : (∃ (a : α), (hull T a)ᶜ = R) ↔
  ∃ (a : Set α), a.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure a) : Set α))ᶜ = R
Tactic: simp only [preimage_compl, mem_setOf_eq, IsLower.lowerBasis, mem_image, exists_exists_and_eq_and]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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 : α), (hull T a)ᶜ = R) ↔
    ∃ (a : Set α), a.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure a) : Set α))ᶜ = R
have h : (∃ (a : α), (hull T a)ᶜ = R) →
  ∃ (a : Set α), a.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure a) : Set α))ᶜ = R
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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
⊢ (∃ (a : α), (hull T a)ᶜ = R) ↔
    ∃ (a : Set α), a.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure a) : Set α))ᶜ = R
have h₁ : (∃ (a : Set α), a.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure a) : Set α))ᶜ = R) →
  ∃ (a : α), (hull T a)ᶜ = R
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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
⊢ ∃ (a : Set α), a.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure a) : Set α))ᶜ = R
have h : ∀ (a : α) (ha' : (hull T a)ᶜ = R),
  ∃ (a : Set α), a.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure a) : Set α))ᶜ = R
Tactic: obtain ⟨a, ha'⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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
⊢ ∃ (a : Set α), a.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure a) : Set α))ᶜ = R
have h : Set.Finite (α := α) {a} ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure {a}) : Set α))ᶜ = R
Tactic: use {a}
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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
⊢ Set.Finite (α := α) {a} ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure {a}) : Set α))ᶜ = R
have 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)ᶜ)
Tactic: rw [← (Function.Injective.preimage_image Subtype.val_injective R), ← ha']
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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
⊢ 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)ᶜ)
have 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)
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]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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
⊢ ∃ (a : α), (hull T a)ᶜ = R
have h : ∀ (F : Set α) (hF : F.Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure F) : Set α))ᶜ = R),
  ∃ (a : α), (hull T a)ᶜ = R
Tactic: obtain ⟨F, hF⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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
⊢ ∃ (a : α), (hull T a)ᶜ = R
have h : ∀ (F : Finset α)
  (hF : (↑F : Set α).Finite ∧ (Subtype.val (p := fun (x : α) ↦ x ∈ T) ⁻¹' (↑(upperClosure (↑F : Set α)) : Set α))ᶜ = R),
  ∃ (a : α), (hull T a)ᶜ = R
Tactic: lift F to Finset α using hF.1
Cleared hypotheses: F, hF
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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
⊢ ∃ (a : α), (hull T a)ᶜ = R
have h : (hull T (F.inf id))ᶜ = R
Tactic: use Finset.inf F id
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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
⊢ (hull T (F.inf id))ᶜ = R
have h : ∀ (x : (↑T : Type u_1)), x ∈ (hull T (F.inf id))ᶜ ↔ x ∈ R
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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)
⊢ IsOpen[instTopologicalSpaceSubtype] S ↔ ∃ (a : α), S = (hull T a)ᶜ
have mp : IsOpen[instTopologicalSpaceSubtype] S → ∃ (a : α), S = (hull T a)ᶜ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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)ᶜ
⊢ IsOpen[instTopologicalSpaceSubtype] S ↔ ∃ (a : α), S = (hull T a)ᶜ
have mpr : (∃ (a : α), S = (hull T a)ᶜ) → IsOpen[instTopologicalSpaceSubtype] S
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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}
⊢ ∃ (a : α), S = (hull T a)ᶜ
have h₁ : S = (hull T (sSup R))ᶜ
Tactic: use sSup R
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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 = (hull T (sSup R))ᶜ
have 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))ᶜ
Tactic: rw [IsTopologicalBasis.open_eq_sUnion' (isTopologicalBasis_relativeLower hT) h]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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)ᶜ
⊢ IsOpen[instTopologicalSpaceSubtype] S
have mpr : ∀ (a : α) (ha : S = (hull T a)ᶜ), IsOpen[instTopologicalSpaceSubtype] S
Tactic: obtain ⟨a, ha⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
S : Set (↑T : Type u_1)
⊢ (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)
have 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)
Tactic: simp only [toDual_sInf, GaloisConnection.closureOperator_apply, ofDual_sSup]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
S : Set (↑T : Type u_1)
⊢ hull T
      (sInf
        (preimage (β := αᵒᵈ) (⇑OrderDual.toDual : (a : α) → αᵒᵈ)
          ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S))) =
    hull T (kernel (T := T) S)
have 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)
Tactic: rw [← preimage_comp, ← OrderDual.toDual_symm_eq, Equiv.symm_comp_self, preimage_id_eq, id_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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)
⊢ hull T
      (sInf
        (preimage (β := αᵒᵈ) (⇑OrderDual.toDual : (a : α) → αᵒᵈ)
          ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S))) =
    hull T (kernel (T := T) S)
have 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)
Tactic: rw [← preimage_comp, ← OrderDual.toDual_symm_eq, Equiv.symm_comp_self, preimage_id_eq, id_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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)
⊢ hull T
      (sInf
        (preimage (β := αᵒᵈ) (⇑OrderDual.toDual : (a : α) → αᵒᵈ)
          ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S))) =
    hull T (kernel (T := T) S)
have rw₂ : hull T (sInf (id ⁻¹' 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]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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)
⊢ hull T
      (sInf
        (preimage (β := αᵒᵈ) (⇑OrderDual.toDual : (a : α) → αᵒᵈ)
          ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S))) =
    hull T (kernel (T := T) S)
have rw₃ : hull T (sInf (id (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]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
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)
⊢ hull T
      (sInf
        (preimage (β := αᵒᵈ) (⇑OrderDual.toDual : (a : α) → αᵒᵈ)
          ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S))) =
    hull T (kernel (T := T) S)
have rw₄ : hull T (sInf (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]