awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : DistribLattice α
s : Set α
hs : SupClosed s
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
⊢ Membership.mem (γ := Set α) ((infClosure : (a : Set α) → Set α) s : Set α)
    ((t ×ˢ u).inf' ⋯ fun (i : α × α) ↦ id i.1 ⊔ id i.2)

Tactic:
finsetInf'_mem_infClosure _
    fun i hi ↦ hs (hts (mem_product.1 hi).1) (hus (mem_product.1 hi).2)

Premises used: And.right, And.left, Iff.mp, finsetInf'_mem_infClosure, Finset.mem_product
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : DistribLattice α
s : Set α
hs : SupClosed s
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
⊢ Membership.mem (γ := Set α) ((infClosure : (a : Set α) → Set α) s : Set α)
    ((t ×ˢ u).inf' ⋯ fun (i : α × α) ↦ id i.1 ⊔ id i.2)

Tactic:
exact finsetInf'_mem_infClosure _
    fun i hi ↦ hs (hts (mem_product.1 hi).1) (hus (mem_product.1 hi).2)

Premises used: And.right, And.left, Iff.mp, finsetInf'_mem_infClosure, Finset.mem_product
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : DistribLattice α
s : Set α
hs : InfClosed s
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
rw :
  Membership.mem (γ := Set α) ((supClosure : (a : Set α) → Set α) s : Set α)
    ((t ×ˢ u).sup' ⋯ fun (i : α × α) ↦ id i.1 ⊓ id i.2)
⊢ Membership.mem (γ := Set α) ((supClosure : (a : Set α) → Set α) s : Set α) (t.sup' ht id ⊓ u.sup' hu id)

Tactic:
rw [sup'_inf_sup']

Premises used: Finset.sup'_inf_sup'
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : DistribLattice α
s : Set α
hs : InfClosed s
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
⊢ Membership.mem (γ := Set α) ((supClosure : (a : Set α) → Set α) s : Set α)
    ((t ×ˢ u).sup' ⋯ fun (i : α × α) ↦ id i.1 ⊓ id i.2)

Tactic:
finsetSup'_mem_supClosure _
    fun i hi ↦ hs (hts (mem_product.1 hi).1) (hus (mem_product.1 hi).2)

Premises used: And.right, And.left, Iff.mp, Finset.mem_product, finsetSup'_mem_supClosure
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : DistribLattice α
s : Set α
hs : InfClosed s
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
⊢ Membership.mem (γ := Set α) ((supClosure : (a : Set α) → Set α) s : Set α)
    ((t ×ˢ u).sup' ⋯ fun (i : α × α) ↦ id i.1 ⊓ id i.2)

Tactic:
exact finsetSup'_mem_supClosure _
    fun i hi ↦ hs (hts (mem_product.1 hi).1) (hus (mem_product.1 hi).2)

Premises used: And.right, And.left, Iff.mp, Finset.mem_product, finsetSup'_mem_supClosure
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : DistribLattice α
s : Set α
⊢ Eq (α := Set α) ((supClosure : (a : Set α) → Set α) ((infClosure : (a : Set α) → Set α) s : Set α) : Set α)
    ((latticeClosure : (a : Set α) → Set α) s : Set α)

Tactic:
le_antisymm (supClosure_min (infClosure_min subset_latticeClosure isSublattice_latticeClosure.2)
    isSublattice_latticeClosure.1) <| latticeClosure_min (subset_infClosure.trans subset_supClosure)
      ⟨supClosed_supClosure, infClosed_infClosure.supClosure⟩

Premises used: isSublattice_latticeClosure, infClosed_infClosure, HasSubset.Subset.trans, IsSublattice.mk, subset_latticeClosure, subset_infClosure, le_antisymm, IsSublattice.supClosed, infClosure_min, InfClosed.supClosure, IsSublattice.infClosed, subset_supClosure, supClosed_supClosure, latticeClosure_min, supClosure_min
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : DistribLattice α
s : Set α
⊢ Eq (α := Set α) ((infClosure : (a : Set α) → Set α) ((supClosure : (a : Set α) → Set α) s : Set α) : Set α)
    ((latticeClosure : (a : Set α) → Set α) s : Set α)

Tactic:
le_antisymm (infClosure_min (supClosure_min subset_latticeClosure isSublattice_latticeClosure.1)
    isSublattice_latticeClosure.2) <| latticeClosure_min (subset_supClosure.trans subset_infClosure)
      ⟨supClosed_supClosure.infClosure, infClosed_infClosure⟩

Premises used: isSublattice_latticeClosure, SupClosed.infClosure, infClosed_infClosure, HasSubset.Subset.trans, IsSublattice.mk, subset_latticeClosure, subset_infClosure, le_antisymm, IsSublattice.supClosed, infClosure_min, IsSublattice.infClosed, subset_supClosure, supClosed_supClosure, latticeClosure_min, supClosure_min
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : DistribLattice α
s : Set α
hs : s.Finite
rw : Set.Finite.{u_3} (α := α) ((supClosure : (a : Set α) → Set α) ((infClosure : (a : Set α) → Set α) s : Set α))
⊢ Set.Finite.{u_3} (α := α) ((_root_.latticeClosure : (a : Set α) → Set α) s)

Tactic:
rw [← supClosure_infClosure]

Premises used: supClosure_infClosure
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : DistribLattice α
s : Set α
hs : s.Finite
⊢ Set.Finite.{u_3} (α := α) ((supClosure : (a : Set α) → Set α) ((infClosure : (a : Set α) → Set α) s : Set α))

Tactic:
hs.infClosure.supClosure

Premises used: Set.Finite.infClosure, Set.Finite.supClosure
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : DistribLattice α
s : Set α
hs : s.Finite
⊢ Set.Finite.{u_3} (α := α) ((supClosure : (a : Set α) → Set α) ((infClosure : (a : Set α) → Set α) s : Set α))

Tactic:
exact hs.infClosure.supClosure

Premises used: Set.Finite.infClosure, Set.Finite.supClosure
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
β : Type u_4
inst : DistribLattice α
inst_1 : DistribLattice β
s : Set α
t : Set β
simp_rw :
  (supClosure : (a : Set (α × β)) → Set (α × β)) ((infClosure : (a : Set (α × β)) → Set (α × β)) (s ×ˢ t)) =
    SProd.sprod (α := Set α) (β := Set β)
      ((supClosure : (a : Set α) → Set α) ((infClosure : (a : Set α) → Set α) s : Set α) : Set α)
      ((supClosure : (a : Set β) → Set β) ((infClosure : (a : Set β) → Set β) t : Set β) : Set β)
⊢ (latticeClosure : (a : Set (α × β)) → Set (α × β)) (s ×ˢ t) =
    SProd.sprod (α := Set α) (β := Set β) ((latticeClosure : (a : Set α) → Set α) s : Set α)
      ((latticeClosure : (a : Set β) → Set β) t : Set β)

Tactic:
simp_rw [← supClosure_infClosure]

Premises used: supClosure_infClosure
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
β : Type u_4
inst : DistribLattice α
inst_1 : DistribLattice β
s : Set α
t : Set β
⊢ (supClosure : (a : Set (α × β)) → Set (α × β)) ((infClosure : (a : Set (α × β)) → Set (α × β)) (s ×ˢ t)) =
    SProd.sprod (α := Set α) (β := Set β)
      ((supClosure : (a : Set α) → Set α) ((infClosure : (a : Set α) → Set α) s : Set α) : Set α)
      ((supClosure : (a : Set β) → Set β) ((infClosure : (a : Set β) → Set β) t : Set β) : Set β)

Tactic:
simp
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
α : Type u_3
inst : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst_1 : Finite ι
inst_2 : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
intro : ∀ (val : Fintype (PLift ι)), ⨆ (i : ι), f i ∈ s
⊢ ⨆ (i : ι), f i ∈ s

Tactic:
cases nonempty_fintype (PLift ι)

Premises used: PLift, nonempty_fintype
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
α : Type u_3
inst : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst_1 : Finite ι
inst_2 : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
val : Fintype (PLift ι)
intro : (sup' univ ⋯ fun (i : PLift ι) ↦ f i.down) ∈ s
⊢ ⨆ (i : ι), f i ∈ s

Tactic:
rw [← iSup_plift_down, ← Finset.sup'_univ_eq_ciSup]

Premises used: iSup_plift_down, Finset.sup'_univ_eq_ciSup
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
α : Type u_3
inst : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst_1 : Finite ι
inst_2 : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
val : Fintype (PLift ι)
⊢ (sup' univ ⋯ fun (i : PLift ι) ↦ f i.down) ∈ s

Tactic:
hs.finsetSup'_mem Finset.univ_nonempty fun _ _ ↦ hf _

Premises used: Finset.univ_nonempty, PLift.down, SupClosed.finsetSup'_mem
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
α : Type u_3
inst : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst_1 : Finite ι
inst_2 : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
val : Fintype (PLift ι)
⊢ (sup' univ ⋯ fun (i : PLift ι) ↦ f i.down) ∈ s

Tactic:
exact hs.finsetSup'_mem Finset.univ_nonempty fun _ _ ↦ hf _

Premises used: Finset.univ_nonempty, SupClosed.finsetSup'_mem
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
α : Type u_3
inst : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst_1 : Finite ι
inst_2 : Nonempty ι
hs : InfClosed s
hf : ∀ (i : ι), f i ∈ s
⊢ ⨅ (i : ι), f i ∈ s

Tactic:
hs.dual.iSup_mem_of_nonempty hf

Premises used: iInf, Set.Mem, iSup, setOf, SupClosed.iSup_mem_of_nonempty, Set.preimage, InfClosed.dual, OrderDual
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
⊢ Finite.{u_3 + 1} (↑t : Type u_3)

Tactic:
have := ht.to_subtype
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this : Finite.{u_3 + 1} (↑t : Type u_3)
⊢ Nonempty.{u_3 + 1} (↑t : Type u_3)

Tactic:
have := ht'.to_subtype
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this_1 : Finite.{u_3 + 1} (↑t : Type u_3)
this : Nonempty.{u_3 + 1} (↑t : Type u_3)
rw : ⨆ (a : (↑t : Type u_3)), (↑a : α) ∈ s
⊢ sSup t ∈ s

Tactic:
rw [sSup_eq_iSup']

Premises used: sSup_eq_iSup'
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this_1 : Finite.{u_3 + 1} (↑t : Type u_3)
this : Nonempty.{u_3 + 1} (↑t : Type u_3)
⊢ ∀ (i : (↑t : Type u_3)), (↑i : α) ∈ s

Tactic:
simpa
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this_1 : Finite.{u_3 + 1} (↑t : Type u_3)
this : Nonempty.{u_3 + 1} (↑t : Type u_3)
⊢ ⨆ (a : (↑t : Type u_3)), (↑a : α) ∈ s

Tactic:
exact hs.iSup_mem_of_nonempty (by simpa)

Premises used: SupClosed.iSup_mem_of_nonempty
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : ConditionallyCompleteLattice α
s t : Set α
hs : InfClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
⊢ sInf t ∈ s

Tactic:
hs.dual.sSup_mem_of_nonempty ht ht' hts

Premises used: Set.Mem, setOf, SupClosed.sSup_mem_of_nonempty, Set.preimage, InfClosed.dual
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : BooleanAlgebra α
s : Set α
⊢ Eq.{u_3 + 1} (α := Set α) (compl '' (latticeClosure : (a : Set α) → Set α) s)
    ((latticeClosure : (a : Set α) → Set α) (compl '' s))

Tactic:
image_latticeClosure' s _ compl_sup_distrib (fun _ _ => compl_inf)

Premises used: compl_inf, image_latticeClosure', compl_sup_distrib
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : BooleanAlgebra α
s : Set α
hs : compl '' s = s
⊢ Eq.{u_3 + 1} (α := Set α) (compl '' (latticeClosure : (a : Set α) → Set α) s)
    ((latticeClosure : (a : Set α) → Set α) s)

Tactic:
compl_image_latticeClosure s ▸ hs.symm ▸ rfl

Premises used: compl_image_latticeClosure, Eq.rec, Eq.symm, rfl
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hf : ∀ i ∈ t, f i ∈ s
rw : sSup (f '' t) ∈ s
⊢ ⨆ i ∈ t, f i ∈ s

Tactic:
rw [← sSup_image]

Premises used: sSup_image
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hf : ∀ i ∈ t, f i ∈ s
⊢ (f '' t).Nonempty

Tactic:
simpa
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hf : ∀ i ∈ t, f i ∈ s
⊢ f '' t ⊆ s

Tactic:
simpa
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hf : ∀ i ∈ t, f i ∈ s
⊢ sSup (f '' t) ∈ s

Tactic:
exact hs.sSup_mem_of_nonempty (ht.image _) (by simpa) (by simpa)

Premises used: SupClosed.sSup_mem_of_nonempty, Set.Finite.image
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : InfClosed s
ht : t.Finite
ht' : t.Nonempty
hf : ∀ i ∈ t, f i ∈ s
⊢ ⨅ i ∈ t, f i ∈ s

Tactic:
hs.dual.biSup_mem_of_nonempty ht ht' hf

Premises used: iInf, SupClosed.biSup_mem_of_nonempty, Set.Mem, iSup, setOf, Set.preimage, InfClosed.dual, OrderDual
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
α : Type u_3
inst : CompleteLattice α
f : ι → α
s : Set α
inst_1 : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
inl : IsEmpty ι → ⨆ (i : ι), f i ∈ s
inr : Nonempty ι → ⨆ (i : ι), f i ∈ s
⊢ ⨆ (i : ι), f i ∈ s

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
α : Type u_3
inst : CompleteLattice α
f : ι → α
s : Set α
inst_1 : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
h : IsEmpty ι
⊢ ⨆ (i : ι), f i ∈ s

Tactic:
simpa [iSup_of_empty]

Premises used: iSup_of_empty
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
α : Type u_3
inst : CompleteLattice α
f : ι → α
s : Set α
inst_1 : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
h : Nonempty ι
⊢ ⨆ (i : ι), f i ∈ s

Tactic:
hs.iSup_mem_of_nonempty hf

Premises used: SupClosed.iSup_mem_of_nonempty
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
α : Type u_3
inst : CompleteLattice α
f : ι → α
s : Set α
inst_1 : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
h : Nonempty ι
⊢ ⨆ (i : ι), f i ∈ s

Tactic:
exact hs.iSup_mem_of_nonempty hf

Premises used: SupClosed.iSup_mem_of_nonempty
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Sort u_1
α : Type u_3
inst : CompleteLattice α
f : ι → α
s : Set α
inst_1 : Finite ι
hs : InfClosed s
htop : ⊤ ∈ s
hf : ∀ (i : ι), f i ∈ s
⊢ ⨅ (i : ι), f i ∈ s

Tactic:
hs.dual.iSup_mem htop hf

Premises used: iInf, Set.Mem, iSup, SupClosed.iSup_mem, setOf, Set.preimage, InfClosed.dual, OrderDual
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
⊢ Finite.{u_3 + 1} (↑t : Type u_3)

Tactic:
have := ht.to_subtype
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
this : Finite.{u_3 + 1} (↑t : Type u_3)
rw : ⨆ (a : (↑t : Type u_3)), (↑a : α) ∈ s
⊢ sSup t ∈ s

Tactic:
rw [sSup_eq_iSup']

Premises used: sSup_eq_iSup'
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
this : Finite.{u_3 + 1} (↑t : Type u_3)
⊢ ∀ (i : (↑t : Type u_3)), (↑i : α) ∈ s

Tactic:
simpa
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
this : Finite.{u_3 + 1} (↑t : Type u_3)
⊢ ⨆ (a : (↑t : Type u_3)), (↑a : α) ∈ s

Tactic:
exact hs.iSup_mem hbot (by simpa)

Premises used: SupClosed.iSup_mem
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : CompleteLattice α
s t : Set α
hs : InfClosed s
ht : t.Finite
htop : ⊤ ∈ s
hts : t ⊆ s
⊢ sInf t ∈ s

Tactic:
hs.dual.sSup_mem ht htop hts

Premises used: Set.Mem, setOf, Set.preimage, SupClosed.sSup_mem, InfClosed.dual
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hf : ∀ i ∈ t, f i ∈ s
rw : sSup (f '' t) ∈ s
⊢ ⨆ i ∈ t, f i ∈ s

Tactic:
rw [← sSup_image]

Premises used: sSup_image
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hf : ∀ i ∈ t, f i ∈ s
⊢ f '' t ⊆ s

Tactic:
simpa
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hf : ∀ i ∈ t, f i ∈ s
⊢ sSup (f '' t) ∈ s

Tactic:
exact hs.sSup_mem (ht.image _) hbot (by simpa)

Premises used: Set.Finite.image, SupClosed.sSup_mem
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : InfClosed s
ht : t.Finite
htop : ⊤ ∈ s
hf : ∀ i ∈ t, f i ∈ s
⊢ ⨅ i ∈ t, f i ∈ s

Tactic:
hs.dual.biSup_mem ht htop hf

Premises used: iInf, Set.Mem, iSup, setOf, SupClosed.biSup_mem, Set.preimage, InfClosed.dual, OrderDual
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
inst_2 : DecidableEq ι
⊢ s.SupIndep f ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)

Tactic:
⟨fun hs _ hi => hs (erase_subset _ _) hi (notMem_erase _ _), fun hs _ ht i hi hit =>
    (hs i hi).mono_right (sup_mono fun _ hj => mem_erase.2 ⟨ne_of_mem_of_not_mem hj hit, ht hj⟩)⟩

Premises used: Iff.mpr, ne_of_mem_of_not_mem, Finset.mem_erase, And.intro, Iff.intro, Finset.sup_mono, Finset.notMem_erase, Disjoint.mono_right, Finset.erase_subset
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s t : Finset ι
f : ι → α
ht : t.SupIndep f
h : s ⊆ t
⊢ s.SupIndep f

Tactic:
fun _ hu _ hi =>
  ht (hu.trans h) (h hi)

Premises used: HasSubset.Subset.trans, Finset.SupIndep
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Finset ι
f g : ι → α
hf : s.SupIndep f
h : ∀ i ∈ s, g i ≤ f i
⊢ s.SupIndep g

Tactic:
fun _ ht j hj htj ↦ (hf ht hj htj).mono (h j hj) (sup_mono_fun fun b a ↦ h b (ht a))

Premises used: Finset.sup_mono_fun, Disjoint.mono, Finset.SupIndep
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
⊢ SupIndep ∅ f

Tactic:
fun _ _ a ha =>
  (notMem_empty a ha).elim

Premises used: False.elim, Finset.notMem_empty, Finset.SupIndep
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
i : ι
f : ι → α
s : Finset ι
hs : s ⊆ {i}
j : ι
hji : Membership.mem (γ := Finset ι) {i} j
hj : j ∉ s
rw : Disjoint (f j) ⊥
⊢ Disjoint (f j) (s.sup f)

Tactic:
rw [eq_empty_of_ssubset_singleton ⟨hs, fun h => hj (h hji)⟩, sup_empty]

Premises used: Finset.sup_empty, Finset.eq_empty_of_ssubset_singleton, And.intro
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
i : ι
f : ι → α
s : Finset ι
hs : s ⊆ {i}
j : ι
hji : Membership.mem (γ := Finset ι) {i} j
hj : j ∉ s
⊢ Disjoint (f j) ⊥

Tactic:
disjoint_bot_right

Premises used: disjoint_bot_right
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
i : ι
f : ι → α
s : Finset ι
hs : s ⊆ {i}
j : ι
hji : Membership.mem (γ := Finset ι) {i} j
hj : j ∉ s
⊢ Disjoint (f j) ⊥

Tactic:
exact disjoint_bot_right

Premises used: disjoint_bot_right
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
hs : s.SupIndep f
⊢ (↑s : Set ι).PairwiseDisjoint f

Tactic:
fun _ ha _ hb hab =>
    sup_singleton.subst <| hs (singleton_subset_iff.2 hb) ha <| notMem_singleton.2 hab

Premises used: Finset.notMem_singleton, Iff.mpr, Finset.sup_singleton, Set.PairwiseDisjoint, Eq.subst, Finset.singleton_subset_iff, Set.Pairwise
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : s.SupIndep f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
⊢ f i ≤ t.sup f ↔ i ∈ t

Tactic:
⟨fun h => ?_, le_sup⟩

Premises used: Iff.intro, Finset.le_sup
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : s.SupIndep f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
refine : ∀ (h : f i ≤ t.sup f), i ∈ t
⊢ f i ≤ t.sup f ↔ i ∈ t

Tactic:
refine ⟨fun h => ?_, le_sup⟩
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : s.SupIndep f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
h : f i ≤ t.sup f
by_contra : ∀ (hit : i ∉ t), False
⊢ i ∈ t

Tactic:
by_contra hit
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : s.SupIndep f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
h : f i ≤ t.sup f
hit : i ∉ t
⊢ False

Tactic:
hf i (disjoint_self.1 <| (hs hts hi hit).mono_right h)

Premises used: Iff.mp, disjoint_self, Disjoint.mono_right
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : s.SupIndep f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
h : f i ≤ t.sup f
hit : i ∉ t
⊢ False

Tactic:
exact hf i (disjoint_self.1 <| (hs hts hi hit).mono_right h)

Premises used: Iff.mp, disjoint_self, Disjoint.mono_right
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Finset ι
f g : ι → α
hle : ∀ x ∈ s, f x ≤ g x
h : s.SupIndep g
⊢ s.SupIndep f

Tactic:
fun _t hts i his hit ↦
  (h hts his hit).mono (hle i his) <| Finset.sup_mono_fun fun x hx ↦ hle x <| hts hx

Premises used: Finset.sup_mono_fun, Disjoint.mono, Finset.SupIndep
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
inst_2 : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι
ht : t ⊆ image g s
i : ι
hi : i ∈ image g s
hit : i ∉ t
rcases :
  ∀ (t : Finset ι') (hts : t ⊆ s) (ht : image g t ⊆ image g s) (hit : i ∉ image g t), Disjoint (f i) ((image g t).sup f)
⊢ Disjoint (f i) (t.sup f)

Tactic:
rcases subset_image_iff.mp ht with ⟨t, hts, rfl⟩

Premises used: Iff.mp, Finset.subset_image_iff, rfl
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
inst_2 : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
i : ι
hi : i ∈ image g s
t : Finset ι'
hts : t ⊆ s
ht : image g t ⊆ image g s
hit : i ∉ image g t
rcases : ∀ (i : ι') (his : i ∈ s) (hi : g i ∈ image g s) (hit : g i ∉ image g t), Disjoint (f (g i)) ((image g t).sup f)
⊢ Disjoint (f i) ((image g t).sup f)

Tactic:
rcases mem_image.mp hi with ⟨i, his, rfl⟩

Premises used: Finset.mem_image, Iff.mp, rfl
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
inst_2 : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι'
hts : t ⊆ s
ht : image g t ⊆ image g s
i : ι'
his : i ∈ s
hi : g i ∈ image g s
hit : g i ∉ image g t
rw : Disjoint (f (g i)) (t.sup (f ∘ g))
⊢ Disjoint (f (g i)) ((image g t).sup f)

Tactic:
rw [sup_image]

Premises used: Finset.sup_image
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
inst_2 : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι'
hts : t ⊆ s
ht : image g t ⊆ image g s
i : ι'
his : i ∈ s
hi : g i ∈ image g s
hit : g i ∉ image g t
⊢ Disjoint (f (g i)) (t.sup (f ∘ g))

Tactic:
hs hts his (hit <| mem_image_of_mem _ ·)

Premises used: Finset.mem_image_of_mem
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
inst_2 : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι'
hts : t ⊆ s
ht : image g t ⊆ image g s
i : ι'
his : i ∈ s
hi : g i ∈ image g s
hit : g i ∉ image g t
⊢ Disjoint (f (g i)) (t.sup (f ∘ g))

Tactic:
exact hs hts his (hit <| mem_image_of_mem _ ·)

Premises used: Finset.mem_image_of_mem
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
⊢ (map g s).SupIndep f ↔ s.SupIndep (f ∘ (⇑g : (a : ι') → ι))

Tactic:
⟨fun hs t ht i hi hit => ?_, fun hs => ?_⟩

Premises used: Iff.intro