internlm/Lean-Github huggingface dataset:
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
h8 : NeZero n
⊢ a1 = a2
Tactic:
rewrite [←congr_iff_mod_eq_Nat, ←congr_iff_mod_eq_Nat] at h5
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 ≡ ↑a2 (MOD m) ∧ ↑a1 ≡ ↑a2 (MOD n)
h6 : m * n ≠ 0
h7 : NeZero m
h8 : NeZero 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 ≡ ↑a2 (MOD m) ∧ ↑a1 ≡ ↑a2 (MOD n)
h6 : m * n ≠ 0
h7 : NeZero m
h8 : NeZero n
⊢ a1 = a2
Tactic:
rewrite [←Lemma_7_4_5 _ _ h1] at h5
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 ≡ ↑a2 (MOD m * n)
h6 : m * n ≠ 0
h7 : NeZero m
h8 : NeZero 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 ≡ ↑a2 (MOD m * n)
h6 : m * n ≠ 0
h7 : NeZero m
h8 : NeZero n
⊢ a1 = a2
Tactic:
rewrite [congr_iff_mod_eq_Nat] at h5
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 * n) = a2 % (m * n)
h6 : m * n ≠ 0
h7 : NeZero m
h8 : NeZero 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 * n) = a2 % (m * n)
h6 : m * n ≠ 0
h7 : NeZero m
h8 : NeZero n
⊢ a1 = a2
Tactic:
rewrite [Nat.mod_eq_of_lt h2.right, Nat.mod_eq_of_lt h3.right] at h5
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 = a2
h6 : m * n ≠ 0
h7 : NeZero m
h8 : NeZero 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 = a2
h6 : m * n ≠ 0
h7 : NeZero m
h8 : NeZero n
⊢ a1 = a2
Tactic:
show a1 = a2 from h5
Proof state after:
no goals
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
⊢ m * n ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.mod_elt_Set_rp_below
Proof state before:
a m : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ a % m ∈ Set_rp_below m
Tactic:
define
Proof state after:
a m : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ rel_prime m (a % m) ∧ a % m < m
Theorem: HTPI.mod_elt_Set_rp_below
Proof state before:
a m : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ rel_prime m (a % m) ∧ a % m < m
Tactic:
rewrite [rel_prime_mod]
Proof state after:
a m : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ rel_prime m a ∧ a % m < m
Theorem: HTPI.mod_elt_Set_rp_below
Proof state before:
a m : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ rel_prime m a ∧ a % m < m
Tactic:
show rel_prime m a ∧ a % m < m from
  And.intro h1 (mod_nonzero_lt a (NeZero.ne m))
Proof state after:
no goals
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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))
Theorem: HTPI.mod_mod_image
Proof 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))
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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]
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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
Proof state after:
no goals
Theorem: HTPI.mod_mod_image
Proof 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
Proof state after:
no goals
Theorem: HTPI.mod_mod_image
Proof 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
Proof state after:
no goals
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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))
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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))
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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)
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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)
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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)
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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)
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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)
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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)
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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)
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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)
Theorem: HTPI.mod_mod_image
Proof 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
Proof state after:
no goals
Theorem: HTPI.mod_mod_image
Proof 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
Proof state after:
no goals
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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]
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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]
Proof 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
Theorem: HTPI.mod_mod_image
Proof 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
Proof state after:
no goals
Theorem: HTPI.mod_mod_image
Proof 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
Proof 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)
Theorem: HTPI.mod_mod_image
Proof 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]
Proof 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)
Theorem: HTPI.mod_mod_image
Proof 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]
Proof 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)
Theorem: HTPI.mod_mod_image
Proof 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
Proof state after:
no goals