awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : DivisionSemiring 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
neg :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (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_inv_cancel_left₀ ha b, C_mul, ← mul_add]

Premises used: mul_inv_cancel_left₀, Polynomial.C_mul, mul_add
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : DivisionSemiring 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
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (a⁻¹ * b) : R[X]))).Splits

Tactic:
(X_add_C (a⁻¹ * b)).C_mul a

Premises used: HMul.hMul, Polynomial.Splits.X_add_C, Inv.inv, Polynomial.Splits.C_mul
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : DivisionSemiring 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
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (a⁻¹ * b) : R[X]))).Splits

Tactic:
exact (X_add_C (a⁻¹ * b)).C_mul a

Premises used: HMul.hMul, Polynomial.Splits.X_add_C, Inv.inv, Polynomial.Splits.C_mul
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : DivisionSemiring R
f : R[X]
hf : f.natDegree = 1
⊢ f.Splits

Tactic:
of_natDegree_le_one hf.le

Premises used: Eq.le, Polynomial.Splits.of_natDegree_le_one
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : DivisionSemiring R
f : R[X]
hf : f.degree ≤ 1
⊢ f.Splits

Tactic:
of_natDegree_le_one (natDegree_le_of_degree_le hf)

Premises used: Polynomial.Splits.of_natDegree_le_one, Polynomial.natDegree_le_of_degree_le
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : DivisionSemiring R
f : R[X]
hf : f.degree = 1
⊢ f.Splits

Tactic:
of_degree_le_one hf.le

Premises used: Eq.le, Polynomial.Splits.of_degree_le_one
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
f : R[X]
i : R →+* S
hf : (map i f).Splits
hi : ∀ a ∈ (map i f).roots, Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) i) a
⊢ f.Splits

Tactic:
hf.of_splits_map_of_injective i.injective hi

Premises used: RingHom.injective, Polynomial.Splits.of_splits_map_of_injective
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
f : R[X]
hf : f.Splits
i : R →+* S
⊢ (map i f).roots = Multiset.map (⇑i : (a : R) → S) f.roots

Tactic:
hf.roots_map_of_injective i.injective

Premises used: Polynomial.Splits.roots_map_of_injective, RingHom.injective
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
f : R[X]
hf : f.Splits
hf0 : f ≠ 0
i : R →+* S
x : S
hx : (map i f).IsRoot x
⊢ ∃ a ∈ f.roots, (i : (a : R) → S) a = x

Tactic:
rw [← mem_roots (map_ne_zero hf0), hf.roots_map, Multiset.mem_map] at hx

Premises used: Multiset.mem_map, Polynomial.Splits.roots_map, Polynomial.mem_roots, Polynomial.map_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
f : R[X]
hf : f.Splits
hf0 : f ≠ 0
i : R →+* S
x : S
hx : ∃ a ∈ f.roots, (i : (a : R) → S) a = x
obtain :
  ∀ (x_1 : R) (hx : (i : (a : R) → S) x_1 = x), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) i) x
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) i) x

Tactic:
obtain ⟨x, -, hx⟩ := hx
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
f : R[X]
hf : f.Splits
hf0 : f ≠ 0
i : R →+* S
x_1 : S
x : R
hx : (i : (a : R) → S) x = x_1
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) i) x_1

Tactic:
⟨x, hx⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
f : R[X]
hf : f.Splits
hf0 : f ≠ 0
i : R →+* S
x_1 : S
x : R
hx : (i : (a : R) → S) x = x_1
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) i) x_1

Tactic:
exact ⟨x, hx⟩
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
f : R[X]
hf : Splits (map (algebraMap R S) f)
x : S
⊢ (aeval x : (a : R[X]) → S) f =
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) f.leadingCoeff : S)
      (Multiset.prod (Multiset.map (fun (x_1 : S) ↦ x - x_1) (f.aroots S)) : S)

Tactic:
simp [← eval_map_algebraMap, hf.eval_eq_prod_roots]

Premises used: Polynomial.Splits.eval_eq_prod_roots, Polynomial.eval_map_algebraMap
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Field A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : IsDomain B
inst_5 : Algebra R B
f : R[X]
inst_6 : Algebra A B
inst_7 : IsScalarTower R A B
hf : Splits (map (algebraMap R A) f)
rw : Multiset.map (⇑(algebraMap A B) : (a : A) → B) (f.aroots A) = aroots (map (algebraMap R A) f) B
rw₁ :
  Multiset.map (⇑(algebraMap A B) : (a : A) → B) (roots (map (algebraMap R A) f)) = aroots (map (algebraMap R A) f) B
rw₂ :
  Multiset.map (⇑(algebraMap A B) : (a : A) → B) (roots (map (algebraMap R A) f)) =
    roots (map (algebraMap A B) (map (algebraMap R A) f))
rw₃ rw₄ :
  Eq.{u_3 + 1} (α := Multiset B) (Multiset.map (⇑(algebraMap A B) : (a : A) → B) (roots (map (algebraMap R A) f)))
    (Multiset.map (⇑(algebraMap A B) : (a : A) → B) (roots (map (algebraMap R A) f)))
⊢ Multiset.map (⇑(algebraMap A B) : (a : A) → B) (f.aroots A) = f.aroots B

Tactic:
rw [← aroots_map B A, aroots, aroots, hf.roots_map]

Premises used: Polynomial.aroots_map, Polynomial.Splits.roots_map, Polynomial.aroots
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Field A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : IsDomain B
inst_5 : Algebra R B
f : R[X]
hf : Splits (map (algebraMap R A) f)
g : A →ₐ[R] B
rw : (⇑g : (a : A) → B) '' (↑(f.aroots A).toFinset : Set A) = f.rootSet B
rw₁ : (↑(Finset.image (⇑g : (a : A) → B) (f.aroots A).toFinset) : Set B) = f.rootSet B
rw₂ : (↑(Multiset.toFinset (Multiset.map (⇑g : (a : A) → B) (f.aroots A))) : Set B) = f.rootSet B
rw₃ : (↑(Multiset.toFinset (Multiset.map (⇑(↑g : A →+* B) : (a : A) → B) (f.aroots A))) : Set B) = f.rootSet B
rw₄ : (↑(roots (map (↑g : A →+* B) (map (algebraMap R A) f))).toFinset : Set B) = f.rootSet B
rw₅ :
  (↑(roots (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A)) f)).toFinset :
      Set B) =
    f.rootSet B
rw₆ : (↑(roots (map (algebraMap R B) f)).toFinset : Set B) = f.rootSet B
rw₇ rw₈ : f.rootSet B = f.rootSet B
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B

Tactic:
rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← g.coe_toRingHom,
    ← hf.roots_map, map_map, g.comp_algebraMap, ← rootSet]

Premises used: AlgHom.coe_toRingHom, AlgHom.comp_algebraMap, Polynomial.rootSet, Finset.coe_image, Polynomial.Splits.roots_map, Multiset.toFinset_map, Polynomial.map_map
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Field A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : IsDomain B
inst_5 : Algebra R B
f : R[X]
hf : Splits (map (algebraMap R A) f)
g : A →ₐ[R] B
rw : (⇑g : (a : A) → B) '' (↑(f.aroots A).toFinset : Set A) = f.rootSet B
rw₁ : (↑(Finset.image (⇑g : (a : A) → B) (f.aroots A).toFinset) : Set B) = f.rootSet B
rw₂ : (↑(Multiset.toFinset (Multiset.map (⇑g : (a : A) → B) (f.aroots A))) : Set B) = f.rootSet B
rw₃ : (↑(Multiset.toFinset (Multiset.map (⇑(↑g : A →+* B) : (a : A) → B) (f.aroots A))) : Set B) = f.rootSet B
rw₄ : (↑(roots (map (↑g : A →+* B) (map (algebraMap R A) f))).toFinset : Set B) = f.rootSet B
rw₅ :
  (↑(roots (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A)) f)).toFinset :
      Set B) =
    f.rootSet B
rw₆ : (↑(roots (map (algebraMap R B) f)).toFinset : Set B) = f.rootSet B
rw₇ rw₈ : f.rootSet B = f.rootSet B
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B

Tactic:
classical
  rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← g.coe_toRingHom,
    ← hf.roots_map, map_map, g.comp_algebraMap, ← rootSet]

Premises used: AlgHom.coe_toRingHom, AlgHom.comp_algebraMap, Polynomial.rootSet, Finset.coe_image, Polynomial.Splits.roots_map, Multiset.toFinset_map, Polynomial.map_map
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Field A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : IsDomain B
inst_5 : Algebra R B
f : R[X]
hf : Splits (map (algebraMap R A) f)
g : A →ₐ[R] B
rw :
  Subalgebra.map g (Algebra.adjoin R (f.rootSet A)) = Subalgebra.map g ⊤ ↔
    Eq (α := Subalgebra R A) (Algebra.adjoin R (f.rootSet A)) ⊤
⊢ Algebra.adjoin R (f.rootSet B) = g.range ↔ Eq (α := Subalgebra R A) (Algebra.adjoin R (f.rootSet A)) ⊤

Tactic:
rw [← hf.image_rootSet g, Algebra.adjoin_image, ← Algebra.map_top]

Premises used: Polynomial.Splits.image_rootSet, Algebra.adjoin_image, Algebra.map_top
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Field A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : IsDomain B
inst_5 : Algebra R B
f : R[X]
hf : Splits (map (algebraMap R A) f)
g : A →ₐ[R] B
⊢ Subalgebra.map g (Algebra.adjoin R (f.rootSet A)) = Subalgebra.map g ⊤ ↔
    Eq (α := Subalgebra R A) (Algebra.adjoin R (f.rootSet A)) ⊤

Tactic:
(Subalgebra.map_injective g.injective).eq_iff

Premises used: Function.Injective.eq_iff, RingHom.injective, Subalgebra.map_injective, AlgHom.toRingHom
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Field A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : IsDomain B
inst_5 : Algebra R B
f : R[X]
hf : Splits (map (algebraMap R A) f)
g : A →ₐ[R] B
⊢ Subalgebra.map g (Algebra.adjoin R (f.rootSet A)) = Subalgebra.map g ⊤ ↔
    Eq (α := Subalgebra R A) (Algebra.adjoin R (f.rootSet A)) ⊤

Tactic:
exact (Subalgebra.map_injective g.injective).eq_iff

Premises used: Function.Injective.eq_iff, RingHom.injective, Subalgebra.map_injective, AlgHom.toRingHom
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f g : R[X]
hp : f.Splits
hp0 : f ≠ 0
hq : f.roots ≤ g.roots
rw :
  Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) ∣
    g
⊢ f ∣ g

Tactic:
rw [hp.eq_prod_roots, C_mul_dvd (leadingCoeff_ne_zero.2 hp0)]

Premises used: Iff.mpr, Polynomial.Splits.eq_prod_roots, Polynomial.C_mul_dvd, Polynomial.leadingCoeff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f g : R[X]
hp : f.Splits
hp0 : f ≠ 0
hq : f.roots ≤ g.roots
⊢ Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) ∣
    g

Tactic:
(Multiset.prod_dvd_prod_of_le (Multiset.map_le_map hq)).trans
    (prod_multiset_X_sub_C_dvd _)

Premises used: Multiset.prod_dvd_prod_of_le, Polynomial.prod_multiset_X_sub_C_dvd, Multiset.map_le_map, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f g : R[X]
hp : f.Splits
hp0 : f ≠ 0
hq : f.roots ≤ g.roots
⊢ Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) ∣
    g

Tactic:
exact (Multiset.prod_dvd_prod_of_le (Multiset.map_le_map hq)).trans
    (prod_multiset_X_sub_C_dvd _)

Premises used: Multiset.prod_dvd_prod_of_le, Polynomial.prod_multiset_X_sub_C_dvd, Multiset.map_le_map, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f g : R[X]
hf : f.Splits
hf0 : f ≠ 0
hg0 : g ≠ 0
⊢ f ∣ g ↔ f.roots ≤ g.roots

Tactic:
⟨roots.le_of_dvd hg0, hf.dvd_of_roots_le_roots hf0⟩

Premises used: Polynomial.roots.le_of_dvd, Iff.intro, Polynomial.Splits.dvd_of_roots_le_roots
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f g : R[X]
hf : f.Splits
hg : g.natDegree ≤ 1
inl : ∀ (hg : natDegree.{u_1} (R := R) 0 ≤ 1), (f.comp 0).Splits
inr : ∀ (hg0 : g ≠ 0), (f.comp g).Splits
⊢ (f.comp g).Splits

Tactic:
rcases eq_or_ne g 0 with rfl | hg0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : f.Splits
hg : natDegree.{u_1} (R := R) 0 ≤ 1
⊢ (f.comp 0).Splits

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f g : R[X]
hf : f.Splits
hg : g.natDegree ≤ 1
hg0 : g ≠ 0
⊢ (f.comp g).Splits

Tactic:
Splits.comp_of_natDegree_le_one_of_invertible hf hg
      (invertibleOfNonzero (leadingCoeff_ne_zero.mpr hg0))

Premises used: Iff.mpr, Polynomial.leadingCoeff_ne_zero, invertibleOfNonzero, Polynomial.Splits.comp_of_natDegree_le_one_of_invertible
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f g : R[X]
hf : f.Splits
hg : g.natDegree ≤ 1
hg0 : g ≠ 0
⊢ (f.comp g).Splits

Tactic:
exact Splits.comp_of_natDegree_le_one_of_invertible hf hg
      (invertibleOfNonzero (leadingCoeff_ne_zero.mpr hg0))

Premises used: Iff.mpr, Polynomial.leadingCoeff_ne_zero, invertibleOfNonzero, Polynomial.Splits.comp_of_natDegree_le_one_of_invertible
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f g : R[X]
hf : f.Splits
hg : g.degree ≤ 1
⊢ (f.comp g).Splits

Tactic:
hf.comp_of_natDegree_le_one (natDegree_le_of_degree_le hg)

Premises used: Polynomial.Splits.comp_of_natDegree_le_one, Polynomial.natDegree_le_of_degree_le
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f g : R[X]
hg : g.natDegree = 1
⊢ f.Splits ↔ (f.comp g).Splits

Tactic:
⟨fun hf ↦ hf.comp_of_natDegree_le_one hg.le, fun hf ↦ ?_⟩

Premises used: Eq.le, Polynomial.Splits.comp_of_natDegree_le_one, Iff.intro
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f g : R[X]
hg : g.natDegree = 1
refine : ∀ (hf : (f.comp g).Splits), f.Splits
⊢ f.Splits ↔ (f.comp g).Splits

Tactic:
refine ⟨fun hf ↦ hf.comp_of_natDegree_le_one hg.le, fun hf ↦ ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f g : R[X]
hg : g.natDegree = 1
hf : (f.comp g).Splits
obtain :
  ∀ (a b : R)
    (hg :
      (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)
    (hf :
      (f.comp
          (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
⊢ f.Splits

Tactic:
obtain ⟨a, b, rfl⟩ := exists_eq_X_add_C_of_natDegree_le_one hg.le

Premises used: Eq.le, Polynomial.exists_eq_X_add_C_of_natDegree_le_one, rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f : R[X]
a b : R
hg :
  (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
hf :
  (f.comp
      (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
contrapose! :
  ∀ (hg : 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])).natDegree ≠
      1
⊢ a ≠ 0

Tactic:
contrapose! hg
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f : R[X]
a b : R
hf :
  (f.comp
      (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
hg : 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])).natDegree ≠
    1

Tactic:
simp [hg]
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f : R[X]
a b : R
hg :
  (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
hf :
  (f.comp
      (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
⊢ a ≠ 0

Tactic:
have ha : a ≠ 0 := by contrapose! hg; simp [hg]
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f : R[X]
a b : R
hg :
  (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
hf :
  (f.comp
      (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
ha : a ≠ 0
simp :
  f =
    f.comp
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))))
        ((C : (a : R) → R[X]) b : R[X]))
⊢ f =
    (f.comp
          (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]))).comp
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))

Tactic:
simp only [comp_assoc, add_comp, mul_comp, C_comp, X_comp]

Premises used: Polynomial.comp_assoc, Polynomial.X_comp, Polynomial.add_comp, Polynomial.C_comp, Polynomial.mul_comp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f : R[X]
a b : R
hg :
  (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
hf :
  (f.comp
      (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
ha : a ≠ 0
rw :
  f =
    f.comp
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) *
          HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
        ((C : (a : R) → R[X]) b : R[X]))
rw₁ :
  f =
    f.comp
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a⁻¹) : R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))
        ((C : (a : R) → R[X]) b : R[X]))
rw₂ :
  f =
    f.comp
      (HAdd.hAdd (β := R[X])
        ((C : (a : R) → R[X]) 1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
        ((C : (a : R) → R[X]) b : R[X]))
rw₃ :
  f =
    f.comp
      (HAdd.hAdd (β := R[X]) (1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
        ((C : (a : R) → R[X]) b : R[X]))
rw₄ :
  f =
    f.comp
      (HAdd.hAdd (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
        ((C : (a : R) → R[X]) b : R[X]))
rw₅ : f = f.comp X
rw₆ rw₇ : f = f
⊢ f =
    f.comp
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))))
        ((C : (a : R) → R[X]) b : R[X]))

Tactic:
rw [← mul_assoc, ← C_mul, mul_inv_cancel₀ ha, C_1, one_mul, sub_add_cancel, comp_X]

Premises used: Polynomial.C_1, mul_inv_cancel₀, mul_assoc, Polynomial.comp_X, Polynomial.C_mul, sub_add_cancel, one_mul
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f : R[X]
a b : R
hg :
  (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
hf :
  (f.comp
      (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
ha : a ≠ 0
⊢ f =
    (f.comp
          (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]))).comp
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))

Tactic:
have : f = (f.comp (C a * X + C b)).comp ((C a⁻¹ * (X - C b))) := by
    simp only [comp_assoc, add_comp, mul_comp, C_comp, X_comp]
    rw [← mul_assoc, ← C_mul, mul_inv_cancel₀ ha, C_1, one_mul, sub_add_cancel, comp_X]
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f : R[X]
a b : R
hg :
  (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
hf :
  (f.comp
      (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
ha : a ≠ 0
this :
  f =
    (f.comp
          (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]))).comp
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))
rw :
  ((f.comp
          (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]))).comp
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))).Splits
⊢ f.Splits

Tactic:
rw [this]
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f : R[X]
a b : R
hg :
  (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
hf :
  (f.comp
      (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
ha : a ≠ 0
this :
  f =
    (f.comp
          (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]))).comp
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))
⊢ ((f.comp
          (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]))).comp
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))).Splits

Tactic:
Splits.comp_of_natDegree_le_one hf ?_

Premises used: Polynomial.Splits.comp_of_natDegree_le_one