awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℕ
⊢ val (n := 0) (↑a : ZMod 0) = a % 0
have zero : val (n := 0) (↑a : ZMod 0) = a
Tactic: rw [Nat.mod_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n a : ℕ
h : a < n
⊢ val (n := n) (↑a : ZMod n) = a
have rwa : a % n = a
Tactic: rwa [val_natCast, Nat.mod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n a : ℕ
h : a < n
rwa : a % n = a
⊢ val (n := n) (↑a : ZMod n) = a
have rwa₁ : a = a
Tactic: rwa [val_natCast, Nat.mod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ZMod 0
⊢ IsUnit n ↔ Int.natAbs n = 1
have rw : n = 1 ∨ n = -1 ↔ Int.natAbs n = 1
Tactic: rw [Int.isUnit_iff, Int.natAbs_eq_iff, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ZMod 0
rw : n = 1 ∨ n = -1 ↔ Int.natAbs n = 1
⊢ IsUnit n ↔ Int.natAbs n = 1
have rw₁ : n = 1 ∨ n = -1 ↔ n = (↑1 : ℤ) ∨ n = -(↑1 : ℤ)
Tactic: rw [Int.isUnit_iff, Int.natAbs_eq_iff, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ZMod 0
rw : n = 1 ∨ n = -1 ↔ Int.natAbs n = 1
rw₁ : n = 1 ∨ n = -1 ↔ n = (↑1 : ℤ) ∨ n = -(↑1 : ℤ)
⊢ IsUnit n ↔ Int.natAbs n = 1
have rw₂ : n = 1 ∨ n = -1 ↔ n = 1 ∨ n = -1
Tactic: rw [Int.isUnit_iff, Int.natAbs_eq_iff, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
h : IsUnit (M := ZMod 0) (↑n : ZMod 0)
⊢ n = 1
have rw : n % 0 = 1
Tactic: rw [← Nat.mod_zero n, ← val_natCast, val_unit'.mp h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
h : IsUnit (M := ZMod 0) (↑n : ZMod 0)
rw : n % 0 = 1
⊢ n = 1
have rw₁ : val (n := 0) (↑n : ZMod 0) = 1
Tactic: rw [← Nat.mod_zero n, ← val_natCast, val_unit'.mp h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
h : IsUnit (M := ZMod 0) (↑n : ZMod 0)
rw : n % 0 = 1
rw₁ : val (n := 0) (↑n : ZMod 0) = 1
⊢ n = 1
have rw₂ : Eq (α := ℕ) 1 1
Tactic: rw [← Nat.mod_zero n, ← val_natCast, val_unit'.mp h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n k : ℕ
⊢ Eq (α := ZMod n) (↑k : ZMod n) 0 ↔ n ∣ k
have zero : Eq (α := ZMod 0) (↑k : ZMod 0) 0 ↔ 0 ∣ k
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n k : ℕ
zero : Eq (α := ZMod 0) (↑k : ZMod 0) 0 ↔ 0 ∣ k
⊢ Eq (α := ZMod n) (↑k : ZMod n) 0 ↔ n ∣ k
have succ : ∀ (n : ℕ), Eq (α := ZMod (n + 1)) (↑k : ZMod (n + 1)) 0 ↔ n + 1 ∣ k
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a n : ℕ
n0 : n ≠ 0
⊢ addOrderOf (G := ZMod n) (↑a : ZMod n) = n / n.gcd a
have zero : addOrderOf (G := ZMod n) (↑0 : ZMod n) = n / n.gcd 0
Tactic: rcases a with - | a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a n : ℕ
n0 : n ≠ 0
zero : addOrderOf (G := ZMod n) (↑0 : ZMod n) = n / n.gcd 0
⊢ addOrderOf (G := ZMod n) (↑a : ZMod n) = n / n.gcd a
have succ : ∀ (a : ℕ), addOrderOf (G := ZMod n) (↑(a + 1) : ZMod n) = n / n.gcd (a + 1)
Tactic: rcases a with - | a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
n0 : n ≠ 0
a : ℕ
⊢ addOrderOf (G := ZMod n) (↑(a + 1) : ZMod n) = n / n.gcd (a + 1)
have succ : addOrderOf (HSMul.hSMul (β := ZMod n) (a + 1) 1) = n / n.gcd (a + 1)
Tactic: rw [← Nat.smul_one_eq_cast, addOrderOf_nsmul' _ a.succ_ne_zero, ZMod.addOrderOf_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
n0 : n ≠ 0
a : ℕ
succ : addOrderOf (HSMul.hSMul (β := ZMod n) (a + 1) 1) = n / n.gcd (a + 1)
⊢ addOrderOf (G := ZMod n) (↑(a + 1) : ZMod n) = n / n.gcd (a + 1)
have succ₁ : addOrderOf (G := ZMod n) 1 / (addOrderOf (G := ZMod n) 1).gcd a.succ = n / n.gcd (a + 1)
Tactic: rw [← Nat.smul_one_eq_cast, addOrderOf_nsmul' _ a.succ_ne_zero, ZMod.addOrderOf_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
n0 : n ≠ 0
a : ℕ
succ : addOrderOf (HSMul.hSMul (β := ZMod n) (a + 1) 1) = n / n.gcd (a + 1)
succ₁ : addOrderOf (G := ZMod n) 1 / (addOrderOf (G := ZMod n) 1).gcd a.succ = n / n.gcd (a + 1)
⊢ addOrderOf (G := ZMod n) (↑(a + 1) : ZMod n) = n / n.gcd (a + 1)
have succ₂ : n / n.gcd a.succ = n / n.gcd (a + 1)
Tactic: rw [← Nat.smul_one_eq_cast, addOrderOf_nsmul' _ a.succ_ne_zero, ZMod.addOrderOf_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a n : ℕ
a0 : a ≠ 0
⊢ addOrderOf (G := ZMod n) (↑a : ZMod n) = n / n.gcd a
have rw : addOrderOf (HSMul.hSMul (β := ZMod n) a 1) = n / n.gcd a
Tactic: rw [← Nat.smul_one_eq_cast, addOrderOf_nsmul' _ a0, ZMod.addOrderOf_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a n : ℕ
a0 : a ≠ 0
rw : addOrderOf (HSMul.hSMul (β := ZMod n) a 1) = n / n.gcd a
⊢ addOrderOf (G := ZMod n) (↑a : ZMod n) = n / n.gcd a
have rw₁ : addOrderOf (G := ZMod n) 1 / (addOrderOf (G := ZMod n) 1).gcd a = n / n.gcd a
Tactic: rw [← Nat.smul_one_eq_cast, addOrderOf_nsmul' _ a0, ZMod.addOrderOf_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a n : ℕ
a0 : a ≠ 0
rw : addOrderOf (HSMul.hSMul (β := ZMod n) a 1) = n / n.gcd a
rw₁ : addOrderOf (G := ZMod n) 1 / (addOrderOf (G := ZMod n) 1).gcd a = n / n.gcd a
⊢ addOrderOf (G := ZMod n) (↑a : ZMod n) = n / n.gcd a
have rw₂ : n / n.gcd a = n / n.gcd a
Tactic: rw [← Nat.smul_one_eq_cast, addOrderOf_nsmul' _ a0, ZMod.addOrderOf_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
⊢ ringChar (ZMod n) = n
have rw : CharP (ZMod n) n
Tactic: rw [ringChar.eq_iff]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
⊢ HAdd.hAdd (α := ZMod (n + 1)) (↑n : ZMod (n + 1)) 1 = 0
have rw : Eq (α := ZMod (n + 1)) (↑(n + 1) : ZMod (n + 1)) 0
Tactic: rw [← Nat.cast_add_one, natCast_self (n + 1)]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
rw : Eq (α := ZMod (n + 1)) (↑(n + 1) : ZMod (n + 1)) 0
⊢ HAdd.hAdd (α := ZMod (n + 1)) (↑n : ZMod (n + 1)) 1 = 0
have rw₁ : Eq (α := ZMod (n + 1)) 0 0
Tactic: rw [← Nat.cast_add_one, natCast_self (n + 1)]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p m n : ℕ
h : n ≤ m
⊢ HPow.hPow (α := ZMod (p ^ n)) (↑p : ZMod (p ^ n)) m = 0
have obtain : ∀ (q : ℕ) (h : n ≤ n + q), HPow.hPow (α := ZMod (p ^ n)) (↑p : ZMod (p ^ n)) (n + q) = 0
Tactic: obtain ⟨q, rfl⟩ := Nat.exists_eq_add_of_le h
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p n q : ℕ
h : n ≤ n + q
⊢ HPow.hPow (α := ZMod (p ^ n)) (↑p : ZMod (p ^ n)) (n + q) = 0
have rw : (↑(p ^ n) : ZMod (p ^ n)) * HPow.hPow (α := ZMod (p ^ n)) (↑p : ZMod (p ^ n)) q = 0
Tactic: rw [pow_add, ← Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : AddGroupWithOne R
⊢ Eq.{u_1 + 1} (α := R) (cast (n := n) 0) 0
have delta : Eq.{u_1 + 1} (α := R)
  ((match (motive := (x : ℕ) → ZMod x → R) n with
      | 0 => Int.cast
      | n.succ => fun (i : ZMod (n + 1)) ↦ (↑i.val : R))
      0 :
    R)
  (0 : R)
Tactic: delta ZMod.cast
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : AddGroupWithOne R
⊢ Eq.{u_1 + 1} (α := R)
    ((match (motive := (x : ℕ) → ZMod x → R) n with
        | 0 => Int.cast
        | n.succ => fun (i : ZMod (n + 1)) ↦ (↑i.val : R))
        0 :
      R)
    (0 : R)
have zero : Eq.{u_1 + 1} (α := R)
  ((match (motive := (x : ℕ) → ZMod x → R) 0 with
      | 0 => Int.cast
      | n.succ => fun (i : ZMod (n + 1)) ↦ (↑i.val : R))
      0 :
    R)
  (0 : R)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : AddGroupWithOne R
zero :
  Eq.{u_1 + 1} (α := R)
    ((match (motive := (x : ℕ) → ZMod x → R) 0 with
        | 0 => Int.cast
        | n.succ => fun (i : ZMod (n + 1)) ↦ (↑i.val : R))
        0 :
      R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((match (motive := (x : ℕ) → ZMod x → R) n with
        | 0 => Int.cast
        | n.succ => fun (i : ZMod (n + 1)) ↦ (↑i.val : R))
        0 :
      R)
    (0 : R)
have succ : ∀ (n : ℕ),
  Eq.{u_1 + 1} (α := R)
    ((match (motive := (x : ℕ) → ZMod x → R) n + 1 with
        | 0 => Int.cast
        | n.succ => fun (i : ZMod (n + 1)) ↦ (↑i.val : R))
        0 :
      R)
    (0 : R)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : AddGroupWithOne R
inst_1 : NeZero n
a : ZMod n
⊢ Eq.{u_1 + 1} (α := R) a.cast (↑a.val : R)
have zero : ∀ [NeZero (R := ℕ) 0] (a : ZMod 0), Eq.{u_1 + 1} (α := R) a.cast (↑a.val : R)
Tactic: cases n
Cleared hypotheses: n, inst_1, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : AddGroupWithOne R
inst_1 : NeZero n
a : ZMod n
zero : ∀ [NeZero (R := ℕ) 0] (a : ZMod 0), Eq.{u_1 + 1} (α := R) a.cast (↑a.val : R)
⊢ Eq.{u_1 + 1} (α := R) a.cast (↑a.val : R)
have succ : ∀ (n : ℕ) [NeZero (n + 1)] (a : ZMod (n + 1)), Eq.{u_1 + 1} (α := R) a.cast (↑a.val : R)
Tactic: cases n
Cleared hypotheses: n, inst_1, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : AddGroupWithOne R
S : Type u_2
inst_1 : AddGroupWithOne S
a : ZMod n
⊢ Eq.{u_1 + 1} (α := R) a.cast.1 a.cast
have zero : ∀ (a : ZMod 0), Eq.{u_1 + 1} (α := R) a.cast.1 a.cast
Tactic: cases n
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : AddGroupWithOne R
S : Type u_2
inst_1 : AddGroupWithOne S
a : ZMod n
zero : ∀ (a : ZMod 0), Eq.{u_1 + 1} (α := R) a.cast.1 a.cast
⊢ Eq.{u_1 + 1} (α := R) a.cast.1 a.cast
have succ : ∀ (n : ℕ) (a : ZMod (n + 1)), Eq.{u_1 + 1} (α := R) a.cast.1 a.cast
Tactic: cases n
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : AddGroupWithOne R
S : Type u_2
inst_1 : AddGroupWithOne S
a : ZMod n
⊢ Eq.{u_2 + 1} (α := S) a.cast.2 a.cast
have zero : ∀ (a : ZMod 0), Eq.{u_2 + 1} (α := S) a.cast.2 a.cast
Tactic: cases n
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : AddGroupWithOne R
S : Type u_2
inst_1 : AddGroupWithOne S
a : ZMod n
zero : ∀ (a : ZMod 0), Eq.{u_2 + 1} (α := S) a.cast.2 a.cast
⊢ Eq.{u_2 + 1} (α := S) a.cast.2 a.cast
have succ : ∀ (n : ℕ) (a : ZMod (n + 1)), Eq.{u_2 + 1} (α := S) a.cast.2 a.cast
Tactic: cases n
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
⊢ (↑a.val : ZMod n) = a
have zero : ∀ [NeZero (R := ℕ) 0] (a : ZMod 0), (↑a.val : ZMod 0) = a
Tactic: cases n
Cleared hypotheses: n, inst, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
zero : ∀ [NeZero (R := ℕ) 0] (a : ZMod 0), (↑a.val : ZMod 0) = a
⊢ (↑a.val : ZMod n) = a
have succ : ∀ (n : ℕ) [NeZero (n + 1)] (a : ZMod (n + 1)), (↑a.val : ZMod (n + 1)) = a
Tactic: cases n
Cleared hypotheses: n, inst, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
⊢ (↑a.cast : ZMod n) = a
have zero : ∀ (a : ZMod 0), (↑a.cast : ZMod 0) = a
Tactic: cases n
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
zero : ∀ (a : ZMod 0), (↑a.cast : ZMod 0) = a
⊢ (↑a.cast : ZMod n) = a
have succ : ∀ (n : ℕ) (a : ZMod (n + 1)), (↑a.cast : ZMod (n + 1)) = a
Tactic: cases n
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
⊢ (↑(↑a.val : ℤ) : ZMod (n + 1)) = a
have succ : (↑a.val : ZMod (n + 1)) = a
Tactic: rw [Int.cast_natCast, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
succ : (↑a.val : ZMod (n + 1)) = a
⊢ (↑(↑a.val : ℤ) : ZMod (n + 1)) = a
have succ₁ : a = a
Tactic: rw [Int.cast_natCast, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : NeZero n
⊢ Eq.{u_1 + 1} (α := ZMod n → R) (Nat.cast ∘ val) cast
have zero : ∀ [NeZero (R := ℕ) 0], Eq.{u_1 + 1} (α := ZMod 0 → R) (Nat.cast ∘ val) cast
Tactic: cases n
Cleared hypotheses: n, inst_1
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : NeZero n
zero : ∀ [NeZero (R := ℕ) 0], Eq.{u_1 + 1} (α := ZMod 0 → R) (Nat.cast ∘ val) cast
⊢ Eq.{u_1 + 1} (α := ZMod n → R) (Nat.cast ∘ val) cast
have succ : ∀ (n : ℕ) [NeZero (n + 1)], Eq.{u_1 + 1} (α := ZMod (n + 1) → R) (Nat.cast ∘ val) cast
Tactic: cases n
Cleared hypotheses: n, inst_1
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
⊢ Eq.{u_1 + 1} (α := ZMod n → R) (Int.cast ∘ cast) cast
have zero : Eq.{u_1 + 1} (α := ZMod 0 → R) (Int.cast ∘ cast) cast
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
zero : Eq.{u_1 + 1} (α := ZMod 0 → R) (Int.cast ∘ cast) cast
⊢ Eq.{u_1 + 1} (α := ZMod n → R) (Int.cast ∘ cast) cast
have succ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := ZMod (n + 1) → R) (Int.cast ∘ cast) cast
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
⊢ Eq.{u_1 + 1} (α := ZMod (n + 1) → R) (Int.cast ∘ cast) cast
have succ : ∀ (x : ZMod (n + 1)), Eq.{u_1 + 1} (α := R) ((Int.cast ∘ cast) x) x.cast
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a b : ZMod n
⊢ (a + b).cast =
    if (↑n : ℤ) ≤ HAdd.hAdd (α := ℤ) a.cast b.cast then HAdd.hAdd (α := ℤ) a.cast b.cast - (↑n : ℤ)
    else HAdd.hAdd (α := ℤ) a.cast b.cast
have zero : ∀ (a b : ZMod 0),
  (a + b).cast =
    if (↑0 : ℤ) ≤ HAdd.hAdd (α := ℤ) a.cast b.cast then HAdd.hAdd (α := ℤ) a.cast b.cast - (↑0 : ℤ)
    else HAdd.hAdd (α := ℤ) a.cast b.cast
Tactic: rcases n with - | n
Cleared hypotheses: n, a, b
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a b : ZMod n
zero :
  ∀ (a b : ZMod 0),
    (a + b).cast =
      if (↑0 : ℤ) ≤ HAdd.hAdd (α := ℤ) a.cast b.cast then HAdd.hAdd (α := ℤ) a.cast b.cast - (↑0 : ℤ)
      else HAdd.hAdd (α := ℤ) a.cast b.cast
⊢ (a + b).cast =
    if (↑n : ℤ) ≤ HAdd.hAdd (α := ℤ) a.cast b.cast then HAdd.hAdd (α := ℤ) a.cast b.cast - (↑n : ℤ)
    else HAdd.hAdd (α := ℤ) a.cast b.cast
have succ : ∀ (n : ℕ) (a b : ZMod (n + 1)),
  (a + b).cast =
    if (↑(n + 1) : ℤ) ≤ HAdd.hAdd (α := ℤ) a.cast b.cast then HAdd.hAdd (α := ℤ) a.cast b.cast - (↑(n + 1) : ℤ)
    else HAdd.hAdd (α := ℤ) a.cast b.cast
Tactic: rcases n with - | n
Cleared hypotheses: n, a, b
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a b : ZMod 0
⊢ (a + b).cast =
    if (↑0 : ℤ) ≤ HAdd.hAdd (α := ℤ) a.cast b.cast then HAdd.hAdd (α := ℤ) a.cast b.cast - (↑0 : ℤ)
    else HAdd.hAdd (α := ℤ) a.cast b.cast
have zero : (a + b).cast = HAdd.hAdd (α := ℤ) a.cast b.cast
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).cast =
    if (↑(n + 1) : ℤ) ≤ HAdd.hAdd (α := ℤ) a.cast b.cast then HAdd.hAdd (α := ℤ) a.cast b.cast - (↑(n + 1) : ℤ)
    else HAdd.hAdd (α := ℤ) a.cast b.cast
have succ : ∀ (a b : Fin (n + 1)),
  (a + b).cast =
    if (↑(n + 1) : ℤ) ≤ HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) then
      HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - (↑(n + 1) : ℤ)
    else HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b)
Tactic: change Fin (n + 1) at a b
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
⊢ (↑(↑(a + b) : ℕ) : ℤ) =
    if (↑(n + 1) : ℤ) ≤ HAdd.hAdd (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) then
      HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - (↑(n + 1) : ℤ)
    else HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b)
have succ : (↑(if n + 1 ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - (n + 1) else (↑a : ℕ) + (↑b : ℕ)) : ℤ) =
  if HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ≤ HAdd.hAdd (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) then
    HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
  else HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b)
Tactic: simp only [Fin.val_add_eq_ite, Int.natCast_succ]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
⊢ (↑(if n + 1 ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - (n + 1) else (↑a : ℕ) + (↑b : ℕ)) : ℤ) =
    if HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ≤ HAdd.hAdd (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) then
      HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
    else HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b)
have succ : (↑(if n + 1 ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - (n + 1) else (↑a : ℕ) + (↑b : ℕ)) : ℤ) =
  if n + 1 ≤ (↑a : ℕ) + (↑b : ℕ) then HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - (↑(n + 1) : ℤ)
  else HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
⊢ (↑(if n + 1 ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - (n + 1) else (↑a : ℕ) + (↑b : ℕ)) : ℤ) =
    if n + 1 ≤ (↑a : ℕ) + (↑b : ℕ) then HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - (↑(n + 1) : ℤ)
    else HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b)
have pos : ∀ (h : n + 1 ≤ (↑a : ℕ) + (↑b : ℕ)),
  (↑((↑a : ℕ) + (↑b : ℕ) - (n + 1)) : ℤ) =
    HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - (↑(n + 1) : ℤ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
pos :
  ∀ (h : n + 1 ≤ (↑a : ℕ) + (↑b : ℕ)),
    (↑((↑a : ℕ) + (↑b : ℕ) - (n + 1)) : ℤ) =
      HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - (↑(n + 1) : ℤ)
⊢ (↑(if n + 1 ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - (n + 1) else (↑a : ℕ) + (↑b : ℕ)) : ℤ) =
    if n + 1 ≤ (↑a : ℕ) + (↑b : ℕ) then HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - (↑(n + 1) : ℤ)
    else HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b)
have neg : ∀ (h : ¬n + 1 ≤ (↑a : ℕ) + (↑b : ℕ)),
  (↑((↑a : ℕ) + (↑b : ℕ)) : ℤ) = HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
h : n + 1 ≤ (↑a : ℕ) + (↑b : ℕ)
⊢ (↑((↑a : ℕ) + (↑b : ℕ) - (n + 1)) : ℤ) =
    HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - (↑(n + 1) : ℤ)
have pos : HSub.hSub (α := ℤ) (↑((↑a : ℕ) + (↑b : ℕ)) : ℤ) (↑(n + 1) : ℤ) =
  HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - (↑(n + 1) : ℤ)
Tactic: rw [Nat.cast_sub h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ n
⊢ Eq.{u_1 + 1} (α := R) (cast (n := n) 1) 1
have zero : ∀ (h : m ∣ 0), Eq.{u_1 + 1} (α := R) (cast (n := 0) 1) 1
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ n
zero : ∀ (h : m ∣ 0), Eq.{u_1 + 1} (α := R) (cast (n := 0) 1) 1
⊢ Eq.{u_1 + 1} (α := R) (cast (n := n) 1) 1
have succ : ∀ (n : ℕ) (h : m ∣ n + 1), Eq.{u_1 + 1} (α := R) (cast (n := n + 1) 1) 1
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
⊢ Eq.{u_1 + 1} (α := R) (cast (n := n + 1) 1) 1
have succ : Eq.{u_1 + 1} (α := R) (↑(1 % (n + 1)) : R) 1
Tactic: change ((1 % (n + 1) : ℕ) : R) = 1
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
⊢ Eq.{u_1 + 1} (α := R) (↑(1 % (n + 1)) : R) 1
have succ : ∀ (h : m ∣ HAdd.hAdd (α := ℕ) 0 1), Eq.{u_1 + 1} (α := R) (↑(1 % HAdd.hAdd (α := ℕ) 0 1) : R) 1
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
succ : ∀ (h : m ∣ HAdd.hAdd (α := ℕ) 0 1), Eq.{u_1 + 1} (α := R) (↑(1 % HAdd.hAdd (α := ℕ) 0 1) : R) 1
⊢ Eq.{u_1 + 1} (α := R) (↑(1 % (n + 1)) : R) 1
have succ₁ : ∀ (n : ℕ) (h : m ∣ n + 1 + 1), Eq.{u_1 + 1} (α := R) (↑(1 % (n + 1 + 1)) : R) 1
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ HAdd.hAdd (α := ℕ) 0 1
⊢ Eq.{u_1 + 1} (α := R) (↑(1 % HAdd.hAdd (α := ℕ) 0 1) : R) 1
have h₁ : m = 1
Tactic: rw [Nat.dvd_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m = 1
⊢ Eq.{u_1 + 1} (α := R) (↑(1 % HAdd.hAdd (α := ℕ) 0 1) : R) 1
have inst : CharP R 1
Tactic: subst m
Cleared hypotheses: m, inst_1, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1 + 1
⊢ Eq.{u_1 + 1} (α := R) (↑(1 % (n + 1 + 1)) : R) 1
have succ : Eq.{u_1 + 1} (α := R) (↑1 : R) 1
Tactic: rw [Nat.mod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1 + 1
succ : Eq.{u_1 + 1} (α := R) (↑1 : R) 1
⊢ Eq.{u_1 + 1} (α := R) (↑(1 % (n + 1 + 1)) : R) 1
have succ₁ : 1 < n + 1 + 1
Tactic: rw [Nat.mod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ n
a b : ZMod n
⊢ (a + b).cast = HAdd.hAdd (α := R) a.cast b.cast
have zero : ∀ (h : m ∣ 0) (a b : ZMod 0), (a + b).cast = HAdd.hAdd (α := R) a.cast b.cast
Tactic: cases n
Cleared hypotheses: n, h, a, b
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ n
a b : ZMod n
zero : ∀ (h : m ∣ 0) (a b : ZMod 0), (a + b).cast = HAdd.hAdd (α := R) a.cast b.cast
⊢ (a + b).cast = HAdd.hAdd (α := R) a.cast b.cast
have succ : ∀ (n : ℕ) (h : m ∣ n + 1) (a b : ZMod (n + 1)), (a + b).cast = HAdd.hAdd (α := R) a.cast b.cast
Tactic: cases n
Cleared hypotheses: n, h, a, b
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
a b : ZMod (n + 1)
⊢ (a + b).cast = HAdd.hAdd (α := R) a.cast b.cast
have succ : HAdd.hAdd (α := R) a.cast b.cast = (a + b).cast
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
a b : ZMod (n + 1)
⊢ HAdd.hAdd (α := R) a.cast b.cast = (a + b).cast
have succ : HAdd.hAdd (α := R) (↑(↑a : ℕ) : R) (↑(↑b : ℕ) : R) = (↑(↑(a + b) : ℕ) : R)
Tactic: dsimp [ZMod, ZMod.cast, ZMod.val]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
a b : ZMod (n + 1)
⊢ HAdd.hAdd (α := R) (↑(↑a : ℕ) : R) (↑(↑b : ℕ) : R) = (↑(↑(a + b) : ℕ) : R)
have succ : m ∣ (↑a : ℕ) + (↑b : ℕ) - ((↑a : ℕ) + (↑b : ℕ)) % (n + 1)
Tactic: rw [← Nat.cast_add, Fin.val_add, ← sub_eq_zero, ← Nat.cast_sub (Nat.mod_le _ _),
    @CharP.cast_eq_zero_iff R _ m]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ n
a b : ZMod n
⊢ (a * b).cast = HMul.hMul (α := R) a.cast b.cast
have zero : ∀ (h : m ∣ 0) (a b : ZMod 0), (a * b).cast = HMul.hMul (α := R) a.cast b.cast
Tactic: cases n
Cleared hypotheses: n, h, a, b
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ n
a b : ZMod n
zero : ∀ (h : m ∣ 0) (a b : ZMod 0), (a * b).cast = HMul.hMul (α := R) a.cast b.cast
⊢ (a * b).cast = HMul.hMul (α := R) a.cast b.cast
have succ : ∀ (n : ℕ) (h : m ∣ n + 1) (a b : ZMod (n + 1)), (a * b).cast = HMul.hMul (α := R) a.cast b.cast
Tactic: cases n
Cleared hypotheses: n, h, a, b
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
a b : ZMod (n + 1)
⊢ (a * b).cast = HMul.hMul (α := R) a.cast b.cast
have succ : HMul.hMul (α := R) a.cast b.cast = (a * b).cast
Tactic: symm