case intro
α : Type u
l l' : List α
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r List.map f (rotate l₁ n)
α : Type u
l l' : List α
β : Type u_1
l₁ l₂ : List α
h : l₁ ~r l₂
f : α → β
⊢ List.map f l₁ ~r List.map f l₂
obtain ⟨n, rfl⟩ := h
case intro
α : Type u
l l' : List α
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r rotate (List.map f l₁) n
case intro
α : Type u
l l' : List α
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r List.map f (rotate l₁ n)
rw [map_rotate]
no goals
case intro
α : Type u
l l' : List α
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r rotate (List.map f l₁) n
use n