Theorem: HTPI.break_prod_twice (HTPILib/Chap7.lean)

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals