α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h : Nodup l
⊢ Nodup (map (fun x => f ↑x (_ : p ↑x)) (List.attach l))
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h : Nodup l
⊢ Nodup (List.pmap f l H)
rw [pmap_eq_map_attach]
no goals
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h : Nodup l
⊢ Nodup (map (fun x => f ↑x (_ : p ↑x)) (List.attach l))
exact h.attach.map fun ⟨a, ha⟩ ⟨b, hb⟩ h => by congr; exact hf a (H _ ha) b (H _ hb) h
case e_val
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b✝ : α
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h✝ : Nodup l
x✝¹ x✝ : { x // x ∈ l }
a : α
ha : a ∈ l
b : α
hb : b ∈ l
h :
  f ↑{ val := a, property := ha } (_ : p ↑{ val := a, property := ha }) =
    f ↑{ val := b, property := hb } (_ : p ↑{ val := b, property := hb })
⊢ a = b
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b✝ : α
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h✝ : Nodup l
x✝¹ x✝ : { x // x ∈ l }
a : α
ha : a ∈ l
b : α
hb : b ∈ l
h :
  f ↑{ val := a, property := ha } (_ : p ↑{ val := a, property := ha }) =
    f ↑{ val := b, property := hb } (_ : p ↑{ val := b, property := hb })
⊢ { val := a, property := ha } = { val := b, property := hb }
congr
no goals
case e_val
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b✝ : α
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h✝ : Nodup l
x✝¹ x✝ : { x // x ∈ l }
a : α
ha : a ∈ l
b : α
hb : b ∈ l
h :
  f ↑{ val := a, property := ha } (_ : p ↑{ val := a, property := ha }) =
    f ↑{ val := b, property := hb } (_ : p ↑{ val := b, property := hb })
⊢ a = b
exact hf a (H _ ha) b (H _ hb) h