awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
p : ℕ
inst_3 : CharP R p
hp : p ≠ 0
⊢ Nat.Prime p

Tactic:
(CharP.char_is_prime_or_zero R p).resolve_right hp

Premises used: CharP.char_is_prime_or_zero, Or.resolve_right
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
obtain : ∀ (p : ℕ) (hchar : CharP R p), CharZero R ∨ ∃ (p : ℕ), Fact (Nat.Prime p) ∧ CharP R p
⊢ CharZero R ∨ ∃ (p : ℕ), Fact (Nat.Prime p) ∧ CharP R p

Tactic:
obtain ⟨p, hchar⟩ := CharP.exists R

Premises used: CharP.exists
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
p : ℕ
hchar : CharP R p
inl : ∀ (h : Nat.Prime p), CharZero R ∨ ∃ (p : ℕ), Fact (Nat.Prime p) ∧ CharP R p
inr : ∀ (hchar : CharP R 0), CharZero R ∨ ∃ (p : ℕ), Fact (Nat.Prime p) ∧ CharP R p
⊢ CharZero R ∨ ∃ (p : ℕ), Fact (Nat.Prime p) ∧ CharP R p

Tactic:
rcases char_is_prime_or_zero R p with h | rfl

Premises used: CharP.char_is_prime_or_zero, rfl
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
p : ℕ
hchar : CharP R p
h : Nat.Prime p
⊢ CharZero R ∨ ∃ (p : ℕ), Fact (Nat.Prime p) ∧ CharP R p

Tactic:
Or.inr ⟨p, Fact.mk h, hchar⟩

Premises used: Fact.mk, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
hchar : CharP R 0
⊢ CharZero R ∨ ∃ (p : ℕ), Fact (Nat.Prime p) ∧ CharP R p

Tactic:
Or.inl (charP_to_charZero R)

Premises used: CharP.charP_to_charZero, Or.inl
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
p : ℕ
hchar : CharP R p
h : Nat.Prime p
⊢ CharZero R ∨ ∃ (p : ℕ), Fact (Nat.Prime p) ∧ CharP R p

Tactic:
exacts [Or.inr ⟨p, Fact.mk h, hchar⟩, Or.inl (charP_to_charZero R)]

Premises used: Or.inr
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
p : ℕ
inst_3 : NeZero p
inst_4 : CharP R p
⊢ Fact (Nat.Prime p)

Tactic:
⟨(CharP.char_is_prime_or_zero R _).resolve_right <| NeZero.ne p⟩

Premises used: CharP.char_is_prime_or_zero, Fact.mk, Or.resolve_right, NeZero.ne
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharP R 1
r : R
rw rw₁ : r = r
⊢ r = 1 * r

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharP R 1
r : R
rw rw₁ : 1 * r = 1 * r
⊢ 1 * r = (↑1 : R) * r

Tactic:
rw [Nat.cast_one]

Premises used: Nat.cast_one
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharP R 1
r : R
rw rw₁ : 0 * r = 0 * r
⊢ (↑1 : R) * r = 0 * r

Tactic:
rw [CharP.cast_eq_zero]

Premises used: CharP.cast_eq_zero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharP R 1
r : R
rw rw₁ : Eq.{u_1 + 1} (α := R) 0 0
⊢ 0 * r = 0

Tactic:
rw [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharP R 1
this : ∀ (r : R), r = 0
a b : R
rw : 0 = b
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ a = b

Tactic:
rw [this a, this b]
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
inst_2 : CharP R 1
⊢ Subsingleton R

Tactic:
have : Subsingleton R := CharOne.subsingleton
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
inst_2 : CharP R 1
this : Subsingleton R
⊢ False

Tactic:
false_of_nontrivial_of_subsingleton R

Premises used: false_of_nontrivial_of_subsingleton
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
inst_2 : CharP R 1
this : Subsingleton R
⊢ False

Tactic:
exact false_of_nontrivial_of_subsingleton R

Premises used: false_of_nontrivial_of_subsingleton
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
⊢ ringChar R ≠ 1

Tactic:
simpa using not_subsingleton R

Premises used: not_subsingleton
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
v : ℕ
hv : v ≠ 1
hr : CharP R v
h : Eq.{u_1 + 1} (α := R) (↑1 : R) 0
rwa : ∀ (h : v ∣ 1), v = 1
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : v = 1), v = 1
⊢ v = 1

Tactic:
rwa [CharP.cast_eq_zero_iff _ v, Nat.dvd_one] at h

Premises used: Nat.dvd_one, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
n p : ℕ
inst_1 : CharP R p
h : ¬p ∣ n
⊢ NeZero.{u_1} (R := R) (↑n : R)

Tactic:
⟨(CharP.cast_eq_zero_iff R p n).not.mpr h⟩

Premises used: Iff.mpr, NeZero.mk, Iff.not, 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 : ℕ
h : NeZero.{u_1} (R := R) (↑k : R)
rwa : ¬Eq.{u_1 + 1} (α := R) (↑k : R) 0
rwa₁ : Ne.{u_1 + 1} (α := R) (↑k : R) 0
rwa₂ rwa₃ rwa₄ rwa₅ : NeZero.{u_1} (R := R) (↑k : R)
⊢ ¬p ∣ k

Tactic:
rwa [← CharP.cast_eq_zero_iff R p k, ← Ne, ← neZero_iff]

Premises used: Ne, CharP.cast_eq_zero_iff, neZero_iff
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
inst_2 : Fact (Nat.Prime p)
⊢ ExpChar R p

Tactic:
ExpChar.prime Fact.out

Premises used: ExpChar.prime, Fact.out
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
⊢ ExpChar R 1

Tactic:
ExpChar.zero

Premises used: ExpChar.zero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
hR : ExpChar R p
zero : ∀ [CharZero R], Ne (α := ℕ) 1 0
prime : Nat.Prime p → ∀ [CharP R p], p ≠ 0
⊢ p ≠ 0

Tactic:
cases hR
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
⊢ Ne (α := ℕ) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
⊢ Ne (α := ℕ) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
hprime : Nat.Prime p
hchar : CharP R p
⊢ p ≠ 0

Tactic:
‹p.Prime›.ne_zero

Premises used: Nat.Prime.ne_zero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
hprime : Nat.Prime p
hchar : CharP R p
⊢ p ≠ 0

Tactic:
exact ‹p.Prime›.ne_zero

Premises used: Nat.Prime.ne_zero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p q : ℕ
hp : ExpChar R p
hq : ExpChar R q
zero : ∀ [CharZero R], 1 = q
prime : ∀ (hp' : Nat.Prime p) [CharP R p], p = q
⊢ p = q

Tactic:
rcases hp with ⟨hp⟩ | ⟨hp'⟩
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
hq : ExpChar R q
inst_1 : CharZero R
zero : ∀ [CharZero R], Eq (α := ℕ) 1 1
zero₁ : ∀ (hq' : Nat.Prime q) [CharP R q], 1 = q
⊢ 1 = q

Tactic:
rcases hq with hq | hq'
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 inst_2 : CharZero R
⊢ Eq (α := ℕ) 1 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
inst_1 : CharZero R
hq' : Nat.Prime q
hchar : CharP R q
⊢ 1 = q

Tactic:
False.elim (Nat.not_prime_zero (CharP.eq R ‹_› (CharP.ofCharZero R) ▸ hq'))

Premises used: False.elim, Eq.rec, Nat.not_prime_zero, CharP.eq, CharP.ofCharZero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 inst_2 : CharZero R
⊢ Eq (α := ℕ) 1 1

Tactic:
exacts [rfl, False.elim (Nat.not_prime_zero (CharP.eq R ‹_› (CharP.ofCharZero R) ▸ hq'))]

Premises used: rfl
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p q : ℕ
hq : ExpChar R q
hp' : Nat.Prime p
hchar : CharP R p
prime : ∀ [CharZero R], p = 1
prime₁ : ∀ (hq' : Nat.Prime q) [CharP R q], p = q
⊢ p = q

Tactic:
rcases hq with hq | hq'
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
hp' : Nat.Prime p
hchar : CharP R p
inst_1 : CharZero R
⊢ p = 1

Tactic:
False.elim (Nat.not_prime_zero (CharP.eq R ‹_› (CharP.ofCharZero R) ▸ hp'))

Premises used: False.elim, Eq.rec, Nat.not_prime_zero, CharP.eq, CharP.ofCharZero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p q : ℕ
hp' : Nat.Prime p
hchar : CharP R p
hq' : Nat.Prime q
hchar_1 : CharP R q
⊢ p = q

Tactic:
CharP.eq R ‹_› ‹_›

Premises used: CharP.eq
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
hp' : Nat.Prime p
hchar : CharP R p
inst_1 : CharZero R
⊢ p = 1

Tactic:
exacts [False.elim (Nat.not_prime_zero (CharP.eq R ‹_› (CharP.ofCharZero R) ▸ hp')),
      CharP.eq R ‹_› ‹_›]

Premises used: False.elim, Eq.rec, Nat.not_prime_zero, CharP.eq, CharP.ofCharZero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p q : ℕ
hq : ExpChar R q
h : q = p
⊢ ExpChar R p

Tactic:
h ▸ hq

Premises used: Eq.rec
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
hp : CharP R 0
hq : ExpChar R q
zero : ∀ [CharZero R], Eq (α := ℕ) 1 1
prime : ∀ (hq_prime : Nat.Prime q) [CharP R q], q = 1
⊢ q = 1

Tactic:
rcases hq with q | hq_prime
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
hp : CharP R 0
inst_1 : CharZero R
⊢ Eq (α := ℕ) 1 1

Tactic:
rfl
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
hp : CharP R 0
hq_prime : Nat.Prime q
hchar : CharP R q
⊢ q = 1

Tactic:
False.elim <| hq_prime.ne_zero <| ‹CharP R q›.eq R hp

Premises used: False.elim, CharP.eq, Nat.Prime.ne_zero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
hp : CharP R 0
hq_prime : Nat.Prime q
hchar : CharP R q
⊢ q = 1

Tactic:
exact False.elim <| hq_prime.ne_zero <| ‹CharP R q›.eq R hp

Premises used: False.elim, CharP.eq, Nat.Prime.ne_zero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p q : ℕ
hp : CharP R p
hq : ExpChar R q
zero : ∀ [CharZero R], p = 1 ↔ Nat.Prime p
prime : ∀ (hq_prime : Nat.Prime q) [CharP R q], p = q ↔ Nat.Prime p
⊢ p = q ↔ Nat.Prime p

Tactic:
rcases hq with q | hq_prime
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
hp : CharP R p
inst_1 : CharZero R
zero : Eq (α := ℕ) 0 1 ↔ Nat.Prime 0
⊢ p = 1 ↔ Nat.Prime p

Tactic:
rw [(CharP.eq R hp (.ofCharZero R) : p = 0)]

Premises used: CharP.eq, CharP.ofCharZero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
hp : CharP R p
inst_1 : CharZero R
⊢ Eq (α := ℕ) 0 1 ↔ Nat.Prime 0

Tactic:
decide
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p q : ℕ
hp : CharP R p
hq_prime : Nat.Prime q
hchar : CharP R q
⊢ p = q ↔ Nat.Prime p

Tactic:
⟨fun hpq => hpq.symm ▸ hq_prime, fun _ => CharP.eq R hp ‹CharP R q›⟩

Premises used: Eq.rec, CharP.eq, Iff.intro, Eq.symm
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p q : ℕ
hp : CharP R p
hq_prime : Nat.Prime q
hchar : CharP R q
⊢ p = q ↔ Nat.Prime p

Tactic:
exact ⟨fun hpq => hpq.symm ▸ hq_prime, fun _ => CharP.eq R hp ‹CharP R q›⟩
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
⊢ Nat.Prime 1 ∨ Eq (α := ℕ) 1 1

Tactic:
.inr rfl

Premises used: Or.inr, rfl
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
⊢ Nat.Prime 1 ∨ Eq (α := ℕ) 1 1

Tactic:
exact .inr rfl
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
hp : Nat.Prime q
hchar : CharP R q
⊢ Nat.Prime q ∨ q = 1

Tactic:
.inl hp

Premises used: Or.inl
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
hp : Nat.Prime q
hchar : CharP R q
⊢ Nat.Prime q ∨ q = 1

Tactic:
exact .inl hp
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
hq : ExpChar R q
zero : ∀ [CharZero R], Nat.Prime 1 ∨ Eq (α := ℕ) 1 1
prime : ∀ (hp : Nat.Prime q) [CharP R q], Nat.Prime q ∨ q = 1
⊢ Nat.Prime q ∨ q = 1

Tactic:
cases hq with
  | zero => exact .inr rfl
  | prime hp => exact .inl hp
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
inst_1 : ExpChar R q
inl : ∀ (h : Nat.Prime q), 0 < q
inr : ∀ [ExpChar R 1], LT.lt (α := ℕ) 0 1
⊢ 0 < q

Tactic:
rcases expChar_is_prime_or_one R q with h | rfl

Premises used: expChar_is_prime_or_one, rfl
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
inst_1 : ExpChar R q
h : Nat.Prime q
⊢ 0 < q

Tactic:
Nat.Prime.pos h

Premises used: Nat.Prime.pos
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : ExpChar R 1
⊢ LT.lt (α := ℕ) 0 1

Tactic:
Nat.one_pos

Premises used: Nat.one_pos
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
inst_1 : ExpChar R q
h : Nat.Prime q
⊢ 0 < q

Tactic:
exacts [Nat.Prime.pos h, Nat.one_pos]

Premises used: Nat.one_pos, Nat.Prime.pos
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
inst_1 : ExpChar R q
n : ℕ
⊢ 0 < q ^ n

Tactic:
Nat.pow_pos (expChar_pos R q)

Premises used: expChar_pos, Nat.pow_pos
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
q : ℕ
h : ExpChar R q
zero : ∀ [CharZero R], ringExpChar R = 1
prime : ∀ (h : Nat.Prime q) [CharP R q], ringExpChar R = q
⊢ ringExpChar R = q

Tactic:
rcases h with _ | h
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharZero R
⊢ CharP R 0

Tactic:
haveI := CharP.ofCharZero R
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharZero R
this : CharP R 0
zero : Eq (α := ℕ) (max 0 1) 1
⊢ ringExpChar R = 1

Tactic:
rw [ringExpChar, ringChar.eq R 0]

Premises used: ringChar.eq, ringExpChar, OfNat.ofNat
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharZero R
this : CharP R 0
⊢ Eq (α := ℕ) (max 0 1) 1

Tactic:
rfl
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
q : ℕ
h : Nat.Prime q
hchar : CharP R q
prime : max q 1 = q
⊢ ringExpChar R = q

Tactic:
rw [ringExpChar, ringChar.eq R q]

Premises used: ringChar.eq, ringExpChar
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
q : ℕ
h : Nat.Prime q
hchar : CharP R q
⊢ max q 1 = q

Tactic:
Nat.max_eq_left h.one_lt.le

Premises used: Nat.Prime.one_lt, Nat.max_eq_left, LT.lt.le
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
q : ℕ
h : Nat.Prime q
hchar : CharP R q
⊢ max q 1 = q

Tactic:
exact Nat.max_eq_left h.one_lt.le

Premises used: Nat.Prime.one_lt, Nat.max_eq_left, LT.lt.le
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharZero R
rw : max (ringChar R) 1 = 1
rw₁ : Eq (α := ℕ) (max 0 1) 1
rw₂ rw₃ : Eq (α := ℕ) 1 1
⊢ ringExpChar R = 1

Tactic:
rw [ringExpChar, ringChar.eq_zero, max_eq_right (Nat.zero_le _)]

Premises used: Nat.zero_le, ringExpChar, max_eq_right, ringChar.eq_zero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
p : ℕ
hp : CharP R p
hq : ExpChar R 1
zero : ∀ [CharZero R], p = 0
prime : Nat.Prime 1 → ∀ [CharP R 1], p = 0
⊢ p = 0

Tactic:
cases hq
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
p : ℕ
hp : CharP R p
inst_2 : CharZero R
⊢ p = 0

Tactic:
CharP.eq R hp (.ofCharZero R)

Premises used: CharP.eq, CharP.ofCharZero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
p : ℕ
hp : CharP R p
inst_2 : CharZero R
⊢ p = 0

Tactic:
exact CharP.eq R hp (.ofCharZero R)

Premises used: CharP.eq, CharP.ofCharZero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
p : ℕ
hp : CharP R p
hprime : Nat.Prime 1
hchar : CharP R 1
⊢ p = 0

Tactic:
False.elim (CharP.char_ne_one R 1 rfl)

Premises used: False.elim, OfNat.ofNat, rfl, CharP.char_ne_one
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
p : ℕ
hp : CharP R p
hprime : Nat.Prime 1
hchar : CharP R 1
⊢ p = 0

Tactic:
exact False.elim (CharP.char_ne_one R 1 rfl)

Premises used: False.elim, OfNat.ofNat, rfl, CharP.char_ne_one
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
hq : ExpChar R 1
zero : ∀ [CharZero R], CharZero R
prime : Nat.Prime 1 → ∀ [CharP R 1], CharZero R
⊢ CharZero R

Tactic:
cases hq
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
inst_2 : CharZero R
⊢ CharZero R

Tactic:
assumption
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
hprime : Nat.Prime 1
hchar : CharP R 1
⊢ CharZero R

Tactic:
False.elim (CharP.char_ne_one R 1 rfl)

Premises used: False.elim, OfNat.ofNat, rfl, CharP.char_ne_one
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
hprime : Nat.Prime 1
hchar : CharP R 1
⊢ CharZero R

Tactic:
exact False.elim (CharP.char_ne_one R 1 rfl)

Premises used: False.elim, OfNat.ofNat, rfl, CharP.char_ne_one
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
p q : ℕ
inst_2 : CharP R p
inst_3 : ExpChar R q
mp : q = 1 → p = 0
mpr : p = 0 → q = 1
⊢ q = 1 ↔ p = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
p : ℕ
inst_2 : CharP R p
inst_3 : ExpChar R 1
⊢ p = 0

Tactic:
char_zero_of_expChar_one R p

Premises used: char_zero_of_expChar_one
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
p : ℕ
inst_2 : CharP R p
inst_3 : ExpChar R 1
⊢ p = 0

Tactic:
exact char_zero_of_expChar_one R p

Premises used: char_zero_of_expChar_one
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
q : ℕ
inst_2 : ExpChar R q
inst_3 : CharP R 0
⊢ q = 1

Tactic:
expChar_one_of_char_zero R q

Premises used: expChar_one_of_char_zero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
q : ℕ
inst_2 : ExpChar R q
inst_3 : CharP R 0
⊢ q = 1

Tactic:
exact expChar_one_of_char_zero R q

Premises used: expChar_one_of_char_zero
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
inl : CharZero R → ∃ (q : ℕ), ExpChar R q
inr : ∀ (p : ℕ), CharP R p → ∀ (hp : Nat.Prime p), ∃ (q : ℕ), ExpChar R q
⊢ ∃ (q : ℕ), ExpChar R q

Tactic:
obtain _ | ⟨p, ⟨hp⟩, _⟩ := CharP.exists' R

Premises used: CharP.exists'
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
h : CharZero R
⊢ ∃ (q : ℕ), ExpChar R q

Tactic:
⟨1, .zero⟩

Premises used: ExpChar.zero, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
p : ℕ
right : CharP R p
hp : Nat.Prime p
⊢ ∃ (q : ℕ), ExpChar R q

Tactic:
⟨p, .prime hp⟩

Premises used: ExpChar.prime, Exists.intro
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
h : CharZero R
⊢ ∃ (q : ℕ), ExpChar R q

Tactic:
exacts [⟨1, .zero⟩, ⟨p, .prime hp⟩]
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
⊢ ∃! q : ℕ, ExpChar R q

Tactic:
let ⟨q, H⟩ := ExpChar.exists R
  ⟨q, H, fun _ H2 ↦ ExpChar.eq H2 H⟩

Premises used: _private.0.ExpChar.exists_unique.match_1, ExpChar, ExistsUnique, And.intro, Exists.intro, ExpChar.exists, ExpChar.eq
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
obtain : ∀ (q : ℕ), ExpChar R q → ExpChar R (ringExpChar R)
⊢ ExpChar R (ringExpChar R)

Tactic:
obtain ⟨q, _⟩ := ExpChar.exists R

Premises used: ExpChar.exists
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
q : ℕ
h rwa rwa₁ rwa₂ rwa₃ : ExpChar R q
⊢ ExpChar R (ringExpChar R)

Tactic:
rwa [ringExpChar.eq R q]

Premises used: ringExpChar.eq
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
q : ℕ
h : ringExpChar R = q
⊢ ExpChar R q

Tactic:
h ▸ ringExpChar.expChar R

Premises used: Eq.rec, ringExpChar.expChar
-- Module: Mathlib.Algebra.CharP.Defs
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
q : ℕ
⊢ ringExpChar R = q ↔ ExpChar R q

Tactic:
⟨ringExpChar.of_eq, fun _ ↦ ringExpChar.eq R q⟩

Premises used: ringExpChar.eq, ringExpChar.of_eq, Iff.intro
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
x : R
⊢ (frobenius R p : (a : R) → R) x = x ^ p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
p n : ℕ
inst_1 : ExpChar R p
x : R
⊢ (iterateFrobenius R p n : (a : R) → R) x = x ^ p ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
p n : ℕ
inst_1 : ExpChar R p
x : R
⊢ (⇑(frobenius R p) : (a : R) → R)^[n] x = x ^ p ^ n

Tactic:
congr_fun (pow_iterate p n) x

Premises used: pow_iterate, congr_fun
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
p n : ℕ
inst_1 : ExpChar R p
a :
  ∀ (x : R),
    Eq (α := R) ((iterateFrobenius R p n : (a : R) → R) x : R)
      ((HPow.hPow (α := R →+* R) (frobenius R p) n : (a : R) → R) x : R)
⊢ iterateFrobenius R p n = HPow.hPow (α := R →+* R) (frobenius R p) n

Tactic:
ext
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
p n : ℕ
inst_1 : ExpChar R p
x : R
⊢ Eq (α := R) ((iterateFrobenius R p n : (a : R) → R) x : R)
    ((HPow.hPow (α := R →+* R) (frobenius R p) n : (a : R) → R) x : R)

Tactic:
simp [iterateFrobenius_def, iterate_frobenius]

Premises used: iterateFrobenius_def, iterate_frobenius
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
p n : ℕ
inst_1 : ExpChar R p
⊢ Eq (α := (a : R) → R) (⇑(iterateFrobenius R p n) : (a : R) → R) (⇑(frobenius R p) : (a : R) → R)^[n]

Tactic:
(pow_iterate p n).symm

Premises used: pow_iterate, Eq.symm
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
x : R
rw : x ^ HPow.hPow (β := ℕ) p 1 = x ^ p
rw₁ rw₂ : x ^ p = x ^ p
⊢ (iterateFrobenius R p 1 : (a : R) → R) x = x ^ p

Tactic:
rw [iterateFrobenius_def, pow_one]

Premises used: iterateFrobenius_def, pow_one
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
⊢ Eq (α := R →+* R) (iterateFrobenius R p 1) (frobenius R p)

Tactic:
RingHom.ext (iterateFrobenius_one_apply R p)

Premises used: iterateFrobenius_one_apply, RingHom.ext
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
x : R
rw : x ^ HPow.hPow (β := ℕ) p 0 = x
rw₁ : HPow.hPow (β := ℕ) x 1 = x
rw₂ rw₃ : x = x
⊢ (iterateFrobenius R p 0 : (a : R) → R) x = x

Tactic:
rw [iterateFrobenius_def, pow_zero, pow_one]

Premises used: iterateFrobenius_def, pow_zero, pow_one
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
⊢ Eq (α := R →+* R) (iterateFrobenius R p 0) (RingHom.id R)

Tactic:
RingHom.ext (iterateFrobenius_zero_apply R p)

Premises used: RingHom.ext, iterateFrobenius_zero_apply