awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card (↑(p.rootSet ℝ) : Type) + 1 ≤ Fintype.card (↑(p.rootSet ℂ) : Type)
p_roots2 : Fintype.card (↑(p.rootSet ℂ) : Type) ≤ Fintype.card (↑(p.rootSet ℝ) : Type) + 3
n : ℕ :=
  Finset.card (α := (↑(p.rootSet ℂ) : Type))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
rw :
  Eq (α := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        (HPow.hPow (α := p.Gal) (β := ℕ)
          ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal) 2) :
      Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (1 : Equiv.Perm (↑(p.rootSet ℂ) : Type))
rw₁ :
  Eq (α := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal)
            (HPow.hPow (α := Gal(ℂ/ℚ)) (β := ℕ) (AlgEquiv.restrictScalars ℚ conjAe) 2) :
          p.Gal) :
      Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (1 : Equiv.Perm (↑(p.rootSet ℂ) : Type))
rw₂ :
  Eq (α := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) 1) :
      Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (1 : Equiv.Perm (↑(p.rootSet ℂ) : Type))
rw₃ :
  Eq (α := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) 1 : Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (1 : Equiv.Perm (↑(p.rootSet ℂ) : Type))
rw₄ rw₅ : Eq (α := Equiv.Perm (↑(p.rootSet ℂ) : Type)) 1 1
⊢ HPow.hPow (α := Equiv.Perm (↑(p.rootSet ℂ) : Type)) (β := ℕ)
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
          ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal) :
        Equiv.Perm (↑(p.rootSet ℂ) : Type))
      2 =
    1

Tactic:
rw [← map_pow, ← map_pow,
          show AlgEquiv.restrictScalars ℚ Complex.conjAe ^ 2 = 1 from
            AlgEquiv.ext Complex.conj_conj,
          map_one, map_one]

Premises used: map_pow, map_one, AlgEquiv.ext, Complex.conj_conj
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card (↑(p.rootSet ℝ) : Type) + 1 ≤ Fintype.card (↑(p.rootSet ℂ) : Type)
p_roots2 : Fintype.card (↑(p.rootSet ℂ) : Type) ≤ Fintype.card (↑(p.rootSet ℝ) : Type) + 3
n : ℕ :=
  Finset.card (α := (↑(p.rootSet ℂ) : Type))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
⊢ 2 ∣ n

Tactic:
have hn : 2 ∣ n :=
    Equiv.Perm.two_dvd_card_support
      (by
         rw [← map_pow, ← map_pow,
          show AlgEquiv.restrictScalars ℚ Complex.conjAe ^ 2 = 1 from
            AlgEquiv.ext Complex.conj_conj,
          map_one, map_one])
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card (↑(p.rootSet ℝ) : Type) + 1 ≤ Fintype.card (↑(p.rootSet ℂ) : Type)
p_roots2 : Fintype.card (↑(p.rootSet ℂ) : Type) ≤ Fintype.card (↑(p.rootSet ℝ) : Type) + 3
n : ℕ :=
  Finset.card (α := (↑(p.rootSet ℂ) : Type))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
hn : 2 ∣ n
⊢ (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card +
      Finset.card (α := (↑(p.rootSet ℂ) : Type))
        (Equiv.Perm.support
          ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
            ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))

Tactic:
have key := card_complex_roots_eq_card_real_add_card_not_gal_inv p
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card (↑(p.rootSet ℝ) : Type) + 1 ≤ Fintype.card (↑(p.rootSet ℂ) : Type)
p_roots2 : Fintype.card (↑(p.rootSet ℂ) : Type) ≤ Fintype.card (↑(p.rootSet ℝ) : Type) + 3
n : ℕ :=
  Finset.card (α := (↑(p.rootSet ℂ) : Type))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
hn : 2 ∣ n
key :
  (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card +
      Finset.card (α := (↑(p.rootSet ℂ) : Type))
        (Equiv.Perm.support
          ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
            ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
⊢ Fintype.card (↑(p.rootSet ℂ) : Type) =
    Fintype.card (↑(p.rootSet ℝ) : Type) +
      Finset.card (α := (↑(p.rootSet ℂ) : Type))
        (Equiv.Perm.support
          ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
            ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))

Tactic:
simp_rw [Set.toFinset_card] at key

Premises used: Set.toFinset_card
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card (↑(p.rootSet ℝ) : Type) + 1 ≤ Fintype.card (↑(p.rootSet ℂ) : Type)
p_roots2 : Fintype.card (↑(p.rootSet ℂ) : Type) ≤ Fintype.card (↑(p.rootSet ℝ) : Type) + 3
n : ℕ :=
  Finset.card (α := (↑(p.rootSet ℂ) : Type))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
hn : 2 ∣ n
key :
  Fintype.card (↑(p.rootSet ℂ) : Type) =
    Fintype.card (↑(p.rootSet ℝ) : Type) +
      Finset.card (α := (↑(p.rootSet ℂ) : Type))
        (Equiv.Perm.support
          ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
            ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
⊢ Fintype.card (↑(p.rootSet ℂ) : Type) = Fintype.card (↑(p.rootSet ℝ) : Type) + 2

Tactic:
lia
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
z : ℂ
h0 : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz : z.im ≠ 0
H :
  IsCoprime (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]))
    (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X]))
H1 :
  HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]) ∣
    map (algebraMap ℝ ℂ) p
H2 : HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X]) ∣ map (algebraMap ℝ ℂ) p
⊢ HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]) *
      HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X]) ∣
    map (algebraMap ℝ ℂ) p

Tactic:
apply IsCoprime.mul_dvd

Premises used: IsCoprime.mul_dvd
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
z : ℂ
h0 : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz : z.im ≠ 0
⊢ IsCoprime (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]))
    (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X]))

Tactic:
isCoprime_X_sub_C_of_isUnit_sub <| .mk0 _ <| sub_ne_zero.2 <| mt conj_eq_iff_im.1 hz

Premises used: Iff.mpr, sub_ne_zero, mt, IsUnit.mk0, Iff.mp, Complex.conj_eq_iff_im, Polynomial.isCoprime_X_sub_C_of_isUnit_sub
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
z : ℂ
h0 : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz : z.im ≠ 0
⊢ IsCoprime (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]))
    (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X]))

Tactic:
exact isCoprime_X_sub_C_of_isUnit_sub <| .mk0 _ <| sub_ne_zero.2 <| mt conj_eq_iff_im.1 hz

Premises used: Iff.mpr, sub_ne_zero, mt, Iff.mp, Complex.conj_eq_iff_im, Polynomial.isCoprime_X_sub_C_of_isUnit_sub
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
z : ℂ
h0 : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz : z.im ≠ 0
⊢ HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X]) ∣ map (algebraMap ℝ ℂ) p

Tactic:
simpa [dvd_iff_isRoot]

Premises used: Polynomial.dvd_iff_isRoot
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
z : ℂ
h0 : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz : z.im ≠ 0
rw :
  map (algebraMap ℝ ℂ)
      (HAdd.hAdd (β := ℝ[X])
        (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 -
          HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) (2 * z.re) : ℝ[X]) X)
        ((C : (a : ℝ) → ℝ[X]) (HPow.hPow (β := ℕ) ‖z‖ 2) : ℝ[X])) ∣
    map (algebraMap ℝ ℂ) p
⊢ HAdd.hAdd (β := ℝ[X])
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 -
        HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) (2 * z.re) : ℝ[X]) X)
      ((C : (a : ℝ) → ℝ[X]) (HPow.hPow (β := ℕ) ‖z‖ 2) : ℝ[X]) ∣
    p

Tactic:
rw [← map_dvd_map' (algebraMap ℝ ℂ)]

Premises used: Real, Algebra.algebraMap, Complex, Polynomial.map_dvd_map'
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
z : ℂ
h0 : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz : z.im ≠ 0
⊢ HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]) *
      HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X]) ∣
    map (algebraMap ℝ ℂ) p

Tactic:
p.mul_star_dvd_of_aeval_eq_zero_im_ne_zero h0 hz

Premises used: Polynomial.mul_star_dvd_of_aeval_eq_zero_im_ne_zero
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
z : ℂ
h0 : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz : z.im ≠ 0
h :
  map (algebraMap ℝ ℂ)
      (HAdd.hAdd (β := ℝ[X])
        (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 -
          HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) (2 * z.re) : ℝ[X]) X)
        ((C : (a : ℝ) → ℝ[X]) (HPow.hPow (β := ℕ) ‖z‖ 2) : ℝ[X])) =
    HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]) *
      HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])
⊢ map (algebraMap ℝ ℂ)
      (HAdd.hAdd (β := ℝ[X])
        (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 -
          HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) (2 * z.re) : ℝ[X]) X)
        ((C : (a : ℝ) → ℝ[X]) (HPow.hPow (β := ℕ) ‖z‖ 2) : ℝ[X])) ∣
    map (algebraMap ℝ ℂ) p

Tactic:
convert! p.mul_star_dvd_of_aeval_eq_zero_im_ne_zero h0 hz

Premises used: Polynomial.mul_star_dvd_of_aeval_eq_zero_im_ne_zero
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
z : ℂ
h0 : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz : z.im ≠ 0
⊢ map (algebraMap ℝ ℂ)
      (HAdd.hAdd (β := ℝ[X])
        (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 -
          HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) (2 * z.re) : ℝ[X]) X)
        ((C : (a : ℝ) → ℝ[X]) (HPow.hPow (β := ℕ) ‖z‖ 2) : ℝ[X])) =
    HAdd.hAdd (β := ℂ[X])
      (HPow.hPow (α := ℂ[X]) (β := ℕ) X 2 -
        HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (↑(2 * z.re) : ℂ) : ℂ[X]) X)
      ((C : (a : ℂ) → ℂ[X]) (HPow.hPow (β := ℕ) (↑‖z‖ : ℂ) 2) : ℂ[X])

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
z : ℂ
h0 : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz : z.im ≠ 0
rw :
  HPow.hPow (α := ℂ[X]) (β := ℕ) X 2 -
        HAdd.hAdd (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])
            ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]) *
          X +
      HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])
        ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]) =
    HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]) *
      HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])
⊢ HAdd.hAdd (β := ℂ[X])
      (HPow.hPow (α := ℂ[X]) (β := ℕ) X 2 -
        HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (↑(2 * z.re) : ℂ) : ℂ[X]) X)
      ((C : (a : ℂ) → ℂ[X]) (HPow.hPow (β := ℕ) (↑‖z‖ : ℂ) 2) : ℂ[X]) =
    HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]) *
      HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])

Tactic:
rw [← add_conj, map_add, ← mul_conj', map_mul]

Premises used: Complex.mul_conj', map_add, Complex.add_conj, map_mul
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
z : ℂ
h0 : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz : z.im ≠ 0
⊢ HPow.hPow (α := ℂ[X]) (β := ℕ) X 2 -
        HAdd.hAdd (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])
            ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]) *
          X +
      HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])
        ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]) =
    HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]) *
      HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
z : ℂ
h0 : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz : z.im ≠ 0
map :
  Polynomial.map (algebraMap ℝ ℂ)
      (HAdd.hAdd (β := ℝ[X])
        (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 -
          HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) (2 * z.re) : ℝ[X]) X)
        ((C : (a : ℝ) → ℝ[X]) (HPow.hPow (β := ℕ) ‖z‖ 2) : ℝ[X])) =
    HAdd.hAdd (β := ℂ[X])
      (HPow.hPow (α := ℂ[X]) (β := ℕ) X 2 -
        HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (↑(2 * z.re) : ℂ) : ℂ[X]) X)
      ((C : (a : ℂ) → ℂ[X]) (HPow.hPow (β := ℕ) (↑‖z‖ : ℂ) 2) : ℂ[X])
map₁ :
  HAdd.hAdd (β := ℂ[X])
      (HPow.hPow (α := ℂ[X]) (β := ℕ) X 2 -
        HMul.hMul (α := ℂ[X]) (β := ℂ[X]) ((C : (a : ℂ) → ℂ[X]) (↑(2 * z.re) : ℂ) : ℂ[X]) X)
      ((C : (a : ℂ) → ℂ[X]) (HPow.hPow (β := ℕ) (↑‖z‖ : ℂ) 2) : ℂ[X]) =
    HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]) *
      HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])
⊢ Polynomial.map (algebraMap ℝ ℂ)
      (HAdd.hAdd (β := ℝ[X])
        (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 -
          HMul.hMul (α := ℝ[X]) (β := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) (2 * z.re) : ℝ[X]) X)
        ((C : (a : ℝ) → ℝ[X]) (HPow.hPow (β := ℕ) ‖z‖ 2) : ℝ[X])) =
    HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]) *
      HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])

Tactic:
calc
    map (algebraMap ℝ ℂ) (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2))
    _ = X ^ 2 - C (↑(2 * z.re) : ℂ) * X + C (‖z‖ ^ 2 : ℂ) := by simp
    _ = (X - C (conj z)) * (X - C z) := by
      rw [← add_conj, map_add, ← mul_conj', map_mul]
      ring

Premises used: Norm.norm, Polynomial.C, Real, HMul.hMul, Algebra.algebraMap, HSub.hSub, Complex.ofReal, Complex.re, HPow.hPow, HAdd.hAdd, Polynomial.map, Complex, starRingEnd, OfNat.ofNat, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
hp : Irreducible p
⊢ ∃ (z : ℂ), Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)

Tactic:
IsAlgClosed.exists_aeval_eq_zero _ p (degree_pos_of_irreducible hp).ne'

Premises used: LT.lt.ne', Polynomial.degree_pos_of_irreducible, IsAlgClosed.exists_aeval_eq_zero
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
hp : Irreducible p
obtain : ∀ (z : ℂ) (hz : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)), p.natDegree ≤ 2
⊢ p.natDegree ≤ 2

Tactic:
obtain ⟨z, hz⟩ : ∃ z : ℂ, aeval z p = 0 :=
    IsAlgClosed.exists_aeval_eq_zero _ p (degree_pos_of_irreducible hp).ne'

Premises used: LT.lt.ne', Polynomial.degree_pos_of_irreducible, IsAlgClosed.exists_aeval_eq_zero
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
hp : Irreducible p
z : ℂ
hz : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
rw : p.natDegree ≤ Module.finrank ℝ ℂ
⊢ p.natDegree ≤ 2

Tactic:
rw [← finrank_real_complex]

Premises used: Complex.finrank_real_complex
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
hp : Irreducible p
z : ℂ
hz : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
suffices : p.natDegree = natDegree (minpoly ℝ z)
⊢ p.natDegree ≤ Module.finrank ℝ ℂ

Tactic:
suffices p.natDegree = (minpoly ℝ z).natDegree from this ▸ minpoly.natDegree_le (A := ℝ) z
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
hp : Irreducible p
z : ℂ
hz : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
⊢ Ne (α := ℝ[X]) ((C : (a : ℝ) → ℝ[X]) p.leadingCoeff⁻¹ : ℝ[X]) (0 : ℝ[X])

Tactic:
simpa using hp.ne_zero

Premises used: Irreducible.ne_zero
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
hp : Irreducible p
z : ℂ
hz : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
rw : p.natDegree = (HMul.hMul (β := ℝ[X]) p ((C : (a : ℝ) → ℝ[X]) p.leadingCoeff⁻¹ : ℝ[X])).natDegree
rw₁ : p.natDegree = p.natDegree + natDegree (R := ℝ) ((C : (a : ℝ) → ℝ[X]) p.leadingCoeff⁻¹)
rw₂ : p.natDegree = p.natDegree + 0
rw₃ rw₄ : p.natDegree = p.natDegree
⊢ p.natDegree = natDegree (minpoly ℝ z)

Tactic:
rw [← minpoly.eq_of_irreducible hp hz, natDegree_mul hp.ne_zero (by simpa using hp.ne_zero),
    natDegree_C, add_zero]

Premises used: minpoly.eq_of_irreducible, Polynomial.natDegree_mul, Polynomial.natDegree_C, Irreducible.ne_zero, add_zero
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℝ[X]
hp : Irreducible p
⊢ p.degree ≤ 2

Tactic:
natDegree_le_iff_degree_le.1 hp.natDegree_le_two

Premises used: Irreducible.natDegree_le_two, Iff.mp, Polynomial.natDegree_le_iff_degree_le
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
z w : ℂ
simp :
  0 ≤ if eval z P = 0 then if w = z then 1 else 0 w else (↑(rootMultiplicity w P) : ℝ) / HPow.hPow (β := ℕ) ‖z - w‖ 2
⊢ 0 ≤ P.derivRootWeight z w

Tactic:
simp only [derivRootWeight, Pi.single, Function.update_apply]

Premises used: Function.update_apply, Pi.single, Polynomial.derivRootWeight
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
z w : ℂ
pos : eval z P = 0 → w = z → LE.le (α := ℝ) 0 1
neg : eval z P = 0 → ¬w = z → LE.le (α := ℝ) 0 (0 w)
neg₁ : ¬eval z P = 0 → 0 ≤ (↑(rootMultiplicity w P) : ℝ) / HPow.hPow (β := ℕ) ‖z - w‖ 2
⊢ 0 ≤ if eval z P = 0 then if w = z then 1 else 0 w else (↑(rootMultiplicity w P) : ℝ) / HPow.hPow (β := ℕ) ‖z - w‖ 2

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
z w : ℂ
h : eval z P = 0
h_1 : w = z
⊢ LE.le (α := ℝ) 0 1

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
z w : ℂ
h : eval z P = 0
h_1 : w = z
⊢ LE.le (α := ℝ) 0 1

Tactic:
first | positivity | simp
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
z w : ℂ
h : eval z P = 0
h_1 : ¬w = z
⊢ LE.le (α := ℝ) 0 (0 w)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
z w : ℂ
h : eval z P = 0
h_1 : ¬w = z
⊢ LE.le (α := ℝ) 0 (0 w)

Tactic:
first | positivity | simp
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
z w : ℂ
h : ¬eval z P = 0
⊢ 0 ≤ (↑(rootMultiplicity w P) : ℝ) / HPow.hPow (β := ℕ) ‖z - w‖ 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
z w : ℂ
h : ¬eval z P = 0
⊢ 0 ≤ (↑(rootMultiplicity w P) : ℝ) / HPow.hPow (β := ℕ) ‖z - w‖ 2

Tactic:
first | positivity | simp
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
z : ℂ
hP : 0 < degree (R := ℂ) 0
⊢ False

Tactic:
simp at hP
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
⊢ P ≠ 0

Tactic:
have hP₀ : P ≠ 0 := by rintro rfl; simp at hP
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
pos : ∀ (hPz : eval z P = 0), LT.lt (α := ℝ) 0 (∑ w ∈ P.roots.toFinset, P.derivRootWeight z w)
neg : ∀ (hPz : ¬eval z P = 0), LT.lt (α := ℝ) 0 (∑ w ∈ P.roots.toFinset, P.derivRootWeight z w)
⊢ LT.lt (α := ℝ) 0 (∑ w ∈ P.roots.toFinset, P.derivRootWeight z w)

Tactic:
by_cases hPz : P.eval z = 0

Premises used: Polynomial.eval
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : eval z P = 0
⊢ LT.lt (α := ℝ) 0 (∑ w ∈ P.roots.toFinset, P.derivRootWeight z w)

Tactic:
simp [derivRootWeight, hPz, hP₀]

Premises used: Polynomial.derivRootWeight
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
neg : LT.lt (α := ℝ) 0 (∑ x ∈ P.roots.toFinset, (↑(rootMultiplicity x P) : ℝ) / HPow.hPow (β := ℕ) ‖z - x‖ 2)
⊢ LT.lt (α := ℝ) 0 (∑ w ∈ P.roots.toFinset, P.derivRootWeight z w)

Tactic:
simp only [derivRootWeight, if_neg hPz]

Premises used: if_neg, Polynomial.derivRootWeight
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
neg : ∀ i ∈ P.roots.toFinset, 0 < (↑(rootMultiplicity i P) : ℝ) / HPow.hPow (β := ℕ) ‖z - i‖ 2
neg₁ : P.roots.toFinset.Nonempty
⊢ LT.lt (α := ℝ) 0 (∑ x ∈ P.roots.toFinset, (↑(rootMultiplicity x P) : ℝ) / HPow.hPow (β := ℕ) ‖z - x‖ 2)

Tactic:
apply Finset.sum_pos

Premises used: Finset.sum_pos
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
w : ℂ
hw : w ∈ P.roots.toFinset
⊢ LT.lt (α := ℝ) 0 (↑(rootMultiplicity w P) : ℝ)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
w : ℂ
hw : w ∈ P.roots.toFinset
neg : 0 < HPow.hPow (β := ℕ) ‖z - w‖ 2
⊢ 0 < (↑(rootMultiplicity w P) : ℝ) / HPow.hPow (β := ℕ) ‖z - w‖ 2

Tactic:
apply div_pos (by simp_all)

Premises used: div_pos
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
w : ℂ
hw : w ∈ P.roots.toFinset
this : z ≠ w
⊢ 0 < HPow.hPow (β := ℕ) ‖z - w‖ 2

Tactic:
simpa [sq_pos_iff, sub_eq_zero]

Premises used: sub_eq_zero, sq_pos_iff
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
w : ℂ
hw : w ∈ P.roots.toFinset
neg : z ≠ w
⊢ 0 < HPow.hPow (β := ℕ) ‖z - w‖ 2

Tactic:
suffices z ≠ w by simpa [sq_pos_iff, sub_eq_zero]
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
hw : z ∈ P.roots.toFinset
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
neg : P.roots ≠ 0
⊢ P.roots.toFinset.Nonempty

Tactic:
rw [Multiset.toFinset_nonempty]

Premises used: Multiset.toFinset_nonempty
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
neg : P.natDegree ≠ 0
⊢ P.roots ≠ 0

Tactic:
apply Splits.roots_ne_zero (IsAlgClosed.splits _)

Premises used: Polynomial.Splits.roots_ne_zero, IsAlgClosed.splits
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
neg : 0 < P.natDegree
neg₁ neg₂ neg₃ neg₄ : 0 < P.degree
⊢ P.natDegree ≠ 0

Tactic:
rwa [← pos_iff_ne_zero, natDegree_pos_iff_degree_pos]

Premises used: Polynomial.natDegree_pos_iff_degree_pos, pos_iff_ne_zero
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z ((derivative : (a : ℂ[X]) → ℂ[X]) P) = 0
set :
  let weight := P.derivRootWeight z;
  z = P.roots.toFinset.centerMass weight id
⊢ z = P.roots.toFinset.centerMass (P.derivRootWeight z) id

Tactic:
set weight : ℂ → ℝ := P.derivRootWeight z

Premises used: Polynomial.derivRootWeight