n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
⊢ ↑(if j = i then 0 else j + 1) = if j = i then 0 else ↑j + 1
n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
⊢ ↑(↑(cycleRange i) j) = if j = i then 0 else ↑j + 1
rw [cycleRange_of_le h]
case inl
n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
h' : j = i
⊢ ↑0 = 0

case inr
n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
h' : ¬j = i
⊢ ↑(j + 1) = ↑j + 1
n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
⊢ ↑(if j = i then 0 else j + 1) = if j = i then 0 else ↑j + 1
split_ifs with h'
no goals
case inr
n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
h' : ¬j = i
⊢ ↑(j + 1) = ↑j + 1
exact
  val_add_one_of_lt
    (calc
      (j : ℕ) < i := Fin.lt_iff_val_lt_val.mp (lt_of_le_of_ne h h')
      _ ≤ n := Nat.lt_succ_iff.mp i.2)
no goals
case inl
n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
h' : j = i
⊢ ↑0 = 0
rfl