awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
a b : ZMod n
⊢ (a - b).cast = HSub.hSub (α := R) a.cast b.cast

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
a : ZMod n
k : ℕ
⊢ (a ^ k).cast = HPow.hPow (α := R) a.cast k

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
k : ℕ
⊢ Eq.{u_1 + 1} (α := R) (cast (n := n) (↑k : ZMod n)) (↑k : R)

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
k : ℤ
⊢ Eq.{u_1 + 1} (α := R) (cast (n := n) (↑k : ZMod n)) (↑k : R)

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
rw : ∀ (a : ZMod n), Eq (α := R) ((castHom ⋯ R : (a : ZMod n) → R) a : R) (0 : R) → a = 0
⊢ Injective (α := ZMod n) (β := R) (⇑(castHom ⋯ R) : (a : ZMod n) → R)

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
x : ZMod n
obtain :
  ∀ (k : ℤ), Eq (α := R) ((castHom ⋯ R : (a : ZMod n) → R) (↑k : ZMod n) : R) (0 : R) → Eq (α := ZMod n) (↑k : ZMod n) 0
⊢ Eq (α := R) ((castHom ⋯ R : (a : ZMod n) → R) x : R) (0 : R) → x = 0

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

Premises used: ZMod.intCast_surjective, rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
k : ℤ
rw : (↑n : ℤ) ∣ k → (↑n : ℤ) ∣ k
⊢ Eq (α := R) ((castHom ⋯ R : (a : ZMod n) → R) (↑k : ZMod n) : R) (0 : R) → Eq (α := ZMod n) (↑k : ZMod n) 0

Tactic:
rw [map_intCast, CharP.intCast_eq_zero_iff R n, CharP.intCast_eq_zero_iff (ZMod n) n]

Premises used: map_intCast, ZMod, CharP.intCast_eq_zero_iff
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
k : ℤ
⊢ (↑n : ℤ) ∣ k → (↑n : ℤ) ∣ k

Tactic:
id

Premises used: id
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
k : ℤ
⊢ (↑n : ℤ) ∣ k → (↑n : ℤ) ∣ k

Tactic:
exact id

Premises used: id
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
inst_2 : Fintype R
h : Fintype.card R = n
hn : n = 0
⊢ Fintype.card R = 0

Tactic:
rw [hn] at h
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
inst_2 : Fintype R
h : Fintype.card R = n
hn : n = 0
h₁ : Fintype.card R = 0
⊢ n = 0

Tactic:
rw [hn] at h
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
inst_2 : Fintype R
h : Fintype.card R = 0
hn : n = 0
⊢ False

Tactic:
(Fintype.card_eq_zero_iff.mp h).elim' 0

Premises used: IsEmpty.elim', Fintype.card_eq_zero_iff, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
inst_2 : Fintype R
h : Fintype.card R = 0
hn : n = 0
⊢ False

Tactic:
exact (Fintype.card_eq_zero_iff.mp h).elim' 0

Premises used: IsEmpty.elim', Fintype.card_eq_zero_iff, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
inst_2 : Fintype R
h : Fintype.card R = n
⊢ NeZero n

Tactic:
haveI : NeZero n :=
    ⟨by
      intro hn
      rw [hn] at h
      exact (Fintype.card_eq_zero_iff.mp h).elim' 0⟩
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
inst_2 : Fintype R
h : Fintype.card R = n
this : NeZero n
rw : Injective (α := ZMod n) (β := R) (⇑(castHom ⋯ R) : (a : ZMod n) → R)
⊢ Bijective (α := ZMod n) (β := R) (⇑(castHom ⋯ R) : (a : ZMod n) → R)

Tactic:
rw [Fintype.bijective_iff_injective_and_card, ZMod.card, h, eq_self_iff_true, and_true]

Premises used: and_true, Fintype.bijective_iff_injective_and_card, eq_self_iff_true, ZMod.card
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
inst_2 : Fintype R
h : Fintype.card R = n
this : NeZero n
⊢ Injective (α := ZMod n) (β := R) (⇑(castHom ⋯ R) : (a : ZMod n) → R)

Tactic:
apply ZMod.castHom_injective

Premises used: ZMod.castHom_injective
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
p : ℕ
inst_2 : CharP R p
hp : Nat.Prime p
hR : Fintype.card R = p
⊢ Eq (α := ZMod p ≃+* R) (ringEquivOfPrime R hp hR) (ringEquiv R hR)

Tactic:
rfl

Premises used: ZMod.ringEquivOfPrime, rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m = n
zero : (h : 0 = n) → ZMod 0 ≃+* ZMod n
succ : (m : ℕ) → (h : m + 1 = n) → ZMod (m + 1) ≃+* ZMod n
⊢ ZMod m ≃+* ZMod n

Tactic:
rcases m with - | m
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
n : ℕ
h : 0 = n
zero : (h : Eq (α := ℕ) 0 0) → ZMod 0 ≃+* ZMod 0
zero₁ : (n : ℕ) → (h : 0 = n + 1) → ZMod 0 ≃+* ZMod (n + 1)
⊢ ZMod 0 ≃+* ZMod n

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
n m : ℕ
h : m + 1 = n
succ : (h : m + 1 = 0) → ZMod (m + 1) ≃+* ZMod 0
succ₁ : (n : ℕ) → (h : m + 1 = n + 1) → ZMod (m + 1) ≃+* ZMod (n + 1)
⊢ ZMod (m + 1) ≃+* ZMod n

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
h : Eq (α := ℕ) 0 0
⊢ ZMod 0 ≃+* ZMod 0

Tactic:
exact RingEquiv.refl _

Premises used: RingEquiv.refl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
n : ℕ
h : 0 = n + 1
zero : False
⊢ ZMod 0 ≃+* ZMod (n + 1)

Tactic:
exfalso
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
n : ℕ
h : 0 = n + 1
⊢ False

Tactic:
n.succ_ne_zero h.symm

Premises used: Nat.succ_ne_zero, Eq.symm
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
n : ℕ
h : 0 = n + 1
⊢ False

Tactic:
exact n.succ_ne_zero h.symm

Premises used: Nat.succ_ne_zero, Eq.symm
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
m : ℕ
h : m + 1 = 0
succ : False
⊢ ZMod (m + 1) ≃+* ZMod 0

Tactic:
exfalso
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
m : ℕ
h : m + 1 = 0
⊢ False

Tactic:
m.succ_ne_zero h

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
m : ℕ
h : m + 1 = 0
⊢ False

Tactic:
exact m.succ_ne_zero h

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
h₁ : (↑(Fin.cast h (a * b)) : ℕ) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
⊢ Fin.cast h (a * b) = Fin.cast h a * Fin.cast h b

Tactic:
ext
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
h₁ : (↑(a * b) : ℕ) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
h₂ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
h₃ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑(Fin.cast h a) : ℕ) * (↑(Fin.cast h b) : ℕ) % (n + 1)
h₄ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑a : ℕ) * (↑(Fin.cast h b) : ℕ) % (n + 1)
h₅ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑a : ℕ) * (↑b : ℕ) % (n + 1)
h₆ h₇ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑a : ℕ) * (↑b : ℕ) % (m + 1)
⊢ (↑(Fin.cast h (a * b)) : ℕ) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)

Tactic:
rw [Fin.val_cast, Fin.val_mul, Fin.val_mul, Fin.val_cast, Fin.val_cast, ← h]

Premises used: Fin.val_mul, Fin.val_cast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
h₁ : (↑(Fin.cast h (a + b)) : ℕ) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
⊢ Fin.cast h (a + b) = Fin.cast h a + Fin.cast h b

Tactic:
ext
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
h₁ : (↑(a + b) : ℕ) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
h₂ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
h₃ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = ((↑(Fin.cast h a) : ℕ) + (↑(Fin.cast h b) : ℕ)) % (n + 1)
h₄ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = ((↑a : ℕ) + (↑(Fin.cast h b) : ℕ)) % (n + 1)
h₅ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = ((↑a : ℕ) + (↑b : ℕ)) % (n + 1)
h₆ h₇ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = ((↑a : ℕ) + (↑b : ℕ)) % (m + 1)
⊢ (↑(Fin.cast h (a + b)) : ℕ) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)

Tactic:
rw [Fin.val_cast, Fin.val_add, Fin.val_add, Fin.val_cast, Fin.val_cast, ← h]

Premises used: Fin.val_add, Fin.val_cast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
⊢ ZMod (m + 1) ≃+* ZMod (n + 1)

Tactic:
exact
      { finCongr h with
        map_mul' := fun a b => by
          dsimp [ZMod]
          ext
          rw [Fin.val_cast, Fin.val_mul, Fin.val_mul, Fin.val_cast, Fin.val_cast, ← h]
        map_add' := fun a b => by
          dsimp [ZMod]
          ext
          rw [Fin.val_cast, Fin.val_add, Fin.val_add, Fin.val_cast, Fin.val_cast, ← h] }

Premises used: finCongr
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℕ
zero : Eq (α := ZMod 0 ≃+* ZMod 0) (ringEquivCongr ⋯) (RingEquiv.refl (ZMod 0))
succ : ∀ (n : ℕ), Eq (α := ZMod (n + 1) ≃+* ZMod (n + 1)) (ringEquivCongr ⋯) (RingEquiv.refl (ZMod (n + 1)))
⊢ Eq (α := ZMod a ≃+* ZMod a) (ringEquivCongr ⋯) (RingEquiv.refl (ZMod a))

Tactic:
cases a
-- Module: Mathlib.Data.ZMod.Basic
Goal:
⊢ Eq (α := ZMod 0 ≃+* ZMod 0) (ringEquivCongr ⋯) (RingEquiv.refl (ZMod 0))

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ Eq (α := ZMod (n + 1) ≃+* ZMod (n + 1)) (ringEquivCongr ⋯) (RingEquiv.refl (ZMod (n + 1)))

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℕ
x : ZMod a
rw : (RingEquiv.refl (ZMod a) : (a_1 : ZMod a) → ZMod a) x = x
⊢ (ringEquivCongr ⋯ : (a_1 : ZMod a) → ZMod a) x = x

Tactic:
rw [ringEquivCongr_refl]

Premises used: ZMod.ringEquivCongr_refl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℕ
x : ZMod a
⊢ (RingEquiv.refl (ZMod a) : (a_1 : ZMod a) → ZMod a) x = x

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b : ℕ
hab : a = b
subst : (ringEquivCongr ⋯).symm = ringEquivCongr ⋯
⊢ (ringEquivCongr hab).symm = ringEquivCongr ⋯

Tactic:
subst hab
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℕ
zero : Eq (α := ZMod 0 ≃+* ZMod 0) (RingEquiv.symm (ringEquivCongr ⋯)) (ringEquivCongr ⋯)
succ : ∀ (n : ℕ), (ringEquivCongr ⋯).symm = ringEquivCongr ⋯
⊢ (ringEquivCongr ⋯).symm = ringEquivCongr ⋯

Tactic:
cases a
-- Module: Mathlib.Data.ZMod.Basic
Goal:
⊢ Eq (α := ZMod 0 ≃+* ZMod 0) (RingEquiv.symm (ringEquivCongr ⋯)) (ringEquivCongr ⋯)

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ (ringEquivCongr ⋯).symm = ringEquivCongr ⋯

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b c : ℕ
hab : a = b
hbc : b = c
subst : (ringEquivCongr ⋯).trans (ringEquivCongr ⋯) = ringEquivCongr ⋯
⊢ (ringEquivCongr hab).trans (ringEquivCongr hbc) = ringEquivCongr ⋯

Tactic:
subst hab hbc
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℕ
zero : Eq (α := ZMod 0 ≃+* ZMod 0) (RingEquiv.trans (ringEquivCongr ⋯) (ringEquivCongr ⋯)) (ringEquivCongr ⋯)
succ : ∀ (n : ℕ), (ringEquivCongr ⋯).trans (ringEquivCongr ⋯) = ringEquivCongr ⋯
⊢ (ringEquivCongr ⋯).trans (ringEquivCongr ⋯) = ringEquivCongr ⋯

Tactic:
cases a
-- Module: Mathlib.Data.ZMod.Basic
Goal:
⊢ Eq (α := ZMod 0 ≃+* ZMod 0) (RingEquiv.trans (ringEquivCongr ⋯) (ringEquivCongr ⋯)) (ringEquivCongr ⋯)

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ (ringEquivCongr ⋯).trans (ringEquivCongr ⋯) = ringEquivCongr ⋯

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b c : ℕ
hab : a = b
hbc : b = c
x : ZMod a
rw :
  Eq (α := ZMod c)
    ((ringEquivCongr hbc : (a : ZMod b) → ZMod c) ((ringEquivCongr hab : (a : ZMod a) → ZMod b) x) : ZMod c)
    (((ringEquivCongr hab).trans (ringEquivCongr hbc) : (a : ZMod a) → ZMod c) x : ZMod c)
⊢ Eq (α := ZMod c)
    ((ringEquivCongr hbc : (a : ZMod b) → ZMod c) ((ringEquivCongr hab : (a : ZMod a) → ZMod b) x) : ZMod c)
    ((ringEquivCongr ⋯ : (a : ZMod a) → ZMod c) x : ZMod c)

Tactic:
rw [← ringEquivCongr_trans hab hbc]

Premises used: ZMod.ringEquivCongr_trans
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b c : ℕ
hab : a = b
hbc : b = c
x : ZMod a
⊢ Eq (α := ZMod c)
    ((ringEquivCongr hbc : (a : ZMod b) → ZMod c) ((ringEquivCongr hab : (a : ZMod a) → ZMod b) x) : ZMod c)
    (((ringEquivCongr hab).trans (ringEquivCongr hbc) : (a : ZMod a) → ZMod c) x : ZMod c)

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b : ℕ
h : a = b
x : ZMod a
subst : val (n := a) ((ringEquivCongr ⋯ : (a_1 : ZMod a) → ZMod a) x) = x.val
⊢ val (n := b) ((ringEquivCongr h : (a : ZMod a) → ZMod b) x) = x.val

Tactic:
subst h
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℕ
x : ZMod a
zero : ∀ (x : ZMod 0), val (n := 0) ((ringEquivCongr ⋯ : (a : ZMod 0) → ZMod 0) x) = x.val
succ : ∀ (n : ℕ) (x : ZMod (n + 1)), val (n := n + 1) ((ringEquivCongr ⋯ : (a : ZMod (n + 1)) → ZMod (n + 1)) x) = x.val
⊢ val (n := a) ((ringEquivCongr ⋯ : (a_1 : ZMod a) → ZMod a) x) = x.val

Tactic:
cases a
-- Module: Mathlib.Data.ZMod.Basic
Goal:
x : ZMod 0
⊢ val (n := 0) ((ringEquivCongr ⋯ : (a : ZMod 0) → ZMod 0) x) = x.val

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
x : ZMod (n + 1)
⊢ val (n := n + 1) ((ringEquivCongr ⋯ : (a : ZMod (n + 1)) → ZMod (n + 1)) x) = x.val

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b : ℕ
h : a = b
z : ℤ
⊢ Eq (α := ZMod b) ((ringEquivCongr h : (a : ZMod a) → ZMod b) (↑z : ZMod a)) (↑z : ZMod b)

Tactic:
map_intCast (ringEquivCongr h) z

Premises used: ZMod.ringEquivCongr, map_intCast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
rw : a.val = 0 ↔ (↑a : ℕ) = (↑0 : ℕ)
⊢ a.val = 0 ↔ a = 0

Tactic:
rw [Fin.ext_iff]

Premises used: Fin.ext_iff
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
⊢ a.val = 0 ↔ (↑a : ℕ) = (↑0 : ℕ)

Tactic:
Iff.rfl

Premises used: Iff.rfl, Nat.mod, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
⊢ a.val = 0 ↔ (↑a : ℕ) = (↑0 : ℕ)

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b : ℤ
c : ℕ
⊢ Eq (α := ZMod c) (↑a : ZMod c) (↑b : ZMod c) ↔ a ≡ b [ZMOD (↑c : ℤ)]

Tactic:
CharP.intCast_eq_intCast (ZMod c) c

Premises used: ZMod, CharP.intCast_eq_intCast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b : ℤ
c : ℕ
⊢ Eq (α := ZMod c) (↑a : ZMod c) (↑b : ZMod c) ↔ a % (↑c : ℤ) = b % (↑c : ℤ)

Tactic:
ZMod.intCast_eq_intCast_iff a b c

Premises used: ZMod.intCast_eq_intCast_iff, Int.ModEq
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ℤ
inst : NeZero n
⊢ LE.le (α := ℤ) 0 (↑(val (n := n) (↑a : ZMod n)) : ℤ)

Tactic:
have hle : (0 : ℤ) ≤ ↑(a : ZMod n).val := Int.natCast_nonneg _
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ℤ
inst : NeZero n
hle : LE.le (α := ℤ) 0 (↑(val (n := n) (↑a : ZMod n)) : ℤ)
⊢ LT.lt (α := ℤ) (↑(val (n := n) (↑a : ZMod n)) : ℤ) (↑n : ℤ)

Tactic:
have hlt : ↑(a : ZMod n).val < (n : ℤ) := Int.ofNat_lt.mpr (ZMod.val_lt a)
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ℤ
inst : NeZero n
hle : LE.le (α := ℤ) 0 (↑(val (n := n) (↑a : ZMod n)) : ℤ)
hlt : LT.lt (α := ℤ) (↑(val (n := n) (↑a : ZMod n)) : ℤ) (↑n : ℤ)
⊢ (↑(val (n := n) (↑a : ZMod n)) : ℤ) = a % (↑n : ℤ)

Tactic:
(Int.emod_eq_of_lt hle hlt).symm.trans ?_

Premises used: Int.emod_eq_of_lt, Eq.symm, Eq.trans
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ℤ
inst : NeZero n
hle : LE.le (α := ℤ) 0 (↑(val (n := n) (↑a : ZMod n)) : ℤ)
hlt : LT.lt (α := ℤ) (↑(val (n := n) (↑a : ZMod n)) : ℤ) (↑n : ℤ)
refine : HMod.hMod (α := ℤ) (↑(val (n := n) (↑a : ZMod n)) : ℤ) (↑n : ℤ) = a % (↑n : ℤ)
⊢ (↑(val (n := n) (↑a : ZMod n)) : ℤ) = a % (↑n : ℤ)

Tactic:
refine (Int.emod_eq_of_lt hle hlt).symm.trans ?_

Premises used: Int.emod_eq_of_lt, Eq.symm, Eq.trans
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ℤ
inst : NeZero n
hle : LE.le (α := ℤ) 0 (↑(val (n := n) (↑a : ZMod n)) : ℤ)
hlt : LT.lt (α := ℤ) (↑(val (n := n) (↑a : ZMod n)) : ℤ) (↑n : ℤ)
rw : Eq (α := ZMod n) (↑(↑(val (n := n) (↑a : ZMod n)) : ℤ) : ZMod n) (↑a : ZMod n)
rw₁ : Eq (α := ZMod n) (↑(val (n := n) (↑a : ZMod n)) : ZMod n) (↑a : ZMod n)
rw₂ : Eq (α := ZMod n) (cast (n := n) (↑a : ZMod n)) (↑a : ZMod n)
rw₃ rw₄ : Eq (α := ZMod n) (↑a : ZMod n) (↑a : ZMod n)
⊢ HMod.hMod (α := ℤ) (↑(val (n := n) (↑a : ZMod n)) : ℤ) (↑n : ℤ) = a % (↑n : ℤ)

Tactic:
rw [← ZMod.intCast_eq_intCast_iff', Int.cast_natCast, ZMod.natCast_val, ZMod.cast_id]

Premises used: Int.cast_natCast, ZMod.natCast_val, ZMod.intCast_eq_intCast_iff', ZMod.cast_id
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b c : ℕ
⊢ Eq (α := ZMod c) (↑a : ZMod c) (↑b : ZMod c) ↔ a ≡ b [MOD c]

Tactic:
simpa [Int.natCast_modEq_iff] using ZMod.intCast_eq_intCast_iff a b c

Premises used: Int.natCast_modEq_iff, Nat.cast, ZMod.intCast_eq_intCast_iff
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b c : ℕ
⊢ Eq (α := ZMod c) (↑a : ZMod c) (↑b : ZMod c) ↔ a % c = b % c

Tactic:
ZMod.natCast_eq_natCast_iff a b c

Premises used: Nat.ModEq, ZMod.natCast_eq_natCast_iff
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℤ
b : ℕ
rw : Eq (α := ZMod b) (↑a : ZMod b) (↑0 : ZMod b) ↔ (↑b : ℤ) ∣ a
rw₁ : a ≡ 0 [ZMOD (↑b : ℤ)] ↔ (↑b : ℤ) ∣ a
rw₂ rw₃ : (↑b : ℤ) ∣ a ↔ (↑b : ℤ) ∣ a
⊢ Eq (α := ZMod b) (↑a : ZMod b) 0 ↔ (↑b : ℤ) ∣ a

Tactic:
rw [← Int.cast_zero, ZMod.intCast_eq_intCast_iff, Int.modEq_zero_iff_dvd]

Premises used: Int.cast_zero, ZMod.intCast_eq_intCast_iff, Int.modEq_zero_iff_dvd
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b : ℤ
c : ℕ
rw : a ≡ b [ZMOD (↑c : ℤ)] ↔ (↑c : ℤ) ∣ b - a
rw₁ rw₂ : (↑c : ℤ) ∣ b - a ↔ (↑c : ℤ) ∣ b - a
⊢ Eq (α := ZMod c) (↑a : ZMod c) (↑b : ZMod c) ↔ (↑c : ℤ) ∣ b - a

Tactic:
rw [ZMod.intCast_eq_intCast_iff, Int.modEq_iff_dvd]

Premises used: Int.modEq_iff_dvd, ZMod.intCast_eq_intCast_iff
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b : ℕ
rw : Eq (α := ZMod b) (↑a : ZMod b) (↑0 : ZMod b) ↔ b ∣ a
rw₁ : a ≡ 0 [MOD b] ↔ b ∣ a
rw₂ rw₃ : b ∣ a ↔ b ∣ a
⊢ Eq (α := ZMod b) (↑a : ZMod b) 0 ↔ b ∣ a

Tactic:
rw [← Nat.cast_zero, ZMod.natCast_eq_natCast_iff, Nat.modEq_zero_iff_dvd]

Premises used: ZMod.natCast_eq_natCast_iff, Nat.cast_zero, Nat.modEq_zero_iff_dvd
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ℤ
zero : cast (n := 0) (↑a : ZMod 0) = a % (↑0 : ℤ)
succ : ∀ (n : ℕ), cast (n := n + 1) (↑a : ZMod (n + 1)) = a % (↑(n + 1) : ℤ)
⊢ cast (n := n) (↑a : ZMod n) = a % (↑n : ℤ)

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℤ
zero : cast (n := 0) a = a
⊢ cast (n := 0) (↑a : ZMod 0) = a % (↑0 : ℤ)

Tactic:
rw [Int.ofNat_zero, Int.emod_zero, Int.cast_id]

Premises used: Int.ofNat_zero, Int.emod_zero, Int.cast_id
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℤ
⊢ cast (n := 0) a = a

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℤ
n : ℕ
succ : Eq (α := ℤ) (cast (n := n + 1) (↑a : ZMod (n + 1))) (↑(↑(↑a : ZMod (n + 1)) : ℕ) : ℤ)
⊢ cast (n := n + 1) (↑a : ZMod (n + 1)) = a % (↑(n + 1) : ℤ)

Tactic:
rw [← val_intCast, val]

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

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
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
rw₃ rw₄ : Eq (α := ℤ) (x + y).cast (x + y).cast
⊢ (x + y).cast = HAdd.hAdd (α := ℤ) x.cast y.cast % (↑n : ℤ)

Tactic:
rw [← ZMod.coe_intCast, Int.cast_add, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]

Premises used: Int.cast_add, ZMod.intCast_zmod_cast, ZMod.coe_intCast
-- Module: Mathlib.Data.ZMod.Basic
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
rw₃ rw₄ : Eq (α := ℤ) (x * y).cast (x * y).cast
⊢ (x * y).cast = HMul.hMul (α := ℤ) x.cast y.cast % (↑n : ℤ)

Tactic:
rw [← ZMod.coe_intCast, Int.cast_mul, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]

Premises used: Int.cast_mul, ZMod.intCast_zmod_cast, ZMod.coe_intCast
-- Module: Mathlib.Data.ZMod.Basic
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
rw₃ rw₄ : Eq (α := ℤ) (x - y).cast (x - y).cast
⊢ (x - y).cast = HSub.hSub (α := ℤ) x.cast y.cast % (↑n : ℤ)

Tactic:
rw [← ZMod.coe_intCast, Int.cast_sub, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]

Premises used: Int.cast_sub, ZMod.intCast_zmod_cast, ZMod.coe_intCast
-- Module: Mathlib.Data.ZMod.Basic
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)))
rw₂ rw₃ : Eq (α := ℤ) (-x).cast (-x).cast
⊢ (-x).cast = HMod.hMod (α := ℤ) (-x.cast) (↑n : ℤ)

Tactic:
rw [← ZMod.coe_intCast, Int.cast_neg, ZMod.intCast_zmod_cast]

Premises used: Int.cast_neg, ZMod.intCast_zmod_cast, ZMod.coe_intCast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
zero : (↑(-1) : ℕ) = 0
succ : ∀ (n : ℕ), (↑(-1) : ℕ) = n + 1
⊢ (↑(-1) : ℕ) = n

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
⊢ (↑(-1) : ℕ) = 0

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
succ succ₁ : n + 1 = n + 1
⊢ (↑(-1) : ℕ) = n + 1

Tactic:
rw [Fin.coe_neg_one]

Premises used: Fin.coe_neg_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
n : ℕ
zero : cast (n := 0) (-1) = HSub.hSub (α := R) (↑0 : R) 1
succ : ∀ (n : ℕ), cast (n := n + 1) (-1) = HSub.hSub (α := R) (↑(n + 1) : R) 1
⊢ cast (n := n) (-1) = HSub.hSub (α := R) (↑n : R) 1

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
zero : (↑(-1) : R) = HSub.hSub (α := R) (↑0 : R) 1
⊢ cast (n := 0) (-1) = HSub.hSub (α := R) (↑0 : R) 1

Tactic:
dsimp [ZMod, ZMod.cast]

Premises used: ZMod.cast, ZMod
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
⊢ (↑(-1) : R) = HSub.hSub (α := R) (↑0 : R) 1

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
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
succ₃ succ₄ : Eq.{u_1 + 1} (α := R) (↑n : R) (↑n : R)
⊢ cast (n := n + 1) (-1) = HSub.hSub (α := R) (↑(n + 1) : R) 1

Tactic:
rw [← natCast_val, val_neg_one, Nat.cast_succ, add_sub_cancel_right]

Premises used: Nat.cast_succ, ZMod.natCast_val, ZMod.val_neg_one, add_sub_cancel_right
-- Module: Mathlib.Data.ZMod.Basic
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
neg : ∀ (hk : ¬k = 0), (k - 1).cast = HSub.hSub (α := R) k.cast 1
⊢ (k - 1).cast = HSub.hSub (α := R) (if k = 0 then (↑n : R) else k.cast) 1

Tactic:
split_ifs with hk
-- Module: Mathlib.Data.ZMod.Basic
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
pos₂ pos₃ : HSub.hSub (α := R) (↑n : R) 1 = HSub.hSub (α := R) (↑n : R) 1
⊢ (k - 1).cast = HSub.hSub (α := R) (↑n : R) 1

Tactic:
rw [hk, zero_sub, ZMod.cast_neg_one]

Premises used: ZMod.cast_neg_one, zero_sub
-- Module: Mathlib.Data.ZMod.Basic
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
neg₁ : ∀ (n : ℕ) (k : ZMod (n + 1)) (hk : ¬k = 0), (k - 1).cast = HSub.hSub (α := R) k.cast 1
⊢ (k - 1).cast = HSub.hSub (α := R) k.cast 1

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
k : ZMod 0
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]

Premises used: ZMod.cast, ZMod