Theorem: impliesOr (NazgandLean4/Prop.lean)

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