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

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

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