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

State before:
A : Type
R : BinRel A
h : partial_order R
⊢ ∀ n ≥ 1, ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
Tactic:
by_induc
State after:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
⊢ ∀ (B : Set A), numElts B 1 → ∃ x, minimalElt R x B

case Induction_Step
A : Type
R : BinRel A
h : partial_order R
⊢ ∀ n ≥ 1,
    (∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B) → ∀ (B : Set A), numElts B (n + 1) → ∃ x, minimalElt R x B

State before:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
⊢ ∀ (B : Set A), numElts B 1 → ∃ x, minimalElt R x B
Tactic:
fix B : Set A
State after:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
⊢ numElts B 1 → ∃ x, minimalElt R x B

State before:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
⊢ numElts B 1 → ∃ x, minimalElt R x B
Tactic:
assume h2 : numElts B 1
State after:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : numElts B 1
⊢ ∃ x, minimalElt R x B

State before:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : numElts B 1
⊢ ∃ x, minimalElt R x B
Tactic:
rewrite [one_elt_iff_singleton] at h2
State after:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
⊢ ∃ x, minimalElt R x B

State before:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
⊢ ∃ x, minimalElt R x B
Tactic:
obtain (b : A) (h3 : B = {b}) from h2
State after:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
⊢ ∃ x, minimalElt R x B

State before:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
⊢ ∃ x, minimalElt R x B
Tactic:
apply Exists.intro b
State after:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
⊢ minimalElt R b B

State before:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
⊢ minimalElt R b B
Tactic:
define
State after:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
⊢ b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b

State before:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
⊢ b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
Tactic:
apply And.intro
State after:
case Base_Case.left
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
⊢ b ∈ B

case Base_Case.right
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
⊢ ¬∃ x ∈ B, R x b ∧ x ≠ b

State before:
case Base_Case.left
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
⊢ b ∈ B
Tactic:
rewrite [h3]
State after:
case Base_Case.left
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
⊢ b ∈ {b}

State before:
case Base_Case.left
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
⊢ b ∈ {b}
Tactic:
define
State after:
case Base_Case.left
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
⊢ b = b

State before:
case Base_Case.left
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
⊢ b = b
Tactic:
rfl
State after:
no goals

State before:
case Base_Case.right
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
⊢ ¬∃ x ∈ B, R x b ∧ x ≠ b
Tactic:
by_contra h4
State after:
case Base_Case.right
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
h4 : ∃ x ∈ B, R x b ∧ x ≠ b
⊢ False

State before:
case Base_Case.right
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
h4 : ∃ x ∈ B, R x b ∧ x ≠ b
⊢ False
Tactic:
obtain (x : A) (h5 : x ∈ B ∧ R x b ∧ x ≠ b) from h4
State after:
case Base_Case.right
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
h4 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h5 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ False

State before:
case Base_Case.right
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
h4 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h5 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ False
Tactic:
have h6 : x ∈ B := h5.left
State after:
case Base_Case.right
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
h4 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h5 : x ∈ B ∧ R x b ∧ x ≠ b
h6 : x ∈ B
⊢ False

State before:
case Base_Case.right
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
h4 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h5 : x ∈ B ∧ R x b ∧ x ≠ b
h6 : x ∈ B
⊢ False
Tactic:
rewrite [h3] at h6
State after:
case Base_Case.right
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
h4 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h5 : x ∈ B ∧ R x b ∧ x ≠ b
h6 : x ∈ {b}
⊢ False

State before:
case Base_Case.right
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
h4 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h5 : x ∈ B ∧ R x b ∧ x ≠ b
h6 : x ∈ {b}
⊢ False
Tactic:
define at h6
State after:
case Base_Case.right
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
h4 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h5 : x ∈ B ∧ R x b ∧ x ≠ b
h6 : x = b
⊢ False

State before:
case Base_Case.right
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ∃ x, B = {x}
b : A
h3 : B = {b}
h4 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h5 : x ∈ B ∧ R x b ∧ x ≠ b
h6 : x = b
⊢ False
Tactic:
show False from h5.right.right h6
State after:
no goals

State before:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
⊢ ∀ n ≥ 1,
    (∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B) → ∀ (B : Set A), numElts B (n + 1) → ∃ x, minimalElt R x B
Tactic:
fix n : Nat
State after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
⊢ n ≥ 1 →
    (∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B) → ∀ (B : Set A), numElts B (n + 1) → ∃ x, minimalElt R x B

State before:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
⊢ n ≥ 1 →
    (∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B) → ∀ (B : Set A), numElts B (n + 1) → ∃ x, minimalElt R x B
Tactic:
assume h2 : n ≥ 1
State after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
⊢ (∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B) → ∀ (B : Set A), numElts B (n + 1) → ∃ x, minimalElt R x B

State before:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
⊢ (∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B) → ∀ (B : Set A), numElts B (n + 1) → ∃ x, minimalElt R x B
Tactic:
assume ih : ∀ (B : Set A), numElts B n → ∃ (x : A), minimalElt R x B
State after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
⊢ ∀ (B : Set A), numElts B (n + 1) → ∃ x, minimalElt R x B

State before:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
⊢ ∀ (B : Set A), numElts B (n + 1) → ∃ x, minimalElt R x B
Tactic:
fix B : Set A
State after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
⊢ numElts B (n + 1) → ∃ x, minimalElt R x B

State before:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
⊢ numElts B (n + 1) → ∃ x, minimalElt R x B
Tactic:
assume h3 : numElts B (n + 1)
State after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
⊢ ∃ x, minimalElt R x B

State before:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
⊢ ∃ x, minimalElt R x B
Tactic:
have h4 : n + 1 > 0 := by linarith
State after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
⊢ ∃ x, minimalElt R x B

State before:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
⊢ ∃ x, minimalElt R x B
Tactic:
obtain (b : A) (h5 : b ∈ B) from nonempty_of_pos_numElts h3 h4
State after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
b : A
h5 : b ∈ B
⊢ ∃ x, minimalElt R x B

State before:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
b : A
h5 : b ∈ B
⊢ ∃ x, minimalElt R x B
Tactic:
set B' : Set A := B \ {b}
State after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
b : A
h5 : b ∈ B
B' : Set A := B \ {b}
⊢ ∃ x, minimalElt R x B

State before:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
b : A
h5 : b ∈ B
B' : Set A := B \ {b}
⊢ ∃ x, minimalElt R x B
Tactic:
have h6 : numElts B' n := remove_one_numElts h3 h5
State after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
b : A
h5 : b ∈ B
B' : Set A := B \ {b}
h6 : numElts B' n
⊢ ∃ x, minimalElt R x B

State before:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
b : A
h5 : b ∈ B
B' : Set A := B \ {b}
h6 : numElts B' n
⊢ ∃ x, minimalElt R x B
Tactic:
obtain (c : A) (h7 : minimalElt R c B') from ih B' h6
State after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
b : A
h5 : b ∈ B
B' : Set A := B \ {b}
h6 : numElts B' n
c : A
h7 : minimalElt R c B'
⊢ ∃ x, minimalElt R x B

State before:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
b : A
h5 : b ∈ B
B' : Set A := B \ {b}
h6 : numElts B' n
c : A
h7 : minimalElt R c B'
⊢ ∃ x, minimalElt R x B
Tactic:
by_cases h8 : R b c
State after:
case pos
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
b : A
h5 : b ∈ B
B' : Set A := B \ {b}
h6 : numElts B' n
c : A
h7 : minimalElt R c B'
h8 : R b c
⊢ ∃ x, minimalElt R x B

case neg
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
b : A
h5 : b ∈ B
B' : Set A := B \ {b}
h6 : numElts B' n
c : A
h7 : minimalElt R c B'
h8 : ¬R b c
⊢ ∃ x, minimalElt R x B

State before:
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
⊢ n + 1 > 0
Tactic:
linarith
State after:
no goals

State before:
case pos
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
b : A
h5 : b ∈ B
B' : Set A := B \ {b}
h6 : numElts B' n
c : A
h7 : minimalElt R c B'
h8 : R b c
⊢ ∃ x, minimalElt R x B
Tactic:
have h9 : minimalElt R b B := Lemma_6_2_1_1 h h5 h7 h8
State after:
case pos
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
b : A
h5 : b ∈ B
B' : Set A := B \ {b}
h6 : numElts B' n
c : A
h7 : minimalElt R c B'
h8 : R b c
h9 : minimalElt R b B
⊢ ∃ x, minimalElt R x B

State before:
case pos
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
b : A
h5 : b ∈ B
B' : Set A := B \ {b}
h6 : numElts B' n
c : A
h7 : minimalElt R c B'
h8 : R b c
h9 : minimalElt R b B
⊢ ∃ x, minimalElt R x B
Tactic:
show ∃ (x : A), minimalElt R x B from Exists.intro b h9
State after:
no goals

State before:
case neg
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
b : A
h5 : b ∈ B
B' : Set A := B \ {b}
h6 : numElts B' n
c : A
h7 : minimalElt R c B'
h8 : ¬R b c
⊢ ∃ x, minimalElt R x B
Tactic:
have h9 : minimalElt R c B := Lemma_6_2_1_2 h h5 h7 h8
State after:
case neg
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
b : A
h5 : b ∈ B
B' : Set A := B \ {b}
h6 : numElts B' n
c : A
h7 : minimalElt R c B'
h8 : ¬R b c
h9 : minimalElt R c B
⊢ ∃ x, minimalElt R x B

State before:
case neg
A : Type
R : BinRel A
h : partial_order R
n : ℕ
h2 : n ≥ 1
ih : ∀ (B : Set A), numElts B n → ∃ x, minimalElt R x B
B : Set A
h3 : numElts B (n + 1)
h4 : n + 1 > 0
b : A
h5 : b ∈ B
B' : Set A := B \ {b}
h6 : numElts B' n
c : A
h7 : minimalElt R c B'
h8 : ¬R b c
h9 : minimalElt R c B
⊢ ∃ x, minimalElt R x B
Tactic:
show ∃ (x : A), minimalElt R x B from Exists.intro c h9
State after:
no goals