awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < natDegree (cyclotomic (p ^ (n + 1)) ℤ) * (HAdd.hAdd (α := ℤ[X]) X 1).natDegree →
      Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
        ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff n_1)
i : ℕ
hi : i < natDegree (cyclotomic (p ^ (n + 1 + 1)) ℤ) * (HAdd.hAdd (α := ℤ[X]) X 1).natDegree
k : ℕ
hk : i = p * k
⊢ HAdd.hAdd (α := ℤ[X]) X 1 = HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < natDegree (cyclotomic (p ^ (n + 1)) ℤ) * (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1)).natDegree →
      Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
        ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))).coeff n_1)
i : ℕ
hi : i < natDegree (cyclotomic (p ^ (n + 1 + 1)) ℤ) * (HAdd.hAdd (α := ℤ[X]) X 1).natDegree
k : ℕ
hk : i = p * k
⊢ HAdd.hAdd (α := ℤ[X]) X 1 = HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree →
      Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
        ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff n_1)
i : ℕ
hi : i < (comp (cyclotomic (p ^ (n + 1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
k : ℕ
hk : i = p * k
refine_2 :
  ∀
    (hn :
      ∀ {n_1 : ℕ},
        n_1 < p ^ n * (p - 1) →
          Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
            ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))).coeff n_1))
    {i : ℕ} (hi : i < p ^ (n + 1) * (p - 1)) (k : ℕ) (hk : i = p * k),
    (comp (cyclotomic (p ^ (n + 1)) (ZMod p)) (HAdd.hAdd (α := (ZMod p)[X]) X 1)).coeff (i / p) = 0
⊢ (comp (cyclotomic (p ^ (n + 1)) (ZMod p)) (HAdd.hAdd (α := (ZMod p)[X]) X 1)).coeff (i / p) = 0

Tactic:
rw [natDegree_comp, show (X + 1 : ℤ[X]) = X + C 1 by simp, natDegree_X_add_C, mul_one,
          natDegree_cyclotomic, Nat.totient_prime_pow hp.out (Nat.succ_pos _), Nat.add_one_sub_one]
          at hn hi

Premises used: Nat.add_one_sub_one, Polynomial.natDegree_cyclotomic, Nat.totient_prime_pow, Polynomial.natDegree_comp, Polynomial.natDegree_X_add_C, Nat.succ_pos, mul_one, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < p ^ n * (p - 1) →
      Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
        ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))).coeff n_1)
i : ℕ
hi : i < p ^ (n + 1) * (p - 1)
k : ℕ
hk : i = p * k
⊢ p * k < p * (p ^ n * (p - 1))

Tactic:
rw [hk, pow_succ', mul_assoc] at hi

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < p ^ n * (p - 1) →
      Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
        ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))).coeff n_1)
i : ℕ
hi : i < p ^ (n + 1) * (p - 1)
k : ℕ
hk : i = p * k
hi₁ : p * k < p * (p ^ n * (p - 1))
⊢ i = p * k

Tactic:
rw [hk, pow_succ', mul_assoc] at hi

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < p ^ n * (p - 1) →
      Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
        ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))).coeff n_1)
i k : ℕ
hi : p * k < p * (p ^ n * (p - 1))
hk : i = p * k
refine_2 : (comp (cyclotomic (p ^ (n + 1)) (ZMod p)) (HAdd.hAdd (α := (ZMod p)[X]) X 1)).coeff k = 0
⊢ (comp (cyclotomic (p ^ (n + 1)) (ZMod p)) (HAdd.hAdd (α := (ZMod p)[X]) X 1)).coeff (i / p) = 0

Tactic:
rw [hk, mul_comm, Nat.mul_div_cancel _ hp.out.pos]

Premises used: Nat.mul_div_cancel, Nat.Prime.pos, mul_comm, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < p ^ n * (p - 1) →
      Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
        ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))).coeff n_1)
i k : ℕ
hi : p * k < p * (p ^ n * (p - 1))
hk : i = p * k
⊢ Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
    ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))).coeff k)

Tactic:
replace hn := hn (lt_of_mul_lt_mul_left' hi)
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i k : ℕ
hi : p * k < p * (p ^ n * (p - 1))
hk : i = p * k
hn :
  Eq (α := ZMod p)
    (↑((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))).coeff k) : ZMod p) 0
⊢ Eq (α := ZMod p)
    ((↑((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))).coeff k) : ZMod p) :
      ZMod p)
    ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p)
        ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))).coeff k) :
      ZMod p)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i k : ℕ
hi : p * k < p * (p ^ n * (p - 1))
hk : i = p * k
hn :
  Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
    ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))).coeff k)
⊢ Eq (α := ZMod p)
    (coeff
      (Polynomial.map (Int.castRingHom (ZMod p))
        (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))))
      k)
    0

Tactic:
rw [Ideal.submodule_span_eq, Ideal.mem_span_singleton, ← ZMod.intCast_zmod_eq_zero_iff_dvd,
           show ↑(_ : ℤ) = Int.castRingHom (ZMod p) _ by rfl, ← coeff_map] at hn

Premises used: Polynomial.coeff_map, Ideal.submodule_span_eq, ZMod.intCast_zmod_eq_zero_iff_dvd, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i k : ℕ
hi : p * k < p * (p ^ n * (p - 1))
hk : i = p * k
hn :
  Eq (α := ZMod p)
    (coeff
      (Polynomial.map (Int.castRingHom (ZMod p))
        (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))))
      k)
    0
⊢ (comp (cyclotomic (p ^ (n + 1)) (ZMod p)) (HAdd.hAdd (α := (ZMod p)[X]) X 1)).coeff k = 0

Tactic:
simpa [map_comp] using hn

Premises used: Polynomial.map_comp
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree →
      Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
        ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff n_1)
i : ℕ
hi : i < (comp (cyclotomic (p ^ (n + 1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
rw rw₁ : p * p ^ n = p * p ^ n
⊢ p ^ (n + 1) = p * p ^ n

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree →
      Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
        ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff n_1)
i : ℕ
hi : i < (comp (cyclotomic (p ^ (n + 1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
⊢ p ∣ p ^ (n + 1)

Tactic:
exact ⟨p ^ n, by rw [pow_succ']⟩
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine_2 :
  ∀ {n : ℕ},
    n < (comp (cyclotomic (p ^ HAdd.hAdd (α := ℕ) 0 1) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree →
      Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
        ((comp (cyclotomic (p ^ HAdd.hAdd (α := ℕ) 0 1) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff n)
refine_2₁ :
  ∀ (n : ℕ)
    (hn :
      ∀ {n_1 : ℕ},
        n_1 < (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree →
          Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
            ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff n_1))
    {n_1 : ℕ},
    n_1 < (comp (cyclotomic (p ^ (n + 1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree →
      Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
        ((comp (cyclotomic (p ^ (n + 1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff n_1)
⊢ ∀ {n_1 : ℕ},
    n_1 < (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree →
      Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
        ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff n_1)

Tactic:
induction n with
    | zero =>
      intro i hi
      rw [Nat.zero_add, pow_one] at hi ⊢
      exact (cyclotomic_comp_X_add_one_isEisensteinAt p).mem hi
    | succ n hn =>
      intro i hi
      rw [Ideal.submodule_span_eq, Ideal.mem_span_singleton, ← ZMod.intCast_zmod_eq_zero_iff_dvd,
        show ↑(_ : ℤ) = Int.castRingHom (ZMod p) _ by rfl, ← coeff_map, map_comp, map_cyclotomic,
        Polynomial.map_add, map_X, Polynomial.map_one, pow_add, pow_one,
        cyclotomic_mul_prime_dvd_eq_pow, pow_comp, ← ZMod.expand_card, coeff_expand hp.out.pos]
      · simp only [ite_eq_right_iff]
        rintro ⟨k, hk⟩
        rw [natDegree_comp, show (X + 1 : ℤ[X]) = X + C 1 by simp, natDegree_X_add_C, mul_one,
          natDegree_cyclotomic, Nat.totient_prime_pow hp.out (Nat.succ_pos _), Nat.add_one_sub_one]
          at hn hi
        rw [hk, pow_succ', mul_assoc] at hi
        rw [hk, mul_comm, Nat.mul_div_cancel _ hp.out.pos]
        replace hn := hn (lt_of_mul_lt_mul_left' hi)
        rw [Ideal.submodule_span_eq, Ideal.mem_span_singleton, ← ZMod.intCast_zmod_eq_zero_iff_dvd,
           show ↑(_ : ℤ) = Int.castRingHom (ZMod p) _ by rfl, ← coeff_map] at hn
        simpa [map_comp] using hn
      · exact ⟨p ^ n, by rw [pow_succ']⟩

Premises used: Polynomial.map_one, Nat.add_one_sub_one, Polynomial.coeff_map, Ideal.submodule_span_eq, Polynomial.pow_comp, Nat.mul_div_cancel, Polynomial.natDegree_cyclotomic, Nat.totient_prime_pow, Polynomial.natDegree_comp, mul_assoc, pow_add, Polynomial.natDegree_X_add_C, Polynomial.cyclotomic_mul_prime_dvd_eq_pow, Polynomial.map_add, Polynomial.map_X, Nat.Prime.pos, ZMod.intCast_zmod_eq_zero_iff_dvd, ite_eq_right_iff, pow_one, Polynomial.coeff_expand, Nat.succ_pos, mul_comm, ZMod.expand_card, Polynomial.map_cyclotomic, mul_one, Nat.zero_add, Polynomial.map_comp, Ideal.mem_span_singleton, pow_succ', Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine_3 :
  ∑ i ∈ range p, eval 1 (HPow.hPow (α := ℤ[X]) X (p ^ n) ^ i) ∉ HPow.hPow (α := Ideal ℤ) (β := ℕ) (ℤ ∙ (↑p : ℤ)) 2
⊢ (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff 0 ∉
    HPow.hPow (α := Ideal ℤ) (β := ℕ) (ℤ ∙ (↑p : ℤ)) 2

Tactic:
rw [coeff_zero_eq_eval_zero, eval_comp, cyclotomic_prime_pow_eq_geom_sum hp.out, eval_add,
      eval_X, eval_one, zero_add, eval_finsetSum]

Premises used: Polynomial.coeff_zero_eq_eval_zero, Polynomial.eval_X, Polynomial.cyclotomic_prime_pow_eq_geom_sum, zero_add, Polynomial.eval_finsetSum, Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_one, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine_3 : ¬HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
⊢ ∑ i ∈ range p, eval 1 (HPow.hPow (α := ℤ[X]) X (p ^ n) ^ i) ∉ HPow.hPow (α := Ideal ℤ) (β := ℕ) (ℤ ∙ (↑p : ℤ)) 2

Tactic:
simp only [eval_pow, eval_X, one_pow, sum_const, card_range, Nat.smul_one_eq_cast,
      submodule_span_eq, Ideal.submodule_span_eq, Ideal.span_singleton_pow,
      Ideal.mem_span_singleton]

Premises used: one_pow, Ideal.submodule_span_eq, Polynomial.eval_X, Polynomial.eval_pow, Finset.card_range, Nat.smul_one_eq_cast, Ideal.mem_span_singleton, Ideal.span_singleton_pow, Finset.sum_const
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
refine_3 : ∀ (k : ℕ) (hk : p = HPow.hPow (β := ℕ) p 2 * k), False
⊢ False

Tactic:
obtain ⟨k, hk⟩ := Int.natCast_dvd_natCast.1 h

Premises used: Iff.mp, Int.natCast_dvd_natCast
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
k : ℕ
hk : p = HPow.hPow (β := ℕ) p 2 * k
⊢ 2 ≤ p

Tactic:
have : 2 ≤ p := Nat.Prime.two_le hp.out
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
k : ℕ
hk : p = HPow.hPow (β := ℕ) p 2 * k
this : 2 ≤ p
⊢ p < HPow.hPow (β := ℕ) p 2

Tactic:
have : p < p ^ 2 := by nlinarith
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
k : ℕ
hk : p = HPow.hPow (β := ℕ) p 2 * k
this_1 : 2 ≤ p
this : p < HPow.hPow (β := ℕ) p 2
refine_3 : ∀ (hk : p = HPow.hPow (β := ℕ) p 2 * 0), False
refine_3₁ : ∀ (n : ℕ) (hk : p = HPow.hPow (β := ℕ) p 2 * (n + 1)), False
⊢ False

Tactic:
cases k
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
this_1 : 2 ≤ p
this : p < HPow.hPow (β := ℕ) p 2
hk : p = HPow.hPow (β := ℕ) p 2 * 0
⊢ False

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
this_1 : 2 ≤ p
this : p < HPow.hPow (β := ℕ) p 2
n_1 : ℕ
hk : p = HPow.hPow (β := ℕ) p 2 * (n_1 + 1)
⊢ False

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
obtain : ∀ (n : ℕ) (hn : B.dim = n.succ), p ∣ Q.coeff 0
⊢ p ∣ Q.coeff 0

Tactic:
obtain ⟨n, hn⟩ := Nat.exists_eq_succ_of_ne_zero B.dim_pos.ne'

Premises used: LT.lt.ne', PowerBasis.dim_pos, Nat.exists_eq_succ_of_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
⊢ Module.finrank K L = B.dim

Tactic:
have finrank_K_L : Module.finrank K L = B.dim := B.finrank
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
⊢ natDegree (minpoly K B.gen) = B.dim

Tactic:
have deg_K_P : (minpoly K B.gen).natDegree = B.dim := B.natDegree_minpoly
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
rw : P.natDegree = natDegree (minpoly K B.gen)
rw₁ : P.natDegree = natDegree (Polynomial.map (algebraMap R K) (minpoly R B.gen))
rw₂ rw₃ : P.natDegree = natDegree (minpoly R B.gen)
⊢ P.natDegree = B.dim

Tactic:
rw [← deg_K_P, minpoly.isIntegrallyClosed_eq_field_fractions' K hBint,
      (minpoly.monic hBint).natDegree_map (algebraMap R K)]

Premises used: minpoly.monic, Algebra.algebraMap, Polynomial.Monic.natDegree_map, minpoly.isIntegrallyClosed_eq_field_fractions'
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
⊢ P.natDegree = B.dim

Tactic:
have deg_R_P : P.natDegree = B.dim := by
    rw [← deg_K_P, minpoly.isIntegrallyClosed_eq_field_fractions' K hBint,
      (minpoly.monic hBint).natDegree_map (algebraMap R K)]
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
choose! :
  ∀ (f : (i : ℕ) → L)
    (hf :
      ∀ (i : ℕ),
        natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ i →
          Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
            HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i),
    p ∣ Q.coeff 0
⊢ p ∣ Q.coeff 0

Tactic:
choose! f hf using
    hei.isWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le (minpoly.aeval R B.gen)
      (minpoly.monic hBint)

Premises used: minpoly.monic, PowerBasis.gen, minpoly.aeval, Polynomial.IsEisensteinAt.isWeaklyEisensteinAt, Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
⊢ ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i

Tactic:
simp only [P, (minpoly.monic hBint).natDegree_map, deg_R_P] at hf

Premises used: minpoly.monic, Polynomial.Monic.natDegree_map
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this_1 : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
this : p ^ n.succ ∣ Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n)
⊢ ¬HPow.hPow (β := ℕ) p 2 ∣ coeff (minpoly R B.gen) 0

Tactic:
have hndiv : ¬p ^ 2 ∣ (minpoly R B.gen).coeff 0 := fun h =>
      hei.notMem ((span_singleton_pow p 2).symm ▸ Ideal.mem_span_singleton.2 h)
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this_1 : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
this : p ^ n.succ ∣ Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ coeff (minpoly R B.gen) 0
⊢ p ∣ Q.coeff 0

Tactic:
hp.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd (n := n) (?_ : _ ∣ _) hndiv

Premises used: Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd