diff --git a/Mathlib/Data/Finset/Density.lean b/Mathlib/Data/Finset/Density.lean
index 61979a81db062..c486e085f6987 100644
--- a/Mathlib/Data/Finset/Density.lean
+++ b/Mathlib/Data/Finset/Density.lean
@@ -145,9 +145,10 @@ lemma dens_sdiff_add_dens_inter (s t : Finset α) : dens (s \ t) + dens (s ∩ t
 lemma dens_inter_add_dens_sdiff (s t : Finset α) : dens (s ∩ t) + dens (s \ t) = dens s := by
   rw [add_comm, dens_sdiff_add_dens_inter]
 
-lemma dens_filter_add_dens_filter_not_eq_dens
+lemma dens_filter_add_dens_filter_not_eq_dens {α : Type*} [Fintype α] {s : Finset α}
     (p : α → Prop) [DecidablePred p] [∀ x, Decidable (¬p x)] :
     dens (s.filter p) + dens (s.filter fun a ↦ ¬ p a) = dens s := by
+  classical
   rw [← dens_union_of_disjoint (disjoint_filter_filter_neg ..), filter_union_filter_neg_eq]
 
 lemma dens_union_le (s t : Finset α) : dens (s ∪ t) ≤ dens s + dens t :=
diff --git a/Mathlib/Data/Fintype/CardEmbedding.lean b/Mathlib/Data/Fintype/CardEmbedding.lean
index bd6ec0bce1dbf..da9e62d27dcf0 100644
--- a/Mathlib/Data/Fintype/CardEmbedding.lean
+++ b/Mathlib/Data/Fintype/CardEmbedding.lean
@@ -48,7 +48,7 @@ theorem card_embedding_eq {α β : Type*} [Fintype α] [Fintype β] [emb : Finty
 
 /-- The cardinality of embeddings from an infinite type to a finite type is zero.
 This is a re-statement of the pigeonhole principle. -/
-theorem card_embedding_eq_of_infinite {α β : Type*} [Infinite α] [Fintype β] [Fintype (α ↪ β)] :
+theorem card_embedding_eq_of_infinite {α β : Type*} [Infinite α] [Finite β] [Fintype (α ↪ β)] :
     ‖α ↪ β‖ = 0 :=
   card_eq_zero
 
diff --git a/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean b/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean
index cd57a471a655c..2e1d5ed83ed2b 100644
--- a/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean
+++ b/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean
@@ -24,7 +24,7 @@ open LinearMap
 section LinearIndependent
 
 variable {K V : Type*} [DivisionRing K] [AddCommGroup V] [Module K V]
-variable [Fintype K] [Fintype V]
+variable [Fintype K] [Finite V]
 
 local notation "q" => Fintype.card K
 local notation "n" => FiniteDimensional.finrank K V