diff --git a/counterexamples/canonically_ordered_comm_semiring_two_mul.lean b/counterexamples/canonically_ordered_comm_semiring_two_mul.lean
index 080176eb758f0..fd6ca5897584d 100644
--- a/counterexamples/canonically_ordered_comm_semiring_two_mul.lean
+++ b/counterexamples/canonically_ordered_comm_semiring_two_mul.lean
@@ -140,7 +140,8 @@ instance socsN2 : strict_ordered_comm_semiring (ℕ × zmod 2) :=
   mul_lt_mul_of_pos_right := mul_lt_mul_of_pos_right,
   ..Nxzmod_2.csrN2_1,
   ..(infer_instance : partial_order (ℕ × zmod 2)),
-  ..(infer_instance : comm_semiring (ℕ × zmod 2)) }
+  ..(infer_instance : comm_semiring (ℕ × zmod 2)),
+  ..pullback_nonzero prod.fst prod.fst_zero prod.fst_one }
 
 end Nxzmod_2
 
diff --git a/src/algebra/geom_sum.lean b/src/algebra/geom_sum.lean
index f2da01a0e2d53..457c133cffdc4 100644
--- a/src/algebra/geom_sum.lean
+++ b/src/algebra/geom_sum.lean
@@ -409,7 +409,7 @@ section order
 
 variables {n : ℕ} {x : α}
 
-lemma geom_sum_pos [strict_ordered_semiring α] [nontrivial α] (hx : 0 ≤ x) (hn : n ≠ 0) :
+lemma geom_sum_pos [strict_ordered_semiring α] (hx : 0 ≤ x) (hn : n ≠ 0) :
   0 < ∑ i in range n, x ^ i :=
 sum_pos' (λ k hk, pow_nonneg hx _) ⟨0, mem_range.2 hn.bot_lt, by simp⟩
 
diff --git a/src/algebra/order/archimedean.lean b/src/algebra/order/archimedean.lean
index 2179b9d00df32..bf4cdcc97a2ec 100644
--- a/src/algebra/order/archimedean.lean
+++ b/src/algebra/order/archimedean.lean
@@ -83,8 +83,7 @@ lemma exists_unique_add_zsmul_mem_Ioc {a : α} (ha : 0 < a) (b c : α) :
 
 end linear_ordered_add_comm_group
 
-theorem exists_nat_gt [strict_ordered_semiring α] [nontrivial α] [archimedean α]
-  (x : α) : ∃ n : ℕ, x < n :=
+theorem exists_nat_gt [strict_ordered_semiring α] [archimedean α] (x : α) : ∃ n : ℕ, x < n :=
 let ⟨n, h⟩ := archimedean.arch x zero_lt_one in
 ⟨n+1, lt_of_le_of_lt (by rwa ← nsmul_one)
   (nat.cast_lt.2 (nat.lt_succ_self _))⟩
@@ -96,8 +95,8 @@ begin
   exact (exists_nat_gt x).imp (λ n, le_of_lt)
 end
 
-lemma add_one_pow_unbounded_of_pos [strict_ordered_semiring α] [nontrivial α] [archimedean α]
-  (x : α) {y : α} (hy : 0 < y) :
+lemma add_one_pow_unbounded_of_pos [strict_ordered_semiring α] [archimedean α] (x : α) {y : α}
+  (hy : 0 < y) :
   ∃ n : ℕ, x < (y + 1) ^ n :=
 have 0 ≤ 1 + y, from add_nonneg zero_le_one hy.le,
 let ⟨n, h⟩ := archimedean.arch x hy in
@@ -109,7 +108,7 @@ let ⟨n, h⟩ := archimedean.arch x hy in
        ... = (y + 1) ^ n : by rw [add_comm]⟩
 
 section strict_ordered_ring
-variables [strict_ordered_ring α] [nontrivial α] [archimedean α]
+variables [strict_ordered_ring α] [archimedean α]
 
 lemma pow_unbounded_of_one_lt (x : α) {y : α} (hy1 : 1 < y) :
   ∃ n : ℕ, x < y ^ n :=
@@ -270,7 +269,7 @@ section linear_ordered_field
 variables [linear_ordered_field α]
 
 lemma archimedean_iff_nat_lt : archimedean α ↔ ∀ x : α, ∃ n : ℕ, x < n :=
-⟨@exists_nat_gt α _ _, λ H, ⟨λ x y y0,
+⟨@exists_nat_gt α _, λ H, ⟨λ x y y0,
   (H (x / y)).imp $ λ n h, le_of_lt $
   by rwa [div_lt_iff y0, ← nsmul_eq_mul] at h⟩⟩
 
@@ -281,7 +280,7 @@ archimedean_iff_nat_lt.trans
    lt_of_le_of_lt h (nat.cast_lt.2 (lt_add_one _))⟩⟩
 
 lemma archimedean_iff_int_lt : archimedean α ↔ ∀ x : α, ∃ n : ℤ, x < n :=
-⟨@exists_int_gt α _ _,
+⟨@exists_int_gt α _,
 begin
   rw archimedean_iff_nat_lt,
   intros h x,
diff --git a/src/algebra/order/ring/cone.lean b/src/algebra/order/ring/cone.lean
index dc7f31fb6a246..a07fdc0f99c79 100644
--- a/src/algebra/order/ring/cone.lean
+++ b/src/algebra/order/ring/cone.lean
@@ -14,6 +14,8 @@ import algebra.order.ring.defs
 
 set_option old_structure_cmd true
 
+variables {α : Type*} [ring α] [nontrivial α]
+
 namespace ring
 
 /-- A positive cone in a ring consists of a positive cone in underlying `add_comm_group`,
@@ -26,11 +28,10 @@ structure positive_cone (α : Type*) [ring α] extends add_comm_group.positive_c
 /-- Forget that a positive cone in a ring respects the multiplicative structure. -/
 add_decl_doc positive_cone.to_positive_cone
 
-/-- A positive cone in a ring induces a linear order if `1` is a positive element. -/
+/-- A total positive cone in a nontrivial ring induces a linear order. -/
 @[nolint has_nonempty_instance]
 structure total_positive_cone (α : Type*) [ring α]
-  extends positive_cone α, add_comm_group.total_positive_cone α :=
-(one_pos : pos 1)
+  extends positive_cone α, add_comm_group.total_positive_cone α
 
 /-- Forget that a `total_positive_cone` in a ring is total. -/
 add_decl_doc total_positive_cone.to_positive_cone
@@ -38,15 +39,17 @@ add_decl_doc total_positive_cone.to_positive_cone
 /-- Forget that a `total_positive_cone` in a ring respects the multiplicative structure. -/
 add_decl_doc total_positive_cone.to_total_positive_cone
 
-end ring
+lemma positive_cone.one_pos (C : positive_cone α) : C.pos 1 :=
+(C.pos_iff _).2 ⟨C.one_nonneg, λ h, one_ne_zero $ C.nonneg_antisymm C.one_nonneg h⟩
 
-namespace strict_ordered_ring
+end ring
 
 open ring
 
 /-- Construct a `strict_ordered_ring` by designating a positive cone in an existing `ring`. -/
-def mk_of_positive_cone {α : Type*} [ring α] (C : positive_cone α) : strict_ordered_ring α :=
-{ zero_le_one := by { change C.nonneg (1 - 0), convert C.one_nonneg, simp, },
+def strict_ordered_ring.mk_of_positive_cone (C : positive_cone α) : strict_ordered_ring α :=
+{ exists_pair_ne := ⟨0, 1, λ h, by simpa [←h, C.pos_iff] using C.one_pos⟩,
+  zero_le_one := by { change C.nonneg (1 - 0), convert C.one_nonneg, simp, },
   mul_pos := λ x y xp yp, begin
     change C.pos (x*y - 0),
     convert C.mul_pos x y (by { convert xp, simp, }) (by { convert yp, simp, }),
@@ -55,23 +58,8 @@ def mk_of_positive_cone {α : Type*} [ring α] (C : positive_cone α) : strict_o
   ..‹ring α›,
   ..ordered_add_comm_group.mk_of_positive_cone C.to_positive_cone }
 
-end strict_ordered_ring
-
-namespace linear_ordered_ring
-
-open ring
-
 /-- Construct a `linear_ordered_ring` by
 designating a positive cone in an existing `ring`. -/
-def mk_of_positive_cone {α : Type*} [ring α] (C : total_positive_cone α) :
-  linear_ordered_ring α :=
-{ exists_pair_ne := ⟨0, 1, begin
-    intro h,
-    have one_pos := C.one_pos,
-    rw [←h, C.pos_iff] at one_pos,
-    simpa using one_pos,
-  end⟩,
-  ..strict_ordered_ring.mk_of_positive_cone C.to_positive_cone,
+def linear_ordered_ring.mk_of_positive_cone (C : total_positive_cone α) : linear_ordered_ring α :=
+{ ..strict_ordered_ring.mk_of_positive_cone C.to_positive_cone,
   ..linear_ordered_add_comm_group.mk_of_positive_cone C.to_total_positive_cone, }
-
-end linear_ordered_ring
diff --git a/src/algebra/order/ring/defs.lean b/src/algebra/order/ring/defs.lean
index 4ec88e8f77544..f812c640f1796 100644
--- a/src/algebra/order/ring/defs.lean
+++ b/src/algebra/order/ring/defs.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
+Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Yaël Dillies
 -/
 import order.min_max
 import algebra.order.monoid.cancel.defs
@@ -29,21 +29,23 @@ For short,
 ## Typeclasses
 
 * `ordered_semiring`: Semiring with a partial order such that `+` and `*` respect `≤`.
-* `strict_ordered_semiring`: Semiring with a partial order such that `+` and `*` respects `<`.
+* `strict_ordered_semiring`: Nontrivial semiring with a partial order such that `+` and `*` respects
+  `<`.
 * `ordered_comm_semiring`: Commutative semiring with a partial order such that `+` and `*` respect
   `≤`.
-* `strict_ordered_comm_semiring`: Commutative semiring with a partial order such that `+` and `*`
-  respect `<`.
+* `strict_ordered_comm_semiring`: Nontrivial commutative semiring with a partial order such that `+`
+  and `*` respect `<`.
 * `ordered_ring`: Ring with a partial order such that `+` respects `≤` and `*` respects `<`.
 * `ordered_comm_ring`: Commutative ring with a partial order such that `+` respects `≤` and
   `*` respects `<`.
-* `linear_ordered_semiring`: Semiring with a linear order such that `+` respects `≤` and
+* `linear_ordered_semiring`: Nontrivial semiring with a linear order such that `+` respects `≤` and
   `*` respects `<`.
-* `linear_ordered_comm_semiring`: Commutative semiring with a linear order such that `+` respects
+* `linear_ordered_comm_semiring`: Nontrivial commutative semiring with a linear order such that `+`
+  respects `≤` and `*` respects `<`.
+* `linear_ordered_ring`: Nontrivial ring with a linear order such that `+` respects `≤` and `*`
+  respects `<`.
+* `linear_ordered_comm_ring`: Nontrivial commutative ring with a linear order such that `+` respects
   `≤` and `*` respects `<`.
-* `linear_ordered_ring`: Ring with a linear order such that `+` respects `≤` and `*` respects `<`.
-* `linear_ordered_comm_ring`: Commutative ring with a linear order such that `+` respects `≤` and
-  `*` respects `<`.
 * `canonically_ordered_comm_semiring`: Commutative semiring with a partial order such that `+`
   respects `≤`, `*` respects `<`, and `a ≤ b ↔ ∃ c, b = a + c`.
 
@@ -57,35 +59,42 @@ immediate predecessors and what conditions are added to each of them.
   - `ordered_add_comm_monoid` & multiplication & `*` respects `≤`
   - `semiring` & partial order structure & `+` respects `≤` & `*` respects `≤`
 * `strict_ordered_semiring`
-  - `ordered_cancel_add_comm_monoid` & multiplication & `*` respects `<`
-  - `ordered_semiring` & `+` respects `<` & `*` respects `<`
+  - `ordered_cancel_add_comm_monoid` & multiplication & `*` respects `<` & nontriviality
+  - `ordered_semiring` & `+` respects `<` & `*` respects `<` & nontriviality
 * `ordered_comm_semiring`
   - `ordered_semiring` & commutativity of multiplication
   - `comm_semiring` & partial order structure & `+` respects `≤` & `*` respects `<`
 * `strict_ordered_comm_semiring`
   - `strict_ordered_semiring` & commutativity of multiplication
-  - `ordered_comm_semiring` & `+` respects `<` & `*` respects `<`
+  - `ordered_comm_semiring` & `+` respects `<` & `*` respects `<` & nontriviality
 * `ordered_ring`
-  - `strict_ordered_semiring` & additive inverses
+  - `ordered_semiring` & additive inverses
   - `ordered_add_comm_group` & multiplication & `*` respects `<`
   - `ring` & partial order structure & `+` respects `≤` & `*` respects `<`
+* `strict_ordered_ring`
+  - `strict_ordered_semiring` & additive inverses
+  - `ordered_semiring` & `+` respects `<` & `*` respects `<` & nontriviality
 * `ordered_comm_ring`
   - `ordered_ring` & commutativity of multiplication
   - `ordered_comm_semiring` & additive inverses
   - `comm_ring` & partial order structure & `+` respects `≤` & `*` respects `<`
+* `strict_ordered_comm_ring`
+  - `strict_ordered_comm_semiring` & additive inverses
+  - `strict_ordered_ring` & commutativity of multiplication
+  - `ordered_comm_ring` & `+` respects `<` & `*` respects `<` & nontriviality
 * `linear_ordered_semiring`
-  - `strict_ordered_semiring` & totality of the order & nontriviality
+  - `strict_ordered_semiring` & totality of the order
   - `linear_ordered_add_comm_monoid` & multiplication & nontriviality & `*` respects `<`
 * `linear_ordered_comm_semiring`
-  - `strict_ordered_comm_semiring` & totality of the order & nontriviality
+  - `strict_ordered_comm_semiring` & totality of the order
   - `linear_ordered_semiring` & commutativity of multiplication
 * `linear_ordered_ring`
-  - `ordered_ring` & totality of the order & nontriviality
+  - `strict_ordered_ring` & totality of the order
   - `linear_ordered_semiring` & additive inverses
   - `linear_ordered_add_comm_group` & multiplication & `*` respects `<`
   - `domain` & linear order structure
 * `linear_ordered_comm_ring`
-  - `ordered_comm_ring` & totality of the order & nontriviality
+  - `strict_ordered_comm_ring` & totality of the order
   - `linear_ordered_ring` & commutativity of multiplication
   - `linear_ordered_comm_semiring` & additive inverses
   - `is_domain` & linear order structure
@@ -133,10 +142,11 @@ and multiplication by a nonnegative number is monotone. -/
 @[protect_proj, ancestor ordered_ring comm_ring]
 class ordered_comm_ring (α : Type u) extends ordered_ring α, comm_ring α
 
-/-- A `strict_ordered_semiring` is a semiring with a partial order such that addition is strictly
-monotone and multiplication by a positive number is strictly monotone. -/
-@[protect_proj, ancestor semiring ordered_cancel_add_comm_monoid]
-class strict_ordered_semiring (α : Type u) extends semiring α, ordered_cancel_add_comm_monoid α :=
+/-- A `strict_ordered_semiring` is a nontrivial semiring with a partial order such that addition is
+strictly monotone and multiplication by a positive number is strictly monotone. -/
+@[protect_proj, ancestor semiring ordered_cancel_add_comm_monoid nontrivial]
+class strict_ordered_semiring (α : Type u)
+  extends semiring α, ordered_cancel_add_comm_monoid α, nontrivial α :=
 (zero_le_one : (0 : α) ≤ 1)
 (mul_lt_mul_of_pos_left  : ∀ a b c : α, a < b → 0 < c → c * a < c * b)
 (mul_lt_mul_of_pos_right : ∀ a b c : α, a < b → 0 < c → a * c < b * c)
@@ -148,8 +158,8 @@ class strict_ordered_comm_semiring (α : Type u) extends strict_ordered_semiring
 
 /-- A `strict_ordered_ring` is a ring with a partial order such that addition is strictly monotone
 and multiplication by a positive number is strictly monotone. -/
-@[protect_proj, ancestor ring ordered_add_comm_group]
-class strict_ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α :=
+@[protect_proj, ancestor ring ordered_add_comm_group nontrivial]
+class strict_ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α, nontrivial α :=
 (zero_le_one : 0 ≤ (1 : α))
 (mul_pos     : ∀ a b : α, 0 < a → 0 < b → 0 < a * b)
 
@@ -165,7 +175,7 @@ explore changing this, but be warned that the instances involving `domain` may c
 search loops. -/
 @[protect_proj, ancestor strict_ordered_semiring linear_ordered_add_comm_monoid nontrivial]
 class linear_ordered_semiring (α : Type u)
-  extends strict_ordered_semiring α, linear_ordered_add_comm_monoid α, nontrivial α
+  extends strict_ordered_semiring α, linear_ordered_add_comm_monoid α
 
 /-- A `linear_ordered_comm_semiring` is a nontrivial commutative semiring with a linear order such
 that addition is monotone and multiplication by a positive number is strictly monotone. -/
@@ -175,8 +185,8 @@ class linear_ordered_comm_semiring (α : Type*)
 
 /-- A `linear_ordered_ring` is a ring with a linear order such that addition is monotone and
 multiplication by a positive number is strictly monotone. -/
-@[protect_proj, ancestor strict_ordered_ring linear_order nontrivial]
-class linear_ordered_ring (α : Type u) extends strict_ordered_ring α, linear_order α, nontrivial α
+@[protect_proj, ancestor strict_ordered_ring linear_order]
+class linear_ordered_ring (α : Type u) extends strict_ordered_ring α, linear_order α
 
 /-- A `linear_ordered_comm_ring` is a commutative ring with a linear order such that addition is
 monotone and multiplication by a positive number is strictly monotone. -/
@@ -518,9 +528,6 @@ lemma strict_mono.mul (hf : strict_mono f) (hg : strict_mono g) (hf₀ : ∀ x,
 
 end monotone
 
-section nontrivial
-variables [nontrivial α]
-
 lemma lt_one_add (a : α) : a < 1 + a := lt_add_of_pos_left _ zero_lt_one
 lemma lt_add_one (a : α) : a < a + 1 := lt_add_of_pos_right _ zero_lt_one
 
@@ -528,19 +535,10 @@ lemma one_lt_two : (1 : α) < 2 := lt_add_one _
 
 lemma lt_two_mul_self (ha : 0 < a) : a < 2 * a := lt_mul_of_one_lt_left ha one_lt_two
 
-lemma nat.strict_mono_cast : strict_mono (coe : ℕ → α) :=
-strict_mono_nat_of_lt_succ $ λ n, by { rw [nat.cast_succ], apply lt_add_one }
-
-/-- `coe : ℕ → α` as an `order_embedding` -/
-@[simps { fully_applied := ff }] def nat.cast_order_embedding : ℕ ↪o α :=
-order_embedding.of_strict_mono coe nat.strict_mono_cast
-
 @[priority 100] -- see Note [lower instance priority]
 instance strict_ordered_semiring.to_no_max_order : no_max_order α :=
 ⟨λ a, ⟨a + 1, lt_add_of_pos_right _ one_pos⟩⟩
 
-end nontrivial
-
 end strict_ordered_semiring
 
 section strict_ordered_comm_semiring
diff --git a/src/algebra/order/ring/inj_surj.lean b/src/algebra/order/ring/inj_surj.lean
index 1cefd24e6fd6b..1d0c95e8c60c1 100644
--- a/src/algebra/order/ring/inj_surj.lean
+++ b/src/algebra/order/ring/inj_surj.lean
@@ -90,7 +90,8 @@ protected def strict_ordered_semiring [strict_ordered_semiring α] [has_zero β]
   mul_lt_mul_of_pos_right := λ a b c h hc, show f (a * c) < f (b * c),
     by simpa only [mul, zero] using mul_lt_mul_of_pos_right ‹f a < f b› (by rwa ←zero),
   ..hf.ordered_cancel_add_comm_monoid f zero add nsmul,
-  ..hf.ordered_semiring f zero one add mul nsmul npow nat_cast }
+  ..hf.ordered_semiring f zero one add mul nsmul npow nat_cast,
+  ..pullback_nonzero f zero one }
 
 /-- Pullback a `strict_ordered_comm_semiring` under an injective map. -/
 @[reducible] -- See note [reducible non-instances]
@@ -143,7 +144,6 @@ protected def linear_ordered_semiring [linear_ordered_semiring α] [has_zero β]
   (hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y)) :
   linear_ordered_semiring β :=
 { .. linear_order.lift f hf hsup hinf,
-  .. pullback_nonzero f zero one,
   .. hf.strict_ordered_semiring f zero one add mul nsmul npow nat_cast }
 
 /-- Pullback a `linear_ordered_semiring` under an injective map. -/
@@ -172,7 +172,6 @@ def linear_ordered_ring [linear_ordered_ring α] [has_zero β] [has_one β] [has
   (hsup : ∀ x y, f (x ⊔ y) = max (f x) (f y)) (hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y)) :
   linear_ordered_ring β :=
 { .. linear_order.lift f hf hsup hinf,
-  .. pullback_nonzero f zero one,
   .. hf.strict_ordered_ring f zero one add mul neg sub nsmul zsmul npow nat_cast int_cast }
 
 /-- Pullback a `linear_ordered_comm_ring` under an injective map. -/
@@ -188,7 +187,6 @@ protected def linear_ordered_comm_ring [linear_ordered_comm_ring α] [has_zero 
   (hsup : ∀ x y, f (x ⊔ y) = max (f x) (f y)) (hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y)) :
   linear_ordered_comm_ring β :=
 { .. linear_order.lift f hf hsup hinf,
-  .. pullback_nonzero f zero one,
   .. hf.strict_ordered_comm_ring f zero one add mul neg sub nsmul zsmul npow nat_cast int_cast }
 
 end function.injective
diff --git a/src/algebra/order/ring/nontrivial.lean b/src/algebra/order/ring/nontrivial.lean
index d09ce734c7d83..c0e3cdd3c0939 100644
--- a/src/algebra/order/ring/nontrivial.lean
+++ b/src/algebra/order/ring/nontrivial.lean
@@ -7,25 +7,12 @@ import algebra.char_zero.defs
 import algebra.order.ring.defs
 
 /-!
-# Nontrivial strict ordered semirings (and hence linear ordered semirings) are characteristic zero.
+# Strict ordered semiring have characteristic zero
 -/
 
 variables {α : Type*}
 
-section strict_ordered_semiring
-variables [strict_ordered_semiring α] [nontrivial α]
-
-/-- Note this is not an instance as `char_zero` implies `nontrivial`, and this would risk forming a
-loop. -/
-lemma strict_ordered_semiring.to_char_zero : char_zero α := ⟨nat.strict_mono_cast.injective⟩
-
-end strict_ordered_semiring
-
-section linear_ordered_semiring
-variables [linear_ordered_semiring α]
-
 @[priority 100] -- see Note [lower instance priority]
-instance linear_ordered_semiring.to_char_zero : char_zero α :=
-strict_ordered_semiring.to_char_zero
-
-end linear_ordered_semiring
+instance strict_ordered_semiring.to_char_zero [strict_ordered_semiring α] : char_zero α :=
+⟨strict_mono.injective $ strict_mono_nat_of_lt_succ $ λ n,
+  by { rw [nat.cast_succ], apply lt_add_one }⟩
diff --git a/src/analysis/box_integral/box/subbox_induction.lean b/src/analysis/box_integral/box/subbox_induction.lean
index 2f9ea954f109e..2dd294e19f74f 100644
--- a/src/analysis/box_integral/box/subbox_induction.lean
+++ b/src/analysis/box_integral/box/subbox_induction.lean
@@ -147,7 +147,7 @@ begin
   { suffices : tendsto (λ m, (J m).upper - (J m).lower) at_top (𝓝 0), by simpa using hJlz.add this,
     refine tendsto_pi_nhds.2 (λ i, _),
     simpa [hJsub] using tendsto_const_nhds.div_at_top
-      (tendsto_pow_at_top_at_top_of_one_lt (@one_lt_two ℝ _ _)) },
+      (tendsto_pow_at_top_at_top_of_one_lt $ @one_lt_two ℝ _) },
   replace hJlz : tendsto (λ m, (J m).lower) at_top (𝓝[Icc I.lower I.upper] z),
     from tendsto_nhds_within_of_tendsto_nhds_of_eventually_within _ hJlz
       (eventually_of_forall hJl_mem),
diff --git a/src/data/complex/basic.lean b/src/data/complex/basic.lean
index 77f656aad7e53..4005e0c2a470c 100644
--- a/src/data/complex/basic.lean
+++ b/src/data/complex/basic.lean
@@ -169,6 +169,8 @@ by { ext; simp [equiv_real_prod] }
 diamond from the other actions they inherit through the `ℝ`-action on `ℂ` and action transitivity
 defined in `data.complex.module.lean`. -/
 
+instance : nontrivial ℂ := pullback_nonzero re rfl rfl
+
 instance : add_comm_group ℂ :=
 by refine_struct
   { zero := (0 : ℂ),
@@ -378,10 +380,9 @@ by rw [inv_def, ← mul_assoc, mul_conj, ← of_real_mul,
 
 noncomputable instance : field ℂ :=
 { inv := has_inv.inv,
-  exists_pair_ne := ⟨0, 1, mt (congr_arg re) zero_ne_one⟩,
   mul_inv_cancel := @complex.mul_inv_cancel,
   inv_zero := complex.inv_zero,
-  ..complex.comm_ring }
+  ..complex.comm_ring, ..complex.nontrivial }
 
 @[simp] lemma I_zpow_bit0 (n : ℤ) : I ^ (bit0 n) = (-1) ^ n :=
 by rw [zpow_bit0', I_mul_I]
@@ -655,8 +656,7 @@ protected def strict_ordered_comm_ring : strict_ordered_comm_ring ℂ :=
   add_le_add_left := λ w z h y, ⟨add_le_add_left h.1 _, congr_arg2 (+) rfl h.2⟩,
   mul_pos := λ z w hz hw,
     by simp [lt_def, mul_re, mul_im, ← hz.2, ← hw.2, mul_pos hz.1 hw.1],
-  .. complex.partial_order,
-  .. complex.comm_ring }
+  ..complex.partial_order, ..complex.comm_ring, ..complex.nontrivial }
 
 localized "attribute [instance] complex.strict_ordered_comm_ring" in complex_order
 
diff --git a/src/data/list/big_operators.lean b/src/data/list/big_operators.lean
index 5ddb9c831b581..f1500e574acf4 100644
--- a/src/data/list/big_operators.lean
+++ b/src/data/list/big_operators.lean
@@ -509,8 +509,7 @@ end
 
 /-- The product of a list of positive natural numbers is positive,
 and likewise for any nontrivial ordered semiring. -/
-lemma prod_pos [strict_ordered_semiring R] [nontrivial R] (l : list R) (h : ∀ a ∈ l, (0 : R) < a) :
-  0 < l.prod :=
+lemma prod_pos [strict_ordered_semiring R] (l : list R) (h : ∀ a ∈ l, (0 : R) < a) : 0 < l.prod :=
 begin
   induction l with a l ih,
   { simp },
diff --git a/src/data/nat/cast/basic.lean b/src/data/nat/cast/basic.lean
index b99a8cdb94364..8ce9dd52252e1 100644
--- a/src/data/nat/cast/basic.lean
+++ b/src/data/nat/cast/basic.lean
@@ -3,12 +3,13 @@ Copyright (c) 2014 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import data.nat.order.basic
-import algebra.order.group.abs
+import algebra.char_zero.defs
+import algebra.group.prod
 import algebra.group_with_zero.commute
-import algebra.group.opposite
 import algebra.hom.ring
+import algebra.order.group.abs
 import algebra.ring.commute
+import data.nat.order.basic
 
 /-!
 # Cast of natural numbers (additional theorems)
@@ -74,6 +75,7 @@ monotone_nat_of_le_succ $ λ n, by rw [nat.cast_succ]; exact le_add_of_nonneg_ri
 @[simp] theorem cast_nonneg (n : ℕ) : 0 ≤ (n : α) :=
 @nat.cast_zero α _ ▸ mono_cast (nat.zero_le n)
 
+section nontrivial
 variable [nontrivial α]
 
 lemma cast_add_one_pos (n : ℕ) : 0 < (n : α) + 1 :=
@@ -81,6 +83,28 @@ zero_lt_one.trans_le $ le_add_of_nonneg_left n.cast_nonneg
 
 @[simp] lemma cast_pos {n : ℕ} : (0 : α) < n ↔ 0 < n := by cases n; simp [cast_add_one_pos]
 
+end nontrivial
+
+variables [char_zero α] {m n : ℕ}
+
+lemma strict_mono_cast : strict_mono (coe : ℕ → α) :=
+mono_cast.strict_mono_of_injective cast_injective
+
+/-- `coe : ℕ → α` as an `order_embedding` -/
+@[simps { fully_applied := ff }] def cast_order_embedding : ℕ ↪o α :=
+order_embedding.of_strict_mono coe nat.strict_mono_cast
+
+@[simp, norm_cast] lemma cast_le : (m : α) ≤ n ↔ m ≤ n := strict_mono_cast.le_iff_le
+@[simp, norm_cast, mono] lemma cast_lt : (m : α) < n ↔ m < n := strict_mono_cast.lt_iff_lt
+
+@[simp, norm_cast] lemma one_lt_cast : 1 < (n : α) ↔ 1 < n := by rw [←cast_one, cast_lt]
+@[simp, norm_cast] lemma one_le_cast : 1 ≤ (n : α) ↔ 1 ≤ n := by rw [←cast_one, cast_le]
+
+@[simp, norm_cast] lemma cast_lt_one : (n : α) < 1 ↔ n = 0 :=
+by rw [←cast_one, cast_lt, lt_succ_iff, ←bot_eq_zero, le_bot_iff]
+
+@[simp, norm_cast] lemma cast_le_one : (n : α) ≤ 1 ↔ n ≤ 1 := by rw [←cast_one, cast_le]
+
 end ordered_semiring
 
 /-- A version of `nat.cast_sub` that works for `ℝ≥0` and `ℚ≥0`. Note that this proof doesn't work
@@ -96,30 +120,6 @@ begin
     rw [add_tsub_cancel_right, cast_add, add_tsub_cancel_right] }
 end
 
-section strict_ordered_semiring
-variables [strict_ordered_semiring α] [nontrivial α]
-
-@[simp, norm_cast] theorem cast_le {m n : ℕ} :
-  (m : α) ≤ n ↔ m ≤ n :=
-strict_mono_cast.le_iff_le
-
-@[simp, norm_cast, mono] theorem cast_lt {m n : ℕ} : (m : α) < n ↔ m < n :=
-strict_mono_cast.lt_iff_lt
-
-@[simp, norm_cast] theorem one_lt_cast {n : ℕ} : 1 < (n : α) ↔ 1 < n :=
-by rw [← cast_one, cast_lt]
-
-@[simp, norm_cast] theorem one_le_cast {n : ℕ} : 1 ≤ (n : α) ↔ 1 ≤ n :=
-by rw [← cast_one, cast_le]
-
-@[simp, norm_cast] theorem cast_lt_one {n : ℕ} : (n : α) < 1 ↔ n = 0 :=
-by rw [← cast_one, cast_lt, lt_succ_iff]; exact le_bot_iff
-
-@[simp, norm_cast] theorem cast_le_one {n : ℕ} : (n : α) ≤ 1 ↔ n ≤ 1 :=
-by rw [← cast_one, cast_le]
-
-end strict_ordered_semiring
-
 @[simp, norm_cast] theorem cast_min [linear_ordered_semiring α] {a b : ℕ} :
   (↑(min a b) : α) = min a b :=
 (@mono_cast α _).map_min
diff --git a/src/data/real/basic.lean b/src/data/real/basic.lean
index 8f9e470a4353b..6e2f41844209e 100644
--- a/src/data/real/basic.lean
+++ b/src/data/real/basic.lean
@@ -239,7 +239,8 @@ begin
 end
 
 instance : strict_ordered_comm_ring ℝ :=
-{ add_le_add_left :=
+{ exists_pair_ne := ⟨0, 1, real.zero_lt_one.ne⟩,
+  add_le_add_left :=
   begin
     simp only [le_iff_eq_or_lt],
     rintros a b ⟨rfl, h⟩,
@@ -258,7 +259,7 @@ instance : ordered_semiring ℝ               := infer_instance
 instance : ordered_add_comm_group ℝ         := infer_instance
 instance : ordered_cancel_add_comm_monoid ℝ := infer_instance
 instance : ordered_add_comm_monoid ℝ        := infer_instance
-instance : nontrivial ℝ                     := ⟨⟨0, 1, ne_of_lt real.zero_lt_one⟩⟩
+instance : nontrivial ℝ                     := infer_instance
 
 @[irreducible]
 private def sup : ℝ → ℝ → ℝ | ⟨x⟩ ⟨y⟩ :=
diff --git a/src/data/real/enat_ennreal.lean b/src/data/real/enat_ennreal.lean
index 87400591b0d8b..34c1e85051716 100644
--- a/src/data/real/enat_ennreal.lean
+++ b/src/data/real/enat_ennreal.lean
@@ -3,8 +3,8 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import data.real.ennreal
 import data.enat.basic
+import data.real.ennreal
 
 /-!
 # Coercion from `ℕ∞` to `ℝ≥0∞`
diff --git a/src/data/real/ennreal.lean b/src/data/real/ennreal.lean
index dc6a22a323421..08e07d67b204f 100644
--- a/src/data/real/ennreal.lean
+++ b/src/data/real/ennreal.lean
@@ -266,7 +266,7 @@ by simp only [ennreal.to_real, nnreal.coe_eq, to_nnreal_eq_to_nnreal_iff' hx hy]
 protected lemma zero_lt_one : 0 < (1 : ℝ≥0∞) := zero_lt_one
 
 @[simp] lemma one_lt_two : (1 : ℝ≥0∞) < 2 :=
-ennreal.coe_one ▸ coe_two ▸ by exact_mod_cast (@one_lt_two ℕ _ _)
+ennreal.coe_one ▸ coe_two ▸ by exact_mod_cast @one_lt_two ℕ _
 @[simp] lemma zero_lt_two : (0:ℝ≥0∞) < 2 := lt_trans ennreal.zero_lt_one one_lt_two
 lemma two_ne_zero : (2:ℝ≥0∞) ≠ 0 := (ne_of_lt zero_lt_two).symm
 lemma two_ne_top : (2:ℝ≥0∞) ≠ ∞ := coe_two ▸ coe_ne_top
diff --git a/src/number_theory/padics/padic_numbers.lean b/src/number_theory/padics/padic_numbers.lean
index 9d38d5c3d71ec..8497902808aea 100644
--- a/src/number_theory/padics/padic_numbers.lean
+++ b/src/number_theory/padics/padic_numbers.lean
@@ -1027,9 +1027,8 @@ lemma norm_le_one_iff_val_nonneg (x : ℚ_[p]) : ∥ x ∥ ≤ 1 ↔ 0 ≤ x.val
 begin
   by_cases hx : x = 0,
   { simp only [hx, norm_zero, valuation_zero, zero_le_one, le_refl], },
-  { rw [norm_eq_pow_val hx, ← zpow_zero (p : ℝ), zpow_le_iff_le
-      (nat.one_lt_cast.mpr (nat.prime.one_lt' p).1), right.neg_nonpos_iff],
-    apply_instance, }
+  { rw [norm_eq_pow_val hx, ← zpow_zero (p : ℝ), zpow_le_iff_le, right.neg_nonpos_iff],
+    exact nat.one_lt_cast.2 (nat.prime.one_lt' p).1 }
 end
 
 end norm_le_iff
diff --git a/src/order/filter/archimedean.lean b/src/order/filter/archimedean.lean
index 5fadc0546fa6d..1734c6a0a5833 100644
--- a/src/order/filter/archimedean.lean
+++ b/src/order/filter/archimedean.lean
@@ -19,11 +19,11 @@ variables {α R : Type*}
 
 open filter set
 
-@[simp] lemma nat.comap_coe_at_top [strict_ordered_semiring R] [nontrivial R] [archimedean R] :
+@[simp] lemma nat.comap_coe_at_top [strict_ordered_semiring R] [archimedean R] :
   comap (coe : ℕ → R) at_top = at_top :=
 comap_embedding_at_top (λ _ _, nat.cast_le) exists_nat_ge
 
-lemma tendsto_coe_nat_at_top_iff [strict_ordered_semiring R] [nontrivial R] [archimedean R]
+lemma tendsto_coe_nat_at_top_iff [strict_ordered_semiring R] [archimedean R]
   {f : α → ℕ} {l : filter α} :
   tendsto (λ n, (f n : R)) l at_top ↔ tendsto f l at_top :=
 tendsto_at_top_embedding (assume a₁ a₂, nat.cast_le) exists_nat_ge
@@ -32,22 +32,22 @@ lemma tendsto_coe_nat_at_top_at_top [strict_ordered_semiring R] [archimedean R]
   tendsto (coe : ℕ → R) at_top at_top :=
 nat.mono_cast.tendsto_at_top_at_top exists_nat_ge
 
-@[simp] lemma int.comap_coe_at_top [strict_ordered_ring R] [nontrivial R] [archimedean R] :
+@[simp] lemma int.comap_coe_at_top [strict_ordered_ring R] [archimedean R] :
   comap (coe : ℤ → R) at_top = at_top :=
 comap_embedding_at_top (λ _ _, int.cast_le) $ λ r,
   let ⟨n, hn⟩ := exists_nat_ge r in ⟨n, by exact_mod_cast hn⟩
 
-@[simp] lemma int.comap_coe_at_bot [strict_ordered_ring R] [nontrivial R] [archimedean R] :
+@[simp] lemma int.comap_coe_at_bot [strict_ordered_ring R] [archimedean R] :
   comap (coe : ℤ → R) at_bot = at_bot :=
 comap_embedding_at_bot (λ _ _, int.cast_le) $ λ r,
   let ⟨n, hn⟩ := exists_nat_ge (-r) in ⟨-n, by simpa [neg_le] using hn⟩
 
-lemma tendsto_coe_int_at_top_iff [strict_ordered_ring R] [nontrivial R] [archimedean R]
+lemma tendsto_coe_int_at_top_iff [strict_ordered_ring R] [archimedean R]
   {f : α → ℤ} {l : filter α} :
   tendsto (λ n, (f n : R)) l at_top ↔ tendsto f l at_top :=
 by rw [← tendsto_comap_iff, int.comap_coe_at_top]
 
-lemma tendsto_coe_int_at_bot_iff [strict_ordered_ring R] [nontrivial R] [archimedean R]
+lemma tendsto_coe_int_at_bot_iff [strict_ordered_ring R] [archimedean R]
   {f : α → ℤ} {l : filter α} :
   tendsto (λ n, (f n : R)) l at_bot ↔ tendsto f l at_bot :=
 by rw [← tendsto_comap_iff, int.comap_coe_at_bot]
diff --git a/src/order/filter/filter_product.lean b/src/order/filter/filter_product.lean
index 0855cf8eb3dd3..1aab2c5ab3f41 100644
--- a/src/order/filter/filter_product.lean
+++ b/src/order/filter/filter_product.lean
@@ -138,7 +138,7 @@ instance [strict_ordered_semiring β] : strict_ordered_semiring β* :=
    (coe_lt.1 hh).mp $ (coe_lt.1 hfg).mono $ λ a, mul_lt_mul_of_pos_left,
   mul_lt_mul_of_pos_right := λ x y z, induction_on₃ x y z $ λ f g h hfg hh, coe_lt.2 $
    (coe_lt.1 hh).mp $ (coe_lt.1 hfg).mono $ λ a, mul_lt_mul_of_pos_right,
-  .. germ.ordered_semiring, ..germ.ordered_cancel_add_comm_monoid }
+  ..germ.ordered_semiring, ..germ.ordered_cancel_add_comm_monoid, ..germ.nontrivial }
 
 instance [strict_ordered_comm_semiring β] : strict_ordered_comm_semiring β* :=
 { .. germ.strict_ordered_semiring, ..germ.ordered_comm_semiring }
@@ -147,13 +147,13 @@ instance [strict_ordered_ring β] : strict_ordered_ring β* :=
 { zero_le_one := const_le zero_le_one,
   mul_pos := λ x y, induction_on₂ x y $ λ f g hf hg, coe_pos.2 $
     (coe_pos.1 hg).mp $ (coe_pos.1 hf).mono $ λ x, mul_pos,
-  .. germ.ring, .. germ.ordered_add_comm_group, .. germ.nontrivial }
+  ..germ.ring, ..germ.strict_ordered_semiring }
 
 instance [strict_ordered_comm_ring β] : strict_ordered_comm_ring β* :=
 { .. germ.strict_ordered_ring, ..germ.ordered_comm_ring }
 
 noncomputable instance [linear_ordered_ring β] : linear_ordered_ring β* :=
-{ ..germ.strict_ordered_ring, ..germ.linear_order, ..germ.nontrivial }
+{ ..germ.strict_ordered_ring, ..germ.linear_order }
 
 noncomputable instance [linear_ordered_field β] : linear_ordered_field β* :=
 { .. germ.linear_ordered_ring, .. germ.field }
diff --git a/src/ring_theory/hahn_series.lean b/src/ring_theory/hahn_series.lean
index d4465f9599bb7..a57d262356ce3 100644
--- a/src/ring_theory/hahn_series.lean
+++ b/src/ring_theory/hahn_series.lean
@@ -1014,7 +1014,7 @@ power_series.coeff_mk _ _
 lemma coeff_to_power_series_symm {f : power_series R} {n : ℕ} :
   (hahn_series.to_power_series.symm f).coeff n = power_series.coeff R n f := rfl
 
-variables (Γ) (R) [strict_ordered_semiring Γ] [nontrivial Γ]
+variables (Γ R) [strict_ordered_semiring Γ]
 
 /-- Casts a power series as a Hahn series with coefficients from an `strict_ordered_semiring`. -/
 def of_power_series : (power_series R) →+* hahn_series Γ R :=
@@ -1133,7 +1133,8 @@ variables (R) [comm_semiring R] {A : Type*} [semiring A] [algebra R A]
   end,
   .. to_power_series }
 
-variables (Γ) (R) [strict_ordered_semiring Γ] [nontrivial Γ]
+variables (Γ R) [strict_ordered_semiring Γ]
+
 /-- Casting a power series as a Hahn series with coefficients from an `strict_ordered_semiring`
   is an algebra homomorphism. -/
 @[simps] def of_power_series_alg : (power_series A) →ₐ[R] hahn_series Γ A :=
diff --git a/src/ring_theory/polynomial/pochhammer.lean b/src/ring_theory/polynomial/pochhammer.lean
index 1a331fa73ca11..6907ad181a46d 100644
--- a/src/ring_theory/polynomial/pochhammer.lean
+++ b/src/ring_theory/polynomial/pochhammer.lean
@@ -146,7 +146,7 @@ end
 end semiring
 
 section strict_ordered_semiring
-variables {S : Type*} [strict_ordered_semiring S] [nontrivial S]
+variables {S : Type*} [strict_ordered_semiring S]
 
 lemma pochhammer_pos (n : ℕ) (s : S) (h : 0 < s) : 0 < (pochhammer S n).eval s :=
 begin
diff --git a/src/ring_theory/subsemiring/basic.lean b/src/ring_theory/subsemiring/basic.lean
index 68a2ec83120c0..23e888b4ba889 100644
--- a/src/ring_theory/subsemiring/basic.lean
+++ b/src/ring_theory/subsemiring/basic.lean
@@ -1112,10 +1112,10 @@ end actions
 
 
 /-- Submonoid of positive elements of an ordered semiring. -/
-def pos_submonoid (R : Type*) [strict_ordered_semiring R] [nontrivial R] : submonoid R :=
+def pos_submonoid (R : Type*) [strict_ordered_semiring R] : submonoid R :=
 { carrier := {x | 0 < x},
   one_mem' := show (0 : R) < 1, from zero_lt_one,
   mul_mem' := λ x y (hx : 0 < x) (hy : 0 < y), mul_pos hx hy }
 
-@[simp] lemma mem_pos_monoid {R : Type*} [strict_ordered_semiring R] [nontrivial R] (u : Rˣ) :
+@[simp] lemma mem_pos_monoid {R : Type*} [strict_ordered_semiring R] (u : Rˣ) :
   ↑u ∈ pos_submonoid R ↔ (0 : R) < u := iff.rfl
diff --git a/src/tactic/omega/coeffs.lean b/src/tactic/omega/coeffs.lean
index d4a5f10aab454..81fbe2f2848fc 100644
--- a/src/tactic/omega/coeffs.lean
+++ b/src/tactic/omega/coeffs.lean
@@ -111,10 +111,9 @@ lemma val_between_set {a : int} {l n : nat} :
 @[simp] lemma val_set {m : nat} {a : int} :
   val v ([] {m ↦ a}) = a * v m :=
 begin
-  apply val_between_set, apply zero_le,
-  apply lt_of_lt_of_le (lt_add_one _),
-  simp only [length_set, zero_add, le_max_right],
-  apply_instance,
+  apply val_between_set (zero_le _),
+  rw [length_set, zero_add],
+  exact lt_max_of_lt_right (lt_add_one _),
 end
 
 lemma val_between_neg {as : list int} {l : nat} :
diff --git a/src/topology/algebra/order/liminf_limsup.lean b/src/topology/algebra/order/liminf_limsup.lean
index 5200a03484d2f..bb85cc154ec69 100644
--- a/src/topology/algebra/order/liminf_limsup.lean
+++ b/src/topology/algebra/order/liminf_limsup.lean
@@ -382,7 +382,7 @@ begin
 end
 
 lemma limsup_eq_tendsto_sum_indicator_at_top
-  (R : Type*) [strict_ordered_semiring R] [nontrivial R] [archimedean R] (s : ℕ → set α) :
+  (R : Type*) [strict_ordered_semiring R] [archimedean R] (s : ℕ → set α) :
   limsup s at_top =
     {ω | tendsto (λ n, ∑ k in finset.range n, (s (k + 1)).indicator (1 : α → R) ω) at_top at_top} :=
 begin