awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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)
⊢ (map φ f).roots = Multiset.map (⇑φ : (a : R) → S) f.roots
have 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
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]
Cleared hypotheses: hf, hφ
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
have rwa : Ne (α := B[X]) (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑φ : A →+* B) (algebraMap R A)) f) 0
Tactic: rwa [map_map, φ.comp_algebraMap]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
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
⊢ (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
have hφ₁ : 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]
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
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
⊢ (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
have hf₁ : 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φ
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
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))
⊢ (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
have hf₁ : 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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
⊢ (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
have replace : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0
Tactic: classical
  replace hφ : (f.map (algebraMap R A)).map (φ : A →+* B) ≠ 0 := by
    rwa [map_map, φ.comp_algebraMap]
  replace hf := hf.roots_map_of_ne_zero hφ
  rw [map_map, φ.comp_algebraMap] at hf
  simp [rootSet, aroots, hf, Multiset.toFinset_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
replace : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0
⊢ (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
have replace₁ : ∀ (hφ : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0), (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
Tactic: classical
  replace hφ : (f.map (algebraMap R A)).map (φ : A →+* B) ≠ 0 := by
    rwa [map_map, φ.comp_algebraMap]
  replace hf := hf.roots_map_of_ne_zero hφ
  rw [map_map, φ.comp_algebraMap] at hf
  simp [rootSet, aroots, hf, Multiset.toFinset_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
replace : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0
replace₁ :
  ∀ (hφ : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0),
    (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
replace₂ : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0
replace₃ replace₄ :
  ∀ (hφ : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0),
    (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
⊢ (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
have replace₅ : ∀ (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))),
  (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
Tactic: classical
  replace hφ : (f.map (algebraMap R A)).map (φ : A →+* B) ≠ 0 := by
    rwa [map_map, φ.comp_algebraMap]
  replace hf := hf.roots_map_of_ne_zero hφ
  rw [map_map, φ.comp_algebraMap] at hf
  simp [rootSet, aroots, hf, Multiset.toFinset_map]
Cleared hypotheses: hf, hφ
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
replace : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0
replace₁ :
  ∀ (hφ : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0),
    (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
replace₂ : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0
replace₃ replace₄ :
  ∀ (hφ : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0),
    (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
replace₅ :
  ∀ (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))),
    (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
⊢ (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
have replace₆ : ∀ (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: classical
  replace hφ : (f.map (algebraMap R A)).map (φ : A →+* B) ≠ 0 := by
    rwa [map_map, φ.comp_algebraMap]
  replace hf := hf.roots_map_of_ne_zero hφ
  rw [map_map, φ.comp_algebraMap] at hf
  simp [rootSet, aroots, hf, Multiset.toFinset_map]
Cleared hypotheses: hf, hφ
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
| f.coeff 0
have 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])) f.roots) :
        R[X])).coeff
  0
Tactic: rw [hf.eq_prod_roots]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
⊢ f.coeff 0 = HPow.hPow (α := R) (-1) f.natDegree * f.leadingCoeff * f.roots.prod
have conv_lhs : (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])) f.roots) :
          R[X])).coeff
    0 =
  HPow.hPow (α := R) (-1) f.natDegree * f.leadingCoeff * f.roots.prod
Tactic: conv_lhs => rw [hf.eq_prod_roots]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
| f.nextCoeff
have 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])) f.roots) :
      R[X])).nextCoeff
Tactic: rw [hf.eq_prod_roots]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
⊢ f.nextCoeff = -f.leadingCoeff * f.roots.sum
have conv_lhs : (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])) f.roots) :
        R[X])).nextCoeff =
  -f.leadingCoeff * f.roots.sum
Tactic: conv_lhs => rw [hf.eq_prod_roots]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
a : R
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits ↔ f.Splits
have refine : ∀ (hf : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits), f.Splits
Tactic: refine ⟨fun hf ↦ ?_, ((Splits.X_sub_C _).mul ·)⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
a : R
hf : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits
⊢ f.Splits
have pos : ∀ (hf₀ : f = 0), f.Splits
Tactic: by_cases hf₀ : f = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
a : R
hf : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits
pos : ∀ (hf₀ : f = 0), f.Splits
⊢ f.Splits
have neg : ∀ (hf₀ : ¬f = 0), f.Splits
Tactic: by_cases hf₀ : f = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
a : R
hf : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits
hf₀ : ¬f = 0
⊢ f.Splits
have this : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f =
  HMul.hMul (α := R[X]) (β := R[X])
    ((C : (a : R) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : 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]))
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).roots) :
      R[X])
Tactic: have := hf.eq_prod_roots
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
a : R
hf : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits
hf₀ : ¬f = 0
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f =
    HMul.hMul (α := R[X]) (β := R[X])
      ((C : (a : R) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : 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]))
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).roots) :
        R[X])
⊢ f.Splits
have this₁ : 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]) *
    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])) f.roots) :
        R[X])
Tactic: rw [leadingCoeff_mul, leadingCoeff_X_sub_C, one_mul,
    roots_mul (mul_ne_zero (X_sub_C_ne_zero _) hf₀), roots_X_sub_C,
    Multiset.singleton_add, Multiset.map_cons, Multiset.prod_cons, mul_left_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
a : R
hf : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits
hf₀ : ¬f = 0
this :
  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]) *
      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])) f.roots) :
          R[X])
⊢ f.Splits
have neg : (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])) f.roots) :
      R[X])).Splits
Tactic: rw [mul_left_cancel₀ (X_sub_C_ne_zero _) this]
-- 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
⊢ (f * g).Splits ↔ f.Splits ∧ g.Splits
have refine : ∀ (h : (f * g).Splits), f.Splits ∧ g.Splits
Tactic: refine ⟨fun h ↦ ?_, and_imp.mpr .mul⟩
-- 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
h : (f * g).Splits
⊢ f.Splits ∧ g.Splits
have generalize : ∀ (p : R[X]) (hp : f * g = p) (h : p.Splits), f.Splits ∧ g.Splits
Tactic: generalize hp : f * g = p at *
Cleared hypotheses: h
-- 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
⊢ f.Splits ∧ g.Splits
have generalize : ∀ (n : ℕ) (hn : p.natDegree = n), f.Splits ∧ g.Splits
Tactic: generalize hn : p.natDegree = n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
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
have hn₁ : f.natDegree = 0 ∧ g.natDegree = 0
Tactic: rw [← hp, natDegree_mul hf₀ hg₀, Nat.add_eq_zero_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
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
have succ : ∀ (a : R) (ha : eval a p = 0), f.Splits ∧ g.Splits
Tactic: obtain ⟨a, ha⟩ := Splits.exists_eval_eq_zero h (degree_ne_of_natDegree_ne <| hn ▸ by simp)
-- 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
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
a : R
ha : eval a p = 0
⊢ f.Splits ∧ g.Splits
have this : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p
Tactic: have := dvd_iff_isRoot.mpr 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
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
a : R
ha : eval a p = 0
this : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p
⊢ f.Splits ∧ g.Splits
have this₁ : 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
Tactic: rw [← hp, (prime_X_sub_C a).dvd_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
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
a : R
ha : eval a p = 0
this :
  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
⊢ f.Splits ∧ g.Splits
have succ : ∀
  (hf2 :
    ∀ {R : Type u_1} [inst : CommRing R] [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)
      {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)
      (a : R) (ha : eval a p = 0)
      (this :
        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)
      (hf : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ f), f.Splits ∧ g.Splits)
  (hf : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ f), f.Splits ∧ g.Splits
Tactic: wlog hf : X - C a ∣ f with hf2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
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
a : R
ha : eval a p = 0
this :
  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
succ :
  ∀
    (hf2 :
      ∀ {R : Type u_1} [inst : CommRing R] [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)
        {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)
        (a : R) (ha : eval a p = 0)
        (this :
          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)
        (hf : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ f), f.Splits ∧ g.Splits)
    (hf : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ f), f.Splits ∧ g.Splits
⊢ f.Splits ∧ g.Splits
have wlog : ∀ {R : Type u_1} [inst : CommRing R] [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)
  {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) (a : R)
  (ha : eval a p = 0)
  (this :
    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)
  (hf : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ f), f.Splits ∧ g.Splits
Tactic: wlog hf : X - C a ∣ f with hf2
Cleared hypotheses: R, inst, inst_1, n, ih, f, g, hf₀, hg₀, p, hp, h, hn, a, ha, this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
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
a : R
ha : eval a p = 0
this :
  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
hf : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ f
⊢ f.Splits ∧ g.Splits
have obtain : ∀ (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
Tactic: obtain ⟨f, rfl⟩ := hf
Cleared hypotheses: f, hf₀, hp, this, hf
-- 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 hp₁ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g) = p
Tactic: rw [mul_assoc] at hp
Cleared hypotheses: hp, this