awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
rw : Ici (succ a) ∩ Iio b = Ioo a b
rw₁ : Ioi a ∩ Iio b = Ioo a b
rw₂ rw₃ : Ioo a b = Ioo a b
⊢ Ico (succ a) b = Ioo a b

Tactic:
rw [← Ici_inter_Iio, Ici_succ_of_not_isMax ha, Ioi_inter_Iio]

Premises used: Order.Ici_succ_of_not_isMax, Set.Ici_inter_Iio, Set.Ioi_inter_Iio
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a : α
⊢ a < succ a

Tactic:
lt_succ_of_not_isMax <| not_isMax a

Premises used: not_isMax, Order.lt_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
⊢ a ≤ b → a < succ b

Tactic:
(lt_succ_of_le_of_not_isMax · <| not_isMax b)

Premises used: not_isMax, Order.lt_succ_of_le_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
⊢ succ a ≤ b ↔ a < b

Tactic:
succ_le_iff_of_not_isMax <| not_isMax a

Premises used: not_isMax, Order.succ_le_iff_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
hab : a < b
⊢ succ a < succ b

Tactic:
simp [hab]
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
⊢ StrictMono.{u_1, u_1} (α := α) succ

Tactic:
fun _ _ => succ_lt_succ

Premises used: StrictMono, Order.succ_lt_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a : α
⊢ a ⋖ succ a

Tactic:
covBy_succ_of_not_isMax <| not_isMax a

Premises used: not_isMax, Order.covBy_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a : α
⊢ Iic a ⊆ Iio (succ a)

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a : α
⊢ Ici (succ a) = Ioi a

Tactic:
Ici_succ_of_not_isMax <| not_isMax _

Premises used: Order.Ici_succ_of_not_isMax, not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a b : α
⊢ Icc a b ⊆ Ico a (succ b)

Tactic:
Icc_subset_Ico_succ_right_of_not_isMax <| not_isMax _

Premises used: not_isMax, Order.Icc_subset_Ico_succ_right_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a b : α
⊢ Ioc a b ⊆ Ioo a (succ b)

Tactic:
Ioc_subset_Ioo_succ_right_of_not_isMax <| not_isMax _

Premises used: not_isMax, Order.Ioc_subset_Ioo_succ_right_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a b : α
⊢ Icc (succ a) b = Ioc a b

Tactic:
Icc_succ_left_of_not_isMax <| not_isMax _

Premises used: Order.Icc_succ_left_of_not_isMax, not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a b : α
⊢ Ico (succ a) b = Ioo a b

Tactic:
Ico_succ_left_of_not_isMax <| not_isMax _

Premises used: not_isMax, Order.Ico_succ_left_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
⊢ succ a = a ↔ IsMax a

Tactic:
⟨fun h => max_of_succ_le h.le, fun h => h.eq_of_ge <| le_succ _⟩

Premises used: Order.max_of_succ_le, Eq.le, Iff.intro, Order.le_succ, IsMax.eq_of_ge
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
pos : ∀ (ha : IsMax a), a ≤ b ↔ a = b ∨ succ a ≤ b
neg : ∀ (ha : ¬IsMax a), a ≤ b ↔ a = b ∨ succ a ≤ b
⊢ a ≤ b ↔ a = b ∨ succ a ≤ b

Tactic:
by_cases ha : IsMax a

Premises used: IsMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
ha : IsMax a
⊢ a ≤ b ↔ a = b ∨ succ a ≤ b

Tactic:
simpa [ha.succ_eq] using le_of_eq

Premises used: le_of_eq, IsMax.succ_eq
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
neg : a ≤ b ↔ a = b ∨ a < b
neg₁ neg₂ : a = b ∨ a < b ↔ a = b ∨ a < b
⊢ a ≤ b ↔ a = b ∨ succ a ≤ b

Tactic:
rw [succ_le_iff_of_not_isMax ha, le_iff_eq_or_lt]

Premises used: le_iff_eq_or_lt, Order.succ_le_iff_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
rw : a ≤ b ↔ a = b ∨ succ a ≤ b
⊢ a ≤ b ↔ b = a ∨ succ a ≤ b

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
⊢ a ≤ b ↔ a = b ∨ succ a ≤ b

Tactic:
le_iff_eq_or_succ_le

Premises used: Order.le_iff_eq_or_succ_le
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
⊢ a ≤ b ↔ a = b ∨ succ a ≤ b

Tactic:
exact le_iff_eq_or_succ_le

Premises used: Order.le_iff_eq_or_succ_le
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
⊢ a ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a

Tactic:
⟨fun h ↦ or_iff_not_imp_left.2 fun hba : b ≠ a ↦
    h.2.antisymm (succ_le_of_lt <| h.1.lt_of_ne <| hba.symm), ?_⟩

Premises used: Iff.mpr, LE.le.antisymm, Order.succ_le_of_lt, Ne.symm, LE.le.lt_of_ne, And.right, And.left, Classical.or_iff_not_imp_left, Iff.intro
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
refine : b = a ∨ b = succ a → a ≤ b ∧ b ≤ succ a
⊢ a ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a

Tactic:
refine ⟨fun h ↦ or_iff_not_imp_left.2 fun hba : b ≠ a ↦
    h.2.antisymm (succ_le_of_lt <| h.1.lt_of_ne <| hba.symm), ?_⟩
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
b : α
⊢ b ≤ b ∧ b ≤ succ b

Tactic:
⟨le_rfl, le_succ b⟩

Premises used: le_rfl, And.intro, Order.le_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
b : α
⊢ b ≤ b ∧ b ≤ succ b

Tactic:
exact ⟨le_rfl, le_succ b⟩
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
⊢ a ≤ succ a ∧ succ a ≤ succ a

Tactic:
⟨le_succ a, le_rfl⟩

Premises used: le_rfl, And.intro, Order.le_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
⊢ a ≤ succ a ∧ succ a ≤ succ a

Tactic:
exact ⟨le_succ a, le_rfl⟩
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
rw : a ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a
⊢ b ≤ succ a ∧ a ≤ b ↔ b = a ∨ b = succ a

Tactic:
rw [and_comm]

Premises used: and_comm
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
⊢ a ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a

Tactic:
le_and_le_succ_iff

Premises used: Order.le_and_le_succ_iff
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
⊢ a ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a

Tactic:
exact le_and_le_succ_iff

Premises used: Order.le_and_le_succ_iff
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
h : a ⋖ b
⊢ succ a = b

Tactic:
(succ_le_of_lt h.lt).antisymm h.wcovBy.le_succ

Premises used: LE.le.antisymm, Order.succ_le_of_lt, WCovBy.le_succ, CovBy.wcovBy, CovBy.lt
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PartialOrder β
inst_3 : SuccOrder β
f : α ≃o β
a : α
pos : ∀ (h : IsMax a), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (succ a) : β) (succ ((f : (a : α) → β) a) : β)
neg : ∀ (h : ¬IsMax a), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (succ a) : β) (succ ((f : (a : α) → β) a) : β)
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (succ a) : β) (succ ((f : (a : α) → β) a) : β)

Tactic:
by_cases h : IsMax a

Premises used: IsMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PartialOrder β
inst_3 : SuccOrder β
f : α ≃o β
a : α
h : IsMax a
pos : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) (succ ((f : (a : α) → β) a) : β)
pos₁ pos₂ : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a : β)
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (succ a) : β) (succ ((f : (a : α) → β) a) : β)

Tactic:
rw [h.succ_eq, (f.isMax_apply.2 h).succ_eq]

Premises used: Iff.mpr, OrderIso.isMax_apply, IsMax.succ_eq
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PartialOrder β
inst_3 : SuccOrder β
f : α ≃o β
a : α
h : ¬IsMax a
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (succ a) : β) (succ ((f : (a : α) → β) a) : β)

Tactic:
((apply_covBy_apply_iff f).2 <| covBy_succ_of_not_isMax h).succ_eq.symm

Premises used: Iff.mpr, CovBy.succ_eq, apply_covBy_apply_iff, Eq.symm, Order.covBy_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PartialOrder β
inst_3 : SuccOrder β
f : α ≃o β
a : α
h : ¬IsMax a
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (succ a) : β) (succ ((f : (a : α) → β) a) : β)

Tactic:
exact ((apply_covBy_apply_iff f).2 <| covBy_succ_of_not_isMax h).succ_eq.symm

Premises used: Iff.mpr, CovBy.succ_eq, apply_covBy_apply_iff, Eq.symm, Order.covBy_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
inst_2 : NoMaxOrder α
⊢ a ⋖ succ a

Tactic:
covBy_succ _

Premises used: Order.covBy_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
inst_2 : NoMaxOrder α
⊢ a ⋖ succ a

Tactic:
exact covBy_succ _

Premises used: Order.covBy_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : OrderTop α
rw : IsMax.{u_1} (α := α) ⊤
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) ⊤ ⊤
⊢ Eq.{u_1 + 1} (α := α) (succ ⊤) ⊤

Tactic:
rw [succ_eq_iff_isMax, isMax_iff_eq_top]

Premises used: isMax_iff_eq_top, Order.succ_eq_iff_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
inst_2 : OrderTop α
⊢ succ a ≤ a ↔ a = ⊤

Tactic:
succ_le_iff_isMax.trans isMax_iff_eq_top

Premises used: isMax_iff_eq_top, Order.succ_le_iff_isMax, Iff.trans
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
inst_2 : OrderTop α
⊢ a < succ a ↔ a ≠ ⊤

Tactic:
lt_succ_iff_not_isMax.trans not_isMax_iff_ne_top

Premises used: Order.lt_succ_iff_not_isMax, Iff.trans, not_isMax_iff_ne_top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : OrderBot α
inst_3 : Nontrivial α
a : α
⊢ ⊥ < succ a

Tactic:
(lt_succ_of_not_isMax not_isMax_bot).trans_le <| succ_le_succ bot_le

Premises used: Order.lt_succ_of_not_isMax, LT.lt.trans_le, Order.succ_le_succ, not_isMax_bot, bot_le
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : OrderBot α
inst_3 : Nontrivial α
a : α
⊢ succ a ≠ ⊥

Tactic:
(bot_lt_succ a).ne'

Premises used: LT.lt.ne', Order.bot_lt_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
⊢ succ (max a b) = max (succ a) (succ b)

Tactic:
succ_mono.map_max

Premises used: Monotone.map_max, Order.succ_mono
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
⊢ succ (min a b) = min (succ a) (succ b)

Tactic:
succ_mono.map_min

Premises used: Order.succ_mono, Monotone.map_min
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a < succ b
by_contra! : ∀ (nh : b < a), False
⊢ a ≤ b

Tactic:
by_contra! nh
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a < succ b
nh : b < a
⊢ False

Tactic:
(h.trans_le (succ_le_of_lt nh)).false

Premises used: Order.succ_le_of_lt, LT.lt.trans_le, LT.lt.false
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a < succ b
nh : b < a
⊢ False

Tactic:
exact (h.trans_le (succ_le_of_lt nh)).false

Premises used: Order.succ_le_of_lt, LT.lt.trans_le, LT.lt.false
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ b < succ a ↔ b ≤ a

Tactic:
⟨le_of_lt_succ, fun h => h.trans_lt <| lt_succ_of_not_isMax ha⟩

Premises used: Order.lt_succ_of_not_isMax, Iff.intro, LE.le.trans_lt, Order.le_of_lt_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
rw : succ a ≤ b ↔ a < b
rw₁ rw₂ : a < b ↔ a < b
⊢ succ a < succ b ↔ a < b

Tactic:
rw [lt_succ_iff_of_not_isMax hb, succ_le_iff_of_not_isMax ha]

Premises used: Order.succ_le_iff_of_not_isMax, Order.lt_succ_iff_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
rw : a < succ b ↔ a ≤ b
rw₁ rw₂ : a ≤ b ↔ a ≤ b
⊢ succ a ≤ succ b ↔ a ≤ b

Tactic:
rw [succ_le_iff_of_not_isMax ha, lt_succ_iff_of_not_isMax hb]

Premises used: Order.succ_le_iff_of_not_isMax, Order.lt_succ_iff_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
ha : ¬IsMax a
⊢ Iio (succ a) = Iic a

Tactic:
Set.ext fun _ => lt_succ_iff_of_not_isMax ha

Premises used: Set.ext, Order.lt_succ_iff_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
rw : Ici a ∩ Iio (succ b) = Icc a b
rw₁ : Ici a ∩ Iic b = Icc a b
rw₂ rw₃ : Icc a b = Icc a b
⊢ Ico a (succ b) = Icc a b

Tactic:
rw [← Ici_inter_Iio, Iio_succ_of_not_isMax hb, Ici_inter_Iic]

Premises used: Order.Iio_succ_of_not_isMax, Set.Ici_inter_Iio, Set.Ici_inter_Iic
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
rw : Ioi a ∩ Iio (succ b) = Ioc a b
rw₁ : Ioi a ∩ Iic b = Ioc a b
rw₂ rw₃ : Ioc a b = Ioc a b
⊢ Ioo a (succ b) = Ioc a b

Tactic:
rw [← Ioi_inter_Iio, Iio_succ_of_not_isMax hb, Ioi_inter_Iic]

Premises used: Order.Iio_succ_of_not_isMax, Set.Ioi_inter_Iic, Set.Ioi_inter_Iio
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
rw : succ a ≤ succ b ∧ ¬succ a < succ b ↔ a = b
rw₁ : succ a ≤ succ b ∧ ¬succ a < succ b ↔ a ≤ b ∧ ¬a < b
rw₂ : a ≤ b ∧ ¬succ a < succ b ↔ a ≤ b ∧ ¬a < b
rw₃ rw₄ : a ≤ b ∧ ¬a < b ↔ a ≤ b ∧ ¬a < b
⊢ succ a = succ b ↔ a = b

Tactic:
rw [eq_iff_le_not_lt, eq_iff_le_not_lt, succ_le_succ_iff_of_not_isMax ha hb,
    succ_lt_succ_iff_of_not_isMax ha hb]

Premises used: Order.succ_le_succ_iff_of_not_isMax, Order.succ_lt_succ_iff_of_not_isMax, eq_iff_le_not_lt
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
pos : ∀ (hb : IsMax b), a ≤ succ b ↔ a = succ b ∨ a ≤ b
neg : ∀ (hb : ¬IsMax b), a ≤ succ b ↔ a = succ b ∨ a ≤ b
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b

Tactic:
by_cases hb : IsMax b

Premises used: IsMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
hb : IsMax b
pos : a ≤ b ↔ a = b ∨ a ≤ b
pos₁ pos₂ : a ≤ b ↔ a ≤ b
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b

Tactic:
rw [hb.succ_eq, or_iff_right_of_imp le_of_eq]

Premises used: or_iff_right_of_imp, le_of_eq, IsMax.succ_eq
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
neg : a ≤ succ b ↔ a = succ b ∨ a < succ b
neg₁ neg₂ : a = succ b ∨ a < succ b ↔ a = succ b ∨ a < succ b
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b

Tactic:
rw [← lt_succ_iff_of_not_isMax hb, le_iff_eq_or_lt]

Premises used: le_iff_eq_or_lt, Order.lt_succ_iff_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ a < succ b ↔ a = b ∨ a < b

Tactic:
(lt_succ_iff_of_not_isMax hb).trans le_iff_eq_or_lt

Premises used: le_iff_eq_or_lt, Iff.trans, Order.lt_succ_iff_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : Nontrivial α
a : α
inl : ∀ (ha : a = succ a), ¬IsMin (succ a)
inr : ∀ (ha : a < succ a), ¬IsMin (succ a)
⊢ ¬IsMin (succ a)

Tactic:
obtain ha | ha := (le_succ a).eq_or_lt

Premises used: LE.le.eq_or_lt, Order.le_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : Nontrivial α
a : α
ha : a = succ a
⊢ ¬IsMin (succ a)

Tactic:
exact (ha ▸ succ_eq_iff_isMax.1 ha.symm).not_isMin
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : Nontrivial α
a : α
ha : a < succ a
⊢ ¬IsMin (succ a)

Tactic:
not_isMin_of_lt ha

Premises used: not_isMin_of_lt
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : Nontrivial α
a : α
ha : a < succ a
⊢ ¬IsMin (succ a)

Tactic:
exact not_isMin_of_lt ha

Premises used: not_isMin_of_lt
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
⊢ Iic (succ a) = insert (succ a) (Iic a)

Tactic:
ext fun _ => le_succ_iff_eq_or_le

Premises used: Set.ext, Order.le_succ_iff_eq_or_le
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a ≤ succ b
simp_rw : Ici a ∩ Iic (succ b) = insert (succ b) (Ici a ∩ Iic b)
simp_rw₁ : Ici a ∩ insert (succ b) (Iic b) = insert (succ b) (Ici a ∩ Iic b)
⊢ Icc a (succ b) = insert (succ b) (Icc a b)

Tactic:
simp_rw [← Ici_inter_Iic, Iic_succ, inter_insert_of_mem (mem_Ici.2 h)]

Premises used: Iff.mpr, Set.inter_insert_of_mem, Set.mem_Ici, Order.Iic_succ, Set.Ici_inter_Iic
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a < succ b
simp_rw : Ioi a ∩ Iic (succ b) = insert (succ b) (Ioi a ∩ Iic b)
simp_rw₁ : Ioi a ∩ insert (succ b) (Iic b) = insert (succ b) (Ioi a ∩ Iic b)
⊢ Ioc a (succ b) = insert (succ b) (Ioc a b)

Tactic:
simp_rw [← Ioi_inter_Iic, Iic_succ, inter_insert_of_mem (mem_Ioi.2 h)]

Premises used: Iff.mpr, Set.Ioi_inter_Iic, Set.mem_Ioi, Set.inter_insert_of_mem, Order.Iic_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
h : ¬IsMax a
⊢ Iio (succ a) = insert a (Iio a)

Tactic:
ext fun _ => lt_succ_iff_eq_or_lt_of_not_isMax h

Premises used: Set.ext, Order.lt_succ_iff_eq_or_lt_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h₁ : a ≤ b
h₂ : ¬IsMax b
simp_rw : Iio (succ b) ∩ Ici a = insert b (Iio b ∩ Ici a)
simp_rw₁ : insert b (Iio b) ∩ Ici a = insert b (Iio b ∩ Ici a)
⊢ Ico a (succ b) = insert b (Ico a b)

Tactic:
simp_rw [← Iio_inter_Ici, Iio_succ_eq_insert_of_not_isMax h₂, insert_inter_of_mem (mem_Ici.2 h₁)]

Premises used: Iff.mpr, Order.Iio_succ_eq_insert_of_not_isMax, Set.insert_inter_of_mem, Set.mem_Ici, Set.Iio_inter_Ici
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h₁ : a < b
h₂ : ¬IsMax b
simp_rw : Iio (succ b) ∩ Ioi a = insert b (Iio b ∩ Ioi a)
simp_rw₁ : insert b (Iio b) ∩ Ioi a = insert b (Iio b ∩ Ioi a)
⊢ Ioo a (succ b) = insert b (Ioo a b)

Tactic:
simp_rw [← Iio_inter_Ioi, Iio_succ_eq_insert_of_not_isMax h₂, insert_inter_of_mem (mem_Ioi.2 h₁)]

Premises used: Iff.mpr, Order.Iio_succ_eq_insert_of_not_isMax, Set.mem_Ioi, Set.insert_inter_of_mem, Set.Iio_inter_Ioi
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
⊢ a < succ b ↔ a ≤ b

Tactic:
lt_succ_iff_of_not_isMax <| not_isMax b

Premises used: not_isMax, Order.lt_succ_iff_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
⊢ succ a ≤ succ b ↔ a ≤ b

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
⊢ succ a < succ b ↔ a < b

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a : α
⊢ Iio (succ a) = Iic a

Tactic:
Iio_succ_of_not_isMax <| not_isMax _

Premises used: Order.Iio_succ_of_not_isMax, not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a b : α
⊢ Ico a (succ b) = Icc a b

Tactic:
Ico_succ_right_of_not_isMax <| not_isMax _

Premises used: Order.Ico_succ_right_of_not_isMax, not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a b : α
⊢ Ioo a (succ b) = Ioc a b

Tactic:
Ioo_succ_right_of_not_isMax <| not_isMax _

Premises used: not_isMax, Order.Ioo_succ_right_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
⊢ succ a = succ b ↔ a = b

Tactic:
succ_eq_succ_iff_of_not_isMax (not_isMax a) (not_isMax b)

Premises used: not_isMax, Order.succ_eq_succ_iff_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
⊢ Injective.{u_1 + 1, u_1 + 1} (α := α) succ

Tactic:
fun _ _ => succ_eq_succ_iff.1

Premises used: Order.succ_eq_succ_iff, Iff.mp, Function.Injective
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
⊢ succ a ≠ succ b ↔ a ≠ b

Tactic:
succ_injective.ne_iff

Premises used: Function.Injective.ne_iff, Order.succ_injective
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
⊢ a < succ b ↔ a = b ∨ a < b

Tactic:
lt_succ_iff.trans le_iff_eq_or_lt

Premises used: le_iff_eq_or_lt, Order.lt_succ_iff, Iff.trans
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
rw : a < succ b ↔ a = b ∨ a < b
rw₁ rw₂ : a = b ∨ a < b ↔ a = b ∨ a < b
⊢ a < succ b ↔ b = a ∨ a < b

Tactic:
rw [eq_comm, lt_succ_iff_eq_or_lt]

Premises used: Order.lt_succ_iff_eq_or_lt, eq_comm
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a : α
⊢ Iio (succ a) = insert a (Iio a)

Tactic:
Iio_succ_eq_insert_of_not_isMax <| not_isMax a

Premises used: Order.Iio_succ_eq_insert_of_not_isMax, not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
h : a ≤ b
⊢ Ico a (succ b) = insert b (Ico a b)

Tactic:
Ico_succ_right_eq_insert_of_not_isMax h <| not_isMax b

Premises used: not_isMax, Order.Ico_succ_right_eq_insert_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
h : a < b
⊢ Ioo a (succ b) = insert b (Ioo a b)

Tactic:
Ioo_succ_right_eq_insert_of_not_isMax h <| not_isMax b

Premises used: not_isMax, Order.Ioo_succ_right_eq_insert_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
⊢ Ioo a b = ∅ ↔ b ≤ succ a

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
refine_1 : ∀ (h : Ioo a b = ∅), b ≤ succ a
refine_2 : ∀ (h : b ≤ succ a), Ioo a b = ∅
⊢ Ioo a b = ∅ ↔ b ≤ succ a

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩