Theorem: decide_and_decide (Algdata/Init/Logic.lean)

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

State before:
case h2.h2
α : Sort u
inst✝² : DecidableEq α
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
⊢ ¬q → ¬p → (decide p && decide q) = decide (p ∧ q)
Tactic:
intro hq hp
State after:
case h2.h2
α : Sort u
inst✝² : DecidableEq α
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
hq : ¬q
hp : ¬p
⊢ (decide p && decide q) = decide (p ∧ q)

State before:
case h2.h2
α : Sort u
inst✝² : DecidableEq α
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
hq : ¬q
hp : ¬p
⊢ (decide p && decide q) = decide (p ∧ q)
Tactic:
simp [hp,hq]
State after:
no goals