-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this :
  LinearIndependent (ι := ChooseBasisIndex ℤ (𝓞 K)) ℝ (M := mixedSpace K)
    (Function.comp (β := (K →+* ℂ) → ℂ) (⇑(commMap K) : (a : (K →+* ℂ) → ℂ) → mixedSpace K)
      (⇑(canonicalEmbedding.latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
        (a : ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))
rw : finrank.{0, u_1} ℤ (𝓞 K) = finrank.{0, u_1} ℝ (mixedSpace K)
rw₁ : finrank ℚ K = finrank.{0, u_1} ℝ (mixedSpace K)
rw₂ :
  finrank ℚ K =
    finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ)
rw₃ :
  finrank ℚ K =
    Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ)
rw₄ :
  finrank ℚ K =
    Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ
rw₅ :
  finrank ℚ K = Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, 2
rw₆ :
  finrank ℚ K =
    Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ) 2
rw₇ :
  finrank ℚ K =
    Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2
rw₈ : finrank ℚ K = nrRealPlaces K + HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2
rw₉ : finrank ℚ K = nrRealPlaces K + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2
rw₁₀ :
  finrank ℚ K =
    Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2
rw₁₁ : finrank ℚ K = Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + nrComplexPlaces K * 2
rw₁₂ : finrank ℚ K = Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + 2 * nrComplexPlaces K
rw₁₃ :
  finrank ℚ K =
    Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      Fintype.card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ }
rw₁₄ :
  Fintype.card.{u_1} (K →+* ℂ) =
    Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      Fintype.card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ }
rw₁₅ :
  Fintype.card.{u_1} (K →+* ℂ) =
    Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      (Fintype.card.{u_1} (K →+* ℂ) - Fintype.card.{u_1} { x : K →+* ℂ // ComplexEmbedding.IsReal x })
rw₁₆ rw₁₇ : Fintype.card.{u_1} (K →+* ℂ) = Fintype.card.{u_1} (K →+* ℂ)
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)

Tactic:
rw [← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank, finrank_prod, finrank_pi,
      finrank_pi_fintype, Complex.finrank_real_complex, sum_const, card_univ, ← nrRealPlaces,
      ← nrComplexPlaces, ← card_real_embeddings, smul_eq_mul, mul_comm,
      ← card_complex_embeddings, ← NumberField.Embeddings.card K ℂ, Fintype.card_subtype_compl,
      Nat.add_sub_of_le (Fintype.card_subtype_le _)]

Premises used: Finset.card_univ, Fintype.card_subtype_le, Nat.add_sub_of_le, NumberField.Embeddings.card, Module.finrank_pi, NumberField.RingOfIntegers.rank, NumberField.InfinitePlace.nrRealPlaces, Module.finrank_pi_fintype, Module.finrank_eq_card_chooseBasisIndex, NumberField.InfinitePlace.card_real_embeddings, Complex.finrank_real_complex, mul_comm, NumberField.InfinitePlace.nrComplexPlaces, smul_eq_mul, Complex, Module.finrank_prod, Fintype.card_subtype_compl, NumberField.InfinitePlace.card_complex_embeddings, Finset.sum_const