chore(*): golf (#17558)

Golfing part of #17553

Author: urkud

src/data/finsupp/fin.lean

@@ -27,35 +27,20 @@ variables {n : ℕ} (i : fin n) {M : Type*} [has_zero M] (y : M)
 
 /-- `tail` for maps `fin (n + 1) →₀ M`. See `fin.tail` for more details. -/
 def tail (s : fin (n + 1) →₀ M) : fin n →₀ M :=
-finsupp.equiv_fun_on_fintype.inv_fun (fin.tail s.to_fun)
+finsupp.equiv_fun_on_fintype.symm (fin.tail s)
 
 /-- `cons` for maps `fin n →₀ M`. See `fin.cons` for more details. -/
 def cons (y : M) (s : fin n →₀ M) : fin (n + 1) →₀ M :=
-finsupp.equiv_fun_on_fintype.inv_fun (fin.cons y s.to_fun)
+finsupp.equiv_fun_on_fintype.symm (fin.cons y s : fin (n + 1) → M)
 
-lemma tail_apply : tail t i = t i.succ :=
-begin
-  simp only [tail, equiv_fun_on_fintype_symm_apply_to_fun, equiv.inv_fun_as_coe],
-  refl,
-end
+lemma tail_apply : tail t i = t i.succ := rfl
 
-@[simp] lemma cons_zero : cons y s 0 = y :=
-by simp [cons, finsupp.equiv_fun_on_fintype]
+@[simp] lemma cons_zero : cons y s 0 = y := rfl
 
-@[simp] lemma cons_succ : cons y s i.succ = s i :=
-begin
-  simp only [finsupp.cons, fin.cons, finsupp.equiv_fun_on_fintype, fin.cases_succ, finsupp.coe_mk],
-  refl,
-end
+@[simp] lemma cons_succ : cons y s i.succ = s i := fin.cons_succ _ _ _
 
 @[simp] lemma tail_cons : tail (cons y s) = s :=
-begin
-  simp only [finsupp.cons, fin.cons, finsupp.tail, fin.tail],
-  ext,
-  simp only [equiv_fun_on_fintype_symm_apply_to_fun, equiv.inv_fun_as_coe,
-    finsupp.coe_mk, fin.cases_succ, equiv_fun_on_fintype],
-  refl,
-end
+ext $ λ k, by simp only [tail_apply, cons_succ]
 
 @[simp] lemma cons_tail : cons (t 0) (tail t) = t :=
 begin

src/linear_algebra/basic.lean

@@ -99,19 +99,11 @@ variables (R M) [add_comm_monoid M] [semiring R] [module R M]
 
 @[simp] lemma linear_equiv_fun_on_fintype_single [decidable_eq α] (x : α) (m : M) :
   (linear_equiv_fun_on_fintype R M α) (single x m) = pi.single x m :=
-begin
-  ext a,
-  change (equiv_fun_on_fintype (single x m)) a = _,
-  convert _root_.congr_fun (equiv_fun_on_fintype_single x m) a,
-end
+equiv_fun_on_fintype_single x m
 
 @[simp] lemma linear_equiv_fun_on_fintype_symm_single [decidable_eq α]
   (x : α) (m : M) : (linear_equiv_fun_on_fintype R M α).symm (pi.single x m) = single x m :=
-begin
-  ext a,
-  change (equiv_fun_on_fintype.symm (pi.single x m)) a = _,
-  convert congr_fun (equiv_fun_on_fintype_symm_single x m) a,
-end
+equiv_fun_on_fintype_symm_single x m
 
 @[simp] lemma linear_equiv_fun_on_fintype_symm_coe (f : α →₀ M) :
   (linear_equiv_fun_on_fintype R M α).symm f = f :=

src/order/well_founded_set.lean

@@ -689,22 +689,18 @@ partially well ordered, and also to consider the case of `set.partially_well_ord
 lemma pi.is_pwo {α : ι → Type*} [Π i, linear_order (α i)] [∀ i, is_well_order (α i) (<)] [finite ι]
   (s : set (Π i, α i)) : s.is_pwo :=
 begin
-  classical,
   casesI nonempty_fintype ι,
-  refine is_pwo.mono _ (subset_univ _),
-  rw is_pwo_iff_exists_monotone_subseq,
-  simp only [mem_univ, forall_const, function.comp_app],
   suffices : ∀ s : finset ι, ∀ (f : ℕ → Π s, α s), ∃ g : ℕ ↪o ℕ,
     ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι) (hs : x ∈ s), (f ∘ g) a x ≤ (f ∘ g) b x,
-  { simpa only [forall_true_left, finset.mem_univ] using this finset.univ },
-  apply' finset.induction,
+  { refine is_pwo_iff_exists_monotone_subseq.2 (λ f hf, _),
+    simpa only [finset.mem_univ, true_implies_iff] using this finset.univ f },
+  refine finset.cons_induction _ _,
   { intros f, existsi rel_embedding.refl (≤),
     simp only [is_empty.forall_iff, implies_true_iff, forall_const, finset.not_mem_empty], },
   { intros x s hx ih f,
     obtain ⟨g, hg⟩ := (is_well_founded.wf.is_wf univ).is_pwo.exists_monotone_subseq (λ n, f n x)
       mem_univ,
     obtain ⟨g', hg'⟩ := ih (f ∘ g),
-    refine ⟨g'.trans g, λ a b hab, _⟩,
-    simp only [finset.mem_insert, rel_embedding.coe_trans, function.comp_app, forall_eq_or_imp],
+    refine ⟨g'.trans g, λ a b hab, (finset.forall_mem_cons _ _).2 _⟩,
     exact ⟨hg (order_hom_class.mono g' hab), hg' hab⟩ }
 end

src/set_theory/cardinal/basic.lean

@@ -893,21 +893,14 @@ lemma mk_finsupp_of_fintype (α β : Type u) [fintype α] [has_zero β] :
 by simp
 
 theorem card_le_of_finset {α} (s : finset α) : (s.card : cardinal) ≤ #α :=
-begin
-  rw (_ : (s.card : cardinal) = #s),
-  { exact ⟨function.embedding.subtype _⟩ },
-  rw [cardinal.mk_fintype, fintype.card_coe]
-end
+@mk_coe_finset _ s ▸ mk_set_le _
 
 @[norm_cast] theorem nat_cast_pow {m n : ℕ} : (↑(pow m n) : cardinal) = m ^ n :=
 by simp only [cardinal.pow_cast_right, coe_pow]
 
 @[simp, norm_cast] theorem nat_cast_le {m n : ℕ} : (m : cardinal) ≤ n ↔ m ≤ n :=
-begin
-  rw [←lift_mk_fin, ←lift_mk_fin, lift_le],
-  exact ⟨λ ⟨⟨f, hf⟩⟩, by simpa only [fintype.card_fin] using fintype.card_le_of_injective f hf,
-    λ h, ⟨(fin.cast_le h).to_embedding⟩⟩
-end
+by rw [← lift_mk_fin, ← lift_mk_fin, lift_le, le_def, function.embedding.nonempty_iff_card_le,
+  fintype.card_fin, fintype.card_fin]
 
 @[simp, norm_cast] theorem nat_cast_lt {m n : ℕ} : (m : cardinal) < n ↔ m < n :=
 by simp [lt_iff_le_not_le, ←not_le]