awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
inst_3 : NoMaxOrder α
a b : α
⊢ (↑(Icc (succ a) b) : Set α) = (↑(Ioc a b) : Set α)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
inst_3 : NoMaxOrder α
a b : α
⊢ (↑(Ico a (succ b)) : Set α) = (↑(Icc a b) : Set α)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
inst_3 : NoMaxOrder α
a b : α
⊢ (↑(Ioo a (succ b)) : Set α) = (↑(Ioc a b) : Set α)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
inst_3 : NoMaxOrder α
a b : α
⊢ (↑(Ico (succ a) (succ b)) : Set α) = (↑(Ioc a b) : Set α)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
a b : α
inst_3 : NoMaxOrder α
h : a ≤ b
⊢ (↑(insert b (Ico a b)) : Set α) = (↑(Ico a (succ b)) : Set α)

Tactic:
simpa using Set.insert_Ico_right_eq_Ico_succ h

Premises used: Set.insert_Ico_right_eq_Ico_succ
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
a b : α
inst_3 : NoMaxOrder α
h : a ≤ b
⊢ (↑(insert (succ b) (Ioc a b)) : Set α) = (↑(Ioc a (succ b)) : Set α)

Tactic:
simpa using Set.insert_Ioc_right_eq_Ioc_succ h

Premises used: Set.insert_Ioc_right_eq_Ioc_succ
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : PredOrder α
a b : α
⊢ (↑(Ioc a (pred b)) : Set α) = (↑(Ioo a b) : Set α)

Tactic:
simpa using Set.Ioc_pred_right_eq_Ioo _ _

Premises used: Set.Ioc_pred_right_eq_Ioo
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : PredOrder α
b : α
hb : ¬IsMin b
a : α
⊢ (↑(Icc a (pred b)) : Set α) = (↑(Ico a b) : Set α)

Tactic:
simpa using Set.Icc_pred_right_eq_Ico_of_not_isMin hb _

Premises used: Set.Icc_pred_right_eq_Ico_of_not_isMin
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ (↑(Ioc (pred a) b) : Set α) = (↑(Icc a b) : Set α)

Tactic:
simpa using Set.Ioc_pred_left_eq_Icc_of_not_isMin ha _

Premises used: Set.Ioc_pred_left_eq_Icc_of_not_isMin
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ (↑(Ioo (pred a) b) : Set α) = (↑(Ico a b) : Set α)

Tactic:
simpa using Set.Ioo_pred_left_eq_Ioc_of_not_isMin ha _

Premises used: Set.Ioo_pred_left_eq_Ioc_of_not_isMin
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ (↑(Ioc (pred a) (pred b)) : Set α) = (↑(Ico a b) : Set α)

Tactic:
simpa using Set.Ioc_pred_pred_eq_Ico_of_not_isMin ha _

Premises used: Set.Ioc_pred_pred_eq_Ico_of_not_isMin
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : PredOrder α
a b : α
h : a ≤ b
⊢ (↑(insert b (Icc a (pred b))) : Set α) = (↑(Icc a b) : Set α)

Tactic:
simpa using Set.insert_Icc_pred_right_eq_Icc h

Premises used: Set.insert_Icc_pred_right_eq_Icc
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : PredOrder α
a b : α
h : pred a ≤ b
⊢ (↑(insert (pred a) (Icc a b)) : Set α) = (↑(Icc (pred a) b) : Set α)

Tactic:
simpa using Set.insert_Icc_left_eq_Icc_pred h

Premises used: Set.insert_Icc_left_eq_Icc_pred
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ (↑(insert a (Ioc a b)) : Set α) = (↑(Ioc (pred a) b) : Set α)

Tactic:
simpa using Set.insert_Ioc_left_eq_Ioc_pred_of_not_isMin h ha

Premises used: Set.insert_Ioc_left_eq_Ioc_pred_of_not_isMin
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : PredOrder α
a b : α
h : a < b
⊢ (↑(insert b (Ioc a (pred b))) : Set α) = (↑(Ioc a b) : Set α)

Tactic:
simpa using Set.insert_Ioc_pred_right_eq_Ioc h

Premises used: Set.insert_Ioc_pred_right_eq_Ioc
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ (↑(insert (pred a) (Ico a b)) : Set α) = (↑(Ico (pred a) b) : Set α)

Tactic:
simpa using Set.insert_Ico_left_eq_Ico_pred_of_not_isMin h ha

Premises used: Set.insert_Ico_left_eq_Ico_pred_of_not_isMin
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : PredOrder α
a b : α
h : a < b
⊢ (↑(insert (pred b) (Ico a (pred b))) : Set α) = (↑(Ico a b) : Set α)

Tactic:
simpa using Set.insert_Ico_pred_right_eq_Ico h

Premises used: Set.insert_Ico_pred_right_eq_Ico
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : PredOrder α
inst_3 : NoMinOrder α
a b : α
⊢ (↑(Icc a (pred b)) : Set α) = (↑(Ico a b) : Set α)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : PredOrder α
inst_3 : NoMinOrder α
a b : α
⊢ (↑(Ioc (pred a) b) : Set α) = (↑(Icc a b) : Set α)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : PredOrder α
inst_3 : NoMinOrder α
a b : α
⊢ (↑(Ioo (pred a) b) : Set α) = (↑(Ico a b) : Set α)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : PredOrder α
inst_3 : NoMinOrder α
a b : α
⊢ (↑(Ioc (pred a) (pred b)) : Set α) = (↑(Ico a b) : Set α)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : PredOrder α
a b : α
inst_3 : NoMinOrder α
h : a ≤ b
⊢ (↑(insert a (Ioc a b)) : Set α) = (↑(Ioc (pred a) b) : Set α)

Tactic:
simpa using Set.insert_Ioc_left_eq_Ioc_pred h

Premises used: Set.insert_Ioc_left_eq_Ioc_pred
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : PredOrder α
a b : α
inst_3 : NoMinOrder α
h : a ≤ b
⊢ insert (pred a) (Ico a b) = Ico (pred a) b

Tactic:
insert_Ico_left_eq_Ico_pred_of_not_isMin h (not_isMin _)

Premises used: not_isMin, Finset.insert_Ico_left_eq_Ico_pred_of_not_isMin
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
inst_3 : PredOrder α
inst_4 : Nontrivial α
a b : α
⊢ (↑(Icc (succ a) (pred b)) : Set α) = (↑(Ioo a b) : Set α)

Tactic:
simpa using Set.Icc_succ_pred_eq_Ioo _ _

Premises used: Set.Icc_succ_pred_eq_Ioo
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : SuccOrder α
b : α
hb : ¬IsMax b
⊢ (↑(Iio (succ b)) : Set α) = (↑(Iic b) : Set α)

Tactic:
simpa using Set.Iio_succ_eq_Iic_of_not_isMax hb

Premises used: Set.Iio_succ_eq_Iic_of_not_isMax
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : SuccOrder α
inst_3 : NoMaxOrder α
b : α
⊢ (↑(Iio (succ b)) : Set α) = (↑(Iic b) : Set α)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : PredOrder α
b : α
hb : ¬IsMin b
⊢ (↑(Iic (pred b)) : Set α) = (↑(Iio b) : Set α)

Tactic:
simpa using Set.Iic_pred_eq_Iio_of_not_isMin hb

Premises used: Set.Iic_pred_eq_Iio_of_not_isMin
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : PredOrder α
inst_3 : NoMinOrder α
b : α
⊢ (↑(Iic (pred b)) : Set α) = (↑(Iio b) : Set α)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : SuccOrder α
a : α
ha : ¬IsMax a
⊢ (↑(Ici (succ a)) : Set α) = (↑(Ioi a) : Set α)

Tactic:
simpa using Set.Ici_succ_eq_Ioi_of_not_isMax ha

Premises used: Set.Ici_succ_eq_Ioi_of_not_isMax
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : SuccOrder α
inst_3 : NoMaxOrder α
a : α
⊢ (↑(Ici (succ a)) : Set α) = (↑(Ioi a) : Set α)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : PredOrder α
a : α
ha : ¬IsMin a
⊢ (↑(Ioi (pred a)) : Set α) = (↑(Ici a) : Set α)

Tactic:
simpa using Set.Ioi_pred_eq_Ici_of_not_isMin ha

Premises used: Set.Ioi_pred_eq_Ici_of_not_isMin
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : PredOrder α
inst_3 : NoMinOrder α
a : α
⊢ (↑(Ioi (pred a)) : Set α) = (↑(Ici a) : Set α)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Lex
Goal:
α : Type u_1
inst : LT α
inst_1 : LE α
x y : NonemptyInterval α
⊢ LE.le (α := Lex (NonemptyInterval α))
      ((toLex : (a : NonemptyInterval α) → Lex (NonemptyInterval α)) x : Lex (NonemptyInterval α))
      ((toLex : (a : NonemptyInterval α) → Lex (NonemptyInterval α)) y : Lex (NonemptyInterval α)) ↔
    y.toProd.1 < x.toProd.1 ∨ x.toProd.1 = y.toProd.1 ∧ x.toProd.2 ≤ y.toProd.2

Tactic:
Prod.lex_def

Premises used: Prod.lex_def, OrderDual
-- Module: Mathlib.Order.Interval.Lex
Goal:
α : Type u_1
inst : LT α
inst_1 : LE α
x y : NonemptyInterval α
⊢ LT.lt (α := Lex (NonemptyInterval α))
      ((toLex : (a : NonemptyInterval α) → Lex (NonemptyInterval α)) x : Lex (NonemptyInterval α))
      ((toLex : (a : NonemptyInterval α) → Lex (NonemptyInterval α)) y : Lex (NonemptyInterval α)) ↔
    y.toProd.1 < x.toProd.1 ∨ x.toProd.1 = y.toProd.1 ∧ x.toProd.2 < y.toProd.2

Tactic:
Prod.lex_def

Premises used: Prod.lex_def, OrderDual
-- Module: Mathlib.Order.Interval.Lex
Goal:
α : Type ?u.3256
inst : LT α
inst_1 : LE α
⊢ LE.le (α := ℕ) (1, 1).1 (1, 1).2

Tactic:
grind
-- Module: Mathlib.Order.Interval.Lex
Goal:
α : Type ?u.3256
inst : LT α
inst_1 : LE α
⊢ LE.le (α := ℕ) (1, 2).1 (1, 2).2

Tactic:
grind
-- Module: Mathlib.Order.Interval.Lex
Goal:
α : Type ?u.3256
inst : LT α
inst_1 : LE α
⊢ LE.le (α := ℕ) (1, 3).1 (1, 3).2

Tactic:
grind
-- Module: Mathlib.Order.Interval.Lex
Goal:
α : Type ?u.3256
inst : LT α
inst_1 : LE α
⊢ LE.le (α := ℕ) (2, 2).1 (2, 2).2

Tactic:
grind
-- Module: Mathlib.Order.Interval.Lex
Goal:
α : Type ?u.3256
inst : LT α
inst_1 : LE α
⊢ LE.le (α := ℕ) (2, 3).1 (2, 3).2

Tactic:
grind
-- Module: Mathlib.Order.Interval.Lex
Goal:
α : Type ?u.3256
inst : LT α
inst_1 : LE α
⊢ LE.le (α := ℕ) (3, 3).1 (3, 3).2

Tactic:
grind
-- Module: Mathlib.Order.Interval.Lex
Goal:
α : Type u_1
inst : PartialOrder α
⊢ Monotone.{u_1, u_1} (α := NonemptyInterval α) (β := Lex (NonemptyInterval α))
    (⇑toLex : (a : NonemptyInterval α) → Lex (NonemptyInterval α))

Tactic:
Prod.Lex.toLex_mono.comp toDualProd_mono

Premises used: NonemptyInterval.toDualProd_mono, NonemptyInterval.toDualProd, Monotone, Monotone.comp, Prod.Lex.toLex_mono
-- Module: Mathlib.Order.Interval.Lex
Goal:
α : Type u_1
inst : PartialOrder α
⊢ StrictMono.{u_1, u_1} (α := NonemptyInterval α) (β := Lex (NonemptyInterval α))
    (⇑toLex : (a : NonemptyInterval α) → Lex (NonemptyInterval α))

Tactic:
Prod.Lex.toLex_strictMono.comp toDualProd_strictMono

Premises used: NonemptyInterval.toDualProd, StrictMono, NonemptyInterval.toDualProd_strictMono, Prod.Lex.toLex_strictMono, StrictMono.comp
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
rw : x ∈ (Finset.Icc a b).val ↔ a ≤ x ∧ x ≤ b
rw₁ : x ∈ Finset.Icc a b ↔ a ≤ x ∧ x ≤ b
rw₂ rw₃ : a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
⊢ x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b

Tactic:
rw [Icc, ← Finset.mem_def, Finset.mem_Icc]

Premises used: Multiset.Icc, Finset.mem_Icc, Finset.mem_def
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
rw : x ∈ (Finset.Ico a b).val ↔ a ≤ x ∧ x < b
rw₁ : x ∈ Finset.Ico a b ↔ a ≤ x ∧ x < b
rw₂ rw₃ : a ≤ x ∧ x < b ↔ a ≤ x ∧ x < b
⊢ x ∈ Ico a b ↔ a ≤ x ∧ x < b

Tactic:
rw [Ico, ← Finset.mem_def, Finset.mem_Ico]

Premises used: Multiset.Ico, Finset.mem_def, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
rw : x ∈ (Finset.Ioc a b).val ↔ a < x ∧ x ≤ b
rw₁ : x ∈ Finset.Ioc a b ↔ a < x ∧ x ≤ b
rw₂ rw₃ : a < x ∧ x ≤ b ↔ a < x ∧ x ≤ b
⊢ x ∈ Ioc a b ↔ a < x ∧ x ≤ b

Tactic:
rw [Ioc, ← Finset.mem_def, Finset.mem_Ioc]

Premises used: Finset.mem_Ioc, Multiset.Ioc, Finset.mem_def
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
rw : x ∈ (Finset.Ioo a b).val ↔ a < x ∧ x < b
rw₁ : x ∈ Finset.Ioo a b ↔ a < x ∧ x < b
rw₂ rw₃ : a < x ∧ x < b ↔ a < x ∧ x < b
⊢ x ∈ Ioo a b ↔ a < x ∧ x < b

Tactic:
rw [Ioo, ← Finset.mem_def, Finset.mem_Ioo]

Premises used: Finset.mem_Ioo, Multiset.Ioo, Finset.mem_def
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a x : α
rw : x ∈ (Finset.Ici a).val ↔ a ≤ x
rw₁ : x ∈ Finset.Ici a ↔ a ≤ x
rw₂ rw₃ : a ≤ x ↔ a ≤ x
⊢ x ∈ Ici a ↔ a ≤ x

Tactic:
rw [Ici, ← Finset.mem_def, Finset.mem_Ici]

Premises used: Finset.mem_Ici, Multiset.Ici, Finset.mem_def
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a x : α
rw : x ∈ (Finset.Ioi a).val ↔ a < x
rw₁ : x ∈ Finset.Ioi a ↔ a < x
rw₂ rw₃ : a < x ↔ a < x
⊢ x ∈ Ioi a ↔ a < x

Tactic:
rw [Ioi, ← Finset.mem_def, Finset.mem_Ioi]

Premises used: Finset.mem_Ioi, Multiset.Ioi, Finset.mem_def
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
b x : α
rw : x ∈ (Finset.Iic b).val ↔ x ≤ b
rw₁ : x ∈ Finset.Iic b ↔ x ≤ b
rw₂ rw₃ : x ≤ b ↔ x ≤ b
⊢ x ∈ Iic b ↔ x ≤ b

Tactic:
rw [Iic, ← Finset.mem_def, Finset.mem_Iic]

Premises used: Multiset.Iic, Finset.mem_Iic, Finset.mem_def
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
b x : α
rw : x ∈ (Finset.Iio b).val ↔ x < b
rw₁ : x ∈ Finset.Iio b ↔ x < b
rw₂ rw₃ : x < b ↔ x < b
⊢ x ∈ Iio b ↔ x < b

Tactic:
rw [Iio, ← Finset.mem_def, Finset.mem_Iio]

Premises used: Multiset.Iio, Finset.mem_Iio, Finset.mem_def
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ (Icc a b).Nodup

Tactic:
Finset.nodup _

Premises used: Multiset.Icc, Finset.nodup
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ (Ico a b).Nodup

Tactic:
Finset.nodup _

Premises used: Finset.nodup, Multiset.Ico
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ (Ioc a b).Nodup

Tactic:
Finset.nodup _

Premises used: Finset.nodup, Multiset.Ioc
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ (Ioo a b).Nodup

Tactic:
Finset.nodup _

Premises used: Finset.nodup, Multiset.Ioo
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
rw : (Finset.Icc a b).val = 0 ↔ ¬a ≤ b
rw₁ : Finset.Icc a b = ∅ ↔ ¬a ≤ b
rw₂ rw₃ : ¬a ≤ b ↔ ¬a ≤ b
⊢ Icc a b = 0 ↔ ¬a ≤ b

Tactic:
rw [Icc, Finset.val_eq_zero, Finset.Icc_eq_empty_iff]

Premises used: Multiset.Icc, Finset.val_eq_zero, Finset.Icc_eq_empty_iff
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
rw : (Finset.Ico a b).val = 0 ↔ ¬a < b
rw₁ : Finset.Ico a b = ∅ ↔ ¬a < b
rw₂ rw₃ : ¬a < b ↔ ¬a < b
⊢ Ico a b = 0 ↔ ¬a < b

Tactic:
rw [Ico, Finset.val_eq_zero, Finset.Ico_eq_empty_iff]

Premises used: Finset.val_eq_zero, Multiset.Ico, Finset.Ico_eq_empty_iff
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
rw : (Finset.Ioc a b).val = 0 ↔ ¬a < b
rw₁ : Finset.Ioc a b = ∅ ↔ ¬a < b
rw₂ rw₃ : ¬a < b ↔ ¬a < b
⊢ Ioc a b = 0 ↔ ¬a < b

Tactic:
rw [Ioc, Finset.val_eq_zero, Finset.Ioc_eq_empty_iff]

Premises used: Finset.val_eq_zero, Finset.Ioc_eq_empty_iff, Multiset.Ioc
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DenselyOrdered α
rw : (Finset.Ioo a b).val = 0 ↔ ¬a < b
rw₁ : Finset.Ioo a b = ∅ ↔ ¬a < b
rw₂ rw₃ : ¬a < b ↔ ¬a < b
⊢ Ioo a b = 0 ↔ ¬a < b

Tactic:
rw [Ioo, Finset.val_eq_zero, Finset.Ioo_eq_empty_iff]

Premises used: Finset.val_eq_zero, Multiset.Ioo, Finset.Ioo_eq_empty_iff
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
h : ¬a < b
⊢ Ioo a b = 0

Tactic:
eq_zero_iff_forall_notMem.2 fun _x hx => h ((mem_Ioo.1 hx).1.trans (mem_Ioo.1 hx).2)

Premises used: Iff.mpr, Multiset.eq_zero_iff_forall_notMem, And.right, And.left, Multiset.mem_Ioo, Iff.mp, LT.lt.trans
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
h : b < a
⊢ Icc a b = 0

Tactic:
Icc_eq_zero h.not_ge

Premises used: LT.lt.not_ge, Multiset.Icc_eq_zero
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
h : b ≤ a
⊢ Ico a b = 0

Tactic:
Ico_eq_zero h.not_gt

Premises used: Multiset.Ico_eq_zero, LE.le.not_gt
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
h : b ≤ a
⊢ Ioc a b = 0

Tactic:
Ioc_eq_zero h.not_gt

Premises used: Multiset.Ioc_eq_zero, LE.le.not_gt
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
h : b ≤ a
⊢ Ioo a b = 0

Tactic:
Ioo_eq_zero h.not_gt

Premises used: LE.le.not_gt, Multiset.Ioo_eq_zero
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a : α
rw : (Finset.Ico a a).val = 0
rw₁ : Eq.{u_1 + 1} (α := Multiset α) (Finset.val ∅) 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := Multiset α) 0 0
⊢ Ico a a = 0

Tactic:
rw [Ico, Finset.Ico_self, Finset.empty_val]

Premises used: Finset.Ico_self, Multiset.Ico, Finset.empty_val
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a : α
rw : (Finset.Ioc a a).val = 0
rw₁ : Eq.{u_1 + 1} (α := Multiset α) (Finset.val ∅) 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := Multiset α) 0 0
⊢ Ioc a a = 0

Tactic:
rw [Ioc, Finset.Ioc_self, Finset.empty_val]

Premises used: Finset.Ioc_self, Finset.empty_val, Multiset.Ioc
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a : α
rw : (Finset.Ioo a a).val = 0
rw₁ : Eq.{u_1 + 1} (α := Multiset α) (Finset.val ∅) 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := Multiset α) 0 0
⊢ Ioo a a = 0

Tactic:
rw [Ioo, Finset.Ioo_self, Finset.empty_val]

Premises used: Finset.Ioo_self, Multiset.Ioo, Finset.empty_val
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ a ∈ Icc a b ↔ a ≤ b

Tactic:
Finset.left_mem_Icc

Premises used: Finset.left_mem_Icc, Multiset.Icc, Set.Mem, setOf, Multiset.Mem
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ a ∈ Ico a b ↔ a < b

Tactic:
Finset.left_mem_Ico

Premises used: Set.Mem, setOf, Multiset.Mem, Multiset.Ico, Finset.left_mem_Ico
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ b ∈ Icc a b ↔ a ≤ b

Tactic:
Finset.right_mem_Icc

Premises used: Multiset.Icc, Set.Mem, setOf, Multiset.Mem, Finset.right_mem_Icc
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ b ∈ Ioc a b ↔ a < b

Tactic:
Finset.right_mem_Ioc

Premises used: Finset.right_mem_Ioc, Set.Mem, setOf, Multiset.Mem, Multiset.Ioc
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ a ∉ Ioc a b

Tactic:
Finset.left_notMem_Ioc

Premises used: Set.Mem, setOf, Multiset.Mem, Finset.left_notMem_Ioc, Multiset.Ioc
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ a ∉ Ioo a b

Tactic:
Finset.left_notMem_Ioo

Premises used: Finset.left_notMem_Ioo, Set.Mem, setOf, Multiset.Ioo, Multiset.Mem
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ b ∉ Ico a b

Tactic:
Finset.right_notMem_Ico

Premises used: Set.Mem, setOf, Multiset.Mem, Multiset.Ico, Finset.right_notMem_Ico
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ b ∉ Ioo a b

Tactic:
Finset.right_notMem_Ioo

Premises used: Finset.right_notMem_Ioo, Set.Mem, setOf, Multiset.Ioo, Multiset.Mem
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ x < c
hca : c ≤ a
rw : Eq.{u_1 + 1} (α := Multiset α) (Finset.val ∅) ∅
⊢ filter (fun (x : α) ↦ x < c) (Ico a b) = ∅

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_left hca]

Premises used: Multiset.Ico, Finset.filter_val, Finset.Ico_filter_lt_of_le_left
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ x < c
hca : c ≤ a
⊢ Eq.{u_1 + 1} (α := Multiset α) (Finset.val ∅) ∅

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ x < c
hbc : b ≤ c
rw : filter (fun (x : α) ↦ x < c) (Finset.Ico a b).val = (Finset.Ico a b).val
rw₁ : {x ∈ Finset.Ico a b | x < c}.val = (Finset.Ico a b).val
rw₂ rw₃ : (Finset.Ico a b).val = (Finset.Ico a b).val
⊢ filter (fun (x : α) ↦ x < c) (Ico a b) = Ico a b

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_right_le hbc]

Premises used: Finset.Ico_filter_lt_of_right_le, Multiset.Ico, Finset.filter_val
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ x < c
hcb : c ≤ b
rw : (Finset.Ico a c).val = Ico a c
⊢ filter (fun (x : α) ↦ x < c) (Ico a b) = Ico a c

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_right hcb]

Premises used: Finset.Ico_filter_lt_of_le_right, Multiset.Ico, Finset.filter_val
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ x < c
hcb : c ≤ b
⊢ (Finset.Ico a c).val = Ico a c

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ c ≤ x
hca : c ≤ a
rw : filter (fun (x : α) ↦ c ≤ x) (Finset.Ico a b).val = (Finset.Ico a b).val
rw₁ : {x ∈ Finset.Ico a b | c ≤ x}.val = (Finset.Ico a b).val
rw₂ rw₃ : (Finset.Ico a b).val = (Finset.Ico a b).val
⊢ filter (fun (x : α) ↦ c ≤ x) (Ico a b) = Ico a b

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_le_left hca]

Premises used: Finset.Ico_filter_le_of_le_left, Multiset.Ico, Finset.filter_val