awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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
refine_2 :
  (if p ∣ i then (comp (cyclotomic (p ^ (n + 1)) (ZMod p)) (HAdd.hAdd (α := (ZMod p)[X]) X 1)).coeff (i / p) else 0) = 0
⊢ Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
    ((comp (cyclotomic (p ^ (n + 1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff i)
have refine_2₁ : p ∣ p ^ (n + 1)
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, 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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
⊢ (if p ∣ i then (comp (cyclotomic (p ^ (n + 1)) (ZMod p)) (HAdd.hAdd (α := (ZMod p)[X]) X 1)).coeff (i / p) else 0) = 0
have refine_2 : p ∣ i → (comp (cyclotomic (p ^ (n + 1)) (ZMod p)) (HAdd.hAdd (α := (ZMod p)[X]) X 1)).coeff (i / p) = 0
Tactic: simp only [ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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
⊢ (comp (cyclotomic (p ^ (n + 1)) (ZMod p)) (HAdd.hAdd (α := (ZMod p)[X]) X 1)).coeff (i / p) = 0
have 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
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
Cleared hypotheses: hn, i, hi, k, hk
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
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
⊢ (comp (cyclotomic (p ^ (n + 1)) (ZMod p)) (HAdd.hAdd (α := (ZMod p)[X]) X 1)).coeff (i / p) = 0
have hi₁ : p * k < p * (p ^ n * (p - 1))
Tactic: rw [hk, pow_succ', mul_assoc] at hi
Cleared hypotheses: hi, hk
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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
⊢ (comp (cyclotomic (p ^ (n + 1)) (ZMod p)) (HAdd.hAdd (α := (ZMod p)[X]) X 1)).coeff (i / p) = 0
have refine_2 : (comp (cyclotomic (p ^ (n + 1)) (ZMod p)) (HAdd.hAdd (α := (ZMod p)[X]) X 1)).coeff k = 0
Tactic: rw [hk, mul_comm, Nat.mul_div_cancel _ hp.out.pos]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
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
⊢ (comp (cyclotomic (p ^ (n + 1)) (ZMod p)) (HAdd.hAdd (α := (ZMod p)[X]) X 1)).coeff k = 0
have hn₁ : 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)
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
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)
⊢ (comp (cyclotomic (p ^ (n + 1)) (ZMod p)) (HAdd.hAdd (α := (ZMod p)[X]) X 1)).coeff k = 0
have 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
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
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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 ^ (n + 1) = p * p ^ n
have rw : p * p ^ n = p * p ^ n
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ {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)
have 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)
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']⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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)
⊢ ∀ {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)
have 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)
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']⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff 0 ∉
    HPow.hPow (α := Ideal ℤ) (β := ℕ) (ℤ ∙ (↑p : ℤ)) 2
have refine_3 : ∑ i ∈ range p, eval 1 (HPow.hPow (α := ℤ[X]) X (p ^ n) ^ i) ∉ 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ i ∈ range p, eval 1 (HPow.hPow (α := ℤ[X]) X (p ^ n) ^ i) ∉ HPow.hPow (α := Ideal ℤ) (β := ℕ) (ℤ ∙ (↑p : ℤ)) 2
have refine_3 : ¬HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
⊢ False
have refine_3 : ∀ (k : ℕ) (hk : p = HPow.hPow (β := ℕ) p 2 * k), False
Tactic: obtain ⟨k, hk⟩ := Int.natCast_dvd_natCast.1 h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
k : ℕ
hk : p = HPow.hPow (β := ℕ) p 2 * k
⊢ False
have this : 2 ≤ p
Tactic: have : 2 ≤ p := Nat.Prime.two_le hp.out
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
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
⊢ False
have this₁ : p < HPow.hPow (β := ℕ) p 2
Tactic: have : p < p ^ 2 := by nlinarith
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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
⊢ False
have refine_3 : ∀ (hk : p = HPow.hPow (β := ℕ) p 2 * 0), False
Tactic: cases k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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
⊢ False
have refine_3₁ : ∀ (n : ℕ) (hk : p = HPow.hPow (β := ℕ) p 2 * (n + 1)), False
Tactic: cases k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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
⊢ p ∣ Q.coeff 0
have obtain : ∀ (n : ℕ) (hn : B.dim = n.succ), p ∣ Q.coeff 0
Tactic: obtain ⟨n, hn⟩ := Nat.exists_eq_succ_of_ne_zero B.dim_pos.ne'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
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
⊢ p ∣ Q.coeff 0
have finrank_K_L : Module.finrank K L = B.dim
Tactic: have finrank_K_L : Module.finrank K L = B.dim := B.finrank
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
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
⊢ p ∣ Q.coeff 0
have deg_K_P : natDegree (minpoly K B.gen) = B.dim
Tactic: have deg_K_P : (minpoly K B.gen).natDegree = B.dim := B.natDegree_minpoly
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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
have rw : P.natDegree = natDegree (minpoly K B.gen)
Tactic: rw [← deg_K_P, minpoly.isIntegrallyClosed_eq_field_fractions' K hBint,
      (minpoly.monic hBint).natDegree_map (algebraMap R K)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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)
⊢ P.natDegree = B.dim
have rw₁ : P.natDegree = natDegree (Polynomial.map (algebraMap R K) (minpoly R B.gen))
Tactic: rw [← deg_K_P, minpoly.isIntegrallyClosed_eq_field_fractions' K hBint,
      (minpoly.monic hBint).natDegree_map (algebraMap R K)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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))
⊢ P.natDegree = B.dim
have rw₂ : P.natDegree = natDegree (minpoly R B.gen)
Tactic: rw [← deg_K_P, minpoly.isIntegrallyClosed_eq_field_fractions' K hBint,
      (minpoly.monic hBint).natDegree_map (algebraMap R K)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
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 ∣ Q.coeff 0
have deg_R_P : 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)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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
⊢ p ∣ Q.coeff 0
have 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
Tactic: choose! f hf using
    hei.isWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le (minpoly.aeval R B.gen)
      (minpoly.monic hBint)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
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
⊢ p ∣ Q.coeff 0
have 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
Tactic: simp only [P, (minpoly.monic hBint).natDegree_map, deg_R_P] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
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)
⊢ p ∣ Q.coeff 0
have hndiv : ¬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)