internlm/Lean-Github huggingface dataset:
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)
Z : ZMod m
h3 : X * Y * Z = [1]_m
⊢ invertible Y
Tactic:
apply Exists.intro (X * Z)
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
⊢ Y * (X * Z) = [1]_m
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)
Z : ZMod m
h3 : X * Y * Z = [1]_m
⊢ Y * (X * Z) = [1]_m
Tactic:
rewrite [←h3]
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
⊢ Y * (X * Z) = X * Y * Z
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)
Z : ZMod m
h3 : X * Y * Z = [1]_m
⊢ Y * (X * Z) = X * Y * Z
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.prod_inv_iff_inv
Proof state before:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
⊢ invertible Y → invertible (X * Y)
Tactic:
assume h2 : invertible Y
Proof state after:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
⊢ invertible (X * Y)
Theorem: HTPI.prod_inv_iff_inv
Proof state before:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
⊢ invertible (X * Y)
Tactic:
obtain (Xi : ZMod m) (h3 : X * Xi = [1]_m) from h1
Proof state after:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
Xi : ZMod m
h3 : X * Xi = [1]_m
⊢ invertible (X * Y)
Theorem: HTPI.prod_inv_iff_inv
Proof state before:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
Xi : ZMod m
h3 : X * Xi = [1]_m
⊢ invertible (X * Y)
Tactic:
obtain (Yi : ZMod m) (h4 : Y * Yi = [1]_m) from h2
Proof state after:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
Xi : ZMod m
h3 : X * Xi = [1]_m
Yi : ZMod m
h4 : Y * Yi = [1]_m
⊢ invertible (X * Y)
Theorem: HTPI.prod_inv_iff_inv
Proof state before:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
Xi : ZMod m
h3 : X * Xi = [1]_m
Yi : ZMod m
h4 : Y * Yi = [1]_m
⊢ invertible (X * Y)
Tactic:
apply Exists.intro (Xi * Yi)
Proof state after:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
Xi : ZMod m
h3 : X * Xi = [1]_m
Yi : ZMod m
h4 : Y * Yi = [1]_m
⊢ X * Y * (Xi * Yi) = [1]_m
Theorem: HTPI.prod_inv_iff_inv
Proof state before:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
Xi : ZMod m
h3 : X * Xi = [1]_m
Yi : ZMod m
h4 : Y * Yi = [1]_m
⊢ X * Y * (Xi * Yi) = [1]_m
Tactic:
show (X * Y) * (Xi * Yi) = [1]_m from
  calc X * Y * (Xi * Yi)
    _ = (X * Xi) * (Y * Yi) := by ring
    _ = [1]_m * [1]_m := by rw [h3, h4]
    _ = [1]_m := Theorem_7_3_6_7 [1]_m
Proof state after:
no goals
Theorem: HTPI.prod_inv_iff_inv
Proof state before:
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
Xi : ZMod m
h3 : X * Xi = [1]_m
Yi : ZMod m
h4 : Y * Yi = [1]_m
⊢ X * Y * (Xi * Yi) = X * Xi * (Y * Yi)
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.prod_inv_iff_inv
Proof state before:
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
Xi : ZMod m
h3 : X * Xi = [1]_m
Yi : ZMod m
h4 : Y * Yi = [1]_m
⊢ X * Xi * (Y * Yi) = [1]_m * [1]_m
Tactic:
rw [h3, h4]
Proof state after:
no goals
Theorem: HTPI.F_rp_def
Proof state before:
m i : ℕ
h : rel_prime m i
⊢ F m i = [↑i]_m
Tactic:
have h1 : F m i = if gcd m i = 1 then [i]_m else [1]_m := by rfl
Proof state after:
m i : ℕ
h : rel_prime m i
h1 : F m i = if gcd m i = 1 then [↑i]_m else [1]_m
⊢ F m i = [↑i]_m
Theorem: HTPI.F_rp_def
Proof state before:
m i : ℕ
h : rel_prime m i
h1 : F m i = if gcd m i = 1 then [↑i]_m else [1]_m
⊢ F m i = [↑i]_m
Tactic:
define at h
Proof state after:
m i : ℕ
h : gcd m i = 1
h1 : F m i = if gcd m i = 1 then [↑i]_m else [1]_m
⊢ F m i = [↑i]_m
Theorem: HTPI.F_rp_def
Proof state before:
m i : ℕ
h : gcd m i = 1
h1 : F m i = if gcd m i = 1 then [↑i]_m else [1]_m
⊢ F m i = [↑i]_m
Tactic:
rewrite [if_pos h] at h1
Proof state after:
m i : ℕ
h : gcd m i = 1
h1 : F m i = [↑i]_m
⊢ F m i = [↑i]_m
Theorem: HTPI.F_rp_def
Proof state before:
m i : ℕ
h : gcd m i = 1
h1 : F m i = [↑i]_m
⊢ F m i = [↑i]_m
Tactic:
show F m i = [i]_m from h1
Proof state after:
no goals
Theorem: HTPI.F_rp_def
Proof state before:
m i : ℕ
h : rel_prime m i
⊢ F m i = if gcd m i = 1 then [↑i]_m else [1]_m
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.F_not_rp_def
Proof state before:
m i : ℕ
h : ¬rel_prime m i
⊢ F m i = [1]_m
Tactic:
have h1 : F m i = if gcd m i = 1 then [i]_m else [1]_m := by rfl
Proof state after:
m i : ℕ
h : ¬rel_prime m i
h1 : F m i = if gcd m i = 1 then [↑i]_m else [1]_m
⊢ F m i = [1]_m
Theorem: HTPI.F_not_rp_def
Proof state before:
m i : ℕ
h : ¬rel_prime m i
h1 : F m i = if gcd m i = 1 then [↑i]_m else [1]_m
⊢ F m i = [1]_m
Tactic:
define at h
Proof state after:
m i : ℕ
h : ¬gcd m i = 1
h1 : F m i = if gcd m i = 1 then [↑i]_m else [1]_m
⊢ F m i = [1]_m
Theorem: HTPI.F_not_rp_def
Proof state before:
m i : ℕ
h : ¬gcd m i = 1
h1 : F m i = if gcd m i = 1 then [↑i]_m else [1]_m
⊢ F m i = [1]_m
Tactic:
rewrite [h1, if_neg h]
Proof state after:
m i : ℕ
h : ¬gcd m i = 1
h1 : F m i = if gcd m i = 1 then [↑i]_m else [1]_m
⊢ [1]_m = [1]_m
Theorem: HTPI.F_not_rp_def
Proof state before:
m i : ℕ
h : ¬gcd m i = 1
h1 : F m i = if gcd m i = 1 then [↑i]_m else [1]_m
⊢ [1]_m = [1]_m
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.F_not_rp_def
Proof state before:
m i : ℕ
h : ¬rel_prime m i
⊢ F m i = if gcd m i = 1 then [↑i]_m else [1]_m
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.prod_seq_base
Proof state before:
m k : ℕ
f : ℕ → ZMod m
⊢ prod_seq 0 k f = [1]_m
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.prod_seq_step
Proof state before:
m n k : ℕ
f : ℕ → ZMod m
⊢ prod_seq (n + 1) k f = prod_seq n k f * f (k + n)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.prod_seq_zero_step
Proof state before:
m n : ℕ
f : ℕ → ZMod m
⊢ prod_seq (n + 1) 0 f = prod_seq n 0 f * f n
Tactic:
rewrite [prod_seq_step, zero_add]
Proof state after:
m n : ℕ
f : ℕ → ZMod m
⊢ prod_seq n 0 f * f n = prod_seq n 0 f * f n
Theorem: HTPI.prod_seq_zero_step
Proof state before:
m n : ℕ
f : ℕ → ZMod m
⊢ prod_seq n 0 f * f n = prod_seq n 0 f * f n
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.prod_one
Proof state before:
m k : ℕ
f : ℕ → ZMod m
⊢ prod_seq 1 k f = f k
Tactic:
rewrite [prod_seq_step, prod_seq_base, add_zero, mul_comm, Theorem_7_3_6_7]
Proof state after:
m k : ℕ
f : ℕ → ZMod m
⊢ f k = f k
Theorem: HTPI.prod_one
Proof state before:
m k : ℕ
f : ℕ → ZMod m
⊢ f k = f k
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.G_def
Proof state before:
m a i : ℕ
⊢ G m a i = a * i % m
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.cc_G
Proof state before:
m a i : ℕ
⊢ [↑(G m a i)]_m = [↑a * ↑i % ↑m]_m
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.G_rp_iff
Proof state before:
m a : ℕ
h1 : rel_prime m a
i : ℕ
⊢ rel_prime m (G m a i) ↔ rel_prime m i
Tactic:
have h2 : invertible [a]_m := (Theorem_7_3_7 m a).rtl h1
Proof state after:
m a : ℕ
h1 : rel_prime m a
i : ℕ
h2 : invertible [↑a]_m
⊢ rel_prime m (G m a i) ↔ rel_prime m i
Theorem: HTPI.G_rp_iff
Proof state before:
m a : ℕ
h1 : rel_prime m a
i : ℕ
h2 : invertible [↑a]_m
⊢ rel_prime m (G m a i) ↔ rel_prime m i
Tactic:
show rel_prime m (G m a i) ↔ rel_prime m i from
  calc rel_prime m (G m a i)
    _ ↔ invertible [G m a i]_m := (Theorem_7_3_7 m (G m a i)).symm
    _ ↔ invertible ([a]_m * [i]_m) := by rw [cc_G]
    _ ↔ invertible [i]_m := prod_inv_iff_inv h2 ([i]_m)
    _ ↔ rel_prime m i := Theorem_7_3_7 m i
Proof state after:
no goals
Theorem: HTPI.G_rp_iff
Proof state before:
m a : ℕ
h1 : rel_prime m a
i : ℕ
h2 : invertible [↑a]_m
⊢ invertible [↑(G m a i)]_m ↔ invertible ([↑a]_m * [↑i]_m)
Tactic:
rw [cc_G]
Proof state after:
no goals
Theorem: HTPI.FG_rp
Proof state before:
m a i : ℕ
h1 : rel_prime m a
h2 : rel_prime m i
⊢ F m (G m a i) = [↑a]_m * F m i
Tactic:
have h3 : rel_prime m (G m a i) := (G_rp_iff h1 i).rtl h2
Proof state after:
m a i : ℕ
h1 : rel_prime m a
h2 : rel_prime m i
h3 : rel_prime m (G m a i)
⊢ F m (G m a i) = [↑a]_m * F m i
Theorem: HTPI.FG_rp
Proof state before:
m a i : ℕ
h1 : rel_prime m a
h2 : rel_prime m i
h3 : rel_prime m (G m a i)
⊢ F m (G m a i) = [↑a]_m * F m i
Tactic:
show F m (G m a i) = [a]_m * F m i from
  calc F m (G m a i)
    _ = [G m a i]_m := F_rp_def h3
    _ = [a]_m * [i]_m := cc_G m a i
    _ = [a]_m * F m i := by rw [F_rp_def h2]
Proof state after:
no goals
Theorem: HTPI.FG_rp
Proof state before:
m a i : ℕ
h1 : rel_prime m a
h2 : rel_prime m i
h3 : rel_prime m (G m a i)
⊢ [↑a]_m * [↑i]_m = [↑a]_m * F m i
Tactic:
rw [F_rp_def h2]
Proof state after:
no goals
Theorem: HTPI.FG_not_rp
Proof state before:
m a i : ℕ
h1 : rel_prime m a
h2 : ¬rel_prime m i
⊢ F m (G m a i) = [1]_m
Tactic:
rewrite [←G_rp_iff h1 i] at h2
Proof state after:
m a i : ℕ
h1 : rel_prime m a
h2 : ¬rel_prime m (G m a i)
⊢ F m (G m a i) = [1]_m
Theorem: HTPI.FG_not_rp
Proof state before:
m a i : ℕ
h1 : rel_prime m a
h2 : ¬rel_prime m (G m a i)
⊢ F m (G m a i) = [1]_m
Tactic:
show F m (G m a i) = [1]_m from F_not_rp_def h2
Proof state after:
no goals
Theorem: HTPI.FG_prod
Proof state before:
m a : ℕ
h1 : rel_prime m a
⊢ ∀ (k : ℕ), prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
Tactic:
by_induc
Proof state after:
case Base_Case
m a : ℕ
h1 : rel_prime m a
⊢ prod_seq 0 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m 0 * prod_seq 0 0 (F m)

case Induction_Step
m a : ℕ
h1 : rel_prime m a
⊢ ∀ (k : ℕ),
    prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) →
      prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Theorem: HTPI.FG_prod
Proof state before:
case Base_Case
m a : ℕ
h1 : rel_prime m a
⊢ prod_seq 0 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m 0 * prod_seq 0 0 (F m)
Tactic:
show prod_seq 0 0 ((F m) ∘ (G m a)) =
      [a]_m ^ (num_rp_below m 0) * prod_seq 0 0 (F m) from
  calc prod_seq 0 0 ((F m) ∘ (G m a))
    _ = [1]_m := prod_seq_base _ _
    _ = [a]_m ^ 0 * [1]_m := by ring
    _ = [a]_m ^ (num_rp_below m 0) * prod_seq 0 0 (F m) := by
          rw [num_rp_below_base, prod_seq_base]
Proof state after:
no goals
Theorem: HTPI.FG_prod
Proof state before:
m a : ℕ
h1 : rel_prime m a
⊢ [1]_m = [↑a]_m ^ 0 * [1]_m
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.FG_prod
Proof state before:
m a : ℕ
h1 : rel_prime m a
⊢ [↑a]_m ^ 0 * [1]_m = [↑a]_m ^ num_rp_below m 0 * prod_seq 0 0 (F m)
Tactic:
rw [num_rp_below_base, prod_seq_base]
Proof state after:
no goals
Theorem: HTPI.FG_prod
Proof state before:
case Induction_Step
m a : ℕ
h1 : rel_prime m a
⊢ ∀ (k : ℕ),
    prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) →
      prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Tactic:
fix k : Nat
Proof state after:
case Induction_Step
m a : ℕ
h1 : rel_prime m a
k : ℕ
⊢ prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) →
    prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Theorem: HTPI.FG_prod
Proof state before:
case Induction_Step
m a : ℕ
h1 : rel_prime m a
k : ℕ
⊢ prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) →
    prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Tactic:
assume ih : prod_seq k 0 ((F m) ∘ (G m a)) =
  [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m)
Proof state after:
case Induction_Step
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
⊢ prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Theorem: HTPI.FG_prod
Proof state before:
case Induction_Step
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
⊢ prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Tactic:
by_cases h2 : rel_prime m k
Proof state after:
case pos
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : rel_prime m k
⊢ prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)

case neg
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : ¬rel_prime m k
⊢ prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Theorem: HTPI.FG_prod
Proof state before:
case pos
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : rel_prime m k
⊢ prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Tactic:
show prod_seq (k + 1) 0 ((F m) ∘ (G m a)) =
    [a]_m ^ (num_rp_below m (k + 1)) *
    prod_seq (k + 1) 0 (F m) from
  calc prod_seq (k + 1) 0 ((F m) ∘ (G m a))
    _ = prod_seq k 0 ((F m) ∘ (G m a)) *
        F m (G m a k) := prod_seq_zero_step _ _
    _ = [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) *
        F m (G m a k) := by rw [ih]
    _ = [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) *
        ([a]_m * F m k) := by rw [FG_rp h1 h2]
    _ = [a]_m ^ ((num_rp_below m k) + 1) *
        ((prod_seq k 0 (F m)) * F m k) := by ring
    _ = [a]_m ^ (num_rp_below m (k + 1)) *
        prod_seq (k + 1) 0 (F m) := by
          rw [num_rp_below_step_rp h2, prod_seq_zero_step]
Proof state after:
no goals
Theorem: HTPI.FG_prod
Proof state before:
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : rel_prime m k
⊢ prod_seq k 0 (F m ∘ G m a) * F m (G m a k) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) * F m (G m a k)
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: HTPI.FG_prod
Proof state before:
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : rel_prime m k
⊢ [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) * F m (G m a k) =
    [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) * ([↑a]_m * F m k)
Tactic:
rw [FG_rp h1 h2]
Proof state after:
no goals
Theorem: HTPI.FG_prod
Proof state before:
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : rel_prime m k
⊢ [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) * ([↑a]_m * F m k) =
    [↑a]_m ^ (num_rp_below m k + 1) * (prod_seq k 0 (F m) * F m k)
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.FG_prod
Proof state before:
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : rel_prime m k
⊢ [↑a]_m ^ (num_rp_below m k + 1) * (prod_seq k 0 (F m) * F m k) =
    [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Tactic:
rw [num_rp_below_step_rp h2, prod_seq_zero_step]
Proof state after:
no goals
Theorem: HTPI.FG_prod
Proof state before:
case neg
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : ¬rel_prime m k
⊢ prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Tactic:
show prod_seq (k + 1) 0 ((F m) ∘ (G m a)) =
    [a]_m ^ (num_rp_below m (k + 1)) *
    prod_seq (k + 1) 0 (F m) from
  calc prod_seq (k + 1) 0 ((F m) ∘ (G m a))
    _ = prod_seq k 0 ((F m) ∘ (G m a)) *
        F m (G m a k) := prod_seq_zero_step _ _
    _ = [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) *
        F m (G m a k) := by rw [ih]
    _ = [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) *
        ([1]_m) := by rw [FG_not_rp h1 h2]
    _ = [a]_m ^ (num_rp_below m k) *
        (prod_seq k 0 (F m) * ([1]_m)) := by ring
    _ = [a]_m ^ (num_rp_below m (k + 1)) *
        prod_seq (k + 1) 0 (F m) := by
          rw [num_rp_below_step_not_rp h2, prod_seq_zero_step,
          F_not_rp_def h2]
Proof state after:
no goals
Theorem: HTPI.FG_prod
Proof state before:
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : ¬rel_prime m k
⊢ prod_seq k 0 (F m ∘ G m a) * F m (G m a k) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) * F m (G m a k)
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: HTPI.FG_prod
Proof state before:
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : ¬rel_prime m k
⊢ [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) * F m (G m a k) =
    [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) * [1]_m
Tactic:
rw [FG_not_rp h1 h2]
Proof state after:
no goals
Theorem: HTPI.FG_prod
Proof state before:
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : ¬rel_prime m k
⊢ [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) * [1]_m = [↑a]_m ^ num_rp_below m k * (prod_seq k 0 (F m) * [1]_m)
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.FG_prod
Proof state before:
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : ¬rel_prime m k
⊢ [↑a]_m ^ num_rp_below m k * (prod_seq k 0 (F m) * [1]_m) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Tactic:
rw [num_rp_below_step_not_rp h2, prod_seq_zero_step,
F_not_rp_def h2]
Proof state after:
no goals
Theorem: HTPI.G_maps_below
Proof state before:
m a : ℕ
inst✝ : NeZero m
⊢ maps_below m (G m a)
Tactic:
define
Proof state after:
m a : ℕ
inst✝ : NeZero m
⊢ ∀ i < m, G m a i < m
Theorem: HTPI.G_maps_below
Proof state before:
m a : ℕ
inst✝ : NeZero m
⊢ ∀ i < m, G m a i < m
Tactic:
fix i : Nat
Proof state after:
m a : ℕ
inst✝ : NeZero m
i : ℕ
⊢ i < m → G m a i < m
Theorem: HTPI.G_maps_below
Proof state before:
m a : ℕ
inst✝ : NeZero m
i : ℕ
⊢ i < m → G m a i < m
Tactic:
assume h1 : i < m
Proof state after:
m a : ℕ
inst✝ : NeZero m
i : ℕ
h1 : i < m
⊢ G m a i < m
Theorem: HTPI.G_maps_below
Proof state before:
m a : ℕ
inst✝ : NeZero m
i : ℕ
h1 : i < m
⊢ G m a i < m
Tactic:
rewrite [G_def]
Proof state after:
m a : ℕ
inst✝ : NeZero m
i : ℕ
h1 : i < m
⊢ a * i % m < m
Theorem: HTPI.G_maps_below
Proof state before:
m a : ℕ
inst✝ : NeZero m
i : ℕ
h1 : i < m
⊢ a * i % m < m
Tactic:
show a * i % m < m from mod_nonzero_lt (a * i) (NeZero.ne m)
Proof state after:
no goals
Theorem: HTPI.right_inv_onto_below
Proof state before:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : maps_below n g'
⊢ onto_below n g
Tactic:
define at h2
Proof state after:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
⊢ onto_below n g
Theorem: HTPI.right_inv_onto_below
Proof state before:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
⊢ onto_below n g
Tactic:
define
Proof state after:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
⊢ ∀ k < n, ∃ i < n, g i = k
Theorem: HTPI.right_inv_onto_below
Proof state before:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
⊢ ∀ k < n, ∃ i < n, g i = k
Tactic:
fix k : Nat
Proof state after:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
k : ℕ
⊢ k < n → ∃ i < n, g i = k
Theorem: HTPI.right_inv_onto_below
Proof state before:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
k : ℕ
⊢ k < n → ∃ i < n, g i = k
Tactic:
assume h3 : k < n
Proof state after:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
k : ℕ
h3 : k < n
⊢ ∃ i < n, g i = k
Theorem: HTPI.right_inv_onto_below
Proof state before:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
k : ℕ
h3 : k < n
⊢ ∃ i < n, g i = k
Tactic:
apply Exists.intro (g' k)
Proof state after:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
k : ℕ
h3 : k < n
⊢ g' k < n ∧ g (g' k) = k
Theorem: HTPI.right_inv_onto_below
Proof state before:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
k : ℕ
h3 : k < n
⊢ g' k < n ∧ g (g' k) = k
Tactic:
show g' k < n ∧ g (g' k) = k from And.intro (h2 k h3) (h1 k h3)
Proof state after:
no goals
Theorem: HTPI.cc_mul_inv_mod_eq_one
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ [↑a]_m * [↑(inv_mod m a)]_m = [1]_m
Tactic:
have h2 : 0 ≤ (gcd_c2 m a) % m := mod_nonneg m (gcd_c2 m a)
Proof state after:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : 0 ≤ gcd_c2 m a % ↑m
⊢ [↑a]_m * [↑(inv_mod m a)]_m = [1]_m
Theorem: HTPI.cc_mul_inv_mod_eq_one
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : 0 ≤ gcd_c2 m a % ↑m
⊢ [↑a]_m * [↑(inv_mod m a)]_m = [1]_m
Tactic:
show [a]_m * [inv_mod m a]_m = [1]_m from
  calc [a]_m * [inv_mod m a]_m
    _ = [a]_m * [Int.toNat ((gcd_c2 m a) % m)]_m := by rfl
    _ = [a]_m * [(gcd_c2 m a) % m]_m := by rw [Int.toNat_of_nonneg h2]
    _ = [a]_m * [gcd_c2 m a]_m := by rw [←cc_eq_mod]
    _ = [1]_m := gcd_c2_inv h1
Proof state after:
no goals
Theorem: HTPI.cc_mul_inv_mod_eq_one
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : 0 ≤ gcd_c2 m a % ↑m
⊢ [↑a]_m * [↑(inv_mod m a)]_m = [↑a]_m * [↑(Int.toNat (gcd_c2 m a % ↑m))]_m
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.cc_mul_inv_mod_eq_one
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : 0 ≤ gcd_c2 m a % ↑m
⊢ [↑a]_m * [↑(Int.toNat (gcd_c2 m a % ↑m))]_m = [↑a]_m * [gcd_c2 m a % ↑m]_m
Tactic:
rw [Int.toNat_of_nonneg h2]
Proof state after:
no goals
Theorem: HTPI.cc_mul_inv_mod_eq_one
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : 0 ≤ gcd_c2 m a % ↑m
⊢ [↑a]_m * [gcd_c2 m a % ↑m]_m = [↑a]_m * [gcd_c2 m a]_m
Tactic:
rw [←cc_eq_mod]
Proof state after:
no goals
Theorem: HTPI.mul_mod_mod_eq_mul_mod
Proof state before:
m a b : ℕ
⊢ a % m * (b % m % m) % m = a % m * (b % m) % m
Tactic:
rw [Nat.mod_mod]
Proof state after:
no goals
Theorem: HTPI.mod_mul_mod_eq_mul_mod
Proof state before:
m a b : ℕ
⊢ a % m * b % m = a * b % m
Tactic:
rewrite [mul_comm, mul_mod_mod_eq_mul_mod, mul_comm]
Proof state after:
m a b : ℕ
⊢ a * b % m = a * b % m
Theorem: HTPI.mod_mul_mod_eq_mul_mod
Proof state before:
m a b : ℕ
⊢ a * b % m = a * b % m
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.mul_inv_mod_cancel
Proof state before:
m a i : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : i < m
⊢ a * inv_mod m a * i % m = i
Tactic:
have h3 : [a]_m * [inv_mod m a]_m = [1]_m := cc_mul_inv_mod_eq_one h1
Proof state after:
m a i : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : i < m
h3 : [↑a]_m * [↑(inv_mod m a)]_m = [1]_m
⊢ a * inv_mod m a * i % m = i
Theorem: HTPI.mul_inv_mod_cancel
Proof state before:
m a i : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : i < m
h3 : [↑a]_m * [↑(inv_mod m a)]_m = [1]_m
⊢ a * inv_mod m a * i % m = i
Tactic:
rewrite [mul_class, cc_eq_iff_congr, ←Nat.cast_mul, ←Nat.cast_one, congr_iff_mod_eq_Nat] at h3
Proof state after:
m a i : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : i < m
h3 : a * inv_mod m a % m = 1 % m
⊢ a * inv_mod m a * i % m = i
Theorem: HTPI.mul_inv_mod_cancel
Proof state before:
m a i : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : i < m
h3 : a * inv_mod m a % m = 1 % m
⊢ a * inv_mod m a * i % m = i
Tactic:
show a * inv_mod m a * i % m = i from
  calc a * (inv_mod m a) * i % m
    _ = (a * inv_mod m a) % m * i % m := by rw [mod_mul_mod_eq_mul_mod]
    _ = 1 % m * i % m := by rw [h3]
    _ = 1 * i % m := by rw [mod_mul_mod_eq_mul_mod]
    _ = i % m := by rw [one_mul]
    _ = i := Nat.mod_eq_of_lt h2
Proof state after:
no goals
Theorem: HTPI.mul_inv_mod_cancel
Proof state before:
m a i : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : i < m
h3 : a * inv_mod m a % m = 1 % m
⊢ a * inv_mod m a * i % m = a * inv_mod m a % m * i % m
Tactic:
rw [mod_mul_mod_eq_mul_mod]
Proof state after:
no goals
Theorem: HTPI.mul_inv_mod_cancel
Proof state before:
m a i : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : i < m
h3 : a * inv_mod m a % m = 1 % m
⊢ a * inv_mod m a % m * i % m = 1 % m * i % m
Tactic:
rw [h3]
Proof state after:
no goals
Theorem: HTPI.mul_inv_mod_cancel
Proof state before:
m a i : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : i < m
h3 : a * inv_mod m a % m = 1 % m
⊢ 1 % m * i % m = 1 * i % m
Tactic:
rw [mod_mul_mod_eq_mul_mod]
Proof state after:
no goals