awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha_1 : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
_ : ‖a‖₊ - 1 + 1 = ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1
_₁ :
  ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 ≤
    (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1
_₂ :
  (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 =
    (p.cauchyBound - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1
_₃ :
  (p.cauchyBound - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1 <
    (p.cauchyBound - 1) * ‖a‖₊ ^ p.natDegree / ‖a‖₊ ^ p.natDegree + 1
_₄ : (p.cauchyBound - 1) * ‖a‖₊ ^ p.natDegree / ‖a‖₊ ^ p.natDegree + 1 = p.cauchyBound
⊢ ‖a‖₊ < p.cauchyBound

Tactic:
calc
        ‖a‖₊ = ‖a‖₊ - 1 + 1 := (tsub_add_cancel_of_le ha.le).symm
        _ = ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 := by field
        _ ≤ (cauchyBound p - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1)
            / ‖a‖₊ ^ p.natDegree + 1 := by gcongr
        _ = (cauchyBound p - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1 := by
          congr 2
          have : ‖a‖₊ - 1 ≠ 0 := fun nh ↦ (ha.trans_le (tsub_eq_zero_iff_le.mp nh)).false
          field
        _ < (cauchyBound p - 1) * ‖a‖₊ ^ p.natDegree / ‖a‖₊ ^ p.natDegree + 1 := by
          gcongr
          · apply lt_of_le_of_ne (by simp)
            contrapose! this
            simp only [← this, zero_mul]
            apply pow_pos
            exact zero_lt_one.trans ha
          simp [zero_lt_one.trans ha]
        _ = cauchyBound p := by simp [field, tsub_add_cancel_of_le]

Premises used: NNNorm.nnnorm, HSub.hSub, tsub_add_cancel_of_le, HDiv.hDiv, LT.lt.le, Polynomial.cauchyBound, HPow.hPow, Polynomial.natDegree, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
suffices : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
⊢ ‖a‖₊ < p.cauchyBound

Tactic:
suffices ‖a‖₊ ^ p.natDegree ≤ (cauchyBound p - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x by
    rcases eq_or_ne ‖a‖₊ 1 with ha | ha
    · simp only [ha, one_pow, sum_const, card_range, nsmul_eq_mul, mul_one, gt_iff_lt] at this ⊢
      apply lt_of_le_of_ne (by simp)
      intro nh
      simp [← nh, tsub_self] at this
    rcases lt_or_gt_of_ne ha with ha | ha
    · apply ha.trans_le
      simp
    · rw [geom_sum_of_one_lt ha] at this
      calc
        ‖a‖₊ = ‖a‖₊ - 1 + 1 := (tsub_add_cancel_of_le ha.le).symm
        _ = ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 := by field
        _ ≤ (cauchyBound p - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1)
            / ‖a‖₊ ^ p.natDegree + 1 := by gcongr
        _ = (cauchyBound p - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1 := by
          congr 2
          have : ‖a‖₊ - 1 ≠ 0 := fun nh ↦ (ha.trans_le (tsub_eq_zero_iff_le.mp nh)).false
          field
        _ < (cauchyBound p - 1) * ‖a‖₊ ^ p.natDegree / ‖a‖₊ ^ p.natDegree + 1 := by
          gcongr
          · apply lt_of_le_of_ne (by simp)
            contrapose! this
            simp only [← this, zero_mul]
            apply pow_pos
            exact zero_lt_one.trans ha
          simp [zero_lt_one.trans ha]
        _ = cauchyBound p := by simp [field, tsub_add_cancel_of_le]
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
⊢ ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)

Tactic:
apply le_of_eq at h

Premises used: le_of_eq
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
⊢ ‖p.leadingCoeff‖₊ ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
⊢ ‖p.leadingCoeff‖₊ ≠ 0

Tactic:
have pld : ‖p.leadingCoeff‖₊ ≠ 0 := by simpa
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
ha : ‖p.leadingCoeff‖₊ ≠ 0
⊢ ‖a‖₊ ^ p.natDegree = ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊

Tactic:
rw [mul_div_cancel_left₀]

Premises used: mul_div_cancel_left₀
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
⊢ ‖p.leadingCoeff‖₊ ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
hc : 0 ≤ ‖p.leadingCoeff‖₊
⊢ ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ ≤
    nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) / ‖p.leadingCoeff‖₊

Tactic:
gcongr
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
hab : nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) ≤ ∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊
⊢ nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) / ‖p.leadingCoeff‖₊ ≤
    (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊

Tactic:
gcongr
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
⊢ nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) ≤ ∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊

Tactic:
apply nnnorm_sum_le

Premises used: nnnorm_sum_le
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
⊢ (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊ =
    (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
hab : ∀ i ∈ range p.natDegree, ‖p.coeff i‖₊ ≤ ‖p.leadingCoeff‖₊ * (p.cauchyBound - 1)
⊢ (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ ≤
    (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (p.cauchyBound - 1) * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊

Tactic:
gcongr (∑ x ∈ _, ?_ * _) / _

Premises used: HMul.hMul, Finset.sum
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
i : ℕ
h_1 : i ∈ range p.natDegree
hab : ‖p.coeff i‖₊ ≤ ‖p.leadingCoeff‖₊ * (((range p.natDegree).sup fun (x : ℕ) ↦ ‖p.coeff x‖₊) / ‖p.leadingCoeff‖₊)
⊢ ‖p.coeff i‖₊ ≤ ‖p.leadingCoeff‖₊ * (p.cauchyBound - 1)

Tactic:
rw [cauchyBound, add_tsub_cancel_right]

Premises used: Polynomial.cauchyBound, add_tsub_cancel_right
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
i : ℕ
h_1 : i ∈ range p.natDegree
hab : ‖p.coeff i‖₊ ≤ (range p.natDegree).sup fun (x : ℕ) ↦ ‖p.coeff x‖₊
⊢ ‖p.coeff i‖₊ ≤ ‖p.leadingCoeff‖₊ * (((range p.natDegree).sup fun (x : ℕ) ↦ ‖p.coeff x‖₊) / ‖p.leadingCoeff‖₊)

Tactic:
field_simp
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
i : ℕ
h_1 : i ∈ range p.natDegree
⊢ ‖p.coeff i‖₊ ≤ (range p.natDegree).sup fun (x : ℕ) ↦ ‖p.coeff x‖₊

Tactic:
apply le_sup (f := (‖p.coeff ·‖₊)) ‹_›

Premises used: Finset.le_sup
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
simp :
  (‖p.leadingCoeff‖₊ * (p.cauchyBound - 1) * ∑ i ∈ range p.natDegree, ‖a‖₊ ^ i) / ‖p.leadingCoeff‖₊ =
    (p.cauchyBound - 1) * ∑ i ∈ range p.natDegree, ‖a‖₊ ^ i
⊢ (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (p.cauchyBound - 1) * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ =
    (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x

Tactic:
simp only [← mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
⊢ (‖p.leadingCoeff‖₊ * (p.cauchyBound - 1) * ∑ i ∈ range p.natDegree, ‖a‖₊ ^ i) / ‖p.leadingCoeff‖₊ =
    (p.cauchyBound - 1) * ∑ i ∈ range p.natDegree, ‖a‖₊ ^ i

Tactic:
field
-- Module: Mathlib.Analysis.Polynomial.CauchyBound
Goal:
K : Type u_1
inst : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ nnnorm.{u_1} (E := K) (∑ i ∈ range p.natDegree, p.coeff i * a ^ i)
pld : ‖p.leadingCoeff‖₊ ≠ 0
calc : ‖a‖₊ ^ p.natDegree = ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊
calc₁ :
  ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ ≤
    nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) / ‖p.leadingCoeff‖₊
calc₂ :
  nnnorm.{u_1} (E := K) (∑ x ∈ range p.natDegree, p.coeff x * a ^ x) / ‖p.leadingCoeff‖₊ ≤
    (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊
calc₃ :
  (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊ =
    (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊
calc₄ :
  (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ ≤
    (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (p.cauchyBound - 1) * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊
calc₅ :
  (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (p.cauchyBound - 1) * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ =
    (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
⊢ ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x

Tactic:
calc ‖a‖₊ ^ p.natDegree
    _ = ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ := by
      rw [mul_div_cancel_left₀]
      simpa
    _ ≤ ‖∑ x ∈ range p.natDegree, p.coeff x * a ^ x‖₊ / ‖p.leadingCoeff‖₊ := by gcongr
    _ ≤ (∑ x ∈ range p.natDegree, ‖p.coeff x * a ^ x‖₊) / ‖p.leadingCoeff‖₊ := by
      gcongr
      apply nnnorm_sum_le
    _ = (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ := by simp
    _ ≤ (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (cauchyBound p - 1) * ‖a‖₊ ^ x) /
        ‖p.leadingCoeff‖₊ := by
      gcongr (∑ x ∈ _, ?_ * _) / _
      rw [cauchyBound, add_tsub_cancel_right]
      field_simp
      apply le_sup (f := (‖p.coeff ·‖₊)) ‹_›
    _ = (cauchyBound p - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x := by
      simp only [← mul_sum]
      field

Premises used: HMul.hMul, NNNorm.nnnorm, HSub.hSub, Polynomial.leadingCoeff, Polynomial.coeff, Finset.range, Polynomial.cauchyBound, HPow.hPow, Polynomial.natDegree, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
F : Type u_1
inst : Field F
inst_1 : IsAlgClosed F
f : F[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
⊢ 0 < f.natDegree

Tactic:
grind [IsMonicOfDegree.natDegree_eq]

Premises used: Polynomial.IsMonicOfDegree.natDegree_eq
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
F : Type u_1
inst : Field F
inst_1 : IsAlgClosed F
f : F[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
obtain :
  ∀ (f₁ : F[X]) (hf₁m : f₁.Monic) (hf₁i : Irreducible f₁) (f₂ : F[X]) (hf₂ : f = f₁ * f₂),
    ∃ (f₁ : F[X]) (f₂ : F[X]), f₁.IsMonicOfDegree 1 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
⊢ ∃ (f₁ : F[X]) (f₂ : F[X]), f₁.IsMonicOfDegree 1 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
obtain ⟨f₁, hf₁m, hf₁i, f₂, hf₂⟩ :=
    exists_monic_irreducible_factor f <| not_isUnit_of_natDegree_pos f <|
      by grind [IsMonicOfDegree.natDegree_eq]

Premises used: Polynomial.not_isUnit_of_natDegree_pos, Polynomial.exists_monic_irreducible_factor
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
F : Type u_1
inst : Field F
inst_1 : IsAlgClosed F
f : F[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : F[X]
hf₁m : f₁.Monic
hf₁i : Irreducible f₁
f₂ : F[X]
hf₂ : f = f₁ * f₂
⊢ (f₁ * f₂).IsMonicOfDegree (1 + n)

Tactic:
rw [hf₂, add_comm] at hf

Premises used: add_comm
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
F : Type u_1
inst : Field F
inst_1 : IsAlgClosed F
f : F[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : F[X]
hf₁m : f₁.Monic
hf₁i : Irreducible f₁
f₂ : F[X]
hf₂ : f = f₁ * f₂
hf₁ : (f₁ * f₂).IsMonicOfDegree (1 + n)
⊢ f = f₁ * f₂

Tactic:
rw [hf₂, add_comm] at hf

Premises used: add_comm
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
F : Type u_1
inst : Field F
inst_1 : IsAlgClosed F
f : F[X]
n : ℕ
f₁ : F[X]
hf₁m : f₁.Monic
hf₁i : Irreducible f₁
f₂ : F[X]
hf : (f₁ * f₂).IsMonicOfDegree (1 + n)
hf₂ : f = f₁ * f₂
⊢ f₁.IsMonicOfDegree 1

Tactic:
have hf₁ : IsMonicOfDegree f₁ 1 :=
    ⟨natDegree_eq_of_degree_eq_some <| IsAlgClosed.degree_eq_one_of_irreducible F hf₁i, hf₁m⟩
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
F : Type u_1
inst : Field F
inst_1 : IsAlgClosed F
f : F[X]
n : ℕ
f₁ : F[X]
hf₁m : f₁.Monic
hf₁i : Irreducible f₁
f₂ : F[X]
hf : (f₁ * f₂).IsMonicOfDegree (1 + n)
hf₂ : f = f₁ * f₂
hf₁ : f₁.IsMonicOfDegree 1
⊢ ∃ (f₁ : F[X]) (f₂ : F[X]), f₁.IsMonicOfDegree 1 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
⟨f₁, f₂, hf₁, hf₁.of_mul_left hf, hf₂⟩

Premises used: Polynomial.IsMonicOfDegree.of_mul_left, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
F : Type u_1
inst : Field F
inst_1 : IsAlgClosed F
f : F[X]
n : ℕ
f₁ : F[X]
hf₁m : f₁.Monic
hf₁i : Irreducible f₁
f₂ : F[X]
hf : (f₁ * f₂).IsMonicOfDegree (1 + n)
hf₂ : f = f₁ * f₂
hf₁ : f₁.IsMonicOfDegree 1
⊢ ∃ (f₁ : F[X]) (f₂ : F[X]), f₁.IsMonicOfDegree 1 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
exact ⟨f₁, f₂, hf₁, hf₁.of_mul_left hf, hf₂⟩
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
⊢ 0 < f.natDegree

Tactic:
grind [IsMonicOfDegree.natDegree_eq]

Premises used: Polynomial.IsMonicOfDegree.natDegree_eq
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
obtain :
  ∀ (f₁ : ℝ[X]) (hm : f₁.Monic) (hirr : Irreducible f₁) (f₂ : ℝ[X]) (hf₂ : f = f₁ * f₂),
    ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), (f₁.IsMonicOfDegree 1 ∨ f₁.IsMonicOfDegree 2) ∧ f = f₁ * f₂
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), (f₁.IsMonicOfDegree 1 ∨ f₁.IsMonicOfDegree 2) ∧ f = f₁ * f₂

Tactic:
obtain ⟨f₁, hm, hirr, f₂, hf₂⟩ :=
    exists_monic_irreducible_factor f <| not_isUnit_of_natDegree_pos f <|
      by grind [IsMonicOfDegree.natDegree_eq]

Premises used: Polynomial.not_isUnit_of_natDegree_pos, Polynomial.exists_monic_irreducible_factor
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : ℝ[X]
hm : f₁.Monic
hirr : Irreducible f₁
f₂ : ℝ[X]
hf₂ : f = f₁ * f₂
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), (f₁.IsMonicOfDegree 1 ∨ f₁.IsMonicOfDegree 2) ∧ f = f₁ * f₂

Tactic:
⟨f₁, f₂, ?_, hf₂⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : ℝ[X]
hm : f₁.Monic
hirr : Irreducible f₁
f₂ : ℝ[X]
hf₂ : f = f₁ * f₂
refine : f₁.IsMonicOfDegree 1 ∨ f₁.IsMonicOfDegree 2
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), (f₁.IsMonicOfDegree 1 ∨ f₁.IsMonicOfDegree 2) ∧ f = f₁ * f₂

Tactic:
refine ⟨f₁, f₂, ?_, hf₂⟩
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : ℝ[X]
hm : f₁.Monic
hirr : Irreducible f₁
f₂ : ℝ[X]
hf₂ : f = f₁ * f₂
P : ℕ → Prop
m : ℕ
hm₀ : 0 < m
hm₂ : m ≤ 2
h : P m
1 : ∀ (hm₀ : LT.lt (α := ℕ) 0 1) (hm₂ : LE.le (α := ℕ) 1 2) (h : P 1), P 1 ∨ P 2
2 : ∀ (hm₀ : LT.lt (α := ℕ) 0 2) (hm₂ : LE.le (α := ℕ) 2 2) (h : P 2), P 1 ∨ P 2
⊢ P 1 ∨ P 2

Tactic:
interval_cases m
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : ℝ[X]
hm : f₁.Monic
hirr : Irreducible f₁
f₂ : ℝ[X]
hf₂ : f = f₁ * f₂
P : ℕ → Prop
m : ℕ
hm₀ : LT.lt (α := ℕ) 0 1
hm₂ : LE.le (α := ℕ) 1 2
h : P 1
1 h_1 : ¬P 1 → P 2
⊢ P 1 ∨ P 2

Tactic:
tauto
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : ℝ[X]
hm : f₁.Monic
hirr : Irreducible f₁
f₂ : ℝ[X]
hf₂ : f = f₁ * f₂
P : ℕ → Prop
m : ℕ
hm₀ : LT.lt (α := ℕ) 0 2
hm₂ : LE.le (α := ℕ) 2 2
h : P 2
2 : ¬P 1 → P 2
⊢ P 1 ∨ P 2

Tactic:
tauto
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : ℝ[X]
hm : f₁.Monic
hirr : Irreducible f₁
f₂ : ℝ[X]
hf₂ : f = f₁ * f₂
⊢ ∀ {P : ℕ → Prop} {m : ℕ} (hm₀ : 0 < m) (hm₂ : m ≤ 2) (h : P m), P 1 ∨ P 2

Tactic:
have help {P : ℕ → Prop} {m : ℕ} (hm₀ : 0 < m) (hm₂ : m ≤ 2) (h : P m) : P 1 ∨ P 2 := by
    interval_cases m <;> tauto
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : ℝ[X]
hm : f₁.Monic
hirr : Irreducible f₁
f₂ : ℝ[X]
hf₂ : f = f₁ * f₂
help : ∀ {P : ℕ → Prop} {m : ℕ} (hm₀ : 0 < m) (hm₂ : m ≤ 2) (h : P m), P 1 ∨ P 2
⊢ f₁.IsMonicOfDegree 1 ∨ f₁.IsMonicOfDegree 2

Tactic:
help hirr.natDegree_pos hirr.natDegree_le_two <| IsMonicOfDegree.mk rfl hm

Premises used: Irreducible.natDegree_le_two, Polynomial.IsMonicOfDegree.mk, Irreducible.natDegree_pos, rfl
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : ℝ[X]
hm : f₁.Monic
hirr : Irreducible f₁
f₂ : ℝ[X]
hf₂ : f = f₁ * f₂
help : ∀ {P : ℕ → Prop} {m : ℕ} (hm₀ : 0 < m) (hm₂ : m ≤ 2) (h : P m), P 1 ∨ P 2
⊢ f₁.IsMonicOfDegree 1 ∨ f₁.IsMonicOfDegree 2

Tactic:
exact help hirr.natDegree_pos hirr.natDegree_le_two <| IsMonicOfDegree.mk rfl hm

Premises used: Irreducible.natDegree_le_two, Polynomial.IsMonicOfDegree.mk, Irreducible.natDegree_pos, rfl
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 2)
inl :
  ∀ (g₁ g₂ : ℝ[X]) (h : f = g₁ * g₂) (hd₁ : g₁.IsMonicOfDegree 1),
    ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
inr :
  ∀ (g₁ g₂ : ℝ[X]) (h : f = g₁ * g₂) (hd₂ : g₁.IsMonicOfDegree 2),
    ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
obtain ⟨g₁, g₂, hd₁ | hd₂, h⟩ := hf.eq_isMonicOfDegree_one_or_two_mul

Premises used: Polynomial.IsMonicOfDegree.eq_isMonicOfDegree_one_or_two_mul
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 2)
g₁ g₂ : ℝ[X]
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
⊢ (g₁ * g₂).IsMonicOfDegree (2 + n)

Tactic:
rw [h, add_comm] at hf

Premises used: add_comm
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 2)
g₁ g₂ : ℝ[X]
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hf₁ : (g₁ * g₂).IsMonicOfDegree (2 + n)
⊢ f = g₁ * g₂

Tactic:
rw [h, add_comm] at hf

Premises used: add_comm
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 2)
g₁ g₂ : ℝ[X]
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hf₁ : (g₁ * g₂).IsMonicOfDegree (2 + n)
h₁ : f = g₁ * g₂
⊢ g₁.IsMonicOfDegree 1

Tactic:
rw [h, add_comm] at hf

Premises used: add_comm
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 2)
g₁ g₂ : ℝ[X]
h : f = g₁ * g₂
hd₂ : g₁.IsMonicOfDegree 2
⊢ (g₁ * g₂).IsMonicOfDegree (2 + n)

Tactic:
rw [h, add_comm] at hf

Premises used: add_comm
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 2)
g₁ g₂ : ℝ[X]
h : f = g₁ * g₂
hd₂ : g₁.IsMonicOfDegree 2
hf₁ : (g₁ * g₂).IsMonicOfDegree (2 + n)
⊢ f = g₁ * g₂

Tactic:
rw [h, add_comm] at hf

Premises used: add_comm
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 2)
g₁ g₂ : ℝ[X]
h : f = g₁ * g₂
hd₂ : g₁.IsMonicOfDegree 2
hf₁ : (g₁ * g₂).IsMonicOfDegree (2 + n)
h₁ : f = g₁ * g₂
⊢ g₁.IsMonicOfDegree 2

Tactic:
rw [h, add_comm] at hf

Premises used: add_comm
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
⊢ 2 + n = 1 + (n + 1)

Tactic:
lia
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
⊢ g₂.IsMonicOfDegree (n + 1)

Tactic:
have hg₂ := of_mul_left hd₁ <| (show 2 + n = 1 + (n + 1) by lia) ▸ hf
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
inl :
  ∀ (p₁ p₂ : ℝ[X]) (h' : g₂ = p₁ * p₂) (hp₁ : p₁.IsMonicOfDegree 1),
    ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
inl₁ :
  ∀ (p₁ p₂ : ℝ[X]) (h' : g₂ = p₁ * p₂) (hp₂ : p₁.IsMonicOfDegree 2),
    ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
obtain ⟨p₁, p₂, hp₁ | hp₂, h'⟩ := hg₂.eq_isMonicOfDegree_one_or_two_mul

Premises used: Polynomial.IsMonicOfDegree.eq_isMonicOfDegree_one_or_two_mul
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
h' : g₂ = p₁ * p₂
hp₁ : p₁.IsMonicOfDegree 1
⊢ (g₁ * p₁ * p₂).IsMonicOfDegree (2 + n)

Tactic:
rw [h', ← mul_assoc] at h hf

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
h' : g₂ = p₁ * p₂
hp₁ : p₁.IsMonicOfDegree 1
hf₁ : (g₁ * p₁ * p₂).IsMonicOfDegree (2 + n)
⊢ f = g₁ * p₁ * p₂

Tactic:
rw [h', ← mul_assoc] at h hf

Premises used: mul_assoc