no goals
α : Sort u_1
β : Sort ?u.32627
σ : α → Sort ?u.32623
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c
by_cases P <;> simp [*, exists_prop_of_true, exists_prop_of_false]