[ci skip][skip ci][skip netlify] -bors-staging-tmp-9242

archive/imo/imo2008_q2.lean

@@ -131,5 +131,5 @@ begin
 
     exact set.infinite_of_infinite_image g hK_inf },
 
-  exact set.infinite_mono hW_sub_S hW_inf,
+  exact hW_inf.mono hW_sub_S,
 end

src/algebra/big_operators/finprod.lean

@@ -217,7 +217,7 @@ f.map_finprod_plift g (finite.of_fintype _)
 begin
   by_cases hg : (mul_support $ g ∘ plift.down).finite, { exact f.map_finprod_plift g hg },
   rw [finprod, dif_neg, f.map_one, finprod, dif_neg],
-  exacts [infinite_mono (λ x hx, mt (hf (g x.down)) hx) hg, hg]
+  exacts [infinite.mono (λ x hx, mt (hf (g x.down)) hx) hg, hg]
 end
 
 @[to_additive] lemma monoid_hom.map_finprod_of_injective (g : M →* N) (hg : injective g)

src/data/set/finite.lean

@@ -316,9 +316,13 @@ h.inter_of_left t
 theorem finite.inf_of_right {s : set α} (h : finite s) (t : set α) : finite (t ⊓ s) :=
 h.inter_of_right t
 
-theorem infinite_mono {s t : set α} (h : s ⊆ t) : infinite s → infinite t :=
+protected theorem infinite.mono {s t : set α} (h : s ⊆ t) : infinite s → infinite t :=
 mt (λ ht, ht.subset h)
 
+lemma infinite.diff {s t : set α} (hs : s.infinite) (ht : t.finite) :
+  (s \ t).infinite :=
+λ h, hs ((h.union ht).subset (s.subset_diff_union t))
+
 instance fintype_image [decidable_eq β] (s : set α) (f : α → β) [fintype s] : fintype (f '' s) :=
 fintype.of_finset (s.to_finset.image f) $ by simp
 
@@ -384,7 +388,7 @@ not_congr $ finite_image_iff hi
 
 theorem infinite_of_inj_on_maps_to {s : set α} {t : set β} {f : α → β}
   (hi : inj_on f s) (hm : maps_to f s t) (hs : infinite s) : infinite t :=
-infinite_mono (maps_to'.mp hm) $ (infinite_image_iff hi).2 hs
+((infinite_image_iff hi).2 hs).mono (maps_to'.mp hm)
 
 theorem infinite.exists_ne_map_eq_of_maps_to {s : set α} {t : set β} {f : α → β}
   (hs : infinite s) (hf : maps_to f s t) (ht : finite t) :
@@ -406,7 +410,7 @@ by { rw [←image_univ, infinite_image_iff (inj_on_of_injective hi _)], exact in
 
 theorem infinite_of_injective_forall_mem [_root_.infinite α] {s : set β} {f : α → β}
   (hi : injective f) (hf : ∀ x : α, f x ∈ s) : infinite s :=
-by { rw ←range_subset_iff at hf, exact infinite_mono hf (infinite_range_of_injective hi) }
+by { rw ←range_subset_iff at hf, exact (infinite_range_of_injective hi).mono hf }
 
 theorem finite.preimage {s : set β} {f : α → β}
   (I : set.inj_on f (f⁻¹' s)) (h : finite s) : finite (f ⁻¹' s) :=
@@ -457,6 +461,12 @@ lemma finite_le_nat (n : ℕ) : finite {i | i ≤ n} := ⟨set.fintype_le_nat _
 
 lemma finite_lt_nat (n : ℕ) : finite {i | i < n} := ⟨set.fintype_lt_nat _⟩
 
+lemma infinite.exists_nat_lt {s : set ℕ} (hs : infinite s) (n : ℕ) : ∃ m ∈ s, n < m :=
+begin
+  obtain ⟨m, hm⟩ := (hs.diff $ set.finite_le_nat n).nonempty,
+  exact ⟨m, by simpa using hm⟩,
+end
+
 instance fintype_prod (s : set α) (t : set β) [fintype s] [fintype t] : fintype (set.prod s t) :=
 fintype.of_finset (s.to_finset.product t.to_finset) $ by simp
 
@@ -725,6 +735,13 @@ lemma finite.card_to_finset {s : set α} [fintype s] (h : s.finite) :
 by { rw [← finset.card_attach, finset.attach_eq_univ, ← fintype.card], congr' 2, funext,
      rw set.finite.mem_to_finset }
 
+lemma infinite.exists_not_mem_finset {s : set α} (hs : s.infinite) (f : finset α) :
+  ∃ a ∈ s, a ∉ f :=
+begin
+  obtain ⟨a, has, haf⟩ := (hs.diff f.finite_to_set).nonempty,
+  refine ⟨a, has, λ h, haf $ finset.mem_coe.1 h⟩,
+end
+
 section decidable_eq
 
 lemma to_finset_compl {α : Type*} [fintype α] [decidable_eq α]

src/data/set/intervals/infinite.lean

@@ -30,13 +30,13 @@ begin
 end
 
 lemma Ico.infinite {a b : α} (h : a < b) : infinite (Ico a b) :=
-infinite_mono Ioo_subset_Ico_self (Ioo.infinite h)
+(Ioo.infinite h).mono Ioo_subset_Ico_self
 
 lemma Ioc.infinite {a b : α} (h : a < b) : infinite (Ioc a b) :=
-infinite_mono Ioo_subset_Ioc_self (Ioo.infinite h)
+(Ioo.infinite h).mono Ioo_subset_Ioc_self
 
 lemma Icc.infinite {a b : α} (h : a < b) : infinite (Icc a b) :=
-infinite_mono Ioo_subset_Icc_self (Ioo.infinite h)
+(Ioo.infinite h).mono Ioo_subset_Icc_self
 
 end bounded
 
@@ -54,7 +54,7 @@ begin
 end
 
 lemma Iic.infinite {b : α} : infinite (Iic b) :=
-infinite_mono Iio_subset_Iic_self Iio.infinite
+Iio.infinite.mono Iio_subset_Iic_self
 
 end unbounded_below
 
@@ -66,7 +66,7 @@ lemma Ioi.infinite {a : α} : infinite (Ioi a) :=
 by apply @Iio.infinite (order_dual α)
 
 lemma Ici.infinite {a : α} : infinite (Ici a) :=
-infinite_mono Ioi_subset_Ici_self Ioi.infinite
+Ioi.infinite.mono Ioi_subset_Ici_self
 
 end unbounded_above
 

src/ring_theory/polynomial/dickson.lean

@@ -195,7 +195,7 @@ begin
   rw [map_dickson, map_pow, map_X],
   apply eq_of_infinite_eval_eq,
   -- The two polynomials agree on all `x` of the form `x = y + y⁻¹`.
-  apply @set.infinite_mono _ {x : K | ∃ y, x = y + y⁻¹ ∧ y ≠ 0},
+  apply @set.infinite.mono _ {x : K | ∃ y, x = y + y⁻¹ ∧ y ≠ 0},
   { rintro _ ⟨x, rfl, hx⟩,
     simp only [eval_X, eval_pow, set.mem_set_of_eq, @add_pow_char K _ p,
       dickson_one_one_eval_add_inv _ _ (mul_inv_cancel hx), inv_pow', zmod.cast_hom_apply,