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

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
⊢ x ≠ y → (x != y) = true
Tactic:
intro h
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
⊢ (x != y) = true

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
⊢ (x != y) = true
Tactic:
rw [bne, Bool.not_eq_true']
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
⊢ (x == y) = false

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
⊢ (x == y) = false
Tactic:
match hb : x == y with
| true => absurd h; exact BEq.eq_of_beq hb
| false => rfl
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
hb : (x == y) = true
⊢ true = false
Tactic:
absurd h
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
hb : (x == y) = true
⊢ x = y

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
hb : (x == y) = true
⊢ x = y
Tactic:
exact BEq.eq_of_beq hb
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
hb : (x == y) = false
⊢ false = false
Tactic:
rfl
State after:
no goals