internlm/Lean-Github huggingface dataset:
Theorem: HTPI.fund_thm_arith
Proof state before:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 l2 : List ℕ
h1 : nondec_prime_list l1 ∧ prod l1 = n
h2 : nondec_prime_list l2 ∧ prod l2 = n
⊢ l1 = l2
Tactic:
have h3 : prod l1 = n := h1.right
Proof state after:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 l2 : List ℕ
h1 : nondec_prime_list l1 ∧ prod l1 = n
h2 : nondec_prime_list l2 ∧ prod l2 = n
h3 : prod l1 = n
⊢ l1 = l2
Theorem: HTPI.fund_thm_arith
Proof state before:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 l2 : List ℕ
h1 : nondec_prime_list l1 ∧ prod l1 = n
h2 : nondec_prime_list l2 ∧ prod l2 = n
h3 : prod l1 = n
⊢ l1 = l2
Tactic:
rewrite [←h2.right] at h3
Proof state after:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 l2 : List ℕ
h1 : nondec_prime_list l1 ∧ prod l1 = n
h2 : nondec_prime_list l2 ∧ prod l2 = n
h3 : prod l1 = prod l2
⊢ l1 = l2
Theorem: HTPI.fund_thm_arith
Proof state before:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 l2 : List ℕ
h1 : nondec_prime_list l1 ∧ prod l1 = n
h2 : nondec_prime_list l2 ∧ prod l2 = n
h3 : prod l1 = prod l2
⊢ l1 = l2
Tactic:
show l1 = l2 from Theorem_7_2_5 l1 l2 h1.left h2.left h3
Proof state after:
no goals
Theorem: HTPI.congr_refl
Proof state before:
m : ℕ
⊢ ∀ (a : ℤ), a ≡ a (MOD m)
Tactic:
fix a : Int
Proof state after:
m : ℕ
a : ℤ
⊢ a ≡ a (MOD m)
Theorem: HTPI.congr_refl
Proof state before:
m : ℕ
a : ℤ
⊢ a ≡ a (MOD m)
Tactic:
define
Proof state after:
m : ℕ
a : ℤ
⊢ ∃ c, a - a = ↑m * c
Theorem: HTPI.congr_refl
Proof state before:
m : ℕ
a : ℤ
⊢ ∃ c, a - a = ↑m * c
Tactic:
apply Exists.intro 0
Proof state after:
m : ℕ
a : ℤ
⊢ a - a = ↑m * 0
Theorem: HTPI.congr_refl
Proof state before:
m : ℕ
a : ℤ
⊢ a - a = ↑m * 0
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.congr_symm
Proof state before:
m : ℕ
⊢ ∀ {a b : ℤ}, a ≡ b (MOD m) → b ≡ a (MOD m)
Tactic:
fix a : Int
Proof state after:
m : ℕ
a : ℤ
⊢ ∀ {b : ℤ}, a ≡ b (MOD m) → b ≡ a (MOD m)
Theorem: HTPI.congr_symm
Proof state before:
m : ℕ
a : ℤ
⊢ ∀ {b : ℤ}, a ≡ b (MOD m) → b ≡ a (MOD m)
Tactic:
fix b : Int
Proof state after:
m : ℕ
a b : ℤ
⊢ a ≡ b (MOD m) → b ≡ a (MOD m)
Theorem: HTPI.congr_symm
Proof state before:
m : ℕ
a b : ℤ
⊢ a ≡ b (MOD m) → b ≡ a (MOD m)
Tactic:
assume h1 : a ≡ b (MOD m)
Proof state after:
m : ℕ
a b : ℤ
h1 : a ≡ b (MOD m)
⊢ b ≡ a (MOD m)
Theorem: HTPI.congr_symm
Proof state before:
m : ℕ
a b : ℤ
h1 : a ≡ b (MOD m)
⊢ b ≡ a (MOD m)
Tactic:
define at h1
Proof state after:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
⊢ b ≡ a (MOD m)
Theorem: HTPI.congr_symm
Proof state before:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
⊢ b ≡ a (MOD m)
Tactic:
define
Proof state after:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
⊢ ∃ c, b - a = ↑m * c
Theorem: HTPI.congr_symm
Proof state before:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
⊢ ∃ c, b - a = ↑m * c
Tactic:
obtain (c : Int) (h2 : a - b = m * c) from h1
Proof state after:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
c : ℤ
h2 : a - b = ↑m * c
⊢ ∃ c, b - a = ↑m * c
Theorem: HTPI.congr_symm
Proof state before:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
c : ℤ
h2 : a - b = ↑m * c
⊢ ∃ c, b - a = ↑m * c
Tactic:
apply Exists.intro (-c)
Proof state after:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
c : ℤ
h2 : a - b = ↑m * c
⊢ b - a = ↑m * -c
Theorem: HTPI.congr_symm
Proof state before:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
c : ℤ
h2 : a - b = ↑m * c
⊢ b - a = ↑m * -c
Tactic:
show b - a = m * (-c) from
  calc b - a
    _ = -(a - b) := by ring
    _ = -(m * c) := by rw [h2]
    _ = m * (-c) := by ring
Proof state after:
no goals
Theorem: HTPI.congr_symm
Proof state before:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
c : ℤ
h2 : a - b = ↑m * c
⊢ b - a = -(a - b)
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.congr_symm
Proof state before:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
c : ℤ
h2 : a - b = ↑m * c
⊢ -(a - b) = -(↑m * c)
Tactic:
rw [h2]
Proof state after:
no goals
Theorem: HTPI.congr_symm
Proof state before:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
c : ℤ
h2 : a - b = ↑m * c
⊢ -(↑m * c) = ↑m * -c
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.val_nat_eq_mod
Proof state before:
n k : ℕ
⊢ ZMod.val [↑k]_(n + 1) = k % (n + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.val_zero
Proof state before:
n : ℕ
⊢ ZMod.val [0]_(n + 1) = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.cc_rep
Proof state before:
m : ℕ
X : ZMod 0
⊢ ∃ a, X = [a]_0
Tactic:
apply Exists.intro X
Proof state after:
m : ℕ
X : ZMod 0
⊢ X = [X]_0
Theorem: HTPI.cc_rep
Proof state before:
m : ℕ
X : ZMod 0
⊢ X = [X]_0
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.cc_rep
Proof state before:
m n : ℕ
X : ZMod (n + 1)
⊢ ∃ a, X = [a]_(n + 1)
Tactic:
apply Exists.intro ↑(X.val)
Proof state after:
m n : ℕ
X : ZMod (n + 1)
⊢ X = [↑(ZMod.val X)]_(n + 1)
Theorem: HTPI.cc_rep
Proof state before:
m n : ℕ
X : ZMod (n + 1)
⊢ X = [↑(ZMod.val X)]_(n + 1)
Tactic:
have h1 : X.val < n + 1 := Fin.prop X
Proof state after:
m n : ℕ
X : ZMod (n + 1)
h1 : ZMod.val X < n + 1
⊢ X = [↑(ZMod.val X)]_(n + 1)
Theorem: HTPI.cc_rep
Proof state before:
m n : ℕ
X : ZMod (n + 1)
h1 : ZMod.val X < n + 1
⊢ X = [↑(ZMod.val X)]_(n + 1)
Tactic:
rewrite [cc_eq_iff_val_eq, val_nat_eq_mod, Nat.mod_eq_of_lt h1]
Proof state after:
m n : ℕ
X : ZMod (n + 1)
h1 : ZMod.val X < n + 1
⊢ ZMod.val X = ZMod.val X
Theorem: HTPI.cc_rep
Proof state before:
m n : ℕ
X : ZMod (n + 1)
h1 : ZMod.val X < n + 1
⊢ ZMod.val X = ZMod.val X
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
m : ℕ
a b : ℤ
⊢ [a]_m = [b]_m ↔ [a - b]_m = [0]_m
Tactic:
apply Iff.intro
Proof state after:
case mp
m : ℕ
a b : ℤ
⊢ [a]_m = [b]_m → [a - b]_m = [0]_m

case mpr
m : ℕ
a b : ℤ
⊢ [a - b]_m = [0]_m → [a]_m = [b]_m
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
case mp
m : ℕ
a b : ℤ
⊢ [a]_m = [b]_m → [a - b]_m = [0]_m
Tactic:
assume h1 : [a]_m = [b]_m
Proof state after:
case mp
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
⊢ [a - b]_m = [0]_m
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
case mp
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
⊢ [a - b]_m = [0]_m
Tactic:
have h2 : a - b = a + (-b) := by ring
Proof state after:
case mp
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
h2 : a - b = a + -b
⊢ [a - b]_m = [0]_m
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
case mp
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
h2 : a - b = a + -b
⊢ [a - b]_m = [0]_m
Tactic:
have h3 : b + (-b) = 0 := by ring
Proof state after:
case mp
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
h2 : a - b = a + -b
h3 : b + -b = 0
⊢ [a - b]_m = [0]_m
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
case mp
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
h2 : a - b = a + -b
h3 : b + -b = 0
⊢ [a - b]_m = [0]_m
Tactic:
show [a - b]_m = [0]_m from
  calc [a - b]_m
    _ = [a + (-b)]_m := by rw [h2]
    _ = [a]_m + [-b]_m := by rw [add_class]
    _ = [b]_m + [-b]_m := by rw [h1]
    _ = [b + -b]_m := by rw [add_class]
    _ = [0]_m := by rw [h3]
Proof state after:
no goals
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
⊢ a - b = a + -b
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
h2 : a - b = a + -b
⊢ b + -b = 0
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
h2 : a - b = a + -b
h3 : b + -b = 0
⊢ [a - b]_m = [a + -b]_m
Tactic:
rw [h2]
Proof state after:
no goals
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
h2 : a - b = a + -b
h3 : b + -b = 0
⊢ [a + -b]_m = [a]_m + [-b]_m
Tactic:
rw [add_class]
Proof state after:
no goals
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
h2 : a - b = a + -b
h3 : b + -b = 0
⊢ [a]_m + [-b]_m = [b]_m + [-b]_m
Tactic:
rw [h1]
Proof state after:
no goals
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
h2 : a - b = a + -b
h3 : b + -b = 0
⊢ [b]_m + [-b]_m = [b + -b]_m
Tactic:
rw [add_class]
Proof state after:
no goals
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
h2 : a - b = a + -b
h3 : b + -b = 0
⊢ [b + -b]_m = [0]_m
Tactic:
rw [h3]
Proof state after:
no goals
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
case mpr
m : ℕ
a b : ℤ
⊢ [a - b]_m = [0]_m → [a]_m = [b]_m
Tactic:
assume h1 : [a - b]_m = [0]_m
Proof state after:
case mpr
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
⊢ [a]_m = [b]_m
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
case mpr
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
⊢ [a]_m = [b]_m
Tactic:
have h2 : b + (a - b) = a := by ring
Proof state after:
case mpr
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
⊢ [a]_m = [b]_m
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
case mpr
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
⊢ [a]_m = [b]_m
Tactic:
have h3 : b + 0 = b := by ring
Proof state after:
case mpr
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
h3 : b + 0 = b
⊢ [a]_m = [b]_m
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
case mpr
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
h3 : b + 0 = b
⊢ [a]_m = [b]_m
Tactic:
show [a]_m = [b]_m from
  calc [a]_m
    _ = [b + (a - b)]_m := by rw [h2]
    _ = [b]_m + [a - b]_m := by rw [add_class]
    _ = [b]_m + [0]_m := by rw [h1]
    _ = [b + 0]_m := by rw [add_class]
    _ = [b]_m := by rw [h3]
Proof state after:
no goals
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
⊢ b + (a - b) = a
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
⊢ b + 0 = b
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
h3 : b + 0 = b
⊢ [a]_m = [b + (a - b)]_m
Tactic:
rw [h2]
Proof state after:
no goals
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
h3 : b + 0 = b
⊢ [b + (a - b)]_m = [b]_m + [a - b]_m
Tactic:
rw [add_class]
Proof state after:
no goals
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
h3 : b + 0 = b
⊢ [b]_m + [a - b]_m = [b]_m + [0]_m
Tactic:
rw [h1]
Proof state after:
no goals
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
h3 : b + 0 = b
⊢ [b]_m + [0]_m = [b + 0]_m
Tactic:
rw [add_class]
Proof state after:
no goals
Theorem: HTPI.cc_eq_iff_sub_zero
Proof state before:
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
h3 : b + 0 = b
⊢ [b + 0]_m = [b]_m
Tactic:
rw [h3]
Proof state after:
no goals
Theorem: HTPI.cc_neg_zero_of_cc_zero
Proof state before:
m : ℕ
a : ℤ
⊢ [a]_m = [0]_m → [-a]_m = [0]_m
Tactic:
assume h1 : [a]_m = [0]_m
Proof state after:
m : ℕ
a : ℤ
h1 : [a]_m = [0]_m
⊢ [-a]_m = [0]_m
Theorem: HTPI.cc_neg_zero_of_cc_zero
Proof state before:
m : ℕ
a : ℤ
h1 : [a]_m = [0]_m
⊢ [-a]_m = [0]_m
Tactic:
have h2 : 0 + (-a) = -a := by ring
Proof state after:
m : ℕ
a : ℤ
h1 : [a]_m = [0]_m
h2 : 0 + -a = -a
⊢ [-a]_m = [0]_m
Theorem: HTPI.cc_neg_zero_of_cc_zero
Proof state before:
m : ℕ
a : ℤ
h1 : [a]_m = [0]_m
h2 : 0 + -a = -a
⊢ [-a]_m = [0]_m
Tactic:
have h3 : a + (-a) = 0 := by ring
Proof state after:
m : ℕ
a : ℤ
h1 : [a]_m = [0]_m
h2 : 0 + -a = -a
h3 : a + -a = 0
⊢ [-a]_m = [0]_m
Theorem: HTPI.cc_neg_zero_of_cc_zero
Proof state before:
m : ℕ
a : ℤ
h1 : [a]_m = [0]_m
h2 : 0 + -a = -a
h3 : a + -a = 0
⊢ [-a]_m = [0]_m
Tactic:
show [-a]_m = [0]_m from
  calc [-a]_m
    _ = [0 + (-a)]_m := by rw [h2]
    _ = [0]_m + [-a]_m := by rw [add_class]
    _ = [a]_m + [-a]_m := by rw [h1]
    _ = [a + (-a)]_m := by rw [add_class]
    _ = [0]_m := by rw [h3]
Proof state after:
no goals
Theorem: HTPI.cc_neg_zero_of_cc_zero
Proof state before:
m : ℕ
a : ℤ
h1 : [a]_m = [0]_m
⊢ 0 + -a = -a
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.cc_neg_zero_of_cc_zero
Proof state before:
m : ℕ
a : ℤ
h1 : [a]_m = [0]_m
h2 : 0 + -a = -a
⊢ a + -a = 0
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.cc_neg_zero_of_cc_zero
Proof state before:
m : ℕ
a : ℤ
h1 : [a]_m = [0]_m
h2 : 0 + -a = -a
h3 : a + -a = 0
⊢ [-a]_m = [0 + -a]_m
Tactic:
rw [h2]
Proof state after:
no goals
Theorem: HTPI.cc_neg_zero_of_cc_zero
Proof state before:
m : ℕ
a : ℤ
h1 : [a]_m = [0]_m
h2 : 0 + -a = -a
h3 : a + -a = 0
⊢ [0 + -a]_m = [0]_m + [-a]_m
Tactic:
rw [add_class]
Proof state after:
no goals
Theorem: HTPI.cc_neg_zero_of_cc_zero
Proof state before:
m : ℕ
a : ℤ
h1 : [a]_m = [0]_m
h2 : 0 + -a = -a
h3 : a + -a = 0
⊢ [0]_m + [-a]_m = [a]_m + [-a]_m
Tactic:
rw [h1]
Proof state after:
no goals
Theorem: HTPI.cc_neg_zero_of_cc_zero
Proof state before:
m : ℕ
a : ℤ
h1 : [a]_m = [0]_m
h2 : 0 + -a = -a
h3 : a + -a = 0
⊢ [a]_m + [-a]_m = [a + -a]_m
Tactic:
rw [add_class]
Proof state after:
no goals
Theorem: HTPI.cc_neg_zero_of_cc_zero
Proof state before:
m : ℕ
a : ℤ
h1 : [a]_m = [0]_m
h2 : 0 + -a = -a
h3 : a + -a = 0
⊢ [a + -a]_m = [0]_m
Tactic:
rw [h3]
Proof state after:
no goals
Theorem: HTPI.cc_neg_zero_iff_cc_zero
Proof state before:
m : ℕ
a : ℤ
⊢ [-a]_m = [0]_m ↔ [a]_m = [0]_m
Tactic:
apply Iff.intro _ (cc_neg_zero_of_cc_zero m a)
Proof state after:
m : ℕ
a : ℤ
⊢ [-a]_m = [0]_m → [a]_m = [0]_m
Theorem: HTPI.cc_neg_zero_iff_cc_zero
Proof state before:
m : ℕ
a : ℤ
⊢ [-a]_m = [0]_m → [a]_m = [0]_m
Tactic:
assume h1 : [-a]_m = [0]_m
Proof state after:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
⊢ [a]_m = [0]_m
Theorem: HTPI.cc_neg_zero_iff_cc_zero
Proof state before:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
⊢ [a]_m = [0]_m
Tactic:
have h2 : [-(-a)]_m = [0]_m := cc_neg_zero_of_cc_zero m (-a) h1
Proof state after:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
h2 : [- -a]_m = [0]_m
⊢ [a]_m = [0]_m
Theorem: HTPI.cc_neg_zero_iff_cc_zero
Proof state before:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
h2 : [- -a]_m = [0]_m
⊢ [a]_m = [0]_m
Tactic:
have h3 : -(-a) = a := by ring
Proof state after:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
h2 : [- -a]_m = [0]_m
h3 : - -a = a
⊢ [a]_m = [0]_m
Theorem: HTPI.cc_neg_zero_iff_cc_zero
Proof state before:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
h2 : [- -a]_m = [0]_m
h3 : - -a = a
⊢ [a]_m = [0]_m
Tactic:
rewrite [h3] at h2
Proof state after:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
h2 : [a]_m = [0]_m
h3 : - -a = a
⊢ [a]_m = [0]_m
Theorem: HTPI.cc_neg_zero_iff_cc_zero
Proof state before:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
h2 : [a]_m = [0]_m
h3 : - -a = a
⊢ [a]_m = [0]_m
Tactic:
show [a]_m = [0]_m from h2
Proof state after:
no goals
Theorem: HTPI.cc_neg_zero_iff_cc_zero
Proof state before:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
h2 : [- -a]_m = [0]_m
⊢ - -a = a
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.cc_mod_0
Proof state before:
a : ℤ
⊢ [a]_0 = a
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.cc_nat_zero_iff_dvd
Proof state before:
m k : ℕ
⊢ [↑k]_0 = [0]_0 ↔ 0 ∣ k
Tactic:
have h : (0 : Int) = (↑(0 : Nat) : Int) := by rfl
Proof state after:
m k : ℕ
h : 0 = ↑0
⊢ [↑k]_0 = [0]_0 ↔ 0 ∣ k
Theorem: HTPI.cc_nat_zero_iff_dvd
Proof state before:
m k : ℕ
h : 0 = ↑0
⊢ [↑k]_0 = [0]_0 ↔ 0 ∣ k
Tactic:
rewrite [cc_mod_0, cc_mod_0, h, Nat.cast_inj]
Proof state after:
m k : ℕ
h : 0 = ↑0
⊢ k = 0 ↔ 0 ∣ k
Theorem: HTPI.cc_nat_zero_iff_dvd
Proof state before:
m k : ℕ
h : 0 = ↑0
⊢ k = 0 ↔ 0 ∣ k
Tactic:
apply Iff.intro
Proof state after:
case mp
m k : ℕ
h : 0 = ↑0
⊢ k = 0 → 0 ∣ k

case mpr
m k : ℕ
h : 0 = ↑0
⊢ 0 ∣ k → k = 0
Theorem: HTPI.cc_nat_zero_iff_dvd
Proof state before:
m k : ℕ
⊢ 0 = ↑0
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.cc_nat_zero_iff_dvd
Proof state before:
case mp
m k : ℕ
h : 0 = ↑0
⊢ k = 0 → 0 ∣ k
Tactic:
assume h1 : k = 0
Proof state after:
case mp
m k : ℕ
h : 0 = ↑0
h1 : k = 0
⊢ 0 ∣ k
Theorem: HTPI.cc_nat_zero_iff_dvd
Proof state before:
case mp
m k : ℕ
h : 0 = ↑0
h1 : k = 0
⊢ 0 ∣ k
Tactic:
rewrite [h1]
Proof state after:
case mp
m k : ℕ
h : 0 = ↑0
h1 : k = 0
⊢ 0 ∣ 0
Theorem: HTPI.cc_nat_zero_iff_dvd
Proof state before:
case mp
m k : ℕ
h : 0 = ↑0
h1 : k = 0
⊢ 0 ∣ 0
Tactic:
show 0 ∣ 0 from dvd_self 0
Proof state after:
no goals
Theorem: HTPI.cc_nat_zero_iff_dvd
Proof state before:
case mpr
m k : ℕ
h : 0 = ↑0
⊢ 0 ∣ k → k = 0
Tactic:
assume h1 : 0 ∣ k
Proof state after:
case mpr
m k : ℕ
h : 0 = ↑0
h1 : 0 ∣ k
⊢ k = 0
Theorem: HTPI.cc_nat_zero_iff_dvd
Proof state before:
case mpr
m k : ℕ
h : 0 = ↑0
h1 : 0 ∣ k
⊢ k = 0
Tactic:
obtain (c : Nat) (h2 : k = 0 * c) from h1
Proof state after:
case mpr
m k : ℕ
h : 0 = ↑0
h1 : 0 ∣ k
c : ℕ
h2 : k = 0 * c
⊢ k = 0
Theorem: HTPI.cc_nat_zero_iff_dvd
Proof state before:
case mpr
m k : ℕ
h : 0 = ↑0
h1 : 0 ∣ k
c : ℕ
h2 : k = 0 * c
⊢ k = 0
Tactic:
rewrite [h2]
Proof state after:
case mpr
m k : ℕ
h : 0 = ↑0
h1 : 0 ∣ k
c : ℕ
h2 : k = 0 * c
⊢ 0 * c = 0
Theorem: HTPI.cc_nat_zero_iff_dvd
Proof state before:
case mpr
m k : ℕ
h : 0 = ↑0
h1 : 0 ∣ k
c : ℕ
h2 : k = 0 * c
⊢ 0 * c = 0
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.cc_nat_zero_iff_dvd
Proof state before:
m k n : ℕ
⊢ [↑k]_(n + 1) = [0]_(n + 1) ↔ n + 1 ∣ k
Tactic:
rewrite [cc_eq_iff_val_eq, val_nat_eq_mod, val_zero]
Proof state after:
m k n : ℕ
⊢ k % (n + 1) = 0 ↔ n + 1 ∣ k
Theorem: HTPI.cc_nat_zero_iff_dvd
Proof state before:
m k n : ℕ
⊢ k % (n + 1) = 0 ↔ n + 1 ∣ k
Tactic:
show k % (n + 1) = 0 ↔ n + 1 ∣ k from
  (Nat.dvd_iff_mod_eq_zero (n + 1) k).symm
Proof state after:
no goals
Theorem: HTPI.cc_zero_iff_dvd
Proof state before:
m : ℕ
a : ℤ
⊢ [a]_m = [0]_m ↔ ↑m ∣ a
Tactic:
obtain (k : Nat) (h1 : a = ↑k ∨ a = -↑k) from Int.eq_nat_or_neg a
Proof state after:
m : ℕ
a : ℤ
k : ℕ
h1 : a = ↑k ∨ a = -↑k
⊢ [a]_m = [0]_m ↔ ↑m ∣ a
Theorem: HTPI.cc_zero_iff_dvd
Proof state before:
m : ℕ
a : ℤ
k : ℕ
h1 : a = ↑k ∨ a = -↑k
⊢ [a]_m = [0]_m ↔ ↑m ∣ a
Tactic:
by_cases on h1
Proof state after:
case Case_1
m : ℕ
a : ℤ
k : ℕ
h1 : a = ↑k
⊢ [a]_m = [0]_m ↔ ↑m ∣ a

case Case_2
m : ℕ
a : ℤ
k : ℕ
h1 : a = -↑k
⊢ [a]_m = [0]_m ↔ ↑m ∣ a
Theorem: HTPI.cc_zero_iff_dvd
Proof state before:
case Case_1
m : ℕ
a : ℤ
k : ℕ
h1 : a = ↑k
⊢ [a]_m = [0]_m ↔ ↑m ∣ a
Tactic:
rewrite [h1, Int.coe_nat_dvd]
Proof state after:
case Case_1
m : ℕ
a : ℤ
k : ℕ
h1 : a = ↑k
⊢ [↑k]_m = [0]_m ↔ m ∣ k
Theorem: HTPI.cc_zero_iff_dvd
Proof state before:
case Case_1
m : ℕ
a : ℤ
k : ℕ
h1 : a = ↑k
⊢ [↑k]_m = [0]_m ↔ m ∣ k
Tactic:
show [↑k]_m = [0]_m ↔ m ∣ k from cc_nat_zero_iff_dvd m k
Proof state after:
no goals
Theorem: HTPI.cc_zero_iff_dvd
Proof state before:
case Case_2
m : ℕ
a : ℤ
k : ℕ
h1 : a = -↑k
⊢ [a]_m = [0]_m ↔ ↑m ∣ a
Tactic:
rewrite [h1, cc_neg_zero_iff_cc_zero, Int.dvd_neg, Int.coe_nat_dvd]
Proof state after:
case Case_2
m : ℕ
a : ℤ
k : ℕ
h1 : a = -↑k
⊢ [↑k]_m = [0]_m ↔ m ∣ k
Theorem: HTPI.cc_zero_iff_dvd
Proof state before:
case Case_2
m : ℕ
a : ℤ
k : ℕ
h1 : a = -↑k
⊢ [↑k]_m = [0]_m ↔ m ∣ k
Tactic:
show [↑k]_m = [0]_m ↔ m ∣ k from cc_nat_zero_iff_dvd m k
Proof state after:
no goals
Theorem: HTPI.cc_eq_iff_congr
Proof state before:
m : ℕ
a b : ℤ
⊢ ↑m ∣ a - b ↔ a ≡ b (MOD m)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.mod_nonneg
Proof state before:
m : ℕ
inst✝ : NeZero m
a : ℤ
⊢ 0 ≤ a % ↑m
Tactic:
have h1 : (↑m : Int) ≠ 0 := (Nat.cast_ne_zero).rtl (NeZero.ne m)
Proof state after:
m : ℕ
inst✝ : NeZero m
a : ℤ
h1 : ↑m ≠ 0
⊢ 0 ≤ a % ↑m
Theorem: HTPI.mod_nonneg
Proof state before:
m : ℕ
inst✝ : NeZero m
a : ℤ
h1 : ↑m ≠ 0
⊢ 0 ≤ a % ↑m
Tactic:
show 0 ≤ a % m from Int.emod_nonneg a h1
Proof state after:
no goals
Theorem: HTPI.mod_lt
Proof state before:
m : ℕ
inst✝ : NeZero m
a : ℤ
⊢ a % ↑m < ↑m
Tactic:
have h1 : m > 0 := Nat.pos_of_ne_zero (NeZero.ne m)
Proof state after:
m : ℕ
inst✝ : NeZero m
a : ℤ
h1 : m > 0
⊢ a % ↑m < ↑m
Theorem: HTPI.mod_lt
Proof state before:
m : ℕ
inst✝ : NeZero m
a : ℤ
h1 : m > 0
⊢ a % ↑m < ↑m
Tactic:
have h2 : (↑m : Int) > 0 := (Nat.cast_pos).rtl h1
Proof state after:
m : ℕ
inst✝ : NeZero m
a : ℤ
h1 : m > 0
h2 : ↑m > 0
⊢ a % ↑m < ↑m
Theorem: HTPI.mod_lt
Proof state before:
m : ℕ
inst✝ : NeZero m
a : ℤ
h1 : m > 0
h2 : ↑m > 0
⊢ a % ↑m < ↑m
Tactic:
show a % m < m from Int.emod_lt_of_pos a h2
Proof state after:
no goals
Theorem: HTPI.congr_mod_mod
Proof state before:
m : ℕ
a : ℤ
⊢ a ≡ a % ↑m (MOD m)
Tactic:
define
Proof state after:
m : ℕ
a : ℤ
⊢ ∃ c, a - a % ↑m = ↑m * c
Theorem: HTPI.congr_mod_mod
Proof state before:
m : ℕ
a : ℤ
⊢ ∃ c, a - a % ↑m = ↑m * c
Tactic:
have h1 : m * (a / m) + a % m = a := Int.ediv_add_emod a m
Proof state after:
m : ℕ
a : ℤ
h1 : ↑m * (a / ↑m) + a % ↑m = a
⊢ ∃ c, a - a % ↑m = ↑m * c
Theorem: HTPI.congr_mod_mod
Proof state before:
m : ℕ
a : ℤ
h1 : ↑m * (a / ↑m) + a % ↑m = a
⊢ ∃ c, a - a % ↑m = ↑m * c
Tactic:
apply Exists.intro (a / m)
Proof state after:
m : ℕ
a : ℤ
h1 : ↑m * (a / ↑m) + a % ↑m = a
⊢ a - a % ↑m = ↑m * (a / ↑m)
Theorem: HTPI.congr_mod_mod
Proof state before:
m : ℕ
a : ℤ
h1 : ↑m * (a / ↑m) + a % ↑m = a
⊢ a - a % ↑m = ↑m * (a / ↑m)
Tactic:
show a - a % m = m * (a / m) from
  calc a - (a % m)
    _ = m * (a / m) + a % m - a % m := by rw [h1]
    _ = m * (a / m) := by ring
Proof state after:
no goals
Theorem: HTPI.congr_mod_mod
Proof state before:
m : ℕ
a : ℤ
h1 : ↑m * (a / ↑m) + a % ↑m = a
⊢ a - a % ↑m = ↑m * (a / ↑m) + a % ↑m - a % ↑m
Tactic:
rw [h1]
Proof state after:
no goals
Theorem: HTPI.congr_mod_mod
Proof state before:
m : ℕ
a : ℤ
h1 : ↑m * (a / ↑m) + a % ↑m = a
⊢ ↑m * (a / ↑m) + a % ↑m - a % ↑m = ↑m * (a / ↑m)
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_1
Proof state before:
m : ℕ
inst✝ : NeZero m
a : ℤ
⊢ ∃! r, 0 ≤ r ∧ r < ↑m ∧ a ≡ r (MOD m)
Tactic:
exists_unique
Proof 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
Theorem: HTPI.Theorem_7_3_1
Proof state before:
case Existence
m : ℕ
inst✝ : NeZero m
a : ℤ
⊢ ∃ r, 0 ≤ r ∧ r < ↑m ∧ a ≡ r (MOD m)
Tactic:
apply Exists.intro (a % m)
Proof state after:
case Existence
m : ℕ
inst✝ : NeZero m
a : ℤ
⊢ 0 ≤ a % ↑m ∧ a % ↑m < ↑m ∧ a ≡ a % ↑m (MOD m)
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_7_3_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_7_3_1
Proof 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)
Proof 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
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)
⊢ 0 ≤ r2 ∧ r2 < ↑m ∧ a ≡ r2 (MOD m) → r1 = r2
Tactic:
assume h2 : 0 ≤ r2 ∧ r2 < m ∧ a ≡ r2 (MOD 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)
⊢ 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)
⊢ r1 = r2
Tactic:
have h3 : r1 ≡ r2 (MOD m) :=
  congr_trans (congr_symm h1.right.right) h2.right.right
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)
⊢ r1 = r2