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
φ : K →+* ℂ
pos :
  ∀ (hφ : ComplexEmbedding.IsReal φ),
    ∃ (a : index K),
      (fun (c : index K) ↦
            (Sum.casesOn (motive :=
                fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
                (h : c = t) → K →+* ℂ) c
                (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
                (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                  Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                    fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                    if j = 0 then (↑w : InfinitePlace K).embedding
                    else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
                ⋯ :
              K →+* ℂ))
          a =
        φ
neg :
  ∀ (hφ : ¬ComplexEmbedding.IsReal φ),
    ∃ (a : index K),
      (fun (c : index K) ↦
            (Sum.casesOn (motive :=
                fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
                (h : c = t) → K →+* ℂ) c
                (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
                (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                  Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                    fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                    if j = 0 then (↑w : InfinitePlace K).embedding
                    else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
                ⋯ :
              K →+* ℂ))
          a =
        φ
⊢ ∃ (a : index K),
    (fun (c : index K) ↦
          (Sum.casesOn (motive :=
              fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
              (h : c = t) → K →+* ℂ) c
              (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
              (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                  fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                  if j = 0 then (↑w : InfinitePlace K).embedding
                  else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
              ⋯ :
            K →+* ℂ))
        a =
      φ

Tactic:
by_cases hφ : ComplexEmbedding.IsReal φ

Premises used: NumberField.ComplexEmbedding.IsReal
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ (fun (c : index K) ↦
        (Sum.casesOn (motive :=
            fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
            (h : c = t) → K →+* ℂ) c
            (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
            (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
              Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                if j = 0 then (↑w : InfinitePlace K).embedding
                else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
            ⋯ :
          K →+* ℂ))
      (Sum.inl
        ((mkReal : (a : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) → { w : InfinitePlace K // w.IsReal })
          (Subtype.mk (p := fun (φ : K →+* ℂ) ↦ ComplexEmbedding.IsReal φ) φ hφ))) =
    φ

Tactic:
simp [embedding_mk_eq_of_isReal hφ]

Premises used: NumberField.InfinitePlace.embedding_mk_eq_of_isReal
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ ∃ (a : index K),
    (fun (c : index K) ↦
          (Sum.casesOn (motive :=
              fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
              (h : c = t) → K →+* ℂ) c
              (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
              (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                  fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                  if j = 0 then (↑w : InfinitePlace K).embedding
                  else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
              ⋯ :
            K →+* ℂ))
        a =
      φ

Tactic:
exact ⟨Sum.inl (InfinitePlace.mkReal ⟨φ, hφ⟩), by simp [embedding_mk_eq_of_isReal hφ]⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
pos :
  ∀ (hw : (InfinitePlace.mk φ).embedding = φ),
    ∃ (a : index K),
      (fun (c : index K) ↦
            (Sum.casesOn (motive :=
                fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
                (h : c = t) → K →+* ℂ) c
                (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
                (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                  Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                    fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                    if j = 0 then (↑w : InfinitePlace K).embedding
                    else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
                ⋯ :
              K →+* ℂ))
          a =
        φ
neg :
  ∀ (hw : ¬(InfinitePlace.mk φ).embedding = φ),
    ∃ (a : index K),
      (fun (c : index K) ↦
            (Sum.casesOn (motive :=
                fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
                (h : c = t) → K →+* ℂ) c
                (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
                (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                  Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                    fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                    if j = 0 then (↑w : InfinitePlace K).embedding
                    else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
                ⋯ :
              K →+* ℂ))
          a =
        φ
⊢ ∃ (a : index K),
    (fun (c : index K) ↦
          (Sum.casesOn (motive :=
              fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
              (h : c = t) → K →+* ℂ) c
              (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
              (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                  fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                  if j = 0 then (↑w : InfinitePlace K).embedding
                  else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
              ⋯ :
            K →+* ℂ))
        a =
      φ

Tactic:
by_cases hw : (InfinitePlace.mk φ).embedding = φ

Premises used: NumberField.InfinitePlace.mk, NumberField.InfinitePlace.embedding
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
hw : (InfinitePlace.mk φ).embedding = φ
⊢ (fun (c : index K) ↦
        (Sum.casesOn (motive :=
            fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
            (h : c = t) → K →+* ℂ) c
            (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
            (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
              Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                if j = 0 then (↑w : InfinitePlace K).embedding
                else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
            ⋯ :
          K →+* ℂ))
      (Sum.inr (mkComplex (Subtype.mk (p := fun (φ : K →+* ℂ) ↦ ¬ComplexEmbedding.IsReal φ) φ hφ), 0)) =
    φ

Tactic:
simp [hw]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
hw : (InfinitePlace.mk φ).embedding = φ
⊢ ∃ (a : index K),
    (fun (c : index K) ↦
          (Sum.casesOn (motive :=
              fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
              (h : c = t) → K →+* ℂ) c
              (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
              (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                  fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                  if j = 0 then (↑w : InfinitePlace K).embedding
                  else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
              ⋯ :
            K →+* ℂ))
        a =
      φ

Tactic:
exact ⟨Sum.inr ⟨InfinitePlace.mkComplex ⟨φ, hφ⟩, 0⟩, by simp [hw]⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
hw : ¬(InfinitePlace.mk φ).embedding = φ
⊢ (fun (c : index K) ↦
        (Sum.casesOn (motive :=
            fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
            (h : c = t) → K →+* ℂ) c
            (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
            (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
              Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                if j = 0 then (↑w : InfinitePlace K).embedding
                else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
            ⋯ :
          K →+* ℂ))
      (Sum.inr (mkComplex (Subtype.mk (p := fun (φ : K →+* ℂ) ↦ ¬ComplexEmbedding.IsReal φ) φ hφ), 1)) =
    φ

Tactic:
simp [(embedding_mk_eq φ).resolve_left hw]

Premises used: Or.resolve_left, NumberField.InfinitePlace.embedding_mk_eq
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
hw : ¬(InfinitePlace.mk φ).embedding = φ
⊢ ∃ (a : index K),
    (fun (c : index K) ↦
          (Sum.casesOn (motive :=
              fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
              (h : c = t) → K →+* ℂ) c
              (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
              (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
                Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
                  fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
                  if j = 0 then (↑w : InfinitePlace K).embedding
                  else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
              ⋯ :
            K →+* ℂ))
        a =
      φ

Tactic:
exact ⟨Sum.inr ⟨InfinitePlace.mkComplex ⟨φ, hφ⟩, 1⟩,
          by simp [(embedding_mk_eq φ).resolve_left hw]⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine_3 : Fintype.card.{u_1} (index K) = finrank ℚ K
refine_3₁ : Fintype.card.{u_1} (index K) = finrank.{0, u_1} ℝ (mixedSpace K)
refine_3₂ refine_3₃ : finrank.{0, u_1} ℝ (mixedSpace K) = finrank.{0, u_1} ℝ (mixedSpace K)
⊢ Fintype.card.{u_1} (index K) = Fintype.card.{u_1} (K →+* ℂ)

Tactic:
rw [Embeddings.card, ← mixedEmbedding.finrank K,
      ← Module.finrank_eq_card_basis (stdBasis K)]

Premises used: NumberField.mixedEmbedding.stdBasis, NumberField.Embeddings.card, Module.finrank_eq_card_basis, NumberField.mixedEmbedding.finrank
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : { w : InfinitePlace K // w.IsReal }
⊢ (indexEquiv K : (a : index K) → K →+* ℂ) (Sum.inl w) = (↑w : InfinitePlace K).embedding

Tactic:
rfl

Premises used: NumberField.InfinitePlace.embedding, Classical.choose, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : { w : InfinitePlace K // w.IsComplex }
⊢ (indexEquiv K : (a : index K) → K →+* ℂ) (Sum.inr (w, 0)) = (↑w : InfinitePlace K).embedding

Tactic:
rfl

Premises used: NumberField.InfinitePlace.embedding, Classical.choose, rfl, ite
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : { w : InfinitePlace K // w.IsComplex }
⊢ (indexEquiv K : (a : index K) → K →+* ℂ) (Sum.inr (w, 1)) =
    ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := ℂ)
    (∏ _k : { w : InfinitePlace K // w.IsComplex },
      (HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)).det)
    (∏ _k : { w : InfinitePlace K // w.IsComplex }, 2⁻¹ * I)

Tactic:
prod_congr (Eq.refl _) (fun _ _ => ?_)

Premises used: Finset.prod_congr, Eq.refl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine :
  ∀ (x : { w : InfinitePlace K // w.IsComplex }),
    Membership.mem (γ := Finset { w : InfinitePlace K // w.IsComplex }) univ x →
      (HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)).det =
        2⁻¹ * I
⊢ Eq (α := ℂ)
    (∏ _k : { w : InfinitePlace K // w.IsComplex },
      (HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)).det)
    (∏ _k : { w : InfinitePlace K // w.IsComplex }, 2⁻¹ * I)

Tactic:
refine prod_congr (Eq.refl _) (fun _ _ => ?_)

Premises used: Finset.prod_congr, Eq.refl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : { w : InfinitePlace K // w.IsComplex }
h : Membership.mem (γ := Finset { w : InfinitePlace K // w.IsComplex }) univ x
simp : HAdd.hAdd (α := ℂ) 1 1 = 2
⊢ (HSMul.hSMul (α := ℂ) (β := Matrix (Fin 2) (Fin 2) ℂ) 2⁻¹ (!![1, 1; -I, I] : Matrix (Fin 2) (Fin 2) ℂ)).det = 2⁻¹ * I

Tactic:
simp [field]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : { w : InfinitePlace K // w.IsComplex }
h : Membership.mem (γ := Finset { w : InfinitePlace K // w.IsComplex }) univ x
⊢ HAdd.hAdd (α := ℂ) 1 1 = 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  (2⁻¹ * I) ^ card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ =
    (2⁻¹ * I) ^ Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }
rw₁ rw₂ :
  (2⁻¹ * I) ^ card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ =
    (2⁻¹ * I) ^ card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ
⊢ ∏ _k : { w : InfinitePlace K // w.IsComplex }, 2⁻¹ * I =
    (2⁻¹ * I) ^ Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }

Tactic:
rw [prod_const, Fintype.card]

Premises used: Fintype.card, Finset.prod_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w : InfinitePlace K // w.IsComplex }
⊢ HAdd.hAdd (β := ℂ) (x (↑w : InfinitePlace K).embedding)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) (x (↑w : InfinitePlace K).embedding) : ℂ) /
      2 =
    2⁻¹ * x (↑w : InfinitePlace K).embedding +
      HMul.hMul (α := ℂ) (β := ℂ) (2⁻¹ : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x (↑w : InfinitePlace K).embedding) : ℂ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w : InfinitePlace K // w.IsComplex }
inr :
  x (↑w : InfinitePlace K).embedding * I⁻¹ * (1 / 2) +
      HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x (↑w : InfinitePlace K).embedding) : ℂ) I⁻¹ * (-1 / 2) =
    x (↑w : InfinitePlace K).embedding * I * (-1 / 2) +
      HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x (↑w : InfinitePlace K).embedding) : ℂ) I * (1 / 2)
⊢ HSub.hSub (β := ℂ) (x (↑w : InfinitePlace K).embedding)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) (x (↑w : InfinitePlace K).embedding) : ℂ) /
      (2 * I) =
    -(2⁻¹ * I * x (↑w : InfinitePlace K).embedding) +
      HMul.hMul (β := ℂ) (2⁻¹ * I) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x (↑w : InfinitePlace K).embedding) : ℂ)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w : InfinitePlace K // w.IsComplex }
⊢ x (↑w : InfinitePlace K).embedding * I⁻¹ * (1 / 2) +
      HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x (↑w : InfinitePlace K).embedding) : ℂ) I⁻¹ * (-1 / 2) =
    x (↑w : InfinitePlace K).embedding * I * (-1 / 2) +
      HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x (↑w : InfinitePlace K).embedding) : ℂ) I * (1 / 2)

Tactic:
simp [field]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Function.Injective (β := ℂ) fun (r : ℝ) ↦ HSMul.hSMul (β := ℂ) r 1

Tactic:
simpa only [Complex.real_smul, mul_one] using Complex.ofReal_injective

Premises used: Complex.real_smul, Complex.ofReal_injective, mul_one
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Function.Injective (β := ℂ) fun (r : ℝ) ↦ HSMul.hSMul (β := ℂ) r 1

Tactic:
{ simpa only [Complex.real_smul, mul_one] using Complex.ofReal_injective }

Premises used: Complex.real_smul, Complex.ofReal_injective, mul_one
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ LinearIndependent (ι := ChooseBasisIndex ℤ (𝓞 K)) ℝ (M := mixedSpace K)
    (Function.comp (β := (K →+* ℂ) → ℂ) (⇑(commMap K) : (a : (K →+* ℂ) → ℂ) → mixedSpace K)
      (⇑(canonicalEmbedding.latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
        (a : ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))

Tactic:
have := LinearIndependent.map (LinearIndependent.restrict_scalars
      (by { simpa only [Complex.real_smul, mul_one] using Complex.ofReal_injective })
      (canonicalEmbedding.latticeBasis K).linearIndependent)
      (disjoint_span_commMap_ker K)
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this :
  LinearIndependent (ι := ChooseBasisIndex ℤ (𝓞 K)) ℝ (M := mixedSpace K)
    (Function.comp (β := (K →+* ℂ) → ℂ) (⇑(commMap K) : (a : (K →+* ℂ) → ℂ) → mixedSpace K)
      (⇑(canonicalEmbedding.latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
        (a : ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))
refine : Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
⊢ Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)

Tactic:
refine basisOfLinearIndependentOfCardEqFinrank this ?_

Premises used: basisOfLinearIndependentOfCardEqFinrank
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
We We₁ We₂ :
  (this :
      LinearIndependent (ι := ChooseBasisIndex ℤ (𝓞 K)) ℝ (M := mixedSpace K)
        (Function.comp (β := (K →+* ℂ) → ℂ) (⇑(commMap K) : (a : (K →+* ℂ) → ℂ) → mixedSpace K)
          (⇑(canonicalEmbedding.latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
            (a : ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))) →
    Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)
We₃ :
  ∀
    (this :
      LinearIndependent (ι := ChooseBasisIndex ℤ (𝓞 K)) ℝ (M := mixedSpace K)
        (Function.comp (β := (K →+* ℂ) → ℂ) (⇑(commMap K) : (a : (K →+* ℂ) → ℂ) → mixedSpace K)
          (⇑(canonicalEmbedding.latticeBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
            (a : ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))),
    Fintype.card.{u_1} (ChooseBasisIndex ℤ (𝓞 K)) = finrank.{0, u_1} ℝ (mixedSpace K)
⊢ Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)

Tactic:
classical
    -- We construct an `ℝ`-linear independent family from the image of
    -- `canonicalEmbedding.lattice_basis` by `commMap`
    have := LinearIndependent.map (LinearIndependent.restrict_scalars
      (by { simpa only [Complex.real_smul, mul_one] using Complex.ofReal_injective })
      (canonicalEmbedding.latticeBasis K).linearIndependent)
      (disjoint_span_commMap_ker K)
    -- and it's a basis since it has the right cardinality
    refine basisOfLinearIndependentOfCardEqFinrank this ?_
    rw [← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank, 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.RingOfIntegers.rank, NumberField.InfinitePlace.nrRealPlaces, Module.finrank_pi_fintype, Module.finrank_eq_card_chooseBasisIndex, 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