awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
⊢ Membership.mem (γ := Set K)
    (⋃ (x : K),
      ⋃ (_ : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x), {y : K | x = y + y⁻¹ ∨ y = 0})
    x
have simp : ∃ (i : K), (∃ (y : K), i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
Tactic: simp only [exists_prop, Set.mem_iUnion, Ne, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
⊢ ∃ (i : K), (∃ (y : K), i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
have pos : ∀ (hx : x = 0), ∃ (i : K), (∃ (y : K), i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
pos : ∀ (hx : x = 0), ∃ (i : K), (∃ (y : K), i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
⊢ ∃ (i : K), (∃ (y : K), i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
have neg : ∀ (hx : ¬x = 0), ∃ (i : K), (∃ (y : K), i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : x = 0
⊢ ∃ (i : K), (∃ (y : K), i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
have pos : ∃ (i : K) (y : K), i = y + y⁻¹ ∧ ¬y = 0
Tactic: simp only [hx, and_true, inv_zero, or_true]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : ¬x = 0
⊢ ∃ (i : K), (∃ (y : K), i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
have neg : ∃ (y : K), x + x⁻¹ = y + y⁻¹ ∧ ¬y = 0
Tactic: simp only [hx, or_false, exists_eq_right]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP R p
⊢ dickson 1 1 p = HPow.hPow (α := R[X]) X p
have h : Eq (α := R) (1 : R) ((ZMod.castHom sorry R : (a : ZMod p) → R) 1 : R)
Tactic: have h : (1 : R) = ZMod.castHom (dvd_refl p) R 1 := by
    simp only [ZMod.castHom_apply, ZMod.cast_one']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP R p
h : Eq (α := R) (1 : R) ((ZMod.castHom ⋯ R : (a : ZMod p) → R) 1 : R)
⊢ dickson 1 1 p = HPow.hPow (α := R[X]) X p
have rw : dickson 1 ((ZMod.castHom sorry R : (a : ZMod p) → R) 1) p = HPow.hPow (α := R[X]) X p
Tactic: rw [h, ← map_dickson (ZMod.castHom (dvd_refl p) R), dickson_one_one_zmod_p, Polynomial.map_pow,
    map_X]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP R p
h : Eq (α := R) (1 : R) ((ZMod.castHom ⋯ R : (a : ZMod p) → R) 1 : R)
rw : dickson 1 ((ZMod.castHom ⋯ R : (a : ZMod p) → R) 1) p = HPow.hPow (α := R[X]) X p
⊢ dickson 1 1 p = HPow.hPow (α := R[X]) X p
have rw₁ : map (ZMod.castHom sorry R) (dickson 1 1 p) = HPow.hPow (α := R[X]) X p
Tactic: rw [h, ← map_dickson (ZMod.castHom (dvd_refl p) R), dickson_one_one_zmod_p, Polynomial.map_pow,
    map_X]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP R p
h : Eq (α := R) (1 : R) ((ZMod.castHom ⋯ R : (a : ZMod p) → R) 1 : R)
rw : dickson 1 ((ZMod.castHom ⋯ R : (a : ZMod p) → R) 1) p = HPow.hPow (α := R[X]) X p
rw₁ : map (ZMod.castHom ⋯ R) (dickson 1 1 p) = HPow.hPow (α := R[X]) X p
⊢ dickson 1 1 p = HPow.hPow (α := R[X]) X p
have rw₂ : map (ZMod.castHom sorry R) (HPow.hPow (α := (ZMod p)[X]) X p) = HPow.hPow (α := R[X]) X p
Tactic: rw [h, ← map_dickson (ZMod.castHom (dvd_refl p) R), dickson_one_one_zmod_p, Polynomial.map_pow,
    map_X]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP R p
h : Eq (α := R) (1 : R) ((ZMod.castHom ⋯ R : (a : ZMod p) → R) 1 : R)
rw : dickson 1 ((ZMod.castHom ⋯ R : (a : ZMod p) → R) 1) p = HPow.hPow (α := R[X]) X p
rw₁ : map (ZMod.castHom ⋯ R) (dickson 1 1 p) = HPow.hPow (α := R[X]) X p
rw₂ : map (ZMod.castHom ⋯ R) (HPow.hPow (α := (ZMod p)[X]) X p) = HPow.hPow (α := R[X]) X p
⊢ dickson 1 1 p = HPow.hPow (α := R[X]) X p
have rw₃ : HPow.hPow (α := R[X]) (map (ZMod.castHom sorry R) X) p = HPow.hPow (α := R[X]) X p
Tactic: rw [h, ← map_dickson (ZMod.castHom (dvd_refl p) R), dickson_one_one_zmod_p, Polynomial.map_pow,
    map_X]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP R p
h : Eq (α := R) (1 : R) ((ZMod.castHom ⋯ R : (a : ZMod p) → R) 1 : R)
rw : dickson 1 ((ZMod.castHom ⋯ R : (a : ZMod p) → R) 1) p = HPow.hPow (α := R[X]) X p
rw₁ : map (ZMod.castHom ⋯ R) (dickson 1 1 p) = HPow.hPow (α := R[X]) X p
rw₂ : map (ZMod.castHom ⋯ R) (HPow.hPow (α := (ZMod p)[X]) X p) = HPow.hPow (α := R[X]) X p
rw₃ : HPow.hPow (α := R[X]) (map (ZMod.castHom ⋯ R) X) p = HPow.hPow (α := R[X]) X p
⊢ dickson 1 1 p = HPow.hPow (α := R[X]) X p
have rw₄ : HPow.hPow (α := R[X]) X p = HPow.hPow (α := R[X]) X p
Tactic: rw [h, ← map_dickson (ZMod.castHom (dvd_refl p) R), dickson_one_one_zmod_p, Polynomial.map_pow,
    map_X]
-- 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.IsWeaklyEisensteinAt 𝓟
A : Type v
inst_1 : CommSemiring A
φ : R →+* A
⊢ (Polynomial.map φ f).IsWeaklyEisensteinAt (Ideal.map φ 𝓟)
have refine : ∀ {n : ℕ} (hn : n < (Polynomial.map φ f).natDegree),
  Membership.mem (γ := Ideal A) (Ideal.map φ 𝓟) ((Polynomial.map φ f).coeff n)
Tactic: refine (isWeaklyEisensteinAt_iff _ _).2 fun hn => ?_
-- 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.IsWeaklyEisensteinAt 𝓟
A : Type v
inst_1 : CommSemiring A
φ : R →+* A
n : ℕ
hn : n < (Polynomial.map φ f).natDegree
⊢ Membership.mem (γ := Ideal A) (Ideal.map φ 𝓟) ((Polynomial.map φ f).coeff n)
have rw : Membership.mem.{v, v} (α := A) (γ := Ideal A) (Ideal.map φ 𝓟) ((φ : (a : R) → A) (f.coeff n) : A)
Tactic: rw [coeff_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
hf' : f'.IsWeaklyEisensteinAt 𝓟
⊢ (f * f').IsWeaklyEisensteinAt 𝓟
have rw : ∀ (hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟) (hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟) {n : ℕ},
  n < (f * f').natDegree → (f * f').coeff n ∈ 𝓟
Tactic: rw [isWeaklyEisensteinAt_iff] at hf hf' ⊢
Cleared hypotheses: hf, hf'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
hn : n < (f * f').natDegree
⊢ (f * f').coeff n ∈ 𝓟
have rw : ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, f.coeff x.1 * f'.coeff x.2 ∈ 𝓟
Tactic: rw [coeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
hn : n < (f * f').natDegree
⊢ ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, f.coeff x.1 * f'.coeff x.2 ∈ 𝓟
have refine : ∀ (x : ℕ × ℕ) (hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ n), f.coeff x.1 * f'.coeff x.2 ∈ 𝓟
Tactic: refine sum_mem _ fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
hn : n < (f * f').natDegree
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ n
⊢ f.coeff x.1 * f'.coeff x.2 ∈ 𝓟
have inl : ∀ (hx1 : x.1 < f.natDegree), f.coeff x.1 * f'.coeff x.2 ∈ 𝓟
Tactic: rcases lt_or_ge x.1 f.natDegree with hx1 | hx1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
hn : n < (f * f').natDegree
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ n
inl : ∀ (hx1 : x.1 < f.natDegree), f.coeff x.1 * f'.coeff x.2 ∈ 𝓟
⊢ f.coeff x.1 * f'.coeff x.2 ∈ 𝓟
have inr : ∀ (hx1 : f.natDegree ≤ x.1), f.coeff x.1 * f'.coeff x.2 ∈ 𝓟
Tactic: rcases lt_or_ge x.1 f.natDegree with hx1 | hx1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
hn : n < (f * f').natDegree
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ n
hx1 : f.natDegree ≤ x.1
⊢ x.2 < f'.natDegree
have by_contra! : ∀ (this : f'.natDegree ≤ x.2), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
hn : n < (f * f').natDegree
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ n
hx1 : f.natDegree ≤ x.1
this : f'.natDegree ≤ x.2
⊢ False
have hx₁ : x.1 + x.2 = n
Tactic: rw [HasAntidiagonal.mem_antidiagonal] at hx
Cleared hypotheses: hx, hx1, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
hn : n < (f * f').natDegree
x : ℕ × ℕ
hx : x.1 + x.2 = n
hx1 : f.natDegree ≤ x.1
this : f'.natDegree ≤ x.2
⊢ False
have hn₁ : n < f.natDegree + f'.natDegree
Tactic: replace hn := hn.trans_le natDegree_mul_le
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
x : ℕ × ℕ
hx : x.1 + x.2 = n
hx1 : f.natDegree ≤ x.1
this : f'.natDegree ≤ x.2
hn : n < f.natDegree + f'.natDegree
⊢ False
have linarith : -1 + (HAdd.hAdd (α := ℤ) (↑x.1 : ℤ) (↑x.2 : ℤ) - (↑n : ℤ)) + HSub.hSub (α := ℤ) (↑f.natDegree : ℤ) (↑x.1 : ℤ) +
      HSub.hSub (α := ℤ) (↑f'.natDegree : ℤ) (↑x.2 : ℤ) +
    (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑f.natDegree : ℤ) (↑f'.natDegree : ℤ)) =
  0
Tactic: linarith
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
hn : n < (f * f').natDegree
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ n
hx1 : f.natDegree ≤ x.1
⊢ f.coeff x.1 * f'.coeff x.2 ∈ 𝓟
have hx1₁ : x.2 < f'.natDegree
Tactic: replace hx1 : x.2 < f'.natDegree := by
    by_contra!
    rw [HasAntidiagonal.mem_antidiagonal] at hx
    replace hn := hn.trans_le natDegree_mul_le
    linarith
Cleared hypotheses: hx1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (hypothesis)
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)
⊢ ∃ (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)
have hx₁ : x ^ natDegree (Polynomial.map (algebraMap R S) f) +
    ∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
      coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ) =
  0
Tactic: rw [aeval_def, Polynomial.eval₂_eq_eval_map, eval_eq_sum_range, range_add_one,
    sum_insert notMem_range_self, sum_range, (hmo.map (algebraMap R S)).coeff_natDegree,
    one_mul] at hx
Cleared hypotheses: hx, hmo, hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (hypothesis)
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 :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) +
      ∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
        coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ) =
    0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
⊢ ∃ (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)
have hx₁ : x ^ natDegree (Polynomial.map (algebraMap R S) f) =
  -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
      coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
Tactic: replace hx := eq_neg_of_add_eq_zero_left hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (hypothesis)
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
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
        coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
⊢ ∃ (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)
have this : ∀ n < f.natDegree, p ∣ f.coeff n
Tactic: have : ∀ n < f.natDegree, p ∣ f.coeff n := by
    intro n hn
    exact mem_span_singleton.1 (by simpa using hf.mem hn)
-- 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
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
        coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
this : ∀ n < f.natDegree, p ∣ f.coeff n
⊢ ∃ (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)
have choose! : ∀ (φ : (n : ℕ) → R) (hφ : ∀ n < f.natDegree, f.coeff n = p * φ n),
  ∃ (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)
Tactic: choose! φ hφ using this
Cleared hypotheses: this
-- 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
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
        coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
φ : (n : ℕ) → R
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
| -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
      coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
have a : ∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
  coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
Tactic: congr
-- 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
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
        coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
φ : (n : ℕ) → R
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
| ∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
    coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
have a : univ
Tactic: congr
-- 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
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
        coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
φ : (n : ℕ) → R
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
a : univ
| ∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
    coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
have a₁ : fun (i : Fin (natDegree (Polynomial.map (algebraMap R S) f))) ↦
  coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
Tactic: congr
-- 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
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
        coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
φ : (n : ℕ) → R
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
| fun (i : Fin (natDegree (Polynomial.map (algebraMap R S) f))) ↦
    coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
have a : ∀ (i : Fin (natDegree (Polynomial.map (algebraMap R S) f))),
  coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
Tactic: ext i
-- 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
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
        coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
φ : (n : ℕ) → R
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
i : Fin (natDegree (Polynomial.map (algebraMap R S) f))
| coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
have a : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S)
  (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (φ (↑i : ℕ)) : S) (x ^ (↑i : ℕ)))
Tactic: rw [coeff_map, hφ i.1 (lt_of_lt_of_le i.2 natDegree_map_le), map_mul, mul_assoc]
-- 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
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
        coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
φ : (n : ℕ) → R
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
| -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
      coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
have a : ∀ (i : Fin (natDegree (Polynomial.map (algebraMap R S) f))),
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S)
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (φ (↑i : ℕ)) : S) (x ^ (↑i : ℕ)))
Tactic: congr
    congr
    · skip
    ext i
    rw [coeff_map, hφ i.1 (lt_of_lt_of_le i.2 natDegree_map_le), map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Basic (hypothesis)
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
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
        coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
φ : (n : ℕ) → R
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ (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)
have hx₁ : x ^ natDegree (Polynomial.map (algebraMap R S) f) =
  -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S)
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (φ (↑i : ℕ)) : S) (x ^ (↑i : ℕ)))
Tactic: conv_rhs at hx =>
    congr
    congr
    · skip
    ext i
    rw [coeff_map, hφ i.1 (lt_of_lt_of_le i.2 natDegree_map_le), map_mul, mul_assoc]
Cleared hypotheses: hx, 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
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
φ : (n : ℕ) → R
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
        HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S)
          (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (φ (↑i : ℕ)) : S) (x ^ (↑i : ℕ)))
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ (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)
have rw : ∃ (y : S),
  Membership.mem (γ := Subalgebra R S) R[x] y ∧
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) y =
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S)
        (HMul.hMul (α := S) (-1)
          (∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
            HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (φ (↑i : ℕ)) : S) (x ^ (↑i : ℕ))))
Tactic: rw [hx, ← mul_sum, neg_eq_neg_one_mul, ← mul_assoc (-1 : S), mul_comm (-1 : S), mul_assoc]
-- 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
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
φ : (n : ℕ) → R
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
        HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S)
          (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (φ (↑i : ℕ)) : S) (x ^ (↑i : ℕ)))
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ (y : S),
    Membership.mem (γ := Subalgebra R S) R[x] y ∧
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) y =
        HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S)
          (HMul.hMul (α := S) (-1)
            (∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
              HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (φ (↑i : ℕ)) : S) (x ^ (↑i : ℕ))))
have i : Membership.mem (γ := Subalgebra R S) R[x]
  (HMul.hMul (α := S) (-1)
    (∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (φ (↑i : ℕ)) : S) (x ^ (↑i : ℕ))))
Tactic: refine
    ⟨-1 * ∑ i : Fin (f.map (algebraMap R S)).natDegree, (algebraMap R S) (φ i.1) * x ^ i.1, ?_, rfl⟩