internlm/Lean-Github huggingface dataset:
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
h3 : x ∈ B
⊢ ∀ (y : A), R x y ∨ R y x
Tactic:
contradict h2
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
this : ¬∀ (y : A), R x y ∨ R y x
⊢ ∃ x, x ∈ B
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
h3 : x ∈ B
this : ¬∀ (y : A), R x y ∨ R y x
⊢ ∃ x, x ∈ B
Tactic:
show ∃ (x : A), x ∈ B from Exists.intro x h3
Proof state after:
no goals
Theorem: HTPI.Exercise_6_2_2
Proof state before:
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
Tactic:
fix n : Nat
Proof state after:
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 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
Tactic:
assume ih : ∀ (B : Set A), numElts B n → ∃ (T : BinRel A),
  partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧
  ∀ (x : A), x ∈ B → ∀ (y : A), T x y ∨ T y x
Proof state after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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 Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
Tactic:
fix B : Set A
Proof state after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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 Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
Tactic:
assume h2 : numElts B (n + 1)
Proof state after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : 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 Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : 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
Tactic:
have h3 : n + 1 > 0 := by linarith
Proof state after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 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 Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 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:
obtain (b : A) (h4 : b ∈ B) from nonempty_of_pos_numElts h2 h3
Proof state after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ 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 Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ 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:
set B' : Set A := B \ {b}
Proof state after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {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 Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {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:
have h5 : numElts B' n := remove_one_numElts h2 h4
Proof state after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : 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
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : 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:
have h6 : ∃ (T : BinRel A), partial_order T ∧
  (∀ (x y : A), R x y → T x y) ∧
  ∀ (x : A), x ∈ B' → ∀ (y : A), T x y ∨ T y x := ih B' h5
Proof state after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
⊢ ∃ 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 Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
⊢ ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Tactic:
obtain (T' : BinRel A)
  (h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧
  ∀ (x : A), x ∈ B' → ∀ (y : A), T' x y ∨ T' y x) from h6
Proof state after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
⊢ ∃ 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 Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
⊢ ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Tactic:
have T'po : partial_order T' := h7.left
Proof state after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
⊢ ∃ 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 Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
⊢ ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Tactic:
have T'extR : ∀ (x y : A), R x y → T' x y := h7.right.left
Proof state after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
T'extR : ∀ (x y : A), R x y → T' x y
⊢ ∃ 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 Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
T'extR : ∀ (x y : A), R x y → T' x y
⊢ ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Tactic:
have T'compB' : ∀ (x : A), x ∈ B' →
  ∀ (y : A), T' x y ∨ T' y x := h7.right.right
Proof state after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
T'extR : ∀ (x y : A), R x y → T' x y
T'compB' : ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
⊢ ∃ 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 Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
T'extR : ∀ (x y : A), R x y → T' x y
T'compB' : ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
⊢ ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Tactic:
set T : BinRel A := extendPO T' b
Proof state after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
T'extR : ∀ (x y : A), R x y → T' x y
T'compB' : ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T : BinRel A := extendPO T' 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 Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
T'extR : ∀ (x y : A), R x y → T' x y
T'compB' : ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T : BinRel A := extendPO T' 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 T
Proof state after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
T'extR : ∀ (x y : A), R x y → T' x y
T'compB' : ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T : BinRel A := extendPO T' b
⊢ 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 Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
T'extR : ∀ (x y : A), R x y → T' x y
T'compB' : ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T : BinRel A := extendPO T' b
⊢ partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Tactic:
apply And.intro (extendPO_is_po T' b T'po)
Proof state after:
case Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
T'extR : ∀ (x y : A), R x y → T' x y
T'compB' : ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T : BinRel A := extendPO T' b
⊢ (∀ (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 Induction_Step
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
T'extR : ∀ (x y : A), R x y → T' x y
T'compB' : ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T : BinRel A := extendPO T' b
⊢ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Tactic:
apply And.intro
Proof state after:
case Induction_Step.left
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
T'extR : ∀ (x y : A), R x y → T' x y
T'compB' : ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T : BinRel A := extendPO T' b
⊢ ∀ (x y : A), R x y → T x y

case Induction_Step.right
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
T'extR : ∀ (x y : A), R x y → T' x y
T'compB' : ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T : BinRel A := extendPO T' b
⊢ ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
Theorem: HTPI.Exercise_6_2_2
Proof state before:
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
⊢ n + 1 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case Induction_Step.left
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
T'extR : ∀ (x y : A), R x y → T' x y
T'compB' : ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T : BinRel A := extendPO T' b
⊢ ∀ (x y : A), R x y → T x y
Tactic:
fix x : A
Proof state after:
case Induction_Step.left
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
T'extR : ∀ (x y : A), R x y → T' x y
T'compB' : ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T : BinRel A := extendPO T' b
x : A
⊢ ∀ (y : A), R x y → T x y
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case Induction_Step.left
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
T'extR : ∀ (x y : A), R x y → T' x y
T'compB' : ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T : BinRel A := extendPO T' b
x : A
⊢ ∀ (y : A), R x y → T x y
Tactic:
fix y : A
Proof state after:
case Induction_Step.left
A : Type
R : BinRel A
h : partial_order R
n : ℕ
ih :
  ∀ (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
h2 : numElts B (n + 1)
h3 : n + 1 > 0
b : A
h4 : b ∈ B
B' : Set A := B \ {b}
h5 : numElts B' n
h6 : ∃ T, partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧ ∀ x ∈ B', ∀ (y : A), T x y ∨ T y x
T' : BinRel A
h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧ ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T'po : partial_order T'
T'extR : ∀ (x y : A), R x y → T' x y
T'compB' : ∀ x ∈ B', ∀ (y : A), T' x y ∨ T' y x
T : BinRel A := extendPO T' b
x y : A
⊢ R x y → T x y