chore(*): linting (#9343)

src/data/mllist.lean

@@ -27,10 +27,10 @@ meta inductive mllist (m : Type u → Type u) (α : Type u) : Type u
 
 namespace mllist
 
-variables {α β : Type u} {m : Type u → Type u} [alternative m]
+variables {α β : Type u} {m : Type u → Type u}
 
 /-- Construct an `mllist` recursively. -/
-meta def fix (f : α → m α) : α → mllist m α
+meta def fix [alternative m] (f : α → m α) : α → mllist m α
 | x := cons $ (λ a, (some x, fix a)) <$> f x <|> pure (some x, nil)
 
 variables [monad m]
@@ -39,7 +39,7 @@ variables [monad m]
 accumulating the elements of the resulting `list β` as a single monadic lazy list.
 
 (This variant allows starting with a specified `list β` of elements, as well. )-/
-meta def fixl_with (f : α → m (α × list β)) : α → list β → mllist m β
+meta def fixl_with [alternative m] (f : α → m (α × list β)) : α → list β → mllist m β
 | s (b :: rest) := cons $ pure (some b, fixl_with s rest)
 | s [] := cons $ do {
             (s', l) ← f s,
@@ -51,7 +51,7 @@ meta def fixl_with (f : α → m (α × list β)) : α → list β → mllist m
 
 /-- Repeatedly apply a function `f : α → m (α × list β)` to an initial `a : α`,
 accumulating the elements of the resulting `list β` as a single monadic lazy list. -/
-meta def fixl (f : α → m (α × list β)) (s : α) : mllist m β := fixl_with f s []
+meta def fixl [alternative m] (f : α → m (α × list β)) (s : α) : mllist m β := fixl_with f s []
 
 /-- Deconstruct an `mllist`, returning inside the monad an optional pair `α × mllist m α`
 representing the head and tail of the list. -/

src/data/multiset/basic.lean

@@ -117,6 +117,7 @@ quotient.hrec_on m (@list.rec α (λl, C ⟦l⟧) C_0 (λa l b, C_cons a ⟦l⟧
     (assume a l l' b b' hl, have ⟦l⟧ = ⟦l'⟧, from quot.sound hl, by cc)
     (assume a a' l, C_cons_heq a a' ⟦l⟧)
 
+/-- Companion to `multiset.rec` with more convenient argument order. -/
 @[elab_as_eliminator]
 protected def rec_on (m : multiset α)
   (C_0 : C 0)
@@ -499,6 +500,10 @@ pos_iff_ne_zero.trans $ not_congr card_eq_zero
 theorem card_pos_iff_exists_mem {s : multiset α} : 0 < card s ↔ ∃ a, a ∈ s :=
 quot.induction_on s $ λ l, length_pos_iff_exists_mem
 
+/-- A strong induction principle for multisets:
+If you construct a value for a particular multiset given values for all strictly smaller multisets,
+you can construct a value for any multiset.
+-/
 @[elab_as_eliminator] def strong_induction_on {p : multiset α → Sort*} :
   ∀ (s : multiset α), (∀ s, (∀t < s, p t) → p s) → p s
 | s := λ ih, ih s $ λ t h,
@@ -905,7 +910,8 @@ foldl_induction' f H x p p s p_f px p_s
 
 /-- Product of a multiset given a commutative monoid structure on `α`.
   `prod {a, b, c} = a * b * c` -/
-@[to_additive]
+@[to_additive "Sum of a multiset given a commutative additive monoid structure on `α`.
+  `sum {a, b, c} = a + b + c`"]
 def prod [comm_monoid α] : multiset α → α :=
 foldr (*) (λ x y z, by simp [mul_left_comm]) 1
 
@@ -1438,6 +1444,8 @@ quotient.induction_on m $ assume l, congr_arg coe $ congr_arg (list.cons _) $
 section decidable_pi_exists
 variables {m : multiset α}
 
+/-- If `p` is a decidable predicate,
+so is the predicate that all elements of a multiset satisfy `p`. -/
 protected def decidable_forall_multiset {p : α → Prop} [hp : ∀a, decidable (p a)] :
   decidable (∀a∈m, p a) :=
 quotient.rec_on_subsingleton m (λl, decidable_of_iff (∀a∈l, p a) $ by simp)
@@ -1453,6 +1461,8 @@ instance decidable_eq_pi_multiset {β : α → Type*} [h : ∀a, decidable_eq (
   decidable_eq (Πa∈m, β a) :=
 assume f g, decidable_of_iff (∀a (h : a ∈ m), f a h = g a h) (by simp [function.funext_iff])
 
+/-- If `p` is a decidable predicate,
+so is the existence of an element in a multiset satisfying `p`. -/
 def decidable_exists_multiset {p : α → Prop} [decidable_pred p] :
   decidable (∃ x ∈ m, p x) :=
 quotient.rec_on_subsingleton m list.decidable_exists_mem

src/data/polynomial/identities.lean

@@ -26,7 +26,9 @@ section identities
 
 Maybe use data.nat.choose to prove it.
  -/
-
+/--
+`(x + y)^n` can be expressed as `x^n + n*x^(n-1)*y + k * y^2` for some `k` in the ring.
+-/
 def pow_add_expansion {R : Type*} [comm_semiring R] (x y : R) : ∀ (n : ℕ),
   {k // (x + y)^n = x^n + n*x^(n-1)*y + k * y^2}
 | 0 := ⟨0, by simp⟩
@@ -64,6 +66,11 @@ private lemma poly_binom_aux3 (f : polynomial R) (x y : R) : f.eval (x + y) =
   f.sum (λ e a, (a *(poly_binom_aux1 x y e a).val)*y^2) :=
 by { rw poly_binom_aux2, simp [left_distrib, sum_add, mul_assoc] }
 
+/--
+A polynomial `f` evaluated at `x + y` can be expressed as
+the evaluation of `f` at `x`, plus `y` times the (polynomial) derivative of `f` at `x`,
+plus some element `k : R` times `y^2`.
+-/
 def binom_expansion (f : polynomial R) (x y : R) :
   {k : R // f.eval (x + y) = f.eval x + (f.derivative.eval x) * y + k * y^2} :=
 begin
@@ -75,6 +82,9 @@ begin
   { exact finset.sum_mul.symm }
 end
 
+/--
+`x^n - y^n` can be expressed as `z * (x - y)` for some `z` in the ring.
+-/
 def pow_sub_pow_factor (x y : R) : Π (i : ℕ), {z : R // x^i - y^i = z * (x - y)}
 | 0 := ⟨0, by simp⟩
 | 1 := ⟨1, by simp⟩
@@ -88,6 +98,10 @@ def pow_sub_pow_factor (x y : R) : Π (i : ℕ), {z : R // x^i - y^i = z * (x -
     ... = (z * x + y ^ (k + 1)) * (x - y) : by ring_exp
   end
 
+/--
+For any polynomial `f`, `f.eval x - f.eval y` can be expressed as `z * (x - y)`
+for some `z` in the ring.
+-/
 def eval_sub_factor (f : polynomial R) (x y : R) :
   {z : R // f.eval x - f.eval y = z * (x - y)} :=
 begin

src/number_theory/pell.lean

@@ -35,7 +35,7 @@ numbers but instead Davis' variant of using solutions to Pell's equation.
 
 ## References
 
-* [M. Carneiro, _A Lean formalization of Matiyasiv's theorem_][carneiro2018matiysevic]
+* [M. Carneiro, _A Lean formalization of Matiyasevič's theorem_][carneiro2018matiyasevic]
 * [M. Davis, _Hilbert's tenth problem is unsolvable_][MR317916]
 
 ## Tags
@@ -44,7 +44,6 @@ Pell's equation, Matiyasevic's theorem, Hilbert's tenth problem
 
 ## TODO
 
-* Please the unused arguments linter.
 * Provide solutions to Pell's equation for the case of arbitrary `d` (not just `d = a ^ 2 - 1` like
   in the current version) and furthermore also for `x ^ 2 - d * y ^ 2 = -1`.
 * Connect solutions to the continued fraction expansion of `√d`.
@@ -89,9 +88,15 @@ show pell n = ((pell n).1, (pell n).2), from match pell n with (a, b) := rfl end
 def xz (n : ℕ) : ℤ := xn n
 /-- The Pell `y` sequence, considered as an integer sequence.-/
 def yz (n : ℕ) : ℤ := yn n
+
+section
+omit a1
+
 /-- The element `a` such that `d = a ^ 2 - 1`, considered as an integer.-/
 def az : ℤ := a
 
+end
+
 theorem asq_pos : 0 < a*a :=
 le_trans (le_of_lt a1) (by have := @nat.mul_le_mul_left 1 a a (le_of_lt a1); rwa mul_one at this)
 
@@ -339,7 +344,7 @@ by rw ke; exact dvd_mul_of_dvd_right
 theorem pell_zd_succ_succ (n) : pell_zd (n + 2) + pell_zd n = (2 * a : ℕ) * pell_zd (n + 1) :=
 have (1:ℤ√d) + ⟨a, 1⟩ * ⟨a, 1⟩ = ⟨a, 1⟩ * (2 * a),
 by { rw zsqrtd.coe_nat_val, change (⟨_,_⟩:ℤ√(d a1))=⟨_,_⟩,
-    rw dz_val, change az a1 with a, rw zsqrtd.ext, dsimp, split; ring },
+    rw dz_val, dsimp [az], rw zsqrtd.ext, dsimp, split; ring },
 by simpa [mul_add, mul_comm, mul_left_comm, add_comm] using congr_arg (* pell_zd a1 n) this
 
 theorem xy_succ_succ (n) : xn (n + 2) + xn n = (2 * a) * xn (n + 1) ∧
@@ -377,10 +382,15 @@ theorem yn_modeq_two : ∀ n, yn n ≡ n [MOD 2]
     exact (dvd_mul_right 2 _).modeq_zero_nat.trans (dvd_mul_right 2 _).zero_modeq_nat,
   end
 
+section
+
+omit a1
 lemma x_sub_y_dvd_pow_lem (y2 y1 y0 yn1 yn0 xn1 xn0 ay a2 : ℤ) :
   (a2 * yn1 - yn0) * ay + y2 - (a2 * xn1 - xn0) =
     y2 - a2 * y1 + y0 + a2 * (yn1 * ay + y1 - xn1) - (yn0 * ay + y0 - xn0) := by ring
 
+end
+
 theorem x_sub_y_dvd_pow (y : ℕ) :
   ∀ n, (2*a*y - y*y - 1 : ℤ) ∣ yz n * (a - y) + ↑(y^n) - xz n
 | 0 := by simp [xz, yz, int.coe_nat_zero, int.coe_nat_one]
@@ -389,7 +399,7 @@ theorem x_sub_y_dvd_pow (y : ℕ) :
   have (2*a*y - y*y - 1 : ℤ) ∣ ↑(y^(n + 2)) - ↑(2 * a) * ↑(y^(n + 1)) + ↑(y^n), from
   ⟨-↑(y^n), by { simp [pow_succ, mul_add, int.coe_nat_mul,
       show ((2:ℕ):ℤ) = 2, from rfl, mul_comm, mul_left_comm], ring }⟩,
-  by { rw [xz_succ_succ, yz_succ_succ, x_sub_y_dvd_pow_lem a1 ↑(y^(n+2)) ↑(y^(n+1)) ↑(y^n)],
+  by { rw [xz_succ_succ, yz_succ_succ, x_sub_y_dvd_pow_lem ↑(y^(n+2)) ↑(y^(n+1)) ↑(y^n)],
   exact
     dvd_sub (dvd_add this $ (x_sub_y_dvd_pow (n+1)).mul_left _) (x_sub_y_dvd_pow n) }