chore(number_theory/dioph): Cleanup (#13403)

Clean up, including:
* Move prerequisites to the correct files
* Make equalities in `poly` operations defeq
* Remove defeq abuse around `set`
* Slightly golf proofs by tweaking explicitness of lemma arguments

Renames

src/control/traversable/instances.lean

@@ -60,8 +60,7 @@ variables [applicative F] [applicative G]
 section
 variables [is_lawful_applicative F] [is_lawful_applicative G]
 
-open applicative functor
-open list (cons)
+open applicative functor list
 
 protected lemma id_traverse {α} (xs : list α) :
   list.traverse id.mk xs = xs :=

src/data/int/basic.lean

@@ -285,6 +285,8 @@ end
 
 /-! ### nat abs -/
 
+variables {a b : ℤ} {n : ℕ}
+
 attribute [simp] nat_abs nat_abs_of_nat nat_abs_zero nat_abs_one
 
 theorem nat_abs_add_le (a b : ℤ) : nat_abs (a + b) ≤ nat_abs a + nat_abs b :=
@@ -355,6 +357,9 @@ begin
   exact int.coe_nat_inj'.symm
 end
 
+lemma eq_nat_abs_iff_mul_eq_zero : a.nat_abs = n ↔ (a - n) * (a + n) = 0 :=
+by rw [nat_abs_eq_iff, mul_eq_zero, sub_eq_zero, add_eq_zero_iff_eq_neg]
+
 lemma nat_abs_lt_iff_mul_self_lt {a b : ℤ} : a.nat_abs < b.nat_abs ↔ a * a < b * b :=
 begin
   rw [← abs_lt_iff_mul_self_lt, abs_eq_nat_abs, abs_eq_nat_abs],

src/data/list/basic.lean

@@ -3707,6 +3707,31 @@ end
 
 end to_chunks
 
+/-! ### all₂ -/
+
+section all₂
+variables {p q : α → Prop} {l : list α}
+
+@[simp] lemma all₂_cons (p : α → Prop) (x : α) : ∀ (l : list α), all₂ p (x :: l) ↔ p x ∧ all₂ p l
+| []       := (and_true _).symm
+| (x :: l) := iff.rfl
+
+lemma all₂_iff_forall : ∀ {l : list α}, all₂ p l ↔ ∀ x ∈ l, p x
+| []       := (iff_true_intro $ ball_nil _).symm
+| (x :: l) := by rw [ball_cons, all₂_cons, all₂_iff_forall]
+
+lemma all₂.imp (h : ∀ x, p x → q x) : ∀ {l : list α}, all₂ p l → all₂ q l
+| []       := id
+| (x :: l) := by simpa using and.imp (h x) all₂.imp
+
+@[simp] lemma all₂_map_iff {p : β → Prop} (f : α → β) : all₂ p (l.map f) ↔ all₂ (p ∘ f) l :=
+by induction l; simp *
+
+instance (p : α → Prop) [decidable_pred p] : decidable_pred (all₂ p) :=
+λ l, decidable_of_iff' _ all₂_iff_forall
+
+end all₂
+
 /-! ### Retroattributes
 
 The list definitions happen earlier than `to_additive`, so here we tag the few multiplicative

src/data/list/defs.lean

@@ -398,6 +398,13 @@ attribute [simp] forall₂.nil
 
 end forall₂
 
+/-- `l.all₂ p` is equivalent to `∀ a ∈ l, p a`, but unfolds directly to a conjunction, i.e.
+`list.all₂ p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2`. -/
+@[simp] def all₂ (p : α → Prop) : list α → Prop
+| []        := true
+| (x :: []) := p x
+| (x :: l)  := p x ∧ all₂ l
+
 /-- Auxiliary definition used to define `transpose`.
   `transpose_aux l L` takes each element of `l` and appends it to the start of
   each element of `L`.

src/data/option/basic.lean

@@ -490,4 +490,11 @@ rfl
 @[simp] lemma to_list_none (α : Type*) : (none : option α).to_list = [] :=
 rfl
 
+--TODO: Swap arguments to `option.elim` so that it is exactly `option.cons`
+/-- Functions from `option` can be combined similarly to `vector.cons`. -/
+def cons (a : β) (f : α → β) : option α → β := λ o, o.elim a f
+
+@[simp] lemma cons_none_some (f : option α → β) : cons (f none) (f ∘ some) = f :=
+funext $ λ o, by cases o; refl
+
 end option