awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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.insert a s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)
j : ℕ
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)
⊢ IsIntegral R (((Insert.insert a s).prod p).coeff j)

Tactic:
rw [Finset.prod_insert has, coeff_mul]

Premises used: Finset.prod_insert, Polynomial.coeff_mul
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 : ℕ
i : ℕ × ℕ
hi : i ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ j
⊢ a ∈ insert a s

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 : ℕ
i : ℕ × ℕ
hi : i ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ j
x : ι
h : x ∈ s
⊢ x ∈ insert a s

Tactic:
aesop
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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.{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:
exact IsIntegral.sum _ fun i hi ↦ .mul (H _ (by simp) _) (IH (fun _ _ ↦ H _ (by aesop)) _)

Premises used: IsIntegral.mul, IsIntegral.sum
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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)
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.insert a s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) (j : ℕ),
    IsIntegral R (((Insert.insert a s).prod p).coeff j)
⊢ IsIntegral R ((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)) _)

Premises used: Polynomial.coeff_one, apply_ite, Polynomial.coeff_mul, Insert.insert, isIntegral_one, isIntegral_zero
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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)
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.insert a s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) (j : ℕ),
    IsIntegral R (((Insert.insert a s).prod p).coeff j)
⊢ IsIntegral R ((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)) _)

Premises used: Polynomial.coeff_one, apply_ite, Polynomial.coeff_mul, Insert.insert, isIntegral_one, isIntegral_zero
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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)

Tactic:
obtain ⟨m, hm⟩ := Polynomial.splits_iff_exists_multiset.mp hp

Premises used: Polynomial.splits_iff_exists_multiset, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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])
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)
⊢ IsIntegral R (p.coeff i)

Tactic:
rw [hm, Multiset.prod_eq_prod_coe, coeff_C_mul]

Premises used: Polynomial.coeff_C_mul, Multiset.prod_eq_prod_coe
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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)

Tactic:
.mul hpmon (isIntegral_coeff_prod _ _ ?_ _)

Premises used: Polynomial.isIntegral_coeff_prod, IsIntegral.mul
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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])
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)
⊢ 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:
refine .mul hpmon (isIntegral_coeff_prod _ _ ?_ _)
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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
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)
⊢ p.IsRoot x

Tactic:
rw [IsRoot, hm, eval_mul, eval_multiset_prod, Multiset.prod_eq_zero, mul_zero]

Premises used: Polynomial.eval_multiset_prod, Multiset.prod_eq_zero, Polynomial.IsRoot, Polynomial.eval_mul, MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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
⊢ 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:
simpa [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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

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]
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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)
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)
⊢ ∀ (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)

Tactic:
obtain ⟨x, hx, rfl⟩ := Multiset.mem_map.mp (Multiset.count_pos.mp (i.zero_le.trans_lt hi))

Premises used: Nat.zero_le, Multiset.mem_map, Multiset.count_pos, Iff.mp, LE.le.trans_lt, rfl
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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
i : ℕ
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:
simp [coeff_X, coeff_C, IsIntegral.sub, apply_ite (IsIntegral R),
    isIntegral_one, isIntegral_zero, hpr x (H hx)]

Premises used: apply_ite, IsIntegral.sub, Polynomial.coeff_C, IsIntegral, isIntegral_one, isIntegral_zero, Polynomial.coeff_X
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 : ℕ
⊢ Nontrivial S

Tactic:
nontriviality S
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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
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)
⊢ IsIntegral R (q.coeff i)

Tactic:
obtain ⟨T, _, _, _, _, _, hqT⟩ := hq.exists_splits_map

Premises used: Polynomial.Monic.exists_splits_map
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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)

Tactic:
(isIntegral_algHom_iff (IsScalarTower.toAlgHom R S T)
    (FaithfulSMul.algebraMap_injective S _)).mp ?_

Premises used: IsScalarTower.toAlgHom, isIntegral_algHom_iff, FaithfulSMul.algebraMap_injective, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 := ⋯
refine : IsIntegral R (A := T) ((IsScalarTower.toAlgHom R S T : (a : S) → T) (q.coeff i) : T)
⊢ IsIntegral R (q.coeff i)

Tactic:
refine (isIntegral_algHom_iff (IsScalarTower.toAlgHom R S T)
    (FaithfulSMul.algebraMap_injective S _)).mp ?_

Premises used: IsScalarTower.toAlgHom, isIntegral_algHom_iff, FaithfulSMul.algebraMap_injective, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 := ⋯
rw : IsIntegral R (coeff (map (algebraMap S T) q) i)
⊢ IsIntegral R (A := T) ((IsScalarTower.toAlgHom R S T : (a : S) → T) (q.coeff i) : T)

Tactic:
rw [IsScalarTower.coe_toAlgHom', ← coeff_map]

Premises used: Polynomial.coeff_map, IsScalarTower.coe_toAlgHom'
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 (leadingCoeff (map (algebraMap S T) q))

Tactic:
simp [hq.map, isIntegral_one]

Premises used: isIntegral_one, Polynomial.Monic.map
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 := ⋯
refine : ∀ (x : T), IsRoot (map (algebraMap S T) q) x → IsIntegral R x
⊢ IsIntegral R (coeff (map (algebraMap S T) q) i)

Tactic:
refine Polynomial.isIntegral_coeff_of_factors _ (by simp [hq.map, isIntegral_one]) hqT ?_ i

Premises used: Polynomial.isIntegral_coeff_of_factors
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 := ⋯
x : T
hx : IsRoot (map (algebraMap S T) q) x
⊢ Eq (α := T) ((aeval x : (a : S[X]) → T) q : T) (0 : T)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 := ⋯
x : T
hx : IsRoot (map (algebraMap S T) q) x
⊢ eval₂ (algebraMap R T) x p = 0

Tactic:
simpa using aeval_eq_zero_of_dvd_aeval_eq_zero (a := x) H (by simp_all)

Premises used: Polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 := ⋯
x : T
hx : IsRoot (map (algebraMap S T) q) x
⊢ IsIntegral R x

Tactic:
exact ⟨p, hp, by simpa using aeval_eq_zero_of_dvd_aeval_eq_zero (a := x) H (by simp_all)⟩
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
p : S[X]
hp : IsAlmostIntegral.{u_1, u_2} R[X] p
i : ℕ
q : S[X]
hq : IsAlmostIntegral.{u_1, u_2} R[X] q
obtain :
  ∀ (p : R[X]) (hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p)
    (hp' :
      ∀ (n : ℕ),
        Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])) (p • q ^ n)),
    IsAlmostIntegral R q.leadingCoeff
⊢ IsAlmostIntegral R q.leadingCoeff

Tactic:
obtain ⟨p, hp, hp'⟩ := hq
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : FaithfulSMul R S
p_1 : S[X]
hp_1 : IsAlmostIntegral.{u_1, u_2} R[X] p_1
i : ℕ
q : S[X]
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
hp' :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S[X]) (RingHom.range.{u_1, u_2} (R := R[X]) (algebraMap R[X] S[X])) (p • q ^ n)
⊢ Membership.mem (γ := Submonoid R) R⁰ p.leadingCoeff

Tactic:
simpa using hp