feat(*): lemmas needed for two projects (#1294)

* feat(multiplicity|enat): add facts needed for IMO 2019-4

* feat(*): various lemmas needed for the cubing a cube proof

* typo

* some cleanup

* fixes, add choose_two_right

* projections for associated.prime and irreducible

Author: fpvandoorn

src/algebra/associated.lean

@@ -110,22 +110,47 @@ lemma dvd_and_not_dvd_iff [integral_domain α] {x y : α} :
   λ ⟨hx0, d, hdu, hdx⟩, ⟨⟨d, hdx⟩, λ ⟨e, he⟩, hdu (is_unit_of_dvd_one _
     ⟨e, (domain.mul_left_inj hx0).1 $ by conv {to_lhs, rw [he, hdx]};simp [mul_assoc]⟩)⟩⟩
 
+lemma pow_dvd_pow_iff [integral_domain α] {x : α} {n m : ℕ} (h0 : x ≠ 0) (h1 : ¬ is_unit x) :
+  x ^ n ∣ x ^ m ↔ n ≤ m :=
+begin
+  split,
+  { intro h, rw [← not_lt], intro hmn, apply h1,
+    have : x * x ^ m ∣ 1 * x ^ m,
+    { rw [← pow_succ, one_mul], exact dvd_trans (pow_dvd_pow _ (nat.succ_le_of_lt hmn)) h },
+    rwa [mul_dvd_mul_iff_right, ← is_unit_iff_dvd_one] at this, apply pow_ne_zero m h0 },
+  { apply pow_dvd_pow }
+end
+
 /-- prime element of a semiring -/
 def prime [comm_semiring α] (p : α) : Prop :=
 p ≠ 0 ∧ ¬ is_unit p ∧ (∀a b, p ∣ a * b → p ∣ a ∨ p ∣ b)
 
-@[simp] lemma not_prime_zero [integral_domain α] : ¬ prime (0 : α)
-| ⟨h, _⟩ := h rfl
+namespace prime
+
+lemma ne_zero [comm_semiring α] {p : α} (hp : prime p) : p ≠ 0 :=
+hp.1
+
+lemma not_unit [comm_semiring α] {p : α} (hp : prime p) : ¬ is_unit p :=
+hp.2.1
+
+lemma div_or_div [comm_semiring α] {p : α} (hp : prime p) {a b : α} (h : p ∣ a * b) :
+  p ∣ a ∨ p ∣ b :=
+hp.2.2 a b h
+
+end prime
+
+@[simp] lemma not_prime_zero [comm_semiring α] : ¬ prime (0 : α) :=
+λ h, h.ne_zero rfl
 
 @[simp] lemma not_prime_one [comm_semiring α] : ¬ prime (1 : α) :=
-λ h, h.2.1 is_unit_one
+λ h, h.not_unit is_unit_one
 
 lemma exists_mem_multiset_dvd_of_prime [comm_semiring α] {s : multiset α} {p : α} (hp : prime p) :
   p ∣ s.prod → ∃a∈s, p ∣ a :=
-multiset.induction_on s (assume h, (hp.2.1 $ is_unit_of_dvd_one _ h).elim) $
+multiset.induction_on s (assume h, (hp.not_unit $ is_unit_of_dvd_one _ h).elim) $
 assume a s ih h,
   have p ∣ a * s.prod, by simpa using h,
-  match hp.2.2 a s.prod this with
+  match hp.div_or_div this with
   | or.inl h := ⟨a, multiset.mem_cons_self a s, h⟩
   | or.inr h := let ⟨a, has, h⟩ := ih h in ⟨a, multiset.mem_cons_of_mem has, h⟩
   end
@@ -138,14 +163,25 @@ monoid allows us to reuse irreducible for associated elements.
 @[class] def irreducible [monoid α] (p : α) : Prop :=
 ¬ is_unit p ∧ ∀a b, p = a * b → is_unit a ∨ is_unit b
 
+namespace irreducible
+
+lemma not_unit [monoid α] {p : α} (hp : irreducible p) : ¬ is_unit p :=
+hp.1
+
+lemma is_unit_or_is_unit [monoid α] {p : α} (hp : irreducible p) {a b : α} (h : p = a * b) :
+  is_unit a ∨ is_unit b :=
+hp.2 a b h
+
+end irreducible
+
 @[simp] theorem not_irreducible_one [monoid α] : ¬ irreducible (1 : α) :=
 by simp [irreducible]
 
 @[simp] theorem not_irreducible_zero [semiring α] : ¬ irreducible (0 : α)
 | ⟨hn0, h⟩ := have is_unit (0:α) ∨ is_unit (0:α), from h 0 0 ((mul_zero 0).symm),
   this.elim hn0 hn0
 
-theorem ne_zero_of_irreducible [semiring α] : ∀ {p:α}, irreducible p → p ≠ 0
+theorem irreducible.ne_zero [semiring α] : ∀ {p:α}, irreducible p → p ≠ 0
 | _ hp rfl := not_irreducible_zero hp
 
 theorem of_irreducible_mul {α} [monoid α] {x y : α} :
@@ -164,8 +200,8 @@ begin
 end
 
 lemma irreducible_of_prime [integral_domain α] {p : α} (hp : prime p) : irreducible p :=
-⟨hp.2.1, λ a b hab,
-  (show a * b ∣ a ∨ a * b ∣ b, from hab ▸ hp.2.2 a b (hab ▸ (dvd_refl _))).elim
+⟨hp.not_unit, λ a b hab,
+  (show a * b ∣ a ∨ a * b ∣ b, from hab ▸ hp.div_or_div (hab ▸ (dvd_refl _))).elim
     (λ ⟨x, hx⟩, or.inr (is_unit_iff_dvd_one.2
       ⟨x, (domain.mul_left_inj (show a ≠ 0, from λ h, by simp [*, prime] at *)).1
         $ by conv {to_lhs, rw hx}; simp [mul_comm, mul_assoc, mul_left_comm]⟩))
@@ -179,9 +215,9 @@ lemma succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul [integral_domain α] {p : α} (hp
 λ ⟨x, hx⟩ ⟨y, hy⟩ ⟨z, hz⟩,
 have h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z),
   by simpa [mul_comm, _root_.pow_add, hx, hy, mul_assoc, mul_left_comm] using hz,
-have hp0: p ^ (k + l) ≠ 0, from pow_ne_zero _ hp.1,
+have hp0: p ^ (k + l) ≠ 0, from pow_ne_zero _ hp.ne_zero,
 have hpd : p ∣ x * y, from ⟨z, by rwa [domain.mul_left_inj hp0] at h⟩,
-(hp.2.2 x y hpd).elim
+(hp.div_or_div hpd).elim
   (λ ⟨d, hd⟩, or.inl ⟨d, by simp [*, _root_.pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩)
   (λ ⟨d, hd⟩, or.inr ⟨d, by simp [*, _root_.pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩)
 
@@ -244,14 +280,14 @@ end
 
 lemma exists_associated_mem_of_dvd_prod [integral_domain α] {p : α}
   (hp : prime p) {s : multiset α} : (∀ r ∈ s, prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q :=
-multiset.induction_on s (by simp [mt is_unit_iff_dvd_one.2 hp.2.1])
+multiset.induction_on s (by simp [mt is_unit_iff_dvd_one.2 hp.not_unit])
   (λ a s ih hs hps, begin
     rw [multiset.prod_cons] at hps,
-    cases hp.2.2 _ _ hps with h h,
+    cases hp.div_or_div hps with h h,
     { use [a, by simp],
       cases h with u hu,
       cases ((irreducible_of_prime (hs a (multiset.mem_cons.2
-        (or.inl rfl)))).2 p u hu).resolve_left hp.2.1 with v hv,
+        (or.inl rfl)))).2 p u hu).resolve_left hp.not_unit with v hv,
       exact ⟨v, by simp [hu, hv]⟩ },
     { rcases ih (λ r hr, hs _ (multiset.mem_cons.2 (or.inr hr))) h with ⟨q, hq₁, hq₂⟩,
       exact ⟨q, multiset.mem_cons.2 (or.inr hq₁), hq₂⟩ }
@@ -275,10 +311,10 @@ lemma ne_zero_iff_of_associated [comm_semiring α] {a b : α} (h : a ~ᵤ b) : a
 by haveI := classical.dec; exact not_iff_not.2 (eq_zero_iff_of_associated h)
 
 lemma prime_of_associated [comm_semiring α] {p q : α} (h : p ~ᵤ q) (hp : prime p) : prime q :=
-⟨(ne_zero_iff_of_associated h).1 hp.1,
+⟨(ne_zero_iff_of_associated h).1 hp.ne_zero,
   let ⟨u, hu⟩ := h in
-    ⟨λ ⟨v, hv⟩, hp.2.1 ⟨v * u⁻¹, by simp [hv.symm, hu.symm]⟩,
-      hu ▸ by simp [mul_unit_dvd_iff]; exact hp.2.2⟩⟩
+    ⟨λ ⟨v, hv⟩, hp.not_unit ⟨v * u⁻¹, by simp [hv.symm, hu.symm]⟩,
+      hu ▸ by { simp [mul_unit_dvd_iff], intros a b, exact hp.div_or_div }⟩⟩
 
 lemma prime_iff_of_associated [comm_semiring α] {p q : α}
   (h : p ~ᵤ q) : prime p ↔ prime q :=
@@ -477,13 +513,23 @@ iff.intro dvd_of_mk_le_mk mk_le_mk_of_dvd
 
 def prime (p : associates α) : Prop := p ≠ 0 ∧ p ≠ 1 ∧ (∀a b, p ≤ a * b → p ≤ a ∨ p ≤ b)
 
+lemma prime.ne_zero {p : associates α} (hp : prime p) : p ≠ 0 :=
+hp.1
+
+lemma prime.ne_one {p : associates α} (hp : prime p) : p ≠ 1 :=
+hp.2.1
+
+lemma prime.le_or_le {p : associates α} (hp : prime p) {a b : associates α} (h : p ≤ a * b) :
+  p ≤ a ∨ p ≤ b :=
+hp.2.2 a b h
+
 lemma exists_mem_multiset_le_of_prime {s : multiset (associates α)} {p : associates α}
   (hp : prime p) :
   p ≤ s.prod → ∃a∈s, p ≤ a :=
-multiset.induction_on s (assume ⟨d, eq⟩, (hp.2.1 (mul_eq_one_iff.1 eq).1).elim) $
+multiset.induction_on s (assume ⟨d, eq⟩, (hp.ne_one (mul_eq_one_iff.1 eq).1).elim) $
 assume a s ih h,
   have p ≤ a * s.prod, by simpa using h,
-  match hp.2.2 a s.prod this with
+  match hp.le_or_le this with
   | or.inl h := ⟨a, multiset.mem_cons_self a s, h⟩
   | or.inr h := let ⟨a, has, h⟩ := ih h in ⟨a, multiset.mem_cons_of_mem has, h⟩
   end

src/algebra/big_operators.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 
 Some big operators for lists and finite sets.
 -/
-import tactic.tauto data.list.basic data.finset
+import tactic.tauto data.list.basic data.finset data.nat.enat
 import algebra.group algebra.ordered_group algebra.group_power
 
 universes u v w
@@ -354,6 +354,18 @@ lemma sum_nat_cast [add_comm_monoid β] [has_one β] (s : finset α) (f : α →
   ↑(s.sum f) = s.sum (λa, f a : α → β) :=
 (sum_hom _).symm
 
+lemma prod_nat_cast [comm_semiring β] (s : finset α) (f : α → ℕ) :
+  ↑(s.prod f) = s.prod (λa, f a : α → β) :=
+(prod_hom _).symm
+
+protected lemma sum_nat_coe_enat [decidable_eq α] (s : finset α) (f : α → ℕ) :
+  s.sum (λ x, (f x : enat)) = (s.sum f : ℕ) :=
+begin
+  induction s using finset.induction with a s has ih h,
+  { simp },
+  { simp [has, ih] }
+end
+
 lemma le_sum_of_subadditive [add_comm_monoid α] [ordered_comm_monoid β]
   (f : α → β) (h_zero : f 0 = 0) (h_add : ∀x y, f (x + y) ≤ f x + f y) (s : finset γ) (g : γ → α) :
   f (s.sum g) ≤ s.sum (λc, f (g c)) :=
@@ -520,6 +532,43 @@ calc s₁.sum f = (s₁.filter (λx, f x = 0)).sum f + (s₁.filter (λx, f x 
 
 end canonically_ordered_monoid
 
+section linear_ordered_comm_ring
+variables [decidable_eq α] [linear_ordered_comm_ring β]
+
+/- this is also true for a ordered commutative multiplicative monoid -/
+lemma prod_nonneg {s : finset α} {f : α → β}
+  (h0 : ∀(x ∈ s), 0 ≤ f x) : 0 ≤ s.prod f :=
+begin
+  induction s using finset.induction with a s has ih h,
+  { simp [zero_le_one] },
+  { simp [has], apply mul_nonneg, apply h0 a (mem_insert_self a s),
+    exact ih (λ x H, h0 x (mem_insert_of_mem H)) }
+end
+
+/- this is also true for a ordered commutative multiplicative monoid -/
+lemma prod_pos {s : finset α} {f : α → β} (h0 : ∀(x ∈ s), 0 < f x) : 0 < s.prod f :=
+begin
+  induction s using finset.induction with a s has ih h,
+  { simp [zero_lt_one] },
+  { simp [has], apply mul_pos, apply h0 a (mem_insert_self a s),
+    exact ih (λ x H, h0 x (mem_insert_of_mem H)) }
+end
+
+/- this is also true for a ordered commutative multiplicative monoid -/
+lemma prod_le_prod {s : finset α} {f g : α → β} (h0 : ∀(x ∈ s), 0 ≤ f x)
+  (h1 : ∀(x ∈ s), f x ≤ g x) : s.prod f ≤ s.prod g :=
+begin
+  induction s using finset.induction with a s has ih h,
+  { simp },
+  { simp [has], apply mul_le_mul,
+      exact h1 a (mem_insert_self a s),
+      apply ih (λ x H, h0 _ _) (λ x H, h1 _ _); exact (mem_insert_of_mem H),
+      apply prod_nonneg (λ x H, h0 x (mem_insert_of_mem H)),
+      apply le_trans (h0 a (mem_insert_self a s)) (h1 a (mem_insert_self a s)) }
+end
+
+end linear_ordered_comm_ring
+
 @[simp] lemma card_pi [decidable_eq α] {δ : α → Type*}
   (s : finset α) (t : Π a, finset (δ a)) :
   (s.pi t).card = s.prod (λ a, card (t a)) :=

src/algebra/order_functions.lean

@@ -45,6 +45,9 @@ lemma le_iff_le (H : strict_mono f) {a b} :
  λ h, (lt_or_eq_of_le h).elim (λ h', le_of_lt (H _ _ h')) (λ h', h' ▸ le_refl _)⟩
 end
 
+protected lemma nat {β} [preorder β] {f : ℕ → β} (h : ∀n, f n < f (n+1)) : strict_mono f :=
+by { intros n m hnm, induction hnm with m' hnm' ih, apply h, exact lt.trans ih (h _) }
+
 -- `preorder α` isn't strong enough: if the preorder on α is an equivalence relation,
 -- then `strict_mono f` is vacuously true.
 lemma monotone [partial_order α] [preorder β] {f : α → β} (H : strict_mono f) : monotone f :=

src/algebra/ordered_group.lean

@@ -401,7 +401,7 @@ instance ordered_cancel_comm_monoid.to_ordered_comm_monoid
 { lt_of_add_lt_add_left := @lt_of_add_lt_add_left _ _, ..H }
 
 section ordered_cancel_comm_monoid
-variables [ordered_cancel_comm_monoid α] {a b c : α}
+variables [ordered_cancel_comm_monoid α] {a b c x y : α}
 
 @[simp] lemma add_le_add_iff_left (a : α) {b c : α} : a + b ≤ a + c ↔ b ≤ c :=
 ⟨le_of_add_le_add_left, λ h, add_le_add_left h _⟩
@@ -429,6 +429,18 @@ by rwa add_zero at this
 @[simp] lemma lt_add_iff_pos_left (a : α) {b : α} : a < b + a ↔ 0 < b :=
 by rw [add_comm, lt_add_iff_pos_right]
 
+@[simp] lemma add_le_iff_nonpos_left : x + y ≤ y ↔ x ≤ 0 :=
+by { convert add_le_add_iff_right y, rw [zero_add] }
+
+@[simp] lemma add_le_iff_nonpos_right : x + y ≤ x ↔ y ≤ 0 :=
+by { convert add_le_add_iff_left x, rw [add_zero] }
+
+@[simp] lemma add_lt_iff_neg_right : x + y < y ↔ x < 0 :=
+by { convert add_lt_add_iff_right y, rw [zero_add] }
+
+@[simp] lemma add_lt_iff_neg_left : x + y < x ↔ y < 0 :=
+by { convert add_lt_add_iff_left x, rw [add_zero] }
+
 lemma add_eq_zero_iff_eq_zero_of_nonneg
   (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 :=
 ⟨λ hab : a + b = 0,

src/data/fin.lean

@@ -210,8 +210,35 @@ rfl
   @fin.cases n C H0 Hs i.succ = Hs i :=
 by cases i; refl
 
+lemma forall_fin_succ {P : fin (n+1) → Prop} :
+  (∀ i, P i) ↔ P 0 ∧ (∀ i:fin n, P i.succ) :=
+⟨λ H, ⟨H 0, λ i, H _⟩, λ ⟨H0, H1⟩ i, fin.cases H0 H1 i⟩
+
+lemma exists_fin_succ {P : fin (n+1) → Prop} :
+  (∃ i, P i) ↔ P 0 ∨ (∃i:fin n, P i.succ) :=
+⟨λ ⟨i, h⟩, fin.cases or.inl (λ i hi, or.inr ⟨i, hi⟩) i h,
+  λ h, or.elim h (λ h, ⟨0, h⟩) $ λ⟨i, hi⟩, ⟨i.succ, hi⟩⟩
+
 end rec
 
+section tuple
+/- We can think of the type `fin n → α` as `n`-tuples in `α`. Here are some relevant operations. -/
+
+def tail {α} (p : fin (n+1) → α) : fin n → α := λ i, p i.succ
+def cons {α} (x : α) (v : fin n → α) : fin (n+1) → α :=
+λ j, fin.cases x v j
+
+@[simp] lemma tail_cons {α} (x : α) (p : fin n → α) : tail (cons x p) = p :=
+by simp [tail, cons]
+
+@[simp] lemma cons_succ {α} (x : α) (p : fin n → α) (i : fin n) : cons x p i.succ = p i :=
+by simp [cons]
+
+@[simp] lemma cons_zero {α} (x : α) (p : fin n → α) : cons x p 0 = x :=
+by simp [cons]
+
+end tuple
+
 section find
 
 def find : Π {n : ℕ} (p : fin n → Prop) [decidable_pred p], option (fin n)

src/data/finset.lean

@@ -1616,6 +1616,16 @@ theorem min_le_of_mem {s : finset α} {a b : α} (h₁ : b ∈ s) (h₂ : a ∈
 by rcases @inf_le (with_top α) _ _ _ _ _ h₁ _ rfl with ⟨b', hb, ab⟩;
    cases h₂.symm.trans hb; assumption
 
+lemma exists_min (s : finset β) (f : β → α)
+  (h : nonempty ↥(↑s : set β)) : ∃ x ∈ s, ∀ x' ∈ s, f x ≤ f x' :=
+begin
+  have : s.image f ≠ ∅,
+    rwa [ne, image_eq_empty, ← ne.def, ← nonempty_iff_ne_empty],
+  cases min_of_ne_empty this with y hy,
+  rcases mem_image.mp (mem_of_min hy) with ⟨x, hx, rfl⟩,
+  exact ⟨x, hx, λ x' hx', min_le_of_mem (mem_image_of_mem f hx') hy⟩
+end
+
 end max_min
 
 section sort

src/data/multiset.lean

@@ -613,6 +613,9 @@ quot.induction_on s $ λ l, mem_map
 @[simp] theorem card_map (f : α → β) (s) : card (map f s) = card s :=
 quot.induction_on s $ λ l, length_map _ _
 
+@[simp] theorem multiset.map_eq_zero {s : multiset α} {f : α → β} : s.map f = 0 ↔ s = 0 :=
+by rw [← multiset.card_eq_zero, multiset.card_map, multiset.card_eq_zero]
+
 theorem mem_map_of_mem (f : α → β) {a : α} {s : multiset α} (h : a ∈ s) : f a ∈ map f s :=
 mem_map.2 ⟨_, h, rfl⟩