awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Icc a b

Tactic:
Ioo_subset_Ico_self.trans Ico_subset_Icc_self

Premises used: HasSubset.Subset.trans, Finset.Ico_subset_Icc_self, Finset.Ioo_subset_Ico_self
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
rw : (↑(Icc a₁ b₁) : Set α) ⊆ (↑(Icc a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
rw₁ : Set.Icc a₁ b₁ ⊆ (↑(Icc a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
rw₂ : Set.Icc a₁ b₁ ⊆ Set.Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
rw₃ rw₄ : a₂ ≤ a₁ ∧ b₁ ≤ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
rw [← coe_subset, coe_Icc, coe_Icc, Set.Icc_subset_Icc_iff h₁]

Premises used: Set.Icc_subset_Icc_iff, Finset.coe_Icc, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
rw : (↑(Icc a₁ b₁) : Set α) ⊆ (↑(Ioo a₂ b₂) : Set α) ↔ a₂ < a₁ ∧ b₁ < b₂
rw₁ : Set.Icc a₁ b₁ ⊆ (↑(Ioo a₂ b₂) : Set α) ↔ a₂ < a₁ ∧ b₁ < b₂
rw₂ : Set.Icc a₁ b₁ ⊆ Set.Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂
rw₃ rw₄ : a₂ < a₁ ∧ b₁ < b₂ ↔ a₂ < a₁ ∧ b₁ < b₂
⊢ Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂

Tactic:
rw [← coe_subset, coe_Icc, coe_Ioo, Set.Icc_subset_Ioo_iff h₁]

Premises used: Finset.coe_Icc, Finset.coe_Ioo, Set.Icc_subset_Ioo_iff, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
rw : (↑(Icc a₁ b₁) : Set α) ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ < b₂
rw₁ : Set.Icc a₁ b₁ ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ < b₂
rw₂ : Set.Icc a₁ b₁ ⊆ Set.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂
rw₃ rw₄ : a₂ ≤ a₁ ∧ b₁ < b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂
⊢ Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂

Tactic:
rw [← coe_subset, coe_Icc, coe_Ico, Set.Icc_subset_Ico_iff h₁]

Premises used: Finset.coe_Ico, Finset.coe_Icc, Set.Icc_subset_Ico_iff, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂

Tactic:
(Icc_subset_Ico_iff h₁.dual).trans and_comm

Premises used: Set.Mem, setOf, Finset.Icc_subset_Ico_iff, and_comm, LE.le.dual, Iff.trans, OrderDual
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
rw : Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂

Tactic:
rw [← coe_ssubset, coe_Icc, coe_Icc]

Premises used: Finset.coe_Icc, Finset.coe_ssubset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂

Tactic:
Set.Icc_ssubset_Icc_left hI ha hb

Premises used: Set.Icc_ssubset_Icc_left
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂

Tactic:
exact Set.Icc_ssubset_Icc_left hI ha hb

Premises used: Set.Icc_ssubset_Icc_left
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
rw : Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂

Tactic:
rw [← coe_ssubset, coe_Icc, coe_Icc]

Premises used: Finset.coe_Icc, Finset.coe_ssubset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
⊢ Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂

Tactic:
Set.Icc_ssubset_Icc_right hI ha hb

Premises used: Set.Icc_ssubset_Icc_right
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
⊢ Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂

Tactic:
exact Set.Icc_ssubset_Icc_right hI ha hb

Premises used: Set.Icc_ssubset_Icc_right
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b c : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
d : α
hbc : b ≤ c
⊢ Disjoint (Ioc a b) (Ioc c d)

Tactic:
disjoint_left.2 fun _ h1 h2 ↦ not_and_of_not_left _
    ((mem_Ioc.1 h1).2.trans hbc).not_gt (mem_Ioc.1 h2)

Premises used: Iff.mpr, not_and_of_not_left, LE.le, And.right, LE.le.not_gt, Iff.mp, Finset.mem_Ioc, LE.le.trans, Finset.disjoint_left
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
a b : α
h : a < b
H :
  ∀ (i : Finset α) (ih : ∀ t ⊂ i, ∀ (b : α) (h : a < b) (hs : Icc a b = t), False) (b : α) (h : a < b)
    (hs : Icc a b = i), False
⊢ False

Tactic:
induction hs : Finset.Icc a b using Finset.strongInduction generalizing b with | H i ih

Premises used: Finset.Icc, Finset.strongInduction
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
a : α
i : Finset α
ih : ∀ t ⊂ i, ∀ (b : α) (h : a < b) (hs : Icc a b = t), False
b : α
h : a < b
hs : Icc a b = i
⊢ ∀ t ⊂ Icc a b, ∀ (b : α) (h : a < b) (hs : Icc a b = t), False

Tactic:
subst hs
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
a b : α
h : a < b
ih : ∀ t ⊂ Icc a b, ∀ (b : α) (h : a < b) (hs : Icc a b = t), False
H : ∀ (c : α) (hac : a < c) (hcb : c < b), False
⊢ False

Tactic:
obtain ⟨c, hac, hcb⟩ := exists_between h

Premises used: exists_between
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
a b : α
h : a < b
ih : ∀ t ⊂ Icc a b, ∀ (b : α) (h : a < b) (hs : Icc a b = t), False
c : α
hac : a < c
hcb : c < b
⊢ False

Tactic:
ih _ ?_ c hac rfl

Premises used: rfl
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
a b : α
h : a < b
ih : ∀ t ⊂ Icc a b, ∀ (b : α) (h : a < b) (hs : Icc a b = t), False
c : α
hac : a < c
hcb : c < b
H : Icc a c ⊂ Icc a b
⊢ False

Tactic:
refine ih _ ?_ c hac rfl

Premises used: rfl
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
a b : α
h : a < b
ih : ∀ t ⊂ Icc a b, ∀ (b : α) (h : a < b) (hs : Icc a b = t), False
c : α
hac : a < c
hcb : c < b
⊢ Icc a c ⊂ Icc a b

Tactic:
Finset.Icc_ssubset_Icc_right (hac.trans hcb).le le_rfl hcb

Premises used: le_rfl, LT.lt.le, Finset.Icc_ssubset_Icc_right, LT.lt.trans
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
a b : α
h : a < b
ih : ∀ t ⊂ Icc a b, ∀ (b : α) (h : a < b) (hs : Icc a b = t), False
c : α
hac : a < c
hcb : c < b
⊢ Icc a c ⊂ Icc a b

Tactic:
exact Finset.Icc_ssubset_Icc_right (hac.trans hcb).le le_rfl hcb

Premises used: le_rfl, LT.lt.le, Finset.Icc_ssubset_Icc_right, LT.lt.trans
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Ico a a = ∅

Tactic:
Ico_eq_empty <| lt_irrefl _

Premises used: Finset.Ico_eq_empty, lt_irrefl
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Ioc a a = ∅

Tactic:
Ioc_eq_empty <| lt_irrefl _

Premises used: lt_irrefl, Finset.Ioc_eq_empty
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Ioo a a = ∅

Tactic:
Ioo_eq_empty <| lt_irrefl _

Premises used: lt_irrefl, Finset.Ioo_eq_empty
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b c : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidablePred fun (x : α) ↦ x < c
hca : c ≤ a
⊢ {x ∈ Ico a b | x < c} = ∅

Tactic:
filter_false_of_mem fun _ hx => (hca.trans (mem_Ico.1 hx).1).not_gt

Premises used: Finset.filter_false_of_mem, LE.le.not_gt, And.left, Iff.mp, LE.le.trans, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b c : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidablePred fun (x : α) ↦ x < c
hbc : b ≤ c
⊢ {x ∈ Ico a b | x < c} = Ico a b

Tactic:
filter_true_of_mem fun _ hx => (mem_Ico.1 hx).2.trans_le hbc

Premises used: Finset.filter_true_of_mem, And.right, LT.lt.trans_le, Iff.mp, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b c : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidablePred fun (x : α) ↦ x < c
hcb : c ≤ b
⊢ {x ∈ Ico a b | x < c} = Ico a c

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ c ≤ x
hca : c ≤ a
⊢ {x ∈ Ico a b | c ≤ x} = Ico a b

Tactic:
filter_true_of_mem fun _ hx => hca.trans (mem_Ico.1 hx).1

Premises used: Finset.filter_true_of_mem, And.left, Iff.mp, LE.le.trans, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidablePred fun (x : α) ↦ b ≤ x
⊢ {x ∈ Ico a b | b ≤ x} = ∅

Tactic:
filter_false_of_mem fun _ hx => (mem_Ico.1 hx).2.not_ge

Premises used: Finset.filter_false_of_mem, And.right, Iff.mp, LT.lt.not_ge, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ c ≤ x
hac : a ≤ c
⊢ {x ∈ Ico a b | c ≤ x} = Ico c b

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ x < c
h : b < c
⊢ {x ∈ Icc a b | x < c} = Icc a b

Tactic:
filter_true_of_mem fun _ hx => lt_of_le_of_lt (mem_Icc.1 hx).2 h

Premises used: lt_of_le_of_lt, Finset.mem_Icc, Finset.filter_true_of_mem, And.right, Iff.mp
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ x < c
h : b < c
⊢ {x ∈ Ioc a b | x < c} = Ioc a b

Tactic:
filter_true_of_mem fun _ hx => lt_of_le_of_lt (mem_Ioc.1 hx).2 h

Premises used: lt_of_le_of_lt, Finset.filter_true_of_mem, And.right, Iff.mp, Finset.mem_Ioc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
a c : α
inst_2 : DecidablePred fun (x : α) ↦ x < c
h : a < c
⊢ {x ∈ Iic a | x < c} = Iic a

Tactic:
filter_true_of_mem fun _ hx => lt_of_le_of_lt (mem_Iic.1 hx) h

Premises used: lt_of_le_of_lt, Finset.mem_Iic, Finset.filter_true_of_mem, Iff.mp
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Fintype α
inst_3 : DecidablePred fun (j : α) ↦ a < j ∧ j < b
h : ∀ (a_1 : α), Membership.mem (γ := Finset α) {j : α | a < j ∧ j < b} a_1 ↔ a_1 ∈ Ioo a b
⊢ {j : α | a < j ∧ j < b} = Ioo a b

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Fintype α
inst_3 : DecidablePred fun (j : α) ↦ a < j ∧ j < b
a_1 : α
⊢ Membership.mem (γ := Finset α) {j : α | a < j ∧ j < b} a_1 ↔ a_1 ∈ Ioo a b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Fintype α
inst_3 : DecidablePred fun (j : α) ↦ a < j ∧ j ≤ b
h : ∀ (a_1 : α), Membership.mem (γ := Finset α) {j : α | a < j ∧ j ≤ b} a_1 ↔ a_1 ∈ Ioc a b
⊢ {j : α | a < j ∧ j ≤ b} = Ioc a b

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Fintype α
inst_3 : DecidablePred fun (j : α) ↦ a < j ∧ j ≤ b
a_1 : α
⊢ Membership.mem (γ := Finset α) {j : α | a < j ∧ j ≤ b} a_1 ↔ a_1 ∈ Ioc a b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Fintype α
inst_3 : DecidablePred fun (j : α) ↦ a ≤ j ∧ j < b
h : ∀ (a_1 : α), Membership.mem (γ := Finset α) {j : α | a ≤ j ∧ j < b} a_1 ↔ a_1 ∈ Ico a b
⊢ {j : α | a ≤ j ∧ j < b} = Ico a b

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Fintype α
inst_3 : DecidablePred fun (j : α) ↦ a ≤ j ∧ j < b
a_1 : α
⊢ Membership.mem (γ := Finset α) {j : α | a ≤ j ∧ j < b} a_1 ↔ a_1 ∈ Ico a b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Fintype α
inst_3 : DecidablePred fun (j : α) ↦ a ≤ j ∧ j ≤ b
h : ∀ (a_1 : α), Membership.mem (γ := Finset α) {j : α | a ≤ j ∧ j ≤ b} a_1 ↔ a_1 ∈ Icc a b
⊢ {j : α | a ≤ j ∧ j ≤ b} = Icc a b

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Fintype α
inst_3 : DecidablePred fun (j : α) ↦ a ≤ j ∧ j ≤ b
a_1 : α
⊢ Membership.mem (γ := Finset α) {j : α | a ≤ j ∧ j ≤ b} a_1 ↔ a_1 ∈ Icc a b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
rw : (↑(Ioi a) : Set α) = ∅ ↔ IsMax a
rw₁ : Set.Ioi a = ∅ ↔ IsMax a
rw₂ rw₃ : IsMax a ↔ IsMax a
⊢ Ioi a = ∅ ↔ IsMax a

Tactic:
rw [← coe_eq_empty, coe_Ioi, Set.Ioi_eq_empty_iff]

Premises used: Finset.coe_eq_empty, Finset.coe_Ioi, Set.Ioi_eq_empty_iff
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
contrapose! : Ioi a = ∅ ↔ IsMax a
⊢ (Ioi a).Nonempty ↔ ¬IsMax a

Tactic:
contrapose!
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
⊢ Ioi a = ∅ ↔ IsMax a

Tactic:
Ioi_eq_empty

Premises used: Finset.Ioi_eq_empty
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
⊢ Ioi a = ∅ ↔ IsMax a

Tactic:
exact Ioi_eq_empty

Premises used: Finset.Ioi_eq_empty
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : OrderTop α
⊢ Eq.{u_2 + 1} (α := Finset α) (Ioi ⊤) ∅

Tactic:
Ioi_eq_empty.mpr isMax_top

Premises used: Iff.mpr, isMax_top, Finset.Ioi_eq_empty
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : OrderBot α
inst_3 : Fintype α
h : ∀ (a : α), Membership.mem (γ := Finset α) (Ici ⊥) a ↔ Membership.mem (γ := Finset α) univ a
⊢ Eq.{u_2 + 1} (α := Finset α) (Ici ⊥) univ

Tactic:
ext a
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : OrderBot α
inst_3 : Fintype α
a : α
⊢ Membership.mem (γ := Finset α) (Ici ⊥) a ↔ Membership.mem (γ := Finset α) univ a

Tactic:
simp only [mem_Ici, bot_le, mem_univ]

Premises used: Finset.mem_univ, Finset.mem_Ici, bot_le
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
⊢ (Ici a).Nonempty

Tactic:
⟨a, mem_Ici.2 le_rfl⟩

Premises used: Iff.mpr, le_rfl, Finset.mem_Ici, Exists.intro, Finset.Nonempty
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
⊢ (Ioi a).Nonempty ↔ ¬IsMax a

Tactic:
simp [Finset.Nonempty]

Premises used: Finset.Nonempty
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
⊢ Ici a ⊆ Ici b ↔ b ≤ a

Tactic:
simp [← coe_subset]

Premises used: Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
⊢ Ici a ⊂ Ici b ↔ b < a

Tactic:
simp [← coe_ssubset]

Premises used: Finset.coe_ssubset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
h : a ≤ b
⊢ Ioi b ⊆ Ioi a

Tactic:
simpa [← coe_subset] using Set.Ioi_subset_Ioi h

Premises used: Set.Ioi_subset_Ioi, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
h : a < b
⊢ Ioi b ⊂ Ioi a

Tactic:
simpa [← coe_ssubset] using Set.Ioi_ssubset_Ioi h

Premises used: Set.Ioi_ssubset_Ioi, Finset.coe_ssubset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : LocallyFiniteOrder α
⊢ Icc a b ⊆ Ici a

Tactic:
simpa [← coe_subset] using Set.Icc_subset_Ici_self

Premises used: Set.Icc_subset_Ici_self, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : LocallyFiniteOrder α
⊢ Ico a b ⊆ Ici a

Tactic:
simpa [← coe_subset] using Set.Ico_subset_Ici_self

Premises used: Set.Ico_subset_Ici_self, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : LocallyFiniteOrder α
⊢ Ioc a b ⊆ Ioi a

Tactic:
simpa [← coe_subset] using Set.Ioc_subset_Ioi_self

Premises used: Set.Ioc_subset_Ioi_self, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ioi a

Tactic:
simpa [← coe_subset] using Set.Ioo_subset_Ioi_self

Premises used: Set.Ioo_subset_Ioi_self, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : LocallyFiniteOrder α
⊢ Ioc a b ⊆ Ici a

Tactic:
Ioc_subset_Icc_self.trans Icc_subset_Ici_self

Premises used: HasSubset.Subset.trans, Finset.Icc_subset_Ici_self, Finset.Ioc_subset_Icc_self
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ici a

Tactic:
Ioo_subset_Ico_self.trans Ico_subset_Ici_self

Premises used: HasSubset.Subset.trans, Finset.Ioo_subset_Ico_self, Finset.Ico_subset_Ici_self
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
⊢ Iio a = ∅ ↔ IsMin a

Tactic:
Ioi_eq_empty (α := αᵒᵈ)

Premises used: Finset.Iio, Finset.Ioi_eq_empty, OrderDual, IsMin
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
contrapose! : Iio a = ∅ ↔ IsMin a
⊢ (Iio a).Nonempty ↔ ¬IsMin a

Tactic:
contrapose!
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
⊢ Iio a = ∅ ↔ IsMin a

Tactic:
Iio_eq_empty

Premises used: Finset.Iio_eq_empty
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
⊢ Iio a = ∅ ↔ IsMin a

Tactic:
exact Iio_eq_empty

Premises used: Finset.Iio_eq_empty
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : OrderBot α
⊢ Eq.{u_2 + 1} (α := Finset α) (Iio ⊥) ∅

Tactic:
Iio_eq_empty.mpr isMin_bot

Premises used: Iff.mpr, isMin_bot, Finset.Iio_eq_empty
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : OrderTop α
inst_3 : Fintype α
h : ∀ (a : α), Membership.mem (γ := Finset α) (Iic ⊤) a ↔ Membership.mem (γ := Finset α) univ a
⊢ Eq.{u_2 + 1} (α := Finset α) (Iic ⊤) univ

Tactic:
ext a
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : OrderTop α
inst_3 : Fintype α
a : α
⊢ Membership.mem (γ := Finset α) (Iic ⊤) a ↔ Membership.mem (γ := Finset α) univ a

Tactic:
simp only [mem_Iic, le_top, mem_univ]

Premises used: Finset.mem_univ, Finset.mem_Iic, le_top
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
⊢ (Iic a).Nonempty

Tactic:
⟨a, mem_Iic.2 le_rfl⟩

Premises used: Iff.mpr, le_rfl, Finset.mem_Iic, Exists.intro, Finset.Nonempty
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
⊢ (Iio a).Nonempty ↔ ¬IsMin a

Tactic:
simp [Finset.Nonempty]

Premises used: Finset.Nonempty
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
⊢ Iic a ⊆ Iic b ↔ a ≤ b

Tactic:
simp [← coe_subset]

Premises used: Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
⊢ Iic a ⊂ Iic b ↔ a < b

Tactic:
simp [← coe_ssubset]

Premises used: Finset.coe_ssubset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
h : a ≤ b
⊢ Iio a ⊆ Iio b

Tactic:
simpa [← coe_subset] using Set.Iio_subset_Iio h

Premises used: Set.Iio_subset_Iio, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
h : a < b
⊢ Iio a ⊂ Iio b

Tactic:
simpa [← coe_ssubset] using Set.Iio_ssubset_Iio h

Premises used: Finset.coe_ssubset, Set.Iio_ssubset_Iio
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
β : Type u_3
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
f : α → β
hf : Monotone f
x : α
h : x ∈ Iic a
⊢ x ≤ a

Tactic:
simpa using h
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
β : Type u_3
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
f : α → β
hf : Monotone f
⊢ a ∈ Iic a

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : LocallyFiniteOrder α
⊢ Icc a b ⊆ Iic b

Tactic:
simpa [← coe_subset] using Set.Icc_subset_Iic_self

Premises used: Set.Icc_subset_Iic_self, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : LocallyFiniteOrder α
⊢ Ioc a b ⊆ Iic b

Tactic:
simpa [← coe_subset] using Set.Ioc_subset_Iic_self

Premises used: Set.Ioc_subset_Iic_self, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : LocallyFiniteOrder α
⊢ Ico a b ⊆ Iio b

Tactic:
simpa [← coe_subset] using Set.Ico_subset_Iio_self

Premises used: Set.Ico_subset_Iio_self, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Iio b

Tactic:
simpa [← coe_subset] using Set.Ioo_subset_Iio_self

Premises used: Set.Ioo_subset_Iio_self, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : LocallyFiniteOrder α
⊢ Ico a b ⊆ Iic b

Tactic:
Ico_subset_Icc_self.trans Icc_subset_Iic_self

Premises used: Finset.Icc_subset_Iic_self, HasSubset.Subset.trans, Finset.Ico_subset_Icc_self
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Iic b

Tactic:
Ioo_subset_Ioc_self.trans Ioc_subset_Iic_self

Premises used: Finset.Ioc_subset_Iic_self, HasSubset.Subset.trans, Finset.Ioo_subset_Ioc_self