chore: don't inline DivInvMonoid default value for Div, for bette…

…r instance transparency (#1897)

See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Instance.20transparency.20issue.3F/near/323637092).  This will make particular `DivInvMonoid`s whose `Div` field is constructed using the default value (such as `ℝ`) behave the same way as generic ones, at the instance transparency level, fixing examples such as the following:

```lean
import Mathlib.Data.Real.Basic

variable [LinearOrderedField α]

/- `.reducible` transparency works correctly over `ℝ`. -/
example {a b : ℝ} : a / 2 ≤ b / 2 := by
  with_reducible (apply mul_le_mul) -- fails, as desired

/- `.instance` transparency works correctly over a generic field. -/
example {a b : α} : a / 2 ≤ b / 2 := by
  with_reducible_and_instances (apply mul_le_mul) -- fails, as desired

/- `.instance` transparency does not work correctly over `ℝ`. -/
example {a b : ℝ} : a / 2 ≤ b / 2 := by
  with_reducible_and_instances (apply mul_le_mul) -- succeeds, wanted it not to
  all_goals sorry
```

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -102,7 +102,9 @@ theorem normUnit_one : normUnit (1 : α) = 1 :=
 /-- Chooses an element of each associate class, by multiplying by `normUnit` -/
 def normalize : α →*₀ α where
   toFun x := x * normUnit x
-  map_zero' := by simp only [normUnit_zero, Units.val_one, mul_one]
+  map_zero' := by
+    simp only [normUnit_zero]
+    exact mul_one (0:α)
   map_one' := by dsimp only; rw [normUnit_one, one_mul]; rfl
   map_mul' x y :=
     (by_cases fun hx : x = 0 => by dsimp only; rw [hx, zero_mul, zero_mul, zero_mul]) fun hx =>

Mathlib/Algebra/Group/Defs.lean

@@ -809,6 +809,14 @@ As a consequence, a few natural structures do not fit in this framework. For exa
 respects everything except for the fact that `(0 * ∞)⁻¹ = 0⁻¹ = ∞` while `∞⁻¹ * 0⁻¹ = 0 * ∞ = 0`.
 -/
 
+/-- In a class equipped with instances of both `Monoid` and `Inv`, this definition records what the
+default definition for `Div` would be: `a * b⁻¹`.  This is later provided as the default value for
+the `Div` instance in `DivInvMonoid`.
+
+We keep it as a separate definition rather than inlining it in `DivInvMonoid` so that the `Div`
+field of individual `DivInvMonoid`s constructed using that default value will not be unfolded at
+`.instance` transparency. -/
+def DivInvMonoid.div' {G : Type u} [Monoid G] [Inv G] (a b : G) : G := a * b⁻¹
 
 /-- A `DivInvMonoid` is a `Monoid` with operations `/` and `⁻¹` satisfying
 `div_eq_mul_inv : ∀ a b, a / b = a * b⁻¹`.
@@ -829,7 +837,7 @@ in diamonds. See the definition of `Monoid` and Note [forgetful inheritance] for
 explanations on this.
 -/
 class DivInvMonoid (G : Type u) extends Monoid G, Inv G, Div G where
-  div a b := a * b⁻¹
+  div := DivInvMonoid.div'
   /-- `a / b := a * b⁻¹` -/
   div_eq_mul_inv : ∀ a b : G, a / b = a * b⁻¹ := by intros; rfl
   /-- The power operation: `a ^ n = a * ··· * a`; `a ^ (-n) = a⁻¹ * ··· a⁻¹` (`n` times) -/
@@ -843,6 +851,17 @@ class DivInvMonoid (G : Type u) extends Monoid G, Inv G, Div G where
   zpow_neg' (n : ℕ) (a : G) : zpow (Int.negSucc n) a = (zpow n.succ a)⁻¹ := by intros; rfl
 #align div_inv_monoid DivInvMonoid
 
+/-- In a class equipped with instances of both `AddMonoid` and `Neg`, this definition records what
+the default definition for `Sub` would be: `a + -b`.  This is later provided as the default value
+for the `Sub` instance in `SubNegMonoid`.
+
+We keep it as a separate definition rather than inlining it in `SubNegMonoid` so that the `Sub`
+field of individual `SubNegMonoid`s constructed using that default value will not be unfolded at
+`.instance` transparency. -/
+def SubNegMonoid.sub' {G : Type u} [AddMonoid G] [Neg G] (a b : G) : G := a + -b
+
+attribute [to_additive existing SubNegMonoid.sub'] DivInvMonoid.div'
+
 /-- A `SubNegMonoid` is an `AddMonoid` with unary `-` and binary `-` operations
 satisfying `sub_eq_add_neg : ∀ a b, a - b = a + -b`.
 
@@ -861,7 +880,7 @@ in diamonds. See the definition of `AddMonoid` and Note [forgetful inheritance]
 explanations on this.
 -/
 class SubNegMonoid (G : Type u) extends AddMonoid G, Neg G, Sub G where
-  sub a b := a + -b
+  sub := SubNegMonoid.sub'
   sub_eq_add_neg : ∀ a b : G, a - b = a + -b := by intros; rfl
   zsmul : ℤ → G → G := zsmulRec
   zsmul_zero' : ∀ a : G, zsmul 0 a = 0 := by intros; rfl

Mathlib/Algebra/Order/WithZero.lean

@@ -206,11 +206,19 @@ theorem mul_lt_right₀ (c : α) (h : a < b) (hc : c ≠ 0) : a * c < b * c := b
 #align mul_lt_right₀ mul_lt_right₀
 
 theorem inv_lt_inv₀ (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ < b⁻¹ ↔ b < a :=
-  show (Units.mk0 a ha)⁻¹ < (Units.mk0 b hb)⁻¹ ↔ Units.mk0 b hb < Units.mk0 a ha from inv_lt_inv_iff
+  show (Units.mk0 a ha)⁻¹ < (Units.mk0 b hb)⁻¹ ↔ Units.mk0 b hb < Units.mk0 a ha from
+    have : CovariantClass αˣ αˣ (· * ·) (· < ·) :=
+      LeftCancelSemigroup.covariant_mul_lt_of_covariant_mul_le αˣ
+    inv_lt_inv_iff
 #align inv_lt_inv₀ inv_lt_inv₀
 
 theorem inv_le_inv₀ (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a :=
-  show (Units.mk0 a ha)⁻¹ ≤ (Units.mk0 b hb)⁻¹ ↔ Units.mk0 b hb ≤ Units.mk0 a ha from inv_le_inv_iff
+  show (Units.mk0 a ha)⁻¹ ≤ (Units.mk0 b hb)⁻¹ ↔ Units.mk0 b hb ≤ Units.mk0 a ha from
+    have : CovariantClass αˣ αˣ (Function.swap (· * ·)) (· ≤ ·) :=
+      OrderedCommMonoid.to_covariantClass_right αˣ
+    have : CovariantClass αˣ αˣ (· * ·) (· ≤ ·) :=
+      OrderedCommGroup.to_covariantClass_left_le αˣ
+    inv_le_inv_iff
 #align inv_le_inv₀ inv_le_inv₀
 
 theorem lt_of_mul_lt_mul_of_le₀ (h : a * b < c * d) (hc : 0 < c) (hh : c ≤ a) : b < d := by

test/InstanceTransparency.lean

@@ -0,0 +1,28 @@
+import Mathlib.Data.Real.Basic
+
+/-! # Test transparency level of `Div` field in `DivInvMonoid`
+
+It is desirable that particular `DivInvMonoid`s have their `Div` instance not unfold at `.instance`
+transparency level, in the same way that the `Div` field of a generic `DivInvMonoid` does not.
+
+To ensure this, in examples where the `Div` field is defined as `fun a b ↦ a * b⁻¹`, we hide this
+under one layer of other function (so for example the `Div` instance for `Rat` is defined to be
+`⟨Rat.div⟩`, where `Rat.div` is defined to be `fun a b ↦ a * b⁻¹`).
+
+This file checks that this and similar tricks have had the desired effect:
+`with_reducible_and_instances apply mul_le_mul` fails although `apply mul_le_mul` succeeds.
+-/
+
+example {a b : α} [LinearOrderedField α] : a / 2 ≤ b / 2 := by
+  fail_if_success with_reducible_and_instances apply mul_le_mul -- fails, as desired
+  sorry
+
+example {a b : ℚ} : a / 2 ≤ b / 2 := by
+  fail_if_success with_reducible_and_instances apply mul_le_mul -- fails, as desired
+  apply mul_le_mul
+  repeat sorry
+
+example {a b : ℝ} : a / 2 ≤ b / 2 := by
+  fail_if_success with_reducible_and_instances apply mul_le_mul -- fails, as desired
+  apply mul_le_mul
+  repeat sorry