awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ih :
  ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n),
    f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
p : R[X]
h : p.Splits
hn : p.natDegree = n + 1
a : R
ha : eval a p = 0
f : R[X]
hf₀ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ≠ 0
hp : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g) = p
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ∨
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ g
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits ∧ g.Splits
have h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).Splits
Tactic: subst hp
Cleared hypotheses: p, h, hn, ha, hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ih :
  ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n),
    f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
p : R[X]
h : p.Splits
hn : p.natDegree = n + 1
a : R
ha : eval a p = 0
f : R[X]
hf₀ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ≠ 0
hp : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g) = p
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ∨
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ g
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).Splits
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits ∧ g.Splits
have hn₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).natDegree = n + 1
Tactic: subst hp
Cleared hypotheses: p, h, hn, ha, hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ih :
  ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n),
    f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
p : R[X]
h : p.Splits
hn : p.natDegree = n + 1
a : R
ha : eval a p = 0
f : R[X]
hf₀ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ≠ 0
hp : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g) = p
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ∨
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ g
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).Splits
hn₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).natDegree = n + 1
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits ∧ g.Splits
have ha₁ : eval a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)) = 0
Tactic: subst hp
Cleared hypotheses: p, h, hn, ha, hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ih :
  ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n),
    f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ≠ 0
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ∨
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ g
h : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).Splits
hn : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).natDegree = n + 1
ha : eval a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)) = 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits ∧ g.Splits
have hn₁ : (f * g).natDegree = n
Tactic: rw [natDegree_mul (by aesop) (by aesop), natDegree_X_sub_C, add_comm, Nat.succ_inj] at hn
Cleared hypotheses: hn, ha
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ih :
  ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n),
    f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ≠ 0
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ∨
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ g
h : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).Splits
hn : (f * g).natDegree = n
ha : eval a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)) = 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits ∧ g.Splits
have this₁ : f.Splits ∧ g.Splits
Tactic: have := ih (by aesop) hg₀ (f * g) rfl (splits_X_sub_C_mul_iff.mp h) hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
inst_1 : IsDomain R
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
n : ℕ
hn : p.natDegree = n
⊢ f.Splits ∧ g.Splits
have zero : ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = 0),
  f.Splits ∧ g.Splits
Tactic: induction n generalizing p f g with
  | zero =>
    rw [← hp, natDegree_mul hf₀ hg₀, Nat.add_eq_zero_iff] at hn
    exact ⟨splits_of_natDegree_eq_zero hn.1, splits_of_natDegree_eq_zero hn.2⟩
  | succ n ih =>
    obtain ⟨a, ha⟩ := Splits.exists_eval_eq_zero h (degree_ne_of_natDegree_ne <| hn ▸ by simp)
    have := dvd_iff_isRoot.mpr ha
    rw [← hp, (prime_X_sub_C a).dvd_mul] at this
    wlog hf : X - C a ∣ f with hf2
    · exact .symm <| hf2 n ih hg₀ hf₀ p ((mul_comm g f).trans hp) h hn a ha this.symm <|
        this.resolve_left hf
    obtain ⟨f, rfl⟩ := hf
    rw [mul_assoc] at hp; subst hp
    rw [natDegree_mul (by aesop) (by aesop), natDegree_X_sub_C, add_comm, Nat.succ_inj] at hn
    have := ih (by aesop) hg₀ (f * g) rfl (splits_X_sub_C_mul_iff.mp h) hn
    aesop
Cleared hypotheses: f, g, hf₀, hg₀, p, hp, h, n, hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
inst_1 : IsDomain R
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
n : ℕ
hn : p.natDegree = n
zero :
  ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = 0),
    f.Splits ∧ g.Splits
⊢ f.Splits ∧ g.Splits
have succ : ∀ (n : ℕ)
  (ih :
    ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n),
      f.Splits ∧ g.Splits)
  {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n + 1),
  f.Splits ∧ g.Splits
Tactic: induction n generalizing p f g with
  | zero =>
    rw [← hp, natDegree_mul hf₀ hg₀, Nat.add_eq_zero_iff] at hn
    exact ⟨splits_of_natDegree_eq_zero hn.1, splits_of_natDegree_eq_zero hn.2⟩
  | succ n ih =>
    obtain ⟨a, ha⟩ := Splits.exists_eval_eq_zero h (degree_ne_of_natDegree_ne <| hn ▸ by simp)
    have := dvd_iff_isRoot.mpr ha
    rw [← hp, (prime_X_sub_C a).dvd_mul] at this
    wlog hf : X - C a ∣ f with hf2
    · exact .symm <| hf2 n ih hg₀ hf₀ p ((mul_comm g f).trans hp) h hn a ha this.symm <|
        this.resolve_left hf
    obtain ⟨f, rfl⟩ := hf
    rw [mul_assoc] at hp; subst hp
    rw [natDegree_mul (by aesop) (by aesop), natDegree_X_sub_C, add_comm, Nat.succ_inj] at hn
    have := ih (by aesop) hg₀ (f * g) rfl (splits_X_sub_C_mul_iff.mp h) hn
    aesop
Cleared hypotheses: f, g, hf₀, hg₀, p, hp, h, n, hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
inst_1 : IsDomain R
hg : g.Splits
hg₀ : g ≠ 0
hfg : f ∣ g
⊢ f.Splits
have obtain : ∀ (g : R[X]) (hg : (f * g).Splits) (hg₀ : f * g ≠ 0), f.Splits
Tactic: obtain ⟨g, rfl⟩ := hfg
Cleared hypotheses: g, hg, hg₀, hfg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ Eq (α := R) (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (s ×ˢ g.roots)))
    (Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) s))
have this : g =
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) g.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])) g.roots) :
      R[X])
Tactic: have := hg'.eq_prod_roots
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this :
  g =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) g.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])) g.roots) :
        R[X])
⊢ Eq (α := R) (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (s ×ˢ g.roots)))
    (Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) s))
have this₁ : g =
  Multiset.prod
    (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) g.roots)
Tactic: rw [hg.leadingCoeff, map_one, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this :
  g =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) g.roots)
| Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) s)
have rw : Multiset.prod
  (Multiset.map
    (fun (x : R) ↦
      eval x
        (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) g.roots)))
    s)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this :
  g =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) g.roots)
⊢ Eq (α := R) (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (s ×ˢ g.roots)))
    (Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) s))
have conv_rhs : Eq (α := R) (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (s ×ˢ g.roots)))
  (Multiset.prod
    (Multiset.map
      (fun (x : R) ↦
        eval x
          (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) g.roots)))
      s))
Tactic: conv_rhs => rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this :
  g =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) g.roots)
⊢ Eq (α := R) (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (s ×ˢ g.roots)))
    (Multiset.prod
      (Multiset.map
        (fun (x : R) ↦
          eval x
            (Multiset.prod
              (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
                g.roots)))
        s))
have simp_rw : Eq (α := R)
  (Multiset.prod (Multiset.map (fun (x : R) ↦ Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) g.roots)) s))
  (Multiset.prod
    (Multiset.map
      (fun (x : R) ↦
        (Multiset.map
            (Function.comp (β := R[X]) (eval x) fun (x : R) ↦
              HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
            g.roots).prod)
      s))
Tactic: simp_rw [eval_multiset_prod, Multiset.prod_map_product_eq_prod_prod, Multiset.map_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this :
  g =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) g.roots)
⊢ Eq (α := R)
    (Multiset.prod (Multiset.map (fun (x : R) ↦ Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) g.roots)) s))
    (Multiset.prod
      (Multiset.map
        (fun (x : R) ↦
          (Multiset.map
              (Function.comp (β := R[X]) (eval x) fun (x : R) ↦
                HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
              g.roots).prod)
        s))
have h : ∀ (x : R) (hx : x ∈ s),
  ∀ x_1 ∈ g.roots,
    Eq (α := R → R) (HSub.hSub x)
      (Function.comp (β := R[X]) (eval x) fun (x : R) ↦
        HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
Tactic: congr! with x hx
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this :
  g =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) g.roots)
x : R
hx : x ∈ s
x_1 : R
h : x_1 ∈ g.roots
⊢ Eq (α := R → R) (HSub.hSub x)
    (Function.comp (β := R[X]) (eval x) fun (x : R) ↦
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
have h : ∀ (x_2 : R),
  x - x_2 =
    Function.comp (β := R[X]) (eval x)
      (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (g.roots ×ˢ s)) =
    HPow.hPow (α := R) (-1) (s.card * g.roots.card) * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) s)
have trans : Eq (α := R) (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (g.roots ×ˢ s)))
  (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)))
Tactic: trans ((s ×ˢ g.roots).map fun ij ↦ (-1) * (ij.1 - ij.2)).prod
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
trans :
  Eq (α := R) (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (g.roots ×ˢ s)))
    (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)))
⊢ Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (g.roots ×ˢ s)) =
    HPow.hPow (α := R) (-1) (s.card * g.roots.card) * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) s)
have trans₁ : Multiset.prod (Multiset.map (fun (ij : R × R) ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)) =
  HPow.hPow (α := R) (-1) (s.card * g.roots.card) * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) s)
Tactic: trans ((s ×ˢ g.roots).map fun ij ↦ (-1) * (ij.1 - ij.2)).prod
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ Eq (α := R) (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (g.roots ×ˢ s)))
    (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)))
have rw : Eq (α := R) (Multiset.prod (Multiset.map ((fun (ij : R × R) ↦ ij.1 - ij.2) ∘ Prod.swap) (s ×ˢ g.roots)))
  (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)))
Tactic: rw [← Multiset.map_swap_product, Multiset.map_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ Multiset.prod (Multiset.map (fun (ij : R × R) ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)) =
    HPow.hPow (α := R) (-1) (s.card * g.roots.card) * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) s)
have rw : HMul.hMul (α := R) (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ -1) (s ×ˢ g.roots)))
    (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (s ×ˢ g.roots))) =
  HPow.hPow (α := R) (-1) (s.card * g.roots.card) * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) s)
Tactic: rw [Multiset.prod_map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : DivisionSemiring R
f : R[X]
hf : f.natDegree ≤ 1
⊢ f.Splits
have 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),
  (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: obtain ⟨a, b, rfl⟩ := exists_eq_X_add_C_of_natDegree_le_one hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
⊢ (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
have pos : ∀ (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
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
pos :
  ∀ (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
have neg : ∀ (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
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
⊢ (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
have 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
Tactic: rw [← mul_inv_cancel_left₀ ha b, C_mul, ← mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
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
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) i) x
have hx₁ : ∃ 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) i) x
have 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
Tactic: obtain ⟨x, -, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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)
⊢ Multiset.map (⇑(algebraMap A B) : (a : A) → B) (f.aroots A) = f.aroots B
have rw : Multiset.map (⇑(algebraMap A B) : (a : A) → B) (f.aroots A) = aroots (map (algebraMap R A) f) B
Tactic: rw [← aroots_map B A, aroots, aroots, hf.roots_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
⊢ Multiset.map (⇑(algebraMap A B) : (a : A) → B) (f.aroots A) = f.aroots B
have rw₁ : Multiset.map (⇑(algebraMap A B) : (a : A) → B) (roots (map (algebraMap R A) f)) = aroots (map (algebraMap R A) f) B
Tactic: rw [← aroots_map B A, aroots, aroots, hf.roots_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
⊢ Multiset.map (⇑(algebraMap A B) : (a : A) → B) (f.aroots A) = f.aroots B
have 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))
Tactic: rw [← aroots_map B A, aroots, aroots, hf.roots_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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))
⊢ Multiset.map (⇑(algebraMap A B) : (a : A) → B) (f.aroots A) = f.aroots B
have 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)))
Tactic: rw [← aroots_map B A, aroots, aroots, hf.roots_map]