awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ : b = b
h₂ : c ∣ b
h₃ : b = b
h₄ h₅ h₆ : c ∣ b
⊢ b = c * (b / c)

Tactic:
rwa [Int.mul_ediv_cancel']

Premises used: Int.mul_ediv_cancel'
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
hc : c ≠ 0
simp : c * m ∣ c * (b - a) → m ∣ b - a
⊢ c * a ≡ c * b [ZMOD c * m] → a ≡ b [ZMOD m]

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

Premises used: Int.modEq_iff_dvd, Int.mul_sub
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
hc : c ≠ 0
⊢ c * m ∣ c * (b - a) → m ∣ b - a

Tactic:
Int.dvd_of_mul_dvd_mul_left hc

Premises used: Int.dvd_of_mul_dvd_mul_left
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
hc : c ≠ 0
⊢ c * m ∣ c * (b - a) → m ∣ b - a

Tactic:
exact Int.dvd_of_mul_dvd_mul_left hc

Premises used: Int.dvd_of_mul_dvd_mul_left
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
hc : c ≠ 0
⊢ c * a ≡ c * b [ZMOD c * m] ↔ a ≡ b [ZMOD m]

Tactic:
⟨ModEq.mul_left_cancel' hc, Int.ModEq.mul_left'⟩

Premises used: Int.ModEq.mul_left', Iff.intro, Int.ModEq.mul_left_cancel'
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
hc : c ≠ 0
simp : m * c ∣ (b - a) * c → m ∣ b - a
⊢ a * c ≡ b * c [ZMOD m * c] → a ≡ b [ZMOD m]

Tactic:
simp only [modEq_iff_dvd, ← Int.sub_mul]

Premises used: Int.modEq_iff_dvd, Int.sub_mul
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
hc : c ≠ 0
⊢ m * c ∣ (b - a) * c → m ∣ b - a

Tactic:
Int.dvd_of_mul_dvd_mul_right hc

Premises used: Int.dvd_of_mul_dvd_mul_right
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
hc : c ≠ 0
⊢ m * c ∣ (b - a) * c → m ∣ b - a

Tactic:
exact Int.dvd_of_mul_dvd_mul_right hc

Premises used: Int.dvd_of_mul_dvd_mul_right
-- Module: Mathlib.Data.Int.ModEq
Goal:
m a b c : ℤ
hc : c ≠ 0
⊢ a * c ≡ b * c [ZMOD m * c] ↔ a ≡ b [ZMOD m]

Tactic:
⟨ModEq.mul_right_cancel' hc, ModEq.mul_right'⟩

Premises used: Int.ModEq.mul_right', Int.ModEq.mul_right_cancel', Iff.intro
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
h : a ≡ b [ZMOD n]
simp : a ≡ 0 [ZMOD n] ↔ b ≡ 0 [ZMOD n]
⊢ n ∣ a ↔ n ∣ b

Tactic:
simp only [← modEq_zero_iff_dvd]

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

Tactic:
⟨fun ha ↦ h.symm.trans ha, h.trans⟩

Premises used: Int.ModEq.symm, Int.ModEq.trans, Iff.intro
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ a ≡ 0 [ZMOD n] ↔ b ≡ 0 [ZMOD n]

Tactic:
exact ⟨fun ha ↦ h.symm.trans ha, h.trans⟩
-- Module: Mathlib.Data.Int.ModEq
Goal:
n : ℤ
⊢ n ≡ 0 [ZMOD n]

Tactic:
simp [ModEq]

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

Tactic:
simp [ModEq]

Premises used: Int.ModEq
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
⊢ a ≡ b [ZMOD (↑n.natAbs : ℤ)] ↔ a ≡ b [ZMOD n]

Tactic:
simp [natCast_natAbs]

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

Tactic:
simp [modEq_iff_dvd]

Premises used: Int.modEq_iff_dvd
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
rw : b + a ≡ b [ZMOD n] ↔ n ∣ a
rw₁ rw₂ : n ∣ a ↔ n ∣ a
⊢ a + b ≡ b [ZMOD n] ↔ n ∣ a

Tactic:
rw [add_comm, add_modEq_left_iff]

Premises used: Int.add_modEq_left_iff, add_comm
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
rw : a + b ≡ a [ZMOD n] ↔ n ∣ b
rw₁ rw₂ : n ∣ b ↔ n ∣ b
⊢ a ≡ a + b [ZMOD n] ↔ n ∣ b

Tactic:
rw [modEq_comm, add_modEq_left_iff]

Premises used: Int.add_modEq_left_iff, Int.modEq_comm
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
rw : a + b ≡ b [ZMOD n] ↔ n ∣ a
rw₁ rw₂ : n ∣ a ↔ n ∣ a
⊢ b ≡ a + b [ZMOD n] ↔ n ∣ a

Tactic:
rw [modEq_comm, add_modEq_right_iff]

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

Tactic:
simp [ModEq]

Premises used: Int.ModEq
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
rw : a + n ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
rw₁ rw₂ : a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
⊢ n + a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
rw [add_comm, add_modulus_modEq_iff]

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

Tactic:
simp [ModEq]

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

Tactic:
simp [ModEq]

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

Tactic:
simp [ModEq]

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

Tactic:
rw [add_comm, add_mul_modulus_modEq_iff]

Premises used: Int.add_mul_modulus_modEq_iff, add_comm
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
⊢ a ≡ b + c * n [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
simp [ModEq]

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

Tactic:
rw [add_comm, modEq_add_mul_modulus_iff]

Premises used: add_comm, Int.modEq_add_mul_modulus_iff
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
⊢ a + n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
simp [ModEq]

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

Tactic:
rw [add_comm, add_modulus_mul_modEq_iff]

Premises used: Int.add_modulus_mul_modEq_iff, add_comm
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
⊢ a ≡ b + n * c [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
simp [ModEq]

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

Tactic:
rw [add_comm, modEq_add_modulus_mul_iff]

Premises used: add_comm, Int.modEq_add_modulus_mul_iff
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
rw : a - n + n ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
rw₁ rw₂ : a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
⊢ a - n ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
rw [← add_modulus_modEq_iff, sub_add_cancel]

Premises used: Int.add_modulus_modEq_iff, sub_add_cancel
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
rw : a - n * b + n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
rw₁ : ℤ
rw₂ rw₃ : a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
⊢ a - n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
rw [← add_modulus_mul_modEq_iff, sub_add_cancel]

Premises used: Int.add_modulus_mul_modEq_iff, sub_add_cancel
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
rw : a ≡ b - n + n [ZMOD n] ↔ a ≡ b [ZMOD n]
rw₁ rw₂ : a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
⊢ a ≡ b - n [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
rw [← modEq_add_modulus_iff, sub_add_cancel]

Premises used: Int.modEq_add_modulus_iff, sub_add_cancel
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b c : ℤ
rw : a ≡ b - n * c + n * c [ZMOD n] ↔ a ≡ b [ZMOD n]
rw₁ : ℤ
rw₂ rw₃ : a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
⊢ a ≡ b - n * c [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
rw [← modEq_add_modulus_mul_iff, sub_add_cancel]

Premises used: Int.modEq_add_modulus_mul_iff, sub_add_cancel
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b : ℤ
⊢ a ≡ b [ZMOD 1]

Tactic:
modEq_of_dvd (one_dvd _)

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

Tactic:
(modEq_of_dvd dvd_rfl).symm

Premises used: Int.ModEq.symm, Int.modEq_of_dvd, dvd_rfl
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b : ℤ
rw : a % 0 = b % 0 ↔ a = b
rw₁ : a = b % 0 ↔ a = b
rw₂ rw₃ : a = b ↔ a = b
⊢ a ≡ b [ZMOD 0] ↔ a = b

Tactic:
rw [ModEq, emod_zero, emod_zero]

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

Tactic:
simp
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a : ℤ
⊢ a + n ≡ a [ZMOD n]

Tactic:
simp
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b m n : ℤ
⊢ a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD (↑(m.lcm n) : ℤ)]

Tactic:
simp only [modEq_iff_dvd, coe_lcm_dvd_iff]

Premises used: Int.coe_lcm_dvd_iff, Int.modEq_iff_dvd
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
⊢ a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD (↑(m.lcm n) : ℤ)]

Tactic:
modEq_and_modEq_iff_modEq_lcm

Premises used: Int.modEq_and_modEq_iff_modEq_lcm
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
h : a ≡ b [ZMOD (↑(m.lcm n) : ℤ)] ↔ a ≡ b [ZMOD m * n]
⊢ a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n]

Tactic:
convert! ← modEq_and_modEq_iff_modEq_lcm using 1

Premises used: Int.modEq_and_modEq_iff_modEq_lcm
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
h : a ≡ b [ZMOD (↑(m.natAbs * n.natAbs) : ℤ)] ↔ a ≡ b [ZMOD m * n]
h₁ : a ≡ b [ZMOD (↑(m * n).natAbs : ℤ)] ↔ a ≡ b [ZMOD m * n]
h₂ h₃ : a ≡ b [ZMOD m * n] ↔ a ≡ b [ZMOD m * n]
⊢ a ≡ b [ZMOD (↑(m.lcm n) : ℤ)] ↔ a ≡ b [ZMOD m * n]

Tactic:
rw [lcm_eq_mul_iff.mpr (.inr <| .inr hmn), ← natAbs_mul, modEq_natAbs]

Premises used: Iff.mpr, Int.natAbs_mul, Int.lcm_eq_mul_iff, Int.modEq_natAbs, Or.inr
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b : ℕ
rw : (↑a : ℤ) * a.gcdA b + 0 ≡ (↑a : ℤ) * a.gcdA b + (↑b : ℤ) * a.gcdB b [ZMOD (↑b : ℤ)]
⊢ (↑a : ℤ) * a.gcdA b ≡ (↑(a.gcd b) : ℤ) [ZMOD (↑b : ℤ)]

Tactic:
rw [← add_zero ((a : ℤ) * _), Nat.gcd_eq_gcd_ab]

Premises used: HMul.hMul, Nat.cast, add_zero, Nat.gcd_eq_gcd_ab
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b : ℕ
⊢ (↑a : ℤ) * a.gcdA b + 0 ≡ (↑a : ℤ) * a.gcdA b + (↑b : ℤ) * a.gcdB b [ZMOD (↑b : ℤ)]

Tactic:
(dvd_mul_right _ _).zero_modEq_int.add_left _

Premises used: Int.ModEq.add_left, Dvd.dvd.zero_modEq_int, dvd_mul_right
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b : ℕ
⊢ (↑a : ℤ) * a.gcdA b + 0 ≡ (↑a : ℤ) * a.gcdA b + (↑b : ℤ) * a.gcdB b [ZMOD (↑b : ℤ)]

Tactic:
exact (dvd_mul_right _ _).zero_modEq_int.add_left _

Premises used: Int.ModEq.add_left, Dvd.dvd.zero_modEq_int, dvd_mul_right
-- Module: Mathlib.Data.Int.ModEq
Goal:
a t n : ℤ
⊢ a + n * t ≡ a [ZMOD n]

Tactic:
simp
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b : ℕ
hab : a.Coprime b
hgcd : a.gcd b = 1
⊢ (↑a : ℤ) * a.gcdA b ≡ (↑a : ℤ) * a.gcdA b + (↑b : ℤ) * a.gcdB b [ZMOD (↑b : ℤ)]

Tactic:
simp
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b : ℕ
hab : a.Coprime b
hgcd : a.gcd b = 1
rw : (↑1 : ℤ) ≡ 1 [ZMOD (↑b : ℤ)]
⊢ (↑a : ℤ) * a.gcdA b + (↑b : ℤ) * a.gcdB b ≡ 1 [ZMOD (↑b : ℤ)]

Tactic:
rw [← Nat.gcd_eq_gcd_ab, hgcd]

Premises used: Nat.gcd_eq_gcd_ab
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b : ℕ
hab : a.Coprime b
hgcd : a.gcd b = 1
⊢ (↑1 : ℤ) ≡ 1 [ZMOD (↑b : ℤ)]

Tactic:
rfl
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b : ℤ
hb : 0 < b
⊢ a % b < |b|

Tactic:
have : a % b < |b| := emod_lt_abs _ (ne_of_gt hb)
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b : ℤ
hb : 0 < b
this : a % b < |b|
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : a % b < b), a % b < b
⊢ a % b < b

Tactic:
rwa [abs_of_pos hb] at this

Premises used: abs_of_pos
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b : ℤ
hb : 0 < b
⊢ a % b ≡ a [ZMOD b]

Tactic:
simp [ModEq]

Premises used: Int.ModEq
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
left : (↑z.natAbs : ℤ) < b
right : (↑z.natAbs : ℤ) ≡ a [ZMOD b]
⊢ (↑z.natAbs : ℤ) < b ∧ (↑z.natAbs : ℤ) ≡ a [ZMOD b]

Tactic:
constructor
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
left : z < b
⊢ (↑z.natAbs : ℤ) < b

Tactic:
rw [natAbs_of_nonneg hz1]

Premises used: Int.natAbs_of_nonneg
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 right : z ≡ a [ZMOD b]
⊢ (↑z.natAbs : ℤ) ≡ a [ZMOD b]

Tactic:
rw [natAbs_of_nonneg hz1]

Premises used: Int.natAbs_of_nonneg
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ z < b

Tactic:
assumption
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ z ≡ a [ZMOD b]

Tactic:
assumption
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b c : ℤ
⊢ a % (b * c) % b = a % b

Tactic:
(mod_modEq _ _).of_mul_right _

Premises used: Int.ModEq.of_mul_right, Int.ModEq, Int.mod_modEq
-- Module: Mathlib.Data.Int.ModEq
Goal:
a b c : ℤ
⊢ a % (b * c) % c = a % c

Tactic:
(mod_modEq _ _).of_mul_left _

Premises used: Int.ModEq.of_mul_left, Int.ModEq, Int.mod_modEq
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
h0 : a / n = b / n
h1 : a ≡ b [ZMOD n]
⊢ a = b

Tactic:
ext_ediv_emod h0 h1

Premises used: Int.ext_ediv_emod
-- Module: Mathlib.Data.Int.ModEq
Goal:
n a b : ℤ
⊢ a = b ↔ a / n = b / n ∧ a ≡ b [ZMOD n]

Tactic:
ext_ediv_emod_iff _ _ _

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

Tactic:
grind [ext_ediv_modEq_iff]

Premises used: Int.ext_ediv_modEq_iff
-- Module: Mathlib.Data.Int.NatAbs
Goal:
a b : ℕ
h : b ≤ a
⊢ (HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)).natAbs = a - b

Tactic:
lia
-- Module: Mathlib.Data.Int.NatAbs
Goal:
a b : ℕ
h : a ≤ b
⊢ (HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)).natAbs = b - a

Tactic:
lia
-- Module: Mathlib.Data.Int.NatPrime
Goal:
a b : ℤ
c : ℕ
ha : a.natAbs ≠ 1
hb : b.natAbs ≠ 1
hc : a * b = (↑c : ℤ)
⊢ ¬Nat.Prime c

Tactic:
not_prime_of_mul_eq (natAbs_mul_natAbs_eq hc) ha hb

Premises used: Int.natAbs_mul_natAbs_eq, Nat.not_prime_of_mul_eq
-- Module: Mathlib.Data.Int.NatPrime
Goal:
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : (↑(p ^ k) : ℤ) ∣ m
hpn : (↑(p ^ l) : ℤ) ∣ n
hpmn : (↑(p ^ (k + l + 1)) : ℤ) ∣ m * n
hpm' : p ^ k ∣ m.natAbs
hpn' : p ^ l ∣ n.natAbs
rw : p ^ (k + l + 1) ∣ (m * n).natAbs
⊢ p ^ (k + l + 1) ∣ m.natAbs * n.natAbs

Tactic:
rw [← Int.natAbs_mul]

Premises used: Int.natAbs_mul
-- Module: Mathlib.Data.Int.NatPrime
Goal:
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : (↑(p ^ k) : ℤ) ∣ m
hpn : (↑(p ^ l) : ℤ) ∣ n
hpmn : (↑(p ^ (k + l + 1)) : ℤ) ∣ m * n
hpm' : p ^ k ∣ m.natAbs
hpn' : p ^ l ∣ n.natAbs
⊢ p ^ (k + l + 1) ∣ (m * n).natAbs

Tactic:
apply Int.natCast_dvd_natCast.1 <| Int.dvd_natAbs.2 hpmn

Premises used: Iff.mpr, Int.dvd_natAbs, Iff.mp, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Int.NatPrime
Goal:
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : (↑(p ^ k) : ℤ) ∣ m
hpn : (↑(p ^ l) : ℤ) ∣ n
hpmn : (↑(p ^ (k + l + 1)) : ℤ) ∣ m * n
hpm' : p ^ k ∣ m.natAbs
hpn' : p ^ l ∣ n.natAbs
hpmn' : p ^ (k + l + 1) ∣ m.natAbs * n.natAbs
hsd : p ^ (k + 1) ∣ m.natAbs ∨ p ^ (l + 1) ∣ n.natAbs := ⋯
hsd1 : p ^ (k + 1) ∣ m.natAbs
apply : Dvd.dvd (α := ℤ) (↑(p ^ (k + 1)) : ℤ) (↑m.natAbs : ℤ)
⊢ (↑(p ^ (k + 1)) : ℤ) ∣ m

Tactic:
apply Int.dvd_natAbs.1

Premises used: Int.dvd_natAbs, Iff.mp
-- Module: Mathlib.Data.Int.NatPrime
Goal:
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : (↑(p ^ k) : ℤ) ∣ m
hpn : (↑(p ^ l) : ℤ) ∣ n
hpmn : (↑(p ^ (k + l + 1)) : ℤ) ∣ m * n
hpm' : p ^ k ∣ m.natAbs
hpn' : p ^ l ∣ n.natAbs
hpmn' : p ^ (k + l + 1) ∣ m.natAbs * n.natAbs
hsd : p ^ (k + 1) ∣ m.natAbs ∨ p ^ (l + 1) ∣ n.natAbs := ⋯
hsd1 : p ^ (k + 1) ∣ m.natAbs
⊢ Dvd.dvd (α := ℤ) (↑(p ^ (k + 1)) : ℤ) (↑m.natAbs : ℤ)

Tactic:
apply Int.natCast_dvd_natCast.2 hsd1

Premises used: Iff.mpr, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Int.NatPrime
Goal:
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : (↑(p ^ k) : ℤ) ∣ m
hpn : (↑(p ^ l) : ℤ) ∣ n
hpmn : (↑(p ^ (k + l + 1)) : ℤ) ∣ m * n
hpm' : p ^ k ∣ m.natAbs
hpn' : p ^ l ∣ n.natAbs
hpmn' : p ^ (k + l + 1) ∣ m.natAbs * n.natAbs
hsd : p ^ (k + 1) ∣ m.natAbs ∨ p ^ (l + 1) ∣ n.natAbs := ⋯
hsd2 : p ^ (l + 1) ∣ n.natAbs
apply : Dvd.dvd (α := ℤ) (↑(p ^ (l + 1)) : ℤ) (↑n.natAbs : ℤ)
⊢ (↑(p ^ (l + 1)) : ℤ) ∣ n

Tactic:
apply Int.dvd_natAbs.1

Premises used: Int.dvd_natAbs, Iff.mp
-- Module: Mathlib.Data.Int.NatPrime
Goal:
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : (↑(p ^ k) : ℤ) ∣ m
hpn : (↑(p ^ l) : ℤ) ∣ n
hpmn : (↑(p ^ (k + l + 1)) : ℤ) ∣ m * n
hpm' : p ^ k ∣ m.natAbs
hpn' : p ^ l ∣ n.natAbs
hpmn' : p ^ (k + l + 1) ∣ m.natAbs * n.natAbs
hsd : p ^ (k + 1) ∣ m.natAbs ∨ p ^ (l + 1) ∣ n.natAbs := ⋯
hsd2 : p ^ (l + 1) ∣ n.natAbs
⊢ Dvd.dvd (α := ℤ) (↑(p ^ (l + 1)) : ℤ) (↑n.natAbs : ℤ)

Tactic:
apply Int.natCast_dvd_natCast.2 hsd2

Premises used: Iff.mpr, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Int.NatPrime
Goal:
p : ℕ
hp : Nat.Prime p
k : ℤ
h : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) k 2
apply : p ∣ HPow.hPow (β := ℕ) k.natAbs 2
⊢ p ∣ k.natAbs

Tactic:
apply @Nat.Prime.dvd_of_dvd_pow _ _ 2 hp

Premises used: Nat.Prime.dvd_of_dvd_pow
-- Module: Mathlib.Data.Int.NatPrime
Goal:
p : ℕ
hp : Nat.Prime p
k : ℤ
h : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) k 2
rwa : p ∣ k.natAbs * k.natAbs
rwa₁ : p ∣ (k * k).natAbs
rwa₂ : (↑p : ℤ) ∣ k * k
rwa₃ rwa₄ rwa₅ rwa₆ : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) k 2
⊢ p ∣ HPow.hPow (β := ℕ) k.natAbs 2

Tactic:
rwa [sq, ← natAbs_mul, ← natCast_dvd, ← sq]

Premises used: Int.natAbs_mul, sq, Int.natCast_dvd
-- Module: Mathlib.Data.Int.Order.Basic
Goal:
a b : ℤ
h : a ≤ b
P : Prop
h' : ∀ (n : ℕ), a + (↑n : ℤ) = b → P
⊢ P

Tactic:
Exists.elim (le.dest h) h'

Premises used: Int.le.dest, Exists.elim
-- Module: Mathlib.Data.Int.Order.Basic
Goal:
a b : ℤ
h : a < b
P : Prop
h' : ∀ (n : ℕ), a + (↑n.succ : ℤ) = b → P
⊢ P

Tactic:
Exists.elim (lt.dest h) h'

Premises used: Int.lt.dest, Exists.elim
-- Module: Mathlib.Data.Int.Order.Basic
Goal:
a b : ℤ
⊢ 0 ≤ a * b → 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
grind [Int.mul_comm, Int.mul_nonneg_iff_of_pos_right]

Premises used: Int.mul_comm, Int.mul_nonneg_iff_of_pos_right
-- Module: Mathlib.Data.Int.Order.Basic
Goal:
a b : ℤ
⊢ 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
⟨nonneg_or_nonpos_of_mul_nonneg, mul_nonneg_of_nonneg_or_nonpos⟩

Premises used: Iff.intro, Int.mul_nonneg_of_nonneg_or_nonpos, Int.nonneg_or_nonpos_of_mul_nonneg
-- Module: Mathlib.Data.Int.Order.Basic
Goal:
a b : ℤ
rw : (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∧ a ≠ 0 ∧ b ≠ 0 ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
rw [Int.lt_iff_le_and_ne, Int.mul_nonneg_iff, ne_comm, Int.mul_ne_zero_iff]

Premises used: Int.mul_nonneg_iff, Int.mul_ne_zero_iff, Int.lt_iff_le_and_ne, ne_comm
-- Module: Mathlib.Data.Int.Order.Basic
Goal:
a b : ℤ
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∧ a ≠ 0 ∧ b ≠ 0 ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
lia
-- Module: Mathlib.Data.Int.Order.Basic
Goal:
a b : ℤ
rw : 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 ↔ ¬(0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b)
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
rw [← not_iff_not, not_le, Int.mul_pos_iff]

Premises used: not_le, not_iff_not, Int.mul_pos_iff
-- Module: Mathlib.Data.Int.Order.Basic
Goal:
a b : ℤ
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 ↔ ¬(0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b)

Tactic:
lia
-- Module: Mathlib.Data.Int.Order.Basic
Goal:
a b : ℤ
rw : 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ ¬(0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b)
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
rw [← not_iff_not, not_lt, Int.mul_nonneg_iff]

Premises used: not_iff_not, Int.mul_nonneg_iff, not_lt
-- Module: Mathlib.Data.Int.Order.Basic
Goal:
a b : ℤ
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ ¬(0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b)

Tactic:
lia
-- Module: Mathlib.Data.Int.Order.Lemmas
Goal:
a b : ℤ
rw : a.natAbs = b.natAbs ↔ Eq (α := ℤ) (↑a.natAbs : ℤ) (↑b.natAbs : ℤ)
⊢ a.natAbs = b.natAbs ↔ a * a = b * b

Tactic:
rw [← abs_eq_iff_mul_self_eq, abs_eq_natAbs, abs_eq_natAbs]

Premises used: abs_eq_iff_mul_self_eq, Int.abs_eq_natAbs
-- Module: Mathlib.Data.Int.Order.Lemmas
Goal:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ Eq (α := ℤ) (↑a.natAbs : ℤ) (↑b.natAbs : ℤ)

Tactic:
Int.natCast_inj.symm

Premises used: Iff.symm, Int.natCast_inj
-- Module: Mathlib.Data.Int.Order.Lemmas
Goal:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ Eq (α := ℤ) (↑a.natAbs : ℤ) (↑b.natAbs : ℤ)

Tactic:
exact Int.natCast_inj.symm

Premises used: Iff.symm, Int.natCast_inj
-- Module: Mathlib.Data.Int.Order.Lemmas
Goal:
a b : ℤ
rw : a.natAbs < b.natAbs ↔ LT.lt (α := ℤ) (↑a.natAbs : ℤ) (↑b.natAbs : ℤ)
⊢ a.natAbs < b.natAbs ↔ a * a < b * b

Tactic:
rw [← abs_lt_iff_mul_self_lt, abs_eq_natAbs, abs_eq_natAbs]

Premises used: abs_lt_iff_mul_self_lt, Int.abs_eq_natAbs
-- Module: Mathlib.Data.Int.Order.Lemmas
Goal:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ LT.lt (α := ℤ) (↑a.natAbs : ℤ) (↑b.natAbs : ℤ)

Tactic:
Int.ofNat_lt.symm

Premises used: Int.ofNat_lt, Iff.symm
-- Module: Mathlib.Data.Int.Order.Lemmas
Goal:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ LT.lt (α := ℤ) (↑a.natAbs : ℤ) (↑b.natAbs : ℤ)

Tactic:
exact Int.ofNat_lt.symm

Premises used: Int.ofNat_lt, Iff.symm
-- Module: Mathlib.Data.Int.Order.Lemmas
Goal:
a b : ℤ
rw : a.natAbs ≤ b.natAbs ↔ LE.le (α := ℤ) (↑a.natAbs : ℤ) (↑b.natAbs : ℤ)
⊢ a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b

Tactic:
rw [← abs_le_iff_mul_self_le, abs_eq_natAbs, abs_eq_natAbs]

Premises used: abs_le_iff_mul_self_le, Int.abs_eq_natAbs
-- Module: Mathlib.Data.Int.Order.Lemmas
Goal:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ LE.le (α := ℤ) (↑a.natAbs : ℤ) (↑b.natAbs : ℤ)

Tactic:
Int.ofNat_le.symm

Premises used: Int.ofNat_le, Iff.symm
-- Module: Mathlib.Data.Int.Order.Lemmas
Goal:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ LE.le (α := ℤ) (↑a.natAbs : ℤ) (↑b.natAbs : ℤ)

Tactic:
exact Int.ofNat_le.symm

Premises used: Int.ofNat_le, Iff.symm
-- Module: Mathlib.Data.Int.Order.Lemmas
Goal:
a b : ℤ
hn : 0 ≤ b
rw : |a| ≤ sqrt b ↔ |a| * |a| ≤ b
rw₁ : |a| ≤ sqrt (↑b.toNat : ℤ) ↔ |a| * |a| ≤ (↑b.toNat : ℤ)
rw₂ : (↑|a|.toNat : ℤ) ≤ sqrt (↑b.toNat : ℤ) ↔ HMul.hMul (α := ℤ) (↑|a|.toNat : ℤ) (↑|a|.toNat : ℤ) ≤ (↑b.toNat : ℤ)
rw₃ :
  LE.le (α := ℤ) (↑|a|.toNat : ℤ) (↑b.toNat.sqrt : ℤ) ↔
    HMul.hMul (α := ℤ) (↑|a|.toNat : ℤ) (↑|a|.toNat : ℤ) ≤ (↑b.toNat : ℤ)
rw₄ : LE.le (α := ℤ) (↑|a|.toNat : ℤ) (↑b.toNat.sqrt : ℤ) ↔ LE.le (α := ℤ) (↑(|a|.toNat * |a|.toNat) : ℤ) (↑b.toNat : ℤ)
rw₅ : |a|.toNat ≤ b.toNat.sqrt ↔ LE.le (α := ℤ) (↑(|a|.toNat * |a|.toNat) : ℤ) (↑b.toNat : ℤ)
rw₆ : |a|.toNat ≤ b.toNat.sqrt ↔ |a|.toNat * |a|.toNat ≤ b.toNat
rw₇ rw₈ : |a|.toNat * |a|.toNat ≤ b.toNat ↔ |a|.toNat * |a|.toNat ≤ b.toNat
⊢ |a| ≤ sqrt b ↔ a * a ≤ b

Tactic:
rw [← abs_mul_abs_self, eq_natCast_toNat.mpr hn, eq_natCast_toNat.mpr (abs_nonneg a),
    Int.sqrt_natCast, ← Int.natCast_mul, Nat.cast_le, Nat.cast_le, Nat.le_sqrt]

Premises used: Iff.mpr, Int.natCast_mul, Int.sqrt_natCast, Nat.le_sqrt, Int.eq_natCast_toNat, abs_mul_abs_self, Nat.cast_le, abs_nonneg
-- Module: Mathlib.Data.Int.Order.Lemmas
Goal:
a b : ℤ
hn : 0 ≤ b
⊢ |a| ≤ sqrt b ↔ HPow.hPow (β := ℕ) a 2 ≤ b

Tactic:
pow_two a ▸ abs_le_sqrt hn

Premises used: Int.abs_le_sqrt, pow_two, Eq.rec, Eq.symm
-- Module: Mathlib.Data.Int.Order.Units
Goal:
x : ℤ
rw : x.natAbs = 1 ↔ |x| = 1
rw₁ : x.natAbs = 1 ↔ Eq (α := ℤ) (↑x.natAbs : ℤ) 1
rw₂ : x.natAbs = 1 ↔ Eq (α := ℤ) (↑x.natAbs : ℤ) (↑1 : ℤ)
rw₃ rw₄ : x.natAbs = 1 ↔ x.natAbs = 1
⊢ IsUnit x ↔ |x| = 1

Tactic:
rw [isUnit_iff_natAbs_eq, abs_eq_natAbs, ← Int.ofNat_one, natCast_inj]

Premises used: Int.isUnit_iff_natAbs_eq, Int.ofNat_one, Int.abs_eq_natAbs, Int.natCast_inj
-- Module: Mathlib.Data.Int.Order.Units
Goal:
a : ℤ
ha : IsUnit a
rw : a * a = 1
rw₁ rw₂ : Eq (α := ℤ) 1 1
⊢ HPow.hPow (β := ℕ) a 2 = 1

Tactic:
rw [sq, isUnit_mul_self ha]

Premises used: Int.isUnit_mul_self, sq
-- Module: Mathlib.Data.Int.Order.Units
Goal:
u : ℤˣ
rw : (↑(HPow.hPow (β := ℕ) u 2) : ℤ) = (↑1 : ℤ)
rw₁ : HPow.hPow (β := ℕ) (↑u : ℤ) 2 = (↑1 : ℤ)
rw₂ : HPow.hPow (β := ℕ) (↑u : ℤ) 2 = 1
rw₃ rw₄ : Eq (α := ℤ) 1 1
⊢ HPow.hPow (β := ℕ) u 2 = 1

Tactic:
rw [Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one, isUnit_sq u.isUnit]

Premises used: Units.ext_iff, Int.isUnit_sq, Units.val_one, Units.isUnit, Units.val_pow_eq_pow_val
-- Module: Mathlib.Data.Int.Order.Units
Goal:
u : ℤˣ
rw : HPow.hPow (β := ℕ) u 2 = 1
rw₁ rw₂ : Eq (α := ℤˣ) 1 1
⊢ u * u = 1

Tactic:
rw [← sq, units_sq]

Premises used: sq, Int.units_sq
-- Module: Mathlib.Data.Int.Order.Units
Goal:
u : ℤˣ
rw : u * u = 1
rw₁ rw₂ : Eq (α := ℤˣ) 1 1
⊢ u⁻¹ = u

Tactic:
rw [inv_eq_iff_mul_eq_one, units_mul_self]

Premises used: Int.units_mul_self, inv_eq_iff_mul_eq_one
-- Module: Mathlib.Data.Int.Order.Units
Goal:
u₁ u₂ : ℤˣ
rw : u₁ * u₂⁻¹ = u₁ * u₂
rw₁ rw₂ : u₁ * u₂ = u₁ * u₂
⊢ u₁ / u₂ = u₁ * u₂

Tactic:
rw [div_eq_mul_inv, units_inv_eq_self]

Premises used: Int.units_inv_eq_self, div_eq_mul_inv