Theorem: Order.eq_false_true_of_cond_succ_lt_of_cond_succ_lt (Controlbits/Order.lean)

State before:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
bm bn : Bool
hmn : (bif bm then succ else id) m < (bif bn then succ else id) n
hnm : (bif bn then id else succ) n < (bif bm then id else succ) m
⊢ bm = false ∧ bn = true ∧ m = n
Tactic:
cases bm <;> cases bn <;>
simp only [false_and, and_false, true_and, and_self, cond_true, cond_false, id_eq,
succ_le_iff, succ_lt_succ_iff, lt_succ_iff] at *
State after:
case false.false
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
hmn : m < n
hnm : n < m
⊢ False

case false.true
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
hmn : m ≤ n
hnm : n ≤ m
⊢ m = n

case true.false
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
hmn : succ m < n
hnm : succ n < m
⊢ False

case true.true
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
hnm : n < m
hmn : m < n
⊢ False

State before:
case false.false
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
hmn : m < n
hnm : n < m
⊢ False
Tactic:
exact hmn.not_lt hnm
State after:
no goals

State before:
case false.true
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
hmn : m ≤ n
hnm : n ≤ m
⊢ m = n
Tactic:
exact le_antisymm hmn hnm
State after:
no goals

State before:
case true.false
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
hmn : succ m < n
hnm : succ n < m
⊢ False
Tactic:
exact lt_irrefl _ (((hnm.trans (lt_succ _)).trans hmn).trans (lt_succ _))
State after:
no goals

State before:
case true.true
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
hnm : n < m
hmn : m < n
⊢ False
Tactic:
exact hmn.not_lt hnm
State after:
no goals