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

State before:
m n : ℕ
h1 : rel_prime m n
⊢ one_one_on (mod_mod m n) (Set_rp_below (m * n))
Tactic:
define
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

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
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

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
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

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)
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

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)
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals