awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : SuccOrder α
a : α
⊢ (↑a : WithBot α).succ = Order.succ a

Tactic:
rfl

Premises used: WithBot.succ, WithBot.recBotCoe, rfl
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : SuccOrder α
inst_3 : NoMaxOrder α
x : WithBot α
⊢ x < (↑x.succ : WithBot α)

Tactic:
succ_eq_succ x ▸ Order.lt_succ x

Premises used: Eq.rec, Order.lt_succ, Eq.symm, WithBot.succ_eq_succ
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : SuccOrder α
x : WithBot α
h : ⊥ ≤ x
⊢ succ ⊥ ≤ x.succ

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : SuccOrder α
a : α
hab : (↑a : WithBot α) ≤ ⊥
⊢ (↑a : WithBot α).succ ≤ succ ⊥

Tactic:
simp at hab
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : SuccOrder α
a b : α
hab : (↑a : WithBot α) ≤ (↑b : WithBot α)
⊢ a ≤ b

Tactic:
simpa using hab
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : SuccOrder α
inst_3 : NoMaxOrder α
b : α
hab : ⊥ < (↑b : WithBot α)
⊢ succ ⊥ < (↑b : WithBot α).succ

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : SuccOrder α
inst_3 : NoMaxOrder α
a b : α
hab : (↑a : WithBot α) < (↑b : WithBot α)
⊢ a < b

Tactic:
simpa using hab
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : SuccOrder α
x y : WithBot α
hxy : x ≤ y
⊢ x.succ ≤ y.succ

Tactic:
succ_mono hxy

Premises used: WithBot.succ_mono
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : SuccOrder α
x y : WithBot α
inst_3 : NoMaxOrder α
hxy : x < y
⊢ x.succ < y.succ

Tactic:
succ_strictMono hxy

Premises used: WithBot.succ_strictMono
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_2
inst : Nontrivial α
inst_1 : LinearOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
a : WithBot α
bot : Eq.{u_2 + 1} (α := α) (succ ⊥) ⊥ ↔ Eq.{u_2 + 1} (α := WithBot α) ⊥ ⊥
coe : ∀ (a : α), (↑a : WithBot α).succ = ⊥ ↔ (↑a : WithBot α) = ⊥
⊢ a.succ = ⊥ ↔ a = ⊥

Tactic:
cases a
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_2
inst : Nontrivial α
inst_1 : LinearOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
⊢ Eq.{u_2 + 1} (α := α) (succ ⊥) ⊥ ↔ Eq.{u_2 + 1} (α := WithBot α) ⊥ ⊥

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_2
inst : Nontrivial α
inst_1 : LinearOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
a : α
⊢ (↑a : WithBot α).succ = ⊥ ↔ (↑a : WithBot α) = ⊥

Tactic:
simpa [WithBot.succ_coe, WithBot.coe_ne_bot, iff_false] using Order.succ_ne_bot _

Premises used: Order.succ_ne_bot, iff_false, WithBot.succ_coe, WithBot.coe_ne_bot
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
⊢ Eq.{u_1 + 1} (α := α) (pred ⊤) ⊤

Tactic:
rfl

Premises used: WithTop.pred, WithTop.recTopCoe, rfl
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
a : α
⊢ (↑a : WithTop α).pred = Order.pred a

Tactic:
rfl

Premises used: WithTop.pred, WithTop.recTopCoe, rfl
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
x : WithTop α
h : x ≤ ⊤
⊢ x.pred ≤ pred ⊤

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
a : α
hab : ⊤ ≤ (↑a : WithTop α)
⊢ pred ⊤ ≤ (↑a : WithTop α).pred

Tactic:
simp at hab
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
a b : α
hab : (↑a : WithTop α) ≤ (↑b : WithTop α)
⊢ a ≤ b

Tactic:
simpa using hab
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
inst_3 : NoMinOrder α
b : α
hab : (↑b : WithTop α) < ⊤
⊢ (↑b : WithTop α).pred < pred ⊤

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
inst_3 : NoMinOrder α
a b : α
hab : (↑a : WithTop α) < (↑b : WithTop α)
⊢ a < b

Tactic:
simpa using hab
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
x y : WithTop α
hxy : x ≤ y
⊢ x.pred ≤ y.pred

Tactic:
pred_mono hxy

Premises used: WithTop.pred_mono
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
x y : WithTop α
inst_3 : NoMinOrder α
hxy : x < y
⊢ x.pred < y.pred

Tactic:
pred_strictMono hxy

Premises used: WithTop.pred_strictMono
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_2
inst : Nontrivial α
inst_1 : LinearOrder α
inst_2 : OrderTop α
inst_3 : PredOrder α
a : WithTop α
top : Eq.{u_2 + 1} (α := α) (pred ⊤) ⊤ ↔ Eq.{u_2 + 1} (α := WithTop α) ⊤ ⊤
coe : ∀ (a : α), (↑a : WithTop α).pred = ⊤ ↔ (↑a : WithTop α) = ⊤
⊢ a.pred = ⊤ ↔ a = ⊤

Tactic:
cases a
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_2
inst : Nontrivial α
inst_1 : LinearOrder α
inst_2 : OrderTop α
inst_3 : PredOrder α
⊢ Eq.{u_2 + 1} (α := α) (pred ⊤) ⊤ ↔ Eq.{u_2 + 1} (α := WithTop α) ⊤ ⊤

Tactic:
simp [Order.pred_ne_top]

Premises used: Order.pred_ne_top
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_2
inst : Nontrivial α
inst_1 : LinearOrder α
inst_2 : OrderTop α
inst_3 : PredOrder α
a : α
⊢ (↑a : WithTop α).pred = ⊤ ↔ (↑a : WithTop α) = ⊤

Tactic:
simp [Order.pred_ne_top]

Premises used: Order.pred_ne_top
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
⊢ SupClosed.{u_3} (α := α) ∅

Tactic:
simp [SupClosed]

Premises used: SupClosed
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
a : α
⊢ SupClosed (α := α) {a}

Tactic:
simp [SupClosed]

Premises used: SupClosed
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
⊢ SupClosed.{u_3} (α := α) univ

Tactic:
simp [SupClosed]

Premises used: SupClosed
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s t : Set α
hs : SupClosed s
ht : SupClosed t
⊢ SupClosed (s ∩ t)

Tactic:
fun _a ha _b hb ↦ ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩

Premises used: Set.Mem, setOf, SupClosed, Set.inter, And.right, And.left, And.intro
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
S : Set (Set α)
hS : ∀ s ∈ S, SupClosed s
⊢ SupClosed (⋂₀ S)

Tactic:
fun _a ha _b hb _s hs ↦ hS _ hs (ha _ hs) (hb _ hs)

Premises used: Set.Mem, setOf, SupClosed, Set.sInter
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
ι : Sort u_5
f : ι → Set α
hf : ∀ (i : ι), SupClosed (f i)
⊢ SupClosed.{u_3} (α := α) (⋂ (i : ι), f i)

Tactic:
supClosed_sInter <| forall_mem_range.2 hf

Premises used: Iff.mpr, iInf, Set.forall_mem_range, Set.iInter, supClosed_sInter
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
hs : SupClosed s
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
fun _a ha _b hb ↦ ⟨_, hs ha hb, le_sup_left, le_sup_right⟩

Premises used: le_sup_left, DirectedOn, le_sup_right, Max.max, And.intro, Exists.intro
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
hs : IsUpperSet s
⊢ SupClosed s

Tactic:
fun _a _ _b ↦ hs le_sup_right

Premises used: SupClosed, le_sup_right
-- Module: Mathlib.Order.SupClosed
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Set α
inst_2 : FunLike F β α
inst_3 : SupHomClass F β α
hs : SupClosed s
f : F
a : β
ha : Membership.mem (γ := Set β) ((⇑f : (a : β) → α) ⁻¹' s) a
b : β
hb : Membership.mem (γ := Set β) ((⇑f : (a : β) → α) ⁻¹' s) b
⊢ Membership.mem (γ := Set β) ((⇑f : (a : β) → α) ⁻¹' s) (a ⊔ b)

Tactic:
simpa [map_sup] using hs ha hb

Premises used: SupHomClass.map_sup
-- Module: Mathlib.Order.SupClosed
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Set α
inst_2 : FunLike F α β
inst_3 : SupHomClass F α β
hs : SupClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
rw : Membership.mem.{u_4, u_4} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' s) ((f : (a : α) → β) (a ⊔ b) : β)
⊢ Membership.mem.{u_4, u_4} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' s)
    ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)

Tactic:
rw [← map_sup]

Premises used: SupHomClass.map_sup
-- Module: Mathlib.Order.SupClosed
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Set α
inst_2 : FunLike F α β
inst_3 : SupHomClass F α β
hs : SupClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Membership.mem.{u_4, u_4} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' s) ((f : (a : α) → β) (a ⊔ b) : β)

Tactic:
Set.mem_image_of_mem _ <| hs ha hb

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Order.SupClosed
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Set α
inst_2 : FunLike F α β
inst_3 : SupHomClass F α β
hs : SupClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Membership.mem.{u_4, u_4} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' s) ((f : (a : α) → β) (a ⊔ b) : β)

Tactic:
exact Set.mem_image_of_mem _ <| hs ha hb

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Order.SupClosed
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : FunLike F α β
inst_3 : SupHomClass F α β
f : F
⊢ SupClosed.{u_4} (α := β) (range.{u_4, u_3 + 1} (ι := α) (⇑f : (a : α) → β))

Tactic:
simpa using supClosed_univ.image f

Premises used: SupClosed.image, supClosed_univ
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Set α
t : Set β
hs : SupClosed s
ht : SupClosed t
⊢ SupClosed (s ×ˢ t)

Tactic:
fun _a ha _b hb ↦ ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩

Premises used: Set.Mem, setOf, Set.prod, SupClosed, And.right, And.left, And.intro
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Type u_6
α : ι → Type u_7
inst : (i : ι) → SemilatticeSup (α i)
s : Set ι
t : (i : ι) → Set (α i)
ht : ∀ i ∈ s, SupClosed (t i)
⊢ SupClosed (s.pi (α := α) t)

Tactic:
fun _a ha _b hb _i hi ↦ ht _ hi (ha _ hi) (hb _ hi)

Premises used: Set.Mem, setOf, SupClosed, Set.pi
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
a : α
hs : SupClosed s
ha : a ∈ upperBounds s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊔ b ∈ insert a s

Tactic:
aesop
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
a : α
h : SupClosed s
ha : a ∈ lowerBounds s
⊢ ∀ b ∈ s, a ≤ b

Tactic:
have ha' : ∀ b ∈ s, a ≤ b := fun _ a ↦ ha a
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
a : α
h : SupClosed s
ha : a ∈ lowerBounds s
ha' : ∀ b ∈ s, a ≤ b
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊔ b ∈ insert a s

Tactic:
aesop
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
ι : Type u_5
f : ι → α
s : Set α
t : Finset ι
hs : SupClosed s
ht : t.Nonempty
⊢ (∀ i ∈ t, f i ∈ s) → t.sup' ht f ∈ s

Tactic:
sup'_induction _ _ hs

Premises used: Finset.sup'_induction
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeSup α
ι : Type u_5
f : ι → α
s : Set α
t : Finset ι
inst_1 : OrderBot α
hs : SupClosed s
ht : t.Nonempty
⊢ (∀ i ∈ t, f i ∈ s) → t.sup f ∈ s

Tactic:
sup'_eq_sup ht f ▸ hs.finsetSup'_mem ht

Premises used: Eq.rec, SupClosed.finsetSup'_mem, Finset.sup'_eq_sup
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
⊢ InfClosed.{u_3} (α := α) ∅

Tactic:
simp [InfClosed]

Premises used: InfClosed
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
a : α
⊢ InfClosed (α := α) {a}

Tactic:
simp [InfClosed]

Premises used: InfClosed
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
⊢ InfClosed.{u_3} (α := α) univ

Tactic:
simp [InfClosed]

Premises used: InfClosed
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s t : Set α
hs : InfClosed s
ht : InfClosed t
⊢ InfClosed (s ∩ t)

Tactic:
fun _a ha _b hb ↦ ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩

Premises used: Set.Mem, setOf, Set.inter, And.right, And.left, And.intro, InfClosed
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
S : Set (Set α)
hS : ∀ s ∈ S, InfClosed s
⊢ InfClosed (⋂₀ S)

Tactic:
fun _a ha _b hb _s hs ↦ hS _ hs (ha _ hs) (hb _ hs)

Premises used: Set.Mem, setOf, InfClosed, Set.sInter
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
ι : Sort u_5
f : ι → Set α
hf : ∀ (i : ι), InfClosed (f i)
⊢ InfClosed.{u_3} (α := α) (⋂ (i : ι), f i)

Tactic:
infClosed_sInter <| forall_mem_range.2 hf

Premises used: Iff.mpr, iInf, Set.forall_mem_range, Set.iInter, infClosed_sInter
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
hs : InfClosed s
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≥ x2) s

Tactic:
fun _a ha _b hb ↦ ⟨_, hs ha hb, inf_le_left, inf_le_right⟩

Premises used: DirectedOn, inf_le_right, And.intro, Exists.intro, inf_le_left, Min.min
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
hs : IsLowerSet s
⊢ InfClosed s

Tactic:
fun _a _ _b ↦ hs inf_le_right

Premises used: inf_le_right, InfClosed
-- Module: Mathlib.Order.SupClosed
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s : Set α
inst_2 : FunLike F β α
inst_3 : InfHomClass F β α
hs : InfClosed s
f : F
a : β
ha : Membership.mem (γ := Set β) ((⇑f : (a : β) → α) ⁻¹' s) a
b : β
hb : Membership.mem (γ := Set β) ((⇑f : (a : β) → α) ⁻¹' s) b
⊢ Membership.mem (γ := Set β) ((⇑f : (a : β) → α) ⁻¹' s) (a ⊓ b)

Tactic:
simpa [map_inf] using hs ha hb

Premises used: InfHomClass.map_inf
-- Module: Mathlib.Order.SupClosed
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s : Set α
inst_2 : FunLike F α β
inst_3 : InfHomClass F α β
hs : InfClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
rw : Membership.mem.{u_4, u_4} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' s) ((f : (a : α) → β) (a ⊓ b) : β)
⊢ Membership.mem.{u_4, u_4} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' s)
    ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β)

Tactic:
rw [← map_inf]

Premises used: InfHomClass.map_inf
-- Module: Mathlib.Order.SupClosed
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s : Set α
inst_2 : FunLike F α β
inst_3 : InfHomClass F α β
hs : InfClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Membership.mem.{u_4, u_4} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' s) ((f : (a : α) → β) (a ⊓ b) : β)

Tactic:
Set.mem_image_of_mem _ <| hs ha hb

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Order.SupClosed
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s : Set α
inst_2 : FunLike F α β
inst_3 : InfHomClass F α β
hs : InfClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Membership.mem.{u_4, u_4} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' s) ((f : (a : α) → β) (a ⊓ b) : β)

Tactic:
exact Set.mem_image_of_mem _ <| hs ha hb

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Order.SupClosed
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
inst_2 : FunLike F α β
inst_3 : InfHomClass F α β
f : F
⊢ InfClosed.{u_4} (α := β) (range.{u_4, u_3 + 1} (ι := α) (⇑f : (a : α) → β))

Tactic:
simpa using infClosed_univ.image f

Premises used: InfClosed.image, infClosed_univ
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s : Set α
t : Set β
hs : InfClosed s
ht : InfClosed t
⊢ InfClosed (s ×ˢ t)

Tactic:
fun _a ha _b hb ↦ ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩

Premises used: Set.Mem, setOf, Set.prod, And.right, And.left, And.intro, InfClosed
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Type u_6
α : ι → Type u_7
inst : (i : ι) → SemilatticeInf (α i)
s : Set ι
t : (i : ι) → Set (α i)
ht : ∀ i ∈ s, InfClosed (t i)
⊢ InfClosed (s.pi (α := α) t)

Tactic:
fun _a ha _b hb _i hi ↦ ht _ hi (ha _ hi) (hb _ hi)

Premises used: Set.Mem, setOf, Set.pi, InfClosed
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
a : α
hs : InfClosed s
ha : a ∈ upperBounds s
⊢ ∀ b ∈ s, b ≤ a

Tactic:
have ha' : ∀ b ∈ s, b ≤ a := fun _ a ↦ ha a
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
a : α
hs : InfClosed s
ha : a ∈ upperBounds s
ha' : ∀ b ∈ s, b ≤ a
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊓ b ∈ insert a s

Tactic:
aesop
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
a : α
h : InfClosed s
ha : a ∈ lowerBounds s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊓ b ∈ insert a s

Tactic:
aesop
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
ι : Type u_5
f : ι → α
s : Set α
t : Finset ι
hs : InfClosed s
ht : t.Nonempty
⊢ (∀ i ∈ t, f i ∈ s) → t.inf' ht f ∈ s

Tactic:
inf'_induction _ _ hs

Premises used: Finset.inf'_induction
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
ι : Type u_5
f : ι → α
s : Set α
t : Finset ι
inst_1 : OrderTop α
hs : InfClosed s
ht : t.Nonempty
⊢ (∀ i ∈ t, f i ∈ s) → t.inf f ∈ s

Tactic:
inf'_eq_inf ht f ▸ hs.finsetInf'_mem ht

Premises used: Eq.rec, InfClosed.finsetInf'_mem, Finset.inf'_eq_inf
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
⊢ IsSublattice.{u_3} (α := α) ∅

Tactic:
⟨supClosed_empty, infClosed_empty⟩

Premises used: supClosed_empty, IsSublattice.mk, infClosed_empty
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
a : α
⊢ IsSublattice (α := α) {a}

Tactic:
⟨supClosed_singleton, infClosed_singleton⟩

Premises used: IsSublattice.mk, supClosed_singleton, infClosed_singleton
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
⊢ IsSublattice.{u_3} (α := α) Set.univ

Tactic:
⟨supClosed_univ, infClosed_univ⟩

Premises used: infClosed_univ, IsSublattice.mk, supClosed_univ
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
s t : Set α
hs : IsSublattice s
ht : IsSublattice t
⊢ IsSublattice (s ∩ t)

Tactic:
⟨hs.1.inter ht.1, hs.2.inter ht.2⟩

Premises used: IsSublattice.mk, IsSublattice.supClosed, SupClosed.inter, IsSublattice.infClosed, InfClosed.inter
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
S : Set (Set α)
hS : ∀ s ∈ S, IsSublattice s
⊢ IsSublattice (⋂₀ S)

Tactic:
⟨supClosed_sInter fun _s hs ↦ (hS _ hs).1, infClosed_sInter fun _s hs ↦ (hS _ hs).2⟩

Premises used: IsSublattice.mk, IsSublattice.supClosed, supClosed_sInter, IsSublattice.infClosed, infClosed_sInter
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
ι : Sort u_5
inst : Lattice α
f : ι → Set α
hf : ∀ (i : ι), IsSublattice (f i)
⊢ IsSublattice.{u_3} (α := α) (⋂ (i : ι), f i)

Tactic:
⟨supClosed_iInter fun _i ↦ (hf _).1, infClosed_iInter fun _i ↦ (hf _).2⟩

Premises used: IsSublattice.mk, infClosed_iInter, supClosed_iInter, IsSublattice.supClosed, IsSublattice.infClosed
-- Module: Mathlib.Order.SupClosed
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : Lattice α
inst_1 : Lattice β
s : Set α
inst_2 : FunLike F β α
inst_3 : LatticeHomClass F β α
hs : IsSublattice s
f : F
⊢ IsSublattice.{u_4} (α := β) ((⇑f : (a : β) → α) ⁻¹' s)

Tactic:
⟨hs.1.preimage _, hs.2.preimage _⟩

Premises used: IsSublattice.mk, InfClosed.preimage, IsSublattice.supClosed, IsSublattice.infClosed, SupClosed.preimage
-- Module: Mathlib.Order.SupClosed
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : Lattice α
inst_1 : Lattice β
s : Set α
inst_2 : FunLike F α β
inst_3 : LatticeHomClass F α β
hs : IsSublattice s
f : F
⊢ IsSublattice.{u_4} (α := β) ((⇑f : (a : α) → β) '' s)

Tactic:
⟨hs.1.image _, hs.2.image _⟩

Premises used: SupClosed.image, InfClosed.image, IsSublattice.mk, IsSublattice.supClosed, IsSublattice.infClosed
-- Module: Mathlib.Order.SupClosed
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : FunLike F α β
inst_3 : LatticeHomClass F α β
f : F
⊢ IsSublattice.{u_4} (α := β) (Set.range.{u_4, u_3 + 1} (ι := α) (⇑f : (a : α) → β))

Tactic:
⟨supClosed_range _, infClosed_range _⟩

Premises used: IsSublattice.mk, infClosed_range, supClosed_range
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
β : Type u_4
inst : Lattice α
inst_1 : Lattice β
s : Set α
t : Set β
hs : IsSublattice s
ht : IsSublattice t
⊢ IsSublattice (s ×ˢ t)

Tactic:
⟨hs.1.prod ht.1, hs.2.prod ht.2⟩

Premises used: IsSublattice.mk, InfClosed.prod, IsSublattice.supClosed, IsSublattice.infClosed, SupClosed.prod
-- Module: Mathlib.Order.SupClosed
Goal:
ι : Type u_6
α : ι → Type u_7
inst : (i : ι) → Lattice (α i)
s : Set ι
t : (i : ι) → Set (α i)
ht : ∀ i ∈ s, IsSublattice (t i)
⊢ IsSublattice (s.pi (α := α) t)

Tactic:
⟨supClosed_pi fun _i hi ↦ (ht _ hi).1, infClosed_pi fun _i hi ↦ (ht _ hi).2⟩

Premises used: supClosed_pi, infClosed_pi, IsSublattice.mk, IsSublattice.supClosed, IsSublattice.infClosed
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
s : Set αᵒᵈ
⊢ SupClosed (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔ InfClosed s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, OrderDual, InfClosed
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
s : Set αᵒᵈ
⊢ InfClosed (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔ SupClosed s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SupClosed, Set.preimage, OrderDual
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
s : Set α
⊢ SupClosed (α := αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ↔ InfClosed s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, OrderDual, InfClosed
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
s : Set α
⊢ InfClosed (α := αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ↔ SupClosed s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SupClosed, Set.preimage, OrderDual
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
s : Set αᵒᵈ
⊢ IsSublattice (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔ IsSublattice s

Tactic:
⟨fun h ↦ ⟨h.2, h.1⟩, fun h ↦ ⟨h.2, h.1⟩⟩

Premises used: IsSublattice.mk, IsSublattice.supClosed, Iff.intro, IsSublattice.infClosed
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
s : Set α
⊢ IsSublattice (α := αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ↔ IsSublattice s

Tactic:
⟨fun h ↦ ⟨h.2, h.1⟩, fun h ↦ ⟨h.2, h.1⟩⟩

Premises used: IsSublattice.mk, IsSublattice.supClosed, Iff.intro, IsSublattice.infClosed
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
inl : a ≤ b → max a b ∈ s
inr : b ≤ a → max a b ∈ s
⊢ max a b ∈ s

Tactic:
cases le_total a b

Premises used: le_total
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h : a ≤ b
⊢ max a b ∈ s

Tactic:
simp [*]
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h : b ≤ a
⊢ max a b ∈ s

Tactic:
simp [*]
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
inl : a ≤ b → min a b ∈ s
inr : b ≤ a → min a b ∈ s
⊢ min a b ∈ s

Tactic:
cases le_total a b

Premises used: le_total
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h : a ≤ b
⊢ min a b ∈ s

Tactic:
simp [*]
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h : b ≤ a
⊢ min a b ∈ s

Tactic:
simp [*]