no goals
α : Sort u_2
β : Sort u_3
σ : α → Sort ?u.38655
f✝ : α → β
P✝ Q : Prop
inst✝² : Decidable P✝
inst✝¹ : Decidable Q
a✝ b✝ c✝ : α
A : P✝ → α
B : ¬P✝ → α
γ : Sort u_1
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)
by_cases h : P <;> simp [h]