feat: add card_eq_NrRealPlaces_add_NrComplexPlaces (#11745)

We add `card_eq_NrRealPlaces_add_NrComplexPlaces: Fintype.card (InfinitePlace K).card =  NrRealPlaces K + NrComplexPlaces K` for a number field `K`.

Author: riccardobrasca

Mathlib/NumberTheory/NumberField/Embeddings.lean

@@ -415,6 +415,11 @@ theorem isReal_or_isComplex (w : InfinitePlace K) : IsReal w ∨ IsComplex w :=
 theorem ne_of_isReal_isComplex {w w' : InfinitePlace K} (h : IsReal w) (h' : IsComplex w') :
     w ≠ w' := fun h_eq ↦ not_isReal_iff_isComplex.mpr h' (h_eq ▸ h)
 
+variable (K) in
+theorem disjoint_isReal_isComplex :
+    Disjoint {(w : InfinitePlace K) | IsReal w} {(w : InfinitePlace K) | IsComplex w} :=
+  Set.disjoint_iff.2 <| fun _ hw ↦ not_isReal_iff_isComplex.2 hw.2 hw.1
+
 /-- The real embedding associated to a real infinite place. -/
 noncomputable def embedding_of_isReal {w : InfinitePlace K} (hw : IsReal w) : K →+* ℝ :=
   ComplexEmbedding.IsReal.embedding (isReal_iff.mp hw)
@@ -581,6 +586,12 @@ theorem card_real_embeddings :
     card { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } = NrRealPlaces K := Fintype.card_congr mkReal
 #align number_field.infinite_place.card_real_embeddings NumberField.InfinitePlace.card_real_embeddings
 
+theorem card_eq_nrRealPlaces_add_nrComplexPlaces :
+    Fintype.card (InfinitePlace K) = NrRealPlaces K + NrComplexPlaces K := by
+  convert Fintype.card_subtype_or_disjoint (IsReal (K := K)) (IsComplex (K := K))
+    (disjoint_isReal_isComplex K) using 1
+  exact (Fintype.card_of_subtype _ (fun w ↦ ⟨fun _ ↦ isReal_or_isComplex w, fun _ ↦ by simp⟩)).symm
+
 theorem card_complex_embeddings :
     card { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } = 2 * NrComplexPlaces K := by
   suffices ∀ w : { w : InfinitePlace K // IsComplex w }, (Finset.univ.filter