internlm/Lean-Github huggingface dataset:
Theorem: Board.lt_last_of_mem_pathB
Proof state before:
case refl
m n : Nat
i : Fin m
k : Nat
hk : k < m - ↑i - 1
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i i_1)) (_ : ↑(Fin.succ (Fin.eadd i i_1)) < m + 1)) (Fin.last n) =
      Fin.rlexProd
        (Fin.castLT (Fin.succ (Fin.eadd i { val := k, isLt := hk }))
          (_ : ↑(Fin.succ (Fin.eadd i { val := k, isLt := hk })) < m + 1))
        (Fin.last n)
⊢ ↑i + k + 1 + (m + 1) * n < m + (m + 1) * n
Tactic:
refine Nat.add_lt_add_right ?_ _
Proof state after:
case refl
m n : Nat
i : Fin m
k : Nat
hk : k < m - ↑i - 1
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i i_1)) (_ : ↑(Fin.succ (Fin.eadd i i_1)) < m + 1)) (Fin.last n) =
      Fin.rlexProd
        (Fin.castLT (Fin.succ (Fin.eadd i { val := k, isLt := hk }))
          (_ : ↑(Fin.succ (Fin.eadd i { val := k, isLt := hk })) < m + 1))
        (Fin.last n)
⊢ ↑i + k + 1 < m
Theorem: Board.lt_last_of_mem_pathB
Proof state before:
case refl
m n : Nat
i : Fin m
k : Nat
hk : k < m - ↑i - 1
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i i_1)) (_ : ↑(Fin.succ (Fin.eadd i i_1)) < m + 1)) (Fin.last n) =
      Fin.rlexProd
        (Fin.castLT (Fin.succ (Fin.eadd i { val := k, isLt := hk }))
          (_ : ↑(Fin.succ (Fin.eadd i { val := k, isLt := hk })) < m + 1))
        (Fin.last n)
⊢ ↑i + k + 1 < m
Tactic:
rewrite [Nat.add_comm i.1 k, Nat.add_assoc]
Proof state after:
case refl
m n : Nat
i : Fin m
k : Nat
hk : k < m - ↑i - 1
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i i_1)) (_ : ↑(Fin.succ (Fin.eadd i i_1)) < m + 1)) (Fin.last n) =
      Fin.rlexProd
        (Fin.castLT (Fin.succ (Fin.eadd i { val := k, isLt := hk }))
          (_ : ↑(Fin.succ (Fin.eadd i { val := k, isLt := hk })) < m + 1))
        (Fin.last n)
⊢ k + (↑i + 1) < m
Theorem: Board.lt_last_of_mem_pathB
Proof state before:
case refl
m n : Nat
i : Fin m
k : Nat
hk : k < m - ↑i - 1
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i i_1)) (_ : ↑(Fin.succ (Fin.eadd i i_1)) < m + 1)) (Fin.last n) =
      Fin.rlexProd
        (Fin.castLT (Fin.succ (Fin.eadd i { val := k, isLt := hk }))
          (_ : ↑(Fin.succ (Fin.eadd i { val := k, isLt := hk })) < m + 1))
        (Fin.last n)
⊢ k + (↑i + 1) < m
Tactic:
exact Nat.add_lt_of_lt_sub hk
Proof state after:
no goals
Theorem: Board.pivot_not_mem_pathB
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathB n i
Tactic:
dsimp [Board.pathB]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈
      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)
Theorem: Board.pivot_not_mem_pathB
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈
      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)
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 (Fin.castLT (Fin.succ (Fin.eadd i x)) (_ : ↑(Fin.succ (Fin.eadd i x)) < m + 1)) (Fin.last n) =
        Board.pivot i j
Theorem: Board.pivot_not_mem_pathB
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ∀ (x : Fin (m - ↑i - 1)),
    ¬Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i x)) (_ : ↑(Fin.succ (Fin.eadd i x)) < m + 1)) (Fin.last n) =
        Board.pivot i j
Tactic:
intro k
Proof state after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ¬Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i k)) (_ : ↑(Fin.succ (Fin.eadd i k)) < m + 1)) (Fin.last n) =
      Board.pivot i j
Theorem: Board.pivot_not_mem_pathB
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ¬Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i k)) (_ : ↑(Fin.succ (Fin.eadd i k)) < m + 1)) (Fin.last n) =
      Board.pivot i 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)
⊢ ↑(Board.pivot i j) <
    ↑(Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i k)) (_ : ↑(Fin.succ (Fin.eadd i k)) < m + 1)) (Fin.last n))
Theorem: Board.pivot_not_mem_pathB
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ↑(Board.pivot i j) <
    ↑(Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i k)) (_ : ↑(Fin.succ (Fin.eadd i k)) < m + 1)) (Fin.last n))
Tactic:
exact Fin.rlexProd_lt_of_snd _ _ j.2
Proof state after:
no goals
Theorem: Board.lt_last_of_mem_pathR
Proof state before:
m n : Nat
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
conv at ha => dsimp [Board.pathR]; rw [List.mem_ofFn]
Proof state after:
m n : Nat
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : ∃ i, Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } = a
⊢ ↑a < (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_pathR
Proof state before:
m n : Nat
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : ∃ i, Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } = a
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
have ⟨⟨k,hk⟩,ha⟩ := ha
Proof state after:
m n : Nat
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha✝ : ∃ i, Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } = a
k : Nat
hk : k < n - ↑j
ha :
  Fin.rlexProd (Fin.last m)
      { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) } =
    a
⊢ ↑a < (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_pathR
Proof state before:
m n : Nat
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha✝ : ∃ i, Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } = a
k : Nat
hk : k < n - ↑j
ha :
  Fin.rlexProd (Fin.last m)
      { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) } =
    a
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
cases ha
Proof state after:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ ↑(Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }) <
    (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_pathR
Proof state before:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ ↑(Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }) <
    (m + 1) * (n + 1) - 1
Tactic:
simp
Proof state after:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ m + (m + 1) * (n - k - 1) < (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_pathR
Proof state before:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ m + (m + 1) * (n - k - 1) < (m + 1) * (n + 1) - 1
Tactic:
conv => rhs; change (m+1)*n + m; rw [Nat.add_comm _ m]
Proof state after:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ m + (m + 1) * (n - k - 1) < m + (m + 1) * n
Theorem: Board.lt_last_of_mem_pathR
Proof state before:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ m + (m + 1) * (n - k - 1) < m + (m + 1) * n
Tactic:
refine Nat.add_lt_add_left ?_ m
Proof state after:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ (m + 1) * (n - k - 1) < (m + 1) * n
Theorem: Board.lt_last_of_mem_pathR
Proof state before:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ (m + 1) * (n - k - 1) < (m + 1) * n
Tactic:
refine Nat.mul_lt_mul_of_pos_left ?_ m.zero_lt_succ
Proof state after:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ n - k - 1 < n
Theorem: Board.lt_last_of_mem_pathR
Proof state before:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ n - k - 1 < n
Tactic:
rewrite [← Nat.sub_add_eq]
Proof state after:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ n - (k + 1) < n
Theorem: Board.lt_last_of_mem_pathR
Proof state before:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ n - (k + 1) < n
Tactic:
exact n.sub_lt j.pos k.zero_lt_succ
Proof state after:
no goals
Theorem: Board.pivot_not_mem_pathR
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathR m j
Tactic:
dsimp [Board.pathR, 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 (Fin.last m) { val := n - ↑x - 1, isLt := (_ : n - ↑x - 1 < n + 1) }
Theorem: Board.pivot_not_mem_pathR
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 (Fin.last m) { val := n - ↑x - 1, isLt := (_ : n - ↑x - 1 < n + 1) }
Tactic:
simp only [List.mem_ofFn, not_exists]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
⊢ ∀ (x : Fin (n - ↑j)),
    ¬Fin.rlexProd (Fin.last m) { val := n - ↑x - 1, isLt := (_ : n - ↑x - 1 < n + 1) } =
        Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)
Theorem: Board.pivot_not_mem_pathR
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ∀ (x : Fin (n - ↑j)),
    ¬Fin.rlexProd (Fin.last m) { val := n - ↑x - 1, isLt := (_ : n - ↑x - 1 < n + 1) } =
        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 (n - ↑j)
⊢ ¬Fin.rlexProd (Fin.last m) { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } =
      Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)
Theorem: Board.pivot_not_mem_pathR
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ¬Fin.rlexProd (Fin.last m) { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } =
      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 (n - ↑j)
⊢ ↑(Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)) <
    ↑(Fin.rlexProd (Fin.last m) { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) })
Theorem: Board.pivot_not_mem_pathR
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ↑(Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)) <
    ↑(Fin.rlexProd (Fin.last m) { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) })
Tactic:
apply Fin.rlexProd_lt_iff.mpr
Proof state after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ Fin.castSucc j < { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∨
    Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∧ Fin.castSucc i < Fin.last m
Theorem: Board.pivot_not_mem_pathR
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ Fin.castSucc j < { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∨
    Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∧ Fin.castSucc i < Fin.last m
Tactic:
show j.1 < n - k.1 - 1 ∨ _ = _ ∧ i.1 < m
Proof state after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ↑j < n - ↑k - 1 ∨ Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∧ ↑i < m
Theorem: Board.pivot_not_mem_pathR
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ↑j < n - ↑k - 1 ∨ Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∧ ↑i < m
Tactic:
rewrite [Decidable.or_iff_not_imp_left]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ¬↑j < n - ↑k - 1 → Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∧ ↑i < m
Theorem: Board.pivot_not_mem_pathR
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ¬↑j < n - ↑k - 1 → Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∧ ↑i < m
Tactic:
simp only [Nat.not_lt, Fin.is_lt, and_true]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ n - ↑k - 1 ≤ ↑j → Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) }
Theorem: Board.pivot_not_mem_pathR
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ n - ↑k - 1 ≤ ↑j → Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) }
Tactic:
intro h
Proof state after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) }
Theorem: Board.pivot_not_mem_pathR
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) }
Tactic:
apply Fin.eq_of_val_eq
Proof state after:
case a
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑(Fin.castSucc j) = ↑{ val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) }
Theorem: Board.pivot_not_mem_pathR
Proof state before:
case a
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑(Fin.castSucc j) = ↑{ val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) }
Tactic:
dsimp
Proof state after:
case a
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j = n - ↑k - 1
Theorem: Board.pivot_not_mem_pathR
Proof state before:
case a
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j = n - ↑k - 1
Tactic:
apply Nat.le_antisymm ?_ h
Proof state after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j ≤ n - ↑k - 1
Theorem: Board.pivot_not_mem_pathR
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j ≤ n - ↑k - 1
Tactic:
rewrite [← Nat.sub_add_eq]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j ≤ n - (↑k + 1)
Theorem: Board.pivot_not_mem_pathR
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j ≤ n - (↑k + 1)
Tactic:
apply Nat.le_sub_of_add_le
Proof state after:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j + (↑k + 1) ≤ n
Theorem: Board.pivot_not_mem_pathR
Proof state before:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j + (↑k + 1) ≤ n
Tactic:
show j.1 + k.1 < n
Proof state after:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j + ↑k < n
Theorem: Board.pivot_not_mem_pathR
Proof state before:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j + ↑k < n
Tactic:
rewrite [Nat.add_comm j.1 k.1]
Proof state after:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑k + ↑j < n
Theorem: Board.pivot_not_mem_pathR
Proof state before:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑k + ↑j < n
Tactic:
exact Nat.add_lt_of_lt_sub k.2
Proof state after:
no goals
Theorem: Board.lt_last_of_mem_pathT
Proof state before:
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
conv at ha => dsimp [Board.pathT]; rw [List.mem_ofFn]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : ∃ i_1, Fin.rlexProd { val := m - ↑i_1 - 1, isLt := (_ : m - ↑i_1 - 1 < m + 1) } (Fin.castSucc j) = a
⊢ ↑a < (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_pathT
Proof state before:
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : ∃ i_1, Fin.rlexProd { val := m - ↑i_1 - 1, isLt := (_ : m - ↑i_1 - 1 < m + 1) } (Fin.castSucc j) = a
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
have ⟨⟨k,hk⟩,ha⟩ := ha
Proof state after:
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha✝ : ∃ i_1, Fin.rlexProd { val := m - ↑i_1 - 1, isLt := (_ : m - ↑i_1 - 1 < m + 1) } (Fin.castSucc j) = a
k : Nat
hk : k < m - ↑i - 1
ha :
  Fin.rlexProd { val := m - ↑{ val := k, isLt := hk } - 1, isLt := (_ : m - ↑{ val := k, isLt := hk } - 1 < m + 1) }
      (Fin.castSucc j) =
    a
⊢ ↑a < (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_pathT
Proof state before:
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha✝ : ∃ i_1, Fin.rlexProd { val := m - ↑i_1 - 1, isLt := (_ : m - ↑i_1 - 1 < m + 1) } (Fin.castSucc j) = a
k : Nat
hk : k < m - ↑i - 1
ha :
  Fin.rlexProd { val := m - ↑{ val := k, isLt := hk } - 1, isLt := (_ : m - ↑{ val := k, isLt := hk } - 1 < m + 1) }
      (Fin.castSucc j) =
    a
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
cases ha
Proof state after:
case refl
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)
⊢ ↑(Fin.rlexProd { val := m - ↑{ val := k, isLt := hk } - 1, isLt := (_ : m - ↑{ val := k, isLt := hk } - 1 < m + 1) }
        (Fin.castSucc j)) <
    (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_pathT
Proof state before:
case refl
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)
⊢ ↑(Fin.rlexProd { val := m - ↑{ val := k, isLt := hk } - 1, isLt := (_ : m - ↑{ val := k, isLt := hk } - 1 < m + 1) }
        (Fin.castSucc j)) <
    (m + 1) * (n + 1) - 1
Tactic:
simp
Proof state after:
case refl
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 + 1) * ↑j < (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_pathT
Proof state before:
case refl
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 + 1) * ↑j < (m + 1) * (n + 1) - 1
Tactic:
conv => rhs; change (m+1)*n + m; rw [Nat.add_comm _ m]
Proof state after:
case refl
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 + 1) * ↑j < m + (m + 1) * n
Theorem: Board.lt_last_of_mem_pathT
Proof state before:
case refl
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 + 1) * ↑j < m + (m + 1) * n
Tactic:
apply Nat.add_lt_add
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

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
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

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:
. rewrite [← Nat.sub_add_eq]
  exact m.sub_lt i.pos k.zero_lt_succ
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 + 1) * ↑j < (m + 1) * n
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