α : Type u_1
β : Type ?u.47240
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ tails (reverse l) = reverse (map reverse (reverse (map reverse (tails (reverse l)))))
α : Type u_1
β : Type ?u.47240
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ tails (reverse l) = reverse (map reverse (inits l))
rw [inits_eq_tails l]
no goals
α : Type u_1
β : Type ?u.47240
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ tails (reverse l) = reverse (map reverse (reverse (map reverse (tails (reverse l)))))
simp [reverse_involutive.comp_self, reverse_map]