-- 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
α : 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₁ : List.map toList (List.map List.toArray xs).toArray.toList = List.map toList (as.push (bs.push y) ++ 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:
simp [Function.comp_def] at h₁

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

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₃ : { 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

Tactic:
replace h₃ := congrArg Array.toList 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 }.toList = (as.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

Proof state:
α : Type u_1
y : α
as : Array (Array α)
bs : Array α
cs : Array (Array α)
h₂ : ∀ (l : Array α), l ∈ cs → l = #[]
⊢ List.map toList as.toList ++ (bs.toList ++ [y]) :: List.map toList cs.toList =
      (map toList as).toList ++ (bs.toList ++ [y]) :: (map toList cs).toList ∧
    (List.map toList as.toList).flatten ++ bs.toList = (map toList as).toList.flatten ++ bs.toList ∧
      [y] = [y] ++ (map toList cs).toList.flatten

Tactic:
simpa

Result:
no goals

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₃ : { toList := ys }.toList = (as.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:
simp at 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₃ : 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

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

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

Result:
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₁ : (List.map List.toArray xs).toArray = as.push (bs.push y) ++ cs
h₂ : ∀ (l : Array α), l ∈ cs → l = #[]
h₃ : { 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 : α
xs : List (List α)
ys : List α
as : Array (Array α)
bs : Array α
cs : Array (Array α)
h₁ : (List.map List.toArray xs).toArray = as.push (bs.push y) ++ cs
h₂ : ∀ (l : Array α), l ∈ cs → l = #[]
h₃ : { 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

Tactic:
replace h₁ := congrArg (List.map Array.toList) (congrArg Array.toList h₁)

Result:
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₁ : List.map toList (List.map List.toArray xs).toArray.toList = List.map toList (as.push (bs.push y) ++ 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

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

Tactic:
simp at h₁ h₂

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

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

Tactic:
simp

Result:
no goals