no goals
α : Type u_1
x : α
x✝ : List α
⊢ x ∈ reverseAux [] x✝ ↔ x ∈ [] ∨ x ∈ x✝
simp
α : Type u_1
x a : α
tail✝ x✝ : List α
⊢ x ∈ tail✝ ∨ x = a ∨ x ∈ x✝ ↔ (x = a ∨ x ∈ tail✝) ∨ x ∈ x✝
α : Type u_1
x a : α
tail✝ x✝ : List α
⊢ x ∈ reverseAux (a :: tail✝) x✝ ↔ x ∈ a :: tail✝ ∨ x ∈ x✝
simp [mem_reverseAux]
no goals
α : Type u_1
x a : α
tail✝ x✝ : List α
⊢ x ∈ tail✝ ∨ x = a ∨ x ∈ x✝ ↔ (x = a ∨ x ∈ tail✝) ∨ x ∈ x✝
rw [← or_assoc, @or_comm (x = a)]