awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
n_1 : ℕ
he : 2 * a.val = (n + 1) * (n_1 + 1 + 1)
⊢ (n + 1) * 2 ≤ (n + 1) * (n_1 + 1 + 1)
have succ : 2 ≤ n_1 + 1 + 1
Tactic: apply Nat.mul_le_mul_left
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
h : 2 * a.val = n + 1
⊢ n + 1 ∣ 2 * a.val
have succ : n + 1 ∣ n + 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n a : ℕ
h : a < n
⊢ val (n := n) (↑a : ZMod n) = a
have rw : a % n = a
Tactic: rw [val_natCast, Nat.mod_eq_of_lt h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n a : ℕ
h : a < n
rw : a % n = a
⊢ val (n := n) (↑a : ZMod n) = a
have rw₁ : a = a
Tactic: rw [val_natCast, Nat.mod_eq_of_lt h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m : ℕ
inst : NeZero m
n : ℕ
inst_1 : NeZero n
a : ZMod m
⊢ val (n := n) a.cast < m
have obtain : ∀ (m : ℕ) [NeZero (m + 1)] (a : ZMod (m + 1)), val (n := n) a.cast < m + 1
Tactic: obtain ⟨m, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne m)
Cleared hypotheses: m, inst, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
m : ℕ
inst_1 : NeZero (m + 1)
a : ZMod (m + 1)
⊢ val (n := n) a.cast < m + 1
have pos : ∀ (h : m < n), val (n := n) a.cast < m + 1
Tactic: by_cases! h : m < n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
m : ℕ
inst_1 : NeZero (m + 1)
a : ZMod (m + 1)
pos : ∀ (h : m < n), val (n := n) a.cast < m + 1
⊢ val (n := n) a.cast < m + 1
have neg : ∀ (h : n ≤ m), val (n := n) a.cast < m + 1
Tactic: by_cases! h : m < n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
m : ℕ
inst_1 : NeZero (m + 1)
a : ZMod (m + 1)
h : m < n
⊢ val (n := n) a.cast < m + 1
have pos : ∀ (n : ℕ) [NeZero (n + 1)] (h : m < n + 1), val (n := n + 1) a.cast < m + 1
Tactic: obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne n)
Cleared hypotheses: n, inst, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m : ℕ
inst : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst_1 : NeZero (n + 1)
h : m < n + 1
⊢ val (n := n + 1) a.cast < m + 1
have pos : a.val < m + 1
Tactic: rw [← natCast_val, val_cast_of_lt]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m : ℕ
inst : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst_1 : NeZero (n + 1)
h : m < n + 1
pos : a.val < m + 1
⊢ val (n := n + 1) a.cast < m + 1
have pos₁ : a.val < n + 1
Tactic: rw [← natCast_val, val_cast_of_lt]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
⊢ (-a).val = (-a).val % n
have rw : (-a).val = (-a).val
Tactic: rw [Nat.mod_eq_of_lt (-a).val_lt]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
⊢ (-a).val + a.val ≡ n - a.val + a.val [MOD n]
have rw : ((-a).val + a.val) % n = (n - a.val + a.val) % n
Tactic: rw [Nat.ModEq, ← val_add, neg_add_cancel, tsub_add_cancel_of_le a.val_le, Nat.mod_self,
            val_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
rw : ((-a).val + a.val) % n = (n - a.val + a.val) % n
⊢ (-a).val + a.val ≡ n - a.val + a.val [MOD n]
have rw₁ : (-a + a).val = (n - a.val + a.val) % n
Tactic: rw [Nat.ModEq, ← val_add, neg_add_cancel, tsub_add_cancel_of_le a.val_le, Nat.mod_self,
            val_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
rw : ((-a).val + a.val) % n = (n - a.val + a.val) % n
rw₁ : (-a + a).val = (n - a.val + a.val) % n
⊢ (-a).val + a.val ≡ n - a.val + a.val [MOD n]
have rw₂ : val (n := n) 0 = (n - a.val + a.val) % n
Tactic: rw [Nat.ModEq, ← val_add, neg_add_cancel, tsub_add_cancel_of_le a.val_le, Nat.mod_self,
            val_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
rw : ((-a).val + a.val) % n = (n - a.val + a.val) % n
rw₁ : (-a + a).val = (n - a.val + a.val) % n
rw₂ : val (n := n) 0 = (n - a.val + a.val) % n
⊢ (-a).val + a.val ≡ n - a.val + a.val [MOD n]
have rw₃ : val (n := n) 0 = n % n
Tactic: rw [Nat.ModEq, ← val_add, neg_add_cancel, tsub_add_cancel_of_le a.val_le, Nat.mod_self,
            val_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
rw : ((-a).val + a.val) % n = (n - a.val + a.val) % n
rw₁ : (-a + a).val = (n - a.val + a.val) % n
rw₂ : val (n := n) 0 = (n - a.val + a.val) % n
rw₃ : val (n := n) 0 = n % n
⊢ (-a).val + a.val ≡ n - a.val + a.val [MOD n]
have rw₄ : val (n := n) 0 = 0
Tactic: rw [Nat.ModEq, ← val_add, neg_add_cancel, tsub_add_cancel_of_le a.val_le, Nat.mod_self,
            val_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
rw : ((-a).val + a.val) % n = (n - a.val + a.val) % n
rw₁ : (-a + a).val = (n - a.val + a.val) % n
rw₂ : val (n := n) 0 = (n - a.val + a.val) % n
rw₃ : val (n := n) 0 = n % n
rw₄ : val (n := n) 0 = 0
⊢ (-a).val + a.val ≡ n - a.val + a.val [MOD n]
have rw₅ : Eq (α := ℕ) 0 0
Tactic: rw [Nat.ModEq, ← val_add, neg_add_cancel, tsub_add_cancel_of_le a.val_le, Nat.mod_self,
            val_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
⊢ (-a).val = if a = 0 then 0 else n - a.val
have rw : (n - a.val) % n = if a = 0 then 0 else n - a.val
Tactic: rw [neg_val']
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val
have pos : ∀ (h : a = 0), (n - a.val) % n = if a = 0 then 0 else n - a.val
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
pos : ∀ (h : a = 0), (n - a.val) % n = if a = 0 then 0 else n - a.val
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val
have neg : ∀ (h : ¬a = 0), (n - a.val) % n = if a = 0 then 0 else n - a.val
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
h : a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val
have pos : (n - a.val) % n = 0
Tactic: rw [if_pos h, h, val_zero, tsub_zero, Nat.mod_self]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
h : a = 0
pos : (n - a.val) % n = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val
have pos₁ : (n - val (n := n) 0) % n = 0
Tactic: rw [if_pos h, h, val_zero, tsub_zero, Nat.mod_self]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
h : a = 0
pos : (n - a.val) % n = 0
pos₁ : (n - val (n := n) 0) % n = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val
have pos₂ : (n - 0) % n = 0
Tactic: rw [if_pos h, h, val_zero, tsub_zero, Nat.mod_self]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
h : a = 0
pos : (n - a.val) % n = 0
pos₁ : (n - val (n := n) 0) % n = 0
pos₂ : (n - 0) % n = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val
have pos₃ : n % n = 0
Tactic: rw [if_pos h, h, val_zero, tsub_zero, Nat.mod_self]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
h : a = 0
pos : (n - a.val) % n = 0
pos₁ : (n - val (n := n) 0) % n = 0
pos₂ : (n - 0) % n = 0
pos₃ : n % n = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val
have pos₄ : Eq (α := ℕ) 0 0
Tactic: rw [if_pos h, h, val_zero, tsub_zero, Nat.mod_self]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val
have neg : (n - a.val) % n = n - a.val
Tactic: rw [if_neg h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = n - a.val
have neg : n - a.val < n
Tactic: apply Nat.mod_eq_of_lt
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : b.val ≤ a.val
⊢ (a - b).val = a.val - b.val
have pos : ∀ (hb : b = 0), (a - b).val = a.val - b.val
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : b.val ≤ a.val
pos : ∀ (hb : b = 0), (a - b).val = a.val - b.val
⊢ (a - b).val = a.val - b.val
have neg : ∀ (hb : ¬b = 0), (a - b).val = a.val - b.val
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : b = 0
⊢ (a - b).val = a.val - b.val
have pos : ∀ (h : val (n := n) 0 ≤ a.val), (a - 0).val = a.val - val (n := n) 0
Tactic: cases hb
Cleared hypotheses: b, h, hb
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
⊢ (a - b).val = a.val - b.val
have this : NeZero b
Tactic: have : NeZero b := ⟨hb⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (a - b).val = a.val - b.val
have neg : (a.val - b.val) % n = a.val - b.val
Tactic: rw [sub_eq_add_neg, val_add, val_neg_of_ne_zero, ← Nat.add_sub_assoc (le_of_lt (val_lt _)),
      add_comm, Nat.add_sub_assoc h, Nat.add_mod_left]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
nzm : NeZero m
a : ZMod m
h : a.val < n
⊢ val (n := n) a.cast = a.val
have obtain : ∀ (m : ℕ) [nzm : NeZero (m + 1)] {a : ZMod (m + 1)} (h : a.val < n), val (n := n) a.cast = a.val
Tactic: obtain ⟨m, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne m)
Cleared hypotheses: m, nzm, a, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
h : a.val < n
⊢ val (n := n) a.cast = a.val
have obtain : ∀ (n : ℕ) (h : a.val < n + 1), val (n := n + 1) a.cast = a.val
Tactic: obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero <| by rintro (rfl : n = 0); simp at h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
⊢ cast (n := n) a.cast = a
have this : NeZero n
Tactic: have : NeZero n := ⟨((Nat.zero_lt_of_ne_zero hm.out).trans_le h).ne'⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
this : NeZero n
⊢ cast (n := n) a.cast = a
have rw : (↑(val (n := n) a.cast) : ZMod m) = a
Tactic: rw [cast_eq_val, val_cast_eq_val_of_lt (a.val_lt.trans_le h), natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
this : NeZero n
rw : (↑(val (n := n) a.cast) : ZMod m) = a
⊢ cast (n := n) a.cast = a
have rw₁ : (↑a.val : ZMod m) = a
Tactic: rw [cast_eq_val, val_cast_eq_val_of_lt (a.val_lt.trans_le h), natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
this : NeZero n
rw : (↑(val (n := n) a.cast) : ZMod m) = a
rw₁ : (↑a.val : ZMod m) = a
⊢ cast (n := n) a.cast = a
have rw₂ : a = a
Tactic: rw [cast_eq_val, val_cast_eq_val_of_lt (a.val_lt.trans_le h), natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : ∀ (h : a.val ^ m < n), (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
⊢ a.val ^ m < n
have inl : ∀ (ih : ∀ (h : val (n := n) 0 ^ m < n), (HPow.hPow (α := ZMod n) 0 m).val = val (n := n) 0 ^ m)
  (h : val (n := n) 0 ^ (m + 1) < n), val (n := n) 0 ^ m < n
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a, ih, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : ∀ (h : a.val ^ m < n), (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
inl :
  ∀ (ih : ∀ (h : val (n := n) 0 ^ m < n), (HPow.hPow (α := ZMod n) 0 m).val = val (n := n) 0 ^ m)
    (h : val (n := n) 0 ^ (m + 1) < n), val (n := n) 0 ^ m < n
⊢ a.val ^ m < n
have inr : ∀ (ha : a ≠ 0), a.val ^ m < n
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : ∀ (h : val (n := n) 0 ^ m < n), (HPow.hPow (α := ZMod n) 0 m).val = val (n := n) 0 ^ m
h : val (n := n) 0 ^ (m + 1) < n
⊢ val (n := n) 0 ^ m < n
have pos : ∀ (hm : m = 0), val (n := n) 0 ^ m < n
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : ∀ (h : val (n := n) 0 ^ m < n), (HPow.hPow (α := ZMod n) 0 m).val = val (n := n) 0 ^ m
h : val (n := n) 0 ^ (m + 1) < n
pos : ∀ (hm : m = 0), val (n := n) 0 ^ m < n
⊢ val (n := n) 0 ^ m < n
have neg : ∀ (hm : ¬m = 0), val (n := n) 0 ^ m < n
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : ∀ (h : val (n := n) 0 ^ m < n), (HPow.hPow (α := ZMod n) 0 m).val = val (n := n) 0 ^ m
h : val (n := n) 0 ^ (m + 1) < n
hm : m = 0
⊢ val (n := n) 0 ^ m < n
have pos : ∀
  (ih :
    ∀ (h : HPow.hPow (β := ℕ) (val (n := n) 0) 0 < n),
      (HPow.hPow (α := ZMod n) (β := ℕ) 0 0).val = HPow.hPow (β := ℕ) (val (n := n) 0) 0)
  (h : val (n := n) 0 ^ HAdd.hAdd (α := ℕ) 0 1 < n), HPow.hPow (β := ℕ) (val (n := n) 0) 0 < n
Tactic: cases hm
Cleared hypotheses: m, ih, h, hm
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : ∀ (h : a.val ^ m < n), (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
ha : a ≠ 0
⊢ a.val > 0
have rwa : 0 < a.val
Tactic: rwa [gt_iff_lt, ZMod.val_pos]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : ∀ (h : a.val ^ m < n), (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
⊢ (a ^ (m + 1)).val = a.val ^ (m + 1)
have this : a.val ^ m < n
Tactic: have : a.val ^ m < n := by
      obtain rfl | ha := eq_or_ne a 0
      · by_cases hm : m = 0
        · cases hm; simp [ilt.out]
        · simp only [val_zero, ne_eq, hm, not_false_eq_true, zero_pow, Nat.zero_lt_of_lt h]
      · exact lt_of_le_of_lt
         (Nat.pow_le_pow_right (by rwa [gt_iff_lt, ZMod.val_pos]) (Nat.le_succ m)) h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : ∀ (h : a.val ^ m < n), (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
this : a.val ^ m < n
⊢ (a ^ (m + 1)).val = a.val ^ (m + 1)
have succ : (a ^ m * a).val = a.val ^ (m + 1)
Tactic: rw [pow_succ, ZMod.val_mul, ih this, ← pow_succ, Nat.mod_eq_of_lt h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : ∀ (h : a.val ^ m < n), (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
this : a.val ^ m < n
succ : (a ^ m * a).val = a.val ^ (m + 1)
⊢ (a ^ (m + 1)).val = a.val ^ (m + 1)
have succ₁ : (a ^ m).val * a.val % n = a.val ^ (m + 1)
Tactic: rw [pow_succ, ZMod.val_mul, ih this, ← pow_succ, Nat.mod_eq_of_lt h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : ∀ (h : a.val ^ m < n), (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
this : a.val ^ m < n
succ : (a ^ m * a).val = a.val ^ (m + 1)
succ₁ : (a ^ m).val * a.val % n = a.val ^ (m + 1)
⊢ (a ^ (m + 1)).val = a.val ^ (m + 1)
have succ₂ : a.val ^ m * a.val % n = a.val ^ (m + 1)
Tactic: rw [pow_succ, ZMod.val_mul, ih this, ← pow_succ, Nat.mod_eq_of_lt h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : ∀ (h : a.val ^ m < n), (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
this : a.val ^ m < n
succ : (a ^ m * a).val = a.val ^ (m + 1)
succ₁ : (a ^ m).val * a.val % n = a.val ^ (m + 1)
succ₂ : a.val ^ m * a.val % n = a.val ^ (m + 1)
⊢ (a ^ (m + 1)).val = a.val ^ (m + 1)
have succ₃ : a.val ^ (m + 1) % n = a.val ^ (m + 1)
Tactic: rw [pow_succ, ZMod.val_mul, ih this, ← pow_succ, Nat.mod_eq_of_lt h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : ∀ (h : a.val ^ m < n), (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
this : a.val ^ m < n
succ : (a ^ m * a).val = a.val ^ (m + 1)
succ₁ : (a ^ m).val * a.val % n = a.val ^ (m + 1)
succ₂ : a.val ^ m * a.val % n = a.val ^ (m + 1)
succ₃ : a.val ^ (m + 1) % n = a.val ^ (m + 1)
⊢ (a ^ (m + 1)).val = a.val ^ (m + 1)
have succ₄ : a.val ^ (m + 1) = a.val ^ (m + 1)
Tactic: rw [pow_succ, ZMod.val_mul, ih this, ← pow_succ, Nat.mod_eq_of_lt h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
a : ZMod n
ilt : Fact (1 < n)
h : a.val ^ m < n
⊢ (a ^ m).val = a.val ^ m
have zero : ∀ (h : HPow.hPow (β := ℕ) a.val 0 < n), (HPow.hPow (β := ℕ) a 0).val = HPow.hPow (β := ℕ) a.val 0
Tactic: induction m with
  | zero => simp [ZMod.val_one]
  | succ m ih =>
    have : a.val ^ m < n := by
      obtain rfl | ha := eq_or_ne a 0
      · by_cases hm : m = 0
        · cases hm; simp [ilt.out]
        · simp only [val_zero, ne_eq, hm, not_false_eq_true, zero_pow, Nat.zero_lt_of_lt h]
      · exact lt_of_le_of_lt
         (Nat.pow_le_pow_right (by rwa [gt_iff_lt, ZMod.val_pos]) (Nat.le_succ m)) h
    rw [pow_succ, ZMod.val_mul, ih this, ← pow_succ, Nat.mod_eq_of_lt h]
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
a : ZMod n
ilt : Fact (1 < n)
h : a.val ^ m < n
zero : ∀ (h : HPow.hPow (β := ℕ) a.val 0 < n), (HPow.hPow (β := ℕ) a 0).val = HPow.hPow (β := ℕ) a.val 0
⊢ (a ^ m).val = a.val ^ m
have succ : ∀ (m : ℕ) (ih : ∀ (h : a.val ^ m < n), (a ^ m).val = a.val ^ m) (h : a.val ^ (m + 1) < n),
  (a ^ (m + 1)).val = a.val ^ (m + 1)
Tactic: induction m with
  | zero => simp [ZMod.val_one]
  | succ m ih =>
    have : a.val ^ m < n := by
      obtain rfl | ha := eq_or_ne a 0
      · by_cases hm : m = 0
        · cases hm; simp [ilt.out]
        · simp only [val_zero, ne_eq, hm, not_false_eq_true, zero_pow, Nat.zero_lt_of_lt h]
      · exact lt_of_le_of_lt
         (Nat.pow_le_pow_right (by rwa [gt_iff_lt, ZMod.val_pos]) (Nat.le_succ m)) h
    rw [pow_succ, ZMod.val_mul, ih this, ← pow_succ, Nat.mod_eq_of_lt h]
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
⊢ (a ^ (m + 1)).val ≤ a.val ^ (m + 1)
have succ : (a ^ m * a).val ≤ a.val ^ m * a.val
Tactic: rw [pow_succ, pow_succ]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
⊢ (a ^ m * a).val ≤ a.val ^ m * a.val
have succ : (a ^ m).val * a.val ≤ a.val ^ m * a.val
Tactic: apply le_trans (ZMod.val_mul_le _ _)
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
inst : Fact (1 < n)
a : ZMod n
⊢ (a ^ m).val ≤ a.val ^ m
have zero : (HPow.hPow (β := ℕ) a 0).val ≤ HPow.hPow (β := ℕ) a.val 0
Tactic: induction m with
  | zero => simp [ZMod.val_one]
  | succ m ih =>
    rw [pow_succ, pow_succ]
    apply le_trans (ZMod.val_mul_le _ _)
    apply Nat.mul_le_mul_right _ ih
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
inst : Fact (1 < n)
a : ZMod n
zero : (HPow.hPow (β := ℕ) a 0).val ≤ HPow.hPow (β := ℕ) a.val 0
⊢ (a ^ m).val ≤ a.val ^ m
have succ : ∀ (m : ℕ) (ih : (a ^ m).val ≤ a.val ^ m), (a ^ (m + 1)).val ≤ a.val ^ (m + 1)
Tactic: induction m with
  | zero => simp [ZMod.val_one]
  | succ m ih =>
    rw [pow_succ, pow_succ]
    apply le_trans (ZMod.val_mul_le _ _)
    apply Nat.mul_le_mul_right _ ih
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
x y : ℤ
he : Eq (α := ZMod n) (↑x : ZMod n) (↑y : ZMod n)
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ y.natAbs
have he₁ : (↑n : ℤ) ∣ y - x
Tactic: rw [intCast_eq_intCast_iff_dvd_sub] at he
Cleared hypotheses: he, hl
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x y : ℤ
he : (↑n : ℤ) ∣ y - x
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ y.natAbs
have obtain : ∀ (m : ℤ) (he : y - x = (↑n : ℤ) * m), x.natAbs ≤ y.natAbs
Tactic: obtain ⟨m, he⟩ := he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
x y : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
he : y - x = (↑n : ℤ) * m
⊢ x.natAbs ≤ y.natAbs
have he₁ : y = (↑n : ℤ) * m + x
Tactic: rw [sub_eq_iff_eq_add] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x y : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
he : y = (↑n : ℤ) * m + x
⊢ x.natAbs ≤ y.natAbs
have subst : x.natAbs ≤ ((↑n : ℤ) * m + x).natAbs
Tactic: subst he
Cleared hypotheses: y, he
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
⊢ x.natAbs ≤ ((↑n : ℤ) * m + x).natAbs
have inl : x.natAbs ≤ (HMul.hMul (α := ℤ) (↑n : ℤ) 0 + x).natAbs
Tactic: obtain rfl | hm := eq_or_ne m 0
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
inl : x.natAbs ≤ (HMul.hMul (α := ℤ) (↑n : ℤ) 0 + x).natAbs
⊢ x.natAbs ≤ ((↑n : ℤ) * m + x).natAbs
have inr : ∀ (hm : m ≠ 0), x.natAbs ≤ ((↑n : ℤ) * m + x).natAbs
Tactic: obtain rfl | hm := eq_or_ne m 0
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ (HMul.hMul (α := ℤ) (↑n : ℤ) 0 + x).natAbs
have inl : x.natAbs ≤ (0 + x).natAbs
Tactic: rw [mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
inl : x.natAbs ≤ (0 + x).natAbs
⊢ x.natAbs ≤ (HMul.hMul (α := ℤ) (↑n : ℤ) 0 + x).natAbs
have inl₁ : x.natAbs ≤ x.natAbs
Tactic: rw [mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ x.natAbs ≤ ((↑n : ℤ) * m + x).natAbs
have inr : n / 2 ≤ ((↑n : ℤ) * m + x).natAbs
Tactic: apply hl.trans
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 ≤ ((↑n : ℤ) * m + x).natAbs
have inr : n / 2 + x.natAbs ≤ ((↑n : ℤ) * m + x).natAbs + x.natAbs
Tactic: rw [← add_le_add_iff_right x.natAbs]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + x.natAbs ≤ ((↑n : ℤ) * m + x).natAbs + x.natAbs
have inr : n / 2 + n / 2 ≤ ((↑n : ℤ) * m + x - x).natAbs
Tactic: refine le_trans (le_trans ((add_le_add_iff_left _).2 hl) ?_) (Int.natAbs_sub_le _ _)
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ ((↑n : ℤ) * m + x - x).natAbs
have inr : n / 2 + n / 2 ≤ n * m.natAbs
Tactic: rw [add_sub_cancel_right, Int.natAbs_mul, Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ n * m.natAbs
have inr : n / 2 + n / 2 ≤ n
Tactic: refine le_trans ?_ (Nat.le_mul_of_pos_right _ <| Int.natAbs_pos.2 hm)
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ n
have inr : n / 2 * 2 ≤ n
Tactic: rw [← mul_two]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : NonAssocSemiring R
f g : ZMod n →+* R
⊢ f = g
have a : ∀ (a : ZMod n), Eq (α := R) ((f : (a : ZMod n) → R) a : R) ((g : (a : ZMod n) → R) a : R)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : NonAssocSemiring R
f g : ZMod n →+* R
a : ZMod n
⊢ Eq (α := R) ((f : (a : ZMod n) → R) a : R) ((g : (a : ZMod n) → R) a : R)
have a₁ : ∀ (k : ℤ), Eq (α := R) ((f : (a : ZMod n) → R) (↑k : ZMod n) : R) ((g : (a : ZMod n) → R) (↑k : ZMod n) : R)
Tactic: obtain ⟨k, rfl⟩ := ZMod.intCast_surjective a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : NonAssocSemiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))
ψ : ℤ →+* R := g.comp (Int.castRingHom (ZMod n))
⊢ Eq (α := R) ((f : (a : ZMod n) → R) (↑k : ZMod n) : R) ((g : (a : ZMod n) → R) (↑k : ZMod n) : R)
have a : Eq (α := R) ((φ : (a : ℤ) → R) k : R) ((ψ : (a : ℤ) → R) k : R)
Tactic: change φ k = ψ k