-- Mathlib/GroupTheory/Perm/Fin.lean
theorem cycleRange_of_le {n : ℕ} [NeZero n] {i j : Fin n} (h : j ≤ i) :
    cycleRange i j = if j = i then 0 else j + 1

Proof state:
case succ.h
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i j : Fin (n✝ + 1)
h : j ≤ i
this : j = castLE ⋯ ⟨↑j, ⋯⟩
⊢ ↑(i.cycleRange j) = ↑(if j = i then 0 else j + 1)

Tactic:
erw [this, cycleRange, ofLeftInverse'_eq_ofInjective, ←
  Function.Embedding.toEquivRange_eq_ofInjective, ← viaFintypeEmbedding,
  viaFintypeEmbedding_apply_image, Function.Embedding.coeFn_mk,
  coe_castLE, coe_finRotate]

Result:
case succ.h
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i j : Fin (n✝ + 1)
h : j ≤ i
this : j = castLE ⋯ ⟨↑j, ⋯⟩
⊢ (if ⟨↑j, ⋯⟩ = last ↑i then 0 else ↑⟨↑j, ⋯⟩ + 1) = ↑(if castLE ⋯ ⟨↑j, ⋯⟩ = i then 0 else castLE ⋯ ⟨↑j, ⋯⟩ + 1)

Proof state:
n : ℕ
inst✝ : NeZero n
i j : Fin n
h : j ≤ i
⊢ i.cycleRange j = if j = i then 0 else j + 1

Tactic:
cases n

Result:
case zero
inst✝ : NeZero 0
i j : Fin 0
h : j ≤ i
⊢ i.cycleRange j = if j = i then 0 else j + 1

case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i j : Fin (n✝ + 1)
h : j ≤ i
⊢ i.cycleRange j = if j = i then 0 else j + 1

Proof state:
case pos
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i j : Fin (n✝ + 1)
h : j ≤ i
this : j = castLE ⋯ ⟨↑j, ⋯⟩
heq : ↑j = ↑i
⊢ 0 = ↑0

Tactic:
rfl

Result:
no goals

Proof state:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i j : Fin (n✝ + 1)
h : j ≤ i
⊢ i.cycleRange j = if j = i then 0 else j + 1

Tactic:
have : j = (Fin.castLE (Nat.succ_le_of_lt i.is_lt))
  ⟨j, lt_of_le_of_lt h (Nat.lt_succ_self i)⟩ := by simp

Result:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i j : Fin (n✝ + 1)
h : j ≤ i
this : j = castLE ⋯ ⟨↑j, ⋯⟩
⊢ i.cycleRange j = if j = i then 0 else j + 1

Proof state:
case succ.h
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i j : Fin (n✝ + 1)
h : j ≤ i
this : j = castLE ⋯ ⟨↑j, ⋯⟩
⊢ (if ⟨↑j, ⋯⟩ = last ↑i then 0 else ↑⟨↑j, ⋯⟩ + 1) = ↑(if castLE ⋯ ⟨↑j, ⋯⟩ = i then 0 else castLE ⋯ ⟨↑j, ⋯⟩ + 1)

Tactic:
simp only [Fin.ext_iff, val_last, val_mk, val_zero, Fin.eta, castLE_mk]

Result:
case succ.h
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i j : Fin (n✝ + 1)
h : j ≤ i
this : j = castLE ⋯ ⟨↑j, ⋯⟩
⊢ (if ↑j = ↑i then 0 else ↑j + 1) = ↑(if ↑j = ↑i then 0 else j + 1)

Proof state:
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i j : Fin (n✝ + 1)
h : j ≤ i
⊢ j = castLE ⋯ ⟨↑j, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
case neg
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i j : Fin (n✝ + 1)
h : j ≤ i
this : j = castLE ⋯ ⟨↑j, ⋯⟩
heq : ¬↑j = ↑i
⊢ j < last n✝

Tactic:
exact lt_of_lt_of_le (lt_of_le_of_ne h (mt (congr_arg _) heq)) (le_last i)

Result:
no goals

Proof state:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i j : Fin (n✝ + 1)
h : j ≤ i
this : j = castLE ⋯ ⟨↑j, ⋯⟩
⊢ i.cycleRange j = if j = i then 0 else j + 1

Tactic:
ext

Result:
case succ.h
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i j : Fin (n✝ + 1)
h : j ≤ i
this : j = castLE ⋯ ⟨↑j, ⋯⟩
⊢ ↑(i.cycleRange j) = ↑(if j = i then 0 else j + 1)

Proof state:
case succ.h
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i j : Fin (n✝ + 1)
h : j ≤ i
this : j = castLE ⋯ ⟨↑j, ⋯⟩
⊢ (if ↑j = ↑i then 0 else ↑j + 1) = ↑(if ↑j = ↑i then 0 else j + 1)

Tactic:
split_ifs with heq

Result:
case pos
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i j : Fin (n✝ + 1)
h : j ≤ i
this : j = castLE ⋯ ⟨↑j, ⋯⟩
heq : ↑j = ↑i
⊢ 0 = ↑0

case neg
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i j : Fin (n✝ + 1)
h : j ≤ i
this : j = castLE ⋯ ⟨↑j, ⋯⟩
heq : ¬↑j = ↑i
⊢ ↑j + 1 = ↑(j + 1)

Proof state:
case zero
inst✝ : NeZero 0
i j : Fin 0
h : j ≤ i
⊢ i.cycleRange j = if j = i then 0 else j + 1

Tactic:
subsingleton

Result:
no goals

Proof state:
case neg
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i j : Fin (n✝ + 1)
h : j ≤ i
this : j = castLE ⋯ ⟨↑j, ⋯⟩
heq : ¬↑j = ↑i
⊢ ↑j + 1 = ↑(j + 1)

Tactic:
rw [Fin.val_add_one_of_lt]

Result:
case neg
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i j : Fin (n✝ + 1)
h : j ≤ i
this : j = castLE ⋯ ⟨↑j, ⋯⟩
heq : ¬↑j = ↑i
⊢ j < last n✝