α✝ : Type ?u.3498
β : Type ?u.3501
α : Type u_1
⊢ Nontrivial α ∨ ¬Nontrivial α
α✝ : Type ?u.3498
β : Type ?u.3501
α : Type u_1
⊢ Subsingleton α ∨ Nontrivial α
rw [← not_nontrivial_iff_subsingleton, or_comm]
no goals
α✝ : Type ?u.3498
β : Type ?u.3501
α : Type u_1
⊢ Nontrivial α ∨ ¬Nontrivial α
exact Classical.em _