awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
h_1 : (C : (a : R) → R[X]) p.leadingCoeff ∣ p
q : R[X]
hMul : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q
h : minpoly R s = q
⊢ Ne (α := R[X]) (minpoly R s) 0

Tactic:
convert! right_ne_zero_of_mul <| hMul ▸ h₀

Premises used: right_ne_zero_of_mul
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
h : (C : (a : R) → R[X]) p.leadingCoeff ∣ p
q : R[X]
hMul : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q
⊢ minpoly R s = q

Tactic:
IsIntegrallyClosed.minpoly.unique ?_ ?_ ?_ |>.symm

Premises used: IsIntegrallyClosed.minpoly.unique, Eq.symm
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
h_1 : (C : (a : R) → R[X]) p.leadingCoeff ∣ p
q : R[X]
hMul : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q
h : q.Monic
h₁ : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S)
h₂ :
  ∀ (Q : R[X]),
    Q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) Q : S) (0 : S) → q.degree ≤ Q.degree
⊢ minpoly R s = q

Tactic:
refine IsIntegrallyClosed.minpoly.unique ?_ ?_ ?_ |>.symm

Premises used: IsIntegrallyClosed.minpoly.unique, Eq.symm
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
h : (C : (a : R) → R[X]) p.leadingCoeff ∣ p
q : R[X]
hMul : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q
⊢ leadingCoeff ((C : (a : R) → R[X]) p.leadingCoeff) * q.leadingCoeff = p.leadingCoeff

Tactic:
have := hMul ▸ leadingCoeff_mul .. |>.symm
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
h : (C : (a : R) → R[X]) p.leadingCoeff ∣ p
q : R[X]
hMul : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q
this : leadingCoeff ((C : (a : R) → R[X]) p.leadingCoeff) * q.leadingCoeff = p.leadingCoeff
⊢ q.leadingCoeff = 1

Tactic:
simp only [leadingCoeff_C, ne_eq, leadingCoeff_eq_zero, h₀, not_false_eq_true, mul_eq_left₀]
        at this

Premises used: mul_eq_left₀, ne_eq, Polynomial.leadingCoeff_C, not_false_eq_true, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
h : (C : (a : R) → R[X]) p.leadingCoeff ∣ p
q : R[X]
hMul : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q
this : q.leadingCoeff = 1
⊢ q.Monic

Tactic:
this

Premises used: Polynomial.Monic
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
h : (C : (a : R) → R[X]) p.leadingCoeff ∣ p
q : R[X]
hMul : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q
this : q.leadingCoeff = 1
⊢ q.Monic

Tactic:
exact this
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
h : (C : (a : R) → R[X]) p.leadingCoeff ∣ p
q : R[X]
hMul : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q
⊢ Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S)
    ((Polynomial.aeval s : (a : R[X]) → S) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q) : S)

Tactic:
have := congrArg (Polynomial.aeval s) hMul
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
h : (C : (a : R) → R[X]) p.leadingCoeff ∣ p
q : R[X]
hMul : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q
this :
  Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S)
    ((Polynomial.aeval s : (a : R[X]) → S) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q) : S)
⊢ Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S)

Tactic:
simp only [hp, h₀, map_mul, aeval_C, zero_eq_mul, FaithfulSMul.algebraMap_eq_zero_iff,
        leadingCoeff_eq_zero, false_or] at this

Premises used: zero_eq_mul, false_or, map_mul, Polynomial.aeval_C, Polynomial.leadingCoeff_eq_zero, FaithfulSMul.algebraMap_eq_zero_iff
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
h : (C : (a : R) → R[X]) p.leadingCoeff ∣ p
q : R[X]
hMul : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q
this : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S)
⊢ Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S)

Tactic:
this
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
h : (C : (a : R) → R[X]) p.leadingCoeff ∣ p
q : R[X]
hMul : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q
this : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S)
⊢ Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S)

Tactic:
exact this
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
h : (C : (a : R) → R[X]) p.leadingCoeff ∣ p
q : R[X]
hMul : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q
⊢ p.leadingCoeff ≠ 0

Tactic:
simp [h₀]
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
s : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) p : S) (0 : S)
h₀ : p ≠ 0
pmin :
  ∀ (q : R[X]),
    q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S) → p.degree ≤ q.degree
h : (C : (a : R) → R[X]) p.leadingCoeff ∣ p
q : R[X]
hMul : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) q
⊢ ∀ (Q : R[X]),
    Q.Monic → Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) Q : S) (0 : S) → q.degree ≤ Q.degree

Tactic:
exact (hMul ▸ degree_C_mul <| by simp [h₀]) ▸ pmin
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
hx : IsIntegral R x
⊢ Prime (M := R[X]) (minpoly R x)

Tactic:
⟨(minpoly.monic hx).ne_zero,
      ⟨fun h_contra => (ne_of_lt (minpoly.degree_pos hx)) (degree_eq_zero_of_isUnit h_contra).symm,
        fun a b h => or_iff_not_imp_left.mpr fun h' => ?_⟩⟩

Premises used: Iff.mpr, minpoly.monic, minpoly.degree_pos, Prime, Polynomial.degree_eq_zero_of_isUnit, Classical.or_iff_not_imp_left, And.intro, Eq.symm, ne_of_lt, Polynomial.Monic.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
hx : IsIntegral R x
h_contra : ∀ (a b : R[X]) (h : minpoly R x ∣ a * b) (h' : ¬minpoly R x ∣ a), minpoly R x ∣ b
⊢ Prime (M := R[X]) (minpoly R x)

Tactic:
refine
    ⟨(minpoly.monic hx).ne_zero,
      ⟨fun h_contra => (ne_of_lt (minpoly.degree_pos hx)) (degree_eq_zero_of_isUnit h_contra).symm,
        fun a b h => or_iff_not_imp_left.mpr fun h' => ?_⟩⟩
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
hx : IsIntegral R x
a b : R[X]
h : minpoly R x ∣ a * b
h' : ¬minpoly R x ∣ a
rw :
  ∀ (h : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) (a * b) : S) (0 : S))
    (h' : ¬Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) a : S) (0 : S)),
    Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) b : S) (0 : S)
⊢ minpoly R x ∣ b

Tactic:
rw [← minpoly.isIntegrallyClosed_dvd_iff hx] at h' h ⊢

Premises used: minpoly.isIntegrallyClosed_dvd_iff
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
hx : IsIntegral R x
a b : R[X]
h : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) (a * b) : S) (0 : S)
h' : ¬Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) a : S) (0 : S)
⊢ HMul.hMul (α := S) (β := S) ((Polynomial.aeval x : (a : R[X]) → S) a : S)
      ((Polynomial.aeval x : (a : R[X]) → S) b : S) =
    0

Tactic:
rw [aeval_mul] at h

Premises used: Polynomial.aeval_mul
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
hx : IsIntegral R x
a b : R[X]
h : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) (a * b) : S) (0 : S)
h' : ¬Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) a : S) (0 : S)
h₁ :
  HMul.hMul (α := S) (β := S) ((Polynomial.aeval x : (a : R[X]) → S) a : S)
      ((Polynomial.aeval x : (a : R[X]) → S) b : S) =
    0
⊢ ¬Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) a : S) (0 : S)

Tactic:
rw [aeval_mul] at h

Premises used: Polynomial.aeval_mul
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
hx : IsIntegral R x
a b : R[X]
h :
  HMul.hMul (α := S) (β := S) ((Polynomial.aeval x : (a : R[X]) → S) a : S)
      ((Polynomial.aeval x : (a : R[X]) → S) b : S) =
    0
h' : ¬Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) a : S) (0 : S)
⊢ Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) b : S) (0 : S)

Tactic:
eq_zero_of_ne_zero_of_mul_left_eq_zero h' h

Premises used: eq_zero_of_ne_zero_of_mul_left_eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
x : S
hx : IsIntegral R x
a b : R[X]
h :
  HMul.hMul (α := S) (β := S) ((Polynomial.aeval x : (a : R[X]) → S) a : S)
      ((Polynomial.aeval x : (a : R[X]) → S) b : S) =
    0
h' : ¬Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) a : S) (0 : S)
⊢ Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) b : S) (0 : S)

Tactic:
exact eq_zero_of_ne_zero_of_mul_left_eq_zero h' h

Premises used: eq_zero_of_ne_zero_of_mul_left_eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
a : map (algebraMap R K) (minpoly R (r • s)) = map (algebraMap R K) (scaleRoots (minpoly R s) r)
⊢ Eq (α := R[X]) (minpoly R (r • s)) (scaleRoots (minpoly R s) r)

Tactic:
apply map_injective _ (FaithfulSMul.algebraMap_injective R K)

Premises used: Polynomial.map_injective, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ Ne (α := K) ((algebraMap R K : (a : R) → K) (leadingCoeff (minpoly R s)) : K) (0 : K)

Tactic:
simpa [minpoly.ne_zero_iff]

Premises used: minpoly.ne_zero_iff
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
a :
  Eq (α := K[X]) (minpoly K (B := L) ((algebraMap S L : (a : S) → L) (r • s) : L))
    (scaleRoots (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L)) ((algebraMap R K : (a : R) → K) r))
⊢ map (algebraMap R K) (minpoly R (r • s)) = map (algebraMap R K) (scaleRoots (minpoly R s) r)

Tactic:
rw [← minpoly.isIntegrallyClosed_eq_field_fractions K L (hs.smul r),
    map_scaleRoots _ _ _ (by simpa [minpoly.ne_zero_iff]),
    ← minpoly.isIntegrallyClosed_eq_field_fractions K L hs]

Premises used: minpoly.isIntegrallyClosed_eq_field_fractions, IsIntegral.smul, Polynomial.map_scaleRoots
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
a :
  Eq (α := K[X])
    (minpoly K
      (HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
        ((algebraMap S L : (a : S) → L) s : L)))
    (scaleRoots (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L)) ((algebraMap R K : (a : R) → K) r))
⊢ Eq (α := K[X]) (minpoly K (B := L) ((algebraMap S L : (a : S) → L) (r • s) : L))
    (scaleRoots (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L)) ((algebraMap R K : (a : R) → K) r))

Tactic:
simp_rw [Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply R K L]

Premises used: map_mul, Algebra.smul_def, IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ Eq (α := K[X])
    (minpoly K
      (HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
        ((algebraMap S L : (a : S) → L) s : L)))
    (scaleRoots (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L)) ((algebraMap R K : (a : R) → K) r))

Tactic:
eq_of_monic_of_associated (minpoly.monic ?_) ?_
    (associated_of_dvd_dvd (minpoly.dvd _ _ ?_) ?_)

Premises used: minpoly.monic, associated_of_dvd_dvd, minpoly.dvd, Polynomial.eq_of_monic_of_associated
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
a :
  IsIntegral K
    (HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
      ((algebraMap S L : (a : S) → L) s : L))
a₁ : Monic (scaleRoots (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L)) ((algebraMap R K : (a : R) → K) r))
a₂ :
  Eq.{u_2 + 1} (α := L)
    ((Polynomial.aeval
            (HMul.hMul (α := L) (β := L)
              (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
              ((algebraMap S L : (a : S) → L) s : L)) :
          (a : K[X]) → L)
        (scaleRoots (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L)) ((algebraMap R K : (a : R) → K) r)) :
      L)
    (0 : L)
a₃ :
  Dvd.dvd (α := K[X])
    (scaleRoots (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L)) ((algebraMap R K : (a : R) → K) r))
    (minpoly K
      (HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
        ((algebraMap S L : (a : S) → L) s : L)))
⊢ Eq (α := K[X])
    (minpoly K
      (HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
        ((algebraMap S L : (a : S) → L) s : L)))
    (scaleRoots (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L)) ((algebraMap R K : (a : R) → K) r))

Tactic:
refine eq_of_monic_of_associated (minpoly.monic ?_) ?_
    (associated_of_dvd_dvd (minpoly.dvd _ _ ?_) ?_)

Premises used: minpoly.monic, associated_of_dvd_dvd, minpoly.dvd, Polynomial.eq_of_monic_of_associated
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ IsIntegral K
    (HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
      ((algebraMap S L : (a : S) → L) s : L))

Tactic:
isIntegral_algebraMap.mul (hs.map (IsScalarTower.toAlgHom R S L)).tower_top

Premises used: IsIntegral.mul, Set.Mem, IsScalarTower.toAlgHom, isIntegral_algebraMap, IsIntegral.map, IsIntegral.tower_top
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ IsIntegral K
    (HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap R K : (a : R) → K) r) : L)
      ((algebraMap S L : (a : S) → L) s : L))

Tactic:
refine isIntegral_algebraMap.mul (hs.map (IsScalarTower.toAlgHom R S L)).tower_top

Premises used: IsIntegral.mul, IsScalarTower.toAlgHom, isIntegral_algebraMap, IsIntegral.map, IsIntegral.tower_top
-- Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : Algebra R S
inst_4 : IsIntegrallyClosed R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ Monic (scaleRoots (minpoly K (B := L) ((algebraMap S L : (a : S) → L) s : L)) ((algebraMap R K : (a : R) → K) r))

Tactic:
simpa [monic_scaleRoots_iff] using minpoly.monic
      (hs.map (IsScalarTower.toAlgHom R S L)).tower_top

Premises used: minpoly.monic, IsScalarTower.toAlgHom, IsIntegral.map, IsIntegral.tower_top, Polynomial.monic_scaleRoots_iff