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

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
⊢ (x == y) = true → (z == x) = (z == y)
Tactic:
intro hxy
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
⊢ (z == x) = (z == y)

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

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

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

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

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

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

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