awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
H : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : ℕ
inst_2 : CharP A p
q : ℕ
h : CharP R q
⊢ CharP R p

Tactic:
exact CharP.eq _ (charP_of_injective_ringHom H q) ‹CharP A p› ▸ h
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
H : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : ℕ
⊢ CharP R p ↔ CharP A p

Tactic:
⟨fun _ ↦ charP_of_injective_ringHom H p, fun _ ↦ f.charP H p⟩

Premises used: charP_of_injective_ringHom, RingHom.charP, Iff.intro
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
q : ℕ
hR : ExpChar R q
zero : ∀ [CharZero R], ExpChar A 1
prime : ∀ (hprime : Nat.Prime q) [CharP R q], ExpChar A q
⊢ ExpChar A q

Tactic:
rcases hR with _ | hprime
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
inst_2 : CharZero R
⊢ CharZero A

Tactic:
haveI := charZero_of_injective_ringHom h
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
inst_2 : CharZero R
this : CharZero A
⊢ ExpChar A 1

Tactic:
.zero

Premises used: ExpChar.zero
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
inst_2 : CharZero R
this : CharZero A
⊢ ExpChar A 1

Tactic:
exact .zero
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
q : ℕ
hprime : Nat.Prime q
hchar : CharP R q
⊢ CharP A q

Tactic:
haveI := charP_of_injective_ringHom h q
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
q : ℕ
hprime : Nat.Prime q
hchar : CharP R q
this : CharP A q
⊢ ExpChar A q

Tactic:
.prime hprime

Premises used: ExpChar.prime
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
q : ℕ
hprime : Nat.Prime q
hchar : CharP R q
this : CharP A q
⊢ ExpChar A q

Tactic:
exact .prime hprime
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
H : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
inst_2 : CharZero A
⊢ CharZero R

Tactic:
haveI := f.charZero
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
H : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
inst_2 : CharZero A
this : CharZero R
⊢ ExpChar R 1

Tactic:
.zero

Premises used: ExpChar.zero
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
H : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
inst_2 : CharZero A
this : CharZero R
⊢ ExpChar R 1

Tactic:
exact .zero
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
H : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : ℕ
hp : Nat.Prime p
hchar : CharP A p
⊢ CharP R p

Tactic:
haveI := f.charP H p
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
H : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : ℕ
hp : Nat.Prime p
hchar : CharP A p
this : CharP R p
⊢ ExpChar R p

Tactic:
.prime hp

Premises used: ExpChar.prime
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
H : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : ℕ
hp : Nat.Prime p
hchar : CharP A p
this : CharP R p
⊢ ExpChar R p

Tactic:
exact .prime hp
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
H : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : ℕ
inst_2 cases : ExpChar A p
zero : ∀ [CharZero A], ExpChar R 1
prime : ∀ (hp : Nat.Prime p) [CharP A p], ExpChar R p
⊢ ExpChar R p

Tactic:
cases ‹ExpChar A p› with
  | zero => haveI := f.charZero; exact .zero
  | prime hp => haveI := f.charP H p; exact .prime hp

Premises used: ExpChar
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring A
f : R →+* A
H : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : ℕ
⊢ ExpChar R p ↔ ExpChar A p

Tactic:
⟨fun _ ↦ expChar_of_injective_ringHom H p, fun _ ↦ f.expChar H p⟩

Premises used: expChar_of_injective_ringHom, Iff.intro, RingHom.expChar
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
q : ℕ
inst_3 : ExpChar R q
⊢ ExpChar A q

Tactic:
expChar_of_injective_ringHom h q

Premises used: expChar_of_injective_ringHom
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
q : ℕ
inst_4 : ExpChar R q
⊢ ExpChar A q

Tactic:
expChar_of_injective_ringHom (FaithfulSMul.algebraMap_injective R A) q

Premises used: expChar_of_injective_ringHom, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : DivisionRing R
L : Subfield R
p : ℕ
inst_1 : CharP R p
⊢ CharP.{u_1} (↥L) p

Tactic:
L.subtype.charP L.subtype_injective p

Premises used: Subfield.subtype, Set.Mem, RingHom.charP, Subfield.subtype_injective
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : DivisionRing R
L : Subfield R
p : ℕ
inst_1 : ExpChar R p
⊢ ExpChar.{u_1} (↥L) p

Tactic:
L.subtype.expChar L.subtype_injective p

Premises used: Subfield.subtype, Set.Mem, RingHom.expChar, Subfield.subtype_injective
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_3
inst : Nontrivial R
inst_1 : Semiring R
inst_2 : Algebra ℚ R
⊢ CharP R 0

Tactic:
charP_of_injective_algebraMap (algebraMap ℚ R).injective 0

Premises used: Algebra.algebraMap, charP_of_injective_algebraMap, Rat, RingHom.injective, OfNat.ofNat
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_3
inst : Nontrivial R
inst_1 : Ring R
inst_2 : Algebra ℚ R
⊢ CharZero R

Tactic:
@CharP.charP_to_charZero R _ (algebraRat.charP_zero R)

Premises used: CharP.charP_to_charZero
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
K : Type u_3
L : Type u_4
inst : DivisionRing K
inst_1 : NonAssocSemiring L
inst_2 : Nontrivial L
f : K →+* L
p : ℕ
⊢ CharP K p ↔ CharP L p

Tactic:
simp only [charP_iff, ← f.injective.eq_iff, map_natCast f, map_zero f]

Premises used: Function.Injective.eq_iff, charP_iff, map_zero, RingHom.injective, map_natCast
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : CommSemiring L
inst_2 : Nontrivial L
inst_3 : Algebra K L
p : ℕ
⊢ CharP K p ↔ CharP L p

Tactic:
(algebraMap K L).charP_iff_charP p

Premises used: Algebra.algebraMap, RingHom.charP_iff_charP
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : CommSemiring L
inst_2 : Nontrivial L
inst_3 : Algebra K L
rw : CharP L (ringChar L)
⊢ ringChar K = ringChar L

Tactic:
rw [ringChar.eq_iff, Algebra.charP_iff K L]

Premises used: Algebra.charP_iff, ringChar.eq_iff
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : CommSemiring L
inst_2 : Nontrivial L
inst_3 : Algebra K L
⊢ CharP L (ringChar L)

Tactic:
apply ringChar.charP

Premises used: ringChar.charP
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R_1 : Type u_1
A : Type u_2
R : Type u_3
X : Type u_4
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
⊢ CharP (FreeAlgebra R X) p

Tactic:
charP_of_injective_algebraMap FreeAlgebra.algebraMap_leftInverse.injective p

Premises used: Function.LeftInverse.injective, charP_of_injective_algebraMap, FreeAlgebra.algebraMap_leftInverse
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R_1 : Type u_1
A : Type u_2
R : Type u_3
X : Type u_4
inst : CommSemiring R
p : ℕ
inst_1 : CharZero R
⊢ CharZero (FreeAlgebra R X)

Tactic:
charZero_of_injective_algebraMap FreeAlgebra.algebraMap_leftInverse.injective

Premises used: Function.LeftInverse.injective, FreeAlgebra.algebraMap_leftInverse, charZero_of_injective_algebraMap
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_3
K : Type u_4
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
p : ℕ
inst_4 : CharP R p
⊢ CharP K p

Tactic:
charP_of_injective_algebraMap (IsFractionRing.injective R K) p

Premises used: charP_of_injective_algebraMap, IsFractionRing.injective
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R : Type u_3
K : Type u_4
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : CharZero R
⊢ CharZero K

Tactic:
@CharP.charP_to_charZero K _ (charP_of_isFractionRing R 0)

Premises used: CharP.charP_to_charZero
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R_1 : Type u_1
A : Type u_2
R : Type u_3
K : Type u_4
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
p : ℕ
inst_4 : IsDomain R
inst_5 : CharP R p
⊢ CharP.{u_3} (FractionRing R) p

Tactic:
charP_of_isFractionRing R p

Premises used: IsFractionRing.charP_of_isFractionRing
-- Module: Mathlib.Algebra.CharP.Algebra
Goal:
R_1 : Type u_1
A : Type u_2
R : Type u_3
K : Type u_4
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
p : ℕ
inst_4 : IsDomain R
inst_5 : CharZero R
⊢ CharZero.{u_3} (FractionRing R)

Tactic:
charZero_of_isFractionRing R

Premises used: IsFractionRing.charZero_of_isFractionRing
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
inr :
  ∀
    (this :
      ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} (h : a ≡ b [MOD p]) (hle : a ≤ b),
        Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R))
    (hle : ¬a ≤ b), Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
wlog :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} (h : a ≡ b [MOD p]) (hle : a ≤ b),
    Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)

Tactic:
wlog hle : a ≤ b
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} (h : a ≡ b [MOD p]) (hle : a ≤ b),
    Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
hle : ¬a ≤ b
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)

Tactic:
(this R p h.symm (le_of_not_ge hle)).symm

Premises used: le_of_not_ge, Nat.ModEq.symm, Eq.symm
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} (h : a ≡ b [MOD p]) (hle : a ≤ b),
    Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
hle : ¬a ≤ b
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)

Tactic:
exact (this R p h.symm (le_of_not_ge hle)).symm

Premises used: le_of_not_ge, Nat.ModEq.symm, Eq.symm
-- Module: Mathlib.Algebra.CharP.Basic
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 : ℕ
h : a ≡ b [MOD p]
hle : a ≤ b
⊢ p ∣ b - a

Tactic:
rw [Nat.modEq_iff_dvd' hle] at h

Premises used: Nat.modEq_iff_dvd'
-- Module: Mathlib.Algebra.CharP.Basic
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 : ℕ
h : a ≡ b [MOD p]
hle : a ≤ b
h₁ : p ∣ b - a
⊢ a ≤ b

Tactic:
rw [Nat.modEq_iff_dvd' hle] at h

Premises used: Nat.modEq_iff_dvd'
-- Module: Mathlib.Algebra.CharP.Basic
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 : ℕ
h : p ∣ b - a
hle : a ≤ b
rw : Eq.{u_1 + 1} (α := R) (↑a : R) (↑(b - a + a) : R)
rw₁ : (↑a : R) = HAdd.hAdd (α := R) (↑(b - a) : R) (↑a : R)
rw₂ : (↑a : R) = HAdd.hAdd (α := R) 0 (↑a : R)
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) (↑a : R) (↑a : R)
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)

Tactic:
rw [← Nat.sub_add_cancel hle, Nat.cast_add, (cast_eq_zero_iff R p _).mpr h, zero_add]

Premises used: Iff.mpr, zero_add, Nat.cast_add, Nat.sub_add_cancel, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
a : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑(a % p) : R)

Tactic:
natCast_eq_natCast' R p (Nat.mod_modEq a p).symm

Premises used: Nat.mod_modEq, Nat.ModEq.symm, CharP.natCast_eq_natCast'
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
a b : ℕ
inst_2 : IsRightCancelAdd R
inr :
  ∀
    (this :
      ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsRightCancelAdd R] (hle : a ≤ b),
        Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p])
    (hle : ¬a ≤ b), Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]
wlog :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsRightCancelAdd R] (hle : a ≤ b),
    Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]

Tactic:
wlog hle : a ≤ b
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
a b : ℕ
inst_2 : IsRightCancelAdd R
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsRightCancelAdd R] (hle : a ≤ b),
    Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]
hle : ¬a ≤ b
inr : Eq.{u_1 + 1} (α := R) (↑b : R) (↑a : R) ↔ a ≡ b [MOD p]
inr₁ : b ≡ a [MOD p] ↔ a ≡ b [MOD p]
inr₂ inr₃ : a ≡ b [MOD p] ↔ a ≡ b [MOD p]
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]

Tactic:
rw [eq_comm, this R p (le_of_not_ge hle), Nat.ModEq.comm]

Premises used: le_of_not_ge, eq_comm, Nat.ModEq.comm
-- Module: Mathlib.Algebra.CharP.Basic
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 : IsRightCancelAdd R
hle : a ≤ b
rw : Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ p ∣ b - a
rw₁ : Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ Eq.{u_1 + 1} (α := R) (↑(b - a) : R) 0
rw₂ :
  Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ HAdd.hAdd (α := R) (↑(b - a) : R) (↑a : R) = HAdd.hAdd (α := R) 0 (↑a : R)
rw₃ : Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ HAdd.hAdd (α := R) (↑(b - a) : R) (↑a : R) = (↑a : R)
rw₄ : Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ Eq.{u_1 + 1} (α := R) (↑(b - a + a) : R) (↑a : R)
rw₅ : Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ Eq.{u_1 + 1} (α := R) (↑b : R) (↑a : R)
rw₆ rw₇ : Eq.{u_1 + 1} (α := R) (↑b : R) (↑a : R) ↔ Eq.{u_1 + 1} (α := R) (↑b : R) (↑a : R)
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]

Tactic:
rw [Nat.modEq_iff_dvd' hle, ← cast_eq_zero_iff R p (b - a),
    ← add_right_cancel_iff (G := R) (a := a) (b := b - a), zero_add, ← Nat.cast_add,
    Nat.sub_add_cancel hle, eq_comm]

Premises used: HSub.hSub, Nat.modEq_iff_dvd', eq_comm, zero_add, Nat.cast_add, Nat.sub_add_cancel, add_right_cancel_iff, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
inst_2 : IsRightCancelAdd R
⊢ InjOn.{0, u_1} (β := R) Nat.cast (Iio p)

Tactic:
fun _a ha _b hb hab ↦ ((natCast_eq_natCast _ _).1 hab).eq_of_lt_of_lt ha hb

Premises used: Nat.ModEq.eq_of_lt_of_lt, CharP.natCast_eq_natCast, Iff.mp, Set.InjOn
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
a b : ℤ
rw : Eq.{u_1 + 1} (α := R) (↑b : R) (↑a : R) ↔ a ≡ b [ZMOD (↑p : ℤ)]
rw₁ : HSub.hSub (α := R) (↑b : R) (↑a : R) = 0 ↔ a ≡ b [ZMOD (↑p : ℤ)]
rw₂ : Eq.{u_1 + 1} (α := R) (↑(b - a) : R) 0 ↔ a ≡ b [ZMOD (↑p : ℤ)]
rw₃ : (↑p : ℤ) ∣ b - a ↔ a ≡ b [ZMOD (↑p : ℤ)]
rw₄ rw₅ : (↑p : ℤ) ∣ b - a ↔ (↑p : ℤ) ∣ b - a
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [ZMOD (↑p : ℤ)]

Tactic:
rw [eq_comm, ← sub_eq_zero, ← Int.cast_sub, CharP.intCast_eq_zero_iff R p, Int.modEq_iff_dvd]

Premises used: Int.modEq_iff_dvd, sub_eq_zero, Int.cast_sub, eq_comm, CharP.intCast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
a : ℤ
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑(a % (↑p : ℤ)) : R)

Tactic:
(CharP.intCast_eq_intCast R p).mpr (Int.mod_modEq a p).symm

Premises used: Iff.mpr, Int.ModEq.symm, Nat.cast, CharP.intCast_eq_intCast, Int.mod_modEq
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
inst_2 : IsRightCancelAdd R
a : ℤ
ha₀ : 0 ≤ a
ha : a < (↑p : ℤ)
b : ℤ
hb₀ : 0 ≤ b
hb : b < (↑p : ℤ)
hab : Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
⊢ 0 ≤ a

Tactic:
ha₀
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
inst_2 : IsRightCancelAdd R
a : ℤ
ha₀ : 0 ≤ a
ha : a < (↑p : ℤ)
b : ℤ
hb₀ : 0 ≤ b
hb : b < (↑p : ℤ)
hab : Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
lift :
  ∀ (a : ℕ) (ha : LT.lt (α := ℤ) (↑a : ℤ) (↑p : ℤ)) (hab : Eq.{u_1 + 1} (α := R) (↑(↑a : ℤ) : R) (↑b : R)), (↑a : ℤ) = b
⊢ a = b

Tactic:
lift a to ℕ using ha₀
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
inst_2 : IsRightCancelAdd R
b : ℤ
hb₀ : 0 ≤ b
hb : b < (↑p : ℤ)
a : ℕ
ha : LT.lt (α := ℤ) (↑a : ℤ) (↑p : ℤ)
hab : Eq.{u_1 + 1} (α := R) (↑(↑a : ℤ) : R) (↑b : R)
⊢ 0 ≤ b

Tactic:
hb₀
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
inst_2 : IsRightCancelAdd R
b : ℤ
hb₀ : 0 ≤ b
hb : b < (↑p : ℤ)
a : ℕ
ha : LT.lt (α := ℤ) (↑a : ℤ) (↑p : ℤ)
hab : Eq.{u_1 + 1} (α := R) (↑(↑a : ℤ) : R) (↑b : R)
lift :
  ∀ (b : ℕ) (hb : LT.lt (α := ℤ) (↑b : ℤ) (↑p : ℤ)) (hab : Eq.{u_1 + 1} (α := R) (↑(↑a : ℤ) : R) (↑(↑b : ℤ) : R)),
    Eq (α := ℤ) (↑a : ℤ) (↑b : ℤ)
⊢ (↑a : ℤ) = b

Tactic:
lift b to ℕ using hb₀
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
inst_2 : IsRightCancelAdd R
a : ℕ
ha : LT.lt (α := ℤ) (↑a : ℤ) (↑p : ℤ)
b : ℕ
hb : LT.lt (α := ℤ) (↑b : ℤ) (↑p : ℤ)
hab : Eq.{u_1 + 1} (α := R) (↑(↑a : ℤ) : R) (↑(↑b : ℤ) : R)
norm_cast : ∀ (ha : a < p) (hb : b < p) (hab : Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)), a = b
⊢ Eq (α := ℤ) (↑a : ℤ) (↑b : ℤ)

Tactic:
norm_cast at *
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
inst_2 : IsRightCancelAdd R
a b : ℕ
ha : a < p
hb : b < p
hab : Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
⊢ a = b

Tactic:
natCast_injOn_Iio _ _ ha hb hab

Premises used: CharP.natCast_injOn_Iio
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
inst_2 : IsRightCancelAdd R
a b : ℕ
ha : a < p
hb : b < p
hab : Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
⊢ a = b

Tactic:
exact natCast_injOn_Iio _ _ ha hb hab

Premises used: CharP.natCast_injOn_Iio
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
p q : ℕ
inst_2 : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h : Eq.{u_1 + 1} (α := R) (↑q : R) 0
⊢ p ∣ q

Tactic:
rw [cast_eq_zero_iff R p q] at h

Premises used: CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
p q : ℕ
inst_2 : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h : p ∣ q
inl : ∀ [CharP R 1] (hneq : 1 ≠ q) (h : 1 ∣ q), False
inr : ∀ (h : p = q), False
⊢ False

Tactic:
rcases hq.eq_one_or_self_of_dvd _ h with rfl | h

Premises used: Nat.Prime.eq_one_or_self_of_dvd, rfl
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
q : ℕ
hq : Nat.Prime q
inst_2 : CharP R 1
hneq : 1 ≠ q
h : 1 ∣ q
⊢ False

Tactic:
false_of_nontrivial_of_char_one (R := R)

Premises used: CharP.false_of_nontrivial_of_char_one
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
q : ℕ
hq : Nat.Prime q
inst_2 : CharP R 1
hneq : 1 ≠ q
h : 1 ∣ q
⊢ False

Tactic:
exact false_of_nontrivial_of_char_one (R := R)

Premises used: CharP.false_of_nontrivial_of_char_one
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
p q : ℕ
inst_2 : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h_1 : p ∣ q
h : p = q
⊢ False

Tactic:
hneq h
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
p q : ℕ
inst_2 : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h_1 : p ∣ q
h : p = q
⊢ False

Tactic:
exact hneq h
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
p : ℕ
hprime : Nat.Prime p
hp0 : Eq.{u_1 + 1} (α := R) (↑p : R) 0
⊢ ringChar R = p

Tactic:
Or.resolve_left ((Nat.dvd_prime hprime).1 (ringChar.dvd hp0)) ringChar_ne_one

Premises used: ringChar.dvd, Or.resolve_left, Nat.dvd_prime, Iff.mp, CharP.ringChar_ne_one
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
p : ℕ
hp : Nat.Prime p
⊢ CharP R p ↔ Eq.{u_1 + 1} (α := R) (↑p : R) 0

Tactic:
⟨fun _ => cast_eq_zero R p,
   fun hp0 => (ringChar_of_prime_eq_zero hp hp0) ▸ inferInstance⟩

Premises used: CharP.cast_eq_zero, Eq.rec, inferInstance, CharP.ringChar_of_prime_eq_zero, Iff.intro
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq.{u_2 + 1} (α := R) 2 2
⊢ Eq.{u_2 + 1} (α := R) 2 (↑2 : R)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
rw : ¬(ringChar R = 1 ∨ ringChar R = 2)
⊢ Ne.{u_2 + 1} (α := R) 2 0

Tactic:
rw [Ne, (by norm_cast : (2 : R) = (2 : ℕ)), ringChar.spec, Nat.dvd_prime Nat.prime_two]

Premises used: Ne, Nat.dvd_prime, Nat.prime_two, ringChar.spec
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
⊢ ¬(ringChar R = 1 ∨ ringChar R = 2)

Tactic:
mt (or_iff_left hR).mp CharP.ringChar_ne_one

Premises used: mt, Iff.mp, or_iff_left, CharP.ringChar_ne_one
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
⊢ ¬(ringChar R = 1 ∨ ringChar R = 2)

Tactic:
exact mt (or_iff_left hR).mp CharP.ringChar_ne_one

Premises used: mt, Iff.mp, or_iff_left, CharP.ringChar_ne_one
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
⊢ Ne.{u_2 + 1} (α := R) (-1) 1

Tactic:
fun h =>
  Ring.two_ne_zero hR (one_add_one_eq_two (R := R) ▸ neg_eq_iff_add_eq_zero.mp h)

Premises used: neg_eq_iff_add_eq_zero, Ring.two_ne_zero, Eq.rec, one_add_one_eq_two, Iff.mp, Not