Theorem: Permutation.sign_cyclic_cons (Fifteen/Data/Permutation/Sign.lean)

State before:
m n✝ n : Nat
i : Fin n
l : List (Fin n)
h : ¬i ∈ l
⊢ sign (cyclic (i :: l)) = (List.length l % 2 == 1)
Tactic:
dsimp [cyclic]
State after:
m n✝ n : Nat
i : Fin n
l : List (Fin n)
h : ¬i ∈ l
⊢ sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)

State before:
m n✝ n : Nat
i : Fin n
l : List (Fin n)
h : ¬i ∈ l
⊢ sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
Tactic:
induction l with
| nil => exact sign_one
| cons j l IH =>
  dsimp
  rewrite [List.mem_cons, not_or] at h
  rewrite [sign_swap _ i j h.1, IH h.2, Bool.eq_iff_iff]
  conv =>
    lhs; rewrite [Nat.not_beq_eq_true_eq]
  conv =>
    rhs; rewrite [beq_iff_eq, Nat.succ_eq_add_one, Nat.add_mod]
    change (l.length % 2 + 1) % 2 = 1
  cases l.length.mod_two_eq_zero_or_one
  all_goals (rename_i h; simp only [h])
State after:
no goals

State before:
case nil
m n✝ n : Nat
i : Fin n
h : ¬i ∈ []
⊢ sign (List.foldr (fun j x => swap x i j) 1 []) = (List.length [] % 2 == 1)
Tactic:
exact sign_one
State after:
no goals

State before:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i ∈ j :: l
⊢ sign (List.foldr (fun j x => swap x i j) 1 (j :: l)) = (List.length (j :: l) % 2 == 1)
Tactic:
dsimp
State after:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i ∈ j :: l
⊢ sign (swap (List.foldr (fun j x => swap x i j) 1 l) i j) = (Nat.succ (List.length l) % 2 == 1)

State before:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i ∈ j :: l
⊢ sign (swap (List.foldr (fun j x => swap x i j) 1 l) i j) = (Nat.succ (List.length l) % 2 == 1)
Tactic:
rewrite [List.mem_cons, not_or] at h
State after:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ sign (swap (List.foldr (fun j x => swap x i j) 1 l) i j) = (Nat.succ (List.length l) % 2 == 1)

State before:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ sign (swap (List.foldr (fun j x => swap x i j) 1 l) i j) = (Nat.succ (List.length l) % 2 == 1)
Tactic:
rewrite [sign_swap _ i j h.1, IH h.2, Bool.eq_iff_iff]
State after:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ (!List.length l % 2 == 1) = true ↔ (Nat.succ (List.length l) % 2 == 1) = true

State before:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ (!List.length l % 2 == 1) = true ↔ (Nat.succ (List.length l) % 2 == 1) = true
Tactic:
conv =>
  lhs; rewrite [Nat.not_beq_eq_true_eq]
State after:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ ¬List.length l % 2 = 1 ↔ (Nat.succ (List.length l) % 2 == 1) = true

State before:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ ¬List.length l % 2 = 1 ↔ (Nat.succ (List.length l) % 2 == 1) = true
Tactic:
conv =>
  rhs; rewrite [beq_iff_eq, Nat.succ_eq_add_one, Nat.add_mod]
  change (l.length % 2 + 1) % 2 = 1
State after:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1

State before:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1
Tactic:
cases l.length.mod_two_eq_zero_or_one
State after:
case cons.inl
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
h✝ : List.length l % 2 = 0
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1

case cons.inr
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
h✝ : List.length l % 2 = 1
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1

State before:
case cons.inl
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
h✝ : List.length l % 2 = 0
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1

case cons.inr
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
h✝ : List.length l % 2 = 1
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1
Tactic:
all_goals (rename_i h; simp only [h])
State after:
no goals

State before:
case cons.inr
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
h✝ : List.length l % 2 = 1
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1
Tactic:
(rename_i h; simp only [h])
State after:
no goals

State before:
case cons.inr
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
h✝ : List.length l % 2 = 1
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1
Tactic:
rename_i h
State after:
case cons.inr
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h✝ : ¬i = j ∧ ¬i ∈ l
h : List.length l % 2 = 1
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1

State before:
case cons.inr
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h✝ : ¬i = j ∧ ¬i ∈ l
h : List.length l % 2 = 1
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1
Tactic:
simp only [h]
State after:
no goals