awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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))
⊢ 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
have rw₄ : Eq (α := Equiv.Perm (↑(p.rootSet ℂ) : Type)) 1 1
Tactic: rw [← map_pow, ← map_pow,
          show AlgEquiv.restrictScalars ℚ Complex.conjAe ^ 2 = 1 from
            AlgEquiv.ext Complex.conj_conj,
          map_one, map_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (hypothesis)
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)))
⊢ Fintype.card (↑(p.rootSet ℂ) : Type) = Fintype.card (↑(p.rootSet ℝ) : Type) + 2
have hn : 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])
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (hypothesis)
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
⊢ Fintype.card (↑(p.rootSet ℂ) : Type) = Fintype.card (↑(p.rootSet ℝ) : Type) + 2
have 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)))
Tactic: have key := card_complex_roots_eq_card_real_add_card_not_gal_inv p
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (hypothesis)
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) + 2
have 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)))
Tactic: simp_rw [Set.toFinset_card] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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
have H : IsCoprime (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]))
  (HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X]))
Tactic: apply IsCoprime.mul_dvd
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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]))
⊢ 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
have H1 : HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]) ∣
  map (algebraMap ℝ ℂ) p
Tactic: apply IsCoprime.mul_dvd
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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
⊢ 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
have H2 : HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X]) ∣ map (algebraMap ℝ ℂ) p
Tactic: apply IsCoprime.mul_dvd
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℝ[X]
z : ℂ
h0 : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz : z.im ≠ 0
⊢ 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
have 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
Tactic: rw [← map_dvd_map' (algebraMap ℝ ℂ)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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])) ∣
    map (algebraMap ℝ ℂ) p
have 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])
Tactic: convert! p.mul_star_dvd_of_aeval_eq_zero_im_ne_zero h0 hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℝ[X]
z : ℂ
h0 : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz : z.im ≠ 0
⊢ 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])
have 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])
Tactic: rw [← add_conj, map_add, ← mul_conj', map_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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])) =
    HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) : ℂ[X]) *
      HSub.hSub (α := ℂ[X]) (β := ℂ[X]) X ((C : (a : ℂ) → ℂ[X]) z : ℂ[X])
have map : 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: 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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])
⊢ 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])
have 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])
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℝ[X]
hp : Irreducible p
⊢ p.natDegree ≤ 2
have obtain : ∀ (z : ℂ) (hz : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)), p.natDegree ≤ 2
Tactic: obtain ⟨z, hz⟩ : ∃ z : ℂ, aeval z p = 0 :=
    IsAlgClosed.exists_aeval_eq_zero _ p (degree_pos_of_irreducible hp).ne'
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℝ[X]
hp : Irreducible p
z : ℂ
hz : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
⊢ p.natDegree ≤ 2
have rw : p.natDegree ≤ Module.finrank ℝ ℂ
Tactic: rw [← finrank_real_complex]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℝ[X]
hp : Irreducible p
z : ℂ
hz : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
⊢ p.natDegree ≤ Module.finrank ℝ ℂ
have suffices : p.natDegree = natDegree (minpoly ℝ z)
Tactic: suffices p.natDegree = (minpoly ℝ z).natDegree from this ▸ minpoly.natDegree_le (A := ℝ) z
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℝ[X]
hp : Irreducible p
z : ℂ
hz : Eq (α := ℂ) ((aeval z : (a : ℝ[X]) → ℂ) p : ℂ) (0 : ℂ)
⊢ p.natDegree = natDegree (minpoly ℝ z)
have rw : p.natDegree = (HMul.hMul (β := ℝ[X]) p ((C : (a : ℝ) → ℝ[X]) p.leadingCoeff⁻¹ : ℝ[X])).natDegree
Tactic: rw [← minpoly.eq_of_irreducible hp hz, natDegree_mul hp.ne_zero (by simpa using hp.ne_zero),
    natDegree_C, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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
⊢ p.natDegree = natDegree (minpoly ℝ z)
have rw₁ : p.natDegree = p.natDegree + natDegree (R := ℝ) ((C : (a : ℝ) → ℝ[X]) p.leadingCoeff⁻¹)
Tactic: rw [← minpoly.eq_of_irreducible hp hz, natDegree_mul hp.ne_zero (by simpa using hp.ne_zero),
    natDegree_C, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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⁻¹)
⊢ p.natDegree = natDegree (minpoly ℝ z)
have rw₂ : p.natDegree = p.natDegree + 0
Tactic: rw [← minpoly.eq_of_irreducible hp hz, natDegree_mul hp.ne_zero (by simpa using hp.ne_zero),
    natDegree_C, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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
⊢ p.natDegree = natDegree (minpoly ℝ z)
have rw₃ : p.natDegree = p.natDegree
Tactic: rw [← minpoly.eq_of_irreducible hp hz, natDegree_mul hp.ne_zero (by simpa using hp.ne_zero),
    natDegree_C, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (goal)
Goal:
P : ℂ[X]
z w : ℂ
⊢ 0 ≤ P.derivRootWeight z w
have 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
Tactic: simp only [derivRootWeight, Pi.single, Function.update_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (goal)
Goal:
P : ℂ[X]
z w : ℂ
⊢ 0 ≤ if eval z P = 0 then if w = z then 1 else 0 w else (↑(rootMultiplicity w P) : ℝ) / HPow.hPow (β := ℕ) ‖z - w‖ 2
have pos : eval z P = 0 → w = z → LE.le (α := ℝ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (goal)
Goal:
P : ℂ[X]
z w : ℂ
pos : eval z P = 0 → w = z → LE.le (α := ℝ) 0 1
⊢ 0 ≤ if eval z P = 0 then if w = z then 1 else 0 w else (↑(rootMultiplicity w P) : ℝ) / HPow.hPow (β := ℕ) ‖z - w‖ 2
have neg : eval z P = 0 → ¬w = z → LE.le (α := ℝ) 0 (0 w)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (goal)
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)
⊢ 0 ≤ if eval z P = 0 then if w = z then 1 else 0 w else (↑(rootMultiplicity w P) : ℝ) / HPow.hPow (β := ℕ) ‖z - w‖ 2
have neg₁ : ¬eval z P = 0 → 0 ≤ (↑(rootMultiplicity w P) : ℝ) / HPow.hPow (β := ℕ) ‖z - w‖ 2
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (hypothesis)
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
⊢ LT.lt (α := ℝ) 0 (∑ w ∈ P.roots.toFinset, P.derivRootWeight z w)
have hP₀ : P ≠ 0
Tactic: have hP₀ : P ≠ 0 := by rintro rfl; simp at hP
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (goal)
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
⊢ LT.lt (α := ℝ) 0 (∑ w ∈ P.roots.toFinset, P.derivRootWeight z w)
have pos : ∀ (hPz : eval z P = 0), LT.lt (α := ℝ) 0 (∑ w ∈ P.roots.toFinset, P.derivRootWeight z w)
Tactic: by_cases hPz : P.eval z = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (goal)
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)
⊢ LT.lt (α := ℝ) 0 (∑ w ∈ P.roots.toFinset, P.derivRootWeight z w)
have neg : ∀ (hPz : ¬eval z P = 0), LT.lt (α := ℝ) 0 (∑ w ∈ P.roots.toFinset, P.derivRootWeight z w)
Tactic: by_cases hPz : P.eval z = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (goal)
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)
have neg : LT.lt (α := ℝ) 0 (∑ x ∈ P.roots.toFinset, (↑(rootMultiplicity x P) : ℝ) / HPow.hPow (β := ℕ) ‖z - x‖ 2)
Tactic: simp only [derivRootWeight, if_neg hPz]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (goal)
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ LT.lt (α := ℝ) 0 (∑ x ∈ P.roots.toFinset, (↑(rootMultiplicity x P) : ℝ) / HPow.hPow (β := ℕ) ‖z - x‖ 2)
have neg : ∀ i ∈ P.roots.toFinset, 0 < (↑(rootMultiplicity i P) : ℝ) / HPow.hPow (β := ℕ) ‖z - i‖ 2
Tactic: apply Finset.sum_pos
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (goal)
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
⊢ LT.lt (α := ℝ) 0 (∑ x ∈ P.roots.toFinset, (↑(rootMultiplicity x P) : ℝ) / HPow.hPow (β := ℕ) ‖z - x‖ 2)
have neg₁ : P.roots.toFinset.Nonempty
Tactic: apply Finset.sum_pos
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (goal)
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
w : ℂ
hw : w ∈ P.roots.toFinset
⊢ 0 < (↑(rootMultiplicity w P) : ℝ) / HPow.hPow (β := ℕ) ‖z - w‖ 2
have neg : 0 < HPow.hPow (β := ℕ) ‖z - w‖ 2
Tactic: apply div_pos (by simp_all)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (goal)
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
w : ℂ
hw : w ∈ P.roots.toFinset
⊢ 0 < HPow.hPow (β := ℕ) ‖z - w‖ 2
have neg : z ≠ w
Tactic: suffices z ≠ w by simpa [sq_pos_iff, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (goal)
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ P.roots.toFinset.Nonempty
have neg : P.roots ≠ 0
Tactic: rw [Multiset.toFinset_nonempty]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (goal)
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ P.roots ≠ 0
have neg : P.natDegree ≠ 0
Tactic: apply Splits.roots_ne_zero (IsAlgClosed.splits _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (goal)
Goal:
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ P.natDegree ≠ 0
have neg : 0 < P.natDegree
Tactic: rwa [← pos_iff_ne_zero, natDegree_pos_iff_degree_pos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (goal)
Goal:
P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z ((derivative : (a : ℂ[X]) → ℂ[X]) P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
this : Eq (α := ℂ) (∑ x ∈ s, weight x • (z - x)) 0
⊢ z = s.centerMass weight fun (x : ℂ) ↦ z
have ha : Ne (α := ℝ) (∑ i ∈ s, weight i) 0
Tactic: rw [Finset.centerMass, ← Finset.sum_smul, inv_smul_smul₀]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (goal)
Goal:
P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z ((derivative : (a : ℂ[X]) → ℂ[X]) P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
this : Eq (α := ℂ) (∑ x ∈ s, weight x • (z - x)) 0
⊢ z = s.centerMass weight id
have z₁ : z = s.centerMass weight fun (x : ℂ) ↦ z
Tactic: calc
    z = s.centerMass weight fun _ ↦ z := by
      rw [Finset.centerMass, ← Finset.sum_smul, inv_smul_smul₀]
      exact (sum_derivRootWeight_pos hP z).ne'
    _ = s.centerMass weight (z - ·) + s.centerMass weight id := by
      simp only [Finset.centerMass, ← smul_add, ← Finset.sum_add_distrib, id, sub_add_cancel]
    _ = s.centerMass weight id := by
      simp only [add_eq_right, Finset.centerMass, this, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.GaussLucas (goal)
Goal:
P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z ((derivative : (a : ℂ[X]) → ℂ[X]) P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
this : Eq (α := ℂ) (∑ x ∈ s, weight x • (z - x)) 0
z₁ : z = s.centerMass weight fun (x : ℂ) ↦ z
⊢ z = s.centerMass weight id
have z₂ : (s.centerMass weight fun (x : ℂ) ↦ z) = (s.centerMass weight fun (x : ℂ) ↦ z - x) + s.centerMass weight id
Tactic: calc
    z = s.centerMass weight fun _ ↦ z := by
      rw [Finset.centerMass, ← Finset.sum_smul, inv_smul_smul₀]
      exact (sum_derivRootWeight_pos hP z).ne'
    _ = s.centerMass weight (z - ·) + s.centerMass weight id := by
      simp only [Finset.centerMass, ← smul_add, ← Finset.sum_add_distrib, id, sub_add_cancel]
    _ = s.centerMass weight id := by
      simp only [add_eq_right, Finset.centerMass, this, smul_zero]