class PartialEquivBEq (α : Type u_1) [BEq α] : Prop

PartialEquivBEq α says that the BEq implementation is a partial equivalence relation, that is:

• it is symmetric: a == b → b == a
• it is transitive: a == b → b == c → a == c.

• symm {a b : α} : (a == b) = true → (b == a) = true

  Symmetry for BEq. If a == b then b == a.

• trans {a b c : α} : (a == b) = true → (b == c) = true → (a == c) = true

  Transitivity for BEq. If a == b and b == c then a == c.

instance instSymmEqBoolBeqTrueOfPartialEquivBEq {α : Type u_1} [BEq α] [PartialEquivBEq α] : Std.Symm fun (x1 x2 : α) => (x1 == x2) = true

class EquivBEq (α : Type u_1) [BEq α] extends PartialEquivBEq α, ReflBEq α : Prop

EquivBEq says that the BEq implementation is an equivalence relation.

• symm {a b : α} : (a == b) = true → (b == a) = true
• trans {a b c : α} : (a == b) = true → (b == c) = true → (a == c) = true
• rfl {a : α} : (a == a) = true

theorem BEq.symm {α : Type u_1} [BEq α] [Std.Symm fun (x1 x2 : α) => (x1 == x2) = true] {a b : α} : (a == b) = true → (b == a) = true

theorem BEq.comm {α : Type u_1} [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a)

theorem bne_eq {α : Type u_1} [BEq α] {a b : α} : (a != b) = !a == b

theorem bne_comm {α : Type u_1} [BEq α] [PartialEquivBEq α] {a b : α} : (a != b) = (b != a)

theorem BEq.symm_false {α : Type u_1} [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = false → (b == a) = false

theorem BEq.trans {α : Type u_1} [BEq α] [PartialEquivBEq α] {a b c : α} : (a == b) = true → (b == c) = true → (a == c) = true

theorem BEq.congr_left {α : Type u_1} [BEq α] [PartialEquivBEq α] {a b c : α} (h : (a == b) = true) : (a == c) = (b == c)

theorem BEq.congr_right {α : Type u_1} [BEq α] [PartialEquivBEq α] {a b c : α} (h : (b == c) = true) : (a == b) = (a == c)

theorem BEq.neq_of_neq_of_beq {α : Type u_1} [BEq α] [PartialEquivBEq α] {a b c : α} : (a == b) = false → (b == c) = true → (a == c) = false

theorem BEq.neq_of_beq_of_neq {α : Type u_1} [BEq α] [PartialEquivBEq α] {a b c : α} : (a == b) = true → (b == c) = false → (a == c) = false

@[instance 100]

instance instEquivBEqOfLawfulBEq {α : Type u_1} [BEq α] [LawfulBEq α] : EquivBEq α

theorem equivBEq_of_iff_apply_eq {α : Type u_1} {β : Sort u_2} [BEq α] (f : α → β) (hf : ∀ (a b : α), (a == b) = true ↔ f a = f b) : EquivBEq α