awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) : ℤ)
have left : (↑n : ℤ) ∣
  (↑a : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) +
    (↑(n.lcm m) : ℤ) *
      (((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) / (↑(n.lcm m) : ℤ))
Tactic: rw [Int.emod_def, ← sub_add]
-- 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
⊢ (↑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) : ℤ) *
      (((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) / (↑(n.lcm m) : ℤ))
Tactic: rw [Int.emod_def, ← sub_add]
-- 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) : ℤ) *
        (((↑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) : ℤ)
Tactic: refine Int.dvd_add ?_ (dvd_mul_of_dvd_left ?_ _)
-- 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 : ℤ) ∣
    (↑a : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) +
      (↑(n.lcm m) : ℤ) *
        (((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) / (↑(n.lcm m) : ℤ))
have left₁ : Dvd.dvd (α := ℤ) (↑n : ℤ) (↑(n.lcm m) : ℤ)
Tactic: refine Int.dvd_add ?_ (dvd_mul_of_dvd_left ?_ _)
-- 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
⊢ (↑m : ℤ) ∣
    (↑b : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) +
      (↑(n.lcm m) : ℤ) *
        (((↑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) : ℤ)
Tactic: refine Int.dvd_add ?_ (dvd_mul_of_dvd_left ?_ _)
-- 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
right : (↑m : ℤ) ∣ (↑b : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ)
⊢ (↑m : ℤ) ∣
    (↑b : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) +
      (↑(n.lcm m) : ℤ) *
        (((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) / (↑(n.lcm m) : ℤ))
have right₁ : Dvd.dvd (α := ℤ) (↑m : ℤ) (↑(n.lcm m) : ℤ)
Tactic: refine Int.dvd_add ?_ (dvd_mul_of_dvd_left ?_ _)
-- 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
⊢ Dvd.dvd (α := ℤ) (↑n : ℤ) (↑(n.lcm m) : ℤ)
have left : n ∣ n.lcm m
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
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
⊢ Dvd.dvd (α := ℤ) (↑n : ℤ) (↑(n.lcm m) : ℤ)
have left : n ∣ n.lcm m
Tactic: try 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
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
⊢ Dvd.dvd (α := ℤ) (↑m : ℤ) (↑(n.lcm m) : ℤ)
have right : m ∣ n.lcm m
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
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
⊢ Dvd.dvd (α := ℤ) (↑m : ℤ) (↑(n.lcm m) : ℤ)
have right : m ∣ n.lcm m
Tactic: try norm_cast
-- 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 : ℤ)
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) : ℤ)
have this₁ : (↑(n.gcd m) : ℤ) - (↑n : ℤ) * n.gcdA m = (↑m : ℤ) * n.gcdB m
Tactic: rw [← sub_eq_iff_eq_add'] at this
Cleared hypotheses: this
-- 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) : ℤ)
have left : (↑n : ℤ) ∣ (↑n : ℤ) * (n.gcdA m * (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) / (↑(n.gcd m) : ℤ)))
Tactic: rw [← this, Int.sub_mul, ← add_sub_assoc, add_comm, add_sub_assoc, ← Int.mul_sub,
            Int.add_ediv_of_dvd_left, Int.mul_ediv_cancel_left _ hnonzero,
            Int.mul_ediv_assoc _ h.dvd, ← sub_sub, sub_self, zero_sub, Int.dvd_neg, mul_assoc]
-- 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 : ℤ) ∣ (↑n : ℤ) * (n.gcdA m * (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) / (↑(n.gcd m) : ℤ)))
⊢ (↑n : ℤ) ∣ (↑a : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ)
have left₁ : (↑(n.gcd m) : ℤ) ∣ HMul.hMul (α := ℤ) (↑(n.gcd m) : ℤ) (↑a : ℤ)
Tactic: rw [← this, Int.sub_mul, ← add_sub_assoc, add_comm, add_sub_assoc, ← Int.mul_sub,
            Int.add_ediv_of_dvd_left, Int.mul_ediv_cancel_left _ hnonzero,
            Int.mul_ediv_assoc _ h.dvd, ← sub_sub, sub_self, zero_sub, Int.dvd_neg, mul_assoc]
-- 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.gcd m) : ℤ) ∣ HMul.hMul (α := ℤ) (↑(n.gcd m) : ℤ) (↑a : ℤ)
have left : n.gcd m ∣ n.gcd m * a
Tactic: norm_cast
-- 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 : ℤ)
this : (↑(n.gcd m) : ℤ) = (↑n : ℤ) * n.gcdA m + (↑m : ℤ) * n.gcdB m
⊢ (↑m : ℤ) ∣ (↑b : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ)
have this₁ : (↑(n.gcd m) : ℤ) - (↑m : ℤ) * n.gcdB m = (↑n : ℤ) * n.gcdA m
Tactic: rw [← sub_eq_iff_eq_add] at this
Cleared hypotheses: this
-- 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) : ℤ) - (↑m : ℤ) * n.gcdB m = (↑n : ℤ) * n.gcdA m
⊢ (↑m : ℤ) ∣ (↑b : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ)
have right : (↑m : ℤ) ∣ (↑m : ℤ) * (n.gcdB m * (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) / (↑(n.gcd m) : ℤ)))
Tactic: rw [← this, Int.sub_mul, sub_add, ← Int.mul_sub, Int.sub_ediv_of_dvd,
            Int.mul_ediv_cancel_left _ hnonzero, Int.mul_ediv_assoc _ h.dvd, ← sub_add, sub_self,
            zero_add, mul_assoc]
-- 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) : ℤ) - (↑m : ℤ) * n.gcdB m = (↑n : ℤ) * n.gcdA m
right : (↑m : ℤ) ∣ (↑m : ℤ) * (n.gcdB m * (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) / (↑(n.gcd m) : ℤ)))
⊢ (↑m : ℤ) ∣ (↑b : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ)
have right₁ : (↑(n.gcd m) : ℤ) ∣ (↑m : ℤ) * n.gcdB m * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: rw [← this, Int.sub_mul, sub_add, ← Int.mul_sub, Int.sub_ediv_of_dvd,
            Int.mul_ediv_cancel_left _ hnonzero, Int.mul_ediv_assoc _ h.dvd, ← sub_add, sub_self,
            zero_add, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ (↑(chineseRemainder' h) : ℕ) < n.lcm m
have dsimp : (↑(if hn : n = 0 then Subtype.mk (p := fun (k : ℕ) ↦ k ≡ a [MOD n] ∧ k ≡ b [MOD m]) a sorry
      else
        if hm : m = 0 then Subtype.mk (p := fun (k : ℕ) ↦ k ≡ a [MOD n] ∧ k ≡ b [MOD m]) b sorry
        else
          Subtype.mk (p := fun (k : ℕ) ↦ k ≡ a [MOD n] ∧ k ≡ b [MOD m])
            (((↑n : ℤ) * (n.xgcd m).1 * (↑b : ℤ) + (↑m : ℤ) * (n.xgcd m).2 * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) %
                (↑(n.lcm m) : ℤ)).toNat
            sorry) :
    ℕ) <
  n.lcm m
Tactic: dsimp only [chineseRemainder']
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ (↑(if hn : n = 0 then Subtype.mk (p := fun (k : ℕ) ↦ k ≡ a [MOD n] ∧ k ≡ b [MOD m]) a ⋯
        else
          if hm : m = 0 then Subtype.mk (p := fun (k : ℕ) ↦ k ≡ a [MOD n] ∧ k ≡ b [MOD m]) b ⋯
          else
            Subtype.mk (p := fun (k : ℕ) ↦ k ≡ a [MOD n] ∧ k ≡ b [MOD m])
              (((↑n : ℤ) * (n.xgcd m).1 * (↑b : ℤ) + (↑m : ℤ) * (n.xgcd m).2 * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) %
                  (↑(n.lcm m) : ℤ)).toNat
              ⋯) :
      ℕ) <
    n.lcm m
have rw : (((↑n : ℤ) * (n.gcdA m, n.gcdB m).1 * (↑b : ℤ) + (↑m : ℤ) * (n.gcdA m, n.gcdB m).2 * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) %
      (↑(Int.toNat (↑(n.lcm m) : ℤ)) : ℤ)).toNat <
  Int.toNat (↑(n.lcm m) : ℤ)
Tactic: rw [dif_neg hn, dif_neg hm, Subtype.coe_mk, xgcd_val, ← Int.toNat_natCast (lcm n m)]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ (((↑n : ℤ) * (n.gcdA m, n.gcdB m).1 * (↑b : ℤ) + (↑m : ℤ) * (n.gcdA m, n.gcdB m).2 * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) %
        (↑(Int.toNat (↑(n.lcm m) : ℤ)) : ℤ)).toNat <
    Int.toNat (↑(n.lcm m) : ℤ)
have lcm_pos : LT.lt (α := ℤ) 0 (↑(n.lcm m) : ℤ)
Tactic: have lcm_pos := Int.natCast_pos.mpr (Nat.pos_of_ne_zero (lcm_ne_zero hn hm))
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ≡ b [MOD m] ∧ a ≡ b [MOD n]
⊢ a ≡ b [MOD m * n]
have h₁ : m ∣ (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs ∧ n ∣ (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs
Tactic: rw [Nat.modEq_iff_dvd, Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.natCast_dvd_natCast,
      ← Int.dvd_natAbs, Int.natCast_dvd_natCast] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs ∧ n ∣ (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs
⊢ a ≡ b [MOD m * n]
have rw : m * n ∣ (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs
Tactic: rw [Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
b a n : ℕ
h : a * b ≡ 1 [MOD n]
⊢ a.Coprime n
have obtain : ∀ (g : ℕ) (hh : n = a.gcd n * g), a.Coprime n
Tactic: obtain ⟨g, hh⟩ := Nat.gcd_dvd_right a n
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
⊢ a.Coprime n
have rw : 1 ≡ 0 [MOD a.gcd n]
Tactic: rw [Nat.coprime_iff_gcd_eq_one, ← Nat.dvd_one, ← Nat.modEq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
⊢ 0 * b = 0
have rw : Eq (α := ℕ) 0 0
Tactic: rw [zero_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
⊢ 1 ≡ 0 [MOD a.gcd n]
have a₁ : 0 * b = 0
Tactic: calc
    1 ≡ a * b [MOD a.gcd n] := (hh ▸ h).symm.of_mul_right g
    _ ≡ 0 * b [MOD a.gcd n] := (Nat.modEq_zero_iff_dvd.mpr (Nat.gcd_dvd_left _ _)).mul_right b
    _ = 0 := by rw [zero_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
⊢ ((a + b) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c
have rw : ((a % c + b % c) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
⊢ ((a % c + b % c) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c
have pos : ∀ (h : c ≤ a % c + b % c), (a % c + b % c) % c + c = a % c + b % c
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
pos : ∀ (h : c ≤ a % c + b % c), (a % c + b % c) % c + c = a % c + b % c
⊢ ((a % c + b % c) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c
have neg : ∀ (h : ¬c ≤ a % c + b % c), (a % c + b % c) % c + 0 = a % c + b % c
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
⊢ a % c + b % c < c * 2
have rw : a % c + b % c < c + c
Tactic: rw [mul_two]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
⊢ (a % c + b % c) % c + c = a % c + b % c
have h2 : (a % c + b % c) / c < 2
Tactic: have h2 : (a % c + b % c) / c < 2 :=
        Nat.div_lt_of_lt_mul
          (by
            rw [mul_two]
            exact
              add_lt_add (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0))
                (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0)))
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
h2 : (a % c + b % c) / c < 2
⊢ (a % c + b % c) % c + c = a % c + b % c
have h0 : 0 < (a % c + b % c) / c
Tactic: have h0 : 0 < (a % c + b % c) / c := Nat.div_pos h (Nat.pos_of_ne_zero hc0)
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
h2 : (a % c + b % c) / c < 2
h0 : 0 < (a % c + b % c) / c
⊢ (a % c + b % c) % c + c = a % c + b % c
have pos : (a % c + b % c) % c + c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)
Tactic: rw [← @add_right_cancel_iff _ _ _ (c * ((a % c + b % c) / c)), add_comm _ c, add_assoc,
        mod_add_div, le_antisymm (le_of_lt_succ h2) h0, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
h2 : (a % c + b % c) / c < 2
h0 : 0 < (a % c + b % c) / c
pos : (a % c + b % c) % c + c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)
⊢ (a % c + b % c) % c + c = a % c + b % c
have pos₁ : c + (a % c + b % c) % c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)
Tactic: rw [← @add_right_cancel_iff _ _ _ (c * ((a % c + b % c) / c)), add_comm _ c, add_assoc,
        mod_add_div, le_antisymm (le_of_lt_succ h2) h0, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
h2 : (a % c + b % c) / c < 2
h0 : 0 < (a % c + b % c) / c
pos : (a % c + b % c) % c + c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)
pos₁ : c + (a % c + b % c) % c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)
⊢ (a % c + b % c) % c + c = a % c + b % c
have pos₂ : c + ((a % c + b % c) % c + c * ((a % c + b % c) / c)) = a % c + b % c + c * ((a % c + b % c) / c)
Tactic: rw [← @add_right_cancel_iff _ _ _ (c * ((a % c + b % c) / c)), add_comm _ c, add_assoc,
        mod_add_div, le_antisymm (le_of_lt_succ h2) h0, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
h2 : (a % c + b % c) / c < 2
h0 : 0 < (a % c + b % c) / c
pos : (a % c + b % c) % c + c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)
pos₁ : c + (a % c + b % c) % c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)
pos₂ : c + ((a % c + b % c) % c + c * ((a % c + b % c) / c)) = a % c + b % c + c * ((a % c + b % c) / c)
⊢ (a % c + b % c) % c + c = a % c + b % c
have pos₃ : c + (a % c + b % c) = a % c + b % c + c * ((a % c + b % c) / c)
Tactic: rw [← @add_right_cancel_iff _ _ _ (c * ((a % c + b % c) / c)), add_comm _ c, add_assoc,
        mod_add_div, le_antisymm (le_of_lt_succ h2) h0, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
h2 : (a % c + b % c) / c < 2
h0 : 0 < (a % c + b % c) / c
pos : (a % c + b % c) % c + c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)
pos₁ : c + (a % c + b % c) % c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)
pos₂ : c + ((a % c + b % c) % c + c * ((a % c + b % c) / c)) = a % c + b % c + c * ((a % c + b % c) / c)
pos₃ : c + (a % c + b % c) = a % c + b % c + c * ((a % c + b % c) / c)
⊢ (a % c + b % c) % c + c = a % c + b % c
have pos₄ : c + (a % c + b % c) = a % c + b % c + c * 1
Tactic: rw [← @add_right_cancel_iff _ _ _ (c * ((a % c + b % c) / c)), add_comm _ c, add_assoc,
        mod_add_div, le_antisymm (le_of_lt_succ h2) h0, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
h2 : (a % c + b % c) / c < 2
h0 : 0 < (a % c + b % c) / c
pos : (a % c + b % c) % c + c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)
pos₁ : c + (a % c + b % c) % c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)
pos₂ : c + ((a % c + b % c) % c + c * ((a % c + b % c) / c)) = a % c + b % c + c * ((a % c + b % c) / c)
pos₃ : c + (a % c + b % c) = a % c + b % c + c * ((a % c + b % c) / c)
pos₄ : c + (a % c + b % c) = a % c + b % c + c * 1
⊢ (a % c + b % c) % c + c = a % c + b % c
have pos₅ : c + (a % c + b % c) = a % c + b % c + c
Tactic: rw [← @add_right_cancel_iff _ _ _ (c * ((a % c + b % c) / c)), add_comm _ c, add_assoc,
        mod_add_div, le_antisymm (le_of_lt_succ h2) h0, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
h2 : (a % c + b % c) / c < 2
h0 : 0 < (a % c + b % c) / c
pos : (a % c + b % c) % c + c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)
pos₁ : c + (a % c + b % c) % c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)
pos₂ : c + ((a % c + b % c) % c + c * ((a % c + b % c) / c)) = a % c + b % c + c * ((a % c + b % c) / c)
pos₃ : c + (a % c + b % c) = a % c + b % c + c * ((a % c + b % c) / c)
pos₄ : c + (a % c + b % c) = a % c + b % c + c * 1
pos₅ : c + (a % c + b % c) = a % c + b % c + c
⊢ (a % c + b % c) % c + c = a % c + b % c
have pos₆ : a % c + b % c + c = a % c + b % c + c
Tactic: rw [← @add_right_cancel_iff _ _ _ (c * ((a % c + b % c) / c)), add_comm _ c, add_assoc,
        mod_add_div, le_antisymm (le_of_lt_succ h2) h0, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : ¬c ≤ a % c + b % c
⊢ (a % c + b % c) % c + 0 = a % c + b % c
have neg : a % c + b % c + 0 = a % c + b % c
Tactic: rw [Nat.mod_eq_of_lt (lt_of_not_ge h), add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : ¬c ≤ a % c + b % c
neg : a % c + b % c + 0 = a % c + b % c
⊢ (a % c + b % c) % c + 0 = a % c + b % c
have neg₁ : a % c + b % c = a % c + b % c
Tactic: rw [Nat.mod_eq_of_lt (lt_of_not_ge h), add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
hc : a % c + b % c < c
⊢ (a + b) % c = a % c + b % c
have rw : (a + b) % c = (a + b) % c + if c ≤ a % c + b % c then c else 0
Tactic: rw [← add_mod_add_ite, if_neg (not_le_of_gt hc), add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
hc : a % c + b % c < c
rw : (a + b) % c = (a + b) % c + if c ≤ a % c + b % c then c else 0
⊢ (a + b) % c = a % c + b % c
have rw₁ : (a + b) % c = (a + b) % c + 0
Tactic: rw [← add_mod_add_ite, if_neg (not_le_of_gt hc), add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
hc : a % c + b % c < c
rw : (a + b) % c = (a + b) % c + if c ≤ a % c + b % c then c else 0
rw₁ : (a + b) % c = (a + b) % c + 0
⊢ (a + b) % c = a % c + b % c
have rw₂ : (a + b) % c = (a + b) % c
Tactic: rw [← add_mod_add_ite, if_neg (not_le_of_gt hc), add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
hc : c ≤ a % c + b % c
⊢ (a + b) % c + c = a % c + b % c
have rw : (a + b) % c + c = (a + b) % c + if c ≤ a % c + b % c then c else 0
Tactic: rw [← add_mod_add_ite, if_pos hc]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
hc : c ≤ a % c + b % c
rw : (a + b) % c + c = (a + b) % c + if c ≤ a % c + b % c then c else 0
⊢ (a + b) % c + c = a % c + b % c
have rw₁ : (a + b) % c + c = (a + b) % c + c
Tactic: rw [← add_mod_add_ite, if_pos hc]