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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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)
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

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
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

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
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

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}
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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)
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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
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

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)
State after:
no goals

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
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

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
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

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
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

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]
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

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
State after:
no goals

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
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

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
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

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
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

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
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

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)
State after:
no goals

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)
State after:
no goals