English
If f is mono, then Rel' f g defines an equivalence relation on X1 ⊕ X2 with respect to pushout.
Русский
Если f моно, Rel' f g определяет эквивалентное отношение на X1 ⊕ X2 в отношении пушоута.
LaTeX
$$Equivalence (Rel' f g)$$
Lean4
theorem equivalence_rel' [Mono f] : _root_.Equivalence (Rel' f g)
where
refl := Rel'.refl
symm h := h.symm
trans := by
rintro x y z (_ | ⟨_, _, h⟩ | s | _) hyz
· exact hyz
· obtain z₁ | z₂ := z
· rw [inl_rel'_inl_iff] at hyz
obtain rfl | ⟨_, _, h', h'', rfl⟩ := hyz
· exact Rel'.inl_inl _ _ h
· obtain rfl := (mono_iff_injective f).1 inferInstance h''
exact Rel'.inl_inl _ _ (h.trans h')
· rw [inl_rel'_inr_iff] at hyz
obtain ⟨s, hs, rfl⟩ := hyz
obtain rfl := (mono_iff_injective f).1 inferInstance hs
rw [← h]
apply Rel'.inl_inr
· obtain z₁ | z₂ := z
· replace hyz := hyz.symm
rw [inl_rel'_inr_iff] at hyz
obtain ⟨s', rfl, hs'⟩ := hyz
exact Rel'.inl_inl _ _ hs'
· rw [inr_rel'_inr_iff] at hyz
subst hyz
apply Rel'.inl_inr
· obtain z₁ | z₂ := z
· rw [inl_rel'_inl_iff] at hyz
obtain rfl | ⟨_, _, h, h', rfl⟩ := hyz
· apply Rel'.inr_inl
· obtain rfl := (mono_iff_injective f).1 inferInstance h'
rw [h]
apply Rel'.inr_inl
· rw [inl_rel'_inr_iff] at hyz
obtain ⟨s, hs, rfl⟩ := hyz
obtain rfl := (mono_iff_injective f).1 inferInstance hs
apply Rel'.refl
