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

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

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

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]
State after:
case Base_Case
m : ℕ
f g : ℕ → ZMod m
k : ℕ
h : ∀ i < 0, f (k + i) = g (k + i)
⊢ [1]_m = [1]_m

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

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

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

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

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

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

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

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

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

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

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

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

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

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