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

State before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
⊢ prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
Tactic:
have h2 : ∀ (i : Nat), i < u → (f ∘ swap u n) (0 + i) = f (0 + i) := by
  fix i : Nat
  assume h2 : i < u
  have h3 : 0 + i ≠ u := by linarith
  have h4 : 0 + i ≠ n := by linarith
  rewrite [comp_def, swap_other h3 h4]
  rfl
  done
State after:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ∀ i < u, (f ∘ swap u n) (0 + i) = f (0 + i)
⊢ prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f

State before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
h2 : ∀ i < u, (f ∘ swap u n) (0 + i) = f (0 + i)
⊢ prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f
Tactic:
show prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f from
  prod_eq_fun (f ∘ swap u n) f 0 u h2
State after:
no goals

State before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
⊢ ∀ i < u, (f ∘ swap u n) (0 + i) = f (0 + i)
Tactic:
fix i : Nat
State after:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
⊢ i < u → (f ∘ swap u n) (0 + i) = f (0 + i)

State before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
⊢ i < u → (f ∘ swap u n) (0 + i) = f (0 + i)
Tactic:
assume h2 : i < u
State after:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
⊢ (f ∘ swap u n) (0 + i) = f (0 + i)

State before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
⊢ (f ∘ swap u n) (0 + i) = f (0 + i)
Tactic:
have h3 : 0 + i ≠ u := by linarith
State after:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
h3 : 0 + i ≠ u
⊢ (f ∘ swap u n) (0 + i) = f (0 + i)

State before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
h3 : 0 + i ≠ u
⊢ (f ∘ swap u n) (0 + i) = f (0 + i)
Tactic:
have h4 : 0 + i ≠ n := by linarith
State after:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
h3 : 0 + i ≠ u
h4 : 0 + i ≠ n
⊢ (f ∘ swap u n) (0 + i) = f (0 + i)

State before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
h3 : 0 + i ≠ u
h4 : 0 + i ≠ n
⊢ (f ∘ swap u n) (0 + i) = f (0 + i)
Tactic:
rewrite [comp_def, swap_other h3 h4]
State after:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
h3 : 0 + i ≠ u
h4 : 0 + i ≠ n
⊢ f (0 + i) = f (0 + i)

State before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
h3 : 0 + i ≠ u
h4 : 0 + i ≠ n
⊢ f (0 + i) = f (0 + i)
Tactic:
rfl
State after:
no goals

State before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
⊢ 0 + i ≠ u
Tactic:
linarith
State after:
no goals

State before:
m u n : ℕ
f : ℕ → ZMod m
h1 : u ≤ n
i : ℕ
h2 : i < u
h3 : 0 + i ≠ u
⊢ 0 + i ≠ n
Tactic:
linarith
State after:
no goals