awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
have rw : Eq.{u_1 + 1} (α := R) (↑a : R) (↑(b - a + a) : R)
Tactic: rw [← Nat.sub_add_cancel hle, Nat.cast_add, (cast_eq_zero_iff R p _).mpr h, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
have rw₁ : (↑a : R) = HAdd.hAdd (α := R) (↑(b - a) : R) (↑a : R)
Tactic: rw [← Nat.sub_add_cancel hle, Nat.cast_add, (cast_eq_zero_iff R p _).mpr h, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
have rw₂ : (↑a : R) = HAdd.hAdd (α := R) 0 (↑a : R)
Tactic: rw [← Nat.sub_add_cancel hle, Nat.cast_add, (cast_eq_zero_iff R p _).mpr h, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)
have rw₃ : Eq.{u_1 + 1} (α := R) (↑a : R) (↑a : R)
Tactic: rw [← Nat.sub_add_cancel hle, Nat.cast_add, (cast_eq_zero_iff R p _).mpr h, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
p : ℕ
inst_1 : CharP R p
a b : ℕ
inst_2 : IsRightCancelAdd R
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]
have 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]
Tactic: wlog hle : a ≤ b
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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]
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]
have 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]
Tactic: wlog hle : a ≤ b
Cleared hypotheses: inst_1, inst_2
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]
have inr : Eq.{u_1 + 1} (α := R) (↑b : R) (↑a : R) ↔ a ≡ b [MOD p]
Tactic: rw [eq_comm, this R p (le_of_not_ge hle), Nat.ModEq.comm]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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]
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]
have inr₁ : b ≡ a [MOD p] ↔ a ≡ b [MOD p]
Tactic: rw [eq_comm, this R p (le_of_not_ge hle), Nat.ModEq.comm]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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]
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]
have inr₂ : a ≡ b [MOD p] ↔ a ≡ b [MOD p]
Tactic: rw [eq_comm, this R p (le_of_not_ge hle), Nat.ModEq.comm]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]
have rw : Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ p ∣ b - a
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]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]
have rw₁ : Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ Eq.{u_1 + 1} (α := R) (↑(b - a) : R) 0
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]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]
have rw₂ : Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ HAdd.hAdd (α := R) (↑(b - a) : R) (↑a : R) = HAdd.hAdd (α := R) 0 (↑a : R)
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]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]
have rw₃ : Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ HAdd.hAdd (α := R) (↑(b - a) : R) (↑a : R) = (↑a : R)
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]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]
have rw₄ : Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ Eq.{u_1 + 1} (α := R) (↑(b - a + a) : R) (↑a : R)
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]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]
have rw₅ : Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ Eq.{u_1 + 1} (α := R) (↑b : R) (↑a : R)
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]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [MOD p]
have rw₆ : Eq.{u_1 + 1} (α := R) (↑b : R) (↑a : R) ↔ Eq.{u_1 + 1} (α := R) (↑b : R) (↑a : R)
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]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
Goal:
R : Type u_1
inst : AddGroupWithOne R
p : ℕ
inst_1 : CharP R p
a b : ℤ
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [ZMOD (↑p : ℤ)]
have rw : Eq.{u_1 + 1} (α := R) (↑b : R) (↑a : 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]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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 : ℤ)]
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [ZMOD (↑p : ℤ)]
have rw₁ : HSub.hSub (α := R) (↑b : R) (↑a : R) = 0 ↔ 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]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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 : ℤ)]
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [ZMOD (↑p : ℤ)]
have rw₂ : Eq.{u_1 + 1} (α := R) (↑(b - a) : R) 0 ↔ 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]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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 : ℤ)]
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [ZMOD (↑p : ℤ)]
have rw₃ : (↑p : ℤ) ∣ b - a ↔ 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]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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 : ℤ)]
⊢ Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R) ↔ a ≡ b [ZMOD (↑p : ℤ)]
have rw₄ : (↑p : ℤ) ∣ b - a ↔ (↑p : ℤ) ∣ b - a
Tactic: rw [eq_comm, ← sub_eq_zero, ← Int.cast_sub, CharP.intCast_eq_zero_iff R p, Int.modEq_iff_dvd]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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)
⊢ a = b
have lift : ∀ (a : ℕ) (ha : LT.lt (α := ℤ) (↑a : ℤ) (↑p : ℤ)) (hab : Eq.{u_1 + 1} (α := R) (↑(↑a : ℤ) : R) (↑b : R)), (↑a : ℤ) = b
Tactic: lift a to ℕ using ha₀
Cleared hypotheses: a, ha₀, ha, hab
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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)
⊢ (↑a : ℤ) = b
have lift : ∀ (b : ℕ) (hb : LT.lt (α := ℤ) (↑b : ℤ) (↑p : ℤ)) (hab : Eq.{u_1 + 1} (α := R) (↑(↑a : ℤ) : R) (↑(↑b : ℤ) : R)),
  Eq (α := ℤ) (↑a : ℤ) (↑b : ℤ)
Tactic: lift b to ℕ using hb₀
Cleared hypotheses: b, hb₀, hb, hab
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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)
⊢ Eq (α := ℤ) (↑a : ℤ) (↑b : ℤ)
have norm_cast : ∀ (ha : a < p) (hb : b < p) (hab : Eq.{u_1 + 1} (α := R) (↑a : R) (↑b : R)), a = b
Tactic: norm_cast at *
Cleared hypotheses: ha, hb, hab
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (hypothesis)
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
⊢ False
have h₁ : p ∣ q
Tactic: rw [cast_eq_zero_iff R p q] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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
⊢ False
have inl : ∀ [CharP R 1] (hneq : 1 ≠ q) (h : 1 ∣ q), False
Tactic: rcases hq.eq_one_or_self_of_dvd _ h with rfl | h
Cleared hypotheses: p, inst_2, hneq, h
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
⊢ Eq.{u_2 + 1} (α := R) 2 (↑2 : R)
have norm_cast : Eq.{u_2 + 1} (α := R) 2 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Nontrivial R
hR : ringChar R ≠ 2
⊢ Ne.{u_2 + 1} (α := R) 2 0
have rw : ¬(ringChar R = 1 ∨ ringChar R = 2)
Tactic: rw [Ne, (by norm_cast : (2 : R) = (2 : ℕ)), ringChar.spec, Nat.dvd_prime Nat.prime_two]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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
have h : p = p.lcm p
Tactic: convert! Nat.lcm.charP R S p p
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (hypothesis)
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)
have h₁ : 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 ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (hypothesis)
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
have h₁ : 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 ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
⊢ CharZero R ↔ ∀ (p : ℕ), Nat.Prime p → Ne.{u_1 + 1} (α := R) (↑p : R) 0
have refine : ∀ (h : ∀ (p : ℕ), Nat.Prime p → Ne.{u_1 + 1} (α := R) (↑p : R) 0), CharZero R
Tactic: refine ⟨fun h p hp => by simp [hp.ne_zero], fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (hypothesis)
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
⊢ CharZero R
have this : CharP R 0
Tactic: have : CharP R 0 := h ▸ inferInstance
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (hypothesis)
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
⊢ CharZero R
have x : 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
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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
⊢ ExpChar (R × S) p
have zero : ∀ [CharZero R] [ExpChar R 1] [ExpChar S 1], ExpChar (R × S) 1
Tactic: obtain hp | ⟨hp⟩ := ‹ExpChar R p›
Cleared hypotheses: p, inst_2, inst_3
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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
⊢ ExpChar (R × S) p
have prime : ∀ (hp : Nat.Prime p) [CharP R p], ExpChar (R × S) p
Tactic: obtain hp | ⟨hp⟩ := ‹ExpChar R p›
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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
⊢ ExpChar (R × S) p
have prime : ∀ [CharZero S] [ExpChar R 1] [ExpChar S 1] (hp : Nat.Prime 1) [CharP R 1], ExpChar (R × S) 1
Tactic: obtain _ | _ := ‹ExpChar S p›
Cleared hypotheses: p, inst_2, inst_3, hp, hchar
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
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
⊢ ExpChar (R × S) p
have prime₁ : Nat.Prime p → ∀ [CharP S p], ExpChar (R × S) p
Tactic: obtain _ | _ := ‹ExpChar S p›
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (hypothesis)
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
⊢ ExpChar (R × S) p
have this : CharP (R × S) p
Tactic: have := Prod.charP R S p
-- Lean 4 proof step from Mathlib.Algebra.CharP.Basic (goal)
Goal:
R : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : IsLeftCancelAdd α
n : ℕ
inst_2 : CharP α n
a b : ℕ
⊢ Eq.{u_2 + 1} (α := α) (OfNat.ofNat a) (OfNat.ofNat b) ↔ a % n = b % n
have rw : Eq.{u_2 + 1} (α := α) (↑a : α) (↑b : α) ↔ a % n = b % n
Tactic: rw [Lean.Grind.Semiring.ofNat_eq_natCast, Lean.Grind.Semiring.ofNat_eq_natCast]
-- Lean 4 proof step from Mathlib.Algebra.CharP.CharAndCard (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
⊢ IsUnit.{u_1} (M := R) (↑p : R) ↔ ¬p ∣ ringChar R
have hch : Eq.{u_1 + 1} (α := R) (↑(ringChar R) : R) 0
Tactic: have hch := CharP.cast_eq_zero R (ringChar R)
-- Lean 4 proof step from Mathlib.Algebra.CharP.CharAndCard (hypothesis)
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
⊢ IsUnit.{u_1} (M := R) (↑p : R) ↔ ¬p ∣ ringChar R
have hp : Nat.Prime p
Tactic: have hp : p.Prime := Fact.out
-- Lean 4 proof step from Mathlib.Algebra.CharP.CharAndCard (goal)
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
⊢ IsUnit.{u_1} (M := R) (↑p : R) ↔ ¬p ∣ ringChar R
have mp : IsUnit.{u_1} (M := R) (↑p : R) → ¬p ∣ ringChar R
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.CharP.CharAndCard (goal)
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
⊢ IsUnit.{u_1} (M := R) (↑p : R) ↔ ¬p ∣ ringChar R
have mpr : ¬p ∣ ringChar R → IsUnit.{u_1} (M := R) (↑p : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.CharP.CharAndCard (goal)
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
⊢ False
have mp : ∀ (a : R) (ha : a * (↑p : R) = 1), False
Tactic: rcases IsUnit.exists_left_inv h₁ with ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.Algebra.CharP.CharAndCard (hypothesis)
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
⊢ False
have hq₁ : ringChar R = ringChar R * (p * r)
Tactic: rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq
Cleared hypotheses: hq, hr
-- Lean 4 proof step from Mathlib.Algebra.CharP.CharAndCard (hypothesis)
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
⊢ False
have hq₁ : ringChar R * 1 = ringChar R * (p * r)
Tactic: nth_rw 1 [← mul_one (ringChar R)] at hq
Cleared hypotheses: hq, hr
-- Lean 4 proof step from Mathlib.Algebra.CharP.CharAndCard (hypothesis)
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
⊢ False
have h₃ : ¬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⟩