case H.h
n : ℕ
i : Fin (Nat.succ n)
⊢ ↑(↑(finRotate (Nat.succ n)) i) = ↑(↑(↑decomposeFin.symm (1, finRotate n)) i)
n : ℕ
⊢ finRotate (Nat.succ n) = ↑decomposeFin.symm (1, finRotate n)
ext i
case H.h.zero
i : Fin (Nat.succ Nat.zero)
⊢ ↑(↑(finRotate (Nat.succ Nat.zero)) i) = ↑(↑(↑decomposeFin.symm (1, finRotate Nat.zero)) i)

case H.h.succ
n✝ : ℕ
i : Fin (Nat.succ (Nat.succ n✝))
⊢ ↑(↑(finRotate (Nat.succ (Nat.succ n✝))) i) = ↑(↑(↑decomposeFin.symm (1, finRotate (Nat.succ n✝))) i)
case H.h
n : ℕ
i : Fin (Nat.succ n)
⊢ ↑(↑(finRotate (Nat.succ n)) i) = ↑(↑(↑decomposeFin.symm (1, finRotate n)) i)
cases n
case H.h.succ.refine'_1
n✝ : ℕ
i : Fin (Nat.succ (Nat.succ n✝))
⊢ ↑(↑(finRotate (Nat.succ (Nat.succ n✝))) 0) = ↑(↑(↑decomposeFin.symm (1, finRotate (Nat.succ n✝))) 0)

case H.h.succ.refine'_2
n✝ : ℕ
i✝ : Fin (Nat.succ (Nat.succ n✝))
i : Fin (n✝ + 1)
⊢ ↑(↑(finRotate (Nat.succ (Nat.succ n✝))) (Fin.succ i)) =
    ↑(↑(↑decomposeFin.symm (1, finRotate (Nat.succ n✝))) (Fin.succ i))
case H.h.succ
n✝ : ℕ
i : Fin (Nat.succ (Nat.succ n✝))
⊢ ↑(↑(finRotate (Nat.succ (Nat.succ n✝))) i) = ↑(↑(↑decomposeFin.symm (1, finRotate (Nat.succ n✝))) i)
refine' Fin.cases _ (fun i => _) i
case H.h.succ.refine'_2
n✝ : ℕ
i✝ : Fin (Nat.succ (Nat.succ n✝))
i : Fin (n✝ + 1)
⊢ (if i = Fin.last n✝ then 0 else ↑(Fin.succ i) + 1) = ↑(↑(swap 0 1) (Fin.succ (↑(finRotate (Nat.succ n✝)) i)))
case H.h.succ.refine'_2
n✝ : ℕ
i✝ : Fin (Nat.succ (Nat.succ n✝))
i : Fin (n✝ + 1)
⊢ ↑(↑(finRotate (Nat.succ (Nat.succ n✝))) (Fin.succ i)) =
    ↑(↑(↑decomposeFin.symm (1, finRotate (Nat.succ n✝))) (Fin.succ i))
rw [coe_finRotate, decomposeFin_symm_apply_succ, if_congr i.succ_eq_last_succ rfl rfl]
case H.h.succ.refine'_2.inl
n✝ : ℕ
i✝ : Fin (Nat.succ (Nat.succ n✝))
i : Fin (n✝ + 1)
h : i = Fin.last n✝
⊢ 0 = ↑(↑(swap 0 1) (Fin.succ (↑(finRotate (Nat.succ n✝)) i)))

case H.h.succ.refine'_2.inr
n✝ : ℕ
i✝ : Fin (Nat.succ (Nat.succ n✝))
i : Fin (n✝ + 1)
h : ¬i = Fin.last n✝
⊢ ↑(Fin.succ i) + 1 = ↑(↑(swap 0 1) (Fin.succ (↑(finRotate (Nat.succ n✝)) i)))
case H.h.succ.refine'_2
n✝ : ℕ
i✝ : Fin (Nat.succ (Nat.succ n✝))
i : Fin (n✝ + 1)
⊢ (if i = Fin.last n✝ then 0 else ↑(Fin.succ i) + 1) = ↑(↑(swap 0 1) (Fin.succ (↑(finRotate (Nat.succ n✝)) i)))
split_ifs with h
no goals
case H.h.zero
i : Fin (Nat.succ Nat.zero)
⊢ ↑(↑(finRotate (Nat.succ Nat.zero)) i) = ↑(↑(↑decomposeFin.symm (1, finRotate Nat.zero)) i)
simp
no goals
case H.h.succ.refine'_1
n✝ : ℕ
i : Fin (Nat.succ (Nat.succ n✝))
⊢ ↑(↑(finRotate (Nat.succ (Nat.succ n✝))) 0) = ↑(↑(↑decomposeFin.symm (1, finRotate (Nat.succ n✝))) 0)
simp
no goals
case H.h.succ.refine'_2.inl
n✝ : ℕ
i✝ : Fin (Nat.succ (Nat.succ n✝))
i : Fin (n✝ + 1)
h : i = Fin.last n✝
⊢ 0 = ↑(↑(swap 0 1) (Fin.succ (↑(finRotate (Nat.succ n✝)) i)))
simp [h]
no goals
case H.h.succ.refine'_2.inr
n✝ : ℕ
i✝ : Fin (Nat.succ (Nat.succ n✝))
i : Fin (n✝ + 1)
h : ¬i = Fin.last n✝
⊢ ↑(Fin.succ i) + 1 = ↑(↑(swap 0 1) (Fin.succ (↑(finRotate (Nat.succ n✝)) i)))
rw [Fin.val_succ, Function.Injective.map_swap Fin.val_injective, Fin.val_succ, coe_finRotate,
  if_neg h, Fin.val_zero, Fin.val_one,
  swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]