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

State before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R
h2 : smallestElt R b B
⊢ minimalElt R b B ∧ ∀ (c : A), minimalElt R c B → b = c
Tactic:
define at h1
State after:
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : smallestElt R b B
⊢ minimalElt R b B ∧ ∀ (c : A), minimalElt R c B → b = c

State before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : smallestElt R b B
⊢ minimalElt R b B ∧ ∀ (c : A), minimalElt R c B → b = c
Tactic:
define at h2
State after:
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
⊢ minimalElt R b B ∧ ∀ (c : A), minimalElt R c B → b = c

State before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
⊢ minimalElt R b B ∧ ∀ (c : A), minimalElt R c B → b = c
Tactic:
apply And.intro
State after:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
⊢ minimalElt R b B

case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
⊢ ∀ (c : A), minimalElt R c B → b = c

State before:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
⊢ minimalElt R b B
Tactic:
define
State after:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
⊢ b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b

State before:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
⊢ b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
Tactic:
apply And.intro h2.left
State after:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
⊢ ¬∃ x ∈ B, R x b ∧ x ≠ b

State before:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
⊢ ¬∃ x ∈ B, R x b ∧ x ≠ b
Tactic:
quant_neg
State after:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
⊢ ∀ (x : A), ¬(x ∈ B ∧ R x b ∧ x ≠ b)

State before:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
⊢ ∀ (x : A), ¬(x ∈ B ∧ R x b ∧ x ≠ b)
Tactic:
fix x : A
State after:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
⊢ ¬(x ∈ B ∧ R x b ∧ x ≠ b)

State before:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
⊢ ¬(x ∈ B ∧ R x b ∧ x ≠ b)
Tactic:
demorgan
State after:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
⊢ x ∉ B ∨ ¬(R x b ∧ x ≠ b)

State before:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
⊢ x ∉ B ∨ ¬(R x b ∧ x ≠ b)
Tactic:
or_right with h3
State after:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
⊢ ¬(R x b ∧ x ≠ b)

State before:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
⊢ ¬(R x b ∧ x ≠ b)
Tactic:
demorgan
State after:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
⊢ ¬R x b ∨ x = b

State before:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
⊢ ¬R x b ∨ x = b
Tactic:
or_right with h4
State after:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
h4 : R x b
⊢ x = b

State before:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
h4 : R x b
⊢ x = b
Tactic:
have h5 : R b x := h2.right x h3
State after:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
h4 : R x b
h5 : R b x
⊢ x = b

State before:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
h4 : R x b
h5 : R b x
⊢ x = b
Tactic:
have h6 : antisymmetric R := h1.right.right
State after:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
h4 : R x b
h5 : R b x
h6 : antisymmetric R
⊢ x = b

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

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

State before:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
⊢ ∀ (c : A), minimalElt R c B → b = c
Tactic:
fix c : A
State after:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
⊢ minimalElt R c B → b = c

State before:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
⊢ minimalElt R c B → b = c
Tactic:
assume h3 : minimalElt R c B
State after:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
h3 : minimalElt R c B
⊢ b = c

State before:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
h3 : minimalElt R c B
⊢ b = c
Tactic:
define at h3
State after:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
h3 : c ∈ B ∧ ¬∃ x ∈ B, R x c ∧ x ≠ c
⊢ b = c

State before:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
h3 : c ∈ B ∧ ¬∃ x ∈ B, R x c ∧ x ≠ c
⊢ b = c
Tactic:
contradict h3.right with h4
State after:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
h3 : c ∈ B ∧ ¬∃ x ∈ B, R x c ∧ x ≠ c
h4 : ¬b = c
⊢ ∃ x ∈ B, R x c ∧ x ≠ c

State before:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
h3 : c ∈ B ∧ ¬∃ x ∈ B, R x c ∧ x ≠ c
h4 : ¬b = c
⊢ ∃ x ∈ B, R x c ∧ x ≠ c
Tactic:
have h5 : R b c := h2.right c h3.left
State after:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
h3 : c ∈ B ∧ ¬∃ x ∈ B, R x c ∧ x ≠ c
h4 : ¬b = c
h5 : R b c
⊢ ∃ x ∈ B, R x c ∧ x ≠ c

State before:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
h3 : c ∈ B ∧ ¬∃ x ∈ B, R x c ∧ x ≠ c
h4 : ¬b = c
h5 : R b c
⊢ ∃ x ∈ B, R x c ∧ x ≠ c
Tactic:
show ∃ (x : A), x ∈ B ∧ R x c ∧ x ≠ c from
  Exists.intro b (And.intro h2.left (And.intro h5 h4))
State after:
no goals