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
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
have rw : finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
    finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
  finrank ℚ K
Tactic: rw [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
rw :
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
have rw₁ : Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
    finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
  finrank ℚ K
Tactic: rw [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
rw :
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₁ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
have rw₂ : Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ =
  finrank ℚ K
Tactic: rw [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
rw :
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₁ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₂ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ =
    finrank ℚ K
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
have rw₃ : Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, 2 = finrank ℚ K
Tactic: rw [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
rw :
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₁ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₂ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ =
    finrank ℚ K
rw₃ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, 2 = finrank ℚ K
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
have rw₄ : Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
    HSMul.hSMul (β := ℕ) (card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ) 2 =
  finrank ℚ K
Tactic: rw [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
rw :
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₁ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₂ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ =
    finrank ℚ K
rw₃ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, 2 = finrank ℚ K
rw₄ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ) 2 =
    finrank ℚ K
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
have rw₅ : Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
    HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 =
  finrank ℚ K
Tactic: rw [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
rw :
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₁ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₂ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ =
    finrank ℚ K
rw₃ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, 2 = finrank ℚ K
rw₄ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ) 2 =
    finrank ℚ K
rw₅ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 =
    finrank ℚ K
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
have rw₆ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 = finrank ℚ K
Tactic: rw [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
rw :
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₁ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₂ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ =
    finrank ℚ K
rw₃ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, 2 = finrank ℚ K
rw₄ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ) 2 =
    finrank ℚ K
rw₅ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 =
    finrank ℚ K
rw₆ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 = finrank ℚ K
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
have rw₇ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 = finrank ℚ K
Tactic: rw [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
rw :
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₁ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₂ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ =
    finrank ℚ K
rw₃ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, 2 = finrank ℚ K
rw₄ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ) 2 =
    finrank ℚ K
rw₅ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 =
    finrank ℚ K
rw₆ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 = finrank ℚ K
rw₇ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 = finrank ℚ K
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
have rw₈ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 =
  finrank ℚ K
Tactic: rw [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
rw :
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₁ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₂ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ =
    finrank ℚ K
rw₃ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, 2 = finrank ℚ K
rw₄ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ) 2 =
    finrank ℚ K
rw₅ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 =
    finrank ℚ K
rw₆ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 = finrank ℚ K
rw₇ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 = finrank ℚ K
rw₈ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 =
    finrank ℚ K
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
have rw₉ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + nrComplexPlaces K * 2 = finrank ℚ K
Tactic: rw [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
rw :
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₁ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₂ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ =
    finrank ℚ K
rw₃ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, 2 = finrank ℚ K
rw₄ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ) 2 =
    finrank ℚ K
rw₅ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 =
    finrank ℚ K
rw₆ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 = finrank ℚ K
rw₇ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 = finrank ℚ K
rw₈ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 =
    finrank ℚ K
rw₉ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + nrComplexPlaces K * 2 = finrank ℚ K
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
have rw₁₀ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + 2 * nrComplexPlaces K = finrank ℚ K
Tactic: rw [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
rw :
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₁ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₂ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ =
    finrank ℚ K
rw₃ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, 2 = finrank ℚ K
rw₄ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ) 2 =
    finrank ℚ K
rw₅ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 =
    finrank ℚ K
rw₆ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 = finrank ℚ K
rw₇ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 = finrank ℚ K
rw₈ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 =
    finrank ℚ K
rw₉ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + nrComplexPlaces K * 2 = finrank ℚ K
rw₁₀ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + 2 * nrComplexPlaces K = finrank ℚ K
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
have rw₁₁ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
    Fintype.card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } =
  finrank ℚ K
Tactic: rw [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
rw :
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₁ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₂ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ =
    finrank ℚ K
rw₃ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, 2 = finrank ℚ K
rw₄ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ) 2 =
    finrank ℚ K
rw₅ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 =
    finrank ℚ K
rw₆ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 = finrank ℚ K
rw₇ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 = finrank ℚ K
rw₈ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 =
    finrank ℚ K
rw₉ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + nrComplexPlaces K * 2 = finrank ℚ K
rw₁₀ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + 2 * nrComplexPlaces K = finrank ℚ K
rw₁₁ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      Fintype.card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } =
    finrank ℚ K
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
have rw₁₂ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
    Fintype.card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } =
  Fintype.card.{u_1} (K →+* ℂ)
Tactic: rw [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
rw :
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₁ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₂ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ =
    finrank ℚ K
rw₃ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, 2 = finrank ℚ K
rw₄ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ) 2 =
    finrank ℚ K
rw₅ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 =
    finrank ℚ K
rw₆ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 = finrank ℚ K
rw₇ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 = finrank ℚ K
rw₈ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 =
    finrank ℚ K
rw₉ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + nrComplexPlaces K * 2 = finrank ℚ K
rw₁₀ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + 2 * nrComplexPlaces K = finrank ℚ K
rw₁₁ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      Fintype.card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } =
    finrank ℚ K
rw₁₂ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      Fintype.card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } =
    Fintype.card.{u_1} (K →+* ℂ)
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
have rw₁₃ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
    (Fintype.card.{u_1} (K →+* ℂ) - Fintype.card.{u_1} { x : K →+* ℂ // ComplexEmbedding.IsReal x }) =
  Fintype.card.{u_1} (K →+* ℂ)
Tactic: rw [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 _)]