awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z ((derivative : (a : ℂ[X]) → ℂ[X]) P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
set :
  let s := P.roots.toFinset;
  z = s.centerMass weight id
⊢ z = P.roots.toFinset.centerMass weight id

Tactic:
set s := P.roots.toFinset

Premises used: Multiset.toFinset, Polynomial.roots
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
ha : Ne (α := ℝ) (∑ i ∈ s, weight i) 0
⊢ z = s.centerMass weight fun (x : ℂ) ↦ z

Tactic:
rw [Finset.centerMass, ← Finset.sum_smul, inv_smul_smul₀]

Premises used: Finset.sum_smul, inv_smul_smul₀, Finset.centerMass
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
⊢ Ne (α := ℝ) (∑ i ∈ s, weight i) 0

Tactic:
(sum_derivRootWeight_pos hP z).ne'

Premises used: LT.lt.ne', Polynomial.sum_derivRootWeight_pos
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
⊢ Ne (α := ℝ) (∑ i ∈ s, weight i) 0

Tactic:
exact (sum_derivRootWeight_pos hP z).ne'

Premises used: LT.lt.ne', Polynomial.sum_derivRootWeight_pos
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
⊢ (s.centerMass weight fun (x : ℂ) ↦ z) = (s.centerMass weight fun (x : ℂ) ↦ z - x) + s.centerMass weight id

Tactic:
simp only [Finset.centerMass, ← smul_add, ← Finset.sum_add_distrib, id, sub_add_cancel]

Premises used: Finset.sum_add_distrib, id, Finset.centerMass, sub_add_cancel, smul_add
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
⊢ (s.centerMass weight fun (x : ℂ) ↦ z - x) + s.centerMass weight id = s.centerMass weight id

Tactic:
simp only [add_eq_right, Finset.centerMass, this, smul_zero]

Premises used: smul_zero, add_eq_right, Finset.centerMass
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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 fun (x : ℂ) ↦ z) = (s.centerMass weight fun (x : ℂ) ↦ z - x) + s.centerMass weight id
z₃ : (s.centerMass weight fun (x : ℂ) ↦ z - x) + s.centerMass weight id = s.centerMass weight id
⊢ z = 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]

Premises used: HSub.hSub, id, Finset.centerMass
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
suffices : Eq (α := ℂ) (∑ x ∈ s, weight x • (z - x)) 0
⊢ z = s.centerMass weight id

Tactic:
suffices ∑ x ∈ s, weight x • (z - x) = 0 by 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]
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
pos : ∀ (hzP : eval z P = 0), Eq (α := ℂ) (∑ x ∈ s, weight x • (z - x)) 0
neg : ∀ (hzP : ¬eval z P = 0), Eq (α := ℂ) (∑ x ∈ s, weight x • (z - x)) 0
⊢ Eq (α := ℂ) (∑ x ∈ s, weight x • (z - x)) 0

Tactic:
by_cases hzP : P.eval z = 0

Premises used: Polynomial.eval
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
hzP : eval z P = 0
pos : Eq (α := ℂ) (∑ x ∈ s, HSMul.hSMul (α := ℝ) (Pi.single (M := fun (a : ℂ) ↦ ℝ) z 1 x : ℝ) (z - x)) 0
⊢ Eq (α := ℂ) (∑ x ∈ s, weight x • (z - x)) 0

Tactic:
simp only [weight, derivRootWeight, if_pos hzP]

Premises used: if_pos, Polynomial.derivRootWeight
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
hzP : eval z P = 0
pos : HSMul.hSMul (α := ℝ) (Pi.single (M := fun (a : ℂ) ↦ ℝ) z 1 z : ℝ) (z - z) = 0
pos₁ : ∀ b ∈ s, b ≠ z → HSMul.hSMul (α := ℝ) (Pi.single (M := fun (a : ℂ) ↦ ℝ) z 1 b : ℝ) (z - b) = 0
pos₂ : z ∉ s → HSMul.hSMul (α := ℝ) (Pi.single (M := fun (a : ℂ) ↦ ℝ) z 1 z : ℝ) (z - z) = 0
⊢ Eq (α := ℂ) (∑ x ∈ s, HSMul.hSMul (α := ℝ) (Pi.single (M := fun (a : ℂ) ↦ ℝ) z 1 x : ℝ) (z - x)) 0

Tactic:
rw [Finset.sum_eq_single z]

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
hzP : eval z P = 0
⊢ HSMul.hSMul (α := ℝ) (Pi.single (M := fun (a : ℂ) ↦ ℝ) z 1 z : ℝ) (z - z) = 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
hzP : eval z P = 0
⊢ ∀ b ∈ s, b ≠ z → HSMul.hSMul (α := ℝ) (Pi.single (M := fun (a : ℂ) ↦ ℝ) z 1 b : ℝ) (z - b) = 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
hzP : eval z P = 0
⊢ z ∉ s → HSMul.hSMul (α := ℝ) (Pi.single (M := fun (a : ℂ) ↦ ℝ) z 1 z : ℝ) (z - z) = 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
hzP : ¬eval z P = 0
simp :
  Eq (α := ℂ) (∑ x ∈ s, ((↑(rootMultiplicity x P) : ℝ) / HPow.hPow (β := ℕ) ‖z - x‖ 2) • (z - x))
    (∑ x ∈ s, (starRingEnd ℂ : (a : ℂ) → ℂ) (rootMultiplicity x P • (1 / (z - x))))
⊢ Eq (α := ℂ) (∑ x ∈ s, weight x • (z - x) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) (∑ x ∈ s, rootMultiplicity x P • (1 / (z - x))) : ℂ)

Tactic:
simp only [map_sum, weight, derivRootWeight, if_neg hzP]

Premises used: map_sum, if_neg, Polynomial.derivRootWeight
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
hzP : ¬eval z P = 0
⊢ Eq (α := ℂ) (∑ x ∈ s, ((↑(rootMultiplicity x P) : ℝ) / HPow.hPow (β := ℕ) ‖z - x‖ 2) • (z - x))
    (∑ x ∈ s, (starRingEnd ℂ : (a : ℂ) → ℂ) (rootMultiplicity x P • (1 / (z - x))))

Tactic:
Finset.sum_congr rfl fun x hx ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
hzP : ¬eval z P = 0
refine :
  ∀ (x : ℂ) (hx : x ∈ s),
    ((↑(rootMultiplicity x P) : ℝ) / HPow.hPow (β := ℕ) ‖z - x‖ 2) • (z - x) =
      (starRingEnd ℂ : (a : ℂ) → ℂ) (rootMultiplicity x P • (1 / (z - x)))
⊢ Eq (α := ℂ) (∑ x ∈ s, ((↑(rootMultiplicity x P) : ℝ) / HPow.hPow (β := ℕ) ‖z - x‖ 2) • (z - x))
    (∑ x ∈ s, (starRingEnd ℂ : (a : ℂ) → ℂ) (rootMultiplicity x P • (1 / (z - x))))

Tactic:
refine Finset.sum_congr rfl fun x hx ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
hzP : ¬eval z P = 0
x : ℂ
hx : x ∈ s
rw : z ≠ x
⊢ z - x ≠ 0

Tactic:
rw [sub_ne_zero]

Premises used: sub_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
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
hzP : ¬eval z P = 0
hx : z ∈ s
⊢ False

Tactic:
simp_all [s]
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
hzP : ¬eval z P = 0
x : ℂ
hx : x ∈ s
⊢ z - x ≠ 0

Tactic:
have : z - x ≠ 0 := by
        rw [sub_ne_zero]
        rintro rfl
        simp_all [s]
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
hzP : ¬eval z P = 0
x : ℂ
hx : x ∈ s
this : z - x ≠ 0
⊢ ((↑(rootMultiplicity x P) : ℝ) / HPow.hPow (β := ℕ) ‖z - x‖ 2) • (z - x) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (rootMultiplicity x P • (1 / (z - x)))

Tactic:
simp [← Complex.conj_mul', field]

Premises used: Complex.conj_mul'
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
hzP : ¬eval z P = 0
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (∑ x ∈ s, rootMultiplicity x P • (1 / (z - x))) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) (Multiset.sum (Multiset.map (fun (x : ℂ) ↦ 1 / (z - x)) P.roots)) : ℂ)

Tactic:
simp only [Finset.sum_multiset_map_count, P.count_roots, s]

Premises used: Polynomial.count_roots, Finset.sum_multiset_map_count
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
hzP : ¬eval z P = 0
rw : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (eval z ((derivative : (a : ℂ[X]) → ℂ[X]) P) / eval z P) : ℂ) (0 : ℂ)
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (Multiset.sum (Multiset.map (fun (x : ℂ) ↦ 1 / (z - x)) P.roots)) : ℂ)
    (0 : ℂ)

Tactic:
rw [← (IsAlgClosed.splits _).eval_derivative_div_eval_of_ne_zero hzP]

Premises used: Polynomial.Splits.eval_derivative_div_eval_of_ne_zero, IsAlgClosed.splits
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
hzP : ¬eval z P = 0
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (eval z ((derivative : (a : ℂ[X]) → ℂ[X]) P) / eval z P) : ℂ) (0 : ℂ)

Tactic:
simp [hz]
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
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
hzP : ¬eval z P = 0
x :
  Eq (α := ℂ) (∑ x ∈ s, weight x • (z - x) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) (∑ x ∈ s, rootMultiplicity x P • (1 / (z - x))) : ℂ)
x₁ :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (∑ x ∈ s, rootMultiplicity x P • (1 / (z - x))) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) (Multiset.sum (Multiset.map (fun (x : ℂ) ↦ 1 / (z - x)) P.roots)) : ℂ)
x₂ :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (Multiset.sum (Multiset.map (fun (x : ℂ) ↦ 1 / (z - x)) P.roots)) : ℂ)
    (0 : ℂ)
⊢ Eq (α := ℂ) (∑ x ∈ s, weight x • (z - x)) 0

Tactic:
calc
    ∑ x ∈ s, weight x • (z - x) = conj (∑ x ∈ s, P.rootMultiplicity x • (1 / (z - x))) := by
      simp only [map_sum, weight, derivRootWeight, if_neg hzP]
      refine Finset.sum_congr rfl fun x hx ↦ ?_
      have : z - x ≠ 0 := by
        rw [sub_ne_zero]
        rintro rfl
        simp_all [s]
      simp [← Complex.conj_mul', field]
    _ = conj (P.roots.map fun x ↦ 1 / (z - x)).sum := by
      simp only [Finset.sum_multiset_map_count, P.count_roots, s]
    _ = 0 := by
      rw [← (IsAlgClosed.splits _).eval_derivative_div_eval_of_ne_zero hzP]
      simp [hz]

Premises used: Multiset.sum, Polynomial.roots, Multiset.map, HSub.hSub, HDiv.hDiv, HSMul.hSMul, Polynomial.rootMultiplicity, starRingEnd, OfNat.ofNat, DFunLike.coe, Finset.sum
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : z ∈ rootSet (T := ℂ) ((derivative : (a : ℂ[X]) → ℂ[X]) P) ℂ
⊢ Ne (α := ℂ[X]) ((derivative : (a : ℂ[X]) → ℂ[X]) P : ℂ[X]) (0 : ℂ[X]) ∧
    eval z ((derivative : (a : ℂ[X]) → ℂ[X]) P) = 0

Tactic:
rw [mem_rootSet, coe_aeval_eq_eval] at hz

Premises used: Polynomial.mem_rootSet, Polynomial.coe_aeval_eq_eval
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz :
  Ne (α := ℂ[X]) ((derivative : (a : ℂ[X]) → ℂ[X]) P : ℂ[X]) (0 : ℂ[X]) ∧
    eval z ((derivative : (a : ℂ[X]) → ℂ[X]) P) = 0
rw :
  Membership.mem (γ := Set ℂ) ((convexHull ℝ : (a : Set ℂ) → Set ℂ) (P.rootSet ℂ) : Set ℂ)
    (P.roots.toFinset.centerMass (P.derivRootWeight z) id)
⊢ Membership.mem (γ := Set ℂ) ((convexHull ℝ : (a : Set ℂ) → Set ℂ) (P.rootSet ℂ) : Set ℂ) z

Tactic:
rw [eq_centerMass_of_eval_derivative_eq_zero h₀ hz.2]

Premises used: Polynomial.eq_centerMass_of_eval_derivative_eq_zero, And.right
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz :
  Ne (α := ℂ[X]) ((derivative : (a : ℂ[X]) → ℂ[X]) P : ℂ[X]) (0 : ℂ[X]) ∧
    eval z ((derivative : (a : ℂ[X]) → ℂ[X]) P) = 0
hw₀ : ∀ i ∈ P.roots.toFinset, 0 ≤ P.derivRootWeight z i
hws : LT.lt (α := ℝ) 0 (∑ i ∈ P.roots.toFinset, P.derivRootWeight z i)
hz₁ : ∀ i ∈ P.roots.toFinset, id i ∈ P.rootSet ℂ
⊢ Membership.mem (γ := Set ℂ) ((convexHull ℝ : (a : Set ℂ) → Set ℂ) (P.rootSet ℂ) : Set ℂ)
    (P.roots.toFinset.centerMass (P.derivRootWeight z) id)

Tactic:
apply Finset.centerMass_mem_convexHull

Premises used: Finset.centerMass_mem_convexHull
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz :
  Ne (α := ℂ[X]) ((derivative : (a : ℂ[X]) → ℂ[X]) P : ℂ[X]) (0 : ℂ[X]) ∧
    eval z ((derivative : (a : ℂ[X]) → ℂ[X]) P) = 0
⊢ ∀ i ∈ P.roots.toFinset, 0 ≤ P.derivRootWeight z i

Tactic:
simp [derivRootWeight_nonneg]

Premises used: Polynomial.derivRootWeight_nonneg
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz :
  Ne (α := ℂ[X]) ((derivative : (a : ℂ[X]) → ℂ[X]) P : ℂ[X]) (0 : ℂ[X]) ∧
    eval z ((derivative : (a : ℂ[X]) → ℂ[X]) P) = 0
⊢ LT.lt (α := ℝ) 0 (∑ i ∈ P.roots.toFinset, P.derivRootWeight z i)

Tactic:
apply sum_derivRootWeight_pos h₀

Premises used: Polynomial.sum_derivRootWeight_pos
-- Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas
Goal:
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz :
  Ne (α := ℂ[X]) ((derivative : (a : ℂ[X]) → ℂ[X]) P : ℂ[X]) (0 : ℂ[X]) ∧
    eval z ((derivative : (a : ℂ[X]) → ℂ[X]) P) = 0
⊢ ∀ i ∈ P.roots.toFinset, id i ∈ P.rootSet ℂ

Tactic:
simp [mem_rootSet]

Premises used: Polynomial.mem_rootSet
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
⊢ Irreducible p

Tactic:
hp.irreducible_of_coprime fun q hq hq' => ?_

Premises used: Polynomial.IsUnitTrinomial.irreducible_of_coprime
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
refine : ∀ (q : ℤ[X]) (hq : q ∣ p) (hq' : q ∣ p.mirror), IsUnit q
⊢ Irreducible p

Tactic:
refine hp.irreducible_of_coprime fun q hq hq' => ?_

Premises used: Polynomial.IsUnitTrinomial.irreducible_of_coprime
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
this : ¬0 < q.natDegree
rcases :
  ∀ (p : ℤ[X]) (hp : (q * p).IsUnitTrinomial)
    (h :
      ∀ (z : ℂ),
        ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * p) : ℂ) (0 : ℂ) ∧
            Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * p).mirror : ℂ) (0 : ℂ)))
    (hq' : q ∣ (q * p).mirror), IsUnit q
⊢ IsUnit q

Tactic:
rcases hq with ⟨p, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
Goal:
q : ℤ[X]
this : ¬0 < q.natDegree
p : ℤ[X]
hp : (q * p).IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * p) : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * p).mirror : ℂ) (0 : ℂ))
hq' : q ∣ (q * p).mirror
⊢ IsUnit (q * p).leadingCoeff

Tactic:
replace hp := hp.leadingCoeff_isUnit
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
Goal:
q : ℤ[X]
this : ¬0 < q.natDegree
p : ℤ[X]
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * p) : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * p).mirror : ℂ) (0 : ℂ))
hq' : q ∣ (q * p).mirror
hp : IsUnit (q * p).leadingCoeff
⊢ IsUnit (q.leadingCoeff * p.leadingCoeff)

Tactic:
rw [leadingCoeff_mul] at hp

Premises used: Polynomial.leadingCoeff_mul
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
Goal:
q : ℤ[X]
this : ¬0 < q.natDegree
p : ℤ[X]
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * p) : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * p).mirror : ℂ) (0 : ℂ))
hq' : q ∣ (q * p).mirror
hp : IsUnit (q.leadingCoeff * p.leadingCoeff)
⊢ IsUnit q.leadingCoeff

Tactic:
replace hp := isUnit_of_mul_isUnit_left hp
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
Goal:
q : ℤ[X]
this : ¬0 < q.natDegree
p : ℤ[X]
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * p) : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * p).mirror : ℂ) (0 : ℂ))
hq' : q ∣ (q * p).mirror
hp : IsUnit q.leadingCoeff
rw :
  ∀ (this : q.natDegree = 0) (p : ℤ[X])
    (h :
      ∀ (z : ℂ),
        ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * p) : ℂ) (0 : ℂ) ∧
            Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * p).mirror : ℂ) (0 : ℂ)))
    (hq' : q ∣ (q * p).mirror) (hp : IsUnit q.leadingCoeff), IsUnit q
⊢ IsUnit q

Tactic:
rw [not_lt, Nat.le_zero] at this

Premises used: Nat.le_zero, not_lt
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
Goal:
q : ℤ[X]
this : q.natDegree = 0
p : ℤ[X]
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * p) : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) (q * p).mirror : ℂ) (0 : ℂ))
hq' : q ∣ (q * p).mirror
hp : IsUnit q.leadingCoeff
rwa : IsUnit (M := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (q.coeff 0) : ℤ[X])
rwa₁ : IsUnit (q.coeff 0)
rwa₂ rwa₃ rwa₄ rwa₅ : IsUnit (q.coeff q.natDegree)
⊢ IsUnit q

Tactic:
rwa [eq_C_of_natDegree_eq_zero this, isUnit_C, ← this]

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, Polynomial.isUnit_C
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
suffices : ¬0 < q.natDegree
⊢ IsUnit q

Tactic:
suffices ¬0 < q.natDegree by
    rcases hq with ⟨p, rfl⟩
    replace hp := hp.leadingCoeff_isUnit
    rw [leadingCoeff_mul] at hp
    replace hp := isUnit_of_mul_isUnit_left hp
    rw [not_lt, Nat.le_zero] at this
    rwa [eq_C_of_natDegree_eq_zero this, isUnit_C, ← this]
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < q.natDegree
⊢ 0 < q.degree

Tactic:
rw [natDegree_pos_iff_degree_pos] at hq''

Premises used: Polynomial.natDegree_pos_iff_degree_pos
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < q.degree
⊢ 0 < (map (algebraMap ℤ ℂ) q).degree

Tactic:
rw [← degree_map_eq_of_injective (algebraMap ℤ ℂ).injective_int] at hq''

Premises used: Algebra.algebraMap, Int, Polynomial.degree_map_eq_of_injective, Complex, RingHom.injective_int
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
obtain : ∀ (z : ℂ) (hz : (map (algebraMap ℤ ℂ) q).IsRoot z), False
⊢ False

Tactic:
obtain ⟨z, hz⟩ := Complex.exists_root hq''

Premises used: Complex.exists_root
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (map (algebraMap ℤ ℂ) q).IsRoot z
⊢ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) q : ℂ) (0 : ℂ)

Tactic:
rw [IsRoot, eval_map_algebraMap] at hz

Premises used: Polynomial.IsRoot, Polynomial.eval_map_algebraMap
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) q : ℂ) (0 : ℂ)
⊢ False

Tactic:
h z ⟨?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
Goal:
p : ℤ[X]
hp : p.IsUnitTrinomial
h :
  ∀ (z : ℂ),
    ¬(Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧
        Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ))
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) q : ℂ) (0 : ℂ)
refine_1 : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
refine_2 : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p.mirror : ℂ) (0 : ℂ)
⊢ False

Tactic:
refine h z ⟨?_, ?_⟩

Premises used: And.intro