chore(*): golf some proofs (#5983)

API changes:

* new lemmas `finset.card_filter_le`, `finset.compl_filter`, `finset.card_lt_univ_of_not_mem`, `fintype.card_le_of_embedding`, `fintype.card_lt_of_injective_not_surjective`;
* rename `finset.card_le_of_inj_on` → `finset.le_card_of_inj_on_range`;
* rename `card_lt_of_injective_of_not_mem` to `fintype.card_lt_of_injective_of_not_mem`;
* generalize `card_units_lt` to a `monoid_with_zero`.

src/analysis/convex/caratheodory.lean

@@ -157,15 +157,10 @@ begin
   apply Union_subset, intro r,
   apply Union_subset, intro h,
   -- Second, for each convex hull of a finite subset, we shrink it.
-  transitivity,
-  { apply caratheodory.shrink, },
-  { -- After that it's just shuffling unions around.
-    apply Union_subset, intro t,
-    apply Union_subset, intro htr,
-    apply Union_subset, intro ht,
-    apply set.subset_subset_Union t,
-    apply set.subset_subset_Union (subset.trans htr h),
-    exact subset_Union _ ht, },
+  refine subset.trans (caratheodory.shrink _) _,
+  -- After that it's just shuffling unions around.
+  refine Union_subset_Union (λ t, _),
+  exact Union_subset_Union2 (λ htr, ⟨subset.trans htr h, subset.refl _⟩)
 end
 
 /--
@@ -218,31 +213,15 @@ begin
   obtain ⟨t, w, b, f, ⟨pos, sum, center⟩⟩ := eq_center_mass_card_le_dim_succ_of_mem_convex_hull h,
   let t' := t.filter (λ z, 0 < f z),
   have t'sum : t'.sum f = 1,
-  { convert sum using 1,
-    symmetry,
-    fapply sum_bij_ne_zero (λ z h w, z),
-    { intros z m nz,
-      exact multiset.mem_filter_of_mem m (lt_of_le_of_ne (pos z m) (ne.symm nz)), },
-    { intros _ _ _ _ _ _ a, exact a, },
-    { intros z m nz,
-      exact ⟨z, mem_of_subset (filter_subset _ t) m, nz, rfl⟩, },
-    { intros, refl, }, },
-  refine ⟨t', _, _, f, ⟨_, _, _⟩⟩,
+  { rw ← sum,
+    exact sum_filter_of_ne (λ x hxt hfx, (pos x hxt).lt_of_ne hfx.symm) },
+  refine ⟨t', _, _, f, ⟨_, t'sum, _⟩⟩,
   { exact subset.trans (filter_subset _ t) w, },
-  { exact le_trans (card_le_of_subset (filter_subset _ t)) b, },
+  { exact (card_filter_le _ _).trans b, },
   { exact λ y H, (mem_filter.mp H).right, },
-  { exact t'sum, },
-  { convert center using 1,
-    symmetry,
+  { rw ← center,
     simp only [center_mass, t'sum, sum, inv_one, one_smul, id.def],
-    fapply sum_bij_ne_zero (λ z h w, z),
-    { intros z m nz,
-      have nz' : f z ≠ 0,
-      { intro a, rw a at nz,
-        simpa using nz, },
-      exact multiset.mem_filter_of_mem m (lt_of_le_of_ne (pos z m) (ne.symm nz')), },
-    { intros _ _ _ _ _ _ a, exact a, },
-    { intros z m nz,
-      exact ⟨z, mem_of_subset (filter_subset _ t) m, nz, rfl⟩, },
-    { intros, refl, }, },
+    refine sum_filter_of_ne (λ x hxt hfx, (pos x hxt).lt_of_ne $ λ hf₀, _),
+    rw [← hf₀, zero_smul] at hfx,
+    exact hfx rfl },
 end

src/data/finset/basic.lean

@@ -1903,6 +1903,10 @@ iff.intro
 theorem card_le_of_subset {s t : finset α} : s ⊆ t → card s ≤ card t :=
 multiset.card_le_of_le ∘ val_le_iff.mpr
 
+theorem card_filter_le (s : finset α) (p : α → Prop) [decidable_pred p] :
+  card (s.filter p) ≤ card s :=
+card_le_of_subset $ filter_subset _ _
+
 theorem eq_of_subset_of_card_le {s t : finset α} (h : s ⊆ t) (h₂ : card t ≤ card s) : s = t :=
 eq_of_veq $ multiset.eq_of_le_of_card_le (val_le_iff.mpr h) h₂
 
@@ -1915,8 +1919,7 @@ lemma card_le_card_of_inj_on {s : finset α} {t : finset β}
 begin
   classical,
   calc card s = card (s.image f) : by rw [card_image_of_inj_on f_inj]
-    ... ≤ card t : card_le_of_subset $
-      assume x hx, match x, finset.mem_image.1 hx with _, ⟨a, ha, rfl⟩ := hf a ha end
+    ... ≤ card t : card_le_of_subset $ image_subset_iff.2 hf
 end
 
 /--
@@ -1932,12 +1935,10 @@ begin
   intros x hx y hy, contrapose, exact hz x hx y hy,
 end
 
-lemma card_le_of_inj_on {n} {s : finset α}
-  (f : ℕ → α) (hf : ∀i<n, f i ∈ s) (f_inj : ∀i j, i<n → j<n → f i = f j → i = j) : n ≤ card s :=
+lemma le_card_of_inj_on_range {n} {s : finset α}
+  (f : ℕ → α) (hf : ∀i<n, f i ∈ s) (f_inj : ∀ (i<n) (j<n), f i = f j → i = j) : n ≤ card s :=
 calc n = card (range n) : (card_range n).symm
-  ... ≤ card s : card_le_card_of_inj_on f
-    (by simpa only [mem_range])
-    (by simp only [mem_range]; exact assume a₁ h₁ a₂ h₂, f_inj a₁ a₂ h₁ h₂)
+  ... ≤ card s : card_le_card_of_inj_on f (by simpa only [mem_range]) (by simpa only [mem_range])
 
 /-- Suppose that, given objects defined on all strict subsets of any finset `s`, one knows how to
 define an object on `s`. Then one can inductively define an object on all finsets, starting from

src/data/fintype/basic.lean

@@ -76,6 +76,11 @@ by simp [compl_eq_univ_sdiff]
 @[simp, norm_cast] lemma coe_compl [decidable_eq α] (s : finset α) : ↑(sᶜ) = (↑s : set α)ᶜ :=
 set.ext $ λ x, mem_compl
 
+@[simp] lemma compl_filter [decidable_eq α] (p : α → Prop) [decidable_pred p]
+  [Π x, decidable (¬p x)] :
+  (univ.filter p)ᶜ = univ.filter (λ x, ¬p x) :=
+(filter_not _ _).symm
+
 theorem eq_univ_iff_forall {s : finset α} : s = univ ↔ ∀ x, x ∈ s :=
 by simp [ext_iff]
 
@@ -325,6 +330,10 @@ lemma finset.card_le_univ [fintype α] (s : finset α) :
   s.card ≤ fintype.card α :=
 card_le_of_subset (subset_univ s)
 
+lemma finset.card_lt_univ_of_not_mem [fintype α] {s : finset α} {x : α} (hx : x ∉ s) :
+  s.card < fintype.card α :=
+card_lt_card ⟨subset_univ s, not_forall.2 ⟨x, λ hx', hx (hx' $ mem_univ x)⟩⟩
+
 lemma finset.card_lt_iff_ne_univ [fintype α] (s : finset α) :
   s.card < fintype.card α ↔ s ≠ finset.univ :=
 s.card_le_univ.lt_iff_ne.trans (not_iff_not_of_iff s.card_eq_iff_eq_univ)
@@ -518,6 +527,18 @@ variables [fintype α] [fintype β]
 lemma card_le_of_injective (f : α → β) (hf : function.injective f) : card α ≤ card β :=
 finset.card_le_card_of_inj_on f (λ _ _, finset.mem_univ _) (λ _ _ _ _ h, hf h)
 
+lemma card_le_of_embedding (f : α ↪ β) : card α ≤ card β := card_le_of_injective f f.2
+
+lemma card_lt_of_injective_of_not_mem (f : α → β) (h : function.injective f)
+  {b : β} (w : b ∉ set.range f) : fintype.card α < fintype.card β :=
+calc card α = (univ.map ⟨f, h⟩).card : (card_map _).symm
+... < card β : finset.card_lt_univ_of_not_mem $
+                 by rwa [← mem_coe, coe_map, coe_univ, set.image_univ]
+
+lemma card_lt_of_injective_not_surjective (f : α → β) (h : function.injective f)
+  (h' : ¬function.surjective f) : fintype.card α < fintype.card β :=
+let ⟨y, hy⟩ := not_forall.1 h' in card_lt_of_injective_of_not_mem f h hy
+
 /--
 The pigeonhole principle for finitely many pigeons and pigeonholes.
 This is the `fintype` version of `finset.exists_ne_map_eq_of_card_lt_of_maps_to`.
@@ -815,12 +836,11 @@ by { ext, simp only [set.mem_empty_eq, set.mem_to_finset, not_mem_empty] }
 
 theorem fintype.card_subtype_le [fintype α] (p : α → Prop) [decidable_pred p] :
   fintype.card {x // p x} ≤ fintype.card α :=
-by rw fintype.subtype_card; exact card_le_of_subset (subset_univ _)
+fintype.card_le_of_embedding (function.embedding.subtype _)
 
 theorem fintype.card_subtype_lt [fintype α] {p : α → Prop} [decidable_pred p]
   {x : α} (hx : ¬ p x) : fintype.card {x // p x} < fintype.card α :=
-by rw [fintype.subtype_card]; exact finset.card_lt_card
-  ⟨subset_univ _, not_forall.2 ⟨x, by simp [hx]⟩⟩
+fintype.card_lt_of_injective_of_not_mem coe subtype.coe_injective $ by rwa subtype.range_coe_subtype
 
 instance psigma.fintype {α : Type*} {β : α → Type*} [fintype α] [∀ a, fintype (β a)] :
   fintype (Σ' a, β a) :=
@@ -860,20 +880,6 @@ lemma mem_image_univ_iff_mem_range
   b ∈ univ.image f ↔ b ∈ set.range f :=
 by simp
 
-lemma card_lt_card_of_injective_of_not_mem
-  {α β : Type*} [fintype α] [fintype β] (f : α → β) (h : function.injective f)
-  {b : β} (w : b ∉ set.range f) : fintype.card α < fintype.card β :=
-begin
-  classical,
-  calc
-    fintype.card α = (univ : finset α).card : rfl
-  ... = (image f univ).card : (card_image_of_injective univ h).symm
-  ... < (insert b (image f univ)).card :
-          card_lt_card (ssubset_insert (mt mem_image_univ_iff_mem_range.mp w))
-  ... ≤ (univ : finset β).card : card_le_of_subset (subset_univ _)
-  ... = fintype.card β : rfl
-end
-
 /-- An auxiliary function for `quotient.fin_choice`.  Given a
 collection of setoids indexed by a type `ι`, a (finite) list `l` of
 indices, and a function that for each `i ∈ l` gives a term of the
@@ -1076,7 +1082,7 @@ fintype.card_congr (equiv_congr (equiv.refl α) e) ▸ fintype.card_perm
 lemma univ_eq_singleton_of_card_one {α} [fintype α] (x : α) (h : fintype.card α = 1) :
   (univ : finset α) = {x} :=
 begin
-  apply symm,
+  symmetry,
   apply eq_of_subset_of_card_le (subset_univ ({x})),
   apply le_of_eq,
   simp [h, finset.card_univ]

src/data/nat/totient.lean

@@ -19,7 +19,7 @@ localized "notation `φ` := nat.totient" in nat
 @[simp] theorem totient_zero : φ 0 = 0 := rfl
 
 lemma totient_le (n : ℕ) : φ n ≤ n :=
-calc totient n ≤ (range n).card : card_le_of_subset (filter_subset _ _)
+calc totient n ≤ (range n).card : card_filter_le _ _
            ... = n              : card_range _
 
 lemma totient_pos : ∀ {n : ℕ}, 0 < n → 0 < φ n

src/data/set/basic.lean

@@ -230,14 +230,14 @@ instance : has_ssubset (set α) := ⟨(<)⟩
 
 theorem ssubset_def : (s ⊂ t) = (s ⊆ t ∧ ¬ (t ⊆ s)) := rfl
 
+theorem eq_or_ssubset_of_subset (h : s ⊆ t) : s = t ∨ s ⊂ t :=
+eq_or_lt_of_le h
+
 lemma exists_of_ssubset {s t : set α} (h : s ⊂ t) : (∃x∈t, x ∉ s) :=
 not_subset.1 h.2
 
 lemma ssubset_iff_subset_ne {s t : set α} : s ⊂ t ↔ s ⊆ t ∧ s ≠ t :=
-and_congr_right $ λ h, not_congr $ (set.subset.antisymm_iff.trans (and_iff_right h)).symm
-
-theorem eq_or_ssubset_of_subset (h : s ⊆ t) : s = t ∨ s ⊂ t :=
-or_iff_not_imp_left.2 $ λ h', ssubset_iff_subset_ne.2 ⟨h, h'⟩
+@lt_iff_le_and_ne (set α) _ s t
 
 lemma ssubset_iff_of_subset {s t : set α} (h : s ⊆ t) : s ⊂ t ↔ ∃ x ∈ t, x ∉ s :=
 ⟨exists_of_ssubset, λ ⟨x, hxt, hxs⟩, ⟨h, λ h, hxs $ h hxt⟩⟩
@@ -2177,19 +2177,17 @@ lemma inclusion_injective {s t : set α} (h : s ⊆ t) :
   function.injective (inclusion h)
 | ⟨_, _⟩ ⟨_, _⟩ := subtype.ext_iff_val.2 ∘ subtype.ext_iff_val.1
 
+@[simp] lemma range_inclusion {s t : set α} (h : s ⊆ t) :
+  range (inclusion h) = {x : t | (x:α) ∈ s} :=
+by { ext ⟨x, hx⟩, simp [inclusion] }
+
 lemma eq_of_inclusion_surjective {s t : set α} {h : s ⊆ t}
   (h_surj : function.surjective (inclusion h)) : s = t :=
 begin
-  apply set.subset.antisymm h,
-  intros x hx,
-  cases h_surj ⟨x, hx⟩ with y key,
-  rw [←subtype.coe_mk x hx, ←key, coe_inclusion],
-  exact subtype.mem y,
+  rw [← range_iff_surjective, range_inclusion, eq_univ_iff_forall] at h_surj,
+  exact set.subset.antisymm h (λ x hx, h_surj ⟨x, hx⟩)
 end
 
-lemma range_inclusion {s t : set α} (h : s ⊆ t) : range (inclusion h) = {x : t | (x:α) ∈ s} :=
-by { ext ⟨x, hx⟩, simp [inclusion] }
-
 end inclusion
 
 /-! ### Injectivity and surjectivity lemmas for image and preimage -/

src/data/set/finite.lean

@@ -516,18 +516,12 @@ lemma finite_range_find_greatest {P : α → ℕ → Prop} [∀ x, decidable_pre
 
 lemma card_lt_card {s t : set α} [fintype s] [fintype t] (h : s ⊂ t) :
   fintype.card s < fintype.card t :=
-begin
-  rw [← s.coe_to_finset, ← t.coe_to_finset, finset.coe_ssubset] at h,
-  rw [fintype.card_of_finset' _ (λ x, mem_to_finset),
-      fintype.card_of_finset' _ (λ x, mem_to_finset)],
-  exact finset.card_lt_card h,
-end
+fintype.card_lt_of_injective_not_surjective (set.inclusion h.1) (set.inclusion_injective h.1) $
+  λ hst, (ssubset_iff_subset_ne.1 h).2 (eq_of_inclusion_surjective hst)
 
 lemma card_le_of_subset {s t : set α} [fintype s] [fintype t] (hsub : s ⊆ t) :
   fintype.card s ≤ fintype.card t :=
-calc fintype.card s = s.to_finset.card : fintype.card_of_finset' _ (by simp)
-... ≤ t.to_finset.card : finset.card_le_of_subset (λ x hx, by simp [set.subset_def, *] at *)
-... = fintype.card t : eq.symm (fintype.card_of_finset' _ (by simp))
+fintype.card_le_of_injective (set.inclusion hsub) (set.inclusion_injective hsub)
 
 lemma eq_of_subset_of_card_le {s t : set α} [fintype s] [fintype t]
    (hsub : s ⊆ t) (hcard : fintype.card t ≤ fintype.card s) : s = t :=

src/field_theory/finite/basic.lean

@@ -73,7 +73,7 @@ end,
 assume hd : disjoint _ _,
 lt_irrefl (2 * ((univ.image (λ x : R, eval x f)) ∪ (univ.image (λ x : R, eval x (-g)))).card) $
 calc 2 * ((univ.image (λ x : R, eval x f)) ∪ (univ.image (λ x : R, eval x (-g)))).card
-    ≤ 2 * fintype.card R : nat.mul_le_mul_left _ (finset.card_le_of_subset (subset_univ _))
+    ≤ 2 * fintype.card R : nat.mul_le_mul_left _ (finset.card_le_univ _)
 ... = fintype.card R + fintype.card R : two_mul _
 ... < nat_degree f * (univ.image (λ x : R, eval x f)).card +
       nat_degree (-g) * (univ.image (λ x : R, eval x (-g))).card :

src/group_theory/order_of_element.lean

@@ -148,9 +148,9 @@ lemma pow_injective_of_lt_order_of {n m : ℕ} (a : α)
   (assume h, (pow_injective_aux a h hm hn eq.symm).symm)
 
 lemma order_of_le_card_univ : order_of a ≤ fintype.card α :=
-finset.card_le_of_inj_on ((^) a)
-  (assume n _, fintype.complete _)
-  (assume i j, pow_injective_of_lt_order_of a)
+finset.le_card_of_inj_on_range ((^) a)
+  (assume n _, finset.mem_univ _)
+  (assume i hi j hj, pow_injective_of_lt_order_of a hi hj)
 
 lemma pow_eq_mod_order_of {n : ℕ} : a ^ n = a ^ (n % order_of a) :=
 calc a ^ n = a ^ (n % order_of a + order_of a * (n / order_of a)) :

src/group_theory/perm/cycles.lean

@@ -345,13 +345,9 @@ end
 lemma fixed_point_card_lt_of_ne_one [fintype α] {σ : perm α} (h : σ ≠ 1) :
   (filter (λ x, σ x = x) univ).card < fintype.card α - 1 :=
 begin
-  rw nat.lt_sub_left_iff_add_lt,
-  apply nat.add_lt_of_lt_sub_right,
-  convert one_lt_nonfixed_point_card_of_ne_one h,
-  rw [nat.sub_eq_iff_eq_add, add_comm], swap, { apply card_le_of_subset, simp },
-  rw ← card_disjoint_union, swap, { rw [disjoint_iff_inter_eq_empty, filter_inter_filter_neg_eq] },
-  rw filter_union_filter_neg_eq,
-  refl
+  rw [nat.lt_sub_left_iff_add_lt, ← nat.lt_sub_right_iff_add_lt, ← finset.card_compl,
+    finset.compl_filter],
+  exact one_lt_nonfixed_point_card_of_ne_one h
 end
 
 end fixed_points

src/measure_theory/haar_measure.lean

@@ -190,7 +190,7 @@ begin
   refine le_trans (add_le_add (this K₁.1 $ subset.trans (subset_union_left _ _) h1s)
     (this K₂.1 $ subset.trans (subset_union_right _ _) h1s)) _,
   rw [← finset.card_union_eq, finset.filter_union_right],
-  { apply finset.card_le_of_subset, apply finset.filter_subset },
+  exact s.card_filter_le _,
   apply finset.disjoint_filter.mpr,
   rintro g₁ h1g₁ ⟨g₂, h1g₂, h2g₂⟩ ⟨g₃, h1g₃, h2g₃⟩,
   simp only [mem_preimage] at h1g₃ h1g₂,

src/ring_theory/fintype.lean

@@ -12,6 +12,6 @@ import data.fintype.basic
 
 open_locale classical
 
-lemma card_units_lt (R : Type*) [semiring R] [nontrivial R] [fintype R] :
-  fintype.card (units R) < fintype.card R :=
-card_lt_card_of_injective_of_not_mem (coe : units R → R) units.ext not_is_unit_zero
+lemma card_units_lt (M₀ : Type*) [monoid_with_zero M₀] [nontrivial M₀] [fintype M₀] :
+  fintype.card (units M₀) < fintype.card M₀ :=
+fintype.card_lt_of_injective_of_not_mem (coe : units M₀ → M₀) units.ext not_is_unit_zero

src/set_theory/cardinal.lean

@@ -610,14 +610,8 @@ by induction n; simp [pow_succ', -_root_.add_comm, power_add, *]
 
 @[simp, norm_cast] theorem nat_cast_le {m n : ℕ} : (m : cardinal) ≤ n ↔ m ≤ n :=
 by rw [← lift_mk_fin, ← lift_mk_fin, lift_le]; exact
-⟨λ ⟨⟨f, hf⟩⟩, begin
-  have : _ = fintype.card _ := finset.card_image_of_injective finset.univ hf,
-  simp at this,
-  rw [← fintype.card_fin n, ← this],
-  exact finset.card_le_of_subset (finset.subset_univ _)
-end,
-λ h, ⟨⟨λ i, ⟨i.1, lt_of_lt_of_le i.2 h⟩, λ a b h,
-  have _, from fin.veq_of_eq h, fin.eq_of_veq this⟩⟩⟩
+⟨λ ⟨⟨f, hf⟩⟩, by simpa only [fintype.card_fin] using fintype.card_le_of_injective f hf,
+  λ h, ⟨(fin.cast_le h).to_embedding⟩⟩
 
 @[simp, norm_cast] theorem nat_cast_lt {m n : ℕ} : (m : cardinal) < n ↔ m < n :=
 by simp [lt_iff_le_not_le, -not_le]