Theorem: HTPI.Theorem_7_3_1 (HTPILib/Chap7.lean)

State before:
m : ℕ
inst✝ : NeZero m
a : ℤ
⊢ ∃! r, 0 ≤ r ∧ r < ↑m ∧ a ≡ r (MOD m)
Tactic:
exists_unique
State after:
case Existence
m : ℕ
inst✝ : NeZero m
a : ℤ
⊢ ∃ r, 0 ≤ r ∧ r < ↑m ∧ a ≡ r (MOD m)

case Uniqueness
m : ℕ
inst✝ : NeZero m
a : ℤ
⊢ ∀ (r_1 r_2 : ℤ), 0 ≤ r_1 ∧ r_1 < ↑m ∧ a ≡ r_1 (MOD m) → 0 ≤ r_2 ∧ r_2 < ↑m ∧ a ≡ r_2 (MOD m) → r_1 = r_2

State before:
case Existence
m : ℕ
inst✝ : NeZero m
a : ℤ
⊢ ∃ r, 0 ≤ r ∧ r < ↑m ∧ a ≡ r (MOD m)
Tactic:
apply Exists.intro (a % m)
State after:
case Existence
m : ℕ
inst✝ : NeZero m
a : ℤ
⊢ 0 ≤ a % ↑m ∧ a % ↑m < ↑m ∧ a ≡ a % ↑m (MOD m)

State before:
case Existence
m : ℕ
inst✝ : NeZero m
a : ℤ
⊢ 0 ≤ a % ↑m ∧ a % ↑m < ↑m ∧ a ≡ a % ↑m (MOD m)
Tactic:
show 0 ≤ a % m ∧ a % m < m ∧ a ≡ a % m (MOD m) from
  mod_cmpl_res m a
State after:
no goals

State before:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a : ℤ
⊢ ∀ (r_1 r_2 : ℤ), 0 ≤ r_1 ∧ r_1 < ↑m ∧ a ≡ r_1 (MOD m) → 0 ≤ r_2 ∧ r_2 < ↑m ∧ a ≡ r_2 (MOD m) → r_1 = r_2
Tactic:
fix r1 : Int
State after:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 : ℤ
⊢ ∀ (r_2 : ℤ), 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m) → 0 ≤ r_2 ∧ r_2 < ↑m ∧ a ≡ r_2 (MOD m) → r1 = r_2

State before:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 : ℤ
⊢ ∀ (r_2 : ℤ), 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m) → 0 ≤ r_2 ∧ r_2 < ↑m ∧ a ≡ r_2 (MOD m) → r1 = r_2
Tactic:
fix r2 : Int
State after:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
⊢ 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m) → 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m) → r1 = r2

State before:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
⊢ 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m) → 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m) → r1 = r2
Tactic:
assume h1 : 0 ≤ r1 ∧ r1 < m ∧ a ≡ r1 (MOD m)
State after:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
⊢ 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m) → r1 = r2

State before:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
⊢ 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m) → r1 = r2
Tactic:
assume h2 : 0 ≤ r2 ∧ r2 < m ∧ a ≡ r2 (MOD m)
State after:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
⊢ r1 = r2

State before:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
⊢ r1 = r2
Tactic:
have h3 : r1 ≡ r2 (MOD m) :=
  congr_trans (congr_symm h1.right.right) h2.right.right
State after:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
⊢ r1 = r2

State before:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
⊢ r1 = r2
Tactic:
obtain (d : Int) (h4 : r1 - r2 = m * d) from h3
State after:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
⊢ r1 = r2

State before:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
⊢ r1 = r2
Tactic:
have h5 : r1 - r2 < m * 1 := by linarith
State after:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : r1 - r2 < ↑m * 1
⊢ r1 = r2

State before:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : r1 - r2 < ↑m * 1
⊢ r1 = r2
Tactic:
have h6 : m * (-1) < r1 - r2 := by linarith
State after:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : r1 - r2 < ↑m * 1
h6 : ↑m * -1 < r1 - r2
⊢ r1 = r2

State before:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : r1 - r2 < ↑m * 1
h6 : ↑m * -1 < r1 - r2
⊢ r1 = r2
Tactic:
rewrite [h4] at h5
State after:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : ↑m * d < ↑m * 1
h6 : ↑m * -1 < r1 - r2
⊢ r1 = r2

State before:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : ↑m * d < ↑m * 1
h6 : ↑m * -1 < r1 - r2
⊢ r1 = r2
Tactic:
rewrite [h4] at h6
State after:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : ↑m * d < ↑m * 1
h6 : ↑m * -1 < ↑m * d
⊢ r1 = r2

State before:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : ↑m * d < ↑m * 1
h6 : ↑m * -1 < ↑m * d
⊢ r1 = r2
Tactic:
have h7 : (↑m : Int) ≥ 0 := Nat.cast_nonneg m
State after:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : ↑m * d < ↑m * 1
h6 : ↑m * -1 < ↑m * d
h7 : ↑m ≥ 0
⊢ r1 = r2

State before:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : ↑m * d < ↑m * 1
h6 : ↑m * -1 < ↑m * d
h7 : ↑m ≥ 0
⊢ r1 = r2
Tactic:
have h8 : d < 1 := lt_of_mul_lt_mul_of_nonneg_left h5 h7
State after:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : ↑m * d < ↑m * 1
h6 : ↑m * -1 < ↑m * d
h7 : ↑m ≥ 0
h8 : d < 1
⊢ r1 = r2

State before:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : ↑m * d < ↑m * 1
h6 : ↑m * -1 < ↑m * d
h7 : ↑m ≥ 0
h8 : d < 1
⊢ r1 = r2
Tactic:
have h9 : -1 < d := lt_of_mul_lt_mul_of_nonneg_left h6 h7
State after:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : ↑m * d < ↑m * 1
h6 : ↑m * -1 < ↑m * d
h7 : ↑m ≥ 0
h8 : d < 1
h9 : -1 < d
⊢ r1 = r2

State before:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : ↑m * d < ↑m * 1
h6 : ↑m * -1 < ↑m * d
h7 : ↑m ≥ 0
h8 : d < 1
h9 : -1 < d
⊢ r1 = r2
Tactic:
have h10 : d = 0 := by linarith
State after:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : ↑m * d < ↑m * 1
h6 : ↑m * -1 < ↑m * d
h7 : ↑m ≥ 0
h8 : d < 1
h9 : -1 < d
h10 : d = 0
⊢ r1 = r2

State before:
case Uniqueness
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : ↑m * d < ↑m * 1
h6 : ↑m * -1 < ↑m * d
h7 : ↑m ≥ 0
h8 : d < 1
h9 : -1 < d
h10 : d = 0
⊢ r1 = r2
Tactic:
show r1 = r2 from
  calc r1
    _ = r1 - r2 + r2 := by ring
    _ = m * 0 + r2 := by rw [h4, h10]
    _ = r2 := by ring
State after:
no goals

State before:
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
⊢ r1 - r2 < ↑m * 1
Tactic:
linarith
State after:
no goals

State before:
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : r1 - r2 < ↑m * 1
⊢ ↑m * -1 < r1 - r2
Tactic:
linarith
State after:
no goals

State before:
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : ↑m * d < ↑m * 1
h6 : ↑m * -1 < ↑m * d
h7 : ↑m ≥ 0
h8 : d < 1
h9 : -1 < d
⊢ d = 0
Tactic:
linarith
State after:
no goals

State before:
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : ↑m * d < ↑m * 1
h6 : ↑m * -1 < ↑m * d
h7 : ↑m ≥ 0
h8 : d < 1
h9 : -1 < d
h10 : d = 0
⊢ r1 = r1 - r2 + r2
Tactic:
ring
State after:
no goals

State before:
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : ↑m * d < ↑m * 1
h6 : ↑m * -1 < ↑m * d
h7 : ↑m ≥ 0
h8 : d < 1
h9 : -1 < d
h10 : d = 0
⊢ r1 - r2 + r2 = ↑m * 0 + r2
Tactic:
rw [h4, h10]
State after:
no goals

State before:
m : ℕ
inst✝ : NeZero m
a r1 r2 : ℤ
h1 : 0 ≤ r1 ∧ r1 < ↑m ∧ a ≡ r1 (MOD m)
h2 : 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m)
h3 : r1 ≡ r2 (MOD m)
d : ℤ
h4 : r1 - r2 = ↑m * d
h5 : ↑m * d < ↑m * 1
h6 : ↑m * -1 < ↑m * d
h7 : ↑m ≥ 0
h8 : d < 1
h9 : -1 < d
h10 : d = 0
⊢ ↑m * 0 + r2 = r2
Tactic:
ring
State after:
no goals