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