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

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

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

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]
State after:
case Base_Case
m n : ℕ
f : ℕ → ZMod m
h : n + 0 = n
⊢ prod_seq n 0 f = prod_seq n 0 f

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

State before:
m n : ℕ
f : ℕ → ZMod m
⊢ n + 0 = n
Tactic:
rfl
State after:
no goals

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

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

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

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