awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i : ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ]
  ↥(Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) :=
  LinearMap.codRestrict
    (Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
    (AlgHom.toLinearMap (RingHom.toRatAlgHom (mixedEmbedding K))) ⋯
suffices :
  Eq (α := K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    ((↑(Basis.repr (Basis.restrictScalars ℚ (latticeBasis K))) :
          ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) →ₗ[ℚ]
            ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) ∘ₗ
        f :
      K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    ((↑(Basis.repr (integralBasis K)) : K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) : K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
⊢ Eq (α := ℚ)
    (((((Basis.repr (Basis.restrictScalars ℚ (latticeBasis K)) :
                  ↥(Submodule.span ℚ
                        (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                          (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                            (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) ≃ₗ[ℚ]
                    ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                (a :
                    ↥(Submodule.span ℚ
                        (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))) →
                  ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
              (Subtype.mk (p := fun (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)
                  ((mixedEmbedding K : (a : K) → mixedSpace K) x) ⋯ :
                ↥(Submodule.span ℚ
                    (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                      (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                        (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))) :
            ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
        i :
      ℚ)
    (((((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                (a : K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
              x :
            ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
        i :
      ℚ)

Tactic:
suffices ((latticeBasis K).restrictScalars ℚ).repr.toLinearMap ∘ₗ f =
    (integralBasis K).repr.toLinearMap from DFunLike.congr_fun (LinearMap.congr_fun this x) i
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i : ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ]
  ↥(Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) :=
  LinearMap.codRestrict
    (Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
    (AlgHom.toLinearMap (RingHom.toRatAlgHom (mixedEmbedding K))) ⋯
⊢ Eq (α := K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    ((↑(Basis.repr (Basis.restrictScalars ℚ (latticeBasis K))) :
          ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) →ₗ[ℚ]
            ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) ∘ₗ
        f :
      K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    ((↑(Basis.repr (integralBasis K)) : K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) : K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)

Tactic:
Basis.ext (integralBasis K) (fun i ↦ ?_)

Premises used: NumberField.integralBasis, Module.Basis.ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i : ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ]
  ↥(Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) :=
  LinearMap.codRestrict
    (Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
    (AlgHom.toLinearMap (RingHom.toRatAlgHom (mixedEmbedding K))) ⋯
refine :
  ∀ (i : ChooseBasisIndex ℤ (𝓞 K)),
    Eq (α := ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
      ((((↑(Basis.repr (Basis.restrictScalars ℚ (latticeBasis K))) :
                  ↥(Submodule.span ℚ
                        (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) →ₗ[ℚ]
                    ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) ∘ₗ
                f :
              K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
            (a : K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
          (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i : K) :
        ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
      ((((↑(Basis.repr (integralBasis K)) : K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
              K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
            (a : K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
          (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i : K) :
        ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
⊢ Eq (α := K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    ((↑(Basis.repr (Basis.restrictScalars ℚ (latticeBasis K))) :
          ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) →ₗ[ℚ]
            ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) ∘ₗ
        f :
      K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    ((↑(Basis.repr (integralBasis K)) : K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) : K →ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)

Tactic:
refine Basis.ext (integralBasis K) (fun i ↦ ?_)

Premises used: NumberField.integralBasis, Module.Basis.ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i_1 : ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ]
  ↥(Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) :=
  LinearMap.codRestrict
    (Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
    (AlgHom.toLinearMap (RingHom.toRatAlgHom (mixedEmbedding K))) ⋯
i : ChooseBasisIndex ℤ (𝓞 K)
a :
  Eq.{u_1 + 1} (α := mixedSpace K)
    (↑((f :
            (a : K) →
              ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
          (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i)) :
      mixedSpace K)
    (↑(((Basis.restrictScalars ℚ (latticeBasis K) :
              Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ
                ↥(Submodule.span ℚ
                    (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                      (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                        (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))) :
            (a : ChooseBasisIndex ℤ (𝓞 K)) →
              ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
          i) :
      mixedSpace K)
⊢ Eq (α :=
    ↥(Submodule.span ℚ
        (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
          (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
            (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
    ((f : (a : K) → ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
        (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i) :
      ↥(Submodule.span ℚ
          (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
            (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
              (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
    (((Basis.restrictScalars ℚ (latticeBasis K) :
            Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ
              ↥(Submodule.span ℚ
                  (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                    (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                      (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) →
            ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
        i :
      ↥(Submodule.span ℚ
          (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
            (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
              (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))

Tactic:
apply Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i_1 : ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ]
  ↥(Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) :=
  LinearMap.codRestrict
    (Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
    (AlgHom.toLinearMap (RingHom.toRatAlgHom (mixedEmbedding K))) ⋯
i : ChooseBasisIndex ℤ (𝓞 K)
a :
  Eq (α := mixedSpace K)
    ((RingHom.toRatAlgHom (mixedEmbedding K) : (a : K) → mixedSpace K)
        (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i) :
      mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K)
        (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i) :
      mixedSpace K)
⊢ Eq.{u_1 + 1} (α := mixedSpace K)
    (↑((f :
            (a : K) →
              ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
          (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i)) :
      mixedSpace K)
    (↑(((Basis.restrictScalars ℚ (latticeBasis K) :
              Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ
                ↥(Submodule.span ℚ
                    (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                      (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                        (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))) :
            (a : ChooseBasisIndex ℤ (𝓞 K)) →
              ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
          i) :
      mixedSpace K)

Tactic:
rw [LinearMap.codRestrict_apply, AlgHom.toLinearMap_apply, Basis.restrictScalars_apply,
      latticeBasis_apply]

Premises used: AlgHom.toLinearMap_apply, Module.Basis.restrictScalars_apply, NumberField.mixedEmbedding.latticeBasis_apply, LinearMap.codRestrict_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i_1 : ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ]
  ↥(Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) :=
  LinearMap.codRestrict
    (Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
    (AlgHom.toLinearMap (RingHom.toRatAlgHom (mixedEmbedding K))) ⋯
i : ChooseBasisIndex ℤ (𝓞 K)
⊢ Eq (α := mixedSpace K)
    ((RingHom.toRatAlgHom (mixedEmbedding K) : (a : K) → mixedSpace K)
        (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i) :
      mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K)
        (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i) :
      mixedSpace K)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i_1 : ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ]
  ↥(Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))) :=
  LinearMap.codRestrict
    (Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
    (AlgHom.toLinearMap (RingHom.toRatAlgHom (mixedEmbedding K))) ⋯
i : ChooseBasisIndex ℤ (𝓞 K)
⊢ Eq (α :=
    ↥(Submodule.span ℚ
        (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
          (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
            (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
    ((f : (a : K) → ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
        (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i) :
      ↥(Submodule.span ℚ
          (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
            (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
              (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
    (((Basis.restrictScalars ℚ (latticeBasis K) :
            Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ
              ↥(Submodule.span ℚ
                  (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
                    (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
                      (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) →
            ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))
        i :
      ↥(Submodule.span ℚ
          (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
            (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
              (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))))

Tactic:
have : f (integralBasis K i) = ((latticeBasis K).restrictScalars ℚ) i := by
    apply Subtype.val_injective
    rw [LinearMap.codRestrict_apply, AlgHom.toLinearMap_apply, Basis.restrictScalars_apply,
      latticeBasis_apply]
    rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_2
inst : Field K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ x ∈ idealLattice K I ↔
    ∃ y ∈ (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Set K), (mixedEmbedding K : (a : K) → mixedSpace K) y = x

Tactic:
simp [idealLattice]

Premises used: NumberField.mixedEmbedding.idealLattice
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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)
suffices :
  Eq (α := ℝ)
    (((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)))) :
      ℝ)
    ((algebraMap ℚ ℝ : (a : ℚ) → ℝ)
        (((Basis.det.{0, u_1, u_1} (R := ℚ) (M := K) (ι := ChooseBasisIndex ℤ (𝓞 K)) (integralBasis K) :
                K [⋀^ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℚ] ℚ) :
              (a : ChooseBasisIndex ℤ (𝓞 K) → 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 (α := ℝ)
    (|((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))))| :
      ℝ)
    ((↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) : ℝ)

Tactic:
suffices Basis.det (latticeBasis K) ((mixedEmbedding K ∘ (basisOfFractionalIdeal K I) ∘ e)) =
      (algebraMap ℚ ℝ) ((Basis.det (integralBasis K)) ((basisOfFractionalIdeal K I) ∘ e)) by
    rw [this, eq_ratCast, ← Rat.cast_abs, ← Equiv.symm_symm e, ← Basis.coe_reindex,
      det_basisOfFractionalIdeal_eq_absNorm K I e]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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)
i j : ChooseBasisIndex ℤ (𝓞 K)
⊢ Eq (α := ℝ)
    (((((Basis.repr (latticeBasis K) : mixedSpace K ≃ₗ[ℝ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℝ) :
                (a : mixedSpace K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℝ)
              ((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)
                    ((e :
                          (a : ChooseBasisIndex ℤ (𝓞 K)) →
                            ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
                        j :
                      ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))) :
                mixedSpace K) :
            ChooseBasisIndex ℤ (𝓞 K) →₀ ℝ) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → ℝ)
        i :
      ℝ)
    ((algebraMap ℚ ℝ : (a : ℚ) → ℝ)
        (((((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                    (a : K) → ChooseBasisIndex ℤ (𝓞 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))
                          j :
                        ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) :
                    K) :
                ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
              (a : ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
            i :
          ℚ) :
      ℝ)

Tactic:
latticeBasis_repr_apply K _ i

Premises used: NumberField.mixedEmbedding.latticeBasis_repr_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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)
i j : ChooseBasisIndex ℤ (𝓞 K)
⊢ Eq (α := ℝ)
    (((((Basis.repr (latticeBasis K) : mixedSpace K ≃ₗ[ℝ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℝ) :
                (a : mixedSpace K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℝ)
              ((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)
                    ((e :
                          (a : ChooseBasisIndex ℤ (𝓞 K)) →
                            ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
                        j :
                      ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))) :
                mixedSpace K) :
            ChooseBasisIndex ℤ (𝓞 K) →₀ ℝ) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → ℝ)
        i :
      ℝ)
    ((algebraMap ℚ ℝ : (a : ℚ) → ℝ)
        (((((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                    (a : K) → ChooseBasisIndex ℤ (𝓞 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))
                          j :
                        ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) :
                    K) :
                ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
              (a : ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
            i :
          ℚ) :
      ℝ)

Tactic:
exact latticeBasis_repr_apply K _ i

Premises used: NumberField.mixedEmbedding.latticeBasis_repr_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
refine :
  Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) =
    Fintype.card.{u_1} (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
⊢ ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)

Tactic:
refine Fintype.equivOfCardEq ?_

Premises used: Fintype.equivOfCardEq