awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
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 : Eq.{u_1 + 1} (α := R) (↑x : R) 0
H2 : ¬x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯ = 0
rwa :
  ∀
    (H1 :
      Eq.{u_1 + 1} (α := R)
        (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯ +
              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)
    (H2 : ¬x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯ = 0),
    Eq.{u_1 + 1} (α := R) (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R) 0
rwa₁ :
  ∀
    (H1 :
      HAdd.hAdd (α := R) (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : 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)
    (H2 : ¬x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯ = 0),
    Eq.{u_1 + 1} (α := R) (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R) 0
rwa₂ :
  ∀
    (H1 :
      (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R) +
          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)
    (H2 : ¬x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯ = 0),
    Eq.{u_1 + 1} (α := R) (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R) 0
⊢ Eq.{u_1 + 1} (α := R) (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R) 0
have rwa₃ : ∀
  (H1 :
    (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) sorry) : R) +
        HMul.hMul (α := R) 0 (↑(x / Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) sorry) : R) =
      0)
  (H2 : ¬x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) sorry = 0),
  Eq.{u_1 + 1} (α := R) (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) sorry) : R) 0
Tactic: rwa [← Nat.mod_add_div x (Nat.find (not_forall.1 H)), Nat.cast_add,
                      Nat.cast_mul,
                      of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
                      zero_mul, add_zero] at H1
Cleared hypotheses: H1, H2
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (↑x : R) 0
have rw : Eq.{u_1 + 1} (α := R)
  (↑(Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) sorry *
        (x / Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) sorry)) :
    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]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (↑x : R) 0
have rw₁ : HMul.hMul (α := R) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) sorry) : R)
    (↑(x / Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) sorry) : 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]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (↑x : R) 0
have rw₂ : HMul.hMul (α := R) 0 (↑(x / Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) sorry) : 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]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (↑x : R) 0
have rw₃ : Eq.{u_1 + 1} (α := R) 0 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]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
⊢ Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
have rw : ringChar R ∣ ringChar R
Tactic: rw [ringChar.spec]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
⊢ ringChar R = 1 ↔ Subsingleton R
have rw : ringChar R ∣ 1 ↔ Subsingleton R
Tactic: rw [← Nat.dvd_one, ← spec, eq_comm, Nat.cast_one, subsingleton_iff_zero_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
rw : ringChar R ∣ 1 ↔ Subsingleton R
⊢ ringChar R = 1 ↔ Subsingleton R
have rw₁ : Eq.{u_1 + 1} (α := R) (↑1 : R) 0 ↔ Subsingleton R
Tactic: rw [← Nat.dvd_one, ← spec, eq_comm, Nat.cast_one, subsingleton_iff_zero_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
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
⊢ ringChar R = 1 ↔ Subsingleton R
have rw₂ : Eq.{u_1 + 1} (α := R) 0 (↑1 : R) ↔ Subsingleton R
Tactic: rw [← Nat.dvd_one, ← spec, eq_comm, Nat.cast_one, subsingleton_iff_zero_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
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
⊢ ringChar R = 1 ↔ Subsingleton R
have rw₃ : Eq.{u_1 + 1} (α := R) 0 1 ↔ Subsingleton R
Tactic: rw [← Nat.dvd_one, ← spec, eq_comm, Nat.cast_one, subsingleton_iff_zero_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
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
⊢ ringChar R = 1 ↔ Subsingleton R
have rw₄ : Subsingleton R ↔ Subsingleton R
Tactic: rw [← Nat.dvd_one, ← spec, eq_comm, Nat.cast_one, subsingleton_iff_zero_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
inst_2 : Fact (2 < p)
⊢ Ne.{u_1 + 1} (α := R) (-1) 1
have rw : ¬p ∣ 2
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]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
⊢ ringChar R = 0 ↔ CharZero R
have rw : CharP R 0 ↔ CharZero R
Tactic: rw [ringChar.eq_iff, charP_zero_iff_charZero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
rw : CharP R 0 ↔ CharZero R
⊢ ringChar R = 0 ↔ CharZero R
have rw₁ : CharZero R ↔ CharZero R
Tactic: rw [ringChar.eq_iff, charP_zero_iff_charZero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
⊢ CharZero R ∨ ∃ (p : ℕ), Fact (Nat.Prime p) ∧ CharP R p
have obtain : ∀ (p : ℕ) (hchar : CharP R p), CharZero R ∨ ∃ (p : ℕ), Fact (Nat.Prime p) ∧ CharP R p
Tactic: obtain ⟨p, hchar⟩ := CharP.exists R
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
p : ℕ
hchar : CharP R p
⊢ CharZero R ∨ ∃ (p : ℕ), Fact (Nat.Prime p) ∧ CharP R p
have inl : ∀ (h : Nat.Prime p), CharZero R ∨ ∃ (p : ℕ), Fact (Nat.Prime p) ∧ CharP R p
Tactic: rcases char_is_prime_or_zero R p with h | rfl
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
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
⊢ CharZero R ∨ ∃ (p : ℕ), Fact (Nat.Prime p) ∧ CharP R p
have inr : ∀ (hchar : CharP R 0), CharZero R ∨ ∃ (p : ℕ), Fact (Nat.Prime p) ∧ CharP R p
Tactic: rcases char_is_prime_or_zero R p with h | rfl
Cleared hypotheses: p, hchar
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharP R 1
r : R
⊢ r = 1 * r
have rw : r = r
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharP R 1
r : R
⊢ 1 * r = (↑1 : R) * r
have rw : 1 * r = 1 * r
Tactic: rw [Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharP R 1
r : R
⊢ (↑1 : R) * r = 0 * r
have rw : 0 * r = 0 * r
Tactic: rw [CharP.cast_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharP R 1
r : R
⊢ 0 * r = 0
have rw : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharP R 1
this : ∀ (r : R), r = 0
a b : R
⊢ a = b
have rw : 0 = b
Tactic: rw [this a, this b]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharP R 1
this : ∀ (r : R), r = 0
a b : R
rw : 0 = b
⊢ a = b
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [this a, this b]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (hypothesis)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
inst_2 : CharP R 1
⊢ False
have this : Subsingleton R
Tactic: have : Subsingleton R := CharOne.subsingleton
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
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
⊢ v = 1
have rwa : ∀ (h : v ∣ 1), v = 1
Tactic: rwa [CharP.cast_eq_zero_iff _ v, Nat.dvd_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
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
⊢ v = 1
have rwa₁ : ∀ (h : v = 1), v = 1
Tactic: rwa [CharP.cast_eq_zero_iff _ v, Nat.dvd_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
k : ℕ
h : NeZero.{u_1} (R := R) (↑k : R)
⊢ ¬p ∣ k
have rwa : ¬Eq.{u_1 + 1} (α := R) (↑k : R) 0
Tactic: rwa [← CharP.cast_eq_zero_iff R p k, ← Ne, ← neZero_iff]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
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
⊢ ¬p ∣ k
have rwa₁ : Ne.{u_1 + 1} (α := R) (↑k : R) 0
Tactic: rwa [← CharP.cast_eq_zero_iff R p k, ← Ne, ← neZero_iff]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
hR : ExpChar R p
⊢ p ≠ 0
have zero : ∀ [CharZero R], Ne (α := ℕ) 1 0
Tactic: cases hR
Cleared hypotheses: p, hR
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
hR : ExpChar R p
zero : ∀ [CharZero R], Ne (α := ℕ) 1 0
⊢ p ≠ 0
have prime : Nat.Prime p → ∀ [CharP R p], p ≠ 0
Tactic: cases hR
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p q : ℕ
hp : ExpChar R p
hq : ExpChar R q
⊢ p = q
have zero : ∀ [CharZero R], 1 = q
Tactic: rcases hp with ⟨hp⟩ | ⟨hp'⟩
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p q : ℕ
hp : ExpChar R p
hq : ExpChar R q
zero : ∀ [CharZero R], 1 = q
⊢ p = q
have prime : ∀ (hp' : Nat.Prime p) [CharP R p], p = q
Tactic: rcases hp with ⟨hp⟩ | ⟨hp'⟩
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
hq : ExpChar R q
inst_1 : CharZero R
⊢ 1 = q
have zero : ∀ [CharZero R], Eq (α := ℕ) 1 1
Tactic: rcases hq with hq | hq'
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
hq : ExpChar R q
inst_1 : CharZero R
zero : ∀ [CharZero R], Eq (α := ℕ) 1 1
⊢ 1 = q
have zero₁ : ∀ (hq' : Nat.Prime q) [CharP R q], 1 = q
Tactic: rcases hq with hq | hq'
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p q : ℕ
hq : ExpChar R q
hp' : Nat.Prime p
hchar : CharP R p
⊢ p = q
have prime : ∀ [CharZero R], p = 1
Tactic: rcases hq with hq | hq'
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
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
⊢ p = q
have prime₁ : ∀ (hq' : Nat.Prime q) [CharP R q], p = q
Tactic: rcases hq with hq | hq'
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
hp : CharP R 0
hq : ExpChar R q
⊢ q = 1
have zero : ∀ [CharZero R], Eq (α := ℕ) 1 1
Tactic: rcases hq with q | hq_prime
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
hp : CharP R 0
hq : ExpChar R q
zero : ∀ [CharZero R], Eq (α := ℕ) 1 1
⊢ q = 1
have prime : ∀ (hq_prime : Nat.Prime q) [CharP R q], q = 1
Tactic: rcases hq with q | hq_prime
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p q : ℕ
hp : CharP R p
hq : ExpChar R q
⊢ p = q ↔ Nat.Prime p
have zero : ∀ [CharZero R], p = 1 ↔ Nat.Prime p
Tactic: rcases hq with q | hq_prime
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
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
⊢ p = q ↔ Nat.Prime p
have prime : ∀ (hq_prime : Nat.Prime q) [CharP R q], p = q ↔ Nat.Prime p
Tactic: rcases hq with q | hq_prime
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
hp : CharP R p
inst_1 : CharZero R
⊢ p = 1 ↔ Nat.Prime p
have zero : Eq (α := ℕ) 0 1 ↔ Nat.Prime 0
Tactic: rw [(CharP.eq R hp (.ofCharZero R) : p = 0)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
hq : ExpChar R q
⊢ Nat.Prime q ∨ q = 1
have zero : ∀ [CharZero R], Nat.Prime 1 ∨ Eq (α := ℕ) 1 1
Tactic: cases hq with
  | zero => exact .inr rfl
  | prime hp => exact .inl hp
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
hq : ExpChar R q
zero : ∀ [CharZero R], Nat.Prime 1 ∨ Eq (α := ℕ) 1 1
⊢ Nat.Prime q ∨ q = 1
have prime : ∀ (hp : Nat.Prime q) [CharP R q], Nat.Prime q ∨ q = 1
Tactic: cases hq with
  | zero => exact .inr rfl
  | prime hp => exact .inl hp
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
inst_1 : ExpChar R q
⊢ 0 < q
have inl : ∀ (h : Nat.Prime q), 0 < q
Tactic: rcases expChar_is_prime_or_one R q with h | rfl
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
q : ℕ
inst_1 : ExpChar R q
inl : ∀ (h : Nat.Prime q), 0 < q
⊢ 0 < q
have inr : ∀ [ExpChar R 1], LT.lt (α := ℕ) 0 1
Tactic: rcases expChar_is_prime_or_one R q with h | rfl
Cleared hypotheses: q, inst_1
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
q : ℕ
h : ExpChar R q
⊢ ringExpChar R = q
have zero : ∀ [CharZero R], ringExpChar R = 1
Tactic: rcases h with _ | h
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
q : ℕ
h : ExpChar R q
zero : ∀ [CharZero R], ringExpChar R = 1
⊢ ringExpChar R = q
have prime : ∀ (h : Nat.Prime q) [CharP R q], ringExpChar R = q
Tactic: rcases h with _ | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (hypothesis)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharZero R
⊢ ringExpChar R = 1
have this : CharP R 0
Tactic: haveI := CharP.ofCharZero R
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharZero R
this : CharP R 0
⊢ ringExpChar R = 1
have zero : Eq (α := ℕ) (max 0 1) 1
Tactic: rw [ringExpChar, ringChar.eq R 0]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
q : ℕ
h : Nat.Prime q
hchar : CharP R q
⊢ ringExpChar R = q
have prime : max q 1 = q
Tactic: rw [ringExpChar, ringChar.eq R q]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharZero R
⊢ ringExpChar R = 1
have rw : max (ringChar R) 1 = 1
Tactic: rw [ringExpChar, ringChar.eq_zero, max_eq_right (Nat.zero_le _)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharZero R
rw : max (ringChar R) 1 = 1
⊢ ringExpChar R = 1
have rw₁ : Eq (α := ℕ) (max 0 1) 1
Tactic: rw [ringExpChar, ringChar.eq_zero, max_eq_right (Nat.zero_le _)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : CharZero R
rw : max (ringChar R) 1 = 1
rw₁ : Eq (α := ℕ) (max 0 1) 1
⊢ ringExpChar R = 1
have rw₂ : Eq (α := ℕ) 1 1
Tactic: rw [ringExpChar, ringChar.eq_zero, max_eq_right (Nat.zero_le _)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
p : ℕ
hp : CharP R p
hq : ExpChar R 1
⊢ p = 0
have zero : ∀ [CharZero R], p = 0
Tactic: cases hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
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
⊢ p = 0
have prime : Nat.Prime 1 → ∀ [CharP R 1], p = 0
Tactic: cases hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
hq : ExpChar R 1
⊢ CharZero R
have zero : ∀ [CharZero R], CharZero R
Tactic: cases hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
hq : ExpChar R 1
zero : ∀ [CharZero R], CharZero R
⊢ CharZero R
have prime : Nat.Prime 1 → ∀ [CharP R 1], CharZero R
Tactic: cases hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
p q : ℕ
inst_2 : CharP R p
inst_3 : ExpChar R q
⊢ q = 1 ↔ p = 0
have mp : q = 1 → p = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
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
⊢ q = 1 ↔ p = 0
have mpr : p = 0 → q = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
⊢ ∃ (q : ℕ), ExpChar R q
have inl : CharZero R → ∃ (q : ℕ), ExpChar R q
Tactic: obtain _ | ⟨p, ⟨hp⟩, _⟩ := CharP.exists' R
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
inl : CharZero R → ∃ (q : ℕ), ExpChar R q
⊢ ∃ (q : ℕ), ExpChar R q
have inr : ∀ (p : ℕ), CharP R p → ∀ (hp : Nat.Prime p), ∃ (q : ℕ), ExpChar R q
Tactic: obtain _ | ⟨p, ⟨hp⟩, _⟩ := CharP.exists' R
-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
⊢ ExpChar R (ringExpChar R)
have obtain : ∀ (q : ℕ), ExpChar R q → ExpChar R (ringExpChar R)
Tactic: obtain ⟨q, _⟩ := ExpChar.exists R
-- Lean 4 proof step from Mathlib.Algebra.CharP.Frobenius (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p n : ℕ
inst_1 : ExpChar R p
⊢ iterateFrobenius R p n = HPow.hPow (α := R →+* R) (frobenius R p) n
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.CharP.Frobenius (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
x : R
⊢ (iterateFrobenius R p 1 : (a : R) → R) x = x ^ p
have rw : x ^ HPow.hPow (β := ℕ) p 1 = x ^ p
Tactic: rw [iterateFrobenius_def, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Frobenius (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
x : R
rw : x ^ HPow.hPow (β := ℕ) p 1 = x ^ p
⊢ (iterateFrobenius R p 1 : (a : R) → R) x = x ^ p
have rw₁ : x ^ p = x ^ p
Tactic: rw [iterateFrobenius_def, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Frobenius (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
x : R
⊢ (iterateFrobenius R p 0 : (a : R) → R) x = x
have rw : x ^ HPow.hPow (β := ℕ) p 0 = x
Tactic: rw [iterateFrobenius_def, pow_zero, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Frobenius (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
x : R
rw : x ^ HPow.hPow (β := ℕ) p 0 = x
⊢ (iterateFrobenius R p 0 : (a : R) → R) x = x
have rw₁ : HPow.hPow (β := ℕ) x 1 = x
Tactic: rw [iterateFrobenius_def, pow_zero, pow_one]