chore(data/finset,order/filter): simplify a few proofs (#1747)

Also add `finset.image_mono` and `finset.range_mono`.

Author: urkud

src/data/finset.lean

@@ -754,11 +754,7 @@ range_succ
 
 @[simp] theorem range_subset {n m} : range n ⊆ range m ↔ n ≤ m := range_subset
 
-theorem exists_nat_subset_range (s : finset ℕ) : ∃n : ℕ, s ⊆ range n :=
-finset.induction_on s ⟨0, empty_subset _⟩ $ λ a s ha ⟨n, hn⟩,
-⟨max (a + 1) n, insert_subset.2
-  ⟨by simpa only [mem_range] using le_max_left (a+1) n,
-  subset.trans hn (by simpa only [range_subset] using le_max_right (a+1) n)⟩⟩
+theorem range_mono : monotone range := λ _ _, range_subset.2
 
 end range
 
@@ -986,6 +982,8 @@ eq_of_veq $ by simp only [image_val, erase_dup_map_erase_dup_eq, multiset.map_ma
 theorem image_subset_image {s₁ s₂ : finset α} (h : s₁ ⊆ s₂) : s₁.image f ⊆ s₂.image f :=
 by simp only [subset_def, image_val, subset_erase_dup', erase_dup_subset', multiset.map_subset_map h]
 
+theorem image_mono (f : α → β) : monotone (finset.image f) := λ _ _, image_subset_image
+
 theorem image_filter {p : β → Prop} [decidable_pred p] :
   (s.image f).filter p = (s.filter (p ∘ f)).image f :=
 ext.2 $ λ b, by simp only [mem_filter, mem_image, exists_prop]; exact
@@ -1566,6 +1564,12 @@ end,
 by letI := classical.dec_eq β; from
 finset.induction_on s (by simp [bot]) (by simp [A] {contextual := tt})
 
+theorem subset_range_sup_succ (s : finset ℕ) : s ⊆ range (s.sup id).succ :=
+λ n hn, mem_range.2 $ nat.lt_succ_of_le $ le_sup hn
+
+theorem exists_nat_subset_range (s : finset ℕ) : ∃n : ℕ, s ⊆ range n :=
+⟨_, s.subset_range_sup_succ⟩
+
 end sup
 
 lemma sup_eq_supr [complete_lattice β] (s : finset α) (f : α → β) : s.sup f = (⨆a∈s, f a) :=

src/order/filter/basic.lean

@@ -1579,16 +1579,13 @@ lemma tendsto_at_top_at_top_of_monotone [nonempty α] [semilattice_sup α] [preo
 alias tendsto_at_top_at_top_of_monotone ← monotone.tendsto_at_top_at_top
 
 lemma tendsto_finset_range : tendsto finset.range at_top at_top :=
-(tendsto_at_top_at_top _).2 (λ s, ⟨s.sup id + 1, λ N hN n hn,
-  finset.mem_range.2 $ lt_of_le_of_lt (finset.le_sup hn) $ nat.lt_of_succ_le hN⟩)
+finset.range_mono.tendsto_at_top_at_top.2 finset.exists_nat_subset_range
 
 lemma tendsto_finset_image_at_top_at_top {i : β → γ} {j : γ → β} (h : ∀x, j (i x) = x) :
-  tendsto (λs:finset γ, s.image j) at_top at_top :=
-tendsto_infi.2 $ assume s, tendsto_infi' (s.image i) $ tendsto_principal_principal.2 $
-  assume t (ht : s.image i ⊆ t),
-  calc s = (s.image i).image j :
-      by simp only [finset.image_image, (∘), h]; exact finset.image_id.symm
-    ... ⊆  t.image j : finset.image_subset_image ht
+  tendsto (finset.image j) at_top at_top :=
+have j ∘ i = id, from funext h,
+(finset.image_mono j).tendsto_at_top_at_top.2 $ assume s,
+  ⟨s.image i, by simp only [finset.image_image, this, finset.image_id, le_refl]⟩
 
 lemma prod_at_top_at_top_eq {β₁ β₂ : Type*} [inhabited β₁] [inhabited β₂] [semilattice_sup β₁]
   [semilattice_sup β₂] : filter.prod (@at_top β₁ _) (@at_top β₂ _) = @at_top (β₁ × β₂) _ :=