chore(Data/Sign/Defs): remove backward.privateInPublic (leanprover-community#33197)

Author: vihdzp

Mathlib/Data/Sign/Defs.lean

@@ -76,17 +76,9 @@ protected inductive LE : SignType → SignType → Prop
 instance : LE SignType :=
   ⟨SignType.LE⟩
 
-instance LE.decidableRel : DecidableRel SignType.LE := fun a b => by
+instance : DecidableLE SignType := fun a b => by
   cases a <;> cases b <;> first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)
 
-set_option backward.privateInPublic true in
-private lemma mul_comm : ∀ (a b : SignType), a * b = b * a := by rintro ⟨⟩ ⟨⟩ <;> rfl
-set_option backward.privateInPublic true in
-private lemma mul_assoc : ∀ (a b c : SignType), (a * b) * c = a * (b * c) := by
-  rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
-
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
 so we only define the `CommGroupWithZero`. -/
 instance : CommGroupWithZero SignType where
@@ -96,27 +88,17 @@ instance : CommGroupWithZero SignType where
   mul_one a := by cases a <;> rfl
   one_mul a := by cases a <;> rfl
   mul_inv_cancel a ha := by cases a <;> trivial
-  mul_comm := mul_comm
-  mul_assoc := mul_assoc
+  mul_comm := by decide
+  mul_assoc := by decide
   exists_pair_ne := ⟨0, 1, by rintro ⟨_⟩⟩
   inv_zero := rfl
 
-set_option backward.privateInPublic true in
-private lemma le_antisymm (a b : SignType) (_ : a ≤ b) (_ : b ≤ a) : a = b := by
-  cases a <;> cases b <;> trivial
-
-set_option backward.privateInPublic true in
-private lemma le_trans (a b c : SignType) (_ : a ≤ b) (_ : b ≤ c) : a ≤ c := by
-  cases a <;> cases b <;> cases c <;> tauto
-
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 instance : LinearOrder SignType where
   le_refl a := by cases a <;> constructor
-  le_total a b := by cases a <;> cases b <;> first | left; constructor | right; constructor
-  le_antisymm := le_antisymm
-  le_trans := le_trans
-  toDecidableLE := LE.decidableRel
+  le_total := by decide
+  le_antisymm := by decide
+  le_trans := by decide
+  toDecidableLE := instDecidableLE
 
 instance : BoundedOrder SignType where
   top := 1