case zero
i j : Fin Nat.zero
⊢ ↑(succAbove (succ i)) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)

case succ
n✝ : ℕ
i j : Fin (Nat.succ n✝)
⊢ ↑(succAbove (succ i)) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
n : ℕ
i j : Fin n
⊢ ↑(succAbove (succ i)) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
cases n
case succ.inl
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
⊢ ↑(succAbove (succ i)) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)

case succ.inr.inl
n✝ : ℕ
i j : Fin (Nat.succ n✝)
heq : j = i
⊢ ↑(succAbove (succ i)) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)

case succ.inr.inr
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hgt : i < j
⊢ ↑(succAbove (succ i)) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
case succ
n✝ : ℕ
i j : Fin (Nat.succ n✝)
⊢ ↑(succAbove (succ i)) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
rcases lt_trichotomy j i with (hlt | heq | hgt)
no goals
case zero
i j : Fin Nat.zero
⊢ ↑(succAbove (succ i)) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
rcases j with ⟨_, ⟨⟩⟩
case succ.inl
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : ↑castSucc (j + 1) = succ j
⊢ ↑(succAbove (succ i)) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
case succ.inl
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
⊢ ↑(succAbove (succ i)) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
have : castSucc (j + 1) = j.succ := by
  ext
  rw [coe_castSucc, val_succ, Fin.val_add_one_of_lt (lt_of_lt_of_le hlt i.le_last)]
case succ.inl.a
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : ↑castSucc (j + 1) = succ j
⊢ succ j ≠ 0

case succ.inl.a
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : ↑castSucc (j + 1) = succ j
⊢ succ j ≠ succ i

case succ.inl.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : ↑castSucc (j + 1) = succ j
⊢ ↑castSucc (j + 1) < succ i
case succ.inl
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : ↑castSucc (j + 1) = succ j
⊢ ↑(succAbove (succ i)) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
rw [Fin.cycleRange_of_lt hlt, Fin.succAbove_below, this, swap_apply_of_ne_of_ne]
case h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
⊢ ↑(↑castSucc (j + 1)) = ↑(succ j)
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
⊢ ↑castSucc (j + 1) = succ j
ext
no goals
case h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
⊢ ↑(↑castSucc (j + 1)) = ↑(succ j)
rw [coe_castSucc, val_succ, Fin.val_add_one_of_lt (lt_of_lt_of_le hlt i.le_last)]
no goals
case succ.inl.a
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : ↑castSucc (j + 1) = succ j
⊢ succ j ≠ 0
apply Fin.succ_ne_zero
no goals
case succ.inl.a
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : ↑castSucc (j + 1) = succ j
⊢ succ j ≠ succ i
exact (Fin.succ_injective _).ne hlt.ne
case succ.inl.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : ↑castSucc (j + 1) = succ j
⊢ ↑(↑castSucc (j + 1)) < ↑(succ i)
case succ.inl.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : ↑castSucc (j + 1) = succ j
⊢ ↑castSucc (j + 1) < succ i
rw [Fin.lt_iff_val_lt_val]
no goals
case succ.inl.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : ↑castSucc (j + 1) = succ j
⊢ ↑(↑castSucc (j + 1)) < ↑(succ i)
simpa [this] using hlt
case succ.inr.inl.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
heq : j = i
⊢ ↑castSucc 0 < succ i
case succ.inr.inl
n✝ : ℕ
i j : Fin (Nat.succ n✝)
heq : j = i
⊢ ↑(succAbove (succ i)) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
rw [heq, Fin.cycleRange_self, Fin.succAbove_below, swap_apply_right, Fin.castSucc_zero]
case succ.inr.inl.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
heq : j = i
⊢ 0 < succ i
case succ.inr.inl.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
heq : j = i
⊢ ↑castSucc 0 < succ i
rw [Fin.castSucc_zero]
no goals
case succ.inr.inl.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
heq : j = i
⊢ 0 < succ i
apply Fin.succ_pos
case succ.inr.inr.a
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hgt : i < j
⊢ succ j ≠ 0

case succ.inr.inr.a
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hgt : i < j
⊢ succ j ≠ succ i

case succ.inr.inr.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hgt : i < j
⊢ succ i ≤ ↑castSucc j
case succ.inr.inr
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hgt : i < j
⊢ ↑(succAbove (succ i)) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
rw [Fin.cycleRange_of_gt hgt, Fin.succAbove_above, swap_apply_of_ne_of_ne]
no goals
case succ.inr.inr.a
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hgt : i < j
⊢ succ j ≠ 0
apply Fin.succ_ne_zero
no goals
case succ.inr.inr.a
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hgt : i < j
⊢ succ j ≠ succ i
apply (Fin.succ_injective _).ne hgt.ne.symm
no goals
case succ.inr.inr.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hgt : i < j
⊢ succ i ≤ ↑castSucc j
simpa [Fin.le_iff_val_le_val] using hgt