awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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]
hmo : P.Monic
hP : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) P : S) (0 : S)
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
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
⊢ leadingCoeff (minpoly R s) = P.leadingCoeff
have h : 1 = P.leadingCoeff
Tactic: rw [(monic hs).leadingCoeff, hmo.leadingCoeff]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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]
hmo : P.Monic
hP : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) P : S) (0 : S)
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
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
h : 1 = P.leadingCoeff
⊢ leadingCoeff (minpoly R s) = P.leadingCoeff
have h₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [(monic hs).leadingCoeff, hmo.leadingCoeff]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
⊢ IsIntegral R s ↔ (C : (a : R) → R[X]) p.leadingCoeff ∣ p
have refine_1 : ∀ (hInt : IsIntegral R s), (C : (a : R) → R[X]) p.leadingCoeff ∣ p
Tactic: refine ⟨fun hInt ↦ ?_, fun ⟨q, hMul⟩ ↦ minpoly.ne_zero_iff.mp ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
refine_1 : ∀ (hInt : IsIntegral R s), (C : (a : R) → R[X]) p.leadingCoeff ∣ p
⊢ IsIntegral R s ↔ (C : (a : R) → R[X]) p.leadingCoeff ∣ p
have refine_2 : (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),
    Ne (α := R[X]) (minpoly R s) 0
Tactic: refine ⟨fun hInt ↦ ?_, fun ⟨q, hMul⟩ ↦ minpoly.ne_zero_iff.mp ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hInt : IsIntegral R s
⊢ (C : (a : R) → R[X]) p.leadingCoeff ∣ p
have h : p = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (minpoly R s)
Tactic: use minpoly R s
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hInt : IsIntegral R s
⊢ p = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (minpoly R s)
have h : ∀ (q : R[X]) (hMul : p = minpoly R s * q),
  p = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (minpoly R s)
Tactic: have ⟨q, hMul⟩ := isIntegrallyClosed_dvd hInt hp
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
⊢ p = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (minpoly R s)
have h : q.degree ≤ 0
Tactic: suffices q.degree ≤ 0 by simp [degree_le_zero_iff.mp this ▸ hMul, minpoly.monic hInt, mul_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
⊢ q.degree ≤ 0
have h : degree (minpoly R s) + q.degree ≤ degree (minpoly R s) + 0
Tactic: apply WithBot.le_of_add_le_add_left <| Polynomial.degree_ne_bot.mpr <| minpoly.ne_zero hInt
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
⊢ degree (minpoly R s) + q.degree ≤ degree (minpoly R s) + 0
have h : degree (minpoly R s) + q.degree = p.degree
Tactic: convert! pmin _ (minpoly.monic hInt) (minpoly.aeval ..)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
h : degree (minpoly R s) + q.degree = p.degree
⊢ degree (minpoly R s) + q.degree ≤ degree (minpoly R s) + 0
have h₁ : degree (minpoly R s) + 0 = degree (minpoly R s)
Tactic: convert! pmin _ (minpoly.monic hInt) (minpoly.aeval ..)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
⊢ degree (minpoly R s) + q.degree = p.degree
have h : degree (minpoly R s) + q.degree = (minpoly R s * q).degree
Tactic: rw [hMul, degree_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
h : degree (minpoly R s) + q.degree = (minpoly R s * q).degree
⊢ degree (minpoly R s) + q.degree = p.degree
have h₁ : degree (minpoly R s) + q.degree = degree (minpoly R s) + q.degree
Tactic: rw [hMul, degree_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
⊢ degree (minpoly R s) + 0 = degree (minpoly R s)
have h : degree (minpoly R s) = degree (minpoly R s)
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
⊢ Ne (α := R[X]) (minpoly R s) 0
have h : minpoly R s = q
Tactic: convert! right_ne_zero_of_mul <| hMul ▸ h₀
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
have h : q.Monic
Tactic: refine IsIntegrallyClosed.minpoly.unique ?_ ?_ ?_ |>.symm
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
⊢ minpoly R s = q
have h₁ : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : R[X]) → S) q : S) (0 : S)
Tactic: refine IsIntegrallyClosed.minpoly.unique ?_ ?_ ?_ |>.symm
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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)
⊢ minpoly R s = q
have 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
Tactic: refine IsIntegrallyClosed.minpoly.unique ?_ ?_ ?_ |>.symm
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (hypothesis)
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.Monic
have this : leadingCoeff ((C : (a : R) → R[X]) p.leadingCoeff) * q.leadingCoeff = p.leadingCoeff
Tactic: have := hMul ▸ leadingCoeff_mul .. |>.symm
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (hypothesis)
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.Monic
have this₁ : q.leadingCoeff = 1
Tactic: simp only [leadingCoeff_C, ne_eq, leadingCoeff_eq_zero, h₀, not_false_eq_true, mul_eq_left₀]
        at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (hypothesis)
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) q : S) (0 : S)
have 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)
Tactic: have := congrArg (Polynomial.aeval s) hMul
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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)
have h_contra : ∀ (a b : R[X]) (h : minpoly R x ∣ a * b) (h' : ¬minpoly R x ∣ a), minpoly R x ∣ b
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' => ?_⟩⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
⊢ minpoly R x ∣ b
have 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)
Tactic: rw [← minpoly.isIntegrallyClosed_dvd_iff hx] at h' h ⊢
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (hypothesis)
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)
⊢ Eq.{u_2 + 1} (α := S) ((Polynomial.aeval x : (a : R[X]) → S) b : S) (0 : S)
have h₁ : 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
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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 (α := R[X]) (minpoly R (r • s)) (scaleRoots (minpoly R s) r)
have a : map (algebraMap R K) (minpoly R (r • s)) = map (algebraMap R K) (scaleRoots (minpoly R s) r)
Tactic: apply map_injective _ (FaithfulSMul.algebraMap_injective R K)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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
⊢ map (algebraMap R K) (minpoly R (r • s)) = map (algebraMap R K) (scaleRoots (minpoly R s) r)
have 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))
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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 (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))
have 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))
Tactic: simp_rw [Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply R K L]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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))
have 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))
Tactic: refine eq_of_monic_of_associated (minpoly.monic ?_) ?_
    (associated_of_dvd_dvd (minpoly.dvd _ _ ?_) ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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))
⊢ 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))
have a₁ : Monic (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 _ _ ?_) ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed (goal)
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))
⊢ 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))
have 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)
Tactic: refine eq_of_monic_of_associated (minpoly.monic ?_) ?_
    (associated_of_dvd_dvd (minpoly.dvd _ _ ?_) ?_)