no goals
α : Type u_1
a b c d : List α
⊢ a ++ b = c ++ d ↔ (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b
induction a generalizing c with
| nil => simp; exact (or_iff_left_of_imp fun ⟨_, ⟨e, rfl⟩, h⟩ => e ▸ h.symm).symm
| cons a as ih => cases c <;> simp [eq_comm, and_assoc, ih, and_or_left]
case nil
α : Type u_1
b d c : List α
⊢ b = c ++ d ↔ b = c ++ d ∨ ∃ c', (c = [] ∧ c' = []) ∧ d = c' ++ b
case nil
α : Type u_1
b d c : List α
⊢ [] ++ b = c ++ d ↔ (∃ a', c = [] ++ a' ∧ b = a' ++ d) ∨ ∃ c', [] = c ++ c' ∧ d = c' ++ b
simp
no goals
case nil
α : Type u_1
b d c : List α
⊢ b = c ++ d ↔ b = c ++ d ∨ ∃ c', (c = [] ∧ c' = []) ∧ d = c' ++ b
exact (or_iff_left_of_imp fun ⟨_, ⟨e, rfl⟩, h⟩ => e ▸ h.symm).symm
no goals
case cons
α : Type u_1
b d : List α
a : α
as : List α
ih : ∀ {c : List α}, as ++ b = c ++ d ↔ (∃ a', c = as ++ a' ∧ b = a' ++ d) ∨ ∃ c', as = c ++ c' ∧ d = c' ++ b
c : List α
⊢ a :: as ++ b = c ++ d ↔ (∃ a', c = a :: as ++ a' ∧ b = a' ++ d) ∨ ∃ c', a :: as = c ++ c' ∧ d = c' ++ b
cases c <;> simp [eq_comm, and_assoc, ih, and_or_left]