[Merged by Bors] - refactor(analysis/analytic/basic): refactor change_origin

src/algebra/big_operators/order.lean

@@ -405,7 +405,7 @@ begin
   induction s using finset.induction with a s has ih h,
   { simp },
   { rw [finset.prod_insert has, finset.prod_insert has],
-    apply canonically_ordered_semiring.mul_le_mul,
+    apply mul_le_mul',
     { exact h _ (finset.mem_insert_self a s) },
     { exact ih (λ i hi, h _ (finset.mem_insert_of_mem hi)) } }
 end
@@ -418,9 +418,9 @@ lemma prod_add_prod_le' (hi : i ∈ s) (h2i : g i + h i ≤ f i)
   ∏ i in s, g i + ∏ i in s, h i ≤ ∏ i in s, f i :=
 begin
   classical, simp_rw [prod_eq_mul_prod_diff_singleton hi],
-  refine le_trans _ (canonically_ordered_semiring.mul_le_mul_right' h2i _),
+  refine le_trans _ (mul_le_mul_right' h2i _),
   rw [right_distrib],
-  apply add_le_add; apply canonically_ordered_semiring.mul_le_mul_left'; apply prod_le_prod';
+  apply add_le_add; apply mul_le_mul_left'; apply prod_le_prod';
   simp only [and_imp, mem_sdiff, mem_singleton]; intros; apply_assumption; assumption
 end
 

src/algebra/group_power/order.lean

@@ -72,25 +72,25 @@ end
 
 end cancel_add_monoid
 
-namespace canonically_ordered_semiring
+namespace canonically_ordered_comm_semiring
 variable [canonically_ordered_comm_semiring R]
 
 theorem pow_pos {a : R} (H : 0 < a) : ∀ n : ℕ, 0 < a ^ n
-| 0     := by { nontriviality, rw pow_zero, exact canonically_ordered_semiring.zero_lt_one }
-| (n+1) := by { rw pow_succ, exact canonically_ordered_semiring.mul_pos.2 ⟨H, pow_pos n⟩ }
+| 0     := by { nontriviality, rw pow_zero, exact zero_lt_one }
+| (n+1) := by { rw pow_succ, exact mul_pos.2 ⟨H, pow_pos n⟩ }
 
 @[mono] lemma pow_le_pow_of_le_left {a b : R} (hab : a ≤ b) : ∀ i : ℕ, a^i ≤ b^i
 | 0     := by simp
 | (k+1) := by { rw [pow_succ, pow_succ],
-    exact canonically_ordered_semiring.mul_le_mul hab (pow_le_pow_of_le_left k) }
+    exact mul_le_mul' hab (pow_le_pow_of_le_left k) }
 
 theorem one_le_pow_of_one_le {a : R} (H : 1 ≤ a) (n : ℕ) : 1 ≤ a ^ n :=
 by simpa only [one_pow] using pow_le_pow_of_le_left H n
 
 theorem pow_le_one {a : R} (H : a ≤ 1) (n : ℕ) : a ^ n ≤ 1:=
 by simpa only [one_pow] using pow_le_pow_of_le_left H n
 
-end canonically_ordered_semiring
+end canonically_ordered_comm_semiring
 
 section ordered_semiring
 variable [ordered_semiring R]

src/algebra/ordered_ring.lean

@@ -1333,37 +1333,29 @@ class canonically_ordered_comm_semiring (α : Type*) extends
   canonically_ordered_add_monoid α, comm_semiring α :=
 (eq_zero_or_eq_zero_of_mul_eq_zero : ∀ a b : α, a * b = 0 → a = 0 ∨ b = 0)
 
-namespace canonically_ordered_semiring
+namespace canonically_ordered_comm_semiring
 variables [canonically_ordered_comm_semiring α] {a b : α}
 
-open canonically_ordered_add_monoid (le_iff_exists_add)
-
 @[priority 100] -- see Note [lower instance priority]
-instance canonically_ordered_comm_semiring.to_no_zero_divisors :
-  no_zero_divisors α :=
+instance to_no_zero_divisors : no_zero_divisors α :=
 ⟨canonically_ordered_comm_semiring.eq_zero_or_eq_zero_of_mul_eq_zero⟩
 
-lemma mul_le_mul {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) : a * c ≤ b * d :=
+@[priority 100] -- see Note [lower instance priority]
+instance to_covariant_mul_le : covariant_class α α (*) (≤) :=
 begin
-  rcases (le_iff_exists_add _ _).1 hab with ⟨b, rfl⟩,
-  rcases (le_iff_exists_add _ _).1 hcd with ⟨d, rfl⟩,
-  suffices : a * c ≤ a * c + (a * d + b * c + b * d), by simpa [mul_add, add_mul, add_assoc],
-  exact (le_iff_exists_add _ _).2 ⟨_, rfl⟩
+  refine ⟨λ a b c h, _⟩,
+  rcases le_iff_exists_add.1 h with ⟨c, rfl⟩,
+  rw mul_add,
+  apply self_le_add_right
 end
 
-lemma mul_le_mul_left' {b c : α} (h : b ≤ c) (a : α) : a * b ≤ a * c :=
-mul_le_mul le_rfl h
-
-lemma mul_le_mul_right' {b c : α} (h : b ≤ c) (a : α) : b * a ≤ c * a :=
-mul_le_mul h le_rfl
-
 /-- A version of `zero_lt_one : 0 < 1` for a `canonically_ordered_comm_semiring`. -/
 lemma zero_lt_one [nontrivial α] : (0:α) < 1 := (zero_le 1).lt_of_ne zero_ne_one
 
 lemma mul_pos : 0 < a * b ↔ (0 < a) ∧ (0 < b) :=
 by simp only [pos_iff_ne_zero, ne.def, mul_eq_zero, not_or_distrib]
 
-end canonically_ordered_semiring
+end canonically_ordered_comm_semiring
 
 /-! ### Structures involving `*` and `0` on `with_top` and `with_bot`
 

src/algebra/squarefree.lean

@@ -217,7 +217,7 @@ begin
   simp only [finset.sep_def, S, finset.mem_filter, finset.mem_range] at hs,
   obtain ⟨hsn1, ⟨a, hsa⟩, ⟨b, hsb⟩⟩ := hs,
   rw hsa at hn,
-  obtain ⟨hlts, hlta⟩ := canonically_ordered_semiring.mul_pos.mp hn,
+  obtain ⟨hlts, hlta⟩ := canonically_ordered_comm_semiring.mul_pos.mp hn,
   rw hsb at hsa hn hlts,
   refine ⟨a, b, hlta, (pow_pos_iff zero_lt_two).mp hlts, hsa.symm, _⟩,
   rintro x ⟨y, hy⟩,