awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
hR : ringChar R ≠ 2
a : R
⊢ -a = a ↔ a = 0

Tactic:
⟨fun h =>
    (mul_eq_zero.mp <| (two_mul a).trans <| neg_eq_iff_add_eq_zero.mp h).resolve_left
      (Ring.two_ne_zero hR),
    fun h => ((congr_arg (fun x => -x) h).trans neg_zero).trans h.symm⟩

Premises used: neg_eq_iff_add_eq_zero, Ring.two_ne_zero, two_mul, Or.resolve_left, mul_eq_zero, congr_arg, Iff.intro, Iff.mp, Eq.symm, neg_zero, Neg.neg, Eq.trans
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
S : Type u_2
inst : AddMonoidWithOne R
inst_1 : AddMonoidWithOne S
p q : ℕ
inst_2 : CharP R p
inst_3 : CharP S q
⊢ ∀ (x : ℕ), Eq (α := R × S) (↑x : R × S) 0 ↔ p.lcm q ∣ x

Tactic:
simp [Prod.ext_iff, CharP.cast_eq_zero_iff R p, CharP.cast_eq_zero_iff S q, Nat.lcm_dvd_iff]

Premises used: Prod.ext_iff, Nat.lcm_dvd_iff, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
S : Type u_2
inst : AddMonoidWithOne R
inst_1 : AddMonoidWithOne S
p q : ℕ
inst_2 : CharP R p
inst_3 : CharP S p
⊢ CharP (R × S) (p.lcm p)

Tactic:
Nat.lcm.charP R S p p

Premises used: Nat.lcm.charP
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
S : Type u_2
inst : AddMonoidWithOne R
inst_1 : AddMonoidWithOne S
p q : ℕ
inst_2 : CharP R p
inst_3 : CharP S p
h : p = p.lcm p
⊢ CharP (R × S) p

Tactic:
convert! Nat.lcm.charP R S p p

Premises used: Nat.lcm.charP
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
S : Type u_2
inst : AddMonoidWithOne R
inst_1 : AddMonoidWithOne S
p q : ℕ
inst_2 : CharP R p
inst_3 : CharP S p
⊢ p = p.lcm p

Tactic:
simp
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
h : Eq.{u_2 + 1} (α := R) (↑0 : R) (↑0 : R)
⊢ Eq (α := ℤ) 0 0

Tactic:
simp only
    [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢

Premises used: Int.cast_neg, Int.cast_zero, zero_eq_neg, zero_ne_one, neg_eq_zero, one_ne_zero, Int.cast_one
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
h : Eq.{u_2 + 1} (α := R) (↑0 : R) (↑1 : R)
⊢ Eq (α := ℤ) 0 1

Tactic:
simp only
    [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢

Premises used: Int.cast_neg, Int.cast_zero, zero_eq_neg, zero_ne_one, neg_eq_zero, one_ne_zero, Int.cast_one
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
h : Eq.{u_2 + 1} (α := R) (↑0 : R) (↑(-1) : R)
⊢ Eq (α := ℤ) 0 (-1)

Tactic:
simp only
    [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢

Premises used: Int.cast_neg, Int.cast_zero, zero_eq_neg, zero_ne_one, neg_eq_zero, one_ne_zero, Int.cast_one
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
h : Eq.{u_2 + 1} (α := R) (↑1 : R) (↑0 : R)
⊢ Eq (α := ℤ) 1 0

Tactic:
simp only
    [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢

Premises used: Int.cast_neg, Int.cast_zero, zero_eq_neg, zero_ne_one, neg_eq_zero, one_ne_zero, Int.cast_one
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
h : Eq.{u_2 + 1} (α := R) (↑1 : R) (↑1 : R)
⊢ Eq (α := ℤ) 1 1

Tactic:
simp only
    [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢

Premises used: Int.cast_neg, Int.cast_zero, zero_eq_neg, zero_ne_one, neg_eq_zero, one_ne_zero, Int.cast_one
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
h : Eq.{u_2 + 1} (α := R) (↑1 : R) (↑(-1) : R)
⊢ Eq.{u_2 + 1} (α := R) 1 (-1)

Tactic:
simp only
    [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢

Premises used: Int.cast_neg, Int.cast_zero, zero_eq_neg, zero_ne_one, neg_eq_zero, one_ne_zero, Int.cast_one
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
h : Eq.{u_2 + 1} (α := R) (↑(-1) : R) (↑0 : R)
⊢ Eq (α := ℤ) (-1) 0

Tactic:
simp only
    [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢

Premises used: Int.cast_neg, Int.cast_zero, zero_eq_neg, zero_ne_one, neg_eq_zero, one_ne_zero, Int.cast_one
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
h : Eq.{u_2 + 1} (α := R) (↑(-1) : R) (↑1 : R)
⊢ Eq.{u_2 + 1} (α := R) (-1) 1

Tactic:
simp only
    [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢

Premises used: Int.cast_neg, Int.cast_zero, zero_eq_neg, zero_ne_one, neg_eq_zero, one_ne_zero, Int.cast_one
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
h : Eq.{u_2 + 1} (α := R) (↑(-1) : R) (↑(-1) : R)
⊢ Eq (α := ℤ) (-1) (-1)

Tactic:
simp only
    [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢

Premises used: Int.cast_neg, Int.cast_zero, zero_eq_neg, zero_ne_one, neg_eq_zero, one_ne_zero, Int.cast_one
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
h : Eq.{u_2 + 1} (α := R) 1 (-1)
⊢ Eq (α := ℤ) 1 (-1)

Tactic:
((Ring.neg_one_ne_one_of_char_ne_two hR).symm h).elim

Premises used: Ring.neg_one_ne_one_of_char_ne_two, False.elim, Ne.symm
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
h : Eq.{u_2 + 1} (α := R) 1 (-1)
⊢ Eq (α := ℤ) 1 (-1)

Tactic:
exact ((Ring.neg_one_ne_one_of_char_ne_two hR).symm h).elim

Premises used: Ring.neg_one_ne_one_of_char_ne_two, False.elim, Ne.symm
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
h : Eq.{u_2 + 1} (α := R) (-1) 1
⊢ Eq (α := ℤ) (-1) 1

Tactic:
((Ring.neg_one_ne_one_of_char_ne_two hR) h).elim

Premises used: Ring.neg_one_ne_one_of_char_ne_two, False.elim
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
h : Eq.{u_2 + 1} (α := R) (-1) 1
⊢ Eq (α := ℤ) (-1) 1

Tactic:
exact ((Ring.neg_one_ne_one_of_char_ne_two hR) h).elim

Premises used: Ring.neg_one_ne_one_of_char_ne_two, False.elim
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
h : CharZero R
p : ℕ
hp : Nat.Prime p
⊢ Ne.{u_1 + 1} (α := R) (↑p : R) 0

Tactic:
simp [hp.ne_zero]

Premises used: Nat.Prime.ne_zero
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
refine : ∀ (h : ∀ (p : ℕ), Nat.Prime p → Ne.{u_1 + 1} (α := R) (↑p : R) 0), CharZero R
⊢ CharZero R ↔ ∀ (p : ℕ), Nat.Prime p → Ne.{u_1 + 1} (α := R) (↑p : R) 0

Tactic:
refine ⟨fun h p hp => by simp [hp.ne_zero], fun h => ?_⟩
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → Ne.{u_1 + 1} (α := R) (↑p : R) 0
p : ℕ := ringChar R
hp : Nat.Prime p
⊢ CharZero R

Tactic:
simpa using h p hp
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
h_1 : ∀ (p : ℕ), Nat.Prime p → Ne.{u_1 + 1} (α := R) (↑p : R) 0
p : ℕ := ringChar R
h : p = 0
⊢ CharP R 0

Tactic:
have : CharP R 0 := h ▸ inferInstance
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
h_1 : ∀ (p : ℕ), Nat.Prime p → Ne.{u_1 + 1} (α := R) (↑p : R) 0
p : ℕ := ringChar R
h : p = 0
this : CharP R 0
⊢ CharZero R

Tactic:
CharP.charP_to_charZero R

Premises used: CharP.charP_to_charZero
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
h_1 : ∀ (p : ℕ), Nat.Prime p → Ne.{u_1 + 1} (α := R) (↑p : R) 0
p : ℕ := ringChar R
h : p = 0
this : CharP R 0
⊢ CharZero R

Tactic:
exact CharP.charP_to_charZero R

Premises used: CharP.charP_to_charZero
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → Ne.{u_1 + 1} (α := R) (↑p : R) 0
p : ℕ := ringChar R
⊢ Nat.Prime p ∨ p = 0

Tactic:
cases CharP.char_is_prime_or_zero R p with
  | inl hp => simpa using h p hp
  | inr h => have : CharP R 0 := h ▸ inferInstance; exact CharP.charP_to_charZero R

Premises used: CharP.char_is_prime_or_zero
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
S : Type u_2
inst_1 : Semiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
zero : ∀ [CharZero R] [ExpChar R 1] [ExpChar S 1], ExpChar (R × S) 1
prime : ∀ (hp : Nat.Prime p) [CharP R p], ExpChar (R × S) p
⊢ ExpChar (R × S) p

Tactic:
obtain hp | ⟨hp⟩ := ‹ExpChar R p›

Premises used: ExpChar
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
S : Type u_2
inst_1 : Semiring S
inst_2 : CharZero R
inst_3 : ExpChar R 1
inst_4 : ExpChar S 1
⊢ ExpChar (R × S) 1

Tactic:
constructor
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
S : Type u_2
inst_1 : Semiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
hp : Nat.Prime p
hchar : CharP R p
prime : ∀ [CharZero S] [ExpChar R 1] [ExpChar S 1] (hp : Nat.Prime 1) [CharP R 1], ExpChar (R × S) 1
prime₁ : Nat.Prime p → ∀ [CharP S p], ExpChar (R × S) p
⊢ ExpChar (R × S) p

Tactic:
obtain _ | _ := ‹ExpChar S p›

Premises used: ExpChar
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
S : Type u_2
inst_1 : Semiring S
inst_2 : CharZero S
inst_3 : ExpChar R 1
inst_4 : ExpChar S 1
hp : Nat.Prime 1
hchar : CharP R 1
⊢ ExpChar (R × S) 1

Tactic:
(Nat.not_prime_one hp).elim

Premises used: Nat.not_prime_one, False.elim
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
S : Type u_2
inst_1 : Semiring S
inst_2 : CharZero S
inst_3 : ExpChar R 1
inst_4 : ExpChar S 1
hp : Nat.Prime 1
hchar : CharP R 1
⊢ ExpChar (R × S) 1

Tactic:
exact (Nat.not_prime_one hp).elim

Premises used: Nat.not_prime_one, False.elim
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
S : Type u_2
inst_1 : Semiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
hp : Nat.Prime p
hchar : CharP R p
hprime : Nat.Prime p
hchar_1 : CharP S p
⊢ CharP (R × S) p

Tactic:
have := Prod.charP R S p
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
S : Type u_2
inst_1 : Semiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
hp : Nat.Prime p
hchar : CharP R p
hprime : Nat.Prime p
hchar_1 : CharP S p
this : CharP (R × S) p
⊢ ExpChar (R × S) p

Tactic:
.prime hp

Premises used: ExpChar.prime
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
S : Type u_2
inst_1 : Semiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
hp : Nat.Prime p
hchar : CharP R p
hprime : Nat.Prime p
hchar_1 : CharP S p
this : CharP (R × S) p
⊢ ExpChar (R × S) p

Tactic:
exact .prime hp
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : IsLeftCancelAdd α
n : ℕ
inst_2 : CharP α n
a b : ℕ
rw : Eq.{u_2 + 1} (α := α) (↑a : α) (↑b : α) ↔ a % n = b % n
⊢ Eq.{u_2 + 1} (α := α) (OfNat.ofNat a) (OfNat.ofNat b) ↔ a % n = b % n

Tactic:
rw [Lean.Grind.Semiring.ofNat_eq_natCast, Lean.Grind.Semiring.ofNat_eq_natCast]

Premises used: Lean.Grind.Semiring.ofNat_eq_natCast
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : IsLeftCancelAdd α
n : ℕ
inst_2 : CharP α n
a b : ℕ
⊢ Eq.{u_2 + 1} (α := α) (↑a : α) (↑b : α) ↔ a % n = b % n

Tactic:
CharP.cast_eq_iff_mod_eq α n

Premises used: CharP.cast_eq_iff_mod_eq
-- Module: Mathlib.Algebra.CharP.Basic
Goal:
R : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : IsLeftCancelAdd α
n : ℕ
inst_2 : CharP α n
a b : ℕ
⊢ Eq.{u_2 + 1} (α := α) (↑a : α) (↑b : α) ↔ a % n = b % n

Tactic:
exact CharP.cast_eq_iff_mod_eq α n

Premises used: CharP.cast_eq_iff_mod_eq
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
⊢ Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0

Tactic:
have hch := CharP.cast_eq_zero R (ringChar R)
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
⊢ Nat.Prime p

Tactic:
have hp : p.Prime := Fact.out
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
mp : IsUnit.{u_1} (M := R) (↑p : R) → ¬p ∣ ringChar R
mpr : ¬p ∣ ringChar R → IsUnit.{u_1} (M := R) (↑p : R)
⊢ IsUnit.{u_1} (M := R) (↑p : R) ↔ ¬p ∣ ringChar R

Tactic:
constructor
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h₁ : IsUnit.{u_1} (M := R) (↑p : R)
q : ℕ
hq : ringChar R = p * q
mp : ∀ (a : R) (ha : a * (↑p : R) = 1), False
⊢ False

Tactic:
rcases IsUnit.exists_left_inv h₁ with ⟨a, ha⟩

Premises used: IsUnit.exists_left_inv
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h₁ : IsUnit.{u_1} (M := R) (↑p : R)
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * (↑p : R) = 1
r : ℕ
hr : q = ringChar R * r
⊢ ringChar R = ringChar R * (p * r)

Tactic:
rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h₁ : IsUnit.{u_1} (M := R) (↑p : R)
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * (↑p : R) = 1
r : ℕ
hr : q = ringChar R * r
hq₁ : ringChar R = ringChar R * (p * r)
⊢ q = ringChar R * r

Tactic:
rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h₁ : IsUnit.{u_1} (M := R) (↑p : R)
q : ℕ
a : R
ha : a * (↑p : R) = 1
r : ℕ
hq : ringChar R = ringChar R * (p * r)
hr : q = ringChar R * r
⊢ ringChar R * 1 = ringChar R * (p * r)

Tactic:
nth_rw 1 [← mul_one (ringChar R)] at hq

Premises used: ringChar, mul_one
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h₁ : IsUnit.{u_1} (M := R) (↑p : R)
q : ℕ
a : R
ha : a * (↑p : R) = 1
r : ℕ
hq : ringChar R = ringChar R * (p * r)
hr : q = ringChar R * r
hq₁ : ringChar R * 1 = ringChar R * (p * r)
⊢ q = ringChar R * r

Tactic:
nth_rw 1 [← mul_one (ringChar R)] at hq

Premises used: ringChar, mul_one
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h₁ : IsUnit.{u_1} (M := R) (↑p : R)
q : ℕ
a : R
ha : a * (↑p : R) = 1
r : ℕ
hq : ringChar R * 1 = ringChar R * (p * r)
hr : q = ringChar R * r
⊢ False

Tactic:
Nat.Prime.not_dvd_one hp ⟨r, mul_left_cancel₀ hR hq⟩

Premises used: mul_left_cancel₀, Exists.intro, Nat.Prime.not_dvd_one
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h₁ : IsUnit.{u_1} (M := R) (↑p : R)
q : ℕ
a : R
ha : a * (↑p : R) = 1
r : ℕ
hq : ringChar R * 1 = ringChar R * (p * r)
hr : q = ringChar R * r
⊢ False

Tactic:
exact Nat.Prime.not_dvd_one hp ⟨r, mul_left_cancel₀ hR hq⟩

Premises used: mul_left_cancel₀, Exists.intro, Nat.Prime.not_dvd_one
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h₁ : IsUnit.{u_1} (M := R) (↑p : R)
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * (↑p : R) = 1
⊢ ¬ringChar R ∣ q

Tactic:
have h₃ : ¬ringChar R ∣ q := by
      rintro ⟨r, hr⟩
      rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq
      nth_rw 1 [← mul_one (ringChar R)] at hq
      exact Nat.Prime.not_dvd_one hp ⟨r, mul_left_cancel₀ hR hq⟩
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h₁ : IsUnit.{u_1} (M := R) (↑p : R)
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * (↑p : R) = 1
h₃ : ¬ringChar R ∣ q
⊢ Fact True

Tactic:
simp_all only [ne_eq]

Premises used: ne_eq
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst_1 : CommRing R
p : ℕ
inst_2 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h₁ : IsUnit.{u_1} (M := R) (↑p : R)
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * (↑p : R) = 1
h₃ : ¬ringChar R ∣ q
inst : Fact True
⊢ ¬p * q = 0

Tactic:
simp_all only [ne_eq]

Premises used: ne_eq
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst_1 : CommRing R
p : ℕ
inst_2 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h₁ : IsUnit.{u_1} (M := R) (↑p : R)
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * (↑p : R) = 1
h₃ : ¬ringChar R ∣ q
inst : Fact True
hR₁ : ¬p * q = 0
⊢ Eq.{u_1 + 1} (α := R) (↑(p * q) : R) 0

Tactic:
simp_all only [ne_eq]

Premises used: ne_eq
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst_1 : CommRing R
p : ℕ
inst_2 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h₁ : IsUnit.{u_1} (M := R) (↑p : R)
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * (↑p : R) = 1
h₃ : ¬ringChar R ∣ q
inst : Fact True
hR₁ : ¬p * q = 0
hch₁ : Eq.{u_1 + 1} (α := R) (↑(p * q) : R) 0
⊢ Nat.Prime p

Tactic:
simp_all only [ne_eq]

Premises used: ne_eq
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst_1 : CommRing R
p : ℕ
inst_2 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h₁ : IsUnit.{u_1} (M := R) (↑p : R)
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * (↑p : R) = 1
h₃ : ¬ringChar R ∣ q
inst : Fact True
hR₁ : ¬p * q = 0
hch₁ : Eq.{u_1 + 1} (α := R) (↑(p * q) : R) 0
hp₁ : Nat.Prime p
⊢ IsUnit.{u_1} (M := R) (↑p : R)

Tactic:
simp_all only [ne_eq]

Premises used: ne_eq
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst_1 : CommRing R
p : ℕ
inst_2 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h₁ : IsUnit.{u_1} (M := R) (↑p : R)
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * (↑p : R) = 1
h₃ : ¬ringChar R ∣ q
inst : Fact True
hR₁ : ¬p * q = 0
hch₁ : Eq.{u_1 + 1} (α := R) (↑(p * q) : R) 0
hp₁ : Nat.Prime p
h₂ : IsUnit.{u_1} (M := R) (↑p : R)
⊢ ringChar R = p * q

Tactic:
simp_all only [ne_eq]

Premises used: ne_eq
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst_1 : CommRing R
p : ℕ
inst_2 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h₁ : IsUnit.{u_1} (M := R) (↑p : R)
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * (↑p : R) = 1
h₃ : ¬ringChar R ∣ q
inst : Fact True
hR₁ : ¬p * q = 0
hch₁ : Eq.{u_1 + 1} (α := R) (↑(p * q) : R) 0
hp₁ : Nat.Prime p
h₂ : IsUnit.{u_1} (M := R) (↑p : R)
hq₁ : ringChar R = p * q
⊢ a * (↑p : R) = 1

Tactic:
simp_all only [ne_eq]

Premises used: ne_eq
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst_1 : CommRing R
p : ℕ
inst_2 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h₁ : IsUnit.{u_1} (M := R) (↑p : R)
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * (↑p : R) = 1
h₃ : ¬ringChar R ∣ q
inst : Fact True
hR₁ : ¬p * q = 0
hch₁ : Eq.{u_1 + 1} (α := R) (↑(p * q) : R) 0
hp₁ : Nat.Prime p
h₂ : IsUnit.{u_1} (M := R) (↑p : R)
hq₁ : ringChar R = p * q
ha₁ : a * (↑p : R) = 1
⊢ ¬p * q ∣ q

Tactic:
simp_all only [ne_eq]

Premises used: ne_eq
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p q : ℕ
a : R
inst_1 : Fact True
hR : ¬p * q = 0
hch : Eq.{u_1 + 1} (α := R) (↑(p * q) : R) 0
hp : Nat.Prime p
h₁ : IsUnit.{u_1} (M := R) (↑p : R)
hq : ringChar R = p * q
ha : a * (↑p : R) = 1
h₃ : ¬p * q ∣ q
⊢ False

Tactic:
grind [ringChar.dvd]

Premises used: ringChar.dvd
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
mpr : ∀ (a b : ℤ) (hab : a * (↑p : ℤ) + b * (↑(ringChar R) : ℤ) = 1), IsUnit.{u_1} (M := R) (↑p : R)
⊢ IsUnit.{u_1} (M := R) (↑p : R)

Tactic:
rcases (hp.coprime_iff_not_dvd.mpr h).isCoprime with ⟨a, b, hab⟩

Premises used: Iff.mpr, Nat.Prime.coprime_iff_not_dvd, Nat.Coprime.isCoprime
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : a * (↑p : ℤ) + b * (↑(ringChar R) : ℤ) = 1
⊢ Eq.{u_1 + 1} (α := R) (↑(a * (↑p : ℤ) + b * (↑(ringChar R) : ℤ)) : R) (↑1 : R)

Tactic:
apply_fun ((↑) : ℤ → R) at hab

Premises used: Int.cast
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : Eq.{u_1 + 1} (α := R) (↑(a * (↑p : ℤ) + b * (↑(ringChar R) : ℤ)) : R) (↑1 : R)
⊢ HMul.hMul (α := R) (↑a : R) (↑p : R) + HMul.hMul (α := R) (↑b : R) (↑(ringChar R) : R) = 1

Tactic:
push_cast at hab
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : HMul.hMul (α := R) (↑a : R) (↑p : R) + HMul.hMul (α := R) (↑b : R) (↑(ringChar R) : R) = 1
⊢ HMul.hMul (α := R) (↑p : R) (↑a : R) = 1

Tactic:
rw [hch, mul_zero, add_zero, mul_comm] at hab

Premises used: MulZeroClass.mul_zero, mul_comm, add_zero
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : HMul.hMul (α := R) (↑p : R) (↑a : R) = 1
⊢ IsUnit.{u_1} (M := R) (↑p : R)

Tactic:
.of_mul_eq_one a hab

Premises used: Int.cast, IsUnit.of_mul_eq_one
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : HMul.hMul (α := R) (↑p : R) (↑a : R) = 1
⊢ IsUnit.{u_1} (M := R) (↑p : R)

Tactic:
exact .of_mul_eq_one a hab
-- Module: Mathlib.Algebra.CharP.CharAndCard
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite R
⊢ IsUnit.{u_1} (M := R) (↑p : R) ↔ ¬p ∣ ringChar R

Tactic:
isUnit_iff_not_dvd_char_of_ringChar_ne_zero R p <| CharP.char_ne_zero_of_finite R (ringChar R)

Premises used: ringChar, isUnit_iff_not_dvd_char_of_ringChar_ne_zero, CharP.char_ne_zero_of_finite