awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.CharP.LinearMaps
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
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
⊢ Eq.{u_2 + 1} (α := M →ₗ[R] M) (↑n : M →ₗ[R] M) 0 ↔ p ∣ n

Tactic:
rw [exact, LinearMap.ext_iff, ← hchar.1]

Premises used: LinearMap.ext_iff, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.LinearMaps
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
h :
  ∀ (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)
x : M
hx : Eq (α := Ideal R) (Ideal.torsionOf R M x) ⊥
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 0

Tactic:
simpa [← Ideal.mem_torsionOf_iff, hx] using h x

Premises used: Ideal.mem_torsionOf_iff
-- Module: Mathlib.Algebra.CharP.LinearMaps
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
⊢ (∀ (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:
exact ⟨fun h ↦ htorsion.casesOn fun x hx ↦ by simpa [← Ideal.mem_torsionOf_iff, hx] using h x,
      fun h ↦ (congrArg (fun t ↦ ∀ x, t • x = 0) h).mpr fun x ↦ zero_smul R x⟩
-- Module: Mathlib.Algebra.CharP.LinearMaps
Goal:
D : Type u_1
inst : DivisionRing D
p : ℕ
inst_1 : CharP D p
⊢ CharP.{u_1} (LinearMap (R := ↥(Subring.center D)) (RingHom.id ↥(Subring.center D)) D D) p

Tactic:
charP_of_injective_ringHom (Algebra.lmul (Subring.center D) D).toRingHom.injective p

Premises used: Algebra.lmul, Subring.center, Membership.mem, charP_of_injective_ringHom, Subtype, RingHom.injective, AlgHom.toRingHom
-- Module: Mathlib.Algebra.CharP.LinearMaps
Goal:
D : Type u_1
inst : DivisionRing D
p : ℕ
inst_1 : ExpChar D p
⊢ ExpChar.{u_1} (LinearMap (R := ↥(Subring.center D)) (RingHom.id ↥(Subring.center D)) D D) p

Tactic:
expChar_of_injective_ringHom (Algebra.lmul (Subring.center D) D).toRingHom.injective p

Premises used: Algebra.lmul, Subring.center, Membership.mem, Subtype, expChar_of_injective_ringHom, RingHom.injective, AlgHom.toRingHom
-- Module: Mathlib.Algebra.CharP.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
apply : ¬q = 0 → IsPrimePow q
⊢ q = 0 ∨ IsPrimePow q

Tactic:
apply or_iff_not_imp_left.2

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.Algebra.CharP.LocalRing
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
⊢ CharP K (ringChar K)

Tactic:
haveI RM_char := ringChar.charP K
-- Module: Mathlib.Algebra.CharP.LocalRing
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
inr : ∀ (r_zero : r = 0), IsPrimePow q
⊢ IsPrimePow q

Tactic:
rcases CharP.char_is_prime_or_zero K r with r_prime | r_zero

Premises used: CharP.char_is_prime_or_zero
-- Module: Mathlib.Algebra.CharP.LocalRing
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
rw rw₁ : q = q
⊢ q = r ^ n * a

Tactic:
rw [Nat.mul_div_cancel' (Nat.ordProj_dvd q r)]

Premises used: Nat.ordProj_dvd, Nat.mul_div_cancel'
-- Module: Mathlib.Algebra.CharP.LocalRing
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

Tactic:
have q_eq_a_mul_rn : q = r ^ n * a := by rw [Nat.mul_div_cancel' (Nat.ordProj_dvd q r)]
-- Module: Mathlib.Algebra.CharP.LocalRing
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 ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)

Tactic:
have r_ne_dvd_a := Nat.not_dvd_ordCompl r_prime q_pos
-- Module: Mathlib.Algebra.CharP.LocalRing
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 : ℕ)
⊢ r ^ n ∣ q

Tactic:
have rn_dvd_q : r ^ n ∣ q := ⟨a, q_eq_a_mul_rn⟩
-- Module: Mathlib.Algebra.CharP.LocalRing
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
⊢ q = a * r ^ n

Tactic:
rw [mul_comm] at q_eq_a_mul_rn

Premises used: mul_comm
-- Module: Mathlib.Algebra.CharP.LocalRing
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
q_eq_a_mul_rn₁ : q = a * r ^ n
⊢ ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)

Tactic:
rw [mul_comm] at q_eq_a_mul_rn

Premises used: mul_comm
-- Module: Mathlib.Algebra.CharP.LocalRing
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
q_eq_a_mul_rn₁ : q = a * r ^ n
r_ne_dvd_a₁ : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
⊢ r ^ n ∣ q

Tactic:
rw [mul_comm] at q_eq_a_mul_rn

Premises used: mul_comm
-- Module: Mathlib.Algebra.CharP.LocalRing
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
by_contra : ∀ (g : ¬IsUnit.{u_1} (M := R) (↑a : R)), False
⊢ IsUnit.{u_1} (M := R) (↑a : R)

Tactic:
by_contra g
-- Module: Mathlib.Algebra.CharP.LocalRing
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)
⊢ (↑a : R) ∈ nonunits R

Tactic:
rw [← mem_nonunits_iff] at g

Premises used: mem_nonunits_iff
-- Module: Mathlib.Algebra.CharP.LocalRing
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
⊢ Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) (↑a : R)

Tactic:
rw [← IsLocalRing.mem_maximalIdeal] at g

Premises used: IsLocalRing.mem_maximalIdeal
-- Module: Mathlib.Algebra.CharP.LocalRing
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)
⊢ 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
-- Module: Mathlib.Algebra.CharP.LocalRing
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
⊢ 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

Premises used: map_natCast
-- Module: Mathlib.Algebra.CharP.LocalRing
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
⊢ ringChar K ∣ a

Tactic:
have r_dvd_a := (ringChar.spec K a).1 a_cast_zero
-- Module: Mathlib.Algebra.CharP.LocalRing
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
r_dvd_a : ringChar K ∣ a
⊢ False

Tactic:
absurd r_dvd_a r_ne_dvd_a

Premises used: absurd
-- Module: Mathlib.Algebra.CharP.LocalRing
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
r_dvd_a : ringChar K ∣ a
⊢ False

Tactic:
exact absurd r_dvd_a r_ne_dvd_a

Premises used: absurd
-- Module: Mathlib.Algebra.CharP.LocalRing
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)

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
-- Module: Mathlib.Algebra.CharP.LocalRing
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
rw₆ rw₇ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := 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]

Premises used: CharP.cast_eq_zero, mul_assoc, Nat.cast, MulZeroClass.mul_zero, Nat.cast_mul, HPow.hPow, IsUnit.val_inv_mul, one_mul
-- Module: Mathlib.Algebra.CharP.LocalRing
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

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]
-- Module: Mathlib.Algebra.CharP.LocalRing
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
⊢ 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
-- Module: Mathlib.Algebra.CharP.LocalRing
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
q_eq_rn : q = r ^ n
n_zero : n = 0
⊢ q = 1

Tactic:
simpa [n_zero] using q_eq_rn
-- Module: Mathlib.Algebra.CharP.LocalRing
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
q_eq_rn : q = r ^ n
⊢ n ≠ 0

Tactic:
have n_pos : n ≠ 0 := fun n_zero =>
      absurd (by simpa [n_zero] using q_eq_rn) (CharP.char_ne_one R q)
-- Module: Mathlib.Algebra.CharP.LocalRing
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
q_eq_rn : q = r ^ n
n_pos : n ≠ 0
⊢ IsPrimePow q

Tactic:
⟨r, ⟨n, ⟨r_prime.prime, ⟨pos_iff_ne_zero.mpr n_pos, q_eq_rn.symm⟩⟩⟩⟩

Premises used: Iff.mpr, IsPrimePow, Nat.Prime.prime, And.intro, Exists.intro, Eq.symm, pos_iff_ne_zero
-- Module: Mathlib.Algebra.CharP.LocalRing
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
q_eq_rn : q = r ^ n
n_pos : n ≠ 0
⊢ IsPrimePow q

Tactic:
exact ⟨r, ⟨n, ⟨r_prime.prime, ⟨pos_iff_ne_zero.mpr n_pos, q_eq_rn.symm⟩⟩⟩⟩
-- Module: Mathlib.Algebra.CharP.LocalRing
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_zero : r = 0
⊢ CharP K 0

Tactic:
haveI K_char_p_0 := ringChar.of_eq r_zero
-- Module: Mathlib.Algebra.CharP.LocalRing
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_zero : r = 0
K_char_p_0 : CharP K 0
⊢ CharZero K

Tactic:
haveI K_char_zero : CharZero K := CharP.charP_to_charZero K
-- Module: Mathlib.Algebra.CharP.LocalRing
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_zero : r = 0
K_char_p_0 : CharP K 0
K_char_zero : CharZero K
⊢ CharZero R

Tactic:
haveI R_char_zero := RingHom.charZero (IsLocalRing.residue R)
-- Module: Mathlib.Algebra.CharP.LocalRing
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_zero : r = 0
K_char_p_0 : CharP K 0
K_char_zero : CharZero K
R_char_zero : CharZero R
⊢ q = 0

Tactic:
have q_zero := CharP.eq R char_R_q (CharP.ofCharZero R)
-- Module: Mathlib.Algebra.CharP.LocalRing
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_zero : r = 0
K_char_p_0 : CharP K 0
K_char_zero : CharZero K
R_char_zero : CharZero R
q_zero : q = 0
⊢ IsPrimePow q

Tactic:
absurd q_zero q_pos

Premises used: absurd
-- Module: Mathlib.Algebra.CharP.LocalRing
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_zero : r = 0
K_char_p_0 : CharP K 0
K_char_zero : CharZero K
R_char_zero : CharZero R
q_zero : q = 0
⊢ IsPrimePow q

Tactic:
exact absurd q_zero q_pos

Premises used: absurd
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
P : Prop
mp : (∀ p > 0, MixedCharZero R p → P) → ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
mpr : (∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P) → ∀ p > 0, MixedCharZero R p → P
⊢ (∀ p > 0, MixedCharZero R p → P) ↔ ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P

Tactic:
constructor
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h : ∀ p > 0, MixedCharZero R p → P
q : ℕ
q_prime : Nat.Prime q
q_mixedChar : MixedCharZero R q
⊢ P

Tactic:
h q (Nat.Prime.pos q_prime) q_mixedChar

Premises used: Nat.Prime.pos
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h : ∀ p > 0, MixedCharZero R p → P
q : ℕ
q_prime : Nat.Prime q
q_mixedChar : MixedCharZero R q
⊢ P

Tactic:
exact h q (Nat.Prime.pos q_prime) q_mixedChar

Premises used: Nat.Prime.pos
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
mpr : ∀ (I : Ideal R) (hI_ne_top : I ≠ ⊤), CharP.{u_1} (R ⧸ I) q → P
⊢ P

Tactic:
rcases q_mixedChar.charP_quotient with ⟨I, hI_ne_top, _⟩

Premises used: MixedCharZero.charP_quotient
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) q
mpr : ∀ (M : Ideal R) (hM_max : M.IsMaximal) (h_IM : I ≤ M), P
⊢ P

Tactic:
rcases Ideal.exists_le_maximal I hI_ne_top with ⟨M, hM_max, h_IM⟩

Premises used: Ideal.exists_le_maximal
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
mpr : P
⊢ P

Tactic:
let r := ringChar (R ⧸ M)