case cons_concat
α : Type u_1
β : Type ?u.273
l✝¹ l : List α
x✝ : α
l✝ : List α
a✝ : Palindrome l✝
a_ih✝ : reverse l✝ = l✝
⊢ reverse (x✝ :: (l✝ ++ [x✝])) = x✝ :: (l✝ ++ [x✝])
α : Type u_1
β : Type ?u.273
l✝ l : List α
p : Palindrome l
⊢ reverse l = l
induction p <;> try (exact rfl)
case cons_concat
α : Type u_1
β : Type ?u.273
l✝¹ l : List α
x✝ : α
l✝ : List α
a✝ : Palindrome l✝
a_ih✝ : reverse l✝ = l✝
⊢ reverse l✝ = l✝
case cons_concat
α : Type u_1
β : Type ?u.273
l✝¹ l : List α
x✝ : α
l✝ : List α
a✝ : Palindrome l✝
a_ih✝ : reverse l✝ = l✝
⊢ reverse (x✝ :: (l✝ ++ [x✝])) = x✝ :: (l✝ ++ [x✝])
simp
no goals
case cons_concat
α : Type u_1
β : Type ?u.273
l✝¹ l : List α
x✝ : α
l✝ : List α
a✝ : Palindrome l✝
a_ih✝ : reverse l✝ = l✝
⊢ reverse l✝ = l✝
assumption
case cons_concat
α : Type u_1
β : Type ?u.273
l✝¹ l : List α
x✝ : α
l✝ : List α
a✝ : Palindrome l✝
a_ih✝ : reverse l✝ = l✝
⊢ reverse (x✝ :: (l✝ ++ [x✝])) = x✝ :: (l✝ ++ [x✝])
case cons_concat
α : Type u_1
β : Type ?u.273
l✝¹ l : List α
x✝ : α
l✝ : List α
a✝ : Palindrome l✝
a_ih✝ : reverse l✝ = l✝
⊢ reverse (x✝ :: (l✝ ++ [x✝])) = x✝ :: (l✝ ++ [x✝])
(exact rfl)
case cons_concat
α : Type u_1
β : Type ?u.273
l✝¹ l : List α
x✝ : α
l✝ : List α
a✝ : Palindrome l✝
a_ih✝ : reverse l✝ = l✝
⊢ reverse (x✝ :: (l✝ ++ [x✝])) = x✝ :: (l✝ ++ [x✝])
case cons_concat
α : Type u_1
β : Type ?u.273
l✝¹ l : List α
x✝ : α
l✝ : List α
a✝ : Palindrome l✝
a_ih✝ : reverse l✝ = l✝
⊢ reverse (x✝ :: (l✝ ++ [x✝])) = x✝ :: (l✝ ++ [x✝])
exact rfl