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

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

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

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

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

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

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

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

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

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

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