awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n a : ℕ
h : a < n
rw : a % n = a
rw₁ rw₂ : a = a
⊢ val (n := n) (↑a : ZMod n) = a

Tactic:
rw [val_natCast, Nat.mod_eq_of_lt h]

Premises used: Nat.mod_eq_of_lt, ZMod.val_natCast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m : ℕ
inst : NeZero m
n : ℕ
inst_1 : NeZero n
a : ZMod m
obtain : ∀ (m : ℕ) [NeZero (m + 1)] (a : ZMod (m + 1)), val (n := n) a.cast < m + 1
⊢ val (n := n) a.cast < m

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne m)

Premises used: Nat.exists_eq_add_one_of_ne_zero, rfl, NeZero.ne
-- Module: Mathlib.Data.ZMod.Basic
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
neg : ∀ (h : n ≤ m), val (n := n) a.cast < m + 1
⊢ val (n := n) a.cast < m + 1

Tactic:
by_cases! h : m < n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
m : ℕ
inst_1 : NeZero (m + 1)
a : ZMod (m + 1)
h : m < n
pos : ∀ (n : ℕ) [NeZero (n + 1)] (h : m < n + 1), val (n := n + 1) a.cast < m + 1
⊢ val (n := n) a.cast < m + 1

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne n)

Premises used: Nat.exists_eq_add_one_of_ne_zero, rfl, NeZero.ne
-- Module: Mathlib.Data.ZMod.Basic
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
pos₁ : a.val < n + 1
⊢ val (n := n + 1) a.cast < m + 1

Tactic:
rw [← natCast_val, val_cast_of_lt]

Premises used: ZMod.val_cast_of_lt, ZMod.natCast_val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m : ℕ
inst : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst_1 : NeZero (n + 1)
h : m < n + 1
⊢ a.val < m + 1

Tactic:
apply a.val_lt

Premises used: ZMod.val_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m : ℕ
inst : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst_1 : NeZero (n + 1)
h : m < n + 1
⊢ a.val < n + 1

Tactic:
apply lt_of_le_of_lt (Nat.le_of_lt_succ (ZMod.val_lt a)) h

Premises used: lt_of_le_of_lt, Nat.le_of_lt_succ, ZMod.val_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
m : ℕ
inst_1 : NeZero (m + 1)
a : ZMod (m + 1)
h : n ≤ m
⊢ val (n := n) a.cast < m + 1

Tactic:
apply lt_of_lt_of_le (ZMod.val_lt _) (le_trans h (Nat.le_succ m))

Premises used: Nat.le_succ, ZMod.val_lt, lt_of_lt_of_le, le_trans
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
rw rw₁ : (-a).val = (-a).val
⊢ (-a).val = (-a).val % n

Tactic:
rw [Nat.mod_eq_of_lt (-a).val_lt]

Premises used: Nat.mod_eq_of_lt, ZMod.val_lt, Neg.neg
-- Module: Mathlib.Data.ZMod.Basic
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
rw₅ rw₆ : Eq (α := ℕ) 0 0
⊢ (-a).val + a.val ≡ n - a.val + a.val [MOD n]

Tactic:
rw [Nat.ModEq, ← val_add, neg_add_cancel, tsub_add_cancel_of_le a.val_le, Nat.mod_self,
            val_zero]

Premises used: Nat.mod_self, ZMod.val_add, tsub_add_cancel_of_le, ZMod.val_zero, Nat.ModEq, neg_add_cancel, ZMod.val_le
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
rw : (n - a.val) % n = if a = 0 then 0 else n - a.val
⊢ (-a).val = if a = 0 then 0 else n - a.val

Tactic:
rw [neg_val']

Premises used: ZMod.neg_val'
-- Module: Mathlib.Data.ZMod.Basic
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
neg : ∀ (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

Tactic:
by_cases h : a = 0
-- Module: Mathlib.Data.ZMod.Basic
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
pos₄ pos₅ : Eq (α := ℕ) 0 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

Tactic:
rw [if_pos h, h, val_zero, tsub_zero, Nat.mod_self]

Premises used: Nat.mod_self, if_pos, ZMod.val_zero, tsub_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
h : ¬a = 0
neg : (n - a.val) % n = n - a.val
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

Tactic:
rw [if_neg h]

Premises used: if_neg
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
h : ¬a = 0
neg : n - a.val < n
⊢ (n - a.val) % n = n - a.val

Tactic:
apply Nat.mod_eq_of_lt

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
h : ¬a = 0
⊢ n - a.val < n

Tactic:
Nat.sub_lt (NeZero.pos n) (val_pos.mpr h)

Premises used: Iff.mpr, Nat.sub_lt, NeZero.pos, ZMod.val_pos
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
h : ¬a = 0
⊢ n - a.val < n

Tactic:
exact Nat.sub_lt (NeZero.pos n) (val_pos.mpr h)

Premises used: Iff.mpr, Nat.sub_lt, NeZero.pos, ZMod.val_pos
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
nz : NeZero n
a : ZMod n
na : NeZero a
⊢ (-a).val = n - a.val

Tactic:
simp_all [neg_val a, na.out]

Premises used: ZMod.neg_val, NeZero.out
-- Module: Mathlib.Data.ZMod.Basic
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
neg : ∀ (hb : ¬b = 0), (a - b).val = a.val - b.val
⊢ (a - b).val = a.val - b.val

Tactic:
by_cases hb : b = 0
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : b = 0
pos : ∀ (h : val (n := n) 0 ≤ a.val), (a - 0).val = a.val - val (n := n) 0
⊢ (a - b).val = a.val - b.val

Tactic:
cases hb
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
h : val (n := n) 0 ≤ a.val
⊢ (a - 0).val = a.val - val (n := n) 0

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
⊢ NeZero b

Tactic:
have : NeZero b := ⟨hb⟩
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
neg : (a.val - b.val) % n = a.val - b.val
⊢ (a - b).val = 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]

Premises used: Nat.add_sub_assoc, sub_eq_add_neg, ZMod.val_add, le_of_lt, ZMod.val_neg_of_ne_zero, add_comm, Nat.add_mod_left, ZMod.val_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (a.val - b.val) % n = a.val - b.val

Tactic:
apply Nat.mod_eq_of_lt (tsub_lt_of_lt (val_lt _))

Premises used: Nat.mod_eq_of_lt, tsub_lt_of_lt, ZMod.val_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
nzm : NeZero m
a : ZMod m
h : a.val < n
obtain : ∀ (m : ℕ) [nzm : NeZero (m + 1)] {a : ZMod (m + 1)} (h : a.val < n), val (n := n) a.cast = a.val
⊢ val (n := n) a.cast = a.val

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne m)

Premises used: Nat.exists_eq_add_one_of_ne_zero, rfl, NeZero.ne
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
h : a.val < 0
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
h : a.val < n
obtain : ∀ (n : ℕ) (h : a.val < n + 1), val (n := n + 1) a.cast = a.val
⊢ val (n := n) a.cast = a.val

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero <| by rintro (rfl : n = 0); simp at h

Premises used: Nat.exists_eq_add_one_of_ne_zero, rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
h : a.val < n + 1
⊢ val (n := n + 1) a.cast = a.val

Tactic:
Fin.val_cast_of_lt h

Premises used: ZMod, Fin.val_cast_of_lt, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
h : a.val < n + 1
⊢ val (n := n + 1) a.cast = a.val

Tactic:
exact Fin.val_cast_of_lt h

Premises used: Fin.val_cast_of_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
⊢ NeZero n

Tactic:
have : NeZero n := ⟨((Nat.zero_lt_of_ne_zero hm.out).trans_le h).ne'⟩
-- Module: Mathlib.Data.ZMod.Basic
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
rw₂ rw₃ : a = a
⊢ cast (n := n) a.cast = a

Tactic:
rw [cast_eq_val, val_cast_eq_val_of_lt (a.val_lt.trans_le h), natCast_zmod_val]

Premises used: ZMod.cast_eq_val, ZMod.natCast_zmod_val, LT.lt.trans_le, ZMod.val_cast_eq_val_of_lt, ZMod.val_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
h : HPow.hPow (β := ℕ) a.val 0 < n
⊢ (HPow.hPow (β := ℕ) a 0).val = HPow.hPow (β := ℕ) a.val 0

Tactic:
simp [ZMod.val_one]

Premises used: ZMod.val_one
-- Module: Mathlib.Data.ZMod.Basic
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
inr : ∀ (ha : a ≠ 0), a.val ^ m < n
⊢ a.val ^ m < n

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ZMod.Basic
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
neg : ∀ (hm : ¬m = 0), val (n := n) 0 ^ m < n
⊢ val (n := n) 0 ^ m < n

Tactic:
by_cases hm : m = 0
-- Module: Mathlib.Data.ZMod.Basic
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
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
⊢ val (n := n) 0 ^ m < n

Tactic:
cases hm
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
ilt : Fact (1 < n)
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:
simp [ilt.out]

Premises used: Fact.out
-- Module: Mathlib.Data.ZMod.Basic
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

Tactic:
simp only [val_zero, ne_eq, hm, not_false_eq_true, zero_pow, Nat.zero_lt_of_lt h]

Premises used: Nat.zero_lt_of_lt, ZMod.val_zero, ne_eq, not_false_eq_true, zero_pow
-- Module: Mathlib.Data.ZMod.Basic
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
rwa : 0 < a.val
rwa₁ rwa₂ rwa₃ rwa₄ : a ≠ 0
⊢ a.val > 0

Tactic:
rwa [gt_iff_lt, ZMod.val_pos]

Premises used: gt_iff_lt, ZMod.val_pos
-- Module: Mathlib.Data.ZMod.Basic
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 ^ m < n

Tactic:
exact lt_of_le_of_lt
         (Nat.pow_le_pow_right (by rwa [gt_iff_lt, ZMod.val_pos]) (Nat.le_succ m)) h

Premises used: lt_of_le_of_lt, Nat.le_succ, Nat.pow_le_pow_right
-- Module: Mathlib.Data.ZMod.Basic
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

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
-- Module: Mathlib.Data.ZMod.Basic
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)
succ₄ succ₅ : a.val ^ (m + 1) = a.val ^ (m + 1)
⊢ (a ^ (m + 1)).val = a.val ^ (m + 1)

Tactic:
rw [pow_succ, ZMod.val_mul, ih this, ← pow_succ, Nat.mod_eq_of_lt h]

Premises used: pow_succ, ZMod.val_mul, Nat.mod_eq_of_lt
-- Module: Mathlib.Data.ZMod.Basic
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
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)
⊢ (a ^ m).val = a.val ^ m

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]

Premises used: pow_succ, ZMod.val_mul, Nat.mod_eq_of_lt, ZMod.val_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : Fact (1 < n)
a : ZMod n
⊢ (HPow.hPow (β := ℕ) a 0).val ≤ HPow.hPow (β := ℕ) a.val 0

Tactic:
simp [ZMod.val_one]

Premises used: ZMod.val_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
succ : (a ^ m * a).val ≤ a.val ^ m * a.val
⊢ (a ^ (m + 1)).val ≤ a.val ^ (m + 1)

Tactic:
rw [pow_succ, pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
succ : (a ^ m).val * a.val ≤ a.val ^ m * a.val
⊢ (a ^ m * a).val ≤ a.val ^ m * a.val

Tactic:
apply le_trans (ZMod.val_mul_le _ _)

Premises used: ZMod.val_mul_le, le_trans
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
⊢ (a ^ m).val * a.val ≤ a.val ^ m * a.val

Tactic:
apply Nat.mul_le_mul_right _ ih

Premises used: Nat.mul_le_mul_right
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
inst : Fact (1 < n)
a : ZMod n
zero : (HPow.hPow (β := ℕ) a 0).val ≤ HPow.hPow (β := ℕ) a.val 0
succ : ∀ (m : ℕ) (ih : (a ^ m).val ≤ a.val ^ m), (a ^ (m + 1)).val ≤ a.val ^ (m + 1)
⊢ (a ^ m).val ≤ a.val ^ m

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

Premises used: pow_succ, ZMod.val_mul_le, ZMod.val_one, le_trans
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x y : ℤ
he : Eq (α := ZMod n) (↑x : ZMod n) (↑y : ZMod n)
hl : x.natAbs ≤ n / 2
⊢ (↑n : ℤ) ∣ y - x

Tactic:
rw [intCast_eq_intCast_iff_dvd_sub] at he

Premises used: ZMod.intCast_eq_intCast_iff_dvd_sub
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x y : ℤ
he : Eq (α := ZMod n) (↑x : ZMod n) (↑y : ZMod n)
hl : x.natAbs ≤ n / 2
he₁ : (↑n : ℤ) ∣ y - x
⊢ x.natAbs ≤ n / 2

Tactic:
rw [intCast_eq_intCast_iff_dvd_sub] at he

Premises used: ZMod.intCast_eq_intCast_iff_dvd_sub
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x y : ℤ
he : (↑n : ℤ) ∣ y - x
hl : x.natAbs ≤ n / 2
obtain : ∀ (m : ℤ) (he : y - x = (↑n : ℤ) * m), x.natAbs ≤ y.natAbs
⊢ x.natAbs ≤ y.natAbs

Tactic:
obtain ⟨m, he⟩ := he
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x y : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
he : y - x = (↑n : ℤ) * m
⊢ y = (↑n : ℤ) * m + x

Tactic:
rw [sub_eq_iff_eq_add] at he

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x y : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
he : y = (↑n : ℤ) * m + x
subst : x.natAbs ≤ ((↑n : ℤ) * m + x).natAbs
⊢ x.natAbs ≤ y.natAbs

Tactic:
subst he
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
inl : x.natAbs ≤ (HMul.hMul (α := ℤ) (↑n : ℤ) 0 + x).natAbs
inr : ∀ (hm : m ≠ 0), x.natAbs ≤ ((↑n : ℤ) * m + x).natAbs
⊢ x.natAbs ≤ ((↑n : ℤ) * m + x).natAbs

Tactic:
obtain rfl | hm := eq_or_ne m 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
inl : x.natAbs ≤ (0 + x).natAbs
inl₁ inl₂ : x.natAbs ≤ x.natAbs
⊢ x.natAbs ≤ (HMul.hMul (α := ℤ) (↑n : ℤ) 0 + x).natAbs

Tactic:
rw [mul_zero, zero_add]

Premises used: zero_add, MulZeroClass.mul_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
inr : n / 2 ≤ ((↑n : ℤ) * m + x).natAbs
⊢ x.natAbs ≤ ((↑n : ℤ) * m + x).natAbs

Tactic:
apply hl.trans

Premises used: LE.le.trans
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
inr : n / 2 + x.natAbs ≤ ((↑n : ℤ) * m + x).natAbs + x.natAbs
⊢ n / 2 ≤ ((↑n : ℤ) * m + x).natAbs

Tactic:
rw [← add_le_add_iff_right x.natAbs]

Premises used: add_le_add_iff_right, Int.natAbs
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + x.natAbs ≤ ((↑n : ℤ) * m + x).natAbs + x.natAbs

Tactic:
le_trans (le_trans ((add_le_add_iff_left _).2 hl) ?_) (Int.natAbs_sub_le _ _)

Premises used: Iff.mpr, add_le_add_iff_left, Int.natAbs_sub_le, le_trans
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
inr : n / 2 + n / 2 ≤ ((↑n : ℤ) * m + x - x).natAbs
⊢ n / 2 + x.natAbs ≤ ((↑n : ℤ) * m + x).natAbs + x.natAbs

Tactic:
refine le_trans (le_trans ((add_le_add_iff_left _).2 hl) ?_) (Int.natAbs_sub_le _ _)

Premises used: Iff.mpr, add_le_add_iff_left, Int.natAbs_sub_le, le_trans
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
inr : n / 2 + n / 2 ≤ n * m.natAbs
⊢ n / 2 + n / 2 ≤ ((↑n : ℤ) * m + x - x).natAbs

Tactic:
rw [add_sub_cancel_right, Int.natAbs_mul, Int.natAbs_natCast]

Premises used: Int.natAbs_mul, Int.natAbs_natCast, add_sub_cancel_right
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ n * m.natAbs

Tactic:
le_trans ?_ (Nat.le_mul_of_pos_right _ <| Int.natAbs_pos.2 hm)

Premises used: Iff.mpr, Nat.le_mul_of_pos_right, Int.natAbs_pos, le_trans
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
inr : n / 2 + n / 2 ≤ n
⊢ n / 2 + n / 2 ≤ n * m.natAbs

Tactic:
refine le_trans ?_ (Nat.le_mul_of_pos_right _ <| Int.natAbs_pos.2 hm)

Premises used: Iff.mpr, Nat.le_mul_of_pos_right, Int.natAbs_pos, le_trans
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
inr : n / 2 * 2 ≤ n
⊢ n / 2 + n / 2 ≤ n

Tactic:
rw [← mul_two]

Premises used: mul_two
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 * 2 ≤ n

Tactic:
apply Nat.div_mul_le_self

Premises used: Nat.div_mul_le_self
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : NonAssocSemiring R
f g : ZMod n →+* R
a : ∀ (a : ZMod n), Eq (α := R) ((f : (a : ZMod n) → R) a : R) ((g : (a : ZMod n) → R) a : R)
⊢ f = g

Tactic:
ext a
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : NonAssocSemiring R
f g : ZMod n →+* R
a : ZMod n
a₁ : ∀ (k : ℤ), Eq (α := R) ((f : (a : ZMod n) → R) (↑k : ZMod n) : R) ((g : (a : ZMod n) → R) (↑k : ZMod n) : R)
⊢ Eq (α := R) ((f : (a : ZMod n) → R) a : R) ((g : (a : ZMod n) → R) a : R)

Tactic:
obtain ⟨k, rfl⟩ := ZMod.intCast_surjective a

Premises used: ZMod.intCast_surjective, rfl
-- Module: Mathlib.Data.ZMod.Basic
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))
a : Eq (α := R) ((φ : (a : ℤ) → R) k : R) ((ψ : (a : ℤ) → R) k : R)
⊢ Eq (α := R) ((f : (a : ZMod n) → R) (↑k : ZMod n) : R) ((g : (a : ZMod n) → R) (↑k : ZMod n) : R)

Tactic:
change φ k = ψ k

Premises used: DFunLike.coe
-- Module: Mathlib.Data.ZMod.Basic
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))
a a₁ : Eq (α := R) ((ψ : (a : ℤ) → R) k : R) ((ψ : (a : ℤ) → R) k : R)
⊢ Eq (α := R) ((φ : (a : ℤ) → R) k : R) ((ψ : (a : ℤ) → R) k : R)

Tactic:
rw [φ.ext_int ψ]

Premises used: RingHom.ext_int
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Semiring R
⊢ Subsingleton.{max (u_1 + 1) 1} (ZMod n →+* R)

Tactic:
⟨RingHom.ext_zmod⟩

Premises used: RingHom.ext_zmod, Subsingleton.intro
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Semiring R
f g : ZMod n ≃+* R
rw : Eq (α := ZMod n →+* R) (↑f : ZMod n →+* R) (↑g : ZMod n →+* R)
⊢ f = g

Tactic:
rw [RingEquiv.coe_ringHom_inj_iff]

Premises used: RingEquiv.coe_ringHom_inj_iff
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Semiring R
f g : ZMod n ≃+* R
⊢ Eq (α := ZMod n →+* R) (↑f : ZMod n →+* R) (↑g : ZMod n →+* R)

Tactic:
apply RingHom.ext_zmod _ _

Premises used: RingHom.ext_zmod
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : NonAssocRing R
f : R →+* ZMod n
k : ZMod n
zero : ∀ (f : R →+* ZMod 0) (k : ZMod 0), (f : (a : R) → ZMod 0) k.cast = k
succ : ∀ (n : ℕ) (f : R →+* ZMod (n + 1)) (k : ZMod (n + 1)), (f : (a : R) → ZMod (n + 1)) k.cast = k
⊢ (f : (a : R) → ZMod n) k.cast = k

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : NonAssocRing R
f : R →+* ZMod 0
k : ZMod 0
zero : (f : (a : R) → ℤ) (↑k : R) = k
⊢ (f : (a : R) → ZMod 0) k.cast = k

Tactic:
dsimp +instances [ZMod, ZMod.cast] at f k ⊢

Premises used: ZMod.cast, ZMod
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : NonAssocRing R
f : R →+* ℤ
k : ℤ
⊢ (f : (a : R) → ℤ) (↑k : R) = k

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : NonAssocRing R
n : ℕ
f : R →+* ZMod (n + 1)
k : ZMod (n + 1)
succ : (f : (a : R) → ZMod (n + 1)) (↑k.val : R) = k
⊢ (f : (a : R) → ZMod (n + 1)) k.cast = k

Tactic:
dsimp [ZMod.cast]

Premises used: ZMod.cast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : NonAssocRing R
n : ℕ
f : R →+* ZMod (n + 1)
k : ZMod (n + 1)
succ : (↑k.val : ZMod (n + 1)) = k
succ₁ succ₂ : k = k
⊢ (f : (a : R) → ZMod (n + 1)) (↑k.val : R) = k

Tactic:
rw [map_natCast, natCast_zmod_val]

Premises used: ZMod.natCast_zmod_val, map_natCast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : NonAssocRing R
f : R →+* ZMod n
⊢ RightInverse (α := R) (β := ZMod n) cast (⇑f : (a : R) → ZMod n)

Tactic:
ringHom_map_cast f

Premises used: Function.LeftInverse, ZMod.ringHom_map_cast, Function.RightInverse
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : NonAssocRing R
f : R →+* ZMod n
⊢ Surjective (α := R) (β := ZMod n) (⇑f : (a : R) → ZMod n)

Tactic:
(ringHom_rightInverse f).surjective

Premises used: ZMod.ringHom_rightInverse, Function.RightInverse.surjective
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ castHom ⋯ (ZMod n) = RingHom.id (ZMod n)

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n m d : ℕ
hm : n ∣ m
hd : m ∣ d
⊢ Eq (α := ZMod d →+* ZMod n) (RingHom.comp (castHom hm (ZMod n)) (castHom hd (ZMod m))) (castHom ⋯ (ZMod n))

Tactic:
RingHom.ext_zmod _ _

Premises used: RingHom.ext_zmod
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
A : Type u_2
inst : AddGroup A
f : ℤ →+ A
rw : Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A) ↔ AddSubgroup.zmultiples (↑n : ℤ) ≤ f.ker
⊢ Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A) ↔
    AddMonoidHom.ker (M := ZMod n) (Int.castAddHom (ZMod n)) ≤ f.ker

Tactic:
rw [ker_intCastAddHom]

Premises used: ZMod.ker_intCastAddHom
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
A : Type u_2
inst : AddGroup A
f : ℤ →+ A
mp : Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A) → AddSubgroup.zmultiples (↑n : ℤ) ≤ f.ker
mpr : AddSubgroup.zmultiples (↑n : ℤ) ≤ f.ker → Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A)
⊢ Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A) ↔ AddSubgroup.zmultiples (↑n : ℤ) ≤ f.ker

Tactic:
constructor