refactor(group_theory/monoid_localization): flip the direction of mul…

…tiplication (#15584)

In a future PR, this will allow `localization` and `module_localization` to be defeq.
Mathematically this makes no difference.

For now, only the primed `localization.r'` is defeq to `localized_module.r`.





Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>

src/algebra/module/localized_module.lean

@@ -46,26 +46,30 @@ variables (M : Type v) [add_comm_monoid M] [module R M]
 
 /--The equivalence relation on `M × S` where `(m1, s1) ≈ (m2, s2)` if and only if
 for some (u : S), u * (s2 • m1 - s1 • m2) = 0-/
-def r : (M × S) → (M × S) → Prop
-| ⟨m1, s1⟩ ⟨m2, s2⟩ := ∃ (u : S), u • s1 • m2 = u • s2 • m1
+def r (a b : M × S) : Prop :=
+∃ (u : S), u • b.2 • a.1 = u • a.2 • b.1
 
 lemma r.is_equiv : is_equiv _ (r S M) :=
 { refl := λ ⟨m, s⟩, ⟨1, by rw [one_smul]⟩,
   trans := λ ⟨m1, s1⟩ ⟨m2, s2⟩ ⟨m3, s3⟩ ⟨u1, hu1⟩ ⟨u2, hu2⟩, begin
     use u1 * u2 * s2,
     -- Put everything in the same shape, sorting the terms using `simp`
-    have hu1' := congr_arg ((•) (u2 * s3)) hu1,
-    have hu2' := congr_arg ((•) (u1 * s1)) hu2,
+    have hu1' := congr_arg ((•) (u2 * s3)) hu1.symm,
+    have hu2' := congr_arg ((•) (u1 * s1)) hu2.symm,
     simp only [← mul_smul, smul_assoc, mul_assoc, mul_comm, mul_left_comm] at ⊢ hu1' hu2',
     rw [hu2', hu1']
   end,
   symm := λ ⟨m1, s1⟩ ⟨m2, s2⟩ ⟨u, hu⟩, ⟨u, hu.symm⟩ }
 
-
 instance r.setoid : setoid (M × S) :=
 { r := r S M,
   iseqv := ⟨(r.is_equiv S M).refl, (r.is_equiv S M).symm, (r.is_equiv S M).trans⟩ }
 
+-- TODO: change `localization` to use `r'` instead of `r` so that the two types are also defeq,
+-- `localization S = localized_module S R`.
+example {R} [comm_semiring R] (S : submonoid R) : ⇑(localization.r' S) = localized_module.r S R :=
+rfl
+
 /--
 If `S` is a multiplicative subset of a ring `R` and `M` an `R`-module, then
 we can localize `M` by `S`.
@@ -80,7 +84,7 @@ variables {M S}
 def mk (m : M) (s : S) : localized_module S M :=
 quotient.mk ⟨m, s⟩
 
-lemma mk_eq {m m' : M} {s s' : S} : mk m s = mk m' s' ↔ ∃ (u : S), u • s • m' = u • s' • m :=
+lemma mk_eq {m m' : M} {s s' : S} : mk m s = mk m' s' ↔ ∃ (u : S), u • s' • m = u • s • m' :=
 quotient.eq
 
 @[elab_as_eliminator]
@@ -149,7 +153,7 @@ begin
   rw [one_smul, one_smul],
   congr' 1,
   { rw [mul_assoc] },
-  { rw [mul_comm, add_assoc, mul_smul, mul_smul, ←mul_smul sx sz, mul_comm, mul_smul], },
+  { rw [eq_comm, mul_comm, add_assoc, mul_smul, mul_smul, ←mul_smul sx sz, mul_comm, mul_smul], },
 end
 
 private lemma add_comm' (x y : localized_module S M) :
@@ -207,9 +211,10 @@ instance {A : Type*} [semiring A] [algebra R A] {S : submonoid R} :
       rintros ⟨a₁, s₁⟩ ⟨a₂, s₂⟩ ⟨b₁, t₁⟩ ⟨b₂, t₂⟩ ⟨u₁, e₁⟩ ⟨u₂, e₂⟩,
       rw mk_eq,
       use u₁ * u₂,
-      dsimp only,
+      dsimp only at ⊢ e₁ e₂,
+      rw eq_comm,
       transitivity (u₁ • t₁ • a₁) • u₂ • t₂ • a₂,
-      rw [← e₁, ← e₂], swap, rw eq_comm,
+      rw [e₁, e₂], swap, rw eq_comm,
       all_goals { rw [smul_smul, mul_mul_mul_comm, ← smul_eq_mul, ← smul_eq_mul A,
         smul_smul_smul_comm, mul_smul, mul_smul] }
     end),
@@ -655,8 +660,9 @@ instance localized_module_is_localized_module :
         localized_module.mk_cancel t ],
     end,
   eq_iff_exists := λ m1 m2,
-  { mp := λ eq1, by simpa only [one_smul] using localized_module.mk_eq.mp eq1,
-    mpr := λ ⟨c, eq1⟩, localized_module.mk_eq.mpr ⟨c, by simpa only [one_smul] using eq1⟩ } }
+  { mp := λ eq1, by simpa only [eq_comm, one_smul] using localized_module.mk_eq.mp eq1,
+    mpr := λ ⟨c, eq1⟩,
+      localized_module.mk_eq.mpr ⟨c, by simpa only [eq_comm, one_smul] using eq1⟩ } }
 
 namespace is_localized_module
 
@@ -674,7 +680,7 @@ begin
   generalize_proofs h1 h2,
   erw [module.End_algebra_map_is_unit_inv_apply_eq_iff, ←h2.unit⁻¹.1.map_smul,
     module.End_algebra_map_is_unit_inv_apply_eq_iff', ←linear_map.map_smul, ←linear_map.map_smul],
-  exact ((is_localized_module.eq_iff_exists S f).mpr ⟨c, eq1⟩).symm,
+  exact (is_localized_module.eq_iff_exists S f).mpr ⟨c, eq1⟩,
 end
 
 @[simp] lemma from_localized_module'_mk (m : M) (s : S) :
@@ -894,7 +900,11 @@ by { rw [mk'_add_mk', ← smul_add, mk'_cancel_left] }
 
 lemma mk'_eq_mk'_iff (m₁ m₂ : M) (s₁ s₂ : S) :
   mk' f m₁ s₁ = mk' f m₂ s₂ ↔ ∃ s : S, s • s₁ • m₂ = s • s₂ • m₁ :=
-by { delta mk', rw [(from_localized_module.inj S f).eq_iff, localized_module.mk_eq] }
+begin
+  delta mk',
+  rw [(from_localized_module.inj S f).eq_iff, localized_module.mk_eq],
+  simp_rw eq_comm
+end
 
 lemma mk'_neg {M M' : Type*} [add_comm_group M] [add_comm_group M'] [module R M]
   [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (m : M) (s : S) :

src/algebraic_geometry/Spec.lean

@@ -353,7 +353,7 @@ begin
       _ _ _ (structure_sheaf.is_localization.to_basic_open S $ algebra_map R S r) x).trans this,
     obtain ⟨⟨_, n, rfl⟩, e⟩ := (is_localization.mk'_eq_zero_iff _ _).mp this,
     refine ⟨⟨r, hpr⟩ ^ n, _⟩,
-    rw [submonoid.smul_def, algebra.smul_def, submonoid.coe_pow, subtype.coe_mk, mul_comm, map_pow],
+    rw [submonoid.smul_def, algebra.smul_def, submonoid.coe_pow, subtype.coe_mk, map_pow],
     exact e },
 end
 

src/algebraic_geometry/morphisms/quasi_separated.lean

@@ -340,11 +340,9 @@ begin
       { simp only [X.basic_open_res],
         rintros x ⟨H₁, H₂⟩, exact ⟨h₂ H₁, H₂⟩ } } },
   use n,
-  conv_lhs at e { rw mul_comm },
-  conv_rhs at e { rw mul_comm },
   simp only [pow_add, map_pow, map_mul, ← comp_apply, ← mul_assoc,
     ← functor.map_comp, subtype.coe_mk] at e ⊢,
-  convert e
+  exact e
 end
 
 lemma exists_eq_pow_mul_of_is_compact_of_is_quasi_separated (X : Scheme)
@@ -468,15 +466,15 @@ begin
       using e.symm },
   { intros x y,
     rw [← sub_eq_zero, ← map_sub, ring_hom.algebra_map_to_algebra],
-    simp_rw [← @sub_eq_zero _ _ (x * _) (y * _), ← sub_mul],
+    simp_rw [← @sub_eq_zero _ _ (_ * x) (_ * y), ← mul_sub],
     generalize : x - y = z,
     split,
     { intro H,
       obtain ⟨n, e⟩ := exists_pow_mul_eq_zero_of_res_basic_open_eq_zero_of_is_compact X hU _ _ H,
       refine ⟨⟨_, n, rfl⟩, _⟩,
       simpa [mul_comm z] using e },
-    { rintro ⟨⟨_, n, rfl⟩, e : z * f ^ n = 0⟩,
-      rw [← ((RingedSpace.is_unit_res_basic_open _ f).pow n).mul_left_inj, zero_mul, ← map_pow,
+    { rintro ⟨⟨_, n, rfl⟩, e : f ^ n * z = 0⟩,
+      rw [← ((RingedSpace.is_unit_res_basic_open _ f).pow n).mul_right_inj, mul_zero, ← map_pow,
         ← map_mul, e, map_zero] } }
 end
 

src/algebraic_geometry/projective_spectrum/scheme.lean

@@ -191,11 +191,11 @@ begin
   change localization.mk (f ^ N) 1 = mk (∑ _, _) 1 at eq1,
   simp only [mk_eq_mk', is_localization.eq] at eq1,
   rcases eq1 with ⟨⟨_, ⟨M, rfl⟩⟩, eq1⟩,
-  erw [mul_one, mul_one] at eq1,
-  change f^_ * f^_ = _ * f^_ at eq1,
+  erw [one_mul, one_mul] at eq1,
+  change f^_ * f^_ = f^_ * _ at eq1,
   rw set.not_disjoint_iff_nonempty_inter,
-  refine ⟨f^N * f^M, eq1.symm ▸ mul_mem_right _ _
-    (sum_mem _ (λ i hi, mul_mem_left _ _ _)), ⟨N+M, by rw pow_add⟩⟩,
+  refine ⟨f^M * f^N, eq1.symm ▸ mul_mem_left _ _
+    (sum_mem _ (λ i hi, mul_mem_left _ _ _)), ⟨M + N, by rw pow_add⟩⟩,
   generalize_proofs h₁ h₂,
   exact (classical.some_spec h₂).1,
 end
@@ -220,9 +220,8 @@ def to_fun (x : Proj.T| (pbo f)) : (Spec.T (A⁰_ f)) :=
   simp only [localization.mk_mul, one_mul] at eq1,
   simp only [mk_eq_mk', is_localization.eq] at eq1,
   rcases eq1 with ⟨⟨_, ⟨M, rfl⟩⟩, eq1⟩,
-  rw [submonoid.coe_one, mul_one] at eq1,
-  change _ * _ * f^_ = _ * (f^_ * f^_) * f^_ at eq1,
-
+  rw [submonoid.coe_one, one_mul] at eq1,
+  change f^_ * (_ * _) = f^_ * (f^_ * f^_ * _) at eq1,
   rcases x.1.is_prime.mem_or_mem (show a1 * a2 * f ^ N * f ^ M ∈ _, from _) with h1|rid2,
   rcases x.1.is_prime.mem_or_mem h1 with h1|rid1,
   rcases x.1.is_prime.mem_or_mem h1 with h1|h2,
@@ -234,8 +233,8 @@ def to_fun (x : Proj.T| (pbo f)) : (Spec.T (A⁰_ f)) :=
     exact ideal.mul_mem_right _ _ (ideal.subset_span ⟨_, h2, rfl⟩), },
   { exact false.elim (x.2 (x.1.is_prime.mem_of_pow_mem N rid1)), },
   { exact false.elim (x.2 (x.1.is_prime.mem_of_pow_mem M rid2)), },
-  { rw [mul_comm _ (f^N), eq1],
-    refine mul_mem_right _ _ (mul_mem_right _ _ (sum_mem _ (λ i hi, mul_mem_left _ _ _))),
+  { rw [←mul_comm (f^M), ←mul_comm (f^N), eq1],
+    refine mul_mem_left _ _ (mul_mem_left _ _ (sum_mem _ (λ i hi, mul_mem_left _ _ _))),
     generalize_proofs h₁ h₂, exact (classical.some_spec h₂).1 },
 end⟩
 
@@ -273,16 +272,16 @@ begin
     change localization.mk (f^N) 1 * mk _ _ = mk (∑ _, _) _ at eq1,
     rw [mk_mul, one_mul, mk_eq_mk', is_localization.eq] at eq1,
     rcases eq1 with ⟨⟨_, ⟨M, rfl⟩⟩, eq1⟩,
-    rw [submonoid.coe_one, mul_one] at eq1,
+    rw [submonoid.coe_one, one_mul] at eq1,
     simp only [subtype.coe_mk] at eq1,
 
     rcases y.1.is_prime.mem_or_mem (show a * f ^ N * f ^ M ∈ _, from _) with H1 | H3,
     rcases y.1.is_prime.mem_or_mem H1 with H1 | H2,
     { exact hy2 H1, },
     { exact y.2 (y.1.is_prime.mem_of_pow_mem N H2), },
     { exact y.2 (y.1.is_prime.mem_of_pow_mem M H3), },
-    { rw [mul_comm _ (f^N), eq1],
-      refine mul_mem_right _ _ (mul_mem_right _ _ (sum_mem _ (λ i hi, mul_mem_left _ _ _))),
+    { rw [mul_comm _ (f^N), mul_comm _ (f^M), eq1],
+      refine mul_mem_left _ _ (mul_mem_left _ _ (sum_mem _ (λ i hi, mul_mem_left _ _ _))),
       generalize_proofs h₁ h₂, exact (classical.some_spec h₂).1, }, },
 end
 

src/algebraic_geometry/structure_sheaf.lean

@@ -358,7 +358,8 @@ by convert is_localization.mk'_mul _ f₁ f₂ ⟨g₁, hu₁ x x.2⟩ ⟨g₂,
 
 lemma const_ext {f₁ f₂ g₁ g₂ : R} {U hu₁ hu₂} (h : f₁ * g₂ = f₂ * g₁) :
   const R f₁ g₁ U hu₁ = const R f₂ g₂ U hu₂ :=
-subtype.eq $ funext $ λ x, is_localization.mk'_eq_of_eq h.symm
+subtype.eq $ funext $ λ x, is_localization.mk'_eq_of_eq
+  (by rw [mul_comm, subtype.coe_mk, ←h, mul_comm, subtype.coe_mk])
 
 lemma const_congr {f₁ f₂ g₁ g₂ : R} {U hu} (hf : f₁ = f₂) (hg : g₁ = g₂) :
   const R f₁ g₁ U hu = const R f₂ g₂ U (hg ▸ hu) :=
@@ -575,17 +576,17 @@ begin
   rw is_localization.eq,
   -- We know that the fractions `a/b` and `c/d` are equal as sections of the structure sheaf on
   -- `basic_open f`. We need to show that they agree as elements in the localization of `R` at `f`.
-  -- This amounts showing that `a * d * r = c * b * r`, for some power `r = f ^ n` of `f`.
+  -- This amounts showing that `r * (d * a) = r * (b * c)`, for some power `r = f ^ n` of `f`.
   -- We define `I` as the ideal of *all* elements `r` satisfying the above equation.
   let I : ideal R :=
-  { carrier := {r : R | a * d * r = c * b * r},
-    zero_mem' := by simp only [set.mem_set_of_eq, mul_zero],
-    add_mem' := λ r₁ r₂ hr₁ hr₂, by { dsimp at hr₁ hr₂ ⊢, simp only [mul_add, hr₁, hr₂] },
-    smul_mem' := λ r₁ r₂ hr₂, by { dsimp at hr₂ ⊢, simp only [mul_comm r₁ r₂, ← mul_assoc, hr₂] }},
+  { carrier := {r : R | r * (d * a) = r * (b * c)},
+    zero_mem' := by simp only [set.mem_set_of_eq, zero_mul],
+    add_mem' := λ r₁ r₂ hr₁ hr₂, by { dsimp at hr₁ hr₂ ⊢, simp only [add_mul, hr₁, hr₂] },
+    smul_mem' := λ r₁ r₂ hr₂, by { dsimp at hr₂ ⊢, simp only [mul_assoc, hr₂] }},
   -- Our claim now reduces to showing that `f` is contained in the radical of `I`
   suffices : f ∈ I.radical,
   { cases this with n hn,
-    exact ⟨⟨f ^ n, n, rfl⟩, hn⟩ },
+    exact ⟨⟨f ^ n, n, rfl⟩, hn⟩, },
   rw [← vanishing_ideal_zero_locus_eq_radical, mem_vanishing_ideal],
   intros p hfp,
   contrapose hfp,

src/data/polynomial/laurent.lean

@@ -508,7 +508,7 @@ lemma is_localization : is_localization (submonoid.closure ({X} : set R[X])) R[T
       exact ⟨1, rfl⟩ },
     { rintro ⟨⟨h, hX⟩, h⟩,
       rcases submonoid.mem_closure_singleton.mp hX with ⟨n, rfl⟩,
-      exact mul_X_pow_injective n (by simpa only [X_pow_mul] using h) }
+      exact mul_X_pow_injective n h }
   end }
 
 end comm_semiring

src/field_theory/ratfunc.lean

@@ -125,7 +125,7 @@ lemma to_fraction_ring_injective :
 /-- Non-dependent recursion principle for `ratfunc K`:
 To construct a term of `P : Sort*` out of `x : ratfunc K`,
 it suffices to provide a constructor `f : Π (p q : K[X]), P`
-and a proof that `f p q = f p' q'` for all `p q p' q'` such that `p * q' = p' * q` where
+and a proof that `f p q = f p' q'` for all `p q p' q'` such that `q' * p = q * p'` where
 both `q` and `q'` are not zero divisors, stated as `q ∉ K[X]⁰`, `q' ∉ K[X]⁰`.
 
 If considering `K` as an integral domain, this is the same as saying that
@@ -137,18 +137,18 @@ of `∀ {p q a : K[X]} (hq : q ≠ 0) (ha : a ≠ 0), f (a * p) (a * q) = f p q)
 -/
 @[irreducible] protected def lift_on {P : Sort v} (x : ratfunc K)
   (f : ∀ (p q : K[X]), P)
-  (H : ∀ {p q p' q'} (hq : q ∈ K[X]⁰) (hq' : q' ∈ K[X]⁰), p * q' = p' * q →
+  (H : ∀ {p q p' q'} (hq : q ∈ K[X]⁰) (hq' : q' ∈ K[X]⁰), q' * p = q * p' →
     f p q = f p' q') :
   P :=
 localization.lift_on
   (by exact to_fraction_ring x) -- Fix timeout by manipulating elaboration order
   (λ p q, f p q) (λ p p' q q' h, H q.2 q'.2
   (let ⟨⟨c, hc⟩, mul_eq⟩ := (localization.r_iff_exists).mp h in
-    mul_cancel_right_coe_non_zero_divisor.mp mul_eq))
+    mul_cancel_left_coe_non_zero_divisor.mp mul_eq))
 
 lemma lift_on_of_fraction_ring_mk {P : Sort v} (n : K[X]) (d : K[X]⁰)
   (f : ∀ (p q : K[X]), P)
-  (H : ∀ {p q p' q'} (hq : q ∈ K[X]⁰) (hq' : q' ∈ K[X]⁰), p * q' = p' * q →
+  (H : ∀ {p q p' q'} (hq : q ∈ K[X]⁰) (hq' : q' ∈ K[X]⁰), q' * p = q * p' →
     f p q = f p' q') :
   ratfunc.lift_on (by exact of_fraction_ring (localization.mk n d)) f @H = f n d :=
 begin
@@ -199,13 +199,13 @@ by rw [← is_localization.mk'_one (fraction_ring K[X]) p, ← mk_coe_def, submo
 lemma mk_eq_mk {p q p' q' : K[X]} (hq : q ≠ 0) (hq' : q' ≠ 0) :
   ratfunc.mk p q = ratfunc.mk p' q' ↔ p * q' = p' * q :=
 by rw [mk_def_of_ne _ hq, mk_def_of_ne _ hq', of_fraction_ring_injective.eq_iff,
-       is_localization.mk'_eq_iff_eq, set_like.coe_mk, set_like.coe_mk,
+       is_localization.mk'_eq_iff_eq', set_like.coe_mk, set_like.coe_mk,
        (is_fraction_ring.injective K[X] (fraction_ring K[X])).eq_iff]
 
 lemma lift_on_mk {P : Sort v} (p q : K[X])
   (f : ∀ (p q : K[X]), P) (f0 : ∀ p, f p 0 = f 0 1)
-  (H' : ∀ {p q p' q'} (hq : q ≠ 0) (hq' : q' ≠ 0), p * q' = p' * q → f p q = f p' q')
-  (H : ∀ {p q p' q'} (hq : q ∈ K[X]⁰) (hq' : q' ∈ K[X]⁰), p * q' = p' * q →
+  (H' : ∀ {p q p' q'} (hq : q ≠ 0) (hq' : q' ≠ 0), q' * p = q * p' → f p q = f p' q')
+  (H : ∀ {p q p' q'} (hq : q ∈ K[X]⁰) (hq' : q' ∈ K[X]⁰), q' * p = q * p' →
     f p q = f p' q' :=
     λ p q p' q' hq hq' h, H' (non_zero_divisors.ne_zero hq) (non_zero_divisors.ne_zero hq') h) :
   (ratfunc.mk p q).lift_on f @H = f p q :=
@@ -218,25 +218,16 @@ begin
                set_like.coe_mk] }
 end
 
+omit hdomain
 lemma lift_on_condition_of_lift_on'_condition {P : Sort v} {f : ∀ (p q : K[X]), P}
   (H : ∀ {p q a} (hq : q ≠ 0) (ha : a ≠ 0), f (a * p) (a * q) = f p q)
-  ⦃p q p' q' : K[X]⦄ (hq : q ≠ 0) (hq' : q' ≠ 0) (h : p * q' = p' * q) :
+  ⦃p q p' q' : K[X]⦄ (hq : q ≠ 0) (hq' : q' ≠ 0) (h : q' * p = q * p') :
   f p q = f p' q' :=
-begin
-  have H0 : f 0 q = f 0 q',
-  { calc f 0 q = f (q' * 0) (q' * q) : (H hq hq').symm
-           ... = f (q * 0) (q * q') : by rw [mul_zero, mul_zero, mul_comm]
-           ... = f 0 q' : H hq' hq },
-  by_cases hp : p = 0,
-  { simp only [hp, hq, zero_mul, or_false, zero_eq_mul] at ⊢ h, rw [h, H0] },
-  by_cases hp' : p' = 0,
-  { simpa only [hp, hp', hq', zero_mul, or_self, mul_eq_zero] using h },
-  calc f p q = f (p' * p) (p' * q) : (H hq hp').symm
-         ... = f (p * p') (p * q') : by rw [mul_comm p p', h]
-         ... = f p' q' : H hq' hp
-end
+calc f p q = f (q' * p) (q' * q) : (H hq hq').symm
+       ... = f (q * p') (q * q') : by rw [h, mul_comm q']
+       ... = f p' q' : H hq' hq
+include hdomain
 
--- f
 /-- Non-dependent recursion principle for `ratfunc K`: if `f p q : P` for all `p q`,
 such that `f (a * p) (a * q) = f p q`, then we can find a value of `P`
 for all elements of `ratfunc K` by setting `lift_on' (p / q) f _ = f p q`.
@@ -496,7 +487,7 @@ def map [monoid_hom_class F R[X] S[X]] (φ : F)
       { exact hφ hq' },
       { exact hφ hq },
       refine localization.r_of_eq _,
-      simpa only [map_mul] using (congr_arg φ h).symm,
+      simpa only [map_mul] using (congr_arg φ h),
     end,
   map_one' := begin
     rw [←of_fraction_ring_one, ←localization.mk_one, lift_on_of_fraction_ring_mk, dif_pos],
@@ -532,7 +523,7 @@ begin
   rintro ⟨x⟩ ⟨y⟩ h, induction x, induction y,
   { simpa only [map_apply_of_fraction_ring_mk, of_fraction_ring_injective.eq_iff,
                 localization.mk_eq_mk_iff, localization.r_iff_exists,
-                mul_cancel_right_coe_non_zero_divisor, exists_const, set_like.coe_mk, ←map_mul,
+                mul_cancel_left_coe_non_zero_divisor, exists_const, set_like.coe_mk, ←map_mul,
                 hf.eq_iff] using h },
   { refl },
   { refl }
@@ -573,7 +564,7 @@ def lift_monoid_with_zero_hom (φ : R[X] →*₀ G₀) (hφ : R[X]⁰ ≤ G₀
 { to_fun := λ f, ratfunc.lift_on f (λ p q, φ p / (φ q)) $ λ p q p' q' hq hq' h, begin
     casesI subsingleton_or_nontrivial R,
     { rw [subsingleton.elim p q, subsingleton.elim p' q, subsingleton.elim q' q] },
-    rw [div_eq_div_iff, ←map_mul, h, map_mul];
+    rw [div_eq_div_iff, ←map_mul, mul_comm p, h, map_mul, mul_comm];
     exact non_zero_divisors.ne_zero (hφ ‹_›),
   end,
   map_one' := by { rw [←of_fraction_ring_one, ←localization.mk_one, lift_on_of_fraction_ring_mk],
@@ -602,8 +593,9 @@ begin
   { simp_rw [lift_monoid_with_zero_hom_apply_of_fraction_ring_mk, localization.mk_eq_mk_iff],
     intro h,
     refine localization.r_of_eq _,
-    simpa only [←hφ.eq_iff, map_mul] using mul_eq_mul_of_div_eq_div _ _ _ _ h.symm;
-    exact (map_ne_zero_of_mem_non_zero_divisors _ hφ (set_like.coe_mem _)) },
+    have := mul_eq_mul_of_div_eq_div _ _ _ _ h,
+    rwa [←map_mul, ←map_mul, hφ.eq_iff, mul_comm, mul_comm y_a] at this,
+    all_goals { exact (map_ne_zero_of_mem_non_zero_divisors _ hφ (set_like.coe_mem _)) } },
   { exact λ _, rfl },
   { exact λ _, rfl }
 end
@@ -827,8 +819,8 @@ variables {K}
 
 @[simp] lemma lift_on_div {P : Sort v} (p q : K[X])
   (f : ∀ (p q : K[X]), P) (f0 : ∀ p, f p 0 = f 0 1)
-  (H' : ∀ {p q p' q'} (hq : q ≠ 0) (hq' : q' ≠ 0), p * q' = p' * q → f p q = f p' q')
-  (H : ∀ {p q p' q'} (hq : q ∈ K[X]⁰) (hq' : q' ∈ K[X]⁰), p * q' = p' * q →
+  (H' : ∀ {p q p' q'} (hq : q ≠ 0) (hq' : q' ≠ 0), q' * p = q * p' → f p q = f p' q')
+  (H : ∀ {p q p' q'} (hq : q ∈ K[X]⁰) (hq' : q' ∈ K[X]⁰), q' * p = q * p' →
   f p q = f p' q' :=
   λ p q p' q' hq hq' h, H' (non_zero_divisors.ne_zero hq) (non_zero_divisors.ne_zero hq') h) :
   (algebra_map _ (ratfunc K) p / algebra_map _ _ q).lift_on f @H = f p q :=