case H.h
n : ℕ
j : Fin (Nat.succ n)
⊢ ↑(↑(cycleRange 0) j) = ↑(↑1 j)
n : ℕ
⊢ cycleRange 0 = 1
ext j
case H.h.refine'_1
n : ℕ
j : Fin (Nat.succ n)
⊢ ↑(↑(cycleRange 0) 0) = ↑(↑1 0)

case H.h.refine'_2
n : ℕ
j✝ : Fin (Nat.succ n)
j : Fin n
⊢ ↑(↑(cycleRange 0) (succ j)) = ↑(↑1 (succ j))
case H.h
n : ℕ
j : Fin (Nat.succ n)
⊢ ↑(↑(cycleRange 0) j) = ↑(↑1 j)
refine' Fin.cases _ (fun j => _) j
no goals
case H.h.refine'_1
n : ℕ
j : Fin (Nat.succ n)
⊢ ↑(↑(cycleRange 0) 0) = ↑(↑1 0)
simp
no goals
case H.h.refine'_2
n : ℕ
j✝ : Fin (Nat.succ n)
j : Fin n
⊢ ↑(↑(cycleRange 0) (succ j)) = ↑(↑1 (succ j))
rw [cycleRange_of_gt (Fin.succ_pos j), one_apply]