-- 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 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)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
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

Tactic:
constructor

Result:
case mp
α : Type u_1
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

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

Proof state:
α : Type u_1
⊢ ([] = [] ∧ [] = []) ∧ [] = [].flatten ∧ [] = [].flatten

Tactic:
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 ∧ 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

Tactic:
simp only [h]

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

Proof state:
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

Tactic:
exact .inr ⟨x :: as, bs, c, cs, ds, by simp⟩

Result:
no goals