awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
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]
⊢ c * a ≡ c * b [ZMOD c * n]
have inr₁ : ∀ (hc : 0 < c), c * a ≡ c * b [ZMOD c * n]
Tactic: obtain hc | rfl | hc := lt_trichotomy c 0
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ c * a ≡ c * b [ZMOD c * n]
have inl : -c * a ≡ -c * b [ZMOD -c * n]
Tactic: rw [← neg_modEq_neg, ← modEq_neg, ← Int.neg_mul, ← Int.neg_mul, ← Int.neg_mul]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ a * c ≡ b * c [ZMOD n * c]
have rw : c * a ≡ c * b [ZMOD c * n]
Tactic: rw [mul_comm a, mul_comm b, mul_comm n]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ n ∣ b + d - (a + c)
have h : b + d - (a + c) = b - a + (d - c)
Tactic: convert! Int.dvd_add h₁.dvd h₂.dvd using 1
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
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 ∣ d - c
have rw : n ∣ b + d - (a + c) - (b - a)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (hypothesis)
Goal:
n a b c d : ℤ
h₁ : c ≡ d [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
⊢ a ≡ b [ZMOD n]
have h₃ : c + a ≡ d + b [ZMOD n]
Tactic: rw [add_comm a, add_comm b] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ a + -a ≡ b + -b [ZMOD n]
have simp_rw : 0 ≡ 0 [ZMOD n]
Tactic: simp_rw [← sub_eq_add_neg, sub_self]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
h : a ≡ b [ZMOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [ZMOD n]
⊢ a ^ (d + 1) ≡ b ^ (d + 1) [ZMOD n]
have succ : a ^ d * a ≡ b ^ d * b [ZMOD n]
Tactic: rw [pow_succ, pow_succ]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
m : ℕ
h : a ≡ b [ZMOD n]
⊢ a ^ m ≡ b ^ m [ZMOD n]
have zero : HPow.hPow (β := ℕ) a 0 ≡ HPow.hPow (β := ℕ) b 0 [ZMOD n]
Tactic: induction m with
  | zero => simp
  | succ d hd => rw [pow_succ, pow_succ]; exact hd.mul h
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
m : ℕ
h : a ≡ b [ZMOD n]
zero : HPow.hPow (β := ℕ) a 0 ≡ HPow.hPow (β := ℕ) b 0 [ZMOD n]
⊢ a ^ m ≡ b ^ m [ZMOD n]
have succ : ∀ (d : ℕ) (hd : a ^ d ≡ b ^ d [ZMOD n]), a ^ (d + 1) ≡ b ^ (d + 1) [ZMOD n]
Tactic: induction m with
  | zero => simp
  | succ d hd => rw [pow_succ, pow_succ]; exact hd.mul h
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b m : ℤ
h : a ≡ b [ZMOD m * n]
⊢ a ≡ b [ZMOD n]
have rw : ∀ (h : m * n ∣ b - a), n ∣ b - a
Tactic: rw [modEq_iff_dvd] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
m a b c : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
d : ℕ := m.gcd c
⊢ a ≡ b [ZMOD m / (↑(m.gcd c) : ℤ)]
have rw : ∀ (h : m ∣ b * c - a * c), m / (↑(m.gcd c) : ℤ) ∣ b - a
Tactic: rw [modEq_iff_dvd] at h ⊢
Cleared hypotheses: h, d
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / (↑(m.gcd c) : ℤ) ∣ b - a
have refine_1 : m / (↑d : ℤ) ∣ c / (↑d : ℤ) * (b - a)
Tactic: refine Int.dvd_of_dvd_mul_right_of_gcd_one (?_ : m / d ∣ c / d * (b - a)) ?_
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
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)
⊢ m / (↑(m.gcd c) : ℤ) ∣ b - a
have refine_2 : (m / (↑(m.gcd c) : ℤ)).gcd (c / (↑d : ℤ)) = 1
Tactic: refine Int.dvd_of_dvd_mul_right_of_gcd_one (?_ : m / d ∣ c / d * (b - a)) ?_
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / (↑d : ℤ) ∣ c / (↑d : ℤ) * (b - a)
have refine_1 : m / (↑d : ℤ) ∣ (b * c - a * c) / (↑(m.gcd c) : ℤ)
Tactic: rw [mul_comm, ← Int.mul_ediv_assoc (b - a) (gcd_dvd_right ..), Int.sub_mul]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ (m / (↑(m.gcd c) : ℤ)).gcd (c / (↑d : ℤ)) = 1
have refine_2 : m.gcd c / natAbs (↑(m.gcd c) : ℤ) = 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')]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
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
⊢ (m / (↑(m.gcd c) : ℤ)).gcd (c / (↑d : ℤ)) = 1
have refine_2₁ : m.gcd c / m.gcd c = 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')]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
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
⊢ (m / (↑(m.gcd c) : ℤ)).gcd (c / (↑d : ℤ)) = 1
have refine_2₂ : Eq (α := ℕ) 1 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')]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
⊢ a ≡ b [ZMOD m]
have h₁ : m = c * (m / c)
Tactic: convert! h.mul_left'
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
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)
⊢ a ≡ b [ZMOD m]
have h₂ : a = c * (a / c)
Tactic: convert! h.mul_left'
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
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)
⊢ a ≡ b [ZMOD m]
have h₃ : b = c * (b / c)
Tactic: convert! h.mul_left'
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
⊢ m = c * (m / c)
have h₁ : m = m
Tactic: rwa [Int.mul_ediv_cancel']
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
⊢ a = c * (a / c)
have h₁ : a = a
Tactic: rwa [Int.mul_ediv_cancel']
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
⊢ b = c * (b / c)
have h₁ : b = b
Tactic: rwa [Int.mul_ediv_cancel']
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
m a b c : ℤ
hc : c ≠ 0
⊢ c * a ≡ c * b [ZMOD c * m] → a ≡ b [ZMOD m]
have simp : c * m ∣ c * (b - a) → m ∣ b - a
Tactic: simp only [modEq_iff_dvd, ← Int.mul_sub]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
m a b c : ℤ
hc : c ≠ 0
⊢ a * c ≡ b * c [ZMOD m * c] → a ≡ b [ZMOD m]
have simp : m * c ∣ (b - a) * c → m ∣ b - a
Tactic: simp only [modEq_iff_dvd, ← Int.sub_mul]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ n ∣ a ↔ n ∣ b
have simp : a ≡ 0 [ZMOD n] ↔ b ≡ 0 [ZMOD n]
Tactic: simp only [← modEq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
⊢ a + b ≡ b [ZMOD n] ↔ n ∣ a
have rw : b + a ≡ b [ZMOD n] ↔ n ∣ a
Tactic: rw [add_comm, add_modEq_left_iff]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
rw : b + a ≡ b [ZMOD n] ↔ n ∣ a
⊢ a + b ≡ b [ZMOD n] ↔ n ∣ a
have rw₁ : n ∣ a ↔ n ∣ a
Tactic: rw [add_comm, add_modEq_left_iff]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
⊢ a ≡ a + b [ZMOD n] ↔ n ∣ b
have rw : a + b ≡ a [ZMOD n] ↔ n ∣ b
Tactic: rw [modEq_comm, add_modEq_left_iff]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
rw : a + b ≡ a [ZMOD n] ↔ n ∣ b
⊢ a ≡ a + b [ZMOD n] ↔ n ∣ b
have rw₁ : n ∣ b ↔ n ∣ b
Tactic: rw [modEq_comm, add_modEq_left_iff]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
⊢ b ≡ a + b [ZMOD n] ↔ n ∣ a
have rw : a + b ≡ b [ZMOD n] ↔ n ∣ a
Tactic: rw [modEq_comm, add_modEq_right_iff]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
rw : a + b ≡ b [ZMOD n] ↔ n ∣ a
⊢ b ≡ a + b [ZMOD n] ↔ n ∣ a
have rw₁ : n ∣ a ↔ n ∣ a
Tactic: rw [modEq_comm, add_modEq_right_iff]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
⊢ n + a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
have rw : a + n ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
Tactic: rw [add_comm, add_modulus_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
rw : a + n ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
⊢ n + a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
have rw₁ : a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
Tactic: rw [add_comm, add_modulus_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b c : ℤ
⊢ b * n + a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
have rw : a + b * n ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
Tactic: rw [add_comm, add_mul_modulus_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b c : ℤ
rw : a + b * n ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
⊢ b * n + a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
have rw₁ : a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
Tactic: rw [add_comm, add_mul_modulus_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b c : ℤ
⊢ a ≡ b * n + c [ZMOD n] ↔ a ≡ c [ZMOD n]
have rw : a ≡ c + b * n [ZMOD n] ↔ a ≡ c [ZMOD n]
Tactic: rw [add_comm, modEq_add_mul_modulus_iff]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b c : ℤ
rw : a ≡ c + b * n [ZMOD n] ↔ a ≡ c [ZMOD n]
⊢ a ≡ b * n + c [ZMOD n] ↔ a ≡ c [ZMOD n]
have rw₁ : a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
Tactic: rw [add_comm, modEq_add_mul_modulus_iff]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b c : ℤ
⊢ n * b + a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
have rw : a + n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
Tactic: rw [add_comm, add_modulus_mul_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b c : ℤ
rw : a + n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
⊢ n * b + a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
have rw₁ : a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
Tactic: rw [add_comm, add_modulus_mul_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b c : ℤ
⊢ a ≡ n * b + c [ZMOD n] ↔ a ≡ c [ZMOD n]
have rw : a ≡ c + n * b [ZMOD n] ↔ a ≡ c [ZMOD n]
Tactic: rw [add_comm, modEq_add_modulus_mul_iff]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b c : ℤ
rw : a ≡ c + n * b [ZMOD n] ↔ a ≡ c [ZMOD n]
⊢ a ≡ n * b + c [ZMOD n] ↔ a ≡ c [ZMOD n]
have rw₁ : a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
Tactic: rw [add_comm, modEq_add_modulus_mul_iff]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
⊢ a - n ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
have rw : a - n + n ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
Tactic: rw [← add_modulus_modEq_iff, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
rw : a - n + n ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
⊢ a - n ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
have rw₁ : a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
Tactic: rw [← add_modulus_modEq_iff, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b c : ℤ
⊢ a - n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
have rw : a - n * b + n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
Tactic: rw [← add_modulus_mul_modEq_iff, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b c : ℤ
rw : a - n * b + n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
rw₁ : ℤ
⊢ a - n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
have rw₂ : a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
Tactic: rw [← add_modulus_mul_modEq_iff, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
⊢ a ≡ b - n [ZMOD n] ↔ a ≡ b [ZMOD n]
have rw : a ≡ b - n + n [ZMOD n] ↔ a ≡ b [ZMOD n]
Tactic: rw [← modEq_add_modulus_iff, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
rw : a ≡ b - n + n [ZMOD n] ↔ a ≡ b [ZMOD n]
⊢ a ≡ b - n [ZMOD n] ↔ a ≡ b [ZMOD n]
have rw₁ : a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
Tactic: rw [← modEq_add_modulus_iff, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b c : ℤ
⊢ a ≡ b - n * c [ZMOD n] ↔ a ≡ b [ZMOD n]
have rw : a ≡ b - n * c + n * c [ZMOD n] ↔ a ≡ b [ZMOD n]
Tactic: rw [← modEq_add_modulus_mul_iff, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b c : ℤ
rw : a ≡ b - n * c + n * c [ZMOD n] ↔ a ≡ b [ZMOD n]
rw₁ : ℤ
⊢ a ≡ b - n * c [ZMOD n] ↔ a ≡ b [ZMOD n]
have rw₂ : a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
Tactic: rw [← modEq_add_modulus_mul_iff, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
a b : ℤ
⊢ a ≡ b [ZMOD 0] ↔ a = b
have rw : a % 0 = b % 0 ↔ a = b
Tactic: rw [ModEq, emod_zero, emod_zero]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
a b : ℤ
rw : a % 0 = b % 0 ↔ a = b
⊢ a ≡ b [ZMOD 0] ↔ a = b
have rw₁ : a = b % 0 ↔ a = b
Tactic: rw [ModEq, emod_zero, emod_zero]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
a b : ℤ
rw : a % 0 = b % 0 ↔ a = b
rw₁ : a = b % 0 ↔ a = b
⊢ a ≡ b [ZMOD 0] ↔ a = b
have rw₂ : a = b ↔ a = b
Tactic: rw [ModEq, emod_zero, emod_zero]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
⊢ a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n]
have h : a ≡ b [ZMOD (↑(m.lcm n) : ℤ)] ↔ a ≡ b [ZMOD m * n]
Tactic: convert! ← modEq_and_modEq_iff_modEq_lcm using 1
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
⊢ a ≡ b [ZMOD (↑(m.lcm n) : ℤ)] ↔ a ≡ b [ZMOD m * n]
have h : a ≡ b [ZMOD (↑(m.natAbs * n.natAbs) : ℤ)] ↔ a ≡ b [ZMOD m * n]
Tactic: rw [lcm_eq_mul_iff.mpr (.inr <| .inr hmn), ← natAbs_mul, modEq_natAbs]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
h : a ≡ b [ZMOD (↑(m.natAbs * n.natAbs) : ℤ)] ↔ a ≡ b [ZMOD m * n]
⊢ a ≡ b [ZMOD (↑(m.lcm n) : ℤ)] ↔ a ≡ b [ZMOD m * n]
have h₁ : a ≡ b [ZMOD (↑(m * n).natAbs : ℤ)] ↔ a ≡ b [ZMOD m * n]
Tactic: rw [lcm_eq_mul_iff.mpr (.inr <| .inr hmn), ← natAbs_mul, modEq_natAbs]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
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]
⊢ a ≡ b [ZMOD (↑(m.lcm n) : ℤ)] ↔ a ≡ b [ZMOD m * n]
have h₂ : a ≡ b [ZMOD m * n] ↔ a ≡ b [ZMOD m * n]
Tactic: rw [lcm_eq_mul_iff.mpr (.inr <| .inr hmn), ← natAbs_mul, modEq_natAbs]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
a b : ℕ
⊢ (↑a : ℤ) * a.gcdA b ≡ (↑(a.gcd b) : ℤ) [ZMOD (↑b : ℤ)]
have rw : (↑a : ℤ) * a.gcdA b + 0 ≡ (↑a : ℤ) * a.gcdA b + (↑b : ℤ) * a.gcdB b [ZMOD (↑b : ℤ)]
Tactic: rw [← add_zero ((a : ℤ) * _), Nat.gcd_eq_gcd_ab]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
a b : ℕ
hab : a.Coprime b
hgcd : a.gcd b = 1
⊢ (↑a : ℤ) * a.gcdA b + (↑b : ℤ) * a.gcdB b ≡ 1 [ZMOD (↑b : ℤ)]
have rw : (↑1 : ℤ) ≡ 1 [ZMOD (↑b : ℤ)]
Tactic: rw [← Nat.gcd_eq_gcd_ab, hgcd]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (hypothesis)
Goal:
a b : ℤ
hb : 0 < b
⊢ a % b < b
have this : a % b < |b|
Tactic: have : a % b < |b| := emod_lt_abs _ (ne_of_gt hb)
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
a b : ℤ
hb : 0 < b
this : a % b < |b|
⊢ a % b < b
have rwa : ∀ (this : a % b < b), a % b < b
Tactic: rwa [abs_of_pos hb] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ (↑z.natAbs : ℤ) < b ∧ (↑z.natAbs : ℤ) ≡ a [ZMOD b]
have left : (↑z.natAbs : ℤ) < b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
left : (↑z.natAbs : ℤ) < b
⊢ (↑z.natAbs : ℤ) < b ∧ (↑z.natAbs : ℤ) ≡ a [ZMOD b]
have right : (↑z.natAbs : ℤ) ≡ a [ZMOD b]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.NatPrime (goal)
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.natAbs * n.natAbs
have rw : p ^ (k + l + 1) ∣ (m * n).natAbs
Tactic: rw [← Int.natAbs_mul]
-- Lean 4 proof step from Mathlib.Data.Int.NatPrime (goal)
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
⊢ (↑(p ^ (k + 1)) : ℤ) ∣ m
have apply : Dvd.dvd (α := ℤ) (↑(p ^ (k + 1)) : ℤ) (↑m.natAbs : ℤ)
Tactic: apply Int.dvd_natAbs.1
-- Lean 4 proof step from Mathlib.Data.Int.NatPrime (goal)
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
⊢ (↑(p ^ (l + 1)) : ℤ) ∣ n
have apply : Dvd.dvd (α := ℤ) (↑(p ^ (l + 1)) : ℤ) (↑n.natAbs : ℤ)
Tactic: apply Int.dvd_natAbs.1
-- Lean 4 proof step from Mathlib.Data.Int.NatPrime (goal)
Goal:
p : ℕ
hp : Nat.Prime p
k : ℤ
h : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) k 2
⊢ p ∣ k.natAbs
have apply : p ∣ HPow.hPow (β := ℕ) k.natAbs 2
Tactic: apply @Nat.Prime.dvd_of_dvd_pow _ _ 2 hp
-- Lean 4 proof step from Mathlib.Data.Int.NatPrime (goal)
Goal:
p : ℕ
hp : Nat.Prime p
k : ℤ
h : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) k 2
⊢ p ∣ HPow.hPow (β := ℕ) k.natAbs 2
have rwa : p ∣ k.natAbs * k.natAbs
Tactic: rwa [sq, ← natAbs_mul, ← natCast_dvd, ← sq]
-- Lean 4 proof step from Mathlib.Data.Int.NatPrime (goal)
Goal:
p : ℕ
hp : Nat.Prime p
k : ℤ
h : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) k 2
rwa : p ∣ k.natAbs * k.natAbs
⊢ p ∣ HPow.hPow (β := ℕ) k.natAbs 2
have rwa₁ : p ∣ (k * k).natAbs
Tactic: rwa [sq, ← natAbs_mul, ← natCast_dvd, ← sq]
-- Lean 4 proof step from Mathlib.Data.Int.NatPrime (goal)
Goal:
p : ℕ
hp : Nat.Prime p
k : ℤ
h : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) k 2
rwa : p ∣ k.natAbs * k.natAbs
rwa₁ : p ∣ (k * k).natAbs
⊢ p ∣ HPow.hPow (β := ℕ) k.natAbs 2
have rwa₂ : (↑p : ℤ) ∣ k * k
Tactic: rwa [sq, ← natAbs_mul, ← natCast_dvd, ← sq]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Basic (goal)
Goal:
a b : ℤ
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have rw : (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∧ a ≠ 0 ∧ b ≠ 0 ↔ 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]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Basic (goal)
Goal:
a b : ℤ
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have rw : 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 ↔ ¬(0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b)
Tactic: rw [← not_iff_not, not_le, Int.mul_pos_iff]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Basic (goal)
Goal:
a b : ℤ
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
have rw : 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ ¬(0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b)
Tactic: rw [← not_iff_not, not_lt, Int.mul_nonneg_iff]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Lemmas (goal)
Goal:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a * a = b * b
have rw : a.natAbs = b.natAbs ↔ Eq (α := ℤ) (↑a.natAbs : ℤ) (↑b.natAbs : ℤ)
Tactic: rw [← abs_eq_iff_mul_self_eq, abs_eq_natAbs, abs_eq_natAbs]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Lemmas (goal)
Goal:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a * a < b * b
have rw : a.natAbs < b.natAbs ↔ LT.lt (α := ℤ) (↑a.natAbs : ℤ) (↑b.natAbs : ℤ)
Tactic: rw [← abs_lt_iff_mul_self_lt, abs_eq_natAbs, abs_eq_natAbs]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Lemmas (goal)
Goal:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b
have rw : a.natAbs ≤ b.natAbs ↔ LE.le (α := ℤ) (↑a.natAbs : ℤ) (↑b.natAbs : ℤ)
Tactic: rw [← abs_le_iff_mul_self_le, abs_eq_natAbs, abs_eq_natAbs]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Lemmas (goal)
Goal:
a b : ℤ
hn : 0 ≤ b
⊢ |a| ≤ sqrt b ↔ a * a ≤ b
have rw : |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]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Lemmas (goal)
Goal:
a b : ℤ
hn : 0 ≤ b
rw : |a| ≤ sqrt b ↔ |a| * |a| ≤ b
⊢ |a| ≤ sqrt b ↔ a * a ≤ b
have rw₁ : |a| ≤ sqrt (↑b.toNat : ℤ) ↔ |a| * |a| ≤ (↑b.toNat : ℤ)
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]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Lemmas (goal)
Goal:
a b : ℤ
hn : 0 ≤ b
rw : |a| ≤ sqrt b ↔ |a| * |a| ≤ b
rw₁ : |a| ≤ sqrt (↑b.toNat : ℤ) ↔ |a| * |a| ≤ (↑b.toNat : ℤ)
⊢ |a| ≤ sqrt b ↔ a * a ≤ b
have rw₂ : (↑|a|.toNat : ℤ) ≤ sqrt (↑b.toNat : ℤ) ↔ HMul.hMul (α := ℤ) (↑|a|.toNat : ℤ) (↑|a|.toNat : ℤ) ≤ (↑b.toNat : ℤ)
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]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Lemmas (goal)
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 : ℤ)
⊢ |a| ≤ sqrt b ↔ a * a ≤ b
have rw₃ : LE.le (α := ℤ) (↑|a|.toNat : ℤ) (↑b.toNat.sqrt : ℤ) ↔
  HMul.hMul (α := ℤ) (↑|a|.toNat : ℤ) (↑|a|.toNat : ℤ) ≤ (↑b.toNat : ℤ)
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]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Lemmas (goal)
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 : ℤ)
⊢ |a| ≤ sqrt b ↔ a * a ≤ b
have rw₄ : LE.le (α := ℤ) (↑|a|.toNat : ℤ) (↑b.toNat.sqrt : ℤ) ↔ LE.le (α := ℤ) (↑(|a|.toNat * |a|.toNat) : ℤ) (↑b.toNat : ℤ)
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]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Lemmas (goal)
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 : ℤ)
⊢ |a| ≤ sqrt b ↔ a * a ≤ b
have rw₅ : |a|.toNat ≤ b.toNat.sqrt ↔ LE.le (α := ℤ) (↑(|a|.toNat * |a|.toNat) : ℤ) (↑b.toNat : ℤ)
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]
-- Lean 4 proof step from Mathlib.Data.Int.Order.Lemmas (goal)
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 : ℤ)
⊢ |a| ≤ sqrt b ↔ a * a ≤ b
have rw₆ : |a|.toNat ≤ b.toNat.sqrt ↔ |a|.toNat * |a|.toNat ≤ b.toNat
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]