[GOAL]
α : Type u_1
β : Type u_2
l✝ l : List α
p : Palindrome l
⊢ reverse l = l
[PROOFSTEP]
induction p
[GOAL]
case nil
α : Type u_1
β : Type u_2
l✝ l : List α
⊢ reverse [] = []
[PROOFSTEP]
try (exact rfl)
[GOAL]
case nil
α : Type u_1
β : Type u_2
l✝ l : List α
⊢ reverse [] = []
[PROOFSTEP]
exact rfl
[GOAL]
case singleton
α : Type u_1
β : Type u_2
l✝ l : List α
x✝ : α
⊢ reverse [x✝] = [x✝]
[PROOFSTEP]
try (exact rfl)
[GOAL]
case singleton
α : Type u_1
β : Type u_2
l✝ l : List α
x✝ : α
⊢ reverse [x✝] = [x✝]
[PROOFSTEP]
exact rfl
[GOAL]
case cons_concat
α : Type u_1
β : Type u_2
l✝¹ l : List α
x✝ : α
l✝ : List α
a✝ : Palindrome l✝
a_ih✝ : reverse l✝ = l✝
⊢ reverse (x✝ :: (l✝ ++ [x✝])) = x✝ :: (l✝ ++ [x✝])
[PROOFSTEP]
try (exact rfl)
[GOAL]
case cons_concat
α : Type u_1
β : Type u_2
l✝¹ l : List α
x✝ : α
l✝ : List α
a✝ : Palindrome l✝
a_ih✝ : reverse l✝ = l✝
⊢ reverse (x✝ :: (l✝ ++ [x✝])) = x✝ :: (l✝ ++ [x✝])
[PROOFSTEP]
exact rfl
[GOAL]
case cons_concat
α : Type u_1
β : Type u_2
l✝¹ l : List α
x✝ : α
l✝ : List α
a✝ : Palindrome l✝
a_ih✝ : reverse l✝ = l✝
⊢ reverse (x✝ :: (l✝ ++ [x✝])) = x✝ :: (l✝ ++ [x✝])
[PROOFSTEP]
simp
[GOAL]
case cons_concat
α : Type u_1
β : Type u_2
l✝¹ l : List α
x✝ : α
l✝ : List α
a✝ : Palindrome l✝
a_ih✝ : reverse l✝ = l✝
⊢ reverse l✝ = l✝
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
l✝ l : List α
⊢ reverse l = l → Palindrome l
[PROOFSTEP]
refine' bidirectionalRecOn l (fun _ => Palindrome.nil) (fun a _ => Palindrome.singleton a) _
[GOAL]
α : Type u_1
β : Type u_2
l✝ l : List α
⊢ ∀ (a : α) (l : List α) (b : α),
    (reverse l = l → Palindrome l) → reverse (a :: (l ++ [b])) = a :: (l ++ [b]) → Palindrome (a :: (l ++ [b]))
[PROOFSTEP]
intro x l y hp hr
[GOAL]
α : Type u_1
β : Type u_2
l✝¹ l✝ : List α
x : α
l : List α
y : α
hp : reverse l = l → Palindrome l
hr : reverse (x :: (l ++ [y])) = x :: (l ++ [y])
⊢ Palindrome (x :: (l ++ [y]))
[PROOFSTEP]
rw [reverse_cons, reverse_append] at hr 
[GOAL]
α : Type u_1
β : Type u_2
l✝¹ l✝ : List α
x : α
l : List α
y : α
hp : reverse l = l → Palindrome l
hr : reverse [y] ++ reverse l ++ [x] = x :: (l ++ [y])
⊢ Palindrome (x :: (l ++ [y]))
[PROOFSTEP]
rw [head_eq_of_cons_eq hr]
[GOAL]
α : Type u_1
β : Type u_2
l✝¹ l✝ : List α
x : α
l : List α
y : α
hp : reverse l = l → Palindrome l
hr : reverse [y] ++ reverse l ++ [x] = x :: (l ++ [y])
⊢ Palindrome (x :: (l ++ [x]))
[PROOFSTEP]
have : Palindrome l := hp (append_inj_left' (tail_eq_of_cons_eq hr) rfl)
[GOAL]
α : Type u_1
β : Type u_2
l✝¹ l✝ : List α
x : α
l : List α
y : α
hp : reverse l = l → Palindrome l
hr : reverse [y] ++ reverse l ++ [x] = x :: (l ++ [y])
this : Palindrome l
⊢ Palindrome (x :: (l ++ [x]))
[PROOFSTEP]
exact Palindrome.cons_concat x this
[GOAL]
α : Type u_1
β : Type u_2
l✝ l : List α
⊢ Palindrome (l ++ reverse l)
[PROOFSTEP]
apply of_reverse_eq
[GOAL]
case a
α : Type u_1
β : Type u_2
l✝ l : List α
⊢ reverse (l ++ reverse l) = l ++ reverse l
[PROOFSTEP]
rw [reverse_append, reverse_reverse]
[GOAL]
α : Type u_1
β : Type u_2
l : List α
f : α → β
p : Palindrome l
⊢ reverse (map f l) = map f l
[PROOFSTEP]
rw [← map_reverse, p.reverse_eq]
