-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatten_eq_cons_iff {xs : List (List α)} {y : α} {ys : List α} :
    xs.flatten = y :: ys ↔
      ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ l, l ∈ as → l = []) ∧ ys = bs ++ cs.flatten

Proof state:
case mp.cons.inr.intro.intro
α : Type u_1
y : α
xs : List (List α)
a' : List α
ih :
  xs.flatten = y :: (a' ++ xs.flatten) →
    ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ a' ++ xs.flatten = bs ++ cs.flatten
⊢ (y :: a') :: xs = [] ++ (y :: a') :: xs ∧ (∀ (l : List α), l ∈ [] → l = []) ∧ a' ++ xs.flatten = a' ++ xs.flatten

Tactic:
simp

Result:
no goals

Proof state:
case mp.cons.inr
α : Type u_1
y : α
ys x : List α
xs : List (List α)
ih :
  xs.flatten = y :: ys →
    ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.flatten
z : ∃ a', x = y :: a' ∧ ys = a' ++ xs.flatten
⊢ ∃ as bs cs, x :: xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.flatten

Tactic:
obtain ⟨a', rfl, rfl⟩ := z

Result:
case mp.cons.inr.intro.intro
α : Type u_1
y : α
xs : List (List α)
a' : List α
ih :
  xs.flatten = y :: (a' ++ xs.flatten) →
    ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ a' ++ xs.flatten = bs ++ cs.flatten
⊢ ∃ as bs cs,
    (y :: a') :: xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ a' ++ xs.flatten = bs ++ cs.flatten

Proof state:
case mp.cons.inl.intro.intro.intro.intro.intro.intro
α : Type u_1
y : α
as : List (List α)
bs : List α
cs : List (List α)
left✝ : ∀ (l : List α), l ∈ as → l = []
ih :
  (as ++ (y :: bs) :: cs).flatten = y :: (bs ++ cs.flatten) →
    ∃ as_1 bs_1 cs_1,
      as ++ (y :: bs) :: cs = as_1 ++ (y :: bs_1) :: cs_1 ∧
        (∀ (l : List α), l ∈ as_1 → l = []) ∧ bs ++ cs.flatten = bs_1 ++ cs_1.flatten
h : (as ++ (y :: bs) :: cs).flatten = y :: (bs ++ cs.flatten)
⊢ [] :: (as ++ (y :: bs) :: cs) = [] :: as ++ (y :: bs) :: cs ∧
    (∀ (l : List α), l ∈ [] :: as → l = []) ∧ bs ++ cs.flatten = bs ++ cs.flatten

Tactic:
simpa

Result:
no goals

Proof state:
case mp.cons
α : Type u_1
y : α
ys x : List α
xs : List (List α)
ih :
  xs.flatten = y :: ys →
    ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.flatten
h : x ++ xs.flatten = y :: ys
⊢ ∃ as bs cs, x :: xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.flatten

Tactic:
replace h := h.symm

Result:
case mp.cons
α : Type u_1
y : α
ys x : List α
xs : List (List α)
ih :
  xs.flatten = y :: ys →
    ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.flatten
h : y :: ys = x ++ xs.flatten
⊢ ∃ as bs cs, x :: xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.flatten

Proof state:
α : Type u_1
xs : List (List α)
y : α
ys : List α
⊢ xs.flatten = y :: ys ↔
    ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.flatten

Tactic:
constructor

Result:
case mp
α : Type u_1
xs : List (List α)
y : α
ys : List α
⊢ xs.flatten = y :: ys →
    ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.flatten

case mpr
α : Type u_1
xs : List (List α)
y : α
ys : List α
⊢ (∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.flatten) →
    xs.flatten = y :: ys