case refine'_1
n m : ℕ
p : Fin (n + 1)
i : Fin n
⊢ ↑(succAbove p) i < p → ↑castSucc i < p

case refine'_2
n m : ℕ
p : Fin (n + 1)
i : Fin n
⊢ ↑castSucc i < p → ↑(succAbove p) i < p
n m : ℕ
p : Fin (n + 1)
i : Fin n
⊢ ↑(succAbove p) i < p ↔ ↑castSucc i < p
refine' Iff.intro _ _
case refine'_1
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : ↑(succAbove p) i < p
⊢ ↑castSucc i < p
case refine'_1
n m : ℕ
p : Fin (n + 1)
i : Fin n
⊢ ↑(succAbove p) i < p → ↑castSucc i < p
intro h
case refine'_1.inl
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : ↑(succAbove p) i < p
H : ↑castSucc i < p
⊢ ↑castSucc i < p

case refine'_1.inr
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : ↑(succAbove p) i < p
H : p ≤ ↑castSucc i
⊢ ↑castSucc i < p
case refine'_1
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : ↑(succAbove p) i < p
⊢ ↑castSucc i < p
cases' succAbove_lt_ge p i with H H
no goals
case refine'_1.inl
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : ↑(succAbove p) i < p
H : ↑castSucc i < p
⊢ ↑castSucc i < p
exact H
case refine'_1.inr
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : succ i < p
H : p ≤ ↑castSucc i
⊢ ↑castSucc i < p
case refine'_1.inr
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : ↑(succAbove p) i < p
H : p ≤ ↑castSucc i
⊢ ↑castSucc i < p
rw [succAbove_above _ _ H] at h
no goals
case refine'_1.inr
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : succ i < p
H : p ≤ ↑castSucc i
⊢ ↑castSucc i < p
exact lt_trans (castSucc_lt_succ i) h
case refine'_2
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : ↑castSucc i < p
⊢ ↑(succAbove p) i < p
case refine'_2
n m : ℕ
p : Fin (n + 1)
i : Fin n
⊢ ↑castSucc i < p → ↑(succAbove p) i < p
intro h
case refine'_2
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : ↑castSucc i < p
⊢ ↑castSucc i < p
case refine'_2
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : ↑castSucc i < p
⊢ ↑(succAbove p) i < p
rw [succAbove_below _ _ h]
no goals
case refine'_2
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : ↑castSucc i < p
⊢ ↑castSucc i < p
exact h