Theorem: distrib (meetings/Foundations.lean)

State before:
r p q R : Prop
⊢ p ∨ q ∧ r ↔ (p ∨ q) ∧ (p ∨ r)
Tactic:
tauto
State after:
no goals