internlm/Lean-Github huggingface dataset:
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h.succ.refl.h
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
          (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) a)) =
      fold' (m + n + 1) f a
⊢ f { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) }
      (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < succ (m + n)) }) init) =
    f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
      (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) init)
Tactic:
apply congrFun
Proof state after:
case h.h.h.h.succ.refl.h.h
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
          (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) a)) =
      fold' (m + n + 1) f a
⊢ f { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) } =
    f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h.succ.refl.h.h
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
          (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) a)) =
      fold' (m + n + 1) f a
⊢ f { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) } =
    f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
Tactic:
apply congrArg
Proof state after:
case h.h.h.h.succ.refl.h.h.h
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
          (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) a)) =
      fold' (m + n + 1) f a
⊢ { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) } =
    { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h.succ.refl.h.h.h
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
          (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) a)) =
      fold' (m + n + 1) f a
⊢ { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) } =
    { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
Tactic:
apply Fin.eq_of_val_eq
Proof state after:
case h.h.h.h.succ.refl.h.h.h.a
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
          (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) a)) =
      fold' (m + n + 1) f a
⊢ { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) }.val =
    { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }.val
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h.succ.refl.h.h.h.a
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
          (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) a)) =
      fold' (m + n + 1) f a
⊢ { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) }.val =
    { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }.val
Tactic:
simp only [Nat.succ_sub_succ_eq_sub, Nat.add_sub_cancel_left]
Proof state after:
case h.h.h.h.succ.refl.h.h.h.a
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
          (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) a)) =
      fold' (m + n + 1) f a
⊢ n = (Fin.last n).val
Theorem: Nat.fold'_eq_fold'TR
Proof state before:
case h.h.h.h.succ.refl.h.h.h.a
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
          (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) a)) =
      fold' (m + n + 1) f a
⊢ n = (Fin.last n).val
Tactic:
rfl
Proof state after:
no goals
Theorem: decide_or
Proof state before:
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
⊢ decide (p ∨ q) = (decide p || decide q)
Tactic:
apply dite p <;> apply dite q <;> intro hp hq <;> simp [hp, hq]
Proof state after:
no goals
Theorem: decide_and
Proof state before:
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
⊢ decide (p ∧ q) = (decide p && decide q)
Tactic:
apply dite p <;> apply dite q <;> intro hp hq <;> simp [hp, hq]
Proof state after:
no goals
Theorem: Bool.bne_comm
Proof state before:
a b : Bool
⊢ (a != b) = (b != a)
Tactic:
cases a <;> cases b <;> decide
Proof state after:
no goals
Theorem: Bool.bne_assoc
Proof state before:
a b c : Bool
⊢ ((a != b) != c) = (a != (b != c))
Tactic:
cases a <;> cases b <;> cases c <;> decide
Proof state after:
no goals
Theorem: Bool.bne_self
Proof state before:
a : Bool
⊢ (a != a) = false
Tactic:
cases a <;> decide
Proof state after:
no goals
Theorem: Bool.bne_false
Proof state before:
a : Bool
⊢ (a != false) = a
Tactic:
cases a <;> decide
Proof state after:
no goals
Theorem: Bool.false_bne
Proof state before:
a : Bool
⊢ (false != a) = a
Tactic:
cases a <;> decide
Proof state after:
no goals
Theorem: Bool.bne_true
Proof state before:
a : Bool
⊢ (a != true) = !a
Tactic:
cases a <;> decide
Proof state after:
no goals
Theorem: Bool.true_bne
Proof state before:
a : Bool
⊢ (true != a) = !a
Tactic:
cases a <;> decide
Proof state after:
no goals
Theorem: Bool.bne_eq_false
Proof state before:
a b : Bool
⊢ (a != b) = false ↔ a = b
Tactic:
cases a <;> cases b <;> decide
Proof state after:
no goals
Theorem: Board.pivot_lt_last
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1
Tactic:
conv =>
  rhs; change (m+1)*n + m; rw [Nat.add_comm _ m]
  change (Fin.rlexProd (Fin.last m) (Fin.last n)).1
Proof state after:
m n : Nat
i : Fin m
j : Fin n
⊢ ↑(Board.pivot i j) < ↑(Fin.rlexProd (Fin.last m) (Fin.last n))
Theorem: Board.pivot_lt_last
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ↑(Board.pivot i j) < ↑(Fin.rlexProd (Fin.last m) (Fin.last n))
Tactic:
exact Fin.rlexProd_lt_of_snd _ _ j.2
Proof state after:
no goals
Theorem: Board.lt_last_of_mem_pathL
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 < (m + 1) * (n + 1) - 1
Tactic:
conv at ha => dsimp [Board.pathL]; 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 (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      a
⊢ ↑a < (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_pathL
Proof state before:
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      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 (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      a
k : Nat
hk : k < n - ↑j
ha :
  Fin.rlexProd (Fin.castSucc i)
      (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk }))) =
    a
⊢ ↑a < (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_pathL
Proof state before:
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha✝ :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      a
k : Nat
hk : k < n - ↑j
ha :
  Fin.rlexProd (Fin.castSucc i)
      (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk }))) =
    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 < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ ↑(Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))) <
    (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_pathL
Proof state before:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ ↑(Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))) <
    (m + 1) * (n + 1) - 1
Tactic:
dsimp
Proof state after:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ ↑i + (m + 1) * (↑j + k + 1) < (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_pathL
Proof state before:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ ↑i + (m + 1) * (↑j + k + 1) < (m + 1) * (n + 1) - 1
Tactic:
conv =>
  change (i.1 + (m+1)*(j.1+k+1)).succ ≤ (m+1)*n+m
  rw [← Nat.succ_add i.1, Nat.add_comm _ m]
Proof state after:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ Nat.succ ↑i + (m + 1) * (↑j + k + 1) ≤ m + (m + 1) * n
Theorem: Board.lt_last_of_mem_pathL
Proof state before:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ Nat.succ ↑i + (m + 1) * (↑j + k + 1) ≤ m + (m + 1) * n
Tactic:
refine Nat.add_le_add i.2 ?_
Proof state after:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ (m + 1) * (↑j + k + 1) ≤ (m + 1) * n
Theorem: Board.lt_last_of_mem_pathL
Proof state before:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ (m + 1) * (↑j + k + 1) ≤ (m + 1) * n
Tactic:
refine Nat.mul_le_mul_left (m+1) ?_
Proof state after:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ ↑j + k + 1 ≤ n
Theorem: Board.lt_last_of_mem_pathL
Proof state before:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ ↑j + k + 1 ≤ n
Tactic:
rewrite [Nat.add_comm j.1 k]
Proof state after:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ k + ↑j + 1 ≤ n
Theorem: Board.lt_last_of_mem_pathL
Proof state before:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ k + ↑j + 1 ≤ n
Tactic:
exact Nat.add_lt_of_lt_sub hk
Proof state after:
no goals
Theorem: Board.pivot_not_mem_pathL
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathL i j
Tactic:
dsimp [Board.pathL]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈
      List.ofFn fun k =>
        Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k)))
Theorem: Board.pivot_not_mem_pathL
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈
      List.ofFn fun k =>
        Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k)))
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.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) x))) =
        Board.pivot i j
Theorem: Board.pivot_not_mem_pathL
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ∀ (x : Fin (n - ↑j)),
    ¬Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) x))) =
        Board.pivot i j
Tactic:
intro k
Proof state after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ¬Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k))) =
      Board.pivot i j
Theorem: Board.pivot_not_mem_pathL
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ¬Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k))) =
      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 (n - ↑j)
⊢ ↑(Board.pivot i j) <
    ↑(Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k))))
Theorem: Board.pivot_not_mem_pathL
Proof state before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ↑(Board.pivot i j) <
    ↑(Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k))))
Tactic:
apply Fin.rlexProd_lt_of_snd
Proof state after:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ Fin.castSucc j < Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k))
Theorem: Board.pivot_not_mem_pathL
Proof state before:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ Fin.castSucc j < Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k))
Tactic:
show j.1 < j.1 + k + 1
Proof state after:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ↑j < ↑j + ↑k + 1
Theorem: Board.pivot_not_mem_pathL
Proof state before:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ↑j < ↑j + ↑k + 1
Tactic:
rewrite [Nat.add_assoc]
Proof state after:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ↑j < ↑j + (↑k + 1)
Theorem: Board.pivot_not_mem_pathL
Proof state before:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ↑j < ↑j + (↑k + 1)
Tactic:
exact j.1.lt_add_of_pos_right k.1.zero_lt_succ
Proof state after:
no goals
Theorem: Board.lt_last_of_mem_pathB
Proof state before:
m n : Nat
i : Fin m
a : Fin ((m + 1) * (n + 1))
ha : a ∈ Board.pathB n i
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
conv at ha => dsimp [Board.pathB]; rw [List.mem_ofFn]
Proof state after:
m n : Nat
i : Fin m
a : Fin ((m + 1) * (n + 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) = a
⊢ ↑a < (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_pathB
Proof state before:
m n : Nat
i : Fin m
a : Fin ((m + 1) * (n + 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) = a
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
have ⟨⟨k,hk⟩,ha⟩ := ha
Proof state after:
m n : Nat
i : Fin m
a : Fin ((m + 1) * (n + 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) = a
k : Nat
hk : k < m - ↑i - 1
ha :
  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) =
    a
⊢ ↑a < (m + 1) * (n + 1) - 1
Theorem: Board.lt_last_of_mem_pathB
Proof state before:
m n : Nat
i : Fin m
a : Fin ((m + 1) * (n + 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) = a
k : Nat
hk : k < m - ↑i - 1
ha :
  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) =
    a
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
cases ha
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)
⊢ ↑(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)) <
    (m + 1) * (n + 1) - 1
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)
⊢ ↑(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)) <
    (m + 1) * (n + 1) - 1
Tactic:
simp
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 + 1) * n < (m + 1) * (n + 1) - 1
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 + 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
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