diff --git a/src/algebra/group/units.lean b/src/algebra/group/units.lean
index 4fbd6325ea83d..fe2f95950e0ce 100644
--- a/src/algebra/group/units.lean
+++ b/src/algebra/group/units.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Mario Carneiro, Johannes Hölzl, Chris Hughes, Jens Wagemaker
 -/
 import algebra.group.basic
+import logic.nontrivial
 
 /-!
 # Units (i.e., invertible elements) of a multiplicative monoid
@@ -225,7 +226,7 @@ a two-sided additive inverse. The actual definition says that `a` is equal to so
 `u : add_units M`, where `add_units M` is a bundled version of `is_add_unit`."]
 def is_unit [monoid M] (a : M) : Prop := ∃ u : units M, (u : M) = a
 
-lemma is_unit_of_subsingleton [monoid M] [subsingleton M] (a : M) : is_unit a :=
+@[nontriviality] lemma is_unit_of_subsingleton [monoid M] [subsingleton M] (a : M) : is_unit a :=
 ⟨⟨a, a, subsingleton.elim _ _, subsingleton.elim _ _⟩, rfl⟩
 
 @[simp, to_additive is_add_unit_add_unit]
diff --git a/src/analysis/asymptotics.lean b/src/analysis/asymptotics.lean
index d1b1bd9ab1278..69bfd6c33274c 100644
--- a/src/analysis/asymptotics.lean
+++ b/src/analysis/asymptotics.lean
@@ -147,6 +147,14 @@ theorem is_O.exists_nonneg (h : is_O f g' l) :
   ∃ c (H : 0 ≤ c), is_O_with c f g' l :=
 let ⟨c, hc⟩ := h in hc.exists_nonneg
 
+/-! ### Subsingleton -/
+
+@[nontriviality] lemma is_o_of_subsingleton [subsingleton E'] : is_o f' g' l :=
+λ c hc, is_O_with.of_bound $ by simp [subsingleton.elim (f' _) 0, mul_nonneg hc.le]
+
+@[nontriviality] lemma is_O_of_subsingleton [subsingleton E'] : is_O f' g' l :=
+is_o_of_subsingleton.is_O
+
 /-! ### Congruence -/
 
 theorem is_O_with_congr {c₁ c₂} {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
diff --git a/src/analysis/calculus/times_cont_diff.lean b/src/analysis/calculus/times_cont_diff.lean
index a64d1e2427050..af88b0d26e7cc 100644
--- a/src/analysis/calculus/times_cont_diff.lean
+++ b/src/analysis/calculus/times_cont_diff.lean
@@ -1533,6 +1533,21 @@ lemma times_cont_diff_within_at_const {n : with_top ℕ} {c : F} :
   times_cont_diff_within_at 𝕜 n (λx : E, c) s x :=
 times_cont_diff_at_const.times_cont_diff_within_at
 
+@[nontriviality] lemma times_cont_diff_of_subsingleton [subsingleton F] {n : with_top ℕ} :
+  times_cont_diff 𝕜 n f :=
+by { rw [subsingleton.elim f (λ _, 0)], exact times_cont_diff_const }
+
+@[nontriviality] lemma times_cont_diff_at_of_subsingleton [subsingleton F] {n : with_top ℕ} :
+  times_cont_diff_at 𝕜 n f x :=
+by { rw [subsingleton.elim f (λ _, 0)], exact times_cont_diff_at_const }
+
+@[nontriviality] lemma times_cont_diff_within_at_of_subsingleton [subsingleton F] {n : with_top ℕ} :
+  times_cont_diff_within_at 𝕜 n f s x :=
+by { rw [subsingleton.elim f (λ _, 0)], exact times_cont_diff_within_at_const }
+
+@[nontriviality] lemma times_cont_diff_on_of_subsingleton [subsingleton F] {n : with_top ℕ} :
+  times_cont_diff_on 𝕜 n f s :=
+by { rw [subsingleton.elim f (λ _, 0)], exact times_cont_diff_on_const }
 
 /-! ### Linear functions -/
 
@@ -2377,6 +2392,7 @@ inversion is `C^n`, for all `n`. -/
 lemma times_cont_diff_at_map_inverse [complete_space E] {n : with_top ℕ} (e : E ≃L[𝕜] F) :
   times_cont_diff_at 𝕜 n inverse (e : E →L[𝕜] F) :=
 begin
+  nontriviality E,
   -- first, we use the lemma `to_ring_inverse` to rewrite in terms of `ring.inverse` in the ring
   -- `E →L[𝕜] E`
   let O₁ : (E →L[𝕜] E) → (F →L[𝕜] E) := λ f, f.comp (e.symm : (F →L[𝕜] E)),
@@ -2390,14 +2406,9 @@ begin
   have h₂ : times_cont_diff 𝕜 n O₂,
   { exact is_bounded_bilinear_map_comp.times_cont_diff.comp (times_cont_diff_id.prod times_cont_diff_const) },
   refine h₁.times_cont_diff_at.comp _ (times_cont_diff_at.comp _ _ h₂.times_cont_diff_at),
-  -- this works differently depending on whether or not `E` is `nontrivial` (the condition for
-  -- `E →L[𝕜] E` to be a `normed_algebra`)
-  cases subsingleton_or_nontrivial E with _i _i; resetI,
-  { rw [subsingleton.elim ring.inverse (λ _, (0 : E →L[𝕜] E))],
-    exact times_cont_diff_at_const },
-  { convert times_cont_diff_at_ring_inverse 𝕜 (E →L[𝕜] E) 1,
-    simp [O₂],
-    refl },
+  convert times_cont_diff_at_ring_inverse 𝕜 (E →L[𝕜] E) 1,
+  simp [O₂],
+  refl
 end
 
 end map_inverse
diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean
index 705f14833b204..ab9588bc08edb 100644
--- a/src/analysis/normed_space/basic.lean
+++ b/src/analysis/normed_space/basic.lean
@@ -142,6 +142,9 @@ dist_zero_right g ▸ dist_eq_zero
 
 @[simp] lemma norm_zero : ∥(0:α)∥ = 0 := norm_eq_zero.2 rfl
 
+@[nontriviality] lemma norm_of_subsingleton [subsingleton α] (x : α) : ∥x∥ = 0 :=
+by rw [subsingleton.elim x 0, norm_zero]
+
 lemma norm_sum_le {β} : ∀(s : finset β) (f : β → α), ∥∑ a in s, f a∥ ≤ ∑ a in s, ∥ f a ∥ :=
 finset.le_sum_of_subadditive norm norm_zero norm_add_le
 
diff --git a/src/analysis/normed_space/units.lean b/src/analysis/normed_space/units.lean
index 41768732a5f1f..8e3d5edca1b11 100644
--- a/src/analysis/normed_space/units.lean
+++ b/src/analysis/normed_space/units.lean
@@ -49,17 +49,14 @@ def one_sub (t : R) (h : ∥t∥ < 1) : units R :=
 def add (x : units R) (t : R) (h : ∥t∥ < ∥(↑x⁻¹ : R)∥⁻¹) : units R :=
 x * (units.one_sub (-(↑x⁻¹ * t))
 begin
-  rcases subsingleton_or_nontrivial R with _i|_i; resetI,
-  { rw subsingleton.elim (↑x⁻¹ : R) 0,
-    have : (0:ℝ) < 1 := by norm_num,
-    simpa, },
-  { have hpos : 0 < ∥(↑x⁻¹ : R)∥ := units.norm_pos x⁻¹,
-    calc ∥-(↑x⁻¹ * t)∥
-        = ∥↑x⁻¹ * t∥                   : by { rw norm_neg }
-    ... ≤ ∥(↑x⁻¹ : R)∥ * ∥t∥            : norm_mul_le x.inv _
-    ... < ∥(↑x⁻¹ : R)∥ * ∥(↑x⁻¹ : R)∥⁻¹ : by nlinarith only [h, hpos]
-    ... = 1                           : mul_inv_cancel (ne_of_gt hpos) },
-end )
+  nontriviality R using [zero_lt_one],
+  have hpos : 0 < ∥(↑x⁻¹ : R)∥ := units.norm_pos x⁻¹,
+  calc ∥-(↑x⁻¹ * t)∥
+      = ∥↑x⁻¹ * t∥                   : by { rw norm_neg }
+  ... ≤ ∥(↑x⁻¹ : R)∥ * ∥t∥            : norm_mul_le x.inv _
+  ... < ∥(↑x⁻¹ : R)∥ * ∥(↑x⁻¹ : R)∥⁻¹ : by nlinarith only [h, hpos]
+  ... = 1                           : mul_inv_cancel (ne_of_gt hpos)
+end)
 
 @[simp] lemma add_coe (x : units R) (t : R) (h : ∥t∥ < ∥(↑x⁻¹ : R)∥⁻¹) :
   ((x.add t h) : R) = x + t := by { unfold units.add, simp [mul_add] }
@@ -75,15 +72,14 @@ x.add ((y : R) - x) h
 /-- The group of units of a complete normed ring is an open subset of the ring. -/
 lemma is_open : is_open {x : R | is_unit x} :=
 begin
-  rcases subsingleton_or_nontrivial R with _i|_i; resetI,
-  { exact is_open_discrete is_unit },
-  { apply metric.is_open_iff.mpr,
-    rintros x' ⟨x, h⟩,
-    refine ⟨∥(↑x⁻¹ : R)∥⁻¹, inv_pos.mpr (units.norm_pos x⁻¹), _⟩,
-    intros y hy,
-    rw [metric.mem_ball, dist_eq_norm, ←h] at hy,
-    use x.unit_of_nearby y hy,
-    simp }
+  nontriviality R,
+  apply metric.is_open_iff.mpr,
+  rintros x' ⟨x, h⟩,
+  refine ⟨∥(↑x⁻¹ : R)∥⁻¹, inv_pos.mpr (units.norm_pos x⁻¹), _⟩,
+  intros y hy,
+  rw [metric.mem_ball, dist_eq_norm, ←h] at hy,
+  use x.unit_of_nearby y hy,
+  simp
 end
 
 lemma nhds (x : units R) : {x : R | is_unit x} ∈ 𝓝 (x : R) :=
@@ -105,25 +101,24 @@ end
 lemma inverse_add (x : units R) :
   ∀ᶠ t in (𝓝 0), inverse ((x : R) + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹ :=
 begin
+  nontriviality R,
   rw [eventually_iff, mem_nhds_iff],
-  casesI subsingleton_or_nontrivial R,
-  { use [1, by norm_num] },
-  { have hinv : 0 < ∥(↑x⁻¹ : R)∥⁻¹,
-    { cancel_denoms,
-      exact x⁻¹.norm_pos },
-    use [∥(↑x⁻¹ : R)∥⁻¹, hinv],
-    intros t ht,
-    simp only [mem_ball, dist_zero_right] at ht,
-    have ht' : ∥-↑x⁻¹ * t∥ < 1,
-    { refine lt_of_le_of_lt (norm_mul_le _ _) _,
-      rw norm_neg,
-      refine lt_of_lt_of_le (mul_lt_mul_of_pos_left ht x⁻¹.norm_pos) _,
-      cancel_denoms },
-    have hright := inverse_one_sub (-↑x⁻¹ * t) ht',
-    have hleft := inverse_unit (x.add t ht),
-    simp only [neg_mul_eq_neg_mul_symm, sub_neg_eq_add] at hright,
-    simp only [units.add_coe] at hleft,
-    simp [hleft, hright, units.add] }
+  have hinv : 0 < ∥(↑x⁻¹ : R)∥⁻¹,
+  { cancel_denoms,
+    exact x⁻¹.norm_pos },
+  use [∥(↑x⁻¹ : R)∥⁻¹, hinv],
+  intros t ht,
+  simp only [mem_ball, dist_zero_right] at ht,
+  have ht' : ∥-↑x⁻¹ * t∥ < 1,
+  { refine lt_of_le_of_lt (norm_mul_le _ _) _,
+    rw norm_neg,
+    refine lt_of_lt_of_le (mul_lt_mul_of_pos_left ht x⁻¹.norm_pos) _,
+    cancel_denoms },
+  have hright := inverse_one_sub (-↑x⁻¹ * t) ht',
+  have hleft := inverse_unit (x.add t ht),
+  simp only [neg_mul_eq_neg_mul_symm, sub_neg_eq_add] at hright,
+  simp only [units.add_coe] at hleft,
+  simp [hleft, hright, units.add]
 end
 
 lemma inverse_one_sub_nth_order (n : ℕ) :
@@ -191,22 +186,19 @@ end
 /-- The function `λ t, inverse (x + t)` is O(1) as `t → 0`. -/
 lemma inverse_add_norm (x : units R) : is_O (λ t, inverse (↑x + t)) (λ t, (1:ℝ)) (𝓝 (0:R)) :=
 begin
+  nontriviality R,
   simp only [is_O_iff, norm_one, mul_one],
-  cases subsingleton_or_nontrivial R; resetI,
-  { refine ⟨1, eventually_of_forall (λ t, _)⟩,
-    have : ∥inverse (↑x + t)∥ = 0 := by simp,
-    linarith },
-  { cases is_O_iff.mp (@inverse_one_sub_norm R _ _) with C hC,
-    use C * ∥((x⁻¹:units R):R)∥,
-    have hzero : tendsto (λ t, - (↑x⁻¹ : R) * t) (𝓝 0) (𝓝 0),
-    { convert ((mul_left_continuous (-↑x⁻¹ : R)).tendsto 0).comp tendsto_id,
-      simp },
-    refine (inverse_add x).mp ((hzero.eventually hC).mp (eventually_of_forall _)),
-    intros t bound iden,
-    rw iden,
-    simp at bound,
-    have hmul := norm_mul_le (inverse (1 + ↑x⁻¹ * t)) ↑x⁻¹,
-    nlinarith [norm_nonneg (↑x⁻¹ : R)] }
+  cases is_O_iff.mp (@inverse_one_sub_norm R _ _) with C hC,
+  use C * ∥((x⁻¹:units R):R)∥,
+  have hzero : tendsto (λ t, - (↑x⁻¹ : R) * t) (𝓝 0) (𝓝 0),
+  { convert ((mul_left_continuous (-↑x⁻¹ : R)).tendsto 0).comp tendsto_id,
+    simp },
+  refine (inverse_add x).mp ((hzero.eventually hC).mp (eventually_of_forall _)),
+  intros t bound iden,
+  rw iden,
+  simp at bound,
+  have hmul := norm_mul_le (inverse (1 + ↑x⁻¹ * t)) ↑x⁻¹,
+  nlinarith [norm_nonneg (↑x⁻¹ : R)]
 end
 
 /-- The function
diff --git a/src/data/polynomial/degree/basic.lean b/src/data/polynomial/degree/basic.lean
index 1dbb400615cdf..fcf6e7359cd8d 100644
--- a/src/data/polynomial/degree/basic.lean
+++ b/src/data/polynomial/degree/basic.lean
@@ -50,6 +50,9 @@ def leading_coeff (p : polynomial R) : R := coeff p (nat_degree p)
 /-- a polynomial is `monic` if its leading coefficient is 1 -/
 def monic (p : polynomial R) := leading_coeff p = (1 : R)
 
+@[nontriviality] lemma monic_of_subsingleton [subsingleton R] (p : polynomial R) : monic p :=
+subsingleton.elim _ _
+
 lemma monic.def : monic p ↔ leading_coeff p = 1 := iff.rfl
 
 instance monic.decidable [decidable_eq R] : decidable (monic p) :=
diff --git a/src/linear_algebra/char_poly/coeff.lean b/src/linear_algebra/char_poly/coeff.lean
index db6b7ac934c33..cf5e1d73c88d4 100644
--- a/src/linear_algebra/char_poly/coeff.lean
+++ b/src/linear_algebra/char_poly/coeff.lean
@@ -82,7 +82,6 @@ end
 lemma det_of_card_zero (h : fintype.card n = 0) (M : matrix n n R) : M.det = 1 :=
 by { rw fintype.card_eq_zero_iff at h, suffices : M = 1, { simp [this] }, ext, tauto }
 
-
 theorem char_poly_degree_eq_dim [nontrivial R] (M : matrix n n R) :
 (char_poly M).degree = fintype.card n :=
 begin
diff --git a/src/linear_algebra/linear_independent.lean b/src/linear_algebra/linear_independent.lean
index 892b5f15e3f5d..514a56a7f3f82 100644
--- a/src/linear_algebra/linear_independent.lean
+++ b/src/linear_algebra/linear_independent.lean
@@ -56,8 +56,6 @@ make the linear independence tests usable as `hv.insert ha` etc.
 We also prove that any family of vectors includes a linear independent subfamily spanning the same
 submodule.
 
-### 
-
 ## Implementation notes
 
 We use families instead of sets because it allows us to say that two identical vectors are linearly
@@ -214,6 +212,7 @@ protected lemma linear_map.linear_independent_iff (f : M →ₗ[R] M') (hf_inj :
   linear_independent R (f ∘ v) ↔ linear_independent R v :=
 ⟨λ h, h.of_comp f, λ h, h.map $ by simp only [hf_inj, disjoint_bot_right]⟩
 
+@[nontriviality]
 lemma linear_independent_of_subsingleton [subsingleton R] : linear_independent R v :=
 linear_independent_iff.2 (λ l hl, subsingleton.elim _ _)
 
@@ -249,8 +248,8 @@ alias linear_independent_subtype_range ↔ linear_independent.of_subtype_range _
 theorem linear_independent.to_subtype_range {ι} {f : ι → M} (hf : linear_independent R f) :
   linear_independent R (coe : range f → M) :=
 begin
-  cases subsingleton_or_nontrivial R; resetI,
-  exacts [linear_independent_of_subsingleton, (linear_independent_subtype_range hf.injective).2 hf]
+  nontriviality R,
+  exact (linear_independent_subtype_range hf.injective).2 hf
 end
 
 theorem linear_independent.to_subtype_range' {ι} {f : ι → M} (hf : linear_independent R f)
@@ -448,7 +447,7 @@ lemma linear_independent_Union_finite {η : Type*} {ιs : η → Type*}
       disjoint (span R (range (f i))) (⨆i∈t, span R (range (f i)))) :
   linear_independent R (λ ji : Σ j, ιs j, f ji.1 ji.2) :=
 begin
-  cases subsingleton_or_nontrivial R; resetI, { exact linear_independent_of_subsingleton },
+  nontriviality R,
   apply linear_independent.of_subtype_range,
   { rintros ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ hxy,
     by_cases h_cases : x₁ = y₁,
diff --git a/src/logic/nontrivial.lean b/src/logic/nontrivial.lean
index 35d95464ce898..c2d3e3b5333c2 100644
--- a/src/logic/nontrivial.lean
+++ b/src/logic/nontrivial.lean
@@ -137,20 +137,30 @@ begin
   { exact ⟨x₂, h⟩ }
 end
 
+mk_simp_attribute nontriviality "Simp lemmas for `nontriviality` tactic"
+
+protected lemma subsingleton.le [preorder α] [subsingleton α] (x y : α) : x ≤ y :=
+le_of_eq (subsingleton.elim x y)
+
+attribute [nontriviality] eq_iff_true_of_subsingleton subsingleton.le
+
 namespace tactic
 
 /--
 Tries to generate a `nontrivial α` instance by performing case analysis on
 `subsingleton_or_nontrivial α`,
-attempting to discharge the subsingleton branch using `le_of_eq` and `subsingleton.elim`.
+attempting to discharge the subsingleton branch using lemmas with `@[nontriviality]` attribute,
+including `subsingleton.le` and `eq_iff_true_of_subsingleton`.
 -/
-meta def nontriviality_by_elim (α : expr) : tactic unit :=
+meta def nontriviality_by_elim (α : expr) (lems : interactive.parse simp_arg_list) : tactic unit :=
 do
   alternative ← to_expr ``(subsingleton_or_nontrivial %%α),
   n ← get_unused_name "_inst",
   tactic.cases alternative [n, n],
-  `[{ resetI, try { apply le_of_eq }, apply subsingleton.elim, }] <|>
-    fail format!"Could not prove goal assuming `subsingleton {α}`",
+  (solve1 $ do
+    reset_instance_cache,
+    interactive.simp none ff lems [`nontriviality] (interactive.loc.ns [none])) <|>
+      fail format!"Could not prove goal assuming `subsingleton {α}`",
   reset_instance_cache
 
 /--
@@ -183,8 +193,10 @@ Otherwise, the type needs to be specified in the tactic invocation, as `nontrivi
 The `nontriviality` tactic will first look for strict inequalities amongst the hypotheses,
 and use these to derive the `nontrivial` instance directly.
 
-Otherwise, it will perform a case split on `subsingleton α ∨ nontrivial α`,
-and attempt to discharge the `subsingleton` goal.
+Otherwise, it will perform a case split on `subsingleton α ∨ nontrivial α`, and attempt to discharge
+the `subsingleton` goal using `simp [lemmas] with nontriviality`, where `[lemmas]` is a list of
+additional `simp` lemmas that can be passed to `nontriviality` using the syntax
+`nontriviality α using [lemmas]`.
 
 ```
 example {R : Type} [ordered_ring R] {a : R} (h : 0 < a) : 0 < a :=
@@ -209,8 +221,21 @@ begin
   dec_trivial
 end
 ```
+
+```
+def myeq {α : Type} (a b : α) : Prop := a = b
+
+example {α : Type} (a b : α) (h : a = b) : myeq a b :=
+begin
+  success_if_fail { nontriviality α }, -- Fails
+  nontriviality α using [myeq], -- There is now a `nontrivial α` hypothesis available
+  assumption
+end
+```
 -/
-meta def nontriviality (t : parse parser.pexpr?) : tactic unit :=
+meta def nontriviality (t : parse texpr?)
+  (lems : parse (tk "using" *> simp_arg_list <|> pure [])) :
+  tactic unit :=
 do
   α ← match t with
   | some α := to_expr α
@@ -222,7 +247,7 @@ do
     fail "The goal is not an (in)equality, so you'll need to specify the desired `nontrivial α`
       instance by invoking `nontriviality α`."
   end,
-  nontriviality_by_assumption α <|> nontriviality_by_elim α
+  nontriviality_by_assumption α <|> nontriviality_by_elim α lems
 
 add_tactic_doc
 { name                     := "nontriviality",
diff --git a/test/nontriviality.lean b/test/nontriviality.lean
index 9a0db53c1c827..63edda3fa3db0 100644
--- a/test/nontriviality.lean
+++ b/test/nontriviality.lean
@@ -2,6 +2,8 @@ import logic.nontrivial
 import algebra.ordered_ring
 import data.nat.basic
 
+/-! ### Test `nontriviality` with inequality hypotheses -/
+
 example {R : Type} [ordered_ring R] {a : R} (h : 0 < a) : 0 < a :=
 begin
   nontriviality,
@@ -9,6 +11,8 @@ begin
   assumption,
 end
 
+/-! ### Test `nontriviality` with equality or non-strict inequality goals -/
+
 example {R : Type} [comm_ring R] {r s : R} : r * s = s * r :=
 begin
   nontriviality,
@@ -16,6 +20,8 @@ begin
   apply mul_comm,
 end
 
+/-! ### Test deducing `nontriviality` by instance search -/
+
 example {R : Type} [ordered_ring R] : 0 ≤ (1 : R) :=
 begin
   nontriviality R,
@@ -42,3 +48,54 @@ begin
   guard_hyp _inst : nontrivial R,
   dec_trivial
 end
+
+/-! Test using `@[nontriviality]` lemmas in `nontriviality and custom `simp` lemmas -/
+
+def empty_or_univ {α : Type*} (s : set α) : Prop := s = ∅ ∨ s = set.univ
+
+lemma subsingleton.set_empty_or_univ {α} [subsingleton α] (s : set α) :
+  s = ∅ ∨ s = set.univ :=
+subsingleton.set_cases (or.inl rfl) (or.inr rfl) s
+
+lemma subsingleton.set_empty_or_univ' {α} [subsingleton α] (s : set α) :
+  empty_or_univ s :=
+subsingleton.set_empty_or_univ s
+
+example {α : Type*} (s : set α) (hs : s = ∅ ∪ set.univ) : empty_or_univ s :=
+begin
+  success_if_fail { nontriviality α },
+  rw [set.empty_union] at hs,
+  exact or.inr hs
+end
+
+section
+
+local attribute [nontriviality] subsingleton.set_empty_or_univ
+
+example {α : Type*} (s : set α) (hs : s = ∅ ∪ set.univ) : empty_or_univ s :=
+begin
+  success_if_fail { nontriviality α },
+  nontriviality α using [subsingleton.set_empty_or_univ'],
+  rw [set.empty_union] at hs,
+  exact or.inr hs
+end
+
+end
+
+local attribute [nontriviality] subsingleton.set_empty_or_univ'
+
+example {α : Type*} (s : set α) (hs : s = ∅ ∪ set.univ) : empty_or_univ s :=
+begin
+  nontriviality α,
+  rw [set.empty_union] at hs,
+  exact or.inr hs
+end
+
+/-! Test with nonatomic type argument -/
+
+example (α : ℕ → Type) (a b : α 0) (h : a = b) : a = b :=
+begin
+  nontriviality α 0 using [nat.zero_lt_one],
+  guard_hyp _inst : nontrivial (α 0),
+  exact h
+end