case intro
α : Type u
l : List α
n : ℕ
⊢ List.reverse l ~r List.reverse (rotate l n)
α : Type u
l l' : List α
h : l ~r l'
⊢ List.reverse l ~r List.reverse l'
obtain ⟨n, rfl⟩ := h
no goals
case intro
α : Type u
l : List α
n : ℕ
⊢ List.reverse l ~r List.reverse (rotate l n)
exact ⟨_, (reverse_rotate _ _).symm⟩