no goals
α : Sort u_1
β : Sort ?u.40023
σ : α → Sort ?u.40019
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
by_cases hp : P <;> by_cases hq : Q <;> simp [hp, hq]