awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
inr : ∀ (h : l = n.divMaxPow p) (hl : ¬p ∣ l) (hp : 1 < p) (hk : k = (p.maxPowDvdDiv n).fst), p.maxPowDvdDiv n = (k, l)
inr₁ :
  ∀ (h : p ^ (p.maxPowDvdDiv n).fst * l = p ^ (p.maxPowDvdDiv n).fst * n.divMaxPow p) (hl : ¬p ∣ l) (hp : 1 < p)
    (hk : k = (p.maxPowDvdDiv n).fst), 0 < p ^ (p.maxPowDvdDiv n).fst
⊢ p.maxPowDvdDiv n = (k, l)

Tactic:
rw [← pow_padicValNat_mul_divMaxPow p n, hk, padicValNat, Nat.mul_left_cancel_iff] at h

Premises used: Nat.mul_left_cancel_iff, padicValNat, Nat.pow_padicValNat_mul_divMaxPow
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n k l : ℕ
hn : n ≠ 0
h : l = n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ p.maxPowDvdDiv n = (k, l)

Tactic:
Prod.ext hk.symm h.symm

Premises used: Prod.ext, Eq.symm
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n k l : ℕ
hn : n ≠ 0
h : l = n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ p.maxPowDvdDiv n = (k, l)

Tactic:
exact Prod.ext hk.symm h.symm

Premises used: Prod.ext
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ (p.maxPowDvdDiv n).fst * l = p ^ (p.maxPowDvdDiv n).fst * n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ 0 < p ^ (p.maxPowDvdDiv n).fst

Tactic:
Nat.pow_pos <| Nat.zero_lt_of_lt hp

Premises used: Nat.zero_lt_of_lt, Nat.pow_pos
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ (p.maxPowDvdDiv n).fst * l = p ^ (p.maxPowDvdDiv n).fst * n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ 0 < p ^ (p.maxPowDvdDiv n).fst

Tactic:
exact Nat.pow_pos <| Nat.zero_lt_of_lt hp

Premises used: Nat.zero_lt_of_lt, Nat.pow_pos
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
hn₁ : p ^ k * n ≠ 0
h : p ^ (padicValNat p n + k) * n.divMaxPow p = p ^ k * n
hl : ¬p ∣ n.divMaxPow p
⊢ p.maxPowDvdDiv (p ^ k * n) = (padicValNat p n + k, n.divMaxPow p)

Tactic:
apply maxPowDvdDiv_of_pow_mul_eq

Premises used: Nat.maxPowDvdDiv_of_pow_mul_eq
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p ^ k * n ≠ 0

Tactic:
Nat.mul_ne_zero (Nat.ne_of_gt <| Nat.pow_pos <| Nat.zero_lt_of_lt hp) hn

Premises used: Nat.mul_ne_zero, Nat.zero_lt_of_lt, Nat.pow_pos, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p ^ k * n ≠ 0

Tactic:
exact Nat.mul_ne_zero (Nat.ne_of_gt <| Nat.pow_pos <| Nat.zero_lt_of_lt hp) hn

Premises used: Nat.mul_ne_zero, Nat.zero_lt_of_lt, Nat.pow_pos, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
h : p ^ padicValNat p n * p ^ k * n.divMaxPow p = p ^ k * n
h₁ : p ^ padicValNat p n * (p ^ k * n.divMaxPow p) = p ^ k * n
h₂ : p ^ k * (p ^ padicValNat p n * n.divMaxPow p) = p ^ k * n
h₃ h₄ : p ^ k * n = p ^ k * n
⊢ p ^ (padicValNat p n + k) * n.divMaxPow p = p ^ k * n

Tactic:
rw [Nat.pow_add, Nat.mul_assoc, Nat.mul_left_comm, pow_padicValNat_mul_divMaxPow]

Premises used: Nat.pow_add, Nat.mul_left_comm, Nat.mul_assoc, Nat.pow_padicValNat_mul_divMaxPow
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ ¬p ∣ n.divMaxPow p

Tactic:
not_dvd_divMaxPow hp hn

Premises used: Nat.not_dvd_divMaxPow
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ ¬p ∣ n.divMaxPow p

Tactic:
exact not_dvd_divMaxPow hp hn

Premises used: Nat.not_dvd_divMaxPow
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ padicValNat p (p ^ k * n) = padicValNat p n + k

Tactic:
simp [padicValNat, *]

Premises used: padicValNat
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
hp : p ≠ 0
n k : ℕ
⊢ p = 1 ∨ 1 < p

Tactic:
grind
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
hp : p ≠ 0
n k : ℕ
inl : ∀ (hp : Ne (α := ℕ) 1 0), (HPow.hPow (α := ℕ) 1 k * n).divMaxPow 1 = n.divMaxPow 1
inr : ∀ (hp1 : 1 < p), (p ^ k * n).divMaxPow p = n.divMaxPow p
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p

Tactic:
obtain rfl | hp1 : p = 1 ∨ 1 < p := by grind

Premises used: rfl
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n k : ℕ
hp : Ne (α := ℕ) 1 0
⊢ (HPow.hPow (α := ℕ) 1 k * n).divMaxPow 1 = n.divMaxPow 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
hp : p ≠ 0
n k : ℕ
hp1 : 1 < p
inr : (p ^ k * 0).divMaxPow p = divMaxPow 0 p
inr₁ : ∀ (hn : n ≠ 0), (p ^ k * n).divMaxPow p = n.divMaxPow p
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
hp : p ≠ 0
k : ℕ
hp1 : 1 < p
⊢ (p ^ k * 0).divMaxPow p = divMaxPow 0 p

Tactic:
simp [divMaxPow, *]

Premises used: Nat.divMaxPow
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
hp : p ≠ 0
n k : ℕ
hp1 : 1 < p
hn : n ≠ 0
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p

Tactic:
simp [divMaxPow, *]

Premises used: Nat.divMaxPow
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
⊢ p.maxPowDvdDiv (p * n) = (padicValNat p n + 1, n.divMaxPow p)

Tactic:
simpa using maxPowDvdDiv_base_pow_mul hp hn 1

Premises used: Nat.maxPowDvdDiv_base_pow_mul, OfNat.ofNat
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
⊢ padicValNat p (p * n) = padicValNat p n + 1

Tactic:
simp [padicValNat, *]

Premises used: padicValNat
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
hp : p ≠ 0
n : ℕ
⊢ (p * n).divMaxPow p = n.divMaxPow p

Tactic:
simpa using divMaxPow_base_pow_mul hp n 1

Premises used: Nat.divMaxPow_base_pow_mul, OfNat.ofNat
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
hp : 1 < p
k : ℕ
⊢ p.maxPowDvdDiv (p ^ k) = (k, 1)

Tactic:
simpa using maxPowDvdDiv_base_pow_mul hp Nat.one_ne_zero k

Premises used: Nat.maxPowDvdDiv_base_pow_mul, Nat.one_ne_zero
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
hp : 1 < p
k : ℕ
⊢ padicValNat p (p ^ k) = k

Tactic:
simp [padicValNat, hp]

Premises used: padicValNat
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
hp : p ≠ 0
k : ℕ
⊢ (p ^ k).divMaxPow p = 1

Tactic:
simpa using divMaxPow_base_pow_mul hp 1 k

Premises used: Nat.divMaxPow_base_pow_mul, OfNat.ofNat
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
hp : 1 < p
⊢ p.maxPowDvdDiv p = (1, 1)

Tactic:
simpa using maxPowDvdDiv_base_pow hp 1

Premises used: Nat.maxPowDvdDiv_base_pow, OfNat.ofNat
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
hp : 1 < p
⊢ padicValNat p p = 1

Tactic:
simpa using padicValNat_base_pow hp 1

Premises used: padicValNat_base_pow, OfNat.ofNat
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
hp : p ≠ 0
⊢ p.divMaxPow p = 1

Tactic:
simpa using divMaxPow_base_pow hp 1

Premises used: Nat.divMaxPow_base_pow, OfNat.ofNat
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
⊢ (p.maxPowDvdDiv n).fst = padicValNat p n

Tactic:
rfl

Premises used: padicValNat, rfl
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
⊢ (p.maxPowDvdDiv n).snd = n.divMaxPow p

Tactic:
rfl

Premises used: Nat.divMaxPow, rfl
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b n : ℕ
mp : a ≡ b [PMOD n] → a ≡ b [MOD n]
mpr : a ≡ b [MOD n] → a ≡ b [PMOD n]
⊢ a ≡ b [PMOD n] ↔ a ≡ b [MOD n]

Tactic:
constructor
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b n : ℕ
mp : (∃ (m : ℕ), ∃ (n_1 : ℕ), m • n + a = n_1 • n + b) → a % n = b % n
⊢ a ≡ b [PMOD n] → a ≡ b [MOD n]

Tactic:
rw [modEq_iff_nsmul, Nat.ModEq]

Premises used: Nat.ModEq, AddCommGroup.modEq_iff_nsmul
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b n k l : ℕ
h : k • n + a = l • n + b
⊢ a % n = b % n

Tactic:
simpa using congr($h % n)
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b n : ℕ
h : a % n = b % n
mpr : (a / n) • n + b % n ≡ (b / n) • n + b % n [PMOD n]
⊢ a ≡ b [PMOD n]

Tactic:
rw [← Nat.div_add_mod' a n, ← Nat.div_add_mod' b n, ← Nat.nsmul_eq_mul, ← Nat.nsmul_eq_mul, h]

Premises used: Nat.nsmul_eq_mul, Nat.div_add_mod'
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b n : ℕ
h : a % n = b % n
⊢ (a / n) • n + b % n ≡ (b / n) • n + b % n [PMOD n]

Tactic:
nsmul_add_modEq _ |>.trans (nsmul_add_modEq _).symm

Premises used: AddCommGroup.ModEq.trans, AddCommGroup.nsmul_add_modEq, AddCommGroup.ModEq.symm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b n : ℕ
h : a % n = b % n
⊢ (a / n) • n + b % n ≡ (b / n) • n + b % n [PMOD n]

Tactic:
exact nsmul_add_modEq _ |>.trans (nsmul_add_modEq _).symm

Premises used: AddCommGroup.ModEq.trans, AddCommGroup.nsmul_add_modEq, AddCommGroup.ModEq.symm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
M : Type u_1
inst : AddCommMonoidWithOne M
a b n : ℕ
h : a ≡ b [MOD n]
⊢ a ≡ b [PMOD n]

Tactic:
rw [← modEq_iff_natModEq] at h

Premises used: AddCommGroup.modEq_iff_natModEq
-- Module: Mathlib.Data.Nat.ModEq
Goal:
M : Type u_1
inst : AddCommMonoidWithOne M
a b n : ℕ
h : a ≡ b [PMOD n]
⊢ ModEq.{u_1} (M := M) (↑n : M) (↑a : M) (↑b : M)

Tactic:
h.map (Nat.castAddMonoidHom M)

Premises used: Nat.castAddMonoidHom, AddCommGroup.ModEq.map
-- Module: Mathlib.Data.Nat.ModEq
Goal:
M : Type u_1
inst : AddCommMonoidWithOne M
a b n : ℕ
h : a ≡ b [PMOD n]
⊢ ModEq.{u_1} (M := M) (↑n : M) (↑a : M) (↑b : M)

Tactic:
exact h.map (Nat.castAddMonoidHom M)

Premises used: Nat.castAddMonoidHom, AddCommGroup.ModEq.map
-- Module: Mathlib.Data.Nat.ModEq
Goal:
M : Type u_1
inst : AddCommMonoidWithOne M
inst_1 : CharZero M
a b n : ℕ
⊢ ModEq.{u_1} (M := M) (↑n : M) (↑a : M) (↑b : M) ↔ a ≡ b [MOD n]

Tactic:
simpa using map_modEq_iff (Nat.castAddMonoidHom M) Nat.cast_injective

Premises used: AddCommGroup.map_modEq_iff, Nat.castAddMonoidHom, Nat.cast_injective
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a : ℕ
⊢ a ≡ a [MOD n]

Tactic:
rfl

Premises used: Nat.ModEq, rfl
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a : ℕ
⊢ a ≡ a [MOD n]

Tactic:
ModEq.refl _

Premises used: Nat.ModEq.refl
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
⊢ Std.Refl n.ModEq

Tactic:
⟨ModEq.refl⟩

Premises used: Nat.ModEq.refl, Std.Refl.mk
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
⊢ a ≡ b [MOD n] → b ≡ a [MOD n]

Tactic:
Eq.symm

Premises used: Nat.ModEq, Eq.symm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
⊢ a ≡ b [MOD n] → b ≡ c [MOD n] → a ≡ c [MOD n]

Tactic:
Eq.trans

Premises used: Nat.ModEq, Eq.trans
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
⊢ a ≡ b [MOD n] ↔ b ≡ a [MOD n]

Tactic:
⟨ModEq.symm, ModEq.symm⟩

Premises used: Nat.ModEq.symm, Iff.intro
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a : ℕ
rw : a % n = 0 % n ↔ n ∣ a
rw₁ : a % n = 0 ↔ n ∣ a
rw₂ rw₃ : a % n = 0 ↔ a % n = 0
⊢ a ≡ 0 [MOD n] ↔ n ∣ a

Tactic:
rw [ModEq, zero_mod, dvd_iff_mod_eq_zero]

Premises used: Nat.ModEq, Nat.dvd_iff_mod_eq_zero, Nat.zero_mod
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a : ℕ
h : n ∣ a
⊢ a ≡ 0 [MOD n]

Tactic:
modEq_zero_iff_dvd.2 h

Premises used: Iff.mpr, Nat.modEq_zero_iff_dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a : ℕ
h : n ∣ a
⊢ 0 ≡ a [MOD n]

Tactic:
h.modEq_zero_nat.symm

Premises used: Dvd.dvd.modEq_zero_nat, Nat.ModEq.symm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
rw : a % n = b % n ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₁ : b % n = a % n ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₂ : Eq (α := ℤ) (↑(b % n) : ℤ) (↑(a % n) : ℤ) ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₃ : HMod.hMod (α := ℤ) (↑b : ℤ) (↑n : ℤ) = (↑(a % n) : ℤ) ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₄ :
  HMod.hMod (α := ℤ) (↑b : ℤ) (↑n : ℤ) = HMod.hMod (α := ℤ) (↑a : ℤ) (↑n : ℤ) ↔
    (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₅ : HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) % (↑n : ℤ) = 0 ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₆ rw₇ : HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) % (↑n : ℤ) = 0 ↔ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) % (↑n : ℤ) = 0
⊢ a ≡ b [MOD n] ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)

Tactic:
rw [ModEq, eq_comm, ← Int.natCast_inj, Int.natCast_mod, Int.natCast_mod,
    Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.dvd_iff_emod_eq_zero]

Premises used: eq_comm, Int.emod_eq_emod_iff_emod_sub_eq_zero, Nat.ModEq, Int.natCast_mod, Int.dvd_iff_emod_eq_zero, Int.natCast_inj
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
h : a ≤ b
rw : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) ↔ n ∣ b - a
rw₁ : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) ↔ Dvd.dvd (α := ℤ) (↑n : ℤ) (↑(b - a) : ℤ)
rw₂ rw₃ : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ a ≡ b [MOD n] ↔ n ∣ b - a

Tactic:
rw [modEq_iff_dvd, ← Int.natCast_dvd_natCast, Int.ofNat_sub h]

Premises used: Int.ofNat_sub, Nat.modEq_iff_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a n : ℕ
⊢ a % n ≡ a [MOD n]

Tactic:
mod_mod _ _

Premises used: Nat.mod_mod, Nat.ModEq
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b : ℕ
⊢ m * a + b ≡ b [MOD m]

Tactic:
simp [Nat.ModEq]

Premises used: Nat.ModEq
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b : ℕ
d : m ∣ n
h : a ≡ b [MOD n]
⊢ a ≡ b [MOD m]

Tactic:
modEq_of_dvd <| Int.ofNat_dvd.mpr d |>.trans h.dvd

Premises used: Iff.mpr, Int.ofNat_dvd, Nat.modEq_of_dvd, Dvd.dvd.trans, Nat.ModEq.dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
h : a % n = b % n
rw : c * (a % n) = c * b % (c * n)
rw₁ : c * (a % n) = c * (b % n)
rw₂ rw₃ : c * (b % n) = c * (b % n)
⊢ c * a % (c * n) = c * b % (c * n)

Tactic:
rw [mul_mod_mul_left, mul_mod_mul_left, h]

Premises used: Nat.mul_mod_mul_left
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD n]

Tactic:
(h.mul_left' _).of_dvd (dvd_mul_left _ _)

Premises used: dvd_mul_left, Nat.ModEq.mul_left', Nat.ModEq.of_dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
h : a ≡ b [MOD n]
rw : c * a ≡ c * b [MOD c * n]
⊢ a * c ≡ b * c [MOD n * c]

Tactic:
rw [mul_comm a, mul_comm b, mul_comm n]

Premises used: mul_comm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD c * n]

Tactic:
h.mul_left' c

Premises used: Nat.ModEq.mul_left'
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD c * n]

Tactic:
exact h.mul_left' c

Premises used: Nat.ModEq.mul_left'
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
h : a ≡ b [MOD n]
rw : c * a ≡ c * b [MOD n]
⊢ a * c ≡ b * c [MOD n]

Tactic:
rw [mul_comm a, mul_comm b]

Premises used: mul_comm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD n]

Tactic:
h.mul_left c

Premises used: Nat.ModEq.mul_left
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD n]

Tactic:
exact h.mul_left c

Premises used: Nat.ModEq.mul_left
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : c ≡ d [MOD n]
⊢ a * c ≡ b * d [MOD n]

Tactic:
(h₂.mul_left _).trans (h₁.mul_right _)

Premises used: Nat.ModEq.mul_right, Nat.ModEq.mul_left, Nat.ModEq.trans
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
h : a ≡ b [MOD n]
⊢ HPow.hPow (β := ℕ) a 0 ≡ HPow.hPow (β := ℕ) b 0 [MOD n]

Tactic:
rfl
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
succ : a ^ d * a ≡ b ^ d * b [MOD n]
⊢ a ^ (d + 1) ≡ b ^ (d + 1) [MOD n]

Tactic:
rw [Nat.pow_succ, Nat.pow_succ]

Premises used: Nat.pow_succ
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ d * a ≡ b ^ d * b [MOD n]

Tactic:
hd.mul h

Premises used: Nat.ModEq.mul
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ d * a ≡ b ^ d * b [MOD n]

Tactic:
exact hd.mul h

Premises used: Nat.ModEq.mul
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b m : ℕ
h : a ≡ b [MOD n]
zero : HPow.hPow (β := ℕ) a 0 ≡ HPow.hPow (β := ℕ) b 0 [MOD n]
succ : ∀ (d : ℕ) (hd : a ^ d ≡ b ^ d [MOD n]), a ^ (d + 1) ≡ b ^ (d + 1) [MOD n]
⊢ a ^ m ≡ b ^ m [MOD n]

Tactic:
induction m with
  | zero => rfl
  | succ d hd =>
    rw [Nat.pow_succ, Nat.pow_succ]
    exact hd.mul h

Premises used: Nat.pow_succ, Nat.zero, Nat.succ
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : c ≡ d [MOD n]
rw : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)
⊢ a + c ≡ b + d [MOD n]

Tactic:
rw [modEq_iff_dvd, Int.natCast_add, Int.natCast_add, add_sub_add_comm]

Premises used: Int.natCast_add, Nat.modEq_iff_dvd, add_sub_add_comm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : c ≡ d [MOD n]
⊢ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)

Tactic:
Int.dvd_add h₁.dvd h₂.dvd

Premises used: Int.dvd_add, Nat.ModEq.dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : c ≡ d [MOD n]
⊢ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)

Tactic:
exact Int.dvd_add h₁.dvd h₂.dvd

Premises used: Int.dvd_add, Nat.ModEq.dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c + a ≡ c + b [MOD n]

Tactic:
ModEq.rfl.add h

Premises used: Nat.ModEq.add, Nat.ModEq.rfl
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ a + c ≡ b + c [MOD n]

Tactic:
h.add ModEq.rfl

Premises used: Nat.ModEq.add, Nat.ModEq.rfl
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : a + c ≡ b + d [MOD n]
simp :
  ∀ (h₁ : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ))
    (h₂ : (↑n : ℤ) ∣ HAdd.hAdd (α := ℤ) (↑b : ℤ) (↑d : ℤ) - HAdd.hAdd (α := ℤ) (↑a : ℤ) (↑c : ℤ)),
    (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)
⊢ c ≡ d [MOD n]

Tactic:
simp only [modEq_iff_dvd, Int.natCast_add] at *

Premises used: Int.natCast_add, Nat.modEq_iff_dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h₁ : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
h₂ : (↑n : ℤ) ∣ HAdd.hAdd (α := ℤ) (↑b : ℤ) (↑d : ℤ) - HAdd.hAdd (α := ℤ) (↑a : ℤ) (↑c : ℤ)
⊢ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)

Tactic:
rw [add_sub_add_comm] at h₂

Premises used: add_sub_add_comm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h₁ : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
h₂ : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)
⊢ (↑n : ℤ) ∣
    HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ) - HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)

Tactic:
Int.dvd_sub h₂ h₁

Premises used: Int.dvd_sub
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h₁ : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
h₂ : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)
h :
  HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ) =
    HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ) - HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)

Tactic:
convert! Int.dvd_sub h₂ h₁ using 1

Premises used: Int.dvd_sub
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h₁ : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
h₂ : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)
h h₃ : HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ) = HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)
⊢ HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ) =
    HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ) - HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)

Tactic:
rw [add_sub_cancel_left]

Premises used: add_sub_cancel_left
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
h : c + a ≡ c + b [MOD n]
⊢ a ≡ b [MOD n]

Tactic:
ModEq.rfl.add_left_cancel h

Premises used: Nat.ModEq.rfl, Nat.ModEq.add_left_cancel
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h : a ≡ b [MOD n]
⊢ a + c ≡ b + d [MOD n] ↔ c ≡ d [MOD n]

Tactic:
⟨h.add_left_cancel, h.add⟩

Premises used: Nat.ModEq.add, Iff.intro, Nat.ModEq.add_left_cancel
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h₁ : c ≡ d [MOD n]
h₂ : a + c ≡ b + d [MOD n]
⊢ c + a ≡ d + b [MOD n]

Tactic:
rw [add_comm a, add_comm b] at h₂

Premises used: add_comm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h₁ : c ≡ d [MOD n]
h₂ : c + a ≡ d + b [MOD n]
⊢ a ≡ b [MOD n]

Tactic:
h₁.add_left_cancel h₂

Premises used: Nat.ModEq.add_left_cancel
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h₁ : c ≡ d [MOD n]
h₂ : c + a ≡ d + b [MOD n]
⊢ a ≡ b [MOD n]

Tactic:
exact h₁.add_left_cancel h₂

Premises used: Nat.ModEq.add_left_cancel
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
h : a + c ≡ b + c [MOD n]
⊢ a ≡ b [MOD n]

Tactic:
ModEq.rfl.add_right_cancel h

Premises used: Nat.ModEq.rfl, Nat.ModEq.add_right_cancel
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h : c ≡ d [MOD n]
⊢ a + c ≡ b + d [MOD n] ↔ a ≡ b [MOD n]

Tactic:
⟨h.add_right_cancel, (.add · h)⟩

Premises used: Nat.ModEq.add, Iff.intro, Nat.ModEq.add_right_cancel
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h : c ≤ a ↔ d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
inl : ∀ (hac : a < c), a - c ≡ b - d [MOD n]
inr : ∀ (hca : c ≤ a), a - c ≡ b - d [MOD n]
⊢ a - c ≡ b - d [MOD n]

Tactic:
obtain hac | hca := lt_or_ge a c

Premises used: lt_or_ge
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h : c ≤ a ↔ d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
hac : a < c
inl : 0 ≡ b - d [MOD n]
inl₁ inl₂ : 0 ≡ 0 [MOD n]
⊢ a - c ≡ b - d [MOD n]

Tactic:
rw [Nat.sub_eq_zero_of_le hac.le, Nat.sub_eq_zero_of_le ((lt_iff_lt_of_le_iff_le h).1 hac).le]

Premises used: LT.lt.le, Iff.mp, lt_iff_lt_of_le_iff_le, Nat.sub_eq_zero_of_le
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h : c ≤ a ↔ d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
hca : c ≤ a
inr : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) - HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)
⊢ a - c ≡ b - d [MOD n]

Tactic:
rw [modEq_iff_dvd, Int.natCast_sub hca, Int.natCast_sub <| h.1 hca, sub_sub_sub_comm]

Premises used: sub_sub_sub_comm, Nat.modEq_iff_dvd, Int.natCast_sub, Iff.mp
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h : c ≤ a ↔ d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
hca : c ≤ a
⊢ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) - HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)

Tactic:
Int.dvd_sub hab.dvd hcd.dvd

Premises used: Int.dvd_sub, Nat.ModEq.dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
h : c ≤ a ↔ d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
hca : c ≤ a
⊢ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) - HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)

Tactic:
exact Int.dvd_sub hab.dvd hcd.dvd

Premises used: Int.dvd_sub, Nat.ModEq.dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
h : b ≤ a ↔ c ≤ a
hbc : b ≡ c [MOD n]
⊢ a - b ≡ a - c [MOD n]

Tactic:
.sub' h .rfl hbc

Premises used: Nat.ModEq.sub', Nat.ModEq.rfl
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
h : a ≤ b ↔ a ≤ c
hbc : b ≡ c [MOD n]
⊢ b - a ≡ c - a [MOD n]

Tactic:
.sub' h hbc .rfl

Premises used: Nat.ModEq.sub', Nat.ModEq.rfl
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c d : ℕ
hca : c ≤ a
hdb : d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
⊢ a - c ≡ b - d [MOD n]

Tactic:
.sub' (iff_of_true hca hdb) hab hcd

Premises used: Nat.ModEq.sub', iff_of_true
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
hba : b ≤ a
hca : c ≤ a
hbc : b ≡ c [MOD n]
⊢ a - b ≡ a - c [MOD n]

Tactic:
.sub hba hca .rfl hbc

Premises used: Nat.ModEq.sub, Nat.ModEq.rfl
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
hab : a ≤ b
hac : a ≤ c
hbc : b ≡ c [MOD n]
⊢ b - a ≡ c - a [MOD n]

Tactic:
.sub hab hac hbc .rfl

Premises used: Nat.ModEq.sub, Nat.ModEq.rfl
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c m : ℕ
hc : c ≠ 0
simp :
  HMul.hMul (α := ℤ) (↑c : ℤ) (↑m : ℤ) ∣ (↑c : ℤ) * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) →
    (↑m : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ c * a ≡ c * b [MOD c * m] → a ≡ b [MOD m]

Tactic:
simp only [modEq_iff_dvd, Int.natCast_mul, ← Int.mul_sub]

Premises used: Int.mul_sub, Nat.modEq_iff_dvd, Int.natCast_mul
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c m : ℕ
hc : c ≠ 0
⊢ HMul.hMul (α := ℤ) (↑c : ℤ) (↑m : ℤ) ∣ (↑c : ℤ) * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) →
    (↑m : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)

Tactic:
fun h => (Int.dvd_of_mul_dvd_mul_left (Int.ofNat_ne_zero.mpr hc) h)

Premises used: Iff.mpr, Int.ofNat_ne_zero, Int.dvd_of_mul_dvd_mul_left