fix(order/complete_lattice): fix diamond in sup vs max and min vs inf (…

…#11309)

`complete_linear_order` has separate `max` and `sup` fields. There is no need to have both, so this removes one of them by telling the structure compiler to merge the two fields. The same is true of `inf` and `min`.

As well as diamonds being possible in the abstract case, a handful of concrete example of this diamond existed.
`linear_order` instances with default-populated fields were usually to blame.

src/algebra/tropical/big_operators.lean

@@ -105,11 +105,7 @@ lemma trop_Inf_image [conditionally_complete_linear_order R] (s : finset S)
 begin
   rcases s.eq_empty_or_nonempty with rfl|h,
   { simp only [set.image_empty, coe_empty, sum_empty, with_top.cInf_empty, trop_top] },
-  rw [←inf'_eq_cInf_image _ h, inf'_eq_inf],
-  convert s.trop_inf f,
-  refine lattice.ext _,
-  intros,
-  exact iff.rfl
+  rw [←inf'_eq_cInf_image _ h, inf'_eq_inf, s.trop_inf],
 end
 
 lemma trop_infi [conditionally_complete_linear_order R] [fintype S] (f : S → with_top R) :
@@ -138,11 +134,7 @@ lemma untrop_sum_eq_Inf_image [conditionally_complete_linear_order R] (s : finse
 begin
   rcases s.eq_empty_or_nonempty with rfl|h,
   { simp only [set.image_empty, coe_empty, sum_empty, with_top.cInf_empty, untrop_zero] },
-  rw [←inf'_eq_cInf_image _ h, inf'_eq_inf],
-  convert s.untrop_sum' f,
-  refine lattice.ext _,
-  intros,
-  exact iff.rfl
+  rw [←inf'_eq_cInf_image _ h, inf'_eq_inf, finset.untrop_sum'],
 end
 
 lemma untrop_sum [conditionally_complete_linear_order R] [fintype S]

src/data/nat/enat.lean

@@ -269,12 +269,17 @@ lemma pos_iff_one_le {x : enat} : 0 < x ↔ 1 ≤ x :=
 enat.cases_on x (by simp only [iff_true, le_top, coe_lt_top, ← @nat.cast_zero enat]) $
   λ n, by { rw [← nat.cast_zero, ← nat.cast_one, enat.coe_lt_coe, enat.coe_le_coe], refl }
 
-noncomputable instance : linear_order enat :=
-{ le_total := λ x y, enat.cases_on x
+instance : is_total enat (≤) :=
+{ total := λ x y, enat.cases_on x
     (or.inr le_top) (enat.cases_on y (λ _, or.inl le_top)
       (λ x y, (le_total x y).elim (or.inr ∘ coe_le_coe.2)
-        (or.inl ∘ coe_le_coe.2))),
+        (or.inl ∘ coe_le_coe.2))) }
+
+noncomputable instance : linear_order enat :=
+{ le_total := is_total.total,
   decidable_le := classical.dec_rel _,
+  max := (⊔),
+  max_def := @sup_eq_max_default _ _ (id _) _,
   ..enat.partial_order }
 
 instance : bounded_order enat :=
@@ -288,12 +293,6 @@ noncomputable instance : lattice enat :=
   le_inf := λ _ _ _, le_min,
   ..enat.semilattice_sup }
 
-lemma sup_eq_max {a b : enat} : a ⊔ b = max a b :=
-le_antisymm (sup_le (le_max_left _ _) (le_max_right _ _))
-  (max_le le_sup_left le_sup_right)
-
-lemma inf_eq_min {a b : enat} : a ⊓ b = min a b := rfl
-
 instance : ordered_add_comm_monoid enat :=
 { add_le_add_left := λ a b ⟨h₁, h₂⟩ c,
     enat.cases_on c (by simp)

src/data/nat/lattice.lean

@@ -183,7 +183,14 @@ namespace enat
 open_locale classical
 
 noncomputable instance : complete_linear_order enat :=
-{ .. enat.linear_order,
-  .. with_top_order_iso.symm.to_galois_insertion.lift_complete_lattice }
+{ inf := (⊓),
+  sup := (⊔),
+  top := ⊤,
+  bot := ⊥,
+  le := (≤),
+  lt := (<),
+  .. enat.lattice,
+  .. with_top_order_iso.symm.to_galois_insertion.lift_complete_lattice,
+  .. enat.linear_order, }
 
 end enat

src/data/real/ennreal.lean

@@ -77,16 +77,13 @@ variables {α : Type*} {β : Type*}
 @[derive [
   has_zero, add_comm_monoid,
   canonically_ordered_comm_semiring, complete_linear_order, densely_ordered, nontrivial,
-  canonically_linear_ordered_add_monoid, has_sub, has_ordered_sub]]
+  canonically_linear_ordered_add_monoid, has_sub, has_ordered_sub,
+  linear_ordered_add_comm_monoid_with_top]]
 def ennreal := with_top ℝ≥0
 
 localized "notation `ℝ≥0∞` := ennreal" in ennreal
 localized "notation `∞` := (⊤ : ennreal)" in ennreal
 
-noncomputable instance : linear_ordered_add_comm_monoid ℝ≥0∞ :=
-{ .. ennreal.canonically_ordered_comm_semiring,
-  .. ennreal.complete_linear_order }
-
 -- TODO: why are the two covariant instances necessary? why aren't they inferred?
 instance covariant_class_mul : covariant_class ℝ≥0∞ ℝ≥0∞ (*) (≤) :=
 canonically_ordered_comm_semiring.to_covariant_mul_le
@@ -273,8 +270,8 @@ lemma supr_ennreal {α : Type*} [complete_lattice α] {f : ℝ≥0∞ → α} :
   (⨆ n, f n) = (⨆ n : ℝ≥0, f n) ⊔ f ∞ :=
 @infi_ennreal (order_dual α) _ _
 
-@[simp] lemma add_top : a + ∞ = ∞ := with_top.add_top
-@[simp] lemma top_add : ∞ + a = ∞ := with_top.top_add
+@[simp] lemma add_top : a + ∞ = ∞ := add_top _
+@[simp] lemma top_add : ∞ + a = ∞ := top_add _
 
 /-- Coercion `ℝ≥0 → ℝ≥0∞` as a `ring_hom`. -/
 noncomputable def of_nnreal_hom : ℝ≥0 →+* ℝ≥0∞ :=

src/order/bounded_order.lean

@@ -317,9 +317,11 @@ instance Prop.bounded_order : bounded_order Prop :=
   bot          := false,
   bot_le       := @false.elim }
 
+instance Prop.le_is_total : is_total Prop (≤) :=
+⟨λ p q, by { change (p → q) ∨ (q → p), tauto! }⟩
+
 noncomputable instance Prop.linear_order : linear_order Prop :=
-@lattice.to_linear_order Prop _ (classical.dec_eq _) (classical.dec_rel _) (classical.dec_rel _) $
-λ p q, by { change (p → q) ∨ (q → p), tauto! }
+by classical; exact lattice.to_linear_order Prop
 
 @[simp] lemma le_Prop_eq : ((≤) : Prop → Prop → Prop) = (→) := rfl
 @[simp] lemma sup_Prop_eq : (⊔) = (∨) := rfl
@@ -586,13 +588,16 @@ lemma coe_inf [semilattice_inf α] (a b : α) : ((a ⊓ b : α) : with_bot α) =
 instance lattice [lattice α] : lattice (with_bot α) :=
 { ..with_bot.semilattice_sup, ..with_bot.semilattice_inf }
 
-instance linear_order [linear_order α] : linear_order (with_bot α) :=
-lattice.to_linear_order _ $ λ o₁ o₂,
+instance le_is_total [preorder α] [is_total α (≤)] : is_total (with_bot α) (≤) :=
+⟨λ o₁ o₂,
 begin
   cases o₁ with a, {exact or.inl bot_le},
   cases o₂ with b, {exact or.inr bot_le},
-  simp [le_total]
-end
+  exact (total_of (≤) a b).imp some_le_some.mpr some_le_some.mpr,
+end⟩
+
+instance linear_order [linear_order α] : linear_order (with_bot α) :=
+lattice.to_linear_order _
 
 @[norm_cast] -- this is not marked simp because the corresponding with_top lemmas are used
 lemma coe_min [linear_order α] (x y : α) : ((min x y : α) : with_bot α) = min x y := rfl
@@ -834,13 +839,16 @@ lemma coe_sup [semilattice_sup α] (a b : α) : ((a ⊔ b : α) : with_top α) =
 instance lattice [lattice α] : lattice (with_top α) :=
 { ..with_top.semilattice_sup, ..with_top.semilattice_inf }
 
-instance linear_order [linear_order α] : linear_order (with_top α) :=
-lattice.to_linear_order _ $ λ o₁ o₂,
+instance le_is_total [preorder α] [is_total α (≤)] : is_total (with_top α) (≤) :=
+⟨λ o₁ o₂,
 begin
   cases o₁ with a, {exact or.inr le_top},
   cases o₂ with b, {exact or.inl le_top},
-  simp [le_total]
-end
+  exact (total_of (≤) a b).imp some_le_some.mpr some_le_some.mpr,
+end⟩
+
+instance linear_order [linear_order α] : linear_order (with_top α) :=
+lattice.to_linear_order _
 
 @[simp, norm_cast]
 lemma coe_min [linear_order α] (x y : α) : ((min x y : α) : with_top α) = min x y := rfl

src/order/complete_lattice.lean

@@ -262,7 +262,8 @@ def complete_lattice_of_complete_semilattice_Sup (α : Type*) [complete_semilatt
 complete_lattice_of_Sup α (λ s, is_lub_Sup s)
 
 /-- A complete linear order is a linear order whose lattice structure is complete. -/
-class complete_linear_order (α : Type*) extends complete_lattice α, linear_order α
+class complete_linear_order (α : Type*) extends complete_lattice α,
+  linear_order α renaming max → sup min → inf
 
 namespace order_dual
 variable (α)

src/order/conditionally_complete_lattice.lean

@@ -87,7 +87,7 @@ complete linear orders, we prefix Inf and Sup by a c everywhere. The same statem
 hold in both worlds, sometimes with additional assumptions of nonemptiness or
 boundedness.-/
 class conditionally_complete_linear_order (α : Type*)
-  extends conditionally_complete_lattice α, linear_order α
+  extends conditionally_complete_lattice α, linear_order α renaming max → sup min → inf
 
 /-- A conditionally complete linear order with `bot` is a linear order with least element, in which
 every nonempty subset which is bounded above has a supremum, and every nonempty subset (necessarily

src/order/lattice.lean

@@ -645,24 +645,33 @@ instance linear_order.to_lattice {α : Type u} [o : linear_order α] :
 theorem sup_eq_max [linear_order α] {x y : α} : x ⊔ y = max x y := rfl
 theorem inf_eq_min [linear_order α] {x y : α} : x ⊓ y = min x y := rfl
 
+lemma sup_eq_max_default [semilattice_sup α] [decidable_rel ((≤) : α → α → Prop)]
+  [is_total α (≤)] : (⊔) = (max_default : α → α → α) :=
+begin
+  ext x y,
+  dunfold max_default,
+  split_ifs with h',
+  exacts [sup_of_le_left h', sup_of_le_right $ (total_of (≤) x y).resolve_right h']
+end
+
+lemma inf_eq_min_default [semilattice_inf α] [decidable_rel ((≤) : α → α → Prop)]
+  [is_total α (≤)] : (⊓) = (min_default : α → α → α) :=
+@sup_eq_max_default (order_dual α) _ _ _
+
 /-- A lattice with total order is a linear order.
 
 See note [reducible non-instances]. -/
 @[reducible] def lattice.to_linear_order (α : Type u) [lattice α] [decidable_eq α]
   [decidable_rel ((≤) : α → α → Prop)] [decidable_rel ((<) : α → α → Prop)]
-  (h : ∀ x y : α, x ≤ y ∨ y ≤ x) :
+  [is_total α (≤)] :
   linear_order α :=
 { decidable_le := ‹_›, decidable_eq := ‹_›, decidable_lt := ‹_›,
-  le_total := h,
+  le_total := total_of (≤),
   max := (⊔),
-  max_def := by
-  { funext x y, dunfold max_default,
-    split_ifs with h', exacts [sup_of_le_left h', sup_of_le_right $ (h x y).resolve_right h'] },
+  max_def := sup_eq_max_default,
   min := (⊓),
-  min_def := by
-  { funext x y, dunfold min_default,
-    split_ifs with h', exacts [inf_of_le_left h', inf_of_le_right $ (h x y).resolve_left h'] },
-  .. ‹lattice α› }
+  min_def := inf_eq_min_default,
+  ..‹lattice α› }
 
 @[priority 100] -- see Note [lower instance priority]
 instance linear_order.to_distrib_lattice {α : Type u} [o : linear_order α] :