awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ HPow.hPow (α := R) (↑b : R) (log b r⁻¹) ≤ r⁻¹

Tactic:
zpow_log_le_self hb (inv_pos.mpr hr)

Premises used: Iff.mpr, inv_pos, Int.zpow_log_le_self
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ HPow.hPow (α := R) (↑b : R) (log b r⁻¹) ≤ r⁻¹

Tactic:
exact zpow_log_le_self hb (inv_pos.mpr hr)

Premises used: Iff.mpr, inv_pos, Int.zpow_log_le_self
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ LT.lt.{u_1} (α := R) 0 (↑b : R)

Tactic:
Nat.cast_pos.mpr (zero_le_one.trans_lt hb)

Premises used: Iff.mpr, Nat.cast_pos, zero_le_one, LE.le.trans_lt
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ LT.lt.{u_1} (α := R) 0 (↑b : R)

Tactic:
exact Nat.cast_pos.mpr (zero_le_one.trans_lt hb)

Premises used: Iff.mpr, Nat.cast_pos, zero_le_one, LE.le.trans_lt
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
rw : r⁻¹ < HPow.hPow (α := R) (↑b : R) (log b r⁻¹ + 1)
rw₁ : 0 < HPow.hPow (α := R) (↑b : R) (log b r⁻¹ + 1)
⊢ HPow.hPow (α := R) (↑b : R) (clog b r - 1) < r

Tactic:
rw [← neg_log_inv_eq_clog, ← neg_add', zpow_neg, inv_lt_comm₀ _ hr]

Premises used: neg_add', inv_lt_comm₀, zpow_neg, Int.neg_log_inv_eq_clog
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ r⁻¹ < HPow.hPow (α := R) (↑b : R) (log b r⁻¹ + 1)

Tactic:
lt_zpow_succ_log_self hb _

Premises used: Int.lt_zpow_succ_log_self
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ r⁻¹ < HPow.hPow (α := R) (↑b : R) (log b r⁻¹ + 1)

Tactic:
exact lt_zpow_succ_log_self hb _

Premises used: Int.lt_zpow_succ_log_self
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ 0 < HPow.hPow (α := R) (↑b : R) (log b r⁻¹ + 1)

Tactic:
zpow_pos (Nat.cast_pos.mpr <| zero_le_one.trans_lt hb) _

Premises used: zpow_pos
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ 0 < HPow.hPow (α := R) (↑b : R) (log b r⁻¹ + 1)

Tactic:
exact zpow_pos (Nat.cast_pos.mpr <| zero_le_one.trans_lt hb) _

Premises used: zpow_pos
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
⊢ clog.{u_1} (R := R) b 0 = 0

Tactic:
clog_of_right_le_zero _ le_rfl

Premises used: le_rfl, Int.clog_of_right_le_zero
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
rw : Eq (α := ℤ) (↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ) 0
rw₁ : Eq (α := ℤ) (↑(Nat.clog b 1) : ℤ) 0
rw₂ : Eq (α := ℤ) (↑0 : ℤ) 0
rw₃ rw₄ : Eq (α := ℤ) 0 0
⊢ clog.{u_1} (R := R) b 1 = 0

Tactic:
rw [clog_of_one_le_right _ le_rfl, Nat.ceil_one, Nat.clog_one_right, Int.ofNat_zero]

Premises used: le_rfl, Nat.ceil_one, Int.ofNat_zero, Int.clog_of_one_le_right, Nat.clog_one_right
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
r : R
pos : ∀ (hr : 1 ≤ r), clog 0 r = 0
neg : ∀ (hr : ¬1 ≤ r), clog 0 r = 0
⊢ clog 0 r = 0

Tactic:
by_cases hr : 1 ≤ r
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
r : R
hr : 1 ≤ r
⊢ clog 0 r = 0

Tactic:
simp only [clog, Nat.clog_zero_left, Nat.cast_zero, Nat.log_zero_left, neg_zero, ite_self]

Premises used: Nat.log_zero_left, ite_self, Nat.clog_zero_left, Int.clog, Nat.cast_zero, neg_zero
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
r : R
hr : ¬1 ≤ r
⊢ clog 0 r = 0

Tactic:
simp only [clog, hr, ite_cond_eq_false, Nat.log_zero_left, Nat.cast_zero, neg_zero]

Premises used: Nat.log_zero_left, Int.clog, Nat.cast_zero, ite_cond_eq_false, neg_zero
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
r : R
⊢ clog 1 r = 0

Tactic:
simp only [clog, Nat.log_one_left, Nat.cast_zero, Nat.clog_one_left, neg_zero, ite_self]

Premises used: ite_self, Nat.clog_one_left, Int.clog, Nat.cast_zero, neg_zero, Nat.log_one_left
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
rw : -log b (HPow.hPow (α := R) (↑b : R) z)⁻¹ = z
rw₁ : -log b (HPow.hPow (α := R) (↑b : R) (-z)) = z
rw₂ : - -z = z
rw₃ rw₄ : z = z
⊢ clog b (HPow.hPow (α := R) (↑b : R) z) = z

Tactic:
rw [← neg_log_inv_eq_clog, ← zpow_neg, log_zpow hb, neg_neg]

Premises used: neg_neg, zpow_neg, Int.log_zpow, Int.neg_log_inv_eq_clog
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
⊢ 0 < r₂

Tactic:
have h₀' : 0 < r₂ := lt_of_lt_of_le h₀ h
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₀' : 0 < r₂
rw : log b r₂⁻¹ ≤ log b r₁⁻¹
⊢ clog b r₁ ≤ clog b r₂

Tactic:
rw [← neg_log_inv_eq_clog, ← neg_log_inv_eq_clog, neg_le_neg_iff]

Premises used: Int.neg_log_inv_eq_clog, neg_le_neg_iff
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₀' : 0 < r₂
⊢ log b r₂⁻¹ ≤ log b r₁⁻¹

Tactic:
log_mono_right (inv_pos_of_pos h₀') <| (inv_le_inv₀ h₀' h₀).2 h

Premises used: Iff.mpr, inv_pos_of_pos, Int.log_mono_right, inv_le_inv₀
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₀' : 0 < r₂
⊢ log b r₂⁻¹ ≤ log b r₁⁻¹

Tactic:
exact log_mono_right (inv_pos_of_pos h₀') <| (inv_le_inv₀ h₀' h₀).2 h

Premises used: Iff.mpr, inv_pos_of_pos, Int.log_mono_right, inv_le_inv₀
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
x : ℤ
r : R
hr : 0 < r
⊢ HPow.hPow (α := R) (↑b : R) x < r ↔ x < clog b r

Tactic:
(@GaloisConnection.lt_iff_lt _ _ _ _ _ _ (clogZPowGi R hb).gc ⟨r, hr⟩ x).symm

Premises used: Int.clogZPowGi, Iff.symm, GaloisInsertion.gc, GaloisConnection.lt_iff_lt
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
x : ℤ
r : R
hr : 0 < r
⊢ r ≤ HPow.hPow (α := R) (↑b : R) x ↔ clog b r ≤ x

Tactic:
(@GaloisConnection.le_iff_le _ _ _ _ _ _ (clogZPowGi R hb).gc ⟨r, hr⟩ x).symm

Premises used: GaloisConnection.le_iff_le, Int.clogZPowGi, Iff.symm, GaloisInsertion.gc
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b z : ℤ
rw : b ≡ a [PMOD z] ↔ a ≡ b [ZMOD z]
⊢ a ≡ b [PMOD z] ↔ a ≡ b [ZMOD z]

Tactic:
rw [modEq_comm]

Premises used: AddCommGroup.modEq_comm
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b z : ℤ
⊢ b ≡ a [PMOD z] ↔ a ≡ b [ZMOD z]

Tactic:
simp [modEq_iff_zsmul', dvd_iff_exists_eq_mul_left, Int.ModEq,
    Int.emod_eq_emod_iff_emod_sub_eq_zero, ← Int.dvd_iff_emod_eq_zero]

Premises used: Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.ModEq, AddCommGroup.modEq_iff_zsmul', dvd_iff_exists_eq_mul_left, Int.dvd_iff_emod_eq_zero
-- Module: Mathlib.Data.Int.ModEq
Goal:
G : Type u_1
inst : AddCommGroupWithOne G
inst_1 : CharZero G
a b z : ℤ
⊢ ModEq.{u_1} (M := G) (↑z : G) (↑a : G) (↑b : G) ↔ a ≡ b [PMOD z]

Tactic:
map_modEq_iff (Int.castAddHom G) Int.cast_injective

Premises used: AddCommGroup.map_modEq_iff, Int.castAddHom, Int.cast_injective
-- Module: Mathlib.Data.Int.ModEq
Goal:
G : Type u_1
inst : AddCommGroupWithOne G
inst_1 : CharZero G
a b : ℤ
n : ℕ
⊢ ModEq.{u_1} (M := G) (↑n : G) (↑a : G) (↑b : G) ↔ a ≡ b [PMOD (↑n : ℤ)]

Tactic:
simpa using intCast_modEq_intCast (G := G) (z := n)

Premises used: AddCommGroup.intCast_modEq_intCast
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a : ℤ
⊢ a ≡ a [ZMOD n]

Tactic:
@rfl _ _

Premises used: Int.ModEq, rfl
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a : ℤ
⊢ a ≡ a [ZMOD n]

Tactic:
ModEq.refl _

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

Tactic:
⟨ModEq.refl⟩

Premises used: Int.ModEq.refl, Std.Refl.mk
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
⊢ a ≡ b [ZMOD n] → b ≡ a [ZMOD n]

Tactic:
Eq.symm

Premises used: Int.ModEq, Eq.symm
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
⊢ a ≡ b [ZMOD n] → b ≡ c [ZMOD n] → a ≡ c [ZMOD n]

Tactic:
Eq.trans

Premises used: Int.ModEq, Eq.trans
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
⊢ a ≡ b [ZMOD n] → a % n = b % n

Tactic:
id

Premises used: id, Int.ModEq
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
⊢ a ≡ b [ZMOD n] ↔ b ≡ a [ZMOD n]

Tactic:
⟨ModEq.symm, ModEq.symm⟩

Premises used: Int.ModEq.symm, Iff.intro
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b n : ℕ
rw :
  HMod.hMod (α := ℤ) (↑a : ℤ) (↑n : ℤ) = HMod.hMod (α := ℤ) (↑b : ℤ) (↑n : ℤ) ↔
    Eq (α := ℤ) (↑(a % n) : ℤ) (↑(b % n) : ℤ)
⊢ HMod.hMod (α := ℤ) (↑a : ℤ) (↑n : ℤ) = HMod.hMod (α := ℤ) (↑b : ℤ) (↑n : ℤ) ↔ a % n = b % n

Tactic:
rw [← Int.ofNat_inj]

Premises used: Int.ofNat_inj
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b n : ℕ
⊢ HMod.hMod (α := ℤ) (↑a : ℤ) (↑n : ℤ) = HMod.hMod (α := ℤ) (↑b : ℤ) (↑n : ℤ) ↔
    Eq (α := ℤ) (↑(a % n) : ℤ) (↑(b % n) : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Int.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 [ZMOD n] ↔ n ∣ a

Tactic:
rw [ModEq, zero_emod, dvd_iff_emod_eq_zero]

Premises used: Int.ModEq, Int.zero_emod, Int.dvd_iff_emod_eq_zero
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a : ℤ
h : n ∣ a
⊢ a ≡ 0 [ZMOD n]

Tactic:
modEq_zero_iff_dvd.2 h

Premises used: Iff.mpr, Int.modEq_zero_iff_dvd
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a : ℤ
h : n ∣ a
⊢ 0 ≡ a [ZMOD n]

Tactic:
h.modEq_zero_int.symm

Premises used: Int.ModEq.symm, Dvd.dvd.modEq_zero_int
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
rw : b % n = a % n ↔ n ∣ b - a
⊢ a ≡ b [ZMOD n] ↔ n ∣ b - a

Tactic:
rw [ModEq, eq_comm]

Premises used: eq_comm, Int.ModEq
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
⊢ b % n = a % n ↔ n ∣ b - a

Tactic:
simp [emod_eq_emod_iff_emod_sub_eq_zero, dvd_iff_emod_eq_zero]

Premises used: Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.dvd_iff_emod_eq_zero
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b n : ℤ
rw : n ∣ b - a ↔ ∃ (t : ℤ), b = a + n * t
⊢ a ≡ b [ZMOD n] ↔ ∃ (t : ℤ), b = a + n * t

Tactic:
rw [modEq_iff_dvd]

Premises used: Int.modEq_iff_dvd
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b n : ℤ
⊢ n ∣ b - a ↔ ∃ (t : ℤ), b = a + n * t

Tactic:
exists_congr fun t => sub_eq_iff_eq_add'

Premises used: exists_congr, sub_eq_iff_eq_add'
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b n : ℤ
⊢ n ∣ b - a ↔ ∃ (t : ℤ), b = a + n * t

Tactic:
exact exists_congr fun t => sub_eq_iff_eq_add'

Premises used: exists_congr, sub_eq_iff_eq_add'
-- Module: Mathlib.Data.Int.ModEq
Goal:
a n : ℤ
⊢ a % n ≡ a [ZMOD n]

Tactic:
emod_emod _ _

Premises used: Int.ModEq, Int.emod_emod
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
⊢ -b - -a = -(b - a)

Tactic:
lia
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
⊢ a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n]

Tactic:
simp [modEq_iff_dvd]

Premises used: Int.modEq_iff_dvd
-- Module: Mathlib.Data.Int.ModEq
Goal:
m n a b : ℤ
d : m ∣ n
h : a ≡ b [ZMOD n]
⊢ a ≡ b [ZMOD m]

Tactic:
modEq_iff_dvd.2 <| d.trans h.dvd

Premises used: Iff.mpr, Int.modEq_iff_dvd, Int.ModEq.dvd, Dvd.dvd.trans
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
h : a ≡ b [ZMOD n]
inl : ∀ (hc : c < 0), c * a ≡ c * b [ZMOD c * n]
inr : 0 * a ≡ 0 * b [ZMOD 0 * n]
inr₁ : ∀ (hc : 0 < c), c * a ≡ c * b [ZMOD c * n]
⊢ c * a ≡ c * b [ZMOD c * n]

Tactic:
obtain hc | rfl | hc := lt_trichotomy c 0

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
inl : -c * a ≡ -c * b [ZMOD -c * n]
⊢ c * a ≡ c * b [ZMOD c * n]

Tactic:
rw [← neg_modEq_neg, ← modEq_neg, ← Int.neg_mul, ← Int.neg_mul, ← Int.neg_mul]

Premises used: Int.neg_modEq_neg, Int.modEq_neg, Int.neg_mul
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ -c * a ≡ -c * b [ZMOD -c * n]

Tactic:
simp only [ModEq, mul_emod_mul_of_pos _ _ (neg_pos.2 hc), h.eq]

Premises used: Iff.mpr, neg_pos, Int.ModEq, Int.mul_emod_mul_of_pos, Int.ModEq.eq
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 * a ≡ 0 * b [ZMOD 0 * n]

Tactic:
simp only [Int.zero_mul, ModEq.rfl]

Premises used: Int.ModEq.rfl, Int.zero_mul
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : 0 < c
⊢ c * a ≡ c * b [ZMOD c * n]

Tactic:
simp only [ModEq, mul_emod_mul_of_pos _ _ hc, h.eq]

Premises used: Int.ModEq, Int.mul_emod_mul_of_pos, Int.ModEq.eq
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
h : a ≡ b [ZMOD n]
rw : c * a ≡ c * b [ZMOD c * n]
⊢ a * c ≡ b * c [ZMOD n * c]

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

Premises used: mul_comm
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ c * b [ZMOD c * n]

Tactic:
h.mul_left'

Premises used: Int.ModEq.mul_left'
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ c * b [ZMOD c * n]

Tactic:
exact h.mul_left'

Premises used: Int.ModEq.mul_left'
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ n ∣ b - a + (d - c)

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

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

Tactic:
convert! Int.dvd_add h₁.dvd h₂.dvd using 1

Premises used: Int.ModEq.dvd, Int.dvd_add
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ b + d - (a + c) = b - a + (d - c)

Tactic:
lia
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ c + a ≡ c + b [ZMOD n]

Tactic:
ModEq.rfl.add h

Premises used: Int.ModEq.rfl, Int.ModEq.add
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ a + c ≡ b + c [ZMOD n]

Tactic:
h.add ModEq.rfl

Premises used: Int.ModEq.rfl, Int.ModEq.add
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
⊢ d - c = b + d - (a + c) - (b - a)

Tactic:
lia
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
this : d - c = b + d - (a + c) - (b - a)
rw : n ∣ b + d - (a + c) - (b - a)
⊢ n ∣ d - c

Tactic:
rw [this]
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
this : d - c = b + d - (a + c) - (b - a)
⊢ n ∣ b + d - (a + c) - (b - a)

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

Premises used: Int.ModEq.dvd, Int.dvd_sub
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
this : d - c = b + d - (a + c) - (b - a)
⊢ n ∣ b + d - (a + c) - (b - a)

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

Premises used: Int.ModEq.dvd, Int.dvd_sub
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
h : c + a ≡ c + b [ZMOD n]
⊢ a ≡ b [ZMOD n]

Tactic:
ModEq.rfl.add_left_cancel h

Premises used: Int.ModEq.rfl, Int.ModEq.add_left_cancel
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c d : ℤ
h₁ : c ≡ d [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
⊢ c + a ≡ d + b [ZMOD n]

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

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

Tactic:
h₁.add_left_cancel h₂

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

Tactic:
exact h₁.add_left_cancel h₂

Premises used: Int.ModEq.add_left_cancel
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
h : a + c ≡ b + c [ZMOD n]
⊢ a ≡ b [ZMOD n]

Tactic:
ModEq.rfl.add_right_cancel h

Premises used: Int.ModEq.rfl, Int.ModEq.add_right_cancel
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
h : a ≡ b [ZMOD n]
simp_rw : 0 ≡ 0 [ZMOD n]
⊢ a + -a ≡ b + -b [ZMOD n]

Tactic:
simp_rw [← sub_eq_add_neg, sub_self]

Premises used: sub_self, sub_eq_add_neg
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 ≡ 0 [ZMOD n]

Tactic:
rfl
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ a + -c ≡ b + -d [ZMOD n]

Tactic:
h₁.add h₂.neg

Premises used: Int.ModEq.neg, Int.ModEq.add
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ a + -c ≡ b + -d [ZMOD n]

Tactic:
exact h₁.add h₂.neg

Premises used: Int.ModEq.neg, Int.ModEq.add
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ c - a ≡ c - b [ZMOD n]

Tactic:
ModEq.rfl.sub h

Premises used: Int.ModEq.sub, Int.ModEq.rfl
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ a - c ≡ b - c [ZMOD n]

Tactic:
h.sub ModEq.rfl

Premises used: Int.ModEq.sub, Int.ModEq.rfl
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ c * b [ZMOD n]

Tactic:
h.mul_left'.of_dvd <| dvd_mul_left _ _

Premises used: Int.ModEq.mul_left', dvd_mul_left, Int.ModEq.of_dvd
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ a * c ≡ b * c [ZMOD n]

Tactic:
h.mul_right'.of_dvd <| dvd_mul_right _ _

Premises used: Int.ModEq.mul_right', dvd_mul_right, Int.ModEq.of_dvd
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ a * c ≡ b * d [ZMOD n]

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

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

Tactic:
simp
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
h : a ≡ b [ZMOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [ZMOD n]
succ : a ^ d * a ≡ b ^ d * b [ZMOD n]
⊢ a ^ (d + 1) ≡ b ^ (d + 1) [ZMOD n]

Tactic:
rw [pow_succ, pow_succ]

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

Tactic:
hd.mul h

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

Tactic:
exact hd.mul h

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

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

Premises used: pow_succ, Int.succ
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b m : ℤ
h : a ≡ b [ZMOD m * n]
rw : ∀ (h : m * n ∣ b - a), n ∣ b - a
⊢ a ≡ b [ZMOD n]

Tactic:
rw [modEq_iff_dvd] at *

Premises used: Int.modEq_iff_dvd
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b m : ℤ
h : m * n ∣ b - a
⊢ n ∣ b - a

Tactic:
(dvd_mul_left n m).trans h

Premises used: dvd_mul_left, Dvd.dvd.trans
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b m : ℤ
h : m * n ∣ b - a
⊢ n ∣ b - a

Tactic:
exact (dvd_mul_left n m).trans h

Premises used: dvd_mul_left, Dvd.dvd.trans
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b m : ℤ
⊢ a ≡ b [ZMOD n * m] → a ≡ b [ZMOD n]

Tactic:
mul_comm m n ▸ of_mul_left _

Premises used: Int.ModEq.of_mul_left, Eq.rec, mul_comm
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
d : ℕ := m.gcd c
rw : ∀ (h : m ∣ b * c - a * c), m / (↑(m.gcd c) : ℤ) ∣ b - a
⊢ a ≡ b [ZMOD m / (↑(m.gcd c) : ℤ)]

Tactic:
rw [modEq_iff_dvd] at h ⊢

Premises used: Int.modEq_iff_dvd
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / (↑(m.gcd c) : ℤ) ∣ b - a

Tactic:
Int.dvd_of_dvd_mul_right_of_gcd_one (?_ : m / d ∣ c / d * (b - a)) ?_

Premises used: Int.dvd_of_dvd_mul_right_of_gcd_one
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
refine_1 : m / (↑d : ℤ) ∣ c / (↑d : ℤ) * (b - a)
refine_2 : (m / (↑(m.gcd c) : ℤ)).gcd (c / (↑d : ℤ)) = 1
⊢ m / (↑(m.gcd c) : ℤ) ∣ b - a

Tactic:
refine Int.dvd_of_dvd_mul_right_of_gcd_one (?_ : m / d ∣ c / d * (b - a)) ?_

Premises used: Int.dvd_of_dvd_mul_right_of_gcd_one
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
refine_1 : m / (↑d : ℤ) ∣ (b * c - a * c) / (↑(m.gcd c) : ℤ)
⊢ m / (↑d : ℤ) ∣ c / (↑d : ℤ) * (b - a)

Tactic:
rw [mul_comm, ← Int.mul_ediv_assoc (b - a) (gcd_dvd_right ..), Int.sub_mul]

Premises used: Int.sub_mul, Int.mul_ediv_assoc, HSub.hSub, mul_comm, Int.gcd_dvd_right
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / (↑d : ℤ) ∣ (b * c - a * c) / (↑(m.gcd c) : ℤ)

Tactic:
Int.ediv_dvd_ediv (gcd_dvd_left ..) h

Premises used: Int.gcd_dvd_left, Int.ediv_dvd_ediv
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / (↑d : ℤ) ∣ (b * c - a * c) / (↑(m.gcd c) : ℤ)

Tactic:
exact Int.ediv_dvd_ediv (gcd_dvd_left ..) h

Premises used: Int.gcd_dvd_left, Int.ediv_dvd_ediv
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
refine_2 : m.gcd c / natAbs (↑(m.gcd c) : ℤ) = 1
refine_2₁ : m.gcd c / m.gcd c = 1
refine_2₂ refine_2₃ : Eq (α := ℕ) 1 1
⊢ (m / (↑(m.gcd c) : ℤ)).gcd (c / (↑d : ℤ)) = 1

Tactic:
rw [gcd_div (gcd_dvd_left ..) (gcd_dvd_right ..), natAbs_natCast,
      Nat.div_self (gcd_pos_of_ne_zero_left c hm.ne')]

Premises used: LT.lt.ne', Nat.div_self, Int.gcd_dvd_left, Int.natAbs_natCast, Int.gcd_dvd_right, Int.gcd_div, Int.gcd_pos_of_ne_zero_left
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
hm : 0 < m
h : c * a ≡ c * b [ZMOD m]
⊢ a * c ≡ b * c [ZMOD m]

Tactic:
simpa [mul_comm] using h

Premises used: mul_comm
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
⊢ c * (a / c) ≡ c * (b / c) [ZMOD c * (m / c)]

Tactic:
h.mul_left'

Premises used: Int.ModEq.mul_left'
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
h₁ : m = c * (m / c)
h₂ : a = c * (a / c)
h₃ : b = c * (b / c)
convert! : ℤ
⊢ a ≡ b [ZMOD m]

Tactic:
convert! h.mul_left'

Premises used: Int.ModEq.mul_left'
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
h₁ : m = m
h₂ : c ∣ m
h₃ : m = m
h₄ h₅ h₆ : c ∣ m
⊢ m = c * (m / c)

Tactic:
rwa [Int.mul_ediv_cancel']

Premises used: Int.mul_ediv_cancel'
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
h₁ : a = a
h₂ : c ∣ a
h₃ : a = a
h₄ h₅ h₆ : c ∣ a
⊢ a = c * (a / c)

Tactic:
rwa [Int.mul_ediv_cancel']

Premises used: Int.mul_ediv_cancel'