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

Proof state:
case of.mk
α : Type u_1
y : α
xs : List (List α)
ys : List α
⊢ (List.map List.toArray xs).toArray.flatten = { toList := ys }.push y ↔
    ∃ as bs cs,
      (List.map List.toArray xs).toArray = as.push (bs.push y) ++ cs ∧
        (∀ (l : Array α), l ∈ cs → l = #[]) ∧ { toList := ys } = as.flatten ++ bs

Tactic:
rw [flatten_toArray_map, List.push_toArray, mk.injEq, List.flatten_eq_append_iff]

Result:
case of.mk
α : Type u_1
y : α
xs : List (List α)
ys : List α
⊢ ((∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ [y] = bs.flatten) ∨
      ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ [y] = c :: cs ++ ds.flatten) ↔
    ∃ as bs cs,
      (List.map List.toArray xs).toArray = as.push (bs.push y) ++ cs ∧
        (∀ (l : Array α), l ∈ cs → l = #[]) ∧ { toList := ys } = as.flatten ++ bs

Proof state:
case of.mk
α : Type u_1
y : α
xs : List (List α)
ys : List α
⊢ ((∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ [y] = bs.flatten) ∨
      ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ [y] = c :: cs ++ ds.flatten) ↔
    ∃ as bs cs,
      (List.map List.toArray xs).toArray = as.push (bs.push y) ++ cs ∧
        (∀ (l : Array α), l ∈ cs → l = #[]) ∧ { toList := ys } = as.flatten ++ bs

Tactic:
constructor

Result:
case of.mk.mp
α : Type u_1
y : α
xs : List (List α)
ys : List α
⊢ ((∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ [y] = bs.flatten) ∨
      ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ [y] = c :: cs ++ ds.flatten) →
    ∃ as bs cs,
      (List.map List.toArray xs).toArray = as.push (bs.push y) ++ cs ∧
        (∀ (l : Array α), l ∈ cs → l = #[]) ∧ { toList := ys } = as.flatten ++ bs

case of.mk.mpr
α : Type u_1
y : α
xs : List (List α)
ys : List α
⊢ (∃ as bs cs,
      (List.map List.toArray xs).toArray = as.push (bs.push y) ++ cs ∧
        (∀ (l : Array α), l ∈ cs → l = #[]) ∧ { toList := ys } = as.flatten ++ bs) →
    (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ [y] = bs.flatten) ∨
      ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ [y] = c :: cs ++ ds.flatten

Proof state:
case of.mk.mpr.intro.intro.intro.intro.intro
α : Type u_1
y : α
ys : List α
as : Array (Array α)
bs : Array α
cs : Array (Array α)
h₂ : ∀ (l : Array α), l ∈ cs → l = #[]
h₃ : ys = (List.map toList as.toList).flatten ++ bs.toList
⊢ (∃ as_1 bs_1,
      List.map toList as.toList ++ (bs.toList ++ [y]) :: List.map toList cs.toList = as_1 ++ bs_1 ∧
        ys = as_1.flatten ∧ [y] = bs_1.flatten) ∨
    ∃ as_1 bs_1 c cs_1 ds,
      List.map toList as.toList ++ (bs.toList ++ [y]) :: List.map toList cs.toList = as_1 ++ (bs_1 ++ c :: cs_1) :: ds ∧
        ys = as_1.flatten ++ bs_1 ∧ [y] = c :: cs_1 ++ ds.flatten

Tactic:
subst h₃

Result:
case of.mk.mpr.intro.intro.intro.intro.intro
α : Type u_1
y : α
as : Array (Array α)
bs : Array α
cs : Array (Array α)
h₂ : ∀ (l : Array α), l ∈ cs → l = #[]
⊢ (∃ as_1 bs_1,
      List.map toList as.toList ++ (bs.toList ++ [y]) :: List.map toList cs.toList = as_1 ++ bs_1 ∧
        (List.map toList as.toList).flatten ++ bs.toList = as_1.flatten ∧ [y] = bs_1.flatten) ∨
    ∃ as_1 bs_1 c cs_1 ds,
      List.map toList as.toList ++ (bs.toList ++ [y]) :: List.map toList cs.toList = as_1 ++ (bs_1 ++ c :: cs_1) :: ds ∧
        (List.map toList as.toList).flatten ++ bs.toList = as_1.flatten ++ bs_1 ∧ [y] = c :: cs_1 ++ ds.flatten

Proof state:
α : Type u_1
y : α
as xs ys : List (List α)
h₁ : ∀ (l : List α), l ∈ xs → l = []
h₂ : ∀ (l : List α), l ∈ ys → l = []
⊢ { toList := as.flatten } = (List.map List.toArray (as ++ xs)).toArray.flatten ++ #[]

Tactic:
rw [flatten_toArray_map]

Result:
α : Type u_1
y : α
as xs ys : List (List α)
h₁ : ∀ (l : List α), l ∈ xs → l = []
h₂ : ∀ (l : List α), l ∈ ys → l = []
⊢ { toList := as.flatten } = (as ++ xs).flatten.toArray ++ #[]

Proof state:
case of.mk.mp.inl.intro.intro.intro.intro
α : Type u_1
y : α
as bs : List (List α)
h : [y] = bs.flatten
⊢ ∃ as_1 bs_1 cs,
    (List.map List.toArray (as ++ bs)).toArray = as_1.push (bs_1.push y) ++ cs ∧
      (∀ (l : Array α), l ∈ cs → l = #[]) ∧ { toList := as.flatten } = as_1.flatten ++ bs_1

Tactic:
rw [List.singleton_eq_flatten_iff] at h

Result:
case of.mk.mp.inl.intro.intro.intro.intro
α : Type u_1
y : α
as bs : List (List α)
h : ∃ as bs_1, bs = as ++ [y] :: bs_1 ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ∀ (l : List α), l ∈ bs_1 → l = []
⊢ ∃ as_1 bs_1 cs,
    (List.map List.toArray (as ++ bs)).toArray = as_1.push (bs_1.push y) ++ cs ∧
      (∀ (l : Array α), l ∈ cs → l = #[]) ∧ { toList := as.flatten } = as_1.flatten ++ bs_1

Proof state:
case of.mk.mpr.intro.intro.intro.intro.intro
α : Type u_1
y : α
as : Array (Array α)
bs : Array α
cs : Array (Array α)
h₂ : ∀ (l : Array α), l ∈ cs → l = #[]
⊢ (∃ as_1 bs_1,
      List.map toList as.toList ++ (bs.toList ++ [y]) :: List.map toList cs.toList = as_1 ++ bs_1 ∧
        (List.map toList as.toList).flatten ++ bs.toList = as_1.flatten ∧ [y] = bs_1.flatten) ∨
    ∃ as_1 bs_1 c cs_1 ds,
      List.map toList as.toList ++ (bs.toList ++ [y]) :: List.map toList cs.toList = as_1 ++ (bs_1 ++ c :: cs_1) :: ds ∧
        (List.map toList as.toList).flatten ++ bs.toList = as_1.flatten ++ bs_1 ∧ [y] = c :: cs_1 ++ ds.flatten

Tactic:
right

Result:
case of.mk.mpr.intro.intro.intro.intro.intro.h
α : Type u_1
y : α
as : Array (Array α)
bs : Array α
cs : Array (Array α)
h₂ : ∀ (l : Array α), l ∈ cs → l = #[]
⊢ ∃ as_1 bs_1 c cs_1 ds,
    List.map toList as.toList ++ (bs.toList ++ [y]) :: List.map toList cs.toList = as_1 ++ (bs_1 ++ c :: cs_1) :: ds ∧
      (List.map toList as.toList).flatten ++ bs.toList = as_1.flatten ++ bs_1 ∧ [y] = c :: cs_1 ++ ds.flatten

Proof state:
case of.mk.mp.inr.intro.intro.intro.intro.intro.intro.intro.inr.intro.intro
α : Type u_1
as : List (List α)
bs : List α
c : α
ds : List (List α)
h₂ : ∀ (l : List α), l ∈ ds → l = []
⊢ ∃ as_1 bs_1 cs,
    (List.map List.toArray (as ++ (bs ++ [c]) :: ds)).toArray = as_1.push (bs_1.push c) ++ cs ∧
      (∀ (l : Array α), l ∈ cs → l = #[]) ∧ { toList := as.flatten ++ bs } = as_1.flatten ++ bs_1

Tactic:
exact ⟨(as.map List.toArray).toArray, bs.toArray, (ds.map List.toArray).toArray, by simpa⟩

Result:
no goals

Proof state:
case of.mk.mp.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
y : α
as : List (List α)
bs : List α
c : α
cs : List α
ds : List (List α)
h : c :: cs = [] ∧ ds.flatten = [y] ∨ c :: cs = [y] ∧ ds.flatten = []
⊢ ∃ as_1 bs_1 cs_1,
    (List.map List.toArray (as ++ (bs ++ c :: cs) :: ds)).toArray = as_1.push (bs_1.push y) ++ cs_1 ∧
      (∀ (l : Array α), l ∈ cs_1 → l = #[]) ∧ { toList := as.flatten ++ bs } = as_1.flatten ++ bs_1

Tactic:
obtain (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩) := h

Result:
case of.mk.mp.inr.intro.intro.intro.intro.intro.intro.intro.inl.intro
α : Type u_1
y : α
as : List (List α)
bs : List α
c : α
cs : List α
ds : List (List α)
h₁ : c :: cs = []
h₂ : ds.flatten = [y]
⊢ ∃ as_1 bs_1 cs_1,
    (List.map List.toArray (as ++ (bs ++ c :: cs) :: ds)).toArray = as_1.push (bs_1.push y) ++ cs_1 ∧
      (∀ (l : Array α), l ∈ cs_1 → l = #[]) ∧ { toList := as.flatten ++ bs } = as_1.flatten ++ bs_1

case of.mk.mp.inr.intro.intro.intro.intro.intro.intro.intro.inr.intro
α : Type u_1
y : α
as : List (List α)
bs : List α
c : α
cs : List α
ds : List (List α)
h₁ : c :: cs = [y]
h₂ : ds.flatten = []
⊢ ∃ as_1 bs_1 cs_1,
    (List.map List.toArray (as ++ (bs ++ c :: cs) :: ds)).toArray = as_1.push (bs_1.push y) ++ cs_1 ∧
      (∀ (l : Array α), l ∈ cs_1 → l = #[]) ∧ { toList := as.flatten ++ bs } = as_1.flatten ++ bs_1