chore(data/fintype/basic): set.to_finset_univ generalization (#11174)

leanprover-community · Jan 4, 2022 · 49cbce2 · 49cbce2
1 parent 037147e
commit 49cbce2
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 8 deletions.
diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean
@@ -817,10 +817,7 @@ lemma card_common_neighbors_top [decidable_eq V] {v w : V} (h : v ≠ w) :
 begin
   simp only [common_neighbors_top_eq, ← set.to_finset_card, set.to_finset_sdiff],
   rw finset.card_sdiff,
-  { congr' 1,
-    { simp_rw [← finset.card_univ, ← set.to_finset_univ],
-      congr, },
-    { simp [h], } },
+  { simp [finset.card_univ, h], },
   { simp only [←set.subset_iff_to_finset_subset, set.subset_univ] },
 end
 

diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean
@@ -1303,8 +1303,8 @@ by { ext, simp [finset.mem_powerset_len] }
   fintype.card {s : finset α // s.card = k} = nat.choose (fintype.card α) k :=
 by simp [fintype.subtype_card, finset.card_univ]
 
-@[simp] lemma set.to_finset_univ [fintype α] :
-  (set.univ : set α).to_finset = finset.univ :=
+@[simp] lemma set.to_finset_univ [hu : fintype (set.univ : set α)] [fintype α] :
+  @set.to_finset _ (set.univ : set α) hu = finset.univ :=
 by { ext, simp only [set.mem_univ, mem_univ, set.mem_to_finset] }
 
 @[simp] lemma set.to_finset_eq_empty_iff {s : set α} [fintype s] :

diff --git a/src/group_theory/specific_groups/cyclic.lean b/src/group_theory/specific_groups/cyclic.lean
@@ -257,8 +257,7 @@ lemma is_cyclic.image_range_order_of (ha : ∀ x : α, x ∈ zpowers a) :
   finset.image (λ i, a ^ i) (range (order_of a)) = univ :=
 begin
   simp_rw [←set_like.mem_coe] at ha,
-  simp only [image_range_order_of, set.eq_univ_iff_forall.mpr ha],
-  convert set.to_finset_univ
+  simp only [image_range_order_of, set.eq_univ_iff_forall.mpr ha, set.to_finset_univ],
 end
 
 @[to_additive]