awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i : 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))) ⋯
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) →₀ ℚ)
⊢ 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:
refine Basis.ext (integralBasis K) (fun i ↦ ?_)

Premises used: NumberField.integralBasis, Module.Basis.ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i_1 : 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)
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 →+* ℂ) → ℂ)
⊢ 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 →+* ℂ) → ℂ)

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

Premises used: NumberField.canonicalEmbedding.latticeBasis_apply, AlgHom.toLinearMap_apply, Module.Basis.restrictScalars_apply, LinearMap.codRestrict_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
i_1 : 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 (α := (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:
rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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 (α :=
    ↥(Submodule.span ℚ
        (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
          (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (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) :
      ↥(Submodule.span ℚ
          (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
            (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (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 :
      ↥(Submodule.span ℚ
          (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
            (⇑(latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))))

Tactic:
have : f (integralBasis K i) = ((latticeBasis K).restrictScalars ℚ) i := by
    apply Subtype.val_injective
    rw [LinearMap.codRestrict_apply, AlgHom.toLinearMap_apply, Basis.restrictScalars_apply,
      latticeBasis_apply]
    rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_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 : ℝ)
simp_rw₁ :
  Eq (α := ℝ)
    ((Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsReal }) ↦ ℝ)
            fun (w : { w : InfinitePlace K // w.IsReal }) ↦ embedding_of_isReal ⋯ :
          (a : K) → { w : InfinitePlace K // w.IsReal } → ℝ)
        x w :
      ℝ)
    ((embedding_of_isReal ⋯ : (a : K) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) (((mixedEmbedding K : (a : K) → mixedSpace K) x).1 w : ℝ) ((embedding_of_isReal ⋯ : (a : K) → ℝ) x : ℝ)

Tactic:
simp_rw [mixedEmbedding, RingHom.prod_apply, Pi.ringHom_apply]

Premises used: NumberField.mixedEmbedding, Pi.ringHom_apply, RingHom.prod_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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 : ℂ)
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 : ℂ)
⊢ Eq (α := ℂ) (((mixedEmbedding K : (a : K) → mixedSpace K) x).2 w : ℂ)
    (((↑w : InfinitePlace K).embedding : (a : K) → ℂ) x : ℂ)

Tactic:
simp_rw [mixedEmbedding, RingHom.prod_apply, Pi.ringHom_apply]

Premises used: NumberField.mixedEmbedding, Pi.ringHom_apply, RingHom.prod_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
obtain : ∀ (w : InfinitePlace K), Nontrivial.{u_1} (mixedSpace K)
⊢ Nontrivial.{u_1} (mixedSpace K)

Tactic:
obtain ⟨w⟩ := (inferInstance : Nonempty (InfinitePlace K))

Premises used: inferInstance
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
inl : ∀ (hw : w.IsReal), Nontrivial.{u_1} (mixedSpace K)
inr : ∀ (hw : w.IsComplex), Nontrivial.{u_1} (mixedSpace K)
⊢ Nontrivial.{u_1} (mixedSpace K)

Tactic:
obtain hw | hw := w.isReal_or_isComplex

Premises used: NumberField.InfinitePlace.isReal_or_isComplex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsReal
⊢ Nonempty.{max 1 (u_1 + 1)} { w : InfinitePlace K // w.IsReal }

Tactic:
have : Nonempty {w : InfinitePlace K // IsReal w} := ⟨⟨w, hw⟩⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsReal
this : Nonempty.{max 1 (u_1 + 1)} { w : InfinitePlace K // w.IsReal }
⊢ Nontrivial.{u_1} (mixedSpace K)

Tactic:
nontrivial_prod_left

Premises used: nontrivial_prod_left
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsReal
this : Nonempty.{max 1 (u_1 + 1)} { w : InfinitePlace K // w.IsReal }
⊢ Nontrivial.{u_1} (mixedSpace K)

Tactic:
exact nontrivial_prod_left

Premises used: nontrivial_prod_left
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ Nonempty.{max 1 (u_1 + 1)} { w : InfinitePlace K // w.IsComplex }

Tactic:
have : Nonempty {w : InfinitePlace K // IsComplex w} := ⟨⟨w, hw⟩⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsComplex
this : Nonempty.{max 1 (u_1 + 1)} { w : InfinitePlace K // w.IsComplex }
⊢ Nontrivial.{u_1} (mixedSpace K)

Tactic:
nontrivial_prod_right

Premises used: nontrivial_prod_right
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsComplex
this : Nonempty.{max 1 (u_1 + 1)} { w : InfinitePlace K // w.IsComplex }
⊢ Nontrivial.{u_1} (mixedSpace K)

Tactic:
exact nontrivial_prod_right

Premises used: nontrivial_prod_right
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₁ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₂ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ =
    finrank ℚ K
rw₃ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, 2 = finrank ℚ K
rw₄ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ) 2 =
    finrank ℚ K
rw₅ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 =
    finrank ℚ K
rw₆ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 = finrank ℚ K
rw₇ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 = finrank ℚ K
rw₈ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 =
    finrank ℚ K
rw₉ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + nrComplexPlaces K * 2 = finrank ℚ K
rw₁₀ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + 2 * nrComplexPlaces K = finrank ℚ K
rw₁₁ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      Fintype.card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } =
    finrank ℚ K
rw₁₂ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      Fintype.card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } =
    Fintype.card.{u_1} (K →+* ℂ)
rw₁₃ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      (Fintype.card.{u_1} (K →+* ℂ) - Fintype.card.{u_1} { x : K →+* ℂ // ComplexEmbedding.IsReal x }) =
    Fintype.card.{u_1} (K →+* ℂ)
rw₁₄ rw₁₅ : Fintype.card.{u_1} (K →+* ℂ) = Fintype.card.{u_1} (K →+* ℂ)
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K

Tactic:
rw [finrank_prod, finrank_pi, finrank_pi_fintype, Complex.finrank_real_complex, sum_const,
    card_univ, ← nrRealPlaces, ← nrComplexPlaces, ← card_real_embeddings, smul_eq_mul,
    mul_comm, ← card_complex_embeddings, ← NumberField.Embeddings.card K ℂ,
    Fintype.card_subtype_compl, Nat.add_sub_of_le (Fintype.card_subtype_le _)]

Premises used: Finset.card_univ, Fintype.card_subtype_le, Nat.add_sub_of_le, NumberField.Embeddings.card, Module.finrank_pi, NumberField.InfinitePlace.nrRealPlaces, Module.finrank_pi_fintype, NumberField.InfinitePlace.card_real_embeddings, Complex.finrank_real_complex, mul_comm, NumberField.InfinitePlace.nrComplexPlaces, smul_eq_mul, Complex, Module.finrank_prod, Fintype.card_subtype_compl, NumberField.InfinitePlace.card_complex_embeddings, Finset.sum_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₁ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₂ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ =
    finrank ℚ K
rw₃ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, 2 = finrank ℚ K
rw₄ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ) 2 =
    finrank ℚ K
rw₅ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 =
    finrank ℚ K
rw₆ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 = finrank ℚ K
rw₇ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 = finrank ℚ K
rw₈ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 =
    finrank ℚ K
rw₉ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + nrComplexPlaces K * 2 = finrank ℚ K
rw₁₀ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + 2 * nrComplexPlaces K = finrank ℚ K
rw₁₁ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      Fintype.card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } =
    finrank ℚ K
rw₁₂ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      Fintype.card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } =
    Fintype.card.{u_1} (K →+* ℂ)
rw₁₃ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      (Fintype.card.{u_1} (K →+* ℂ) - Fintype.card.{u_1} { x : K →+* ℂ // ComplexEmbedding.IsReal x }) =
    Fintype.card.{u_1} (K →+* ℂ)
rw₁₄ rw₁₅ : Fintype.card.{u_1} (K →+* ℂ) = Fintype.card.{u_1} (K →+* ℂ)
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K

Tactic:
classical
  rw [finrank_prod, finrank_pi, finrank_pi_fintype, Complex.finrank_real_complex, sum_const,
    card_univ, ← nrRealPlaces, ← nrComplexPlaces, ← card_real_embeddings, smul_eq_mul,
    mul_comm, ← card_complex_embeddings, ← NumberField.Embeddings.card K ℂ,
    Fintype.card_subtype_compl, Nat.add_sub_of_le (Fintype.card_subtype_le _)]

Premises used: Finset.card_univ, Fintype.card_subtype_le, Nat.add_sub_of_le, NumberField.Embeddings.card, Module.finrank_pi, NumberField.InfinitePlace.nrRealPlaces, Module.finrank_pi_fintype, NumberField.InfinitePlace.card_real_embeddings, Complex.finrank_real_complex, mul_comm, NumberField.InfinitePlace.nrComplexPlaces, smul_eq_mul, Complex, Module.finrank_prod, Fintype.card_subtype_compl, NumberField.InfinitePlace.card_complex_embeddings, Finset.sum_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Function.Injective (α := K) (β := mixedSpace K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)

Tactic:
RingHom.injective _

Premises used: RingHom.injective
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Function.Injective (α := K) (β := mixedSpace K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)

Tactic:
exact RingHom.injective _

Premises used: RingHom.injective
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsAddHaarMeasure.{u_1} (G := mixedSpace K) volume

Tactic:
prod.instIsAddHaarMeasure volume volume

Premises used: MeasureTheory.Measure.prod.instIsAddHaarMeasure, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
obtain : ∀ (w : InfinitePlace K), NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
obtain ⟨w⟩ := (inferInstance : Nonempty (InfinitePlace K))

Premises used: inferInstance
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
pos : ∀ (hw : w.IsReal), NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume
neg : ∀ (hw : ¬w.IsReal), NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
by_cases hw : IsReal w

Premises used: NumberField.InfinitePlace.IsReal
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsReal
⊢ NoAtoms.{u_1} (α := { w : InfinitePlace K // w.IsReal } → ℝ) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
have : NoAtoms (volume : Measure ({w : InfinitePlace K // IsReal w} → ℝ)) := pi_noAtoms ⟨w, hw⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsReal
this : NoAtoms.{u_1} (α := { w : InfinitePlace K // w.IsReal } → ℝ) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
prod.instNoAtoms_fst

Premises used: MeasureTheory.Measure.prod.instNoAtoms_fst
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsReal
this : NoAtoms.{u_1} (α := { w : InfinitePlace K // w.IsReal } → ℝ) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
exact prod.instNoAtoms_fst

Premises used: MeasureTheory.Measure.prod.instNoAtoms_fst
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
⊢ NoAtoms.{u_1} (α := { w : InfinitePlace K // w.IsComplex } → ℂ) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
have : NoAtoms (volume : Measure ({w : InfinitePlace K // IsComplex w} → ℂ)) :=
      pi_noAtoms ⟨w, not_isReal_iff_isComplex.mp hw⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
this : NoAtoms.{u_1} (α := { w : InfinitePlace K // w.IsComplex } → ℂ) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
prod.instNoAtoms_snd

Premises used: MeasureTheory.Measure.prod.instNoAtoms_snd