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 (γ := 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
have 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
Tactic: rw [← Submodule.map_span, ← SetLike.mem_coe, Submodule.map_coe]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
⊢ 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
have 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
Tactic: rw [← RingHom.map_range, Subring.mem_map, Set.mem_image]
-- 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 →+* ℂ) → ℂ
⊢ (∃
      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
have 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
Tactic: simp only [SetLike.mem_coe, mem_span_integralBasis K]
-- 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 (α := (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 →+* ℂ) → ℂ)
have 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)))
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 ℚ ((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)))
have 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 →+* ℂ) → ℂ))
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 ℚ ((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 →+* ℂ) → ℂ))
have 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 →+* ℂ) → ℂ)
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 : 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 →+* ℂ) → ℂ))
    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ)
        (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) i :
          K) :
      (K →+* ℂ) → ℂ)
have 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 →+* ℂ) → ℂ)
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 : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ 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) :
        ℂ) :
      ℂ)
have 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) sorry :
              ↥(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 :
    ℚ)
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 : 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) →₀ ℚ)
have refine : ∀ (i : Free.ChooseBasisIndex ℤ (𝓞 K)),
  Eq (α := 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) →₀ ℚ) :
          (a : K) → Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
        (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) i :
          K) :
      Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
    ((((↑(Basis.repr (integralBasis K)) : K →ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
            K →ₗ[ℚ] Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
          (a : K) → Free.ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ)
        (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) i :
          K) :
      Free.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 : 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))) ⋯
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ Eq.{u_1 + 1} (α := (K →+* ℂ) → ℂ)
    (↑((f :
            (a : K) →
              ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))))
          (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
            i)) :
      (K →+* ℂ) → ℂ)
    (↑(((Basis.restrictScalars ℚ (latticeBasis K) :
              Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ
                ↥(Submodule.span ℚ
                    (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
                      (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
                        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) →
              ↥(Submodule.span ℚ (Set.range (⇑(latticeBasis K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))))
          i) :
      (K →+* ℂ) → ℂ)
have a : Eq (α := (K →+* ℂ) → ℂ)
  ((RingHom.toRatAlgHom (canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ)
      (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) i :
        K) :
    (K →+* ℂ) → ℂ)
  ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ)
      (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) i :
        K) :
    (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
x : K
w : { w : InfinitePlace K // w.IsReal }
⊢ Eq (α := ℝ) (((mixedEmbedding K : (a : K) → mixedSpace K) x).1 w : ℝ) ((embedding_of_isReal ⋯ : (a : K) → ℝ) x : ℝ)
have simp_rw : Eq (α := ℝ)
  (((RingHom.prod
              (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsReal }) ↦ ℝ)
                fun (w : { w : InfinitePlace K // w.IsReal }) ↦ embedding_of_isReal sorry)
              (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ)
                fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K).embedding) :
            (a : K) → mixedSpace K)
          x).1
      w :
    ℝ)
  ((embedding_of_isReal sorry : (a : K) → ℝ) x : ℝ)
Tactic: simp_rw [mixedEmbedding, RingHom.prod_apply, Pi.ringHom_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : K
w : { w : InfinitePlace K // w.IsReal }
simp_rw :
  Eq (α := ℝ)
    (((RingHom.prod
                (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsReal }) ↦ ℝ)
                  fun (w : { w : InfinitePlace K // w.IsReal }) ↦ embedding_of_isReal ⋯)
                (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ)
                  fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K).embedding) :
              (a : K) → mixedSpace K)
            x).1
        w :
      ℝ)
    ((embedding_of_isReal ⋯ : (a : K) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) (((mixedEmbedding K : (a : K) → mixedSpace K) x).1 w : ℝ) ((embedding_of_isReal ⋯ : (a : K) → ℝ) x : ℝ)
have simp_rw₁ : Eq (α := ℝ)
  ((Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) fun (w : { w : InfinitePlace K // w.IsReal }) ↦
          embedding_of_isReal sorry :
        (a : K) → { w : InfinitePlace K // w.IsReal } → ℝ)
      x w :
    ℝ)
  ((embedding_of_isReal sorry : (a : K) → ℝ) x : ℝ)
Tactic: simp_rw [mixedEmbedding, RingHom.prod_apply, Pi.ringHom_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : K
w : { w : InfinitePlace K // w.IsComplex }
⊢ Eq (α := ℂ) (((mixedEmbedding K : (a : K) → mixedSpace K) x).2 w : ℂ)
    (((↑w : InfinitePlace K).embedding : (a : K) → ℂ) x : ℂ)
have simp_rw : Eq (α := ℂ)
  (((RingHom.prod
              (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsReal }) ↦ ℝ)
                fun (w : { w : InfinitePlace K // w.IsReal }) ↦ embedding_of_isReal sorry)
              (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ)
                fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K).embedding) :
            (a : K) → mixedSpace K)
          x).2
      w :
    ℂ)
  (((↑w : InfinitePlace K).embedding : (a : K) → ℂ) x : ℂ)
Tactic: simp_rw [mixedEmbedding, RingHom.prod_apply, Pi.ringHom_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : K
w : { w : InfinitePlace K // w.IsComplex }
simp_rw :
  Eq (α := ℂ)
    (((RingHom.prod
                (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsReal }) ↦ ℝ)
                  fun (w : { w : InfinitePlace K // w.IsReal }) ↦ embedding_of_isReal ⋯)
                (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ)
                  fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K).embedding) :
              (a : K) → mixedSpace K)
            x).2
        w :
      ℂ)
    (((↑w : InfinitePlace K).embedding : (a : K) → ℂ) x : ℂ)
⊢ Eq (α := ℂ) (((mixedEmbedding K : (a : K) → mixedSpace K) x).2 w : ℂ)
    (((↑w : InfinitePlace K).embedding : (a : K) → ℂ) x : ℂ)
have simp_rw₁ : Eq (α := ℂ)
  ((Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ)
          fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K).embedding :
        (a : K) → { w : InfinitePlace K // w.IsComplex } → ℂ)
      x w :
    ℂ)
  (((↑w : InfinitePlace K).embedding : (a : K) → ℂ) x : ℂ)
Tactic: simp_rw [mixedEmbedding, RingHom.prod_apply, Pi.ringHom_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Nontrivial.{u_1} (mixedSpace K)
have obtain : ∀ (w : InfinitePlace K), Nontrivial.{u_1} (mixedSpace K)
Tactic: obtain ⟨w⟩ := (inferInstance : Nonempty (InfinitePlace K))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
⊢ Nontrivial.{u_1} (mixedSpace K)
have inl : ∀ (hw : w.IsReal), Nontrivial.{u_1} (mixedSpace K)
Tactic: obtain hw | hw := w.isReal_or_isComplex
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
inl : ∀ (hw : w.IsReal), Nontrivial.{u_1} (mixedSpace K)
⊢ Nontrivial.{u_1} (mixedSpace K)
have inr : ∀ (hw : w.IsComplex), Nontrivial.{u_1} (mixedSpace K)
Tactic: obtain hw | hw := w.isReal_or_isComplex
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsReal
⊢ Nontrivial.{u_1} (mixedSpace K)
have this : Nonempty.{max 1 (u_1 + 1)} { w : InfinitePlace K // w.IsReal }
Tactic: have : Nonempty {w : InfinitePlace K // IsReal w} := ⟨⟨w, hw⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ Nontrivial.{u_1} (mixedSpace K)
have this : Nonempty.{max 1 (u_1 + 1)} { w : InfinitePlace K // w.IsComplex }
Tactic: have : Nonempty {w : InfinitePlace K // IsComplex w} := ⟨⟨w, hw⟩⟩