Theorem: decide_or (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