awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IrreducibleRing (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ) (hi : i ≠ 0), IsNilpotent (b.coeff i)
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))
have hc : f.leadingCoeff = coeff (a * b) f.natDegree
Tactic: have hc : f.leadingCoeff = _ := congr(coeff $h f.natDegree)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IrreducibleRing (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ) (hi : i ≠ 0), IsNilpotent (b.coeff i)
hc : f.leadingCoeff = coeff (a * b) f.natDegree
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))
have hc₁ : 1 - a.coeff f.natDegree * b.coeff 0 = ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)
Tactic: rw [hm, coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j ↦ a.coeff i * b.coeff j,
    Finset.sum_range_succ, ← sub_eq_iff_eq_add, Nat.sub_self] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IrreducibleRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ideal.IsPrime (nilradical R)
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := HasQuotient.Quotient R (B := Ideal R) (nilradical R)
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ) (hi : i ≠ 0), IsNilpotent (b.coeff i)
hc : 1 - a.coeff f.natDegree * b.coeff 0 = ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))
have rw : IsUnit (HSub.hSub (α := R) (∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)) 1)
Tactic: rw [← add_sub_cancel_left 1 (-(_ * _)), ← sub_eq_add_neg, hc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : ι → S[X]
a : ι
s : Finset ι
has : a ∉ s
IH : ∀ (H : ∀ i ∈ s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) (j : ℕ), IsIntegral R ((s.prod p).coeff j)
H : ∀ i ∈ insert a s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)
j : ℕ
⊢ IsIntegral R (((insert a s).prod p).coeff j)
have insert : IsIntegral.{u_1, u_2} R (A := S)
  (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ j, (p a).coeff x.1 * coeff (∏ x ∈ s, p x) x.2)
Tactic: rw [Finset.prod_insert has, coeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : Finset ι
p : ι → S[X]
H : ∀ i ∈ s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)
j : ℕ
⊢ IsIntegral R ((s.prod p).coeff j)
have empty : ∀ (H : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) (j : ℕ),
  IsIntegral R ((Finset.prod ∅ p).coeff j)
Tactic: induction s using Finset.induction generalizing j with
  | empty => simp [coeff_one, apply_ite, isIntegral_zero, isIntegral_one]
  | insert a s has IH =>
    rw [Finset.prod_insert has, coeff_mul]
    exact IsIntegral.sum _ fun i hi ↦ .mul (H _ (by simp) _) (IH (fun _ _ ↦ H _ (by aesop)) _)
Cleared hypotheses: s, H, j
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : Finset ι
p : ι → S[X]
H : ∀ i ∈ s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)
j : ℕ
empty :
  ∀ (H : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) (j : ℕ),
    IsIntegral R ((Finset.prod ∅ p).coeff j)
⊢ IsIntegral R ((s.prod p).coeff j)
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (IH : ∀ (H : ∀ i ∈ s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) (j : ℕ), IsIntegral R ((s.prod p).coeff j))
  (H : ∀ i ∈ insert a s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) (j : ℕ), IsIntegral R (((insert a s).prod p).coeff j)
Tactic: induction s using Finset.induction generalizing j with
  | empty => simp [coeff_one, apply_ite, isIntegral_zero, isIntegral_one]
  | insert a s has IH =>
    rw [Finset.prod_insert has, coeff_mul]
    exact IsIntegral.sum _ fun i hi ↦ .mul (H _ (by simp) _) (IH (fun _ _ ↦ H _ (by aesop)) _)
Cleared hypotheses: s, H, j
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : Finset ι
p : ι → S[X]
H : ∀ i ∈ s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)
j : ℕ
⊢ IsIntegral R ((s.prod p).coeff j)
have empty : ∀ (H : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) (j : ℕ),
  IsIntegral R ((Finset.prod ∅ p).coeff j)
Tactic: classical
  induction s using Finset.induction generalizing j with
  | empty => simp [coeff_one, apply_ite, isIntegral_zero, isIntegral_one]
  | insert a s has IH =>
    rw [Finset.prod_insert has, coeff_mul]
    exact IsIntegral.sum _ fun i hi ↦ .mul (H _ (by simp) _) (IH (fun _ _ ↦ H _ (by aesop)) _)
Cleared hypotheses: s, H, j
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : Finset ι
p : ι → S[X]
H : ∀ i ∈ s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)
j : ℕ
empty :
  ∀ (H : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) (j : ℕ),
    IsIntegral R ((Finset.prod ∅ p).coeff j)
⊢ IsIntegral R ((s.prod p).coeff j)
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (IH : ∀ (H : ∀ i ∈ s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) (j : ℕ), IsIntegral R ((s.prod p).coeff j))
  (H : ∀ i ∈ insert a s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) (j : ℕ), IsIntegral R (((insert a s).prod p).coeff j)
Tactic: classical
  induction s using Finset.induction generalizing j with
  | empty => simp [coeff_one, apply_ite, isIntegral_zero, isIntegral_one]
  | insert a s has IH =>
    rw [Finset.prod_insert has, coeff_mul]
    exact IsIntegral.sum _ fun i hi ↦ .mul (H _ (by simp) _) (IH (fun _ _ ↦ H _ (by aesop)) _)
Cleared hypotheses: s, H, j
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
⊢ IsIntegral R (p.coeff i)
have obtain : ∀ (m : Multiset S)
  (hm :
    p =
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.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])) m) :
          S[X])),
  IsIntegral R (p.coeff i)
Tactic: obtain ⟨m, hm⟩ := Polynomial.splits_iff_exists_multiset.mp hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
m : Multiset S
hm :
  p =
    HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.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])) m) :
        S[X])
⊢ IsIntegral R (p.coeff i)
have rw : IsIntegral R
  (p.leadingCoeff *
    coeff
      (∏ x : (Multiset.map (fun (x : S) ↦ X - (C : (a : S) → S[X]) x) m).ToType,
        x.fst (β := fun (x : S[X]) ↦
          Fin
            (Multiset.count x
              (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m))))
      i)
Tactic: rw [hm, Multiset.prod_eq_prod_coe, coeff_C_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
m : Multiset S
hm :
  p =
    HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.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])) m) :
        S[X])
⊢ IsIntegral R
    (p.leadingCoeff *
      coeff
        (∏ x : (Multiset.map (fun (x : S) ↦ X - (C : (a : S) → S[X]) x) m).ToType,
          x.fst (β := fun (x : S[X]) ↦
            Fin
              (Multiset.count x
                (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m))))
        i)
have refine : ∀
  (i :
    Multiset.ToType (α := S[X])
      (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)),
  Membership.mem (γ :=
      Finset
        (Multiset.ToType (α := S[X])
          (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)))
      Finset.univ i →
    ∀ (j : ℕ),
      IsIntegral R
        (i.fst (β := fun (x : S[X]) ↦
              Fin
                (Multiset.count x
                  (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
                    m))).coeff
          j)
Tactic: refine .mul hpmon (isIntegral_coeff_prod _ _ ?_ _)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
m : Multiset S
hm :
  p =
    HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.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])) m) :
        S[X])
x : S
hx : x ∈ m
⊢ p.IsRoot x
have rw : 0 ∈
  Multiset.map (α := S[X]) (eval x)
    (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)
Tactic: rw [IsRoot, hm, eval_mul, eval_multiset_prod, Multiset.prod_eq_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
m : Multiset S
hm :
  p =
    HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.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])) m) :
        S[X])
⊢ ∀
    (i :
      Multiset.ToType (α := S[X])
        (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)),
    Membership.mem (γ :=
        Finset
          (Multiset.ToType (α := S[X])
            (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)))
        Finset.univ i →
      ∀ (j : ℕ),
        IsIntegral R
          (i.fst (β := fun (x : S[X]) ↦
                Fin
                  (Multiset.count x
                    (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
                      m))).coeff
            j)
have H : ∀ {x : S} (hx : x ∈ m), p.IsRoot x
Tactic: have H {x} (hx : x ∈ m) : p.IsRoot x := by
    rw [IsRoot, hm, eval_mul, eval_multiset_prod, Multiset.prod_eq_zero, mul_zero]
    simpa [sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i_1 : ℕ
m : Multiset S
hm :
  p =
    HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.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])) m) :
        S[X])
H : ∀ {x : S} (hx : x ∈ m), p.IsRoot x
a : S[X]
i : ℕ
hi :
  i <
    Multiset.count a
      (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)
⊢ ∀ (j : ℕ),
    IsIntegral R
      ((Sigma.fst (β := fun (x : S[X]) ↦
            Fin
              (Multiset.count x
                (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)))
            (Sigma.mk (β := fun (x : S[X]) ↦
              Fin
                (Multiset.count x
                  (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)))
              a
              (⟨i, hi⟩ :
                Fin
                  (Multiset.count a
                    (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
                      m))))).coeff
        j)
have obtain : ∀ (x : S) (hx : x ∈ m)
  (hi :
    i <
      Multiset.count (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
        (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m))
  (j : ℕ),
  IsIntegral R
    ((Sigma.fst (β := fun (x : S[X]) ↦
          Fin
            (Multiset.count x
              (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)))
          (Sigma.mk (β := fun (x : S[X]) ↦
            Fin
              (Multiset.count x
                (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)))
            (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
            (⟨i, hi⟩ :
              Fin
                (Multiset.count (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
                  (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
                    m))))).coeff
      j)
Tactic: obtain ⟨x, hx, rfl⟩ := Multiset.mem_map.mp (Multiset.count_pos.mp (i.zero_le.trans_lt hi))
Cleared hypotheses: a, hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
⊢ IsIntegral R (p.coeff i)
have obtain : ∀ (m : Multiset S)
  (hm :
    p =
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.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])) m) :
          S[X])),
  IsIntegral R (p.coeff i)
Tactic: classical
  obtain ⟨m, hm⟩ := Polynomial.splits_iff_exists_multiset.mp hp
  rw [hm, Multiset.prod_eq_prod_coe, coeff_C_mul]
  refine .mul hpmon (isIntegral_coeff_prod _ _ ?_ _)
  have H {x} (hx : x ∈ m) : p.IsRoot x := by
    rw [IsRoot, hm, eval_mul, eval_multiset_prod, Multiset.prod_eq_zero, mul_zero]
    simpa [sub_eq_zero]
  rintro ⟨a, ⟨i, hi⟩⟩ -
  obtain ⟨x, hx, rfl⟩ := Multiset.mem_map.mp (Multiset.count_pos.mp (i.zero_le.trans_lt hi))
  simp [coeff_X, coeff_C, IsIntegral.sub, apply_ite (IsIntegral R),
    isIntegral_one, isIntegral_zero, hpr x (H hx)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
obtain :
  ∀ (m : Multiset S)
    (hm :
      p =
        HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.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])) m) :
            S[X])),
    IsIntegral R (p.coeff i)
⊢ IsIntegral R (p.coeff i)
have obtain₁ : ∀ (m : Multiset S)
  (hm :
    p =
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.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])) m) :
          S[X])),
  IsIntegral R
    (p.leadingCoeff *
      coeff
        (∏ x : (Multiset.map (fun (x : S) ↦ X - (C : (a : S) → S[X]) x) m).ToType,
          x.fst (β := fun (x : S[X]) ↦
            Fin
              (Multiset.count x
                (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m))))
        i)
Tactic: classical
  obtain ⟨m, hm⟩ := Polynomial.splits_iff_exists_multiset.mp hp
  rw [hm, Multiset.prod_eq_prod_coe, coeff_C_mul]
  refine .mul hpmon (isIntegral_coeff_prod _ _ ?_ _)
  have H {x} (hx : x ∈ m) : p.IsRoot x := by
    rw [IsRoot, hm, eval_mul, eval_multiset_prod, Multiset.prod_eq_zero, mul_zero]
    simpa [sub_eq_zero]
  rintro ⟨a, ⟨i, hi⟩⟩ -
  obtain ⟨x, hx, rfl⟩ := Multiset.mem_map.mp (Multiset.count_pos.mp (i.zero_le.trans_lt hi))
  simp [coeff_X, coeff_C, IsIntegral.sub, apply_ite (IsIntegral R),
    isIntegral_one, isIntegral_zero, hpr x (H hx)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
obtain :
  ∀ (m : Multiset S)
    (hm :
      p =
        HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.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])) m) :
            S[X])),
    IsIntegral R (p.coeff i)
obtain₁ :
  ∀ (m : Multiset S)
    (hm :
      p =
        HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.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])) m) :
            S[X])),
    IsIntegral R
      (p.leadingCoeff *
        coeff
          (∏ x : (Multiset.map (fun (x : S) ↦ X - (C : (a : S) → S[X]) x) m).ToType,
            x.fst (β := fun (x : S[X]) ↦
              Fin
                (Multiset.count x
                  (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
                    m))))
          i)
⊢ IsIntegral R (p.coeff i)
have obtain₂ : ∀ (m : Multiset S)
  (hm :
    p =
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) p.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])) m) :
          S[X]))
  (i :
    Multiset.ToType (α := S[X])
      (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)),
  Membership.mem (γ :=
      Finset
        (Multiset.ToType (α := S[X])
          (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) m)))
      Finset.univ i →
    ∀ (j : ℕ),
      IsIntegral R
        (i.fst (β := fun (x : S[X]) ↦
              Fin
                (Multiset.count x
                  (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
                    m))).coeff
          j)
Tactic: classical
  obtain ⟨m, hm⟩ := Polynomial.splits_iff_exists_multiset.mp hp
  rw [hm, Multiset.prod_eq_prod_coe, coeff_C_mul]
  refine .mul hpmon (isIntegral_coeff_prod _ _ ?_ _)
  have H {x} (hx : x ∈ m) : p.IsRoot x := by
    rw [IsRoot, hm, eval_mul, eval_multiset_prod, Multiset.prod_eq_zero, mul_zero]
    simpa [sub_eq_zero]
  rintro ⟨a, ⟨i, hi⟩⟩ -
  obtain ⟨x, hx, rfl⟩ := Multiset.mem_map.mp (Multiset.count_pos.mp (i.zero_le.trans_lt hi))
  simp [coeff_X, coeff_C, IsIntegral.sub, apply_ite (IsIntegral R),
    isIntegral_one, isIntegral_zero, hpr x (H hx)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : R[X]
q : S[X]
hp : p.Monic
hq : q.Monic
H : q ∣ map (algebraMap R S) p
i : ℕ
⊢ IsIntegral R (q.coeff i)
have a : Nontrivial S
Tactic: nontriviality S
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : R[X]
q : S[X]
hp : p.Monic
hq : q.Monic
H : q ∣ map (algebraMap R S) p
i : ℕ
h : Nontrivial S
⊢ IsIntegral R (q.coeff i)
have obtain : ∀ (T : Type u_2) (w : CommRing T) (w_1 : Algebra S T),
  Module.Finite S T →
    Module.Free S T → Nontrivial T → ∀ (hqT : (map (algebraMap S T) q).Splits), IsIntegral R (q.coeff i)
Tactic: obtain ⟨T, _, _, _, _, _, hqT⟩ := hq.exists_splits_map
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : R[X]
q : S[X]
hp : p.Monic
hq : q.Monic
H : q ∣ map (algebraMap R S) p
i : ℕ
h : Nontrivial S
T : Type u_2
w : CommRing T
w_1 : Algebra S T
w_2 : Module.Finite S T
w_3 : Module.Free S T
w_4 : Nontrivial T
hqT : Splits (map (algebraMap S T) q)
algInst : Algebra R T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S))
scalarTowerInst : IsScalarTower R S T := ⋯
⊢ IsIntegral R (q.coeff i)
have refine : IsIntegral R (A := T) ((IsScalarTower.toAlgHom R S T : (a : S) → T) (q.coeff i) : T)
Tactic: refine (isIntegral_algHom_iff (IsScalarTower.toAlgHom R S T)
    (FaithfulSMul.algebraMap_injective S _)).mp ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : R[X]
q : S[X]
hp : p.Monic
hq : q.Monic
H : q ∣ map (algebraMap R S) p
i : ℕ
h : Nontrivial S
T : Type u_2
w : CommRing T
w_1 : Algebra S T
w_2 : Module.Finite S T
w_3 : Module.Free S T
w_4 : Nontrivial T
hqT : Splits (map (algebraMap S T) q)
algInst : Algebra R T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S))
scalarTowerInst : IsScalarTower R S T := ⋯
⊢ IsIntegral R (A := T) ((IsScalarTower.toAlgHom R S T : (a : S) → T) (q.coeff i) : T)
have rw : IsIntegral R (coeff (map (algebraMap S T) q) i)
Tactic: rw [IsScalarTower.coe_toAlgHom', ← coeff_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : R[X]
q : S[X]
hp : p.Monic
hq : q.Monic
H : q ∣ map (algebraMap R S) p
i : ℕ
h : Nontrivial S
T : Type u_2
w : CommRing T
w_1 : Algebra S T
w_2 : Module.Finite S T
w_3 : Module.Free S T
w_4 : Nontrivial T
hqT : Splits (map (algebraMap S T) q)
algInst : Algebra R T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S))
scalarTowerInst : IsScalarTower R S T := ⋯
⊢ IsIntegral R (coeff (map (algebraMap S T) q) i)
have refine : ∀ (x : T), IsRoot (map (algebraMap S T) q) x → IsIntegral R x
Tactic: refine Polynomial.isIntegral_coeff_of_factors _ (by simp [hq.map, isIntegral_one]) hqT ?_ i