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

State before:
m : ℕ
bm : Bool
n : ℕ
bn : Bool
hmn : (m + bif bm then 1 else 0) < n + bif bn then 1 else 0
hnm : (n + bif bn then 0 else 1) < m + bif bm then 0 else 1
⊢ bm = false ∧ bn = true ∧ m = n
Tactic:
refine Order.eq_false_true_of_cond_succ_lt_of_cond_succ_lt ?_ ?_
State after:
case refine_1
m : ℕ
bm : Bool
n : ℕ
bn : Bool
hmn : (m + bif bm then 1 else 0) < n + bif bn then 1 else 0
hnm : (n + bif bn then 0 else 1) < m + bif bm then 0 else 1
⊢ (bif bm then Order.succ else id) m < (bif bn then Order.succ else id) n

case refine_2
m : ℕ
bm : Bool
n : ℕ
bn : Bool
hmn : (m + bif bm then 1 else 0) < n + bif bn then 1 else 0
hnm : (n + bif bn then 0 else 1) < m + bif bm then 0 else 1
⊢ (bif bn then id else Order.succ) n < (bif bm then id else Order.succ) m

State before:
case refine_1
m : ℕ
bm : Bool
n : ℕ
bn : Bool
hmn : (m + bif bm then 1 else 0) < n + bif bn then 1 else 0
hnm : (n + bif bn then 0 else 1) < m + bif bm then 0 else 1
⊢ (bif bm then Order.succ else id) m < (bif bn then Order.succ else id) n
Tactic:
cases bm <;> cases bn <;>
simp only [succ_eq_succ, cond_true, cond_false, id_eq] at hnm hmn ⊢ <;> exact hmn
State after:
no goals

State before:
case refine_2
m : ℕ
bm : Bool
n : ℕ
bn : Bool
hmn : (m + bif bm then 1 else 0) < n + bif bn then 1 else 0
hnm : (n + bif bn then 0 else 1) < m + bif bm then 0 else 1
⊢ (bif bn then id else Order.succ) n < (bif bm then id else Order.succ) m
Tactic:
cases bm <;> cases bn <;>
simp only [succ_eq_succ, cond_true, cond_false, id_eq] at hnm hmn ⊢ <;> exact hnm
State after:
no goals