-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_eq_push_iff {f : α → Option β} {l : Array α} {l' : Array β} {b : β} :
    filterMap f l = l'.push b ↔ ∃ l₁ a l₂,
      l = l₁.push a ++ l₂ ∧ filterMap f l₁ = l' ∧ f a = some b ∧ (∀ x, x ∈ l₂ → f x = none)

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
l' : Array β
b : β
⊢ filterMap f l = l'.push b ↔
    ∃ l₁ a l₂, l = l₁.push a ++ l₂ ∧ filterMap f l₁ = l' ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
l' : Array β
b : β
l : List α
⊢ filterMap f { toList := l } = l'.push b ↔
    ∃ l₁ a l₂, { toList := l } = l₁.push a ++ l₂ ∧ filterMap f l₁ = l' ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
l₁ : List α
a : α
l₂ : List α
h₁ : { toList := l } = { toList := l₁ }.push a ++ { toList := l₂ }
h₂ : filterMap f { toList := l₁ } = { toList := l' }
h₃ : f a = some b
h₄ : ∀ (x : α), x ∈ { toList := l₂ } → f x = none
⊢ l.reverse = l₂.reverse ++ a :: l₁.reverse ∧
    (∀ (x : α), x ∈ l₂.reverse → f x = none) ∧ f a = some b ∧ List.filterMap f l₁.reverse = l'.reverse

Tactic:
simp_all

Result:
no goals

Proof state:
case mk.mk.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
l₁ : List α
a : α
l₂ : List α
h₁ : l.reverse = l₁ ++ a :: l₂
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
h₃ : f a = some b
h₄ : List.filterMap f l₂ = l'.reverse
⊢ ∃ l₁ a l₂,
    { toList := l } = l₁.push a ++ l₂ ∧
      filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none

Tactic:
refine ⟨l₂.reverse.toArray, a, l₁.reverse.toArray, by simp_all⟩

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
⊢ (List.filterMap f l).reverse = (l' ++ [b]).reverse ↔
    ∃ l₁ a l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none

Tactic:
simp only [← List.filterMap_reverse]

Result:
case mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
⊢ List.filterMap f l.reverse = (l' ++ [b]).reverse ↔
    ∃ l₁ a l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
⊢ List.filterMap f l = l' ++ [b] ↔
    ∃ l₁ a l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none

Tactic:
rw [← List.reverse_inj]

Result:
case mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
⊢ (List.filterMap f l).reverse = (l' ++ [b]).reverse ↔
    ∃ l₁ a l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
l₁ : List α
a : α
l₂ : List α
h₁ : l.reverse = l₁ ++ a :: l₂
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
h₃ : f a = some b
h₄ : List.filterMap f l₂ = l'.reverse
⊢ { toList := l } = l₂.reverse.toArray.push a ++ l₁.reverse.toArray ∧
    filterMap f l₂.reverse.toArray = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁.reverse.toArray → f x = none

Tactic:
simp_all

Result:
no goals

Proof state:
case mk.mk.mp
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
⊢ (∃ l₁ a l₂,
      l.reverse = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → f x = none) ∧ f a = some b ∧ List.filterMap f l₂ = l'.reverse) →
    ∃ l₁ a l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none

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

Result:
case mk.mk.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
l₁ : List α
a : α
l₂ : List α
h₁ : l.reverse = l₁ ++ a :: l₂
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
h₃ : f a = some b
h₄ : List.filterMap f l₂ = l'.reverse
⊢ ∃ l₁ a l₂,
    { toList := l } = l₁.push a ++ l₂ ∧
      filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none

Proof state:
case mk.mk.mpr
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
⊢ (∃ l₁ a l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none) →
    ∃ l₁ a l₂,
      l.reverse = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → f x = none) ∧ f a = some b ∧ List.filterMap f l₂ = l'.reverse

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

Result:
case mk.mk.mpr.intro.mk.intro.intro.mk.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
l₁ : List α
a : α
l₂ : List α
h₁ : { toList := l } = { toList := l₁ }.push a ++ { toList := l₂ }
h₂ : filterMap f { toList := l₁ } = { toList := l' }
h₃ : f a = some b
h₄ : ∀ (x : α), x ∈ { toList := l₂ } → f x = none
⊢ ∃ l₁ a l₂,
    l.reverse = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → f x = none) ∧ f a = some b ∧ List.filterMap f l₂ = l'.reverse

Proof state:
case mk.mk.mpr.intro.mk.intro.intro.mk.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
l₁ : List α
a : α
l₂ : List α
h₁ : { toList := l } = { toList := l₁ }.push a ++ { toList := l₂ }
h₂ : filterMap f { toList := l₁ } = { toList := l' }
h₃ : f a = some b
h₄ : ∀ (x : α), x ∈ { toList := l₂ } → f x = none
⊢ ∃ l₁ a l₂,
    l.reverse = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → f x = none) ∧ f a = some b ∧ List.filterMap f l₂ = l'.reverse

Tactic:
refine ⟨l₂.reverse, a, l₁.reverse, by simp_all⟩

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
⊢ List.filterMap f l.reverse = (l' ++ [b]).reverse ↔
    ∃ l₁ a l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none

Tactic:
simp only [List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append,
  List.singleton_append]

Result:
case mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
⊢ List.filterMap f l.reverse = b :: l'.reverse ↔
    ∃ l₁ a l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
⊢ filterMap f { toList := l } = { toList := l' }.push b ↔
    ∃ l₁ a l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none

Tactic:
simp only [size_toArray, List.filterMap_toArray', List.push_toArray, mk.injEq]

Result:
case mk.mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : List α
l' : List β
⊢ List.filterMap f l = l' ++ [b] ↔
    ∃ l₁ a l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filterMap f l₁ = { toList := l' } ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → f x = none