awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b c : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : LocallyFiniteOrder α
h : a ≤ b
⊢ Disjoint (Iic a) (Ioc b c)

Tactic:
disjoint_left.2 fun _ hax hbcx ↦ (mem_Iic.1 hax).not_gt <| lt_of_le_of_lt h (mem_Ioc.1 hbcx).1

Premises used: Iff.mpr, lt_of_le_of_lt, Finset.mem_Iic, LE.le.not_gt, And.left, Iff.mp, Finset.mem_Ioc, Finset.disjoint_left
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
ι : Type u_1
α : Type u_2
a_1 a₁ a₂ b_1 b₁ b₂ c x : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : LocallyFiniteOrder α
a : α
b : (↑(Set.Iic a) : Type u_2)
rw : (↑b : α) ∈ Set.Iic a
⊢ (↑b : α) ∈ Iic a

Tactic:
rw [← mem_coe, coe_Iic a]

Premises used: Finset.coe_Iic, Finset.mem_coe
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
ι : Type u_1
α : Type u_2
a_1 a₁ a₂ b_1 b₁ b₂ c x : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : LocallyFiniteOrder α
a : α
b : (↑(Set.Iic a) : Type u_2)
⊢ (↑b : α) ∈ Set.Iic a

Tactic:
b.2

Premises used: Subtype.property
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
ι : Type u_1
α : Type u_2
a_1 a₁ a₂ b_1 b₁ b₂ c x : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : LocallyFiniteOrder α
a : α
b : (↑(Set.Iic a) : Type u_2)
⊢ (↑b : α) ∈ Set.Iic a

Tactic:
exact b.2

Premises used: Subtype.property
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
⊢ Ioi a ⊆ Ici a

Tactic:
simpa [← coe_subset] using Set.Ioi_subset_Ici_self

Premises used: Set.Ioi_subset_Ici_self, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
s : Set α
hs : BddBelow s
⊢ s.Finite

Tactic:
let ⟨a, ha⟩ := hs
  (Ici a).finite_toSet.subset fun _ hx => mem_Ici.2 <| ha hx

Premises used: Iff.mpr, Finset.mem_Ici, Set.Finite, _private.0.BddBelow.finite.match_1, Finset.Ici, Set.Finite.subset, Finset.finite_toSet
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
s : Set α
⊢ s.Infinite → ¬BddBelow s

Tactic:
mt BddBelow.finite

Premises used: mt, BddBelow.finite, Set.Infinite
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
inst_2 : Fintype α
inst_3 : DecidablePred fun (x : α) ↦ a < x
h : ∀ (a_1 : α), Membership.mem (γ := Finset α) {x : α | a < x} a_1 ↔ a_1 ∈ Ioi a
⊢ {x : α | a < x} = Ioi a

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

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

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

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

Tactic:
simpa [← coe_subset] using Set.Iio_subset_Iic_self

Premises used: Set.Iio_subset_Iic_self, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
s : Set α
hs : BddAbove s
⊢ s.Finite

Tactic:
hs.dual.finite

Premises used: Set.Mem, setOf, Set.preimage, BddAbove.dual, OrderDual, BddBelow.finite
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
s : Set α
⊢ s.Infinite → ¬BddAbove s

Tactic:
mt BddAbove.finite

Premises used: mt, BddAbove.finite, Set.Infinite
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
a : α
inst_2 : Fintype α
inst_3 : DecidablePred fun (x : α) ↦ x < a
h : ∀ (a_1 : α), Membership.mem (γ := Finset α) {x : α | x < a} a_1 ↔ a_1 ∈ Iio a
⊢ {x : α | x < a} = Iio a

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

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

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

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

Tactic:
rfl

Premises used: Finset.Icc, Finset.Iic, rfl
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : OrderTop α
⊢ Icc a ⊤ = Ici a

Tactic:
rfl

Premises used: Finset.Ici, Finset.Icc, rfl
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : OrderBot α
⊢ Ico ⊥ a = Iio a

Tactic:
rfl

Premises used: Finset.Iio, Finset.Ico, rfl
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : OrderTop α
⊢ Ioc a ⊤ = Ioi a

Tactic:
rfl

Premises used: Finset.Ioi, rfl, Finset.Ioc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : BoundedOrder α
inst_3 : Fintype α
rw : Eq.{u_2 + 1} (α := Finset α) (Iic ⊤) univ
rw₁ rw₂ : Eq.{u_2 + 1} (α := Finset α) univ univ
⊢ Eq.{u_2 + 1} (α := Finset α) (Icc ⊥ ⊤) univ

Tactic:
rw [Icc_bot, Iic_top]

Premises used: Finset.Iic_top, Finset.Icc_bot
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : LocallyFiniteOrderBot α
a : α
⊢ Disjoint (Ioi a) (Iio a)

Tactic:
disjoint_left.2 fun _ hab hba => (mem_Ioi.1 hab).not_gt <| mem_Iio.1 hba

Premises used: Iff.mpr, Finset.mem_Ioi, Iff.mp, LT.lt.not_gt, Finset.mem_Iio, Finset.disjoint_left
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a : α
rw : (↑(Icc a a) : Set α) = {a}
rw₁ : Set.Icc a a = {a}
rw₂ rw₃ : Eq (α := Set α) {a} {a}
⊢ Icc a a = {a}

Tactic:
rw [← coe_eq_singleton, coe_Icc, Set.Icc_self]

Premises used: Finset.coe_eq_singleton, Set.Icc_self, Finset.coe_Icc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : (↑(Icc a b) : Set α) = {c} ↔ a = c ∧ b = c
rw₁ : Set.Icc a b = {c} ↔ a = c ∧ b = c
rw₂ rw₃ : a = c ∧ b = c ↔ a = c ∧ b = c
⊢ Icc a b = {c} ↔ a = c ∧ b = c

Tactic:
rw [← coe_eq_singleton, coe_Icc, Set.Icc_eq_singleton_iff]

Premises used: Finset.coe_eq_singleton, Finset.coe_Icc, Set.Icc_eq_singleton_iff
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ Disjoint (Ico a b) (Ico b c)

Tactic:
disjoint_left.2 fun _ hab hbc => (mem_Ico.mp hab).2.not_ge (mem_Ico.mp hbc).1

Premises used: Iff.mpr, And.right, And.left, Iff.mp, Finset.disjoint_left, LT.lt.not_ge, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : OrderTop α
⊢ Eq (α := Finset α) (Ici ⊤) {⊤}

Tactic:
Icc_eq_singleton_iff.2 ⟨rfl, rfl⟩

Premises used: Iff.mpr, Finset.Ici, Finset.Icc, Finset.Icc_eq_singleton_iff, And.intro, rfl
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : OrderBot α
⊢ Eq (α := Finset α) (Iic ⊥) {⊥}

Tactic:
Icc_eq_singleton_iff.2 ⟨rfl, rfl⟩

Premises used: Iff.mpr, Finset.Icc, Finset.Icc_eq_singleton_iff, And.intro, Finset.Iic, rfl
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
ι : Type u_1
α : Type u_2
a_1 a₁ a₂ b_1 b₁ b₂ c_1 x : α
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : OrderBot α
rw : Unique ↥{⊥}
⊢ Unique ↥(Iic ⊥)

Tactic:
rw [Iic_bot]

Premises used: Finset.Iic_bot
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
ι : Type u_1
α : Type u_2
a_1 a₁ a₂ b_1 b₁ b₂ c_1 x : α
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : OrderBot α
⊢ Unique ↥{⊥}

Tactic:
infer_instance
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
a b : α
⊢ (Icc a b).erase a = Ioc a b

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
a b : α
⊢ (Icc a b).erase b = Ico a b

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
a b : α
⊢ (Ico a b).erase a = Ioo a b

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
a b : α
⊢ (Ioc a b).erase b = Ioo a b

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
a b : α
⊢ Icc a b \ {a, b} = Ioo a b

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
rw : (↑(insert b (Ico a b)) : Set α) = (↑(Icc a b) : Set α)
rw₁ : insert b (↑(Ico a b) : Set α) = (↑(Icc a b) : Set α)
rw₂ : insert b (↑(Ico a b) : Set α) = Set.Icc a b
rw₃ : insert b (Set.Ico a b) = Set.Icc a b
rw₄ : {b} ∪ Set.Ico a b = Set.Icc a b
rw₅ : Set.Ico a b ∪ {b} = Set.Icc a b
rw₆ rw₇ : Set.Icc a b = Set.Icc a b
⊢ insert b (Ico a b) = Icc a b

Tactic:
rw [← coe_inj, coe_insert, coe_Icc, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ico_union_right h]

Premises used: Finset.coe_Ico, Set.insert_eq, Finset.coe_Icc, Finset.coe_inj, Set.union_comm, Finset.coe_insert, Set.Ico_union_right
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
rw : (↑(insert a (Ioc a b)) : Set α) = (↑(Icc a b) : Set α)
rw₁ : insert a (↑(Ioc a b) : Set α) = (↑(Icc a b) : Set α)
rw₂ : insert a (Set.Ioc a b) = (↑(Icc a b) : Set α)
rw₃ : insert a (Set.Ioc a b) = Set.Icc a b
rw₄ : {a} ∪ Set.Ioc a b = Set.Icc a b
rw₅ : Set.Ioc a b ∪ {a} = Set.Icc a b
rw₆ rw₇ : Set.Icc a b = Set.Icc a b
⊢ insert a (Ioc a b) = Icc a b

Tactic:
rw [← coe_inj, coe_insert, coe_Ioc, coe_Icc, Set.insert_eq, Set.union_comm, Set.Ioc_union_left h]

Premises used: Set.insert_eq, Finset.coe_Icc, Finset.coe_inj, Finset.coe_Ioc, Set.union_comm, Set.Ioc_union_left, Finset.coe_insert
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
rw : (↑(insert a (Ioo a b)) : Set α) = (↑(Ico a b) : Set α)
rw₁ : insert a (↑(Ioo a b) : Set α) = (↑(Ico a b) : Set α)
rw₂ : insert a (Set.Ioo a b) = (↑(Ico a b) : Set α)
rw₃ : insert a (Set.Ioo a b) = Set.Ico a b
rw₄ : {a} ∪ Set.Ioo a b = Set.Ico a b
rw₅ : Set.Ioo a b ∪ {a} = Set.Ico a b
rw₆ rw₇ : Set.Ico a b = Set.Ico a b
⊢ insert a (Ioo a b) = Ico a b

Tactic:
rw [← coe_inj, coe_insert, coe_Ioo, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ioo_union_left h]

Premises used: Finset.coe_Ico, Set.insert_eq, Set.Ioo_union_left, Finset.coe_inj, Finset.coe_Ioo, Set.union_comm, Finset.coe_insert
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
rw : (↑(insert b (Ioo a b)) : Set α) = (↑(Ioc a b) : Set α)
rw₁ : insert b (↑(Ioo a b) : Set α) = (↑(Ioc a b) : Set α)
rw₂ : insert b (Set.Ioo a b) = (↑(Ioc a b) : Set α)
rw₃ : insert b (Set.Ioo a b) = Set.Ioc a b
rw₄ : {b} ∪ Set.Ioo a b = Set.Ioc a b
rw₅ : Set.Ioo a b ∪ {b} = Set.Ioc a b
rw₆ rw₇ : Set.Ioc a b = Set.Ioc a b
⊢ insert b (Ioo a b) = Ioc a b

Tactic:
rw [← coe_inj, coe_insert, coe_Ioo, coe_Ioc, Set.insert_eq, Set.union_comm, Set.Ioo_union_right h]

Premises used: Set.insert_eq, Finset.coe_inj, Finset.coe_Ioc, Finset.coe_Ioo, Set.union_comm, Set.Ioo_union_right, Finset.coe_insert
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
⊢ Icc a b \ Ico a b = {b}

Tactic:
simp [← coe_inj, h]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
⊢ Icc a b \ Ioc a b = {a}

Tactic:
simp [← coe_inj, h]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
⊢ Icc a b \ Ioo a b = {a, b}

Tactic:
simp [← coe_inj, h]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
⊢ Ico a b \ Ioo a b = {a}

Tactic:
simp [← coe_inj, h]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
⊢ Ioc a b \ Ioo a b = {b}

Tactic:
simp [← coe_inj, h]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
a b c : α
⊢ Ico a b ∩ Ico b c = ∅

Tactic:
(Ico_disjoint_Ico_consecutive a b c).eq_bot

Premises used: Finset.Ico_disjoint_Ico_consecutive, Disjoint.eq_bot
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
rw : Icc a b = insert b (Ico a b)
rw₁ rw₂ : Icc a b = Icc a b
⊢ Icc a b = cons b (Ico a b) ⋯

Tactic:
rw [cons_eq_insert, Ico_insert_right h]

Premises used: Finset.Ico_insert_right, Finset.cons_eq_insert
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
classical : Icc a b = insert b (Ico a b)
classical₁ classical₂ : Icc a b = Icc a b
⊢ Icc a b = cons b (Ico a b) ⋯

Tactic:
classical rw [cons_eq_insert, Ico_insert_right h]

Premises used: Finset.cons_eq_insert
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
rw : Icc a b = insert a (Ioc a b)
rw₁ rw₂ : Icc a b = Icc a b
⊢ Icc a b = cons a (Ioc a b) ⋯

Tactic:
rw [cons_eq_insert, Ioc_insert_left h]

Premises used: Finset.Ioc_insert_left, Finset.cons_eq_insert
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
classical : Icc a b = insert a (Ioc a b)
classical₁ classical₂ : Icc a b = Icc a b
⊢ Icc a b = cons a (Ioc a b) ⋯

Tactic:
classical rw [cons_eq_insert, Ioc_insert_left h]

Premises used: Finset.cons_eq_insert
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
rw : Ioc a b = insert b (Ioo a b)
rw₁ rw₂ : Ioc a b = Ioc a b
⊢ Ioc a b = cons b (Ioo a b) ⋯

Tactic:
rw [cons_eq_insert, Ioo_insert_right h]

Premises used: Finset.Ioo_insert_right, Finset.cons_eq_insert
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
classical : Ioc a b = insert b (Ioo a b)
classical₁ classical₂ : Ioc a b = Ioc a b
⊢ Ioc a b = cons b (Ioo a b) ⋯

Tactic:
classical rw [cons_eq_insert, Ioo_insert_right h]

Premises used: Finset.cons_eq_insert
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
rw : Ico a b = insert a (Ioo a b)
rw₁ rw₂ : Ico a b = Ico a b
⊢ Ico a b = cons a (Ioo a b) ⋯

Tactic:
rw [cons_eq_insert, Ioo_insert_left h]

Premises used: Finset.cons_eq_insert, Finset.Ioo_insert_left
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
classical : Ico a b = insert a (Ioo a b)
classical₁ classical₂ : Ico a b = Ico a b
⊢ Ico a b = cons a (Ioo a b) ⋯

Tactic:
classical rw [cons_eq_insert, Ioo_insert_left h]

Premises used: Finset.cons_eq_insert
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidablePred fun (x : α) ↦ x ≤ a
hab : a < b
⊢ {x ∈ Ico a b | x ≤ a} = {a}

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
pos : ∀ (h : a ≤ b), #(Ico a b) = #(Icc a b) - 1
neg : ∀ (h : ¬a ≤ b), #(Ico a b) = #(Icc a b) - 1
⊢ #(Ico a b) = #(Icc a b) - 1

Tactic:
by_cases h : a ≤ b
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
pos : #(Ico a b) = #(Ico a b) + 1 - 1
⊢ #(Ico a b) = #(Icc a b) - 1

Tactic:
rw [Icc_eq_cons_Ico h, card_cons]

Premises used: Finset.card_cons, Finset.Icc_eq_cons_Ico
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ #(Ico a b) = #(Ico a b) + 1 - 1

Tactic:
(Nat.add_sub_cancel _ _).symm

Premises used: Nat.add_sub_cancel, Eq.symm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ #(Ico a b) = #(Ico a b) + 1 - 1

Tactic:
exact (Nat.add_sub_cancel _ _).symm

Premises used: Nat.add_sub_cancel, Eq.symm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : ¬a ≤ b
neg : card.{u_2} (α := α) ∅ = #(Icc a b) - 1
neg₁ : card.{u_2} (α := α) ∅ = card.{u_2} (α := α) ∅ - 1
neg₂ : 0 = HSub.hSub (α := ℕ) 0 1
neg₃ neg₄ : Eq (α := ℕ) 0 0
⊢ #(Ico a b) = #(Icc a b) - 1

Tactic:
rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, Nat.zero_sub]

Premises used: Finset.Ico_eq_empty, Nat.zero_sub, LT.lt.le, Finset.card_empty, Finset.Icc_eq_empty
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
pos : ∀ (h : a ≤ b), #(Ico a b) = #(Icc a b) - 1
neg neg₁ : ∀ (h : ¬a ≤ b), #(Ico a b) = #(Icc a b) - 1
⊢ #(Ico a b) = #(Icc a b) - 1

Tactic:
classical
    by_cases h : a ≤ b
    · rw [Icc_eq_cons_Ico h, card_cons]
      exact (Nat.add_sub_cancel _ _).symm
    · rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, Nat.zero_sub]

Premises used: Nat.zero_sub, Finset.card_empty, Finset.card_cons, Nat.add_sub_cancel, Eq.symm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ #(Ioc a b) = #(Icc a b) - 1

Tactic:
@card_Ico_eq_card_Icc_sub_one αᵒᵈ _ _ _ _

Premises used: Finset.Icc, Finset.card_Ico_eq_card_Icc_sub_one, OrderDual, Finset.Ioc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
pos : ∀ (h : a < b), #(Ioo a b) = #(Ico a b) - 1
neg : ∀ (h : ¬a < b), #(Ioo a b) = #(Ico a b) - 1
⊢ #(Ioo a b) = #(Ico a b) - 1

Tactic:
by_cases h : a < b
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
pos : #(Ioo a b) = #(Ioo a b) + 1 - 1
⊢ #(Ioo a b) = #(Ico a b) - 1

Tactic:
rw [Ico_eq_cons_Ioo h, card_cons]

Premises used: Finset.card_cons, Finset.Ico_eq_cons_Ioo
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
⊢ #(Ioo a b) = #(Ioo a b) + 1 - 1

Tactic:
(Nat.add_sub_cancel _ _).symm

Premises used: Nat.add_sub_cancel, Eq.symm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
⊢ #(Ioo a b) = #(Ioo a b) + 1 - 1

Tactic:
exact (Nat.add_sub_cancel _ _).symm

Premises used: Nat.add_sub_cancel, Eq.symm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : ¬a < b
neg : card.{u_2} (α := α) ∅ = #(Ico a b) - 1
neg₁ : card.{u_2} (α := α) ∅ = card.{u_2} (α := α) ∅ - 1
neg₂ : 0 = HSub.hSub (α := ℕ) 0 1
neg₃ neg₄ : Eq (α := ℕ) 0 0
⊢ #(Ioo a b) = #(Ico a b) - 1

Tactic:
rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, Nat.zero_sub]

Premises used: Finset.Ico_eq_empty, Nat.zero_sub, Finset.card_empty, Finset.Ioo_eq_empty
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
pos : ∀ (h : a < b), #(Ioo a b) = #(Ico a b) - 1
neg neg₁ : ∀ (h : ¬a < b), #(Ioo a b) = #(Ico a b) - 1
⊢ #(Ioo a b) = #(Ico a b) - 1

Tactic:
classical
    by_cases h : a < b
    · rw [Ico_eq_cons_Ioo h, card_cons]
      exact (Nat.add_sub_cancel _ _).symm
    · rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, Nat.zero_sub]

Premises used: Nat.zero_sub, Finset.card_empty, Finset.card_cons, Nat.add_sub_cancel, Eq.symm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ #(Ioo a b) = #(Ioc a b) - 1

Tactic:
@card_Ioo_eq_card_Ico_sub_one αᵒᵈ _ _ _ _

Premises used: Finset.card_Ioo_eq_card_Ico_sub_one, OrderDual, Finset.Ioo, Finset.Ioc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
rw : #(Icc a b) - 1 - 1 = #(Icc a b) - 2
⊢ #(Ioo a b) = #(Icc a b) - 2

Tactic:
rw [card_Ioo_eq_card_Ico_sub_one, card_Ico_eq_card_Icc_sub_one]

Premises used: Finset.card_Ico_eq_card_Icc_sub_one, Finset.card_Ioo_eq_card_Ico_sub_one
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ #(Icc a b) - 1 - 1 = #(Icc a b) - 2

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
a b : α
c : β
⊢ map (Embedding.sectL α c) [[a, b]] = [[(a, c), (b, c)]]

Tactic:
aesop (add safe forward [le_antisymm])

Premises used: le_antisymm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : PartialOrder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
a b : α
c : β
⊢ map (Embedding.sectL α c) (Icc a b) = Icc (a, c) (b, c)

Tactic:
aesop (add safe forward [le_antisymm])

Premises used: le_antisymm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : PartialOrder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : DecidableLE (α × β)
a b : α
c : β
⊢ map (Embedding.sectL α c) (Ioc a b) = Ioc (a, c) (b, c)

Tactic:
aesop (add safe forward [le_antisymm, le_of_lt])

Premises used: le_of_lt, le_antisymm