internlm/Lean-Github huggingface dataset:
Theorem: HTPI.perm_prod
Proof 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]
Proof state after:
case Base_Case
m : ℕ
f : ℕ → ZMod m
g : ℕ → ℕ
h1 : perm_below 0 g
⊢ [1]_m = [1]_m
Theorem: HTPI.perm_prod
Proof state before:
case Base_Case
m : ℕ
f : ℕ → ZMod m
g : ℕ → ℕ
h1 : perm_below 0 g
⊢ [1]_m = [1]_m
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.perm_prod
Proof 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
Proof 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)
Theorem: HTPI.perm_prod
Proof 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)
Proof 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)
Theorem: HTPI.perm_prod
Proof 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
Proof 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)
Theorem: HTPI.perm_prod
Proof 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
Proof 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)
Theorem: HTPI.perm_prod
Proof 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
Proof 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)
Theorem: HTPI.perm_prod
Proof 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
Proof 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)
Theorem: HTPI.perm_prod
Proof 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
Proof 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)
Theorem: HTPI.perm_prod
Proof 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
Proof 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)
Theorem: HTPI.perm_prod
Proof 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
Proof 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)
Theorem: HTPI.perm_prod
Proof 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
Proof 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)
Theorem: HTPI.perm_prod
Proof 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
Proof 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)
Theorem: HTPI.perm_prod
Proof 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
Proof 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)
Theorem: HTPI.perm_prod
Proof 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
Proof 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)
Theorem: HTPI.perm_prod
Proof 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
Proof 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)
Theorem: HTPI.perm_prod
Proof 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
Proof 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)
Theorem: HTPI.perm_prod
Proof 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
Proof state after:
no goals
Theorem: HTPI.perm_prod
Proof 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
Proof state after:
no goals
Theorem: HTPI.perm_prod
Proof 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
Proof state after:
no goals
Theorem: HTPI.perm_prod
Proof 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]
Proof state after:
no goals
Theorem: HTPI.perm_prod
Proof 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
Proof state after:
no goals
Theorem: HTPI.perm_prod
Proof 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]
Proof state after:
no goals
Theorem: HTPI.perm_prod
Proof 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
Proof state after:
no goals
Theorem: HTPI.perm_prod
Proof 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
Proof state after:
no goals
Theorem: HTPI.F_invertible
Proof state before:
m i : ℕ
⊢ invertible (F m i)
Tactic:
by_cases h : rel_prime m i
Proof state after:
case pos
m i : ℕ
h : rel_prime m i
⊢ invertible (F m i)

case neg
m i : ℕ
h : ¬rel_prime m i
⊢ invertible (F m i)
Theorem: HTPI.F_invertible
Proof state before:
case pos
m i : ℕ
h : rel_prime m i
⊢ invertible (F m i)
Tactic:
rewrite [F_rp_def h]
Proof state after:
case pos
m i : ℕ
h : rel_prime m i
⊢ invertible [↑i]_m
Theorem: HTPI.F_invertible
Proof state before:
case pos
m i : ℕ
h : rel_prime m i
⊢ invertible [↑i]_m
Tactic:
show invertible [i]_m from (Theorem_7_3_7 m i).rtl h
Proof state after:
no goals
Theorem: HTPI.F_invertible
Proof state before:
case neg
m i : ℕ
h : ¬rel_prime m i
⊢ invertible (F m i)
Tactic:
rewrite [F_not_rp_def h]
Proof state after:
case neg
m i : ℕ
h : ¬rel_prime m i
⊢ invertible [1]_m
Theorem: HTPI.F_invertible
Proof state before:
case neg
m i : ℕ
h : ¬rel_prime m i
⊢ invertible [1]_m
Tactic:
apply Exists.intro [1]_m
Proof state after:
case neg
m i : ℕ
h : ¬rel_prime m i
⊢ [1]_m * [1]_m = [1]_m
Theorem: HTPI.F_invertible
Proof state before:
case neg
m i : ℕ
h : ¬rel_prime m i
⊢ [1]_m * [1]_m = [1]_m
Tactic:
show [1]_m * [1]_m = [1]_m from Theorem_7_3_6_7 [1]_m
Proof state after:
no goals
Theorem: HTPI.Fprod_invertible
Proof state before:
m : ℕ
⊢ ∀ (k : ℕ), invertible (prod_seq k 0 (F m))
Tactic:
by_induc
Proof state after:
case Base_Case
m : ℕ
⊢ invertible (prod_seq 0 0 (F m))

case Induction_Step
m : ℕ
⊢ ∀ (k : ℕ), invertible (prod_seq k 0 (F m)) → invertible (prod_seq (k + 1) 0 (F m))
Theorem: HTPI.Fprod_invertible
Proof state before:
case Base_Case
m : ℕ
⊢ invertible (prod_seq 0 0 (F m))
Tactic:
apply Exists.intro [1]_m
Proof state after:
case Base_Case
m : ℕ
⊢ prod_seq 0 0 (F m) * [1]_m = [1]_m
Theorem: HTPI.Fprod_invertible
Proof state before:
case Base_Case
m : ℕ
⊢ prod_seq 0 0 (F m) * [1]_m = [1]_m
Tactic:
show prod_seq 0 0 (F m) * [1]_m = [1]_m from
  calc prod_seq 0 0 (F m) * [1]_m
    _ = [1]_m * [1]_m := by rw [prod_seq_base]
    _ = [1]_m := Theorem_7_3_6_7 ([1]_m)
Proof state after:
no goals
Theorem: HTPI.Fprod_invertible
Proof state before:
m : ℕ
⊢ prod_seq 0 0 (F m) * [1]_m = [1]_m * [1]_m
Tactic:
rw [prod_seq_base]
Proof state after:
no goals
Theorem: HTPI.Fprod_invertible
Proof state before:
case Induction_Step
m : ℕ
⊢ ∀ (k : ℕ), invertible (prod_seq k 0 (F m)) → invertible (prod_seq (k + 1) 0 (F m))
Tactic:
fix k : Nat
Proof state after:
case Induction_Step
m k : ℕ
⊢ invertible (prod_seq k 0 (F m)) → invertible (prod_seq (k + 1) 0 (F m))
Theorem: HTPI.Fprod_invertible
Proof state before:
case Induction_Step
m k : ℕ
⊢ invertible (prod_seq k 0 (F m)) → invertible (prod_seq (k + 1) 0 (F m))
Tactic:
assume ih : invertible (prod_seq k 0 (F m))
Proof state after:
case Induction_Step
m k : ℕ
ih : invertible (prod_seq k 0 (F m))
⊢ invertible (prod_seq (k + 1) 0 (F m))
Theorem: HTPI.Fprod_invertible
Proof state before:
case Induction_Step
m k : ℕ
ih : invertible (prod_seq k 0 (F m))
⊢ invertible (prod_seq (k + 1) 0 (F m))
Tactic:
rewrite [prod_seq_zero_step]
Proof state after:
case Induction_Step
m k : ℕ
ih : invertible (prod_seq k 0 (F m))
⊢ invertible (prod_seq k 0 (F m) * F m k)
Theorem: HTPI.Fprod_invertible
Proof state before:
case Induction_Step
m k : ℕ
ih : invertible (prod_seq k 0 (F m))
⊢ invertible (prod_seq k 0 (F m) * F m k)
Tactic:
show invertible (prod_seq k 0 (F m) * (F m k)) from
  (prod_inv_iff_inv ih (F m k)).rtl (F_invertible m k)
Proof state after:
no goals
Theorem: HTPI.Theorem_7_4_2
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ [↑a]_m ^ phi m = [1]_m
Tactic:
have h2 : invertible (prod_seq m 0 (F m)) := Fprod_invertible m m
Proof state after:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
⊢ [↑a]_m ^ phi m = [1]_m
Theorem: HTPI.Theorem_7_4_2
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
⊢ [↑a]_m ^ phi m = [1]_m
Tactic:
obtain (Y : ZMod m) (h3 : prod_seq m 0 (F m) * Y = [1]_m) from h2
Proof state after:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
Y : ZMod m
h3 : prod_seq m 0 (F m) * Y = [1]_m
⊢ [↑a]_m ^ phi m = [1]_m
Theorem: HTPI.Theorem_7_4_2
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
Y : ZMod m
h3 : prod_seq m 0 (F m) * Y = [1]_m
⊢ [↑a]_m ^ phi m = [1]_m
Tactic:
show [a]_m ^ (phi m) = [1]_m from
  calc [a]_m ^ (phi m)
    _ = [a]_m ^ (phi m) * [1]_m := (Theorem_7_3_6_7 _).symm
    _ = [a]_m ^ (phi m) * (prod_seq m 0 (F m) * Y) := by rw [h3]
    _ = ([a]_m ^ (phi m) * prod_seq m 0 (F m)) * Y := by ring
    _ = prod_seq m 0 (F m ∘ G m a) * Y := by rw [FG_prod h1 m, phi_def]
    _ = prod_seq m 0 (F m) * Y := by
          rw [perm_prod (F m) m (G m a) (G_perm_below h1)]
    _ = [1]_m := by rw [h3]
Proof state after:
no goals
Theorem: HTPI.Theorem_7_4_2
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
Y : ZMod m
h3 : prod_seq m 0 (F m) * Y = [1]_m
⊢ [↑a]_m ^ phi m * [1]_m = [↑a]_m ^ phi m * (prod_seq m 0 (F m) * Y)
Tactic:
rw [h3]
Proof state after:
no goals
Theorem: HTPI.Theorem_7_4_2
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
Y : ZMod m
h3 : prod_seq m 0 (F m) * Y = [1]_m
⊢ [↑a]_m ^ phi m * (prod_seq m 0 (F m) * Y) = [↑a]_m ^ phi m * prod_seq m 0 (F m) * Y
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Theorem_7_4_2
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
Y : ZMod m
h3 : prod_seq m 0 (F m) * Y = [1]_m
⊢ [↑a]_m ^ phi m * prod_seq m 0 (F m) * Y = prod_seq m 0 (F m ∘ G m a) * Y
Tactic:
rw [FG_prod h1 m, phi_def]
Proof state after:
no goals
Theorem: HTPI.Theorem_7_4_2
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
Y : ZMod m
h3 : prod_seq m 0 (F m) * Y = [1]_m
⊢ prod_seq m 0 (F m ∘ G m a) * Y = prod_seq m 0 (F m) * Y
Tactic:
rw [perm_prod (F m) m (G m a) (G_perm_below h1)]
Proof state after:
no goals
Theorem: HTPI.Theorem_7_4_2
Proof state before:
m a : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
h2 : invertible (prod_seq m 0 (F m))
Y : ZMod m
h3 : prod_seq m 0 (F m) * Y = [1]_m
⊢ prod_seq m 0 (F m) * Y = [1]_m
Tactic:
rw [h3]
Proof state after:
no goals
Theorem: HTPI.Exercise_7_4_5_Nat
Proof state before:
m a n : ℕ
⊢ [↑a]_m ^ n = [↑a ^ n]_m
Tactic:
rewrite [Exercise_7_4_5_Int]
Proof state after:
m a n : ℕ
⊢ [↑a ^ n]_m = [↑a ^ n]_m
Theorem: HTPI.Exercise_7_4_5_Nat
Proof state before:
m a n : ℕ
⊢ [↑a ^ n]_m = [↑a ^ n]_m
Tactic:
rfl
Proof state after:
no goals