awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommRing R
f : R[X]
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : R
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
⊢ ∃ (y : S),
    Membership.mem (γ := Subalgebra R S) R[x] y ∧ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) y = x ^ i
have obtain : ∀ (k : ℕ) (hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k),
  ∃ (y : S),
    Membership.mem (γ := Subalgebra R S) R[x] y ∧ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) y = x ^ i
Tactic: obtain ⟨k, hk⟩ := exists_add_of_le hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommRing R
f : R[X]
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : R
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ ∃ (y : S),
    Membership.mem (γ := Subalgebra R S) R[x] y ∧ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) y = x ^ i
have rw : ∃ (y : S),
  Membership.mem (γ := Subalgebra R S) R[x] y ∧
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) y =
      x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
Tactic: rw [hk, pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommRing R
f : R[X]
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : R
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ ∃ (y : S),
    Membership.mem (γ := Subalgebra R S) R[x] y ∧
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) y =
        x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
have obtain : ∀ (y : S) (hy : Membership.mem (γ := Subalgebra R S) R[x] y)
  (H : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) y = x ^ natDegree (Polynomial.map (algebraMap R S) f)),
  ∃ (y : S),
    Membership.mem (γ := Subalgebra R S) R[x] y ∧
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) y =
        x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
Tactic: obtain ⟨y, hy, H⟩ := exists_mem_adjoin_mul_eq_pow_natDegree hx hmo hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommRing R
f : R[X]
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : R
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
y : S
hy : Membership.mem (γ := Subalgebra R S) R[x] y
H : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
⊢ ∃ (y : S),
    Membership.mem (γ := Subalgebra R S) R[x] y ∧
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) y =
        x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
have refine_1 : Membership.mem (γ := Subalgebra R S) R[x] (y * x ^ k)
Tactic: refine ⟨y * x ^ k, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommRing R
f : R[X]
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : R
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
y : S
hy : Membership.mem (γ := Subalgebra R S) R[x] y
H : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
refine_1 : Membership.mem (γ := Subalgebra R S) R[x] (y * x ^ k)
⊢ ∃ (y : S),
    Membership.mem (γ := Subalgebra R S) R[x] y ∧
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) y =
        x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
have refine_2 : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) (y * x ^ k) =
  x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
Tactic: refine ⟨y * x ^ k, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommRing R
f : R[X]
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : R
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
y : S
hy : Membership.mem (γ := Subalgebra R S) R[x] y
H : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) (y * x ^ k) =
    x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
have refine_2 : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) y * x ^ k =
  x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
Tactic: rw [← mul_assoc _ y, H]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommRing R
f : R[X]
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : R
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
y : S
hy : Membership.mem (γ := Subalgebra R S) R[x] y
H : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
refine_2 :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) y * x ^ k =
    x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) (y * x ^ k) =
    x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
have refine_2₁ : x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k = x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
Tactic: rw [← mul_assoc _ y, H]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : f.IsRoot x
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
⊢ x ^ i ∈ 𝓟
have obtain : ∀ (k : ℕ) (hk : i = f.natDegree + k), x ^ i ∈ 𝓟
Tactic: obtain ⟨k, hk⟩ := exists_add_of_le hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : f.IsRoot x
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ x ^ i ∈ 𝓟
have rw : x ^ f.natDegree * x ^ k ∈ 𝓟
Tactic: rw [hk, pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : f.IsRoot x
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ x ^ f.natDegree * x ^ k ∈ 𝓟
have suffices : x ^ f.natDegree ∈ 𝓟
Tactic: suffices x ^ f.natDegree ∈ 𝓟 by exact mul_mem_right (x ^ k) 𝓟 this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : f.IsRoot x
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ x ^ f.natDegree ∈ 𝓟
have rw : ∀ (hroot : x ^ f.natDegree + ∑ i : Fin f.natDegree, f.coeff (↑i : ℕ) * x ^ (↑i : ℕ) = 0) (hmo : f.Monic) (i : ℕ)
  (hi : f.natDegree ≤ i) (k : ℕ) (hk : i = f.natDegree + k), x ^ f.natDegree ∈ 𝓟
Tactic: rw [IsRoot.def, eval_eq_sum_range, Finset.range_add_one,
    Finset.sum_insert Finset.notMem_range_self, Finset.sum_range, hmo.coeff_natDegree, one_mul] at
    *
Cleared hypotheses: hroot, hmo, i, hi, k, hk
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : x ^ f.natDegree + ∑ i : Fin f.natDegree, f.coeff (↑i : ℕ) * x ^ (↑i : ℕ) = 0
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ x ^ f.natDegree ∈ 𝓟
have rw : ∑ i : Fin f.natDegree, f.coeff (↑i : ℕ) * x ^ (↑i : ℕ) ∈ 𝓟
Tactic: rw [eq_neg_of_add_eq_zero_left hroot, neg_mem_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
hmo : f.Monic
this :
  Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 𝓟)
    (x ^ natDegree (Polynomial.map (algebraMap R S) f))
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 𝓟) (x ^ i)
have obtain : ∀ (k : ℕ) (hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k),
  Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 𝓟) (x ^ i)
Tactic: obtain ⟨k, hk⟩ := exists_add_of_le hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
hmo : f.Monic
this :
  Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 𝓟)
    (x ^ natDegree (Polynomial.map (algebraMap R S) f))
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 𝓟) (x ^ i)
have rw : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 𝓟)
  (x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k)
Tactic: rw [hk, pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
hmo : f.Monic
⊢ ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R S) f) ≤ i →
      Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 𝓟) (x ^ i)
have suffices : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 𝓟)
  (x ^ natDegree (Polynomial.map (algebraMap R S) f))
Tactic: suffices x ^ (f.map (algebraMap R S)).natDegree ∈ 𝓟.map (algebraMap R S) by
    intro i hi
    obtain ⟨k, hk⟩ := exists_add_of_le hi
    rw [hk, pow_add]
    exact mul_mem_right _ _ this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
hmo : f.Monic
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 𝓟)
    (x ^ natDegree (Polynomial.map (algebraMap R S) f))
have hx₁ : IsRoot (Polynomial.map (algebraMap R S) f) x
Tactic: rw [aeval_def, eval₂_eq_eval_map, ← IsRoot.def] at hx
Cleared hypotheses: hx, hmo
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
⊢ (p.scaleRoots x).IsWeaklyEisensteinAt P
have refine : ∀ {n : ℕ} (i : n < (p.scaleRoots x).natDegree), (p.scaleRoots x).coeff n ∈ P
Tactic: refine ⟨fun i => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n : ℕ
i : n < (p.scaleRoots x).natDegree
⊢ (p.scaleRoots x).coeff n ∈ P
have rw : p.coeff n * x ^ (p.natDegree - n) ∈ P
Tactic: rw [coeff_scaleRoots]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n : ℕ
i : n < (p.scaleRoots x).natDegree
⊢ p.coeff n * x ^ (p.natDegree - n) ∈ P
have i₁ : 0 < p.natDegree - n
Tactic: rw [natDegree_scaleRoots, ← tsub_pos_iff_lt] at i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : HMul.hMul (α := A) ((f : (a : R) → A) x : A) z = (f : (a : R) → A) y
⊢ x ∣ y ^ p.natDegree
have rw : Membership.mem (γ := Ideal R) (span {x}) (y ^ (p.scaleRoots x).natDegree)
Tactic: rw [← natDegree_scaleRoots p x, ← Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : HMul.hMul (α := A) ((f : (a : R) → A) x : A) z = (f : (a : R) → A) y
⊢ Membership.mem (γ := Ideal R) (span {x}) (y ^ (p.scaleRoots x).natDegree)
have dvd_refl : (p.scaleRoots x).IsRoot y
Tactic: refine
    (scaleRoots.isWeaklyEisensteinAt _
          (Ideal.mem_span_singleton.mpr <| dvd_refl x)).pow_natDegree_le_of_root_of_monic_mem
      ?_ ((monic_scaleRoots_iff x).mpr hp) _ le_rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : HMul.hMul (α := A) ((f : (a : R) → A) x : A) z = (f : (a : R) → A) y
⊢ (p.scaleRoots x).IsRoot y
have rw : ∀ (hf : ∀ (a : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) a : A) (0 : A) ↔ a = 0) {p : R[X]} (hp : p.Monic) (x y : R)
  (z : A) (h : eval₂ f z p = 0) (hz : HMul.hMul (α := A) ((f : (a : R) → A) x : A) z = (f : (a : R) → A) y),
  (p.scaleRoots x).IsRoot y
Tactic: rw [injective_iff_map_eq_zero'] at hf
Cleared hypotheses: hf, p, hp, x, y, z, h, hz
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (hypothesis)
Goal:
R : Type u
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
f : R →+* A
hf : ∀ (a : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) a : A) (0 : A) ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : HMul.hMul (α := A) ((f : (a : R) → A) x : A) z = (f : (a : R) → A) y
⊢ (p.scaleRoots x).IsRoot y
have this : eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) x : A) z) (p.scaleRoots x) = 0
Tactic: have : eval₂ f _ (p.scaleRoots x) = 0 := scaleRoots_eval₂_eq_zero f h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
f : R →+* A
hf : ∀ (a : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) a : A) (0 : A) ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : HMul.hMul (α := A) ((f : (a : R) → A) x : A) z = (f : (a : R) → A) y
this : eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) x : A) z) (p.scaleRoots x) = 0
⊢ (p.scaleRoots x).IsRoot y
have rwa : ∀ (this : eval₂ f ((f : (a : R) → A) y) (p.scaleRoots x) = 0), (p.scaleRoots x).IsRoot y
Tactic: rwa [hz, Polynomial.eval₂_at_apply, hf] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
f : R →+* A
hf : ∀ (a : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) a : A) (0 : A) ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : HMul.hMul (α := A) ((f : (a : R) → A) x : A) z = (f : (a : R) → A) y
this : eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) x : A) z) (p.scaleRoots x) = 0
rwa : ∀ (this : eval₂ f ((f : (a : R) → A) y) (p.scaleRoots x) = 0), (p.scaleRoots x).IsRoot y
⊢ (p.scaleRoots x).IsRoot y
have rwa₁ : ∀ (this : Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) (eval y (p.scaleRoots x)) : A) (0 : A)), (p.scaleRoots x).IsRoot y
Tactic: rwa [hz, Polynomial.eval₂_at_apply, hf] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
f : R →+* A
hf : ∀ (a : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) a : A) (0 : A) ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : HMul.hMul (α := A) ((f : (a : R) → A) x : A) z = (f : (a : R) → A) y
this : eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) x : A) z) (p.scaleRoots x) = 0
rwa : ∀ (this : eval₂ f ((f : (a : R) → A) y) (p.scaleRoots x) = 0), (p.scaleRoots x).IsRoot y
rwa₁ :
  ∀ (this : Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) (eval y (p.scaleRoots x)) : A) (0 : A)), (p.scaleRoots x).IsRoot y
⊢ (p.scaleRoots x).IsRoot y
have rwa₂ : ∀ (this : eval y (p.scaleRoots x) = 0), (p.scaleRoots x).IsRoot y
Tactic: rwa [hz, Polynomial.eval₂_at_apply, hf] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
⊢ f.coeff n ∈ 𝓟
have inl : ∀ (h₁ : n < f.natDegree), f.coeff n ∈ 𝓟
Tactic: rcases ne_iff_lt_or_gt.1 hn with h₁ | h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
inl : ∀ (h₁ : n < f.natDegree), f.coeff n ∈ 𝓟
⊢ f.coeff n ∈ 𝓟
have inr : ∀ (h₂ : f.natDegree < n), f.coeff n ∈ 𝓟
Tactic: rcases ne_iff_lt_or_gt.1 hn with h₁ | h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
h₂ : f.natDegree < n
⊢ f.coeff n ∈ 𝓟
have inr : 0 ∈ 𝓟
Tactic: rw [coeff_eq_zero_of_natDegree_lt h₂]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hf_prim : f.IsPrimitive
hfmodP :
  map (algebraMap R K) f =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) f.leadingCoeff) : K[X])
      (HPow.hPow (α := K[X]) (map (algebraMap R K) q) p)
hg_div : g ∣ f
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
⊢ ∃ (m : ℕ) (r : R[X]),
    g = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) + r ∧
      Eq (α := K[X]) (map (algebraMap R K) r) 0 ∧ (m = 0 → IsUnit g)
have hP : P.IsPrime
Tactic: have hP : P.IsPrime := ker_isPrime (algebraMap R K)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hf_prim : f.IsPrimitive
hfmodP :
  map (algebraMap R K) f =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) f.leadingCoeff) : K[X])
      (HPow.hPow (α := K[X]) (map (algebraMap R K) q) p)
hg_div : g ∣ f
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
⊢ g.leadingCoeff ∉ P
have simp : ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) g.leadingCoeff : K) (0 : K)
Tactic: simp only [mem_ker, P]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hf_prim : f.IsPrimitive
hfmodP :
  map (algebraMap R K) f =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) f.leadingCoeff) : K[X])
      (HPow.hPow (α := K[X]) (map (algebraMap R K) q) p)
hg_div : g ∣ f
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
⊢ ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) g.leadingCoeff : K) (0 : K)
have obtain : ∀ (h : R[X]) (hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (g * h).leadingCoeff : K) (0 : K))
  (hf_prim : (g * h).IsPrimitive)
  (hfmodP :
    map (algebraMap R K) (g * h) =
      HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) (g * h).leadingCoeff) : K[X])
        (HPow.hPow (α := K[X]) (map (algebraMap R K) q) p)),
  ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) g.leadingCoeff : K) (0 : K)
Tactic: obtain ⟨h, rfl⟩ := hg_div
Cleared hypotheses: f, hf_lC, hf_prim, hfmodP, hg_div
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
h : R[X]
hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (g * h).leadingCoeff : K) (0 : K)
hf_prim : (g * h).IsPrimitive
hfmodP :
  map (algebraMap R K) (g * h) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) (g * h).leadingCoeff) : K[X])
      (HPow.hPow (α := K[X]) (map (algebraMap R K) q) p)
⊢ ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) g.leadingCoeff : K) (0 : K)
have hf_lC₁ : ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) g.leadingCoeff : K) (0 : K) ∧
  ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) h.leadingCoeff : K) (0 : K)
Tactic: simp only [leadingCoeff_mul, map_mul, ne_eq, mul_eq_zero, not_or] at hf_lC
Cleared hypotheses: hf_lC
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hf_prim : f.IsPrimitive
hfmodP :
  map (algebraMap R K) f =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) f.leadingCoeff) : K[X])
      (HPow.hPow (α := K[X]) (map (algebraMap R K) q) p)
hg_div : g ∣ f
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
⊢ ∃ (m : ℕ) (r : R[X]),
    g = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) + r ∧
      Eq (α := K[X]) (map (algebraMap R K) r) 0 ∧ (m = 0 → IsUnit g)
have hgP : g.leadingCoeff ∉ P
Tactic: have hgP : g.leadingCoeff ∉ P := by
    simp only [mem_ker, P]
    obtain ⟨h, rfl⟩ := hg_div
    simp only [leadingCoeff_mul, map_mul, ne_eq, mul_eq_zero, not_or] at hf_lC
    exact hf_lC.1