Theorem: HTPI.extendPO_extends (HTPILib/Chap6.lean)

State before:
A : Type
R : BinRel A
b x y : A
⊢ R x y → extendPO R b x y
Tactic:
assume h1 : R x y
State after:
A : Type
R : BinRel A
b x y : A
h1 : R x y
⊢ extendPO R b x y

State before:
A : Type
R : BinRel A
b x y : A
h1 : R x y
⊢ extendPO R b x y
Tactic:
define
State after:
A : Type
R : BinRel A
b x y : A
h1 : R x y
⊢ R x y ∨ R x b ∧ ¬R y b

State before:
A : Type
R : BinRel A
b x y : A
h1 : R x y
⊢ R x y ∨ R x b ∧ ¬R y b
Tactic:
show R x y ∨ R x b ∧ ¬R y b from Or.inl h1
State after:
no goals