find all assumptions of the shape ¬ (p ∧ q) or ¬ (p ∨ q) and replace them using de Morgan's law.

tautology breaks down assumptions of the form _ ∧ _, _ ∨ _, _ ↔ _ and ∃ _, _ and splits a goal of the form _ ∧ _, _ ↔ _ or ∃ _, _ until it can be discharged using reflexivity or solve_by_elim

Shorter name for the tactic tautology.