Theorem: HTPI.Lemma_7_4_5 (HTPILib/Chap7.lean)

State before:
m n : ℕ
a b : ℤ
h1 : rel_prime m n
⊢ a ≡ b (MOD m * n) ↔ a ≡ b (MOD m) ∧ a ≡ b (MOD n)
Tactic:
apply Iff.intro
State after:
case mp
m n : ℕ
a b : ℤ
h1 : rel_prime m n
⊢ a ≡ b (MOD m * n) → a ≡ b (MOD m) ∧ a ≡ b (MOD n)

case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
⊢ a ≡ b (MOD m) ∧ a ≡ b (MOD n) → a ≡ b (MOD m * n)

State before:
case mp
m n : ℕ
a b : ℤ
h1 : rel_prime m n
⊢ a ≡ b (MOD m * n) → a ≡ b (MOD m) ∧ a ≡ b (MOD n)
Tactic:
assume h2 : a ≡ b (MOD m * n)
State after:
case mp
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
⊢ a ≡ b (MOD m) ∧ a ≡ b (MOD n)

State before:
case mp
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
⊢ a ≡ b (MOD m) ∧ a ≡ b (MOD n)
Tactic:
obtain (j : Int) (h3 : a - b = (m * n) * j) from h2
State after:
case mp
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a ≡ b (MOD m) ∧ a ≡ b (MOD n)

State before:
case mp
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a ≡ b (MOD m) ∧ a ≡ b (MOD n)
Tactic:
apply And.intro
State after:
case mp.left
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a ≡ b (MOD m)

case mp.right
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a ≡ b (MOD n)

State before:
case mp.left
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a ≡ b (MOD m)
Tactic:
apply Exists.intro (n * j)
State after:
case mp.left
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a - b = ↑m * (↑n * j)

State before:
case mp.left
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a - b = ↑m * (↑n * j)
Tactic:
show a - b = m * (n * j) from
  calc a - b
    _ = m * n * j := h3
    _ = m * (n * j) := by ring
State after:
no goals

State before:
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ ↑m * ↑n * j = ↑m * (↑n * j)
Tactic:
ring
State after:
no goals

State before:
case mp.right
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a ≡ b (MOD n)
Tactic:
apply Exists.intro (m * j)
State after:
case mp.right
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a - b = ↑n * (↑m * j)

State before:
case mp.right
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ a - b = ↑n * (↑m * j)
Tactic:
show a - b = n * (m * j) from
  calc a - b
    _ = m * n * j := h3
    _ = n * (m * j) := by ring
State after:
no goals

State before:
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m * n)
j : ℤ
h3 : a - b = ↑m * ↑n * j
⊢ ↑m * ↑n * j = ↑n * (↑m * j)
Tactic:
ring
State after:
no goals

State before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
⊢ a ≡ b (MOD m) ∧ a ≡ b (MOD n) → a ≡ b (MOD m * n)
Tactic:
assume h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
State after:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
⊢ a ≡ b (MOD m * n)

State before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
⊢ a ≡ b (MOD m * n)
Tactic:
obtain (j : Int) (h3 : a - b = m * j) from h2.left
State after:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
⊢ a ≡ b (MOD m * n)

State before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
⊢ a ≡ b (MOD m * n)
Tactic:
have h4 : (↑n : Int) ∣ a - b := h2.right
State after:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ a - b
⊢ a ≡ b (MOD m * n)

State before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ a - b
⊢ a ≡ b (MOD m * n)
Tactic:
rewrite [h3] at h4
State after:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
⊢ a ≡ b (MOD m * n)

State before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
⊢ a ≡ b (MOD m * n)
Tactic:
have h5 : ↑n ∣ j := Theorem_7_2_2_Int h4 h1
State after:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
⊢ a ≡ b (MOD m * n)

State before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
⊢ a ≡ b (MOD m * n)
Tactic:
obtain (k : Int) (h6 : j = n * k) from h5
State after:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
k : ℤ
h6 : j = ↑n * k
⊢ a ≡ b (MOD m * n)

State before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
k : ℤ
h6 : j = ↑n * k
⊢ a ≡ b (MOD m * n)
Tactic:
apply Exists.intro k
State after:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
k : ℤ
h6 : j = ↑n * k
⊢ a - b = ↑(m * n) * k

State before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
k : ℤ
h6 : j = ↑n * k
⊢ a - b = ↑(m * n) * k
Tactic:
rewrite [Nat.cast_mul]
State after:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
k : ℤ
h6 : j = ↑n * k
⊢ a - b = ↑m * ↑n * k

State before:
case mpr
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
k : ℤ
h6 : j = ↑n * k
⊢ a - b = ↑m * ↑n * k
Tactic:
show a - b = (m * n) * k from
  calc a - b
    _ = m * j := h3
    _ = m * (n * k) := by rw [h6]
    _ = (m * n) * k := by ring
State after:
no goals

State before:
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
k : ℤ
h6 : j = ↑n * k
⊢ ↑m * j = ↑m * (↑n * k)
Tactic:
rw [h6]
State after:
no goals

State before:
m n : ℕ
a b : ℤ
h1 : rel_prime m n
h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
j : ℤ
h3 : a - b = ↑m * j
h4 : ↑n ∣ ↑m * j
h5 : ↑n ∣ j
k : ℤ
h6 : j = ↑n * k
⊢ ↑m * (↑n * k) = ↑m * ↑n * k
Tactic:
ring
State after:
no goals