awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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]
hf : Splits (map (algebraMap R A) f)
g : A →ₐ[R] B
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B
have rw : (⇑g : (a : A) → B) '' (↑(f.aroots A).toFinset : Set 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]
-- 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]
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
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B
have rw₁ : (↑(Finset.image (⇑g : (a : A) → B) (f.aroots A).toFinset) : Set B) = f.rootSet B
Tactic: rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← g.coe_toRingHom,
    ← hf.roots_map, map_map, g.comp_algebraMap, ← rootSet]
-- 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]
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
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B
have rw₂ : (↑(Multiset.toFinset (Multiset.map (⇑g : (a : A) → B) (f.aroots A))) : Set B) = f.rootSet B
Tactic: rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← g.coe_toRingHom,
    ← hf.roots_map, map_map, g.comp_algebraMap, ← rootSet]
-- 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]
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
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B
have rw₃ : (↑(Multiset.toFinset (Multiset.map (⇑(↑g : A →+* B) : (a : A) → B) (f.aroots A))) : Set B) = f.rootSet B
Tactic: rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← g.coe_toRingHom,
    ← hf.roots_map, map_map, g.comp_algebraMap, ← rootSet]
-- 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]
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
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B
have rw₄ : (↑(roots (map (↑g : A →+* B) (map (algebraMap R A) f))).toFinset : Set B) = f.rootSet B
Tactic: rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← g.coe_toRingHom,
    ← hf.roots_map, map_map, g.comp_algebraMap, ← rootSet]
-- 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]
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
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B
have rw₅ : (↑(roots (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A)) f)).toFinset :
    Set B) =
  f.rootSet B
Tactic: rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← g.coe_toRingHom,
    ← hf.roots_map, map_map, g.comp_algebraMap, ← rootSet]
-- 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]
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
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B
have rw₆ : (↑(roots (map (algebraMap R B) f)).toFinset : Set B) = f.rootSet B
Tactic: rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← g.coe_toRingHom,
    ← hf.roots_map, map_map, g.comp_algebraMap, ← rootSet]
-- 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]
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
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B
have rw₇ : f.rootSet B = f.rootSet B
Tactic: rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← g.coe_toRingHom,
    ← hf.roots_map, map_map, g.comp_algebraMap, ← rootSet]
-- 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]
hf : Splits (map (algebraMap R A) f)
g : A →ₐ[R] B
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B
have rw : (⇑g : (a : A) → B) '' (↑(f.aroots A).toFinset : Set 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]
-- 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]
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
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B
have rw₁ : (↑(Finset.image (⇑g : (a : A) → B) (f.aroots A).toFinset) : Set B) = 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]
-- 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]
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
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B
have rw₂ : (↑(Multiset.toFinset (Multiset.map (⇑g : (a : A) → B) (f.aroots A))) : Set B) = 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]
-- 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]
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
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B
have rw₃ : (↑(Multiset.toFinset (Multiset.map (⇑(↑g : A →+* B) : (a : A) → B) (f.aroots A))) : Set B) = 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]
-- 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]
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
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B
have rw₄ : (↑(roots (map (↑g : A →+* B) (map (algebraMap R A) f))).toFinset : Set B) = 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]
-- 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]
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
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B
have rw₅ : (↑(roots (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A)) f)).toFinset :
    Set B) =
  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]
-- 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]
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
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B
have rw₆ : (↑(roots (map (algebraMap R B) f)).toFinset : Set B) = 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]
-- 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]
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
⊢ (⇑g : (a : A) → B) '' f.rootSet A = f.rootSet B
have rw₇ : f.rootSet B = 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]
-- 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]
hf : Splits (map (algebraMap R A) f)
g : A →ₐ[R] B
⊢ Algebra.adjoin R (f.rootSet B) = g.range ↔ Eq (α := Subalgebra R A) (Algebra.adjoin R (f.rootSet A)) ⊤
have rw : Subalgebra.map g (Algebra.adjoin R (f.rootSet A)) = Subalgebra.map g ⊤ ↔
  Eq (α := Subalgebra R A) (Algebra.adjoin R (f.rootSet A)) ⊤
Tactic: rw [← hf.image_rootSet g, Algebra.adjoin_image, ← Algebra.map_top]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f g : R[X]
hp : f.Splits
hp0 : f ≠ 0
hq : f.roots ≤ g.roots
⊢ f ∣ g
have 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
Tactic: rw [hp.eq_prod_roots, C_mul_dvd (leadingCoeff_ne_zero.2 hp0)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f g : R[X]
hf : f.Splits
hg : g.natDegree ≤ 1
⊢ (f.comp g).Splits
have inl : ∀ (hg : natDegree.{u_1} (R := R) 0 ≤ 1), (f.comp 0).Splits
Tactic: rcases eq_or_ne g 0 with rfl | hg0
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
⊢ (f.comp g).Splits
have inr : ∀ (hg0 : g ≠ 0), (f.comp g).Splits
Tactic: rcases eq_or_ne g 0 with rfl | hg0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f g : R[X]
hg : g.natDegree = 1
⊢ f.Splits ↔ (f.comp g).Splits
have refine : ∀ (hf : (f.comp g).Splits), f.Splits
Tactic: refine ⟨fun hf ↦ hf.comp_of_natDegree_le_one hg.le, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f g : R[X]
hg : g.natDegree = 1
hf : (f.comp g).Splits
⊢ f.Splits
have 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
Tactic: obtain ⟨a, b, rfl⟩ := exists_eq_X_add_C_of_natDegree_le_one hg.le
Cleared hypotheses: g, hg, hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
have 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
Tactic: contrapose! hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
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
⊢ f.Splits
have ha : a ≠ 0
Tactic: have ha : a ≠ 0 := by contrapose! hg; simp [hg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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])))
have 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]))
Tactic: simp only [comp_assoc, add_comp, mul_comp, C_comp, X_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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]) ((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]))
have 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]))
Tactic: rw [← mul_assoc, ← C_mul, mul_inv_cancel₀ ha, C_1, one_mul, sub_add_cancel, comp_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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]))
⊢ 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]))
have 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]))
Tactic: rw [← mul_assoc, ← C_mul, mul_inv_cancel₀ ha, C_1, one_mul, sub_add_cancel, comp_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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]))
⊢ 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]))
have 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]))
Tactic: rw [← mul_assoc, ← C_mul, mul_inv_cancel₀ ha, C_1, one_mul, sub_add_cancel, comp_X]