definedAtRight — Mathlib

Lean4
/-- The set of partial isomorphisms defined at `b : β`, together with a proof that any
partial isomorphism can be extended to include `b`. We prove this by symmetry. -/
def definedAtRight [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] [Nonempty α] (b : β) : Cofinal (PartialIso α β)
    where
  carrier := {f | ∃ a, (a, b) ∈ f.val}
  isCofinal
    f := by
    rcases (definedAtLeft α b).isCofinal f.comm with ⟨f', ⟨a, ha⟩, hl⟩
    refine ⟨f'.comm, ⟨a, ?_⟩, ?_⟩
    · change (a, b) ∈ f'.val.image _
      rwa [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage]
    · change _ ⊆ f'.val.image _
      rwa [← Finset.coe_subset, Finset.coe_image, ← Equiv.symm_image_subset, ← Finset.coe_image, Finset.coe_subset]
Похожие утверждения