awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
hpq : Associated p q
⊢ p = q
have obtain : ∀ (u : R[X]ˣ) (hq : (p * (↑u : R[X])).Monic), p = p * (↑u : R[X])
Tactic: obtain ⟨u, rfl⟩ := hpq
Cleared hypotheses: q, hq, hpq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
u : R[X]ˣ
hq : (p * (↑u : R[X])).Monic
⊢ p = p * (↑u : R[X])
have rw : p = p * 1
Tactic: rw [(hp.of_mul_monic_left hq).eq_one_of_isUnit u.isUnit, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
u : R[X]ˣ
hq : (p * (↑u : R[X])).Monic
rw : p = p * 1
⊢ p = p * (↑u : R[X])
have rw₁ : p = p
Tactic: rw [(hp.of_mul_monic_left hq).eq_one_of_isUnit u.isUnit, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : MonicDegreeEq R n
⊢ (↑p : R[X]).Monic
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : MonicDegreeEq R n
h : Nontrivial R
⊢ (↑p : R[X]).Monic
have rw : (↑p : R[X]).leadingCoeff = 1
Tactic: rw [Monic, leadingCoeff, p.natDegree, p.2.1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : MonicDegreeEq R n
h : Nontrivial R
rw : (↑p : R[X]).leadingCoeff = 1
⊢ (↑p : R[X]).Monic
have rw₁ : (↑p : R[X]).coeff (↑p : R[X]).natDegree = 1
Tactic: rw [Monic, leadingCoeff, p.natDegree, p.2.1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : MonicDegreeEq R n
h : Nontrivial R
rw : (↑p : R[X]).leadingCoeff = 1
rw₁ : (↑p : R[X]).coeff (↑p : R[X]).natDegree = 1
⊢ (↑p : R[X]).Monic
have rw₂ : (↑p : R[X]).coeff n = 1
Tactic: rw [Monic, leadingCoeff, p.natDegree, p.2.1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : MonicDegreeEq R n
h : Nontrivial R
rw : (↑p : R[X]).leadingCoeff = 1
rw₁ : (↑p : R[X]).coeff (↑p : R[X]).natDegree = 1
rw₂ : (↑p : R[X]).coeff n = 1
⊢ (↑p : R[X]).Monic
have rw₃ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [Monic, leadingCoeff, p.natDegree, p.2.1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : MonicDegreeEq R n
i : ℕ
hi : n ≤ i
⊢ (↑p : R[X]).coeff i = if i = n then 1 else 0
have pos : i = n → (↑p : R[X]).coeff i = 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : MonicDegreeEq R n
i : ℕ
hi : n ≤ i
pos : i = n → (↑p : R[X]).coeff i = 1
⊢ (↑p : R[X]).coeff i = if i = n then 1 else 0
have neg : ¬i = n → (↑p : R[X]).coeff i = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst : Semiring R
p_1 q r : R[X]
inst_1 : Semiring S
p : R[X]
hp : p.Monic
hp' : p.natDegree = n
⊢ p.coeff n = 1
have rw : p.coeff p.natDegree = 1
Tactic: rw [← hp', ← leadingCoeff, hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst : Semiring R
p_1 q r : R[X]
inst_1 : Semiring S
p : R[X]
hp : p.Monic
hp' : p.natDegree = n
rw : p.coeff p.natDegree = 1
⊢ p.coeff n = 1
have rw₁ : p.leadingCoeff = 1
Tactic: rw [← hp', ← leadingCoeff, hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst : Semiring R
p_1 q r : R[X]
inst_1 : Semiring S
p : R[X]
hp : p.Monic
hp' : p.natDegree = n
rw : p.coeff p.natDegree = 1
rw₁ : p.leadingCoeff = 1
⊢ p.coeff n = 1
have rw₂ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [← hp', ← leadingCoeff, hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
t : Multiset ι
f : ι → R[X]
ht : ∀ i ∈ t, (f i).Monic
⊢ (Multiset.map f t).prod.Monic
have revert : ∀ (ht : ∀ i ∈ t, (f i).Monic), (Multiset.map f t).prod.Monic
Tactic: revert ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ ∀ (ht : ∀ i ∈ t, (f i).Monic), (Multiset.map f t).prod.Monic
have refine_1 : ∀ (ht : ∀ (i : ι), Membership.mem (γ := Multiset ι) 0 i → (f i).Monic), (Multiset.map f 0).prod.Monic
Tactic: refine t.induction_on ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
t : Multiset ι
f : ι → R[X]
refine_1 : ∀ (ht : ∀ (i : ι), Membership.mem (γ := Multiset ι) 0 i → (f i).Monic), (Multiset.map f 0).prod.Monic
⊢ ∀ (ht : ∀ i ∈ t, (f i).Monic), (Multiset.map f t).prod.Monic
have refine_2 : ∀ (a : ι) (s : Multiset ι),
  (∀ (ht : ∀ i ∈ s, (f i).Monic), (Multiset.map f s).prod.Monic) →
    ∀ (ht : ∀ i ∈ a ::ₘ s, (f i).Monic), (Multiset.map f (a ::ₘ s)).prod.Monic
Tactic: refine t.induction_on ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
t_1 : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : ∀ (ht : ∀ i ∈ t, (f i).Monic), (Multiset.map f t).prod.Monic
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f (a ::ₘ t)).prod.Monic
have refine_2 : (f a * (Multiset.map f t).prod).Monic
Tactic: rw [Multiset.map_cons, Multiset.prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
⊢ (finprod f).Monic
have rw : Monic.{u} (R := R)
  (if h : Function.HasFiniteMulSupport f then ∏ i ∈ Set.Finite.toFinset (s := Function.mulSupport f) h, f i else 1)
Tactic: rw [finprod_def]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
⊢ Monic.{u} (R := R)
    (if h : Function.HasFiniteMulSupport f then ∏ i ∈ Set.Finite.toFinset (s := Function.mulSupport f) h, f i else 1)
have pos : ∀ (h : Function.HasFiniteMulSupport f),
  Monic.{u} (R := R) (∏ i ∈ Set.Finite.toFinset (s := Function.mulSupport f) h, f i)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
pos :
  ∀ (h : Function.HasFiniteMulSupport f),
    Monic.{u} (R := R) (∏ i ∈ Set.Finite.toFinset (s := Function.mulSupport f) h, f i)
⊢ Monic.{u} (R := R)
    (if h : Function.HasFiniteMulSupport f then ∏ i ∈ Set.Finite.toFinset (s := Function.mulSupport f) h, f i else 1)
have neg : ¬Function.HasFiniteMulSupport f → Monic.{u} (R := R) 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
⊢ (finprod f).Monic
have rw : Monic.{u} (R := R)
  (if h : Function.HasFiniteMulSupport f then ∏ i ∈ Set.Finite.toFinset (s := Function.mulSupport f) h, f i else 1)
Tactic: classical
  rw [finprod_def]
  split_ifs
  · exact monic_prod_of_monic _ _ fun a ha => hf a ((Set.Finite.mem_toFinset _).mp ha)
  · exact monic_one
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
rw rw₁ rw₂ :
  Monic.{u} (R := R)
    (if h : Function.HasFiniteMulSupport f then ∏ i ∈ Set.Finite.toFinset (s := Function.mulSupport f) h, f i else 1)
⊢ (finprod f).Monic
have pos : ∀ (h : Function.HasFiniteMulSupport f),
  Monic.{u} (R := R) (∏ i ∈ Set.Finite.toFinset (s := Function.mulSupport f) h, f i)
Tactic: classical
  rw [finprod_def]
  split_ifs
  · exact monic_prod_of_monic _ _ fun a ha => hf a ((Set.Finite.mem_toFinset _).mp ha)
  · exact monic_one
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
rw rw₁ rw₂ :
  Monic.{u} (R := R)
    (if h : Function.HasFiniteMulSupport f then ∏ i ∈ Set.Finite.toFinset (s := Function.mulSupport f) h, f i else 1)
pos :
  ∀ (h : Function.HasFiniteMulSupport f),
    Monic.{u} (R := R) (∏ i ∈ Set.Finite.toFinset (s := Function.mulSupport f) h, f i)
⊢ (finprod f).Monic
have neg : ¬Function.HasFiniteMulSupport f → Monic.{u} (R := R) 1
Tactic: classical
  rw [finprod_def]
  split_ifs
  · exact monic_prod_of_monic _ _ fun a ha => hf a ((Set.Finite.mem_toFinset _).mp ha)
  · exact monic_one
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
t : Multiset ι
f : ι → R[X]
h : ∀ i ∈ t, (f i).Monic
⊢ (Multiset.map f t).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) t)
have revert : ∀ (h : ∀ i ∈ t, (f i).Monic),
  (Multiset.map f t).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) t)
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ ∀ (h : ∀ i ∈ t, (f i).Monic),
    (Multiset.map f t).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) t)
have refine_1 : ∀ (h : ∀ (i : ι), Membership.mem (γ := Multiset ι) 0 i → (f i).Monic),
  (Multiset.map f 0).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) 0)
Tactic: refine Multiset.induction_on t ?_ fun a t ih ht => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
t : Multiset ι
f : ι → R[X]
refine_1 :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Multiset ι) 0 i → (f i).Monic),
    (Multiset.map f 0).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) 0)
⊢ ∀ (h : ∀ i ∈ t, (f i).Monic),
    (Multiset.map f t).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) t)
have refine_2 : ∀ (a : ι) (t : Multiset ι)
  (ih :
    ∀ (h : ∀ i ∈ t, (f i).Monic),
      (Multiset.map f t).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) t))
  (ht : ∀ i ∈ a ::ₘ t, (f i).Monic),
  (Multiset.map f (a ::ₘ t)).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) (a ::ₘ t))
Tactic: refine Multiset.induction_on t ?_ fun a t ih ht => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ ∀ (h : ∀ (i : ι), Membership.mem (γ := Multiset ι) 0 i → (f i).Monic),
    (Multiset.map f 0).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) 0)
have refine_1 : Eq.{u + 1} (α := R) (nextCoeff 1) 0
Tactic: simp only [Multiset.notMem_zero, forall_prop_of_true, forall_prop_of_false, Multiset.map_zero,
      Multiset.prod_zero, Multiset.sum_zero, not_false_iff, forall_true_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ Eq.{u + 1} (α := R) (nextCoeff ((C : (a : R) → R[X]) 1)) 0
have refine_1 : Eq.{u + 1} (α := R) 0 0
Tactic: rw [nextCoeff_C_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
t_1 : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  ∀ (h : ∀ i ∈ t, (f i).Monic),
    (Multiset.map f t).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) t)
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f (a ::ₘ t)).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) (a ::ₘ t))
have refine_2 : ∀ i ∈ t, (f i).Monic
Tactic: rw [Multiset.map_cons, Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons,
      Monic.nextCoeff_mul, ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
t_1 : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  ∀ (h : ∀ i ∈ t, (f i).Monic),
    (Multiset.map f t).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) t)
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
refine_2 : ∀ i ∈ t, (f i).Monic
⊢ (Multiset.map f (a ::ₘ t)).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) (a ::ₘ t))
have refine_2₁ : (f a).Monic
Tactic: rw [Multiset.map_cons, Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons,
      Monic.nextCoeff_mul, ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
t_1 : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  ∀ (h : ∀ i ∈ t, (f i).Monic),
    (Multiset.map f t).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) t)
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
refine_2 : ∀ i ∈ t, (f i).Monic
refine_2₁ : (f a).Monic
⊢ (Multiset.map f (a ::ₘ t)).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) (a ::ₘ t))
have refine_2₂ : (Multiset.map f t).prod.Monic
Tactic: rw [Multiset.map_cons, Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons,
      Monic.nextCoeff_mul, ih]
-- 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 ↔ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
have refine_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),
  (HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X])).Monic
Tactic: refine
    ⟨fun h f g hf hg hp => (h.2 hp.symm).imp hf.eq_one_of_isUnit hg.eq_one_of_isUnit, fun h =>
      ⟨hp1 ∘ hp.eq_one_of_isUnit, fun f g hfg =>
        (h (g * C f.leadingCoeff) (f * C g.leadingCoeff) ?_ ?_ ?_).symm.imp
          (.of_mul_eq_one _)
          (.of_mul_eq_one _)⟩⟩
-- 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
refine_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),
    (HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X])).Monic
⊢ Irreducible p ↔ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
have refine_2 : ∀ (h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1) (f g : R[X]) (hfg : p = f * g),
  (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X])).Monic
Tactic: refine
    ⟨fun h f g hf hg hp => (h.2 hp.symm).imp hf.eq_one_of_isUnit hg.eq_one_of_isUnit, fun h =>
      ⟨hp1 ∘ hp.eq_one_of_isUnit, fun f g hfg =>
        (h (g * C f.leadingCoeff) (f * C g.leadingCoeff) ?_ ?_ ?_).symm.imp
          (.of_mul_eq_one _)
          (.of_mul_eq_one _)⟩⟩
-- 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
refine_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),
    (HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X])).Monic
refine_2 :
  ∀ (h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1) (f g : R[X]) (hfg : p = f * g),
    (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X])).Monic
⊢ Irreducible p ↔ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
have refine_3 : ∀ (h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1) (f g : R[X]) (hfg : p = f * g),
  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
Tactic: refine
    ⟨fun h f g hf hg hp => (h.2 hp.symm).imp hf.eq_one_of_isUnit hg.eq_one_of_isUnit, fun h =>
      ⟨hp1 ∘ hp.eq_one_of_isUnit, fun f g hfg =>
        (h (g * C f.leadingCoeff) (f * C g.leadingCoeff) ?_ ?_ ?_).symm.imp
          (.of_mul_eq_one _)
          (.of_mul_eq_one _)⟩⟩
-- 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
⊢ (HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X])).Monic
have refine_1 : (HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X])).leadingCoeff = 1
Tactic: rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, mul_comm, ← hfg, ← Monic]
-- 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_1 : (HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X])).leadingCoeff = 1
⊢ (HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X])).Monic
have refine_1₁ : g.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) f.leadingCoeff) = 1
Tactic: rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, mul_comm, ← hfg, ← Monic]
-- 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_1 : (HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X])).leadingCoeff = 1
refine_1₁ : g.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) f.leadingCoeff) = 1
⊢ (HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X])).Monic
have refine_1₂ : g.leadingCoeff * f.leadingCoeff = 1
Tactic: rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, mul_comm, ← hfg, ← Monic]
-- 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_1 : (HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X])).leadingCoeff = 1
refine_1₁ : g.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) f.leadingCoeff) = 1
refine_1₂ : g.leadingCoeff * f.leadingCoeff = 1
⊢ (HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X])).Monic
have refine_1₃ : (g * f).leadingCoeff = 1
Tactic: rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, mul_comm, ← hfg, ← Monic]
-- 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_1 : (HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X])).leadingCoeff = 1
refine_1₁ : g.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) f.leadingCoeff) = 1
refine_1₂ : g.leadingCoeff * f.leadingCoeff = 1
refine_1₃ : (g * f).leadingCoeff = 1
⊢ (HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X])).Monic
have refine_1₄ : (f * g).leadingCoeff = 1
Tactic: rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, mul_comm, ← hfg, ← Monic]
-- 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_1 : (HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X])).leadingCoeff = 1
refine_1₁ : g.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) f.leadingCoeff) = 1
refine_1₂ : g.leadingCoeff * f.leadingCoeff = 1
refine_1₃ : (g * f).leadingCoeff = 1
refine_1₄ : (f * g).leadingCoeff = 1
⊢ (HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X])).Monic
have refine_1₅ : p.leadingCoeff = 1
Tactic: rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, mul_comm, ← hfg, ← Monic]
-- 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
⊢ (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X])).Monic
have refine_2 : (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X])).leadingCoeff = 1
Tactic: rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, ← hfg, ← Monic]
-- 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_2 : (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X])).leadingCoeff = 1
⊢ (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X])).Monic
have refine_2₁ : f.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) g.leadingCoeff) = 1
Tactic: rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, ← hfg, ← Monic]
-- 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_2 : (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X])).leadingCoeff = 1
refine_2₁ : f.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) g.leadingCoeff) = 1
⊢ (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X])).Monic
have refine_2₂ : f.leadingCoeff * g.leadingCoeff = 1
Tactic: rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, ← hfg, ← Monic]
-- 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_2 : (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X])).leadingCoeff = 1
refine_2₁ : f.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) g.leadingCoeff) = 1
refine_2₂ : f.leadingCoeff * g.leadingCoeff = 1
⊢ (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X])).Monic
have refine_2₃ : (f * g).leadingCoeff = 1
Tactic: rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, ← hfg, ← Monic]
-- 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_2 : (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X])).leadingCoeff = 1
refine_2₁ : f.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) g.leadingCoeff) = 1
refine_2₂ : f.leadingCoeff * g.leadingCoeff = 1
refine_2₃ : (f * g).leadingCoeff = 1
⊢ (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X])).Monic
have refine_2₄ : p.leadingCoeff = 1
Tactic: rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, ← hfg, ← Monic]
-- 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
⊢ 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 *
    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
Tactic: rw [mul_mul_mul_comm, ← C_mul, ← leadingCoeff_mul, ← hfg, hp.leadingCoeff, C_1, mul_one,
      mul_comm, ← hfg]