awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
A : Type u_2
inst : AddGroup A
f : ℤ →+ A
hf : Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A)
x : ℤ
⊢ (fun (x : ℤ) ↦ HSMul.hSMul (β := ℤ) x (↑n : ℤ)) x ∈ f.ker

Tactic:
simp only [f.map_zsmul, zsmul_zero, f.mem_ker, hf]

Premises used: AddMonoidHom.map_zsmul, zsmul_zero, AddMonoidHom.mem_ker
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
A : Type u_2
inst : AddGroup A
f : ℤ →+ A
h : AddSubgroup.zmultiples (↑n : ℤ) ≤ f.ker
⊢ Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A)

Tactic:
h (AddSubgroup.mem_zmultiples _)

Premises used: AddSubgroup.mem_zmultiples, Set.Mem, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
A : Type u_2
inst : AddGroup A
f : ℤ →+ A
h : AddSubgroup.zmultiples (↑n : ℤ) ≤ f.ker
⊢ Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A)

Tactic:
exact h (AddSubgroup.mem_zmultiples _)

Premises used: AddSubgroup.mem_zmultiples
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
A : Type u_2
inst : AddGroup A
f : { f : ℤ →+ A // Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A) }
x : ℤ
⊢ Eq (α := A)
    ((((lift n : (a : { f : ℤ →+ A // (f : (a : ℤ) → A) (↑n : ℤ) = 0 }) → ZMod n →+ A) f : ZMod n →+ A) :
          (a : ZMod n) → A)
        (↑x : ZMod n) :
      A)
    (((↑f : ℤ →+ A) : (a : ℤ) → A) x : A)

Tactic:
AddMonoidHom.liftOfRightInverse_comp_apply _ _ (fun _ => intCast_zmod_cast _) _ _

Premises used: AddMonoidHom.liftOfRightInverse_comp_apply
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
A : Type u_2
inst : AddGroup A
f : { f : ℤ →+ A // Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A) }
x : ℤ
⊢ Eq (α := A)
    ((((lift n : (a : { f : ℤ →+ A // (f : (a : ℤ) → A) (↑n : ℤ) = 0 }) → ZMod n →+ A) f : ZMod n →+ A) :
          (a : ZMod n) → A)
        ((Int.castAddHom (ZMod n) : (a : ℤ) → ZMod n) x : ZMod n) :
      A)
    (((↑f : ℤ →+ A) : (a : ℤ) → A) x : A)

Tactic:
AddMonoidHom.liftOfRightInverse_comp_apply _ _ (fun _ => intCast_zmod_cast _) _ _

Premises used: AddMonoidHom.liftOfRightInverse_comp_apply
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
A : Type u_2
inst : AddGroup A
f : { f : ℤ →+ A // Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A) }
⊢ Eq (α := ℤ → A)
    (comp (β := ZMod n)
      (⇑((lift n : (a : { f : ℤ →+ A // (f : (a : ℤ) → A) (↑n : ℤ) = 0 }) → ZMod n →+ A) f : ZMod n →+ A) :
        (a : ZMod n) → A)
      Int.cast)
    (⇑(↑f : ℤ →+ A) : (a : ℤ) → A)

Tactic:
funext <| lift_coe _ _

Premises used: funext, ZMod.lift_coe
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
A : Type u_2
inst : AddGroup A
f : { f : ℤ →+ A // Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A) }
⊢ AddMonoidHom.comp (N := ZMod n) ((lift n : (a : { f : ℤ →+ A // (f : (a : ℤ) → A) (↑n : ℤ) = 0 }) → ZMod n →+ A) f)
      (Int.castAddHom (ZMod n)) =
    (↑f : ℤ →+ A)

Tactic:
AddMonoidHom.ext <| lift_castAddHom _ _

Premises used: ZMod.lift_castAddHom, AddMonoidHom.ext
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
A : Type u_2
inst : AddGroup A
f : { f : ℤ →+ A // Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A) }
⊢ Injective (α := ZMod n) (β := A)
      (⇑((lift n : (a : { f : ℤ →+ A // (f : (a : ℤ) → A) (↑n : ℤ) = 0 }) → ZMod n →+ A) f : ZMod n →+ A) :
        (a : ZMod n) → A) ↔
    ∀ (m : ℤ), Eq (α := A) (((↑f : ℤ →+ A) : (a : ℤ) → A) m : A) (0 : A) → Eq (α := ZMod n) (↑m : ZMod n) 0

Tactic:
simp only [← AddMonoidHom.ker_eq_bot_iff, eq_bot_iff, SetLike.le_def,
    ZMod.intCast_surjective.forall, ZMod.lift_coe, AddMonoidHom.mem_ker, AddSubgroup.mem_bot]

Premises used: Function.Surjective.forall, AddMonoidHom.ker_eq_bot_iff, SetLike.le_def, AddSubgroup.mem_bot, ZMod.lift_coe, eq_bot_iff, AddMonoidHom.mem_ker, ZMod.intCast_surjective
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
S : Type u_1
G : Type u_2
inst : AddCommGroup G
inst_1 : SetLike S G
inst_2 : AddSubgroupClass S G
K : S
inst_3 : Module (ZMod n) G
x : G
hx : x ∈ K
⊢ ∀ (a : ZMod n), a • x ∈ K

Tactic:
simpa [ZMod.forall, Int.cast_smul_eq_zsmul] using zsmul_mem hx

Premises used: zsmul_mem, ZMod.forall, Int.cast_smul_eq_zsmul
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
S : Type u_1
G : Type u_2
inst : AddCommGroup G
inst_1 : SetLike S G
inst_2 : AddSubgroupClass S G
K : S
inst_3 : Module (ZMod n) G
a : ZMod n
x : ↥K
⊢ (↑(a • x) : G) = a • (↑x : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
G : Type u_2
inst : AddCommGroup G
inst_1 : Module (ZMod n) G
x : G
⊢ n • x = 0

Tactic:
simp [← Nat.cast_smul_eq_nsmul (ZMod n)]

Premises used: ZMod, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Data.ZMod.Basic
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : Nontrivial G
inst_2 : Module (ZMod 1) G
obtain : ∀ (x : G) (hx : x ≠ 0), False
⊢ False

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : G)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Data.ZMod.Basic
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : Nontrivial G
inst_2 : Module (ZMod 1) G
x : G
hx : x ≠ 0
⊢ x = 0

Tactic:
simpa using char_nsmul_eq_zero 1 x

Premises used: ZModModule.char_nsmul_eq_zero, OfNat.ofNat
-- Module: Mathlib.Data.ZMod.Basic
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : Nontrivial G
inst_2 : Module (ZMod 1) G
x : G
hx : x ≠ 0
⊢ False

Tactic:
exact hx <| by simpa using char_nsmul_eq_zero 1 x
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
G : Type u_2
inst : AddCommGroup G
inst_1 : Module (ZMod n) G
inst_2 : NeZero n
inst_3 : Nontrivial G
⊢ n ≠ 0

Tactic:
have := NeZero.ne n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
G : Type u_2
inst : AddCommGroup G
inst_1 : Module (ZMod n) G
inst_2 : NeZero n
inst_3 : Nontrivial G
this : n ≠ 0
⊢ n ≠ 1

Tactic:
have := char_ne_one n G
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
G : Type u_2
inst : AddCommGroup G
inst_1 : Module (ZMod n) G
inst_2 : NeZero n
inst_3 : Nontrivial G
this_1 : n ≠ 0
this : n ≠ 1
⊢ 2 ≤ n

Tactic:
lia
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
G : Type u_2
inst : AddCommGroup G
inst_1 : Module (ZMod n) G
inst_2 : NeZero n
x y : G
⊢ IsPeriodicPt (fun (x_1 : G) ↦ x + x_1) n y

Tactic:
simpa [char_nsmul_eq_zero, IsPeriodicPt] using isFixedPt_id _

Premises used: ZModModule.char_nsmul_eq_zero, Function.isFixedPt_id, Function.IsPeriodicPt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : Module (ZMod 2) G
x : G
⊢ x + x = 0

Tactic:
simpa [two_nsmul] using char_nsmul_eq_zero 2 x

Premises used: ZModModule.char_nsmul_eq_zero, OfNat.ofNat, two_nsmul
-- Module: Mathlib.Data.ZMod.Basic
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : Module (ZMod 2) G
x : G
⊢ -x = x

Tactic:
simp [add_self, eq_comm, ← sub_eq_zero]

Premises used: sub_eq_zero, eq_comm, ZModModule.add_self
-- Module: Mathlib.Data.ZMod.Basic
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : Module (ZMod 2) G
x y : G
⊢ x - y = x + y

Tactic:
simp [neg_eq_self, sub_eq_add_neg]

Premises used: sub_eq_add_neg, ZModModule.neg_eq_self
-- Module: Mathlib.Data.ZMod.Basic
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : Module (ZMod 2) G
x y z : G
⊢ x + y + (y + z) = x + z

Tactic:
simpa [sub_eq_add] using sub_add_sub_cancel x y z

Premises used: sub_add_sub_cancel, ZModModule.sub_eq_add
-- Module: Mathlib.Data.ZMod.Basic
Goal:
α : Type u_1
inst : Group α
n : ℕ
hn : (Nat.card α).gcd n = 1
a : α
⊢ (Nat.card α).Coprime n

Tactic:
replace hn : (Nat.card α).Coprime n := hn
-- Module: Mathlib.Data.ZMod.Basic
Goal:
α : Type u_1
inst : Group α
n : ℕ
a : α
hn : (Nat.card α).Coprime n
rw : a ^ (n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) = a
rw₁ : a ^ (n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹ % Nat.card α) = a
rw₂ : a ^ val (n := Nat.card α) (↑(n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) : ZMod (Nat.card α)) = a
rw₃ :
  a ^
      (HMul.hMul (α := ZMod (Nat.card α)) (↑n : ZMod (Nat.card α))
          (↑(val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) : ZMod (Nat.card α))).val =
    a
rw₄ : a ^ val (n := Nat.card α) 1 = a
rw₅ : a ^ (1 % Nat.card α) = a
rw₆ : HPow.hPow (β := ℕ) a 1 = a
rw₇ rw₈ : a = a
⊢ (a ^ val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) ^ n = a

Tactic:
rw [← pow_mul', ← pow_mod_natCard, ← ZMod.val_natCast, Nat.cast_mul, ZMod.mul_val_inv hn.symm,
    ZMod.val_one_eq_one_mod, pow_mod_natCard, pow_one]

Premises used: Nat.Coprime.symm, pow_mod_natCard, ZMod.val_one_eq_one_mod, ZMod.mul_val_inv, Nat.cast_mul, pow_one, ZMod.val_natCast, pow_mul'
-- Module: Mathlib.Data.ZMod.Basic
Goal:
α : Type u_1
inst : Group α
n : ℕ
hn : (Nat.card α).gcd n = 1
a : α
rw : (a ^ val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) ^ n = a
rw₁ rw₂ : a = a
⊢ (a ^ n) ^ val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹ = a

Tactic:
rw [pow_right_comm, pow_zmod_val_inv_pow hn]

Premises used: pow_right_comm, pow_zmod_val_inv_pow
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m k : ℕ
h :
  ∀ (n : ℕ),
    Membership.mem (γ := Set ℕ) (Set.range fun (n : ℕ) ↦ m * n + k) n ↔
      Membership.mem (γ := Set ℕ) {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} n
⊢ Eq (α := Set ℕ) (Set.range fun (n : ℕ) ↦ m * n + k) {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n}

Tactic:
ext n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m k n : ℕ
h : ∀ (y : ℕ), m * y + k = n
| (∃ (y : ℕ), m * y + k = n) ↔ Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n

Tactic:
enter [1, 1, y]
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m k n y : ℕ
h : n = k + m * y
| m * y + k = n

Tactic:
rw [add_comm, eq_comm]

Premises used: eq_comm, add_comm
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m k n : ℕ
h : ∀ (y : ℕ), n = k + m * y
| (∃ (y : ℕ), m * y + k = n) ↔ Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n

Tactic:
enter [1, 1, y]; rw [add_comm, eq_comm]

Premises used: eq_comm, add_comm
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m k n : ℕ
h : (∃ (y : ℕ), n = k + m * y) ↔ Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n
⊢ (∃ (y : ℕ), m * y + k = n) ↔ Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n

Tactic:
conv => enter [1, 1, y]; rw [add_comm, eq_comm]

Premises used: eq_comm, add_comm
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m k n : ℕ
⊢ (∃ (y : ℕ), n = k + m * y) ↔ Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n

Tactic:
⟨fun ⟨a, ha⟩ ↦ ⟨?_, le_iff_exists_add.mpr ⟨_, ha⟩⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩

Premises used: Iff.mpr, HMul.hMul, le_iff_exists_add, _private.0.Nat.range_mul_add.match_1, Exists, LE.le, Nat.cast, _private.0.Nat.range_mul_add.match_2, And, HAdd.hAdd, And.intro, Iff.intro, Exists.intro, Eq
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m k n : ℕ
h : (∃ (y : ℕ), n = k + m * y) → ∀ (a : ℕ) (ha : n = k + m * a), Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)
h₁ :
  Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n →
    ∀ (H₁ : Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)) (H₂ : k ≤ n), ∃ (y : ℕ), n = k + m * y
⊢ (∃ (y : ℕ), n = k + m * y) ↔ Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n

Tactic:
refine ⟨fun ⟨a, ha⟩ ↦ ⟨?_, le_iff_exists_add.mpr ⟨_, ha⟩⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m k n : ℕ
h : ∃ (y : ℕ), n = k + m * y
a : ℕ
ha : n = k + m * a
⊢ Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)

Tactic:
simpa using congr_arg ((↑) : ℕ → ZMod m) ha

Premises used: Nat.cast, congr_arg
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m k n : ℕ
h_1 : Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n
H₁ : Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)
H₂ : k ≤ n
h : ∀ (a : ℕ) (ha : n = k + a), ∃ (y : ℕ), n = k + m * y
⊢ ∃ (y : ℕ), n = k + m * y

Tactic:
obtain ⟨a, ha⟩ := le_iff_exists_add.mp H₂

Premises used: le_iff_exists_add, Iff.mp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m k n : ℕ
h : Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n
H₁ : Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)
H₂ : k ≤ n
a : ℕ
ha : n = k + a
⊢ m ∣ a

Tactic:
simp only [ha, Nat.cast_add, add_eq_left, ZMod.natCast_eq_zero_iff] at H₁

Premises used: ZMod.natCast_eq_zero_iff, Nat.cast_add, add_eq_left
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m k n : ℕ
h_1 : Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n
H₂ : k ≤ n
a : ℕ
ha : n = k + a
H₁ : m ∣ a
h : ∀ (b : ℕ) (ha : n = k + m * b), ∃ (y : ℕ), n = k + m * y
⊢ ∃ (y : ℕ), n = k + m * y

Tactic:
obtain ⟨b, rfl⟩ := H₁

Premises used: rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m k n : ℕ
h : Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n
H₂ : k ≤ n
b : ℕ
ha : n = k + m * b
⊢ ∃ (y : ℕ), n = k + m * y

Tactic:
⟨b, ha⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m k n : ℕ
h : Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n
H₂ : k ≤ n
b : ℕ
ha : n = k + m * b
⊢ ∃ (y : ℕ), n = k + m * y

Tactic:
exact ⟨b, ha⟩
-- Module: Mathlib.Data.ZMod.Basic
Goal:
N : ℕ
inst : NeZero N
n : ℕ
⊢ (fun (p : ZMod N × ℕ) ↦ p.1.val + N * p.2) ((fun (n : ℕ) ↦ (((↑n : ZMod N), n / N) : ZMod N × ℕ)) n) = n

Tactic:
simpa only [val_natCast] using mod_add_div n N

Premises used: Nat.mod_add_div, ZMod.val_natCast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
N : ℕ
inst : NeZero N
p : ZMod N × ℕ
fst : ((fun (n : ℕ) ↦ (((↑n : ZMod N), n / N) : ZMod N × ℕ)) ((fun (p : ZMod N × ℕ) ↦ p.1.val + N * p.2) p)).1 = p.1
snd : ((fun (n : ℕ) ↦ (((↑n : ZMod N), n / N) : ZMod N × ℕ)) ((fun (p : ZMod N × ℕ) ↦ p.1.val + N * p.2) p)).2 = p.2
⊢ (fun (n : ℕ) ↦ (((↑n : ZMod N), n / N) : ZMod N × ℕ)) ((fun (p : ZMod N × ℕ) ↦ p.1.val + N * p.2) p) = p

Tactic:
ext1
-- Module: Mathlib.Data.ZMod.Basic
Goal:
N : ℕ
inst : NeZero N
p : ZMod N × ℕ
⊢ ((fun (n : ℕ) ↦ (((↑n : ZMod N), n / N) : ZMod N × ℕ)) ((fun (p : ZMod N × ℕ) ↦ p.1.val + N * p.2) p)).1 = p.1

Tactic:
simp only [add_comm p.1.val, cast_add, cast_mul, natCast_self, zero_mul, natCast_val,
        cast_id', id_eq, zero_add]

Premises used: ZMod.natCast_self, MulZeroClass.zero_mul, ZMod.natCast_val, zero_add, add_comm, Prod.fst, ZMod.cast_id', Nat.cast_add, Nat.cast_mul, id_eq, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
N : ℕ
inst : NeZero N
p : ZMod N × ℕ
⊢ ((fun (n : ℕ) ↦ (((↑n : ZMod N), n / N) : ZMod N × ℕ)) ((fun (p : ZMod N × ℕ) ↦ p.1.val + N * p.2) p)).2 = p.2

Tactic:
simp only [add_comm p.1.val, mul_add_div (NeZero.pos _),
        (Nat.div_eq_zero_iff).2 <| .inr p.1.val_lt, add_zero]

Premises used: Iff.mpr, Nat.mul_add_div, add_comm, Prod.fst, Nat.div_eq_zero_iff, NeZero.pos, add_zero, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
M : Type u_1
inst : AddCommMonoid M
zero : Subsingleton.{max (u_1 + 1) 1} (Module (ZMod 0) M)
succ : ∀ (n : ℕ), Subsingleton.{max (u_1 + 1) 1} (Module (ZMod (n + 1)) M)
⊢ Subsingleton.{max (u_1 + 1) 1} (Module (ZMod n) M)

Tactic:
obtain _ | n := n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
⊢ Subsingleton.{max (u_1 + 1) 1} (Module (ZMod 0) M)

Tactic:
inferInstanceAs (Subsingleton (Module ℤ M))

Premises used: _private.0.ZMod.instSubsingletonModule._proof_1
-- Module: Mathlib.Data.ZMod.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
⊢ Subsingleton.{max (u_1 + 1) 1} (Module (ZMod 0) M)

Tactic:
exact inferInstanceAs (Subsingleton (Module ℤ M))
-- Module: Mathlib.Data.ZMod.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
n : ℕ
⊢ Subsingleton.{max (u_1 + 1) 1} (Module (ZMod (n + 1)) M)

Tactic:
⟨fun m1 m2 ↦ Module.ext' _ _ fun r m ↦ ?_⟩

Premises used: Module.ext', Subsingleton.intro
-- Module: Mathlib.Data.ZMod.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
n : ℕ
succ : ∀ (m1 m2 : Module (ZMod (n + 1)) M) (r : ZMod (n + 1)) (m : M), r • m = r • m
⊢ Subsingleton.{max (u_1 + 1) 1} (Module (ZMod (n + 1)) M)

Tactic:
refine ⟨fun m1 m2 ↦ Module.ext' _ _ fun r m ↦ ?_⟩
-- Module: Mathlib.Data.ZMod.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
n : ℕ
m1 m2 : Module (ZMod (n + 1)) M
r : ZMod (n + 1)
m : M
succ :
  ∀ (r : ℕ),
    HSMul.hSMul (α := ZMod (n + 1)) (↑r : ZMod (n + 1)) m = HSMul.hSMul (α := ZMod (n + 1)) (↑r : ZMod (n + 1)) m
⊢ r • m = r • m

Tactic:
obtain ⟨r, rfl⟩ := ZMod.natCast_zmod_surjective r

Premises used: ZMod.natCast_zmod_surjective, rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
n : ℕ
m1 m2 : Module (ZMod (n + 1)) M
m : M
r : ℕ
succ : r • m = HSMul.hSMul (α := ZMod (n + 1)) (↑r : ZMod (n + 1)) m
succ₁ succ₂ : r • m = r • m
⊢ HSMul.hSMul (α := ZMod (n + 1)) (↑r : ZMod (n + 1)) m = HSMul.hSMul (α := ZMod (n + 1)) (↑r : ZMod (n + 1)) m

Tactic:
rw [(letI := m1; Nat.cast_smul_eq_nsmul _ r m), Nat.cast_smul_eq_nsmul _ r m]

Premises used: Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Data.ZMod.Coprime
Goal:
n : ℤ
m : ℕ
rw : Associated (M := ZMod m) (↑n : ZMod m) (↑n.natAbs : ZMod (↑m : ℤ).natAbs)
⊢ IsUnit (M := ZMod m) (↑n : ZMod m) ↔ IsCoprime (↑m : ℤ) n

Tactic:
rw [Int.isCoprime_iff_nat_coprime, Nat.coprime_comm, ← isUnit_iff_coprime, Associated.isUnit_iff]

Premises used: ZMod.isUnit_iff_coprime, Int.isCoprime_iff_nat_coprime, Associated.isUnit_iff, Nat.coprime_comm
-- Module: Mathlib.Data.ZMod.Coprime
Goal:
n : ℤ
m : ℕ
⊢ Associated (M := ZMod m) (↑n : ZMod m) (↑n.natAbs : ZMod (↑m : ℤ).natAbs)

Tactic:
simpa only [eq_intCast, Int.cast_natCast] using (Int.associated_natAbs _).map (Int.castRingHom _)

Premises used: Int.cast_natCast, eq_intCast, Int.castRingHom, Associated.map, Int.associated_natAbs
-- Module: Mathlib.Data.ZMod.Coprime
Goal:
a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
rw : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬a.gcd (↑p : ℤ) = 1
rw₁ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬Int.gcd (↑p : ℤ) a = 1
rw₂ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬IsCoprime (↑p : ℤ) a
rw₃ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬¬(↑p : ℤ) ∣ a
rw₄ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ (↑p : ℤ) ∣ a
rw₅ rw₆ : (↑p : ℤ) ∣ a ↔ (↑p : ℤ) ∣ a
⊢ Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ a.gcd (↑p : ℤ) ≠ 1

Tactic:
rw [Ne, Int.gcd_comm, ← Int.isCoprime_iff_gcd_eq_one,
    (Nat.prime_iff_prime_int.1 pp.1).coprime_iff_not_dvd, Classical.not_not,
    intCast_zmod_eq_zero_iff_dvd]

Premises used: Nat.prime_iff_prime_int, Prime.coprime_iff_not_dvd, Int.isCoprime_iff_gcd_eq_one, Classical.not_not, Ne, ZMod.intCast_zmod_eq_zero_iff_dvd, Iff.mp, Int.gcd_comm, Fact.out
-- Module: Mathlib.Data.ZMod.Coprime
Goal:
a : ℤ
p : ℕ
pp : Nat.Prime p
h : a.gcd (↑p : ℤ) = 1
⊢ Ne (α := ZMod p) (↑a : ZMod p) 0

Tactic:
mt (@eq_zero_iff_gcd_ne_one a p ⟨pp⟩).mp (Classical.not_not.mpr h)

Premises used: Iff.mpr, Classical.not_not, mt, ZMod.eq_zero_iff_gcd_ne_one, Iff.mp
-- Module: Mathlib.Data.ZMod.Coprime
Goal:
a : ℤ
p : ℕ
pp : Nat.Prime p
h : a.gcd (↑p : ℤ) ≠ 1
⊢ Eq (α := ZMod p) (↑a : ZMod p) 0

Tactic:
(@eq_zero_iff_gcd_ne_one a p ⟨pp⟩).mpr h

Premises used: Iff.mpr, ZMod.eq_zero_iff_gcd_ne_one
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : NeZero n
x : ℤ
rw : (↑(if 0 ≤ x then (↑x.natAbs : Fin n) else -(↑x.natAbs : Fin n)) : ℕ) = (x % (↑n : ℤ)).toNat
⊢ (↑(↑x : Fin n) : ℕ) = (x % (↑n : ℤ)).toNat

Tactic:
rw [Fin.intCast_def']

Premises used: Fin.intCast_def'
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : NeZero n
x : ℤ
isTrue : 0 ≤ x → (↑(↑x.natAbs : Fin n) : ℕ) = (x % (↑n : ℤ)).toNat
isFalse : ¬0 ≤ x → (↑(-(↑x.natAbs : Fin n)) : ℕ) = (x % (↑n : ℤ)).toNat
⊢ (↑(if 0 ≤ x then (↑x.natAbs : Fin n) else -(↑x.natAbs : Fin n)) : ℕ) = (x % (↑n : ℤ)).toNat

Tactic:
split
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h : 0 ≤ x
⊢ (↑(↑x.natAbs : Fin n) : ℕ) = (x % (↑n : ℤ)).toNat

Tactic:
simp [Int.emod_natAbs_of_nonneg h]

Premises used: Int.emod_natAbs_of_nonneg
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h : ¬0 ≤ x
isFalse : (if n ∣ x.natAbs then 0 else n - x.natAbs % n) = (x % (↑n : ℤ)).toNat
⊢ (↑(-(↑x.natAbs : Fin n)) : ℕ) = (x % (↑n : ℤ)).toNat

Tactic:
simp only [Fin.val_neg, Fin.natCast_eq_zero, Fin.val_natCast]

Premises used: Fin.val_natCast, Fin.natCast_eq_zero, Fin.val_neg
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h : ¬0 ≤ x
isFalse : n ∣ x.natAbs → 0 = (x % (↑n : ℤ)).toNat
isFalse₁ : ¬n ∣ x.natAbs → n - x.natAbs % n = (x % (↑n : ℤ)).toNat
⊢ (if n ∣ x.natAbs then 0 else n - x.natAbs % n) = (x % (↑n : ℤ)).toNat

Tactic:
split
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h_1 : ¬0 ≤ x
h : n ∣ x.natAbs
⊢ (↑n : ℤ) ∣ x

Tactic:
rw [← Int.natCast_dvd] at h

Premises used: Int.natCast_dvd
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h_1 : ¬0 ≤ x
h : (↑n : ℤ) ∣ x
isFalse : 0 = toNat 0
isFalse₁ isFalse₂ : Eq (α := ℕ) 0 0
⊢ 0 = (x % (↑n : ℤ)).toNat

Tactic:
rw [Int.emod_eq_zero_of_dvd h, Int.toNat_zero]

Premises used: Int.toNat_zero, Int.emod_eq_zero_of_dvd
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h_1 : ¬0 ≤ x
h : ¬n ∣ x.natAbs
⊢ x < 0

Tactic:
lia
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h_1 : ¬0 ≤ x
h : ¬n ∣ x.natAbs
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : ¬(↑n : ℤ) ∣ x), ¬(↑n : ℤ) ∣ x
⊢ ¬(↑n : ℤ) ∣ x

Tactic:
rwa [← Int.natCast_dvd] at h

Premises used: Int.natCast_dvd
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h_1 : ¬0 ≤ x
h : ¬n ∣ x.natAbs
isFalse : n - (n - (x % (↑n : ℤ)).toNat) = (x % (↑n : ℤ)).toNat
⊢ n - x.natAbs % n = (x % (↑n : ℤ)).toNat

Tactic:
rw [Int.emod_natAbs_of_neg (by lia) (NeZero.ne n),
        if_neg (by rwa [← Int.natCast_dvd] at h)]

Premises used: Int.emod_natAbs_of_neg, if_neg, NeZero.ne
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h_1 : ¬0 ≤ x
h : ¬n ∣ x.natAbs
⊢ n ≠ 0

Tactic:
have := NeZero.ne n
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h_1 : ¬0 ≤ x
h : ¬n ∣ x.natAbs
this : n ≠ 0
⊢ LT.lt (α := ℤ) 0 (↑n : ℤ)

Tactic:
lia
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h_1 : ¬0 ≤ x
h : ¬n ∣ x.natAbs
⊢ x % (↑n : ℤ) < (↑n : ℤ)

Tactic:
have : x % n < n := Int.emod_lt_of_pos x (by have := NeZero.ne n; lia)
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h_1 : ¬0 ≤ x
h : ¬n ∣ x.natAbs
this : x % (↑n : ℤ) < (↑n : ℤ)
⊢ n - (n - (x % (↑n : ℤ)).toNat) = (x % (↑n : ℤ)).toNat

Tactic:
lia
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
x x_1 x_2 : Fin n
a : ℕ
isLt : a < n
b : ℕ
isLt_1 : b < n
c : ℕ
isLt_2 : c < n
rw rw₁ : a * (b * c) ≡ a * (b * c) [MOD n]
⊢ a * b * c ≡ a * (b * c) [MOD n]

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
x x_1 x_2 : Fin n
a : ℕ
isLt : a < n
b : ℕ
isLt_1 : b < n
c : ℕ
isLt_2 : c < n
rw rw₁ : a * b + a * c ≡ a * b + a * c [MOD n]
⊢ a * (b + c) ≡ a * b + a * c [MOD n]

Tactic:
rw [mul_add]

Premises used: mul_add
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
a b c : Fin n
rw : c * (a + b) = a * c + b * c
rw₁ : c * a + c * b = a * c + b * c
rw₂ : c * a + b * c = a * c + b * c
rw₃ rw₄ : a * c + b * c = a * c + b * c
⊢ (a + b) * c = a * c + b * c

Tactic:
rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm]

Premises used: _private.0.Fin.left_distrib_aux, mul_comm
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : NeZero n
⊢ NeZero (R := Fin (n + 1)) 1

Tactic:
open Fin.CommRing in inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.ZMod.Defs
Goal:
⊢ Infinite (ZMod 0)

Tactic:
Int.infinite

Premises used: ZMod, Int.infinite
-- Module: Mathlib.Data.ZMod.Defs
Goal:
inst : Fintype (ZMod 0)
⊢ Fintype.card (ZMod 0) = 0

Tactic:
(not_finite (ZMod 0)).elim

Premises used: False.elim, ZMod, OfNat.ofNat, not_finite
-- Module: Mathlib.Data.ZMod.Defs
Goal:
inst : Fintype (ZMod 0)
⊢ Fintype.card (ZMod 0) = 0

Tactic:
exact (not_finite (ZMod 0)).elim

Premises used: False.elim, ZMod, OfNat.ofNat, not_finite
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : Fintype (ZMod (n + 1))
⊢ Fintype.card (Fin (n + 1)) = n + 1

Tactic:
Fintype.card_fin (n + 1)

Premises used: Fintype.card_fin, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : Fintype (ZMod (n + 1))
⊢ Fintype.card (ZMod (n + 1)) = n + 1

Tactic:
convert! Fintype.card_fin (n + 1) using 2

Premises used: Fintype.card_fin, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.ZMod.Defs
Goal:
n : ℕ
inst : Fintype (ZMod n)
zero : ∀ [inst : Fintype (ZMod 0)], Fintype.card (ZMod 0) = 0
succ : ∀ (n : ℕ) [inst : Fintype (ZMod (n + 1))], Fintype.card (ZMod (n + 1)) = n + 1
⊢ Fintype.card (ZMod n) = n

Tactic:
cases n with
  | zero => exact (not_finite (ZMod 0)).elim
  | succ n => convert! Fintype.card_fin (n + 1) using 2

Premises used: Fintype.card_fin, HAdd.hAdd, OfNat.ofNat