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

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : rel_prime m n
a b : ℕ
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
set s : Int := gcd_c1 m n
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : rel_prime m n
a b : ℕ
s : ℤ := gcd_c1 m n
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : rel_prime m n
a b : ℕ
s : ℤ := gcd_c1 m n
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
set t : Int := gcd_c2 m n
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : rel_prime m n
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : rel_prime m n
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
have h4 : s * m + t * n = gcd m n := gcd_lin_comb n m
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : rel_prime m n
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = ↑(gcd m n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : rel_prime m n
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = ↑(gcd m n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
define at h1
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = ↑(gcd m n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = ↑(gcd m n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
rewrite [h1, Nat.cast_one] at h4
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = 1
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = 1
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
set x : Int := t * n * a + s * m * b
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
have h5 : x ≡ a (MOD m) := Lemma_7_4_7_aux h4 a b
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : s * ↑m + t * ↑n = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
rewrite [add_comm] at h4
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
have h6 : s * m * b + t * n * a ≡ b (MOD n) :=
  Lemma_7_4_7_aux h4 b a
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : s * ↑m * ↑b + t * ↑n * ↑a ≡ ↑b (MOD n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : s * ↑m * ↑b + t * ↑n * ↑a ≡ ↑b (MOD n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
have h7 : s * m * b + t * n * a = x := by ring
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : s * ↑m * ↑b + t * ↑n * ↑a ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : s * ↑m * ↑b + t * ↑n * ↑a ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
rewrite [h7] at h6
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
have h8 : m * n ≠ 0 := mul_ne_zero (NeZero.ne m) (NeZero.ne n)
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : m * n ≠ 0
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : m * n ≠ 0
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
rewrite [←neZero_iff] at h8
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
have h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧
  x ≡ x % ↑(m * n) (MOD m * n) := mod_cmpl_res (m * n) x
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
have h10 : x % ↑(m * n) < ↑(m * n) ∧
  x ≡ x % ↑(m * n) (MOD m * n) := h9.right
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
h10 : x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
h10 : x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
set r : Nat := Int.toNat (x % ↑(m * n))
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
h10 : x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
h10 : x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
have h11 : x % ↑(m * n) = ↑r := (Int.toNat_of_nonneg h9.left).symm
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
h10 : x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
h11 : x % ↑(m * n) = ↑r
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
h10 : x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
h11 : x % ↑(m * n) = ↑r
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
rewrite [h11, Nat.cast_lt] at h10
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
h10 : r < m * n ∧ x ≡ ↑r (MOD m * n)
h11 : x % ↑(m * n) = ↑r
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
h10 : r < m * n ∧ x ≡ ↑r (MOD m * n)
h11 : x % ↑(m * n) = ↑r
⊢ ∃ r < m * n, ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
apply Exists.intro r
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
h10 : r < m * n ∧ x ≡ ↑r (MOD m * n)
h11 : x % ↑(m * n) = ↑r
⊢ r < m * n ∧ ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
h10 : r < m * n ∧ x ≡ ↑r (MOD m * n)
h11 : x % ↑(m * n) = ↑r
⊢ r < m * n ∧ ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
apply And.intro h10.left
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
h10 : r < m * n ∧ x ≡ ↑r (MOD m * n)
h11 : x % ↑(m * n) = ↑r
⊢ ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
h10 : r < m * n ∧ x ≡ ↑r (MOD m * n)
h11 : x % ↑(m * n) = ↑r
⊢ ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
have h12 : r ≡ x (MOD (m * n)) := congr_symm h10.right
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
h10 : r < m * n ∧ x ≡ ↑r (MOD m * n)
h11 : x % ↑(m * n) = ↑r
h12 : ↑r ≡ x (MOD m * n)
⊢ ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
h10 : r < m * n ∧ x ≡ ↑r (MOD m * n)
h11 : x % ↑(m * n) = ↑r
h12 : ↑r ≡ x (MOD m * n)
⊢ ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
rewrite [Lemma_7_4_5 _ _ h1] at h12
State after:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
h10 : r < m * n ∧ x ≡ ↑r (MOD m * n)
h11 : x % ↑(m * n) = ↑r
h12 : ↑r ≡ x (MOD m) ∧ ↑r ≡ x (MOD n)
⊢ ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
h10 : r < m * n ∧ x ≡ ↑r (MOD m * n)
h11 : x % ↑(m * n) = ↑r
h12 : ↑r ≡ x (MOD m) ∧ ↑r ≡ x (MOD n)
⊢ ↑r ≡ ↑a (MOD m) ∧ ↑r ≡ ↑b (MOD n)
Tactic:
apply And.intro
State after:
case left
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
h10 : r < m * n ∧ x ≡ ↑r (MOD m * n)
h11 : x % ↑(m * n) = ↑r
h12 : ↑r ≡ x (MOD m) ∧ ↑r ≡ x (MOD n)
⊢ ↑r ≡ ↑a (MOD m)

case right
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
h10 : r < m * n ∧ x ≡ ↑r (MOD m * n)
h11 : x % ↑(m * n) = ↑r
h12 : ↑r ≡ x (MOD m) ∧ ↑r ≡ x (MOD n)
⊢ ↑r ≡ ↑b (MOD n)

State before:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : s * ↑m * ↑b + t * ↑n * ↑a ≡ ↑b (MOD n)
⊢ s * ↑m * ↑b + t * ↑n * ↑a = x
Tactic:
ring
State after:
no goals

State before:
case left
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
h10 : r < m * n ∧ x ≡ ↑r (MOD m * n)
h11 : x % ↑(m * n) = ↑r
h12 : ↑r ≡ x (MOD m) ∧ ↑r ≡ x (MOD n)
⊢ ↑r ≡ ↑a (MOD m)
Tactic:
show r ≡ a (MOD m) from congr_trans h12.left h5
State after:
no goals

State before:
case right
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h1 : gcd m n = 1
a b : ℕ
s : ℤ := gcd_c1 m n
t : ℤ := gcd_c2 m n
h4 : t * ↑n + s * ↑m = 1
x : ℤ := t * ↑n * ↑a + s * ↑m * ↑b
h5 : x ≡ ↑a (MOD m)
h6 : x ≡ ↑b (MOD n)
h7 : s * ↑m * ↑b + t * ↑n * ↑a = x
h8 : NeZero (m * n)
h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧ x ≡ x % ↑(m * n) (MOD m * n)
r : ℕ := Int.toNat (x % ↑(m * n))
h10 : r < m * n ∧ x ≡ ↑r (MOD m * n)
h11 : x % ↑(m * n) = ↑r
h12 : ↑r ≡ x (MOD m) ∧ ↑r ≡ x (MOD n)
⊢ ↑r ≡ ↑b (MOD n)
Tactic:
show r ≡ b (MOD n) from congr_trans h12.right h6
State after:
no goals