fix

src/field_theory/ratfunc.lean

@@ -137,16 +137,16 @@ 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 (to_fraction_ring x) (λ 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 (of_fraction_ring (localization.mk n d)) f @H = f n d :=
 begin
@@ -202,8 +202,8 @@ by rw [mk_def_of_ne _ hq, mk_def_of_ne _ hq', of_fraction_ring_injective.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,19 +218,19 @@ end
 
 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] },
+  { simp only [hp, hq, mul_zero, false_or, 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 },
+  { simpa only [hp, hp', hq', mul_zero, 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 * p') (p * q') : by rw [mul_comm p p', mul_comm _ q, ←h, mul_comm p]
          ... = f p' q' : H hq' hp
 end
 
@@ -494,7 +494,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],
@@ -530,7 +530,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 }
@@ -571,7 +571,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],
@@ -600,8 +600,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
@@ -825,8 +826,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 :=