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

State before:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : minimalElt R c (B \ {b})
h4 : R b c
⊢ minimalElt R b B
Tactic:
define at h3
State after:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
⊢ minimalElt R b B

State before:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
⊢ minimalElt R b B
Tactic:
define
State after:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
⊢ b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b

State before:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
⊢ b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
Tactic:
apply And.intro h2
State after:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
⊢ ¬∃ x ∈ B, R x b ∧ x ≠ b

State before:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
⊢ ¬∃ x ∈ B, R x b ∧ x ≠ b
Tactic:
contradict h3.right with h5
State after:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
⊢ ∃ x ∈ B \ {b}, R x c ∧ x ≠ c

State before:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
⊢ ∃ x ∈ B \ {b}, R x c ∧ x ≠ c
Tactic:
obtain (x : A) (h6 : x ∈ B ∧ R x b ∧ x ≠ b) from h5
State after:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ ∃ x ∈ B \ {b}, R x c ∧ x ≠ c

State before:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ ∃ x ∈ B \ {b}, R x c ∧ x ≠ c
Tactic:
apply Exists.intro x
State after:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ x ∈ B \ {b} ∧ R x c ∧ x ≠ c

State before:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ x ∈ B \ {b} ∧ R x c ∧ x ≠ c
Tactic:
apply And.intro
State after:
case left
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ x ∈ B \ {b}

case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ R x c ∧ x ≠ c

State before:
case left
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ x ∈ B \ {b}
Tactic:
show x ∈ B \ {b} from And.intro h6.left h6.right.right
State after:
no goals

State before:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ R x c ∧ x ≠ c
Tactic:
have Rtrans : transitive R := h1.right.left
State after:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
Rtrans : transitive R
⊢ R x c ∧ x ≠ c

State before:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
Rtrans : transitive R
⊢ R x c ∧ x ≠ c
Tactic:
have h7 : R x c := Rtrans x b c h6.right.left h4
State after:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
Rtrans : transitive R
h7 : R x c
⊢ R x c ∧ x ≠ c

State before:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
Rtrans : transitive R
h7 : R x c
⊢ R x c ∧ x ≠ c
Tactic:
apply And.intro h7
State after:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
Rtrans : transitive R
h7 : R x c
⊢ x ≠ c

State before:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
Rtrans : transitive R
h7 : R x c
⊢ x ≠ c
Tactic:
by_contra h8
State after:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
Rtrans : transitive R
h7 : R x c
h8 : x = c
⊢ False

State before:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
Rtrans : transitive R
h7 : R x c
h8 : x = c
⊢ False
Tactic:
rewrite [h8] at h6
State after:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : c ∈ B ∧ R c b ∧ c ≠ b
Rtrans : transitive R
h7 : R x c
h8 : x = c
⊢ False

State before:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : c ∈ B ∧ R c b ∧ c ≠ b
Rtrans : transitive R
h7 : R x c
h8 : x = c
⊢ False
Tactic:
have Rantisymm : antisymmetric R := h1.right.right
State after:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : c ∈ B ∧ R c b ∧ c ≠ b
Rtrans : transitive R
h7 : R x c
h8 : x = c
Rantisymm : antisymmetric R
⊢ False

State before:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : c ∈ B ∧ R c b ∧ c ≠ b
Rtrans : transitive R
h7 : R x c
h8 : x = c
Rantisymm : antisymmetric R
⊢ False
Tactic:
have h9 : c = b := Rantisymm c b h6.right.left h4
State after:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : c ∈ B ∧ R c b ∧ c ≠ b
Rtrans : transitive R
h7 : R x c
h8 : x = c
Rantisymm : antisymmetric R
h9 : c = b
⊢ False

State before:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : c ∈ B ∧ R c b ∧ c ≠ b
Rtrans : transitive R
h7 : R x c
h8 : x = c
Rantisymm : antisymmetric R
h9 : c = b
⊢ False
Tactic:
show False from h6.right.right h9
State after:
no goals