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

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
⊢ (x != y) = true → ∀ (z : α), (x != z) = true ∨ (z != y) = true
Tactic:
unfold bne
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
⊢ (!x == y) = true → ∀ (z : α), (!x == z) = true ∨ (!z == y) = true

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

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

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
hxz : (x == z) = true
hyz : (z == y) = true
⊢ (!true) = true ∨ (!true) = true
Tactic:
rw [BEq.subst_right hyz] at hxz
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
hxz : (x == y) = true
hyz : (z == y) = true
⊢ (!true) = true ∨ (!true) = true

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
hxz : (x == y) = true
hyz : (z == y) = true
⊢ (!true) = true ∨ (!true) = true
Tactic:
rw [hxz] at hxy
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!true) = true
z : α
hxz : (x == y) = true
hyz : (z == y) = true
⊢ (!true) = true ∨ (!true) = true

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!true) = true
z : α
hxz : (x == y) = true
hyz : (z == y) = true
⊢ (!true) = true ∨ (!true) = true
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
x✝ : Bool
hxz : (x == z) = false
hyz : (z == y) = x✝
⊢ (!false) = true ∨ (!x✝) = true
Tactic:
left
State after:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
x✝ : Bool
hxz : (x == z) = false
hyz : (z == y) = x✝
⊢ (!false) = true

State before:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
x✝ : Bool
hxz : (x == z) = false
hyz : (z == y) = x✝
⊢ (!false) = true
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
x✝ : Bool
hxz : (x == z) = x✝
hyz : (z == y) = false
⊢ (!x✝) = true ∨ (!false) = true
Tactic:
right
State after:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
x✝ : Bool
hxz : (x == z) = x✝
hyz : (z == y) = false
⊢ (!false) = true

State before:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
x✝ : Bool
hxz : (x == z) = x✝
hyz : (z == y) = false
⊢ (!false) = true
Tactic:
rfl
State after:
no goals