internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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]
Proof 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}
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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)
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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}
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Example_6_2_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_2_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.extendPO_extends
Proof state before:
A : Type
R : BinRel A
b x y : A
⊢ R x y → extendPO R b x y
Tactic:
assume h1 : R x y
Proof state after:
A : Type
R : BinRel A
b x y : A
h1 : R x y
⊢ extendPO R b x y
Theorem: HTPI.extendPO_extends
Proof state before:
A : Type
R : BinRel A
b x y : A
h1 : R x y
⊢ extendPO R b x y
Tactic:
define
Proof state after:
A : Type
R : BinRel A
b x y : A
h1 : R x y
⊢ R x y ∨ R x b ∧ ¬R y b
Theorem: HTPI.extendPO_extends
Proof state before:
A : Type
R : BinRel A
b x y : A
h1 : R x y
⊢ R x y ∨ R x b ∧ ¬R y b
Tactic:
show R x y ∨ R x b ∧ ¬R y b from Or.inl h1
Proof state after:
no goals
Theorem: HTPI.extendPO_all_comp
Proof 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
Proof 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
Theorem: HTPI.extendPO_all_comp
Proof 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
Proof 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
Theorem: HTPI.extendPO_all_comp
Proof 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
Proof 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
Theorem: HTPI.extendPO_all_comp
Proof 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
Proof 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
Theorem: HTPI.extendPO_all_comp
Proof 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
Proof 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
Theorem: HTPI.extendPO_all_comp
Proof 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
Proof 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
Theorem: HTPI.extendPO_all_comp
Proof 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
Proof 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
Theorem: HTPI.extendPO_all_comp
Proof 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
Proof state after:
no goals
Theorem: HTPI.Exercise_6_2_2
Proof state before:
A : Type
R : BinRel A
h : partial_order R
⊢ ∀ (n : ℕ) (B : Set A),
    numElts B n → ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Tactic:
by_induc
Proof state after:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
⊢ ∀ (B : Set A), numElts B 0 → ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x

case Induction_Step
A : Type
R : BinRel A
h : partial_order R
⊢ ∀ (n : ℕ),
    (∀ (B : Set A),
        numElts B n → ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x) →
      ∀ (B : Set A),
        numElts B (n + 1) → ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
⊢ ∀ (B : Set A), numElts B 0 → ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Tactic:
fix B : Set A
Proof state after:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
⊢ numElts B 0 → ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
⊢ numElts B 0 → ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Tactic:
assume h2 : numElts B 0
Proof state after:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : numElts B 0
⊢ ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : numElts B 0
⊢ ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Tactic:
rewrite [zero_elts_iff_empty] at h2
Proof state after:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : empty B
⊢ ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : empty B
⊢ ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Tactic:
define at h2
Proof state after:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
⊢ ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
⊢ ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Tactic:
apply Exists.intro R
Proof state after:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
⊢ partial_order R ∧ (∀ (x y : A), R x y → R x y) ∧ ∀ x ∈ B, ∀ (y : A), R x y ∨ R y x
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
⊢ partial_order R ∧ (∀ (x y : A), R x y → R x y) ∧ ∀ x ∈ B, ∀ (y : A), R x y ∨ R y x
Tactic:
apply And.intro h
Proof state after:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
⊢ (∀ (x y : A), R x y → R x y) ∧ ∀ x ∈ B, ∀ (y : A), R x y ∨ R y x
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case Base_Case
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
⊢ (∀ (x y : A), R x y → R x y) ∧ ∀ x ∈ B, ∀ (y : A), R x y ∨ R y x
Tactic:
apply And.intro
Proof state after:
case Base_Case.left
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
⊢ ∀ (x y : A), R x y → R x y

case Base_Case.right
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
⊢ ∀ x ∈ B, ∀ (y : A), R x y ∨ R y x
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case Base_Case.left
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
⊢ ∀ (x y : A), R x y → R x y
Tactic:
fix x : A
Proof state after:
case Base_Case.left
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
x : A
⊢ ∀ (y : A), R x y → R x y
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case Base_Case.left
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
x : A
⊢ ∀ (y : A), R x y → R x y
Tactic:
fix y : A
Proof state after:
case Base_Case.left
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
x y : A
⊢ R x y → R x y
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case Base_Case.left
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
x y : A
⊢ R x y → R x y
Tactic:
assume h3 : R x y
Proof state after:
case Base_Case.left
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
x y : A
h3 : R x y
⊢ R x y
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case Base_Case.left
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
x y : A
h3 : R x y
⊢ R x y
Tactic:
show R x y from h3
Proof state after:
no goals
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case Base_Case.right
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
⊢ ∀ x ∈ B, ∀ (y : A), R x y ∨ R y x
Tactic:
fix x : A
Proof state after:
case Base_Case.right
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
x : A
⊢ x ∈ B → ∀ (y : A), R x y ∨ R y x
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case Base_Case.right
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
x : A
⊢ x ∈ B → ∀ (y : A), R x y ∨ R y x
Tactic:
assume h3 : x ∈ B
Proof state after:
case Base_Case.right
A : Type
R : BinRel A
h : partial_order R
B : Set A
h2 : ¬∃ x, x ∈ B
x : A
h3 : x ∈ B
⊢ ∀ (y : A), R x y ∨ R y x