-- 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
α : 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:
simp only [flatten_cons] at h

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 : x ++ xs.flatten = y :: ys
⊢ ∃ as bs cs, x :: xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.flatten

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 : y :: ys = x ++ xs.flatten
⊢ ∃ as bs cs, x :: xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.flatten

Tactic:
rw [cons_eq_append_iff] at h

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 : x = [] ∧ xs.flatten = y :: ys ∨ ∃ 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

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 ∨ ∃ 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 (⟨rfl, h⟩ | ⟨z⟩) := h

Result:
case mp.cons.inl.intro
α : Type u_1
y : α
ys : 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 : xs.flatten = y :: ys
⊢ ∃ as bs cs, [] :: xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.flatten

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

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

Tactic:
refine ⟨[] :: as, bs, cs, ?_⟩

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

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

Tactic:
rintro ⟨as, bs, cs, rfl, h₁, rfl⟩

Result:
case mpr.intro.intro.intro.intro.intro
α : Type u_1
y : α
as : List (List α)
bs : List α
cs : List (List α)
h₁ : ∀ (l : List α), l ∈ as → l = []
⊢ (as ++ (y :: bs) :: cs).flatten = y :: (bs ++ cs.flatten)

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
⊢ (x :: xs).flatten = y :: ys →
    ∃ as bs cs, x :: xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.flatten

Tactic:
intro h

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 : (x :: xs).flatten = y :: ys
⊢ ∃ as bs cs, x :: xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), 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
⊢ ∃ as bs cs,
    (y :: a') :: xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ a' ++ xs.flatten = bs ++ cs.flatten

Tactic:
refine ⟨[], a', xs, ?_⟩

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
⊢ (y :: a') :: xs = [] ++ (y :: a') :: xs ∧ (∀ (l : List α), l ∈ [] → l = []) ∧ a' ++ xs.flatten = a' ++ xs.flatten

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

Tactic:
simp

Result:
no goals

Proof state:
case mp.cons.inl.intro
α : Type u_1
y : α
ys : 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 : xs.flatten = y :: ys
⊢ ∃ as bs cs, [] :: xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.flatten

Tactic:
obtain ⟨as, bs, cs, rfl, _, rfl⟩ := ih h

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

Proof state:
case mpr.intro.intro.intro.intro.intro
α : Type u_1
y : α
as : List (List α)
bs : List α
cs : List (List α)
h₁ : ∀ (l : List α), l ∈ as → l = []
⊢ (as ++ (y :: bs) :: cs).flatten = y :: (bs ++ cs.flatten)

Tactic:
simp [flatten_eq_nil_iff.mpr h₁]

Result:
no goals