awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
φ : (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
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 : ℕ))))
⊢ ∃ (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:
rw [hx, ← mul_sum, neg_eq_neg_one_mul, ← mul_assoc (-1 : S), mul_comm (-1 : S), mul_assoc]

Premises used: Finset.mul_sum, mul_assoc, neg_eq_neg_one_mul, mul_comm, OfNat.ofNat, Neg.neg
-- 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)
φ : (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 : ℕ))))

Tactic:
⟨-1 * ∑ i : Fin (f.map (algebraMap R S)).natDegree, (algebraMap R S) (φ i.1) * x ^ i.1, ?_, rfl⟩

Premises used: HMul.hMul, Finset.univ, Algebra.algebraMap, Fin.val, HPow.hPow, And.intro, Exists.intro, OfNat.ofNat, DFunLike.coe, Finset.sum, Neg.neg, rfl
-- 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)
φ : (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
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 : ℕ))))
⊢ ∃ (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:
refine
    ⟨-1 * ∑ i : Fin (f.map (algebraMap R S)).natDegree, (algebraMap R S) (φ i.1) * x ^ i.1, ?_, rfl⟩
-- 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)
φ : (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
⊢ 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:
Subalgebra.mul_mem _ (Subalgebra.neg_mem _ (Subalgebra.one_mem _))
      (Subalgebra.sum_mem _ fun i _ =>
        Subalgebra.mul_mem _ (Subalgebra.algebraMap_mem _ _)
          (Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton x)) _))

Premises used: Subalgebra.mul_mem, Set.mem_singleton, Algebra.subset_adjoin, Algebra.adjoin, Subalgebra.sum_mem, Subalgebra.neg_mem, Fin.val, Subalgebra.pow_mem, Subalgebra.algebraMap_mem, Singleton.singleton, Subalgebra.one_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)
φ : (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
⊢ 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:
exact
    Subalgebra.mul_mem _ (Subalgebra.neg_mem _ (Subalgebra.one_mem _))
      (Subalgebra.sum_mem _ fun i _ =>
        Subalgebra.mul_mem _ (Subalgebra.algebraMap_mem _ _)
          (Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton x)) _))

Premises used: Subalgebra.mul_mem, Set.mem_singleton, Algebra.subset_adjoin, Algebra.adjoin, Subalgebra.sum_mem, Subalgebra.neg_mem, Subalgebra.pow_mem, Subalgebra.algebraMap_mem, Singleton.singleton, Subalgebra.one_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
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
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
⊢ ∃ (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

Premises used: ExistsAddOfLE.exists_add_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
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
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
⊢ ∃ (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:
rw [hk, pow_add]

Premises used: pow_add
-- 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)
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
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
⊢ ∃ (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

Premises used: Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree
-- 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)
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

Tactic:
⟨y * x ^ k, ?_, ?_⟩

Premises used: HMul.hMul, HPow.hPow, And.intro, Exists.intro
-- 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)
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)
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
⊢ ∃ (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:
refine ⟨y * x ^ k, ?_, ?_⟩
-- 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)
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)
⊢ Membership.mem (γ := Subalgebra R S) R[x] (y * x ^ k)

Tactic:
Subalgebra.mul_mem _ hy (Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton x)) _)

Premises used: Subalgebra.mul_mem, Set.mem_singleton, Algebra.subset_adjoin, Subalgebra.pow_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
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)
⊢ Membership.mem (γ := Subalgebra R S) R[x] (y * x ^ k)

Tactic:
exact Subalgebra.mul_mem _ hy (Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton x)) _)

Premises used: Subalgebra.mul_mem, Set.mem_singleton, Algebra.subset_adjoin, Subalgebra.pow_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
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
refine_2₁ refine_2₂ :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) * 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

Tactic:
rw [← mul_assoc _ y, H]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
obtain : ∀ (k : ℕ) (hk : i = f.natDegree + k), x ^ i ∈ 𝓟
⊢ x ^ i ∈ 𝓟

Tactic:
obtain ⟨k, hk⟩ := exists_add_of_le hi

Premises used: ExistsAddOfLE.exists_add_of_le
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
rw : x ^ f.natDegree * x ^ k ∈ 𝓟
⊢ x ^ i ∈ 𝓟

Tactic:
rw [hk, pow_add]

Premises used: pow_add
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
this : x ^ f.natDegree ∈ 𝓟
⊢ x ^ f.natDegree * x ^ k ∈ 𝓟

Tactic:
mul_mem_right (x ^ k) 𝓟 this

Premises used: Set.Mem, HPow.hPow, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
this : x ^ f.natDegree ∈ 𝓟
⊢ x ^ f.natDegree * x ^ k ∈ 𝓟

Tactic:
exact mul_mem_right (x ^ k) 𝓟 this

Premises used: HPow.hPow, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
suffices : x ^ f.natDegree ∈ 𝓟
⊢ x ^ f.natDegree * x ^ k ∈ 𝓟

Tactic:
suffices x ^ f.natDegree ∈ 𝓟 by exact mul_mem_right (x ^ k) 𝓟 this
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
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 ∈ 𝓟
⊢ 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
    *

Premises used: Polynomial.IsRoot.def, Finset.range_add_one, Finset.sum_range, Finset.notMem_range_self, Polynomial.Monic.coeff_natDegree, Polynomial.eval_eq_sum_range, Finset.sum_insert, one_mul
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
rw : ∑ i : Fin f.natDegree, f.coeff (↑i : ℕ) * x ^ (↑i : ℕ) ∈ 𝓟
⊢ x ^ f.natDegree ∈ 𝓟

Tactic:
rw [eq_neg_of_add_eq_zero_left hroot, neg_mem_iff]

Premises used: neg_mem_iff, eq_neg_of_add_eq_zero_left
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
⊢ ∑ i : Fin f.natDegree, f.coeff (↑i : ℕ) * x ^ (↑i : ℕ) ∈ 𝓟

Tactic:
Submodule.sum_mem _ fun i _ => mul_mem_right _ _ (hf.mem (Fin.is_lt i))

Premises used: Set.Mem, Submodule.sum_mem, Fin.is_lt, Fin.val, HPow.hPow, Ideal.mul_mem_right, Polynomial.IsWeaklyEisensteinAt.mem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
⊢ ∑ i : Fin f.natDegree, f.coeff (↑i : ℕ) * x ^ (↑i : ℕ) ∈ 𝓟

Tactic:
exact Submodule.sum_mem _ fun i _ => mul_mem_right _ _ (hf.mem (Fin.is_lt i))

Premises used: Submodule.sum_mem, Fin.is_lt, Ideal.mul_mem_right, Polynomial.IsWeaklyEisensteinAt.mem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
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)
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 𝓟) (x ^ i)

Tactic:
obtain ⟨k, hk⟩ := exists_add_of_le hi

Premises used: ExistsAddOfLE.exists_add_of_le
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
rw :
  Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 𝓟)
    (x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k)
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 𝓟) (x ^ i)

Tactic:
rw [hk, pow_add]

Premises used: pow_add
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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 ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k)

Tactic:
mul_mem_right _ _ this

Premises used: Set.Mem, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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 ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k)

Tactic:
exact mul_mem_right _ _ this

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
suffices :
  Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 𝓟)
    (x ^ natDegree (Polynomial.map (algebraMap R S) f))
⊢ ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R S) f) ≤ i →
      Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 𝓟) (x ^ i)

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
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
⊢ IsRoot (Polynomial.map (algebraMap R S) f) x

Tactic:
rw [aeval_def, eval₂_eq_eval_map, ← IsRoot.def] at hx

Premises used: Polynomial.IsRoot.def, Polynomial.aeval_def, Polynomial.eval₂_eq_eval_map
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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
hx₁ : IsRoot (Polynomial.map (algebraMap R S) f) x
⊢ f.Monic

Tactic:
rw [aeval_def, eval₂_eq_eval_map, ← IsRoot.def] at hx

Premises used: Polynomial.IsRoot.def, Polynomial.aeval_def, Polynomial.eval₂_eq_eval_map
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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 : IsRoot (Polynomial.map (algebraMap R S) f) x
hmo : f.Monic
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 𝓟)
    (x ^ natDegree (Polynomial.map (algebraMap R S) f))

Tactic:
pow_natDegree_le_of_root_of_monic_mem (hf.map _) hx (hmo.map _) _ rfl.le

Premises used: Eq.le, Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_root_of_monic_mem, Polynomial.IsWeaklyEisensteinAt.map, Polynomial.Monic.map, rfl
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
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 : IsRoot (Polynomial.map (algebraMap R S) f) x
hmo : f.Monic
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 𝓟)
    (x ^ natDegree (Polynomial.map (algebraMap R S) f))

Tactic:
exact pow_natDegree_le_of_root_of_monic_mem (hf.map _) hx (hmo.map _) _ rfl.le

Premises used: Eq.le, Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_root_of_monic_mem, Polynomial.IsWeaklyEisensteinAt.map, Polynomial.Monic.map, rfl