awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
⊢ IsSublattice s

Tactic:
⟨LinearOrder.supClosed _, LinearOrder.infClosed _⟩

Premises used: IsSublattice.mk, LinearOrder.infClosed, LinearOrder.supClosed
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s_1 t : Set α
a_1 b : α
s : Set α
a : α
ha : a ∈ s
⊢ (↑{a} : Set α) ⊆ s ∧ sup' {a} ⋯ id = a

Tactic:
simpa
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s_1 t_1 : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
⊢ Membership.mem (γ := Set α)
    ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.sup' ht id = a} : Set α)) s)
    (t.sup' ht id ⊔ u.sup' hu id)

Tactic:
⟨_, ht.mono subset_union_left, ?_, sup'_union ht hu _⟩

Premises used: Set.Mem, setOf, Finset.subset_union_left, And.intro, Exists.intro, Finset.sup'_union, Finset.Nonempty.mono
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s_1 t_1 : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
refine : (↑(t ∪ u) : Set α) ⊆ s
⊢ Membership.mem (γ := Set α)
    ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.sup' ht id = a} : Set α)) s)
    (t.sup' ht id ⊔ u.sup' hu id)

Tactic:
refine ⟨_, ht.mono subset_union_left, ?_, sup'_union ht hu _⟩
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s_1 t_1 : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
rw : (↑t : Set α) ∪ (↑u : Set α) ⊆ s
⊢ (↑(t ∪ u) : Set α) ⊆ s

Tactic:
rw [coe_union]

Premises used: Finset.coe_union
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s_1 t_1 : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
⊢ (↑t : Set α) ∪ (↑u : Set α) ⊆ s

Tactic:
Set.union_subset hts hus

Premises used: Set.union_subset
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s_1 t_1 : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
⊢ (↑t : Set α) ∪ (↑u : Set α) ⊆ s

Tactic:
exact Set.union_subset hts hus

Premises used: Set.union_subset
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s t : Set α
a b : α
rintro :
  ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
    (hus : (↑u : Set α) ⊆ s),
    Membership.mem (γ := Set α)
      ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.sup' ht id = a} : Set α))
        s)
      (t.sup' ht id ⊔ u.sup' hu id)
rintro₁ :
  ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
    (hus : (↑u : Set α) ⊆ s), (↑(t ∪ u) : Set α) ⊆ s
rintro₂ :
  ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
    (hus : (↑u : Set α) ⊆ s), (↑t : Set α) ∪ (↑u : Set α) ⊆ s
⊢ ∀ (x : Set α),
    SupClosed.{u_3} (α := α)
      ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.sup' ht id = a} : Set α))
        x)

Tactic:
classical
    rintro s _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
    refine ⟨_, ht.mono subset_union_left, ?_, sup'_union ht hu _⟩
    rw [coe_union]
    exact Set.union_subset hts hus

Premises used: rfl, Finset.coe_union
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s t_1 : Set α
a b : α
s₁ s₂ : Set α
hs : s₁ ≤ s₂
h₂ : SupClosed s₂
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s₁
⊢ t.sup' ht id ∈ s₂

Tactic:
h₂.finsetSup'_mem ht fun i hi ↦ hs <| hts hi

Premises used: SupClosed.finsetSup'_mem
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s t_1 : Set α
a b : α
s₁ s₂ : Set α
hs : s₁ ≤ s₂
h₂ : SupClosed s₂
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s₁
⊢ t.sup' ht id ∈ s₂

Tactic:
exact h₂.finsetSup'_mem ht fun i hi ↦ hs <| hts hi

Premises used: SupClosed.finsetSup'_mem
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
⊢ s ⊆ (supClosure : (a : Set α) → Set α) s

Tactic:
supClosure.le_closure _

Premises used: supClosure, ClosureOperator.le_closure
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
⊢ SupClosed.{u_3} (α := α) ((supClosure : (a : Set α) → Set α) s)

Tactic:
supClosure.isClosed_closure _

Premises used: supClosure, SupClosed, ClosureOperator.isClosed_closure
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
⊢ Monotone.{u_3, u_3} (α := Set α) (β := Set α) (⇑supClosure : (a : Set α) → Set α)

Tactic:
supClosure.monotone

Premises used: supClosure, ClosureOperator.monotone
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
⊢ (supClosure : (a : Set α) → Set α) s = s ↔ SupClosed s

Tactic:
supClosure.isClosed_iff.symm

Premises used: supClosure, SupClosed, ClosureOperator.isClosed_iff, Iff.symm
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
⊢ Eq (α := Set α) ((supClosure : (a : Set α) → Set α) ((supClosure : (a : Set α) → Set α) s : Set α) : Set α)
    ((supClosure : (a : Set α) → Set α) s : Set α)

Tactic:
supClosure.idempotent _

Premises used: supClosure, ClosureOperator.idempotent
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
⊢ Eq.{u_3 + 1} (α := Set α) ((supClosure : (a : Set α) → Set α) ∅ : Set α) (∅ : Set α)

Tactic:
simp
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
a : α
⊢ Eq (α := Set α) ((supClosure : (a : Set α) → Set α) {a} : Set α) ({a} : Set α)

Tactic:
simp
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
⊢ Eq.{u_3 + 1} (α := Set α) ((supClosure : (a : Set α) → Set α) Set.univ : Set α) (Set.univ : Set α)

Tactic:
simp
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
a : α
ha : a ∈ upperBounds s
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
⊢ t.sup' ht id ≤ a

Tactic:
sup'_le _ _ fun b hb ↦ ha <| hts hb

Premises used: Finset.sup'_le
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
a : α
ha : a ∈ upperBounds s
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
⊢ t.sup' ht id ≤ a

Tactic:
exact sup'_le _ _ fun b hb ↦ ha <| hts hb

Premises used: Finset.sup'_le
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
a : α
⊢ IsLUB ((supClosure : (a : Set α) → Set α) s) a ↔ IsLUB s a

Tactic:
simp [IsLUB]

Premises used: IsLUB
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ Membership.mem (γ := Set α) ((supClosure : (a : Set α) → Set α) s : Set α) (a ⊔ b)

Tactic:
supClosed_supClosure (subset_supClosure ha) (subset_supClosure hb)

Premises used: subset_supClosure, supClosed_supClosure
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
ι : Type u_5
t : Finset ι
ht : t.Nonempty
f : ι → α
hf : ∀ i ∈ t, f i ∈ s
⊢ Membership.mem (γ := Set α) ((supClosure : (a : Set α) → Set α) s : Set α) (t.sup' ht f)

Tactic:
supClosed_supClosure.finsetSup'_mem _ fun _i hi ↦ subset_supClosure <| hf _ hi

Premises used: SupClosed.finsetSup'_mem, subset_supClosure, supClosed_supClosure
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s t : Set α
⊢ s ⊆ t → SupClosed t → (supClosure : (a : Set α) → Set α) s ⊆ t

Tactic:
supClosure.closure_min

Premises used: SupClosed, ClosureOperator.closure_min
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
hs : s.Finite
⊢ s.Finite

Tactic:
hs
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
hs : s.Finite
lift : ∀ (s : Finset α), Set.Finite.{u_3} (α := α) ((supClosure : (a : Set α) → Set α) (↑s : Set α))
⊢ Set.Finite.{u_3} (α := α) ((supClosure : (a : Set α) → Set α) s)

Tactic:
lift s to Finset α using hs

Premises used: Finset
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Finset α
⊢ Set.Finite.{u_3} (α := α) ((supClosure : (a : Set α) → Set α) (↑s : Set α))

Tactic:
({t ∈ s.powerset | t.Nonempty}.attach.image
    fun t ↦ t.1.sup' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_

Premises used: Set.Finite.subset, Finset.attach, Finset.powerset, Finset.finite_toSet, Finset.filter, Finset.image
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Finset α
refine :
  (supClosure : (a : Set α) → Set α) (↑s : Set α) ⊆
    (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).sup' ⋯ id)
          {t ∈ s.powerset | t.Nonempty}.attach) :
      Set α)
⊢ Set.Finite.{u_3} (α := α) ((supClosure : (a : Set α) → Set α) (↑s : Set α))

Tactic:
refine ({t ∈ s.powerset | t.Nonempty}.attach.image
    fun t ↦ t.1.sup' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_

Premises used: Set.Finite.subset, Finset.attach, Finset.powerset, Finset.finite_toSet, Finset.filter, Finset.image
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ (↑s : Set α)
simp : ∃ (a : Finset α) (h : a ⊆ s ∧ a.Nonempty), Eq (α := α) (a.sup' ⋯ fun (x : α) ↦ x) (t.sup' ⋯ fun (x : α) ↦ x)
⊢ t.sup' ht id ∈
    (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).sup' ⋯ id)
          {t ∈ s.powerset | t.Nonempty}.attach) :
      Set α)

Tactic:
simp only [id_eq, coe_image, mem_image, mem_coe, mem_attach, true_and, Subtype.exists,
    Finset.mem_powerset, mem_filter]

Premises used: Finset.mem_attach, Set.mem_image, Subtype.exists, Finset.coe_image, Finset.mem_powerset, Finset.mem_filter, Finset.mem_coe, true_and, id_eq
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ (↑s : Set α)
⊢ ∃ (a : Finset α) (h : a ⊆ s ∧ a.Nonempty), Eq (α := α) (a.sup' ⋯ fun (x : α) ↦ x) (t.sup' ⋯ fun (x : α) ↦ x)

Tactic:
⟨t, ⟨hts, ht⟩, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ (↑s : Set α)
⊢ ∃ (a : Finset α) (h : a ⊆ s ∧ a.Nonempty), Eq (α := α) (a.sup' ⋯ fun (x : α) ↦ x) (t.sup' ⋯ fun (x : α) ↦ x)

Tactic:
exact ⟨t, ⟨hts, ht⟩, rfl⟩
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Finset α
refine :
  (supClosure : (a : Set α) → Set α) (↑s : Set α) ⊆
    (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).sup' ⋯ id)
          {t ∈ s.powerset | t.Nonempty}.attach) :
      Set α)
refine₁ :
  ∀ (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ (↑s : Set α)),
    t.sup' ht id ∈
      (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).sup' ⋯ id)
            {t ∈ s.powerset | t.Nonempty}.attach) :
        Set α)
refine₂ :
  ∀ (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ (↑s : Set α)),
    ∃ (a : Finset α) (h : a ⊆ s ∧ a.Nonempty), Eq (α := α) (a.sup' ⋯ fun (x : α) ↦ x) (t.sup' ⋯ fun (x : α) ↦ x)
⊢ Set.Finite.{u_3} (α := α) ((supClosure : (a : Set α) → Set α) (↑s : Set α))

Tactic:
classical
  refine ({t ∈ s.powerset | t.Nonempty}.attach.image
    fun t ↦ t.1.sup' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_
  rintro _ ⟨t, ht, hts, rfl⟩
  simp only [id_eq, coe_image, mem_image, mem_coe, mem_attach, true_and, Subtype.exists,
    Finset.mem_powerset, mem_filter]
  exact ⟨t, ⟨hts, ht⟩, rfl⟩

Premises used: Finset.mem_attach, Set.mem_image, Subtype.exists, Finset.coe_image, Set.Finite.subset, Finset.mem_powerset, Finset.attach, Finset.powerset, Finset.mem_filter, Finset.finite_toSet, Finset.filter, Finset.image, Finset.mem_coe, rfl, true_and, id_eq
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
v : Finset β
hv : v.Nonempty
hvt : (↑v : Set β) ⊆ t
⊢ Membership.mem (γ := Set (α × β)) ((supClosure : (a : Set (α × β)) → Set (α × β)) (s ×ˢ t) : Set (α × β))
    (u.sup' hu id, v.sup' hv id)

Tactic:
⟨u ×ˢ v, hu.product hv, ?_, ?_⟩

Premises used: SProd.sprod, Set.Mem, setOf, Finset.Nonempty.product, And.intro, Exists.intro
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
v : Finset β
hv : v.Nonempty
hvt : (↑v : Set β) ⊆ t
refine_1 : (↑(u ×ˢ v) : Set (α × β)) ⊆ s ×ˢ t
refine_2 : (u ×ˢ v).sup' ⋯ id = (u.sup' hu id, v.sup' hv id)
⊢ Membership.mem (γ := Set (α × β)) ((supClosure : (a : Set (α × β)) → Set (α × β)) (s ×ˢ t) : Set (α × β))
    (u.sup' hu id, v.sup' hv id)

Tactic:
refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
v : Finset β
hv : v.Nonempty
hvt : (↑v : Set β) ⊆ t
⊢ (↑(u ×ˢ v) : Set (α × β)) ⊆ s ×ˢ t

Tactic:
simpa only [coe_product] using Set.prod_mono hus hvt

Premises used: Finset.coe_product, Set.prod_mono
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
v : Finset β
hv : v.Nonempty
hvt : (↑v : Set β) ⊆ t
⊢ (u ×ˢ v).sup' ⋯ id = (u.sup' hu id, v.sup' hv id)

Tactic:
simp [prodMk_sup'_sup']

Premises used: Finset.prodMk_sup'_sup'
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s_1 t : Set α
a_1 b : α
s : Set α
a : α
ha : a ∈ s
⊢ (↑{a} : Set α) ⊆ s ∧ inf' {a} ⋯ id = a

Tactic:
simpa
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s_1 t_1 : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
⊢ Membership.mem (γ := Set α)
    ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.inf' ht id = a} : Set α)) s)
    (t.inf' ht id ⊓ u.inf' hu id)

Tactic:
⟨_, ht.mono subset_union_left, ?_, inf'_union ht hu _⟩

Premises used: Set.Mem, setOf, Finset.subset_union_left, And.intro, Exists.intro, Finset.Nonempty.mono, Finset.inf'_union
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s_1 t_1 : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
refine : (↑(t ∪ u) : Set α) ⊆ s
⊢ Membership.mem (γ := Set α)
    ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.inf' ht id = a} : Set α)) s)
    (t.inf' ht id ⊓ u.inf' hu id)

Tactic:
refine ⟨_, ht.mono subset_union_left, ?_, inf'_union ht hu _⟩
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s_1 t_1 : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
rw : (↑t : Set α) ∪ (↑u : Set α) ⊆ s
⊢ (↑(t ∪ u) : Set α) ⊆ s

Tactic:
rw [coe_union]

Premises used: Finset.coe_union
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s_1 t_1 : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
⊢ (↑t : Set α) ∪ (↑u : Set α) ⊆ s

Tactic:
Set.union_subset hts hus

Premises used: Set.union_subset
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s_1 t_1 : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
⊢ (↑t : Set α) ∪ (↑u : Set α) ⊆ s

Tactic:
exact Set.union_subset hts hus

Premises used: Set.union_subset
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s t : Set α
a b : α
rintro :
  ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
    (hus : (↑u : Set α) ⊆ s),
    Membership.mem (γ := Set α)
      ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.inf' ht id = a} : Set α))
        s)
      (t.inf' ht id ⊓ u.inf' hu id)
rintro₁ :
  ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
    (hus : (↑u : Set α) ⊆ s), (↑(t ∪ u) : Set α) ⊆ s
rintro₂ :
  ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
    (hus : (↑u : Set α) ⊆ s), (↑t : Set α) ∪ (↑u : Set α) ⊆ s
⊢ ∀ (x : Set α),
    InfClosed.{u_3} (α := α)
      ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.inf' ht id = a} : Set α))
        x)

Tactic:
classical
    rintro s _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
    refine ⟨_, ht.mono subset_union_left, ?_, inf'_union ht hu _⟩
    rw [coe_union]
    exact Set.union_subset hts hus

Premises used: rfl, Finset.coe_union
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s t_1 : Set α
a b : α
s₁ s₂ : Set α
hs : s₁ ≤ s₂
h₂ : InfClosed s₂
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s₁
⊢ t.inf' ht id ∈ s₂

Tactic:
h₂.finsetInf'_mem ht fun i hi ↦ hs <| hts hi

Premises used: InfClosed.finsetInf'_mem
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s t_1 : Set α
a b : α
s₁ s₂ : Set α
hs : s₁ ≤ s₂
h₂ : InfClosed s₂
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s₁
⊢ t.inf' ht id ∈ s₂

Tactic:
exact h₂.finsetInf'_mem ht fun i hi ↦ hs <| hts hi

Premises used: InfClosed.finsetInf'_mem
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
⊢ s ⊆ (infClosure : (a : Set α) → Set α) s

Tactic:
infClosure.le_closure _

Premises used: infClosure, ClosureOperator.le_closure
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
⊢ InfClosed.{u_3} (α := α) ((infClosure : (a : Set α) → Set α) s)

Tactic:
infClosure.isClosed_closure _

Premises used: infClosure, InfClosed, ClosureOperator.isClosed_closure
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
⊢ Monotone.{u_3, u_3} (α := Set α) (β := Set α) (⇑infClosure : (a : Set α) → Set α)

Tactic:
infClosure.monotone

Premises used: infClosure, ClosureOperator.monotone
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
⊢ (infClosure : (a : Set α) → Set α) s = s ↔ InfClosed s

Tactic:
infClosure.isClosed_iff.symm

Premises used: infClosure, ClosureOperator.isClosed_iff, InfClosed, Iff.symm
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
⊢ Eq (α := Set α) ((infClosure : (a : Set α) → Set α) ((infClosure : (a : Set α) → Set α) s : Set α) : Set α)
    ((infClosure : (a : Set α) → Set α) s : Set α)

Tactic:
infClosure.idempotent _

Premises used: infClosure, ClosureOperator.idempotent
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
⊢ Eq.{u_3 + 1} (α := Set α) ((infClosure : (a : Set α) → Set α) ∅ : Set α) (∅ : Set α)

Tactic:
simp
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
a : α
⊢ Eq (α := Set α) ((infClosure : (a : Set α) → Set α) {a} : Set α) ({a} : Set α)

Tactic:
simp
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
⊢ Eq.{u_3 + 1} (α := Set α) ((infClosure : (a : Set α) → Set α) Set.univ : Set α) (Set.univ : Set α)

Tactic:
simp
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
a : α
ha : a ∈ lowerBounds s
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
⊢ a ≤ t.inf' ht id

Tactic:
le_inf' _ _ fun b hb ↦ ha <| hts hb

Premises used: Finset.le_inf'
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
a : α
ha : a ∈ lowerBounds s
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
⊢ a ≤ t.inf' ht id

Tactic:
exact le_inf' _ _ fun b hb ↦ ha <| hts hb

Premises used: Finset.le_inf'
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
a : α
⊢ IsGLB ((infClosure : (a : Set α) → Set α) s) a ↔ IsGLB s a

Tactic:
simp [IsGLB]

Premises used: IsGLB
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ Membership.mem (γ := Set α) ((infClosure : (a : Set α) → Set α) s : Set α) (a ⊓ b)

Tactic:
infClosed_infClosure (subset_infClosure ha) (subset_infClosure hb)

Premises used: infClosed_infClosure, subset_infClosure
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
ι : Type u_5
t : Finset ι
ht : t.Nonempty
f : ι → α
hf : ∀ i ∈ t, f i ∈ s
⊢ Membership.mem (γ := Set α) ((infClosure : (a : Set α) → Set α) s : Set α) (t.inf' ht f)

Tactic:
infClosed_infClosure.finsetInf'_mem _ fun _i hi ↦ subset_infClosure <| hf _ hi

Premises used: infClosed_infClosure, subset_infClosure, InfClosed.finsetInf'_mem
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s t : Set α
⊢ s ⊆ t → InfClosed t → (infClosure : (a : Set α) → Set α) s ⊆ t

Tactic:
infClosure.closure_min

Premises used: ClosureOperator.closure_min, InfClosed
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
hs : s.Finite
⊢ s.Finite

Tactic:
hs
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
hs : s.Finite
lift : ∀ (s : Finset α), Set.Finite.{u_3} (α := α) ((infClosure : (a : Set α) → Set α) (↑s : Set α))
⊢ Set.Finite.{u_3} (α := α) ((infClosure : (a : Set α) → Set α) s)

Tactic:
lift s to Finset α using hs

Premises used: Finset
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Finset α
⊢ Set.Finite.{u_3} (α := α) ((infClosure : (a : Set α) → Set α) (↑s : Set α))

Tactic:
({t ∈ s.powerset | t.Nonempty}.attach.image
    fun t ↦ t.1.inf' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_

Premises used: Set.Finite.subset, Finset.attach, Finset.powerset, Finset.finite_toSet, Finset.filter, Finset.image
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Finset α
refine :
  (infClosure : (a : Set α) → Set α) (↑s : Set α) ⊆
    (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).inf' ⋯ id)
          {t ∈ s.powerset | t.Nonempty}.attach) :
      Set α)
⊢ Set.Finite.{u_3} (α := α) ((infClosure : (a : Set α) → Set α) (↑s : Set α))

Tactic:
refine ({t ∈ s.powerset | t.Nonempty}.attach.image
    fun t ↦ t.1.inf' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_

Premises used: Set.Finite.subset, Finset.attach, Finset.powerset, Finset.finite_toSet, Finset.filter, Finset.image