awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fintype R
p : ℕ
inst_2 : Fact (Nat.Prime p)
⊢ p ∣ ringChar R ↔ p ∣ Fintype.card R

Tactic:
⟨fun h =>
      h.trans <|
        Int.natCast_dvd_natCast.mp <|
          (CharP.intCast_eq_zero_iff R (ringChar R) (Fintype.card R)).mp <|
            mod_cast Nat.cast_card_eq_zero R,
      fun h => ?_⟩

Premises used: Int.cast, Int.cast_natCast, congrArg, Int.cast_zero, cast, Nat.cast_card_eq_zero, Fintype.card, Nat.cast, ringChar, congr, Iff.intro, Iff.mp, Nat.cast_zero, Eq.symm, Eq, CharP.intCast_eq_zero_iff, Eq.trans, Int.natCast_dvd_natCast, Dvd.dvd.trans
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fintype R
p : ℕ
inst_2 : Fact (Nat.Prime p)
h : ∀ (h : p ∣ Fintype.card R), p ∣ ringChar R
⊢ p ∣ ringChar R ↔ p ∣ Fintype.card R

Tactic:
refine
    ⟨fun h =>
      h.trans <|
        Int.natCast_dvd_natCast.mp <|
          (CharP.intCast_eq_zero_iff R (ringChar R) (Fintype.card R)).mp <|
            mod_cast Nat.cast_card_eq_zero R,
      fun h => ?_⟩
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fintype R
p : ℕ
inst_2 : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
by_contra : ∀ (h₀ : ¬p ∣ ringChar R), False
⊢ p ∣ ringChar R

Tactic:
by_contra h₀
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fintype R
p : ℕ
inst_2 : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
rcases : ∀ (r : R) (hr : addOrderOf r = p), False
⊢ False

Tactic:
rcases exists_prime_addOrderOf_dvd_card p h with ⟨r, hr⟩

Premises used: exists_prime_addOrderOf_dvd_card
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fintype R
p : ℕ
inst_2 : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
⊢ addOrderOf r • r = 0

Tactic:
have hr₁ := addOrderOf_nsmul_eq_zero r
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fintype R
p : ℕ
inst_2 : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
hr₁ : addOrderOf r • r = 0
⊢ (↑p : R) * r = 0

Tactic:
rw [hr, nsmul_eq_mul] at hr₁

Premises used: nsmul_eq_mul
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fintype R
p : ℕ
inst_2 : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
hr₁ : (↑p : R) * r = 0
rcases : ∀ (u : R) (hu : u * (↑p : R) = 1), False
⊢ False

Tactic:
rcases IsUnit.exists_left_inv ((isUnit_iff_not_dvd_char R p).mpr h₀) with ⟨u, hu⟩

Premises used: Iff.mpr, isUnit_iff_not_dvd_char, IsUnit.exists_left_inv
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fintype R
p : ℕ
inst_2 : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
hr₁ : (↑p : R) * r = 0
u : R
hu : u * (↑p : R) = 1
⊢ u * ((↑p : R) * r) = u * 0

Tactic:
apply_fun (· * ·) u at hr₁

Premises used: HMul.hMul
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fintype R
p : ℕ
inst_2 : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
u : R
hu : u * (↑p : R) = 1
hr₁ : u * ((↑p : R) * r) = u * 0
⊢ r = 0

Tactic:
rw [mul_zero, ← mul_assoc, hu, one_mul] at hr₁

Premises used: mul_assoc, MulZeroClass.mul_zero, one_mul
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fintype R
p : ℕ
inst_2 : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
u : R
hu : u * (↑p : R) = 1
hr₁ : r = 0
⊢ False

Tactic:
mt AddMonoid.addOrderOf_eq_one_iff.mpr (ne_of_eq_of_ne hr (Nat.Prime.ne_one Fact.out)) hr₁

Premises used: Iff.mpr, ne_of_eq_of_ne, AddMonoid.addOrderOf_eq_one_iff, mt, Nat.Prime.ne_one, Fact.out
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fintype R
p : ℕ
inst_2 : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
u : R
hu : u * (↑p : R) = 1
hr₁ : r = 0
⊢ False

Tactic:
exact mt AddMonoid.addOrderOf_eq_one_iff.mpr (ne_of_eq_of_ne hr (Nat.Prime.ne_one Fact.out)) hr₁

Premises used: Iff.mpr, ne_of_eq_of_ne, AddMonoid.addOrderOf_eq_one_iff, mt, Nat.Prime.ne_one, Fact.out
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fintype R
p : ℕ
inst_2 : Fact (Nat.Prime p)
hp : p ∣ Fintype.card R
⊢ ¬IsUnit.{u_1} (M := R) (↑p : R)

Tactic:
mt (isUnit_iff_not_dvd_char R p).mp
    (Classical.not_not.mpr ((prime_dvd_char_iff_dvd_card p).mpr hp))

Premises used: Iff.mpr, Classical.not_not, prime_dvd_char_iff_dvd_card, mt, isUnit_iff_not_dvd_char, Iff.mp
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
hR : Fintype.card R = p
⊢ CharP R p

Tactic:
have := Fintype.one_lt_card_iff_nontrivial.1 (hR ▸ hp.1.one_lt)
  (CharP.charP_iff_prime_eq_zero hp.1).2 (hR ▸ Nat.cast_card_eq_zero R)

Premises used: Iff.mpr, Eq.rec, Nat.cast_card_eq_zero, Fintype.one_lt_card_iff_nontrivial, Iff.mp, CharP.charP_iff_prime_eq_zero, Fact.out
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Fintype R
p f : ℕ
hp : Fact (Nat.Prime p)
hR : Fintype.card R = p ^ f
h0 : f = 0
⊢ Fintype.card R ≤ 1

Tactic:
simpa [h0] using hR.le

Premises used: Eq.le
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Fintype R
p f : ℕ
hp : Fact (Nat.Prime p)
hR : Fintype.card R = p ^ f
hf : f ≠ 0
⊢ Eq.{u_1 + 1} (α := R) (↑p : R) 0

Tactic:
simpa [hf, hR] using Nat.cast_card_eq_zero R

Premises used: Nat.cast_card_eq_zero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
a : ℕ
inst_2 : a.AtLeastTwo
h : p ∣ a
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : Eq.{u_1 + 1} (α := R) (↑a : R) 0), Eq.{u_1 + 1} (α := R) (OfNat.ofNat a) 0
⊢ Eq.{u_1 + 1} (α := R) (OfNat.ofNat a) 0

Tactic:
rwa [← CharP.cast_eq_zero_iff R p] at h

Premises used: CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
q : ℕ
h : p = q
⊢ CharP R q

Tactic:
h ▸ ‹CharP R p›

Premises used: Eq.rec
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
⊢ Eq.{u_1 + 1} (α := R) (↑p : R) 0

Tactic:
(cast_eq_zero_iff R p p).2 dvd_rfl

Premises used: Iff.mpr, dvd_rfl, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
k a : ℕ
rw : p ∣ p * a
⊢ Eq.{u_1 + 1} (α := R) (↑(p * a) : R) 0

Tactic:
rw [CharP.cast_eq_zero_iff R p]

Premises used: CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
k a : ℕ
⊢ p ∣ p * a

Tactic:
Nat.dvd_mul_right p a

Premises used: Nat.dvd_mul_right
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
k a : ℕ
⊢ p ∣ p * a

Tactic:
exact Nat.dvd_mul_right p a

Premises used: Nat.dvd_mul_right
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
k : ℕ
this : ∀ (a : ℕ), Eq.{u_1 + 1} (α := R) (↑(p * a) : R) 0
rw rw₁ : Eq.{u_1 + 1} (α := R) (↑k : R) (↑k : R)
⊢ Eq.{u_1 + 1} (α := R) (↑k : R) (↑(k % p + p * (k / p)) : R)

Tactic:
rw [Nat.mod_add_div]

Premises used: Nat.mod_add_div
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
k : ℕ
this : ∀ (a : ℕ), Eq.{u_1 + 1} (α := R) (↑(p * a) : R) 0
⊢ Eq.{u_1 + 1} (α := R) (↑(k % p + p * (k / p)) : R) (↑(k % p) : R)

Tactic:
simp [this]
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
a b : ℕ
inst_2 : IsLeftCancelAdd R
inr :
  ∀
    (this :
      ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsLeftCancelAdd R] (hle : a ≤ b),
        Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a % p = b % p)
    (hle : b < a), Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a % p = b % p
wlog! :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsLeftCancelAdd R] (hle : a ≤ b),
    Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a % p = b % p
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a % p = b % p

Tactic:
wlog! hle : a ≤ b
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
a b : ℕ
inst_2 : IsLeftCancelAdd R
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsLeftCancelAdd R] (hle : a ≤ b),
    Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a % p = b % p
hle : b < a
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a % p = b % p

Tactic:
simpa only [eq_comm] using (this _ _ hle.le)

Premises used: LT.lt.le, eq_comm
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R_1 : Type u_1
inst : AddMonoidWithOne R_1
p_1 a_1 b_1 : ℕ
R : Type u_1
inst_1 : AddMonoidWithOne R
p : ℕ
inst_2 : CharP R p
a b : ℕ
inst_3 : IsLeftCancelAdd R
hle : a ≤ b
obtain : ∀ (c : ℕ) (hle : a ≤ a + c), Eq.{u_1 + 1} (α := R) (↑a : R) (↑(a + c) : R) ↔ a % p = (a + c) % p
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a % p = b % p

Tactic:
obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_le hle

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R_1 : Type u_1
inst : AddMonoidWithOne R_1
p_1 a_1 b : ℕ
R : Type u_1
inst_1 : AddMonoidWithOne R
p : ℕ
inst_2 : CharP R p
a : ℕ
inst_3 : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
rw : p ∣ c ↔ a % p = (a + c) % p
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑(a + c) : R) ↔ a % p = (a + c) % p

Tactic:
rw [Nat.cast_add, left_eq_add, CharP.cast_eq_zero_iff R p]

Premises used: left_eq_add, Nat.cast_add, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R_1 : Type u_1
inst : AddMonoidWithOne R_1
p_1 a_1 b : ℕ
R : Type u_1
inst_1 : AddMonoidWithOne R
p : ℕ
inst_2 : CharP R p
a : ℕ
inst_3 : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
mp : p ∣ c → a % p = (a + c) % p
mpr : a % p = (a + c) % p → p ∣ c
⊢ p ∣ c ↔ a % p = (a + c) % p

Tactic:
constructor
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R_1 : Type u_1
inst : AddMonoidWithOne R_1
p_1 a_1 b : ℕ
R : Type u_1
inst_1 : AddMonoidWithOne R
p : ℕ
inst_2 : CharP R p
a : ℕ
inst_3 : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
⊢ p ∣ c → a % p = (a + c) % p

Tactic:
simp +contextual [Nat.add_mod, Nat.dvd_iff_mod_eq_zero]

Premises used: Nat.dvd_iff_mod_eq_zero, Nat.add_mod
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R_1 : Type u_1
inst : AddMonoidWithOne R_1
p_1 a_1 b : ℕ
R : Type u_1
inst_1 : AddMonoidWithOne R
p : ℕ
inst_2 : CharP R p
a : ℕ
inst_3 : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
h : a % p = (a + c) % p
⊢ (a + c - a) % p = 0

Tactic:
have := Nat.sub_mod_eq_zero_of_mod_eq h.symm
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R_1 : Type u_1
inst : AddMonoidWithOne R_1
p_1 a_1 b : ℕ
R : Type u_1
inst_1 : AddMonoidWithOne R
p : ℕ
inst_2 : CharP R p
a : ℕ
inst_3 : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
h : a % p = (a + c) % p
this : (a + c - a) % p = 0
⊢ p ∣ c

Tactic:
simpa [Nat.dvd_iff_mod_eq_zero] using this

Premises used: Nat.dvd_iff_mod_eq_zero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
inst_2 : p.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := R) (OfNat.ofNat p) 0

Tactic:
cast_eq_zero R p

Premises used: CharP.cast_eq_zero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p q : ℕ
hp : CharP R p
hq : CharP R q
⊢ p = q

Tactic:
Nat.dvd_antisymm ((cast_eq_zero_iff (self := hp) R p q).1 (@cast_eq_zero _ _ _ hq))
    ((cast_eq_zero_iff (self := hq) R q p).1 (@cast_eq_zero _ _ _ hp))

Premises used: CharP.cast_eq_zero, Iff.mp, CharP.cast_eq_zero_iff, Nat.dvd_antisymm
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
a b : ℕ
inst_2 : CharZero R
x : ℕ
rw : Eq.{u_1 + 1} (α := R) (↑x : R) 0 ↔ x = 0
rw₁ : Eq.{u_1 + 1} (α := R) (↑x : R) (↑0 : R) ↔ x = 0
rw₂ rw₃ : x = 0 ↔ x = 0
⊢ Eq.{u_1 + 1} (α := R) (↑x : R) 0 ↔ 0 ∣ x

Tactic:
rw [zero_dvd_iff, ← Nat.cast_zero, Nat.cast_inj]

Premises used: zero_dvd_iff, Nat.cast_inj, Nat.cast_zero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
a : ℤ
inl : ∀ (h : a < 0), Eq.{u_1 + 1} (α := R) (↑a : R) 0 ↔ (↑p : ℤ) ∣ a
inr : Eq.{u_1 + 1} (α := R) (↑0 : R) 0 ↔ Dvd.dvd (α := ℤ) (↑p : ℤ) 0
inr₁ : ∀ (h : 0 < a), Eq.{u_1 + 1} (α := R) (↑a : R) 0 ↔ (↑p : ℤ) ∣ a
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) 0 ↔ (↑p : ℤ) ∣ a

Tactic:
rcases lt_trichotomy a 0 with (h | rfl | h)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
a : ℤ
h : a < 0
inl : Eq.{u_1 + 1} (α := R) (↑(-a) : R) 0 ↔ (↑p : ℤ) ∣ -a
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) 0 ↔ (↑p : ℤ) ∣ a

Tactic:
rw [← neg_eq_zero, ← Int.cast_neg, ← Int.dvd_neg]

Premises used: Int.cast_neg, neg_eq_zero, Int.dvd_neg
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
a : ℤ
h : a < 0
⊢ 0 ≤ -a

Tactic:
Int.neg_nonneg.mpr (le_of_lt h)

Premises used: Iff.mpr, le_of_lt, Int.neg_nonneg
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
a : ℤ
h : a < 0
inl : ∀ (b : ℕ), Eq.{u_1 + 1} (α := R) (↑(↑b : ℤ) : R) 0 ↔ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑b : ℤ)
⊢ Eq.{u_1 + 1} (α := R) (↑(-a) : R) 0 ↔ (↑p : ℤ) ∣ -a

Tactic:
lift -a to ℕ using Int.neg_nonneg.mpr (le_of_lt h) with b

Premises used: Iff.mpr, le_of_lt, Int.neg_nonneg
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
a : ℤ
h : a < 0
b : ℕ
inl : Eq.{u_1 + 1} (α := R) (↑b : R) 0 ↔ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑b : ℤ)
inl₁ : p ∣ b ↔ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑b : ℤ)
inl₂ inl₃ : p ∣ b ↔ p ∣ b
⊢ Eq.{u_1 + 1} (α := R) (↑(↑b : ℤ) : R) 0 ↔ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑b : ℤ)

Tactic:
rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]

Premises used: Int.cast_natCast, CharP.cast_eq_zero_iff, Int.natCast_dvd_natCast
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
⊢ Eq.{u_1 + 1} (α := R) (↑0 : R) 0 ↔ Dvd.dvd (α := ℤ) (↑p : ℤ) 0

Tactic:
simp
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
a : ℤ
h : 0 < a
⊢ 0 ≤ a

Tactic:
le_of_lt h

Premises used: le_of_lt
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
a : ℤ
h : 0 < a
inr :
  ∀ (b : ℕ) (h : LT.lt (α := ℤ) 0 (↑b : ℤ)),
    Eq.{u_1 + 1} (α := R) (↑(↑b : ℤ) : R) 0 ↔ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑b : ℤ)
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) 0 ↔ (↑p : ℤ) ∣ a

Tactic:
lift a to ℕ using le_of_lt h with b

Premises used: le_of_lt
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
a : ℤ
b : ℕ
h : LT.lt (α := ℤ) 0 (↑b : ℤ)
inr : Eq.{u_1 + 1} (α := R) (↑b : R) 0 ↔ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑b : ℤ)
inr₁ : p ∣ b ↔ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑b : ℤ)
inr₂ inr₃ : p ∣ b ↔ p ∣ b
⊢ Eq.{u_1 + 1} (α := R) (↑(↑b : ℤ) : R) 0 ↔ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑b : ℤ)

Tactic:
rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]

Premises used: Int.cast_natCast, CharP.cast_eq_zero_iff, Int.natCast_dvd_natCast
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
inst_1 : CharP R 0
⊢ CharZero R

Tactic:
charZero_of_inj_zero fun n h0 => eq_zero_of_zero_dvd ((cast_eq_zero_iff R 0 n).mp h0)

Premises used: charZero_of_inj_zero, Iff.mp, eq_zero_of_zero_dvd, CharP.cast_eq_zero_iff, OfNat.ofNat
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
⊢ CharP R 0 ↔ CharZero R

Tactic:
⟨fun _ ↦ charP_to_charZero R, fun _ ↦ ofCharZero R⟩

Premises used: CharP.charP_to_charZero, Iff.intro, CharP.ofCharZero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), Eq.{u_1 + 1} (α := R) (↑p : R) 0 → p = 0
x : ℕ
rw : Eq.{u_1 + 1} (α := R) (↑x : R) 0 ↔ x = 0
⊢ Eq.{u_1 + 1} (α := R) (↑x : R) 0 ↔ 0 ∣ x

Tactic:
rw [zero_dvd_iff]

Premises used: zero_dvd_iff
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), Eq.{u_1 + 1} (α := R) (↑p : R) 0 → p = 0
⊢ Eq.{u_1 + 1} (α := R) (↑0 : R) 0

Tactic:
simp
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), Eq.{u_1 + 1} (α := R) (↑p : R) 0 → p = 0
x : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑x : R) 0 ↔ x = 0

Tactic:
exact ⟨H x, by rintro rfl; simp⟩
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ¬∀ (p : ℕ), Eq.{u_1 + 1} (α := R) (↑p : R) 0 → p = 0
x : ℕ
H1 : Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯ ∣ x
rw :
  Eq.{u_1 + 1} (α := R)
    (↑(Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯ *
          (x / Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯)) :
      R)
    0
rw₁ :
  HMul.hMul (α := R) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R)
      (↑(x / Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R) =
    0
rw₂ : HMul.hMul (α := R) 0 (↑(x / Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R) = 0
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) (↑x : R) 0

Tactic:
rw [← Nat.mul_div_cancel' H1, Nat.cast_mul,
            of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
            zero_mul]

Premises used: MulZeroClass.zero_mul, not_not_of_not_imp, Nat.cast_mul, Iff.mp, of_not_not, Classical.not_forall, Nat.mul_div_cancel', Nat.find_spec
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
⊢ ∃! p : ℕ, CharP R p

Tactic:
let ⟨c, H⟩ := CharP.exists R
  ⟨c, H, fun _y H2 => CharP.eq R H2 H⟩

Premises used: CharP.exists, CharP.eq, ExistsUnique, And.intro, Exists.intro, CharP, _private.0.CharP.existsUnique.match_1
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
this : CharP R (ringChar R) := ⋯
⊢ ∀ (x : ℕ), Eq.{u_1 + 1} (α := R) (↑x : R) 0 ↔ ringChar R ∣ x

Tactic:
CharP.cast_eq_zero_iff R (ringChar R)

Premises used: ringChar, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
this : CharP R (ringChar R) := ⋯
⊢ ∀ (x : ℕ), Eq.{u_1 + 1} (α := R) (↑x : R) 0 ↔ ringChar R ∣ x

Tactic:
exact CharP.cast_eq_zero_iff R (ringChar R)

Premises used: ringChar, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
C : CharP R p
⊢ ringChar R = p

Tactic:
((Classical.choose_spec (CharP.existsUnique R)).2 p C).symm

Premises used: CharP.existsUnique, Classical.choose_spec, And.right, ringChar, Eq.symm
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
⊢ CharP R (ringChar R)

Tactic:
⟨spec R⟩

Premises used: ringChar.spec, CharP.mk
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
h : ringChar R = p
⊢ CharP R p

Tactic:
CharP.congr (ringChar R) h

Premises used: CharP.congr, ringChar
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
⊢ ringChar R = p ↔ CharP R p

Tactic:
⟨of_eq, @eq R _ p⟩

Premises used: ringChar.of_eq, ringChar.eq, Iff.intro
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
x : ℕ
hx : Eq.{u_1 + 1} (α := R) (↑x : R) 0
⊢ ringChar R ∣ x

Tactic:
(spec R x).1 hx

Premises used: ringChar.spec, Iff.mp
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharZero R
⊢ ringChar R = 0

Tactic:
eq R 0

Premises used: ringChar.eq, OfNat.ofNat
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
rw rw₁ : ringChar R ∣ ringChar R
⊢ Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0

Tactic:
rw [ringChar.spec]

Premises used: ringChar.spec
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
rw : ringChar R ∣ 1 ↔ Subsingleton R
rw₁ : Eq.{u_1 + 1} (α := R) (↑1 : R) 0 ↔ Subsingleton R
rw₂ : Eq.{u_1 + 1} (α := R) 0 (↑1 : R) ↔ Subsingleton R
rw₃ : Eq.{u_1 + 1} (α := R) 0 1 ↔ Subsingleton R
rw₄ rw₅ : Subsingleton R ↔ Subsingleton R
⊢ ringChar R = 1 ↔ Subsingleton R

Tactic:
rw [← Nat.dvd_one, ← spec, eq_comm, Nat.cast_one, subsingleton_iff_zero_eq_one]

Premises used: Nat.dvd_one, eq_comm, ringChar.spec, subsingleton_iff_zero_eq_one, Nat.cast_one
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Subsingleton R
⊢ ringChar R = 1

Tactic:
simpa
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
inst_2 : Fact (2 < p)
rw : ¬p ∣ 2
⊢ Ne.{u_1 + 1} (α := R) (-1) 1

Tactic:
rw [ne_comm, ← sub_ne_zero, sub_neg_eq_add, one_add_one_eq_two, ← Nat.cast_two, Ne,
    CharP.cast_eq_zero_iff R p 2]

Premises used: sub_ne_zero, Ne, one_add_one_eq_two, ne_comm, CharP.cast_eq_zero_iff, OfNat.ofNat, Nat.cast_two, sub_neg_eq_add
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
inst_2 : Fact (2 < p)
⊢ ¬p ∣ 2

Tactic:
fun h ↦ (Fact.out : 2 < p).not_ge <| Nat.le_of_dvd Nat.zero_lt_two h

Premises used: Nat.zero_lt_two, LT.lt.not_ge, Nat.le_of_dvd, Not, Fact.out
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
inst_2 : Fact (2 < p)
⊢ ¬p ∣ 2

Tactic:
exact fun h ↦ (Fact.out : 2 < p).not_ge <| Nat.le_of_dvd Nat.zero_lt_two h

Premises used: Nat.zero_lt_two, LT.lt.not_ge, Nat.le_of_dvd, Fact.out
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocRing R
rw : CharP R 0 ↔ CharZero R
rw₁ rw₂ : CharZero R ↔ CharZero R
⊢ ringChar R = 0 ↔ CharZero R

Tactic:
rw [ringChar.eq_iff, charP_zero_iff_charZero]

Premises used: CharP.charP_zero_iff_charZero, ringChar.eq_iff
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
p : ℕ
hc : CharP R p
hp : p = 1
⊢ Eq.{u_1 + 1} (α := R) 1 0

Tactic:
simpa using (cast_eq_zero_iff R p 1).mpr (hp ▸ dvd_refl p)

Premises used: Iff.mpr, Eq.rec, CharP.cast_eq_zero_iff, OfNat.ofNat, dvd_refl
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : NoZeroDivisors R
p : ℕ
inst_2 : CharP R p
hp : 2 ≤ p
d : ℕ
hdvd : ∃ (e : ℕ), p = d * e
e : ℕ
hmul : p = d * e
this_1 : Eq.{u_1 + 1} (α := R) (↑p : R) 0
this_2 : HMul.hMul (α := R) (↑d : R) (↑e : R) = 0
he : Eq.{u_1 + 1} (α := R) (↑e : R) 0
this_3 : p ∣ e
this_4 : e ∣ p
this : e = p
⊢ 0 < p

Tactic:
grind
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : NoZeroDivisors R
p : ℕ
inst_2 : CharP R p
hp : 2 ≤ p
d : ℕ
hdvd : ∃ (e : ℕ), p = d * e
e : ℕ
hmul : p = d * e
this_1 : Eq.{u_1 + 1} (α := R) (↑p : R) 0
this_2 : HMul.hMul (α := R) (↑d : R) (↑e : R) = 0
he : Eq.{u_1 + 1} (α := R) (↑e : R) 0
this_3 : p ∣ e
this_4 : e ∣ p
this : e = p
h₀ : 0 < p
⊢ d * p = 1 * p

Tactic:
grind
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
p : ℕ
hc : CharP R p
⊢ Nat.Prime p ∨ p = 0

Tactic:
match p, hc with
  | 0, _ => Or.inr rfl
  | 1, hc => absurd (Eq.refl (1 : ℕ)) (@char_ne_one R _ _ (1 : ℕ) hc)
  | m + 2, hc => Or.inl (@char_is_prime_of_two_le R _ _ (m + 2) hc (Nat.le_add_left 2 m))

Premises used: Nat.Prime, Nat.le_add_left, absurd, CharP.char_is_prime_of_two_le, HAdd.hAdd, Eq.refl, Or.inl, Or, _private.0.CharP.char_is_prime_or_zero.match_1, OfNat.ofNat, Eq, Or.inr, rfl, CharP.char_ne_one