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

State before:
m : ℕ
⊢ ∀ (k : ℕ), invertible (prod_seq k 0 (F m))
Tactic:
by_induc
State after:
case Base_Case
m : ℕ
⊢ invertible (prod_seq 0 0 (F m))

case Induction_Step
m : ℕ
⊢ ∀ (k : ℕ), invertible (prod_seq k 0 (F m)) → invertible (prod_seq (k + 1) 0 (F m))

State before:
case Base_Case
m : ℕ
⊢ invertible (prod_seq 0 0 (F m))
Tactic:
apply Exists.intro [1]_m
State after:
case Base_Case
m : ℕ
⊢ prod_seq 0 0 (F m) * [1]_m = [1]_m

State before:
case Base_Case
m : ℕ
⊢ prod_seq 0 0 (F m) * [1]_m = [1]_m
Tactic:
show prod_seq 0 0 (F m) * [1]_m = [1]_m from
  calc prod_seq 0 0 (F m) * [1]_m
    _ = [1]_m * [1]_m := by rw [prod_seq_base]
    _ = [1]_m := Theorem_7_3_6_7 ([1]_m)
State after:
no goals

State before:
m : ℕ
⊢ prod_seq 0 0 (F m) * [1]_m = [1]_m * [1]_m
Tactic:
rw [prod_seq_base]
State after:
no goals

State before:
case Induction_Step
m : ℕ
⊢ ∀ (k : ℕ), invertible (prod_seq k 0 (F m)) → invertible (prod_seq (k + 1) 0 (F m))
Tactic:
fix k : Nat
State after:
case Induction_Step
m k : ℕ
⊢ invertible (prod_seq k 0 (F m)) → invertible (prod_seq (k + 1) 0 (F m))

State before:
case Induction_Step
m k : ℕ
⊢ invertible (prod_seq k 0 (F m)) → invertible (prod_seq (k + 1) 0 (F m))
Tactic:
assume ih : invertible (prod_seq k 0 (F m))
State after:
case Induction_Step
m k : ℕ
ih : invertible (prod_seq k 0 (F m))
⊢ invertible (prod_seq (k + 1) 0 (F m))

State before:
case Induction_Step
m k : ℕ
ih : invertible (prod_seq k 0 (F m))
⊢ invertible (prod_seq (k + 1) 0 (F m))
Tactic:
rewrite [prod_seq_zero_step]
State after:
case Induction_Step
m k : ℕ
ih : invertible (prod_seq k 0 (F m))
⊢ invertible (prod_seq k 0 (F m) * F m k)

State before:
case Induction_Step
m k : ℕ
ih : invertible (prod_seq k 0 (F m))
⊢ invertible (prod_seq k 0 (F m) * F m k)
Tactic:
show invertible (prod_seq k 0 (F m) * (F m k)) from
  (prod_inv_iff_inv ih (F m k)).rtl (F_invertible m k)
State after:
no goals