awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
n k l : ℕ
h : k • p + a = l • p + b
h₁ : k • n • p + n • a = l • n • p + n • b
⊢ ∃ (m : ℕ), ∃ (n_1 : ℕ), m • n • p + n • a = n_1 • n • p + n • b

Tactic:
use k, l
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
n k l : ℕ
h : k • p + a = l • p + b
h₁ : (n * k) • p + n • a = l • n • p + n • b
h₂ : n • k • p + n • a = l • n • p + n • b
h₃ : n • (k • p + a) = l • n • p + n • b
h₄ : n • (l • p + b) = l • n • p + n • b
h₅ : n • l • p + n • b = l • n • p + n • b
h₆ : (l * n) • p + n • b = l • n • p + n • b
h₇ h₈ : l • n • p + n • b = l • n • p + n • b
⊢ k • n • p + n • a = l • n • p + n • b

Tactic:
rw [← mul_nsmul, mul_nsmul', ← nsmul_add, h, nsmul_add, ← mul_nsmul, mul_nsmul']

Premises used: mul_nsmul', mul_nsmul, nsmul_add
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
n : ℕ
⊢ a ≡ b [PMOD p] → a + n • p ≡ b [PMOD p]

Tactic:
(add_nsmul_modEq _).trans

Premises used: AddCommGroup.ModEq.trans, AddCommGroup.add_nsmul_modEq
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
n : ℕ
⊢ a ≡ b [PMOD p] → n • p + a ≡ b [PMOD p]

Tactic:
(nsmul_add_modEq _).trans

Premises used: AddCommGroup.ModEq.trans, AddCommGroup.nsmul_add_modEq
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
h : a ≡ b [PMOD p]
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b

Tactic:
rw [modEq_iff_nsmul] at *

Premises used: AddCommGroup.modEq_iff_nsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
h : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
rcases :
  ∀ (m n : ℕ) (h : m • p + a = n • p + b),
    ∃ (m : ℕ),
      ∃ (n : ℕ),
        HAdd.hAdd (β := N) (HSMul.hSMul (β := N) m ((f : (a : M) → N) p : N)) ((f : (a : M) → N) a : N) =
          HAdd.hAdd (β := N) (HSMul.hSMul (β := N) n ((f : (a : M) → N) p : N)) ((f : (a : M) → N) b : N)
⊢ ∃ (m : ℕ),
    ∃ (n : ℕ),
      HAdd.hAdd (β := N) (HSMul.hSMul (β := N) m ((f : (a : M) → N) p : N)) ((f : (a : M) → N) a : N) =
        HAdd.hAdd (β := N) (HSMul.hSMul (β := N) n ((f : (a : M) → N) p : N)) ((f : (a : M) → N) b : N)

Tactic:
rcases h with ⟨m, n, h⟩
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
m n : ℕ
h : m • p + a = n • p + b
h₁ :
  HAdd.hAdd (β := N) (HSMul.hSMul (β := N) m ((f : (a : M) → N) p : N)) ((f : (a : M) → N) a : N) =
    HAdd.hAdd (β := N) (HSMul.hSMul (β := N) n ((f : (a : M) → N) p : N)) ((f : (a : M) → N) b : N)
⊢ ∃ (m : ℕ),
    ∃ (n : ℕ),
      HAdd.hAdd (β := N) (HSMul.hSMul (β := N) m ((f : (a : M) → N) p : N)) ((f : (a : M) → N) a : N) =
        HAdd.hAdd (β := N) (HSMul.hSMul (β := N) n ((f : (a : M) → N) p : N)) ((f : (a : M) → N) b : N)

Tactic:
use m, n
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
m n : ℕ
h : m • p + a = n • p + b
⊢ HAdd.hAdd (β := N) (HSMul.hSMul (β := N) m ((f : (a : M) → N) p : N)) ((f : (a : M) → N) a : N) =
    HAdd.hAdd (β := N) (HSMul.hSMul (β := N) n ((f : (a : M) → N) p : N)) ((f : (a : M) → N) b : N)

Tactic:
simpa using congr(f $h)
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ ModEq.{u_2} (M := N) ((f : (a : M) → N) p : N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) ↔ a ≡ b [PMOD p]

Tactic:
simp only [modEq_iff_nsmul, ← map_nsmul, ← map_add, hf.eq_iff]

Premises used: Function.Injective.eq_iff, map_add, map_nsmul, AddCommGroup.modEq_iff_nsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
inst_1 : IsAddTorsionFree M
n : ℕ
hn : n ≠ 0
⊢ n • a ≡ n • b [PMOD n • p] ↔ a ≡ b [PMOD p]

Tactic:
simp only [modEq_iff_nsmul, ← mul_nsmul _ n, mul_nsmul' _ n, ← nsmul_add, nsmul_right_inj hn]

Premises used: mul_nsmul', mul_nsmul, nsmul_add, nsmul_right_inj, AddCommGroup.modEq_iff_nsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
h : a ≡ b [PMOD p]
⊢ a + c ≡ b + d [PMOD p] ↔ c ≡ d [PMOD p]

Tactic:
⟨fun hadd ↦ ?_, h.add⟩

Premises used: Iff.intro, AddCommGroup.ModEq.add
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
h : a ≡ b [PMOD p]
refine : ∀ (hadd : a + c ≡ b + d [PMOD p]), c ≡ d [PMOD p]
⊢ a + c ≡ b + d [PMOD p] ↔ c ≡ d [PMOD p]

Tactic:
refine ⟨fun hadd ↦ ?_, h.add⟩
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
h : a ≡ b [PMOD p]
hadd : a + c ≡ b + d [PMOD p]
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b

Tactic:
rw [modEq_iff_nsmul] at *

Premises used: AddCommGroup.modEq_iff_nsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
h : a ≡ b [PMOD p]
hadd : a + c ≡ b + d [PMOD p]
h₁ : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + (a + c) = n • p + (b + d)

Tactic:
rw [modEq_iff_nsmul] at *

Premises used: AddCommGroup.modEq_iff_nsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
h : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
hadd : ∃ (m : ℕ), ∃ (n : ℕ), m • p + (a + c) = n • p + (b + d)
rcases : ∀ (k l : ℕ) (h : k • p + a = l • p + b), ∃ (m : ℕ), ∃ (n : ℕ), m • p + c = n • p + d
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + c = n • p + d

Tactic:
rcases h with ⟨k, l, h⟩
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
hadd : ∃ (m : ℕ), ∃ (n : ℕ), m • p + (a + c) = n • p + (b + d)
k l : ℕ
h : k • p + a = l • p + b
rcases : ∀ (m n : ℕ) (hadd : m • p + (a + c) = n • p + (b + d)), ∃ (m : ℕ), ∃ (n : ℕ), m • p + c = n • p + d
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + c = n • p + d

Tactic:
rcases hadd with ⟨m, n, hadd⟩
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
h₁ : (m + l) • p + c = (n + k) • p + d
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + c = n • p + d

Tactic:
use m + l, n + k
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
h₁ : (m + l) • p + c + a = (n + k) • p + d + a
⊢ (m + l) • p + c = (n + k) • p + d

Tactic:
apply add_right_cancel (b := a)

Premises used: add_right_cancel
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
h₁ : (m + l) • p + (c + a) = (n + k) • p + d + a
h₂ : (m + l) • p + (a + c) = (n + k) • p + d + a
h₃ : m • p + l • p + (a + c) = (n + k) • p + d + a
h₄ : m • p + (a + c) + l • p = (n + k) • p + d + a
h₅ : n • p + (b + d) + l • p = (n + k) • p + d + a
h₆ : n • p + b + d + l • p = (n + k) • p + d + a
h₇ : n • p + d + b + l • p = (n + k) • p + d + a
h₈ : n • p + d + l • p + b = (n + k) • p + d + a
h₉ : n • p + d + (l • p + b) = (n + k) • p + d + a
h₁₀ : n • p + d + (k • p + a) = (n + k) • p + d + a
h₁₁ : n • p + k • p + (d + a) = (n + k) • p + d + a
h₁₂ : n • p + k • p + (d + a) = n • p + k • p + d + a
h₁₃ h₁₄ : n • p + k • p + d + a = n • p + k • p + d + a
⊢ (m + l) • p + c + a = (n + k) • p + d + a

Tactic:
rw [add_assoc, add_comm c, add_nsmul, add_right_comm, hadd, ← add_assoc, add_right_comm _ b,
    add_right_comm _ b, add_assoc, ← h, add_add_add_comm, add_nsmul, ← add_assoc]

Premises used: add_assoc, add_right_comm, add_comm, add_add_add_comm, add_nsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
h : c ≡ d [PMOD p]
⊢ a + c ≡ b + d [PMOD p] ↔ a ≡ b [PMOD p]

Tactic:
simpa only [add_comm c, add_comm d] using h.add_iff_left

Premises used: add_comm, AddCommGroup.ModEq.add_iff_left
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b p c : M
⊢ c + a ≡ c + b [PMOD p] → a ≡ b [PMOD p]

Tactic:
modEq_rfl.add_left_cancel

Premises used: AddCommGroup.ModEq.add_left_cancel, AddCommGroup.modEq_rfl
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b p c : M
⊢ a + c ≡ b + c [PMOD p] → a ≡ b [PMOD p]

Tactic:
modEq_rfl.add_right_cancel

Premises used: AddCommGroup.ModEq.add_right_cancel, AddCommGroup.modEq_rfl
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b p : M
⊢ a + b ≡ a [PMOD p] ↔ b ≡ 0 [PMOD p]

Tactic:
simpa using (modEq_refl a).add_iff_left (d := 0)

Premises used: AddCommGroup.modEq_refl, AddCommGroup.ModEq.add_iff_left
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b p : M
⊢ a + b ≡ b [PMOD p] ↔ a ≡ 0 [PMOD p]

Tactic:
simp [add_comm a]

Premises used: add_comm
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
mp : (∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b) → ∃ (m : ℤ), m • p = b - a
mpr : (∃ (m : ℤ), m • p = b - a) → ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
⊢ (∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b) ↔ ∃ (m : ℤ), m • p = b - a

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
m n : ℕ
h : m • p + a = n • p + b
h₁ : HSub.hSub (α := ℤ) (↑m : ℤ) (↑n : ℤ) • p = b - a
⊢ ∃ (m : ℤ), m • p = b - a

Tactic:
use m - n
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
m n : ℕ
h : m • p + a = n • p + b
h₁ : HSMul.hSMul (α := ℤ) (↑m : ℤ) p + a = HSMul.hSMul (α := ℤ) (↑n : ℤ) p + b
⊢ HSub.hSub (α := ℤ) (↑m : ℤ) (↑n : ℤ) • p = b - a

Tactic:
rw [sub_zsmul, ← sub_eq_add_neg, sub_eq_sub_iff_add_eq_add, add_comm b]

Premises used: sub_eq_add_neg, sub_eq_sub_iff_add_eq_add, add_comm, sub_zsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
m n : ℕ
h : m • p + a = n • p + b
⊢ HSMul.hSMul (α := ℤ) (↑m : ℤ) p + a = HSMul.hSMul (α := ℤ) (↑n : ℤ) p + b

Tactic:
mod_cast h

Premises used: congrArg, cast, HAdd.hAdd, congr, congrFun', Eq.symm, Eq, natCast_zsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
m n : ℕ
h : m • p + a = n • p + b
⊢ HSMul.hSMul (α := ℤ) (↑m : ℤ) p + a = HSMul.hSMul (α := ℤ) (↑n : ℤ) p + b

Tactic:
exact mod_cast h
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
m : ℤ
h : m • p = b - a
h₁ : m.toNat • p + a = (-m).toNat • p + b
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b

Tactic:
use m.toNat, (-m).toNat

Premises used: Int.toNat, Neg.neg
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
m : ℤ
h : m • p = b - a
h₁ : m.toNat • p + a = b + (-m).toNat • p
h₂ : m.toNat • p - (-m).toNat • p = b - a
h₃ : HSMul.hSMul (α := ℤ) (↑m.toNat : ℤ) p - (-m).toNat • p = b - a
h₄ : HSMul.hSMul (α := ℤ) (↑m.toNat : ℤ) p - HSMul.hSMul (α := ℤ) (↑(-m).toNat : ℤ) p = b - a
h₅ : HSMul.hSMul (α := ℤ) (↑m.toNat : ℤ) p + -HSMul.hSMul (α := ℤ) (↑(-m).toNat : ℤ) p = b - a
h₆ : HSub.hSub (α := ℤ) (↑m.toNat : ℤ) (↑(-m).toNat : ℤ) • p = b - a
h₇ h₈ h₉ h₁₀ : m • p = b - a
⊢ m.toNat • p + a = (-m).toNat • p + b

Tactic:
rwa [add_comm _ b, ← sub_eq_sub_iff_add_eq_add, ← natCast_zsmul, ← natCast_zsmul,
      sub_eq_add_neg, ← sub_zsmul, m.toNat_sub_toNat_neg]

Premises used: sub_eq_add_neg, sub_eq_sub_iff_add_eq_add, add_comm, sub_zsmul, Int.toNat_sub_toNat_neg, natCast_zsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
⊢ a ≡ b [PMOD p] ↔ ∃ (m : ℤ), b - a = m • p

Tactic:
simp only [modEq_iff_zsmul, eq_comm]

Premises used: AddCommGroup.modEq_iff_zsmul, eq_comm
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
⊢ -b ≡ -a [PMOD p] ↔ a ≡ b [PMOD p]

Tactic:
simp [modEq_iff_zsmul, neg_add_eq_sub]

Premises used: neg_add_eq_sub, AddCommGroup.modEq_iff_zsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
⊢ b ≡ a [PMOD -p] ↔ a ≡ b [PMOD p]

Tactic:
simp [modEq_iff_zsmul, neg_eq_iff_eq_neg]

Premises used: neg_eq_iff_eq_neg, AddCommGroup.modEq_iff_zsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
a b : G
⊢ HSMul.hSMul (α := ℕ) 1 (b - a) + a = HSMul.hSMul (α := ℕ) 0 (b - a) + b

Tactic:
simp [one_nsmul]

Premises used: one_nsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p : G
z : ℤ
⊢ -z • p = 0 - z • p

Tactic:
simp
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a : G
z : ℤ
⊢ -z • p = a - (a + z • p)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a : G
z : ℤ
⊢ -z • p = a - (z • p + a)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z : ℤ
⊢ a ≡ b [PMOD p] → a + z • p ≡ b [PMOD p]

Tactic:
(add_zsmul_modEq _).trans

Premises used: AddCommGroup.ModEq.trans, AddCommGroup.add_zsmul_modEq
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z : ℤ
⊢ a ≡ b [PMOD p] → z • p + a ≡ b [PMOD p]

Tactic:
(zsmul_add_modEq _).trans

Premises used: AddCommGroup.ModEq.trans, AddCommGroup.zsmul_add_modEq
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z : ℤ
h : a ≡ b [PMOD z • p]
rw : ∀ (h : ∃ (m : ℤ), m • z • p = b - a), ∃ (m : ℤ), m • p = b - a
⊢ a ≡ b [PMOD p]

Tactic:
rw [modEq_iff_zsmul] at *

Premises used: AddCommGroup.modEq_iff_zsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z : ℤ
h : ∃ (m : ℤ), m • z • p = b - a
rcases : ∀ (m : ℤ) (h : m • z • p = b - a), ∃ (m : ℤ), m • p = b - a
⊢ ∃ (m : ℤ), m • p = b - a

Tactic:
rcases h with ⟨m, h⟩
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z m : ℤ
h : m • z • p = b - a
⊢ ∃ (m : ℤ), m • p = b - a

Tactic:
simp [← h, ← mul_zsmul]

Premises used: mul_zsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z : ℤ
h : a ≡ b [PMOD p]
rw : ∀ (h : ∃ (m : ℤ), m • p = b - a), ∃ (m : ℤ), m • z • p = z • b - z • a
⊢ z • a ≡ z • b [PMOD z • p]

Tactic:
rw [modEq_iff_zsmul] at *

Premises used: AddCommGroup.modEq_iff_zsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z : ℤ
h : ∃ (m : ℤ), m • p = b - a
rcases : ∀ (m : ℤ) (h : m • p = b - a), ∃ (m : ℤ), m • z • p = z • b - z • a
⊢ ∃ (m : ℤ), m • z • p = z • b - z • a

Tactic:
rcases h with ⟨m, h⟩
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z m : ℤ
h : m • p = b - a
h₁ : m • z • p = z • b - z • a
⊢ ∃ (m : ℤ), m • z • p = z • b - z • a

Tactic:
use m
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z m : ℤ
h : m • p = b - a
h₁ : m • z • p = z • (b - a)
h₂ : m • z • p = z • m • p
h₃ : (m * z) • p = z • m • p
h₄ h₅ : (m * z) • p = (m * z) • p
⊢ m • z • p = z • b - z • a

Tactic:
rw [← zsmul_sub, ← h, ← mul_zsmul, ← mul_zsmul']

Premises used: mul_zsmul, zsmul_sub, mul_zsmul'
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z : ℤ
inst_1 : IsAddTorsionFree G
hn : z ≠ 0
⊢ z • a ≡ z • b [PMOD z • p] ↔ a ≡ b [PMOD p]

Tactic:
simp [modEq_iff_zsmul, ← zsmul_sub, zsmul_comm, zsmul_right_inj hn]

Premises used: zsmul_comm, AddCommGroup.modEq_iff_zsmul, zsmul_sub, zsmul_right_inj
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a₁ a₂ b₁ b₂ : G
h : a₁ ≡ b₁ [PMOD p]
⊢ a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₂ ≡ b₂ [PMOD p]

Tactic:
simp [sub_eq_add_neg, h]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a₁ a₂ b₁ b₂ : G
h : a₂ ≡ b₂ [PMOD p]
⊢ a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₁ ≡ b₁ [PMOD p]

Tactic:
simp [h, sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b c : G
h : a ≡ b [PMOD p]
⊢ c - a ≡ c - b [PMOD p]

Tactic:
modEq_rfl.sub h

Premises used: AddCommGroup.ModEq.sub, AddCommGroup.modEq_rfl
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b c : G
h : a ≡ b [PMOD p]
⊢ a - c ≡ b - c [PMOD p]

Tactic:
h.sub modEq_rfl

Premises used: AddCommGroup.ModEq.sub, AddCommGroup.modEq_rfl
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b c : G
⊢ c - a ≡ c - b [PMOD p] → a ≡ b [PMOD p]

Tactic:
modEq_rfl.sub_left_cancel

Premises used: AddCommGroup.modEq_rfl, AddCommGroup.ModEq.sub_left_cancel
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b c : G
⊢ a - c ≡ b - c [PMOD p] → a ≡ b [PMOD p]

Tactic:
modEq_rfl.sub_right_cancel

Premises used: AddCommGroup.ModEq.sub_right_cancel, AddCommGroup.modEq_rfl
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b c : G
⊢ a ≡ b - c [PMOD p] ↔ c + a ≡ b [PMOD p]

Tactic:
simp [modEq_iff_zsmul', sub_sub]

Premises used: sub_sub, AddCommGroup.modEq_iff_zsmul'
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b c : G
rw rw₁ : a + c ≡ b [PMOD p] ↔ a + c ≡ b [PMOD p]
⊢ c + a ≡ b [PMOD p] ↔ a + c ≡ b [PMOD p]

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b c : G
⊢ a - b ≡ c [PMOD p] ↔ a ≡ b + c [PMOD p]

Tactic:
modEq_comm.trans <| modEq_sub_iff_add_modEq'.trans modEq_comm

Premises used: AddCommGroup.modEq_sub_iff_add_modEq', AddCommGroup.modEq_comm, Iff.trans
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b c : G
⊢ a - b ≡ c [PMOD p] ↔ a ≡ c + b [PMOD p]

Tactic:
modEq_comm.trans <| modEq_sub_iff_add_modEq.trans modEq_comm

Premises used: AddCommGroup.modEq_comm, Iff.trans, AddCommGroup.modEq_sub_iff_add_modEq
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
⊢ a - b ≡ 0 [PMOD p] ↔ a ≡ b [PMOD p]

Tactic:
simp [sub_modEq_iff_modEq_add]

Premises used: AddCommGroup.sub_modEq_iff_modEq_add
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
simp_rw : (∃ (m : ℤ), b - a = m • p) ↔ ∃ (z : ℤ), b = a + z • p
⊢ a ≡ b [PMOD p] ↔ ∃ (z : ℤ), b = a + z • p

Tactic:
simp_rw [modEq_iff_zsmul', sub_eq_iff_eq_add']

Premises used: AddCommGroup.modEq_iff_zsmul', sub_eq_iff_eq_add'
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a : G
rw : (∃ (z : ℤ), a = 0 + z • p) ↔ ∃ (z : ℤ), a = z • p
⊢ a ≡ 0 [PMOD p] ↔ ∃ (z : ℤ), a = z • p

Tactic:
rw [modEq_comm, modEq_iff_eq_add_zsmul]

Premises used: AddCommGroup.modEq_comm, AddCommGroup.modEq_iff_eq_add_zsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a : G
⊢ (∃ (z : ℤ), a = 0 + z • p) ↔ ∃ (z : ℤ), a = z • p

Tactic:
simp_rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
rw : (¬∃ (z : ℤ), b = a + z • p) ↔ ∀ (z : ℤ), b ≠ a + z • p
rw₁ rw₂ : (∀ (x : ℤ), ¬b = a + x • p) ↔ ∀ (z : ℤ), b ≠ a + z • p
⊢ ¬a ≡ b [PMOD p] ↔ ∀ (z : ℤ), b ≠ a + z • p

Tactic:
rw [modEq_iff_eq_add_zsmul, not_exists]

Premises used: not_exists, AddCommGroup.modEq_iff_eq_add_zsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
simp_rw : b ≡ a [PMOD p] ↔ ∃ (i : ℕ), i < n ∧ b ≡ a - i • p [PMOD n • p]
⊢ a ≡ b [PMOD p] ↔ ∃ (i : ℕ), i < n ∧ a ≡ b + i • p [PMOD n • p]

Tactic:
simp_rw [← sub_modEq_iff_modEq_add, modEq_comm (b := b)]

Premises used: AddCommGroup.modEq_comm, AddCommGroup.sub_modEq_iff_modEq_add
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
simp_rw : (∃ (m : ℤ), a - b = m • p) ↔ ∃ (i : ℕ), i < n ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + (↑i : ℤ)) • p
⊢ b ≡ a [PMOD p] ↔ ∃ (i : ℕ), i < n ∧ b ≡ a - i • p [PMOD n • p]

Tactic:
simp_rw [modEq_iff_zsmul', sub_right_comm, sub_eq_iff_eq_add (b := _ • _), ← natCast_zsmul,
    ← mul_zsmul, ← add_zsmul]

Premises used: add_zsmul, sub_right_comm, mul_zsmul, sub_eq_iff_eq_add, AddCommGroup.modEq_iff_zsmul', natCast_zsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
mp : (∃ (m : ℤ), a - b = m • p) → ∃ (i : ℕ), i < n ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + (↑i : ℤ)) • p
mpr : (∃ (i : ℕ), i < n ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + (↑i : ℤ)) • p) → ∃ (m : ℤ), a - b = m • p
⊢ (∃ (m : ℤ), a - b = m • p) ↔ ∃ (i : ℕ), i < n ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + (↑i : ℤ)) • p

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ ∃ (i : ℕ), i < n ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + (↑i : ℤ)) • p

Tactic:
⟨(k % n).toNat, ?_⟩

Premises used: Nat.cast, HMod.hMod, Exists.intro, Int.toNat
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
mp : (k % (↑n : ℤ)).toNat < n ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + (↑(k % (↑n : ℤ)).toNat : ℤ)) • p
⊢ ∃ (i : ℕ), i < n ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + (↑i : ℤ)) • p

Tactic:
refine ⟨(k % n).toNat, ?_⟩
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
mp : k % (↑n : ℤ) < (↑n : ℤ) ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + k % (↑n : ℤ)) • p
⊢ (k % (↑n : ℤ)).toNat < n ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + (↑(k % (↑n : ℤ)).toNat : ℤ)) • p

Tactic:
rw [← Int.ofNat_lt, Int.toNat_of_nonneg (Int.emod_nonneg _ (mod_cast hn))]

Premises used: Int.toNat_of_nonneg, Int.ofNat_lt, Int.emod_nonneg
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ k % (↑n : ℤ) < (↑n : ℤ) ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + k % (↑n : ℤ)) • p

Tactic:
⟨?_, k / n, ?_⟩

Premises used: HDiv.hDiv, Nat.cast, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
mp : k % (↑n : ℤ) < (↑n : ℤ)
mp₁ : a - b = (k / (↑n : ℤ) * (↑n : ℤ) + k % (↑n : ℤ)) • p
⊢ k % (↑n : ℤ) < (↑n : ℤ) ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + k % (↑n : ℤ)) • p

Tactic:
refine ⟨?_, k / n, ?_⟩
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ k % (↑n : ℤ) < (↑n : ℤ)

Tactic:
Int.emod_lt_of_pos _ ?_

Premises used: Int.emod_lt_of_pos
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
mp : LT.lt (α := ℤ) 0 (↑n : ℤ)
⊢ k % (↑n : ℤ) < (↑n : ℤ)

Tactic:
refine Int.emod_lt_of_pos _ ?_

Premises used: Int.emod_lt_of_pos
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ LT.lt (α := ℤ) 0 (↑n : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
mp : k • p = (k / (↑n : ℤ) * (↑n : ℤ) + k % (↑n : ℤ)) • p
mp₁ mp₂ : k • p = k • p
⊢ a - b = (k / (↑n : ℤ) * (↑n : ℤ) + k % (↑n : ℤ)) • p

Tactic:
rw [hk, Int.ediv_mul_add_emod]

Premises used: Int.ediv_mul_add_emod