Theorem: compareOfLE.le_trans (GMLInit/Data/OrdInstances.lean)

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
⊢ compareOfLE x y ≠ gt → compareOfLE y z ≠ gt → compareOfLE x z ≠ gt
Tactic:
unfold compareOfLE
State after:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt →
    (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt → (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt →
    (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt → (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt
Tactic:
intro cxy cyz
State after:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
⊢ (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
⊢ (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt
Tactic:
have : x ≤ y := by by_contradiction | assuming h => split at cxy <;> contradiction
State after:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this : x ≤ y
⊢ (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this : x ≤ y
⊢ (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt
Tactic:
have : y ≤ z := by by_contradiction | assuming h => split at cyz <;> contradiction
State after:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this✝ : x ≤ y
this : y ≤ z
⊢ (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this✝ : x ≤ y
this : y ≤ z
⊢ (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt
Tactic:
have : x ≤ z := by transitivity y <;> assumption
State after:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this✝¹ : x ≤ y
this✝ : y ≤ z
this : x ≤ z
⊢ (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this✝¹ : x ≤ y
this✝ : y ≤ z
this : x ≤ z
⊢ (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt
Tactic:
split <;> split <;> (intro; contradiction)
State after:
no goals

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
⊢ x ≤ y
Tactic:
by_contradiction | assuming h => split at cxy <;> contradiction
State after:
no goals

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
h : ¬x ≤ y
⊢ False
Tactic:
split at cxy <;> contradiction
State after:
no goals

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this : x ≤ y
⊢ y ≤ z
Tactic:
by_contradiction | assuming h => split at cyz <;> contradiction
State after:
no goals

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this : x ≤ y
h : ¬y ≤ z
⊢ False
Tactic:
split at cyz <;> contradiction
State after:
no goals

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this✝ : x ≤ y
this : y ≤ z
⊢ x ≤ z
Tactic:
transitivity y <;> assumption
State after:
no goals

State before:
case isFalse.isFalse
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this✝¹ : x ≤ y
this✝ : y ≤ z
this : x ≤ z
h✝¹ : ¬x ≤ z
h✝ : ¬z ≤ x
⊢ lt ≠ gt
Tactic:
intro
State after:
case isFalse.isFalse
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this✝¹ : x ≤ y
this✝ : y ≤ z
this : x ≤ z
h✝¹ : ¬x ≤ z
h✝ : ¬z ≤ x
a✝ : lt = gt
⊢ False

State before:
case isFalse.isFalse
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this✝¹ : x ≤ y
this✝ : y ≤ z
this : x ≤ z
h✝¹ : ¬x ≤ z
h✝ : ¬z ≤ x
a✝ : lt = gt
⊢ False
Tactic:
contradiction
State after:
no goals