awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ZMod.Basic
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
neg₁ neg₂ : HSub.hSub (α := R) (↑k : R) 1 = HSub.hSub (α := R) (↑k : R) 1
⊢ (↑(k - 1) : R) = HSub.hSub (α := R) (↑k : R) 1

Tactic:
rw [Int.cast_sub, Int.cast_one]

Premises used: Int.cast_sub, Int.cast_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod (n + 1)
hk : ¬k = 0
neg : (↑(↑(k - 1) : ℕ) : R) = HSub.hSub (α := R) (↑(↑k : ℕ) : R) 1
⊢ (k - 1).cast = HSub.hSub (α := R) k.cast 1

Tactic:
dsimp [ZMod, ZMod.cast, ZMod.val]

Premises used: ZMod.cast, ZMod, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod (n + 1)
hk : ¬k = 0
neg : (↑((↑k : ℕ) - 1) : R) = HSub.hSub (α := R) (↑(↑k : ℕ) : R) 1
neg₁ : ¬k = 0
⊢ (↑(↑(k - 1) : ℕ) : R) = HSub.hSub (α := R) (↑(↑k : ℕ) : R) 1

Tactic:
rw [Fin.coe_sub_one, if_neg]

Premises used: Fin.coe_sub_one, if_neg
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod (n + 1)
hk : ¬k = 0
neg : 1 ≤ (↑k : ℕ)
⊢ (↑((↑k : ℕ) - 1) : R) = HSub.hSub (α := R) (↑(↑k : ℕ) : R) 1

Tactic:
rw [Nat.cast_sub, Nat.cast_one]

Premises used: Nat.cast_sub, Nat.cast_one
-- Module: Mathlib.Data.ZMod.Basic
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 : ℕ)
neg₃ neg₄ neg₅ neg₆ : ∀ (hk : 1 ≤ (↑k : ℕ)), 1 ≤ (↑k : ℕ)
⊢ 1 ≤ (↑k : ℕ)

Tactic:
rwa [Fin.ext_iff, Fin.val_zero, ← Ne, ← Nat.one_le_iff_ne_zero] at hk

Premises used: Fin.ext_iff, Ne, Nat.one_le_iff_ne_zero, Fin.val_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod (n + 1)
hk : ¬k = 0
⊢ ¬k = 0

Tactic:
hk

Premises used: ZMod
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
n : ℕ
k : ZMod (n + 1)
hk : ¬k = 0
⊢ ¬k = 0

Tactic:
exact hk
-- Module: Mathlib.Data.ZMod.Basic
Goal:
p n : ℕ
z : ZMod p
inst : NeZero p
mp : (↑n : ZMod p) = z → ∃ (k : ℕ), n = z.val + p * k
mpr : (∃ (k : ℕ), n = z.val + p * k) → (↑n : ZMod p) = z
⊢ (↑n : ZMod p) = z ↔ ∃ (k : ℕ), n = z.val + p * k

Tactic:
constructor
-- Module: Mathlib.Data.ZMod.Basic
Goal:
p n : ℕ
inst : NeZero p
⊢ ∃ (k : ℕ), n = val (n := p) (↑n : ZMod p) + p * k

Tactic:
⟨n / p, ?_⟩

Premises used: HDiv.hDiv, Exists.intro
-- Module: Mathlib.Data.ZMod.Basic
Goal:
p n : ℕ
inst : NeZero p
mp : n = val (n := p) (↑n : ZMod p) + p * (n / p)
⊢ ∃ (k : ℕ), n = val (n := p) (↑n : ZMod p) + p * k

Tactic:
refine ⟨n / p, ?_⟩
-- Module: Mathlib.Data.ZMod.Basic
Goal:
p n : ℕ
inst : NeZero p
mp : n = n % p + p * (n / p)
mp₁ mp₂ : n = n
⊢ n = val (n := p) (↑n : ZMod p) + p * (n / p)

Tactic:
rw [val_natCast, Nat.mod_add_div]

Premises used: Nat.mod_add_div, ZMod.val_natCast
-- Module: Mathlib.Data.ZMod.Basic
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
mpr₅ mpr₆ : z = z
⊢ (↑(z.val + p * k) : ZMod p) = z

Tactic:
rw [Nat.cast_add, natCast_zmod_val, Nat.cast_mul, natCast_self, zero_mul,
      add_zero]

Premises used: ZMod.natCast_self, MulZeroClass.zero_mul, Nat.cast_add, ZMod.natCast_zmod_val, Nat.cast_mul, add_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
p : ℕ
n : ℤ
z : ZMod p
inst : NeZero p
mp : (↑n : ZMod p) = z → ∃ (k : ℤ), n = (↑z.val : ℤ) + (↑p : ℤ) * k
mpr : (∃ (k : ℤ), n = (↑z.val : ℤ) + (↑p : ℤ) * k) → (↑n : ZMod p) = z
⊢ (↑n : ZMod p) = z ↔ ∃ (k : ℤ), n = (↑z.val : ℤ) + (↑p : ℤ) * k

Tactic:
constructor
-- Module: Mathlib.Data.ZMod.Basic
Goal:
p : ℕ
n : ℤ
inst : NeZero p
⊢ ∃ (k : ℤ), n = (↑(val (n := p) (↑n : ZMod p)) : ℤ) + (↑p : ℤ) * k

Tactic:
⟨n / p, ?_⟩

Premises used: HDiv.hDiv, Nat.cast, Exists.intro
-- Module: Mathlib.Data.ZMod.Basic
Goal:
p : ℕ
n : ℤ
inst : NeZero p
mp : n = (↑(val (n := p) (↑n : ZMod p)) : ℤ) + (↑p : ℤ) * (n / (↑p : ℤ))
⊢ ∃ (k : ℤ), n = (↑(val (n := p) (↑n : ZMod p)) : ℤ) + (↑p : ℤ) * k

Tactic:
refine ⟨n / p, ?_⟩
-- Module: Mathlib.Data.ZMod.Basic
Goal:
p : ℕ
n : ℤ
inst : NeZero p
mp : n = n % (↑p : ℤ) + (↑p : ℤ) * (n / (↑p : ℤ))
mp₁ mp₂ : n = n
⊢ n = (↑(val (n := p) (↑n : ZMod p)) : ℤ) + (↑p : ℤ) * (n / (↑p : ℤ))

Tactic:
rw [val_intCast, Int.emod_add_mul_ediv]

Premises used: Int.emod_add_mul_ediv, ZMod.val_intCast
-- Module: Mathlib.Data.ZMod.Basic
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
mpr₆ : HAdd.hAdd (α := ZMod p) z.cast 0 = z
mpr₇ : z.cast = z
mpr₈ mpr₉ : z = z
⊢ (↑((↑z.val : ℤ) + (↑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]

Premises used: Int.cast_natCast, ZMod.natCast_self, MulZeroClass.zero_mul, Int.cast_add, ZMod.natCast_val, Int.cast_mul, ZMod.cast_id, add_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℤ
b : ℕ
rw : a % (↑b : ℤ) ≡ a [ZMOD (↑b : ℤ)]
⊢ Eq (α := ZMod b) (↑(a % (↑b : ℤ)) : ZMod b) (↑a : ZMod b)

Tactic:
rw [ZMod.intCast_eq_intCast_iff]

Premises used: ZMod.intCast_eq_intCast_iff
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℤ
b : ℕ
⊢ a % (↑b : ℤ) ≡ a [ZMOD (↑b : ℤ)]

Tactic:
apply Int.mod_modEq

Premises used: Int.mod_modEq
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
h :
  ∀ (x : ℤ),
    x ∈ AddMonoidHom.ker (M := ZMod n) (Int.castAddHom (ZMod n)) ↔
      Membership.mem (γ := AddSubgroup ℤ) (AddSubgroup.zmultiples (↑n : ℤ)) x
⊢ AddMonoidHom.ker (M := ZMod n) (Int.castAddHom (ZMod n)) = AddSubgroup.zmultiples (↑n : ℤ)

Tactic:
ext
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x : ℤ
h : x ∈ AddMonoidHom.ker (M := ZMod n) (Int.castAddHom (ZMod n)) ↔ (↑n : ℤ) ∣ x
h₁ : Eq (α := ZMod n) ((Int.castAddHom (ZMod n) : (a : ℤ) → ZMod n) x : ZMod n) (0 : ZMod n) ↔ (↑n : ℤ) ∣ x
h₂ : Eq (α := ZMod n) ((fun (x : ℤ) ↦ ((↑x : ZMod n) : ZMod n)) x) 0 ↔ (↑n : ℤ) ∣ x
h₃ h₄ : (↑n : ℤ) ∣ x ↔ (↑n : ℤ) ∣ x
⊢ x ∈ AddMonoidHom.ker (M := ZMod n) (Int.castAddHom (ZMod n)) ↔
    Membership.mem (γ := AddSubgroup ℤ) (AddSubgroup.zmultiples (↑n : ℤ)) x

Tactic:
rw [Int.mem_zmultiples_iff, AddMonoidHom.mem_ker, Int.coe_castAddHom,
    intCast_zmod_eq_zero_iff_dvd]

Premises used: Int.coe_castAddHom, Int.mem_zmultiples_iff, ZMod.intCast_zmod_eq_zero_iff_dvd, AddMonoidHom.mem_ker
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
nzm : NeZero (R := ℕ) 0
h : 0 ≤ n
⊢ Ne (α := ℕ) 0 0

Tactic:
cases nzm
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
h : 0 ≤ n
out : Ne (α := ℕ) 0 0
⊢ Injective (α := ZMod 0) (β := ZMod n) cast

Tactic:
simp_all
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
x : ℕ
hx : x < m + 1
y : ℕ
hy : y < m + 1
f : Eq (α := ZMod n) (cast (n := m + 1) (⟨x, hx⟩ : Fin (m + 1))) (cast (n := m + 1) (⟨y, hy⟩ : Fin (m + 1)))
⊢ x = y

Tactic:
simp only [cast, val, natCast_eq_natCast_iff',
      Nat.mod_eq_of_lt (hx.trans_le h), Nat.mod_eq_of_lt (hy.trans_le h)] at f

Premises used: ZMod.cast, ZMod.natCast_eq_natCast_iff', Nat.mod_eq_of_lt, LT.lt.trans_le, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
x : ℕ
hx : x < m + 1
y : ℕ
hy : y < m + 1
f : x = y
succ : (↑(⟨x, hx⟩ : Fin (m + 1)) : ℕ) = (↑(⟨y, hy⟩ : Fin (m + 1)) : ℕ)
⊢ (⟨x, hx⟩ : Fin (m + 1)) = ⟨y, hy⟩

Tactic:
apply Fin.ext

Premises used: Fin.ext
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
x : ℕ
hx : x < m + 1
y : ℕ
hy : y < m + 1
f : x = y
⊢ (↑(⟨x, hx⟩ : Fin (m + 1)) : ℕ) = (↑(⟨y, hy⟩ : Fin (m + 1)) : ℕ)

Tactic:
f
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
x : ℕ
hx : x < m + 1
y : ℕ
hy : y < m + 1
f : x = y
⊢ (↑(⟨x, hx⟩ : Fin (m + 1)) : ℕ) = (↑(⟨y, hy⟩ : Fin (m + 1)) : ℕ)

Tactic:
exact f
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
nzm : NeZero m
h : m ≤ n
zero : ∀ [nzm : NeZero (R := ℕ) 0] (h : 0 ≤ n), Injective (α := ZMod 0) (β := ZMod n) cast
succ : ∀ (m : ℕ) [nzm : NeZero (m + 1)] (h : m + 1 ≤ n), Injective (α := ZMod (m + 1)) (β := ZMod n) cast
⊢ Injective (α := ZMod m) (β := ZMod n) cast

Tactic:
cases m with
  | zero => cases nzm; simp_all
  | succ m =>
    rintro ⟨x, hx⟩ ⟨y, hy⟩ f
    simp only [cast, val, natCast_eq_natCast_iff',
      Nat.mod_eq_of_lt (hx.trans_le h), Nat.mod_eq_of_lt (hy.trans_le h)] at f
    apply Fin.ext
    exact f

Premises used: ZMod.cast, ZMod.natCast_eq_natCast_iff', Fin.ext, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
inst : NeZero m
h : m ≤ n
a : ZMod m
rw : Eq (α := ZMod n) a.cast (cast (n := m) 0) ↔ a = 0
⊢ Eq (α := ZMod n) a.cast 0 ↔ a = 0

Tactic:
rw [← ZMod.cast_zero (n := m)]

Premises used: ZMod.cast_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
inst : NeZero m
h : m ≤ n
a : ZMod m
⊢ Eq (α := ZMod n) a.cast (cast (n := m) 0) ↔ a = 0

Tactic:
Injective.eq_iff' (cast_injective_of_le h) rfl

Premises used: ZMod.cast_injective_of_le, Function.Injective.eq_iff', rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
inst : NeZero m
h : m ≤ n
a : ZMod m
⊢ Eq (α := ZMod n) a.cast (cast (n := m) 0) ↔ a = 0

Tactic:
exact Injective.eq_iff' (cast_injective_of_le h) rfl

Premises used: ZMod.cast_injective_of_le, Function.Injective.eq_iff', rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
p n : ℕ
_h : LE.le (α := ℤ) 0 (↑n : ℤ)
⊢ Eq (α := ZMod p) (↑(Int.toNat (↑n : ℤ)) : ZMod p) (↑(↑n : ℤ) : ZMod p)

Tactic:
simp only [Int.cast_natCast, Int.toNat_natCast]

Premises used: Int.cast_natCast, Int.toNat_natCast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
p n : ℕ
h : 0 ≤ Int.negSucc n
⊢ Eq (α := ZMod p) (↑(Int.negSucc n).toNat : ZMod p) (↑(Int.negSucc n) : ZMod p)

Tactic:
simp at h
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
zero : ∀ [NeZero (R := ℕ) 0], Injective (α := ZMod 0) val
succ : ∀ (n : ℕ) [NeZero (n + 1)], Injective (α := ZMod (n + 1)) val
⊢ Injective (α := ZMod n) val

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
inst : NeZero (R := ℕ) 0
⊢ Injective (α := ZMod 0) val

Tactic:
cases NeZero.ne 0 rfl

Premises used: OfNat.ofNat, rfl, NeZero.ne
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero (n + 1)
a b : ZMod (n + 1)
h : a.val = b.val
succ : (↑a : ℕ) = (↑b : ℕ)
⊢ a = b

Tactic:
ext
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero (n + 1)
a b : ZMod (n + 1)
h : a.val = b.val
⊢ (↑a : ℕ) = (↑b : ℕ)

Tactic:
h

Premises used: ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero (n + 1)
a b : ZMod (n + 1)
h : a.val = b.val
⊢ (↑a : ℕ) = (↑b : ℕ)

Tactic:
exact h
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
rw : val (n := n) (↑1 : ZMod n) = 1 % n
rw₁ rw₂ : 1 % n = 1 % n
⊢ val (n := n) 1 = 1 % n

Tactic:
rw [← Nat.cast_one, val_natCast]

Premises used: ZMod.val_natCast, Nat.cast_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
rw : val (n := n) (↑2 : ZMod n) = 2 % n
rw₁ rw₂ : 2 % n = 2 % n
⊢ val (n := n) 2 = 2 % n

Tactic:
rw [← Nat.cast_two, val_natCast]

Premises used: ZMod.val_natCast, Nat.cast_two
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : Fact (1 < n)
rw : 1 % n = 1
⊢ val (n := n) 1 = 1

Tactic:
rw [val_one_eq_one_mod]

Premises used: ZMod.val_one_eq_one_mod
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : Fact (1 < n)
⊢ 1 % n = 1

Tactic:
Nat.mod_eq_of_lt Fact.out

Premises used: Nat.mod_eq_of_lt, Fact.out
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : Fact (1 < n)
⊢ 1 % n = 1

Tactic:
exact Nat.mod_eq_of_lt Fact.out

Premises used: Nat.mod_eq_of_lt, Fact.out
-- Module: Mathlib.Data.ZMod.Basic
Goal:
hn : Ne (α := ℕ) 1 1
⊢ val (n := 1) 1 = 1

Tactic:
cases hn rfl

Premises used: rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
h : n + 2 ≠ 1
⊢ 1 < n + 2

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
zero : ∀ [NeZero (R := ℕ) 0] (a b : ZMod 0), (a + b).val = (a.val + b.val) % 0
succ : ∀ (n : ℕ) [NeZero (n + 1)] (a b : ZMod (n + 1)), (a + b).val = (a.val + b.val) % (n + 1)
⊢ (a + b).val = (a.val + b.val) % n

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
inst : NeZero (R := ℕ) 0
a b : ZMod 0
⊢ (a + b).val = (a.val + b.val) % 0

Tactic:
cases NeZero.ne 0 rfl

Premises used: OfNat.ofNat, rfl, NeZero.ne
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero (n + 1)
a b : ZMod (n + 1)
⊢ (a + b).val = (a.val + b.val) % (n + 1)

Tactic:
apply Fin.val_add

Premises used: Fin.val_add
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : ZMod n
h : a.val + b.val < n
out : n ≠ 0
⊢ NeZero n

Tactic:
constructor
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b : ZMod 0
h : a.val + b.val < 0
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : ZMod n
h : a.val + b.val < n
⊢ NeZero n

Tactic:
have : NeZero n := by constructor; rintro rfl; simp at h
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : ZMod n
h : a.val + b.val < n
this : NeZero n
rw : (a.val + b.val) % n = a.val + b.val
rw₁ rw₂ : a.val + b.val = a.val + b.val
⊢ (a + b).val = a.val + b.val

Tactic:
rw [ZMod.val_add, Nat.mod_eq_of_lt h]

Premises used: ZMod.val_add, Nat.mod_eq_of_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
rw : n ≤ a.val % n + b.val % n
⊢ a.val + b.val = (a + b).val + n

Tactic:
rw [val_add, Nat.add_mod_add_of_le_add_mod, Nat.mod_eq_of_lt (val_lt _),
    Nat.mod_eq_of_lt (val_lt _)]

Premises used: ZMod.val_add, Nat.mod_eq_of_lt, Nat.add_mod_add_of_le_add_mod, ZMod.val_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
rwa : n ≤ a.val + b.val % n
rwa₁ rwa₂ rwa₃ rwa₄ : n ≤ a.val + b.val
⊢ n ≤ a.val % n + b.val % n

Tactic:
rwa [Nat.mod_eq_of_lt (val_lt _), Nat.mod_eq_of_lt (val_lt _)]

Premises used: Nat.mod_eq_of_lt, ZMod.val_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
rw : (a + b).val = (a + b).val + n - n
⊢ (a + b).val = a.val + b.val - n

Tactic:
rw [val_add_val_of_le h]

Premises used: ZMod.val_add_val_of_le
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ (a + b).val = (a + b).val + n - n

Tactic:
eq_tsub_of_add_eq rfl

Premises used: eq_tsub_of_add_eq, rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ (a + b).val = (a + b).val + n - n

Tactic:
exact eq_tsub_of_add_eq rfl

Premises used: eq_tsub_of_add_eq, rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : ZMod n
zero : ∀ (a b : ZMod 0), (a + b).val ≤ a.val + b.val
succ : ∀ (n : ℕ) (a b : ZMod (n + 1)), (a + b).val ≤ a.val + b.val
⊢ (a + b).val ≤ a.val + b.val

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b : ZMod 0
⊢ (a + b).val ≤ a.val + b.val

Tactic:
simpa [ZMod.val] using Int.natAbs_add_le _ _

Premises used: Int.natAbs_add_le, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).val ≤ a.val + b.val

Tactic:
simpa [ZMod.val_add] using Nat.mod_le _ _

Premises used: ZMod.val_add, Nat.mod_le
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : ZMod n
zero : ∀ (a b : ZMod 0), (a * b).val = a.val * b.val % 0
succ : ∀ (n : ℕ) (a b : ZMod (n + 1)), (a * b).val = a.val * b.val % (n + 1)
⊢ (a * b).val = a.val * b.val % n

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b : ZMod 0
zero : (a * b).val = a.val * b.val
⊢ (a * b).val = a.val * b.val % 0

Tactic:
rw [Nat.mod_zero]

Premises used: Nat.mod_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b : ZMod 0
⊢ (a * b).val = a.val * b.val

Tactic:
apply Int.natAbs_mul

Premises used: Int.natAbs_mul
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : ZMod (n + 1)
⊢ (a * b).val = a.val * b.val % (n + 1)

Tactic:
apply Fin.val_mul

Premises used: Fin.val_mul
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : ZMod n
rw : a.val * b.val % n ≤ a.val * b.val
⊢ (a * b).val ≤ a.val * b.val

Tactic:
rw [val_mul]

Premises used: ZMod.val_mul
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : ZMod n
⊢ a.val * b.val % n ≤ a.val * b.val

Tactic:
apply Nat.mod_le

Premises used: Nat.mod_le
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : ZMod n
h : a.val * b.val < n
rw : a.val * b.val % n = a.val * b.val
⊢ (a * b).val = a.val * b.val

Tactic:
rw [val_mul]

Premises used: ZMod.val_mul
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : ZMod n
h : a.val * b.val < n
⊢ a.val * b.val % n = a.val * b.val

Tactic:
apply Nat.mod_eq_of_lt h

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
mp : (a * b).val = a.val * b.val → a.val * b.val < n
mpr : a.val * b.val < n → (a * b).val = a.val * b.val
⊢ (a * b).val = a.val * b.val ↔ a.val * b.val < n

Tactic:
constructor
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : (a * b).val = a.val * b.val
mp : (a * b).val < n
⊢ a.val * b.val < n

Tactic:
rw [← h]
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : (a * b).val = a.val * b.val
⊢ (a * b).val < n

Tactic:
apply ZMod.val_lt

Premises used: ZMod.val_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : a.val * b.val < n
⊢ (a * b).val = a.val * b.val

Tactic:
apply ZMod.val_mul_of_lt h

Premises used: ZMod.val_mul_of_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n_1 n : ℕ
inst : Fact (1 < n)
h : Eq (α := ZMod n) 0 1
rw rw₁ : Eq (α := ℕ) 0 0
⊢ 0 = val (n := n) 0

Tactic:
rw [val_zero]

Premises used: ZMod.val_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
⊢ Nontrivial
    (match (motive := ℕ → Type) 0 with
    | 0 => ℤ
    | n.succ => Fin (n + 1))

Tactic:
infer_instance
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
rw : Eq (α := ZMod n) (↑1 : ZMod n) 0 ↔ n = 1
rw₁ : n ∣ 1 ↔ n = 1
rw₂ rw₃ : n = 1 ↔ n = 1
⊢ Eq (α := ZMod n) 1 0 ↔ n = 1

Tactic:
rw [← Nat.cast_one, natCast_eq_zero_iff, Nat.dvd_one]

Premises used: Nat.dvd_one, ZMod.natCast_eq_zero_iff, Nat.cast_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ Eq (α := ZMod (n + 1))
    (↑(Nat.strongRec' (p := fun (x : ℕ) ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
              (fun (n : ℕ) (ih : (m : ℕ) → m < n → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) (s t : ℤ) (r' : ℕ) (s' t' : ℤ) ↦
                match (motive := (n : ℕ) → (ih : (m : ℕ) → m < n → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → ℕ × ℤ × ℤ) n,
                  ih with
                | 0, ih => (r', s', t')
                | k.succ, ih =>
                  have q := r' / k.succ;
                  ih (r' % k.succ) ⋯ (s' - (↑q : ℤ) * s) (t' - (↑q : ℤ) * t) k.succ s t)
              0 1 0 (n + 1) 0 1).2.1 :
      ZMod (n + 1))
    0

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod n
zero : ∀ (a : ZMod 0), a * a⁻¹ = (↑(a.val.gcd 0) : ZMod 0)
succ : ∀ (n : ℕ) (a : ZMod (n + 1)), a * a⁻¹ = (↑(a.val.gcd (n + 1)) : ZMod (n + 1))
⊢ a * a⁻¹ = (↑(a.val.gcd n) : ZMod n)

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℤ
⊢ a * a.sign = a * a.sign

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℤ
rw rw₁ : Eq (α := ℤ) (↑a.natAbs : ℤ) (↑a.natAbs : ℤ)
⊢ a * a.sign = (↑a.natAbs : ℤ)

Tactic:
rw [Int.mul_sign_self]

Premises used: Int.mul_sign_self
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℤ
rw rw₁ : Eq (α := ℤ) (↑a.natAbs : ℤ) (↑a.natAbs : ℤ)
⊢ Eq (α := ℤ) (↑a.natAbs : ℤ) (↑(a.natAbs.gcd 0) : ℤ)

Tactic:
rw [Nat.gcd_zero_right]

Premises used: Nat.gcd_zero_right
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℤ
_ : a * a.sign = (↑a.natAbs : ℤ)
_₁ : Eq (α := ℤ) (↑a.natAbs : ℤ) (↑(a.natAbs.gcd 0) : ℤ)
⊢ a * a⁻¹ = (↑((val (n := 0) a).gcd 0) : ℤ)

Tactic:
calc
      _ = a * Int.sign a := rfl
      _ = a.natAbs := by rw [Int.mul_sign_self]
      _ = a.natAbs.gcd 0 := by rw [Nat.gcd_zero_right]

Premises used: Nat.gcd, Int.sign, Int.natAbs, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
rw : a * a⁻¹ = a * a⁻¹ + HMul.hMul (α := ZMod (n + 1)) 0 (↑(a.val.gcdB n.succ) : ZMod (n + 1))
rw₁ : a * a⁻¹ = a * a⁻¹ + 0
rw₂ rw₃ : a * a⁻¹ = a * a⁻¹
⊢ a * a⁻¹ = a * a⁻¹ + HMul.hMul (α := ZMod (n + 1)) (↑n.succ : ZMod (n + 1)) (↑(a.val.gcdB n.succ) : ZMod (n + 1))

Tactic:
rw [natCast_self, zero_mul, add_zero]

Premises used: ZMod.natCast_self, MulZeroClass.zero_mul, add_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
push_cast :
  a * a⁻¹ + HAdd.hAdd (α := ZMod (n + 1)) (↑n : ZMod (n + 1)) 1 * (↑(a.val.gcdB n.succ) : ZMod (n + 1)) =
    HMul.hMul (α := ZMod (n + 1)) (↑a.val : ZMod (n + 1)) (↑(a.val.gcdA n.succ) : ZMod (n + 1)) +
      HAdd.hAdd (α := ZMod (n + 1)) (↑n : ZMod (n + 1)) 1 * (↑(a.val.gcdB n.succ) : ZMod (n + 1))
⊢ a * a⁻¹ + HMul.hMul (α := ZMod (n + 1)) (↑n.succ : ZMod (n + 1)) (↑(a.val.gcdB n.succ) : ZMod (n + 1)) =
    (↑((↑a.val : ℤ) * a.val.gcdA n.succ + (↑n.succ : ℤ) * a.val.gcdB n.succ) : ZMod (n + 1))

Tactic:
push_cast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
rw :
  a * a⁻¹ + HAdd.hAdd (α := ZMod (n + 1)) (↑n : ZMod (n + 1)) 1 * (↑(a.val.gcdB n.succ) : ZMod (n + 1)) =
    a * (↑(a.val.gcdA n.succ) : ZMod (n + 1)) +
      HAdd.hAdd (α := ZMod (n + 1)) (↑n : ZMod (n + 1)) 1 * (↑(a.val.gcdB n.succ) : ZMod (n + 1))
⊢ a * a⁻¹ + HAdd.hAdd (α := ZMod (n + 1)) (↑n : ZMod (n + 1)) 1 * (↑(a.val.gcdB n.succ) : ZMod (n + 1)) =
    HMul.hMul (α := ZMod (n + 1)) (↑a.val : ZMod (n + 1)) (↑(a.val.gcdA n.succ) : ZMod (n + 1)) +
      HAdd.hAdd (α := ZMod (n + 1)) (↑n : ZMod (n + 1)) 1 * (↑(a.val.gcdB n.succ) : ZMod (n + 1))

Tactic:
rw [natCast_zmod_val]

Premises used: ZMod.natCast_zmod_val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ + HAdd.hAdd (α := ZMod (n + 1)) (↑n : ZMod (n + 1)) 1 * (↑(a.val.gcdB n.succ) : ZMod (n + 1)) =
    a * (↑(a.val.gcdA n.succ) : ZMod (n + 1)) +
      HAdd.hAdd (α := ZMod (n + 1)) (↑n : ZMod (n + 1)) 1 * (↑(a.val.gcdB n.succ) : ZMod (n + 1))

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
rw : Eq (α := ZMod (n + 1)) (↑(↑(a.val.gcd n.succ) : ℤ) : ZMod (n + 1)) (↑(a.val.gcd n.succ) : ZMod (n + 1))
⊢ Eq (α := ZMod (n + 1)) (↑((↑a.val : ℤ) * a.val.gcdA n.succ + (↑n.succ : ℤ) * a.val.gcdB n.succ) : ZMod (n + 1))
    (↑(a.val.gcd n.succ) : ZMod (n + 1))

Tactic:
rw [← Nat.gcd_eq_gcd_ab a.val n.succ]

Premises used: Nat.succ, Nat.gcd_eq_gcd_ab, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
⊢ Eq (α := ZMod (n + 1)) (↑(↑(a.val.gcd n.succ) : ℤ) : ZMod (n + 1)) (↑(a.val.gcd n.succ) : ZMod (n + 1))

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
a₁ : a * a⁻¹ = a * a⁻¹ + HMul.hMul (α := ZMod (n + 1)) (↑n.succ : ZMod (n + 1)) (↑(a.val.gcdB n.succ) : ZMod (n + 1))
a₂ :
  a * a⁻¹ + HMul.hMul (α := ZMod (n + 1)) (↑n.succ : ZMod (n + 1)) (↑(a.val.gcdB n.succ) : ZMod (n + 1)) =
    (↑((↑a.val : ℤ) * a.val.gcdA n.succ + (↑n.succ : ℤ) * a.val.gcdB n.succ) : ZMod (n + 1))
a₃ :
  Eq (α := ZMod (n + 1)) (↑((↑a.val : ℤ) * a.val.gcdA n.succ + (↑n.succ : ℤ) * a.val.gcdB n.succ) : ZMod (n + 1))
    (↑(a.val.gcd n.succ) : ZMod (n + 1))
⊢ a * a⁻¹ = (↑(a.val.gcd (n + 1)) : ZMod (n + 1))

Tactic:
calc
      a * a⁻¹ = a * a⁻¹ + n.succ * Nat.gcdB (val a) n.succ := by
        rw [natCast_self, zero_mul, add_zero]
      _ = ↑(↑a.val * Nat.gcdA (val a) n.succ + n.succ * Nat.gcdB (val a) n.succ) := by
        push_cast
        rw [natCast_zmod_val]
        rfl
      _ = Nat.gcd a.val n.succ := by rw [← Nat.gcd_eq_gcd_ab a.val n.succ]; rfl

Premises used: Nat.gcd, HMul.hMul, Nat.cast, Nat.gcdB, HAdd.hAdd, Nat.gcdA, Nat.succ, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inl : Eq (α := ZMod 1) 1⁻¹ 1
inr : ∀ (hn : n ≠ 1), Eq (α := ZMod n) 1⁻¹ 1
⊢ Eq (α := ZMod n) 1⁻¹ 1

Tactic:
obtain rfl | hn := eq_or_ne n 1

Premises used: eq_or_ne, OfNat.ofNat, rfl