chore(*): golf (#14939)

Some golfs I made while working on a large refactor.

src/data/W/cardinal.lean

@@ -69,11 +69,7 @@ calc cardinal.sum (λ a : α, m ^ #(β a))
       (λ a : α, m ^ #(β a)) :
   mul_le_mul' (le_max_left _ _) le_rfl
 ... = m : mul_eq_left.{u} (le_max_right _ _)
-  (cardinal.sup_le (λ i, begin
-    cases lt_aleph_0.1 (lt_aleph_0_of_fintype (β i)) with n hn,
-    rw [hn],
-    exact power_nat_le (le_max_right _ _)
-  end))
+  (cardinal.sup_le (λ i, pow_le (le_max_right _ _) (lt_aleph_0_of_fintype _)))
   (pos_iff_ne_zero.1 (order.succ_le_iff.1
     begin
       rw [succ_zero],

src/data/analysis/filter.lean

@@ -187,8 +187,7 @@ protected def cofinite [decidable_eq α] : (@cofinite α).realizer := ⟨finset
   inf_le_right := λ s t a, mt (finset.mem_union_right _) },
 filter_eq $ set.ext $ λ x,
 ⟨λ ⟨s, h⟩, s.finite_to_set.subset (compl_subset_comm.1 h),
- λ ⟨fs⟩, by exactI ⟨xᶜ.to_finset, λ a (h : a ∉ xᶜ.to_finset),
-  classical.by_contradiction $ λ h', h (mem_to_finset.2 h')⟩⟩⟩
+ λ h, ⟨h.to_finset, by simp⟩⟩⟩
 
 /-- Construct a realizer for filter bind -/
 protected def bind {f : filter α} {m : α → filter β} (F : f.realizer) (G : ∀ i, (m i).realizer) :

src/data/set/countable.lean

@@ -208,10 +208,8 @@ begin
   refine countable.mono _ (countable_range
     (λ t : finset s, {a | ∃ h:a ∈ s, subtype.mk a h ∈ t})),
   rintro t ⟨⟨ht⟩, ts⟩, resetI,
-  refine ⟨finset.univ.map (embedding_of_subset _ _ ts),
-    set.ext $ λ a, _⟩,
-  suffices : a ∈ s ∧ a ∈ t ↔ a ∈ t, by simpa,
-  exact ⟨and.right, λ h, ⟨ts h, h⟩⟩
+  refine ⟨finset.univ.map (embedding_of_subset _ _ ts), set.ext $ λ a, _⟩,
+  simpa using @ts a
 end
 
 lemma countable_pi {π : α → Type*} [fintype α] {s : Πa, set (π a)} (hs : ∀a, (s a).countable) :

src/data/set/finite.lean

@@ -496,7 +496,6 @@ lemma finite_range_const {c : β} : (range (λ x : α, c)).finite :=
 
 end set_finite_constructors
 
-
 /-! ### Properties -/
 
 instance finite.inhabited : inhabited {s : set α // s.finite} := ⟨⟨∅, finite_empty⟩⟩
@@ -579,19 +578,12 @@ let ⟨I, Ifin, hI⟩ := finite_subset_Union tfin h in
 @[elab_as_eliminator]
 theorem finite.induction_on {C : set α → Prop} {s : set α} (h : s.finite)
   (H0 : C ∅) (H1 : ∀ {a s}, a ∉ s → set.finite s → C s → C (insert a s)) : C s :=
-let ⟨t⟩ := h in by exactI
-match s.to_finset, @mem_to_finset _ s _ with
-| ⟨l, nd⟩, al := begin
-    change ∀ a, a ∈ l ↔ a ∈ s at al,
-    clear _let_match _match t h, revert s nd al,
-    refine multiset.induction_on l _ (λ a l IH, _); intros s nd al,
-    { rw show s = ∅, from eq_empty_iff_forall_not_mem.2 (by simpa using al),
-      exact H0 },
-    { rw ← show insert a {x | x ∈ l} = s, from set.ext (by simpa using al),
-      cases multiset.nodup_cons.1 nd with m nd',
-      refine H1 _ ⟨finset.subtype.fintype ⟨l, nd'⟩⟩ (IH nd' (λ _, iff.rfl)),
-      exact m }
-  end
+begin
+  lift s to finset α using h,
+  induction s using finset.cons_induction_on with a s ha hs,
+  { rwa [finset.coe_empty] },
+  { rw [finset.coe_cons],
+    exact @H1 a s ha (set.finite_of_fintype _) hs }
 end
 
 @[elab_as_eliminator]
@@ -632,7 +624,6 @@ end⟩
 
 end
 
-
 /-! ### Cardinality -/
 
 theorem empty_card : fintype.card (∅ : set α) = 0 := rfl

src/linear_algebra/dimension.lean

@@ -490,10 +490,9 @@ theorem mk_eq_mk_of_basis (v : basis ι R M) (v' : basis ι' R M) :
   cardinal.lift.{w'} (#ι) = cardinal.lift.{w} (#ι') :=
 begin
   haveI := nontrivial_of_invariant_basis_number R,
-  by_cases h : #ι < ℵ₀,
+  casesI fintype_or_infinite ι,
   { -- `v` is a finite basis, so by `basis_fintype_of_finite_spans` so is `v'`.
-    haveI : fintype ι := (cardinal.lt_aleph_0_iff_fintype.mp h).some,
-    haveI : fintype (range v) := set.fintype_range ⇑v,
+    haveI : fintype (range v) := set.fintype_range v,
     haveI := basis_fintype_of_finite_spans _ v.span_eq v',
     -- We clean up a little:
     rw [cardinal.mk_fintype, cardinal.mk_fintype],
@@ -506,16 +505,10 @@ begin
     -- so by `infinite_basis_le_maximal_linear_independent`, `v'` is at least as big,
     -- and then applying `infinite_basis_le_maximal_linear_independent` again
     -- we see they have the same cardinality.
-    simp only [not_lt] at h,
-    haveI : infinite ι := cardinal.infinite_iff.mpr h,
     have w₁ :=
       infinite_basis_le_maximal_linear_independent' v _ v'.linear_independent v'.maximal,
-    haveI : infinite ι' := cardinal.infinite_iff.mpr (begin
-      apply cardinal.lift_le.{w' w}.mp,
-      have p := (cardinal.lift_le.mpr h).trans w₁,
-      rw cardinal.lift_aleph_0 at ⊢ p,
-      exact p,
-    end),
+    rcases cardinal.lift_mk_le'.mp w₁ with ⟨f⟩,
+    haveI : infinite ι' := infinite.of_injective f f.2,
     have w₂ :=
       infinite_basis_le_maximal_linear_independent' v' _ v.linear_independent v.maximal,
     exact le_antisymm w₁ w₂, }
@@ -609,7 +602,7 @@ begin
     { exact not_le_of_lt this ⟨set.embedding_of_subset _ _ hs⟩ },
     refine lt_of_le_of_lt (le_trans cardinal.mk_Union_le_sum_mk
       (cardinal.sum_le_sum _ (λ _, ℵ₀) _)) _,
-    { exact λ j, le_of_lt (cardinal.lt_aleph_0_iff_finite.2 $ (finset.finite_to_set _).image _) },
+    { exact λ j, (cardinal.lt_aleph_0_of_fintype _).le },
     { simpa } },
 end
 

src/topology/constructions.lean

@@ -126,19 +126,15 @@ instance : topological_space (cofinite_topology α) :=
 { is_open := λ s, s.nonempty → set.finite sᶜ,
   is_open_univ := by simp,
   is_open_inter := λ s t, begin
-    classical,
     rintros hs ht ⟨x, hxs, hxt⟩,
-    haveI := set.finite.fintype (hs ⟨x, hxs⟩),
-    haveI := set.finite.fintype (ht ⟨x, hxt⟩),
     rw compl_inter,
-    exact set.finite.intro (sᶜ.fintype_union tᶜ),
+    exact (hs ⟨x, hxs⟩).union (ht ⟨x, hxt⟩),
   end,
   is_open_sUnion := begin
     rintros s h ⟨x, t, hts, hzt⟩,
     rw set.compl_sUnion,
-    apply set.finite.sInter _ (h t hts ⟨x, hzt⟩),
-    simp [hts]
-    end }
+    exact set.finite.sInter (mem_image_of_mem _ hts) (h t hts ⟨x, hzt⟩),
+  end }
 
 lemma is_open_iff {s : set (cofinite_topology α)} :
   is_open s ↔ (s.nonempty → (sᶜ).finite) := iff.rfl