internlm/Lean-Github huggingface dataset:
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:
assume h8 : R x y
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
h8 : 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 y : A
h8 : R x y
⊢ T x y
Tactic:
have h9 : T' x y := T'extR x y h8
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
h8 : R x y
h9 : T' 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 y : A
h8 : R x y
h9 : T' x y
⊢ T x y
Tactic:
show T x y from (extendPO_extends T' b x y h9)
Proof state after:
no goals
Theorem: HTPI.Exercise_6_2_2
Proof state before:
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
Tactic:
fix x : A
Proof state after:
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 : A
⊢ x ∈ B → ∀ (y : A), T x y ∨ T y x
Theorem: HTPI.Exercise_6_2_2
Proof state before:
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 : A
⊢ x ∈ B → ∀ (y : A), T x y ∨ T y x
Tactic:
assume h8 : x ∈ B
Proof state after:
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 : A
h8 : x ∈ B
⊢ ∀ (y : A), T x y ∨ T y x
Theorem: HTPI.Exercise_6_2_2
Proof state before:
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 : A
h8 : x ∈ B
⊢ ∀ (y : A), T x y ∨ T y x
Tactic:
by_cases h9 : x = b
Proof state after:
case pos
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
h8 : x ∈ B
h9 : x = b
⊢ ∀ (y : A), T x y ∨ T y x

case neg
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
h8 : x ∈ B
h9 : ¬x = b
⊢ ∀ (y : A), T x y ∨ T y x
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case pos
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
h8 : x ∈ B
h9 : x = b
⊢ ∀ (y : A), T x y ∨ T y x
Tactic:
rewrite [h9]
Proof state after:
case pos
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
h8 : x ∈ B
h9 : x = b
⊢ ∀ (y : A), T b y ∨ T y b
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case pos
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
h8 : x ∈ B
h9 : x = b
⊢ ∀ (y : A), T b y ∨ T y b
Tactic:
show ∀ (y : A), T b y ∨ T y b from extendPO_all_comp T' b T'po
Proof state after:
no goals
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case neg
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
h8 : x ∈ B
h9 : ¬x = b
⊢ ∀ (y : A), T x y ∨ T y x
Tactic:
have h10 : x ∈ B' := And.intro h8 h9
Proof state after:
case neg
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
h8 : x ∈ B
h9 : ¬x = b
h10 : x ∈ B'
⊢ ∀ (y : A), T x y ∨ T y x
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case neg
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
h8 : x ∈ B
h9 : ¬x = b
h10 : x ∈ B'
⊢ ∀ (y : A), T x y ∨ T y x
Tactic:
fix y : A
Proof state after:
case neg
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
h8 : x ∈ B
h9 : ¬x = b
h10 : x ∈ B'
y : A
⊢ T x y ∨ T y x
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case neg
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
h8 : x ∈ B
h9 : ¬x = b
h10 : x ∈ B'
y : A
⊢ T x y ∨ T y x
Tactic:
have h11 : T' x y ∨ T' y x := T'compB' x h10 y
Proof state after:
case neg
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
h8 : x ∈ B
h9 : ¬x = b
h10 : x ∈ B'
y : A
h11 : T' x y ∨ T' y x
⊢ T x y ∨ T y x
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case neg
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
h8 : x ∈ B
h9 : ¬x = b
h10 : x ∈ B'
y : A
h11 : T' x y ∨ T' y x
⊢ T x y ∨ T y x
Tactic:
by_cases on h11
Proof state after:
case neg.Case_1
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
h8 : x ∈ B
h9 : ¬x = b
h10 : x ∈ B'
y : A
h11 : T' x y
⊢ T x y ∨ T y x

case neg.Case_2
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
h8 : x ∈ B
h9 : ¬x = b
h10 : x ∈ B'
y : A
h11 : T' y x
⊢ T x y ∨ T y x
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case neg.Case_1
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
h8 : x ∈ B
h9 : ¬x = b
h10 : x ∈ B'
y : A
h11 : T' x y
⊢ T x y ∨ T y x
Tactic:
show T x y ∨ T y x from
  Or.inl (extendPO_extends T' b x y h11)
Proof state after:
no goals
Theorem: HTPI.Exercise_6_2_2
Proof state before:
case neg.Case_2
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
h8 : x ∈ B
h9 : ¬x = b
h10 : x ∈ B'
y : A
h11 : T' y x
⊢ T x y ∨ T y x
Tactic:
show T x y ∨ T y x from
  Or.inr (extendPO_extends T' b y x h11)
Proof state after:
no goals
Theorem: HTPI.Example_6_3_1
Proof state before:
⊢ ∀ n ≥ 4, fact n > 2 ^ n
Tactic:
by_induc
Proof state after:
case Base_Case

⊢ fact 4 > 2 ^ 4

case Induction_Step

⊢ ∀ n ≥ 4, fact n > 2 ^ n → fact (n + 1) > 2 ^ (n + 1)
Theorem: HTPI.Example_6_3_1
Proof state before:
case Base_Case

⊢ fact 4 > 2 ^ 4
Tactic:
decide
Proof state after:
no goals
Theorem: HTPI.Example_6_3_1
Proof state before:
case Induction_Step

⊢ ∀ n ≥ 4, fact n > 2 ^ n → fact (n + 1) > 2 ^ (n + 1)
Tactic:
fix n : Nat
Proof state after:
case Induction_Step
n : ℕ
⊢ n ≥ 4 → fact n > 2 ^ n → fact (n + 1) > 2 ^ (n + 1)
Theorem: HTPI.Example_6_3_1
Proof state before:
case Induction_Step
n : ℕ
⊢ n ≥ 4 → fact n > 2 ^ n → fact (n + 1) > 2 ^ (n + 1)
Tactic:
assume h1 : n ≥ 4
Proof state after:
case Induction_Step
n : ℕ
h1 : n ≥ 4
⊢ fact n > 2 ^ n → fact (n + 1) > 2 ^ (n + 1)
Theorem: HTPI.Example_6_3_1
Proof state before:
case Induction_Step
n : ℕ
h1 : n ≥ 4
⊢ fact n > 2 ^ n → fact (n + 1) > 2 ^ (n + 1)
Tactic:
assume ih : fact n > 2 ^ n
Proof state after:
case Induction_Step
n : ℕ
h1 : n ≥ 4
ih : fact n > 2 ^ n
⊢ fact (n + 1) > 2 ^ (n + 1)
Theorem: HTPI.Example_6_3_1
Proof state before:
case Induction_Step
n : ℕ
h1 : n ≥ 4
ih : fact n > 2 ^ n
⊢ fact (n + 1) > 2 ^ (n + 1)
Tactic:
have h2 : n + 1 > 2 := by linarith
Proof state after:
case Induction_Step
n : ℕ
h1 : n ≥ 4
ih : fact n > 2 ^ n
h2 : n + 1 > 2
⊢ fact (n + 1) > 2 ^ (n + 1)
Theorem: HTPI.Example_6_3_1
Proof state before:
case Induction_Step
n : ℕ
h1 : n ≥ 4
ih : fact n > 2 ^ n
h2 : n + 1 > 2
⊢ fact (n + 1) > 2 ^ (n + 1)
Tactic:
show fact (n + 1) > 2 ^ (n + 1) from
  calc fact (n + 1)
    _ = (n + 1) * fact n := by rfl
    _ > (n + 1) * 2 ^ n := by rel [ih]
    _ > 2 * 2 ^ n := by rel [h2]
    _ = 2 ^ (n + 1) := by ring
Proof state after:
no goals
Theorem: HTPI.Example_6_3_1
Proof state before:
n : ℕ
h1 : n ≥ 4
ih : fact n > 2 ^ n
⊢ n + 1 > 2
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.Example_6_3_1
Proof state before:
n : ℕ
h1 : n ≥ 4
ih : fact n > 2 ^ n
h2 : n + 1 > 2
⊢ fact (n + 1) = (n + 1) * fact n
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Example_6_3_1
Proof state before:
n : ℕ
h1 : n ≥ 4
ih : fact n > 2 ^ n
h2 : n + 1 > 2
⊢ (n + 1) * fact n > (n + 1) * 2 ^ n
Tactic:
rel [ih]
Proof state after:
no goals
Theorem: HTPI.Example_6_3_1
Proof state before:
n : ℕ
h1 : n ≥ 4
ih : fact n > 2 ^ n
h2 : n + 1 > 2
⊢ (n + 1) * 2 ^ n > 2 * 2 ^ n
Tactic:
rel [h2]
Proof state after:
no goals
Theorem: HTPI.Example_6_3_1
Proof state before:
n : ℕ
h1 : n ≥ 4
ih : fact n > 2 ^ n
h2 : n + 1 > 2
⊢ 2 * 2 ^ n = 2 ^ (n + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Example_6_3_2_cheating
Proof state before:
⊢ ∀ (a : ℝ) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n
Tactic:
fix a : Real
Proof state after:
a : ℝ
⊢ ∀ (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n
Theorem: HTPI.Example_6_3_2_cheating
Proof state before:
a : ℝ
⊢ ∀ (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n
Tactic:
fix m : Nat
Proof state after:
a : ℝ
m : ℕ
⊢ ∀ (n : ℕ), a ^ (m + n) = a ^ m * a ^ n
Theorem: HTPI.Example_6_3_2_cheating
Proof state before:
a : ℝ
m : ℕ
⊢ ∀ (n : ℕ), a ^ (m + n) = a ^ m * a ^ n
Tactic:
fix n : Nat
Proof state after:
a : ℝ
m n : ℕ
⊢ a ^ (m + n) = a ^ m * a ^ n
Theorem: HTPI.Example_6_3_2_cheating
Proof state before:
a : ℝ
m n : ℕ
⊢ a ^ (m + n) = a ^ m * a ^ n
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Example_6_3_2
Proof state before:
⊢ ∀ (a : ℝ) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n
Tactic:
fix a : Real
Proof state after:
a : ℝ
⊢ ∀ (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n
Theorem: HTPI.Example_6_3_2
Proof state before:
a : ℝ
⊢ ∀ (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n
Tactic:
fix m : Nat
Proof state after:
a : ℝ
m : ℕ
⊢ ∀ (n : ℕ), a ^ (m + n) = a ^ m * a ^ n
Theorem: HTPI.Example_6_3_2
Proof state before:
a : ℝ
m : ℕ
⊢ ∀ (n : ℕ), a ^ (m + n) = a ^ m * a ^ n
Tactic:
by_induc
Proof state after:
case Base_Case
a : ℝ
m : ℕ
⊢ a ^ (m + 0) = a ^ m * a ^ 0

case Induction_Step
a : ℝ
m : ℕ
⊢ ∀ (n : ℕ), a ^ (m + n) = a ^ m * a ^ n → a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)
Theorem: HTPI.Example_6_3_2
Proof state before:
case Base_Case
a : ℝ
m : ℕ
⊢ a ^ (m + 0) = a ^ m * a ^ 0
Tactic:
show a ^ (m + 0) = a ^ m * a ^ 0 from
  calc a ^ (m + 0)
    _ = a ^ m := by rfl
    _ = a ^ m * 1 := (mul_one (a ^ m)).symm
    _ = a ^ m * a ^ 0 := by rfl
Proof state after:
no goals
Theorem: HTPI.Example_6_3_2
Proof state before:
a : ℝ
m : ℕ
⊢ a ^ (m + 0) = a ^ m
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Example_6_3_2
Proof state before:
a : ℝ
m : ℕ
⊢ a ^ m * 1 = a ^ m * a ^ 0
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Example_6_3_2
Proof state before:
case Induction_Step
a : ℝ
m : ℕ
⊢ ∀ (n : ℕ), a ^ (m + n) = a ^ m * a ^ n → a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)
Tactic:
fix n : Nat
Proof state after:
case Induction_Step
a : ℝ
m n : ℕ
⊢ a ^ (m + n) = a ^ m * a ^ n → a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)