n : ℕ
h : n ≠ 0
⊢ map (Int.castRingHom ℤ)
      (Exists.choose
        (_ : ∃ P, map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ degree P = degree (cyclotomic' n ℂ) ∧ Monic P)) =
    Exists.choose (_ : ∃ P, map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ degree P = degree (cyclotomic' n ℂ) ∧ Monic P)
n : ℕ
h : n ≠ 0
⊢ cyclotomic n ℤ =
    Exists.choose (_ : ∃ P, map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ degree P = degree (cyclotomic' n ℂ) ∧ Monic P)
simp only [cyclotomic, h, dif_neg, not_false_iff]
case a
n : ℕ
h : n ≠ 0
i : ℕ
⊢ coeff
      (map (Int.castRingHom ℤ)
        (Exists.choose
          (_ : ∃ P, map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ degree P = degree (cyclotomic' n ℂ) ∧ Monic P)))
      i =
    coeff
      (Exists.choose
        (_ : ∃ P, map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ degree P = degree (cyclotomic' n ℂ) ∧ Monic P))
      i
n : ℕ
h : n ≠ 0
⊢ map (Int.castRingHom ℤ)
      (Exists.choose
        (_ : ∃ P, map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ degree P = degree (cyclotomic' n ℂ) ∧ Monic P)) =
    Exists.choose (_ : ∃ P, map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ degree P = degree (cyclotomic' n ℂ) ∧ Monic P)
ext i
no goals
case a
n : ℕ
h : n ≠ 0
i : ℕ
⊢ coeff
      (map (Int.castRingHom ℤ)
        (Exists.choose
          (_ : ∃ P, map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ degree P = degree (cyclotomic' n ℂ) ∧ Monic P)))
      i =
    coeff
      (Exists.choose
        (_ : ∃ P, map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ degree P = degree (cyclotomic' n ℂ) ∧ Monic P))
      i
simp only [coeff_map, Int.cast_id, eq_intCast]