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
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
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
have rw₁₁ : finrank ℚ K = Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + 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
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
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
have rw₁₂ : finrank ℚ K = Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + 2 * nrComplexPlaces 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)
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
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
have rw₁₃ : finrank ℚ K =
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
    Fintype.card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ }
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
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 φ }
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
have rw₁₄ : Fintype.card.{u_1} (K →+* ℂ) =
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
    Fintype.card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ }
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
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 φ }
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
have 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 })
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
⊢ Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)
have We : (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)
Tactic: classical
    -- We construct an `ℝ`-linear independent family from the image of
    -- `canonicalEmbedding.lattice_basis` by `commMap`
    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)
    -- and it's a basis since it has the right cardinality
    refine basisOfLinearIndependentOfCardEqFinrank this ?_
    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
We We₁ We₂ :
  (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)
⊢ Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)
have We₃ : ∀
  (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)
Tactic: classical
    -- We construct an `ℝ`-linear independent family from the image of
    -- `canonicalEmbedding.lattice_basis` by `commMap`
    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)
    -- and it's a basis since it has the right cardinality
    refine basisOfLinearIndependentOfCardEqFinrank this ?_
    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
x : mixedSpace K
⊢ Eq (α := Set (mixedSpace K))
    (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
      (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
        (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))
    (Set.image (α := K) (⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (mixedEmbedding K))) : (a : K) → mixedSpace K)
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K)))
have rw : Eq (α := Set (mixedSpace K))
  (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
    (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
      (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))
  (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
    (Function.comp (β := K) (⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (mixedEmbedding K))) : (a : K) → mixedSpace K)
      (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K)))
Tactic: rw [← Set.range_comp]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
⊢ Membership.mem (γ := Submodule ℤ (mixedSpace K))
      (Submodule.span ℤ
        (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
          (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
            (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
      x ↔
    Membership.mem (γ := Submodule ℤ (mixedSpace K)) (mixedEmbedding.integerLattice K) x
have rw : Membership.mem (γ := Submodule ℤ (mixedSpace K))
    (Submodule.span ℤ
      (Set.image (α := K) (⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (mixedEmbedding K))) : (a : K) → mixedSpace K)
        (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
          (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K))))
    x ↔
  Membership.mem (γ := Submodule ℤ (mixedSpace K)) (mixedEmbedding.integerLattice K) x
Tactic: rw [show Set.range (latticeBasis K) =
      (mixedEmbedding K).toIntAlgHom.toLinearMap '' (Set.range (integralBasis K)) by
    rw [← Set.range_comp]; exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
⊢ Membership.mem (γ := Submodule ℤ (mixedSpace K))
      (Submodule.span ℤ
        (Set.image (α := K) (⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (mixedEmbedding K))) : (a : K) → mixedSpace K)
          (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
            (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K))))
      x ↔
    Membership.mem (γ := Submodule ℤ (mixedSpace K)) (mixedEmbedding.integerLattice K) x
have rw : Membership.mem (γ := Set (mixedSpace K))
    ((⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (mixedEmbedding K))) : (a : K) → mixedSpace K) ''
      (↑(Submodule.span ℤ
            (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
              (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K))) :
        Set K))
    x ↔
  Membership.mem (γ := Submodule ℤ (mixedSpace K)) (mixedEmbedding.integerLattice K) x
Tactic: rw [← Submodule.map_span, ← SetLike.mem_coe, Submodule.map_coe]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
⊢ Membership.mem (γ := Set (mixedSpace K))
      ((⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (mixedEmbedding K))) : (a : K) → mixedSpace K) ''
        (↑(Submodule.span ℤ
              (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                (⇑(integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K))) :
          Set K))
      x ↔
    Membership.mem (γ := Submodule ℤ (mixedSpace K)) (mixedEmbedding.integerLattice K) x
have simp : (∃ (a : 𝓞 K),
    (AlgHom.toLinearMap (RingHom.toIntAlgHom (mixedEmbedding K)) : (a : K) → mixedSpace K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a) =
      x) ↔
  Membership.mem (γ := Submodule ℤ (mixedSpace K)) (mixedEmbedding.integerLattice K) x
Tactic: simp only [Set.mem_image, SetLike.mem_coe, mem_span_integralBasis K,
    RingHom.mem_range, exists_exists_eq_and]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ DiscreteTopology.{u_1} ↥(mixedEmbedding.integerLattice K)
have rw : DiscreteTopology.{u_1}
  ↥(Submodule.span ℤ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
Tactic: rw [← span_latticeBasis]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ DiscreteTopology.{u_1} ↥(mixedEmbedding.integerLattice K)
have rw : DiscreteTopology.{u_1}
  ↥(Submodule.span ℤ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
Tactic: classical
  rw [← span_latticeBasis]
  infer_instance
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ MeasureTheory.IsAddFundamentalDomain.{u_1, u_1} ↥(mixedEmbedding.integerLattice K) (α := mixedSpace K)
    (ZSpan.fundamentalDomain (ι := ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K))
    (MeasureTheory.volume : MeasureTheory.Measure (mixedSpace K))
have rw : MeasureTheory.IsAddFundamentalDomain.{u_1, u_1}
  ↥(Submodule.span ℤ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
  (α := mixedSpace K) (ZSpan.fundamentalDomain (ι := ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K))
  (MeasureTheory.volume : MeasureTheory.Measure (mixedSpace K))
Tactic: rw [← span_latticeBasis]