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

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

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

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

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

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

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

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

Tactic:
constructor

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

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

Proof state:
α : Type u_1
y : α
as cs : List (List α)
h₁ : ∀ (l : List α), l ∈ as → l = []
h₂ : ∀ (l : List α), l ∈ cs → l = []
⊢ as ++ [y] :: cs = as ++ [y] :: cs

Tactic:
simp

Result:
no goals

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

Tactic:
simpa

Result:
no goals

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

Tactic:
simp at h₂

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_1
y : α
as : List (List α)
bs : List α
cs : List (List α)
h₁ : ∀ (l : List α), l ∈ as → l = []
h₂ : bs = [] ∧ ∀ (l : List α), l ∈ cs → l = []
⊢ ∃ as_1 bs_1,
    as ++ (y :: bs) :: cs = as_1 ++ [y] :: bs_1 ∧
      (∀ (l : List α), l ∈ as_1 → l = []) ∧ ∀ (l : List α), l ∈ bs_1 → l = []

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

Tactic:
exact ⟨as, [], bs, rfl, h₁, by simpa⟩

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_1
y : α
as : List (List α)
bs : List α
cs : List (List α)
h₁ : ∀ (l : List α), l ∈ as → l = []
h₂ : bs = [] ∧ ∀ (l : List α), l ∈ cs → l = []
⊢ ∃ as_1 bs_1,
    as ++ (y :: bs) :: cs = as_1 ++ [y] :: bs_1 ∧
      (∀ (l : List α), l ∈ as_1 → l = []) ∧ ∀ (l : List α), l ∈ bs_1 → l = []

Tactic:
obtain ⟨rfl, h₂⟩ := h₂

Result:
case mp.intro.intro.intro.intro.intro.intro
α : Type u_1
y : α
as cs : List (List α)
h₁ : ∀ (l : List α), l ∈ as → l = []
h₂ : ∀ (l : List α), l ∈ cs → l = []
⊢ ∃ as_1 bs, as ++ [y] :: cs = as_1 ++ [y] :: bs ∧ (∀ (l : List α), l ∈ as_1 → l = []) ∧ ∀ (l : List α), l ∈ bs → l = []

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

Tactic:
exact ⟨as, cs, by simp, h₁, h₂⟩

Result:
no goals

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

Tactic:
rw [flatten_eq_cons_iff]

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