Theorem: exercise2_1 (LeanCourse/Assignments/Assignment2.lean)

State before:
α : Type u_1
p q : α → Prop
⊢ (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ ∃ x, q x
Tactic:
sorry
State after:
no goals