internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_1
Proof 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]
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_6_1
Proof state before:
m : ℕ
X Y : ZMod m
⊢ X + Y = Y + X
Tactic:
obtain (a : Int) (h1 : X = [a]_m) from cc_rep X
Proof state after:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
⊢ X + Y = Y + X
Theorem: HTPI.Theorem_7_3_6_1
Proof state before:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
⊢ X + Y = Y + X
Tactic:
obtain (b : Int) (h2 : Y = [b]_m) from cc_rep Y
Proof state after:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
b : ℤ
h2 : Y = [b]_m
⊢ X + Y = Y + X
Theorem: HTPI.Theorem_7_3_6_1
Proof state before:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
b : ℤ
h2 : Y = [b]_m
⊢ X + Y = Y + X
Tactic:
rewrite [h1, h2]
Proof state after:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
b : ℤ
h2 : Y = [b]_m
⊢ [a]_m + [b]_m = [b]_m + [a]_m
Theorem: HTPI.Theorem_7_3_6_1
Proof state before:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
b : ℤ
h2 : Y = [b]_m
⊢ [a]_m + [b]_m = [b]_m + [a]_m
Tactic:
have h3 : a + b = b + a := by ring
Proof state after:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
b : ℤ
h2 : Y = [b]_m
h3 : a + b = b + a
⊢ [a]_m + [b]_m = [b]_m + [a]_m
Theorem: HTPI.Theorem_7_3_6_1
Proof state before:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
b : ℤ
h2 : Y = [b]_m
h3 : a + b = b + a
⊢ [a]_m + [b]_m = [b]_m + [a]_m
Tactic:
show [a]_m + [b]_m = [b]_m + [a]_m from
  calc [a]_m + [b]_m
    _ = [a + b]_m := add_class m a b
    _ = [b + a]_m := by rw [h3]
    _ = [b]_m + [a]_m := (add_class m b a).symm
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_6_1
Proof state before:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
b : ℤ
h2 : Y = [b]_m
⊢ a + b = b + a
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_6_1
Proof state before:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
b : ℤ
h2 : Y = [b]_m
h3 : a + b = b + a
⊢ [a + b]_m = [b + a]_m
Tactic:
rw [h3]
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_6_7
Proof state before:
m : ℕ
X : ZMod m
⊢ X * [1]_m = X
Tactic:
obtain (a : Int) (h1 : X = [a]_m) from cc_rep X
Proof state after:
m : ℕ
X : ZMod m
a : ℤ
h1 : X = [a]_m
⊢ X * [1]_m = X
Theorem: HTPI.Theorem_7_3_6_7
Proof state before:
m : ℕ
X : ZMod m
a : ℤ
h1 : X = [a]_m
⊢ X * [1]_m = X
Tactic:
rewrite [h1]
Proof state after:
m : ℕ
X : ZMod m
a : ℤ
h1 : X = [a]_m
⊢ [a]_m * [1]_m = [a]_m
Theorem: HTPI.Theorem_7_3_6_7
Proof state before:
m : ℕ
X : ZMod m
a : ℤ
h1 : X = [a]_m
⊢ [a]_m * [1]_m = [a]_m
Tactic:
have h2 : a * 1 = a := by ring
Proof state after:
m : ℕ
X : ZMod m
a : ℤ
h1 : X = [a]_m
h2 : a * 1 = a
⊢ [a]_m * [1]_m = [a]_m
Theorem: HTPI.Theorem_7_3_6_7
Proof state before:
m : ℕ
X : ZMod m
a : ℤ
h1 : X = [a]_m
h2 : a * 1 = a
⊢ [a]_m * [1]_m = [a]_m
Tactic:
show [a]_m * [1]_m = [a]_m from
  calc [a]_m * [1]_m
    _ = [a * 1]_m := mul_class m a 1
    _ = [a]_m := by rw [h2]
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_6_7
Proof state before:
m : ℕ
X : ZMod m
a : ℤ
h1 : X = [a]_m
⊢ a * 1 = a
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_6_7
Proof state before:
m : ℕ
X : ZMod m
a : ℤ
h1 : X = [a]_m
h2 : a * 1 = a
⊢ [a * 1]_m = [a]_m
Tactic:
rw [h2]
Proof state after:
no goals
Theorem: HTPI.gcd_c2_inv
Proof state before:
m a : ℕ
h1 : rel_prime m a
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m
Tactic:
set s : Int := gcd_c1 m a
Proof state after:
m a : ℕ
h1 : rel_prime m a
s : ℤ := gcd_c1 m a
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m
Theorem: HTPI.gcd_c2_inv
Proof state before:
m a : ℕ
h1 : rel_prime m a
s : ℤ := gcd_c1 m a
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m
Tactic:
have h2 : s * m + (gcd_c2 m a) * a = gcd m a := gcd_lin_comb a m
Proof state after:
m a : ℕ
h1 : rel_prime m a
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = ↑(gcd m a)
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m
Theorem: HTPI.gcd_c2_inv
Proof state before:
m a : ℕ
h1 : rel_prime m a
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = ↑(gcd m a)
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m
Tactic:
define at h1
Proof state after:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = ↑(gcd m a)
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m
Theorem: HTPI.gcd_c2_inv
Proof state before:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = ↑(gcd m a)
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m
Tactic:
rewrite [h1, Nat.cast_one] at h2
Proof state after:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m
Theorem: HTPI.gcd_c2_inv
Proof state before:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ [↑a]_m * [gcd_c2 m a]_m = [1]_m
Tactic:
rewrite [mul_class, cc_eq_iff_congr]
Proof state after:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ ↑a * gcd_c2 m a ≡ 1 (MOD m)
Theorem: HTPI.gcd_c2_inv
Proof state before:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ ↑a * gcd_c2 m a ≡ 1 (MOD m)
Tactic:
define
Proof state after:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ ∃ c, ↑a * gcd_c2 m a - 1 = ↑m * c
Theorem: HTPI.gcd_c2_inv
Proof state before:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ ∃ c, ↑a * gcd_c2 m a - 1 = ↑m * c
Tactic:
apply Exists.intro (-s)
Proof state after:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ ↑a * gcd_c2 m a - 1 = ↑m * -s
Theorem: HTPI.gcd_c2_inv
Proof state before:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ ↑a * gcd_c2 m a - 1 = ↑m * -s
Tactic:
show a * (gcd_c2 m a) - 1 = m * (-s) from
  calc a * (gcd_c2 m a) - 1
    _ = s * m + (gcd_c2 m a) * a + m * (-s) - 1 := by ring
    _ = 1 + m * (-s) - 1 := by rw [h2]
    _ = m * (-s) := by ring
Proof state after:
no goals
Theorem: HTPI.gcd_c2_inv
Proof state before:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ ↑a * gcd_c2 m a - 1 = s * ↑m + gcd_c2 m a * ↑a + ↑m * -s - 1
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.gcd_c2_inv
Proof state before:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ s * ↑m + gcd_c2 m a * ↑a + ↑m * -s - 1 = 1 + ↑m * -s - 1
Tactic:
rw [h2]
Proof state after:
no goals
Theorem: HTPI.gcd_c2_inv
Proof state before:
m a : ℕ
h1 : gcd m a = 1
s : ℤ := gcd_c1 m a
h2 : s * ↑m + gcd_c2 m a * ↑a = 1
⊢ 1 + ↑m * -s - 1 = ↑m * -s
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_7
Proof state before:
m a : ℕ
⊢ invertible [↑a]_m ↔ rel_prime m a
Tactic:
apply Iff.intro
Proof state after:
case mp
m a : ℕ
⊢ invertible [↑a]_m → rel_prime m a

case mpr
m a : ℕ
⊢ rel_prime m a → invertible [↑a]_m
Theorem: HTPI.Theorem_7_3_7
Proof state before:
case mp
m a : ℕ
⊢ invertible [↑a]_m → rel_prime m a
Tactic:
assume h1 : invertible [a]_m
Proof state after:
case mp
m a : ℕ
h1 : invertible [↑a]_m
⊢ rel_prime m a
Theorem: HTPI.Theorem_7_3_7
Proof state before:
case mp
m a : ℕ
h1 : invertible [↑a]_m
⊢ rel_prime m a
Tactic:
define at h1
Proof state after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
⊢ rel_prime m a
Theorem: HTPI.Theorem_7_3_7
Proof state before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
⊢ rel_prime m a
Tactic:
obtain (Y : ZMod m) (h2 : [a]_m * Y = [1]_m) from h1
Proof state after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
h2 : [↑a]_m * Y = [1]_m
⊢ rel_prime m a
Theorem: HTPI.Theorem_7_3_7
Proof state before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
h2 : [↑a]_m * Y = [1]_m
⊢ rel_prime m a
Tactic:
obtain (b : Int) (h3 : Y = [b]_m) from cc_rep Y
Proof state after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
h2 : [↑a]_m * Y = [1]_m
b : ℤ
h3 : Y = [b]_m
⊢ rel_prime m a
Theorem: HTPI.Theorem_7_3_7
Proof state before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
h2 : [↑a]_m * Y = [1]_m
b : ℤ
h3 : Y = [b]_m
⊢ rel_prime m a
Tactic:
rewrite [h3, mul_class, cc_eq_iff_congr] at h2
Proof state after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ↑a * b ≡ 1 (MOD m)
h3 : Y = [b]_m
⊢ rel_prime m a
Theorem: HTPI.Theorem_7_3_7
Proof state before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ↑a * b ≡ 1 (MOD m)
h3 : Y = [b]_m
⊢ rel_prime m a
Tactic:
define at h2
Proof state after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
⊢ rel_prime m a
Theorem: HTPI.Theorem_7_3_7
Proof state before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
⊢ rel_prime m a
Tactic:
obtain (c : Int) (h4 : a * b - 1 = m * c) from h2
Proof state after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ rel_prime m a
Theorem: HTPI.Theorem_7_3_7
Proof state before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ rel_prime m a
Tactic:
rewrite [Exercise_7_2_6]
Proof state after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ ∃ s t, s * ↑m + t * ↑a = 1
Theorem: HTPI.Theorem_7_3_7
Proof state before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ ∃ s t, s * ↑m + t * ↑a = 1
Tactic:
apply Exists.intro (-c)
Proof state after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ ∃ t, -c * ↑m + t * ↑a = 1
Theorem: HTPI.Theorem_7_3_7
Proof state before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ ∃ t, -c * ↑m + t * ↑a = 1
Tactic:
apply Exists.intro b
Proof state after:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ -c * ↑m + b * ↑a = 1
Theorem: HTPI.Theorem_7_3_7
Proof state before:
case mp
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ -c * ↑m + b * ↑a = 1
Tactic:
show (-c) * m + b * a = 1 from
  calc (-c) * m + b * a
    _ = (-c) * m + (a * b - 1) + 1 := by ring
    _ = (-c) * m + m * c + 1 := by rw [h4]
    _ = 1 := by ring
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_7
Proof state before:
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ -c * ↑m + b * ↑a = -c * ↑m + (↑a * b - 1) + 1
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_7
Proof state before:
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ -c * ↑m + (↑a * b - 1) + 1 = -c * ↑m + ↑m * c + 1
Tactic:
rw [h4]
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_7
Proof state before:
m a : ℕ
h1 : ∃ Y, [↑a]_m * Y = [1]_m
Y : ZMod m
b : ℤ
h2 : ∃ c, ↑a * b - 1 = ↑m * c
h3 : Y = [b]_m
c : ℤ
h4 : ↑a * b - 1 = ↑m * c
⊢ -c * ↑m + ↑m * c + 1 = 1
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_7
Proof state before:
case mpr
m a : ℕ
⊢ rel_prime m a → invertible [↑a]_m
Tactic:
assume h1 : rel_prime m a
Proof state after:
case mpr
m a : ℕ
h1 : rel_prime m a
⊢ invertible [↑a]_m
Theorem: HTPI.Theorem_7_3_7
Proof state before:
case mpr
m a : ℕ
h1 : rel_prime m a
⊢ invertible [↑a]_m
Tactic:
define
Proof state after:
case mpr
m a : ℕ
h1 : rel_prime m a
⊢ ∃ Y, [↑a]_m * Y = [1]_m
Theorem: HTPI.Theorem_7_3_7
Proof state before:
case mpr
m a : ℕ
h1 : rel_prime m a
⊢ ∃ Y, [↑a]_m * Y = [1]_m
Tactic:
show ∃ (Y : ZMod m), [a]_m * Y = [1]_m from
  Exists.intro [gcd_c2 m a]_m (gcd_c2_inv h1)
Proof state after:
no goals
Theorem: HTPI.num_rp_below_base
Proof state before:
m : ℕ
⊢ num_rp_below m 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.num_rp_below_step_rp
Proof state before:
m j : ℕ
h : rel_prime m j
⊢ num_rp_below m (j + 1) = num_rp_below m j + 1
Tactic:
have h1 : num_rp_below m (j + 1) =
  if gcd m j = 1 then (num_rp_below m j) + 1
  else num_rp_below m j := by rfl
Proof state after:
m j : ℕ
h : rel_prime m j
h1 : num_rp_below m (j + 1) = if gcd m j = 1 then num_rp_below m j + 1 else num_rp_below m j
⊢ num_rp_below m (j + 1) = num_rp_below m j + 1
Theorem: HTPI.num_rp_below_step_rp
Proof state before:
m j : ℕ
h : rel_prime m j
h1 : num_rp_below m (j + 1) = if gcd m j = 1 then num_rp_below m j + 1 else num_rp_below m j
⊢ num_rp_below m (j + 1) = num_rp_below m j + 1
Tactic:
define at h
Proof state after:
m j : ℕ
h : gcd m j = 1
h1 : num_rp_below m (j + 1) = if gcd m j = 1 then num_rp_below m j + 1 else num_rp_below m j
⊢ num_rp_below m (j + 1) = num_rp_below m j + 1
Theorem: HTPI.num_rp_below_step_rp
Proof state before:
m j : ℕ
h : gcd m j = 1
h1 : num_rp_below m (j + 1) = if gcd m j = 1 then num_rp_below m j + 1 else num_rp_below m j
⊢ num_rp_below m (j + 1) = num_rp_below m j + 1
Tactic:
rewrite [if_pos h] at h1
Proof state after:
m j : ℕ
h : gcd m j = 1
h1 : num_rp_below m (j + 1) = num_rp_below m j + 1
⊢ num_rp_below m (j + 1) = num_rp_below m j + 1
Theorem: HTPI.num_rp_below_step_rp
Proof state before:
m j : ℕ
h : gcd m j = 1
h1 : num_rp_below m (j + 1) = num_rp_below m j + 1
⊢ num_rp_below m (j + 1) = num_rp_below m j + 1
Tactic:
show num_rp_below m (j + 1) = num_rp_below m j + 1 from h1
Proof state after:
no goals
Theorem: HTPI.num_rp_below_step_rp
Proof state before:
m j : ℕ
h : rel_prime m j
⊢ num_rp_below m (j + 1) = if gcd m j = 1 then num_rp_below m j + 1 else num_rp_below m j
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.num_rp_below_step_not_rp
Proof state before:
m j : ℕ
h : ¬rel_prime m j
⊢ num_rp_below m (j + 1) = num_rp_below m j
Tactic:
have h1 : num_rp_below m (j +1) =
  if gcd m j = 1 then (num_rp_below m j) + 1
  else num_rp_below m j := by rfl
Proof state after:
m j : ℕ
h : ¬rel_prime m j
h1 : num_rp_below m (j + 1) = if gcd m j = 1 then num_rp_below m j + 1 else num_rp_below m j
⊢ num_rp_below m (j + 1) = num_rp_below m j
Theorem: HTPI.num_rp_below_step_not_rp
Proof state before:
m j : ℕ
h : ¬rel_prime m j
h1 : num_rp_below m (j + 1) = if gcd m j = 1 then num_rp_below m j + 1 else num_rp_below m j
⊢ num_rp_below m (j + 1) = num_rp_below m j
Tactic:
define at h
Proof state after:
m j : ℕ
h : ¬gcd m j = 1
h1 : num_rp_below m (j + 1) = if gcd m j = 1 then num_rp_below m j + 1 else num_rp_below m j
⊢ num_rp_below m (j + 1) = num_rp_below m j
Theorem: HTPI.num_rp_below_step_not_rp
Proof state before:
m j : ℕ
h : ¬gcd m j = 1
h1 : num_rp_below m (j + 1) = if gcd m j = 1 then num_rp_below m j + 1 else num_rp_below m j
⊢ num_rp_below m (j + 1) = num_rp_below m j
Tactic:
rewrite [if_neg h] at h1
Proof state after:
m j : ℕ
h : ¬gcd m j = 1
h1 : num_rp_below m (j + 1) = num_rp_below m j
⊢ num_rp_below m (j + 1) = num_rp_below m j
Theorem: HTPI.num_rp_below_step_not_rp
Proof state before:
m j : ℕ
h : ¬gcd m j = 1
h1 : num_rp_below m (j + 1) = num_rp_below m j
⊢ num_rp_below m (j + 1) = num_rp_below m j
Tactic:
show num_rp_below m (j + 1) = num_rp_below m j from h1
Proof state after:
no goals
Theorem: HTPI.num_rp_below_step_not_rp
Proof state before:
m j : ℕ
h : ¬rel_prime m j
⊢ num_rp_below m (j + 1) = if gcd m j = 1 then num_rp_below m j + 1 else num_rp_below m j
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.phi_def
Proof state before:
m : ℕ
⊢ phi m = num_rp_below m m
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.prod_inv_iff_inv
Proof state before:
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
⊢ invertible (X * Y) ↔ invertible Y
Tactic:
apply Iff.intro
Proof state after:
case mp
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
⊢ invertible (X * Y) → invertible Y

case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
⊢ invertible Y → invertible (X * Y)
Theorem: HTPI.prod_inv_iff_inv
Proof state before:
case mp
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
⊢ invertible (X * Y) → invertible Y
Tactic:
assume h2 : invertible (X * Y)
Proof state after:
case mp
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible (X * Y)
⊢ invertible Y
Theorem: HTPI.prod_inv_iff_inv
Proof state before:
case mp
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible (X * Y)
⊢ invertible Y
Tactic:
obtain (Z : ZMod m) (h3 : X * Y * Z = [1]_m) from h2
Proof state after:
case mp
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible (X * Y)
Z : ZMod m
h3 : X * Y * Z = [1]_m
⊢ invertible Y