Theorem: getRes_zero_eq_and_getBit_zero_opp_of_lt_of_flipBit_gt (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
r q : BV (a✝ + 1)
h : r < q
hf : (flipBit 0) q < (flipBit 0) r
⊢ getBit 0 r = false ∧ getBit 0 q = true ∧ getRes 0 r = getRes 0 q
Tactic:
rcases mergeBitRes_surj 0 q with ⟨bq, pq, rfl⟩
State after:
case intro.intro
a✝ : ℕ
r : BV (a✝ + 1)
bq : Bool
pq : BV a✝
h : r < mergeBitRes 0 bq pq
hf : (flipBit 0) (mergeBitRes 0 bq pq) < (flipBit 0) r
⊢ getBit 0 r = false ∧ getBit 0 (mergeBitRes 0 bq pq) = true ∧ getRes 0 r = getRes 0 (mergeBitRes 0 bq pq)

State before:
case intro.intro
a✝ : ℕ
r : BV (a✝ + 1)
bq : Bool
pq : BV a✝
h : r < mergeBitRes 0 bq pq
hf : (flipBit 0) (mergeBitRes 0 bq pq) < (flipBit 0) r
⊢ getBit 0 r = false ∧ getBit 0 (mergeBitRes 0 bq pq) = true ∧ getRes 0 r = getRes 0 (mergeBitRes 0 bq pq)
Tactic:
rcases mergeBitRes_surj 0 r with ⟨br, pr, rfl⟩
State after:
case intro.intro.intro.intro
a✝ : ℕ
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
h : mergeBitRes 0 br pr < mergeBitRes 0 bq pq
hf : (flipBit 0) (mergeBitRes 0 bq pq) < (flipBit 0) (mergeBitRes 0 br pr)
⊢ getBit 0 (mergeBitRes 0 br pr) = false ∧
    getBit 0 (mergeBitRes 0 bq pq) = true ∧ getRes 0 (mergeBitRes 0 br pr) = getRes 0 (mergeBitRes 0 bq pq)

State before:
case intro.intro.intro.intro
a✝ : ℕ
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
h : mergeBitRes 0 br pr < mergeBitRes 0 bq pq
hf : (flipBit 0) (mergeBitRes 0 bq pq) < (flipBit 0) (mergeBitRes 0 br pr)
⊢ getBit 0 (mergeBitRes 0 br pr) = false ∧
    getBit 0 (mergeBitRes 0 bq pq) = true ∧ getRes 0 (mergeBitRes 0 br pr) = getRes 0 (mergeBitRes 0 bq pq)
Tactic:
simp_rw [flipBit_mergeBitRes, getBit_mergeBitRes, getRes_mergeBitRes,
  Fin.lt_iff_val_lt_val, mergeBitRes_zero, finProdFinEquiv_apply_val, Bool.cond_not, add_comm,
  Bool.apply_cond (Fin.val), Fin.val_one, Fin.val_zero] at hf h ⊢
State after:
case intro.intro.intro.intro
a✝ : ℕ
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
hf : (2 * ↑pq + bif bq then 0 else 1) < 2 * ↑pr + bif br then 0 else 1
h : (2 * ↑pr + bif br then 1 else 0) < 2 * ↑pq + bif bq then 1 else 0
⊢ br = false ∧ bq = true ∧ pr = pq

State before:
case intro.intro.intro.intro
a✝ : ℕ
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
hf : (2 * ↑pq + bif bq then 0 else 1) < 2 * ↑pr + bif br then 0 else 1
h : (2 * ↑pr + bif br then 1 else 0) < 2 * ↑pq + bif bq then 1 else 0
⊢ br = false ∧ bq = true ∧ pr = pq
Tactic:
rcases Nat.eq_false_true_of_cond_succ_lt_of_cond_succ_lt h hf with ⟨hr, hq, he⟩
State after:
case intro.intro.intro.intro.intro.intro
a✝ : ℕ
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
hf : (2 * ↑pq + bif bq then 0 else 1) < 2 * ↑pr + bif br then 0 else 1
h : (2 * ↑pr + bif br then 1 else 0) < 2 * ↑pq + bif bq then 1 else 0
hr : br = false
hq : bq = true
he : 2 * ↑pr = 2 * ↑pq
⊢ br = false ∧ bq = true ∧ pr = pq

State before:
case intro.intro.intro.intro.intro.intro
a✝ : ℕ
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
hf : (2 * ↑pq + bif bq then 0 else 1) < 2 * ↑pr + bif br then 0 else 1
h : (2 * ↑pr + bif br then 1 else 0) < 2 * ↑pq + bif bq then 1 else 0
hr : br = false
hq : bq = true
he : 2 * ↑pr = 2 * ↑pq
⊢ br = false ∧ bq = true ∧ pr = pq
Tactic:
exact ⟨hr, hq, Fin.ext (Nat.eq_of_mul_eq_mul_left zero_lt_two he)⟩
State after:
no goals