awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Dickson
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
rw₄ rw₅ : HPow.hPow (α := R[X]) X p = HPow.hPow (α := R[X]) X p
⊢ 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]

Premises used: Polynomial.map_dickson, Polynomial.map_pow, Polynomial.map_X, Polynomial.dickson_one_one_zmod_p, dvd_refl, ZMod.castHom
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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 φ 𝓟)

Tactic:
(isWeaklyEisensteinAt_iff _ _).2 fun hn => ?_

Premises used: Iff.mpr, Polynomial.isWeaklyEisensteinAt_iff
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
A : Type v
inst_1 : CommSemiring A
φ : R →+* A
refine :
  ∀ {n : ℕ} (hn : n < (Polynomial.map φ f).natDegree),
    Membership.mem (γ := Ideal A) (Ideal.map φ 𝓟) ((Polynomial.map φ f).coeff n)
⊢ (Polynomial.map φ f).IsWeaklyEisensteinAt (Ideal.map φ 𝓟)

Tactic:
refine (isWeaklyEisensteinAt_iff _ _).2 fun hn => ?_

Premises used: Iff.mpr, Polynomial.isWeaklyEisensteinAt_iff
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
rw : Membership.mem.{v, v} (α := A) (γ := Ideal A) (Ideal.map φ 𝓟) ((φ : (a : R) → A) (f.coeff n) : A)
⊢ Membership.mem (γ := Ideal A) (Ideal.map φ 𝓟) ((Polynomial.map φ f).coeff n)

Tactic:
rw [coeff_map]

Premises used: Polynomial.coeff_map
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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.{v, v} (α := A) (γ := Ideal A) (Ideal.map φ 𝓟) ((φ : (a : R) → A) (f.coeff n) : A)

Tactic:
mem_map_of_mem _ (hf.mem (lt_of_lt_of_le hn natDegree_map_le))

Premises used: Ideal.mem_map_of_mem, Set.Mem, Polynomial.natDegree_map_le, Polynomial.IsWeaklyEisensteinAt.mem, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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.{v, v} (α := A) (γ := Ideal A) (Ideal.map φ 𝓟) ((φ : (a : R) → A) (f.coeff n) : A)

Tactic:
exact mem_map_of_mem _ (hf.mem (lt_of_lt_of_le hn natDegree_map_le))
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
hf' : f'.IsWeaklyEisensteinAt 𝓟
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 ∈ 𝓟
⊢ (f * f').IsWeaklyEisensteinAt 𝓟

Tactic:
rw [isWeaklyEisensteinAt_iff] at hf hf' ⊢

Premises used: Polynomial.isWeaklyEisensteinAt_iff
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
rw : ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, f.coeff x.1 * f'.coeff x.2 ∈ 𝓟
⊢ (f * f').coeff n ∈ 𝓟

Tactic:
rw [coeff_mul]

Premises used: Polynomial.coeff_mul
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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 ∈ 𝓟

Tactic:
sum_mem _ fun x hx ↦ ?_

Premises used: Ideal.sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
refine : ∀ (x : ℕ × ℕ) (hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ n), f.coeff x.1 * f'.coeff x.2 ∈ 𝓟
⊢ ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, f.coeff x.1 * f'.coeff x.2 ∈ 𝓟

Tactic:
refine sum_mem _ fun x hx ↦ ?_

Premises used: Ideal.sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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 ∈ 𝓟
inr : ∀ (hx1 : f.natDegree ≤ x.1), f.coeff x.1 * f'.coeff x.2 ∈ 𝓟
⊢ f.coeff x.1 * f'.coeff x.2 ∈ 𝓟

Tactic:
rcases lt_or_ge x.1 f.natDegree with hx1 | hx1

Premises used: Prod.fst, lt_or_ge, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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 : x.1 < f.natDegree
⊢ f.coeff x.1 * f'.coeff x.2 ∈ 𝓟

Tactic:
mul_mem_right _ _ (hf hx1)

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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 : x.1 < f.natDegree
⊢ f.coeff x.1 * f'.coeff x.2 ∈ 𝓟

Tactic:
exact mul_mem_right _ _ (hf hx1)

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
by_contra! : ∀ (this : f'.natDegree ≤ x.2), False
⊢ x.2 < f'.natDegree

Tactic:
by_contra!
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
⊢ x.1 + x.2 = n

Tactic:
rw [HasAntidiagonal.mem_antidiagonal] at hx

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
hx₁ : x.1 + x.2 = n
⊢ f.natDegree ≤ x.1

Tactic:
rw [HasAntidiagonal.mem_antidiagonal] at hx

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
hx₁ : x.1 + x.2 = n
hx1₁ : f.natDegree ≤ x.1
⊢ f'.natDegree ≤ x.2

Tactic:
rw [HasAntidiagonal.mem_antidiagonal] at hx

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
⊢ n < f.natDegree + f'.natDegree

Tactic:
replace hn := hn.trans_le natDegree_mul_le
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
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
⊢ False

Tactic:
linarith
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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

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
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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 : x.2 < f'.natDegree
⊢ f.coeff x.1 * f'.coeff x.2 ∈ 𝓟

Tactic:
mul_mem_left _ _ (hf' hx1)

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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 : x.2 < f'.natDegree
⊢ f.coeff x.1 * f'.coeff x.2 ∈ 𝓟

Tactic:
exact mul_mem_left _ _ (hf' hx1)

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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)
⊢ 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

Premises used: Algebra.algebraMap, Finset.range_add_one, Polynomial.aeval_def, Finset.sum_range, Finset.notMem_range_self, Polynomial.Monic.coeff_natDegree, Polynomial.eval_eq_sum_range, Finset.sum_insert, Polynomial.Monic.map, Polynomial.eval₂_eq_eval_map, one_mul
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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)
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
⊢ f.Monic

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

Premises used: Algebra.algebraMap, Finset.range_add_one, Polynomial.aeval_def, Finset.sum_range, Finset.notMem_range_self, Polynomial.Monic.coeff_natDegree, Polynomial.eval_eq_sum_range, Finset.sum_insert, Polynomial.Monic.map, Polynomial.eval₂_eq_eval_map, one_mul
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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)
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
⊢ f.IsWeaklyEisensteinAt (R ∙ p)

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

Premises used: Algebra.algebraMap, Finset.range_add_one, Polynomial.aeval_def, Finset.sum_range, Finset.notMem_range_self, Polynomial.Monic.coeff_natDegree, Polynomial.eval_eq_sum_range, Finset.sum_insert, Polynomial.Monic.map, Polynomial.eval₂_eq_eval_map, one_mul
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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)
⊢ 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
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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 : ℕ
hn : n < f.natDegree
⊢ Membership.mem (γ := Ideal R) (span {p}) (f.coeff n)

Tactic:
simpa using hf.mem hn

Premises used: Polynomial.IsWeaklyEisensteinAt.mem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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 : ℕ
hn : n < f.natDegree
⊢ p ∣ f.coeff n

Tactic:
exact mem_span_singleton.1 (by simpa using hf.mem hn)

Premises used: Iff.mp, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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 < 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)
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
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)
⊢ ∃ (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
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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 :
  ∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
    coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
| -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
      coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)

Tactic:
congr
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
a₁ :
  fun (i : Fin (natDegree (Polynomial.map (algebraMap R S) f))) ↦
    coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
| ∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
    coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)

Tactic:
congr
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
| univ

Tactic:
· skip
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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 :
  ∀ (i : Fin (natDegree (Polynomial.map (algebraMap R S) f))),
    coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)
| fun (i : Fin (natDegree (Polynomial.map (algebraMap R S) f))) ↦
    coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)

Tactic:
ext i
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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))
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 : ℕ)))
| coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * x ^ (↑i : ℕ)

Tactic:
rw [coeff_map, hφ i.1 (lt_of_lt_of_le i.2 natDegree_map_le), map_mul, mul_assoc]

Premises used: Polynomial.coeff_map, mul_assoc, Fin.isLt, Fin.val, map_mul, Polynomial.natDegree_map_le, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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 :
  ∀ (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 : ℕ)))
| -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree,
      coeff (Polynomial.map (algebraMap R S) f) (↑i : ℕ) * 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]

Premises used: Polynomial.coeff_map, mul_assoc, map_mul
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
⊢ 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]

Premises used: Polynomial.coeff_map, mul_assoc, map_mul
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
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 : ℕ)))
⊢ ∀ n < f.natDegree, f.coeff n = p * φ n

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]

Premises used: Polynomial.coeff_map, mul_assoc, map_mul