Theorem: BEq.ne_of_bne (GMLInit/Data/BEq.lean)

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : EquivBEq α
x y : α
⊢ (x != y) = true → x ≠ y
Tactic:
intro | h, rfl => rw [bne, BEq.refl] at h; contradiction
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : EquivBEq α
x y : α
x✝¹ : (x != y) = true
x✝ : x = y
h : (x != x) = true
⊢ False
Tactic:
rw [bne, BEq.refl] at h
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : EquivBEq α
x y : α
x✝¹ : (x != y) = true
x✝ : x = y
h : (!true) = true
⊢ False

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : EquivBEq α
x y : α
x✝¹ : (x != y) = true
x✝ : x = y
h : (!true) = true
⊢ False
Tactic:
contradiction
State after:
no goals