awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsComplex
h :
  { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
      mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw } →
    { x : K →+* ℂ // mk x = w }
h₁ :
  ∀
    (x x_1 :
      { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
        mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw })
    (h :
      Eq (α := { x : K →+* ℂ // mk x = w })
        (match (motive :=
            { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
                mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw } →
              { x : K →+* ℂ // mk x = w })
            x with
          | ⟨φ, hφ⟩ => Subtype.mk (p := fun (x : K →+* ℂ) ↦ mk x = w) (↑φ : K →+* ℂ) ⋯ :
          { x : K →+* ℂ // mk x = w })
        (match (motive :=
            { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
                mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw } →
              { x : K →+* ℂ // mk x = w })
            x_1 with
          | ⟨φ, hφ⟩ => Subtype.mk (p := fun (x : K →+* ℂ) ↦ mk x = w) (↑φ : K →+* ℂ) ⋯ :
          { x : K →+* ℂ // mk x = w })),
    x = x_1
h₂ :
  ∀ (x : { x : K →+* ℂ // mk x = w }) (φ : K →+* ℂ) (hφ : mk φ = w),
    ∃ (a :
      { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
        mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw }),
      Eq (α := { x : K →+* ℂ // mk x = w })
        (match (motive :=
            { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
                mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw } →
              { x : K →+* ℂ // mk x = w })
            a with
          | ⟨φ, hφ⟩ => Subtype.mk (p := fun (x : K →+* ℂ) ↦ mk x = w) (↑φ : K →+* ℂ) ⋯ :
          { x : K →+* ℂ // mk x = w })
        (Subtype.mk (p := fun (x : K →+* ℂ) ↦ mk x = w) φ hφ : { x : K →+* ℂ // mk x = w })
⊢ card.{u_1}
      { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
        mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw } =
    card.{u_1} { x : K →+* ℂ // mk x = w }

Tactic:
refine Fintype.card_congr (Equiv.ofBijective ?_ ⟨fun _ _ h => ?_, fun ⟨φ, hφ⟩ => ?_⟩)

Premises used: Fintype.card_congr, And.intro, Equiv.ofBijective
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x :
  { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
    mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw }
φ : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ }
hφ : mkComplex φ = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (hφ :
      (↑(mkComplex φ) : InfinitePlace K) =
        (↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw) : InfinitePlace K)),
    mk (↑φ : K →+* ℂ) = w
⊢ mk (↑φ : K →+* ℂ) = w

Tactic:
rwa [Subtype.ext_iff] at hφ

Premises used: Subtype.ext_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
      mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw } →
    { x : K →+* ℂ // mk x = w }

Tactic:
exact fun ⟨φ, hφ⟩ => ⟨φ.val, by rwa [Subtype.ext_iff] at hφ⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x x_1 :
  { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
    mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw }
h :
  Eq (α := { x : K →+* ℂ // mk x = w })
    (match (motive :=
        { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
            mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw } →
          { x : K →+* ℂ // mk x = w })
        x with
      | ⟨φ, hφ⟩ => Subtype.mk (p := fun (x : K →+* ℂ) ↦ mk x = w) (↑φ : K →+* ℂ) ⋯ :
      { x : K →+* ℂ // mk x = w })
    (match (motive :=
        { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
            mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw } →
          { x : K →+* ℂ // mk x = w })
        x_1 with
      | ⟨φ, hφ⟩ => Subtype.mk (p := fun (x : K →+* ℂ) ↦ mk x = w) (↑φ : K →+* ℂ) ⋯ :
      { x : K →+* ℂ // mk x = w })
h₁ :
  ∀
    (h :
      (↑(↑x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ }) : K →+* ℂ) =
        (↑(↑x_1 : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ }) : K →+* ℂ)),
    x = x_1
h₂ :
  ∀ (h : (↑x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ }) = (↑x_1 : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ })),
    x = x_1
h₃ h₄ h₅ h₆ : ∀ (h : x = x_1), x = x_1
⊢ x = x_1

Tactic:
rwa [Subtype.mk_eq_mk, ← Subtype.ext_iff, ← Subtype.ext_iff] at h

Premises used: Subtype.ext_iff, Subtype.mk_eq_mk
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x : { x : K →+* ℂ // mk x = w }
φ : K →+* ℂ
hφ : mk φ = w
⊢ ∃ (a :
    { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
      mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw }),
    Eq (α := { x : K →+* ℂ // mk x = w })
      (match (motive :=
          { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
              mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw } →
            { x : K →+* ℂ // mk x = w })
          a with
        | ⟨φ, hφ⟩ => Subtype.mk (p := fun (x : K →+* ℂ) ↦ mk x = w) (↑φ : K →+* ℂ) ⋯ :
        { x : K →+* ℂ // mk x = w })
      (Subtype.mk (p := fun (x : K →+* ℂ) ↦ mk x = w) φ hφ : { x : K →+* ℂ // mk x = w })

Tactic:
⟨⟨⟨φ, not_isReal_of_mk_isComplex (hφ.symm ▸ hw)⟩, ?_⟩, rfl⟩

Premises used: NumberField.InfinitePlace.not_isReal_of_mk_isComplex, Eq.rec, Subtype.mk, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x : { x : K →+* ℂ // mk x = w }
φ : K →+* ℂ
hφ : mk φ = w
h :
  mkComplex (Subtype.mk (p := fun (φ : K →+* ℂ) ↦ ¬ComplexEmbedding.IsReal φ) φ ⋯) =
    Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw
⊢ ∃ (a :
    { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
      mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw }),
    Eq (α := { x : K →+* ℂ // mk x = w })
      (match (motive :=
          { x : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } //
              mkComplex x = Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw } →
            { x : K →+* ℂ // mk x = w })
          a with
        | ⟨φ, hφ⟩ => Subtype.mk (p := fun (x : K →+* ℂ) ↦ mk x = w) (↑φ : K →+* ℂ) ⋯ :
        { x : K →+* ℂ // mk x = w })
      (Subtype.mk (p := fun (x : K →+* ℂ) ↦ mk x = w) φ hφ : { x : K →+* ℂ // mk x = w })

Tactic:
refine ⟨⟨⟨φ, not_isReal_of_mk_isComplex (hφ.symm ▸ hw)⟩, ?_⟩, rfl⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x : { x : K →+* ℂ // mk x = w }
φ : K →+* ℂ
hφ : mk φ = w
h :
  (↑(mkComplex (Subtype.mk (p := fun (φ : K →+* ℂ) ↦ ¬ComplexEmbedding.IsReal φ) φ ⋯)) : InfinitePlace K) =
    (↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw) : InfinitePlace K)
h₁ h₂ h₃ h₄ :
  mk (↑(Subtype.mk (p := fun (φ : K →+* ℂ) ↦ ¬ComplexEmbedding.IsReal φ) φ ⋯) : K →+* ℂ) =
    (↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw) : InfinitePlace K)
⊢ mkComplex (Subtype.mk (p := fun (φ : K →+* ℂ) ↦ ¬ComplexEmbedding.IsReal φ) φ ⋯) =
    Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw

Tactic:
rwa [Subtype.ext_iff, mkComplex_coe]

Premises used: Subtype.ext_iff, NumberField.InfinitePlace.mkComplex_coe
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsComplex
h : Eq (α := ℕ) 2 (if w.IsReal then 1 else 2)
h₁ : Eq (α := ℕ) 2 (if False then 1 else 2)
⊢ 2 = w.mult

Tactic:
simp_rw [mult, not_isReal_iff_isComplex.mpr hw, ite_false]

Premises used: Iff.mpr, ite_false, NumberField.InfinitePlace.mult, NumberField.InfinitePlace.not_isReal_iff_isComplex
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } ≤ card.{u_1} (K →+* ℂ)
⊢ nrRealPlaces K + 2 * nrComplexPlaces K = finrank ℚ K

Tactic:
rw [← card_real_embeddings, ← card_complex_embeddings, Fintype.card_subtype_compl,
    ← Embeddings.card K ℂ, Nat.add_sub_of_le]

Premises used: Nat.add_sub_of_le, NumberField.Embeddings.card, NumberField.InfinitePlace.card_real_embeddings, Complex, Fintype.card_subtype_compl, NumberField.InfinitePlace.card_complex_embeddings
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } ≤ card.{u_1} (K →+* ℂ)

Tactic:
Fintype.card_subtype_le _

Premises used: Fintype.card_subtype_le
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } ≤ card.{u_1} (K →+* ℂ)

Tactic:
exact Fintype.card_subtype_le _

Premises used: Fintype.card_subtype_le
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + 2 * nrComplexPlaces K = finrank ℚ K
rw₁ :
  card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } =
    finrank ℚ K
rw₂ :
  card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      (card.{u_1} (K →+* ℂ) - card.{u_1} { x : K →+* ℂ // ComplexEmbedding.IsReal x }) =
    finrank ℚ K
rw₃ :
  card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      (card.{u_1} (K →+* ℂ) - card.{u_1} { x : K →+* ℂ // ComplexEmbedding.IsReal x }) =
    card.{u_1} (K →+* ℂ)
rw₄ : card.{u_1} (K →+* ℂ) = card.{u_1} (K →+* ℂ)
rw₅ : card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } ≤ card.{u_1} (K →+* ℂ)
rw₆ : card.{u_1} (K →+* ℂ) = card.{u_1} (K →+* ℂ)
rw₇ rw₈ : card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } ≤ card.{u_1} (K →+* ℂ)
⊢ nrRealPlaces K + 2 * nrComplexPlaces K = finrank ℚ K

Tactic:
classical
  rw [← card_real_embeddings, ← card_complex_embeddings, Fintype.card_subtype_compl,
    ← Embeddings.card K ℂ, Nat.add_sub_of_le]
  exact Fintype.card_subtype_le _

Premises used: Fintype.card_subtype_le, Nat.add_sub_of_le, NumberField.Embeddings.card, NumberField.InfinitePlace.card_real_embeddings, Complex, Fintype.card_subtype_compl, NumberField.InfinitePlace.card_complex_embeddings
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : HPow.hPow (α := Equiv.Perm (K →+* ℂ)) (β := ℕ) (Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯) 2 = 1
⊢ ((Equiv.Perm.sign : Equiv.Perm (K →+* ℂ) →* ℤˣ) : (a : Equiv.Perm (K →+* ℂ)) → ℤˣ)
      (Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯) =
    HPow.hPow (α := ℤˣ) (-1) (nrComplexPlaces K)

Tactic:
rw [Equiv.Perm.sign_of_pow_two_eq_one, Embeddings.card, ← card_add_two_mul_card_eq_rank,
    ← card_real_embeddings, Fintype.card, Fintype.card, Nat.add_sub_cancel_left,
    Nat.mul_div_cancel_left _ zero_lt_two]

Premises used: Nat.mul_div_cancel_left, Nat.add_sub_cancel_left, Fintype.card, NumberField.Embeddings.card, Equiv.Perm.sign_of_pow_two_eq_one, NumberField.InfinitePlace.card_real_embeddings, NumberField.InfinitePlace.card_add_two_mul_card_eq_rank, zero_lt_two
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ HPow.hPow (α := Equiv.Perm (K →+* ℂ)) (β := ℕ) (Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯) 2 = 1

Tactic:
Equiv.ext (ComplexEmbedding.involutive_conjugate K).toPerm_involutive

Premises used: NumberField.ComplexEmbedding.involutive_conjugate, Equiv.ext, Function.Involutive.toPerm_involutive
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ HPow.hPow (α := Equiv.Perm (K →+* ℂ)) (β := ℕ) (Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯) 2 = 1

Tactic:
exact Equiv.ext (ComplexEmbedding.involutive_conjugate K).toPerm_involutive
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : finrank ℚ K = 1
linarith :
  nrComplexPlaces K < 0 →
    -1 + HSub.hSub (α := ℤ) 0 (↑(nrComplexPlaces K) : ℤ) + (HAdd.hAdd (α := ℤ) (↑(nrComplexPlaces K) : ℤ) 1 - 0) = 0
linarith₁ :
  0 < nrComplexPlaces K →
    -1 + HSub.hSub (α := ℤ) 0 (↑(nrRealPlaces K) : ℤ) + HSub.hSub (α := ℤ) (↑(finrank ℚ K) : ℤ) 1 +
          2 * (HAdd.hAdd (α := ℤ) 0 1 - (↑(nrComplexPlaces K) : ℤ)) +
        ((↑(nrRealPlaces K) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(nrComplexPlaces K) : ℤ) - (↑(finrank ℚ K) : ℤ)) =
      0
linarith₂ : 0 < nrComplexPlaces K → GT.gt (α := ℤ) 2 0
⊢ nrComplexPlaces K = 0

Tactic:
linarith [card_add_two_mul_card_eq_rank K]

Premises used: NumberField.InfinitePlace.card_add_two_mul_card_eq_rank
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : finrank ℚ K = 1
⊢ nrRealPlaces K + 2 * nrComplexPlaces K = finrank ℚ K

Tactic:
have := card_add_two_mul_card_eq_rank K
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : finrank ℚ K = 1
this : nrRealPlaces K + 2 * nrComplexPlaces K = finrank ℚ K
rwa : ∀ (this : nrRealPlaces K + HMul.hMul (α := ℕ) 2 0 = finrank ℚ K), nrRealPlaces K = 1
rwa₁ : ∀ (this : nrRealPlaces K + HMul.hMul (α := ℕ) 2 0 = 1), nrRealPlaces K = 1
rwa₂ : ∀ (this : nrRealPlaces K + 0 = 1), nrRealPlaces K = 1
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : nrRealPlaces K = 1), nrRealPlaces K = 1
⊢ nrRealPlaces K = 1

Tactic:
rwa [nrComplexPlaces_eq_zero_of_finrank_eq_one h, h, mul_zero, add_zero] at this

Premises used: MulZeroClass.mul_zero, NumberField.InfinitePlace.nrComplexPlaces_eq_zero_of_finrank_eq_one, add_zero
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (finrank ℚ K)
⊢ 0 < nrRealPlaces K

Tactic:
Nat.pos_of_ne_zero ?_

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (finrank ℚ K)
refine : nrRealPlaces K ≠ 0
⊢ 0 < nrRealPlaces K

Tactic:
refine Nat.pos_of_ne_zero ?_

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (finrank ℚ K)
by_contra : ∀ (hc : nrRealPlaces K = 0), False
⊢ nrRealPlaces K ≠ 0

Tactic:
by_contra hc
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (finrank ℚ K)
hc : nrRealPlaces K = 0
⊢ False

Tactic:
(Nat.not_odd_iff_even.mpr ?_) h

Premises used: Iff.mpr, Nat.not_odd_iff_even
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (finrank ℚ K)
hc : nrRealPlaces K = 0
refine : Even (finrank ℚ K)
⊢ False

Tactic:
refine (Nat.not_odd_iff_even.mpr ?_) h

Premises used: Iff.mpr, Nat.not_odd_iff_even
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (finrank ℚ K)
hc : nrRealPlaces K = 0
rw : Even (2 * nrComplexPlaces K)
⊢ Even (finrank ℚ K)

Tactic:
rw [← card_add_two_mul_card_eq_rank, hc, zero_add]

Premises used: zero_add, NumberField.InfinitePlace.card_add_two_mul_card_eq_rank
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (finrank ℚ K)
hc : nrRealPlaces K = 0
⊢ Even (2 * nrComplexPlaces K)

Tactic:
even_two_mul (nrComplexPlaces K)

Premises used: even_two_mul, NumberField.InfinitePlace.nrComplexPlaces
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (finrank ℚ K)
hc : nrRealPlaces K = 0
⊢ Even (2 * nrComplexPlaces K)

Tactic:
exact even_two_mul (nrComplexPlaces K)

Premises used: even_two_mul, NumberField.InfinitePlace.nrComplexPlaces
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
⊢ nrRealPlaces K = 0

Tactic:
(@Fintype.card_eq_zero_iff _ (_)).2 ⟨fun ⟨w, hwreal⟩ ↦ ?_⟩

Premises used: Iff.mpr, False, IsEmpty.mk, Fintype.card_eq_zero_iff, _private.0.NumberField.InfinitePlace.IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_lt.match_1
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
refine : ∀ (x : { w : InfinitePlace K // w.IsReal }) (w : InfinitePlace K) (hwreal : w.IsReal), False
⊢ nrRealPlaces K = 0

Tactic:
refine (@Fintype.card_eq_zero_iff _ (_)).2 ⟨fun ⟨w, hwreal⟩ ↦ ?_⟩

Premises used: Iff.mpr, IsEmpty.mk, Fintype.card_eq_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x : { w : InfinitePlace K // w.IsReal }
w : InfinitePlace K
hwreal : w.IsReal
⊢ ComplexEmbedding.IsReal w.embedding

Tactic:
rw [NumberField.InfinitePlace.isReal_iff] at hwreal

Premises used: NumberField.InfinitePlace.isReal_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x : { w : InfinitePlace K // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
⊢ IsPrimitiveRoot (M := ℂ) ((f : (a : K) → ℂ) ζ : ℂ) k

Tactic:
have hζ' : IsPrimitiveRoot (f ζ) k := hζ.map_of_injective f.injective
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x : { w : InfinitePlace K // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (M := ℂ) ((f : (a : K) → ℂ) ζ : ℂ) k
rw : Eq (α := ℂ) ((ComplexEmbedding.conjugate f : (a : K) → ℂ) ζ : ℂ) ((f : (a : K) → ℂ) ζ : ℂ)
⊢ Complex.im ((f : (a : K) → ℂ) ζ) = 0

Tactic:
rw [← Complex.conj_eq_iff_im, ← NumberField.ComplexEmbedding.conjugate_coe_eq]

Premises used: Complex.conj_eq_iff_im, NumberField.ComplexEmbedding.conjugate_coe_eq
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x : { w : InfinitePlace K // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (M := ℂ) ((f : (a : K) → ℂ) ζ : ℂ) k
⊢ Eq (α := ℂ) ((ComplexEmbedding.conjugate f : (a : K) → ℂ) ζ : ℂ) ((f : (a : K) → ℂ) ζ : ℂ)

Tactic:
congr
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x : { w : InfinitePlace K // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (M := ℂ) ((f : (a : K) → ℂ) ζ : ℂ) k
⊢ Complex.im ((f : (a : K) → ℂ) ζ) = 0

Tactic:
have him : (f ζ).im = 0 := by
    rw [← Complex.conj_eq_iff_im, ← NumberField.ComplexEmbedding.conjugate_coe_eq]
    congr
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x : { w : InfinitePlace K // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (M := ℂ) ((f : (a : K) → ℂ) ζ : ℂ) k
him : Complex.im ((f : (a : K) → ℂ) ζ) = 0
⊢ |Complex.re ((f : (a : K) → ℂ) ζ)| = norm (E := ℂ) ((f : (a : K) → ℂ) ζ : ℂ)

Tactic:
rw [← Complex.abs_re_eq_norm] at him

Premises used: Complex.abs_re_eq_norm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x : { w : InfinitePlace K // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (M := ℂ) ((f : (a : K) → ℂ) ζ : ℂ) k
him : |Complex.re ((f : (a : K) → ℂ) ζ)| = norm (E := ℂ) ((f : (a : K) → ℂ) ζ : ℂ)
⊢ k ≠ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x : { w : InfinitePlace K // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (M := ℂ) ((f : (a : K) → ℂ) ζ : ℂ) k
him : |Complex.re ((f : (a : K) → ℂ) ζ)| = norm (E := ℂ) ((f : (a : K) → ℂ) ζ : ℂ)
⊢ norm (E := ℂ) ((f : (a : K) → ℂ) ζ : ℂ) = 1

Tactic:
have := Complex.norm_eq_one_of_pow_eq_one hζ'.pow_eq_one (by lia)
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x : { w : InfinitePlace K // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (M := ℂ) ((f : (a : K) → ℂ) ζ : ℂ) k
him : |Complex.re ((f : (a : K) → ℂ) ζ)| = norm (E := ℂ) ((f : (a : K) → ℂ) ζ : ℂ)
this : norm (E := ℂ) ((f : (a : K) → ℂ) ζ : ℂ) = 1
rwa :
  ∀ (this : |Complex.re ((f : (a : K) → ℂ) ζ)| = 1),
    Complex.re ((f : (a : K) → ℂ) ζ) = 1 ∨ Complex.re ((f : (a : K) → ℂ) ζ) = -1
rwa₁ :
  ∀ (this : |Complex.re ((f : (a : K) → ℂ) ζ)| = |1|),
    Complex.re ((f : (a : K) → ℂ) ζ) = 1 ∨ Complex.re ((f : (a : K) → ℂ) ζ) = -1
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (this : Complex.re ((f : (a : K) → ℂ) ζ) = 1 ∨ Complex.re ((f : (a : K) → ℂ) ζ) = -1),
    Complex.re ((f : (a : K) → ℂ) ζ) = 1 ∨ Complex.re ((f : (a : K) → ℂ) ζ) = -1
⊢ Complex.re ((f : (a : K) → ℂ) ζ) = 1 ∨ Complex.re ((f : (a : K) → ℂ) ζ) = -1

Tactic:
rwa [← him, ← abs_one, abs_eq_abs] at this

Premises used: abs_one, abs_eq_abs
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x : { w : InfinitePlace K // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (M := ℂ) ((f : (a : K) → ℂ) ζ : ℂ) k
him : Complex.im ((f : (a : K) → ℂ) ζ) = 0
⊢ Complex.re ((f : (a : K) → ℂ) ζ) = 1 ∨ Complex.re ((f : (a : K) → ℂ) ζ) = -1

Tactic:
have hre : (f ζ).re = 1 ∨ (f ζ).re = -1 := by
    rw [← Complex.abs_re_eq_norm] at him
    have := Complex.norm_eq_one_of_pow_eq_one hζ'.pow_eq_one (by lia)
    rwa [← him, ← abs_one, abs_eq_abs] at this
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x : { w : InfinitePlace K // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (M := ℂ) ((f : (a : K) → ℂ) ζ : ℂ) k
him : Complex.im ((f : (a : K) → ℂ) ζ) = 0
hone : Complex.re ((f : (a : K) → ℂ) ζ) = 1
⊢ 1 < k

Tactic:
lia