feat(logic/nontrivial): make nontriviality work for more goals (#4574)

The goal is to make `nontriviality` work for the following goals:

* [x] `nontriviality α` if the goal is `is_open s`, `s : set α`;
* [x] `nontriviality E` if the goal is `is_O f g` or `is_o f g`, where `f : α → E`;
* [x] `nontriviality R` if the goal is `linear_independent R _`;
* [ ] `nontriviality R` if the goal is `is_O f g` or `is_o f g`, where `f : α → E`, `[semimodule R E]`;
  in this case `nontriviality` should add a local instance `semimodule.subsingleton R`.

The last case was never needed in `mathlib`, and there is a workaround: run `nontriviality E`, then deduce `nontrivial R` from `nontrivial E`.

Misc feature:

* [x] make `nontriviality` accept an optional list of additional `simp` lemmas.



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

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]

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 α}

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

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
 

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

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) :=

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

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₁,

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",