chore(EReal): clean up instances (leanprover-community#37300)

This PR uses `deriving` to generate most instances on `EReal`.

Previously, there was a diamond because the `Top` instance was declared only after the `CompleteLinearOrder` instance, meaning there were two `Top` instances that weren't defeq in `reducible_and_instances`.

Author: JovanGerb

Mathlib/Data/EReal/Basic.lean

@@ -32,41 +32,16 @@ noncomputable section
 
 /-- The type of extended real numbers `[-∞, ∞]`, constructed as `WithBot (WithTop ℝ)`. -/
 def EReal := WithBot (WithTop ℝ)
-  deriving Bot, Zero, One, Nontrivial, AddMonoid, PartialOrder, AddCommMonoid
-
-instance : ZeroLEOneClass EReal := inferInstanceAs (ZeroLEOneClass (WithBot (WithTop ℝ)))
-instance : SupSet EReal := inferInstanceAs (SupSet (WithBot (WithTop ℝ)))
-instance : InfSet EReal := inferInstanceAs (InfSet (WithBot (WithTop ℝ)))
-
-instance : CompleteLinearOrder EReal :=
-  inferInstanceAs (CompleteLinearOrder (WithBot (WithTop ℝ)))
-
-instance : LinearOrder EReal :=
-  inferInstanceAs (LinearOrder (WithBot (WithTop ℝ)))
-
-instance : IsOrderedAddMonoid EReal :=
-  inferInstanceAs (IsOrderedAddMonoid (WithBot (WithTop ℝ)))
-
-instance : AddCommMonoidWithOne EReal :=
-  inferInstanceAs (AddCommMonoidWithOne (WithBot (WithTop ℝ)))
-
-instance : DenselyOrdered EReal :=
-  inferInstanceAs (DenselyOrdered (WithBot (WithTop ℝ)))
-
-instance : CharZero EReal := inferInstanceAs (CharZero (WithBot (WithTop ℝ)))
+deriving Nontrivial,
+  Zero, One, AddMonoid, AddCommMonoid, AddCommMonoidWithOne, CharZero,
+  Top, Bot, SupSet, InfSet, PartialOrder, LinearOrder, CompleteLinearOrder, DenselyOrdered,
+  ZeroLEOneClass, IsOrderedAddMonoid
 
 /-- The canonical inclusion from reals to ereals. Registered as a coercion. -/
 @[coe] def Real.toEReal : ℝ → EReal := WithBot.some ∘ WithTop.some
 
 namespace EReal
 
--- things unify with `WithBot.decidableLT` later if we don't provide this explicitly.
-instance decidableLT : DecidableLT EReal :=
-  WithBot.decidableLT
-
--- TODO: Provide explicitly, otherwise it is inferred noncomputably from `CompleteLinearOrder`
-instance : Top EReal := ⟨WithBot.some ⊤⟩
-
 instance : Coe ℝ EReal := ⟨Real.toEReal⟩
 
 theorem coe_strictMono : StrictMono Real.toEReal :=
@@ -383,7 +358,6 @@ lemma toReal_pos {x : EReal} (hx : 0 < x) (h'x : x ≠ ⊤) : 0 < x.toReal := by
   lift x to ℝ using by aesop
   simpa using hx
 
-set_option backward.isDefEq.respectTransparency false in
 lemma toReal_neg {x : EReal} (hx : x < 0) (h'x : x ≠ ⊥) : x.toReal < 0 := by
   lift x to ℝ using by aesop
   simpa using hx
@@ -398,7 +372,6 @@ lemma toReal_neg {x : EReal} (hx : x < 0) (h'x : x ≠ ⊥) : x.toReal < 0 := by
     use (x : EReal)
     simpa using hx
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp] lemma toReal_image_Ioo_bot_zero : toReal '' (Ioo ⊥ 0) = Iio 0 := by
   ext x
   constructor
@@ -424,7 +397,6 @@ theorem le_coe_toReal {x : EReal} (h : x ≠ ⊤) : x ≤ x.toReal := by
   · simp only [h', bot_le]
   · simp only [le_refl, coe_toReal h h']
 
-set_option backward.isDefEq.respectTransparency false in
 theorem coe_toReal_le {x : EReal} (h : x ≠ ⊥) : ↑x.toReal ≤ x := by
   by_cases h' : x = ⊤
   · simp only [h', le_top]
@@ -515,10 +487,9 @@ lemma preimage_coe_Ioi (x : ℝ) : Real.toEReal ⁻¹' Ioi x = Ioi x := by
   refine preimage_comp.trans ?_
   simp only [WithBot.preimage_coe_Ioi, WithTop.preimage_coe_Ioi]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma preimage_coe_Ioi_bot : Real.toEReal ⁻¹' Ioi ⊥ = univ := by
-  change (WithBot.some ∘ WithTop.some) ⁻¹' (Ioi ⊥) = _
+  change ((WithBot.some ∘ WithTop.some) ⁻¹' (Ioi (⊥ : WithBot (WithTop ℝ))) : Set ℝ) = _
   refine preimage_comp.trans ?_
   simp only [WithBot.preimage_coe_Ioi_bot, preimage_univ]
 
@@ -534,10 +505,9 @@ lemma preimage_coe_Iio (y : ℝ) : Real.toEReal ⁻¹' Iio y = Iio y := by
   refine preimage_comp.trans ?_
   simp only [WithBot.preimage_coe_Iio, WithTop.preimage_coe_Iio]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma preimage_coe_Iio_top : Real.toEReal ⁻¹' Iio ⊤ = univ := by
-  change (WithBot.some ∘ WithTop.some) ⁻¹' (Iio (WithBot.some ⊤)) = _
+  change (WithBot.some ∘ WithTop.some) ⁻¹' (Iio (WithBot.some (⊤ : WithTop ℝ))) = _
   refine preimage_comp.trans ?_
   simp only [WithBot.preimage_coe_Iio, WithTop.preimage_coe_Iio_top]
 
@@ -741,7 +711,6 @@ lemma toENNReal_of_nonpos {x : EReal} (hx : x ≤ 0) : x.toENNReal = 0 := by
 lemma toENNReal_bot : (⊥ : EReal).toENNReal = 0 := toENNReal_of_nonpos bot_le
 lemma toENNReal_zero : (0 : EReal).toENNReal = 0 := toENNReal_of_nonpos le_rfl
 
-set_option backward.isDefEq.respectTransparency false in
 lemma toENNReal_eq_zero_iff {x : EReal} : x.toENNReal = 0 ↔ x ≤ 0 := by
   induction x <;> simp [toENNReal]
 
@@ -786,7 +755,6 @@ lemma toENNReal_eq_toENNReal {x y : EReal} (hx : 0 ≤ x) (hy : 0 ≤ y) :
     x.toENNReal = y.toENNReal ↔ x = y := by
   induction x <;> induction y <;> simp_all
 
-set_option backward.isDefEq.respectTransparency false in
 lemma toENNReal_le_toENNReal {x y : EReal} (h : x ≤ y) : x.toENNReal ≤ y.toENNReal := by
   induction x
   · simp

Mathlib/Data/EReal/Inv.lean

@@ -493,7 +493,6 @@ private lemma exists_lt_mul_right_of_nonneg (ha : 0 ≤ a) (hc : 0 ≤ c) (h : c
   simp_rw [mul_comm a] at h ⊢
   exact exists_lt_mul_left_of_nonneg hb.le hc h
 
-set_option backward.isDefEq.respectTransparency false in
 private lemma exists_mul_left_lt (h₁ : a ≠ 0 ∨ b ≠ ⊤) (h₂ : a ≠ ⊤ ∨ 0 < b) (hc : a * b < c) :
     ∃ a' ∈ Ioo a ⊤, a' * b < c := by
   rcases eq_top_or_lt_top a with rfl | a_top

Mathlib/Data/EReal/Operations.lean

@@ -127,7 +127,6 @@ lemma toENNReal_add_le {x y : EReal} : (x + y).toENNReal ≤ x.toENNReal + y.toE
   induction x <;> induction y <;> try {· simp}
   exact ENNReal.ofReal_add_le
 
-set_option backward.isDefEq.respectTransparency false in
 theorem addLECancellable_coe (x : ℝ) : AddLECancellable (x : EReal)
   | _, ⊤, _ => le_top
   | ⊥, _, _ => bot_le
@@ -150,7 +149,6 @@ theorem add_lt_add {x y z t : EReal} (h1 : x < y) (h2 : z < t) : x + z < y + t :
     calc (x : EReal) + z < x + t := add_lt_add_left_coe h2 _
     _ ≤ y + t := by gcongr
 
-set_option backward.isDefEq.respectTransparency false in
 theorem add_lt_add_of_lt_of_le' {x y z t : EReal} (h : x < y) (h' : z ≤ t) (hbot : t ≠ ⊥)
     (htop : t = ⊤ → z = ⊤ → x = ⊥) : x + z < y + t := by
   rcases h'.eq_or_lt with (rfl | hlt)
@@ -372,20 +370,16 @@ lemma sub_self {x : EReal} (h_top : x ≠ ⊤) (h_bot : x ≠ ⊥) : x - x = 0 :
 lemma sub_self_le_zero {x : EReal} : x - x ≤ 0 := by
   cases x <;> simp
 
-set_option backward.isDefEq.respectTransparency false in
 lemma sub_nonneg {x y : EReal} (h_top : x ≠ ⊤ ∨ y ≠ ⊤) (h_bot : x ≠ ⊥ ∨ y ≠ ⊥) :
     0 ≤ x - y ↔ y ≤ x := by
   cases x <;> cases y <;> simp_all [← EReal.coe_sub]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma sub_nonpos {x y : EReal} : x - y ≤ 0 ↔ x ≤ y := by
   cases x <;> cases y <;> simp [← EReal.coe_sub]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma sub_pos {x y : EReal} : 0 < x - y ↔ y < x := by
   cases x <;> cases y <;> simp [← EReal.coe_sub]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma sub_neg {x y : EReal} (h_top : x ≠ ⊤ ∨ y ≠ ⊤) (h_bot : x ≠ ⊥ ∨ y ≠ ⊥) :
     x - y < 0 ↔ x < y := by
   cases x <;> cases y <;> simp_all [← EReal.coe_sub]
@@ -442,7 +436,6 @@ lemma sub_add_cancel_right {a : EReal} {b : Real} : b - (a + b) = -a := by
 lemma sub_add_cancel_left {a : EReal} {b : Real} : b - (b + a) = -a := by
   rw [add_comm, sub_add_cancel_right]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma le_sub_iff_add_le {a b c : EReal} (hb : b ≠ ⊥ ∨ c ≠ ⊥) (ht : b ≠ ⊤ ∨ c ≠ ⊤) :
     a ≤ c - b ↔ a + b ≤ c := by
   induction b with
@@ -637,7 +630,6 @@ instance : NoZeroDivisors EReal where
     · rcases lt_or_gt_of_ne h.2 with (h | h)
         <;> simp [EReal.top_mul_of_pos, EReal.top_mul_of_neg, h]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma mul_pos_iff {a b : EReal} : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 := by
   induction a, b using EReal.induction₂_symm with
   | symm h => simp [EReal.mul_comm, h, and_comm]
@@ -724,7 +716,6 @@ lemma mul_nonpos_iff {a b : EReal} : a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a 
   nth_rw 1 [← neg_zero]
   rw [EReal.le_neg, ← mul_neg, mul_nonneg_iff, EReal.neg_le, EReal.le_neg, neg_zero]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma mul_eq_top (a b : EReal) :
     a * b = ⊤ ↔ (a = ⊥ ∧ b < 0) ∨ (a < 0 ∧ b = ⊥) ∨ (a = ⊤ ∧ 0 < b) ∨ (0 < a ∧ b = ⊤) := by
   induction a, b using EReal.induction₂_symm with

Mathlib/Topology/Instances/EReal/Lemmas.lean

@@ -100,7 +100,6 @@ theorem continuous_coe_ennreal_iff {f : α → ℝ≥0∞} :
 
 /-! ### Neighborhoods of infinity -/
 
-set_option backward.isDefEq.respectTransparency false in
 theorem nhds_top : 𝓝 (⊤ : EReal) = ⨅ (a) (_ : a ≠ ⊤), 𝓟 (Ioi a) :=
   nhds_top_order.trans <| by simp only [lt_top_iff_ne_top]
 
@@ -138,7 +137,6 @@ theorem tendsto_nhds_bot_iff_real {α : Type*} {m : α → EReal} {f : Filter α
     Tendsto m f (𝓝 ⊥) ↔ ∀ x : ℝ, ∀ᶠ a in f, m a < x :=
   nhds_bot_basis.tendsto_right_iff.trans <| by simp only [true_implies, mem_Iio]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma nhdsWithin_top : 𝓝[≠] (⊤ : EReal) = (atTop).map Real.toEReal := by
   apply (nhdsWithin_hasBasis nhds_top_basis_Ici _).ext (atTop_basis.map Real.toEReal)
   · simp only [EReal.image_coe_Ici, true_and]
@@ -152,7 +150,6 @@ lemma nhdsWithin_top : 𝓝[≠] (⊤ : EReal) = (atTop).map Real.toEReal := by
     refine fun x ↦ ⟨x, ⟨EReal.coe_lt_top x, fun x ⟨(h1 : _ ≤ x), h2⟩ ↦ ?_⟩⟩
     simp [h1, Ne.lt_top' fun a ↦ h2 a.symm]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma nhdsWithin_bot : 𝓝[≠] (⊥ : EReal) = (atBot).map Real.toEReal := by
   apply (nhdsWithin_hasBasis nhds_bot_basis_Iic _).ext (atBot_basis.map Real.toEReal)
   · simp only [EReal.image_coe_Iic,
@@ -288,7 +285,6 @@ lemma limsup_add_bot_of_ne_top (h : limsup u f = ⊥) (h' : limsup v f ≠ ⊤)
   · rw [h]; exact .inl bot_ne_top
   · rw [h, bot_add]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma limsup_add_le_of_le {a b : EReal} (ha : limsup u f < a) (hb : limsup v f ≤ b) :
     limsup (u + v) f ≤ a + b := by
   rcases eq_top_or_lt_top b with rfl | h
@@ -299,7 +295,6 @@ lemma liminf_add_gt_of_gt {a b : EReal} (ha : a < liminf u f) (hb : b < liminf v
     a + b < liminf (u + v) f :=
   (add_lt_add ha hb).trans_le le_liminf_add
 
-set_option backward.isDefEq.respectTransparency false in
 lemma liminf_add_top_of_ne_bot (h : liminf u f = ⊤) (h' : liminf v f ≠ ⊥) :
     liminf (u + v) f = ⊤ := by
   apply top_le_iff.1 (le_trans _ le_liminf_add)
@@ -333,7 +328,6 @@ theorem liminf_const_mul_of_nonpos_of_ne_bot [NeBot f] {c : EReal} (h₁ : c ≤
   simpa [neg_mul, ← Pi.neg_def, limsup_neg] using
     limsup_const_mul_of_nonneg_of_ne_top (c := -c) (by aesop) (by aesop)
 
-set_option backward.isDefEq.respectTransparency false in
 lemma le_limsup_mul (hu : ∃ᶠ x in f, 0 ≤ u x) (hv : 0 ≤ᶠ[f] v) :
     limsup u f * liminf v f ≤ limsup (u * v) f := by
   rcases f.eq_or_neBot with rfl | _