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 →+* ℂ) → ℂ
rw :
  Eq (α := Set ((K →+* ℂ) → ℂ))
    (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
      (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))
    (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
      (Function.comp (β := K)
        (⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) : (a : K) → (K →+* ℂ) → ℂ)
        (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))
⊢ Eq (α := Set ((K →+* ℂ) → ℂ))
    (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
      (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))
    (Set.image (α := K) (⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) : (a : K) → (K →+* ℂ) → ℂ)
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
        (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.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 : (K →+* ℂ) → ℂ
⊢ Eq (α := Set ((K →+* ℂ) → ℂ))
    (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
      (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))
    (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
      (Function.comp (β := K)
        (⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) : (a : K) → (K →+* ℂ) → ℂ)
        (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))

Tactic:
congrArg Set.range (funext (fun i => latticeBasis_apply K i))

Premises used: NumberField.canonicalEmbedding.latticeBasis_apply, congrArg, funext, Set.range
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
⊢ Eq (α := Set ((K →+* ℂ) → ℂ))
    (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
      (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))
    (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
      (Function.comp (β := K)
        (⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) : (a : K) → (K →+* ℂ) → ℂ)
        (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))

Tactic:
exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))

Premises used: NumberField.canonicalEmbedding.latticeBasis_apply, congrArg, funext, Set.range
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
rw :
  Membership.mem (γ := Submodule ℤ ((K →+* ℂ) → ℂ))
      (Submodule.span ℤ
        (Set.image (α := K)
          (⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) : (a : K) → (K →+* ℂ) → ℂ)
          (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
            (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))))
      x ↔
    Membership.mem (γ := Subring ((K →+* ℂ) → ℂ))
      (RingHom.range (R := 𝓞 K) (RingHom.comp (canonicalEmbedding K) (algebraMap (𝓞 K) K))) x
⊢ Membership.mem (γ := Submodule ℤ ((K →+* ℂ) → ℂ))
      (Submodule.span ℤ
        (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
          (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))
      x ↔
    Membership.mem (γ := Subring ((K →+* ℂ) → ℂ))
      (RingHom.range (R := 𝓞 K) (RingHom.comp (canonicalEmbedding K) (algebraMap (𝓞 K) K))) x

Tactic:
rw [show Set.range (latticeBasis K) =
      (canonicalEmbedding 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 : (K →+* ℂ) → ℂ
rw :
  Membership.mem (γ := Set ((K →+* ℂ) → ℂ))
      ((⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) : (a : K) → (K →+* ℂ) → ℂ) ''
        (↑(Submodule.span ℤ
              (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
                (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
                  (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))) :
          Set K))
      x ↔
    Membership.mem (γ := Subring ((K →+* ℂ) → ℂ))
      (RingHom.range (R := 𝓞 K) (RingHom.comp (canonicalEmbedding K) (algebraMap (𝓞 K) K))) x
⊢ Membership.mem (γ := Submodule ℤ ((K →+* ℂ) → ℂ))
      (Submodule.span ℤ
        (Set.image (α := K)
          (⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) : (a : K) → (K →+* ℂ) → ℂ)
          (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
            (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))))
      x ↔
    Membership.mem (γ := Subring ((K →+* ℂ) → ℂ))
      (RingHom.range (R := 𝓞 K) (RingHom.comp (canonicalEmbedding K) (algebraMap (𝓞 K) 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 : (K →+* ℂ) → ℂ
rw :
  (∃
      x_1 ∈
        (↑(Submodule.span ℤ
              (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
                (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
                  (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))) :
          Set K),
      (AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K)) : (a : K) → (K →+* ℂ) → ℂ) x_1 = x) ↔
    ∃ (x_1 : K),
      Membership.mem (γ := Subring K) (RingHom.range (R := 𝓞 K) (algebraMap (𝓞 K) K)) x_1 ∧
        (canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x_1 = x
⊢ Membership.mem (γ := Set ((K →+* ℂ) → ℂ))
      ((⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K))) : (a : K) → (K →+* ℂ) → ℂ) ''
        (↑(Submodule.span ℤ
              (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
                (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
                  (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))) :
          Set K))
      x ↔
    Membership.mem (γ := Subring ((K →+* ℂ) → ℂ))
      (RingHom.range (R := 𝓞 K) (RingHom.comp (canonicalEmbedding K) (algebraMap (𝓞 K) K))) x

Tactic:
rw [← RingHom.map_range, Subring.mem_map, Set.mem_image]

Premises used: Set.mem_image, RingHom.map_range, Subring.mem_map
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
simp :
  (∃ (x_1 : K),
      Membership.mem (γ := Subring K) (RingHom.range (R := 𝓞 K) (algebraMap (𝓞 K) K)) x_1 ∧
        (AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K)) : (a : K) → (K →+* ℂ) → ℂ) x_1 = x) ↔
    ∃ (x_1 : K),
      Membership.mem (γ := Subring K) (RingHom.range (R := 𝓞 K) (algebraMap (𝓞 K) K)) x_1 ∧
        (canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x_1 = x
⊢ (∃
      x_1 ∈
        (↑(Submodule.span ℤ
              (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
                (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
                  (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))) :
          Set K),
      (AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K)) : (a : K) → (K →+* ℂ) → ℂ) x_1 = x) ↔
    ∃ (x_1 : K),
      Membership.mem (γ := Subring K) (RingHom.range (R := 𝓞 K) (algebraMap (𝓞 K) K)) x_1 ∧
        (canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x_1 = x

Tactic:
simp only [SetLike.mem_coe, mem_span_integralBasis K]

Premises used: 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 : (K →+* ℂ) → ℂ
⊢ (∃ (x_1 : K),
      Membership.mem (γ := Subring K) (RingHom.range (R := 𝓞 K) (algebraMap (𝓞 K) K)) x_1 ∧
        (AlgHom.toLinearMap (RingHom.toIntAlgHom (canonicalEmbedding K)) : (a : K) → (K →+* ℂ) → ℂ) x_1 = x) ↔
    ∃ (x_1 : K),
      Membership.mem (γ := Subring K) (RingHom.range (R := 𝓞 K) (algebraMap (𝓞 K) K)) x_1 ∧
        (canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x_1 = x

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
rw :
  Membership.mem (γ := Submodule ℚ ((K →+* ℂ) → ℂ))
    (Submodule.span ℚ
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))
    (∑ x_1 : Free.ChooseBasisIndex ℤ (𝓞 K),
      (canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ)
        (HSMul.hSMul (α := ℚ) (β := K)
          (((((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                      (a : K) → Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
                    x :
                  Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
              x_1 :
            ℚ)
          (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
              x_1 :
            K)))
⊢ Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Submodule ℚ ((K →+* ℂ) → ℂ))
    (Submodule.span ℚ
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))
    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (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 ℚ ((K →+* ℂ) → ℂ))
    (Submodule.span ℚ
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))
    (∑ x_1 : Free.ChooseBasisIndex ℤ (𝓞 K),
      HSMul.hSMul (α := ℚ) (β := (K →+* ℂ) → ℂ)
        (((((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                    (a : K) → Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
                  x :
                Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
            x_1 :
          ℚ)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ)
            (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
                x_1 :
              K) :
          (K →+* ℂ) → ℂ))
⊢ Membership.mem (γ := Submodule ℚ ((K →+* ℂ) → ℂ))
    (Submodule.span ℚ
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))
    (∑ x_1 : Free.ChooseBasisIndex ℤ (𝓞 K),
      (canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ)
        (HSMul.hSMul (α := ℚ) (β := K)
          (((((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                      (a : K) → Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
                    x :
                  Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
              x_1 :
            ℚ)
          (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.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 ℚ ((K →+* ℂ) → ℂ))
    (Submodule.span ℚ
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))
    (∑ x_1 : Free.ChooseBasisIndex ℤ (𝓞 K),
      HSMul.hSMul (α := ℚ) (β := (K →+* ℂ) → ℂ)
        (((((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                    (a : K) → Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
                  x :
                Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
            x_1 :
          ℚ)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ)
            (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
                x_1 :
              K) :
          (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 : Free.ChooseBasisIndex ℤ (𝓞 K)),
    Membership.mem (γ := Finset (Free.ChooseBasisIndex ℤ (𝓞 K))) Finset.univ i →
      Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ))
        (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
          (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ)
            (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
                i :
              K) :
          (K →+* ℂ) → ℂ)
⊢ Membership.mem (γ := Submodule ℚ ((K →+* ℂ) → ℂ))
    (Submodule.span ℚ
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))
    (∑ x_1 : Free.ChooseBasisIndex ℤ (𝓞 K),
      HSMul.hSMul (α := ℚ) (β := (K →+* ℂ) → ℂ)
        (((((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                    (a : K) → Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
                  x :
                Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
            x_1 :
          ℚ)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ)
            (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
                x_1 :
              K) :
          (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 : Free.ChooseBasisIndex ℤ (𝓞 K)
h : Membership.mem (γ := Finset (Free.ChooseBasisIndex ℤ (𝓞 K))) Finset.univ i
rw :
  Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ))
    (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
      (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))
    (((latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)
        i :
      (K →+* ℂ) → ℂ)
⊢ Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ))
    (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
      (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))
    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ)
        (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) i :
          K) :
      (K →+* ℂ) → ℂ)

Tactic:
rw [← latticeBasis_apply]

Premises used: NumberField.canonicalEmbedding.latticeBasis_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i : Free.ChooseBasisIndex ℤ (𝓞 K)
h : Membership.mem (γ := Finset (Free.ChooseBasisIndex ℤ (𝓞 K))) Finset.univ i
⊢ Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ))
    (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
      (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))
    (((latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)
        i :
      (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 : Free.ChooseBasisIndex ℤ (𝓞 K)
h : Membership.mem (γ := Finset (Free.ChooseBasisIndex ℤ (𝓞 K))) Finset.univ i
⊢ Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ))
    (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
      (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))
    (((latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)
        i :
      (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 : Free.ChooseBasisIndex ℤ (𝓞 K)
rw :
  Eq (α := ℚ)
    (((((Basis.repr (Basis.restrictScalars ℚ (latticeBasis K)) :
                  ↥(Submodule.span ℚ
                        (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
                          (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
                            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))) ≃ₗ[ℚ]
                    Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                (a :
                    ↥(Submodule.span ℚ
                        (Set.range (⇑(latticeBasis K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))) →
                  Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
              (Subtype.mk (p := fun (x : (K →+* ℂ) → ℂ) ↦
                  Membership.mem (γ := Submodule ℚ ((K →+* ℂ) → ℂ))
                    (Submodule.span ℚ
                      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
                        (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
                          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))
                    x)
                  ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x) ⋯ :
                ↥(Submodule.span ℚ
                    (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
                      (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
                        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))) :
            Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
        i :
      ℚ)
    (((((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                (a : K) → Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
              x :
            Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
        i :
      ℚ)
⊢ Eq (α := ℂ)
    (((((Basis.repr (latticeBasis K) : ((K →+* ℂ) → ℂ) ≃ₗ[ℂ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℂ) :
                (a : (K →+* ℂ) → ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℂ)
              ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) :
            Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℂ) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ℂ)
        i :
      ℂ)
    ((↑(((((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                    (a : K) → Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
                  x :
                Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
              (a : Free.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, NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, eq_ratCast
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i : Free.ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ]
  ↥(Submodule.span ℚ
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))) :=
  LinearMap.codRestrict
    (Submodule.span ℚ
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
        (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))
    (AlgHom.toLinearMap (RingHom.toRatAlgHom (canonicalEmbedding K))) ⋯
⊢ Eq (α := K →ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    ((↑(Basis.repr (Basis.restrictScalars ℚ (latticeBasis K))) :
          ↥(Submodule.span ℚ
                (Set.range (⇑(latticeBasis K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))) →ₗ[ℚ]
            Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) ∘ₗ
        f :
      K →ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    ((↑(Basis.repr (integralBasis K)) : K →ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
      K →ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)

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

Premises used: NumberField.integralBasis, Module.Basis.ext