α : Sort u_1
r p q : α → Prop
P Q : (x : α) → p x → Prop
b : Prop
⊢ (∃ x, (p x ∨ q x) ∧ r x) ↔ (∃ x, p x ∧ r x) ∨ ∃ x, q x ∧ r x
α : Sort u_1
r p q : α → Prop
P Q : (x : α) → p x → Prop
b : Prop
⊢ (∃ x x_1, r x) ↔ (∃ x x_1, r x) ∨ ∃ x x_1, r x
simp only [exists_prop]
no goals
α : Sort u_1
r p q : α → Prop
P Q : (x : α) → p x → Prop
b : Prop
⊢ (∃ x, (p x ∨ q x) ∧ r x) ↔ (∃ x, p x ∧ r x) ∨ ∃ x, q x ∧ r x
exact Iff.trans (exists_congr fun x ↦ or_and_right) exists_or