Reverse of List.attachWith_congr

Stream: new members

[Jakub Nowak]

I'm looking for a reverse of List.attachWith_congr. Is it missing API, or is there some tactic I'm supposed to use for this?

opaque P : Nat → Prop

example (l₁ l₂ : List Nat) (H₁ : ∀ x ∈ l₁, P x) (H₂ : ∀ x ∈ l₂, P x) :
    l₁.attachWith P H₁ = l₂.attachWith P H₂ → l₁ = l₂ := by
  intro eq
  sorry

[Jakub Nowak]

Kinda analogous lemma for Subtype is called Subtype.ext_iff.mp.

[Ruben Van de Velde]

import Mathlib
opaque P : Nat → Prop

example (l₁ l₂ : List Nat) (H₁ : ∀ x ∈ l₁, P x) (H₂ : ∀ x ∈ l₂, P x) :
    l₁.attachWith P H₁ = l₂.attachWith P H₂ → l₁ = l₂ := by
  intro h
  apply_fun List.unattach at h
  simpa using h