apply Decidable.byCases (p:=p) <;> apply Decidable.byCases (p:=q)
<;> (intro hq hp; simp [hp,hq])
α : Sort u
inst✝² : DecidableEq α
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
⊢ (decide p && decide q) = decide (p ∧ q)
no goals