awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
rw : (x - y) ^ n = (x - y) ^ (n % p) * ((x - y) ^ p) ^ (n / p)
rw₁ : (x - y) ^ n = (x - y) ^ (n % p) * (x - y) ^ (p * (n / p))
⊢ (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
have rw₂ : (x - y) ^ n = (x - y) ^ (n % p + p * (n / p))
Tactic: rw [← sub_pow_expChar_of_commute _ h, ← pow_mul, ← pow_add, Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
rw : (x - y) ^ n = (x - y) ^ (n % p) * ((x - y) ^ p) ^ (n / p)
rw₁ : (x - y) ^ n = (x - y) ^ (n % p) * (x - y) ^ (p * (n / p))
rw₂ : (x - y) ^ n = (x - y) ^ (n % p + p * (n / p))
⊢ (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
have rw₃ : (x - y) ^ n = (x - y) ^ n
Tactic: rw [← sub_pow_expChar_of_commute _ h, ← pow_mul, ← pow_add, Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hR : ExpChar R p
⊢ HPow.hPow (α := R) (-1) p = -1
have rw : HPow.hPow (α := R) (-1) p + 1 = 0
Tactic: rw [eq_neg_iff_add_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hR : ExpChar R p
⊢ HPow.hPow (α := R) (-1) p + 1 = 0
have nth_rw : HPow.hPow (α := R) (-1) p + HPow.hPow (α := R) 1 p = 0
Tactic: nth_rw 2 [← one_pow p]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hR : ExpChar R p
⊢ HPow.hPow (α := R) (-1) p + HPow.hPow (α := R) 1 p = 0
have rw : HAdd.hAdd (α := R) (-1) 1 ^ p = 0
Tactic: rw [← add_pow_expChar_of_commute _ (Commute.one_right _), neg_add_cancel,
    zero_pow (expChar_ne_zero R p)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hR : ExpChar R p
rw : HAdd.hAdd (α := R) (-1) 1 ^ p = 0
⊢ HPow.hPow (α := R) (-1) p + HPow.hPow (α := R) 1 p = 0
have rw₁ : HPow.hPow (α := R) 0 p = 0
Tactic: rw [← add_pow_expChar_of_commute _ (Commute.one_right _), neg_add_cancel,
    zero_pow (expChar_ne_zero R p)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hR : ExpChar R p
rw : HAdd.hAdd (α := R) (-1) 1 ^ p = 0
rw₁ : HPow.hPow (α := R) 0 p = 0
⊢ HPow.hPow (α := R) (-1) p + HPow.hPow (α := R) 1 p = 0
have rw₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← add_pow_expChar_of_commute _ (Commute.one_right _), neg_add_cancel,
    zero_pow (expChar_ne_zero R p)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
p n : ℕ
hR : ExpChar R p
⊢ HPow.hPow (α := R) (-1) (p ^ n) = -1
have rw : HPow.hPow (α := R) (-1) (p ^ n) + 1 = 0
Tactic: rw [eq_neg_iff_add_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
p n : ℕ
hR : ExpChar R p
⊢ HPow.hPow (α := R) (-1) (p ^ n) + 1 = 0
have nth_rw : HPow.hPow (α := R) (-1) (p ^ n) + HPow.hPow (α := R) 1 (p ^ n) = 0
Tactic: nth_rw 2 [← one_pow (p ^ n)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
p n : ℕ
hR : ExpChar R p
⊢ HPow.hPow (α := R) (-1) (p ^ n) + HPow.hPow (α := R) 1 (p ^ n) = 0
have rw : HAdd.hAdd (α := R) (-1) 1 ^ p ^ n = 0
Tactic: rw [← add_pow_expChar_pow_of_commute _ _ (Commute.one_right _), neg_add_cancel,
    zero_pow (pow_ne_zero _ <| expChar_ne_zero R p)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
p n : ℕ
hR : ExpChar R p
rw : HAdd.hAdd (α := R) (-1) 1 ^ p ^ n = 0
⊢ HPow.hPow (α := R) (-1) (p ^ n) + HPow.hPow (α := R) 1 (p ^ n) = 0
have rw₁ : HPow.hPow (α := R) 0 (p ^ n) = 0
Tactic: rw [← add_pow_expChar_pow_of_commute _ _ (Commute.one_right _), neg_add_cancel,
    zero_pow (pow_ne_zero _ <| expChar_ne_zero R p)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
p n : ℕ
hR : ExpChar R p
rw : HAdd.hAdd (α := R) (-1) 1 ^ p ^ n = 0
rw₁ : HPow.hPow (α := R) 0 (p ^ n) = 0
⊢ HPow.hPow (α := R) (-1) (p ^ n) + HPow.hPow (α := R) 1 (p ^ n) = 0
have rw₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← add_pow_expChar_pow_of_commute _ _ (Commute.one_right _), neg_add_cancel,
    zero_pow (pow_ne_zero _ <| expChar_ne_zero R p)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ (↑p : R) * x
⊢ r ∣ (x + y) ^ p - y ^ p
have rw : r ∣ x ^ p + (↑p : R) * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * (↑(p.choose k / p) : R)
Tactic: rw [add_pow_prime_eq hpri, add_right_comm, add_assoc, add_sub_assoc, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (hypothesis)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Finite R
inst_2 : CharP R 0
⊢ False
have this : CharZero R
Tactic: haveI : CharZero R := charP_to_charZero R
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
inst_3 : Finite R
⊢ Nat.Prime (ringChar R)
have apply : ringChar R ≠ 0
Tactic: apply CharP.char_prime_of_ne_zero R
-- Lean 4 proof step from Mathlib.Algebra.CharP.LinearMaps (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : ℕ
hchar : CharP R p
htorsion : ∃ (x : M), Eq (α := Ideal R) (Ideal.torsionOf R M x) ⊥
n : ℕ
⊢ Eq.{u_2 + 1} (α := M →ₗ[R] M) (↑n : M →ₗ[R] M) 0 ↔ p ∣ n
have exact : (↑n : M →ₗ[R] M) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) 1
Tactic: have exact : (n : M →ₗ[R] M) = (n : R) • 1 := by
      simp only [Nat.cast_smul_eq_nsmul, nsmul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.LinearMaps (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : ℕ
hchar : CharP R p
htorsion : ∃ (x : M), Eq (α := Ideal R) (Ideal.torsionOf R M x) ⊥
n : ℕ
exact : (↑n : M →ₗ[R] M) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) 1
⊢ Eq.{u_2 + 1} (α := M →ₗ[R] M) (↑n : M →ₗ[R] M) 0 ↔ p ∣ n
have rw : (∀ (x : M),
    Eq (α := M) ((HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) 1 : (a : M) → M) x : M)
      ((0 : (a : M) → M) x : M)) ↔
  Eq.{u_1 + 1} (α := R) (↑n : R) 0
Tactic: rw [exact, LinearMap.ext_iff, ← hchar.1]
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
⊢ q = 0 ∨ IsPrimePow q
have apply : ¬q = 0 → IsPrimePow q
Tactic: apply or_iff_not_imp_left.2
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
⊢ IsPrimePow q
have RM_char : CharP K (ringChar K)
Tactic: haveI RM_char := ringChar.charP K
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
⊢ IsPrimePow q
have inl : ∀ (r_prime : Nat.Prime r), IsPrimePow q
Tactic: rcases CharP.char_is_prime_or_zero K r with r_prime | r_zero
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
inl : ∀ (r_prime : Nat.Prime r), IsPrimePow q
⊢ IsPrimePow q
have inr : ∀ (r_zero : r = 0), IsPrimePow q
Tactic: rcases CharP.char_is_prime_or_zero K r with r_prime | r_zero
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
⊢ q = r ^ n * a
have rw : q = q
Tactic: rw [Nat.mul_div_cancel' (Nat.ordProj_dvd q r)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
⊢ IsPrimePow q
have q_eq_a_mul_rn : q = r ^ n * a
Tactic: have q_eq_a_mul_rn : q = r ^ n * a := by rw [Nat.mul_div_cancel' (Nat.ordProj_dvd q r)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = r ^ n * a
⊢ IsPrimePow q
have r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
Tactic: have r_ne_dvd_a := Nat.not_dvd_ordCompl r_prime q_pos
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = r ^ n * a
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
⊢ IsPrimePow q
have rn_dvd_q : r ^ n ∣ q
Tactic: have rn_dvd_q : r ^ n ∣ q := ⟨a, q_eq_a_mul_rn⟩
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = r ^ n * a
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
⊢ IsPrimePow q
have q_eq_a_mul_rn₁ : q = a * r ^ n
Tactic: rw [mul_comm] at q_eq_a_mul_rn
Cleared hypotheses: q_eq_a_mul_rn, r_ne_dvd_a, rn_dvd_q
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
⊢ IsUnit.{u_1} (M := R) (↑a : R)
have by_contra : ∀ (g : ¬IsUnit.{u_1} (M := R) (↑a : R)), False
Tactic: by_contra g
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
g : ¬IsUnit.{u_1} (M := R) (↑a : R)
⊢ False
have g₁ : (↑a : R) ∈ nonunits R
Tactic: rw [← mem_nonunits_iff] at g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
g : (↑a : R) ∈ nonunits R
⊢ False
have g₁ : Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) (↑a : R)
Tactic: rw [← IsLocalRing.mem_maximalIdeal] at g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
g : Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) (↑a : R)
⊢ False
have a_cast_zero : Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) (IsLocalRing.maximalIdeal R : Ideal R))
  ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal R) : (a : R) → R ⧸ IsLocalRing.maximalIdeal R) (↑a : R)) 0
Tactic: have a_cast_zero := Ideal.Quotient.eq_zero_iff_mem.2 g
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
g : Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) (↑a : R)
a_cast_zero :
  Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) (IsLocalRing.maximalIdeal R : Ideal R))
    ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal R) : (a : R) → R ⧸ IsLocalRing.maximalIdeal R) (↑a : R)) 0
⊢ False
have a_cast_zero₁ : Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) (IsLocalRing.maximalIdeal R : Ideal R))
  (↑a : R ⧸ IsLocalRing.maximalIdeal R) 0
Tactic: rw [map_natCast] at a_cast_zero
Cleared hypotheses: a_cast_zero
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
g : Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) (↑a : R)
a_cast_zero :
  Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) (IsLocalRing.maximalIdeal R : Ideal R))
    (↑a : R ⧸ IsLocalRing.maximalIdeal R) 0
⊢ False
have r_dvd_a : ringChar K ∣ a
Tactic: have r_dvd_a := (ringChar.spec K a).1 a_cast_zero
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
⊢ IsPrimePow q
have a_unit : IsUnit.{u_1} (M := R) (↑a : R)
Tactic: have a_unit : IsUnit (a : R) := by
      by_contra g
      rw [← mem_nonunits_iff] at g
      rw [← IsLocalRing.mem_maximalIdeal] at g
      have a_cast_zero := Ideal.Quotient.eq_zero_iff_mem.2 g
      rw [map_natCast] at a_cast_zero
      have r_dvd_a := (ringChar.spec K a).1 a_cast_zero
      exact absurd r_dvd_a r_ne_dvd_a
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit.{u_1} (M := R) (↑a : R)
⊢ Eq.{u_1 + 1} (α := R) (↑(r ^ n) : R) 0
have rw : HMul.hMul (α := R) 1 (↑(r ^ n) : R) = 0
Tactic: rw [← one_mul (↑(r ^ n) : R), ← a_unit.val_inv_mul, mul_assoc, ← Nat.cast_mul,
        ← q_eq_a_mul_rn, CharP.cast_eq_zero R q, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit.{u_1} (M := R) (↑a : R)
rw : HMul.hMul (α := R) 1 (↑(r ^ n) : R) = 0
⊢ Eq.{u_1 + 1} (α := R) (↑(r ^ n) : R) 0
have rw₁ : (↑a_unit.unit⁻¹ : R) * (↑a : R) * (↑(r ^ n) : R) = 0
Tactic: rw [← one_mul (↑(r ^ n) : R), ← a_unit.val_inv_mul, mul_assoc, ← Nat.cast_mul,
        ← q_eq_a_mul_rn, CharP.cast_eq_zero R q, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit.{u_1} (M := R) (↑a : R)
rw : HMul.hMul (α := R) 1 (↑(r ^ n) : R) = 0
rw₁ : (↑a_unit.unit⁻¹ : R) * (↑a : R) * (↑(r ^ n) : R) = 0
⊢ Eq.{u_1 + 1} (α := R) (↑(r ^ n) : R) 0
have rw₂ : (↑a_unit.unit⁻¹ : R) * HMul.hMul (α := R) (↑a : R) (↑(r ^ n) : R) = 0
Tactic: rw [← one_mul (↑(r ^ n) : R), ← a_unit.val_inv_mul, mul_assoc, ← Nat.cast_mul,
        ← q_eq_a_mul_rn, CharP.cast_eq_zero R q, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit.{u_1} (M := R) (↑a : R)
rw : HMul.hMul (α := R) 1 (↑(r ^ n) : R) = 0
rw₁ : (↑a_unit.unit⁻¹ : R) * (↑a : R) * (↑(r ^ n) : R) = 0
rw₂ : (↑a_unit.unit⁻¹ : R) * HMul.hMul (α := R) (↑a : R) (↑(r ^ n) : R) = 0
⊢ Eq.{u_1 + 1} (α := R) (↑(r ^ n) : R) 0
have rw₃ : (↑a_unit.unit⁻¹ : R) * (↑(a * r ^ n) : R) = 0
Tactic: rw [← one_mul (↑(r ^ n) : R), ← a_unit.val_inv_mul, mul_assoc, ← Nat.cast_mul,
        ← q_eq_a_mul_rn, CharP.cast_eq_zero R q, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit.{u_1} (M := R) (↑a : R)
rw : HMul.hMul (α := R) 1 (↑(r ^ n) : R) = 0
rw₁ : (↑a_unit.unit⁻¹ : R) * (↑a : R) * (↑(r ^ n) : R) = 0
rw₂ : (↑a_unit.unit⁻¹ : R) * HMul.hMul (α := R) (↑a : R) (↑(r ^ n) : R) = 0
rw₃ : (↑a_unit.unit⁻¹ : R) * (↑(a * r ^ n) : R) = 0
⊢ Eq.{u_1 + 1} (α := R) (↑(r ^ n) : R) 0
have rw₄ : (↑a_unit.unit⁻¹ : R) * (↑q : R) = 0
Tactic: rw [← one_mul (↑(r ^ n) : R), ← a_unit.val_inv_mul, mul_assoc, ← Nat.cast_mul,
        ← q_eq_a_mul_rn, CharP.cast_eq_zero R q, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit.{u_1} (M := R) (↑a : R)
rw : HMul.hMul (α := R) 1 (↑(r ^ n) : R) = 0
rw₁ : (↑a_unit.unit⁻¹ : R) * (↑a : R) * (↑(r ^ n) : R) = 0
rw₂ : (↑a_unit.unit⁻¹ : R) * HMul.hMul (α := R) (↑a : R) (↑(r ^ n) : R) = 0
rw₃ : (↑a_unit.unit⁻¹ : R) * (↑(a * r ^ n) : R) = 0
rw₄ : (↑a_unit.unit⁻¹ : R) * (↑q : R) = 0
⊢ Eq.{u_1 + 1} (α := R) (↑(r ^ n) : R) 0
have rw₅ : (↑a_unit.unit⁻¹ : R) * 0 = 0
Tactic: rw [← one_mul (↑(r ^ n) : R), ← a_unit.val_inv_mul, mul_assoc, ← Nat.cast_mul,
        ← q_eq_a_mul_rn, CharP.cast_eq_zero R q, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit.{u_1} (M := R) (↑a : R)
rw : HMul.hMul (α := R) 1 (↑(r ^ n) : R) = 0
rw₁ : (↑a_unit.unit⁻¹ : R) * (↑a : R) * (↑(r ^ n) : R) = 0
rw₂ : (↑a_unit.unit⁻¹ : R) * HMul.hMul (α := R) (↑a : R) (↑(r ^ n) : R) = 0
rw₃ : (↑a_unit.unit⁻¹ : R) * (↑(a * r ^ n) : R) = 0
rw₄ : (↑a_unit.unit⁻¹ : R) * (↑q : R) = 0
rw₅ : (↑a_unit.unit⁻¹ : R) * 0 = 0
⊢ Eq.{u_1 + 1} (α := R) (↑(r ^ n) : R) 0
have rw₆ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← one_mul (↑(r ^ n) : R), ← a_unit.val_inv_mul, mul_assoc, ← Nat.cast_mul,
        ← q_eq_a_mul_rn, CharP.cast_eq_zero R q, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit.{u_1} (M := R) (↑a : R)
⊢ IsPrimePow q
have rn_cast_zero : Eq.{u_1 + 1} (α := R) (↑(r ^ n) : R) 0
Tactic: have rn_cast_zero : ↑(r ^ n) = (0 : R) := by
      rw [← one_mul (↑(r ^ n) : R), ← a_unit.val_inv_mul, mul_assoc, ← Nat.cast_mul,
        ← q_eq_a_mul_rn, CharP.cast_eq_zero R q, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit.{u_1} (M := R) (↑a : R)
rn_cast_zero : Eq.{u_1 + 1} (α := R) (↑(r ^ n) : R) 0
⊢ IsPrimePow q
have q_eq_rn : q = r ^ n
Tactic: have q_eq_rn := Nat.dvd_antisymm ((CharP.cast_eq_zero_iff R q (r ^ n)).mp rn_cast_zero) rn_dvd_q