chore(*): golf some proofs (#5548)

Parts of #5539

src/algebra/big_operators/ring.lean

@@ -46,8 +46,7 @@ end semiring
 
 lemma sum_div [division_ring β] {s : finset α} {f : α → β} {b : β} :
   (∑ x in s, f x) / b = ∑ x in s, f x / b :=
-calc (∑ x in s, f x) / b = ∑ x in s, f x * (1 / b) : by rw [div_eq_mul_one_div, sum_mul]
-                     ... = ∑ x in s, f x / b : by { congr' with x, rw ← div_eq_mul_one_div (f x) b }
+by simp only [div_eq_mul_inv, sum_mul]
 
 section comm_semiring
 variables [comm_semiring β]

src/algebra/group_power/basic.lean

@@ -433,8 +433,7 @@ end
 mt pow_eq_zero h
 
 lemma pow_abs [linear_ordered_comm_ring R] (a : R) (n : ℕ) : (abs a)^n = abs (a^n) :=
-by induction n with n ih; [exact (abs_one).symm,
-  rw [pow_succ, pow_succ, ih, abs_mul]]
+(abs_hom.to_monoid_hom.map_pow a n).symm
 
 lemma abs_neg_one_pow [linear_ordered_comm_ring R] (n : ℕ) : abs ((-1 : R)^n) = 1 :=
 by rw [←pow_abs, abs_neg, abs_one, one_pow]

src/algebra/ordered_ring.lean

@@ -886,6 +886,7 @@ end linear_nonneg_ring
 /-- A canonically ordered commutative semiring is an ordered, commutative semiring
 in which `a ≤ b` iff there exists `c` with `b = a + c`. This is satisfied by the
 natural numbers, for example, but not the integers or other ordered groups. -/
+@[protect_proj]
 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)
@@ -904,15 +905,15 @@ lemma mul_le_mul {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) : a * c ≤ b *
 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, _root_.add_assoc],
+  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⟩
 end
 
 lemma mul_le_mul_left' {b c : α} (h : b ≤ c) (a : α) : a * b ≤ a * c :=
-mul_le_mul (le_refl a) h
+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_refl 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

src/analysis/complex/polynomial.lean

@@ -36,7 +36,8 @@ let ⟨δ', hδ'₁, hδ'₂⟩ := continuous_iff.1 (polynomial.continuous g) z
   ((g.eval z₀).abs) (complex.abs_pos.2 hg0) in
 let δ := min (min (δ' / 2) 1) (((f.eval z₀).abs / (g.eval z₀).abs) / 2) in
 have hf0' : 0 < (f.eval z₀).abs, from complex.abs_pos.2 hf0,
-have hfg0 : 0 < abs (eval z₀ f) * (abs (eval z₀ g))⁻¹, from div_pos hf0' (complex.abs_pos.2 hg0),
+have hg0' : 0 < abs (eval z₀ g), from complex.abs_pos.2 hg0,
+have hfg0 : 0 < (f.eval z₀).abs / abs (eval z₀ g), from div_pos hf0' hg0',
 have hδ0 : 0 < δ, from lt_min (lt_min (half_pos hδ'₁) (by norm_num)) (half_pos hfg0),
 have hδ : ∀ z : ℂ, abs (z - z₀) = δ → abs (g.eval z - g.eval z₀) < (g.eval z₀).abs,
   from λ z hz, hδ'₂ z (by rw [complex.dist_eq, hz];
@@ -52,12 +53,11 @@ have hF₁ : F.eval z' = f.eval z₀ - f.eval z₀ * (g.eval z₀).abs * δ ^ n
       neg_mul_eq_neg_mul_symm, mul_one, div_eq_mul_inv];
     simp only [mul_comm, mul_left_comm, mul_assoc],
 have hδs : (g.eval z₀).abs * δ ^ n / (f.eval z₀).abs < 1,
-  by rw [div_eq_mul_inv, mul_right_comm, mul_comm, ← @inv_inv' _ _ (complex.abs _ * _),
-      mul_inv_rev', inv_inv', ← div_eq_mul_inv, div_lt_iff hfg0, one_mul];
-    calc δ ^ n ≤ δ ^ 1 : pow_le_pow_of_le_one (le_of_lt hδ0) hδ1 hn0
-      ... = δ : pow_one _
-      ... ≤ ((f.eval z₀).abs / (g.eval z₀).abs) / 2 : min_le_right _ _
-      ... < _ : half_lt_self hfg0,
+  from (div_lt_one hf0').2 $ (lt_div_iff' hg0').1 $
+  calc δ ^ n ≤ δ ^ 1 : pow_le_pow_of_le_one (le_of_lt hδ0) hδ1 hn0
+         ... = δ : pow_one _
+         ... ≤ ((f.eval z₀).abs / (g.eval z₀).abs) / 2 : min_le_right _ _
+         ... < _ : half_lt_self (div_pos hf0' hg0'),
 have hF₂ : (F.eval z').abs = (f.eval z₀).abs - (g.eval z₀).abs * δ ^ n,
   from calc (F.eval z').abs = (f.eval z₀ - f.eval z₀ * (g.eval z₀).abs
     * δ ^ n / (f.eval z₀).abs).abs : congr_arg abs hF₁

src/analysis/convex/basic.lean

@@ -910,10 +910,9 @@ lemma finset.center_mass_insert (ha : i ∉ t) (hw : ∑ j in t, w j ≠ 0) :
   (insert i t).center_mass w z = (w i / (w i + ∑ j in t, w j)) • z i +
     ((∑ j in t, w j) / (w i + ∑ j in t, w j)) • t.center_mass w z :=
 begin
-  simp only [center_mass, sum_insert ha, smul_add, (mul_smul _ _ _).symm],
+  simp only [center_mass, sum_insert ha, smul_add, (mul_smul _ _ _).symm, ← div_eq_inv_mul],
   congr' 2,
-  { apply mul_comm },
-  { rw [div_mul_eq_mul_div, mul_inv_cancel hw, one_div] }
+  rw [div_mul_eq_mul_div, mul_inv_cancel hw, one_div]
 end
 
 lemma finset.center_mass_singleton (hw : w i ≠ 0) : ({i} : finset ι).center_mass w z = z i :=

src/analysis/hofer.lean

@@ -83,11 +83,8 @@ begin
   clear hu key,
   -- Hence u is Cauchy
   have cauchy_u : cauchy_seq u,
-  { apply cauchy_seq_of_le_geometric _ ε (by norm_num : 1/(2:ℝ) < 1),
-    intro n,
-    convert key₁ n,
-    rw [one_div, inv_pow'],
-    congr },
+  { refine cauchy_seq_of_le_geometric _ ε one_half_lt_one (λ n, _),
+    simpa only [one_div, inv_pow'] using key₁ n },
   -- So u converges to some y
   obtain ⟨y, limy⟩ : ∃ y, tendsto u at_top (𝓝 y),
     from complete_space.complete cauchy_u,

src/data/rat/cast.lean

@@ -204,10 +204,8 @@ by simp only [mk_eq_div, cast_div, cast_coe_int]
 end with_div_ring
 
 @[simp, norm_cast] theorem cast_nonneg [linear_ordered_field α] : ∀ {n : ℚ}, 0 ≤ (n : α) ↔ 0 ≤ n
-| ⟨n, d, h, c⟩ := show 0 ≤ (n * d⁻¹ : α) ↔ 0 ≤ (⟨n, d, h, c⟩ : ℚ),
-  by rw [num_denom', ← nonneg_iff_zero_le, mk_nonneg _ (int.coe_nat_pos.2 h),
-    mul_nonneg_iff_right_nonneg_of_pos ((@inv_pos α _ _).2 (nat.cast_pos.2 h)),
-    int.cast_nonneg]
+| ⟨n, d, h, c⟩ :=
+  by { rw [num_denom', cast_mk, mk_eq_div, div_nonneg_iff, div_nonneg_iff], norm_cast }
 
 @[simp, norm_cast] theorem cast_le [linear_ordered_field α] {m n : ℚ} : (m : α) ≤ n ↔ m ≤ n :=
 by rw [← sub_nonneg, ← cast_sub, cast_nonneg, sub_nonneg]
@@ -225,7 +223,7 @@ by rw [← cast_zero, cast_lt]
 by rw [← cast_zero, cast_lt]
 
 @[simp, norm_cast] theorem cast_id : ∀ n : ℚ, ↑n = n
-| ⟨n, d, h, c⟩ := show (n / (d : ℤ) : ℚ) = _, by rw [num_denom', mk_eq_div]
+| ⟨n, d, h, c⟩ := by rw [num_denom', cast_mk, mk_eq_div]
 
 @[simp, norm_cast] theorem cast_min [linear_ordered_field α] {a b : ℚ} :
   (↑(min a b) : α) = min a b :=

src/data/real/ennreal.lean

@@ -261,8 +261,8 @@ def of_nnreal_hom : ℝ≥0 →+* ennreal :=
 @[simp, norm_cast] lemma coe_pow (n : ℕ) : (↑(r^n) : ennreal) = r^n :=
 of_nnreal_hom.map_pow r n
 
-lemma add_eq_top : a + b = ∞ ↔ a = ∞ ∨ b = ∞ := with_top.add_eq_top
-lemma add_lt_top : a + b < ∞ ↔ a < ∞ ∧ b < ∞ := with_top.add_lt_top
+@[simp] lemma add_eq_top : a + b = ∞ ↔ a = ∞ ∨ b = ∞ := with_top.add_eq_top
+@[simp] lemma add_lt_top : a + b < ∞ ↔ a < ∞ ∧ b < ∞ := with_top.add_lt_top
 
 lemma to_nnreal_add {r₁ r₂ : ennreal} (h₁ : r₁ < ∞) (h₂ : r₂ < ∞) :
   (r₁ + r₂).to_nnreal = r₁.to_nnreal + r₂.to_nnreal :=
@@ -479,19 +479,11 @@ end
 
 lemma add_lt_add (ac : a < c) (bd : b < d) : a + b < c + d :=
 begin
-  rcases exists_between ac with ⟨a', aa', a'c⟩,
-  rcases lt_iff_exists_coe.1 aa' with ⟨aR, rfl, _⟩,
-  rcases lt_iff_exists_coe.1 a'c with ⟨a'R, rfl, _⟩,
-  rcases exists_between bd with ⟨b', bb', b'd⟩,
-  rcases lt_iff_exists_coe.1 bb' with ⟨bR, rfl, _⟩,
-  rcases lt_iff_exists_coe.1 b'd with ⟨b'R, rfl, _⟩,
-  have I : ↑aR + ↑bR < ↑a'R + ↑b'R :=
-  begin
-    rw [← coe_add, ← coe_add, coe_lt_coe],
-    apply add_lt_add (coe_lt_coe.1 aa') (coe_lt_coe.1 bb')
-  end,
-  have J : ↑a'R + ↑b'R ≤ c + d := add_le_add (le_of_lt a'c) (le_of_lt b'd),
-  apply lt_of_lt_of_le I J
+  lift a to ℝ≥0 using ne_top_of_lt ac,
+  lift b to ℝ≥0 using ne_top_of_lt bd,
+  cases c, { simp }, cases d, { simp },
+  simp only [← coe_add, some_eq_coe, coe_lt_coe] at *,
+  exact add_lt_add ac bd
 end
 
 @[norm_cast] lemma coe_min : ((min r p:ℝ≥0):ennreal) = min r p :=
@@ -535,6 +527,19 @@ section mul
 lemma mul_le_mul : a ≤ b → c ≤ d → a * c ≤ b * d :=
 canonically_ordered_semiring.mul_le_mul
 
+lemma mul_lt_mul (ac : a < c) (bd : b < d) : a * b < c * d :=
+begin
+  rcases lt_iff_exists_nnreal_btwn.1 ac with ⟨a', aa', a'c⟩,
+  lift a to ℝ≥0 using ne_top_of_lt aa',
+  rcases lt_iff_exists_nnreal_btwn.1 bd with ⟨b', bb', b'd⟩,
+  lift b to ℝ≥0 using ne_top_of_lt bb',
+  norm_cast at *,
+  calc ↑(a * b) < ↑(a' * b') :
+    coe_lt_coe.2 (mul_lt_mul' aa'.le bb' (zero_le _) ((zero_le a).trans_lt aa'))
+  ... = ↑a' * ↑b' : coe_mul
+  ... ≤ c * d : mul_le_mul a'c.le b'd.le
+end
+
 lemma mul_left_mono : monotone ((*) a) := λ b c, mul_le_mul (le_refl a)
 
 lemma mul_right_mono : monotone (λ x, x * a) := λ b c h, mul_le_mul h (le_refl a)

src/field_theory/adjoin.lean

@@ -301,15 +301,15 @@ begin
   { rw [h, inv_zero], exact subalgebra.zero_mem (algebra.adjoin F {α}) },
 
   let ϕ := alg_equiv.adjoin_singleton_equiv_adjoin_root_minimal_polynomial F α hα,
-  let inv := (@adjoin_root.field F _ _ (minimal_polynomial.irreducible hα)).inv,
-  suffices : ϕ ⟨x, hx⟩ * inv (ϕ ⟨x, hx⟩) = 1,
-  { convert subtype.mem (ϕ.symm (inv (ϕ ⟨x, hx⟩))),
+  haveI := minimal_polynomial.irreducible hα,
+  suffices : ϕ ⟨x, hx⟩ * (ϕ ⟨x, hx⟩)⁻¹ = 1,
+  { convert subtype.mem (ϕ.symm (ϕ ⟨x, hx⟩)⁻¹),
     refine (eq_inv_of_mul_right_eq_one _).symm,
     apply_fun ϕ.symm at this,
     rw [alg_equiv.map_one, alg_equiv.map_mul, alg_equiv.symm_apply_apply] at this,
     rw [←subsemiring.coe_one, ←this, subsemiring.coe_mul, subtype.coe_mk] },
 
-  rw field.mul_inv_cancel (mt (λ key, _) h),
+  rw mul_inv_cancel (mt (λ key, _) h),
   rw ← ϕ.map_zero at key,
   change ↑(⟨x, hx⟩ : algebra.adjoin F {α}) = _,
   rw [ϕ.injective key, submodule.coe_zero]

src/topology/instances/ennreal.lean

@@ -228,23 +228,14 @@ protected lemma tendsto_mul (ha : a ≠ 0 ∨ b ≠ ⊤) (hb : b ≠ 0 ∨ a ≠
   tendsto (λp:ennreal×ennreal, p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b)) :=
 have ht : ∀b:ennreal, b ≠ 0 → tendsto (λp:ennreal×ennreal, p.1 * p.2) (𝓝 ((⊤:ennreal), b)) (𝓝 ⊤),
 begin
-  refine assume b hb, tendsto_nhds_top $ assume n, _,
-  rcases exists_between (zero_lt_iff_ne_zero.2 hb) with ⟨ε', hε', hεb'⟩,
-  rcases ennreal.lt_iff_exists_coe.1 hεb' with ⟨ε, rfl, h⟩,
-  rcases exists_nat_gt (↑n / ε) with ⟨m, hm⟩,
-  have hε : ε > 0, from coe_lt_coe.1 hε',
-  filter_upwards [prod_mem_nhds_sets (lt_mem_nhds $ @coe_lt_top m) (lt_mem_nhds $ h)],
+  refine assume b hb, tendsto_nhds_top_iff_nnreal.2 $ assume n, _,
+  rcases lt_iff_exists_nnreal_btwn.1 (zero_lt_iff_ne_zero.2 hb) with ⟨ε, hε, hεb⟩,
+  replace hε : 0 < ε, from coe_pos.1 hε,
+  filter_upwards [prod_mem_nhds_sets (lt_mem_nhds $ @coe_lt_top (n / ε)) (lt_mem_nhds hεb)],
   rintros ⟨a₁, a₂⟩ ⟨h₁, h₂⟩,
   dsimp at h₁ h₂ ⊢,
-  calc (n:ennreal) = ↑(((n:ℝ≥0) / ε) * ε) :
-    begin
-      norm_cast,
-      simp [nnreal.div_def, mul_assoc, nnreal.inv_mul_cancel (ne_of_gt hε)]
-    end
-    ... < (↑m * ε : ℝ≥0) : coe_lt_coe.2 $ mul_lt_mul hm (le_refl _) hε (nat.cast_nonneg _)
-    ... ≤ a₁ * a₂ : by rw [coe_mul]; exact canonically_ordered_semiring.mul_le_mul
-      (le_of_lt h₁)
-      (le_of_lt h₂)
+  rw [← div_mul_cancel n hε.ne', coe_mul],
+  exact mul_lt_mul h₁ h₂
 end,
 begin
   cases a, {simp [none_eq_top] at hb, simp [none_eq_top, ht b hb, top_mul, hb] },