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

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

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

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hxz : (x == z) = true
hyz : (y == z) = 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
hxz : (x == z) = true
hyz : (y == z) = false
⊢ true = false
Tactic:
rw [BEq.trans (BEq.symm hxy) hxz] at hyz
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hxz : (x == z) = true
hyz : true = false
⊢ true = false

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hxz : (x == z) = true
hyz : 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
hxz : (x == z) = false
hyz : (y == z) = true
⊢ false = true
Tactic:
rw [BEq.trans hxy hyz] at hxz
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hxz : true = false
hyz : (y == z) = true
⊢ false = true

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hxz : true = false
hyz : (y == z) = 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
hxz : (x == z) = false
hyz : (y == z) = false
⊢ false = false
Tactic:
rfl
State after:
no goals