awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
refine_3 :
  g * f *
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) =
    p
⊢ HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) *
      HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) =
    p
have refine_3₁ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) (f.leadingCoeff * g.leadingCoeff) : R[X]) = p
Tactic: rw [mul_mul_mul_comm, ← C_mul, ← leadingCoeff_mul, ← hfg, hp.leadingCoeff, C_1, mul_one,
      mul_comm, ← hfg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
refine_3 :
  g * f *
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) =
    p
refine_3₁ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) (f.leadingCoeff * g.leadingCoeff) : R[X]) = p
⊢ HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) *
      HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) =
    p
have refine_3₂ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) (f * g).leadingCoeff : R[X]) = p
Tactic: rw [mul_mul_mul_comm, ← C_mul, ← leadingCoeff_mul, ← hfg, hp.leadingCoeff, C_1, mul_one,
      mul_comm, ← hfg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
refine_3 :
  g * f *
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) =
    p
refine_3₁ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) (f.leadingCoeff * g.leadingCoeff) : R[X]) = p
refine_3₂ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) (f * g).leadingCoeff : R[X]) = p
⊢ HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) *
      HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) =
    p
have refine_3₃ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) = p
Tactic: rw [mul_mul_mul_comm, ← C_mul, ← leadingCoeff_mul, ← hfg, hp.leadingCoeff, C_1, mul_one,
      mul_comm, ← hfg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
refine_3 :
  g * f *
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) =
    p
refine_3₁ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) (f.leadingCoeff * g.leadingCoeff) : R[X]) = p
refine_3₂ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) (f * g).leadingCoeff : R[X]) = p
refine_3₃ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) = p
⊢ HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) *
      HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) =
    p
have refine_3₄ : g * f * (C : (a : R) → R[X]) 1 = p
Tactic: rw [mul_mul_mul_comm, ← C_mul, ← leadingCoeff_mul, ← hfg, hp.leadingCoeff, C_1, mul_one,
      mul_comm, ← hfg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
refine_3 :
  g * f *
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) =
    p
refine_3₁ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) (f.leadingCoeff * g.leadingCoeff) : R[X]) = p
refine_3₂ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) (f * g).leadingCoeff : R[X]) = p
refine_3₃ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) = p
refine_3₄ : g * f * (C : (a : R) → R[X]) 1 = p
⊢ HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) *
      HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) =
    p
have refine_3₅ : g * f * 1 = p
Tactic: rw [mul_mul_mul_comm, ← C_mul, ← leadingCoeff_mul, ← hfg, hp.leadingCoeff, C_1, mul_one,
      mul_comm, ← hfg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
refine_3 :
  g * f *
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) =
    p
refine_3₁ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) (f.leadingCoeff * g.leadingCoeff) : R[X]) = p
refine_3₂ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) (f * g).leadingCoeff : R[X]) = p
refine_3₃ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) = p
refine_3₄ : g * f * (C : (a : R) → R[X]) 1 = p
refine_3₅ : g * f * 1 = p
⊢ HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) *
      HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) =
    p
have refine_3₆ : g * f = p
Tactic: rw [mul_mul_mul_comm, ← C_mul, ← leadingCoeff_mul, ← hfg, hp.leadingCoeff, C_1, mul_one,
      mul_comm, ← hfg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
refine_3 :
  g * f *
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) =
    p
refine_3₁ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) (f.leadingCoeff * g.leadingCoeff) : R[X]) = p
refine_3₂ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) (f * g).leadingCoeff : R[X]) = p
refine_3₃ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) = p
refine_3₄ : g * f * (C : (a : R) → R[X]) 1 = p
refine_3₅ : g * f * 1 = p
refine_3₆ : g * f = p
⊢ HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) *
      HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) =
    p
have refine_3₇ : f * g = p
Tactic: rw [mul_mul_mul_comm, ← C_mul, ← leadingCoeff_mul, ← hfg, hp.leadingCoeff, C_1, mul_one,
      mul_comm, ← hfg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
refine_3 :
  g * f *
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) =
    p
refine_3₁ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) (f.leadingCoeff * g.leadingCoeff) : R[X]) = p
refine_3₂ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) (f * g).leadingCoeff : R[X]) = p
refine_3₃ : HMul.hMul (β := R[X]) (g * f) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) = p
refine_3₄ : g * f * (C : (a : R) → R[X]) 1 = p
refine_3₅ : g * f * 1 = p
refine_3₆ : g * f = p
refine_3₇ : f * g = p
⊢ HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) *
      HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) =
    p
have refine_3₈ : p = p
Tactic: rw [mul_mul_mul_comm, ← C_mul, ← leadingCoeff_mul, ← hfg, hp.leadingCoeff, C_1, mul_one,
      mul_comm, ← hfg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
have pos : ∀ (hp1 : p = 1),
  Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
Tactic: by_cases hp1 : p = 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
pos :
  ∀ (hp1 : p = 1),
    Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
have neg : ∀ (hp1 : ¬p = 1),
  Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
Tactic: by_cases hp1 : p = 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
have neg : (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1) ↔
  ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
Tactic: rw [irreducible_of_monic hp hp1, and_iff_right hp1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1) ↔
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
have neg : ∀ (a b : R[X]) (ha : a.Monic) (hb : b.Monic), a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → a.natDegree = 0 ∨ b.natDegree = 0
Tactic: refine forall₄_congr fun a b ha hb => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
a b : R[X]
ha : a.Monic
hb : b.Monic
⊢ a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → a.natDegree = 0 ∨ b.natDegree = 0
have neg : a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → a = 1 ∨ b.natDegree = 0
Tactic: rw [ha.natDegree_eq_zero, hb.natDegree_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
a b : R[X]
ha : a.Monic
hb : b.Monic
neg : a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → a = 1 ∨ b.natDegree = 0
⊢ a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → a.natDegree = 0 ∨ b.natDegree = 0
have neg₁ : a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → a = 1 ∨ b = 1
Tactic: rw [ha.natDegree_eq_zero, hb.natDegree_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)
have simp_rw : (p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔
  p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
Tactic: simp_rw [hp.irreducible_iff_natDegree, mem_Ioc, Nat.le_div_iff_mul_le zero_lt_two, mul_two]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔
    p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
have h : (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔
  ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
Tactic: apply and_congr_right'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
have h : (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) →
  ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
h :
  (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) →
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
have h₁ : (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)) →
  ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
f g : R[X]
hf : f.Monic
hg : g.Monic
he : f * g = p
⊢ ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
have h₁ : ∀ (hp : (f * g).Monic)
  (h : ∀ (f_1 g_1 : R[X]), f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → f_1.natDegree = 0 ∨ g_1.natDegree = 0),
  ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ (f * g).natDegree)
Tactic: subst he
Cleared hypotheses: p, hp, h, he
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
f g : R[X]
hf : f.Monic
hg : g.Monic
he : f * g = p
⊢ f.natDegree = 0 ∨ g.natDegree = 0
have hp₁ : (f * g).Monic
Tactic: subst he
Cleared hypotheses: p, hp, h, he
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
f g : R[X]
hf : f.Monic
hg : g.Monic
he : f * g = p
hp₁ : (f * g).Monic
⊢ f.natDegree = 0 ∨ g.natDegree = 0
have h₁ : ∀ (f_1 g_1 : R[X]),
  f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → ¬(0 < g_1.natDegree ∧ g_1.natDegree + g_1.natDegree ≤ (f * g).natDegree)
Tactic: subst he
Cleared hypotheses: p, hp, h, he
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : ∀ (f_1 g_1 : R[X]), f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → f_1.natDegree = 0 ∨ g_1.natDegree = 0
⊢ ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ (f * g).natDegree)
have h₁ : ¬(0 < g.natDegree ∧ g.natDegree ≤ f.natDegree)
Tactic: rw [hf.natDegree_mul hg, add_le_add_iff_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h :
  ∀ (f_1 g_1 : R[X]),
    f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → ¬(0 < g_1.natDegree ∧ g_1.natDegree + g_1.natDegree ≤ (f * g).natDegree)
⊢ f.natDegree = 0 ∨ g.natDegree = 0
have h₁ : ∀ (f_1 g_1 : R[X]),
  f_1.Monic →
    g_1.Monic → f_1 * g_1 = f * g → ¬(g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree)
Tactic: simp_rw [hf.natDegree_mul hg, pos_iff_ne_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h :
  ∀ (f_1 g_1 : R[X]),
    f_1.Monic →
      g_1.Monic → f_1 * g_1 = f * g → ¬(g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree)
⊢ f.natDegree = 0 ∨ g.natDegree = 0
have h₁ : ∀ (h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0),
  ∃ (f_1 : R[X]) (g_1 : R[X]),
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
⊢ ∃ (f_1 : R[X]) (g_1 : R[X]),
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree
have h₁ : ∀ (hl : f.natDegree ≤ g.natDegree),
  ∃ (f_1 : R[X]) (g_1 : R[X]),
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree
Tactic: obtain hl | hl := le_total f.natDegree g.natDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
h₁ :
  ∀ (hl : f.natDegree ≤ g.natDegree),
    ∃ (f_1 : R[X]) (g_1 : R[X]),
      f_1.Monic ∧
        g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree
⊢ ∃ (f_1 : R[X]) (g_1 : R[X]),
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree
have h₂ : ∀ (hl : g.natDegree ≤ f.natDegree),
  ∃ (f_1 : R[X]) (g_1 : R[X]),
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree
Tactic: obtain hl | hl := le_total f.natDegree g.natDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p
have rw : (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) ↔
  ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p
Tactic: rw [hp.irreducible_iff_natDegree', and_iff_right hp1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) ↔
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p
have mp : (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) →
  ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
mp :
  (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) →
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) ↔
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p
have mpr : (∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p) →
  ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
⊢ ¬Irreducible p ↔ ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
have inl : Subsingleton R → (¬Irreducible p ↔ ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
inl : Subsingleton R → (¬Irreducible p ↔ ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂)
⊢ ¬Irreducible p ↔ ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
have inr : Nontrivial R → (¬Irreducible p ↔ ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h : Nontrivial R
⊢ ¬Irreducible p ↔ ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
have inr : (¬∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (2 / 2)) ↔
  ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
Tactic: rw [hm.irreducible_iff_natDegree', and_iff_right, hnd]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h : Nontrivial R
inr :
  (¬∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (2 / 2)) ↔
    ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
⊢ ¬Irreducible p ↔ ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
have inr₁ : p ≠ 1
Tactic: rw [hm.irreducible_iff_natDegree', and_iff_right, hnd]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h : Nontrivial R
⊢ (¬∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (2 / 2)) ↔
    ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
have inr : (∃ (f : R[X]) (g : R[X]), f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)) ↔
  ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
Tactic: push Not
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h : Nontrivial R
⊢ (∃ (f : R[X]) (g : R[X]), f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)) ↔
    ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
have inr : (∃ (f : R[X]) (g : R[X]), f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)) →
  ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h : Nontrivial R
inr :
  (∃ (f : R[X]) (g : R[X]), f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)) →
    ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
⊢ (∃ (f : R[X]) (g : R[X]), f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)) ↔
    ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
have inr₁ : (∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂) →
  ∃ (f : R[X]) (g : R[X]), f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
h : Nontrivial R
a b : R[X]
ha : a.Monic
hb : b.Monic
hdb : b.natDegree ∈ Ioc 0 (2 / 2)
hm : (a * b).Monic
hnd : (a * b).natDegree = 2
⊢ ∃ (c₁ : R) (c₂ : R), (a * b).coeff 0 = c₁ * c₂ ∧ (a * b).coeff 1 = c₁ + c₂
have hdb₁ : b.natDegree = 1
Tactic: simp only [Nat.Ioc_succ_singleton, zero_add, mem_singleton] at hdb
Cleared hypotheses: hdb