awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
S : Type u_4
inst_1 : CommRing S
inst_2 : IsDomain S
i : R →+* S
hi : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑i : (a : R) → S)
hf : (map i f).Splits
j : (a : S) → a ∈ (map i f).roots → R
hj : ∀ (a : S) (a_1 : a ∈ (map i f).roots), (i : (a : R) → S) (j a a_1) = a
⊢ ∃ (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) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
          R[X])

Tactic:
⟨(f.map i).roots.pmap j fun _ ↦ id, map_injective i hi ?_⟩

Premises used: Polynomial.roots, id, Polynomial.map_injective, Multiset.pmap, Exists.intro, Polynomial.map
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
S : Type u_4
inst_1 : CommRing S
inst_2 : IsDomain S
i : R →+* S
hi : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑i : (a : R) → S)
hf : (map i f).Splits
j : (a : S) → a ∈ (map i f).roots → R
hj : ∀ (a : S) (a_1 : a ∈ (map i f).roots), (i : (a : R) → S) (j a a_1) = a
refine :
  map i f =
    map i
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
              (Multiset.pmap (p := Membership.mem (map i f).roots) j (map i f).roots ⋯)) :
          R[X]))
⊢ ∃ (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) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
          R[X])

Tactic:
refine ⟨(f.map i).roots.pmap j fun _ ↦ id, map_injective i hi ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
S : Type u_4
inst_1 : CommRing S
inst_2 : IsDomain S
i : R →+* S
hi : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑i : (a : R) → S)
hf : (map i f).Splits
j : (a : S) → a ∈ (map i f).roots → R
hj : ∀ (a : S) (a_1 : a ∈ (map i f).roots), (i : (a : R) → S) (j a a_1) = a
rw :
  HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((i : (a : R) → S) f.leadingCoeff) : S[X])
    (Multiset.prod
        (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
          (map i f).roots) :
      S[X])
| map i f

Tactic:
rw [hf.eq_prod_roots, leadingCoeff_map_of_injective hi]

Premises used: Polynomial.Splits.eq_prod_roots, Polynomial.leadingCoeff_map_of_injective
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
S : Type u_4
inst_1 : CommRing S
inst_2 : IsDomain S
i : R →+* S
hi : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑i : (a : R) → S)
hf : (map i f).Splits
j : (a : S) → a ∈ (map i f).roots → R
hj : ∀ (a : S) (a_1 : a ∈ (map i f).roots), (i : (a : R) → S) (j a a_1) = a
conv_lhs :
  HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((i : (a : R) → S) f.leadingCoeff) : S[X])
      (Multiset.prod
          (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
            (map i f).roots) :
        S[X]) =
    map i
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
              (Multiset.pmap (p := Membership.mem (map i f).roots) j (map i f).roots ⋯)) :
          R[X]))
⊢ map i f =
    map i
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
              (Multiset.pmap (p := Membership.mem (map i f).roots) j (map i f).roots ⋯)) :
          R[X]))

Tactic:
conv_lhs => rw [hf.eq_prod_roots, leadingCoeff_map_of_injective hi]

Premises used: Polynomial.Splits.eq_prod_roots, Polynomial.leadingCoeff_map_of_injective
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
S : Type u_4
inst_1 : CommRing S
inst_2 : IsDomain S
i : R →+* S
hi : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑i : (a : R) → S)
hf : (map i f).Splits
j : (a : S) → a ∈ (map i f).roots → R
hj : ∀ (a : S) (a_1 : a ∈ (map i f).roots), (i : (a : R) → S) (j a a_1) = a
⊢ HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((i : (a : R) → S) f.leadingCoeff) : S[X])
      (Multiset.prod
          (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
            (map i f).roots) :
        S[X]) =
    map i
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
              (Multiset.pmap (p := Membership.mem (map i f).roots) j (map i f).roots ⋯)) :
          R[X]))

Tactic:
simp [Multiset.pmap_eq_map, hj, Multiset.map_pmap, Polynomial.map_multiset_prod]

Premises used: Multiset.pmap_eq_map, Multiset.map_pmap, Polynomial.map_multiset_prod
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hm : f.Monic
S : Type u_4
inst_2 : Ring S
i : S →+* R
hr : ∀ a ∈ f.roots, Membership.mem (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) i) a
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) ∈
    liftsRing i
⊢ f ∈ lifts i

Tactic:
rw [hf.eq_prod_roots_of_monic hm, lifts_iff_liftsRing]

Premises used: Polynomial.Splits.eq_prod_roots_of_monic, Polynomial.lifts_iff_liftsRing
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hm : f.Monic
S : Type u_4
inst_2 : Ring S
i : S →+* R
hr : ∀ a ∈ f.roots, Membership.mem (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) i) a
⊢ Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) ∈
    liftsRing i

Tactic:
Subring.multiset_prod_mem _ _ fun g hg => ?_

Premises used: Set.Mem, Subring.multiset_prod_mem
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hm : f.Monic
S : Type u_4
inst_2 : Ring S
i : S →+* R
hr : ∀ a ∈ f.roots, Membership.mem (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) i) a
refine :
  ∀ (g : R[X])
    (hg :
      Membership.mem (γ := Multiset R[X])
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) g),
    g ∈ liftsRing i
⊢ Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) ∈
    liftsRing i

Tactic:
refine Subring.multiset_prod_mem _ _ fun g hg => ?_

Premises used: Subring.multiset_prod_mem
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hm : f.Monic
S : Type u_4
inst_2 : Ring S
i : S →+* R
hr : ∀ a ∈ f.roots, Membership.mem (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) i) a
g : R[X]
hg :
  Membership.mem (γ := Multiset R[X])
    (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) g
obtain :
  ∀ (x : R) (hx : x ∈ f.roots)
    (hg :
      Membership.mem (γ := Multiset R[X])
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))),
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ∈ liftsRing i
⊢ g ∈ liftsRing i

Tactic:
obtain ⟨x, hx, rfl⟩ := Multiset.mem_map.mp hg

Premises used: Multiset.mem_map, Iff.mp, rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hm : f.Monic
S : Type u_4
inst_2 : Ring S
i : S →+* R
hr : ∀ a ∈ f.roots, Membership.mem (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) i) a
x : R
hx : x ∈ f.roots
hg :
  Membership.mem (γ := Multiset R[X])
    (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots)
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ∈ liftsRing i

Tactic:
Subring.sub_mem _ (X_mem_lifts i) (C'_mem_lifts (hr x hx))

Premises used: Polynomial.X_mem_lifts, Set.Mem, Subring.sub_mem, Polynomial.C'_mem_lifts
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hm : f.Monic
S : Type u_4
inst_2 : Ring S
i : S →+* R
hr : ∀ a ∈ f.roots, Membership.mem (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) i) a
x : R
hx : x ∈ f.roots
hg :
  Membership.mem (γ := Multiset R[X])
    (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots)
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ∈ liftsRing i

Tactic:
exact Subring.sub_mem _ (X_mem_lifts i) (C'_mem_lifts (hr x hx))

Premises used: Subring.sub_mem
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
x : R
hr : f.roots = {x}
rw :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) {x}) :
        R[X]) =
    HMul.hMul (α := R[X])
      ((C : (a : R) → R[X])
          (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
              (Multiset.prod
                  (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
                    {x}) :
                R[X])).leadingCoeff :
        R[X])
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
⊢ f =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))

Tactic:
rw [hf.eq_prod_roots, hr]

Premises used: Polynomial.Splits.eq_prod_roots
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
x : R
hr : f.roots = {x}
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) {x}) :
        R[X]) =
    HMul.hMul (α := R[X])
      ((C : (a : R) → R[X])
          (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
              (Multiset.prod
                  (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
                    {x}) :
                R[X])).leadingCoeff :
        R[X])
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
pos : ∀ (hf0 : f.leadingCoeff = 0), f.natDegree = f.roots.card
neg : ∀ (hf0 : ¬f.leadingCoeff = 0), f.natDegree = f.roots.card
⊢ f.natDegree = f.roots.card

Tactic:
by_cases hf0 : f.leadingCoeff = 0

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hf0 : f.leadingCoeff = 0
⊢ f.natDegree = f.roots.card

Tactic:
simp [leadingCoeff_eq_zero.mp hf0]

Premises used: Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 0
rw : f.roots.card
| f.natDegree

Tactic:
rw [hf.eq_prod_roots, natDegree_C_mul hf0, natDegree_multiset_prod_X_sub_C_eq_card]

Premises used: Polynomial.Splits.eq_prod_roots, Polynomial.natDegree_C_mul, Polynomial.natDegree_multiset_prod_X_sub_C_eq_card
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 0
conv_lhs : f.natDegree = f.roots.card
neg : f.roots.card = f.roots.card
⊢ f.natDegree = f.roots.card

Tactic:
conv_lhs => rw [hf.eq_prod_roots, natDegree_C_mul hf0, natDegree_multiset_prod_X_sub_C_eq_card]

Premises used: Polynomial.Splits.eq_prod_roots, Polynomial.natDegree_C_mul, Polynomial.natDegree_multiset_prod_X_sub_C_eq_card
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hf0 : f ≠ 0
⊢ f.degree = (↑f.roots.card : WithBot ℕ)

Tactic:
(degree_eq_iff_natDegree_eq hf0).mpr hf.natDegree_eq_card_roots

Premises used: Iff.mpr, Polynomial.Splits.natDegree_eq_card_roots, Polynomial.degree_eq_iff_natDegree_eq
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
⊢ f.Splits ↔ f.roots.card = f.natDegree

Tactic:
⟨fun h ↦ h.natDegree_eq_card_roots.symm, fun h ↦ splits_iff_exists_multiset.mpr
    ⟨f.roots, (C_leadingCoeff_mul_prod_multiset_X_sub_C h).symm⟩⟩

Premises used: Iff.mpr, Polynomial.splits_iff_exists_multiset, Polynomial.roots, Polynomial.Splits.natDegree_eq_card_roots, Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C, Iff.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hf0 : f.natDegree ≠ 0
⊢ f.roots ≠ 0

Tactic:
simpa [hf.natDegree_eq_card_roots] using hf0

Premises used: Polynomial.Splits.natDegree_eq_card_roots
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_4
inst_2 : CommRing S
inst_3 : IsDomain S
f : R[X]
φ : R →+* S
p : R[X]
hp :
  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})
    p
hφ : map φ p ≠ 0
mem :
  ∀ (r : R) (hφ : map φ ((C : (a : R) → R[X]) r) ≠ 0),
    (map φ ((C : (a : R) → R[X]) r)).roots =
      Multiset.map.{u_4, u_1} (α := R) (⇑φ : (a : R) → S) (roots ((C : (a : R) → R[X]) r))
mem₁ :
  ∀ (a : R) (hφ : map φ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ≠ 0),
    (map φ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))).roots =
      Multiset.map (⇑φ : (a : R) → S) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).roots
⊢ (map φ p).roots = Multiset.map (⇑φ : (a : R) → S) p.roots

Tactic:
obtain (⟨r, rfl⟩ | ⟨a, rfl⟩) := hp

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_4
inst_2 : CommRing S
inst_3 : IsDomain S
f : R[X]
φ : R →+* S
r : R
hφ : map φ ((C : (a : R) → R[X]) r) ≠ 0
⊢ (map φ ((C : (a : R) → R[X]) r)).roots =
    Multiset.map.{u_4, u_1} (α := R) (⇑φ : (a : R) → S) (roots ((C : (a : R) → R[X]) r))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_4
inst_2 : CommRing S
inst_3 : IsDomain S
f : R[X]
φ : R →+* S
a : R
hφ : map φ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ≠ 0
⊢ (map φ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))).roots =
    Multiset.map (⇑φ : (a : R) → S) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).roots

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_4
inst_2 : CommRing S
inst_3 : IsDomain S
f : R[X]
φ : R →+* S
hφ : map φ 1 ≠ 0
⊢ (map φ 1).roots = Multiset.map.{u_4, u_1} (α := R) (⇑φ : (a : R) → S) (roots 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_4
inst_2 : CommRing S
inst_3 : IsDomain S
f : R[X]
φ : R →+* S
x y : R[X]
hx_1 :
  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_1 :
  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
hx : ∀ (hφ : map φ x ≠ 0), (map φ x).roots = Multiset.map (⇑φ : (a : R) → S) x.roots
hy : ∀ (hφ : map φ y ≠ 0), (map φ y).roots = Multiset.map (⇑φ : (a : R) → S) y.roots
hφ : map φ (x * y) ≠ 0
⊢ x * y ≠ 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_4
inst_2 : CommRing S
inst_3 : IsDomain S
f : R[X]
φ : R →+* S
x y : R[X]
hx_1 :
  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_1 :
  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
hx : ∀ (hφ : map φ x ≠ 0), (map φ x).roots = Multiset.map (⇑φ : (a : R) → S) x.roots
hy : ∀ (hφ : map φ y ≠ 0), (map φ y).roots = Multiset.map (⇑φ : (a : R) → S) y.roots
hφ : map φ (x * y) ≠ 0
⊢ (map φ (x * y)).roots = Multiset.map (⇑φ : (a : R) → S) (x * y).roots

Tactic:
simp_all [roots_mul, show x * y ≠ 0 by aesop]

Premises used: Polynomial.roots_mul
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_4
inst_2 : CommRing S
inst_3 : IsDomain S
f : R[X]
hf : f.Splits
φ : R →+* S
hφ : map φ f ≠ 0
mem :
  ∀ (p : R[X])
    (hp :
      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})
        p)
    (hφ : map φ p ≠ 0), (map φ p).roots = Multiset.map (⇑φ : (a : R) → S) p.roots
one : ∀ (hφ : map φ 1 ≠ 0), (map φ 1).roots = Multiset.map.{u_4, u_1} (α := R) (⇑φ : (a : R) → S) (roots 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 →
        ∀ (hx : ∀ (hφ : map φ x ≠ 0), (map φ x).roots = Multiset.map (⇑φ : (a : R) → S) x.roots)
          (hy : ∀ (hφ : map φ y ≠ 0), (map φ y).roots = Multiset.map (⇑φ : (a : R) → S) y.roots)
          (hφ : map φ (x * y) ≠ 0), (map φ (x * y)).roots = Multiset.map (⇑φ : (a : R) → S) (x * y).roots
⊢ (map φ f).roots = Multiset.map (⇑φ : (a : R) → S) f.roots

Tactic:
induction hf using Submonoid.closure_induction with
  | mem p hp => obtain (⟨r, rfl⟩ | ⟨a, rfl⟩) := hp <;> simp
  | one => simp
  | mul x y _ _ hx hy => simp_all [roots_mul, show x * y ≠ 0 by aesop]

Premises used: Polynomial.roots_mul, rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
S : Type u_4
inst_2 : CommRing S
inst_3 : IsDomain S
hf : f.Splits
i : R →+* S
hi : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑i : (a : R) → S)
⊢ (map i f).roots = Multiset.map (⇑i : (a : R) → S) f.roots

Tactic:
(roots_map_of_injective_of_card_eq_natDegree hi hf.natDegree_eq_card_roots.symm).symm

Premises used: Polynomial.roots_map_of_injective_of_card_eq_natDegree, Polynomial.Splits.natDegree_eq_card_roots, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : IsDomain A
inst_4 : IsDomain B
inst_5 : Algebra R A
inst_6 : Algebra R B
hf : Splits (map (algebraMap R A) f)
φ : A →ₐ[R] B
hφ : Ne (α := B[X]) (map (algebraMap R B) f) 0
rwa : Ne (α := B[X]) (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑φ : A →+* B) (algebraMap R A)) f) 0
rwa₁ rwa₂ rwa₃ rwa₄ : Ne (α := B[X]) (map (algebraMap R B) f) 0
⊢ Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0

Tactic:
rwa [map_map, φ.comp_algebraMap]

Premises used: AlgHom.comp_algebraMap, Polynomial.map_map
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : IsDomain A
inst_4 : IsDomain B
inst_5 : Algebra R A
inst_6 : Algebra R B
hf : Splits (map (algebraMap R A) f)
φ : A →ₐ[R] B
hφ : Ne (α := B[X]) (map (algebraMap R B) f) 0
⊢ Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0

Tactic:
replace hφ : (f.map (algebraMap R A)).map (φ : A →+* B) ≠ 0 := by
    rwa [map_map, φ.comp_algebraMap]
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : IsDomain A
inst_4 : IsDomain B
inst_5 : Algebra R A
inst_6 : Algebra R B
hf : Splits (map (algebraMap R A) f)
φ : A →ₐ[R] B
hφ : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0
⊢ roots (map (↑φ : A →+* B) (map (algebraMap R A) f)) =
    Multiset.map (⇑(↑φ : A →+* B) : (a : A) → B) (roots (map (algebraMap R A) f))

Tactic:
replace hf := hf.roots_map_of_ne_zero hφ
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : IsDomain A
inst_4 : IsDomain B
inst_5 : Algebra R A
inst_6 : Algebra R B
φ : A →ₐ[R] B
hφ : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0
hf :
  roots (map (↑φ : A →+* B) (map (algebraMap R A) f)) =
    Multiset.map (⇑(↑φ : A →+* B) : (a : A) → B) (roots (map (algebraMap R A) f))
⊢ roots (map (algebraMap R B) f) = Multiset.map (⇑(↑φ : A →+* B) : (a : A) → B) (roots (map (algebraMap R A) f))

Tactic:
rw [map_map, φ.comp_algebraMap] at hf

Premises used: AlgHom.comp_algebraMap, Polynomial.map_map
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : IsDomain A
inst_4 : IsDomain B
inst_5 : Algebra R A
inst_6 : Algebra R B
φ : A →ₐ[R] B
hφ : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0
hf : roots (map (algebraMap R B) f) = Multiset.map (⇑(↑φ : A →+* B) : (a : A) → B) (roots (map (algebraMap R A) f))
⊢ (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B

Tactic:
simp [rootSet, aroots, hf, Multiset.toFinset_map]

Premises used: Polynomial.rootSet, Polynomial.aroots, Multiset.toFinset_map