internlm/Lean-Github huggingface dataset:
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 * i % m = i % m
Tactic:
rw [one_mul]
Proof state after:
no goals
Theorem: HTPI.Ginv_def
Proof state before:
m a i : ℕ
⊢ Ginv m a i = G m (inv_mod m a) i
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Ginv_right_inv
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ ∀ i < m, G m a (Ginv m a i) = i
Tactic:
fix i : Nat
Proof state after:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
⊢ i < m → G m a (Ginv m a i) = i
Theorem: HTPI.Ginv_right_inv
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
⊢ i < m → G m a (Ginv m a i) = i
Tactic:
assume h2 : i < m
Proof state after:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
h2 : i < m
⊢ G m a (Ginv m a i) = i
Theorem: HTPI.Ginv_right_inv
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
h2 : i < m
⊢ G m a (Ginv m a i) = i
Tactic:
show G m a (Ginv m a i) = i from
  calc G m a (Ginv m a i)
    _ = a * ((inv_mod m a * i) % m) % m := by rfl
    _ = a * (inv_mod m a * i) % m := by rw [mul_mod_mod_eq_mul_mod]
    _ = a * inv_mod m a * i % m := by rw [←mul_assoc]
    _ = i := mul_inv_mod_cancel h1 h2
Proof state after:
no goals
Theorem: HTPI.Ginv_right_inv
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
h2 : i < m
⊢ G m a (Ginv m a i) = a * (inv_mod m a * i % m) % m
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Ginv_right_inv
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
h2 : i < m
⊢ a * (inv_mod m a * i % m) % m = a * (inv_mod m a * i) % m
Tactic:
rw [mul_mod_mod_eq_mul_mod]
Proof state after:
no goals
Theorem: HTPI.Ginv_right_inv
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
h2 : i < m
⊢ a * (inv_mod m a * i) % m = a * inv_mod m a * i % m
Tactic:
rw [←mul_assoc]
Proof state after:
no goals
Theorem: HTPI.Ginv_left_inv
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ ∀ i < m, Ginv m a (G m a i) = i
Tactic:
fix i : Nat
Proof state after:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
⊢ i < m → Ginv m a (G m a i) = i
Theorem: HTPI.Ginv_left_inv
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
⊢ i < m → Ginv m a (G m a i) = i
Tactic:
assume h2 : i < m
Proof state after:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
h2 : i < m
⊢ Ginv m a (G m a i) = i
Theorem: HTPI.Ginv_left_inv
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
h2 : i < m
⊢ Ginv m a (G m a i) = i
Tactic:
show Ginv m a (G m a i) = i from
  calc Ginv m a (G m a i)
    _ = inv_mod m a * ((a * i) % m) % m := by rfl
    _ = inv_mod m a * (a * i) % m := by rw [mul_mod_mod_eq_mul_mod]
    _ = a * inv_mod m a * i % m := by rw [←mul_assoc, mul_comm (inv_mod m a)]
    _ = i := mul_inv_mod_cancel h1 h2
Proof state after:
no goals
Theorem: HTPI.Ginv_left_inv
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
h2 : i < m
⊢ Ginv m a (G m a i) = inv_mod m a * (a * i % m) % m
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Ginv_left_inv
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
h2 : i < m
⊢ inv_mod m a * (a * i % m) % m = inv_mod m a * (a * i) % m
Tactic:
rw [mul_mod_mod_eq_mul_mod]
Proof state after:
no goals
Theorem: HTPI.Ginv_left_inv
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
i : ℕ
h2 : i < m
⊢ inv_mod m a * (a * i) % m = a * inv_mod m a * i % m
Tactic:
rw [←mul_assoc, mul_comm (inv_mod m a)]
Proof state after:
no goals
Theorem: HTPI.swap_fst
Proof state before:
u v : ℕ
⊢ swap u v u = v
Tactic:
define : swap u v u
Proof state after:
u v : ℕ
⊢ (if u = u then v else if u = v then u else u) = v
Theorem: HTPI.swap_fst
Proof state before:
u v : ℕ
⊢ (if u = u then v else if u = v then u else u) = v
Tactic:
have h : u = u := by rfl
Proof state after:
u v : ℕ
h : u = u
⊢ (if u = u then v else if u = v then u else u) = v
Theorem: HTPI.swap_fst
Proof state before:
u v : ℕ
h : u = u
⊢ (if u = u then v else if u = v then u else u) = v
Tactic:
rewrite [if_pos h]
Proof state after:
u v : ℕ
h : u = u
⊢ v = v
Theorem: HTPI.swap_fst
Proof state before:
u v : ℕ
h : u = u
⊢ v = v
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.swap_fst
Proof state before:
u v : ℕ
⊢ u = u
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.swap_snd
Proof state before:
u v : ℕ
⊢ swap u v v = u
Tactic:
define : swap u v v
Proof state after:
u v : ℕ
⊢ (if v = u then v else if v = v then u else v) = u
Theorem: HTPI.swap_snd
Proof state before:
u v : ℕ
⊢ (if v = u then v else if v = v then u else v) = u
Tactic:
by_cases h1 : v = u
Proof state after:
case pos
u v : ℕ
h1 : v = u
⊢ (if v = u then v else if v = v then u else v) = u

case neg
u v : ℕ
h1 : ¬v = u
⊢ (if v = u then v else if v = v then u else v) = u
Theorem: HTPI.swap_snd
Proof state before:
case pos
u v : ℕ
h1 : v = u
⊢ (if v = u then v else if v = v then u else v) = u
Tactic:
rewrite [if_pos h1]
Proof state after:
case pos
u v : ℕ
h1 : v = u
⊢ v = u
Theorem: HTPI.swap_snd
Proof state before:
case pos
u v : ℕ
h1 : v = u
⊢ v = u
Tactic:
show v = u from h1
Proof state after:
no goals
Theorem: HTPI.swap_snd
Proof state before:
case neg
u v : ℕ
h1 : ¬v = u
⊢ (if v = u then v else if v = v then u else v) = u
Tactic:
rewrite [if_neg h1]
Proof state after:
case neg
u v : ℕ
h1 : ¬v = u
⊢ (if v = v then u else v) = u
Theorem: HTPI.swap_snd
Proof state before:
case neg
u v : ℕ
h1 : ¬v = u
⊢ (if v = v then u else v) = u
Tactic:
have h2 : v = v := by rfl
Proof state after:
case neg
u v : ℕ
h1 : ¬v = u
h2 : v = v
⊢ (if v = v then u else v) = u
Theorem: HTPI.swap_snd
Proof state before:
case neg
u v : ℕ
h1 : ¬v = u
h2 : v = v
⊢ (if v = v then u else v) = u
Tactic:
rewrite [if_pos h2]
Proof state after:
case neg
u v : ℕ
h1 : ¬v = u
h2 : v = v
⊢ u = u
Theorem: HTPI.swap_snd
Proof state before:
case neg
u v : ℕ
h1 : ¬v = u
h2 : v = v
⊢ u = u
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.swap_snd
Proof state before:
u v : ℕ
h1 : ¬v = u
⊢ v = v
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.swap_other
Proof state before:
u v i : ℕ
h1 : i ≠ u
h2 : i ≠ v
⊢ swap u v i = i
Tactic:
define : swap u v i
Proof state after:
u v i : ℕ
h1 : i ≠ u
h2 : i ≠ v
⊢ (if i = u then v else if i = v then u else i) = i
Theorem: HTPI.swap_other
Proof state before:
u v i : ℕ
h1 : i ≠ u
h2 : i ≠ v
⊢ (if i = u then v else if i = v then u else i) = i
Tactic:
rewrite [if_neg h1, if_neg h2]
Proof state after:
u v i : ℕ
h1 : i ≠ u
h2 : i ≠ v
⊢ i = i
Theorem: HTPI.swap_other
Proof state before:
u v i : ℕ
h1 : i ≠ u
h2 : i ≠ v
⊢ i = i
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.swap_values
Proof state before:
u v i : ℕ
⊢ swap u v i = v ∨ swap u v i = u ∨ swap u v i = i
Tactic:
by_cases h1 : i = u
Proof state after:
case pos
u v i : ℕ
h1 : i = u
⊢ swap u v i = v ∨ swap u v i = u ∨ swap u v i = i

case neg
u v i : ℕ
h1 : ¬i = u
⊢ swap u v i = v ∨ swap u v i = u ∨ swap u v i = i
Theorem: HTPI.swap_values
Proof state before:
case pos
u v i : ℕ
h1 : i = u
⊢ swap u v i = v ∨ swap u v i = u ∨ swap u v i = i
Tactic:
apply Or.inl
Proof state after:
case pos.h
u v i : ℕ
h1 : i = u
⊢ swap u v i = v
Theorem: HTPI.swap_values
Proof state before:
case pos.h
u v i : ℕ
h1 : i = u
⊢ swap u v i = v
Tactic:
rewrite [h1]
Proof state after:
case pos.h
u v i : ℕ
h1 : i = u
⊢ swap u v u = v
Theorem: HTPI.swap_values
Proof state before:
case pos.h
u v i : ℕ
h1 : i = u
⊢ swap u v u = v
Tactic:
show swap u v u = v from swap_fst u v
Proof state after:
no goals
Theorem: HTPI.swap_values
Proof state before:
case neg
u v i : ℕ
h1 : ¬i = u
⊢ swap u v i = v ∨ swap u v i = u ∨ swap u v i = i
Tactic:
apply Or.inr
Proof state after:
case neg.h
u v i : ℕ
h1 : ¬i = u
⊢ swap u v i = u ∨ swap u v i = i
Theorem: HTPI.swap_values
Proof state before:
case neg.h
u v i : ℕ
h1 : ¬i = u
⊢ swap u v i = u ∨ swap u v i = i
Tactic:
by_cases h2 : i = v
Proof state after:
case pos
u v i : ℕ
h1 : ¬i = u
h2 : i = v
⊢ swap u v i = u ∨ swap u v i = i

case neg
u v i : ℕ
h1 : ¬i = u
h2 : ¬i = v
⊢ swap u v i = u ∨ swap u v i = i
Theorem: HTPI.swap_values
Proof state before:
case pos
u v i : ℕ
h1 : ¬i = u
h2 : i = v
⊢ swap u v i = u ∨ swap u v i = i
Tactic:
apply Or.inl
Proof state after:
case pos.h
u v i : ℕ
h1 : ¬i = u
h2 : i = v
⊢ swap u v i = u
Theorem: HTPI.swap_values
Proof state before:
case pos.h
u v i : ℕ
h1 : ¬i = u
h2 : i = v
⊢ swap u v i = u
Tactic:
rewrite [h2]
Proof state after:
case pos.h
u v i : ℕ
h1 : ¬i = u
h2 : i = v
⊢ swap u v v = u
Theorem: HTPI.swap_values
Proof state before:
case pos.h
u v i : ℕ
h1 : ¬i = u
h2 : i = v
⊢ swap u v v = u
Tactic:
show swap u v v = u from swap_snd u v
Proof state after:
no goals
Theorem: HTPI.swap_values
Proof state before:
case neg
u v i : ℕ
h1 : ¬i = u
h2 : ¬i = v
⊢ swap u v i = u ∨ swap u v i = i
Tactic:
apply Or.inr
Proof state after:
case neg.h
u v i : ℕ
h1 : ¬i = u
h2 : ¬i = v
⊢ swap u v i = i
Theorem: HTPI.swap_values
Proof state before:
case neg.h
u v i : ℕ
h1 : ¬i = u
h2 : ¬i = v
⊢ swap u v i = i
Tactic:
show swap u v i = i from swap_other h1 h2
Proof state after:
no goals
Theorem: HTPI.swap_maps_below
Proof state before:
u v n : ℕ
h1 : u < n
h2 : v < n
⊢ maps_below n (swap u v)
Tactic:
define
Proof state after:
u v n : ℕ
h1 : u < n
h2 : v < n
⊢ ∀ i < n, swap u v i < n
Theorem: HTPI.swap_maps_below
Proof state before:
u v n : ℕ
h1 : u < n
h2 : v < n
⊢ ∀ i < n, swap u v i < n
Tactic:
fix i : Nat
Proof state after:
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
⊢ i < n → swap u v i < n
Theorem: HTPI.swap_maps_below
Proof state before:
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
⊢ i < n → swap u v i < n
Tactic:
assume h3 : i < n
Proof state after:
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
⊢ swap u v i < n
Theorem: HTPI.swap_maps_below
Proof state before:
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
⊢ swap u v i < n
Tactic:
have h4 : swap u v i = v ∨ swap u v i = u ∨ swap u v i = i := swap_values u v i
Proof state after:
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = v ∨ swap u v i = u ∨ swap u v i = i
⊢ swap u v i < n
Theorem: HTPI.swap_maps_below
Proof state before:
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = v ∨ swap u v i = u ∨ swap u v i = i
⊢ swap u v i < n
Tactic:
by_cases on h4
Proof state after:
case Case_1
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = v
⊢ swap u v i < n

case Case_2
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = u ∨ swap u v i = i
⊢ swap u v i < n
Theorem: HTPI.swap_maps_below
Proof state before:
case Case_1
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = v
⊢ swap u v i < n
Tactic:
rewrite [h4]
Proof state after:
case Case_1
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = v
⊢ v < n
Theorem: HTPI.swap_maps_below
Proof state before:
case Case_1
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = v
⊢ v < n
Tactic:
show v < n from h2
Proof state after:
no goals
Theorem: HTPI.swap_maps_below
Proof state before:
case Case_2
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = u ∨ swap u v i = i
⊢ swap u v i < n
Tactic:
by_cases on h4
Proof state after:
case Case_2.Case_1
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = u
⊢ swap u v i < n

case Case_2.Case_2
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = i
⊢ swap u v i < n
Theorem: HTPI.swap_maps_below
Proof state before:
case Case_2.Case_1
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = u
⊢ swap u v i < n
Tactic:
rewrite [h4]
Proof state after:
case Case_2.Case_1
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = u
⊢ u < n
Theorem: HTPI.swap_maps_below
Proof state before:
case Case_2.Case_1
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = u
⊢ u < n
Tactic:
show u < n from h1
Proof state after:
no goals
Theorem: HTPI.swap_maps_below
Proof state before:
case Case_2.Case_2
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = i
⊢ swap u v i < n
Tactic:
rewrite [h4]
Proof state after:
case Case_2.Case_2
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = i
⊢ i < n
Theorem: HTPI.swap_maps_below
Proof state before:
case Case_2.Case_2
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = i
⊢ i < n
Tactic:
show i < n from h3
Proof state after:
no goals
Theorem: HTPI.swap_swap
Proof state before:
u v n : ℕ
⊢ ∀ i < n, swap u v (swap u v i) = i
Tactic:
fix i : Nat
Proof state after:
u v n i : ℕ
⊢ i < n → swap u v (swap u v i) = i
Theorem: HTPI.swap_swap
Proof state before:
u v n i : ℕ
⊢ i < n → swap u v (swap u v i) = i
Tactic:
assume h : i < n
Proof state after:
u v n i : ℕ
h : i < n
⊢ swap u v (swap u v i) = i
Theorem: HTPI.swap_swap
Proof state before:
u v n i : ℕ
h : i < n
⊢ swap u v (swap u v i) = i
Tactic:
by_cases h1 : i = u
Proof state after:
case pos
u v n i : ℕ
h : i < n
h1 : i = u
⊢ swap u v (swap u v i) = i

case neg
u v n i : ℕ
h : i < n
h1 : ¬i = u
⊢ swap u v (swap u v i) = i
Theorem: HTPI.swap_swap
Proof state before:
case pos
u v n i : ℕ
h : i < n
h1 : i = u
⊢ swap u v (swap u v i) = i
Tactic:
rewrite [h1, swap_fst, swap_snd]
Proof state after:
case pos
u v n i : ℕ
h : i < n
h1 : i = u
⊢ u = u
Theorem: HTPI.swap_swap
Proof state before:
case pos
u v n i : ℕ
h : i < n
h1 : i = u
⊢ u = u
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.swap_swap
Proof state before:
case neg
u v n i : ℕ
h : i < n
h1 : ¬i = u
⊢ swap u v (swap u v i) = i
Tactic:
by_cases h2 : i = v
Proof state after:
case pos
u v n i : ℕ
h : i < n
h1 : ¬i = u
h2 : i = v
⊢ swap u v (swap u v i) = i

case neg
u v n i : ℕ
h : i < n
h1 : ¬i = u
h2 : ¬i = v
⊢ swap u v (swap u v i) = i
Theorem: HTPI.swap_swap
Proof state before:
case pos
u v n i : ℕ
h : i < n
h1 : ¬i = u
h2 : i = v
⊢ swap u v (swap u v i) = i
Tactic:
rewrite [h2, swap_snd, swap_fst]
Proof state after:
case pos
u v n i : ℕ
h : i < n
h1 : ¬i = u
h2 : i = v
⊢ v = v
Theorem: HTPI.swap_swap
Proof state before:
case pos
u v n i : ℕ
h : i < n
h1 : ¬i = u
h2 : i = v
⊢ v = v
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.swap_swap
Proof state before:
case neg
u v n i : ℕ
h : i < n
h1 : ¬i = u
h2 : ¬i = v
⊢ swap u v (swap u v i) = i
Tactic:
rewrite [swap_other h1 h2, swap_other h1 h2]
Proof state after:
case neg
u v n i : ℕ
h : i < n
h1 : ¬i = u
h2 : ¬i = v
⊢ i = i
Theorem: HTPI.swap_swap
Proof state before:
case neg
u v n i : ℕ
h : i < n
h1 : ¬i = u
h2 : ¬i = v
⊢ i = i
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.trivial_swap
Proof state before:
u : ℕ
⊢ swap u u = id
Tactic:
apply funext
Proof state after:
case h
u : ℕ
⊢ ∀ (x : ℕ), swap u u x = id x
Theorem: HTPI.trivial_swap
Proof state before:
case h
u : ℕ
⊢ ∀ (x : ℕ), swap u u x = id x
Tactic:
fix x : Nat
Proof state after:
case h
u x : ℕ
⊢ swap u u x = id x
Theorem: HTPI.trivial_swap
Proof state before:
case h
u x : ℕ
⊢ swap u u x = id x
Tactic:
by_cases h1 : x = u
Proof state after:
case pos
u x : ℕ
h1 : x = u
⊢ swap u u x = id x

case neg
u x : ℕ
h1 : ¬x = u
⊢ swap u u x = id x
Theorem: HTPI.trivial_swap
Proof state before:
case pos
u x : ℕ
h1 : x = u
⊢ swap u u x = id x
Tactic:
rewrite [h1, swap_fst]
Proof state after:
case pos
u x : ℕ
h1 : x = u
⊢ u = id u
Theorem: HTPI.trivial_swap
Proof state before:
case pos
u x : ℕ
h1 : x = u
⊢ u = id u
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.trivial_swap
Proof state before:
case neg
u x : ℕ
h1 : ¬x = u
⊢ swap u u x = id x
Tactic:
rewrite [swap_other h1 h1]
Proof state after:
case neg
u x : ℕ
h1 : ¬x = u
⊢ x = id x
Theorem: HTPI.trivial_swap
Proof state before:
case neg
u x : ℕ
h1 : ¬x = u
⊢ x = id x
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.prod_eq_fun
Proof state before:
m : ℕ
f g : ℕ → ZMod m
k : ℕ
⊢ ∀ (n : ℕ), (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
Tactic:
by_induc
Proof state after:
case Base_Case
m : ℕ
f g : ℕ → ZMod m
k : ℕ
⊢ (∀ i < 0, f (k + i) = g (k + i)) → prod_seq 0 k f = prod_seq 0 k g

case Induction_Step
m : ℕ
f g : ℕ → ZMod m
k : ℕ
⊢ ∀ (n : ℕ),
    ((∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g) →
      (∀ i < n + 1, f (k + i) = g (k + i)) → prod_seq (n + 1) k f = prod_seq (n + 1) k g
Theorem: HTPI.prod_eq_fun
Proof state before:
case Base_Case
m : ℕ
f g : ℕ → ZMod m
k : ℕ
⊢ (∀ i < 0, f (k + i) = g (k + i)) → prod_seq 0 k f = prod_seq 0 k g
Tactic:
assume h : (∀ i < 0, f (k + i) = g (k + i))
Proof state after:
case Base_Case
m : ℕ
f g : ℕ → ZMod m
k : ℕ
h : ∀ i < 0, f (k + i) = g (k + i)
⊢ prod_seq 0 k f = prod_seq 0 k g
Theorem: HTPI.prod_eq_fun
Proof state before:
case Base_Case
m : ℕ
f g : ℕ → ZMod m
k : ℕ
h : ∀ i < 0, f (k + i) = g (k + i)
⊢ prod_seq 0 k f = prod_seq 0 k g
Tactic:
rewrite [prod_seq_base, prod_seq_base]
Proof state after:
case Base_Case
m : ℕ
f g : ℕ → ZMod m
k : ℕ
h : ∀ i < 0, f (k + i) = g (k + i)
⊢ [1]_m = [1]_m
Theorem: HTPI.prod_eq_fun
Proof state before:
case Base_Case
m : ℕ
f g : ℕ → ZMod m
k : ℕ
h : ∀ i < 0, f (k + i) = g (k + i)
⊢ [1]_m = [1]_m
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.prod_eq_fun
Proof state before:
case Induction_Step
m : ℕ
f g : ℕ → ZMod m
k : ℕ
⊢ ∀ (n : ℕ),
    ((∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g) →
      (∀ i < n + 1, f (k + i) = g (k + i)) → prod_seq (n + 1) k f = prod_seq (n + 1) k g
Tactic:
fix n : Nat
Proof state after:
case Induction_Step
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
⊢ ((∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g) →
    (∀ i < n + 1, f (k + i) = g (k + i)) → prod_seq (n + 1) k f = prod_seq (n + 1) k g
Theorem: HTPI.prod_eq_fun
Proof state before:
case Induction_Step
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
⊢ ((∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g) →
    (∀ i < n + 1, f (k + i) = g (k + i)) → prod_seq (n + 1) k f = prod_seq (n + 1) k g
Tactic:
assume ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
Proof state after:
case Induction_Step
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
⊢ (∀ i < n + 1, f (k + i) = g (k + i)) → prod_seq (n + 1) k f = prod_seq (n + 1) k g
Theorem: HTPI.prod_eq_fun
Proof state before:
case Induction_Step
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
⊢ (∀ i < n + 1, f (k + i) = g (k + i)) → prod_seq (n + 1) k f = prod_seq (n + 1) k g
Tactic:
assume h1 : ∀ i < n + 1, f (k + i) = g (k + i)
Proof state after:
case Induction_Step
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
⊢ prod_seq (n + 1) k f = prod_seq (n + 1) k g
Theorem: HTPI.prod_eq_fun
Proof state before:
case Induction_Step
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
⊢ prod_seq (n + 1) k f = prod_seq (n + 1) k g
Tactic:
have h2 : ∀ i < n, f (k + i) = g (k + i) := by
  fix i : Nat
  assume h2 : i < n
  have h3 : i < n + 1 := by linarith
  show f (k + i) = g (k + i) from h1 i h3
  done
Proof state after:
case Induction_Step
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
h2 : ∀ i < n, f (k + i) = g (k + i)
⊢ prod_seq (n + 1) k f = prod_seq (n + 1) k g
Theorem: HTPI.prod_eq_fun
Proof state before:
case Induction_Step
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
h2 : ∀ i < n, f (k + i) = g (k + i)
⊢ prod_seq (n + 1) k f = prod_seq (n + 1) k g
Tactic:
have h3 : prod_seq n k f = prod_seq n k g := ih h2
Proof state after:
case Induction_Step
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
h2 : ∀ i < n, f (k + i) = g (k + i)
h3 : prod_seq n k f = prod_seq n k g
⊢ prod_seq (n + 1) k f = prod_seq (n + 1) k g
Theorem: HTPI.prod_eq_fun
Proof state before:
case Induction_Step
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
h2 : ∀ i < n, f (k + i) = g (k + i)
h3 : prod_seq n k f = prod_seq n k g
⊢ prod_seq (n + 1) k f = prod_seq (n + 1) k g
Tactic:
have h4 : n < n + 1 := Nat.lt_succ_self n
Proof state after:
case Induction_Step
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
h2 : ∀ i < n, f (k + i) = g (k + i)
h3 : prod_seq n k f = prod_seq n k g
h4 : n < n + 1
⊢ prod_seq (n + 1) k f = prod_seq (n + 1) k g
Theorem: HTPI.prod_eq_fun
Proof state before:
case Induction_Step
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
h2 : ∀ i < n, f (k + i) = g (k + i)
h3 : prod_seq n k f = prod_seq n k g
h4 : n < n + 1
⊢ prod_seq (n + 1) k f = prod_seq (n + 1) k g
Tactic:
rewrite [prod_seq_step, prod_seq_step, h3, h1 n h4]
Proof state after:
case Induction_Step
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
h2 : ∀ i < n, f (k + i) = g (k + i)
h3 : prod_seq n k f = prod_seq n k g
h4 : n < n + 1
⊢ prod_seq n k g * g (k + n) = prod_seq n k g * g (k + n)
Theorem: HTPI.prod_eq_fun
Proof state before:
case Induction_Step
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
h2 : ∀ i < n, f (k + i) = g (k + i)
h3 : prod_seq n k f = prod_seq n k g
h4 : n < n + 1
⊢ prod_seq n k g * g (k + n) = prod_seq n k g * g (k + n)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.prod_eq_fun
Proof state before:
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
⊢ ∀ i < n, f (k + i) = g (k + i)
Tactic:
fix i : Nat
Proof state after:
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
i : ℕ
⊢ i < n → f (k + i) = g (k + i)
Theorem: HTPI.prod_eq_fun
Proof state before:
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
i : ℕ
⊢ i < n → f (k + i) = g (k + i)
Tactic:
assume h2 : i < n
Proof state after:
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
i : ℕ
h2 : i < n
⊢ f (k + i) = g (k + i)
Theorem: HTPI.prod_eq_fun
Proof state before:
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
i : ℕ
h2 : i < n
⊢ f (k + i) = g (k + i)
Tactic:
have h3 : i < n + 1 := by linarith
Proof state after:
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
i : ℕ
h2 : i < n
h3 : i < n + 1
⊢ f (k + i) = g (k + i)
Theorem: HTPI.prod_eq_fun
Proof state before:
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
i : ℕ
h2 : i < n
h3 : i < n + 1
⊢ f (k + i) = g (k + i)
Tactic:
show f (k + i) = g (k + i) from h1 i h3
Proof state after:
no goals
Theorem: HTPI.prod_eq_fun
Proof state before:
m : ℕ
f g : ℕ → ZMod m
k n : ℕ
ih : (∀ i < n, f (k + i) = g (k + i)) → prod_seq n k f = prod_seq n k g
h1 : ∀ i < n + 1, f (k + i) = g (k + i)
i : ℕ
h2 : i < n
⊢ i < n + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.swap_prod_eq_prod_below
Proof state before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
⊢ prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
Tactic:
have h2 : ∀ (i : Nat), i < u → (f ∘ swap u n) (0 + i) = f (0 + i) := by
  fix i : Nat
  assume h2 : i < u
  have h3 : 0 + i ≠ u := by linarith
  have h4 : 0 + i ≠ n := by linarith
  rewrite [comp_def, swap_other h3 h4]
  rfl
  done
Proof state after:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ∀ i < u, (f ∘ swap u n) (0 + i) = f (0 + i)
⊢ prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f