-- 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
α : 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 α
⊢ (x :: xs).flatten = ys ++ zs →
    (∃ 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:
intro h

Result:
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 : (x :: xs).flatten = ys ++ zs
⊢ (∃ 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

Proof state:
α : 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)
⊢ x :: (as ++ (bs ++ c :: cs) :: ds) = x :: as ++ (bs ++ c :: cs) :: ds ∧
    x ++ (as.flatten ++ bs) = (x :: as).flatten ++ bs ∧ c :: cs ++ ds.flatten = c :: cs ++ ds.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 : (x :: xs).flatten = ys ++ zs
⊢ (∃ 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:
simp only [flatten_cons] at h

Result:
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 : x ++ xs.flatten = ys ++ zs
⊢ (∃ 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

Proof state:
α : 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
⊢ (ys ++ []) :: xs = [ys] ++ xs ∧ ys = [ys].flatten ∧ [] ++ xs.flatten = xs.flatten

Tactic:
simp

Result:
no goals

Proof state:
case mp.nil
α : Type u_1
zs ys : List α
⊢ [].flatten = ys ++ zs →
    (∃ as bs, [] = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
      ∃ as bs c cs ds, [] = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ zs = c :: cs ++ ds.flatten

Tactic:
simp only [flatten_nil, nil_eq, append_eq_nil_iff, and_false, cons_append, false_and,
  exists_const, exists_false, or_false, and_imp, List.cons_ne_nil]

Result:
case mp.nil
α : Type u_1
zs ys : List α
⊢ ys = [] → zs = [] → ∃ as bs, (as = [] ∧ bs = []) ∧ ys = as.flatten ∧ zs = bs.flatten

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 : x ++ xs.flatten = ys ++ zs
⊢ (∃ 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:
rw [append_eq_append_iff] at h

Result:
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

Proof state:
α : 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 α
x : α
c' : List α
h : zs = x :: c' ++ xs.flatten
⊢ (ys ++ x :: c') :: xs = [] ++ (ys ++ x :: c') :: xs ∧
    ys = [].flatten ++ ys ∧ x :: c' ++ xs.flatten = x :: c' ++ xs.flatten

Tactic:
simp

Result:
no goals

Proof state:
case mpr
α : Type u_1
xs : List (List α)
ys zs : List α
⊢ ((∃ 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) →
    xs.flatten = ys ++ zs

Tactic:
rintro (⟨as, bs, rfl, rfl, rfl⟩ | ⟨as, bs, c, cs, ds, rfl, rfl, rfl⟩)

Result:
case mpr.inl.intro.intro.intro.intro
α : Type u_1
as bs : List (List α)
⊢ (as ++ bs).flatten = as.flatten ++ bs.flatten

case mpr.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
as : List (List α)
bs : List α
c : α
cs : List α
ds : List (List α)
⊢ (as ++ (bs ++ c :: cs) :: ds).flatten = as.flatten ++ bs ++ (c :: cs ++ ds.flatten)

Proof state:
case mpr.inl.intro.intro.intro.intro
α : Type u_1
as bs : List (List α)
⊢ (as ++ bs).flatten = as.flatten ++ bs.flatten

Tactic:
simp

Result:
no goals

Proof state:
case mp.cons.inr.intro.intro.cons
α : 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 α
x : α
c' : List α
h : zs = x :: c' ++ xs.flatten
⊢ (∃ as bs, (ys ++ x :: c') :: xs = as ++ bs ∧ ys = as.flatten ∧ x :: c' ++ xs.flatten = bs.flatten) ∨
    ∃ as bs c cs ds,
      (ys ++ x :: c') :: xs = as ++ (bs ++ c :: cs) :: ds ∧
        ys = as.flatten ++ bs ∧ x :: c' ++ xs.flatten = c :: cs ++ ds.flatten

Tactic:
exact .inr ⟨[], ys, x, c', xs, by simp⟩

Result:
no goals

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

Tactic:
rintro rfl rfl

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