rw [BEq.trans (BEq.symm hxy) hxz] at hyz
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hxz : (x == z) = true
hyz : (y == z) = false
⊢ true = false
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hxz : (x == z) = true
hyz : true = false
⊢ true = false