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

State before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
by_cases h2 : u = n
State after:
case pos
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : u = n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f

case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f

State before:
case pos
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : u = n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
rewrite [h2, trivial_swap n]
State after:
case pos
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : u = n
⊢ prod_seq (n + 1) 0 (f ∘ id) = prod_seq (n + 1) 0 f

State before:
case pos
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : u = n
⊢ prod_seq (n + 1) 0 (f ∘ id) = prod_seq (n + 1) 0 f
Tactic:
rfl
State after:
no goals

State before:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
have h3 : u + 1 ≤ n := Nat.lt_of_le_of_ne h1 h2
State after:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f

State before:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
obtain (j : Nat) (h4 : n = u + 1 + j) from Nat.exists_eq_add_of_le h3
State after:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f

State before:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
have break_f : prod_seq (n + 1) 0 f =
  prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n :=
  break_prod_twice f h4
State after:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f

State before:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
have break_fs : prod_seq (n + 1) 0 (f ∘ swap u n) =
  prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u *
  prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n :=
  break_prod_twice (f ∘ swap u n) h4
State after:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f

State before:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
have f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) =
  prod_seq u 0 f := swap_prod_eq_prod_below f h1
State after:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f

State before:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
have f_eq_fs_btwn : prod_seq j (u + 1) (f ∘ swap u n) =
  prod_seq j (u + 1) f := swap_prod_eq_prod_between f h4
State after:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
f_eq_fs_btwn : prod_seq j (u + 1) (f ∘ swap u n) = prod_seq j (u + 1) f
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f

State before:
case neg
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
f_eq_fs_btwn : prod_seq j (u + 1) (f ∘ swap u n) = prod_seq j (u + 1) f
⊢ prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f
Tactic:
show prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f from
  calc prod_seq (n + 1) 0 (f ∘ swap u n)
    _ = prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u *
        prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n :=
          break_fs
    _ = prod_seq u 0 f * (f ∘ swap u n) u *
        prod_seq j (u + 1) f * (f ∘ swap u n) n := by
          rw [f_eq_fs_below, f_eq_fs_btwn]
    _ = prod_seq u 0 f * f (swap u n u) *
        prod_seq j (u + 1) f * f (swap u n n) := by rfl
    _ = prod_seq u 0 f * f n * prod_seq j (u + 1) f * f u := by
          rw [swap_fst, swap_snd]
    _ = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n := by ring
    _ = prod_seq (n + 1) 0 f := break_f.symm
State after:
no goals

State before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
f_eq_fs_btwn : prod_seq j (u + 1) (f ∘ swap u n) = prod_seq j (u + 1) f
⊢ prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n =
    prod_seq u 0 f * (f ∘ swap u n) u * prod_seq j (u + 1) f * (f ∘ swap u n) n
Tactic:
rw [f_eq_fs_below, f_eq_fs_btwn]
State after:
no goals

State before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
f_eq_fs_btwn : prod_seq j (u + 1) (f ∘ swap u n) = prod_seq j (u + 1) f
⊢ prod_seq u 0 f * (f ∘ swap u n) u * prod_seq j (u + 1) f * (f ∘ swap u n) n =
    prod_seq u 0 f * f (swap u n u) * prod_seq j (u + 1) f * f (swap u n n)
Tactic:
rfl
State after:
no goals

State before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
f_eq_fs_btwn : prod_seq j (u + 1) (f ∘ swap u n) = prod_seq j (u + 1) f
⊢ prod_seq u 0 f * f (swap u n u) * prod_seq j (u + 1) f * f (swap u n n) =
    prod_seq u 0 f * f n * prod_seq j (u + 1) f * f u
Tactic:
rw [swap_fst, swap_snd]
State after:
no goals

State before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ¬u = n
h3 : u + 1 ≤ n
j : ℕ
h4 : n = u + 1 + j
break_f : prod_seq (n + 1) 0 f = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
break_fs :
  prod_seq (n + 1) 0 (f ∘ swap u n) =
    prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u * prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n
f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
f_eq_fs_btwn : prod_seq j (u + 1) (f ∘ swap u n) = prod_seq j (u + 1) f
⊢ prod_seq u 0 f * f n * prod_seq j (u + 1) f * f u = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n
Tactic:
ring
State after:
no goals