awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
⊢ Membership.mem (α := mixedSpace K) (γ := Submodule ℚ (mixedSpace K))
    (Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
    ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K)
have rw : Membership.mem (γ := Submodule ℚ (mixedSpace K))
  (Submodule.span ℚ
    (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
      (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
        (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
  (∑ x_1 : ChooseBasisIndex ℤ (𝓞 K),
    (mixedEmbedding K : (a : K) → mixedSpace K)
      (HSMul.hSMul (α := ℚ) (β := K)
        (((((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                    (a : K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
                  x :
                ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
              (a : ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
            x_1 :
          ℚ)
        (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) x_1 : K)))
Tactic: rw [← Basis.sum_repr (integralBasis K) x, map_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
⊢ Membership.mem (γ := Submodule ℚ (mixedSpace K))
    (Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
    (∑ x_1 : ChooseBasisIndex ℤ (𝓞 K),
      (mixedEmbedding K : (a : K) → mixedSpace K)
        (HSMul.hSMul (α := ℚ) (β := K)
          (((((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                      (a : K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
                    x :
                  ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                (a : ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
              x_1 :
            ℚ)
          (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) x_1 : K)))
have simp_rw : Membership.mem (γ := Submodule ℚ (mixedSpace K))
  (Submodule.span ℚ
    (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
      (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
        (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
  (∑ x_1 : ChooseBasisIndex ℤ (𝓞 K),
    HSMul.hSMul (α := ℚ) (β := mixedSpace K)
      (((((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                  (a : K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
                x :
              ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
            (a : ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
          x_1 :
        ℚ)
      ((mixedEmbedding K : (a : K) → mixedSpace K)
          (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) x_1) :
        mixedSpace K))
Tactic: simp_rw [map_rat_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
⊢ Membership.mem (γ := Submodule ℚ (mixedSpace K))
    (Submodule.span ℚ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
    (∑ x_1 : ChooseBasisIndex ℤ (𝓞 K),
      HSMul.hSMul (α := ℚ) (β := mixedSpace K)
        (((((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                    (a : K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
                  x :
                ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
              (a : ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
            x_1 :
          ℚ)
        ((mixedEmbedding K : (a : K) → mixedSpace K)
            (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) x_1) :
          mixedSpace K))
have refine : ∀ (i : ChooseBasisIndex ℤ (𝓞 K)),
  Membership.mem (γ := Finset (ChooseBasisIndex ℤ (𝓞 K))) univ i →
    Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K))
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))
      ((mixedEmbedding K : (a : K) → mixedSpace K)
          (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i) :
        mixedSpace K)
Tactic: refine Submodule.sum_smul_mem _ _ (fun i _ ↦ Submodule.subset_span ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i : ChooseBasisIndex ℤ (𝓞 K)
h : Membership.mem (γ := Finset (ChooseBasisIndex ℤ (𝓞 K))) univ i
⊢ Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K))
    (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
      (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
        (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))
    ((mixedEmbedding K : (a : K) → mixedSpace K)
        (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i) :
      mixedSpace K)
have rw : Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K))
  (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
    (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
      (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K))
  (((latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
        (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)
      i :
    mixedSpace K)
Tactic: rw [← latticeBasis_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i : ChooseBasisIndex ℤ (𝓞 K)
⊢ Eq (α := ℝ)
    (((((Basis.repr (latticeBasis K) : mixedSpace K ≃ₗ[ℝ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℝ) :
                (a : mixedSpace K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℝ)
              ((mixedEmbedding K : (a : K) → mixedSpace K) x : 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) :
        ℝ) :
      ℝ)
have rw : 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) sorry :
              ↥(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: rw [← Basis.restrictScalars_repr_apply ℚ _ ⟨_, mem_rat_span_latticeBasis K x⟩, eq_ratCast,
    Rat.cast_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
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 (α := ℚ)
    (((((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 :
      ℚ)
have 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) →₀ ℚ)
Tactic: suffices ((latticeBasis K).restrictScalars ℚ).repr.toLinearMap ∘ₗ f =
    (integralBasis K).repr.toLinearMap from DFunLike.congr_fun (LinearMap.congr_fun this x) 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 : 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) →₀ ℚ)
have 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) →₀ ℚ)
Tactic: refine Basis.ext (integralBasis K) (fun 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 : 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))))
have 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)
Tactic: apply Subtype.val_injective
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
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.{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)
have 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)
Tactic: rw [LinearMap.codRestrict_apply, AlgHom.toLinearMap_apply, Basis.restrictScalars_apply,
      latticeBasis_apply]
-- 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)
⊢ 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)) : ℝ) : ℝ)
have 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))) :
        ℚ) :
    ℝ)
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]
-- 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)ˣ
⊢ ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)
have refine : Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) =
  Fintype.card.{u_1} (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
Tactic: refine Fintype.equivOfCardEq ?_
-- 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)ˣ
⊢ 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) =
  Fintype.card.{u_1} (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) 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)ˣ
rw :
  finrank.{0, u_1} ℤ (𝓞 K) =
    Fintype.card.{u_1} (ChooseBasisIndex ℤ ↥(↑(↑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} ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)
Tactic: rw [← finrank_eq_card_chooseBasisIndex, ← finrank_eq_card_chooseBasisIndex,
      fractionalIdeal_rank]