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

State before:
m a : ℕ
h1 : rel_prime m a
⊢ ∀ (k : ℕ), prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
Tactic:
by_induc
State after:
case Base_Case
m a : ℕ
h1 : rel_prime m a
⊢ prod_seq 0 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m 0 * prod_seq 0 0 (F m)

case Induction_Step
m a : ℕ
h1 : rel_prime m a
⊢ ∀ (k : ℕ),
    prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) →
      prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)

State before:
case Base_Case
m a : ℕ
h1 : rel_prime m a
⊢ prod_seq 0 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m 0 * prod_seq 0 0 (F m)
Tactic:
show prod_seq 0 0 ((F m) ∘ (G m a)) =
      [a]_m ^ (num_rp_below m 0) * prod_seq 0 0 (F m) from
  calc prod_seq 0 0 ((F m) ∘ (G m a))
    _ = [1]_m := prod_seq_base _ _
    _ = [a]_m ^ 0 * [1]_m := by ring
    _ = [a]_m ^ (num_rp_below m 0) * prod_seq 0 0 (F m) := by
          rw [num_rp_below_base, prod_seq_base]
State after:
no goals

State before:
m a : ℕ
h1 : rel_prime m a
⊢ [1]_m = [↑a]_m ^ 0 * [1]_m
Tactic:
ring
State after:
no goals

State before:
m a : ℕ
h1 : rel_prime m a
⊢ [↑a]_m ^ 0 * [1]_m = [↑a]_m ^ num_rp_below m 0 * prod_seq 0 0 (F m)
Tactic:
rw [num_rp_below_base, prod_seq_base]
State after:
no goals

State before:
case Induction_Step
m a : ℕ
h1 : rel_prime m a
⊢ ∀ (k : ℕ),
    prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) →
      prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Tactic:
fix k : Nat
State after:
case Induction_Step
m a : ℕ
h1 : rel_prime m a
k : ℕ
⊢ prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) →
    prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)

State before:
case Induction_Step
m a : ℕ
h1 : rel_prime m a
k : ℕ
⊢ prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) →
    prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Tactic:
assume ih : prod_seq k 0 ((F m) ∘ (G m a)) =
  [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m)
State after:
case Induction_Step
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
⊢ prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)

State before:
case Induction_Step
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
⊢ prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Tactic:
by_cases h2 : rel_prime m k
State after:
case pos
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : rel_prime m k
⊢ prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)

case neg
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : ¬rel_prime m k
⊢ prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)

State before:
case pos
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : rel_prime m k
⊢ prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Tactic:
show prod_seq (k + 1) 0 ((F m) ∘ (G m a)) =
    [a]_m ^ (num_rp_below m (k + 1)) *
    prod_seq (k + 1) 0 (F m) from
  calc prod_seq (k + 1) 0 ((F m) ∘ (G m a))
    _ = prod_seq k 0 ((F m) ∘ (G m a)) *
        F m (G m a k) := prod_seq_zero_step _ _
    _ = [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) *
        F m (G m a k) := by rw [ih]
    _ = [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) *
        ([a]_m * F m k) := by rw [FG_rp h1 h2]
    _ = [a]_m ^ ((num_rp_below m k) + 1) *
        ((prod_seq k 0 (F m)) * F m k) := by ring
    _ = [a]_m ^ (num_rp_below m (k + 1)) *
        prod_seq (k + 1) 0 (F m) := by
          rw [num_rp_below_step_rp h2, prod_seq_zero_step]
State after:
no goals

State before:
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : rel_prime m k
⊢ prod_seq k 0 (F m ∘ G m a) * F m (G m a k) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) * F m (G m a k)
Tactic:
rw [ih]
State after:
no goals

State before:
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : rel_prime m k
⊢ [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) * F m (G m a k) =
    [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) * ([↑a]_m * F m k)
Tactic:
rw [FG_rp h1 h2]
State after:
no goals

State before:
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : rel_prime m k
⊢ [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) * ([↑a]_m * F m k) =
    [↑a]_m ^ (num_rp_below m k + 1) * (prod_seq k 0 (F m) * F m k)
Tactic:
ring
State after:
no goals

State before:
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : rel_prime m k
⊢ [↑a]_m ^ (num_rp_below m k + 1) * (prod_seq k 0 (F m) * F m k) =
    [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Tactic:
rw [num_rp_below_step_rp h2, prod_seq_zero_step]
State after:
no goals

State before:
case neg
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : ¬rel_prime m k
⊢ prod_seq (k + 1) 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Tactic:
show prod_seq (k + 1) 0 ((F m) ∘ (G m a)) =
    [a]_m ^ (num_rp_below m (k + 1)) *
    prod_seq (k + 1) 0 (F m) from
  calc prod_seq (k + 1) 0 ((F m) ∘ (G m a))
    _ = prod_seq k 0 ((F m) ∘ (G m a)) *
        F m (G m a k) := prod_seq_zero_step _ _
    _ = [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) *
        F m (G m a k) := by rw [ih]
    _ = [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) *
        ([1]_m) := by rw [FG_not_rp h1 h2]
    _ = [a]_m ^ (num_rp_below m k) *
        (prod_seq k 0 (F m) * ([1]_m)) := by ring
    _ = [a]_m ^ (num_rp_below m (k + 1)) *
        prod_seq (k + 1) 0 (F m) := by
          rw [num_rp_below_step_not_rp h2, prod_seq_zero_step,
          F_not_rp_def h2]
State after:
no goals

State before:
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : ¬rel_prime m k
⊢ prod_seq k 0 (F m ∘ G m a) * F m (G m a k) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) * F m (G m a k)
Tactic:
rw [ih]
State after:
no goals

State before:
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : ¬rel_prime m k
⊢ [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) * F m (G m a k) =
    [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) * [1]_m
Tactic:
rw [FG_not_rp h1 h2]
State after:
no goals

State before:
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : ¬rel_prime m k
⊢ [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m) * [1]_m = [↑a]_m ^ num_rp_below m k * (prod_seq k 0 (F m) * [1]_m)
Tactic:
ring
State after:
no goals

State before:
m a : ℕ
h1 : rel_prime m a
k : ℕ
ih : prod_seq k 0 (F m ∘ G m a) = [↑a]_m ^ num_rp_below m k * prod_seq k 0 (F m)
h2 : ¬rel_prime m k
⊢ [↑a]_m ^ num_rp_below m k * (prod_seq k 0 (F m) * [1]_m) = [↑a]_m ^ num_rp_below m (k + 1) * prod_seq (k + 1) 0 (F m)
Tactic:
rw [num_rp_below_step_not_rp h2, prod_seq_zero_step,
F_not_rp_def h2]
State after:
no goals