case nil
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁ l₂ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁
H : Pairwise (fun a b => f a → f b → False) []
⊢ eraseP (fun b => decide (f b)) [] ~ eraseP (fun b => decide (f b)) []

case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁✝
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : Pairwise (fun a b => f a → f b → False) l₁ → eraseP (fun b => decide (f b)) l₁ ~ eraseP (fun b => decide (f b)) l₂
H : Pairwise (fun a b => f a → f b → False) (a :: l₁)
⊢ eraseP (fun b => decide (f b)) (a :: l₁) ~ eraseP (fun b => decide (f b)) (a :: l₂)

case swap
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁ l₂ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁
a b : α
l : List α
H : Pairwise (fun a b => f a → f b → False) (b :: a :: l)
⊢ eraseP (fun b => decide (f b)) (b :: a :: l) ~ eraseP (fun b => decide (f b)) (a :: b :: l)

case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁✝
l₁ l₂ l₃ : List α
p₁ : l₁ ~ l₂
a✝ : l₂ ~ l₃
IH₁ : Pairwise (fun a b => f a → f b → False) l₁ → eraseP (fun b => decide (f b)) l₁ ~ eraseP (fun b => decide (f b)) l₂
IH₂ : Pairwise (fun a b => f a → f b → False) l₂ → eraseP (fun b => decide (f b)) l₂ ~ eraseP (fun b => decide (f b)) l₃
H : Pairwise (fun a b => f a → f b → False) l₁
⊢ eraseP (fun b => decide (f b)) l₁ ~ eraseP (fun b => decide (f b)) l₃
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁ l₂ : List α
H : Pairwise (fun a b => f a → f b → False) l₁
p : l₁ ~ l₂
⊢ eraseP (fun b => decide (f b)) l₁ ~ eraseP (fun b => decide (f b)) l₂
induction' p with a l₁ l₂ p IH a b l l₁ l₂ l₃ p₁ _ IH₁ IH₂
no goals
case nil
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁ l₂ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁
H : Pairwise (fun a b => f a → f b → False) []
⊢ eraseP (fun b => decide (f b)) [] ~ eraseP (fun b => decide (f b)) []
simp
case pos
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁✝
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : Pairwise (fun a b => f a → f b → False) l₁ → eraseP (fun b => decide (f b)) l₁ ~ eraseP (fun b => decide (f b)) l₂
H : Pairwise (fun a b => f a → f b → False) (a :: l₁)
h : f a
⊢ eraseP (fun b => decide (f b)) (a :: l₁) ~ eraseP (fun b => decide (f b)) (a :: l₂)

case neg
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁✝
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : Pairwise (fun a b => f a → f b → False) l₁ → eraseP (fun b => decide (f b)) l₁ ~ eraseP (fun b => decide (f b)) l₂
H : Pairwise (fun a b => f a → f b → False) (a :: l₁)
h : ¬f a
⊢ eraseP (fun b => decide (f b)) (a :: l₁) ~ eraseP (fun b => decide (f b)) (a :: l₂)
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁✝
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : Pairwise (fun a b => f a → f b → False) l₁ → eraseP (fun b => decide (f b)) l₁ ~ eraseP (fun b => decide (f b)) l₂
H : Pairwise (fun a b => f a → f b → False) (a :: l₁)
⊢ eraseP (fun b => decide (f b)) (a :: l₁) ~ eraseP (fun b => decide (f b)) (a :: l₂)
by_cases h : f a
no goals
case pos
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁✝
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : Pairwise (fun a b => f a → f b → False) l₁ → eraseP (fun b => decide (f b)) l₁ ~ eraseP (fun b => decide (f b)) l₂
H : Pairwise (fun a b => f a → f b → False) (a :: l₁)
h : f a
⊢ eraseP (fun b => decide (f b)) (a :: l₁) ~ eraseP (fun b => decide (f b)) (a :: l₂)
simp [h, p]
case neg
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁✝
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : Pairwise (fun a b => f a → f b → False) l₁ → eraseP (fun b => decide (f b)) l₁ ~ eraseP (fun b => decide (f b)) l₂
H : Pairwise (fun a b => f a → f b → False) (a :: l₁)
h : ¬f a
⊢ eraseP (fun b => decide (f b)) l₁ ~ eraseP (fun b => decide (f b)) l₂
case neg
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁✝
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : Pairwise (fun a b => f a → f b → False) l₁ → eraseP (fun b => decide (f b)) l₁ ~ eraseP (fun b => decide (f b)) l₂
H : Pairwise (fun a b => f a → f b → False) (a :: l₁)
h : ¬f a
⊢ eraseP (fun b => decide (f b)) (a :: l₁) ~ eraseP (fun b => decide (f b)) (a :: l₂)
simp [h]
no goals
case neg
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁✝
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : Pairwise (fun a b => f a → f b → False) l₁ → eraseP (fun b => decide (f b)) l₁ ~ eraseP (fun b => decide (f b)) l₂
H : Pairwise (fun a b => f a → f b → False) (a :: l₁)
h : ¬f a
⊢ eraseP (fun b => decide (f b)) l₁ ~ eraseP (fun b => decide (f b)) l₂
exact IH (pairwise_cons.1 H).2
case pos
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁ l₂ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁
a b : α
l : List α
H : Pairwise (fun a b => f a → f b → False) (b :: a :: l)
h₁ : f a
h₂ : f b
⊢ a :: l ~ b :: l

case neg
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁ l₂ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁
a b : α
l : List α
H : Pairwise (fun a b => f a → f b → False) (b :: a :: l)
h₁ : ¬f a
h₂ : ¬f b
⊢ b :: a :: eraseP (fun b => decide (f b)) l ~ a :: b :: eraseP (fun b => decide (f b)) l
case swap
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁ l₂ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁
a b : α
l : List α
H : Pairwise (fun a b => f a → f b → False) (b :: a :: l)
⊢ eraseP (fun b => decide (f b)) (b :: a :: l) ~ eraseP (fun b => decide (f b)) (a :: b :: l)
by_cases h₁ : f a <;> by_cases h₂ : f b <;> simp [h₁, h₂]
no goals
case pos
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁ l₂ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁
a b : α
l : List α
H : Pairwise (fun a b => f a → f b → False) (b :: a :: l)
h₁ : f a
h₂ : f b
⊢ a :: l ~ b :: l
cases (pairwise_cons.1 H).1 _ (mem_cons.2 (Or.inl rfl)) h₂ h₁
no goals
case neg
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁ l₂ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁
a b : α
l : List α
H : Pairwise (fun a b => f a → f b → False) (b :: a :: l)
h₁ : ¬f a
h₂ : ¬f b
⊢ b :: a :: eraseP (fun b => decide (f b)) l ~ a :: b :: eraseP (fun b => decide (f b)) l
apply swap
case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁✝
l₁ l₂ l₃ : List α
p₁ : l₁ ~ l₂
a✝ : l₂ ~ l₃
IH₁ : Pairwise (fun a b => f a → f b → False) l₁ → eraseP (fun b => decide (f b)) l₁ ~ eraseP (fun b => decide (f b)) l₂
IH₂ : Pairwise (fun a b => f a → f b → False) l₂ → eraseP (fun b => decide (f b)) l₂ ~ eraseP (fun b => decide (f b)) l₃
H : Pairwise (fun a b => f a → f b → False) l₁
⊢ Symmetric fun a b => f a → f b → False
case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁✝
l₁ l₂ l₃ : List α
p₁ : l₁ ~ l₂
a✝ : l₂ ~ l₃
IH₁ : Pairwise (fun a b => f a → f b → False) l₁ → eraseP (fun b => decide (f b)) l₁ ~ eraseP (fun b => decide (f b)) l₂
IH₂ : Pairwise (fun a b => f a → f b → False) l₂ → eraseP (fun b => decide (f b)) l₂ ~ eraseP (fun b => decide (f b)) l₃
H : Pairwise (fun a b => f a → f b → False) l₁
⊢ eraseP (fun b => decide (f b)) l₁ ~ eraseP (fun b => decide (f b)) l₃
refine' (IH₁ H).trans (IH₂ ((p₁.pairwise_iff _).1 H))
no goals
case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Prop
inst✝ : DecidablePred f
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => f a → f b → False) l₁✝
l₁ l₂ l₃ : List α
p₁ : l₁ ~ l₂
a✝ : l₂ ~ l₃
IH₁ : Pairwise (fun a b => f a → f b → False) l₁ → eraseP (fun b => decide (f b)) l₁ ~ eraseP (fun b => decide (f b)) l₂
IH₂ : Pairwise (fun a b => f a → f b → False) l₂ → eraseP (fun b => decide (f b)) l₂ ~ eraseP (fun b => decide (f b)) l₃
H : Pairwise (fun a b => f a → f b → False) l₁
⊢ Symmetric fun a b => f a → f b → False
exact fun a b h h₁ h₂ => h h₂ h₁