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

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
⊢ (x == y) = (y == x)
Tactic:
match hxy : x == y, hyx : y == x with
| true, true => rfl
| true, false => rw [BEq.symm hxy] at hyx; contradiction
| false, true => rw [BEq.symm hyx] at hxy; contradiction
| false, false => rfl
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (x == y) = true
hyx : (y == x) = true
⊢ true = true
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (x == y) = true
hyx : (y == x) = false
⊢ true = false
Tactic:
rw [BEq.symm hxy] at hyx
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (x == y) = true
hyx : true = false
⊢ true = false

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (x == y) = true
hyx : true = false
⊢ true = false
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (x == y) = false
hyx : (y == x) = true
⊢ false = true
Tactic:
rw [BEq.symm hyx] at hxy
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : true = false
hyx : (y == x) = true
⊢ false = true

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : true = false
hyx : (y == x) = true
⊢ false = true
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (x == y) = false
hyx : (y == x) = false
⊢ false = false
Tactic:
rfl
State after:
no goals