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
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
rw :
  finrank.{0, u_1} ℤ (𝓞 K) =
    Fintype.card.{u_1} (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
rw₁ : finrank.{0, u_1} ℤ (𝓞 K) = finrank.{0, u_1} ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)
⊢ Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) =
    Fintype.card.{u_1} (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
have rw₂ : finrank.{0, u_1} ℤ (𝓞 K) = finrank.{0, u_1} ℤ (𝓞 K)
Tactic: rw [← finrank_eq_card_chooseBasisIndex, ← finrank_eq_card_chooseBasisIndex,
      fractionalIdeal_rank]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) :=
  Fintype.equivOfCardEq ⋯
⊢ Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)
have refine : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)
Tactic: refine Basis.reindex ?_ e
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) :=
  Fintype.equivOfCardEq ⋯
this :
  IsUnit (M := ℝ)
    (((Basis.det (latticeBasis K) : mixedSpace K [⋀^ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℝ] ℝ) :
          (a : ChooseBasisIndex ℤ (𝓞 K) → mixedSpace K) → ℝ)
        (Function.comp (β := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
          (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (⇑(basisOfFractionalIdeal K I :
                  Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
              (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
            (⇑e :
              (a : ChooseBasisIndex ℤ (𝓞 K)) →
                ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))) :
      ℝ)
⊢ Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)
have this₁ : LinearIndependent (ι := ChooseBasisIndex ℤ (𝓞 K)) ℝ (M := mixedSpace K)
    (Function.comp (β := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
      (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
        (⇑(basisOfFractionalIdeal K I :
              Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
          (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
        (⇑e :
          (a : ChooseBasisIndex ℤ (𝓞 K)) →
            ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))) ∧
  Eq (α := Submodule ℝ (mixedSpace K))
    (Submodule.span ℝ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (Function.comp (β := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
          (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (⇑(basisOfFractionalIdeal K I :
                  Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
              (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
            (⇑e :
              (a : ChooseBasisIndex ℤ (𝓞 K)) →
                ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))))))
    ⊤
Tactic: rw [← Basis.is_basis_iff_det] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) :=
  Fintype.equivOfCardEq ⋯
this :
  LinearIndependent (ι := ChooseBasisIndex ℤ (𝓞 K)) ℝ (M := mixedSpace K)
      (Function.comp (β := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
        (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(basisOfFractionalIdeal K I :
                Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
            (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
          (⇑e :
            (a : ChooseBasisIndex ℤ (𝓞 K)) →
              ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))) ∧
    Eq (α := Submodule ℝ (mixedSpace K))
      (Submodule.span ℝ
        (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
          (Function.comp (β := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
            (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
              (⇑(basisOfFractionalIdeal K I :
                    Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
                (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
              (⇑e :
                (a : ChooseBasisIndex ℤ (𝓞 K)) →
                  ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))))))
      ⊤
⊢ LE.le (α := Submodule ℝ (mixedSpace K)) ⊤
    (Submodule.span ℝ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (Function.comp (β := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
          (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (⇑(basisOfFractionalIdeal K I :
                  Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
              (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
            (⇑e :
              (a : ChooseBasisIndex ℤ (𝓞 K)) →
                ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))))))
have rw : LE.le.{u_1} (α := Submodule ℝ (mixedSpace K)) ⊤ ⊤
Tactic: rw [this.2]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) :=
  Fintype.equivOfCardEq ⋯
⊢ Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)
have suffices : IsUnit (M := ℝ)
  (((Basis.det (latticeBasis K) : mixedSpace K [⋀^ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℝ] ℝ) :
        (a : ChooseBasisIndex ℤ (𝓞 K) → mixedSpace K) → ℝ)
      (Function.comp (β := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
        (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(basisOfFractionalIdeal K I :
                Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
            (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
          (⇑e :
            (a : ChooseBasisIndex ℤ (𝓞 K)) →
              ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))) :
    ℝ)
Tactic: suffices IsUnit ((latticeBasis K).det ((mixedEmbedding K) ∘ (basisOfFractionalIdeal K I) ∘ e)) by
    rw [← Basis.is_basis_iff_det] at this
    exact Basis.mk this.1 (by rw [this.2])
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) :=
  Fintype.equivOfCardEq ⋯
⊢ IsUnit (M := ℝ)
    (((Basis.det (latticeBasis K) : mixedSpace K [⋀^ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℝ] ℝ) :
          (a : ChooseBasisIndex ℤ (𝓞 K) → mixedSpace K) → ℝ)
        (Function.comp (β := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
          (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (⇑(basisOfFractionalIdeal K I :
                  Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
              (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
            (⇑e :
              (a : ChooseBasisIndex ℤ (𝓞 K)) →
                ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))) :
      ℝ)
have rw : ¬(↑I : FractionalIdeal (𝓞 K)⁰ K) = 0
Tactic: rw [isUnit_iff_ne_zero, ne_eq, ← abs_eq_zero.not, det_basisOfFractionalIdeal_eq_norm,
    Rat.cast_eq_zero, FractionalIdeal.absNorm_eq_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ Eq (α := Set (mixedSpace K))
    (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
      (⇑(fractionalIdealLatticeBasis K I :
            Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
        (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K))
    (Set.image (α := K) (⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (mixedEmbedding K))) : (a : K) → mixedSpace K)
      (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
        (⇑(basisOfFractionalIdeal K I :
              Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
          (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)))
have rw : Eq (α := Set (mixedSpace K))
  (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
    (⇑(fractionalIdealLatticeBasis K I :
          Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
      (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K))
  (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
    (Function.comp (β := K) (⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (mixedEmbedding K))) : (a : K) → mixedSpace K)
      (⇑(basisOfFractionalIdeal K I :
            Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
        (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) 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
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ Membership.mem (γ := Submodule ℤ (mixedSpace K))
      (Submodule.span ℤ
        (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(fractionalIdealLatticeBasis K I :
                Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
            (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)))
      x ↔
    Membership.mem (γ := Set (mixedSpace K))
      ((⇑(mixedEmbedding K) : (a : K) → mixedSpace K) '' (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Set 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 ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(basisOfFractionalIdeal K I :
                Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
            (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K))))
    x ↔
  Membership.mem (γ := Set (mixedSpace K))
    ((⇑(mixedEmbedding K) : (a : K) → mixedSpace K) '' (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Set K)) x
Tactic: rw [show Set.range (fractionalIdealLatticeBasis K I) =
        (mixedEmbedding K).toIntAlgHom.toLinearMap '' (Set.range (basisOfFractionalIdeal K I)) by
      rw [← Set.range_comp]
      exact congr_arg Set.range (funext (fun i ↦ fractionalIdealLatticeBasis_apply K I i))]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ 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 ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (⇑(basisOfFractionalIdeal K I :
                  Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
              (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K))))
      x ↔
    Membership.mem (γ := Set (mixedSpace K))
      ((⇑(mixedEmbedding K) : (a : K) → mixedSpace K) '' (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Set K)) x
have rw : Membership.mem (γ := Set (mixedSpace K))
    ((⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (mixedEmbedding K))) : (a : K) → mixedSpace K) ''
      (↑(Submodule.span ℤ
            (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
              (⇑(basisOfFractionalIdeal K I :
                    Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
                (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K))) :
        Set K))
    x ↔
  Membership.mem (γ := Set (mixedSpace K))
    ((⇑(mixedEmbedding K) : (a : K) → mixedSpace K) '' (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Set 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
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ (↑(Submodule.span ℤ
          (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (⇑(basisOfFractionalIdeal K I :
                  Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
              (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K))) :
      Set K) =
    (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Set K)
have h : ∀ (x : K),
  x ∈
      (↑(Submodule.span ℤ
            (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
              (⇑(basisOfFractionalIdeal K I :
                    Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
                (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K))) :
        Set K) ↔
    x ∈ (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Set K)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ Membership.mem (γ := Set (mixedSpace K))
      ((⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (mixedEmbedding K))) : (a : K) → mixedSpace K) ''
        (↑(Submodule.span ℤ
              (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
                (⇑(basisOfFractionalIdeal K I :
                      Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
                  (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K))) :
          Set K))
      x ↔
    Membership.mem (γ := Set (mixedSpace K))
      ((⇑(mixedEmbedding K) : (a : K) → mixedSpace K) '' (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Set K)) x
have rw : Membership.mem (γ := Set (mixedSpace K))
    ((⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (mixedEmbedding K))) : (a : K) → mixedSpace K) ''
      (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Set K))
    x ↔
  Membership.mem (γ := Set (mixedSpace K))
    ((⇑(mixedEmbedding K) : (a : K) → mixedSpace K) '' (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Set K)) x
Tactic: rw [show Submodule.span ℤ (Set.range (basisOfFractionalIdeal K I)) = (I : Set K) by
        ext; simp [mem_span_basisOfFractionalIdeal]]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
⊢ Submodule.span ℤ
      (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
        (⇑(fractionalIdealLatticeBasis K I :
              Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)) =
    idealLattice K I
have h : ∀ (x : mixedSpace K),
  Membership.mem (γ := Submodule ℤ (mixedSpace K))
      (Submodule.span ℤ
        (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(fractionalIdealLatticeBasis K I :
                Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
            (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)))
      x ↔
    x ∈ idealLattice K I
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
⊢ DiscreteTopology.{u_1} ↥(idealLattice K I)
have rw : DiscreteTopology.{u_1}
  ↥(Submodule.span ℤ
      (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
        (⇑(fractionalIdealLatticeBasis K I :
              Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)))
Tactic: rw [← span_idealLatticeBasis]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
⊢ DiscreteTopology.{u_1} ↥(idealLattice K I)
have rw : DiscreteTopology.{u_1}
  ↥(Submodule.span ℤ
      (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
        (⇑(fractionalIdealLatticeBasis K I :
              Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)))
Tactic: classical
  rw [← span_idealLatticeBasis]
  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
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
⊢ IsZLattice.{0, u_1} ℝ (E := mixedSpace K) (idealLattice K I)
have simp_rw : IsZLattice ℝ (E := mixedSpace K)
  (Submodule.span ℤ
    (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
      (⇑(fractionalIdealLatticeBasis K I :
            Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
        (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)))
Tactic: simp_rw [← span_idealLatticeBasis]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
⊢ MeasureTheory.IsAddFundamentalDomain.{u_1, u_1} ↥(idealLattice K I) (α := mixedSpace K)
    (ZSpan.fundamentalDomain (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
      (fractionalIdealLatticeBasis K I))
    (MeasureTheory.volume : MeasureTheory.Measure (mixedSpace K))
have rw : MeasureTheory.IsAddFundamentalDomain.{u_1, u_1}
  ↥(Submodule.span ℤ
      (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
        (⇑(fractionalIdealLatticeBasis K I :
              Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)))
  (α := mixedSpace K)
  (ZSpan.fundamentalDomain (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
    (fractionalIdealLatticeBasis K I))
  (MeasureTheory.volume : MeasureTheory.Measure (mixedSpace K))
Tactic: rw [← span_idealLatticeBasis]
-- 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} ℝ (euclidean.mixedSpace K) = finrank ℚ K
have rw : finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
Tactic: rw [LinearEquiv.finrank_eq (toMixed K).toLinearEquiv, mixedEmbedding.finrank]
-- 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} ℝ (mixedSpace K) = finrank ℚ K
⊢ finrank.{0, u_1} ℝ (euclidean.mixedSpace K) = finrank ℚ K
have rw₁ : finrank ℚ K = finrank ℚ K
Tactic: rw [LinearEquiv.finrank_eq (toMixed K).toLinearEquiv, mixedEmbedding.finrank]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := Basis (index K) ℝ (mixedSpace K))
    (Basis.map (OrthonormalBasis.toBasis (stdOrthonormalBasis K))
      (↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K))
    (stdBasis K)
have a : ∀ (i : index K) (x : { w : InfinitePlace K // w.IsReal }),
  Eq (α := ℝ)
    (((Basis.map (OrthonormalBasis.toBasis (stdOrthonormalBasis K))
              (↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) :
            (a : index K) → mixedSpace K)
          i).1
      x)
    (((stdBasis K : (a : index K) → mixedSpace K) i).1 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a :
  ∀ (i : index K) (x : { w : InfinitePlace K // w.IsReal }),
    Eq (α := ℝ)
      (((Basis.map (OrthonormalBasis.toBasis (stdOrthonormalBasis K))
                (↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) :
              (a : index K) → mixedSpace K)
            i).1
        x)
      (((stdBasis K : (a : index K) → mixedSpace K) i).1 x)
⊢ Eq (α := Basis (index K) ℝ (mixedSpace K))
    (Basis.map (OrthonormalBasis.toBasis (stdOrthonormalBasis K))
      (↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K))
    (stdBasis K)
have a₁ : ∀ (i : index K) (x : { w : InfinitePlace K // w.IsComplex }),
  Eq (α := ℂ)
    (((Basis.map (OrthonormalBasis.toBasis (stdOrthonormalBasis K))
              (↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) :
            (a : index K) → mixedSpace K)
          i).2
      x)
    (((stdBasis K : (a : index K) → mixedSpace K) i).2 x)
Tactic: ext