-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseP_eq_iff {p} {l : Array α} :
    l.eraseP p = l' ↔
      ((∀ a ∈ l, ¬ p a) ∧ l = l') ∨
        ∃ a l₁ l₂, (∀ b ∈ l₁, ¬ p b) ∧ p a ∧ l = l₁.push a ++ l₂ ∧ l' = l₁ ++ l₂

Proof state:
α : Type u_1
p : α → Bool
a : α
l₁ : List α
h₁ : ∀ (b : α), b ∈ { toList := l₁ } → p b = false
h₂ : p a = true
x : List α
⊢ { toList := l₁ }.toList ++ a :: { toList := x }.toList = l₁ ++ a :: x ∧
    { toList := l₁ }.toList ++ { toList := x }.toList = l₁ ++ x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
l₁ : List α
h₁ : ∀ (b : α), b ∈ l₁ → p b = false
h₂ : p a = true
x : List α
⊢ ∀ (b : α), b ∈ { toList := l₁ } → p b = false

Tactic:
simpa using h₁

Result:
no goals

Proof state:
case mk.mk.mpr
α : Type u_1
p : α → Bool
l l' : List α
⊢ ((∀ (a : α), a ∈ l → p a = false) ∧ l = l' ∨
      ∃ a l₁,
        (∀ (b : α), b ∈ l₁ → p b = false) ∧
          p a = true ∧ ∃ x, l = l₁.toList ++ a :: x.toList ∧ l' = l₁.toList ++ x.toList) →
    (∀ (a : α), a ∈ l → p a = false) ∧ l = l' ∨
      ∃ a l₁, (∀ (b : α), b ∈ l₁ → p b = false) ∧ p a = true ∧ ∃ x, l = l₁ ++ a :: x ∧ l' = l₁ ++ x

Tactic:
rintro (h | ⟨a, ⟨l₁⟩, h₁, h₂, ⟨⟨x⟩, rfl, rfl⟩⟩)

Result:
case mk.mk.mpr.inl
α : Type u_1
p : α → Bool
l l' : List α
h : (∀ (a : α), a ∈ l → p a = false) ∧ l = l'
⊢ (∀ (a : α), a ∈ l → p a = false) ∧ l = l' ∨
    ∃ a l₁, (∀ (b : α), b ∈ l₁ → p b = false) ∧ p a = true ∧ ∃ x, l = l₁ ++ a :: x ∧ l' = l₁ ++ x

case mk.mk.mpr.inr.intro.intro.mk.intro.intro.intro.mk.intro
α : Type u_1
p : α → Bool
a : α
l₁ : List α
h₁ : ∀ (b : α), b ∈ { toList := l₁ } → p b = false
h₂ : p a = true
x : List α
⊢ (∀ (a_1 : α), a_1 ∈ { toList := l₁ }.toList ++ a :: { toList := x }.toList → p a_1 = false) ∧
      { toList := l₁ }.toList ++ a :: { toList := x }.toList = { toList := l₁ }.toList ++ { toList := x }.toList ∨
    ∃ a_1 l₁_1,
      (∀ (b : α), b ∈ l₁_1 → p b = false) ∧
        p a_1 = true ∧
          ∃ x_1,
            { toList := l₁ }.toList ++ a :: { toList := x }.toList = l₁_1 ++ a_1 :: x_1 ∧
              { toList := l₁ }.toList ++ { toList := x }.toList = l₁_1 ++ x_1

Proof state:
α : Type u_1
p : α → Bool
a : α
l₁ : List α
h₁ : ∀ (b : α), b ∈ l₁ → p b = false
h₂ : p a = true
x : List α
⊢ l₁ ++ a :: x = { toList := l₁ }.toList ++ a :: { toList := x }.toList ∧
    l₁ ++ x = { toList := l₁ }.toList ++ { toList := x }.toList

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk.mpr.inl
α : Type u_1
p : α → Bool
l l' : List α
h : (∀ (a : α), a ∈ l → p a = false) ∧ l = l'
⊢ (∀ (a : α), a ∈ l → p a = false) ∧ l = l' ∨
    ∃ a l₁, (∀ (b : α), b ∈ l₁ → p b = false) ∧ p a = true ∧ ∃ x, l = l₁ ++ a :: x ∧ l' = l₁ ++ x

Tactic:
exact Or.inl h

Result:
no goals

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

Tactic:
rcases l' with ⟨l'⟩

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

Proof state:
case mk.mk.mpr.inr.intro.intro.mk.intro.intro.intro.mk.intro
α : Type u_1
p : α → Bool
a : α
l₁ : List α
h₁ : ∀ (b : α), b ∈ { toList := l₁ } → p b = false
h₂ : p a = true
x : List α
⊢ (∀ (a_1 : α), a_1 ∈ { toList := l₁ }.toList ++ a :: { toList := x }.toList → p a_1 = false) ∧
      { toList := l₁ }.toList ++ a :: { toList := x }.toList = { toList := l₁ }.toList ++ { toList := x }.toList ∨
    ∃ a_1 l₁_1,
      (∀ (b : α), b ∈ l₁_1 → p b = false) ∧
        p a_1 = true ∧
          ∃ x_1,
            { toList := l₁ }.toList ++ a :: { toList := x }.toList = l₁_1 ++ a_1 :: x_1 ∧
              { toList := l₁ }.toList ++ { toList := x }.toList = l₁_1 ++ x_1

Tactic:
exact Or.inr ⟨a, l₁, by simpa using h₁, h₂, ⟨x, by simp⟩⟩

Result:
no goals

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

Tactic:
rcases l with ⟨l⟩

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

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

Tactic:
constructor

Result:
case mk.mk.mp
α : Type u_1
p : α → Bool
l l' : List α
⊢ ((∀ (a : α), a ∈ l → p a = false) ∧ l = l' ∨
      ∃ a l₁, (∀ (b : α), b ∈ l₁ → p b = false) ∧ p a = true ∧ ∃ x, l = l₁ ++ a :: x ∧ l' = l₁ ++ x) →
    (∀ (a : α), a ∈ l → p a = false) ∧ l = l' ∨
      ∃ a l₁,
        (∀ (b : α), b ∈ l₁ → p b = false) ∧
          p a = true ∧ ∃ x, l = l₁.toList ++ a :: x.toList ∧ l' = l₁.toList ++ x.toList

case mk.mk.mpr
α : Type u_1
p : α → Bool
l l' : List α
⊢ ((∀ (a : α), a ∈ l → p a = false) ∧ l = l' ∨
      ∃ a l₁,
        (∀ (b : α), b ∈ l₁ → p b = false) ∧
          p a = true ∧ ∃ x, l = l₁.toList ++ a :: x.toList ∧ l' = l₁.toList ++ x.toList) →
    (∀ (a : α), a ∈ l → p a = false) ∧ l = l' ∨
      ∃ a l₁, (∀ (b : α), b ∈ l₁ → p b = false) ∧ p a = true ∧ ∃ x, l = l₁ ++ a :: x ∧ l' = l₁ ++ x

Proof state:
case mk.mk.mp.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
l₁ : List α
h₁ : ∀ (b : α), b ∈ l₁ → p b = false
h₂ : p a = true
x : List α
⊢ (∀ (a_1 : α), a_1 ∈ l₁ ++ a :: x → p a_1 = false) ∧ l₁ ++ a :: x = l₁ ++ x ∨
    ∃ a_1 l₁_1,
      (∀ (b : α), b ∈ l₁_1 → p b = false) ∧
        p a_1 = true ∧ ∃ x_1, l₁ ++ a :: x = l₁_1.toList ++ a_1 :: x_1.toList ∧ l₁ ++ x = l₁_1.toList ++ x_1.toList

Tactic:
exact Or.inr ⟨a, ⟨l₁⟩, by simpa using h₁, h₂, ⟨⟨x⟩, by simp⟩⟩

Result:
no goals

Proof state:
case mk.mk.mp.inl
α : Type u_1
p : α → Bool
l l' : List α
h : (∀ (a : α), a ∈ l → p a = false) ∧ l = l'
⊢ (∀ (a : α), a ∈ l → p a = false) ∧ l = l' ∨
    ∃ a l₁,
      (∀ (b : α), b ∈ l₁ → p b = false) ∧ p a = true ∧ ∃ x, l = l₁.toList ++ a :: x.toList ∧ l' = l₁.toList ++ x.toList

Tactic:
exact Or.inl h

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
l₁ : List α
h₁ : ∀ (b : α), b ∈ { toList := l₁ } → p b = false
h₂ : p a = true
x : List α
⊢ ∀ (b : α), b ∈ l₁ → p b = false

Tactic:
simpa using h₁

Result:
no goals