Lean4
/-- An equivalence `e : α ≃ β` generates an equivalence between quotient spaces,
if `ra a₁ a₂ ↔ rb (e a₁) (e a₂)`. -/
protected def congr {ra : α → α → Prop} {rb : β → β → Prop} (e : α ≃ β) (eq : ∀ a₁ a₂, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) :
Quot ra ≃ Quot rb where
toFun := Quot.map e fun a₁ a₂ => (eq a₁ a₂).1
invFun :=
Quot.map e.symm fun b₁ b₂ h =>
(eq (e.symm b₁) (e.symm b₂)).2 ((e.apply_symm_apply b₁).symm ▸ (e.apply_symm_apply b₂).symm ▸ h)
left_inv := by rintro ⟨a⟩; simp only [Quot.map, Equiv.symm_apply_apply]
right_inv := by rintro ⟨a⟩; simp only [Quot.map, Equiv.apply_symm_apply]
