Theorem: HTPI.mod_mod_image (HTPILib/Chap8Part2.lean)

State before:
m n : ℕ
h1 : rel_prime m n
⊢ image (mod_mod m n) (Set_rp_below (m * n)) = Set_rp_below m ×ₛ Set_rp_below n
Tactic:
apply Set.ext
State after:
case h
m n : ℕ
h1 : rel_prime m n
⊢ ∀ (x : ℕ × ℕ), x ∈ image (mod_mod m n) (Set_rp_below (m * n)) ↔ x ∈ Set_rp_below m ×ₛ Set_rp_below n

State before:
case h
m n : ℕ
h1 : rel_prime m n
⊢ ∀ (x : ℕ × ℕ), x ∈ image (mod_mod m n) (Set_rp_below (m * n)) ↔ x ∈ Set_rp_below m ×ₛ Set_rp_below n
Tactic:
fix (b, c) : Nat × Nat
State after:
case h
m n : ℕ
h1 : rel_prime m n
b c : ℕ
⊢ (b, c) ∈ image (mod_mod m n) (Set_rp_below (m * n)) ↔ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n

State before:
case h
m n : ℕ
h1 : rel_prime m n
b c : ℕ
⊢ (b, c) ∈ image (mod_mod m n) (Set_rp_below (m * n)) ↔ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n
Tactic:
apply Iff.intro
State after:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
⊢ (b, c) ∈ image (mod_mod m n) (Set_rp_below (m * n)) → (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n

case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
⊢ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n → (b, c) ∈ image (mod_mod m n) (Set_rp_below (m * n))

State before:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
⊢ (b, c) ∈ image (mod_mod m n) (Set_rp_below (m * n)) → (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n
Tactic:
assume h2 : (b, c) ∈ image (mod_mod m n) (Set_rp_below (m * n))
State after:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (b, c) ∈ image (mod_mod m n) (Set_rp_below (m * n))
⊢ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n

State before:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (b, c) ∈ image (mod_mod m n) (Set_rp_below (m * n))
⊢ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n
Tactic:
define at h2
State after:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
⊢ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n

State before:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
⊢ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n
Tactic:
obtain (a : Nat)
  (h3 : a ∈ Set_rp_below (m * n) ∧ mod_mod m n a = (b, c)) from h2
State after:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : a ∈ Set_rp_below (m * n) ∧ mod_mod m n a = (b, c)
⊢ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n

State before:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : a ∈ Set_rp_below (m * n) ∧ mod_mod m n a = (b, c)
⊢ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n
Tactic:
rewrite [Set_rp_below_def, mod_mod_def] at h3
State after:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
⊢ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n

State before:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
⊢ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n
Tactic:
have h4 : rel_prime (m * n) a := h3.left.left
State after:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime (m * n) a
⊢ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n

State before:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime (m * n) a
⊢ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n
Tactic:
rewrite [Lemma_7_4_6] at h4
State after:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
⊢ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n

State before:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
⊢ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n
Tactic:
have h5 : a % m = b ∧ a % n = c := Prod.mk.inj h3.right
State after:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
h5 : a % m = b ∧ a % n = c
⊢ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n

State before:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
h5 : a % m = b ∧ a % n = c
⊢ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n
Tactic:
define
State after:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
h5 : a % m = b ∧ a % n = c
⊢ b ∈ Set_rp_below m ∧ c ∈ Set_rp_below n

State before:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
h5 : a % m = b ∧ a % n = c
⊢ b ∈ Set_rp_below m ∧ c ∈ Set_rp_below n
Tactic:
rewrite [←h5.left, ←h5.right]
State after:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
h5 : a % m = b ∧ a % n = c
⊢ a % m ∈ Set_rp_below m ∧ a % n ∈ Set_rp_below n

State before:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
h5 : a % m = b ∧ a % n = c
⊢ a % m ∈ Set_rp_below m ∧ a % n ∈ Set_rp_below n
Tactic:
have h6 : m * n ≠ 0 := by linarith
State after:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
h5 : a % m = b ∧ a % n = c
h6 : m * n ≠ 0
⊢ a % m ∈ Set_rp_below m ∧ a % n ∈ Set_rp_below n

State before:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
h5 : a % m = b ∧ a % n = c
h6 : m * n ≠ 0
⊢ a % m ∈ Set_rp_below m ∧ a % n ∈ Set_rp_below n
Tactic:
have h7 : NeZero m := left_NeZero_of_mul h6
State after:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
h5 : a % m = b ∧ a % n = c
h6 : m * n ≠ 0
h7 : NeZero m
⊢ a % m ∈ Set_rp_below m ∧ a % n ∈ Set_rp_below n

State before:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
h5 : a % m = b ∧ a % n = c
h6 : m * n ≠ 0
h7 : NeZero m
⊢ a % m ∈ Set_rp_below m ∧ a % n ∈ Set_rp_below n
Tactic:
have h8 : NeZero n := right_NeZero_of_mul h6
State after:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
h5 : a % m = b ∧ a % n = c
h6 : m * n ≠ 0
h7 : NeZero m
h8 : NeZero n
⊢ a % m ∈ Set_rp_below m ∧ a % n ∈ Set_rp_below n

State before:
case h.mp
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
h5 : a % m = b ∧ a % n = c
h6 : m * n ≠ 0
h7 : NeZero m
h8 : NeZero n
⊢ a % m ∈ Set_rp_below m ∧ a % n ∈ Set_rp_below n
Tactic:
apply And.intro
State after:
case h.mp.left
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
h5 : a % m = b ∧ a % n = c
h6 : m * n ≠ 0
h7 : NeZero m
h8 : NeZero n
⊢ a % m ∈ Set_rp_below m

case h.mp.right
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
h5 : a % m = b ∧ a % n = c
h6 : m * n ≠ 0
h7 : NeZero m
h8 : NeZero n
⊢ a % n ∈ Set_rp_below n

State before:
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
h5 : a % m = b ∧ a % n = c
⊢ m * n ≠ 0
Tactic:
linarith
State after:
no goals

State before:
case h.mp.left
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
h5 : a % m = b ∧ a % n = c
h6 : m * n ≠ 0
h7 : NeZero m
h8 : NeZero n
⊢ a % m ∈ Set_rp_below m
Tactic:
show a % m ∈ Set_rp_below m from mod_elt_Set_rp_below h4.left
State after:
no goals

State before:
case h.mp.right
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
a : ℕ
h3 : (rel_prime (m * n) a ∧ a < m * n) ∧ (a % m, a % n) = (b, c)
h4 : rel_prime m a ∧ rel_prime n a
h5 : a % m = b ∧ a % n = c
h6 : m * n ≠ 0
h7 : NeZero m
h8 : NeZero n
⊢ a % n ∈ Set_rp_below n
Tactic:
show a % n ∈ Set_rp_below n from mod_elt_Set_rp_below h4.right
State after:
no goals

State before:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
⊢ (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n → (b, c) ∈ image (mod_mod m n) (Set_rp_below (m * n))
Tactic:
assume h2 : (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n
State after:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n
⊢ (b, c) ∈ image (mod_mod m n) (Set_rp_below (m * n))

State before:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (b, c) ∈ Set_rp_below m ×ₛ Set_rp_below n
⊢ (b, c) ∈ image (mod_mod m n) (Set_rp_below (m * n))
Tactic:
rewrite [Set_prod_def, Set_rp_below_def, Set_rp_below_def] at h2
State after:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
⊢ (b, c) ∈ image (mod_mod m n) (Set_rp_below (m * n))

State before:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
⊢ (b, c) ∈ image (mod_mod m n) (Set_rp_below (m * n))
Tactic:
define
State after:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
⊢ ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)

State before:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
⊢ ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
Tactic:
have h3 : m ≠ 0 := by linarith
State after:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : m ≠ 0
⊢ ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)

State before:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : m ≠ 0
⊢ ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
Tactic:
have h4 : n ≠ 0 := by linarith
State after:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : m ≠ 0
h4 : n ≠ 0
⊢ ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)

State before:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : m ≠ 0
h4 : n ≠ 0
⊢ ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
Tactic:
rewrite [←neZero_iff] at h3
State after:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : n ≠ 0
⊢ ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)

State before:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : n ≠ 0
⊢ ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
Tactic:
rewrite [←neZero_iff] at h4
State after:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
⊢ ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)

State before:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
⊢ ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
Tactic:
obtain (a : Nat) (h5 : a < m * n ∧ a ≡ b (MOD m) ∧ a ≡ c (MOD n))
  from Lemma_7_4_7 h1 b c
State after:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ ↑a ≡ ↑b (MOD m) ∧ ↑a ≡ ↑c (MOD n)
⊢ ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)

State before:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ ↑a ≡ ↑b (MOD m) ∧ ↑a ≡ ↑c (MOD n)
⊢ ∃ x ∈ Set_rp_below (m * n), mod_mod m n x = (b, c)
Tactic:
apply Exists.intro a
State after:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ ↑a ≡ ↑b (MOD m) ∧ ↑a ≡ ↑c (MOD n)
⊢ a ∈ Set_rp_below (m * n) ∧ mod_mod m n a = (b, c)

State before:
case h.mpr
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ ↑a ≡ ↑b (MOD m) ∧ ↑a ≡ ↑c (MOD n)
⊢ a ∈ Set_rp_below (m * n) ∧ mod_mod m n a = (b, c)
Tactic:
apply And.intro
State after:
case h.mpr.left
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ ↑a ≡ ↑b (MOD m) ∧ ↑a ≡ ↑c (MOD n)
⊢ a ∈ Set_rp_below (m * n)

case h.mpr.right
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ ↑a ≡ ↑b (MOD m) ∧ ↑a ≡ ↑c (MOD n)
⊢ mod_mod m n a = (b, c)

State before:
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
⊢ m ≠ 0
Tactic:
linarith
State after:
no goals

State before:
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : m ≠ 0
⊢ n ≠ 0
Tactic:
linarith
State after:
no goals

State before:
case h.mpr.left
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ ↑a ≡ ↑b (MOD m) ∧ ↑a ≡ ↑c (MOD n)
⊢ a ∈ Set_rp_below (m * n)
Tactic:
define
State after:
case h.mpr.left
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ ↑a ≡ ↑b (MOD m) ∧ ↑a ≡ ↑c (MOD n)
⊢ rel_prime (m * n) a ∧ a < m * n

State before:
case h.mpr.left
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ ↑a ≡ ↑b (MOD m) ∧ ↑a ≡ ↑c (MOD n)
⊢ rel_prime (m * n) a ∧ a < m * n
Tactic:
apply And.intro _ h5.left
State after:
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ ↑a ≡ ↑b (MOD m) ∧ ↑a ≡ ↑c (MOD n)
⊢ rel_prime (m * n) a

State before:
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ ↑a ≡ ↑b (MOD m) ∧ ↑a ≡ ↑c (MOD n)
⊢ rel_prime (m * n) a
Tactic:
rewrite [Lemma_7_4_6]
State after:
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ ↑a ≡ ↑b (MOD m) ∧ ↑a ≡ ↑c (MOD n)
⊢ rel_prime m a ∧ rel_prime n a

State before:
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ ↑a ≡ ↑b (MOD m) ∧ ↑a ≡ ↑c (MOD n)
⊢ rel_prime m a ∧ rel_prime n a
Tactic:
rewrite [congr_rel_prime h5.right.left,
  congr_rel_prime h5.right.right]
State after:
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ ↑a ≡ ↑b (MOD m) ∧ ↑a ≡ ↑c (MOD n)
⊢ rel_prime m b ∧ rel_prime n c

State before:
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ ↑a ≡ ↑b (MOD m) ∧ ↑a ≡ ↑c (MOD n)
⊢ rel_prime m b ∧ rel_prime n c
Tactic:
show rel_prime m b ∧ rel_prime n c from
  And.intro h2.left.left h2.right.left
State after:
no goals

State before:
case h.mpr.right
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ ↑a ≡ ↑b (MOD m) ∧ ↑a ≡ ↑c (MOD n)
⊢ mod_mod m n a = (b, c)
Tactic:
rewrite [congr_iff_mod_eq_Nat, congr_iff_mod_eq_Nat] at h5
State after:
case h.mpr.right
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ a % m = b % m ∧ a % n = c % n
⊢ mod_mod m n a = (b, c)

State before:
case h.mpr.right
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ a % m = b % m ∧ a % n = c % n
⊢ mod_mod m n a = (b, c)
Tactic:
rewrite [mod_mod_def, h5.right.left, h5.right.right]
State after:
case h.mpr.right
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ a % m = b % m ∧ a % n = c % n
⊢ (b % m, c % n) = (b, c)

State before:
case h.mpr.right
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ a % m = b % m ∧ a % n = c % n
⊢ (b % m, c % n) = (b, c)
Tactic:
rewrite [Nat.mod_eq_of_lt h2.left.right,
  Nat.mod_eq_of_lt h2.right.right]
State after:
case h.mpr.right
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ a % m = b % m ∧ a % n = c % n
⊢ (b, c) = (b, c)

State before:
case h.mpr.right
m n : ℕ
h1 : rel_prime m n
b c : ℕ
h2 : (rel_prime m b ∧ b < m) ∧ rel_prime n c ∧ c < n
h3 : NeZero m
h4 : NeZero n
a : ℕ
h5 : a < m * n ∧ a % m = b % m ∧ a % n = c % n
⊢ (b, c) = (b, c)
Tactic:
rfl
State after:
no goals