awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ (↑((((Basis.repr (stdBasis K) : (a : mixedSpace K) → index K →₀ ℝ)
                ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x : mixedSpace K) :
              index K →₀ ℝ) :
            (a : index K) → ℝ)
          c) :
      ℂ) =
    (matrixToStdBasis K *ᵥ x ∘ (⇑(indexEquiv K) : (a : index K) → K →+* ℂ)) c
have simp_rw : (↑((((Basis.repr (stdBasis K) :
                (a : mixedSpace K) →
                  { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2 →₀ ℝ)
              (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (x (↑w : InfinitePlace K).embedding).re,
                fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ x (↑w : InfinitePlace K).embedding) :
            { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2 →₀ ℝ) :
          (a : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) → ℝ)
        c) :
    ℂ) =
  HAdd.hAdd (α := ℂ)
    (∑ x_1 : { w : InfinitePlace K // w.IsReal },
      fromBlocks (m := { w : InfinitePlace K // w.IsComplex } × Fin 2) 1 0 0
          (submatrix (blockDiagonal fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I])
            Prod.swap Prod.swap)
          c (Sum.inl x_1) *
        x (↑x_1 : InfinitePlace K).embedding)
    (∑ x_1 : { w : InfinitePlace K // w.IsComplex },
      (fromBlocks (l := { w : InfinitePlace K // w.IsReal }) (m := { w : InfinitePlace K // w.IsComplex } × Fin 2) 1 0 0
            (submatrix
              (blockDiagonal fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I])
              Prod.swap Prod.swap)
            c (Sum.inr (x_1, 0)) *
          x (↑x_1 : InfinitePlace K).embedding +
        fromBlocks (l := { w : InfinitePlace K // w.IsReal }) (m := { w : InfinitePlace K // w.IsComplex } × Fin 2) 1 0
            0
            (submatrix
              (blockDiagonal fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I])
              Prod.swap Prod.swap)
            c (Sum.inr (x_1, 1)) *
          x (ComplexEmbedding.conjugate (↑x_1 : InfinitePlace K).embedding)))
Tactic: simp_rw [commMap, matrixToStdBasis, LinearMap.coe_mk, AddHom.coe_mk,
    mulVec, dotProduct, Function.comp_apply, index, Fintype.sum_sum_type,
    diagonal_one, reindex_apply, ← univ_product_univ, sum_product,
    indexEquiv_apply_isReal, Fin.sum_univ_two, indexEquiv_apply_isComplex_fst,
    indexEquiv_apply_isComplex_snd, smul_of, smul_cons, smul_eq_mul,
    mul_one, Matrix.smul_empty, Equiv.prodComm_symm, Equiv.coe_prodComm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w : InfinitePlace K // w.IsComplex }
⊢ HSub.hSub (β := ℂ) (x (↑w : InfinitePlace K).embedding)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) (x (↑w : InfinitePlace K).embedding) : ℂ) /
      (2 * I) =
    -(2⁻¹ * I * x (↑w : InfinitePlace K).embedding) +
      HMul.hMul (β := ℂ) (2⁻¹ * I) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x (↑w : InfinitePlace K).embedding) : ℂ)
have inr : x (↑w : InfinitePlace K).embedding * I⁻¹ * (1 / 2) +
    HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x (↑w : InfinitePlace K).embedding) : ℂ) I⁻¹ * (-1 / 2) =
  x (↑w : InfinitePlace K).embedding * I * (-1 / 2) +
    HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x (↑w : InfinitePlace K).embedding) : ℂ) I * (1 / 2)
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)
have 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 →+* ℂ) → ℂ))
Tactic: have := LinearIndependent.map (LinearIndependent.restrict_scalars
      (by { simpa only [Complex.real_smul, mul_one] using Complex.ofReal_injective })
      (canonicalEmbedding.latticeBasis K).linearIndependent)
      (disjoint_span_commMap_ker K)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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 →+* ℂ) → ℂ))
⊢ Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)
have refine : Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
Tactic: refine basisOfLinearIndependentOfCardEqFinrank this ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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 →+* ℂ) → ℂ))
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
have rw : finrank.{0, u_1} ℤ (𝓞 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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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)
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
have rw₁ : finrank ℚ 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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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)
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
have rw₂ : finrank ℚ K =
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
    finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ)
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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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 } → ℂ)
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
have rw₃ : finrank ℚ K =
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
    finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ)
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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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 } → ℂ)
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
have rw₄ : finrank ℚ K =
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ
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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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 ℝ ℂ
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
have rw₅ : finrank ℚ K = Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, 2
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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
have rw₆ : finrank ℚ K =
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
    HSMul.hSMul (β := ℕ) (card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ) 2
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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
have rw₇ : finrank ℚ K =
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
    HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2
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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
have rw₈ : finrank ℚ K = nrRealPlaces K + HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2
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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
have rw₉ : finrank ℚ K = nrRealPlaces K + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2
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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
have rw₁₀ : finrank ℚ K =
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2
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 _)]