feat(*): add lemmas, golf (#11294)

### New lemmas

* `function.mul_support_nonempty_iff` and `function.support_nonempty_iff`;
* `set.infinite_union`;
* `nat.exists_subseq_of_forall_mem_union` (to be used in an upcoming mass golfing of `is_pwo`/`is_wf`);
* `hahn_series.coeff_inj`, `hahn_series.coeff_injective`, `hahn_series.coeff_fun_eq_zero_iff`, `hahn_series.support_eq_empty_iff`;
* `nat.coe_order_embedding_of_set` (`simp` + `rfl`);
* `nat.subtype.of_nat_range`, `nat.subtype.coe_comp_of_nat_range`.

### Golfed proofs

* `set.countable.prod`;
*  `nat.order_embedding_of_set_range`;
*  `hahn-series.support_nonempty_iff`;

### Renamed

* `set.finite.union_iff` → `set.finite_union`, add `@[simp]` attr;
* `set.finite.diff` → `set.finite.of_diff`, drop 1 arg;

src/algebra/support.lean

@@ -58,6 +58,10 @@ forall_congr $ λ x, not_imp_comm
   mul_support f = ∅ ↔ f = 1 :=
 by { simp_rw [← subset_empty_iff, mul_support_subset_iff', funext_iff], simp }
 
+@[simp, to_additive] lemma mul_support_nonempty_iff {f : α → M} :
+  (mul_support f).nonempty ↔ f ≠ 1 :=
+by rw [← ne_empty_iff_nonempty, ne.def, mul_support_eq_empty_iff]
+
 @[simp, to_additive] lemma mul_support_one' : mul_support (1 : α → M) = ∅ :=
 mul_support_eq_empty_iff.2 rfl
 

src/data/equiv/denumerable.lean

@@ -228,6 +228,11 @@ using_well_founded {dec_tac := `[tauto]}
 lemma of_nat_surjective : surjective (of_nat s) :=
 λ ⟨x, hx⟩, of_nat_surjective_aux hx
 
+@[simp] lemma of_nat_range : set.range (of_nat s) = set.univ := of_nat_surjective.range_eq
+
+@[simp] lemma coe_comp_of_nat_range : set.range (coe ∘ of_nat s : ℕ → ℕ) = s :=
+by rw [set.range_comp coe, of_nat_range, set.image_univ, subtype.range_coe]
+
 private def to_fun_aux (x : s) : ℕ :=
 (list.range x).countp (∈ s)
 

src/data/set/countable.lean

@@ -225,11 +225,7 @@ protected lemma countable.prod {s : set α} {t : set β} (hs : countable s) (ht
 begin
   haveI : encodable s := hs.to_encodable,
   haveI : encodable t := ht.to_encodable,
-  haveI : encodable (s × t), { apply_instance },
-  have : range (prod.map coe coe : s × t → α × β) = set.prod s t,
-    by rw [range_prod_map, subtype.range_coe, subtype.range_coe],
-  rw ← this,
-  exact countable_range _
+  exact ⟨of_equiv (s × t) (equiv.set.prod _ _)⟩
 end
 
 lemma countable.image2 {s : set α} {t : set β} (hs : countable s) (ht : countable t)

src/data/set/finite.lean

@@ -305,15 +305,12 @@ by rw ← inter_eq_self_of_subset_right h; apply_instance
 theorem finite.subset {s : set α} : finite s → ∀ {t : set α}, t ⊆ s → finite t
 | ⟨hs⟩ t h := ⟨@set.fintype_subset _ _ _ hs (classical.dec_pred t) h⟩
 
-lemma finite.union_iff {s t : set α} : finite (s ∪ t) ↔ finite s ∧ finite t :=
+@[simp] lemma finite_union {s t : set α} : finite (s ∪ t) ↔ finite s ∧ finite t :=
 ⟨λ h, ⟨h.subset (subset_union_left _ _), h.subset (subset_union_right _ _)⟩,
  λ ⟨hs, ht⟩, hs.union ht⟩
 
-lemma finite.diff {s t u : set α} (hs : s.finite) (ht : t.finite) (h : u \ t ≤ s) : u.finite :=
-begin
-  refine finite.subset (ht.union hs) _,
-  exact diff_subset_iff.mp h
-end
+lemma finite.of_diff {s t : set α} (hd : finite (s \ t)) (ht : finite t) : finite s :=
+(hd.union ht).subset $ subset_diff_union _ _
 
 theorem finite.inter_of_left {s : set α} (h : finite s) (t : set α) : finite (s ∩ t) :=
 h.subset (inter_subset_left _ _)
@@ -336,7 +333,10 @@ 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))
+λ h, hs $ h.of_diff ht
+
+@[simp] lemma infinite_union {s t : set α} : infinite (s ∪ t) ↔ infinite s ∨ infinite t :=
+by simp only [infinite, finite_union, not_and_distrib]
 
 instance fintype_image [decidable_eq β] (s : set α) (f : α → β) [fintype s] : fintype (f '' s) :=
 fintype.of_finset (s.to_finset.image f) $ by simp

src/number_theory/modular.lean

@@ -192,39 +192,29 @@ theorem tendsto_lc_row0 {cd : fin 2 → ℤ} (hcd : is_coprime (cd 0) (cd 1)) :
 begin
   let mB : ℝ → (matrix (fin 2) (fin 2)  ℝ) := λ t, ![![t, (-(1:ℤ):ℝ)], coe ∘ cd],
   have hmB : continuous mB,
-  { refine continuous_pi (λ i, _),
-    fin_cases i,
-    { refine continuous_pi (λ j, _),
-      fin_cases j,
-      { exact continuous_id },
-      { exact @continuous_const _ _ _ _ (-(1:ℤ):ℝ) } },
-    exact @continuous_const _ _ _ _ (coe ∘ cd) },
-  convert filter.tendsto.of_tendsto_comp _ (comap_cocompact hmB),
+  { simp only [continuous_pi_iff, fin.forall_fin_two],
+    have : ∀ c : ℝ, continuous (λ x : ℝ, c) := λ c, continuous_const,
+    exact ⟨⟨continuous_id, @this (-1 : ℤ)⟩, ⟨this (cd 0), this (cd 1)⟩⟩ },
+  refine filter.tendsto.of_tendsto_comp _ (comap_cocompact hmB),
   let f₁ : SL(2, ℤ) → matrix (fin 2) (fin 2) ℝ :=
     λ g, matrix.map (↑g : matrix _ _ ℤ) (coe : ℤ → ℝ),
   have cocompact_ℝ_to_cofinite_ℤ_matrix :
     tendsto (λ m : matrix (fin 2) (fin 2) ℤ, matrix.map m (coe : ℤ → ℝ)) cofinite (cocompact _),
-  { convert tendsto.pi_map_Coprod (λ i, tendsto.pi_map_Coprod (λ j, int.tendsto_coe_cofinite)),
-    { simp [Coprod_cofinite] },
-    { simp only [Coprod_cocompact],
-      refl } },
+  { simpa only [Coprod_cofinite, Coprod_cocompact]
+      using tendsto.pi_map_Coprod (λ i : fin 2, tendsto.pi_map_Coprod
+        (λ j : fin 2, int.tendsto_coe_cofinite)) },
   have hf₁ : tendsto f₁ cofinite (cocompact _) :=
     cocompact_ℝ_to_cofinite_ℤ_matrix.comp subtype.coe_injective.tendsto_cofinite,
   have hf₂ : closed_embedding (lc_row0_extend hcd) :=
     (lc_row0_extend hcd).to_continuous_linear_equiv.to_homeomorph.closed_embedding,
   convert hf₂.tendsto_cocompact.comp (hf₁.comp subtype.coe_injective.tendsto_cofinite) using 1,
-  funext g,
-  obtain ⟨g, hg⟩ := g,
-  funext j,
-  fin_cases j,
-  { ext i,
-    fin_cases i,
-    { simp [mB, f₁, matrix.mul_vec, matrix.dot_product, fin.sum_univ_succ] },
-    { convert congr_arg (λ n : ℤ, (-n:ℝ)) g.det_coe.symm using 1,
-      simp [f₁, ← hg, matrix.mul_vec, matrix.dot_product, fin.sum_univ_succ, matrix.det_fin_two,
-        -special_linear_group.det_coe],
-      ring } },
-  { exact congr_arg (λ p, (coe : ℤ → ℝ) ∘ p) hg.symm }
+  ext ⟨g, rfl⟩ i j : 3,
+  fin_cases i; [fin_cases j, skip],
+  { simp [mB, f₁, mul_vec, dot_product, fin.sum_univ_two] },
+  { convert congr_arg (λ n : ℤ, (-n:ℝ)) g.det_coe.symm using 1,
+    simp [f₁, mul_vec, dot_product, mB, fin.sum_univ_two, matrix.det_fin_two],
+    ring },
+  { refl }
 end
 
 /-- This replaces `(g•z).re = a/c + *` in the standard theory with the following novel identity:

src/order/order_iso_nat.lean

@@ -78,8 +78,9 @@ rel_iso.of_surjective (rel_embedding.order_embedding_of_lt_embedding
 variable {s}
 
 @[simp]
-lemma order_embedding_of_set_apply {n : ℕ} : order_embedding_of_set s n = subtype.of_nat s n :=
-rfl
+lemma coe_order_embedding_of_set : ⇑(order_embedding_of_set s) = coe ∘ subtype.of_nat s := rfl
+
+lemma order_embedding_of_set_apply {n : ℕ} : order_embedding_of_set s n = subtype.of_nat s n := rfl
 
 @[simp]
 lemma subtype.order_iso_of_nat_apply {n : ℕ} :
@@ -88,18 +89,20 @@ by { simp [subtype.order_iso_of_nat] }
 
 variable (s)
 
-@[simp]
 lemma order_embedding_of_set_range : set.range (nat.order_embedding_of_set s) = s :=
+subtype.coe_comp_of_nat_range
+
+theorem exists_subseq_of_forall_mem_union {α : Type*} {s t : set α} (e : ℕ → α)
+  (he : ∀ n, e n ∈ s ∪ t) :
+  ∃ g : ℕ ↪o ℕ, (∀ n, e (g n) ∈ s) ∨ (∀ n, e (g n) ∈ t) :=
 begin
-  ext x,
-  rw [set.mem_range, nat.order_embedding_of_set],
-  split; intro h,
-  { obtain ⟨y, rfl⟩ := h,
-    simp },
-  { refine ⟨(nat.subtype.order_iso_of_nat s).symm ⟨x, h⟩, _⟩,
-    simp only [rel_embedding.coe_trans, rel_embedding.order_embedding_of_lt_embedding_apply,
-      rel_embedding.nat_lt_apply, function.comp_app, order_embedding.subtype_apply],
-    rw [← subtype.order_iso_of_nat_apply, order_iso.apply_symm_apply, subtype.coe_mk] }
+  classical,
+  have : infinite (e ⁻¹' s) ∨ infinite (e ⁻¹' t),
+    by simp only [set.infinite_coe_iff, ← set.infinite_union, ← set.preimage_union,
+      set.eq_univ_of_forall (λ n, set.mem_preimage.2 (he n)), set.infinite_univ],
+  casesI this,
+  exacts [⟨nat.order_embedding_of_set (e ⁻¹' s), or.inl $ λ n, (nat.subtype.of_nat (e ⁻¹' s) _).2⟩,
+    ⟨nat.order_embedding_of_set (e ⁻¹' t), or.inr $ λ n, (nat.subtype.of_nat (e ⁻¹' t) _).2⟩]
 end
 
 end nat

src/ring_theory/hahn_series.lean

@@ -46,7 +46,7 @@ in the file `ring_theory/laurent_series`.
 
 -/
 
-open finset
+open finset function
 open_locale big_operators classical pointwise
 noncomputable theory
 
@@ -55,7 +55,7 @@ noncomputable theory
 @[ext]
 structure hahn_series (Γ : Type*) (R : Type*) [partial_order Γ] [has_zero R] :=
 (coeff : Γ → R)
-(is_pwo_support' : (function.support coeff).is_pwo)
+(is_pwo_support' : (support coeff).is_pwo)
 
 variables {Γ : Type*} {R : Type*}
 
@@ -64,9 +64,14 @@ namespace hahn_series
 section zero
 variables [partial_order Γ] [has_zero R]
 
+lemma coeff_injective : injective (coeff : hahn_series Γ R → (Γ → R)) := ext
+
+@[simp] lemma coeff_inj {x y : hahn_series Γ R} : x.coeff = y.coeff ↔ x = y :=
+coeff_injective.eq_iff
+
 /-- The support of a Hahn series is just the set of indices whose coefficients are nonzero.
   Notably, it is well-founded. -/
-def support (x : hahn_series Γ R) : set Γ := function.support x.coeff
+def support (x : hahn_series Γ R) : set Γ := support x.coeff
 
 @[simp]
 lemma is_pwo_support (x : hahn_series Γ R) : x.support.is_pwo := x.is_pwo_support'
@@ -86,31 +91,22 @@ instance : inhabited (hahn_series Γ R) := ⟨0⟩
 instance [subsingleton R] : subsingleton (hahn_series Γ R) :=
 ⟨λ a b, a.ext b (subsingleton.elim _ _)⟩
 
-@[simp]
-lemma zero_coeff {a : Γ} : (0 : hahn_series Γ R).coeff a = 0 := rfl
+@[simp] lemma zero_coeff {a : Γ} : (0 : hahn_series Γ R).coeff a = 0 := rfl
+
+@[simp] lemma coeff_fun_eq_zero_iff {x : hahn_series Γ R} : x.coeff = 0 ↔ x = 0 :=
+coeff_injective.eq_iff' rfl
 
 lemma ne_zero_of_coeff_ne_zero {x : hahn_series Γ R} {g : Γ} (h : x.coeff g ≠ 0) :
   x ≠ 0 :=
 mt (λ x0, (x0.symm ▸ zero_coeff : x.coeff g = 0)) h
 
-@[simp]
-lemma support_zero : support (0 : hahn_series Γ R) = ∅ := function.support_zero
+@[simp] lemma support_zero : support (0 : hahn_series Γ R) = ∅ := function.support_zero
 
-@[simp]
-lemma support_nonempty_iff {x : hahn_series Γ R} :
-  x.support.nonempty ↔ x ≠ 0 :=
-begin
-  split,
-  { rintro ⟨a, ha⟩ rfl,
-    apply ha zero_coeff },
-  { contrapose!,
-    rw set.not_nonempty_iff_eq_empty,
-    intro h,
-    ext a,
-    have ha := set.not_mem_empty a,
-    rw [← h, mem_support, not_not] at ha,
-    rw [ha, zero_coeff] }
-end
+@[simp] lemma support_nonempty_iff {x : hahn_series Γ R} : x.support.nonempty ↔ x ≠ 0 :=
+by rw [support, support_nonempty_iff, ne.def, coeff_fun_eq_zero_iff]
+
+@[simp] lemma support_eq_empty_iff {x : hahn_series Γ R} : x.support = ∅ ↔ x = 0 :=
+support_eq_empty_iff.trans coeff_fun_eq_zero_iff
 
 /-- `single a r` is the Hahn series which has coefficient `r` at `a` and zero otherwise. -/
 def single (a : Γ) : zero_hom R (hahn_series Γ R) :=