feat: split Logic.Nontrivial (#6959)

This continues reducing the import requirements for the basic algebraic hierarchy. In combination with #6954 #6955 #6956 #6957, this reduces the imports for `Mathlib.Algebra.Field.Defs` from * [before.pdf](https://github.com/leanprover-community/mathlib4/files/12518547/before.pdf) * [after.pdf](https://github.com/leanprover-community/mathlib4/files/12518546/after.pdf) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Sep 5, 2023 · 560425d · 560425d
1 parent 6226f93
commit 560425d
Show file tree

Hide file tree

Showing 15 changed files with 129 additions and 106 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2326,7 +2326,8 @@ import Mathlib.Logic.Hydra
 import Mathlib.Logic.IsEmpty
 import Mathlib.Logic.Lemmas
 import Mathlib.Logic.Nonempty
-import Mathlib.Logic.Nontrivial
+import Mathlib.Logic.Nontrivial.Basic
+import Mathlib.Logic.Nontrivial.Defs
 import Mathlib.Logic.Pairwise
 import Mathlib.Logic.Relation
 import Mathlib.Logic.Relator

diff --git a/Mathlib/Algebra/EuclideanDomain/Defs.lean b/Mathlib/Algebra/EuclideanDomain/Defs.lean
@@ -3,7 +3,6 @@ Copyright (c) 2018 Louis Carlin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Louis Carlin, Mario Carneiro
 -/
-import Mathlib.Logic.Nontrivial
 import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.Ring.Defs

diff --git a/Mathlib/Algebra/Group/TypeTags.lean b/Mathlib/Algebra/Group/TypeTags.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Algebra.Hom.Group
+import Mathlib.Logic.Nontrivial.Basic
 import Mathlib.Logic.Equiv.Defs
 import Mathlib.Data.Finite.Defs
 

diff --git a/Mathlib/Algebra/Group/ULift.lean b/Mathlib/Algebra/Group/ULift.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+import Mathlib.Logic.Nontrivial.Basic
 import Mathlib.Data.Int.Cast.Defs
 import Mathlib.Algebra.Hom.Equiv.Basic
 import Mathlib.Algebra.GroupWithZero.InjSurj

diff --git a/Mathlib/Algebra/Group/Units.lean b/Mathlib/Algebra/Group/Units.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Mario Carneiro, Johannes Hölzl, Chris Hughes, Jens Wagemaker, Jon Eugster
 -/
 import Mathlib.Algebra.Group.Basic
-import Mathlib.Logic.Nontrivial
 import Mathlib.Logic.Unique
 import Mathlib.Tactic.Nontriviality
 

diff --git a/Mathlib/Algebra/GroupWithZero/Defs.lean b/Mathlib/Algebra/GroupWithZero/Defs.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 import Mathlib.Algebra.Group.Defs
-import Mathlib.Logic.Nontrivial
+import Mathlib.Logic.Nontrivial.Defs
 import Mathlib.Algebra.NeZero
 
 #align_import algebra.group_with_zero.defs from "leanprover-community/mathlib"@"2f3994e1b117b1e1da49bcfb67334f33460c3ce4"

diff --git a/Mathlib/Algebra/GroupWithZero/Units/Basic.lean b/Mathlib/Algebra/GroupWithZero/Units/Basic.lean
@@ -5,6 +5,7 @@ Authors: Johan Commelin
 -/
 import Mathlib.Algebra.GroupWithZero.Basic
 import Mathlib.Algebra.Group.Units
+import Mathlib.Logic.Nontrivial.Basic
 import Mathlib.Tactic.Nontriviality
 import Mathlib.Util.AssertExists
 

diff --git a/Mathlib/Algebra/Opposites.lean b/Mathlib/Algebra/Opposites.lean
@@ -5,7 +5,7 @@ Authors: Kenny Lau
 -/
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Logic.Equiv.Defs
-import Mathlib.Logic.Nontrivial
+import Mathlib.Logic.Nontrivial.Basic
 import Mathlib.Logic.IsEmpty
 
 #align_import algebra.opposites from "leanprover-community/mathlib"@"7a89b1aed52bcacbcc4a8ad515e72c5c07268940"

diff --git a/Mathlib/Data/Int/Basic.lean b/Mathlib/Data/Int/Basic.lean
@@ -7,7 +7,6 @@ import Mathlib.Init.Data.Int.Order
 import Mathlib.Data.Int.Cast.Basic
 import Mathlib.Algebra.Ring.Basic
 import Mathlib.Order.Monotone.Basic
-import Mathlib.Logic.Nontrivial
 
 #align_import data.int.basic from "leanprover-community/mathlib"@"00d163e35035c3577c1c79fa53b68de17781ffc1"
 

diff --git a/Mathlib/Data/TwoPointing.lean b/Mathlib/Data/TwoPointing.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Data.Sum.Basic
-import Mathlib.Logic.Nontrivial
+import Mathlib.Logic.Nontrivial.Defs
 
 #align_import data.two_pointing from "leanprover-community/mathlib"@"fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e"
 

diff --git a/Mathlib/Logic/Nontrivial/Basic.lean b/Mathlib/Logic/Nontrivial/Basic.lean
@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sébastien Gouëzel
+-/
+import Mathlib.Logic.Nontrivial.Defs
+import Mathlib.Tactic.Attr.Register
+import Mathlib.Data.Prod.Basic
+import Mathlib.Data.Subtype
+import Mathlib.Logic.Function.Basic
+import Mathlib.Logic.Unique
+
+#align_import logic.nontrivial from "leanprover-community/mathlib"@"48fb5b5280e7c81672afc9524185ae994553ebf4"
+
+/-!
+# Nontrivial types
+
+Results about `Nontrivial`.
+-/
+
+
+variable {α : Type*} {β : Type*}
+
+open Classical
+
+-- `x` and `y` are explicit here, as they are often needed to guide typechecking of `h`.
+theorem nontrivial_of_lt [Preorder α] (x y : α) (h : x < y) : Nontrivial α :=
+  ⟨⟨x, y, ne_of_lt h⟩⟩
+#align nontrivial_of_lt nontrivial_of_lt
+
+theorem exists_pair_lt (α : Type*) [Nontrivial α] [LinearOrder α] : ∃ x y : α, x < y := by
+  rcases exists_pair_ne α with ⟨x, y, hxy⟩
+  cases lt_or_gt_of_ne hxy <;> exact ⟨_, _, ‹_›⟩
+#align exists_pair_lt exists_pair_lt
+
+theorem nontrivial_iff_lt [LinearOrder α] : Nontrivial α ↔ ∃ x y : α, x < y :=
+  ⟨fun h ↦ @exists_pair_lt α h _, fun ⟨x, y, h⟩ ↦ nontrivial_of_lt x y h⟩
+#align nontrivial_iff_lt nontrivial_iff_lt
+
+theorem Subtype.nontrivial_iff_exists_ne (p : α → Prop) (x : Subtype p) :
+    Nontrivial (Subtype p) ↔ ∃ (y : α) (_ : p y), y ≠ x := by
+  simp only [_root_.nontrivial_iff_exists_ne x, Subtype.exists, Ne.def, Subtype.ext_iff]
+#align subtype.nontrivial_iff_exists_ne Subtype.nontrivial_iff_exists_ne
+
+/-- An inhabited type is either nontrivial, or has a unique element. -/
+noncomputable def nontrivialPSumUnique (α : Type*) [Inhabited α] :
+    PSum (Nontrivial α) (Unique α) :=
+  if h : Nontrivial α then PSum.inl h
+  else
+    PSum.inr
+      { default := default,
+        uniq := fun x : α ↦ by
+          by_contra H
+          exact h ⟨_, _, H⟩ }
+#align nontrivial_psum_unique nontrivialPSumUnique
+
+instance Option.nontrivial [Nonempty α] : Nontrivial (Option α) := by
+  inhabit α
+  exact ⟨none, some default, fun .⟩
+
+/-- Pushforward a `Nontrivial` instance along an injective function. -/
+protected theorem Function.Injective.nontrivial [Nontrivial α] {f : α → β}
+    (hf : Function.Injective f) : Nontrivial β :=
+  let ⟨x, y, h⟩ := exists_pair_ne α
+  ⟨⟨f x, f y, hf.ne h⟩⟩
+#align function.injective.nontrivial Function.Injective.nontrivial
+
+/-- An injective function from a nontrivial type has an argument at
+which it does not take a given value. -/
+protected theorem Function.Injective.exists_ne [Nontrivial α] {f : α → β}
+    (hf : Function.Injective f) (y : β) : ∃ x, f x ≠ y := by
+  rcases exists_pair_ne α with ⟨x₁, x₂, hx⟩
+  by_cases h:f x₂ = y
+  · exact ⟨x₁, (hf.ne_iff' h).2 hx⟩
+  · exact ⟨x₂, h⟩
+#align function.injective.exists_ne Function.Injective.exists_ne
+
+instance nontrivial_prod_right [Nonempty α] [Nontrivial β] : Nontrivial (α × β) :=
+  Prod.snd_surjective.nontrivial
+
+instance nontrivial_prod_left [Nontrivial α] [Nonempty β] : Nontrivial (α × β) :=
+  Prod.fst_surjective.nontrivial
+
+namespace Pi
+
+variable {I : Type*} {f : I → Type*}
+
+/-- A pi type is nontrivial if it's nonempty everywhere and nontrivial somewhere. -/
+theorem nontrivial_at (i' : I) [inst : ∀ i, Nonempty (f i)] [Nontrivial (f i')] :
+    Nontrivial (∀ i : I, f i) := by
+  letI := Classical.decEq (∀ i : I, f i)
+  exact (Function.update_injective (fun i ↦ Classical.choice (inst i)) i').nontrivial
+#align pi.nontrivial_at Pi.nontrivial_at
+
+/-- As a convenience, provide an instance automatically if `(f default)` is nontrivial.
+
+If a different index has the non-trivial type, then use `haveI := nontrivial_at that_index`.
+-/
+instance nontrivial [Inhabited I] [∀ i, Nonempty (f i)] [Nontrivial (f default)] :
+    Nontrivial (∀ i : I, f i) :=
+  nontrivial_at default
+
+end Pi
+
+instance Function.nontrivial [h : Nonempty α] [Nontrivial β] : Nontrivial (α → β) :=
+  h.elim fun a ↦ Pi.nontrivial_at a
+
+@[nontriviality]
+protected theorem Subsingleton.le [Preorder α] [Subsingleton α] (x y : α) : x ≤ y :=
+  le_of_eq (Subsingleton.elim x y)
+#align subsingleton.le Subsingleton.le
+
+@[to_additive]
+theorem Subsingleton.eq_one [One α] [Subsingleton α] (a : α) : a = 1 :=
+  Subsingleton.elim _ _
diff --git a/Mathlib/Logic/Nontrivial.lean → Mathlib/Logic/Nontrivial/Defs.lean b/Mathlib/Logic/Nontrivial.lean → Mathlib/Logic/Nontrivial/Defs.lean
@@ -3,11 +3,7 @@ Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.Tactic.Attr.Register
-import Mathlib.Data.Prod.Basic
-import Mathlib.Data.Subtype
-import Mathlib.Logic.Function.Basic
-import Mathlib.Logic.Unique
+import Mathlib.Logic.Basic
 
 #align_import logic.nontrivial from "leanprover-community/mathlib"@"48fb5b5280e7c81672afc9524185ae994553ebf4"
 
@@ -19,6 +15,8 @@ A type is *nontrivial* if it contains at least two elements. This is useful in p
 (where it is equivalent to the fact that the dimension is positive).
 
 We introduce a typeclass `Nontrivial` formalizing this property.
+
+Basic results about nontrivial types are in `Mathlib.Logic.Nontrivial.Basic`.
 -/
 
 
@@ -60,29 +58,10 @@ theorem nontrivial_of_ne (x y : α) (h : x ≠ y) : Nontrivial α :=
   ⟨⟨x, y, h⟩⟩
 #align nontrivial_of_ne nontrivial_of_ne
 
--- `x` and `y` are explicit here, as they are often needed to guide typechecking of `h`.
-theorem nontrivial_of_lt [Preorder α] (x y : α) (h : x < y) : Nontrivial α :=
-  ⟨⟨x, y, ne_of_lt h⟩⟩
-#align nontrivial_of_lt nontrivial_of_lt
-
-theorem exists_pair_lt (α : Type*) [Nontrivial α] [LinearOrder α] : ∃ x y : α, x < y := by
-  rcases exists_pair_ne α with ⟨x, y, hxy⟩
-  cases lt_or_gt_of_ne hxy <;> exact ⟨_, _, ‹_›⟩
-#align exists_pair_lt exists_pair_lt
-
-theorem nontrivial_iff_lt [LinearOrder α] : Nontrivial α ↔ ∃ x y : α, x < y :=
-  ⟨fun h ↦ @exists_pair_lt α h _, fun ⟨x, y, h⟩ ↦ nontrivial_of_lt x y h⟩
-#align nontrivial_iff_lt nontrivial_iff_lt
-
 theorem nontrivial_iff_exists_ne (x : α) : Nontrivial α ↔ ∃ y, y ≠ x :=
   ⟨fun h ↦ @exists_ne α h x, fun ⟨_, hy⟩ ↦ nontrivial_of_ne _ _ hy⟩
 #align nontrivial_iff_exists_ne nontrivial_iff_exists_ne
 
-theorem Subtype.nontrivial_iff_exists_ne (p : α → Prop) (x : Subtype p) :
-    Nontrivial (Subtype p) ↔ ∃ (y : α) (_ : p y), y ≠ x := by
-  simp only [_root_.nontrivial_iff_exists_ne x, Subtype.exists, Ne.def, Subtype.ext_iff]
-#align subtype.nontrivial_iff_exists_ne Subtype.nontrivial_iff_exists_ne
-
 instance : Nontrivial Prop :=
   ⟨⟨True, False, true_ne_false⟩⟩
 
@@ -95,18 +74,6 @@ instance (priority := 500) Nontrivial.to_nonempty [Nontrivial α] : Nonempty α
   let ⟨x, _⟩ := _root_.exists_pair_ne α
   ⟨x⟩
 
-/-- An inhabited type is either nontrivial, or has a unique element. -/
-noncomputable def nontrivialPSumUnique (α : Type*) [Inhabited α] :
-    PSum (Nontrivial α) (Unique α) :=
-  if h : Nontrivial α then PSum.inl h
-  else
-    PSum.inr
-      { default := default,
-        uniq := fun x : α ↦ by
-          by_contra H
-          exact h ⟨_, _, H⟩ }
-#align nontrivial_psum_unique nontrivialPSumUnique
-
 theorem subsingleton_iff : Subsingleton α ↔ ∀ x y : α, x = y :=
   ⟨by
     intro h
@@ -135,17 +102,6 @@ theorem false_of_nontrivial_of_subsingleton (α : Type*) [Nontrivial α] [Subsin
   not_nontrivial _ ‹_›
 #align false_of_nontrivial_of_subsingleton false_of_nontrivial_of_subsingleton
 
-instance Option.nontrivial [Nonempty α] : Nontrivial (Option α) := by
-  inhabit α
-  exact ⟨none, some default, fun .⟩
-
-/-- Pushforward a `Nontrivial` instance along an injective function. -/
-protected theorem Function.Injective.nontrivial [Nontrivial α] {f : α → β}
-    (hf : Function.Injective f) : Nontrivial β :=
-  let ⟨x, y, h⟩ := exists_pair_ne α
-  ⟨⟨f x, f y, hf.ne h⟩⟩
-#align function.injective.nontrivial Function.Injective.nontrivial
-
 /-- Pullback a `Nontrivial` instance along a surjective function. -/
 protected theorem Function.Surjective.nontrivial [Nontrivial β] {f : α → β}
     (hf : Function.Surjective f) : Nontrivial α := by
@@ -158,56 +114,6 @@ protected theorem Function.Surjective.nontrivial [Nontrivial β] {f : α → β}
   exact ⟨⟨x', y', this⟩⟩
 #align function.surjective.nontrivial Function.Surjective.nontrivial
 
-/-- An injective function from a nontrivial type has an argument at
-which it does not take a given value. -/
-protected theorem Function.Injective.exists_ne [Nontrivial α] {f : α → β}
-    (hf : Function.Injective f) (y : β) : ∃ x, f x ≠ y := by
-  rcases exists_pair_ne α with ⟨x₁, x₂, hx⟩
-  by_cases h:f x₂ = y
-  · exact ⟨x₁, (hf.ne_iff' h).2 hx⟩
-  · exact ⟨x₂, h⟩
-#align function.injective.exists_ne Function.Injective.exists_ne
-
-
-instance nontrivial_prod_right [Nonempty α] [Nontrivial β] : Nontrivial (α × β) :=
-  Prod.snd_surjective.nontrivial
-
-instance nontrivial_prod_left [Nontrivial α] [Nonempty β] : Nontrivial (α × β) :=
-  Prod.fst_surjective.nontrivial
-
-namespace Pi
-
-variable {I : Type*} {f : I → Type*}
-
-/-- A pi type is nontrivial if it's nonempty everywhere and nontrivial somewhere. -/
-theorem nontrivial_at (i' : I) [inst : ∀ i, Nonempty (f i)] [Nontrivial (f i')] :
-    Nontrivial (∀ i : I, f i) := by
-  letI := Classical.decEq (∀ i : I, f i)
-  exact (Function.update_injective (fun i ↦ Classical.choice (inst i)) i').nontrivial
-#align pi.nontrivial_at Pi.nontrivial_at
-
-/-- As a convenience, provide an instance automatically if `(f default)` is nontrivial.
-
-If a different index has the non-trivial type, then use `haveI := nontrivial_at that_index`.
--/
-instance nontrivial [Inhabited I] [∀ i, Nonempty (f i)] [Nontrivial (f default)] :
-    Nontrivial (∀ i : I, f i) :=
-  nontrivial_at default
-
-end Pi
-
-instance Function.nontrivial [h : Nonempty α] [Nontrivial β] : Nontrivial (α → β) :=
-  h.elim fun a ↦ Pi.nontrivial_at a
-
-@[nontriviality]
-protected theorem Subsingleton.le [Preorder α] [Subsingleton α] (x y : α) : x ≤ y :=
-  le_of_eq (Subsingleton.elim x y)
-#align subsingleton.le Subsingleton.le
-
-@[to_additive]
-theorem Subsingleton.eq_one [One α] [Subsingleton α] (a : α) : a = 1 :=
-  Subsingleton.elim _ _
-
 namespace Bool
 
 instance : Nontrivial Bool :=

diff --git a/Mathlib/Order/Synonym.lean b/Mathlib/Order/Synonym.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Damiano Testa, Yaël Dillies
 -/
 import Mathlib.Logic.Equiv.Defs
-import Mathlib.Logic.Nontrivial
+import Mathlib.Logic.Nontrivial.Defs
 import Mathlib.Order.Basic
 
 #align_import order.synonym from "leanprover-community/mathlib"@"c4658a649d216f57e99621708b09dcb3dcccbd23"

diff --git a/Mathlib/Order/WithBot.lean b/Mathlib/Order/WithBot.lean
@@ -3,6 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
+import Mathlib.Logic.Nontrivial.Basic
 import Mathlib.Order.BoundedOrder
 import Mathlib.Data.Option.NAry
 

diff --git a/Mathlib/Tactic/Nontriviality/Core.lean b/Mathlib/Tactic/Nontriviality/Core.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Mario Carneiro
 -/
 import Qq.MetaM
-import Mathlib.Logic.Nontrivial
+import Mathlib.Logic.Nontrivial.Basic
 import Mathlib.Tactic.SolveByElim
 
 /-! # The `nontriviality` tactic. -/