-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isInfix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l₂ : List β} :
    l₂ <:+: filterMap f l₁ ↔ ∃ l, l <:+: l₁ ∧ l₂ = filterMap f l

Proof state:
case mp
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ s t l₁_1 l₂_1,
      l₁ = l₁_1 ++ l₂_1 ∧
        (∃ l₁ l₂_2, l₁_1 = l₁ ++ l₂_2 ∧ filterMap f l₁ = s ∧ filterMap f l₂_2 = l₂) ∧ filterMap f l₂_1 = t) →
    ∃ l, (∃ s t, s ++ l ++ t = l₁) ∧ l₂ = filterMap f l

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

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ l₃ : List α
⊢ ∃ l, (∃ s t, s ++ l ++ t = l₂ ++ l₃ ++ l₁) ∧ filterMap f l₃ = filterMap f l

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₃ l₂ l₁ : List α
⊢ ∃ s t l₁_1 l₂_1,
    l₂ ++ l₃ ++ l₁ = l₁_1 ++ l₂_1 ∧
      (∃ l₁ l₂, l₁_1 = l₁ ++ l₂ ∧ filterMap f l₁ = s ∧ filterMap f l₂ = filterMap f l₃) ∧ filterMap f l₂_1 = t

Tactic:
exact ⟨_, _, _, l₁, rfl, ⟨⟨l₂, l₃, rfl, rfl, rfl⟩, rfl⟩⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ l, (∃ s t, s ++ l ++ t = l₁) ∧ l₂ = filterMap f l) →
    ∃ s t l₁_1 l₂_1,
      l₁ = l₁_1 ++ l₂_1 ∧
        (∃ l₁ l₂_2, l₁_1 = l₁ ++ l₂_2 ∧ filterMap f l₁ = s ∧ filterMap f l₂_2 = l₂) ∧ filterMap f l₂_1 = t

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

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₃ l₂ l₁ : List α
⊢ ∃ s t l₁_1 l₂_1,
    l₂ ++ l₃ ++ l₁ = l₁_1 ++ l₂_1 ∧
      (∃ l₁ l₂, l₁_1 = l₁ ++ l₂ ∧ filterMap f l₁ = s ∧ filterMap f l₂ = filterMap f l₃) ∧ filterMap f l₂_1 = t

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ l₃ : List α
⊢ ∃ l, (∃ s t, s ++ l ++ t = l₂ ++ l₃ ++ l₁) ∧ filterMap f l₃ = filterMap f l

Tactic:
exact ⟨l₃, ⟨l₂, l₁, rfl⟩, rfl⟩

Result:
no goals

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

Tactic:
simp only [IsInfix, append_eq_filterMap_iff, filterMap_eq_append_iff]

Result:
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ s t l₁_1 l₂_1,
      l₁ = l₁_1 ++ l₂_1 ∧
        (∃ l₁ l₂_2, l₁_1 = l₁ ++ l₂_2 ∧ filterMap f l₁ = s ∧ filterMap f l₂_2 = l₂) ∧ filterMap f l₂_1 = t) ↔
    ∃ l, (∃ s t, s ++ l ++ t = l₁) ∧ l₂ = filterMap f l

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ s t l₁_1 l₂_1,
      l₁ = l₁_1 ++ l₂_1 ∧
        (∃ l₁ l₂_2, l₁_1 = l₁ ++ l₂_2 ∧ filterMap f l₁ = s ∧ filterMap f l₂_2 = l₂) ∧ filterMap f l₂_1 = t) ↔
    ∃ l, (∃ s t, s ++ l ++ t = l₁) ∧ l₂ = filterMap f l

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ s t l₁_1 l₂_1,
      l₁ = l₁_1 ++ l₂_1 ∧
        (∃ l₁ l₂_2, l₁_1 = l₁ ++ l₂_2 ∧ filterMap f l₁ = s ∧ filterMap f l₂_2 = l₂) ∧ filterMap f l₂_1 = t) →
    ∃ l, (∃ s t, s ++ l ++ t = l₁) ∧ l₂ = filterMap f l

case mpr
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ l, (∃ s t, s ++ l ++ t = l₁) ∧ l₂ = filterMap f l) →
    ∃ s t l₁_1 l₂_1,
      l₁ = l₁_1 ++ l₂_1 ∧
        (∃ l₁ l₂_2, l₁_1 = l₁ ++ l₂_2 ∧ filterMap f l₁ = s ∧ filterMap f l₂_2 = l₂) ∧ filterMap f l₂_1 = t