case cons
α✝ : Type u_1
b : List α✝
x : α✝
c : List α✝
a : α✝
as : List α✝
⊢ a = x ∧ as ++ b = c ↔ ∃ a', (a = x ∧ as = a') ∧ c = a' ++ b
α✝ : Type u_1
a b : List α✝
x : α✝
c : List α✝
⊢ a ++ b = x :: c ↔ a = [] ∧ b = x :: c ∨ ∃ a', a = x :: a' ∧ c = a' ++ b
cases a with simp | cons a as => ?_
no goals
case cons
α✝ : Type u_1
b : List α✝
x : α✝
c : List α✝
a : α✝
as : List α✝
⊢ a = x ∧ as ++ b = c ↔ ∃ a', (a = x ∧ as = a') ∧ c = a' ++ b
exact ⟨fun h => ⟨as, by simp [h]⟩, fun ⟨a', ⟨aeq, aseq⟩, h⟩ => ⟨aeq, by rw [aseq, h]⟩⟩
no goals
α✝ : Type u_1
b : List α✝
x : α✝
c : List α✝
a : α✝
as : List α✝
h : a = x ∧ as ++ b = c
⊢ (a = x ∧ as = as) ∧ c = as ++ b
simp [h]
no goals
α✝ : Type u_1
b : List α✝
x : α✝
c : List α✝
a : α✝
as : List α✝
x✝ : ∃ a', (a = x ∧ as = a') ∧ c = a' ++ b
a' : List α✝
aeq : a = x
aseq : as = a'
h : c = a' ++ b
⊢ as ++ b = c
rw [aseq, h]