n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : ↑castSucc j < i
h' : ↑castSucc (succ j) < succ i
⊢ ↑(succAbove (succ i)) (succ j) = succ (↑(succAbove i) j)
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : ↑castSucc j < i
⊢ ↑(succAbove (succ i)) (succ j) = succ (↑(succAbove i) j)
have h' : castSucc j.succ < i.succ := by simpa [lt_iff_val_lt_val] using h
case h
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : ↑castSucc j < i
h' : ↑castSucc (succ j) < succ i
⊢ ↑(↑(succAbove (succ i)) (succ j)) = ↑(succ (↑(succAbove i) j))
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : ↑castSucc j < i
h' : ↑castSucc (succ j) < succ i
⊢ ↑(succAbove (succ i)) (succ j) = succ (↑(succAbove i) j)
ext
no goals
case h
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : ↑castSucc j < i
h' : ↑castSucc (succ j) < succ i
⊢ ↑(↑(succAbove (succ i)) (succ j)) = ↑(succ (↑(succAbove i) j))
simp [succAbove_below _ _ h, succAbove_below _ _ h']
no goals
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : ↑castSucc j < i
⊢ ↑castSucc (succ j) < succ i
simpa [lt_iff_val_lt_val] using h
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : ↑castSucc j ≥ i
h' : succ i ≤ ↑castSucc (succ j)
⊢ ↑(succAbove (succ i)) (succ j) = succ (↑(succAbove i) j)
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : ↑castSucc j ≥ i
⊢ ↑(succAbove (succ i)) (succ j) = succ (↑(succAbove i) j)
have h' : i.succ ≤ castSucc j.succ := by simpa [le_iff_val_le_val] using h
case h
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : ↑castSucc j ≥ i
h' : succ i ≤ ↑castSucc (succ j)
⊢ ↑(↑(succAbove (succ i)) (succ j)) = ↑(succ (↑(succAbove i) j))
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : ↑castSucc j ≥ i
h' : succ i ≤ ↑castSucc (succ j)
⊢ ↑(succAbove (succ i)) (succ j) = succ (↑(succAbove i) j)
ext
no goals
case h
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : ↑castSucc j ≥ i
h' : succ i ≤ ↑castSucc (succ j)
⊢ ↑(↑(succAbove (succ i)) (succ j)) = ↑(succ (↑(succAbove i) j))
simp [succAbove_above _ _ h, succAbove_above _ _ h']
no goals
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : ↑castSucc j ≥ i
⊢ succ i ≤ ↑castSucc (succ j)
simpa [le_iff_val_le_val] using h