Theorem: combineCases (NazgandLean4/Prop.lean)

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