Theorem: HTPI.Theorem_4_4_6_3 (HTPILib/Chap4.lean)

State before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : total_order R
h2 : minimalElt R b B
⊢ smallestElt R b B
Tactic:
define at h1
State after:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : minimalElt R b B
⊢ smallestElt R b B

State before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : minimalElt R b B
⊢ smallestElt R b B
Tactic:
define at h2
State after:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
⊢ smallestElt R b B

State before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
⊢ smallestElt R b B
Tactic:
define
State after:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
⊢ b ∈ B ∧ ∀ x ∈ B, R b x

State before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
⊢ b ∈ B ∧ ∀ x ∈ B, R b x
Tactic:
apply And.intro h2.left
State after:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
⊢ ∀ x ∈ B, R b x

State before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
⊢ ∀ x ∈ B, R b x
Tactic:
fix x : A
State after:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
⊢ x ∈ B → R b x

State before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
⊢ x ∈ B → R b x
Tactic:
assume h3 : x ∈ B
State after:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
⊢ R b x

State before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
⊢ R b x
Tactic:
by_cases h4 : x = b
State after:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
⊢ R b x

case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
⊢ R b x

State before:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
⊢ R b x
Tactic:
rewrite [h4]
State after:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
⊢ R b b

State before:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
⊢ R b b
Tactic:
have h5 : partial_order R := h1.left
State after:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
h5 : partial_order R
⊢ R b b

State before:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
h5 : partial_order R
⊢ R b b
Tactic:
define at h5
State after:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
h5 : reflexive R ∧ transitive R ∧ antisymmetric R
⊢ R b b

State before:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
h5 : reflexive R ∧ transitive R ∧ antisymmetric R
⊢ R b b
Tactic:
have h6 : reflexive R := h5.left
State after:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
h5 : reflexive R ∧ transitive R ∧ antisymmetric R
h6 : reflexive R
⊢ R b b

State before:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
h5 : reflexive R ∧ transitive R ∧ antisymmetric R
h6 : reflexive R
⊢ R b b
Tactic:
define at h6
State after:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
h5 : reflexive R ∧ transitive R ∧ antisymmetric R
h6 : ∀ (x : A), R x x
⊢ R b b

State before:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
h5 : reflexive R ∧ transitive R ∧ antisymmetric R
h6 : ∀ (x : A), R x x
⊢ R b b
Tactic:
show R b b from h6 b
State after:
no goals

State before:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
⊢ R b x
Tactic:
have h5 : ∀ (x y : A), R x y ∨ R y x := h1.right
State after:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
⊢ R b x

State before:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
⊢ R b x
Tactic:
have h6 : R x b ∨ R b x := h5 x b
State after:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h6 : R x b ∨ R b x
⊢ R b x

State before:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h6 : R x b ∨ R b x
⊢ R b x
Tactic:
have h7 : ¬R x b := by
  contradict h2.right with h8
  show ∃ (x : A), x ∈ B ∧ R x b ∧ x ≠ b from
    Exists.intro x (And.intro h3 (And.intro h8 h4))
  done
State after:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h6 : R x b ∨ R b x
h7 : ¬R x b
⊢ R b x

State before:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h6 : R x b ∨ R b x
h7 : ¬R x b
⊢ R b x
Tactic:
disj_syll h6 h7
State after:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h7 : ¬R x b
h6 : R b x
⊢ R b x

State before:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h7 : ¬R x b
h6 : R b x
⊢ R b x
Tactic:
show R b x from h6
State after:
no goals

State before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h6 : R x b ∨ R b x
⊢ ¬R x b
Tactic:
contradict h2.right with h8
State after:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h6 : R x b ∨ R b x
h8 : R x b
⊢ ∃ x ∈ B, R x b ∧ x ≠ b

State before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h6 : R x b ∨ R b x
h8 : R x b
⊢ ∃ x ∈ B, R x b ∧ x ≠ b
Tactic:
show ∃ (x : A), x ∈ B ∧ R x b ∧ x ≠ b from
  Exists.intro x (And.intro h3 (And.intro h8 h4))
State after:
no goals