theorem setoid_trans {a : Sort u_1} (r : Setoid a) (x y z : a) (h : r x y ∧ r y z) : r x z

theorem setoid_refl {a : Sort u_1} (r : Setoid a) (x : a) : r x x

theorem classes_nonempty {a : Type u_1} (r : Setoid a) : ∅ ∉ r.classes

theorem classes_pw_disjoint {a : Type u_1} (r : Setoid a) : r.classes.PairwiseDisjoint id

theorem nondisjoint_classes_eq {a : Type u_1} {x y : Set a} {z : a} (r : Setoid a) (h1 : x ∈ r.classes) (h2 : y ∈ r.classes) (hz : z ∈ x ∧ z ∈ y) : x = y

theorem exists_class {a : Type u_1} (r : Setoid a) (x : a) : ∃ b ∈ r.classes, x ∈ b

theorem covers_unique {a : Type u_1} (r : Setoid a) (x : a) : ∃! b : Set a, b ∈ r.classes ∧ x ∈ b

theorem setoid_is_partition {a : Type u_1} (r : Setoid a) : Setoid.IsPartition r.classes

theorem mathlib_inj_iff_has_left_inv {A : Sort u_1} {B : Sort u_2} (f : A → B) [Nonempty A] : Function.Injective f ↔ Function.HasLeftInverse f

theorem mathlib_inj_iff_has_left_inv2 {A : Sort u_1} {B : Sort u_2} (f : A → B) (hne : Nonempty A) : Function.Injective f ↔ Function.HasLeftInverse f

theorem hasa_prop {A : Sort u_1} (h : ∃ (x : A), True) : Nonempty A

theorem g_surj_if_left_inv {A : Sort u_1} {B : Sort u_2} {g : B → A} (f : A → B) (h : Function.LeftInverse g f) : Function.Surjective g