internlm/Lean-Github huggingface dataset:
Theorem: HTPI.swap_prod_eq_prod_below
Proof state before:
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
Tactic:
show prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f from
  prod_eq_fun (f ∘ swap u n) f 0 u h2
Proof state after:
no goals
Theorem: HTPI.swap_prod_eq_prod_below
Proof state before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
⊢ ∀ i < u, (f ∘ swap u n) (0 + i) = f (0 + i)
Tactic:
fix i : Nat
Proof state after:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
⊢ i < u → (f ∘ swap u n) (0 + i) = f (0 + i)
Theorem: HTPI.swap_prod_eq_prod_below
Proof state before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
⊢ i < u → (f ∘ swap u n) (0 + i) = f (0 + i)
Tactic:
assume h2 : i < u
Proof state after:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
⊢ (f ∘ swap u n) (0 + i) = f (0 + i)
Theorem: HTPI.swap_prod_eq_prod_below
Proof state before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
⊢ (f ∘ swap u n) (0 + i) = f (0 + i)
Tactic:
have h3 : 0 + i ≠ u := by linarith
Proof state after:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
h3 : 0 + i ≠ u
⊢ (f ∘ swap u n) (0 + i) = f (0 + i)
Theorem: HTPI.swap_prod_eq_prod_below
Proof state before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
h3 : 0 + i ≠ u
⊢ (f ∘ swap u n) (0 + i) = f (0 + i)
Tactic:
have h4 : 0 + i ≠ n := by linarith
Proof state after:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
h3 : 0 + i ≠ u
h4 : 0 + i ≠ n
⊢ (f ∘ swap u n) (0 + i) = f (0 + i)
Theorem: HTPI.swap_prod_eq_prod_below
Proof state before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
h3 : 0 + i ≠ u
h4 : 0 + i ≠ n
⊢ (f ∘ swap u n) (0 + i) = f (0 + i)
Tactic:
rewrite [comp_def, swap_other h3 h4]
Proof state after:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
h3 : 0 + i ≠ u
h4 : 0 + i ≠ n
⊢ f (0 + i) = f (0 + i)
Theorem: HTPI.swap_prod_eq_prod_below
Proof state before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
h3 : 0 + i ≠ u
h4 : 0 + i ≠ n
⊢ f (0 + i) = f (0 + i)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.swap_prod_eq_prod_below
Proof state before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
⊢ 0 + i ≠ u
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
i : ℕ
h2 : i < u
h3 : 0 + i ≠ u
⊢ 0 + i ≠ n
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.swap_prod_eq_prod_between
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
⊢ prod_seq j (u + 1) (f ∘ swap u n) = prod_seq j (u + 1) f
Tactic:
have h2 : ∀ i < j, (f ∘ swap u n) (u + 1 + i) = f (u + 1 + i) := by
  fix i : Nat
  assume h2 : i < j
  have h3 : u + 1 + i ≠ u := by linarith
  have h4 : u + 1 + i ≠ n := by linarith
  rewrite [comp_def, swap_other h3 h4]
  rfl
Proof state after:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
h2 : ∀ i < j, (f ∘ swap u n) (u + 1 + i) = f (u + 1 + i)
⊢ prod_seq j (u + 1) (f ∘ swap u n) = prod_seq j (u + 1) f
Theorem: HTPI.swap_prod_eq_prod_between
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
h2 : ∀ i < j, (f ∘ swap u n) (u + 1 + i) = f (u + 1 + i)
⊢ prod_seq j (u + 1) (f ∘ swap u n) = prod_seq j (u + 1) f
Tactic:
show prod_seq j (u + 1) (f ∘ swap u n) = prod_seq j (u + 1) f from
  prod_eq_fun (f ∘ swap u n) f (u + 1) j h2
Proof state after:
no goals
Theorem: HTPI.swap_prod_eq_prod_between
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
⊢ ∀ i < j, (f ∘ swap u n) (u + 1 + i) = f (u + 1 + i)
Tactic:
fix i : Nat
Proof state after:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
i : ℕ
⊢ i < j → (f ∘ swap u n) (u + 1 + i) = f (u + 1 + i)
Theorem: HTPI.swap_prod_eq_prod_between
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
i : ℕ
⊢ i < j → (f ∘ swap u n) (u + 1 + i) = f (u + 1 + i)
Tactic:
assume h2 : i < j
Proof state after:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
i : ℕ
h2 : i < j
⊢ (f ∘ swap u n) (u + 1 + i) = f (u + 1 + i)
Theorem: HTPI.swap_prod_eq_prod_between
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
i : ℕ
h2 : i < j
⊢ (f ∘ swap u n) (u + 1 + i) = f (u + 1 + i)
Tactic:
have h3 : u + 1 + i ≠ u := by linarith
Proof state after:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
i : ℕ
h2 : i < j
h3 : u + 1 + i ≠ u
⊢ (f ∘ swap u n) (u + 1 + i) = f (u + 1 + i)
Theorem: HTPI.swap_prod_eq_prod_between
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
i : ℕ
h2 : i < j
h3 : u + 1 + i ≠ u
⊢ (f ∘ swap u n) (u + 1 + i) = f (u + 1 + i)
Tactic:
have h4 : u + 1 + i ≠ n := by linarith
Proof state after:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
i : ℕ
h2 : i < j
h3 : u + 1 + i ≠ u
h4 : u + 1 + i ≠ n
⊢ (f ∘ swap u n) (u + 1 + i) = f (u + 1 + i)
Theorem: HTPI.swap_prod_eq_prod_between
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
i : ℕ
h2 : i < j
h3 : u + 1 + i ≠ u
h4 : u + 1 + i ≠ n
⊢ (f ∘ swap u n) (u + 1 + i) = f (u + 1 + i)
Tactic:
rewrite [comp_def, swap_other h3 h4]
Proof state after:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
i : ℕ
h2 : i < j
h3 : u + 1 + i ≠ u
h4 : u + 1 + i ≠ n
⊢ f (u + 1 + i) = f (u + 1 + i)
Theorem: HTPI.swap_prod_eq_prod_between
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
i : ℕ
h2 : i < j
h3 : u + 1 + i ≠ u
h4 : u + 1 + i ≠ n
⊢ f (u + 1 + i) = f (u + 1 + i)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.swap_prod_eq_prod_between
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
i : ℕ
h2 : i < j
⊢ u + 1 + i ≠ u
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.swap_prod_eq_prod_between
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
i : ℕ
h2 : i < j
h3 : u + 1 + i ≠ u
⊢ u + 1 + i ≠ n
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.break_prod
Proof state before:
m n : ℕ
f : ℕ → ZMod m
⊢ ∀ (j : ℕ), prod_seq (n + j) 0 f = prod_seq n 0 f * prod_seq j n f
Tactic:
by_induc
Proof state after:
case Base_Case
m n : ℕ
f : ℕ → ZMod m
⊢ prod_seq (n + 0) 0 f = prod_seq n 0 f * prod_seq 0 n f

case Induction_Step
m n : ℕ
f : ℕ → ZMod m
⊢ ∀ (j : ℕ),
    prod_seq (n + j) 0 f = prod_seq n 0 f * prod_seq j n f →
      prod_seq (n + (j + 1)) 0 f = prod_seq n 0 f * prod_seq (j + 1) n f
Theorem: HTPI.break_prod
Proof state before:
case Base_Case
m n : ℕ
f : ℕ → ZMod m
⊢ prod_seq (n + 0) 0 f = prod_seq n 0 f * prod_seq 0 n f
Tactic:
have h : n + 0 = n := by rfl
Proof state after:
case Base_Case
m n : ℕ
f : ℕ → ZMod m
h : n + 0 = n
⊢ prod_seq (n + 0) 0 f = prod_seq n 0 f * prod_seq 0 n f
Theorem: HTPI.break_prod
Proof state before:
case Base_Case
m n : ℕ
f : ℕ → ZMod m
h : n + 0 = n
⊢ prod_seq (n + 0) 0 f = prod_seq n 0 f * prod_seq 0 n f
Tactic:
rewrite [prod_seq_base, h, Theorem_7_3_6_7]
Proof state after:
case Base_Case
m n : ℕ
f : ℕ → ZMod m
h : n + 0 = n
⊢ prod_seq n 0 f = prod_seq n 0 f
Theorem: HTPI.break_prod
Proof state before:
case Base_Case
m n : ℕ
f : ℕ → ZMod m
h : n + 0 = n
⊢ prod_seq n 0 f = prod_seq n 0 f
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.break_prod
Proof state before:
m n : ℕ
f : ℕ → ZMod m
⊢ n + 0 = n
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.break_prod
Proof state before:
case Induction_Step
m n : ℕ
f : ℕ → ZMod m
⊢ ∀ (j : ℕ),
    prod_seq (n + j) 0 f = prod_seq n 0 f * prod_seq j n f →
      prod_seq (n + (j + 1)) 0 f = prod_seq n 0 f * prod_seq (j + 1) n f
Tactic:
fix j : Nat
Proof state after:
case Induction_Step
m n : ℕ
f : ℕ → ZMod m
j : ℕ
⊢ prod_seq (n + j) 0 f = prod_seq n 0 f * prod_seq j n f →
    prod_seq (n + (j + 1)) 0 f = prod_seq n 0 f * prod_seq (j + 1) n f
Theorem: HTPI.break_prod
Proof state before:
case Induction_Step
m n : ℕ
f : ℕ → ZMod m
j : ℕ
⊢ prod_seq (n + j) 0 f = prod_seq n 0 f * prod_seq j n f →
    prod_seq (n + (j + 1)) 0 f = prod_seq n 0 f * prod_seq (j + 1) n f
Tactic:
assume ih : prod_seq (n + j) 0 f = prod_seq n 0 f * prod_seq j n f
Proof state after:
case Induction_Step
m n : ℕ
f : ℕ → ZMod m
j : ℕ
ih : prod_seq (n + j) 0 f = prod_seq n 0 f * prod_seq j n f
⊢ prod_seq (n + (j + 1)) 0 f = prod_seq n 0 f * prod_seq (j + 1) n f
Theorem: HTPI.break_prod
Proof state before:
case Induction_Step
m n : ℕ
f : ℕ → ZMod m
j : ℕ
ih : prod_seq (n + j) 0 f = prod_seq n 0 f * prod_seq j n f
⊢ prod_seq (n + (j + 1)) 0 f = prod_seq n 0 f * prod_seq (j + 1) n f
Tactic:
rewrite [←add_assoc, prod_seq_zero_step, prod_seq_step, ih, mul_assoc]
Proof state after:
case Induction_Step
m n : ℕ
f : ℕ → ZMod m
j : ℕ
ih : prod_seq (n + j) 0 f = prod_seq n 0 f * prod_seq j n f
⊢ prod_seq n 0 f * (prod_seq j n f * f (n + j)) = prod_seq n 0 f * (prod_seq j n f * f (n + j))
Theorem: HTPI.break_prod
Proof state before:
case Induction_Step
m n : ℕ
f : ℕ → ZMod m
j : ℕ
ih : prod_seq (n + j) 0 f = prod_seq n 0 f * prod_seq j n f
⊢ prod_seq n 0 f * (prod_seq j n f * f (n + j)) = prod_seq n 0 f * (prod_seq j n f * f (n + j))
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.break_prod_twice
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
⊢ prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
Tactic:
have h2 : prod_seq (n + 1) 0 f = prod_seq n 0 f * prod_seq 1 n f :=
  break_prod n f 1
Proof state after:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
h2 : prod_seq (n + 1) 0 f = prod_seq n 0 f * prod_seq 1 n f
⊢ prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
Theorem: HTPI.break_prod_twice
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
h2 : prod_seq (n + 1) 0 f = prod_seq n 0 f * prod_seq 1 n f
⊢ prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
Tactic:
rewrite [prod_one] at h2
Proof state after:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
h2 : prod_seq (n + 1) 0 f = prod_seq n 0 f * f n
⊢ prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
Theorem: HTPI.break_prod_twice
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
h2 : prod_seq (n + 1) 0 f = prod_seq n 0 f * f n
⊢ prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
Tactic:
have h3 : prod_seq (u + 1 + j) 0 f = prod_seq (u + 1) 0 f * prod_seq j (u + 1) f :=
  break_prod (u + 1) f j
Proof state after:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
h2 : prod_seq (n + 1) 0 f = prod_seq n 0 f * f n
h3 : prod_seq (u + 1 + j) 0 f = prod_seq (u + 1) 0 f * prod_seq j (u + 1) f
⊢ prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
Theorem: HTPI.break_prod_twice
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
h2 : prod_seq (n + 1) 0 f = prod_seq n 0 f * f n
h3 : prod_seq (u + 1 + j) 0 f = prod_seq (u + 1) 0 f * prod_seq j (u + 1) f
⊢ prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
Tactic:
rewrite [←h1] at h3
Proof state after:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
h2 : prod_seq (n + 1) 0 f = prod_seq n 0 f * f n
h3 : prod_seq n 0 f = prod_seq (u + 1) 0 f * prod_seq j (u + 1) f
⊢ prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
Theorem: HTPI.break_prod_twice
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
h2 : prod_seq (n + 1) 0 f = prod_seq n 0 f * f n
h3 : prod_seq n 0 f = prod_seq (u + 1) 0 f * prod_seq j (u + 1) f
⊢ prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
Tactic:
have h4 : prod_seq (u + 1) 0 f = prod_seq u 0 f * prod_seq 1 u f :=
  break_prod u f 1
Proof state after:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
h2 : prod_seq (n + 1) 0 f = prod_seq n 0 f * f n
h3 : prod_seq n 0 f = prod_seq (u + 1) 0 f * prod_seq j (u + 1) f
h4 : prod_seq (u + 1) 0 f = prod_seq u 0 f * prod_seq 1 u f
⊢ prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
Theorem: HTPI.break_prod_twice
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
h2 : prod_seq (n + 1) 0 f = prod_seq n 0 f * f n
h3 : prod_seq n 0 f = prod_seq (u + 1) 0 f * prod_seq j (u + 1) f
h4 : prod_seq (u + 1) 0 f = prod_seq u 0 f * prod_seq 1 u f
⊢ prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
Tactic:
rewrite [prod_one] at h4
Proof state after:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
h2 : prod_seq (n + 1) 0 f = prod_seq n 0 f * f n
h3 : prod_seq n 0 f = prod_seq (u + 1) 0 f * prod_seq j (u + 1) f
h4 : prod_seq (u + 1) 0 f = prod_seq u 0 f * f u
⊢ prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
Theorem: HTPI.break_prod_twice
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
h2 : prod_seq (n + 1) 0 f = prod_seq n 0 f * f n
h3 : prod_seq n 0 f = prod_seq (u + 1) 0 f * prod_seq j (u + 1) f
h4 : prod_seq (u + 1) 0 f = prod_seq u 0 f * f u
⊢ prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
Tactic:
rewrite [h3, h4] at h2
Proof state after:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
h2 : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
h3 : prod_seq n 0 f = prod_seq (u + 1) 0 f * prod_seq j (u + 1) f
h4 : prod_seq (u + 1) 0 f = prod_seq u 0 f * f u
⊢ prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
Theorem: HTPI.break_prod_twice
Proof state before:
m u j n : ℕ
f : ℕ → ZMod m
h1 : n = u + 1 + j
h2 : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
h3 : prod_seq n 0 f = prod_seq (u + 1) 0 f * prod_seq j (u + 1) f
h4 : prod_seq (u + 1) 0 f = prod_seq u 0 f * f u
⊢ prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
Tactic:
show prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n from h2
Proof state after:
no goals
Theorem: HTPI.swap_prod_eq_prod
Proof state before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
by_cases h2 : u = n
Proof state after:
case pos
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : u = n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f

case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Theorem: HTPI.swap_prod_eq_prod
Proof state before:
case pos
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : u = n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
rewrite [h2, trivial_swap n]
Proof state after:
case pos
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : u = n
⊢ prod_seq (n + 1) 0 (f ∘ id) = prod_seq (n + 1) 0 f
Theorem: HTPI.swap_prod_eq_prod
Proof state before:
case pos
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : u = n
⊢ prod_seq (n + 1) 0 (f ∘ id) = prod_seq (n + 1) 0 f
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.swap_prod_eq_prod
Proof state before:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
have h3 : u + 1 ≤ n := Nat.lt_of_le_of_ne h1 h2
Proof state after:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Theorem: HTPI.swap_prod_eq_prod
Proof state before:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
obtain (j : Nat) (h4 : n = u + 1 + j) from Nat.exists_eq_add_of_le h3
Proof state after:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Theorem: HTPI.swap_prod_eq_prod
Proof state before:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
have break_f : prod_seq (n + 1) 0 f =
  prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n :=
  break_prod_twice f h4
Proof state after:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Theorem: HTPI.swap_prod_eq_prod
Proof state before:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
have break_fs : prod_seq (n + 1) 0 (f ∘ swap u n) =
  prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u *
  prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n :=
  break_prod_twice (f ∘ swap u n) h4
Proof state after:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Theorem: HTPI.swap_prod_eq_prod
Proof state before:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
have f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) =
  prod_seq u 0 f := swap_prod_eq_prod_below f h1
Proof state after:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Theorem: HTPI.swap_prod_eq_prod
Proof state before:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
have f_eq_fs_btwn : prod_seq j (u + 1) (f ∘ swap u n) =
  prod_seq j (u + 1) f := swap_prod_eq_prod_between f h4
Proof state after:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
f_eq_fs_btwn : prod_seq j (u + 1) (f ∘ swap u n) = prod_seq j (u + 1) f
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Theorem: HTPI.swap_prod_eq_prod
Proof state before:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
f_eq_fs_btwn : prod_seq j (u + 1) (f ∘ swap u n) = prod_seq j (u + 1) f
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
show prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f from
  calc prod_seq (n + 1) 0 (f ∘ swap u n)
    _ = prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u *
        prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n :=
          break_fs
    _ = prod_seq u 0 f * (f ∘ swap u n) u *
        prod_seq j (u + 1) f * (f ∘ swap u n) n := by
          rw [f_eq_fs_below, f_eq_fs_btwn]
    _ = prod_seq u 0 f * f (swap u n u) *
        prod_seq j (u + 1) f * f (swap u n n) := by rfl
    _ = prod_seq u 0 f * f n * prod_seq j (u + 1) f * f u := by
          rw [swap_fst, swap_snd]
    _ = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n := by ring
    _ = prod_seq (n + 1) 0 f := break_f.symm
Proof state after:
no goals
Theorem: HTPI.swap_prod_eq_prod
Proof state before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
f_eq_fs_btwn : prod_seq j (u + 1) (f ∘ swap u n) = prod_seq j (u + 1) f
⊢ prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n =
    prod_seq u 0 f * (f ∘ swap u n) u * prod_seq j (u + 1) f * (f ∘ swap u n) n
Tactic:
rw [f_eq_fs_below, f_eq_fs_btwn]
Proof state after:
no goals
Theorem: HTPI.swap_prod_eq_prod
Proof state before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
f_eq_fs_btwn : prod_seq j (u + 1) (f ∘ swap u n) = prod_seq j (u + 1) f
⊢ prod_seq u 0 f * (f ∘ swap u n) u * prod_seq j (u + 1) f * (f ∘ swap u n) n =
    prod_seq u 0 f * f (swap u n u) * prod_seq j (u + 1) f * f (swap u n n)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.swap_prod_eq_prod
Proof state before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
f_eq_fs_btwn : prod_seq j (u + 1) (f ∘ swap u n) = prod_seq j (u + 1) f
⊢ prod_seq u 0 f * f (swap u n u) * prod_seq j (u + 1) f * f (swap u n n) =
    prod_seq u 0 f * f n * prod_seq j (u + 1) f * f u
Tactic:
rw [swap_fst, swap_snd]
Proof state after:
no goals
Theorem: HTPI.swap_prod_eq_prod
Proof state before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
f_eq_fs_btwn : prod_seq j (u + 1) (f ∘ swap u n) = prod_seq j (u + 1) f
⊢ prod_seq u 0 f * f n * prod_seq j (u + 1) f * f u = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.perm_prod
Proof state before:
m : ℕ
f : ℕ → ZMod m
⊢ ∀ (n : ℕ) (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
Tactic:
by_induc
Proof state after:
case Base_Case
m : ℕ
f : ℕ → ZMod m
⊢ ∀ (g : ℕ → ℕ), perm_below 0 g → prod_seq 0 0 f = prod_seq 0 0 (f ∘ g)

case Induction_Step
m : ℕ
f : ℕ → ZMod m
⊢ ∀ (n : ℕ),
    (∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)) →
      ∀ (g : ℕ → ℕ), perm_below (n + 1) g → prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)
Theorem: HTPI.perm_prod
Proof state before:
case Base_Case
m : ℕ
f : ℕ → ZMod m
⊢ ∀ (g : ℕ → ℕ), perm_below 0 g → prod_seq 0 0 f = prod_seq 0 0 (f ∘ g)
Tactic:
fix g : Nat → Nat
Proof state after:
case Base_Case
m : ℕ
f : ℕ → ZMod m
g : ℕ → ℕ
⊢ perm_below 0 g → prod_seq 0 0 f = prod_seq 0 0 (f ∘ g)
Theorem: HTPI.perm_prod
Proof state before:
case Base_Case
m : ℕ
f : ℕ → ZMod m
g : ℕ → ℕ
⊢ perm_below 0 g → prod_seq 0 0 f = prod_seq 0 0 (f ∘ g)
Tactic:
assume h1 : perm_below 0 g
Proof state after:
case Base_Case
m : ℕ
f : ℕ → ZMod m
g : ℕ → ℕ
h1 : perm_below 0 g
⊢ prod_seq 0 0 f = prod_seq 0 0 (f ∘ g)