Lean4
/-- Partial map. If `f : ∀ a, p a → β` is a partial function defined on `a : α` satisfying `p`,
then `pmap f s h` is essentially the same as `map f s` but is defined only when all members of `s`
satisfy `p`, using the proof to apply `f`.
-/
def pmap {P : α → Prop} (f : ∀ a, P a → β) (s : Sym2 α) : (∀ a ∈ s, P a) → Sym2 β :=
let g (p : α × α) (H : ∀ a ∈ Sym2.mk p, P a) : Sym2 β :=
s(f p.1 (H p.1 <| mem_mk_left _ _), f p.2 (H p.2 <| mem_mk_right _ _))
Quot.recOn s g fun p q hpq =>
funext fun Hq => by
rw [rel_iff'] at hpq
have Hp : ∀ a ∈ Sym2.mk p, P a := fun a hmem => Hq a (Sym2.mk_eq_mk_iff.2 hpq ▸ hmem : a ∈ Sym2.mk q)
have h : ∀ {s₂ e H}, Eq.ndrec (motive := fun s => (∀ a ∈ s, P a) → Sym2 β) (g p) (b := s₂) e H = g p Hp :=
by
rintro s₂ rfl _
rfl
refine h.trans (Quot.sound ?_)
rw [rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]
apply hpq.imp <;> rintro rfl <;> simp
