chore: make argument to mul_inv_cancel implicit (leanprover#737)

This matches mathlib3.

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -212,7 +212,7 @@ theorem mul_inv_cancel_left₀ (h : a ≠ 0) (b : G₀) : a * (a⁻¹ * b) = b :
 
 -- Porting note: used `simpa` to prove `False` in lean3
 theorem inv_ne_zero (h : a ≠ 0) : a⁻¹ ≠ 0 := fun a_eq_0 => by
-  have := mul_inv_cancel a h
+  have := mul_inv_cancel h
   simp [a_eq_0] at this
 
 @[simp]
@@ -289,7 +289,7 @@ theorem mul_self_mul_inv (a : G₀) : a * a * a⁻¹ = a := by
   by_cases h : a = 0
   · rw [h, inv_zero, mul_zero]
 
-  · rw [mul_assoc, mul_inv_cancel _ h, mul_one]
+  · rw [mul_assoc, mul_inv_cancel h, mul_one]
 
 
 /-- Multiplying `a` by its inverse and then by itself results in `a`
@@ -299,7 +299,7 @@ theorem mul_inv_mul_self (a : G₀) : a * a⁻¹ * a = a := by
   by_cases h : a = 0
   · rw [h, inv_zero, mul_zero]
 
-  · rw [mul_inv_cancel _ h, one_mul]
+  · rw [mul_inv_cancel h, one_mul]
 
 
 /-- Multiplying `a⁻¹` by `a` twice results in `a` (whether or not `a`
@@ -356,7 +356,7 @@ theorem eq_zero_of_one_div_eq_zero {a : G₀} (h : 1 / a = 0) : a = 0 :=
   Classical.byCases (fun ha => ha) fun ha => ((one_div_ne_zero ha) h).elim
 
 theorem mul_left_surjective₀ {a : G₀} (h : a ≠ 0) : Surjective fun g => a * g := fun g =>
-  ⟨a⁻¹ * g, by simp [← mul_assoc, mul_inv_cancel _ h]⟩
+  ⟨a⁻¹ * g, by simp [← mul_assoc, mul_inv_cancel h]⟩
 
 theorem mul_right_surjective₀ {a : G₀} (h : a ≠ 0) : Surjective fun g => g * a := fun g =>
   ⟨g * a⁻¹, by simp [mul_assoc, inv_mul_cancel h]⟩

Mathlib/Algebra/GroupWithZero/Defs.lean

@@ -114,8 +114,11 @@ class GroupWithZero (G₀ : Type u) extends MonoidWithZero G₀, DivInvMonoid G
   /-- Every nonzero element of a group with zero is invertible. -/
   mul_inv_cancel (a : G₀) : a ≠ 0 → a * a⁻¹ = 1
 
-export GroupWithZero (inv_zero mul_inv_cancel)
-attribute [simp] inv_zero mul_inv_cancel
+export GroupWithZero (inv_zero)
+attribute [simp] inv_zero
+
+@[simp] lemma mul_inv_cancel [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) : a * a⁻¹ = 1 :=
+GroupWithZero.mul_inv_cancel a h
 
 /-- A type `G₀` is a commutative “group with zero”
 if it is a commutative monoid with zero element (distinct from `1`)

Mathlib/Algebra/GroupWithZero/InjSurj.lean

@@ -202,7 +202,7 @@ protected def Function.Injective.groupWithZero [Zero G₀'] [Mul G₀'] [One G
     pullback_nonzero f zero one with
     inv_zero := hf <| by erw [inv, zero, inv_zero],
     mul_inv_cancel := fun x hx => hf <| by
-      erw [one, mul, inv, mul_inv_cancel _ ((hf.ne_iff' zero).2 hx)] }
+      erw [one, mul, inv, mul_inv_cancel ((hf.ne_iff' zero).2 hx)] }
 #align function.injective.group_with_zero Function.Injective.groupWithZero
 
 /-- Pushforward a `GroupWithZero` along an surjective function.
@@ -217,7 +217,7 @@ protected def Function.Surjective.groupWithZero [Zero G₀'] [Mul G₀'] [One G
   { hf.monoidWithZero f zero one mul npow, hf.divInvMonoid f one mul inv div npow zpow with
     inv_zero := by erw [← zero, ← inv, inv_zero],
     mul_inv_cancel := hf.forall.2 fun x hx => by
-        erw [← inv, ← mul, mul_inv_cancel _ (mt (congr_arg f) <| fun h ↦ hx (h.trans zero)), one]
+        erw [← inv, ← mul, mul_inv_cancel (mt (congr_arg f) <| fun h ↦ hx (h.trans zero)), one]
     exists_pair_ne := ⟨0, 1, h01⟩ }
 #align function.surjective.group_with_zero Function.Surjective.groupWithZero