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

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

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

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

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

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

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

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

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
State after:
no goals

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

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
State after:
no goals

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
State after:
no goals