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

Tactic:
exact ⟨(as.map Array.toList).toList, bs.toList, y, [], (cs.map Array.toList).toList, by simpa⟩

Result:
no goals

Proof state:
case of.mk.mpr.intro.intro.intro.intro.intro
α : Type u_1
y : α
xs : List (List α)
ys : List α
as : Array (Array α)
bs : Array α
cs : Array (Array α)
h₂ : ∀ (l : Array α), l ∈ cs → l = #[]
h₃ : { toList := ys } = as.flatten ++ bs
h₁ : xs = List.map toList as.toList ++ (bs.toList ++ [y]) :: List.map toList cs.toList
⊢ (∃ 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

Tactic:
subst h₁

Result:
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₃ : { toList := ys } = as.flatten ++ bs
⊢ (∃ 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

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

Tactic:
obtain ⟨xs, ys, rfl, h₁, h₂⟩ := h

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

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

Tactic:
exact ⟨((as ++ xs).map List.toArray).toArray, #[], (ys.map List.toArray).toArray, by simp,
  by simpa using h₂, by rw [flatten_toArray_map]; simpa⟩

Result:
no goals

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

Tactic:
rcases ys with ⟨ys⟩

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

Proof state:
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 = y ∧ cs = []
h₂ : ∀ (l : List α), l ∈ ds → l = []
⊢ ∃ 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 ⟨rfl, rfl⟩ := h₁

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

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 } = (as ++ xs).flatten.toArray ++ #[]

Tactic:
simpa

Result:
no goals

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

Tactic:
simp at h₁

Result:
no goals

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

Tactic:
simpa using h₂

Result:
no goals

Proof state:
α : Type u_1
as : List (List α)
bs : List α
c : α
ds : List (List α)
h₂ : ∀ (l : List α), l ∈ ds → l = []
⊢ (List.map List.toArray (as ++ (bs ++ [c]) :: ds)).toArray =
      (List.map List.toArray as).toArray.push (bs.toArray.push c) ++ (List.map List.toArray ds).toArray ∧
    (∀ (l : Array α), l ∈ (List.map List.toArray ds).toArray → l = #[]) ∧
      { toList := as.flatten ++ bs } = (List.map List.toArray as).toArray.flatten ++ bs.toArray

Tactic:
simpa

Result:
no goals

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

Tactic:
rintro (⟨as, bs, rfl, rfl, h⟩ | ⟨as, bs, c, cs, ds, rfl, rfl, h⟩)

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

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 : [y] = c :: cs ++ 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