Theorem: forall_iff_forall_mergeBitRes_bool (Controlbits/BitResiduum.lean)

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

case intro.true.intro
m : ℕ
i : Fin (m + 1)
pr : BV (m + 1) → Prop
h : (∀ (p : BV m), pr (mergeBitRes i false p)) ∧ ∀ (p : BV m), pr (mergeBitRes i true p)
p : BV m
⊢ pr (mergeBitRes i true p)

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

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