awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
ha : p.leadingCoeff⁻¹ ≠ 0
hp2₁ : 2 ≤ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).natDegree
hp3₁ : (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).natDegree ≤ 3
⊢ Irreducible p ↔ p.roots = 0

Tactic:
rw [← irreducible_mul_leadingCoeff_inv,
      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_roots_eq_zero_of_degree_le_three,
      mul_comm, roots_C_mul]

Premises used: Polynomial.roots_C_mul, Polynomial.irreducible_mul_leadingCoeff_inv, Polynomial.monic_mul_leadingCoeff_inv, mul_comm, Polynomial.Monic.irreducible_iff_roots_eq_zero_of_degree_le_three
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ p.leadingCoeff⁻¹ ≠ 0

Tactic:
inv_ne_zero (leadingCoeff_ne_zero.mpr hp0)

Premises used: Iff.mpr, Polynomial.leadingCoeff_ne_zero, inv_ne_zero
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ p.leadingCoeff⁻¹ ≠ 0

Tactic:
exact inv_ne_zero (leadingCoeff_ne_zero.mpr hp0)

Premises used: Iff.mpr, Polynomial.leadingCoeff_ne_zero, inv_ne_zero
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp2₁ hp2₂ hp2₃ hp2₄ : 2 ≤ p.natDegree
⊢ 2 ≤ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).natDegree

Tactic:
rwa [natDegree_mul_leadingCoeff_inv _ hp0]

Premises used: Polynomial.natDegree_mul_leadingCoeff_inv
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp3₁ hp3₂ hp3₃ hp3₄ : p.natDegree ≤ 3
⊢ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).natDegree ≤ 3

Tactic:
rwa [natDegree_mul_leadingCoeff_inv _ hp0]

Premises used: Polynomial.natDegree_mul_leadingCoeff_inv
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : Membership.mem (γ := Finset ℕ) (Finset.Icc 1 3) p.natDegree
hnot : ∀ (x : K), ¬p.IsRoot x
⊢ 1 ≤ p.natDegree ∧ p.natDegree ≤ 3

Tactic:
rw [Finset.mem_Icc] at hdeg

Premises used: Finset.mem_Icc
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : Membership.mem (γ := Finset ℕ) (Finset.Icc 1 3) p.natDegree
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg₁ : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
⊢ ∀ (x : K), ¬p.IsRoot x

Tactic:
rw [Finset.mem_Icc] at hdeg

Premises used: Finset.mem_Icc
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
pos : ∀ (hdeg2 : 2 ≤ p.natDegree), Irreducible p
neg : ∀ (hdeg2 : ¬2 ≤ p.natDegree), Irreducible p
⊢ Irreducible p

Tactic:
by_cases hdeg2 : 2 ≤ p.natDegree

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : 2 ≤ p.natDegree
pos : p.roots = 0
⊢ Irreducible p

Tactic:
rw [Polynomial.irreducible_iff_roots_eq_zero_of_degree_le_three hdeg2 hdeg.2]

Premises used: Polynomial.irreducible_iff_roots_eq_zero_of_degree_le_three, And.right
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : 2 ≤ p.natDegree
pos : ∀ (x : K), x ∉ p.roots
⊢ p.roots = 0

Tactic:
apply Multiset.eq_zero_of_forall_notMem

Premises used: Multiset.eq_zero_of_forall_notMem
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : 2 ≤ p.natDegree
⊢ ∀ (x : K), x ∉ p.roots

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
neg : p.degree = 1
⊢ Irreducible p

Tactic:
apply Polynomial.irreducible_of_degree_eq_one

Premises used: Polynomial.irreducible_of_degree_eq_one
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
⊢ LT.lt (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
neg : p.natDegree = 1
⊢ p.degree = 1

Tactic:
rw [← Nat.cast_one, Polynomial.degree_eq_iff_natDegree_eq_of_pos (by simp)]

Premises used: Polynomial.degree_eq_iff_natDegree_eq_of_pos, Nat.cast_one
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
rwa : ∀ (hdeg2 : p.natDegree < 2), p.natDegree ≤ 1
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hdeg2 : p.natDegree ≤ 1), p.natDegree ≤ 1
⊢ p.natDegree ≤ 1

Tactic:
rwa [not_le, Nat.lt_succ_iff] at hdeg2

Premises used: not_le, Nat.lt_succ_iff
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
⊢ p.natDegree = 1

Tactic:
exact le_antisymm (by rwa [not_le, Nat.lt_succ_iff] at hdeg2) hdeg.1

Premises used: le_antisymm, And.left
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
a : R
⊢ Splits.{u_1} (R := R) ((C : (a : R) → R[X]) a)

Tactic:
Submonoid.mem_closure_of_mem (Set.mem_union_left _ ⟨a, rfl⟩)

Premises used: Exists.intro, Set.mem_union_left, Polynomial.Splits, Submonoid.mem_closure_of_mem, rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
⊢ Splits.{u_1} (R := R) 0

Tactic:
simpa using Splits.C (0 : R)

Premises used: OfNat.ofNat, Polynomial.Splits.C
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
⊢ Splits.{u_1} (R := R) 1

Tactic:
Splits.C (1 : R)

Premises used: OfNat.ofNat, Polynomial.Splits.C
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
a : R
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).Splits

Tactic:
Submonoid.mem_closure_of_mem (Set.mem_union_right _ ⟨a, rfl⟩)

Premises used: Set.mem_union_right, Exists.intro, Polynomial.Splits, Submonoid.mem_closure_of_mem, rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
⊢ Splits.{u_1} (R := R) X

Tactic:
simpa using Splits.X_add_C (0 : R)

Premises used: Polynomial.Splits.X_add_C, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
f g : R[X]
hf : f.Splits
hg : g.Splits
⊢ (f * g).Splits

Tactic:
mul_mem hf hg

Premises used: Polynomial.Splits, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.Splits
a : R
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f).Splits

Tactic:
(Splits.C a).mul hf

Premises used: Polynomial.Splits.C, Polynomial.Splits.mul
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
l : List R[X]
h : ∀ f ∈ l, f.Splits
⊢ l.prod.Splits

Tactic:
list_prod_mem h

Premises used: list_prod_mem, Set.Mem, Polynomial.Splits
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.Splits
n : ℕ
⊢ (f ^ n).Splits

Tactic:
pow_mem hf n

Premises used: pow_mem, Polynomial.Splits
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ (HPow.hPow (α := R[X]) X n).Splits

Tactic:
Splits.X.pow n

Premises used: Polynomial.Splits.X, Polynomial.Splits.pow
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
a : R
n : ℕ
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).Splits

Tactic:
(Splits.X_pow n).C_mul a

Premises used: Polynomial.Splits.X_pow, Polynomial.Splits.C_mul
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
⊢ Splits.{u_1} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a)

Tactic:
simp [← C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.Splits
S : Type u_2
inst_1 : Semiring S
i : R →+* S
mem :
  ∀ (x : R[X]),
    Membership.mem (γ := Set R[X])
        ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
          {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
        x →
      (map i x).Splits
one : (map i 1).Splits
mul :
  ∀ (x y : R[X]),
    Membership.mem (γ := Submonoid R[X])
        (Submonoid.closure
          ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
            {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
        x →
      Membership.mem (γ := Submonoid R[X])
          (Submonoid.closure
            ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
              {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
          y →
        (map i x).Splits → (map i y).Splits → (map i (x * y)).Splits
⊢ (map i f).Splits

Tactic:
induction hf using Submonoid.closure_induction
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
S : Type u_2
inst_1 : Semiring S
i : R →+* S
x : R[X]
h :
  Membership.mem (γ := Set R[X])
    ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
      {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
    x
⊢ (map i x).Splits

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
S : Type u_2
inst_1 : Semiring S
i : R →+* S
⊢ (map i 1).Splits

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
S : Type u_2
inst_1 : Semiring S
i : R →+* S
x y : R[X]
hx :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    x
hy :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    y
h : (map i x).Splits
h_1 : (map i y).Splits
⊢ (map i (x * y)).Splits

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.natDegree = 0
rw : Splits.{u_1} (R := R) ((C : (a : R) → R[X]) (⋯.choose (p := fun (x : R) ↦ (C : (a : R) → R[X]) x = f)))
⊢ f.Splits

Tactic:
rw [← (natDegree_eq_zero.mp hf).choose_spec]

Premises used: Exists.choose_spec, Iff.mp, Polynomial.natDegree_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.natDegree = 0
⊢ Splits.{u_1} (R := R) ((C : (a : R) → R[X]) (⋯.choose (p := fun (x : R) ↦ (C : (a : R) → R[X]) x = f)))

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.degree ≤ 0
⊢ f.Splits

Tactic:
splits_of_natDegree_eq_zero (natDegree_eq_zero_iff_degree_le_zero.mpr hf)

Premises used: Iff.mpr, Polynomial.splits_of_natDegree_eq_zero, Polynomial.natDegree_eq_zero_iff_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
f : R[X]
hf : IsUnit f
⊢ f.Splits

Tactic:
splits_of_natDegree_eq_zero (natDegree_eq_zero_of_isUnit hf)

Premises used: Polynomial.splits_of_natDegree_eq_zero, Polynomial.natDegree_eq_zero_of_isUnit
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.natDegree ≤ 1
h : Invertible f.leadingCoeff
obtain :
  ∀ (a b : R)
    (hf :
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
            ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
        1)
    (h :
      Invertible
        (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
            ((C : (a : R) → R[X]) b : R[X])).leadingCoeff),
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).Splits
⊢ f.Splits

Tactic:
obtain ⟨a, b, rfl⟩ := exists_eq_X_add_C_of_natDegree_le_one hf

Premises used: Polynomial.exists_eq_X_add_C_of_natDegree_le_one, rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
a b : R
hf :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
    1
h :
  Invertible
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).leadingCoeff
inl :
  ∀
    (hf :
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 0) X)
            ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
        1)
    (h :
      Invertible
        (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 0) X)
            ((C : (a : R) → R[X]) b : R[X])).leadingCoeff),
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 0) X) ((C : (a : R) → R[X]) b : R[X])).Splits
inr :
  ∀ (ha : a ≠ 0),
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).Splits
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) b : R[X])).Splits

Tactic:
rcases eq_or_ne a 0 with rfl | ha

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
b : R
hf :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 0) X) ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
    1
h :
  Invertible
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 0) X)
        ((C : (a : R) → R[X]) b : R[X])).leadingCoeff
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 0) X) ((C : (a : R) → R[X]) b : R[X])).Splits

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
a b : R
hf :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
    1
h :
  Invertible
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).leadingCoeff
ha : a ≠ 0
⊢ Invertible a

Tactic:
simpa [leadingCoeff, ha] using h

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
a b : R
hf :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
    1
h :
  Invertible
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).leadingCoeff
ha : a ≠ 0
inr :
  ∀ (h : Invertible a),
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).Splits
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) b : R[X])).Splits

Tactic:
replace h : Invertible a := by simpa [leadingCoeff, ha] using h
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
a b : R
hf :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
    1
ha : a ≠ 0
h : Invertible a
inr :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HAdd.hAdd (α := R[X]) (β := R[X]) X
        ((C : (a : R) → R[X]) (@Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * b) : R[X]))).Splits
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) b : R[X])).Splits

Tactic:
rw [← mul_invOf_cancel_left a b, C_mul, ← mul_add]

Premises used: mul_invOf_cancel_left, Polynomial.C_mul, mul_add
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
a b : R
hf :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
    1
ha : a ≠ 0
h : Invertible a
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HAdd.hAdd (α := R[X]) (β := R[X]) X
        ((C : (a : R) → R[X]) (@Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * b) : R[X]))).Splits

Tactic:
(Splits.C a).mul (Splits.X_add_C _)

Premises used: Polynomial.Splits.X_add_C, Polynomial.Splits.C, Polynomial.Splits.mul
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
a b : R
hf :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
    1
ha : a ≠ 0
h : Invertible a
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HAdd.hAdd (α := R[X]) (β := R[X]) X
        ((C : (a : R) → R[X]) (@Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * b) : R[X]))).Splits

Tactic:
exact (Splits.C a).mul (Splits.X_add_C _)

Premises used: Polynomial.Splits.X_add_C, Polynomial.Splits.C, Polynomial.Splits.mul
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.degree ≤ 1
h : Invertible f.leadingCoeff
⊢ f.Splits

Tactic:
splits_of_natDegree_le_one_of_invertible (natDegree_le_of_degree_le hf) h

Premises used: Polynomial.splits_of_natDegree_le_one_of_invertible, Polynomial.natDegree_le_of_degree_le
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.natDegree ≤ 1
h : f.Monic
⊢ f.Splits

Tactic:
splits_of_natDegree_le_one_of_invertible hf (h.leadingCoeff ▸ invertibleOne)

Premises used: Polynomial.splits_of_natDegree_le_one_of_invertible, Eq.rec, Polynomial.Monic.leadingCoeff, Eq.symm, invertibleOne
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.degree ≤ 1
h : f.Monic
⊢ f.Splits

Tactic:
splits_of_natDegree_le_one_of_monic (natDegree_le_of_degree_le hf) h

Premises used: Polynomial.natDegree_le_of_degree_le, Polynomial.splits_of_natDegree_le_one_of_monic
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
m : Multiset R[X]
hm : ∀ f ∈ m, f.Splits
⊢ m.prod.Splits

Tactic:
multiset_prod_mem _ hm

Premises used: multiset_prod_mem, Polynomial.Splits
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
s : Finset ι
h : ∀ i ∈ s, (f i).Splits
⊢ Splits.{u_1} (R := R) (∏ i ∈ s, f i)

Tactic:
prod_mem h

Premises used: Polynomial.Splits, prod_mem
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r i : R
⊢ (HAdd.hAdd (β := R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))
      ((C : (a : R) → R[X]) i : R[X])).Splits

Tactic:
simpa [add_assoc] using Splits.X_add_C (r + i)

Premises used: add_assoc, Polynomial.Splits.X_add_C, HAdd.hAdd
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
⊢ ∀ (i : R),
    (HAdd.hAdd (β := R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))
        ((C : (a : R) → R[X]) i : R[X])).Splits

Tactic:
have (i : _) : (X + C r + C i).Splits := by simpa [add_assoc] using Splits.X_add_C (r + i)
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
this :
  ∀ (i : R),
    (HAdd.hAdd (β := R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))
        ((C : (a : R) → R[X]) i : R[X])).Splits
mem :
  ∀ (x : R[X]),
    Membership.mem (γ := Set R[X])
        ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
          {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
        x →
      Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) x)
one : Splits (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) 1)
mul :
  ∀ (x y : R[X]),
    Membership.mem (γ := Submonoid R[X])
        (Submonoid.closure
          ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
            {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
        x →
      Membership.mem (γ := Submonoid R[X])
          (Submonoid.closure
            ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
              {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
          y →
        Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) x) →
          Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) y) →
            Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) (x * y))
⊢ Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) p)

Tactic:
induction hp using Submonoid.closure_induction
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
this :
  ∀ (i : R),
    (HAdd.hAdd (β := R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))
        ((C : (a : R) → R[X]) i : R[X])).Splits
x : R[X]
h :
  Membership.mem (γ := Set R[X])
    ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
      {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
    x
⊢ Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) x)

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
this :
  ∀ (i : R),
    (HAdd.hAdd (β := R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))
        ((C : (a : R) → R[X]) i : R[X])).Splits
⊢ Splits (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) 1)

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r : R
this :
  ∀ (i : R),
    (HAdd.hAdd (β := R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))
        ((C : (a : R) → R[X]) i : R[X])).Splits
x y : R[X]
hx :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    x
hy :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    y
h : Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) x)
h_1 : Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) y)
⊢ Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) (x * y))

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
⊢ f.Splits ↔
    ∃ (m : Multiset R),
      f =
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
          (Multiset.prod
              (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
            R[X])

Tactic:
⟨fun hf ↦ ?_, ?_⟩

Premises used: Iff.intro