internlm/Lean-Github huggingface dataset:
Theorem: Board.lt_last_of_mem_pathT
Proof state before:
case refl.h₁
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < m - ↑i - 1
ha :
  ∃ i_1,
    Fin.rlexProd { val := m - ↑i_1 - 1, isLt := (_ : m - ↑i_1 - 1 < m + 1) } (Fin.castSucc j) =
      Fin.rlexProd { val := m - ↑{ val := k, isLt := hk } - 1, isLt := (_ : m - ↑{ val := k, isLt := hk } - 1 < m + 1) }
        (Fin.castSucc j)
⊢ m - k - 1 < m
Tactic:
rewrite [← Nat.sub_add_eq]
Proof state after:
case refl.h₁
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < m - ↑i - 1
ha :
  ∃ i_1,
    Fin.rlexProd { val := m - ↑i_1 - 1, isLt := (_ : m - ↑i_1 - 1 < m + 1) } (Fin.castSucc j) =
      Fin.rlexProd { val := m - ↑{ val := k, isLt := hk } - 1, isLt := (_ : m - ↑{ val := k, isLt := hk } - 1 < m + 1) }
        (Fin.castSucc j)
⊢ m - (k + 1) < m
Theorem: Board.lt_last_of_mem_pathT
Proof state before:
case refl.h₁
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < m - ↑i - 1
ha :
  ∃ i_1,
    Fin.rlexProd { val := m - ↑i_1 - 1, isLt := (_ : m - ↑i_1 - 1 < m + 1) } (Fin.castSucc j) =
      Fin.rlexProd { val := m - ↑{ val := k, isLt := hk } - 1, isLt := (_ : m - ↑{ val := k, isLt := hk } - 1 < m + 1) }
        (Fin.castSucc j)
⊢ m - (k + 1) < m
Tactic:
exact m.sub_lt i.pos k.zero_lt_succ
Proof state after:
no goals
Theorem: Board.lt_last_of_mem_pathT
Proof state before:
case refl.h₂
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < m - ↑i - 1
ha :
  ∃ i_1,
    Fin.rlexProd { val := m - ↑i_1 - 1, isLt := (_ : m - ↑i_1 - 1 < m + 1) } (Fin.castSucc j) =
      Fin.rlexProd { val := m - ↑{ val := k, isLt := hk } - 1, isLt := (_ : m - ↑{ val := k, isLt := hk } - 1 < m + 1) }
        (Fin.castSucc j)
⊢ (m + 1) * ↑j < (m + 1) * n
Tactic:
exact Nat.mul_lt_mul_of_pos_left j.2 m.zero_lt_succ
Proof state after:
no goals
Theorem: Board.pivot_not_mem_pathT
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathT i j
Tactic:
dsimp [Board.pathT, Board.pivot]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j) ∈
      List.ofFn fun x => Fin.rlexProd { val := m - ↑x - 1, isLt := (_ : m - ↑x - 1 < m + 1) } (Fin.castSucc j)
Theorem: Board.pivot_not_mem_pathT
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j) ∈
      List.ofFn fun x => Fin.rlexProd { val := m - ↑x - 1, isLt := (_ : m - ↑x - 1 < m + 1) } (Fin.castSucc j)
Tactic:
simp only [List.mem_ofFn, not_exists]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
⊢ ∀ (x : Fin (m - ↑i - 1)),
    ¬Fin.rlexProd { val := m - ↑x - 1, isLt := (_ : m - ↑x - 1 < m + 1) } (Fin.castSucc j) =
        Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)
Theorem: Board.pivot_not_mem_pathT
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ∀ (x : Fin (m - ↑i - 1)),
    ¬Fin.rlexProd { val := m - ↑x - 1, isLt := (_ : m - ↑x - 1 < m + 1) } (Fin.castSucc j) =
        Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)
Tactic:
intro k
Proof state after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ¬Fin.rlexProd { val := m - ↑k - 1, isLt := (_ : m - ↑k - 1 < m + 1) } (Fin.castSucc j) =
      Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)
Theorem: Board.pivot_not_mem_pathT
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ¬Fin.rlexProd { val := m - ↑k - 1, isLt := (_ : m - ↑k - 1 < m + 1) } (Fin.castSucc j) =
      Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)
Tactic:
refine Fin.ne_of_val_ne (Nat.ne_of_gt ?_)
Proof state after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ↑(Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)) <
    ↑(Fin.rlexProd { val := m - ↑k - 1, isLt := (_ : m - ↑k - 1 < m + 1) } (Fin.castSucc j))
Theorem: Board.pivot_not_mem_pathT
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ↑(Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)) <
    ↑(Fin.rlexProd { val := m - ↑k - 1, isLt := (_ : m - ↑k - 1 < m + 1) } (Fin.castSucc j))
Tactic:
refine Fin.rlexProd_lt_iff.mpr (Or.inr ?_)
Proof state after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ Fin.castSucc j = Fin.castSucc j ∧ Fin.castSucc i < { val := m - ↑k - 1, isLt := (_ : m - ↑k - 1 < m + 1) }
Theorem: Board.pivot_not_mem_pathT
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ Fin.castSucc j = Fin.castSucc j ∧ Fin.castSucc i < { val := m - ↑k - 1, isLt := (_ : m - ↑k - 1 < m + 1) }
Tactic:
simp only [Fin.castSucc_lt_castSucc_iff, true_and]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ Fin.castSucc i < { val := m - ↑k - 1, isLt := (_ : m - ↑k - 1 < m + 1) }
Theorem: Board.pivot_not_mem_pathT
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ Fin.castSucc i < { val := m - ↑k - 1, isLt := (_ : m - ↑k - 1 < m + 1) }
Tactic:
show i < m-k.1-1
Proof state after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ↑i < m - ↑k - 1
Theorem: Board.pivot_not_mem_pathT
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ↑i < m - ↑k - 1
Tactic:
rewrite [← Nat.sub_add_eq]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ↑i < m - (↑k + 1)
Theorem: Board.pivot_not_mem_pathT
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ↑i < m - (↑k + 1)
Tactic:
apply Nat.lt_sub_of_add_lt
Proof state after:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ↑i + (↑k + 1) < m
Theorem: Board.pivot_not_mem_pathT
Proof state before:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ↑i + (↑k + 1) < m
Tactic:
rewrite [← Nat.add_assoc, Nat.add_comm i.1 k.1, Nat.add_assoc]
Proof state after:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ↑k + (↑i + 1) < m
Theorem: Board.pivot_not_mem_pathT
Proof state before:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ↑k + (↑i + 1) < m
Tactic:
exact Nat.add_lt_of_lt_sub k.2
Proof state after:
no goals
Theorem: Board.lt_last_of_mem_path
Proof state before:
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : a ∈ Board.path i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
conv at ha =>
  dsimp [Board.path]
  simp only [List.mem_append, or_assoc]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : a ∈ Board.pathL i j ∨ a ∈ Board.pathB n i ∨ a ∈ Board.pathR m j ∨ a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_path
Proof state before:
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : a ∈ Board.pathL i j ∨ a ∈ Board.pathB n i ∨ a ∈ Board.pathR m j ∨ a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
rcases ha with hL | hB | hR | hT
Proof state after:
case inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hL : a ∈ Board.pathL i j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hB : a ∈ Board.pathB n i
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hR : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_path
Proof state before:
case inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hL : a ∈ Board.pathL i j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hB : a ∈ Board.pathB n i
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hR : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
. exact lt_last_of_mem_pathL i j a hL
Proof state after:
case inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hB : a ∈ Board.pathB n i
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hR : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_path
Proof state before:
case inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hB : a ∈ Board.pathB n i
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hR : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
. exact lt_last_of_mem_pathB n i a hB
Proof state after:
case inr.inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hR : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_path
Proof state before:
case inr.inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hR : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
. exact lt_last_of_mem_pathR m j a hR
Proof state after:
case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_path
Proof state before:
case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
. exact lt_last_of_mem_pathT i j a hT
Proof state after:
no goals
Theorem: Board.lt_last_of_mem_path
Proof state before:
case inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hL : a ∈ Board.pathL i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
exact lt_last_of_mem_pathL i j a hL
Proof state after:
no goals
Theorem: Board.lt_last_of_mem_path
Proof state before:
case inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hB : a ∈ Board.pathB n i
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
exact lt_last_of_mem_pathB n i a hB
Proof state after:
no goals
Theorem: Board.lt_last_of_mem_path
Proof state before:
case inr.inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hR : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
exact lt_last_of_mem_pathR m j a hR
Proof state after:
no goals
Theorem: Board.lt_last_of_mem_path
Proof state before:
case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
exact lt_last_of_mem_pathT i j a hT
Proof state after:
no goals
Theorem: Board.pivot_not_mem_path
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.path i j
Tactic:
dsimp [Board.path]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathL i j ++ Board.pathB n i ++ Board.pathR m j ++ Board.pathT i j
Theorem: Board.pivot_not_mem_path
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathL i j ++ Board.pathB n i ++ Board.pathR m j ++ Board.pathT i j
Tactic:
simp only [List.mem_append, or_assoc, not_or]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathL i j ∧
    ¬Board.pivot i j ∈ Board.pathB n i ∧ ¬Board.pivot i j ∈ Board.pathR m j ∧ ¬Board.pivot i j ∈ Board.pathT i j
Theorem: Board.pivot_not_mem_path
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathL i j ∧
    ¬Board.pivot i j ∈ Board.pathB n i ∧ ¬Board.pivot i j ∈ Board.pathR m j ∧ ¬Board.pivot i j ∈ Board.pathT i j
Tactic:
exact ⟨
  pivot_not_mem_pathL i j,
  pivot_not_mem_pathB i j,
  pivot_not_mem_pathR i j,
  pivot_not_mem_pathT i j
⟩
Proof state after:
no goals
Theorem: Board.sign_cycle
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ Permutation.sign (cycle i j) = false
Tactic:
dsimp [cycle]
Proof 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
Theorem: Board.sign_cycle
Proof 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]
Proof 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)
Theorem: Board.sign_cycle
Proof 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
Proof 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)
Theorem: Board.sign_cycle
Proof 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
Proof state after:
no goals
Theorem: Board.sign_cycle
Proof 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]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬List.length (Board.path i j) % 2 = 1
Theorem: Board.sign_cycle
Proof 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]
Proof 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
Theorem: Board.sign_cycle
Proof 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]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬(n - ↑j + (m - ↑i - 1) + (n - ↑j) + (m - ↑i - 1)) % 2 = 1
Theorem: Board.sign_cycle
Proof 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]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬0 = 1
Theorem: Board.sign_cycle
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬0 = 1
Tactic:
decide
Proof state after:
no goals
Theorem: Board.sign_cycle
Proof 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]
Proof 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)
Theorem: Board.sign_cycle
Proof 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
Proof 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
Theorem: Board.sign_cycle
Proof 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
Proof 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
Theorem: Board.sign_cycle
Proof 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
Proof state after:
no goals
Theorem: randNat_range
Proof state before:
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
⊢ lo ≤ (randNat g lo hi).fst ∧ (randNat g lo hi).fst ≤ hi
Tactic:
dsimp [randNat]
Proof state after:
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
⊢ lo ≤
      (if lo > hi then hi else lo) +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) * 1000) (0, g)).fst %
          (((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) ∧
    (if lo > hi then hi else lo) +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) * 1000) (0, g)).fst %
          (((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) ≤
      hi
Theorem: randNat_range
Proof state before:
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
⊢ lo ≤
      (if lo > hi then hi else lo) +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) * 1000) (0, g)).fst %
          (((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) ∧
    (if lo > hi then hi else lo) +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) * 1000) (0, g)).fst %
          (((if lo > hi then lo else hi) - if lo > hi then hi else lo) + 1) ≤
      hi
Tactic:
simp only [if_neg (Nat.not_lt_of_le h)]
Proof state after:
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
⊢ lo ≤
      lo +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((hi - lo + 1) * 1000) (0, g)).fst %
          (hi - lo + 1) ∧
    lo +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((hi - lo + 1) * 1000) (0, g)).fst %
          (hi - lo + 1) ≤
      hi
Theorem: randNat_range
Proof state before:
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
⊢ lo ≤
      lo +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((hi - lo + 1) * 1000) (0, g)).fst %
          (hi - lo + 1) ∧
    lo +
        (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1)
              ((hi - lo + 1) * 1000) (0, g)).fst %
          (hi - lo + 1) ≤
      hi
Tactic:
generalize (randNatAux (RandomGen.range g).fst ((RandomGen.range g).snd - (RandomGen.range g).fst + 1) ((hi - lo + 1) * 1000) (0, g)).fst = x
Proof state after:
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo ≤ lo + x % (hi - lo + 1) ∧ lo + x % (hi - lo + 1) ≤ hi
Theorem: randNat_range
Proof state before:
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo ≤ lo + x % (hi - lo + 1) ∧ lo + x % (hi - lo + 1) ≤ hi
Tactic:
apply And.intro
Proof state after:
case left
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo ≤ lo + x % (hi - lo + 1)

case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo + x % (hi - lo + 1) ≤ hi
Theorem: randNat_range
Proof state before:
case left
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo ≤ lo + x % (hi - lo + 1)

case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo + x % (hi - lo + 1) ≤ hi
Tactic:
. show lo ≤ _
  exact Nat.le_add_right lo _
Proof state after:
case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo + x % (hi - lo + 1) ≤ hi
Theorem: randNat_range
Proof state before:
case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo + x % (hi - lo + 1) ≤ hi
Tactic:
. show _ ≤ hi
  conv =>
    rhs; rewrite [← Nat.sub_add_cancel h, Nat.add_comm]
  refine Nat.add_le_add_left ?_ lo
  apply Nat.le_of_lt_succ
  exact x.mod_lt (hi - lo).zero_lt_succ
Proof state after:
no goals
Theorem: randNat_range
Proof state before:
case left
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo ≤ lo + x % (hi - lo + 1)
Tactic:
exact Nat.le_add_right lo _
Proof state after:
no goals
Theorem: randNat_range
Proof state before:
case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo + x % (hi - lo + 1) ≤ hi
Tactic:
conv =>
  rhs; rewrite [← Nat.sub_add_cancel h, Nat.add_comm]
Proof state after:
case right
gen : Type u
inst : RandomGen gen
g : gen
lo hi : Nat
h : lo ≤ hi
x : Nat
⊢ lo + x % (hi - lo + 1) ≤ lo + (hi - lo)