-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_eq_push_iff {p : α → Bool} {l l' : Array α} {a : α} :
    filter p l = l'.push a ↔
      ∃ l₁ l₂, l = l₁.push a ++ l₂ ∧ filter p l₁ = l' ∧ p a ∧ (∀ x, x ∈ l₂ → ¬p x)

Proof state:
case mk.mk.mp.intro.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
l l' l₁ l₂ : List α
h₁ : l.reverse = l₁ ++ a :: l₂
h₂ : ∀ (x : α), x ∈ l₁ → ¬p x = true
h₃ : p a = true
h₄ : List.filter p l₂ = l'.reverse
⊢ ∃ l₁ l₂,
    { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → p x = false

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

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l l' : Array α
a : α
⊢ filter p l = l'.push a ↔
    ∃ l₁ l₂, l = l₁.push a ++ l₂ ∧ filter p l₁ = l' ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → ¬p x = true

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
l' : Array α
a : α
l : List α
⊢ filter p { toList := l } = l'.push a ↔
    ∃ l₁ l₂, { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = l' ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → ¬p x = true

Proof state:
case mk.mk
α : Type u_1
p : α → Bool
a : α
l l' : List α
⊢ (∃ l₁ l₂,
      l.reverse = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ List.filter p l₂ = l'.reverse) ↔
    ∃ l₁ l₂,
      { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → p x = false

Tactic:
constructor

Result:
case mk.mk.mp
α : Type u_1
p : α → Bool
a : α
l l' : List α
⊢ (∃ l₁ l₂,
      l.reverse = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ List.filter p l₂ = l'.reverse) →
    ∃ l₁ l₂,
      { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → p x = false

case mk.mk.mpr
α : Type u_1
p : α → Bool
a : α
l l' : List α
⊢ (∃ l₁ l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → p x = false) →
    ∃ l₁ l₂, l.reverse = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ List.filter p l₂ = l'.reverse

Proof state:
case mk.mk
α : Type u_1
p : α → Bool
a : α
l l' : List α
⊢ filter p { toList := l } = { toList := l' }.push a ↔
    ∃ l₁ l₂,
      { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → ¬p x = true

Tactic:
simp only [size_toArray, List.filter_toArray', List.push_toArray, mk.injEq, Bool.not_eq_true]

Result:
case mk.mk
α : Type u_1
p : α → Bool
a : α
l l' : List α
⊢ List.filter p l = l' ++ [a] ↔
    ∃ l₁ l₂,
      { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → p x = false

Proof state:
case mk.mk.mpr.intro.mk.intro.mk.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
l l' l₁ l₂ : List α
h₁ : { toList := l } = { toList := l₁ }.push a ++ { toList := l₂ }
h₂ : filter p { toList := l₁ } = { toList := l' }
h₃ : p a = true
h₄ : ∀ (x : α), x ∈ { toList := l₂ } → p x = false
⊢ ∃ l₁ l₂, l.reverse = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ List.filter p l₂ = l'.reverse

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

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
p : α → Bool
a : α
l l' : List α
⊢ List.filter p l.reverse = (l' ++ [a]).reverse ↔
    ∃ l₁ l₂,
      { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → p x = false

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
p : α → Bool
a : α
l l' : List α
⊢ List.filter p l.reverse = a :: l'.reverse ↔
    ∃ l₁ l₂,
      { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → p x = false

Proof state:
case mk.mk.mp
α : Type u_1
p : α → Bool
a : α
l l' : List α
⊢ (∃ l₁ l₂,
      l.reverse = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ List.filter p l₂ = l'.reverse) →
    ∃ l₁ l₂,
      { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → p x = false

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

Result:
case mk.mk.mp.intro.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
l l' l₁ l₂ : List α
h₁ : l.reverse = l₁ ++ a :: l₂
h₂ : ∀ (x : α), x ∈ l₁ → ¬p x = true
h₃ : p a = true
h₄ : List.filter p l₂ = l'.reverse
⊢ ∃ l₁ l₂,
    { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → p x = false

Proof state:
case mk.mk
α : Type u_1
p : α → Bool
a : α
l l' : List α
⊢ List.filter p l.reverse = a :: l'.reverse ↔
    ∃ l₁ l₂,
      { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → p x = false

Tactic:
rw [List.filter_eq_cons_iff]

Result:
case mk.mk
α : Type u_1
p : α → Bool
a : α
l l' : List α
⊢ (∃ l₁ l₂,
      l.reverse = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ List.filter p l₂ = l'.reverse) ↔
    ∃ l₁ l₂,
      { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → p x = false

Proof state:
α : Type u_1
p : α → Bool
a : α
l l' l₁ l₂ : List α
h₁ : l.reverse = l₁ ++ a :: l₂
h₂ : ∀ (x : α), x ∈ l₁ → ¬p x = true
h₃ : p a = true
h₄ : List.filter p l₂ = l'.reverse
⊢ { toList := l } = l₂.reverse.toArray.push a ++ l₁.reverse.toArray ∧
    filter p l₂.reverse.toArray = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₁.reverse.toArray → p x = false

Tactic:
simp_all

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
p : α → Bool
a : α
l l' : List α
⊢ List.filter p l = l' ++ [a] ↔
    ∃ l₁ l₂,
      { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → p x = false

Tactic:
rw [← List.reverse_inj]

Result:
case mk.mk
α : Type u_1
p : α → Bool
a : α
l l' : List α
⊢ (List.filter p l).reverse = (l' ++ [a]).reverse ↔
    ∃ l₁ l₂,
      { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → p x = false

Proof state:
α : Type u_1
p : α → Bool
a : α
l l' l₁ l₂ : List α
h₁ : { toList := l } = { toList := l₁ }.push a ++ { toList := l₂ }
h₂ : filter p { toList := l₁ } = { toList := l' }
h₃ : p a = true
h₄ : ∀ (x : α), x ∈ { toList := l₂ } → p x = false
⊢ l.reverse = l₂.reverse ++ a :: l₁.reverse ∧
    (∀ (x : α), x ∈ l₂.reverse → ¬p x = true) ∧ p a = true ∧ List.filter p l₁.reverse = l'.reverse

Tactic:
simp_all

Result:
no goals

Proof state:
case mk.mk.mpr
α : Type u_1
p : α → Bool
a : α
l l' : List α
⊢ (∃ l₁ l₂,
      { toList := l } = l₁.push a ++ l₂ ∧
        filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → p x = false) →
    ∃ l₁ l₂, l.reverse = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ List.filter p l₂ = l'.reverse

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

Result:
case mk.mk.mpr.intro.mk.intro.mk.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
l l' l₁ l₂ : List α
h₁ : { toList := l } = { toList := l₁ }.push a ++ { toList := l₂ }
h₂ : filter p { toList := l₁ } = { toList := l' }
h₃ : p a = true
h₄ : ∀ (x : α), x ∈ { toList := l₂ } → p x = false
⊢ ∃ l₁ l₂, l.reverse = l₁ ++ a :: l₂ ∧ (∀ (x : α), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ List.filter p l₂ = l'.reverse

Proof state:
case mk.mk
α : Type u_1
p : α → Bool
a : α
l l' : List α
⊢ (List.filter p l).reverse = (l' ++ [a]).reverse ↔
    ∃ l₁ l₂,
      { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → p x = false

Tactic:
simp only [← List.filter_reverse]

Result:
case mk.mk
α : Type u_1
p : α → Bool
a : α
l l' : List α
⊢ List.filter p l.reverse = (l' ++ [a]).reverse ↔
    ∃ l₁ l₂,
      { toList := l } = l₁.push a ++ l₂ ∧ filter p l₁ = { toList := l' } ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → p x = false