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