internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Lemma_7_4_7
Proof 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
Proof 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)
Theorem: HTPI.Lemma_7_4_7
Proof 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
Proof 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)
Theorem: HTPI.Lemma_7_4_7
Proof 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))
Proof 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)
Theorem: HTPI.Lemma_7_4_7
Proof 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
Proof 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)
Theorem: HTPI.Lemma_7_4_7
Proof 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
Proof 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)
Theorem: HTPI.Lemma_7_4_7
Proof 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
Proof 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)
Theorem: HTPI.Lemma_7_4_7
Proof 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
Proof 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)
Theorem: HTPI.Lemma_7_4_7
Proof 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
Proof 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)
Theorem: HTPI.Lemma_7_4_7
Proof 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
Proof 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)
Theorem: HTPI.Lemma_7_4_7
Proof 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
Proof 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)
Theorem: HTPI.Lemma_7_4_7
Proof 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
Proof state after:
no goals
Theorem: HTPI.Lemma_7_4_7
Proof 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
Proof state after:
no goals
Theorem: HTPI.Lemma_7_4_7
Proof 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
Proof state after:
no goals
Theorem: HTPI.Set_prod_def
Proof state before:
U V : Type
A : Set U
B : Set V
a : U
b : V
⊢ (a, b) ∈ A ×ₛ B ↔ a ∈ A ∧ b ∈ B
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Rel_prod_def
Proof state before:
U V W X : Type
R : Rel U V
S : Rel W X
u : U
v : V
w : W
x : X
⊢ (R ×ᵣ S) (u, w) (v, x) ↔ R u v ∧ S w x
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_2_1
Proof state before:
U V W X : Type
A : Set U
B : Set V
C : Set W
D : Set X
h1 : A ∼ B
h2 : C ∼ D
⊢ A ×ₛ C ∼ B ×ₛ D
Tactic:
obtain (R : Rel U V) (h3 : matching R A B) from h1
Proof state after:
U V W X : Type
A : Set U
B : Set V
C : Set W
D : Set X
h1 : A ∼ B
h2 : C ∼ D
R : Rel U V
h3 : matching R A B
⊢ A ×ₛ C ∼ B ×ₛ D
Theorem: HTPI.Theorem_8_1_2_1
Proof state before:
U V W X : Type
A : Set U
B : Set V
C : Set W
D : Set X
h1 : A ∼ B
h2 : C ∼ D
R : Rel U V
h3 : matching R A B
⊢ A ×ₛ C ∼ B ×ₛ D
Tactic:
obtain (S : Rel W X) (h4 : matching S C D) from h2
Proof state after:
U V W X : Type
A : Set U
B : Set V
C : Set W
D : Set X
h1 : A ∼ B
h2 : C ∼ D
R : Rel U V
h3 : matching R A B
S : Rel W X
h4 : matching S C D
⊢ A ×ₛ C ∼ B ×ₛ D
Theorem: HTPI.Theorem_8_1_2_1
Proof state before:
U V W X : Type
A : Set U
B : Set V
C : Set W
D : Set X
h1 : A ∼ B
h2 : C ∼ D
R : Rel U V
h3 : matching R A B
S : Rel W X
h4 : matching S C D
⊢ A ×ₛ C ∼ B ×ₛ D
Tactic:
apply Exists.intro (R ×ᵣ S)
Proof state after:
U V W X : Type
A : Set U
B : Set V
C : Set W
D : Set X
h1 : A ∼ B
h2 : C ∼ D
R : Rel U V
h3 : matching R A B
S : Rel W X
h4 : matching S C D
⊢ matching (R ×ᵣ S) (A ×ₛ C) (B ×ₛ D)
Theorem: HTPI.Theorem_8_1_2_1
Proof state before:
U V W X : Type
A : Set U
B : Set V
C : Set W
D : Set X
h1 : A ∼ B
h2 : C ∼ D
R : Rel U V
h3 : matching R A B
S : Rel W X
h4 : matching S C D
⊢ matching (R ×ᵣ S) (A ×ₛ C) (B ×ₛ D)
Tactic:
show matching (R ×ᵣ S) (A ×ₛ C) (B ×ₛ D) from prod_match h3 h4
Proof state after:
no goals
Theorem: HTPI.qr_def
Proof state before:
n a : ℕ
⊢ qr n a = (a / n, a % n)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.qr_one_one
Proof state before:
n : ℕ
⊢ one_to_one (qr n)
Tactic:
define
Proof state after:
n : ℕ
⊢ ∀ (x1 x2 : ℕ), qr n x1 = qr n x2 → x1 = x2
Theorem: HTPI.qr_one_one
Proof state before:
n : ℕ
⊢ ∀ (x1 x2 : ℕ), qr n x1 = qr n x2 → x1 = x2
Tactic:
fix a1 : Nat
Proof state after:
n a1 : ℕ
⊢ ∀ (x2 : ℕ), qr n a1 = qr n x2 → a1 = x2
Theorem: HTPI.qr_one_one
Proof state before:
n a1 : ℕ
⊢ ∀ (x2 : ℕ), qr n a1 = qr n x2 → a1 = x2
Tactic:
fix a2 : Nat
Proof state after:
n a1 a2 : ℕ
⊢ qr n a1 = qr n a2 → a1 = a2
Theorem: HTPI.qr_one_one
Proof state before:
n a1 a2 : ℕ
⊢ qr n a1 = qr n a2 → a1 = a2
Tactic:
assume h1 : qr n a1 = qr n a2
Proof state after:
n a1 a2 : ℕ
h1 : qr n a1 = qr n a2
⊢ a1 = a2
Theorem: HTPI.qr_one_one
Proof state before:
n a1 a2 : ℕ
h1 : qr n a1 = qr n a2
⊢ a1 = a2
Tactic:
rewrite [qr_def, qr_def] at h1
Proof state after:
n a1 a2 : ℕ
h1 : (a1 / n, a1 % n) = (a2 / n, a2 % n)
⊢ a1 = a2
Theorem: HTPI.qr_one_one
Proof state before:
n a1 a2 : ℕ
h1 : (a1 / n, a1 % n) = (a2 / n, a2 % n)
⊢ a1 = a2
Tactic:
have h2 : a1 / n = a2 / n ∧ a1 % n = a2 % n := Prod.mk.inj h1
Proof state after:
n a1 a2 : ℕ
h1 : (a1 / n, a1 % n) = (a2 / n, a2 % n)
h2 : a1 / n = a2 / n ∧ a1 % n = a2 % n
⊢ a1 = a2
Theorem: HTPI.qr_one_one
Proof state before:
n a1 a2 : ℕ
h1 : (a1 / n, a1 % n) = (a2 / n, a2 % n)
h2 : a1 / n = a2 / n ∧ a1 % n = a2 % n
⊢ a1 = a2
Tactic:
show a1 = a2 from
  calc a1
    _ = n * (a1 / n) + a1 % n := (Nat.div_add_mod a1 n).symm
    _ = n * (a2 / n) + a2 % n := by rw [h2.left, h2.right]
    _ = a2 := Nat.div_add_mod a2 n
Proof state after:
no goals
Theorem: HTPI.qr_one_one
Proof state before:
n a1 a2 : ℕ
h1 : (a1 / n, a1 % n) = (a2 / n, a2 % n)
h2 : a1 / n = a2 / n ∧ a1 % n = a2 % n
⊢ n * (a1 / n) + a1 % n = n * (a2 / n) + a2 % n
Tactic:
rw [h2.left, h2.right]
Proof state after:
no goals
Theorem: HTPI.numElts_prod
Proof state before:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : numElts A m
h2 : numElts B n
⊢ numElts (A ×ₛ B) (m * n)
Tactic:
rewrite [numElts_def] at h1
Proof state after:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : I m ∼ A
h2 : numElts B n
⊢ numElts (A ×ₛ B) (m * n)
Theorem: HTPI.numElts_prod
Proof state before:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : I m ∼ A
h2 : numElts B n
⊢ numElts (A ×ₛ B) (m * n)
Tactic:
rewrite [numElts_def] at h2
Proof state after:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ B
⊢ numElts (A ×ₛ B) (m * n)
Theorem: HTPI.numElts_prod
Proof state before:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ B
⊢ numElts (A ×ₛ B) (m * n)
Tactic:
rewrite [numElts_def]
Proof state after:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ B
⊢ I (m * n) ∼ A ×ₛ B
Theorem: HTPI.numElts_prod
Proof state before:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ B
⊢ I (m * n) ∼ A ×ₛ B
Tactic:
have h3 : I m ×ₛ I n ∼ A ×ₛ B := Theorem_8_1_2_1 h1 h2
Proof state after:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ B
h3 : I m ×ₛ I n ∼ A ×ₛ B
⊢ I (m * n) ∼ A ×ₛ B
Theorem: HTPI.numElts_prod
Proof state before:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ B
h3 : I m ×ₛ I n ∼ A ×ₛ B
⊢ I (m * n) ∼ A ×ₛ B
Tactic:
have h4 : I (m * n) ∼ I m ×ₛ I n := I_prod m n
Proof state after:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ B
h3 : I m ×ₛ I n ∼ A ×ₛ B
h4 : I (m * n) ∼ I m ×ₛ I n
⊢ I (m * n) ∼ A ×ₛ B
Theorem: HTPI.numElts_prod
Proof state before:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ B
h3 : I m ×ₛ I n ∼ A ×ₛ B
h4 : I (m * n) ∼ I m ×ₛ I n
⊢ I (m * n) ∼ A ×ₛ B
Tactic:
show I (m * n) ∼ A ×ₛ B from Theorem_8_1_3_3 h4 h3
Proof state after:
no goals
Theorem: HTPI.mod_mod_def
Proof state before:
m n a : ℕ
⊢ mod_mod m n a = (a % m, a % n)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.mod_mod_one_one_on
Proof state before:
m n : ℕ
h1 : rel_prime m n
⊢ one_one_on (mod_mod m n) (Set_rp_below (m * n))
Tactic:
define
Proof state after:
m n : ℕ
h1 : rel_prime m n
⊢ ∀ ⦃x1 x2 : ℕ⦄, x1 ∈ Set_rp_below (m * n) → x2 ∈ Set_rp_below (m * n) → mod_mod m n x1 = mod_mod m n x2 → x1 = x2
Theorem: HTPI.mod_mod_one_one_on
Proof state before:
m n : ℕ
h1 : rel_prime m n
⊢ ∀ ⦃x1 x2 : ℕ⦄, x1 ∈ Set_rp_below (m * n) → x2 ∈ Set_rp_below (m * n) → mod_mod m n x1 = mod_mod m n x2 → x1 = x2
Tactic:
fix a1 : Nat
Proof state after:
m n : ℕ
h1 : rel_prime m n
a1 : ℕ
⊢ ∀ ⦃x2 : ℕ⦄, a1 ∈ Set_rp_below (m * n) → x2 ∈ Set_rp_below (m * n) → mod_mod m n a1 = mod_mod m n x2 → a1 = x2
Theorem: HTPI.mod_mod_one_one_on
Proof state before:
m n : ℕ
h1 : rel_prime m n
a1 : ℕ
⊢ ∀ ⦃x2 : ℕ⦄, a1 ∈ Set_rp_below (m * n) → x2 ∈ Set_rp_below (m * n) → mod_mod m n a1 = mod_mod m n x2 → a1 = x2
Tactic:
fix a2 : Nat
Proof state after:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
⊢ a1 ∈ Set_rp_below (m * n) → a2 ∈ Set_rp_below (m * n) → mod_mod m n a1 = mod_mod m n a2 → a1 = a2
Theorem: HTPI.mod_mod_one_one_on
Proof state before:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
⊢ a1 ∈ Set_rp_below (m * n) → a2 ∈ Set_rp_below (m * n) → mod_mod m n a1 = mod_mod m n a2 → a1 = a2
Tactic:
assume h2 : a1 ∈ Set_rp_below (m * n)
Proof state after:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : a1 ∈ Set_rp_below (m * n)
⊢ a2 ∈ Set_rp_below (m * n) → mod_mod m n a1 = mod_mod m n a2 → a1 = a2
Theorem: HTPI.mod_mod_one_one_on
Proof state before:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : a1 ∈ Set_rp_below (m * n)
⊢ a2 ∈ Set_rp_below (m * n) → mod_mod m n a1 = mod_mod m n a2 → a1 = a2
Tactic:
assume h3 : a2 ∈ Set_rp_below (m * n)
Proof state after:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : a1 ∈ Set_rp_below (m * n)
h3 : a2 ∈ Set_rp_below (m * n)
⊢ mod_mod m n a1 = mod_mod m n a2 → a1 = a2
Theorem: HTPI.mod_mod_one_one_on
Proof state before:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : a1 ∈ Set_rp_below (m * n)
h3 : a2 ∈ Set_rp_below (m * n)
⊢ mod_mod m n a1 = mod_mod m n a2 → a1 = a2
Tactic:
assume h4 : mod_mod m n a1 = mod_mod m n a2
Proof state after:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : a1 ∈ Set_rp_below (m * n)
h3 : a2 ∈ Set_rp_below (m * n)
h4 : mod_mod m n a1 = mod_mod m n a2
⊢ a1 = a2
Theorem: HTPI.mod_mod_one_one_on
Proof state before:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : a1 ∈ Set_rp_below (m * n)
h3 : a2 ∈ Set_rp_below (m * n)
h4 : mod_mod m n a1 = mod_mod m n a2
⊢ a1 = a2
Tactic:
define at h2
Proof state after:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : rel_prime (m * n) a1 ∧ a1 < m * n
h3 : a2 ∈ Set_rp_below (m * n)
h4 : mod_mod m n a1 = mod_mod m n a2
⊢ a1 = a2
Theorem: HTPI.mod_mod_one_one_on
Proof state before:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : rel_prime (m * n) a1 ∧ a1 < m * n
h3 : a2 ∈ Set_rp_below (m * n)
h4 : mod_mod m n a1 = mod_mod m n a2
⊢ a1 = a2
Tactic:
define at h3
Proof state after:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : rel_prime (m * n) a1 ∧ a1 < m * n
h3 : rel_prime (m * n) a2 ∧ a2 < m * n
h4 : mod_mod m n a1 = mod_mod m n a2
⊢ a1 = a2
Theorem: HTPI.mod_mod_one_one_on
Proof state before:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : rel_prime (m * n) a1 ∧ a1 < m * n
h3 : rel_prime (m * n) a2 ∧ a2 < m * n
h4 : mod_mod m n a1 = mod_mod m n a2
⊢ a1 = a2
Tactic:
rewrite [mod_mod_def, mod_mod_def] at h4
Proof state after:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : rel_prime (m * n) a1 ∧ a1 < m * n
h3 : rel_prime (m * n) a2 ∧ a2 < m * n
h4 : (a1 % m, a1 % n) = (a2 % m, a2 % n)
⊢ a1 = a2
Theorem: HTPI.mod_mod_one_one_on
Proof state before:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : rel_prime (m * n) a1 ∧ a1 < m * n
h3 : rel_prime (m * n) a2 ∧ a2 < m * n
h4 : (a1 % m, a1 % n) = (a2 % m, a2 % n)
⊢ a1 = a2
Tactic:
have h5 : a1 % m = a2 % m ∧ a1 % n = a2 % n := Prod.mk.inj h4
Proof state after:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : rel_prime (m * n) a1 ∧ a1 < m * n
h3 : rel_prime (m * n) a2 ∧ a2 < m * n
h4 : (a1 % m, a1 % n) = (a2 % m, a2 % n)
h5 : a1 % m = a2 % m ∧ a1 % n = a2 % n
⊢ a1 = a2
Theorem: HTPI.mod_mod_one_one_on
Proof state before:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : rel_prime (m * n) a1 ∧ a1 < m * n
h3 : rel_prime (m * n) a2 ∧ a2 < m * n
h4 : (a1 % m, a1 % n) = (a2 % m, a2 % n)
h5 : a1 % m = a2 % m ∧ a1 % n = a2 % n
⊢ a1 = a2
Tactic:
have h6 : m * n ≠ 0 := by linarith
Proof state after:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : rel_prime (m * n) a1 ∧ a1 < m * n
h3 : rel_prime (m * n) a2 ∧ a2 < m * n
h4 : (a1 % m, a1 % n) = (a2 % m, a2 % n)
h5 : a1 % m = a2 % m ∧ a1 % n = a2 % n
h6 : m * n ≠ 0
⊢ a1 = a2
Theorem: HTPI.mod_mod_one_one_on
Proof state before:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : rel_prime (m * n) a1 ∧ a1 < m * n
h3 : rel_prime (m * n) a2 ∧ a2 < m * n
h4 : (a1 % m, a1 % n) = (a2 % m, a2 % n)
h5 : a1 % m = a2 % m ∧ a1 % n = a2 % n
h6 : m * n ≠ 0
⊢ a1 = a2
Tactic:
have h7 : NeZero m := left_NeZero_of_mul h6
Proof state after:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : rel_prime (m * n) a1 ∧ a1 < m * n
h3 : rel_prime (m * n) a2 ∧ a2 < m * n
h4 : (a1 % m, a1 % n) = (a2 % m, a2 % n)
h5 : a1 % m = a2 % m ∧ a1 % n = a2 % n
h6 : m * n ≠ 0
h7 : NeZero m
⊢ a1 = a2
Theorem: HTPI.mod_mod_one_one_on
Proof state before:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : rel_prime (m * n) a1 ∧ a1 < m * n
h3 : rel_prime (m * n) a2 ∧ a2 < m * n
h4 : (a1 % m, a1 % n) = (a2 % m, a2 % n)
h5 : a1 % m = a2 % m ∧ a1 % n = a2 % n
h6 : m * n ≠ 0
h7 : NeZero m
⊢ a1 = a2
Tactic:
have h8 : NeZero n := right_NeZero_of_mul h6
Proof state after:
m n : ℕ
h1 : rel_prime m n
a1 a2 : ℕ
h2 : rel_prime (m * n) a1 ∧ a1 < m * n
h3 : rel_prime (m * n) a2 ∧ a2 < m * n
h4 : (a1 % m, a1 % n) = (a2 % m, a2 % n)
h5 : a1 % m = a2 % m ∧ a1 % n = a2 % n
h6 : m * n ≠ 0
h7 : NeZero m
h8 : NeZero n
⊢ a1 = a2