α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : (a == b) = false
h' : a = b
⊢ False
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : (a == b) = false
⊢ a ≠ b
intro h'
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : (a == a) = false
⊢ False
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : (a == b) = false
h' : a = b
⊢ False
subst h'
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : (a == a) = false
this : true = false
⊢ False
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : (a == a) = false
⊢ False
have : true = false := Eq.trans LawfulBEq.rfl.symm h
no goals
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : (a == a) = false
this : true = false
⊢ False
contradiction