chore(*): remove edge case assumptions from lemmas (#10774)

Remove edge case assumptions from lemmas when the result is easy to prove without the assumption.

We clean up a few lemmas in the library which assume something like `n \ne 0`,  `0 < n`, or `set.nonempty` but where the result is easy to prove by case splitting on this instead and then simplifying.
Removing these unneeded assumptions makes such lemmas easier to apply, and lets us minorly golf a few other proofs along the way.
The main external changes are to remove assumptions to around 30 lemmas, and make some arguments explicit when they were no longer inferable, all other lines are just fixing up the proofs, which shortens some proofs in the process.
I also added a couple of lemmas to help simp in a couple of examples.

The code I used to find these is in the branch https://github.com/leanprover-community/mathlib/tree/alexjbest/simple_edge_cases_linter

src/algebra/group_with_zero/power.lean

@@ -240,8 +240,12 @@ by simp only [div_eq_mul_inv, mul_pow, inv_pow₀]
   (a / b) ^ n = a ^ n / b ^ n :=
 by simp only [div_eq_mul_inv, mul_zpow₀, inv_zpow₀]
 
-lemma div_sq_cancel {a : G₀} (ha : a ≠ 0) (b : G₀) : a ^ 2 * b / a = a * b :=
-by rw [sq, mul_assoc, mul_div_cancel_left _ ha]
+lemma div_sq_cancel (a b : G₀) : a ^ 2 * b / a = a * b :=
+begin
+  by_cases ha : a = 0,
+  { simp [ha] },
+  rw [sq, mul_assoc, mul_div_cancel_left _ ha]
+end
 
 end
 

src/analysis/complex/roots_of_unity.lean

@@ -86,7 +86,11 @@ end
 lemma card_roots_of_unity (n : ℕ+) : fintype.card (roots_of_unity n ℂ) = n :=
 (is_primitive_root_exp n n.ne_zero).card_roots_of_unity
 
-lemma card_primitive_roots (k : ℕ) (h : k ≠ 0) : (primitive_roots k ℂ).card = φ k :=
-(is_primitive_root_exp k h).card_primitive_roots (nat.pos_of_ne_zero h)
+lemma card_primitive_roots (k : ℕ) : (primitive_roots k ℂ).card = φ k :=
+begin
+  by_cases h : k = 0,
+  { simp [h] },
+  exact (is_primitive_root_exp k h).card_primitive_roots,
+end
 
 end complex

src/data/bitvec/core.lean

@@ -240,8 +240,7 @@ theorem to_nat_of_nat {k n : ℕ}
 begin
   induction k with k ih generalizing n,
   { simp [nat.mod_one], refl },
-  { have h : 0 < 2, { apply le_succ },
-    rw [of_nat_succ, to_nat_append, ih, bits_to_nat_to_bool, mod_pow_succ h, nat.mul_comm] }
+  { rw [of_nat_succ, to_nat_append, ih, bits_to_nat_to_bool, mod_pow_succ, nat.mul_comm] }
 end
 
 /-- Return the integer encoded by the input bitvector -/

src/data/int/basic.lean

@@ -1088,8 +1088,13 @@ not_lt.mp (mt (eq_zero_of_dvd_of_nat_abs_lt_nat_abs hst) ht)
 lemma nat_abs_eq_of_dvd_dvd {s t : ℤ} (hst : s ∣ t) (hts : t ∣ s) : nat_abs s = nat_abs t :=
 nat.dvd_antisymm (nat_abs_dvd_iff_dvd.mpr hst) (nat_abs_dvd_iff_dvd.mpr hts)
 
-lemma div_dvd_of_ne_zero_dvd {s t : ℤ} (hst : s ∣ t) (hs : s ≠ 0) : (t / s) ∣ t :=
-by { rcases hst with ⟨c, hc⟩, simp [hc, int.mul_div_cancel_left _ hs] }
+lemma div_dvd_of_ne_zero_dvd {s t : ℤ} (hst : s ∣ t) : (t / s) ∣ t :=
+begin
+  by_cases hs : s = 0,
+  { simp [*] at *, },
+  rcases hst with ⟨c, hc⟩,
+  simp [hc, int.mul_div_cancel_left _ hs],
+end
 
 /-! ### to_nat -/
 

src/data/nat/digits.lean

@@ -301,9 +301,14 @@ begin
   simp,
 end
 
-lemma digits_last {b m : ℕ} (h : 2 ≤ b) (hm : 0 < m) (p q) :
+lemma digits_last {b : ℕ} (m : ℕ) (h : 2 ≤ b) (p q) :
   (digits b m).last p = (digits b (m/b)).last q :=
-by { simp only [digits_last_aux h hm], rw list.last_cons }
+begin
+  by_cases hm : m = 0,
+  { simp [hm], },
+  simp only [digits_last_aux h (nat.pos_of_ne_zero hm)],
+  rw list.last_cons,
+end
 
 lemma digits.injective (b : ℕ) : function.injective b.digits :=
 function.left_inverse.injective (of_digits_digits b)
@@ -327,7 +332,7 @@ begin
   by_cases hnb : n < b + 2,
   { simp_rw [digits_of_lt b.succ.succ n hnpos hnb],
     exact pos_iff_ne_zero.mp hnpos },
-  { rw digits_last (show 2 ≤ b + 2, from dec_trivial) hnpos,
+  { rw digits_last n (show 2 ≤ b + 2, from dec_trivial),
     refine IH _ (nat.div_lt_self hnpos dec_trivial) _,
     { rw ←pos_iff_ne_zero,
       exact nat.div_pos (le_of_not_lt hnb) dec_trivial } },

src/data/nat/pow.lean

@@ -115,9 +115,12 @@ alias nat.sq_sub_sq ← nat.pow_two_sub_pow_two
 
 /-! ### `pow` and `mod` / `dvd` -/
 
-theorem mod_pow_succ {b : ℕ} (b_pos : 0 < b) (w m : ℕ) :
+theorem mod_pow_succ {b : ℕ} (w m : ℕ) :
   m % (b^succ w) = b * (m/b % b^w) + m % b :=
 begin
+  by_cases b_h : b = 0,
+  { simp [b_h, pow_succ], },
+  have b_pos := nat.pos_of_ne_zero b_h,
   apply nat.strong_induction_on m,
   clear m,
   intros p IH,

src/data/polynomial/field_division.lean

@@ -427,18 +427,18 @@ begin
   rw [← C_inj, this, C_0],
 end
 
-lemma prod_multiset_root_eq_finset_root {p : polynomial R} (hzero : p ≠ 0) :
+lemma prod_multiset_root_eq_finset_root (p : polynomial R) :
   (multiset.map (λ (a : R), X - C a) p.roots).prod =
   ∏ a in (multiset.to_finset p.roots), (λ (a : R), (X - C a) ^ (root_multiplicity a p)) a :=
-by simp only [count_roots hzero, finset.prod_multiset_map_count]
+by simp only [count_roots, finset.prod_multiset_map_count]
 
 /-- The product `∏ (X - a)` for `a` inside the multiset `p.roots` divides `p`. -/
 lemma prod_multiset_X_sub_C_dvd (p : polynomial R) :
   (multiset.map (λ (a : R), X - C a) p.roots).prod ∣ p :=
 begin
   by_cases hp0 : p = 0,
   { simp only [hp0, roots_zero, is_unit_one, multiset.prod_zero, multiset.map_zero, is_unit.dvd] },
-  rw prod_multiset_root_eq_finset_root hp0,
+  rw prod_multiset_root_eq_finset_root p,
   have hcoprime : pairwise (is_coprime on λ (a : R), polynomial.X - C (id a)) :=
     pairwise_coprime_X_sub function.injective_id,
   have H : pairwise (is_coprime on λ (a : R), (polynomial.X - C (id a)) ^ (root_multiplicity a p)),
@@ -457,7 +457,7 @@ begin
   intro b,
   have prodzero : C a * p ≠ 0,
   { simp only [hpzero, or_false, ne.def, mul_eq_zero, C_eq_zero, hzero, not_false_iff] },
-  rw [count_roots hpzero, count_roots prodzero, root_multiplicity_mul prodzero],
+  rw [count_roots, count_roots, root_multiplicity_mul prodzero],
   have mulzero : root_multiplicity b (C a) = 0,
   { simp only [hzero, root_multiplicity_eq_zero, eval_C, is_root.def, not_false_iff] },
   simp only [mulzero, zero_add]

src/data/polynomial/ring_division.lean

@@ -315,8 +315,12 @@ begin
   exact (classical.some_spec (exists_multiset_roots hp0)).1
 end
 
-lemma card_roots' {p : polynomial R} (hp0 : p ≠ 0) : p.roots.card ≤ nat_degree p :=
-with_bot.coe_le_coe.1 (le_trans (card_roots hp0) (le_of_eq $ degree_eq_nat_degree hp0))
+lemma card_roots' (p : polynomial R) : p.roots.card ≤ nat_degree p :=
+begin
+  by_cases hp0 : p = 0,
+  { simp [hp0], },
+  exact with_bot.coe_le_coe.1 (le_trans (card_roots hp0) (le_of_eq $ degree_eq_nat_degree hp0))
+end
 
 lemma card_roots_sub_C {p : polynomial R} {a : R} (hp0 : 0 < degree p) :
   ((p - C a).roots.card : with_bot ℕ) ≤ degree p :=
@@ -329,11 +333,16 @@ lemma card_roots_sub_C' {p : polynomial R} {a : R} (hp0 : 0 < degree p) :
 with_bot.coe_le_coe.1 (le_trans (card_roots_sub_C hp0) (le_of_eq $ degree_eq_nat_degree
   (λ h, by simp [*, lt_irrefl] at *)))
 
-@[simp] lemma count_roots (hp : p ≠ 0) : p.roots.count a = root_multiplicity a p :=
-by { rw [roots, dif_neg hp], exact (classical.some_spec (exists_multiset_roots hp)).2 a }
+@[simp] lemma count_roots (p : polynomial R) : p.roots.count a = root_multiplicity a p :=
+begin
+  by_cases hp : p = 0,
+  { simp [hp], },
+  rw [roots, dif_neg hp],
+  exact (classical.some_spec (exists_multiset_roots hp)).2 a
+end
 
 @[simp] lemma mem_roots (hp : p ≠ 0) : a ∈ p.roots ↔ is_root p a :=
-by rw [← count_pos, count_roots hp, root_multiplicity_pos hp]
+by rw [← count_pos, count_roots p, root_multiplicity_pos hp]
 
 lemma eq_zero_of_infinite_is_root
   (p : polynomial R) (h : set.infinite {x | is_root p x}) : p = 0 :=
@@ -363,8 +372,8 @@ end
 
 lemma roots_mul {p q : polynomial R} (hpq : p * q ≠ 0) : (p * q).roots = p.roots + q.roots :=
 multiset.ext.mpr $ λ r,
-  by rw [count_add, count_roots hpq, count_roots (left_ne_zero_of_mul hpq),
-         count_roots (right_ne_zero_of_mul hpq), root_multiplicity_mul hpq]
+  by rw [count_add, count_roots, count_roots,
+         count_roots, root_multiplicity_mul hpq]
 
 @[simp] lemma mem_roots_sub_C {p : polynomial R} {a x : R} (hp0 : 0 < degree p) :
   x ∈ (p - C a).roots ↔ p.eval x = a :=
@@ -375,7 +384,7 @@ multiset.ext.mpr $ λ r,
 @[simp] lemma roots_X_sub_C (r : R) : roots (X - C r) = {r} :=
 begin
   ext s,
-  rw [count_roots (X_sub_C_ne_zero r), root_multiplicity_X_sub_C],
+  rw [count_roots, root_multiplicity_X_sub_C],
   split_ifs with h,
   { rw [h, count_singleton_self] },
   { rw [singleton_eq_cons, count_cons_of_ne h, count_zero] }
@@ -385,7 +394,7 @@ end
 if H : x = 0 then by rw [H, C_0, roots_zero] else multiset.ext.mpr $ λ r,
 have h : C x ≠ 0, from λ h, H $ C_inj.1 $ h.symm ▸ C_0.symm,
 have not_root : ¬ is_root (C x) r := mt (λ (h : eval r (C x) = 0), trans eval_C.symm h) H,
-by rw [count_roots h, count_zero, root_multiplicity_eq_zero not_root]
+by rw [count_roots, count_zero, root_multiplicity_eq_zero not_root]
 
 @[simp] lemma roots_one : (1 : polynomial R).roots = ∅ :=
 roots_C 1
@@ -455,6 +464,8 @@ multiset.to_finset (nth_roots n (1 : R))
   x ∈ nth_roots_finset n R ↔ x ^ (n : ℕ) = 1 :=
 by rw [nth_roots_finset, mem_to_finset, mem_nth_roots h]
 
+@[simp] lemma nth_roots_finset_zero : nth_roots_finset 0 R = ∅ := by simp [nth_roots_finset]
+
 end nth_roots
 
 lemma coeff_comp_degree_mul_degree (hqd0 : nat_degree q ≠ 0) :

src/field_theory/is_alg_closed/basic.lean

@@ -115,10 +115,10 @@ theorem of_exists_root (H : ∀ p : polynomial k, p.monic → irreducible p →
  let ⟨x, hx⟩ := H (q * C (leading_coeff q)⁻¹) (monic_mul_leading_coeff_inv hq.ne_zero) this in
  degree_mul_leading_coeff_inv q hq.ne_zero ▸ degree_eq_one_of_irreducible_of_root this hx⟩
 
-lemma degree_eq_one_of_irreducible [is_alg_closed k] {p : polynomial k} (h_nz : p ≠ 0)
+lemma degree_eq_one_of_irreducible [is_alg_closed k] {p : polynomial k}
   (hp : irreducible p) :
   p.degree = 1 :=
-degree_eq_one_of_irreducible_of_splits h_nz hp (is_alg_closed.splits_codomain _)
+degree_eq_one_of_irreducible_of_splits hp (is_alg_closed.splits_codomain _)
 
 lemma algebra_map_surjective_of_is_integral {k K : Type*} [field k] [ring K] [is_domain K]
   [hk : is_alg_closed k] [algebra k K] (hf : algebra.is_integral k K) :
@@ -127,7 +127,7 @@ begin
   refine λ x, ⟨-((minpoly k x).coeff 0), _⟩,
   have hq : (minpoly k x).leading_coeff = 1 := minpoly.monic (hf x),
   have h : (minpoly k x).degree = 1 := degree_eq_one_of_irreducible k
-    (minpoly.ne_zero (hf x)) (minpoly.irreducible (hf x)),
+    (minpoly.irreducible (hf x)),
   have : (aeval x (minpoly k x)) = 0 := minpoly.aeval k x,
   rw [eq_X_add_C_of_degree_eq_one h, hq, C_1, one_mul,
     aeval_add, aeval_X, aeval_C, add_eq_zero_iff_eq_neg] at this,
@@ -221,8 +221,9 @@ instance : preorder (subfield_with_hom K L M hL) :=
 open lattice
 
 lemma maximal_subfield_with_hom_chain_bounded (c : set (subfield_with_hom K L M hL))
-  (hc : chain (≤) c) (hcn  : c.nonempty) :
+  (hc : chain (≤) c) :
   ∃ ub : subfield_with_hom K L M hL, ∀ N, N ∈ c → N ≤ ub :=
+if hcn : c.nonempty then
 let ub : subfield_with_hom K L M hL :=
 by haveI : nonempty c := set.nonempty.to_subtype hcn; exact
 { carrier := ⨆ i : c, (i : subfield_with_hom K L M hL).carrier,
@@ -245,12 +246,13 @@ by haveI : nonempty c := set.nonempty.to_subtype hcn; exact
     simp [ub],
     refl
   end⟩⟩
+else by { rw [set.not_nonempty_iff_eq_empty] at hcn, simp [hcn], }
 
 variables (hL M)
 
 lemma exists_maximal_subfield_with_hom : ∃ E : subfield_with_hom K L M hL,
   ∀ N, E ≤ N → N ≤ E :=
-zorn.exists_maximal_of_nonempty_chains_bounded
+zorn.exists_maximal_of_chains_bounded
   maximal_subfield_with_hom_chain_bounded (λ _ _ _, le_trans)
 
 /-- The maximal `subfield_with_hom`. We later prove that this is equal to `⊤`. -/

src/field_theory/ratfunc.lean

@@ -607,9 +607,11 @@ by { convert denom_div (1 : polynomial K) one_ne_zero; simp }
   denom (algebra_map _ (ratfunc K) p) = 1 :=
 by { convert denom_div p one_ne_zero; simp }
 
-@[simp] lemma denom_div_dvd (p : polynomial K) {q : polynomial K} (hq : q ≠ 0) :
+@[simp] lemma denom_div_dvd (p q : polynomial K) :
   denom (algebra_map _ _ p / algebra_map _ _ q) ∣ q :=
 begin
+  by_cases hq : q = 0,
+  { simp [hq], },
   rw [denom_div _ hq, C_mul_dvd],
   { exact euclidean_domain.div_dvd_of_dvd (gcd_dvd_right p q) },
   { simpa only [ne.def, inv_eq_zero, polynomial.leading_coeff_eq_zero]
@@ -689,7 +691,7 @@ begin
     rw [ring_hom.map_mul, ring_hom.map_mul, ← div_mul_div, div_self, mul_one, num_div_denom],
     { exact algebra_map_ne_zero hp } },
   { rintro ⟨p, rfl⟩,
-    exact denom_div_dvd p hq },
+    exact denom_div_dvd p q },
 end
 
 lemma num_mul_dvd (x y : ratfunc K) : num (x * y) ∣ num x * num y :=

src/field_theory/separable.lean

@@ -205,9 +205,15 @@ begin
     rw [coeff_expand_mul hp, ← leading_coeff], exact mt leading_coeff_eq_zero.1 hf }
 end
 
-theorem map_expand {p : ℕ} (hp : 0 < p) {f : R →+* S} {q : polynomial R} :
+theorem map_expand {p : ℕ} {f : R →+* S} {q : polynomial R} :
   map f (expand R p q) = expand S p (map f q) :=
-by { ext, rw [coeff_map, coeff_expand hp, coeff_expand hp], split_ifs; simp, }
+begin
+  by_cases hp : p = 0,
+  { simp [hp] },
+  ext,
+  rw [coeff_map, coeff_expand (nat.pos_of_ne_zero hp), coeff_expand (nat.pos_of_ne_zero hp)],
+  split_ifs; simp,
+end
 
 /-- Expansion is injective. -/
 lemma expand_injective {n : ℕ} (hn : 0 < n) :
@@ -301,7 +307,7 @@ begin
   { simp [ring_hom.one_def] },
   symmetry,
   rw [pow_succ', pow_mul, ← n_ih, ← expand_char, pow_succ, ring_hom.mul_def,
-      ← map_map, mul_comm, expand_mul, ← map_expand (nat.prime.pos hp.1)]
+      ← map_map, mul_comm, expand_mul, ← map_expand]
 end
 
 end char_p
@@ -394,9 +400,11 @@ begin
               nat.sub_add_cancel (show 1 ≤ n, from hpos), sub_add_cancel]
 end
 
-lemma root_multiplicity_le_one_of_separable [nontrivial R] {p : polynomial R} (hp : p ≠ 0)
+lemma root_multiplicity_le_one_of_separable [nontrivial R] {p : polynomial R}
   (hsep : separable p) (x : R) : root_multiplicity x p ≤ 1 :=
 begin
+  by_cases hp : p = 0,
+  { simp [hp], },
   rw [root_multiplicity_eq_multiplicity, dif_neg hp, ← enat.coe_le_coe, enat.coe_get, nat.cast_one],
   exact multiplicity_le_one_of_separable (not_is_unit_X_sub_C _) hsep
 end
@@ -430,10 +438,8 @@ ih $ of_irreducible_expand hp $ by { rw pow_succ at hf, rwa [expand_expand] }
 lemma count_roots_le_one {p : polynomial R} (hsep : separable p) (x : R) :
   p.roots.count x ≤ 1 :=
 begin
-  rcases eq_or_ne p 0 with rfl | hp,
-  { simp },
-  rw count_roots hp,
-  exact root_multiplicity_le_one_of_separable hp hsep x
+  rw count_roots p,
+  exact root_multiplicity_le_one_of_separable hsep x
 end
 
 lemma nodup_roots {p : polynomial R} (hsep : separable p) : p.roots.nodup :=

src/field_theory/splitting_field.lean

@@ -176,9 +176,11 @@ begin
 end
 
 lemma degree_eq_one_of_irreducible_of_splits {p : polynomial L}
-  (h_nz : p ≠ 0) (hp : irreducible p) (hp_splits : splits (ring_hom.id L) p) :
+  (hp : irreducible p) (hp_splits : splits (ring_hom.id L) p) :
   p.degree = 1 :=
 begin
+  by_cases h_nz : p = 0,
+  { exfalso, simp [*] at *, },
   rcases hp_splits,
   { contradiction },
   { apply hp_splits hp, simp }
@@ -378,7 +380,7 @@ lemma prod_multiset_X_sub_C_of_monic_of_roots_card_eq {p : polynomial K}
   (multiset.map (λ (a : K), X - C a) p.roots).prod = p :=
 begin
   have hprodmonic : (multiset.map (λ (a : K), X - C a) p.roots).prod.monic,
-  { simp only [prod_multiset_root_eq_finset_root (ne_zero_of_monic hmonic),
+  { simp only [prod_multiset_root_eq_finset_root p,
       monic_prod_of_monic, monic_X_sub_C, monic_pow, forall_true_iff] },
   have hdegree : (multiset.map (λ (a : K), X - C a) p.roots).prod.nat_degree = p.nat_degree,
   { rw [← hroots, nat_degree_multiset_prod _ (zero_nmem_multiset_map_X_sub_C _ (λ a : K, a))],