awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : (m : ℕ) → R
hg :
  ∀ k ∈ range (j + 1),
    Q.coeff k • B.gen ^ k = HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g k • B.gen ^ k)
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
hf₁ :
  ∀ k ∈ (range (Q.natDegree - j)).erase 0,
    Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
      HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (Q.coeff (j + 1 + k) • f (k + P.natDegree - 1))
hQ :
  Eq.{v + 1} (α := K)
    ((Algebra.norm K : (a : L) → K)
        (HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) (Q.coeff (j + 1)) : L)
          (B.gen ^ (j + 1 + (P.natDegree - (j + 2))))) :
      K)
    ((Algebra.norm K : (a : L) → K)
        (p • z * B.gen ^ (P.natDegree - (j + 2)) -
          HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L)
            (HAdd.hAdd (α := L) (∑ i ∈ (range (Q.natDegree - j)).erase 0, Q.coeff (j + 1 + i) • f (i + P.natDegree - 1))
              (∑ i ∈ range (j + 1), g i • B.gen ^ i * B.gen ^ (P.natDegree - (j + 2))))) :
      K)
hintsum :
  IsIntegral R
    (z * B.gen ^ (P.natDegree - (j + 2)) -
      HAdd.hAdd (α := L) (∑ x ∈ (range (Q.natDegree - j)).erase 0, Q.coeff (j + 1 + x) • f (x + P.natDegree - 1))
        (∑ x ∈ range (j + 1), g x • B.gen ^ x * B.gen ^ (P.natDegree - (j + 2))))
⊢ p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * coeff (minpoly R B.gen) 0 ^ (j.succ + (P.natDegree - (j + 2)))
have neg : ∀ (r : R)
  (hr :
    Eq.{v + 1} (α := K) ((algebraMap R K : (a : R) → K) r : K)
      ((Algebra.norm K : (a : L) → K)
          (z * B.gen ^ (P.natDegree - (j + 2)) -
            HAdd.hAdd (α := L) (∑ x ∈ (range (Q.natDegree - j)).erase 0, Q.coeff (j + 1 + x) • f (x + P.natDegree - 1))
              (∑ x ∈ range (j + 1), g x • B.gen ^ x * B.gen ^ (P.natDegree - (j + 2)))) :
        K)),
  p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * coeff (minpoly R B.gen) 0 ^ (j.succ + (P.natDegree - (j + 2)))
Tactic: obtain ⟨r, hr⟩ := isIntegral_iff.1 (isIntegral_norm K hintsum)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : (m : ℕ) → R
hg :
  ∀ k ∈ range (j + 1),
    Q.coeff k • B.gen ^ k = HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g k • B.gen ^ k)
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
hf₁ :
  ∀ k ∈ (range (Q.natDegree - j)).erase 0,
    Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
      HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (Q.coeff (j + 1 + k) • f (k + P.natDegree - 1))
hintsum :
  IsIntegral R
    (z * B.gen ^ (P.natDegree - (j + 2)) -
      HAdd.hAdd (α := L) (∑ x ∈ (range (Q.natDegree - j)).erase 0, Q.coeff (j + 1 + x) • f (x + P.natDegree - 1))
        (∑ x ∈ range (j + 1), g x • B.gen ^ x * B.gen ^ (P.natDegree - (j + 2))))
r : R
hQ :
  Eq.{v + 1} (α := K)
    ((algebraMap R K : (a : R) → K)
        (Q.coeff (j + 1) ^ B.dim *
          (HPow.hPow (α := R) (-1) B.dim * coeff (minpoly R B.gen) 0) ^ (j + 1 + (P.natDegree - (j + 2)))) :
      K)
    ((algebraMap R K : (a : R) → K) (p ^ B.dim * r) : K)
hr :
  Eq.{v + 1} (α := K) ((algebraMap R K : (a : R) → K) r : K)
    ((Algebra.norm K : (a : L) → K)
        (z * B.gen ^ (P.natDegree - (j + 2)) -
          HAdd.hAdd (α := L) (∑ x ∈ (range (Q.natDegree - j)).erase 0, Q.coeff (j + 1 + x) • f (x + P.natDegree - 1))
            (∑ x ∈ range (j + 1), g x • B.gen ^ x * B.gen ^ (P.natDegree - (j + 2)))) :
      K)
⊢ p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * coeff (minpoly R B.gen) 0 ^ (j.succ + (P.natDegree - (j + 2)))
have hppdiv : p ^ B.dim ∣ p ^ B.dim * r
Tactic: have hppdiv : p ^ B.dim ∣ p ^ B.dim * r := dvd_mul_of_dvd_left dvd_rfl _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : (m : ℕ) → R
hg :
  ∀ k ∈ range (j + 1),
    Q.coeff k • B.gen ^ k = HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g k • B.gen ^ k)
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
hf₁ :
  ∀ k ∈ (range (Q.natDegree - j)).erase 0,
    Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
      HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (Q.coeff (j + 1 + k) • f (k + P.natDegree - 1))
hintsum :
  IsIntegral R
    (z * B.gen ^ (P.natDegree - (j + 2)) -
      HAdd.hAdd (α := L) (∑ x ∈ (range (Q.natDegree - j)).erase 0, Q.coeff (j + 1 + x) • f (x + P.natDegree - 1))
        (∑ x ∈ range (j + 1), g x • B.gen ^ x * B.gen ^ (P.natDegree - (j + 2))))
r : R
hQ :
  Eq.{v + 1} (α := K)
    ((algebraMap R K : (a : R) → K)
        (Q.coeff (j + 1) ^ B.dim *
          (HPow.hPow (α := R) (-1) B.dim * coeff (minpoly R B.gen) 0) ^ (j + 1 + (P.natDegree - (j + 2)))) :
      K)
    ((algebraMap R K : (a : R) → K) (p ^ B.dim * r) : K)
hr :
  Eq.{v + 1} (α := K) ((algebraMap R K : (a : R) → K) r : K)
    ((Algebra.norm K : (a : L) → K)
        (z * B.gen ^ (P.natDegree - (j + 2)) -
          HAdd.hAdd (α := L) (∑ x ∈ (range (Q.natDegree - j)).erase 0, Q.coeff (j + 1 + x) • f (x + P.natDegree - 1))
            (∑ x ∈ range (j + 1), g x • B.gen ^ x * B.gen ^ (P.natDegree - (j + 2)))) :
      K)
hppdiv : p ^ B.dim ∣ p ^ B.dim * r
⊢ p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * coeff (minpoly R B.gen) 0 ^ (j.succ + (P.natDegree - (j + 2)))
have neg : ∀
  (hppdiv :
    p ^ B.dim ∣
      Q.coeff (j + 1) ^ B.dim *
        (HPow.hPow (α := R) (-1) B.dim * coeff (minpoly R B.gen) 0) ^ (j + 1 + (P.natDegree - (j + 2)))),
  p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * coeff (minpoly R B.gen) 0 ^ (j.succ + (P.natDegree - (j + 2)))
Tactic: rwa [← IsFractionRing.injective R K hQ, mul_comm, ← Units.coe_neg_one, mul_pow, ←
      Units.val_pow_eq_pow_val, ← Units.val_pow_eq_pow_val, mul_assoc,
      Units.dvd_mul_left, mul_comm, ← Nat.succ_eq_add_one, hn] at hppdiv
Cleared hypotheses: hppdiv
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
n : ℕ
hn : ∀ (hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p ^ n • z)), Membership.mem (γ := Subalgebra R L) R[B.gen] z
hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p ^ (n + 1) • z)
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z
have hz₁ : Membership.mem (γ := Subalgebra R L) R[B.gen] (p • p ^ n • z)
Tactic: rw [_root_.pow_succ', mul_smul] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
n : ℕ
z : L
hzint : IsIntegral R z
hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p ^ n • z)
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z
have zero : ∀ (hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (HPow.hPow (β := ℕ) p 0 • z)),
  Membership.mem (γ := Subalgebra R L) R[B.gen] z
Tactic: induction n with
  | zero => simpa using hz
  | succ n hn =>
    rw [_root_.pow_succ', mul_smul] at hz
    exact
      hn (mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt hp hBint (hzint.smul _) hz hei)
Cleared hypotheses: n, hz
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
n : ℕ
z : L
hzint : IsIntegral R z
hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p ^ n • z)
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
zero :
  ∀ (hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (HPow.hPow (β := ℕ) p 0 • z)),
    Membership.mem (γ := Subalgebra R L) R[B.gen] z
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z
have succ : ∀ (n : ℕ)
  (hn :
    ∀ (hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p ^ n • z)), Membership.mem (γ := Subalgebra R L) R[B.gen] z)
  (hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p ^ (n + 1) • z)),
  Membership.mem (γ := Subalgebra R L) R[B.gen] z
Tactic: induction n with
  | zero => simpa using hz
  | succ n hn =>
    rw [_root_.pow_succ', mul_smul] at hz
    exact
      hn (mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt hp hBint (hzint.smul _) hz hei)
Cleared hypotheses: n, hz
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ↥(integralClosure R K)) (algebraMap (↥(integralClosure R K)) K)) g
have refine_2 : ∀
  (this :
    Membership.mem (γ := Subsemiring g.SplittingField[X])
      (lifts (R := ↥(integralClosure R g.SplittingField))
        (algebraMap (↥(integralClosure R g.SplittingField)) g.SplittingField))
      (map (algebraMap K g.SplittingField) g)),
  Membership.mem (γ := Subsemiring K[X]) (lifts (R := ↥(integralClosure R K)) (algebraMap (↥(integralClosure R K)) K)) g
Tactic: have := (SplittingField.splits g).mem_lift_of_roots_mem_range (hg.map _)
    (algebraMap (integralClosure R g.SplittingField) g.SplittingField)
     fun a ha =>
      (SetLike.ext_iff.mp (integralClosure R g.SplittingField).range_algebraMap _).mpr <|
        roots_mem_integralClosure hf ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
refine_2 :
  ∀
    (this :
      Membership.mem (γ := Subsemiring g.SplittingField[X])
        (lifts (R := ↥(integralClosure R g.SplittingField))
          (algebraMap (↥(integralClosure R g.SplittingField)) g.SplittingField))
        (map (algebraMap K g.SplittingField) g)),
    Membership.mem (γ := Subsemiring K[X]) (lifts (R := ↥(integralClosure R K)) (algebraMap (↥(integralClosure R K)) K))
      g
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ↥(integralClosure R K)) (algebraMap (↥(integralClosure R K)) K)) g
have refine_1 : ∀ (a : g.SplittingField)
  (ha : Membership.mem (γ := Multiset g.SplittingField) (roots (map (algebraMap K g.SplittingField) g)) a),
  Membership.mem (γ := Multiset g.SplittingField) (f.aroots g.SplittingField) a
Tactic: have := (SplittingField.splits g).mem_lift_of_roots_mem_range (hg.map _)
    (algebraMap (integralClosure R g.SplittingField) g.SplittingField)
     fun a ha =>
      (SetLike.ext_iff.mp (integralClosure R g.SplittingField).range_algebraMap _).mpr <|
        roots_mem_integralClosure hf ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  Membership.mem (γ := Subsemiring g.SplittingField[X])
    (lifts (R := ↥(integralClosure R g.SplittingField))
      (algebraMap (↥(integralClosure R g.SplittingField)) g.SplittingField))
    (map (algebraMap K g.SplittingField) g)
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ↥(integralClosure R K)) (algebraMap (↥(integralClosure R K)) K)) g
have this₁ : ∀ (n : ℕ),
  coeff (map (algebraMap K g.SplittingField) g) n ∈
    (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)
Tactic: rw [lifts_iff_coeff_lifts, ← RingHom.coe_range, Subalgebra.range_algebraMap] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K g.SplittingField) g) n ∈
      (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ↥(integralClosure R K)) (algebraMap (↥(integralClosure R K)) K)) g
have refine_2 : ∀ (n : ℕ),
  Membership.mem (γ := Set K)
    (Set.range (ι := ↥(integralClosure R K))
      (⇑(algebraMap (↥(integralClosure R K)) K) : (a : ↥(integralClosure R K)) → K))
    (g.coeff n)
Tactic: refine (lifts_iff_coeff_lifts _).2 fun n => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K g.SplittingField) g) n ∈
      (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)
n : ℕ
⊢ Membership.mem (γ := Set K)
    (Set.range (ι := ↥(integralClosure R K))
      (⇑(algebraMap (↥(integralClosure R K)) K) : (a : ↥(integralClosure R K)) → K))
    (g.coeff n)
have refine_2 : g.coeff n ∈ (↑(Subalgebra.toSubring (integralClosure R K)) : Set K)
Tactic: rw [← RingHom.coe_range, Subalgebra.range_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K g.SplittingField) g) n ∈
      (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)
n : ℕ
⊢ g.coeff n ∈ (↑(Subalgebra.toSubring (integralClosure R K)) : Set K)
have refine_2 : ∀ (p : R[X]) (hp : p.Monic)
  (he :
    Eq (α := g.SplittingField)
      (eval₂ (algebraMap R g.SplittingField) (coeff (map (algebraMap K g.SplittingField) g) n) p) 0),
  g.coeff n ∈ (↑(Subalgebra.toSubring (integralClosure R K)) : Set K)
Tactic: obtain ⟨p, hp, he⟩ := SetLike.mem_coe.mp (this n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K g.SplittingField) g) n ∈
      (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)
n : ℕ
p : R[X]
hp : p.Monic
he :
  Eq (α := g.SplittingField) (eval₂ (algebraMap R g.SplittingField) (coeff (map (algebraMap K g.SplittingField) g) n) p)
    0
⊢ g.coeff n ∈ (↑(Subalgebra.toSubring (integralClosure R K)) : Set K)
have right : eval₂ (algebraMap R K) (g.coeff n) p = 0
Tactic: use p, hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K g.SplittingField) g) n ∈
      (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)
n : ℕ
p : R[X]
hp : p.Monic
he :
  Eq (α := g.SplittingField) (eval₂ (algebraMap R g.SplittingField) (coeff (map (algebraMap K g.SplittingField) g) n) p)
    0
⊢ eval₂ (algebraMap R K) (g.coeff n) p = 0
have he₁ : Eq (α := g.SplittingField)
  ((algebraMap K g.SplittingField : (a : K) → g.SplittingField) (eval (g.coeff n) (map (algebraMap R K) p)) :
    g.SplittingField)
  (0 : g.SplittingField)
Tactic: rw [IsScalarTower.algebraMap_eq R K, coeff_map, ← eval₂_map, eval₂_at_apply] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K g.SplittingField) g) n ∈
      (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)
n : ℕ
p : R[X]
hp : p.Monic
he :
  Eq (α := g.SplittingField)
    ((algebraMap K g.SplittingField : (a : K) → g.SplittingField) (eval (g.coeff n) (map (algebraMap R K) p)) :
      g.SplittingField)
    (0 : g.SplittingField)
⊢ eval₂ (algebraMap R K) (g.coeff n) p = 0
have right : eval (g.coeff n) (map (algebraMap R K) p) = 0
Tactic: rw [eval₂_eq_eval_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K g.SplittingField) g) n ∈
      (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)
n : ℕ
p : R[X]
hp : p.Monic
he :
  Eq (α := g.SplittingField)
    ((algebraMap K g.SplittingField : (a : K) → g.SplittingField) (eval (g.coeff n) (map (algebraMap R K) p)) :
      g.SplittingField)
    (0 : g.SplittingField)
⊢ eval (g.coeff n) (map (algebraMap R K) p) = 0
have apply : Function.Injective (α := K) (β := g.SplittingField) (⇑(algebraMap K g.SplittingField) : (a : K) → g.SplittingField)
Tactic: apply (injective_iff_map_eq_zero _).1 _ _ he
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
a : g.SplittingField
ha : Membership.mem (γ := Multiset g.SplittingField) (roots (map (algebraMap K g.SplittingField) g)) a
⊢ Membership.mem (γ := Multiset g.SplittingField) (f.aroots g.SplittingField) a
have refine_1 : Membership.mem (γ := Multiset g.SplittingField) (roots (map (algebraMap K g.SplittingField) (map (algebraMap R K) f))) a
Tactic: rw [aroots_def, IsScalarTower.algebraMap_eq R K _, ← map_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
a : g.SplittingField
ha : Membership.mem (γ := Multiset g.SplittingField) (roots (map (algebraMap K g.SplittingField) g)) a
⊢ Membership.mem (γ := Multiset g.SplittingField) (roots (map (algebraMap K g.SplittingField) (map (algebraMap R K) f)))
    a
have refine_1 : Dvd.dvd (α := g.SplittingField[X]) (map (algebraMap K g.SplittingField) g)
  (map (algebraMap K g.SplittingField) (map (algebraMap R K) f))
Tactic: refine Multiset.mem_of_le (roots.le_of_dvd ((hf.map _).map _).ne_zero ?_) ha
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
⊢ ∃ (g' : R[X]),
    HMul.hMul (α := K[X]) (β := K[X]) (map (algebraMap R K) g') ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) = g
have g_ne_0 : g ≠ 0
Tactic: have g_ne_0 : g ≠ 0 := ne_zero_of_dvd_ne_zero (Monic.ne_zero <| hf.map (algebraMap R K)) hg
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
lem : ∃ (g' : R[X]), map (algebraMap R K) g' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
⊢ ∃ (g' : R[X]),
    HMul.hMul (α := K[X]) (β := K[X]) (map (algebraMap R K) g') ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) = g
have obtain : ∀ (g' : R[X]) (hg' : map (algebraMap R K) g' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])),
  ∃ (g' : R[X]),
    HMul.hMul (α := K[X]) (β := K[X]) (map (algebraMap R K) g') ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) = g
Tactic: obtain ⟨g', hg'⟩ := lem
Cleared hypotheses: lem
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g' : R[X]
hg' : map (algebraMap R K) g' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
⊢ ∃ (g' : R[X]),
    HMul.hMul (α := K[X]) (β := K[X]) (map (algebraMap R K) g') ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) = g
have h : HMul.hMul (α := K[X]) (β := K[X]) (map (algebraMap R K) g') ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) = g
Tactic: use g'