-- Mathlib/NumberTheory/Cyclotomic/Embeddings.lean
theorem nrComplexPlaces_eq_totient_div_two [h : IsCyclotomicExtension {n} ℚ K] :
    haveI := IsCyclotomicExtension.numberField {n} ℚ K
    nrComplexPlaces K = φ n / 2

Proof state:
case neg
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : ¬1 < ↑n
⊢ φ ↑n = 1

Tactic:
convert totient_one

Result:
case h.e'_2.h.e'_1
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : ¬1 < ↑n
⊢ ↑n = 1

Proof state:
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
⊢ nrComplexPlaces K = φ ↑n / 2

Tactic:
have := IsCyclotomicExtension.numberField {n} ℚ K

Result:
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ nrComplexPlaces K = φ ↑n / 2

Proof state:
case pos.intro
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : 2 < n
k : ℕ
hk : φ ↑n = k + k
key : nrComplexPlaces K = k
⊢ nrComplexPlaces K = φ ↑n / 2

Tactic:
simp [hk, key, ← two_mul]

Result:
no goals

Proof state:
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
⊢ φ ↑n = 1

Tactic:
by_cases h1 : 1 < n.1

Result:
case pos
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : 1 < ↑n
⊢ φ ↑n = 1

case neg
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : ¬1 < ↑n
⊢ φ ↑n = 1

Proof state:
case h.e'_2.h.e'_1
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : ¬1 < ↑n
⊢ n = 1

Tactic:
exact eq_of_le_of_not_lt (not_lt.mp h1) (PNat.not_lt_one _)

Result:
no goals

Proof state:
case neg.h
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this✝ : NumberField K
hn : ¬2 < n
this : φ ↑n = 1
⊢ Module.finrank ℚ K = 1

Tactic:
rw [IsCyclotomicExtension.finrank K (cyclotomic.irreducible_rat n.pos), this]

Result:
no goals

Proof state:
case pos.intro
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : 2 < n
k : ℕ
hk : φ ↑n = k + k
⊢ nrComplexPlaces K = φ ↑n / 2

Tactic:
have key := card_add_two_mul_card_eq_rank K

Result:
case pos.intro
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : 2 < n
k : ℕ
hk : φ ↑n = k + k
key : nrRealPlaces K + 2 * nrComplexPlaces K = Module.finrank ℚ K
⊢ nrComplexPlaces K = φ ↑n / 2

Proof state:
case h.e'_2.h.e'_1
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : 1 < ↑n
⊢ ↑n = 2

Tactic:
exact (eq_of_le_of_not_lt (succ_le_of_lt h1) hn).symm

Result:
no goals

Proof state:
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ nrComplexPlaces K = φ ↑n / 2

Tactic:
by_cases hn : 2 < n

Result:
case pos
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : 2 < n
⊢ nrComplexPlaces K = φ ↑n / 2

case neg
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
⊢ nrComplexPlaces K = φ ↑n / 2

Proof state:
case pos
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : 2 < n
⊢ nrComplexPlaces K = φ ↑n / 2

Tactic:
obtain ⟨k, hk : φ n = k + k⟩ := totient_even hn

Result:
case pos.intro
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : 2 < n
k : ℕ
hk : φ ↑n = k + k
⊢ nrComplexPlaces K = φ ↑n / 2

Proof state:
case h.e'_2.h.e'_1
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : ¬1 < ↑n
⊢ ↑n = 1

Tactic:
rw [← PNat.one_coe, PNat.coe_inj]

Result:
case h.e'_2.h.e'_1
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : ¬1 < ↑n
⊢ n = 1

Proof state:
case neg
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this✝ : NumberField K
hn : ¬2 < n
this : φ ↑n = 1
⊢ nrComplexPlaces K = φ ↑n / 2

Tactic:
rw [this]

Result:
case neg
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this✝ : NumberField K
hn : ¬2 < n
this : φ ↑n = 1
⊢ nrComplexPlaces K = 1 / 2

Proof state:
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : 2 < n
k : ℕ
hk : φ ↑n = k + k
key : 2 * nrComplexPlaces K = 2 * k
⊢ 2 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
case pos
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : 1 < ↑n
⊢ φ ↑n = 1

Tactic:
convert totient_two

Result:
case h.e'_2.h.e'_1
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : 1 < ↑n
⊢ ↑n = 2

Proof state:
case neg
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this✝ : NumberField K
hn : ¬2 < n
this : φ ↑n = 1
⊢ nrComplexPlaces K = 1 / 2

Tactic:
apply nrComplexPlaces_eq_zero_of_finrank_eq_one

Result:
case neg.h
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this✝ : NumberField K
hn : ¬2 < n
this : φ ↑n = 1
⊢ Module.finrank ℚ K = 1

Proof state:
case pos.intro
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : 2 < n
k : ℕ
hk : φ ↑n = k + k
key : nrRealPlaces K + 2 * nrComplexPlaces K = Module.finrank ℚ K
⊢ nrComplexPlaces K = φ ↑n / 2

Tactic:
rw [nrRealPlaces_eq_zero K hn, zero_add, IsCyclotomicExtension.finrank (n := n) K
  (cyclotomic.irreducible_rat n.pos), hk, ← two_mul, Nat.mul_right_inj (by norm_num)] at key

Result:
case pos.intro
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : 2 < n
k : ℕ
hk : φ ↑n = k + k
key : nrComplexPlaces K = k
⊢ nrComplexPlaces K = φ ↑n / 2