Theorem: getBit_ext_iff (Controlbits/BitResiduum.lean)

State before:
m : ℕ
q q' : BV (m + 1)
⊢ q = q' ↔ ∀ (i : Fin (m + 1)), getBit i q = getBit i q'
Tactic:
refine' ⟨fun h _ => h ▸ rfl, fun h => _⟩
State after:
m : ℕ
q q' : BV (m + 1)
h : ∀ (i : Fin (m + 1)), getBit i q = getBit i q'
⊢ q = q'

State before:
m : ℕ
q q' : BV (m + 1)
h : ∀ (i : Fin (m + 1)), getBit i q = getBit i q'
⊢ q = q'
Tactic:
induction' m with m IH
State after:
case zero
q q' : BV (0 + 1)
h : ∀ (i : Fin (0 + 1)), getBit i q = getBit i q'
⊢ q = q'

case succ
m : ℕ
IH : ∀ {q q' : BV (m + 1)}, (∀ (i : Fin (m + 1)), getBit i q = getBit i q') → q = q'
q q' : BV (m + 1 + 1)
h : ∀ (i : Fin (m + 1 + 1)), getBit i q = getBit i q'
⊢ q = q'

State before:
case zero
q q' : BV (0 + 1)
h : ∀ (i : Fin (0 + 1)), getBit i q = getBit i q'
⊢ q = q'
Tactic:
simp_rw [getRes_getBit_inj_iff 0, Fin.eq_zero, and_true, h]
State after:
no goals

State before:
case succ
m : ℕ
IH : ∀ {q q' : BV (m + 1)}, (∀ (i : Fin (m + 1)), getBit i q = getBit i q') → q = q'
q q' : BV (m + 1 + 1)
h : ∀ (i : Fin (m + 1 + 1)), getBit i q = getBit i q'
⊢ q = q'
Tactic:
simp_rw [Fin.forall_fin_succ (P := fun i => getBit i q = getBit i q'), getBit_succ] at h
State after:
case succ
m : ℕ
IH : ∀ {q q' : BV (m + 1)}, (∀ (i : Fin (m + 1)), getBit i q = getBit i q') → q = q'
q q' : BV (m + 1 + 1)
h : getBit 0 q = getBit 0 q' ∧ ∀ (i : Fin (m + 1)), getBit i (getRes 0 q) = getBit i (getRes 0 q')
⊢ q = q'

State before:
case succ
m : ℕ
IH : ∀ {q q' : BV (m + 1)}, (∀ (i : Fin (m + 1)), getBit i q = getBit i q') → q = q'
q q' : BV (m + 1 + 1)
h : getBit 0 q = getBit 0 q' ∧ ∀ (i : Fin (m + 1)), getBit i (getRes 0 q) = getBit i (getRes 0 q')
⊢ q = q'
Tactic:
exact (getRes_getBit_inj_iff 0).mpr ⟨h.1, IH h.2⟩
State after:
no goals