awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
zero : (HPow.hPow (β := ℕ) p 0).natDegree = 0 * p.natDegree
succ : ∀ (n : ℕ) (hn : (p ^ n).natDegree = n * p.natDegree), (p ^ (n + 1)).natDegree = (n + 1) * p.natDegree
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
induction n with
  | zero => simp
  | succ n hn => rw [pow_succ, (hp.pow n).natDegree_mul hp, hn, Nat.succ_mul, add_comm]

Premises used: pow_succ, add_comm, Nat.succ_mul, Polynomial.Monic.pow, Polynomial.Monic.natDegree_mul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
r : R
rw : n * (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).natDegree = n
rw₁ : n * 1 = n
rw₂ rw₃ : n = n
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ n).natDegree = n

Tactic:
rw [(monic_X_add_C r).natDegree_pow, natDegree_X_add_C, mul_one]

Premises used: Polynomial.Monic.natDegree_pow, Polynomial.natDegree_X_add_C, Polynomial.monic_X_add_C, mul_one
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
h : Nontrivial R
obtain : ∀ (q : R[X]) (h : p * q = 1), p = 1
⊢ p = 1

Tactic:
obtain ⟨q, h⟩ := hpu.exists_right_inv

Premises used: IsUnit.exists_right_inv
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
h_1 : Nontrivial R
q : R[X]
h : p * q = 1
⊢ (p * q).natDegree = p.natDegree + q.natDegree

Tactic:
have := hm.natDegree_mul' (right_ne_zero_of_mul_eq_one h)
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
h_1 : Nontrivial R
q : R[X]
h : p * q = 1
this : (p * q).natDegree = p.natDegree + q.natDegree
⊢ p.natDegree = 0 ∧ q.natDegree = 0

Tactic:
rw [h, natDegree_one, eq_comm, add_eq_zero] at this

Premises used: eq_comm, Polynomial.natDegree_one, add_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
h_1 : Nontrivial R
q : R[X]
h : p * q = 1
this : p.natDegree = 0 ∧ q.natDegree = 0
⊢ p = 1

Tactic:
hm.natDegree_eq_zero.mp this.1

Premises used: Polynomial.Monic.natDegree_eq_zero, And.left, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
h_1 : Nontrivial R
q : R[X]
h : p * q = 1
this : p.natDegree = 0 ∧ q.natDegree = 0
⊢ p = 1

Tactic:
exact hm.natDegree_eq_zero.mp this.1

Premises used: Polynomial.Monic.natDegree_eq_zero, And.left, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hm : p.Monic
⊢ IsUnit p ↔ p = 1

Tactic:
⟨hm.eq_one_of_isUnit, fun h => h.symm ▸ isUnit_one⟩

Premises used: Eq.rec, isUnit_one, Iff.intro, Polynomial.Monic.eq_one_of_isUnit, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
hpq : Associated p q
obtain : ∀ (u : R[X]ˣ) (hq : (p * (↑u : R[X])).Monic), p = p * (↑u : R[X])
⊢ p = q

Tactic:
obtain ⟨u, rfl⟩ := hpq

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Monic
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
rw₁ rw₂ : p = p
⊢ p = p * (↑u : R[X])

Tactic:
rw [(hp.of_mul_monic_left hq).eq_one_of_isUnit u.isUnit, mul_one]

Premises used: Polynomial.Monic.of_mul_monic_left, Units.isUnit, mul_one, Polynomial.Monic.eq_one_of_isUnit
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
n : ℕ
inst : Semiring R
inst_1 : Nontrivial R
p : MonicDegreeEq R n
⊢ (↑p : R[X]).coeff n ≠ 0

Tactic:
simp [p.2.1]

Premises used: And.left, Subtype.property
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : MonicDegreeEq R n
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Monic
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
rw₃ rw₄ : Eq.{u + 1} (α := R) 1 1
⊢ (↑p : R[X]).Monic

Tactic:
rw [Monic, leadingCoeff, p.natDegree, p.2.1]

Premises used: Polynomial.leadingCoeff, Polynomial.Monic, And.left, Polynomial.MonicDegreeEq.natDegree, Subtype.property
-- Module: Mathlib.Algebra.Polynomial.Monic
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
neg : ¬i = n → (↑p : R[X]).coeff i = 0
⊢ (↑p : R[X]).coeff i = if i = n then 1 else 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : MonicDegreeEq R n
i : ℕ
hi : n ≤ i
h : i = n
⊢ (↑p : R[X]).coeff i = 1

Tactic:
simp_all [p.2.1, p.2.2 _ (hi.lt_of_ne (.symm _))]

Premises used: Ne.symm, LE.le.lt_of_ne, And.right, And.left, Subtype.property
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : MonicDegreeEq R n
i : ℕ
hi : n ≤ i
h : ¬i = n
⊢ (↑p : R[X]).coeff i = 0

Tactic:
simp_all [p.2.1, p.2.2 _ (hi.lt_of_ne (.symm _))]

Premises used: Ne.symm, LE.le.lt_of_ne, And.right, And.left, Subtype.property
-- Module: Mathlib.Algebra.Polynomial.Monic
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
rw₂ rw₃ : Eq.{u + 1} (α := R) 1 1
⊢ p.coeff n = 1

Tactic:
rw [← hp', ← leadingCoeff, hp]

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Monic
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 : MonicDegreeEq R n
f : R →+* S
⊢ (Polynomial.map f (↑p : R[X])).coeff n = 1 ∧ ∀ i > n, (Polynomial.map f (↑p : R[X])).coeff i = 0

Tactic:
simp +contextual [coeff_map, p.2]

Premises used: Polynomial.coeff_map, Subtype.property
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
t : Multiset ι
f : ι → R[X]
ht : ∀ i ∈ t, (f i).Monic
revert : ∀ (ht : ∀ i ∈ t, (f i).Monic), (Multiset.map f t).prod.Monic
⊢ (Multiset.map f t).prod.Monic

Tactic:
revert ht
-- Module: Mathlib.Algebra.Polynomial.Monic
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

Tactic:
t.induction_on ?_ ?_

Premises used: Multiset.induction_on
-- Module: Mathlib.Algebra.Polynomial.Monic
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
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
⊢ ∀ (ht : ∀ i ∈ t, (f i).Monic), (Multiset.map f t).prod.Monic

Tactic:
refine t.induction_on ?_ ?_
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ ∀ (ht : ∀ (i : ι), Membership.mem (γ := Multiset ι) 0 i → (f i).Monic), (Multiset.map f 0).prod.Monic

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Monic
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
refine_2 : (f a * (Multiset.map f t).prod).Monic
⊢ (Multiset.map f (a ::ₘ t)).prod.Monic

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons]

Premises used: Multiset.map_cons, Multiset.prod_cons
-- Module: Mathlib.Algebra.Polynomial.Monic
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
⊢ (f a * (Multiset.map f t).prod).Monic

Tactic:
(ht _ (Multiset.mem_cons_self _ _)).mul (ih fun _ hi => ht _ (Multiset.mem_cons_of_mem hi))

Premises used: Multiset.mem_cons_of_mem, Multiset.mem_cons_self, Polynomial.Monic.mul
-- Module: Mathlib.Algebra.Polynomial.Monic
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
⊢ (f a * (Multiset.map f t).prod).Monic

Tactic:
exact (ht _ (Multiset.mem_cons_self _ _)).mul (ih fun _ hi => ht _ (Multiset.mem_cons_of_mem hi))

Premises used: Multiset.mem_cons_of_mem, Multiset.mem_cons_self, Polynomial.Monic.mul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
s : Finset ι
f : ι → R[X]
hs : ∀ i ∈ s, (f i).Monic
⊢ Monic.{u} (R := R) (∏ i ∈ s, f i)

Tactic:
monic_multiset_prod_of_monic s.1 f hs

Premises used: Polynomial.monic_multiset_prod_of_monic, Finset.val, Finset.prod
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
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

Tactic:
rw [finprod_def]

Premises used: finprod_def
-- Module: Mathlib.Algebra.Polynomial.Monic
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)
neg : ¬Function.HasFiniteMulSupport f → Monic.{u} (R := R) 1
⊢ Monic.{u} (R := R)
    (if h : Function.HasFiniteMulSupport f then ∏ i ∈ Set.Finite.toFinset (s := Function.mulSupport f) h, f i else 1)

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
h : Function.HasFiniteMulSupport f
⊢ Monic.{u} (R := R) (∏ i ∈ Set.Finite.toFinset (s := Function.mulSupport f) h, f i)

Tactic:
monic_prod_of_monic _ _ fun a ha => hf a ((Set.Finite.mem_toFinset _).mp ha)

Premises used: Set.Finite.mem_toFinset, Polynomial.monic_prod_of_monic, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
h : Function.HasFiniteMulSupport f
⊢ Monic.{u} (R := R) (∏ i ∈ Set.Finite.toFinset (s := Function.mulSupport f) h, f i)

Tactic:
exact monic_prod_of_monic _ _ fun a ha => hf a ((Set.Finite.mem_toFinset _).mp ha)

Premises used: Set.Finite.mem_toFinset, Polynomial.monic_prod_of_monic, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
h : ¬Function.HasFiniteMulSupport f
⊢ Monic.{u} (R := R) 1

Tactic:
monic_one

Premises used: Polynomial.monic_one
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
h : ¬Function.HasFiniteMulSupport f
⊢ Monic.{u} (R := R) 1

Tactic:
exact monic_one

Premises used: Polynomial.monic_one
-- Module: Mathlib.Algebra.Polynomial.Monic
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)
neg neg₁ : ¬Function.HasFiniteMulSupport f → Monic.{u} (R := R) 1
⊢ (finprod f).Monic

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

Premises used: Set.Finite.mem_toFinset, Polynomial.monic_prod_of_monic, Iff.mp, Polynomial.monic_one, finprod_def
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
t : Multiset ι
f : ι → R[X]
h : ∀ i ∈ t, (f i).Monic
revert :
  ∀ (h : ∀ i ∈ t, (f i).Monic),
    (Multiset.map f t).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) t)
⊢ (Multiset.map f t).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) t)

Tactic:
revert h
-- Module: Mathlib.Algebra.Polynomial.Monic
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)

Tactic:
Multiset.induction_on t ?_ fun a t ih ht => ?_

Premises used: Multiset.induction_on
-- Module: Mathlib.Algebra.Polynomial.Monic
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)
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))
⊢ ∀ (h : ∀ i ∈ t, (f i).Monic),
    (Multiset.map f t).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) t)

Tactic:
refine Multiset.induction_on t ?_ fun a t ih ht => ?_
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
t : Multiset ι
f : ι → R[X]
refine_1 : Eq.{u + 1} (α := R) (nextCoeff 1) 0
⊢ ∀ (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:
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]

Premises used: Multiset.prod_zero, Multiset.notMem_zero, Multiset.map_zero, forall_prop_of_false, Multiset.sum_zero, forall_prop_of_true, forall_true_iff, not_false_iff
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
t : Multiset ι
f : ι → R[X]
refine_1 refine_1₁ : Eq.{u + 1} (α := R) 0 0
⊢ Eq.{u + 1} (α := R) (nextCoeff ((C : (a : R) → R[X]) 1)) 0

Tactic:
rw [nextCoeff_C_eq_zero]

Premises used: Polynomial.nextCoeff_C_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
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
refine_2₂ : (Multiset.map f t).prod.Monic
⊢ (Multiset.map f (a ::ₘ t)).prod.nextCoeff = Multiset.sum (Multiset.map (fun (i : ι) ↦ (f i).nextCoeff) (a ::ₘ t))

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons,
      Monic.nextCoeff_mul, ih]

Premises used: Multiset.map_cons, Multiset.prod_cons, Polynomial.Monic.nextCoeff_mul, Multiset.sum_cons
-- Module: Mathlib.Algebra.Polynomial.Monic
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
⊢ ∀ i ∈ t, (f i).Monic

Tactic:
fun i hi => ht i (Multiset.mem_cons_of_mem hi)

Premises used: Multiset.mem_cons_of_mem
-- Module: Mathlib.Algebra.Polynomial.Monic
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
⊢ (f a).Monic

Tactic:
ht a (Multiset.mem_cons_self _ _)

Premises used: Multiset.mem_cons_self
-- Module: Mathlib.Algebra.Polynomial.Monic
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 t).prod.Monic

Tactic:
monic_multiset_prod_of_monic _ _ fun b bs => ht _ (Multiset.mem_cons_of_mem bs)

Premises used: Polynomial.monic_multiset_prod_of_monic, Multiset.mem_cons_of_mem
-- Module: Mathlib.Algebra.Polynomial.Monic
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
⊢ ∀ i ∈ t, (f i).Monic

Tactic:
exacts [fun i hi => ht i (Multiset.mem_cons_of_mem hi), ht a (Multiset.mem_cons_self _ _),
      monic_multiset_prod_of_monic _ _ fun b bs => ht _ (Multiset.mem_cons_of_mem bs)]

Premises used: Polynomial.monic_multiset_prod_of_monic, Multiset.mem_cons_of_mem, Multiset.mem_cons_self
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
s : Finset ι
f : ι → R[X]
h : ∀ i ∈ s, (f i).Monic
⊢ Eq.{u + 1} (α := R) (nextCoeff (∏ i ∈ s, f i)) (∑ i ∈ s, (f i).nextCoeff)

Tactic:
Monic.nextCoeff_multiset_prod s.1 f h

Premises used: Finset.val, Finset.prod, Polynomial.Monic.nextCoeff_multiset_prod, Finset.sum
-- Module: Mathlib.Algebra.Polynomial.Monic
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

Tactic:
⟨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 _)⟩⟩

Premises used: Polynomial.C, HMul.hMul, IsUnit.of_mul_eq_one, Function.comp, Irreducible.mk, Polynomial.leadingCoeff, Or.symm, Irreducible.isUnit_or_isUnit, Iff.intro, Or.imp, Polynomial.Monic.eq_one_of_isUnit, Eq.symm, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Monic
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
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
⊢ Irreducible p ↔ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1

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 _)⟩⟩
-- Module: Mathlib.Algebra.Polynomial.Monic
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
refine_1₅ : p.leadingCoeff = 1
refine_1₆ refine_1₇ refine_1₈ refine_1₉ : p.Monic
⊢ (HMul.hMul (β := R[X]) g ((C : (a : R) → R[X]) f.leadingCoeff : R[X])).Monic

Tactic:
rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, mul_comm, ← hfg, ← Monic]

Premises used: Polynomial.leadingCoeff_mul, Polynomial.Monic, mul_comm, Polynomial.leadingCoeff_C
-- Module: Mathlib.Algebra.Polynomial.Monic
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
refine_2₄ : p.leadingCoeff = 1
refine_2₅ refine_2₆ refine_2₇ refine_2₈ : p.Monic
⊢ (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) g.leadingCoeff : R[X])).Monic

Tactic:
rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, ← hfg, ← Monic]

Premises used: Polynomial.leadingCoeff_mul, Polynomial.Monic, Polynomial.leadingCoeff_C
-- Module: Mathlib.Algebra.Polynomial.Monic
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
refine_3₈ refine_3₉ : p = 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

Tactic:
rw [mul_mul_mul_comm, ← C_mul, ← leadingCoeff_mul, ← hfg, hp.leadingCoeff, C_1, mul_one,
      mul_comm, ← hfg]

Premises used: Polynomial.C_1, mul_mul_mul_comm, Polynomial.leadingCoeff_mul, Polynomial.C_mul, mul_comm, Polynomial.Monic.leadingCoeff, mul_one
-- Module: Mathlib.Algebra.Polynomial.Monic
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
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
⊢ 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
-- Module: Mathlib.Algebra.Polynomial.Monic
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

Tactic:
simp [hp1]
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
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
⊢ Irreducible p ↔ p ≠ 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]

Premises used: Polynomial.irreducible_of_monic, and_iff_right