awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b m : ℕ
h : a ≡ b [MOD n]
zero : HPow.hPow (β := ℕ) a 0 ≡ HPow.hPow (β := ℕ) b 0 [MOD n]
⊢ a ^ m ≡ b ^ m [MOD n]
have succ : ∀ (d : ℕ) (hd : a ^ d ≡ b ^ d [MOD n]), a ^ (d + 1) ≡ b ^ (d + 1) [MOD n]
Tactic: induction m with
  | zero => rfl
  | succ d hd =>
    rw [Nat.pow_succ, Nat.pow_succ]
    exact hd.mul h
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : c ≡ d [MOD n]
⊢ a + c ≡ b + d [MOD n]
have rw : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)
Tactic: rw [modEq_iff_dvd, Int.natCast_add, Int.natCast_add, add_sub_add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : a + c ≡ b + d [MOD n]
⊢ c ≡ d [MOD n]
have simp : ∀ (h₁ : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ))
  (h₂ : (↑n : ℤ) ∣ HAdd.hAdd (α := ℤ) (↑b : ℤ) (↑d : ℤ) - HAdd.hAdd (α := ℤ) (↑a : ℤ) (↑c : ℤ)),
  (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)
Tactic: simp only [modEq_iff_dvd, Int.natCast_add] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
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 (α := ℤ) (↑d : ℤ) (↑c : ℤ)
have h₃ : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)
Tactic: rw [add_sub_add_comm] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
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 (α := ℤ) (↑d : ℤ) (↑c : ℤ)
have h : HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ) =
  HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ) - HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: convert! Int.dvd_sub h₂ h₁ using 1
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c d : ℕ
h₁ : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
h₂ : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)
⊢ HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ) =
    HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ) - HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
have h : HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ) = HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)
Tactic: rw [add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
n a b c d : ℕ
h₁ : c ≡ d [MOD n]
h₂ : a + c ≡ b + d [MOD n]
⊢ a ≡ b [MOD n]
have h₃ : c + a ≡ d + b [MOD n]
Tactic: rw [add_comm a, add_comm b] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c d : ℕ
h : c ≤ a ↔ d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
⊢ a - c ≡ b - d [MOD n]
have inl : ∀ (hac : a < c), a - c ≡ b - d [MOD n]
Tactic: obtain hac | hca := lt_or_ge a c
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
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]
⊢ a - c ≡ b - d [MOD n]
have inr : ∀ (hca : c ≤ a), a - c ≡ b - d [MOD n]
Tactic: obtain hac | hca := lt_or_ge a c
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c d : ℕ
h : c ≤ a ↔ d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
hac : a < c
⊢ a - c ≡ b - d [MOD n]
have inl : 0 ≡ 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]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
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]
⊢ a - c ≡ b - d [MOD n]
have inl₁ : 0 ≡ 0 [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]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c d : ℕ
h : c ≤ a ↔ d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
hca : c ≤ a
⊢ a - c ≡ b - d [MOD n]
have inr : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) - HSub.hSub (α := ℤ) (↑d : ℤ) (↑c : ℤ)
Tactic: rw [modEq_iff_dvd, Int.natCast_sub hca, Int.natCast_sub <| h.1 hca, sub_sub_sub_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c m : ℕ
hc : c ≠ 0
⊢ c * a ≡ c * b [MOD c * m] → a ≡ b [MOD m]
have simp : HMul.hMul (α := ℤ) (↑c : ℤ) (↑m : ℤ) ∣ (↑c : ℤ) * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) →
  (↑m : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: simp only [modEq_iff_dvd, Int.natCast_mul, ← Int.mul_sub]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c m : ℕ
hc : c ≠ 0
⊢ a * c ≡ b * c [MOD m * c] → a ≡ b [MOD m]
have simp : HMul.hMul (α := ℤ) (↑m : ℤ) (↑c : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) * (↑c : ℤ) →
  (↑m : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: simp only [modEq_iff_dvd, Int.natCast_mul, ← Int.sub_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b m : ℕ
h : a ≡ b [MOD m * n]
⊢ a ≡ b [MOD n]
have rw : ∀ (h : (↑(m * n) : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)), (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: rw [modEq_iff_dvd] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m a b c : ℕ
h : a / c ≡ b / c [MOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
⊢ a ≡ b [MOD m]
have h₁ : m = c * (m / c)
Tactic: convert! h.mul_left' c
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m a b c : ℕ
h : a / c ≡ b / c [MOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
h₁ : m = c * (m / c)
⊢ a ≡ b [MOD m]
have h₂ : a = c * (a / c)
Tactic: convert! h.mul_left' c
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m a b c : ℕ
h : a / c ≡ b / c [MOD 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 [MOD m]
have h₃ : b = c * (b / c)
Tactic: convert! h.mul_left' c
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m a b c : ℕ
h : a / c ≡ b / c [MOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
⊢ m = c * (m / c)
have h₁ : m = m
Tactic: rwa [Nat.mul_div_cancel']
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m a b c : ℕ
h : a / c ≡ b / c [MOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
⊢ a = c * (a / c)
have h₁ : a = a
Tactic: rwa [Nat.mul_div_cancel']
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m a b c : ℕ
h : a / c ≡ b / c [MOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
⊢ b = c * (b / c)
have h₁ : b = b
Tactic: rwa [Nat.mul_div_cancel']
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
⊢ a + b ≡ b [MOD n] ↔ n ∣ a
have rw : b + a ≡ b [MOD n] ↔ n ∣ a
Tactic: rw [add_comm, add_modEq_left_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
rw : b + a ≡ b [MOD n] ↔ n ∣ a
⊢ a + b ≡ b [MOD n] ↔ n ∣ a
have rw₁ : n ∣ a ↔ n ∣ a
Tactic: rw [add_comm, add_modEq_left_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
⊢ a ≡ a + b [MOD n] ↔ n ∣ b
have rw : a + b ≡ a [MOD n] ↔ n ∣ b
Tactic: rw [ModEq.comm, add_modEq_left_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
rw : a + b ≡ a [MOD n] ↔ n ∣ b
⊢ a ≡ a + b [MOD n] ↔ n ∣ b
have rw₁ : n ∣ b ↔ n ∣ b
Tactic: rw [ModEq.comm, add_modEq_left_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
⊢ b ≡ a + b [MOD n] ↔ n ∣ a
have rw : a + b ≡ b [MOD n] ↔ n ∣ a
Tactic: rw [ModEq.comm, add_modEq_right_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
rw : a + b ≡ b [MOD n] ↔ n ∣ a
⊢ b ≡ a + b [MOD n] ↔ n ∣ a
have rw₁ : n ∣ a ↔ n ∣ a
Tactic: rw [ModEq.comm, add_modEq_right_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
⊢ n + a ≡ b [MOD n] ↔ a ≡ b [MOD n]
have rw : a + n ≡ b [MOD n] ↔ a ≡ b [MOD n]
Tactic: rw [add_comm, add_modulus_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
rw : a + n ≡ b [MOD n] ↔ a ≡ b [MOD n]
⊢ n + a ≡ b [MOD n] ↔ a ≡ b [MOD n]
have rw₁ : a ≡ b [MOD n] ↔ a ≡ b [MOD n]
Tactic: rw [add_comm, add_modulus_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c : ℕ
⊢ b * n + a ≡ c [MOD n] ↔ a ≡ c [MOD n]
have rw : a + b * n ≡ c [MOD n] ↔ a ≡ c [MOD n]
Tactic: rw [add_comm, add_mul_modulus_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c : ℕ
rw : a + b * n ≡ c [MOD n] ↔ a ≡ c [MOD n]
⊢ b * n + a ≡ c [MOD n] ↔ a ≡ c [MOD n]
have rw₁ : a ≡ c [MOD n] ↔ a ≡ c [MOD n]
Tactic: rw [add_comm, add_mul_modulus_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c : ℕ
⊢ a ≡ b * n + c [MOD n] ↔ a ≡ c [MOD n]
have rw : a ≡ c + b * n [MOD n] ↔ a ≡ c [MOD n]
Tactic: rw [add_comm, modEq_add_mul_modulus_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c : ℕ
rw : a ≡ c + b * n [MOD n] ↔ a ≡ c [MOD n]
⊢ a ≡ b * n + c [MOD n] ↔ a ≡ c [MOD n]
have rw₁ : a ≡ c [MOD n] ↔ a ≡ c [MOD n]
Tactic: rw [add_comm, modEq_add_mul_modulus_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c : ℕ
⊢ n * b + a ≡ c [MOD n] ↔ a ≡ c [MOD n]
have rw : a + n * b ≡ c [MOD n] ↔ a ≡ c [MOD n]
Tactic: rw [add_comm, add_modulus_mul_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c : ℕ
rw : a + n * b ≡ c [MOD n] ↔ a ≡ c [MOD n]
⊢ n * b + a ≡ c [MOD n] ↔ a ≡ c [MOD n]
have rw₁ : a ≡ c [MOD n] ↔ a ≡ c [MOD n]
Tactic: rw [add_comm, add_modulus_mul_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c : ℕ
⊢ a ≡ n * b + c [MOD n] ↔ a ≡ c [MOD n]
have rw : a ≡ c + n * b [MOD n] ↔ a ≡ c [MOD n]
Tactic: rw [add_comm, modEq_add_modulus_mul_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c : ℕ
rw : a ≡ c + n * b [MOD n] ↔ a ≡ c [MOD n]
⊢ a ≡ n * b + c [MOD n] ↔ a ≡ c [MOD n]
have rw₁ : a ≡ c [MOD n] ↔ a ≡ c [MOD n]
Tactic: rw [add_comm, modEq_add_modulus_mul_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
h : n ≤ a
⊢ a - n ≡ b [MOD n] ↔ a ≡ b [MOD n]
have rw : a - n + n ≡ b [MOD n] ↔ a ≡ b [MOD n]
Tactic: rw [← add_modulus_modEq_iff, Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
h : n ≤ a
rw : a - n + n ≡ b [MOD n] ↔ a ≡ b [MOD n]
⊢ a - n ≡ b [MOD n] ↔ a ≡ b [MOD n]
have rw₁ : a ≡ b [MOD n] ↔ a ≡ b [MOD n]
Tactic: rw [← add_modulus_modEq_iff, Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
h : n ≤ b
⊢ a ≡ b - n [MOD n] ↔ a ≡ b [MOD n]
have rw : a ≡ b - n + n [MOD n] ↔ a ≡ b [MOD n]
Tactic: rw [← modEq_add_modulus_iff, Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
h : n ≤ b
rw : a ≡ b - n + n [MOD n] ↔ a ≡ b [MOD n]
⊢ a ≡ b - n [MOD n] ↔ a ≡ b [MOD n]
have rw₁ : a ≡ b [MOD n] ↔ a ≡ b [MOD n]
Tactic: rw [← modEq_add_modulus_iff, Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b : ℕ
h : b ≤ a
⊢ (↑(a - b) : ℤ) ∣ HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)
have rw : HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ) ∣ HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)
Tactic: rw [Int.ofNat_sub h]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b : ℕ
⊢ a ≡ b [MOD 0] ↔ a = b
have rw : a % 0 = b % 0 ↔ a = b
Tactic: rw [ModEq, mod_zero, mod_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b : ℕ
rw : a % 0 = b % 0 ↔ a = b
⊢ a ≡ b [MOD 0] ↔ a = b
have rw₁ : a = b % 0 ↔ a = b
Tactic: rw [ModEq, mod_zero, mod_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b : ℕ
rw : a % 0 = b % 0 ↔ a = b
rw₁ : a = b % 0 ↔ a = b
⊢ a ≡ b [MOD 0] ↔ a = b
have rw₂ : a = b ↔ a = b
Tactic: rw [ModEq, mod_zero, mod_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
h : a ≤ b
⊢ a ≡ b [MOD n] ↔ ∃ (t : ℕ), b = a + n * t
have rw : (∃ (c : ℕ), b - a = n * c) ↔ ∃ (t : ℕ), b = a + n * t
Tactic: rw [modEq_iff_dvd' h, dvd_def]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m a b d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
⊢ d ∣ a ↔ d ∣ b
have simp : a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]
Tactic: simp only [← modEq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
m a b d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
⊢ a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]
have h₁ : a ≡ b [MOD d]
Tactic: replace h := h.of_dvd hdm
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
m a b : ℕ
h : a ≡ b [MOD m]
⊢ a.gcd m = b.gcd m
have h1 : a.gcd m ∣ m
Tactic: have h1 := gcd_dvd_right a m
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
m a b : ℕ
h : a ≡ b [MOD m]
h1 : a.gcd m ∣ m
⊢ a.gcd m = b.gcd m
have h2 : b.gcd m ∣ m
Tactic: have h2 := gcd_dvd_right b m
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m a b : ℕ
h : a ≡ b [MOD m]
h2 : |HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)| < (↑m : ℤ)
⊢ a = b
have x : Int.ofNat a = Int.ofNat b
Tactic: apply Int.ofNat.inj
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m a b : ℕ
h : a ≡ b [MOD m]
h2 : |HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)| < (↑m : ℤ)
⊢ Int.ofNat a = Int.ofNat b
have x : Int.ofNat b - Int.ofNat a = 0
Tactic: rw [eq_comm, ← sub_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
⊢ a ≡ b [MOD m / m.gcd c]
have hmd : m.gcd c ∣ m
Tactic: have hmd := gcd_dvd_left m c
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
⊢ a ≡ b [MOD m / m.gcd c]
have hcd : m.gcd c ∣ c
Tactic: have hcd := gcd_dvd_right m c
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ a ≡ b [MOD m / m.gcd c]
have rw : (↑(m / m.gcd c) : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: rw [modEq_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ (↑(m / m.gcd c) : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
have refine_1 : HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑d : ℤ) ∣ HDiv.hDiv (α := ℤ) (↑c : ℤ) (↑d : ℤ) * HSub.hSub (α := ℤ) (↑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.Nat.ModEq (goal)
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
refine_1 :
  HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑d : ℤ) ∣ HDiv.hDiv (α := ℤ) (↑c : ℤ) (↑d : ℤ) * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ (↑(m / m.gcd c) : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
have refine_2 : (HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑d : ℤ)).gcd (HDiv.hDiv (α := ℤ) (↑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.Nat.ModEq (goal)
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑d : ℤ) ∣ HDiv.hDiv (α := ℤ) (↑c : ℤ) (↑d : ℤ) * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
have refine_1 : HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑d : ℤ) ∣ (↑c : ℤ) * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) / (↑(m.gcd c) : ℤ)
Tactic: rw [mul_comm, ← Int.mul_ediv_assoc (b - a) (Int.natCast_dvd_natCast.mpr hcd), mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑d : ℤ) ∣ (↑c : ℤ) * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) / (↑(m.gcd c) : ℤ)
have refine_1 : (↑m : ℤ) ∣ (↑c : ℤ) * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: apply Int.ediv_dvd_ediv (Int.natCast_dvd_natCast.mpr hmd)
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ (↑m : ℤ) ∣ (↑c : ℤ) * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
have refine_1 : (↑m : ℤ) ∣ HMul.hMul (α := ℤ) (↑c : ℤ) (↑b : ℤ) - HMul.hMul (α := ℤ) (↑c : ℤ) (↑a : ℤ)
Tactic: rw [Int.mul_sub]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m a b c : ℕ
hm : 0 < m
h : a * c ≡ b * c [MOD m]
⊢ a ≡ b [MOD m / m.gcd c]
have apply : c * a ≡ c * b [MOD m]
Tactic: apply cancel_left_div_gcd hm
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m a b c : ℕ
hmc : m.gcd c = 1
h : c * a ≡ c * b [MOD m]
⊢ a ≡ b [MOD m]
have inl : ∀ (hmc : gcd 0 c = 1) (h : c * a ≡ c * b [MOD 0]), a ≡ b [MOD 0]
Tactic: rcases m.eq_zero_or_pos with (rfl | hm)
Cleared hypotheses: m, hmc, h
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m a b c : ℕ
hmc : m.gcd c = 1
h : c * a ≡ c * b [MOD m]
inl : ∀ (hmc : gcd 0 c = 1) (h : c * a ≡ c * b [MOD 0]), a ≡ b [MOD 0]
⊢ a ≡ b [MOD m]
have inr : ∀ (hm : m > 0), a ≡ b [MOD m]
Tactic: rcases m.eq_zero_or_pos with (rfl | hm)
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
a b c : ℕ
hmc : gcd 0 c = 1
h : c * a ≡ c * b [MOD 0]
⊢ a ≡ b [MOD 0]
have hmc₁ : c = 1
Tactic: simp only [gcd_zero_left] at hmc
Cleared hypotheses: hmc
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
a b c : ℕ
h : c * a ≡ c * b [MOD 0]
hmc : c = 1
⊢ a ≡ b [MOD 0]
have h₁ : a = b
Tactic: simp only [hmc, one_mul, modEq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
hmc : c = 1
h : a = b
⊢ a ≡ b [MOD 0]
have inl : a ≡ a [MOD 0]
Tactic: subst h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n = 0
⊢ a ≡ a [MOD n] ∧ a ≡ b [MOD m]
have h₁ : a ≡ b [MOD m]
Tactic: rw [hn, gcd_zero_left] at h
Cleared hypotheses: h, hn
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD m]
hn : n = 0
⊢ a ≡ a [MOD n] ∧ a ≡ b [MOD m]
have left : a ≡ a [MOD n]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ a [MOD n] ∧ b ≡ b [MOD m]
have h₁ : a ≡ b [MOD n]
Tactic: rw [hm, gcd_zero_right] at h
Cleared hypotheses: h, hn, hm
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ a [MOD n] ∧ b ≡ b [MOD m]
have left : b ≡ a [MOD n]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n]
hn : ¬n = 0
hm : m = 0
left : b ≡ a [MOD n]
⊢ b ≡ a [MOD n] ∧ b ≡ b [MOD m]
have right : b ≡ b [MOD m]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ (match (motive := ℤ × ℤ → ℕ) n.xgcd m with
      | (c, d) => (((↑n : ℤ) * c * (↑b : ℤ) + (↑m : ℤ) * d * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)).toNat) ≡
      a [MOD n] ∧
    (match (motive := ℤ × ℤ → ℕ) n.xgcd m with
      | (c, d) => (((↑n : ℤ) * c * (↑b : ℤ) + (↑m : ℤ) * d * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)).toNat) ≡
      b [MOD m]
have rw : (match (motive := ℤ × ℤ → ℕ) (n.gcdA m, n.gcdB m) with
    | (c, d) => (((↑n : ℤ) * c * (↑b : ℤ) + (↑m : ℤ) * d * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)).toNat) ≡
    a [MOD n] ∧
  (match (motive := ℤ × ℤ → ℕ) (n.gcdA m, n.gcdB m) with
    | (c, d) => (((↑n : ℤ) * c * (↑b : ℤ) + (↑m : ℤ) * d * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)).toNat) ≡
    b [MOD m]
Tactic: rw [xgcd_val]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ (((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)).toNat ≡
      a [MOD n] ∧
    (((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)).toNat ≡
      b [MOD m]
have rw : (↑n : ℤ) ∣
    (↑a : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ) ∧
  (↑m : ℤ) ∣
    (↑b : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)
Tactic: rw [modEq_iff_dvd, modEq_iff_dvd,
          Int.toNat_of_nonneg (Int.emod_nonneg _ (Int.natCast_ne_zero.2 (lcm_ne_zero hn hm)))]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ Ne (α := ℤ) (↑(n.gcd m) : ℤ) 0
have norm_cast : ¬n.gcd m = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ ¬n.gcd m = 0
have rw : n = 0 → ¬m = 0
Tactic: rw [Nat.gcd_eq_zero_iff, not_and]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ (↑n : ℤ) ∣
      (↑a : ℤ) -
        ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ) ∧
    (↑m : ℤ) ∣
      (↑b : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)
have hnonzero : Ne (α := ℤ) (↑(n.gcd m) : ℤ) 0
Tactic: have hnonzero : (gcd n m : ℤ) ≠ 0 := by
          norm_cast
          rw [Nat.gcd_eq_zero_iff, not_and]
          exact fun _ => hm
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : Ne (α := ℤ) (↑(n.gcd m) : ℤ) 0
⊢ (↑n : ℤ) ∣
      (↑a : ℤ) -
        ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ) ∧
    (↑m : ℤ) ∣
      (↑b : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)
have hcoedvd : ∀ (t : ℤ), (↑(n.gcd m) : ℤ) ∣ t * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: have hcoedvd : ∀ t, (gcd n m : ℤ) ∣ t * (b - a) := fun t => h.dvd.mul_left _
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : Ne (α := ℤ) (↑(n.gcd m) : ℤ) 0
hcoedvd : ∀ (t : ℤ), (↑(n.gcd m) : ℤ) ∣ t * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ (↑n : ℤ) ∣
      (↑a : ℤ) -
        ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ) ∧
    (↑m : ℤ) ∣
      (↑b : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)
have this : (↑(n.gcd m) : ℤ) = (↑n : ℤ) * n.gcdA m + (↑m : ℤ) * n.gcdB m
Tactic: have := gcd_eq_gcd_ab n m
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : Ne (α := ℤ) (↑(n.gcd m) : ℤ) 0
hcoedvd : ∀ (t : ℤ), (↑(n.gcd m) : ℤ) ∣ t * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
this : (↑(n.gcd m) : ℤ) = (↑n : ℤ) * n.gcdA m + (↑m : ℤ) * n.gcdB m
⊢ (↑n : ℤ) ∣
      (↑a : ℤ) -
        ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ) ∧
    (↑m : ℤ) ∣
      (↑b : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)
have left : (↑n : ℤ) ∣
  (↑a : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : Ne (α := ℤ) (↑(n.gcd m) : ℤ) 0
hcoedvd : ∀ (t : ℤ), (↑(n.gcd m) : ℤ) ∣ t * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
this : (↑(n.gcd m) : ℤ) = (↑n : ℤ) * n.gcdA m + (↑m : ℤ) * n.gcdB m
left :
  (↑n : ℤ) ∣
    (↑a : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)
⊢ (↑n : ℤ) ∣
      (↑a : ℤ) -
        ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ) ∧
    (↑m : ℤ) ∣
      (↑b : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)
have right : (↑m : ℤ) ∣
  (↑b : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)
Tactic: constructor