awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x y : ZMod n
⊢ (x + y).cast = HAdd.hAdd (α := ℤ) x.cast y.cast % (↑n : ℤ)
have rw : Eq (α := ℤ) (x + y).cast (cast (n := n) (↑(HAdd.hAdd (α := ℤ) x.cast y.cast) : ZMod n))
Tactic: rw [← ZMod.coe_intCast, Int.cast_add, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x y : ZMod n
rw : Eq (α := ℤ) (x + y).cast (cast (n := n) (↑(HAdd.hAdd (α := ℤ) x.cast y.cast) : ZMod n))
⊢ (x + y).cast = HAdd.hAdd (α := ℤ) x.cast y.cast % (↑n : ℤ)
have rw₁ : Eq (α := ℤ) (x + y).cast (HAdd.hAdd (α := ZMod n) (↑x.cast : ZMod n) (↑y.cast : ZMod n)).cast
Tactic: rw [← ZMod.coe_intCast, Int.cast_add, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x y : ZMod n
rw : Eq (α := ℤ) (x + y).cast (cast (n := n) (↑(HAdd.hAdd (α := ℤ) x.cast y.cast) : ZMod n))
rw₁ : Eq (α := ℤ) (x + y).cast (HAdd.hAdd (α := ZMod n) (↑x.cast : ZMod n) (↑y.cast : ZMod n)).cast
⊢ (x + y).cast = HAdd.hAdd (α := ℤ) x.cast y.cast % (↑n : ℤ)
have rw₂ : Eq (α := ℤ) (x + y).cast (x + (↑y.cast : ZMod n)).cast
Tactic: rw [← ZMod.coe_intCast, Int.cast_add, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x y : ZMod n
rw : Eq (α := ℤ) (x + y).cast (cast (n := n) (↑(HAdd.hAdd (α := ℤ) x.cast y.cast) : ZMod n))
rw₁ : Eq (α := ℤ) (x + y).cast (HAdd.hAdd (α := ZMod n) (↑x.cast : ZMod n) (↑y.cast : ZMod n)).cast
rw₂ : Eq (α := ℤ) (x + y).cast (x + (↑y.cast : ZMod n)).cast
⊢ (x + y).cast = HAdd.hAdd (α := ℤ) x.cast y.cast % (↑n : ℤ)
have rw₃ : Eq (α := ℤ) (x + y).cast (x + y).cast
Tactic: rw [← ZMod.coe_intCast, Int.cast_add, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x y : ZMod n
⊢ (x * y).cast = HMul.hMul (α := ℤ) x.cast y.cast % (↑n : ℤ)
have rw : Eq (α := ℤ) (x * y).cast (cast (n := n) (↑(HMul.hMul (α := ℤ) x.cast y.cast) : ZMod n))
Tactic: rw [← ZMod.coe_intCast, Int.cast_mul, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x y : ZMod n
rw : Eq (α := ℤ) (x * y).cast (cast (n := n) (↑(HMul.hMul (α := ℤ) x.cast y.cast) : ZMod n))
⊢ (x * y).cast = HMul.hMul (α := ℤ) x.cast y.cast % (↑n : ℤ)
have rw₁ : Eq (α := ℤ) (x * y).cast (HMul.hMul (α := ZMod n) (↑x.cast : ZMod n) (↑y.cast : ZMod n)).cast
Tactic: rw [← ZMod.coe_intCast, Int.cast_mul, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x y : ZMod n
rw : Eq (α := ℤ) (x * y).cast (cast (n := n) (↑(HMul.hMul (α := ℤ) x.cast y.cast) : ZMod n))
rw₁ : Eq (α := ℤ) (x * y).cast (HMul.hMul (α := ZMod n) (↑x.cast : ZMod n) (↑y.cast : ZMod n)).cast
⊢ (x * y).cast = HMul.hMul (α := ℤ) x.cast y.cast % (↑n : ℤ)
have rw₂ : Eq (α := ℤ) (x * y).cast (x * (↑y.cast : ZMod n)).cast
Tactic: rw [← ZMod.coe_intCast, Int.cast_mul, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x y : ZMod n
rw : Eq (α := ℤ) (x * y).cast (cast (n := n) (↑(HMul.hMul (α := ℤ) x.cast y.cast) : ZMod n))
rw₁ : Eq (α := ℤ) (x * y).cast (HMul.hMul (α := ZMod n) (↑x.cast : ZMod n) (↑y.cast : ZMod n)).cast
rw₂ : Eq (α := ℤ) (x * y).cast (x * (↑y.cast : ZMod n)).cast
⊢ (x * y).cast = HMul.hMul (α := ℤ) x.cast y.cast % (↑n : ℤ)
have rw₃ : Eq (α := ℤ) (x * y).cast (x * y).cast
Tactic: rw [← ZMod.coe_intCast, Int.cast_mul, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x y : ZMod n
⊢ (x - y).cast = HSub.hSub (α := ℤ) x.cast y.cast % (↑n : ℤ)
have rw : Eq (α := ℤ) (x - y).cast (cast (n := n) (↑(HSub.hSub (α := ℤ) x.cast y.cast) : ZMod n))
Tactic: rw [← ZMod.coe_intCast, Int.cast_sub, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x y : ZMod n
rw : Eq (α := ℤ) (x - y).cast (cast (n := n) (↑(HSub.hSub (α := ℤ) x.cast y.cast) : ZMod n))
⊢ (x - y).cast = HSub.hSub (α := ℤ) x.cast y.cast % (↑n : ℤ)
have rw₁ : Eq (α := ℤ) (x - y).cast (HSub.hSub (α := ZMod n) (↑x.cast : ZMod n) (↑y.cast : ZMod n)).cast
Tactic: rw [← ZMod.coe_intCast, Int.cast_sub, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x y : ZMod n
rw : Eq (α := ℤ) (x - y).cast (cast (n := n) (↑(HSub.hSub (α := ℤ) x.cast y.cast) : ZMod n))
rw₁ : Eq (α := ℤ) (x - y).cast (HSub.hSub (α := ZMod n) (↑x.cast : ZMod n) (↑y.cast : ZMod n)).cast
⊢ (x - y).cast = HSub.hSub (α := ℤ) x.cast y.cast % (↑n : ℤ)
have rw₂ : Eq (α := ℤ) (x - y).cast (x - (↑y.cast : ZMod n)).cast
Tactic: rw [← ZMod.coe_intCast, Int.cast_sub, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x y : ZMod n
rw : Eq (α := ℤ) (x - y).cast (cast (n := n) (↑(HSub.hSub (α := ℤ) x.cast y.cast) : ZMod n))
rw₁ : Eq (α := ℤ) (x - y).cast (HSub.hSub (α := ZMod n) (↑x.cast : ZMod n) (↑y.cast : ZMod n)).cast
rw₂ : Eq (α := ℤ) (x - y).cast (x - (↑y.cast : ZMod n)).cast
⊢ (x - y).cast = HSub.hSub (α := ℤ) x.cast y.cast % (↑n : ℤ)
have rw₃ : Eq (α := ℤ) (x - y).cast (x - y).cast
Tactic: rw [← ZMod.coe_intCast, Int.cast_sub, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x : ZMod n
⊢ (-x).cast = HMod.hMod (α := ℤ) (-x.cast) (↑n : ℤ)
have rw : Eq (α := ℤ) (-x).cast (cast (n := n) (↑(-x.cast) : ZMod n))
Tactic: rw [← ZMod.coe_intCast, Int.cast_neg, ZMod.intCast_zmod_cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x : ZMod n
rw : Eq (α := ℤ) (-x).cast (cast (n := n) (↑(-x.cast) : ZMod n))
⊢ (-x).cast = HMod.hMod (α := ℤ) (-x.cast) (↑n : ℤ)
have rw₁ : Eq (α := ℤ) (-x).cast (cast (n := n) (-(↑x.cast : ZMod n)))
Tactic: rw [← ZMod.coe_intCast, Int.cast_neg, ZMod.intCast_zmod_cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x : ZMod n
rw : Eq (α := ℤ) (-x).cast (cast (n := n) (↑(-x.cast) : ZMod n))
rw₁ : Eq (α := ℤ) (-x).cast (cast (n := n) (-(↑x.cast : ZMod n)))
⊢ (-x).cast = HMod.hMod (α := ℤ) (-x.cast) (↑n : ℤ)
have rw₂ : Eq (α := ℤ) (-x).cast (-x).cast
Tactic: rw [← ZMod.coe_intCast, Int.cast_neg, ZMod.intCast_zmod_cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
⊢ (↑(-1) : ℕ) = n
have zero : (↑(-1) : ℕ) = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
zero : (↑(-1) : ℕ) = 0
⊢ (↑(-1) : ℕ) = n
have succ : ∀ (n : ℕ), (↑(-1) : ℕ) = n + 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
⊢ (↑(-1) : ℕ) = n + 1
have succ : n + 1 = n + 1
Tactic: rw [Fin.coe_neg_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
⊢ cast (n := n) (-1) = HSub.hSub (α := R) (↑n : R) 1
have zero : cast (n := 0) (-1) = HSub.hSub (α := R) (↑0 : R) 1
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
zero : cast (n := 0) (-1) = HSub.hSub (α := R) (↑0 : R) 1
⊢ cast (n := n) (-1) = HSub.hSub (α := R) (↑n : R) 1
have succ : ∀ (n : ℕ), cast (n := n + 1) (-1) = HSub.hSub (α := R) (↑(n + 1) : R) 1
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
⊢ cast (n := 0) (-1) = HSub.hSub (α := R) (↑0 : R) 1
have zero : (↑(-1) : R) = HSub.hSub (α := R) (↑0 : R) 1
Tactic: dsimp [ZMod, ZMod.cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
⊢ cast (n := n + 1) (-1) = HSub.hSub (α := R) (↑(n + 1) : R) 1
have succ : (↑(val (n := n + 1) (-1)) : R) = HSub.hSub (α := R) (↑(n + 1) : R) 1
Tactic: rw [← natCast_val, val_neg_one, Nat.cast_succ, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
succ : (↑(val (n := n + 1) (-1)) : R) = HSub.hSub (α := R) (↑(n + 1) : R) 1
⊢ cast (n := n + 1) (-1) = HSub.hSub (α := R) (↑(n + 1) : R) 1
have succ₁ : (↑n : R) = HSub.hSub (α := R) (↑(n + 1) : R) 1
Tactic: rw [← natCast_val, val_neg_one, Nat.cast_succ, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
succ : (↑(val (n := n + 1) (-1)) : R) = HSub.hSub (α := R) (↑(n + 1) : R) 1
succ₁ : (↑n : R) = HSub.hSub (α := R) (↑(n + 1) : R) 1
⊢ cast (n := n + 1) (-1) = HSub.hSub (α := R) (↑(n + 1) : R) 1
have succ₂ : (↑n : R) = HAdd.hAdd (α := R) (↑n : R) 1 - 1
Tactic: rw [← natCast_val, val_neg_one, Nat.cast_succ, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
succ : (↑(val (n := n + 1) (-1)) : R) = HSub.hSub (α := R) (↑(n + 1) : R) 1
succ₁ : (↑n : R) = HSub.hSub (α := R) (↑(n + 1) : R) 1
succ₂ : (↑n : R) = HAdd.hAdd (α := R) (↑n : R) 1 - 1
⊢ cast (n := n + 1) (-1) = HSub.hSub (α := R) (↑(n + 1) : R) 1
have succ₃ : Eq.{u_1 + 1} (α := R) (↑n : R) (↑n : R)
Tactic: rw [← natCast_val, val_neg_one, Nat.cast_succ, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod n
⊢ (k - 1).cast = HSub.hSub (α := R) (if k = 0 then (↑n : R) else k.cast) 1
have pos : ∀ (hk : k = 0), (k - 1).cast = HSub.hSub (α := R) (↑n : R) 1
Tactic: split_ifs with hk
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod n
pos : ∀ (hk : k = 0), (k - 1).cast = HSub.hSub (α := R) (↑n : R) 1
⊢ (k - 1).cast = HSub.hSub (α := R) (if k = 0 then (↑n : R) else k.cast) 1
have neg : ∀ (hk : ¬k = 0), (k - 1).cast = HSub.hSub (α := R) k.cast 1
Tactic: split_ifs with hk
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod n
hk : k = 0
⊢ (k - 1).cast = HSub.hSub (α := R) (↑n : R) 1
have pos : (HSub.hSub (α := ZMod n) 0 1).cast = HSub.hSub (α := R) (↑n : R) 1
Tactic: rw [hk, zero_sub, ZMod.cast_neg_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod n
hk : k = 0
pos : (HSub.hSub (α := ZMod n) 0 1).cast = HSub.hSub (α := R) (↑n : R) 1
⊢ (k - 1).cast = HSub.hSub (α := R) (↑n : R) 1
have pos₁ : cast (n := n) (-1) = HSub.hSub (α := R) (↑n : R) 1
Tactic: rw [hk, zero_sub, ZMod.cast_neg_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod n
hk : k = 0
pos : (HSub.hSub (α := ZMod n) 0 1).cast = HSub.hSub (α := R) (↑n : R) 1
pos₁ : cast (n := n) (-1) = HSub.hSub (α := R) (↑n : R) 1
⊢ (k - 1).cast = HSub.hSub (α := R) (↑n : R) 1
have pos₂ : HSub.hSub (α := R) (↑n : R) 1 = HSub.hSub (α := R) (↑n : R) 1
Tactic: rw [hk, zero_sub, ZMod.cast_neg_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod n
hk : ¬k = 0
⊢ (k - 1).cast = HSub.hSub (α := R) k.cast 1
have neg : ∀ (k : ZMod 0) (hk : ¬k = 0), (k - 1).cast = HSub.hSub (α := R) k.cast 1
Tactic: cases n
Cleared hypotheses: n, k, hk
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod n
hk : ¬k = 0
neg : ∀ (k : ZMod 0) (hk : ¬k = 0), (k - 1).cast = HSub.hSub (α := R) k.cast 1
⊢ (k - 1).cast = HSub.hSub (α := R) k.cast 1
have neg₁ : ∀ (n : ℕ) (k : ZMod (n + 1)) (hk : ¬k = 0), (k - 1).cast = HSub.hSub (α := R) k.cast 1
Tactic: cases n
Cleared hypotheses: n, k, hk
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
k : ZMod 0
hk : ¬k = 0
⊢ (k - 1).cast = HSub.hSub (α := R) k.cast 1
have neg : (↑(k - 1) : R) = HSub.hSub (α := R) (↑k : R) 1
Tactic: dsimp [ZMod, ZMod.cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
k : ZMod 0
hk : ¬k = 0
⊢ (↑(k - 1) : R) = HSub.hSub (α := R) (↑k : R) 1
have neg : HSub.hSub (α := R) (↑k : R) (↑1 : R) = HSub.hSub (α := R) (↑k : R) 1
Tactic: rw [Int.cast_sub, Int.cast_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
k : ZMod 0
hk : ¬k = 0
neg : HSub.hSub (α := R) (↑k : R) (↑1 : R) = HSub.hSub (α := R) (↑k : R) 1
⊢ (↑(k - 1) : R) = HSub.hSub (α := R) (↑k : R) 1
have neg₁ : HSub.hSub (α := R) (↑k : R) 1 = HSub.hSub (α := R) (↑k : R) 1
Tactic: rw [Int.cast_sub, Int.cast_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod (n + 1)
hk : ¬k = 0
⊢ (k - 1).cast = HSub.hSub (α := R) k.cast 1
have neg : (↑(↑(k - 1) : ℕ) : R) = HSub.hSub (α := R) (↑(↑k : ℕ) : R) 1
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
n : ℕ
k : ZMod (n + 1)
hk : ¬k = 0
⊢ (↑(↑(k - 1) : ℕ) : R) = HSub.hSub (α := R) (↑(↑k : ℕ) : R) 1
have neg : (↑((↑k : ℕ) - 1) : R) = HSub.hSub (α := R) (↑(↑k : ℕ) : R) 1
Tactic: rw [Fin.coe_sub_one, if_neg]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod (n + 1)
hk : ¬k = 0
⊢ (↑((↑k : ℕ) - 1) : R) = HSub.hSub (α := R) (↑(↑k : ℕ) : R) 1
have neg : 1 ≤ (↑k : ℕ)
Tactic: rw [Nat.cast_sub, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod (n + 1)
hk : ¬k = 0
⊢ 1 ≤ (↑k : ℕ)
have neg : ∀ (hk : ¬(↑k : ℕ) = (↑0 : ℕ)), 1 ≤ (↑k : ℕ)
Tactic: rwa [Fin.ext_iff, Fin.val_zero, ← Ne, ← Nat.one_le_iff_ne_zero] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod (n + 1)
hk : ¬k = 0
neg : ∀ (hk : ¬(↑k : ℕ) = (↑0 : ℕ)), 1 ≤ (↑k : ℕ)
⊢ 1 ≤ (↑k : ℕ)
have neg₁ : ∀ (hk : ¬(↑k : ℕ) = 0), 1 ≤ (↑k : ℕ)
Tactic: rwa [Fin.ext_iff, Fin.val_zero, ← Ne, ← Nat.one_le_iff_ne_zero] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod (n + 1)
hk : ¬k = 0
neg : ∀ (hk : ¬(↑k : ℕ) = (↑0 : ℕ)), 1 ≤ (↑k : ℕ)
neg₁ : ∀ (hk : ¬(↑k : ℕ) = 0), 1 ≤ (↑k : ℕ)
⊢ 1 ≤ (↑k : ℕ)
have neg₂ : ∀ (hk : (↑k : ℕ) ≠ 0), 1 ≤ (↑k : ℕ)
Tactic: rwa [Fin.ext_iff, Fin.val_zero, ← Ne, ← Nat.one_le_iff_ne_zero] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod (n + 1)
hk : ¬k = 0
neg : ∀ (hk : ¬(↑k : ℕ) = (↑0 : ℕ)), 1 ≤ (↑k : ℕ)
neg₁ : ∀ (hk : ¬(↑k : ℕ) = 0), 1 ≤ (↑k : ℕ)
neg₂ : ∀ (hk : (↑k : ℕ) ≠ 0), 1 ≤ (↑k : ℕ)
⊢ 1 ≤ (↑k : ℕ)
have neg₃ : ∀ (hk : 1 ≤ (↑k : ℕ)), 1 ≤ (↑k : ℕ)
Tactic: rwa [Fin.ext_iff, Fin.val_zero, ← Ne, ← Nat.one_le_iff_ne_zero] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p n : ℕ
z : ZMod p
inst : NeZero p
⊢ (↑n : ZMod p) = z ↔ ∃ (k : ℕ), n = z.val + p * k
have mp : (↑n : ZMod p) = z → ∃ (k : ℕ), n = z.val + p * k
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p n : ℕ
z : ZMod p
inst : NeZero p
mp : (↑n : ZMod p) = z → ∃ (k : ℕ), n = z.val + p * k
⊢ (↑n : ZMod p) = z ↔ ∃ (k : ℕ), n = z.val + p * k
have mpr : (∃ (k : ℕ), n = z.val + p * k) → (↑n : ZMod p) = z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p n : ℕ
inst : NeZero p
⊢ ∃ (k : ℕ), n = val (n := p) (↑n : ZMod p) + p * k
have mp : n = val (n := p) (↑n : ZMod p) + p * (n / p)
Tactic: refine ⟨n / p, ?_⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p n : ℕ
inst : NeZero p
⊢ n = val (n := p) (↑n : ZMod p) + p * (n / p)
have mp : n = n % p + p * (n / p)
Tactic: rw [val_natCast, Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p n : ℕ
inst : NeZero p
mp : n = n % p + p * (n / p)
⊢ n = val (n := p) (↑n : ZMod p) + p * (n / p)
have mp₁ : n = n
Tactic: rw [val_natCast, Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
z : ZMod p
inst : NeZero p
k : ℕ
⊢ (↑(z.val + p * k) : ZMod p) = z
have mpr : HAdd.hAdd (α := ZMod p) (↑z.val : ZMod p) (↑(p * k) : ZMod p) = z
Tactic: rw [Nat.cast_add, natCast_zmod_val, Nat.cast_mul, natCast_self, zero_mul,
      add_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
z : ZMod p
inst : NeZero p
k : ℕ
mpr : HAdd.hAdd (α := ZMod p) (↑z.val : ZMod p) (↑(p * k) : ZMod p) = z
⊢ (↑(z.val + p * k) : ZMod p) = z
have mpr₁ : z + (↑(p * k) : ZMod p) = z
Tactic: rw [Nat.cast_add, natCast_zmod_val, Nat.cast_mul, natCast_self, zero_mul,
      add_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
z : ZMod p
inst : NeZero p
k : ℕ
mpr : HAdd.hAdd (α := ZMod p) (↑z.val : ZMod p) (↑(p * k) : ZMod p) = z
mpr₁ : z + (↑(p * k) : ZMod p) = z
⊢ (↑(z.val + p * k) : ZMod p) = z
have mpr₂ : z + HMul.hMul (α := ZMod p) (↑p : ZMod p) (↑k : ZMod p) = z
Tactic: rw [Nat.cast_add, natCast_zmod_val, Nat.cast_mul, natCast_self, zero_mul,
      add_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
z : ZMod p
inst : NeZero p
k : ℕ
mpr : HAdd.hAdd (α := ZMod p) (↑z.val : ZMod p) (↑(p * k) : ZMod p) = z
mpr₁ : z + (↑(p * k) : ZMod p) = z
mpr₂ : z + HMul.hMul (α := ZMod p) (↑p : ZMod p) (↑k : ZMod p) = z
⊢ (↑(z.val + p * k) : ZMod p) = z
have mpr₃ : z + HMul.hMul (α := ZMod p) 0 (↑k : ZMod p) = z
Tactic: rw [Nat.cast_add, natCast_zmod_val, Nat.cast_mul, natCast_self, zero_mul,
      add_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
z : ZMod p
inst : NeZero p
k : ℕ
mpr : HAdd.hAdd (α := ZMod p) (↑z.val : ZMod p) (↑(p * k) : ZMod p) = z
mpr₁ : z + (↑(p * k) : ZMod p) = z
mpr₂ : z + HMul.hMul (α := ZMod p) (↑p : ZMod p) (↑k : ZMod p) = z
mpr₃ : z + HMul.hMul (α := ZMod p) 0 (↑k : ZMod p) = z
⊢ (↑(z.val + p * k) : ZMod p) = z
have mpr₄ : z + 0 = z
Tactic: rw [Nat.cast_add, natCast_zmod_val, Nat.cast_mul, natCast_self, zero_mul,
      add_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
z : ZMod p
inst : NeZero p
k : ℕ
mpr : HAdd.hAdd (α := ZMod p) (↑z.val : ZMod p) (↑(p * k) : ZMod p) = z
mpr₁ : z + (↑(p * k) : ZMod p) = z
mpr₂ : z + HMul.hMul (α := ZMod p) (↑p : ZMod p) (↑k : ZMod p) = z
mpr₃ : z + HMul.hMul (α := ZMod p) 0 (↑k : ZMod p) = z
mpr₄ : z + 0 = z
⊢ (↑(z.val + p * k) : ZMod p) = z
have mpr₅ : z = z
Tactic: rw [Nat.cast_add, natCast_zmod_val, Nat.cast_mul, natCast_self, zero_mul,
      add_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
n : ℤ
z : ZMod p
inst : NeZero p
⊢ (↑n : ZMod p) = z ↔ ∃ (k : ℤ), n = (↑z.val : ℤ) + (↑p : ℤ) * k
have mp : (↑n : ZMod p) = z → ∃ (k : ℤ), n = (↑z.val : ℤ) + (↑p : ℤ) * k
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
n : ℤ
z : ZMod p
inst : NeZero p
mp : (↑n : ZMod p) = z → ∃ (k : ℤ), n = (↑z.val : ℤ) + (↑p : ℤ) * k
⊢ (↑n : ZMod p) = z ↔ ∃ (k : ℤ), n = (↑z.val : ℤ) + (↑p : ℤ) * k
have mpr : (∃ (k : ℤ), n = (↑z.val : ℤ) + (↑p : ℤ) * k) → (↑n : ZMod p) = z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
n : ℤ
inst : NeZero p
⊢ ∃ (k : ℤ), n = (↑(val (n := p) (↑n : ZMod p)) : ℤ) + (↑p : ℤ) * k
have mp : n = (↑(val (n := p) (↑n : ZMod p)) : ℤ) + (↑p : ℤ) * (n / (↑p : ℤ))
Tactic: refine ⟨n / p, ?_⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
n : ℤ
inst : NeZero p
⊢ n = (↑(val (n := p) (↑n : ZMod p)) : ℤ) + (↑p : ℤ) * (n / (↑p : ℤ))
have mp : n = n % (↑p : ℤ) + (↑p : ℤ) * (n / (↑p : ℤ))
Tactic: rw [val_intCast, Int.emod_add_mul_ediv]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
n : ℤ
inst : NeZero p
mp : n = n % (↑p : ℤ) + (↑p : ℤ) * (n / (↑p : ℤ))
⊢ n = (↑(val (n := p) (↑n : ZMod p)) : ℤ) + (↑p : ℤ) * (n / (↑p : ℤ))
have mp₁ : n = n
Tactic: rw [val_intCast, Int.emod_add_mul_ediv]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
z : ZMod p
inst : NeZero p
k : ℤ
⊢ (↑((↑z.val : ℤ) + (↑p : ℤ) * k) : ZMod p) = z
have mpr : HAdd.hAdd (α := ZMod p) (↑(↑z.val : ℤ) : ZMod p) (↑((↑p : ℤ) * k) : ZMod p) = z
Tactic: rw [Int.cast_add, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_val,
      ZMod.natCast_self, zero_mul, add_zero, cast_id]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
z : ZMod p
inst : NeZero p
k : ℤ
mpr : HAdd.hAdd (α := ZMod p) (↑(↑z.val : ℤ) : ZMod p) (↑((↑p : ℤ) * k) : ZMod p) = z
⊢ (↑((↑z.val : ℤ) + (↑p : ℤ) * k) : ZMod p) = z
have mpr₁ : (↑(↑z.val : ℤ) : ZMod p) + HMul.hMul (α := ZMod p) (↑(↑p : ℤ) : ZMod p) (↑k : ZMod p) = z
Tactic: rw [Int.cast_add, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_val,
      ZMod.natCast_self, zero_mul, add_zero, cast_id]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
z : ZMod p
inst : NeZero p
k : ℤ
mpr : HAdd.hAdd (α := ZMod p) (↑(↑z.val : ℤ) : ZMod p) (↑((↑p : ℤ) * k) : ZMod p) = z
mpr₁ : (↑(↑z.val : ℤ) : ZMod p) + HMul.hMul (α := ZMod p) (↑(↑p : ℤ) : ZMod p) (↑k : ZMod p) = z
⊢ (↑((↑z.val : ℤ) + (↑p : ℤ) * k) : ZMod p) = z
have mpr₂ : (↑z.val : ZMod p) + HMul.hMul (α := ZMod p) (↑(↑p : ℤ) : ZMod p) (↑k : ZMod p) = z
Tactic: rw [Int.cast_add, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_val,
      ZMod.natCast_self, zero_mul, add_zero, cast_id]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
z : ZMod p
inst : NeZero p
k : ℤ
mpr : HAdd.hAdd (α := ZMod p) (↑(↑z.val : ℤ) : ZMod p) (↑((↑p : ℤ) * k) : ZMod p) = z
mpr₁ : (↑(↑z.val : ℤ) : ZMod p) + HMul.hMul (α := ZMod p) (↑(↑p : ℤ) : ZMod p) (↑k : ZMod p) = z
mpr₂ : (↑z.val : ZMod p) + HMul.hMul (α := ZMod p) (↑(↑p : ℤ) : ZMod p) (↑k : ZMod p) = z
⊢ (↑((↑z.val : ℤ) + (↑p : ℤ) * k) : ZMod p) = z
have mpr₃ : (↑z.val : ZMod p) + HMul.hMul (α := ZMod p) (↑p : ZMod p) (↑k : ZMod p) = z
Tactic: rw [Int.cast_add, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_val,
      ZMod.natCast_self, zero_mul, add_zero, cast_id]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
z : ZMod p
inst : NeZero p
k : ℤ
mpr : HAdd.hAdd (α := ZMod p) (↑(↑z.val : ℤ) : ZMod p) (↑((↑p : ℤ) * k) : ZMod p) = z
mpr₁ : (↑(↑z.val : ℤ) : ZMod p) + HMul.hMul (α := ZMod p) (↑(↑p : ℤ) : ZMod p) (↑k : ZMod p) = z
mpr₂ : (↑z.val : ZMod p) + HMul.hMul (α := ZMod p) (↑(↑p : ℤ) : ZMod p) (↑k : ZMod p) = z
mpr₃ : (↑z.val : ZMod p) + HMul.hMul (α := ZMod p) (↑p : ZMod p) (↑k : ZMod p) = z
⊢ (↑((↑z.val : ℤ) + (↑p : ℤ) * k) : ZMod p) = z
have mpr₄ : z.cast + HMul.hMul (α := ZMod p) (↑p : ZMod p) (↑k : ZMod p) = z
Tactic: rw [Int.cast_add, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_val,
      ZMod.natCast_self, zero_mul, add_zero, cast_id]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
z : ZMod p
inst : NeZero p
k : ℤ
mpr : HAdd.hAdd (α := ZMod p) (↑(↑z.val : ℤ) : ZMod p) (↑((↑p : ℤ) * k) : ZMod p) = z
mpr₁ : (↑(↑z.val : ℤ) : ZMod p) + HMul.hMul (α := ZMod p) (↑(↑p : ℤ) : ZMod p) (↑k : ZMod p) = z
mpr₂ : (↑z.val : ZMod p) + HMul.hMul (α := ZMod p) (↑(↑p : ℤ) : ZMod p) (↑k : ZMod p) = z
mpr₃ : (↑z.val : ZMod p) + HMul.hMul (α := ZMod p) (↑p : ZMod p) (↑k : ZMod p) = z
mpr₄ : z.cast + HMul.hMul (α := ZMod p) (↑p : ZMod p) (↑k : ZMod p) = z
⊢ (↑((↑z.val : ℤ) + (↑p : ℤ) * k) : ZMod p) = z
have mpr₅ : z.cast + HMul.hMul (α := ZMod p) 0 (↑k : ZMod p) = z
Tactic: rw [Int.cast_add, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_val,
      ZMod.natCast_self, zero_mul, add_zero, cast_id]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
z : ZMod p
inst : NeZero p
k : ℤ
mpr : HAdd.hAdd (α := ZMod p) (↑(↑z.val : ℤ) : ZMod p) (↑((↑p : ℤ) * k) : ZMod p) = z
mpr₁ : (↑(↑z.val : ℤ) : ZMod p) + HMul.hMul (α := ZMod p) (↑(↑p : ℤ) : ZMod p) (↑k : ZMod p) = z
mpr₂ : (↑z.val : ZMod p) + HMul.hMul (α := ZMod p) (↑(↑p : ℤ) : ZMod p) (↑k : ZMod p) = z
mpr₃ : (↑z.val : ZMod p) + HMul.hMul (α := ZMod p) (↑p : ZMod p) (↑k : ZMod p) = z
mpr₄ : z.cast + HMul.hMul (α := ZMod p) (↑p : ZMod p) (↑k : ZMod p) = z
mpr₅ : z.cast + HMul.hMul (α := ZMod p) 0 (↑k : ZMod p) = z
⊢ (↑((↑z.val : ℤ) + (↑p : ℤ) * k) : ZMod p) = z
have mpr₆ : HAdd.hAdd (α := ZMod p) z.cast 0 = z
Tactic: rw [Int.cast_add, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_val,
      ZMod.natCast_self, zero_mul, add_zero, cast_id]