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

State before:
A : Type
R : BinRel A
b : A
h : partial_order R
⊢ ∀ (x : A), extendPO R b b x ∨ extendPO R b x b
Tactic:
have Rref : reflexive R := h.left
State after:
A : Type
R : BinRel A
b : A
h : partial_order R
Rref : reflexive R
⊢ ∀ (x : A), extendPO R b b x ∨ extendPO R b x b

State before:
A : Type
R : BinRel A
b : A
h : partial_order R
Rref : reflexive R
⊢ ∀ (x : A), extendPO R b b x ∨ extendPO R b x b
Tactic:
fix x : A
State after:
A : Type
R : BinRel A
b : A
h : partial_order R
Rref : reflexive R
x : A
⊢ extendPO R b b x ∨ extendPO R b x b

State before:
A : Type
R : BinRel A
b : A
h : partial_order R
Rref : reflexive R
x : A
⊢ extendPO R b b x ∨ extendPO R b x b
Tactic:
or_left with h1
State after:
A : Type
R : BinRel A
b : A
h : partial_order R
Rref : reflexive R
x : A
h1 : ¬extendPO R b x b
⊢ extendPO R b b x

State before:
A : Type
R : BinRel A
b : A
h : partial_order R
Rref : reflexive R
x : A
h1 : ¬extendPO R b x b
⊢ extendPO R b b x
Tactic:
define at h1
State after:
A : Type
R : BinRel A
b : A
h : partial_order R
Rref : reflexive R
x : A
h1 : ¬(R x b ∨ R x b ∧ ¬R b b)
⊢ extendPO R b b x

State before:
A : Type
R : BinRel A
b : A
h : partial_order R
Rref : reflexive R
x : A
h1 : ¬(R x b ∨ R x b ∧ ¬R b b)
⊢ extendPO R b b x
Tactic:
demorgan at h1
State after:
A : Type
R : BinRel A
b : A
h : partial_order R
Rref : reflexive R
x : A
h1 : ¬R x b ∧ ¬(R x b ∧ ¬R b b)
⊢ extendPO R b b x

State before:
A : Type
R : BinRel A
b : A
h : partial_order R
Rref : reflexive R
x : A
h1 : ¬R x b ∧ ¬(R x b ∧ ¬R b b)
⊢ extendPO R b b x
Tactic:
define
State after:
A : Type
R : BinRel A
b : A
h : partial_order R
Rref : reflexive R
x : A
h1 : ¬R x b ∧ ¬(R x b ∧ ¬R b b)
⊢ R b x ∨ R b b ∧ ¬R x b

State before:
A : Type
R : BinRel A
b : A
h : partial_order R
Rref : reflexive R
x : A
h1 : ¬R x b ∧ ¬(R x b ∧ ¬R b b)
⊢ R b x ∨ R b b ∧ ¬R x b
Tactic:
apply Or.inr
State after:
case h
A : Type
R : BinRel A
b : A
h : partial_order R
Rref : reflexive R
x : A
h1 : ¬R x b ∧ ¬(R x b ∧ ¬R b b)
⊢ R b b ∧ ¬R x b

State before:
case h
A : Type
R : BinRel A
b : A
h : partial_order R
Rref : reflexive R
x : A
h1 : ¬R x b ∧ ¬(R x b ∧ ¬R b b)
⊢ R b b ∧ ¬R x b
Tactic:
show R b b ∧ ¬R x b from And.intro (Rref b) h1.left
State after:
no goals