Theorem: eq_flipBit_zero_of_lt_of_flipBit_zero_gt' (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
r q : BV (a✝ + 1)
i : Fin (a✝ + 1)
h : r < q
hf : (flipBit i) q < (flipBit i) r
⊢ ∀ k ≥ i, getBit k r = getBit k ((flipBit i) q)
Tactic:
rcases mergeBitRes_surj i q with ⟨bq, pq, rfl⟩
State after:
case intro.intro
a✝ : ℕ
r : BV (a✝ + 1)
i : Fin (a✝ + 1)
bq : Bool
pq : BV a✝
h : r < mergeBitRes i bq pq
hf : (flipBit i) (mergeBitRes i bq pq) < (flipBit i) r
⊢ ∀ k ≥ i, getBit k r = getBit k ((flipBit i) (mergeBitRes i bq pq))

State before:
case intro.intro
a✝ : ℕ
r : BV (a✝ + 1)
i : Fin (a✝ + 1)
bq : Bool
pq : BV a✝
h : r < mergeBitRes i bq pq
hf : (flipBit i) (mergeBitRes i bq pq) < (flipBit i) r
⊢ ∀ k ≥ i, getBit k r = getBit k ((flipBit i) (mergeBitRes i bq pq))
Tactic:
rcases mergeBitRes_surj i r with ⟨br, pr, rfl⟩
State after:
case intro.intro.intro.intro
a✝ : ℕ
i : Fin (a✝ + 1)
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
h : mergeBitRes i br pr < mergeBitRes i bq pq
hf : (flipBit i) (mergeBitRes i bq pq) < (flipBit i) (mergeBitRes i br pr)
⊢ ∀ k ≥ i, getBit k (mergeBitRes i br pr) = getBit k ((flipBit i) (mergeBitRes i bq pq))

State before:
case intro.intro.intro.intro
a✝ : ℕ
i : Fin (a✝ + 1)
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
h : mergeBitRes i br pr < mergeBitRes i bq pq
hf : (flipBit i) (mergeBitRes i bq pq) < (flipBit i) (mergeBitRes i br pr)
⊢ ∀ k ≥ i, getBit k (mergeBitRes i br pr) = getBit k ((flipBit i) (mergeBitRes i bq pq))
Tactic:
simp_rw [flipBit_mergeBitRes] at hf
State after:
case intro.intro.intro.intro
a✝ : ℕ
i : Fin (a✝ + 1)
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
h : mergeBitRes i br pr < mergeBitRes i bq pq
hf : mergeBitRes i (!bq) pq < mergeBitRes i (!br) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i br pr) = getBit k ((flipBit i) (mergeBitRes i bq pq))

State before:
case intro.intro.intro.intro
a✝ : ℕ
i : Fin (a✝ + 1)
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
h : mergeBitRes i br pr < mergeBitRes i bq pq
hf : mergeBitRes i (!bq) pq < mergeBitRes i (!br) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i br pr) = getBit k ((flipBit i) (mergeBitRes i bq pq))
Tactic:
cases br <;> cases bq
State after:
case intro.intro.intro.intro.false.false
a✝ : ℕ
i : Fin (a✝ + 1)
pq pr : BV a✝
h : mergeBitRes i false pr < mergeBitRes i false pq
hf : mergeBitRes i (!false) pq < mergeBitRes i (!false) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i false pr) = getBit k ((flipBit i) (mergeBitRes i false pq))

case intro.intro.intro.intro.false.true
a✝ : ℕ
i : Fin (a✝ + 1)
pq pr : BV a✝
h : mergeBitRes i false pr < mergeBitRes i true pq
hf : mergeBitRes i (!true) pq < mergeBitRes i (!false) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i false pr) = getBit k ((flipBit i) (mergeBitRes i true pq))

case intro.intro.intro.intro.true.false
a✝ : ℕ
i : Fin (a✝ + 1)
pq pr : BV a✝
h : mergeBitRes i true pr < mergeBitRes i false pq
hf : mergeBitRes i (!false) pq < mergeBitRes i (!true) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i true pr) = getBit k ((flipBit i) (mergeBitRes i false pq))

case intro.intro.intro.intro.true.true
a✝ : ℕ
i : Fin (a✝ + 1)
pq pr : BV a✝
h : mergeBitRes i true pr < mergeBitRes i true pq
hf : mergeBitRes i (!true) pq < mergeBitRes i (!true) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i true pr) = getBit k ((flipBit i) (mergeBitRes i true pq))

State before:
case intro.intro.intro.intro.false.false
a✝ : ℕ
i : Fin (a✝ + 1)
pq pr : BV a✝
h : mergeBitRes i false pr < mergeBitRes i false pq
hf : mergeBitRes i (!false) pq < mergeBitRes i (!false) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i false pr) = getBit k ((flipBit i) (mergeBitRes i false pq))
Tactic:
sorry
State after:
no goals

State before:
case intro.intro.intro.intro.false.true
a✝ : ℕ
i : Fin (a✝ + 1)
pq pr : BV a✝
h : mergeBitRes i false pr < mergeBitRes i true pq
hf : mergeBitRes i (!true) pq < mergeBitRes i (!false) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i false pr) = getBit k ((flipBit i) (mergeBitRes i true pq))
Tactic:
sorry
State after:
no goals

State before:
case intro.intro.intro.intro.true.false
a✝ : ℕ
i : Fin (a✝ + 1)
pq pr : BV a✝
h : mergeBitRes i true pr < mergeBitRes i false pq
hf : mergeBitRes i (!false) pq < mergeBitRes i (!true) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i true pr) = getBit k ((flipBit i) (mergeBitRes i false pq))
Tactic:
sorry
State after:
no goals

State before:
case intro.intro.intro.intro.true.true
a✝ : ℕ
i : Fin (a✝ + 1)
pq pr : BV a✝
h : mergeBitRes i true pr < mergeBitRes i true pq
hf : mergeBitRes i (!true) pq < mergeBitRes i (!true) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i true pr) = getBit k ((flipBit i) (mergeBitRes i true pq))
Tactic:
sorry
State after:
no goals