Theorem: decide_and (Fifteen/Logic/Basic.lean)

State before:
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
⊢ decide (p ∧ q) = (decide p && decide q)
Tactic:
apply dite p <;> apply dite q <;> intro hp hq <;> simp [hp, hq]
State after:
no goals