From 0ec98ed0d3bd20fcb6096e46c995534e33246ec3 Mon Sep 17 00:00:00 2001
From: Joseph Myers <jsm@polyomino.org.uk>
Date: Thu, 29 Sep 2022 01:02:47 +0000
Subject: [PATCH] refactor(data/real/ereal): `sub_neg_zero_monoid` instance
 (#16688)

Add a `sub_neg_zero_monoid` instance for `ereal`, so eliminating its `neg_zero`, `sub_zero` and `sub_eq_add_neg` lemmas and allowing results for `neg_zero_class` to be applied to `ereal`.
---
 src/data/real/ereal.lean                          | 15 ++++++++-------
 .../integral/vitali_caratheodory.lean             |  2 +-
 2 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/data/real/ereal.lean b/src/data/real/ereal.lean
index f9371a704457d..dffc98ea3e875 100644
--- a/src/data/real/ereal.lean
+++ b/src/data/real/ereal.lean
@@ -380,7 +380,6 @@ instance : has_neg ereal := ⟨ereal.neg⟩
 
 @[simp] lemma neg_top : - (⊤ : ereal) = ⊥ := rfl
 @[simp] lemma neg_bot : - (⊥ : ereal) = ⊤ := rfl
-@[simp] lemma neg_zero : - (0 : ereal) = 0 := by { change ((-0 : ℝ) : ereal) = 0, simp }
 
 instance : has_involutive_neg ereal :=
 { neg := has_neg.neg,
@@ -402,7 +401,7 @@ by { rw neg_eq_iff_neg_eq, simp [eq_comm] }
 by { rw neg_eq_iff_neg_eq, simp [eq_comm] }
 
 @[simp] lemma neg_eg_zero_iff {x : ereal} : - x = 0 ↔ x = 0 :=
-by { rw neg_eq_iff_neg_eq, simp [eq_comm] }
+by { rw neg_eq_iff_neg_eq, change ((-0 : ℝ) : ereal) = _ ↔ _, simp [eq_comm] }
 
 /-- if `-a ≤ b` then `-b ≤ a` on `ereal`. -/
 protected theorem neg_le_of_neg_le : ∀ {a b : ereal} (h : -a ≤ b), -b ≤ a
@@ -448,11 +447,16 @@ lemma neg_lt_iff_neg_lt {a b : ereal} : -a < b ↔ -b < a :=
 
 /-- Subtraction on `ereal`, defined by `x - y = x + (-y)`. Since addition is badly behaved at some
 points, so is subtraction. There is no standard algebraic typeclass involving subtraction that is
-registered on `ereal` because of this bad behavior. -/
+registered on `ereal`, beyond `sub_neg_zero_monoid`, because of this bad behavior. -/
 protected noncomputable def sub (x y : ereal) : ereal := x + (-y)
 
 noncomputable instance : has_sub ereal := ⟨ereal.sub⟩
 
+noncomputable instance : sub_neg_zero_monoid ereal :=
+{ neg_zero := by { change ((-0 : ℝ) : ereal) = 0, simp },
+  ..(infer_instance : add_monoid ereal),
+  ..ereal.has_neg }
+
 @[simp] lemma top_sub (x : ereal) : ⊤ - x = ⊤ := top_add x
 @[simp] lemma sub_bot (x : ereal) : x - ⊥ = ⊤ := add_top x
 
@@ -460,11 +464,8 @@ noncomputable instance : has_sub ereal := ⟨ereal.sub⟩
 @[simp] lemma bot_sub_coe (x : ℝ) : (⊥ : ereal) - x = ⊥ := rfl
 @[simp] lemma coe_sub_bot (x : ℝ) : (x : ereal) - ⊤ = ⊥ := rfl
 
-@[simp] lemma sub_zero (x : ereal) : x - 0 = x := by { change x + (-0) = x, simp }
 @[simp] lemma zero_sub (x : ereal) : 0 - x = - x := by { change 0 + (-x) = - x, simp }
 
-lemma sub_eq_add_neg (x y : ereal) : x - y = x + -y := rfl
-
 lemma sub_le_sub {x y z t : ereal} (h : x ≤ y) (h' : t ≤ z) : x - z ≤ y - t :=
 add_le_add h (neg_le_neg_iff.2 h')
 
@@ -491,7 +492,7 @@ end
 lemma to_real_sub {x y : ereal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) (hy : y ≠ ⊤) (h'y : y ≠ ⊥) :
   to_real (x - y) = to_real x - to_real y :=
 begin
-  rw [ereal.sub_eq_add_neg, to_real_add hx h'x, to_real_neg],
+  rw [sub_eq_add_neg, to_real_add hx h'x, to_real_neg],
   { refl },
   { simpa using hy },
   { simpa using h'y }
diff --git a/src/measure_theory/integral/vitali_caratheodory.lean b/src/measure_theory/integral/vitali_caratheodory.lean
index 6b3e57b920466..a5c8e8ae91696 100644
--- a/src/measure_theory/integral/vitali_caratheodory.lean
+++ b/src/measure_theory/integral/vitali_caratheodory.lean
@@ -480,7 +480,7 @@ begin
       by { congr' 1, field_simp [δ, mul_comm] },
   show ∀ᵐ (x : α) ∂μ, g x < ⊤,
   { filter_upwards [gp_lt_top] with _ hx,
-    simp [g, ereal.sub_eq_add_neg, lt_top_iff_ne_top, lt_top_iff_ne_top.1 hx], },
+    simp [g, sub_eq_add_neg, lt_top_iff_ne_top, lt_top_iff_ne_top.1 hx], },
   show ∀ x, (f x : ereal) < g x,
   { assume x,
     rw ereal.coe_real_ereal_eq_coe_to_nnreal_sub_coe_to_nnreal (f x),