-- Mathlib/Analysis/Complex/Polynomial/Basic.lean
/-- An irreducible real polynomial has degree at most two. -/
lemma Irreducible.degree_le_two {p : ℝ[X]} (hp : Irreducible p) : degree p ≤ 2

Proof state:
z : ℂ
hz0 : z.im ≠ 0
q : ℝ[X]
hp : Irreducible ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q)
hz : (aeval z) ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q) = 0
hd : (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)).degree = 2
⊢ ¬2 = 0

Tactic:
exact two_ne_zero

Result:
no goals

Proof state:
case intro.inr.intro
z : ℂ
hz0 : z.im ≠ 0
q : ℝ[X]
hp : Irreducible ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q)
hz : (aeval z) ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q) = 0
hd : (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)).degree = 2
hq : IsUnit q
⊢ (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)).degree + q.degree = 2

Tactic:
rwa [isUnit_iff_degree_eq_zero.1 hq, add_zero]

Result:
no goals

Proof state:
case intro.inr.intro
z : ℂ
hz0 : z.im ≠ 0
q : ℝ[X]
hp : Irreducible ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q)
hz : (aeval z) ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q) = 0
hd : (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)).degree = 2
⊢ ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q).degree ≤ 2

Tactic:
have hq : IsUnit q := by
  refine (of_irreducible_mul hp).resolve_left (mt isUnit_iff_degree_eq_zero.1 ?_)
  rw [hd]
  exact two_ne_zero

Result:
case intro.inr.intro
z : ℂ
hz0 : z.im ≠ 0
q : ℝ[X]
hp : Irreducible ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q)
hz : (aeval z) ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q) = 0
hd : (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)).degree = 2
hq : IsUnit q
⊢ ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q).degree ≤ 2

Proof state:
case intro.inl
p : ℝ[X]
hp : Irreducible p
z : ℂ
hz : (aeval z) p = 0
hz0 : z.im = 0
⊢ p.degree ≤ 2

Tactic:
lift z to ℝ using hz0

Result:
case intro.inl.intro
p : ℝ[X]
hp : Irreducible p
z : ℝ
hz : (aeval ↑z) p = 0
⊢ p.degree ≤ 2

Proof state:
case intro.inr.intro
z : ℂ
hz0 : z.im ≠ 0
q : ℝ[X]
hp : Irreducible ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q)
hz : (aeval z) ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q) = 0
⊢ ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q).degree ≤ 2

Tactic:
have hd : degree (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) = 2 := by
  compute_degree!

Result:
case intro.inr.intro
z : ℂ
hz0 : z.im ≠ 0
q : ℝ[X]
hp : Irreducible ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q)
hz : (aeval z) ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q) = 0
hd : (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)).degree = 2
⊢ ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q).degree ≤ 2

Proof state:
case intro.inr
p : ℝ[X]
hp : Irreducible p
z : ℂ
hz : (aeval z) p = 0
hz0 : z.im ≠ 0
⊢ p.degree ≤ 2

Tactic:
obtain ⟨q, rfl⟩ := p.quadratic_dvd_of_aeval_eq_zero_im_ne_zero hz hz0

Result:
case intro.inr.intro
z : ℂ
hz0 : z.im ≠ 0
q : ℝ[X]
hp : Irreducible ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q)
hz : (aeval z) ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q) = 0
⊢ ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q).degree ≤ 2

Proof state:
case intro.inl.intro
p : ℝ[X]
hp : Irreducible p
z : ℝ
hz : (aeval ↑z) p = 0
⊢ p.degree ≤ 2

Tactic:
erw [aeval_ofReal, RCLike.ofReal_eq_zero] at hz

Result:
case intro.inl.intro
p : ℝ[X]
hp : Irreducible p
z : ℝ
hz : eval z p = 0
⊢ p.degree ≤ 2

Proof state:
case intro.inl.intro
p : ℝ[X]
hp : Irreducible p
z : ℝ
hz : eval z p = 0
⊢ p.degree ≤ 2

Tactic:
exact (degree_eq_one_of_irreducible_of_root hp hz).trans_le one_le_two

Result:
no goals

Proof state:
z : ℂ
hz0 : z.im ≠ 0
q : ℝ[X]
hp : Irreducible ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q)
hz : (aeval z) ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q) = 0
⊢ (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)).degree = 2

Tactic:
compute_degree!

Result:
no goals

Proof state:
case intro.inr.intro
z : ℂ
hz0 : z.im ≠ 0
q : ℝ[X]
hp : Irreducible ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q)
hz : (aeval z) ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q) = 0
hd : (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)).degree = 2
hq : IsUnit q
⊢ ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q).degree ≤ 2

Tactic:
refine (degree_mul_le _ _).trans_eq ?_

Result:
case intro.inr.intro
z : ℂ
hz0 : z.im ≠ 0
q : ℝ[X]
hp : Irreducible ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q)
hz : (aeval z) ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q) = 0
hd : (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)).degree = 2
hq : IsUnit q
⊢ (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)).degree + q.degree = 2

Proof state:
case intro
p : ℝ[X]
hp : Irreducible p
z : ℂ
hz : (aeval z) p = 0
⊢ p.degree ≤ 2

Tactic:
cases eq_or_ne z.im 0 with
| inl hz0 =>
  lift z to ℝ using hz0
  erw [aeval_ofReal, RCLike.ofReal_eq_zero] at hz
  exact (degree_eq_one_of_irreducible_of_root hp hz).trans_le one_le_two
| inr hz0 =>
  obtain ⟨q, rfl⟩ := p.quadratic_dvd_of_aeval_eq_zero_im_ne_zero hz hz0
  have hd : degree (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) = 2 := by
    compute_degree!
  have hq : IsUnit q := by
    refine (of_irreducible_mul hp).resolve_left (mt isUnit_iff_degree_eq_zero.1 ?_)
    rw [hd]
    exact two_ne_zero
  refine (degree_mul_le _ _).trans_eq ?_
  rwa [isUnit_iff_degree_eq_zero.1 hq, add_zero]

Result:
no goals

Proof state:
z : ℂ
hz0 : z.im ≠ 0
q : ℝ[X]
hp : Irreducible ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q)
hz : (aeval z) ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q) = 0
hd : (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)).degree = 2
⊢ ¬(X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)).degree = 0

Tactic:
rw [hd]

Result:
z : ℂ
hz0 : z.im ≠ 0
q : ℝ[X]
hp : Irreducible ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q)
hz : (aeval z) ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q) = 0
hd : (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)).degree = 2
⊢ ¬2 = 0

Proof state:
p : ℝ[X]
hp : Irreducible p
⊢ p.degree ≤ 2

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

Result:
case intro
p : ℝ[X]
hp : Irreducible p
z : ℂ
hz : (aeval z) p = 0
⊢ p.degree ≤ 2

Proof state:
z : ℂ
hz0 : z.im ≠ 0
q : ℝ[X]
hp : Irreducible ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q)
hz : (aeval z) ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q) = 0
hd : (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)).degree = 2
⊢ IsUnit q

Tactic:
refine (of_irreducible_mul hp).resolve_left (mt isUnit_iff_degree_eq_zero.1 ?_)

Result:
z : ℂ
hz0 : z.im ≠ 0
q : ℝ[X]
hp : Irreducible ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q)
hz : (aeval z) ((X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) * q) = 0
hd : (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)).degree = 2
⊢ ¬(X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)).degree = 0