-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_eq_append_iff {p : α → Bool} :
    filter p l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂

Proof state:
case mk.mk.mk
α : Type u_1
p : α → Bool
l L₁ L₂ : List α
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filter p l₁ = L₁ ∧ List.filter p l₂ = L₂) ↔
    ∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filter p l₁ = { toList := L₁ } ∧ filter p l₂ = { toList := L₂ }

Tactic:
constructor

Result:
case mk.mk.mk.mp
α : Type u_1
p : α → Bool
l L₁ L₂ : List α
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filter p l₁ = L₁ ∧ List.filter p l₂ = L₂) →
    ∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filter p l₁ = { toList := L₁ } ∧ filter p l₂ = { toList := L₂ }

case mk.mk.mk.mpr
α : Type u_1
p : α → Bool
l L₁ L₂ : List α
⊢ (∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filter p l₁ = { toList := L₁ } ∧ filter p l₂ = { toList := L₂ }) →
    ∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filter p l₁ = L₁ ∧ List.filter p l₂ = L₂

Proof state:
case mk.mk
α : Type u_1
L₂ : Array α
p : α → Bool
l L₁ : List α
⊢ filter p { toList := l } = { toList := L₁ } ++ L₂ ↔
    ∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filter p l₁ = { toList := L₁ } ∧ filter p l₂ = L₂

Tactic:
rcases L₂ with ⟨L₂⟩

Result:
case mk.mk.mk
α : Type u_1
p : α → Bool
l L₁ L₂ : List α
⊢ filter p { toList := l } = { toList := L₁ } ++ { toList := L₂ } ↔
    ∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filter p l₁ = { toList := L₁ } ∧ filter p l₂ = { toList := L₂ }

Proof state:
case mk.mk.mk
α : Type u_1
p : α → Bool
l L₁ L₂ : List α
⊢ filter p { toList := l } = { toList := L₁ } ++ { toList := L₂ } ↔
    ∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filter p l₁ = { toList := L₁ } ∧ filter p l₂ = { toList := L₂ }

Tactic:
simp only [size_toArray, List.filter_toArray', List.append_toArray, mk.injEq,
  List.filter_eq_append_iff]

Result:
case mk.mk.mk
α : Type u_1
p : α → Bool
l L₁ L₂ : List α
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filter p l₁ = L₁ ∧ List.filter p l₂ = L₂) ↔
    ∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filter p l₁ = { toList := L₁ } ∧ filter p l₂ = { toList := L₂ }

Proof state:
case mk
α : Type u_1
L₁ L₂ : Array α
p : α → Bool
l : List α
⊢ filter p { toList := l } = L₁ ++ L₂ ↔ ∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂

Tactic:
rcases L₁ with ⟨L₁⟩

Result:
case mk.mk
α : Type u_1
L₂ : Array α
p : α → Bool
l L₁ : List α
⊢ filter p { toList := l } = { toList := L₁ } ++ L₂ ↔
    ∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filter p l₁ = { toList := L₁ } ∧ filter p l₂ = L₂

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ { toList := l₁ ++ l₂ } = l₁.toArray ++ l₂.toArray ∧
    filter p l₁.toArray = { toList := List.filter p l₁ } ∧ filter p l₂.toArray = { toList := List.filter p l₂ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l L₁ L₂ : Array α
p : α → Bool
⊢ filter p l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
L₁ L₂ : Array α
p : α → Bool
l : List α
⊢ filter p { toList := l } = L₁ ++ L₂ ↔ ∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂

Proof state:
α : Type u_1
p : α → Bool
l L₁ L₂ l₁ l₂ : List α
h₁ : { toList := l } = { toList := l₁ } ++ { toList := l₂ }
h₂ : filter p { toList := l₁ } = { toList := L₁ }
h₃ : filter p { toList := l₂ } = { toList := L₂ }
⊢ l = l₁ ++ l₂ ∧ List.filter p l₁ = L₁ ∧ List.filter p l₂ = L₂

Tactic:
simp_all

Result:
no goals

Proof state:
case mk.mk.mk.mpr
α : Type u_1
p : α → Bool
l L₁ L₂ : List α
⊢ (∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filter p l₁ = { toList := L₁ } ∧ filter p l₂ = { toList := L₂ }) →
    ∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filter p l₁ = L₁ ∧ List.filter p l₂ = L₂

Tactic:
rintro ⟨⟨l₁⟩, ⟨l₂⟩, h₁, h₂, h₃⟩

Result:
case mk.mk.mk.mpr.intro.mk.intro.mk.intro.intro
α : Type u_1
p : α → Bool
l L₁ L₂ l₁ l₂ : List α
h₁ : { toList := l } = { toList := l₁ } ++ { toList := l₂ }
h₂ : filter p { toList := l₁ } = { toList := L₁ }
h₃ : filter p { toList := l₂ } = { toList := L₂ }
⊢ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filter p l₁ = L₁ ∧ List.filter p l₂ = L₂

Proof state:
case mk.mk.mk.mp
α : Type u_1
p : α → Bool
l L₁ L₂ : List α
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filter p l₁ = L₁ ∧ List.filter p l₂ = L₂) →
    ∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filter p l₁ = { toList := L₁ } ∧ filter p l₂ = { toList := L₂ }

Tactic:
rintro ⟨l₁, l₂, rfl, rfl, rfl⟩

Result:
case mk.mk.mk.mp.intro.intro.intro.intro
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ ∃ l₁_1 l₂_1,
    { toList := l₁ ++ l₂ } = l₁_1 ++ l₂_1 ∧
      filter p l₁_1 = { toList := List.filter p l₁ } ∧ filter p l₂_1 = { toList := List.filter p l₂ }

Proof state:
case mk.mk.mk.mp.intro.intro.intro.intro
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ ∃ l₁_1 l₂_1,
    { toList := l₁ ++ l₂ } = l₁_1 ++ l₂_1 ∧
      filter p l₁_1 = { toList := List.filter p l₁ } ∧ filter p l₂_1 = { toList := List.filter p l₂ }

Tactic:
refine ⟨l₁.toArray, l₂.toArray, by simp⟩

Result:
no goals

Proof state:
case mk.mk.mk.mpr.intro.mk.intro.mk.intro.intro
α : Type u_1
p : α → Bool
l L₁ L₂ l₁ l₂ : List α
h₁ : { toList := l } = { toList := l₁ } ++ { toList := l₂ }
h₂ : filter p { toList := l₁ } = { toList := L₁ }
h₃ : filter p { toList := l₂ } = { toList := L₂ }
⊢ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filter p l₁ = L₁ ∧ List.filter p l₂ = L₂

Tactic:
refine ⟨l₁, l₂, by simp_all⟩

Result:
no goals