Theorem: Board.sign_cycle (Fifteen/Data/Board/Cycle.lean)

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ Permutation.sign (cycle i j) = false
Tactic:
dsimp [cycle]
State after:
m n : Nat
i : Fin m
j : Fin n
⊢ Permutation.sign
      (Permutation.cyclic
        (Fin.restrict (Board.pivot i j) (_ : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1) ::
          List.pmap Fin.restrict (Board.path i j)
            (_ : ∀ (a : Fin ((m + 1) * (n + 1))), a ∈ Board.path i j → ↑a < (m + 1) * (n + 1) - 1))) =
    false

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ Permutation.sign
      (Permutation.cyclic
        (Fin.restrict (Board.pivot i j) (_ : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1) ::
          List.pmap Fin.restrict (Board.path i j)
            (_ : ∀ (a : Fin ((m + 1) * (n + 1))), a ∈ Board.path i j → ↑a < (m + 1) * (n + 1) - 1))) =
    false
Tactic:
rewrite [Permutation.sign_cyclic_cons]
State after:
m n : Nat
i : Fin m
j : Fin n
⊢ (List.length
          (List.pmap Fin.restrict (Board.path i j)
            (_ : ∀ (a : Fin ((m + 1) * (n + 1))), a ∈ Board.path i j → ↑a < (m + 1) * (n + 1) - 1)) %
        2 ==
      1) =
    false

m n : Nat
i : Fin m
j : Fin n
⊢ ¬Fin.restrict (Board.pivot i j) (_ : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1) ∈
      List.pmap Fin.restrict (Board.path i j)
        (_ : ∀ (a : Fin ((m + 1) * (n + 1))), a ∈ Board.path i j → ↑a < (m + 1) * (n + 1) - 1)

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ (List.length
          (List.pmap Fin.restrict (Board.path i j)
            (_ : ∀ (a : Fin ((m + 1) * (n + 1))), a ∈ Board.path i j → ↑a < (m + 1) * (n + 1) - 1)) %
        2 ==
      1) =
    false

m n : Nat
i : Fin m
j : Fin n
⊢ ¬Fin.restrict (Board.pivot i j) (_ : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1) ∈
      List.pmap Fin.restrict (Board.path i j)
        (_ : ∀ (a : Fin ((m + 1) * (n + 1))), a ∈ Board.path i j → ↑a < (m + 1) * (n + 1) - 1)
Tactic:
. simp only [List.length_pmap, beq_eq_false_iff_ne, ne_eq]
  dsimp [Board.path, Board.pathL, Board.pathB, Board.pathR, Board.pathT]
  simp only [List.length_append, List.length_ofFn]
  rewrite [Nat.add_assoc (n-j.1 + (m-i.1-1)), ← Nat.mul_two, Nat.mul_mod_left]
  decide
State after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Fin.restrict (Board.pivot i j) (_ : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1) ∈
      List.pmap Fin.restrict (Board.path i j)
        (_ : ∀ (a : Fin ((m + 1) * (n + 1))), a ∈ Board.path i j → ↑a < (m + 1) * (n + 1) - 1)

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Fin.restrict (Board.pivot i j) (_ : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1) ∈
      List.pmap Fin.restrict (Board.path i j)
        (_ : ∀ (a : Fin ((m + 1) * (n + 1))), a ∈ Board.path i j → ↑a < (m + 1) * (n + 1) - 1)
Tactic:
. simp only [List.mem_pmap, not_exists]
  intro a ha hcntr
  cases Fin.restrict_inj _ _ hcntr.2
  exact absurd hcntr.1 <| pivot_not_mem_path i j
State after:
no goals

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ (List.length
          (List.pmap Fin.restrict (Board.path i j)
            (_ : ∀ (a : Fin ((m + 1) * (n + 1))), a ∈ Board.path i j → ↑a < (m + 1) * (n + 1) - 1)) %
        2 ==
      1) =
    false
Tactic:
simp only [List.length_pmap, beq_eq_false_iff_ne, ne_eq]
State after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬List.length (Board.path i j) % 2 = 1

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬List.length (Board.path i j) % 2 = 1
Tactic:
dsimp [Board.path, Board.pathL, Board.pathB, Board.pathR, Board.pathT]
State after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬List.length
          ((((List.ofFn fun k =>
                  Fin.rlexProd (Fin.castSucc i)
                    (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k)))) ++
                List.ofFn fun k =>
                  Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i k)) (_ : ↑(Fin.succ (Fin.eadd i k)) < m + 1))
                    (Fin.last n)) ++
              List.ofFn fun x => Fin.rlexProd (Fin.last m) { val := n - ↑x - 1, isLt := (_ : n - ↑x - 1 < n + 1) }) ++
            List.ofFn fun x => Fin.rlexProd { val := m - ↑x - 1, isLt := (_ : m - ↑x - 1 < m + 1) } (Fin.castSucc j)) %
        2 =
      1

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬List.length
          ((((List.ofFn fun k =>
                  Fin.rlexProd (Fin.castSucc i)
                    (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k)))) ++
                List.ofFn fun k =>
                  Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i k)) (_ : ↑(Fin.succ (Fin.eadd i k)) < m + 1))
                    (Fin.last n)) ++
              List.ofFn fun x => Fin.rlexProd (Fin.last m) { val := n - ↑x - 1, isLt := (_ : n - ↑x - 1 < n + 1) }) ++
            List.ofFn fun x => Fin.rlexProd { val := m - ↑x - 1, isLt := (_ : m - ↑x - 1 < m + 1) } (Fin.castSucc j)) %
        2 =
      1
Tactic:
simp only [List.length_append, List.length_ofFn]
State after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬(n - ↑j + (m - ↑i - 1) + (n - ↑j) + (m - ↑i - 1)) % 2 = 1

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬(n - ↑j + (m - ↑i - 1) + (n - ↑j) + (m - ↑i - 1)) % 2 = 1
Tactic:
rewrite [Nat.add_assoc (n-j.1 + (m-i.1-1)), ← Nat.mul_two, Nat.mul_mod_left]
State after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬0 = 1

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬0 = 1
Tactic:
decide
State after:
no goals

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Fin.restrict (Board.pivot i j) (_ : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1) ∈
      List.pmap Fin.restrict (Board.path i j)
        (_ : ∀ (a : Fin ((m + 1) * (n + 1))), a ∈ Board.path i j → ↑a < (m + 1) * (n + 1) - 1)
Tactic:
simp only [List.mem_pmap, not_exists]
State after:
m n : Nat
i : Fin m
j : Fin n
⊢ ∀ (x : Fin ((m + 1) * (n + 1))) (x_1 : ↑x < (m + 1) * (n + 1) - 1),
    ¬(x ∈ Board.path i j ∧
        Fin.restrict (Board.pivot i j) (_ : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1) = Fin.restrict x x_1)

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ∀ (x : Fin ((m + 1) * (n + 1))) (x_1 : ↑x < (m + 1) * (n + 1) - 1),
    ¬(x ∈ Board.path i j ∧
        Fin.restrict (Board.pivot i j) (_ : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1) = Fin.restrict x x_1)
Tactic:
intro a ha hcntr
State after:
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : ↑a < (m + 1) * (n + 1) - 1
hcntr :
  a ∈ Board.path i j ∧
    Fin.restrict (Board.pivot i j) (_ : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1) = Fin.restrict a ha
⊢ False

State before:
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : ↑a < (m + 1) * (n + 1) - 1
hcntr :
  a ∈ Board.path i j ∧
    Fin.restrict (Board.pivot i j) (_ : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1) = Fin.restrict a ha
⊢ False
Tactic:
cases Fin.restrict_inj _ _ hcntr.2
State after:
case refl
m n : Nat
i : Fin m
j : Fin n
ha : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1
hcntr :
  Board.pivot i j ∈ Board.path i j ∧
    Fin.restrict (Board.pivot i j) (_ : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1) = Fin.restrict (Board.pivot i j) ha
⊢ False

State before:
case refl
m n : Nat
i : Fin m
j : Fin n
ha : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1
hcntr :
  Board.pivot i j ∈ Board.path i j ∧
    Fin.restrict (Board.pivot i j) (_ : ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1) = Fin.restrict (Board.pivot i j) ha
⊢ False
Tactic:
exact absurd hcntr.1 <| pivot_not_mem_path i j
State after:
no goals