| example : (p → q → False) ↔ (¬ p ∨ ¬ q) := by | |
| apply Iff.intro | |
| · intro h | |
| by_cases hp:p <;> by_cases hq:q | |
| · specialize h hp hq; contradiction | |
| · exact Or.inr hq | |
| · exact Or.inl hp | |
| · exact Or.inr hq | |
| · intro | |
| | Or.inl hnp => intros; contradiction | |
| | Or.inr hnq => intros; contradiction |