-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.eraseP (f : α → Bool) {l₁ l₂ : List α}
    (H : Pairwise (fun a b => f a → f b → False) l₁) (p : l₁ ~ l₂) : eraseP f l₁ ~ eraseP f l₂

Proof state:
case swap
α : Type u_1
f : α → Bool
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b => f a = true → f b = true → False) (b :: a :: l)
⊢ List.eraseP f (b :: a :: l) ~ List.eraseP f (a :: b :: l)

Tactic:
by_cases h₁ : f a <;> by_cases h₂ : f b <;> simp [h₁, h₂]

Result:
case pos
α : Type u_1
f : α → Bool
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b => f a = true → f b = true → False) (b :: a :: l)
h₁ : f a = true
h₂ : f b = true
⊢ a :: l ~ b :: l

case neg
α : Type u_1
f : α → Bool
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b => f a = true → f b = true → False) (b :: a :: l)
h₁ : ¬f a = true
h₂ : ¬f b = true
⊢ b :: a :: List.eraseP f l ~ a :: b :: List.eraseP f l

Proof state:
case pos
α : Type u_1
f : α → Bool
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b => f a = true → f b = true → False) (b :: a :: l)
h₁ : f a = true
h₂ : f b = true
⊢ a :: l ~ b :: l

Tactic:
cases (pairwise_cons.1 H).1 _ (mem_cons.2 (Or.inl rfl)) h₂ h₁

Result:
no goals

Proof state:
case nil
α : Type u_1
f : α → Bool
l₁ l₂ : List α
H : Pairwise (fun a b => f a = true → f b = true → False) []
⊢ List.eraseP f [] ~ List.eraseP f []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
f : α → Bool
l₁ l₂ : List α
a : α
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
IH : Pairwise (fun a b => f a = true → f b = true → False) l₁✝ → List.eraseP f l₁✝ ~ List.eraseP f l₂✝
H : Pairwise (fun a b => f a = true → f b = true → False) (a :: l₁✝)
h : f a = true
⊢ List.eraseP f (a :: l₁✝) ~ List.eraseP f (a :: l₂✝)

Tactic:
simp [h, p]

Result:
no goals

Proof state:
case neg
α : Type u_1
f : α → Bool
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b => f a = true → f b = true → False) (b :: a :: l)
h₁ : ¬f a = true
h₂ : ¬f b = true
⊢ b :: a :: List.eraseP f l ~ a :: b :: List.eraseP f l

Tactic:
apply swap

Result:
no goals

Proof state:
α : Type u_1
f : α → Bool
l₁ l₂ : List α
a : α
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
IH : Pairwise (fun a b => f a = true → f b = true → False) l₁✝ → List.eraseP f l₁✝ ~ List.eraseP f l₂✝
H : Pairwise (fun a b => f a = true → f b = true → False) (a :: l₁✝)
h : ¬f a = true
⊢ List.eraseP f (a :: l₁✝) ~ List.eraseP f (a :: l₂✝)

Tactic:
simp [h]

Result:
α : Type u_1
f : α → Bool
l₁ l₂ : List α
a : α
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
IH : Pairwise (fun a b => f a = true → f b = true → False) l₁✝ → List.eraseP f l₁✝ ~ List.eraseP f l₂✝
H : Pairwise (fun a b => f a = true → f b = true → False) (a :: l₁✝)
h : ¬f a = true
⊢ List.eraseP f l₁✝ ~ List.eraseP f l₂✝

Proof state:
α : Type u_1
f : α → Bool
l₁ l₂ : List α
a : α
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
IH : Pairwise (fun a b => f a = true → f b = true → False) l₁✝ → List.eraseP f l₁✝ ~ List.eraseP f l₂✝
H : Pairwise (fun a b => f a = true → f b = true → False) (a :: l₁✝)
h : ¬f a = true
⊢ List.eraseP f l₁✝ ~ List.eraseP f l₂✝

Tactic:
exact IH (pairwise_cons.1 H).2

Result:
no goals

Proof state:
case cons
α : Type u_1
f : α → Bool
l₁ l₂ : List α
a : α
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
IH : Pairwise (fun a b => f a = true → f b = true → False) l₁✝ → List.eraseP f l₁✝ ~ List.eraseP f l₂✝
H : Pairwise (fun a b => f a = true → f b = true → False) (a :: l₁✝)
⊢ List.eraseP f (a :: l₁✝) ~ List.eraseP f (a :: l₂✝)

Tactic:
if h : f a then simp [h, p]
else simp [h]; exact IH (pairwise_cons.1 H).2

Result:
no goals

Proof state:
case trans
α : Type u_1
f : α → Bool
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
p₁ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
IH₁ : Pairwise (fun a b => f a = true → f b = true → False) l₁✝ → List.eraseP f l₁✝ ~ List.eraseP f l₂✝
IH₂ : Pairwise (fun a b => f a = true → f b = true → False) l₂✝ → List.eraseP f l₂✝ ~ List.eraseP f l₃✝
H : Pairwise (fun a b => f a = true → f b = true → False) l₁✝
⊢ ∀ {x y : α}, (f x = true → f y = true → False) → f y = true → f x = true → False

Tactic:
exact fun h h₁ h₂ => h h₂ h₁

Result:
no goals

Proof state:
case trans
α : Type u_1
f : α → Bool
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
p₁ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
IH₁ : Pairwise (fun a b => f a = true → f b = true → False) l₁✝ → List.eraseP f l₁✝ ~ List.eraseP f l₂✝
IH₂ : Pairwise (fun a b => f a = true → f b = true → False) l₂✝ → List.eraseP f l₂✝ ~ List.eraseP f l₃✝
H : Pairwise (fun a b => f a = true → f b = true → False) l₁✝
⊢ List.eraseP f l₁✝ ~ List.eraseP f l₃✝

Tactic:
refine (IH₁ H).trans (IH₂ ((p₁.pairwise_iff ?_).1 H))

Result:
case trans
α : Type u_1
f : α → Bool
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
p₁ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
IH₁ : Pairwise (fun a b => f a = true → f b = true → False) l₁✝ → List.eraseP f l₁✝ ~ List.eraseP f l₂✝
IH₂ : Pairwise (fun a b => f a = true → f b = true → False) l₂✝ → List.eraseP f l₂✝ ~ List.eraseP f l₃✝
H : Pairwise (fun a b => f a = true → f b = true → False) l₁✝
⊢ ∀ {x y : α}, (f x = true → f y = true → False) → f y = true → f x = true → False