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

State before:
m : ℕ
f : ℕ → ZMod m
⊢ ∀ (n : ℕ) (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
Tactic:
by_induc
State after:
case Base_Case
m : ℕ
f : ℕ → ZMod m
⊢ ∀ (g : ℕ → ℕ), perm_below 0 g → prod_seq 0 0 f = prod_seq 0 0 (f ∘ g)

case Induction_Step
m : ℕ
f : ℕ → ZMod m
⊢ ∀ (n : ℕ),
    (∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)) →
      ∀ (g : ℕ → ℕ), perm_below (n + 1) g → prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)

State before:
case Base_Case
m : ℕ
f : ℕ → ZMod m
⊢ ∀ (g : ℕ → ℕ), perm_below 0 g → prod_seq 0 0 f = prod_seq 0 0 (f ∘ g)
Tactic:
fix g : Nat → Nat
State after:
case Base_Case
m : ℕ
f : ℕ → ZMod m
g : ℕ → ℕ
⊢ perm_below 0 g → prod_seq 0 0 f = prod_seq 0 0 (f ∘ g)

State before:
case Base_Case
m : ℕ
f : ℕ → ZMod m
g : ℕ → ℕ
⊢ perm_below 0 g → prod_seq 0 0 f = prod_seq 0 0 (f ∘ g)
Tactic:
assume h1 : perm_below 0 g
State after:
case Base_Case
m : ℕ
f : ℕ → ZMod m
g : ℕ → ℕ
h1 : perm_below 0 g
⊢ prod_seq 0 0 f = prod_seq 0 0 (f ∘ g)

State before:
case Base_Case
m : ℕ
f : ℕ → ZMod m
g : ℕ → ℕ
h1 : perm_below 0 g
⊢ prod_seq 0 0 f = prod_seq 0 0 (f ∘ g)
Tactic:
rewrite [prod_seq_base, prod_seq_base]
State after:
case Base_Case
m : ℕ
f : ℕ → ZMod m
g : ℕ → ℕ
h1 : perm_below 0 g
⊢ [1]_m = [1]_m

State before:
case Base_Case
m : ℕ
f : ℕ → ZMod m
g : ℕ → ℕ
h1 : perm_below 0 g
⊢ [1]_m = [1]_m
Tactic:
rfl
State after:
no goals

State before:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
⊢ ∀ (n : ℕ),
    (∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)) →
      ∀ (g : ℕ → ℕ), perm_below (n + 1) g → prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)
Tactic:
fix n : Nat
State after:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
⊢ (∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)) →
    ∀ (g : ℕ → ℕ), perm_below (n + 1) g → prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)

State before:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
⊢ (∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)) →
    ∀ (g : ℕ → ℕ), perm_below (n + 1) g → prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)
Tactic:
assume ih : ∀ (g : Nat → Nat), perm_below n g →
  prod_seq n 0 f = prod_seq n 0 (f ∘ g)
State after:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
⊢ ∀ (g : ℕ → ℕ), perm_below (n + 1) g → prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)

State before:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
⊢ ∀ (g : ℕ → ℕ), perm_below (n + 1) g → prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)
Tactic:
fix g : Nat → Nat
State after:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
⊢ perm_below (n + 1) g → prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)

State before:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
⊢ perm_below (n + 1) g → prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)
Tactic:
assume g_pb : perm_below (n + 1) g
State after:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : perm_below (n + 1) g
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)

State before:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : perm_below (n + 1) g
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)
Tactic:
define at g_pb
State after:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)

State before:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)
Tactic:
have g_ob : onto_below (n + 1) g := g_pb.right.right
State after:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : onto_below (n + 1) g
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)

State before:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : onto_below (n + 1) g
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)
Tactic:
define at g_ob
State after:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)

State before:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)
Tactic:
have h1 : n < n + 1 := by linarith
State after:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)

State before:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)
Tactic:
obtain (u : Nat) (h2 : u < n + 1 ∧ g u = n) from g_ob n h1
State after:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)

State before:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)
Tactic:
have s_pb : perm_below (n + 1) (swap u n) :=
  swap_perm_below h2.left h1
State after:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)

State before:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)
Tactic:
have gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n) :=
  comp_perm_below g_pb s_pb
State after:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n)
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)

State before:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n)
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)
Tactic:
have gs_fix_n : (g ∘ swap u n) n = n :=
  calc (g ∘ swap u n) n
    _ = g (swap u n n) := by rfl
    _ = g u := by rw [swap_snd]
    _ = n := h2.right
State after:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n)
gs_fix_n : (g ∘ swap u n) n = n
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)

State before:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n)
gs_fix_n : (g ∘ swap u n) n = n
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)
Tactic:
have gs_pb_n : perm_below n (g ∘ swap u n) :=
  perm_below_fixed gs_pb_n1 gs_fix_n
State after:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n)
gs_fix_n : (g ∘ swap u n) n = n
gs_pb_n : perm_below n (g ∘ swap u n)
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)

State before:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n)
gs_fix_n : (g ∘ swap u n) n = n
gs_pb_n : perm_below n (g ∘ swap u n)
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)
Tactic:
have gs_prod : prod_seq n 0 f = prod_seq n 0 (f ∘ (g ∘ swap u n)) :=
  ih (g ∘ swap u n) gs_pb_n
State after:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n)
gs_fix_n : (g ∘ swap u n) n = n
gs_pb_n : perm_below n (g ∘ swap u n)
gs_prod : prod_seq n 0 f = prod_seq n 0 (f ∘ g ∘ swap u n)
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)

State before:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n)
gs_fix_n : (g ∘ swap u n) n = n
gs_pb_n : perm_below n (g ∘ swap u n)
gs_prod : prod_seq n 0 f = prod_seq n 0 (f ∘ g ∘ swap u n)
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)
Tactic:
have h3 : u ≤ n := by linarith
State after:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n)
gs_fix_n : (g ∘ swap u n) n = n
gs_pb_n : perm_below n (g ∘ swap u n)
gs_prod : prod_seq n 0 f = prod_seq n 0 (f ∘ g ∘ swap u n)
h3 : u ≤ n
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)

State before:
case Induction_Step
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n)
gs_fix_n : (g ∘ swap u n) n = n
gs_pb_n : perm_below n (g ∘ swap u n)
gs_prod : prod_seq n 0 f = prod_seq n 0 (f ∘ g ∘ swap u n)
h3 : u ≤ n
⊢ prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g)
Tactic:
show prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g) from
  calc prod_seq (n + 1) 0 f
    _ = prod_seq n 0 f * f n := prod_seq_zero_step n f
    _ = prod_seq n 0 (f ∘ (g ∘ swap u n)) *
        f ((g ∘ swap u n) n) := by rw [gs_prod, gs_fix_n]
    _ = prod_seq n 0 (f ∘ g ∘ swap u n) *
        (f ∘ g ∘ swap u n) n := by rfl
    _ = prod_seq (n + 1) 0 (f ∘ g ∘ swap u n) :=
          (prod_seq_zero_step n (f ∘ g ∘ swap u n)).symm
    _ = prod_seq (n + 1) 0 ((f ∘ g) ∘ swap u n) := by rfl
    _ = prod_seq (n + 1) 0 (f ∘ g) := swap_prod_eq_prod (f ∘ g) h3
State after:
no goals

State before:
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
⊢ n < n + 1
Tactic:
linarith
State after:
no goals

State before:
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n)
⊢ (g ∘ swap u n) n = g (swap u n n)
Tactic:
rfl
State after:
no goals

State before:
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n)
⊢ g (swap u n n) = g u
Tactic:
rw [swap_snd]
State after:
no goals

State before:
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n)
gs_fix_n : (g ∘ swap u n) n = n
gs_pb_n : perm_below n (g ∘ swap u n)
gs_prod : prod_seq n 0 f = prod_seq n 0 (f ∘ g ∘ swap u n)
⊢ u ≤ n
Tactic:
linarith
State after:
no goals

State before:
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n)
gs_fix_n : (g ∘ swap u n) n = n
gs_pb_n : perm_below n (g ∘ swap u n)
gs_prod : prod_seq n 0 f = prod_seq n 0 (f ∘ g ∘ swap u n)
h3 : u ≤ n
⊢ prod_seq n 0 f * f n = prod_seq n 0 (f ∘ g ∘ swap u n) * f ((g ∘ swap u n) n)
Tactic:
rw [gs_prod, gs_fix_n]
State after:
no goals

State before:
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n)
gs_fix_n : (g ∘ swap u n) n = n
gs_pb_n : perm_below n (g ∘ swap u n)
gs_prod : prod_seq n 0 f = prod_seq n 0 (f ∘ g ∘ swap u n)
h3 : u ≤ n
⊢ prod_seq n 0 (f ∘ g ∘ swap u n) * f ((g ∘ swap u n) n) = prod_seq n 0 (f ∘ g ∘ swap u n) * (f ∘ g ∘ swap u n) n
Tactic:
rfl
State after:
no goals

State before:
m : ℕ
f : ℕ → ZMod m
n : ℕ
ih : ∀ (g : ℕ → ℕ), perm_below n g → prod_seq n 0 f = prod_seq n 0 (f ∘ g)
g : ℕ → ℕ
g_pb : maps_below (n + 1) g ∧ one_one_below (n + 1) g ∧ onto_below (n + 1) g
g_ob : ∀ k < n + 1, ∃ i < n + 1, g i = k
h1 : n < n + 1
u : ℕ
h2 : u < n + 1 ∧ g u = n
s_pb : perm_below (n + 1) (swap u n)
gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n)
gs_fix_n : (g ∘ swap u n) n = n
gs_pb_n : perm_below n (g ∘ swap u n)
gs_prod : prod_seq n 0 f = prod_seq n 0 (f ∘ g ∘ swap u n)
h3 : u ≤ n
⊢ prod_seq (n + 1) 0 (f ∘ g ∘ swap u n) = prod_seq (n + 1) 0 ((f ∘ g) ∘ swap u n)
Tactic:
rfl
State after:
no goals