-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatten_eq_append_iff {xs : List (List α)} {ys zs : List α} :
    xs.flatten = ys ++ zs ↔
      (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
        ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧
          zs = c :: cs ++ ds.flatten

Proof state:
case mp.cons.inr.intro.intro.nil
α : Type u_1
zs : List α
xs : List (List α)
ih :
  ∀ {ys : List α},
    xs.flatten = ys ++ zs →
      (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
        ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ zs = c :: cs ++ ds.flatten
ys : List α
h : zs = [] ++ xs.flatten
⊢ (∃ as bs, (ys ++ []) :: xs = as ++ bs ∧ ys = as.flatten ∧ [] ++ xs.flatten = bs.flatten) ∨
    ∃ as bs c cs ds,
      (ys ++ []) :: xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ [] ++ xs.flatten = c :: cs ++ ds.flatten

Tactic:
exact .inl ⟨[ys], xs, by simp⟩

Result:
no goals

Proof state:
case mp.cons.inl.intro.intro.inl.intro.intro.intro.intro
α : Type u_1
x : List α
as bs : List (List α)
ih :
  ∀ {ys : List α},
    (as ++ bs).flatten = ys ++ bs.flatten →
      (∃ as_1 bs_1, as ++ bs = as_1 ++ bs_1 ∧ ys = as_1.flatten ∧ bs.flatten = bs_1.flatten) ∨
        ∃ as_1 bs_1 c cs ds,
          as ++ bs = as_1 ++ (bs_1 ++ c :: cs) :: ds ∧ ys = as_1.flatten ++ bs_1 ∧ bs.flatten = c :: cs ++ ds.flatten
h : (as ++ bs).flatten = as.flatten ++ bs.flatten
⊢ (∃ as_1 bs_1, x :: (as ++ bs) = as_1 ++ bs_1 ∧ x ++ as.flatten = as_1.flatten ∧ bs.flatten = bs_1.flatten) ∨
    ∃ as_1 bs_1 c cs ds,
      x :: (as ++ bs) = as_1 ++ (bs_1 ++ c :: cs) :: ds ∧
        x ++ as.flatten = as_1.flatten ++ bs_1 ∧ bs.flatten = c :: cs ++ ds.flatten

Tactic:
exact .inl ⟨x :: as, bs, by simp⟩

Result:
no goals

Proof state:
case mp.cons.inr.intro.intro
α : Type u_1
zs : List α
xs : List (List α)
ih :
  ∀ {ys : List α},
    xs.flatten = ys ++ zs →
      (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
        ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ zs = c :: cs ++ ds.flatten
ys c' : List α
h : zs = c' ++ xs.flatten
⊢ (∃ as bs, (ys ++ c') :: xs = as ++ bs ∧ ys = as.flatten ∧ c' ++ xs.flatten = bs.flatten) ∨
    ∃ as bs c cs ds,
      (ys ++ c') :: xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ c' ++ xs.flatten = c :: cs ++ ds.flatten

Tactic:
cases c' with
| nil => exact .inl ⟨[ys], xs, by simp⟩
| cons x c' => exact .inr ⟨[], ys, x, c', xs, by simp⟩

Result:
no goals

Proof state:
case mp.nil
α : Type u_1
⊢ ∃ as bs, (as = [] ∧ bs = []) ∧ [] = as.flatten ∧ [] = bs.flatten

Tactic:
exact ⟨[], [], by simp⟩

Result:
no goals

Proof state:
α : Type u_1
x : List α
as bs : List (List α)
ih :
  ∀ {ys : List α},
    (as ++ bs).flatten = ys ++ bs.flatten →
      (∃ as_1 bs_1, as ++ bs = as_1 ++ bs_1 ∧ ys = as_1.flatten ∧ bs.flatten = bs_1.flatten) ∨
        ∃ as_1 bs_1 c cs ds,
          as ++ bs = as_1 ++ (bs_1 ++ c :: cs) :: ds ∧ ys = as_1.flatten ++ bs_1 ∧ bs.flatten = c :: cs ++ ds.flatten
h : (as ++ bs).flatten = as.flatten ++ bs.flatten
⊢ x :: (as ++ bs) = x :: as ++ bs ∧ x ++ as.flatten = (x :: as).flatten ∧ bs.flatten = bs.flatten

Tactic:
simp

Result:
no goals

Proof state:
case mp.cons
α : Type u_1
zs x : List α
xs : List (List α)
ih :
  ∀ {ys : List α},
    xs.flatten = ys ++ zs →
      (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
        ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ zs = c :: cs ++ ds.flatten
ys : List α
h : (∃ a', ys = x ++ a' ∧ xs.flatten = a' ++ zs) ∨ ∃ c', x = ys ++ c' ∧ zs = c' ++ xs.flatten
⊢ (∃ as bs, x :: xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
    ∃ as bs c cs ds, x :: xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ zs = c :: cs ++ ds.flatten

Tactic:
obtain (⟨ys, rfl, h⟩ | ⟨c', rfl, h⟩) := h

Result:
case mp.cons.inl.intro.intro
α : Type u_1
zs x : List α
xs : List (List α)
ih :
  ∀ {ys : List α},
    xs.flatten = ys ++ zs →
      (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
        ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ zs = c :: cs ++ ds.flatten
ys : List α
h : xs.flatten = ys ++ zs
⊢ (∃ as bs, x :: xs = as ++ bs ∧ x ++ ys = as.flatten ∧ zs = bs.flatten) ∨
    ∃ as bs c cs ds, x :: xs = as ++ (bs ++ c :: cs) :: ds ∧ x ++ ys = as.flatten ++ bs ∧ zs = c :: cs ++ ds.flatten

case mp.cons.inr.intro.intro
α : Type u_1
zs : List α
xs : List (List α)
ih :
  ∀ {ys : List α},
    xs.flatten = ys ++ zs →
      (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
        ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ zs = c :: cs ++ ds.flatten
ys c' : List α
h : zs = c' ++ xs.flatten
⊢ (∃ as bs, (ys ++ c') :: xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
    ∃ as bs c cs ds, (ys ++ c') :: xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ zs = c :: cs ++ ds.flatten

Proof state:
case mp.cons.inl.intro.intro
α : Type u_1
zs x : List α
xs : List (List α)
ih :
  ∀ {ys : List α},
    xs.flatten = ys ++ zs →
      (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
        ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ zs = c :: cs ++ ds.flatten
ys : List α
h : xs.flatten = ys ++ zs
⊢ (∃ as bs, x :: xs = as ++ bs ∧ x ++ ys = as.flatten ∧ zs = bs.flatten) ∨
    ∃ as bs c cs ds, x :: xs = as ++ (bs ++ c :: cs) :: ds ∧ x ++ ys = as.flatten ++ bs ∧ zs = c :: cs ++ ds.flatten

Tactic:
obtain (⟨as, bs, rfl, rfl, rfl⟩ | ⟨as, bs, c, cs, ds, rfl, rfl, rfl⟩) := ih h

Result:
case mp.cons.inl.intro.intro.inl.intro.intro.intro.intro
α : Type u_1
x : List α
as bs : List (List α)
ih :
  ∀ {ys : List α},
    (as ++ bs).flatten = ys ++ bs.flatten →
      (∃ as_1 bs_1, as ++ bs = as_1 ++ bs_1 ∧ ys = as_1.flatten ∧ bs.flatten = bs_1.flatten) ∨
        ∃ as_1 bs_1 c cs ds,
          as ++ bs = as_1 ++ (bs_1 ++ c :: cs) :: ds ∧ ys = as_1.flatten ++ bs_1 ∧ bs.flatten = c :: cs ++ ds.flatten
h : (as ++ bs).flatten = as.flatten ++ bs.flatten
⊢ (∃ as_1 bs_1, x :: (as ++ bs) = as_1 ++ bs_1 ∧ x ++ as.flatten = as_1.flatten ∧ bs.flatten = bs_1.flatten) ∨
    ∃ as_1 bs_1 c cs ds,
      x :: (as ++ bs) = as_1 ++ (bs_1 ++ c :: cs) :: ds ∧
        x ++ as.flatten = as_1.flatten ++ bs_1 ∧ bs.flatten = c :: cs ++ ds.flatten

case mp.cons.inl.intro.intro.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
x : List α
as : List (List α)
bs : List α
c : α
cs : List α
ds : List (List α)
ih :
  ∀ {ys : List α},
    (as ++ (bs ++ c :: cs) :: ds).flatten = ys ++ (c :: cs ++ ds.flatten) →
      (∃ as_1 bs_1,
          as ++ (bs ++ c :: cs) :: ds = as_1 ++ bs_1 ∧ ys = as_1.flatten ∧ c :: cs ++ ds.flatten = bs_1.flatten) ∨
        ∃ as_1 bs_1 c_1 cs_1 ds_1,
          as ++ (bs ++ c :: cs) :: ds = as_1 ++ (bs_1 ++ c_1 :: cs_1) :: ds_1 ∧
            ys = as_1.flatten ++ bs_1 ∧ c :: cs ++ ds.flatten = c_1 :: cs_1 ++ ds_1.flatten
h : (as ++ (bs ++ c :: cs) :: ds).flatten = as.flatten ++ bs ++ (c :: cs ++ ds.flatten)
⊢ (∃ as_1 bs_1,
      x :: (as ++ (bs ++ c :: cs) :: ds) = as_1 ++ bs_1 ∧
        x ++ (as.flatten ++ bs) = as_1.flatten ∧ c :: cs ++ ds.flatten = bs_1.flatten) ∨
    ∃ as_1 bs_1 c_1 cs_1 ds_1,
      x :: (as ++ (bs ++ c :: cs) :: ds) = as_1 ++ (bs_1 ++ c_1 :: cs_1) :: ds_1 ∧
        x ++ (as.flatten ++ bs) = as_1.flatten ++ bs_1 ∧ c :: cs ++ ds.flatten = c_1 :: cs_1 ++ ds_1.flatten