Theorem: forall_iff_forall_mergeBitRes (Controlbits/BitResiduum.lean)

State before:
m : ℕ
i : Fin (m + 1)
pr : BV (m + 1) → Prop
h : ∀ (b : Bool) (p : BV m), pr (mergeBitRes i b p)
q : BV (m + 1)
⊢ pr q
Tactic:
rcases mergeBitRes_surj i q with ⟨b, p, rfl⟩
State after:
case intro.intro
m : ℕ
i : Fin (m + 1)
pr : BV (m + 1) → Prop
h : ∀ (b : Bool) (p : BV m), pr (mergeBitRes i b p)
b : Bool
p : BV m
⊢ pr (mergeBitRes i b p)

State before:
case intro.intro
m : ℕ
i : Fin (m + 1)
pr : BV (m + 1) → Prop
h : ∀ (b : Bool) (p : BV m), pr (mergeBitRes i b p)
b : Bool
p : BV m
⊢ pr (mergeBitRes i b p)
Tactic:
exact h _ _
State after:
no goals