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
i : ChooseBasisIndex ℤ (𝓞 K)
⊢ Eq (α := mixedSpace K)
    (((latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)
        i :
      mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K)
        (((integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : ChooseBasisIndex ℤ (𝓞 K)) → K) i) :
      mixedSpace K)

Tactic:
simp only [latticeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, Function.comp_apply,
    canonicalEmbedding.latticeBasis_apply, integralBasis_apply, commMap_canonical_eq_mixed]

Premises used: NumberField.integralBasis_apply, NumberField.canonicalEmbedding.latticeBasis_apply, NumberField.mixedEmbedding.latticeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, Function.comp_apply, NumberField.mixedEmbedding.commMap_canonical_eq_mixed
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
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)))
⊢ 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)))

Tactic:
rw [← Set.range_comp]

Premises used: Set.range_comp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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.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:
congrArg Set.range (funext (fun i => latticeBasis_apply K i))

Premises used: congrArg, funext, NumberField.mixedEmbedding.latticeBasis_apply, Set.range
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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.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:
exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))

Premises used: congrArg, funext, NumberField.mixedEmbedding.latticeBasis_apply, Set.range
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
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
⊢ 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

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))]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
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
⊢ 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 [← Submodule.map_span, ← SetLike.mem_coe, Submodule.map_coe]

Premises used: SetLike.mem_coe, Submodule.map_span, Submodule.map_coe
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
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
⊢ 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:
simp only [Set.mem_image, SetLike.mem_coe, mem_span_integralBasis K,
    RingHom.mem_range, exists_exists_eq_and]

Premises used: RingHom.mem_range, Set.mem_image, exists_exists_eq_and, SetLike.mem_coe, NumberField.mem_span_integralBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
⊢ (∃ (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:
rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := Submodule ℤ (mixedSpace K))
    (Submodule.span ℤ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
    (mixedEmbedding.integerLattice K)

Tactic:
Submodule.ext_iff.mpr fun _ ↦ mem_span_latticeBasis K

Premises used: Iff.mpr, Submodule.ext_iff, NumberField.mixedEmbedding.mem_span_latticeBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  DiscreteTopology.{u_1}
    ↥(Submodule.span ℤ
        (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
          (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
            (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
⊢ DiscreteTopology.{u_1} ↥(mixedEmbedding.integerLattice K)

Tactic:
rw [← span_latticeBasis]

Premises used: NumberField.mixedEmbedding.span_latticeBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ DiscreteTopology.{u_1}
    ↥(Submodule.span ℤ
        (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
          (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
            (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw rw₁ rw₂ :
  DiscreteTopology.{u_1}
    ↥(Submodule.span ℤ
        (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
          (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
            (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))
⊢ DiscreteTopology.{u_1} ↥(mixedEmbedding.integerLattice K)

Tactic:
classical
  rw [← span_latticeBasis]
  infer_instance

Premises used: NumberField.mixedEmbedding.span_latticeBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsZLattice ℝ (E := mixedSpace K)
    (Submodule.span ℤ
      (Set.range (ι := ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)))

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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))
⊢ MeasureTheory.IsAddFundamentalDomain.{u_1, u_1} ↥(mixedEmbedding.integerLattice K) (α := mixedSpace K)
    (ZSpan.fundamentalDomain (ι := ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K))
    (MeasureTheory.volume : MeasureTheory.Measure (mixedSpace K))

Tactic:
rw [← span_latticeBasis]

Premises used: NumberField.mixedEmbedding.span_latticeBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 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:
ZSpan.isAddFundamentalDomain (latticeBasis K) _

Premises used: NumberField.mixedEmbedding.latticeBasis, Set.Mem, setOf, ZSpan.isAddFundamentalDomain
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 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:
exact ZSpan.isAddFundamentalDomain (latticeBasis K) _

Premises used: NumberField.mixedEmbedding.latticeBasis, ZSpan.isAddFundamentalDomain
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
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)))
⊢ 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)

Tactic:
rw [← Basis.sum_repr (integralBasis K) x, map_sum]

Premises used: NumberField.integralBasis, map_sum, Module.Basis.sum_repr
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
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))
⊢ 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:
simp_rw [map_rat_smul]

Premises used: map_rat_smul
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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))

Tactic:
Submodule.sum_smul_mem _ _ (fun i _ ↦ Submodule.subset_span ?_)

Premises used: Submodule.sum_smul_mem, Set.Mem, Submodule.subset_span
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
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)
⊢ 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:
refine Submodule.sum_smul_mem _ _ (fun i _ ↦ Submodule.subset_span ?_)

Premises used: Submodule.sum_smul_mem, Submodule.subset_span
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
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)
⊢ 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:
rw [← latticeBasis_apply]

Premises used: NumberField.mixedEmbedding.latticeBasis_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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))
    (((latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)
        i :
      mixedSpace K)

Tactic:
Set.mem_range_self i

Premises used: Set.mem_range_self
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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))
    (((latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)
        i :
      mixedSpace K)

Tactic:
exact Set.mem_range_self i

Premises used: Set.mem_range_self
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i : ChooseBasisIndex ℤ (𝓞 K)
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) ⋯ :
                ↥(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 :
      ℚ)
⊢ 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) :
        ℝ) :
      ℝ)

Tactic:
rw [← Basis.restrictScalars_repr_apply ℚ _ ⟨_, mem_rat_span_latticeBasis K x⟩, eq_ratCast,
    Rat.cast_inj]

Premises used: Rat, Rat.cast_inj, Module.Basis.restrictScalars_repr_apply, Subtype.mk, eq_ratCast, NumberField.mixedEmbedding.mem_rat_span_latticeBasis