awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.ModEq
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.gcd m) : ℤ) = (↑n : ℤ) * n.gcdA m + (↑m : ℤ) * n.gcdB m

Tactic:
have := gcd_eq_gcd_ab n m
-- Module: Mathlib.Data.Nat.ModEq
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) : ℤ)
right :
  (↑m : ℤ) ∣
    (↑b : ℤ) - ((↑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) : ℤ)

Tactic:
constructor
-- Module: Mathlib.Data.Nat.ModEq
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 : ℤ) * 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) : ℤ)

Tactic:
rw [Int.emod_def, ← sub_add]

Premises used: sub_add, Int.emod_def
-- Module: Mathlib.Data.Nat.ModEq
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) : ℤ) +
      (↑(n.lcm m) : ℤ) *
        (((↑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 [Int.emod_def, ← sub_add]

Premises used: sub_add, Int.emod_def
-- Module: Mathlib.Data.Nat.ModEq
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) : ℤ))

Tactic:
Int.dvd_add ?_ (dvd_mul_of_dvd_left ?_ _)

Premises used: dvd_mul_of_dvd_left, Int.dvd_add
-- Module: Mathlib.Data.Nat.ModEq
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) : ℤ)
left₁ : Dvd.dvd (α := ℤ) (↑n : ℤ) (↑(n.lcm 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) : ℤ))

Tactic:
refine Int.dvd_add ?_ (dvd_mul_of_dvd_left ?_ _)

Premises used: dvd_mul_of_dvd_left, Int.dvd_add
-- Module: Mathlib.Data.Nat.ModEq
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) : ℤ))

Tactic:
Int.dvd_add ?_ (dvd_mul_of_dvd_left ?_ _)

Premises used: dvd_mul_of_dvd_left, Int.dvd_add
-- Module: Mathlib.Data.Nat.ModEq
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) : ℤ)
right₁ : Dvd.dvd (α := ℤ) (↑m : ℤ) (↑(n.lcm 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) : ℤ))

Tactic:
refine Int.dvd_add ?_ (dvd_mul_of_dvd_left ?_ _)

Premises used: dvd_mul_of_dvd_left, Int.dvd_add
-- Module: Mathlib.Data.Nat.ModEq
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.lcm m
⊢ Dvd.dvd (α := ℤ) (↑n : ℤ) (↑(n.lcm m) : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.Data.Nat.ModEq
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.lcm m
⊢ Dvd.dvd (α := ℤ) (↑n : ℤ) (↑(n.lcm m) : ℤ)

Tactic:
try norm_cast
-- Module: Mathlib.Data.Nat.ModEq
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 ∣ n.lcm m
⊢ Dvd.dvd (α := ℤ) (↑m : ℤ) (↑(n.lcm m) : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.Data.Nat.ModEq
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 ∣ n.lcm m
⊢ Dvd.dvd (α := ℤ) (↑m : ℤ) (↑(n.lcm m) : ℤ)

Tactic:
try norm_cast
-- Module: Mathlib.Data.Nat.ModEq
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) : ℤ) - (↑n : ℤ) * n.gcdA m = (↑m : ℤ) * n.gcdB m

Tactic:
rw [← sub_eq_iff_eq_add'] at this

Premises used: sub_eq_iff_eq_add'
-- Module: Mathlib.Data.Nat.ModEq
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) : ℤ)))
left₁ : (↑(n.gcd m) : ℤ) ∣ HMul.hMul (α := ℤ) (↑(n.gcd m) : ℤ) (↑a : ℤ)
⊢ (↑n : ℤ) ∣ (↑a : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑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]

Premises used: add_sub_assoc, sub_self, Int.sub_mul, mul_assoc, Int.mul_ediv_assoc, Int.mul_sub, add_comm, Int.dvd_neg, sub_sub, Int.mul_ediv_cancel_left, Int.add_ediv_of_dvd_left, zero_sub, Nat.ModEq.dvd
-- Module: Mathlib.Data.Nat.ModEq
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 : ℤ) ∣ (↑n : ℤ) * (n.gcdA m * (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) / (↑(n.gcd m) : ℤ)))

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Data.Nat.ModEq
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 : ℤ) ∣ (↑n : ℤ) * (n.gcdA m * (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) / (↑(n.gcd m) : ℤ)))

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Data.Nat.ModEq
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.gcd m ∣ n.gcd m * a
⊢ (↑(n.gcd m) : ℤ) ∣ HMul.hMul (α := ℤ) (↑(n.gcd m) : ℤ) (↑a : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.Data.Nat.ModEq
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 ∣ n.gcd m * a

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Data.Nat.ModEq
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 ∣ n.gcd m * a

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Data.Nat.ModEq
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 ∣ n.lcm m

Tactic:
dvd_lcm_left n m

Premises used: Nat.dvd_lcm_left
-- Module: Mathlib.Data.Nat.ModEq
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 ∣ n.lcm m

Tactic:
exact dvd_lcm_left n m

Premises used: Nat.dvd_lcm_left
-- Module: Mathlib.Data.Nat.ModEq
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) : ℤ) - (↑m : ℤ) * n.gcdB m = (↑n : ℤ) * n.gcdA m

Tactic:
rw [← sub_eq_iff_eq_add] at this

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.Data.Nat.ModEq
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) : ℤ)))
right₁ : (↑(n.gcd m) : ℤ) ∣ (↑m : ℤ) * n.gcdB m * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ (↑m : ℤ) ∣ (↑b : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑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]

Premises used: sub_add, sub_self, Int.sub_ediv_of_dvd, Int.sub_mul, mul_assoc, Int.mul_ediv_assoc, Int.mul_sub, zero_add, Int.mul_ediv_cancel_left, Nat.ModEq.dvd
-- Module: Mathlib.Data.Nat.ModEq
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 : ℤ) ∣ (↑m : ℤ) * (n.gcdB m * (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) / (↑(n.gcd m) : ℤ)))

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Data.Nat.ModEq
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 : ℤ) ∣ (↑m : ℤ) * (n.gcdB m * (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) / (↑(n.gcd m) : ℤ)))

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Data.Nat.ModEq
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
⊢ (↑(n.gcd m) : ℤ) ∣ (↑m : ℤ) * n.gcdB m * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)

Tactic:
hcoedvd _
-- Module: Mathlib.Data.Nat.ModEq
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
⊢ (↑(n.gcd m) : ℤ) ∣ (↑m : ℤ) * n.gcdB m * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)

Tactic:
exact hcoedvd _
-- Module: Mathlib.Data.Nat.ModEq
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 ∣ n.lcm m

Tactic:
dvd_lcm_right n m

Premises used: Nat.dvd_lcm_right
-- Module: Mathlib.Data.Nat.ModEq
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 ∣ n.lcm m

Tactic:
exact dvd_lcm_right n m

Premises used: Nat.dvd_lcm_right
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a_1 b_1 c d : ℕ
co : n.Coprime m
a b : ℕ
⊢ a ≡ b [MOD 1]

Tactic:
@modEq_one a b

Premises used: Nat.modEq_one
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a_1 b_1 c d : ℕ
co : n.Coprime m
a b : ℕ
⊢ a ≡ b [MOD n.gcd m]

Tactic:
convert! @modEq_one a b

Premises used: Nat.modEq_one
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
dsimp :
  (↑(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
⊢ (↑(chineseRemainder' h) : ℕ) < n.lcm m

Tactic:
dsimp only [chineseRemainder']

Premises used: Nat.chineseRemainder'
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
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) : ℤ)
⊢ (↑(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

Tactic:
rw [dif_neg hn, dif_neg hm, Subtype.coe_mk, xgcd_val, ← Int.toNat_natCast (lcm n m)]

Premises used: Nat.lcm, Subtype.coe_mk, Int.toNat_natCast, dif_neg, Nat.xgcd_val
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ LT.lt (α := ℤ) 0 (↑(n.lcm m) : ℤ)

Tactic:
have lcm_pos := Int.natCast_pos.mpr (Nat.pos_of_ne_zero (lcm_ne_zero hn hm))
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
lcm_pos : LT.lt (α := ℤ) 0 (↑(n.lcm m) : ℤ)
⊢ (((↑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:
(Int.toNat_lt_toNat lcm_pos).mpr (Int.emod_lt_of_pos _ lcm_pos)

Premises used: Iff.mpr, Int.toNat_lt_toNat, Int.emod_lt_of_pos
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
lcm_pos : LT.lt (α := ℤ) 0 (↑(n.lcm m) : ℤ)
⊢ (((↑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:
exact (Int.toNat_lt_toNat lcm_pos).mpr (Int.emod_lt_of_pos _ lcm_pos)

Premises used: Iff.mpr, Int.toNat_lt_toNat, Int.emod_lt_of_pos
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n : ℕ
co : n.Coprime m
a b : ℕ
hn : n ≠ 0
hm : m ≠ 0
⊢ (↑(chineseRemainder co a b) : ℕ) < n * m

Tactic:
lt_of_lt_of_le (chineseRemainder'_lt_lcm _ hn hm) (le_of_eq co.lcm_eq_mul)

Premises used: Nat.chineseRemainder'_lt_lcm, Nat.Coprime.lcm_eq_mul, le_of_eq, lt_of_lt_of_le
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b : ℕ
hn : a ≡ b [MOD n]
hm : a ≡ b [MOD m]
⊢ a ≡ b [MOD n.lcm m]

Tactic:
Nat.modEq_iff_dvd.mpr <| Int.coe_lcm_dvd (Nat.modEq_iff_dvd.mp hn) (Nat.modEq_iff_dvd.mp hm)

Premises used: Iff.mpr, Nat.modEq_iff_dvd, Iff.mp, Int.coe_lcm_dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n : ℕ
co : n.Coprime m
a b z : ℕ
hzan : z ≡ a [MOD n]
hzbm : z ≡ b [MOD m]
⊢ z ≡ (↑(chineseRemainder co a b) : ℕ) [MOD n * m]

Tactic:
simpa [Nat.Coprime.lcm_eq_mul co] using
    mod_lcm (hzan.trans ((chineseRemainder co a b).prop.1).symm)
      (hzbm.trans ((chineseRemainder co a b).prop.2).symm)

Premises used: Nat.chineseRemainder, Nat.mod_lcm, And.right, And.left, Nat.ModEq.symm, Subtype.prop, Nat.Coprime.lcm_eq_mul, Nat.ModEq.trans
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ≡ b [MOD m] ∧ a ≡ b [MOD n]
⊢ 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

Premises used: Int.dvd_natAbs, Nat.modEq_iff_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs ∧ n ∣ (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs
rw : m * n ∣ (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs
⊢ a ≡ b [MOD m * n]

Tactic:
rw [Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.natCast_dvd_natCast]

Premises used: Int.dvd_natAbs, Nat.modEq_iff_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs ∧ n ∣ (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs
⊢ m * n ∣ (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs

Tactic:
hmn.mul_dvd_of_dvd_of_dvd h.1 h.2

Premises used: And.right, And.left, Nat.Coprime.mul_dvd_of_dvd_of_dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs ∧ n ∣ (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs
⊢ m * n ∣ (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs

Tactic:
exact hmn.mul_dvd_of_dvd_of_dvd h.1 h.2

Premises used: And.right, And.left, Nat.Coprime.mul_dvd_of_dvd_of_dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
b a n : ℕ
h : a * b ≡ 1 [MOD n]
obtain : ∀ (g : ℕ) (hh : n = a.gcd n * g), a.Coprime n
⊢ a.Coprime n

Tactic:
obtain ⟨g, hh⟩ := Nat.gcd_dvd_right a n

Premises used: Nat.gcd_dvd_right
-- Module: Mathlib.Data.Nat.ModEq
Goal:
b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
rw : 1 ≡ 0 [MOD a.gcd n]
⊢ a.Coprime n

Tactic:
rw [Nat.coprime_iff_gcd_eq_one, ← Nat.dvd_one, ← Nat.modEq_zero_iff_dvd]

Premises used: Nat.dvd_one, Nat.coprime_iff_gcd_eq_one, Nat.modEq_zero_iff_dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
⊢ a * b ≡ 0 * b [MOD a.gcd n]

Tactic:
(Nat.modEq_zero_iff_dvd.mpr (Nat.gcd_dvd_left _ _)).mul_right b

Premises used: Iff.mpr, Nat.gcd_dvd_left, Nat.ModEq.mul_right, Nat.modEq_zero_iff_dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
rw rw₁ : Eq (α := ℕ) 0 0
⊢ 0 * b = 0

Tactic:
rw [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Data.Nat.ModEq
Goal:
b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
a₁ : 0 * b = 0
⊢ 1 ≡ 0 [MOD a.gcd n]

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]

Premises used: Nat.gcd, Iff.mpr, Nat.gcd_dvd_left, Nat.ModEq.mul_right, Nat.modEq_zero_iff_dvd
-- Module: Mathlib.Data.Nat.ModEq
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

Tactic:
simp [hc0, Nat.mod_zero]

Premises used: Nat.mod_zero
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
rw : ((a % c + b % c) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c
⊢ ((a + b) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c

Tactic:
rw [this]
-- Module: Mathlib.Data.Nat.ModEq
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
neg : ∀ (h : ¬c ≤ a % c + b % c), (a % c + b % c) % c + 0 = a % c + b % c
⊢ ((a % c + b % c) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
rw : a % c + b % c < c + c
⊢ a % c + b % c < c * 2

Tactic:
rw [mul_two]

Premises used: mul_two
-- Module: Mathlib.Data.Nat.ModEq
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

Tactic:
add_lt_add (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0))
                (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0))

Premises used: Nat.mod_lt, Nat.add_lt_add, Nat.pos_of_ne_zero
-- Module: Mathlib.Data.Nat.ModEq
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

Tactic:
exact
              add_lt_add (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0))
                (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0))

Premises used: Nat.mod_lt, Nat.add_lt_add, Nat.pos_of_ne_zero