-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_eq_append_iff {f : α → Option β} :
    filterMap f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Proof state:
case mk.mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
L₁ L₂ : List β
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filterMap f l₁ = L₁ ∧ List.filterMap f l₂ = L₂) ↔
    ∃ l₁ l₂, l = l₁.toList ++ l₂.toList ∧ filterMap f l₁ = { toList := L₁ } ∧ filterMap f l₂ = { toList := L₂ }

Tactic:
constructor

Result:
case mk.mk.mk.mp
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
L₁ L₂ : List β
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filterMap f l₁ = L₁ ∧ List.filterMap f l₂ = L₂) →
    ∃ l₁ l₂, l = l₁.toList ++ l₂.toList ∧ filterMap f l₁ = { toList := L₁ } ∧ filterMap f l₂ = { toList := L₂ }

case mk.mk.mk.mpr
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
L₁ L₂ : List β
⊢ (∃ l₁ l₂, l = l₁.toList ++ l₂.toList ∧ filterMap f l₁ = { toList := L₁ } ∧ filterMap f l₂ = { toList := L₂ }) →
    ∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filterMap f l₁ = L₁ ∧ List.filterMap f l₂ = L₂

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
L₁ L₂ : List β
l₁ l₂ : List α
h₁ : filterMap f { toList := l₁ } = { toList := L₁ }
h₂ : filterMap f { toList := l₂ } = { toList := L₂ }
⊢ { toList := l₁ }.toList ++ { toList := l₂ }.toList = l₁ ++ l₂ ∧ List.filterMap f l₁ = L₁ ∧ List.filterMap f l₂ = L₂

Tactic:
simp_all

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
L₂ : Array β
f : α → Option β
l : List α
L₁ : List β
⊢ filterMap f { toList := l } = { toList := L₁ } ++ L₂ ↔
    ∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filterMap f l₁ = { toList := L₁ } ∧ filterMap f l₂ = L₂

Tactic:
rcases L₂ with ⟨L₂⟩

Result:
case mk.mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
L₁ L₂ : List β
⊢ filterMap f { toList := l } = { toList := L₁ } ++ { toList := L₂ } ↔
    ∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filterMap f l₁ = { toList := L₁ } ∧ filterMap f l₂ = { toList := L₂ }

Proof state:
case mk.mk.mk.mp
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
L₁ L₂ : List β
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filterMap f l₁ = L₁ ∧ List.filterMap f l₂ = L₂) →
    ∃ l₁ l₂, l = l₁.toList ++ l₂.toList ∧ filterMap f l₁ = { toList := L₁ } ∧ filterMap f l₂ = { toList := L₂ }

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

Result:
case mk.mk.mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
⊢ ∃ l₁_1 l₂_1,
    l₁ ++ l₂ = l₁_1.toList ++ l₂_1.toList ∧
      filterMap f l₁_1 = { toList := List.filterMap f l₁ } ∧ filterMap f l₂_1 = { toList := List.filterMap f l₂ }

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
⊢ l₁ ++ l₂ = { toList := l₁ }.toList ++ { toList := l₂ }.toList ∧
    filterMap f { toList := l₁ } = { toList := List.filterMap f l₁ } ∧
      filterMap f { toList := l₂ } = { toList := List.filterMap f l₂ }

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
L₁ L₂ : Array β
f : α → Option β
l : List α
⊢ filterMap f { toList := l } = L₁ ++ L₂ ↔
    ∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Tactic:
rcases L₁ with ⟨L₁⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
L₂ : Array β
f : α → Option β
l : List α
L₁ : List β
⊢ filterMap f { toList := l } = { toList := L₁ } ++ L₂ ↔
    ∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filterMap f l₁ = { toList := L₁ } ∧ filterMap f l₂ = L₂

Proof state:
case mk.mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
L₁ L₂ : List β
⊢ filterMap f { toList := l } = { toList := L₁ } ++ { toList := L₂ } ↔
    ∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filterMap f l₁ = { toList := L₁ } ∧ filterMap f l₂ = { toList := L₂ }

Tactic:
simp only [size_toArray, List.filterMap_toArray', List.append_toArray, mk.injEq,
  List.filterMap_eq_append_iff, toArray_eq_append_iff]

Result:
case mk.mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
L₁ L₂ : List β
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filterMap f l₁ = L₁ ∧ List.filterMap f l₂ = L₂) ↔
    ∃ l₁ l₂, l = l₁.toList ++ l₂.toList ∧ filterMap f l₁ = { toList := L₁ } ∧ filterMap f l₂ = { toList := L₂ }

Proof state:
α : Type u_1
β : Type u_2
l : Array α
L₁ L₂ : Array β
f : α → Option β
⊢ filterMap f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
L₁ L₂ : Array β
f : α → Option β
l : List α
⊢ filterMap f { toList := l } = L₁ ++ L₂ ↔
    ∃ l₁ l₂, { toList := l } = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Proof state:
case mk.mk.mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
⊢ ∃ l₁_1 l₂_1,
    l₁ ++ l₂ = l₁_1.toList ++ l₂_1.toList ∧
      filterMap f l₁_1 = { toList := List.filterMap f l₁ } ∧ filterMap f l₂_1 = { toList := List.filterMap f l₂ }

Tactic:
exact ⟨⟨l₁⟩, ⟨l₂⟩, by simp⟩

Result:
no goals

Proof state:
case mk.mk.mk.mpr
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
L₁ L₂ : List β
⊢ (∃ l₁ l₂, l = l₁.toList ++ l₂.toList ∧ filterMap f l₁ = { toList := L₁ } ∧ filterMap f l₂ = { toList := L₂ }) →
    ∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filterMap f l₁ = L₁ ∧ List.filterMap f l₂ = L₂

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

Result:
case mk.mk.mk.mpr.intro.mk.intro.mk.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
L₁ L₂ : List β
l₁ l₂ : List α
h₁ : filterMap f { toList := l₁ } = { toList := L₁ }
h₂ : filterMap f { toList := l₂ } = { toList := L₂ }
⊢ ∃ l₁_1 l₂_1,
    { toList := l₁ }.toList ++ { toList := l₂ }.toList = l₁_1 ++ l₂_1 ∧
      List.filterMap f l₁_1 = L₁ ∧ List.filterMap f l₂_1 = L₂

Proof state:
case mk.mk.mk.mpr.intro.mk.intro.mk.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
L₁ L₂ : List β
l₁ l₂ : List α
h₁ : filterMap f { toList := l₁ } = { toList := L₁ }
h₂ : filterMap f { toList := l₂ } = { toList := L₂ }
⊢ ∃ l₁_1 l₂_1,
    { toList := l₁ }.toList ++ { toList := l₂ }.toList = l₁_1 ++ l₂_1 ∧
      List.filterMap f l₁_1 = L₁ ∧ List.filterMap f l₂_1 = L₂

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

Result:
no goals