internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Theorem_4_4_6_2
Proof state before:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
⊢ ¬(R x b ∧ x ≠ b)
Tactic:
demorgan
Proof state after:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
⊢ ¬R x b ∨ x = b
Theorem: HTPI.Theorem_4_4_6_2
Proof state before:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
⊢ ¬R x b ∨ x = b
Tactic:
or_right with h4
Proof state after:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
h4 : R x b
⊢ x = b
Theorem: HTPI.Theorem_4_4_6_2
Proof state before:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
h4 : R x b
⊢ x = b
Tactic:
have h5 : R b x := h2.right x h3
Proof state after:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
h4 : R x b
h5 : R b x
⊢ x = b
Theorem: HTPI.Theorem_4_4_6_2
Proof state before:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
h4 : R x b
h5 : R b x
⊢ x = b
Tactic:
have h6 : antisymmetric R := h1.right.right
Proof state after:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
h4 : R x b
h5 : R b x
h6 : antisymmetric R
⊢ x = b
Theorem: HTPI.Theorem_4_4_6_2
Proof state before:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
h4 : R x b
h5 : R b x
h6 : antisymmetric R
⊢ x = b
Tactic:
define at h6
Proof state after:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
h4 : R x b
h5 : R b x
h6 : ∀ (x y : A), R x y → R y x → x = y
⊢ x = b
Theorem: HTPI.Theorem_4_4_6_2
Proof state before:
case left
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
x : A
h3 : x ∈ B
h4 : R x b
h5 : R b x
h6 : ∀ (x y : A), R x y → R y x → x = y
⊢ x = b
Tactic:
show x = b from h6 x b h4 h5
Proof state after:
no goals
Theorem: HTPI.Theorem_4_4_6_2
Proof state before:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
⊢ ∀ (c : A), minimalElt R c B → b = c
Tactic:
fix c : A
Proof state after:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
⊢ minimalElt R c B → b = c
Theorem: HTPI.Theorem_4_4_6_2
Proof state before:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
⊢ minimalElt R c B → b = c
Tactic:
assume h3 : minimalElt R c B
Proof state after:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
h3 : minimalElt R c B
⊢ b = c
Theorem: HTPI.Theorem_4_4_6_2
Proof state before:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
h3 : minimalElt R c B
⊢ b = c
Tactic:
define at h3
Proof state after:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
h3 : c ∈ B ∧ ¬∃ x ∈ B, R x c ∧ x ≠ c
⊢ b = c
Theorem: HTPI.Theorem_4_4_6_2
Proof state before:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
h3 : c ∈ B ∧ ¬∃ x ∈ B, R x c ∧ x ≠ c
⊢ b = c
Tactic:
contradict h3.right with h4
Proof state after:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
h3 : c ∈ B ∧ ¬∃ x ∈ B, R x c ∧ x ≠ c
h4 : ¬b = c
⊢ ∃ x ∈ B, R x c ∧ x ≠ c
Theorem: HTPI.Theorem_4_4_6_2
Proof state before:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
h3 : c ∈ B ∧ ¬∃ x ∈ B, R x c ∧ x ≠ c
h4 : ¬b = c
⊢ ∃ x ∈ B, R x c ∧ x ≠ c
Tactic:
have h5 : R b c := h2.right c h3.left
Proof state after:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
h3 : c ∈ B ∧ ¬∃ x ∈ B, R x c ∧ x ≠ c
h4 : ¬b = c
h5 : R b c
⊢ ∃ x ∈ B, R x c ∧ x ≠ c
Theorem: HTPI.Theorem_4_4_6_2
Proof state before:
case right
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : b ∈ B ∧ ∀ x ∈ B, R b x
c : A
h3 : c ∈ B ∧ ¬∃ x ∈ B, R x c ∧ x ≠ c
h4 : ¬b = c
h5 : R b c
⊢ ∃ x ∈ B, R x c ∧ x ≠ c
Tactic:
show ∃ (x : A), x ∈ B ∧ R x c ∧ x ≠ c from
  Exists.intro b (And.intro h2.left (And.intro h5 h4))
Proof state after:
no goals
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : total_order R
h2 : minimalElt R b B
⊢ smallestElt R b B
Tactic:
define at h1
Proof state after:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : minimalElt R b B
⊢ smallestElt R b B
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : minimalElt R b B
⊢ smallestElt R b B
Tactic:
define at h2
Proof state after:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
⊢ smallestElt R b B
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
⊢ smallestElt R b B
Tactic:
define
Proof state after:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
⊢ b ∈ B ∧ ∀ x ∈ B, R b x
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
⊢ b ∈ B ∧ ∀ x ∈ B, R b x
Tactic:
apply And.intro h2.left
Proof state after:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
⊢ ∀ x ∈ B, R b x
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
⊢ ∀ x ∈ B, R b x
Tactic:
fix x : A
Proof state after:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
⊢ x ∈ B → R b x
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
⊢ x ∈ B → R b x
Tactic:
assume h3 : x ∈ B
Proof state after:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
⊢ R b x
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
⊢ R b x
Tactic:
by_cases h4 : x = b
Proof state after:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
⊢ R b x

case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
⊢ R b x
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
⊢ R b x
Tactic:
rewrite [h4]
Proof state after:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
⊢ R b b
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
⊢ R b b
Tactic:
have h5 : partial_order R := h1.left
Proof state after:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
h5 : partial_order R
⊢ R b b
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
h5 : partial_order R
⊢ R b b
Tactic:
define at h5
Proof state after:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
h5 : reflexive R ∧ transitive R ∧ antisymmetric R
⊢ R b b
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
h5 : reflexive R ∧ transitive R ∧ antisymmetric R
⊢ R b b
Tactic:
have h6 : reflexive R := h5.left
Proof state after:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
h5 : reflexive R ∧ transitive R ∧ antisymmetric R
h6 : reflexive R
⊢ R b b
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
h5 : reflexive R ∧ transitive R ∧ antisymmetric R
h6 : reflexive R
⊢ R b b
Tactic:
define at h6
Proof state after:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
h5 : reflexive R ∧ transitive R ∧ antisymmetric R
h6 : ∀ (x : A), R x x
⊢ R b b
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
case pos
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : x = b
h5 : reflexive R ∧ transitive R ∧ antisymmetric R
h6 : ∀ (x : A), R x x
⊢ R b b
Tactic:
show R b b from h6 b
Proof state after:
no goals
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
⊢ R b x
Tactic:
have h5 : ∀ (x y : A), R x y ∨ R y x := h1.right
Proof state after:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
⊢ R b x
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
⊢ R b x
Tactic:
have h6 : R x b ∨ R b x := h5 x b
Proof state after:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h6 : R x b ∨ R b x
⊢ R b x
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h6 : R x b ∨ R b x
⊢ R b x
Tactic:
have h7 : ¬R x b := by
  contradict h2.right with h8
  show ∃ (x : A), x ∈ B ∧ R x b ∧ x ≠ b from
    Exists.intro x (And.intro h3 (And.intro h8 h4))
  done
Proof state after:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h6 : R x b ∨ R b x
h7 : ¬R x b
⊢ R b x
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h6 : R x b ∨ R b x
h7 : ¬R x b
⊢ R b x
Tactic:
disj_syll h6 h7
Proof state after:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h7 : ¬R x b
h6 : R b x
⊢ R b x
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
case neg
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h7 : ¬R x b
h6 : R b x
⊢ R b x
Tactic:
show R b x from h6
Proof state after:
no goals
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h6 : R x b ∨ R b x
⊢ ¬R x b
Tactic:
contradict h2.right with h8
Proof state after:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h6 : R x b ∨ R b x
h8 : R x b
⊢ ∃ x ∈ B, R x b ∧ x ≠ b
Theorem: HTPI.Theorem_4_4_6_3
Proof state before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R ∧ ∀ (x y : A), R x y ∨ R y x
h2 : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
x : A
h3 : x ∈ B
h4 : ¬x = b
h5 : ∀ (x y : A), R x y ∨ R y x
h6 : R x b ∨ R b x
h8 : R x b
⊢ ∃ x ∈ B, R x b ∧ x ≠ b
Tactic:
show ∃ (x : A), x ∈ B ∧ R x b ∧ x ≠ b from
  Exists.intro x (And.intro h3 (And.intro h8 h4))
Proof state after:
no goals
Theorem: HTPI.Lemma_4_5_5_1
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
⊢ ∀ (x : A), x ∈ equivClass R x
Tactic:
fix x : A
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ x ∈ equivClass R x
Theorem: HTPI.Lemma_4_5_5_1
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ x ∈ equivClass R x
Tactic:
define
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ R x x
Theorem: HTPI.Lemma_4_5_5_1
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ R x x
Tactic:
define at h
Proof state after:
A : Type
R : BinRel A
h : reflexive R ∧ symmetric R ∧ transitive R
x : A
⊢ R x x
Theorem: HTPI.Lemma_4_5_5_1
Proof state before:
A : Type
R : BinRel A
h : reflexive R ∧ symmetric R ∧ transitive R
x : A
⊢ R x x
Tactic:
have Rref : reflexive R := h.left
Proof state after:
A : Type
R : BinRel A
h : reflexive R ∧ symmetric R ∧ transitive R
x : A
Rref : reflexive R
⊢ R x x
Theorem: HTPI.Lemma_4_5_5_1
Proof state before:
A : Type
R : BinRel A
h : reflexive R ∧ symmetric R ∧ transitive R
x : A
Rref : reflexive R
⊢ R x x
Tactic:
show R x x from Rref x
Proof state after:
no goals
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
⊢ ∀ (x y : A), y ∈ equivClass R x ↔ equivClass R y = equivClass R x
Tactic:
have Rsymm : symmetric R := h.right.left
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
⊢ ∀ (x y : A), y ∈ equivClass R x ↔ equivClass R y = equivClass R x
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
⊢ ∀ (x y : A), y ∈ equivClass R x ↔ equivClass R y = equivClass R x
Tactic:
have Rtrans : transitive R := h.right.right
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
⊢ ∀ (x y : A), y ∈ equivClass R x ↔ equivClass R y = equivClass R x
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
⊢ ∀ (x y : A), y ∈ equivClass R x ↔ equivClass R y = equivClass R x
Tactic:
fix x : A
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x : A
⊢ ∀ (y : A), y ∈ equivClass R x ↔ equivClass R y = equivClass R x
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x : A
⊢ ∀ (y : A), y ∈ equivClass R x ↔ equivClass R y = equivClass R x
Tactic:
fix y : A
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
⊢ y ∈ equivClass R x ↔ equivClass R y = equivClass R x
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
⊢ y ∈ equivClass R x ↔ equivClass R y = equivClass R x
Tactic:
apply Iff.intro
Proof state after:
case mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
⊢ y ∈ equivClass R x → equivClass R y = equivClass R x

case mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
⊢ equivClass R y = equivClass R x → y ∈ equivClass R x
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
case mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
⊢ y ∈ equivClass R x → equivClass R y = equivClass R x
Tactic:
assume h2 :
  y ∈ equivClass R x
Proof state after:
case mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : y ∈ equivClass R x
⊢ equivClass R y = equivClass R x
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
case mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : y ∈ equivClass R x
⊢ equivClass R y = equivClass R x
Tactic:
define at h2
Proof state after:
case mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
⊢ equivClass R y = equivClass R x
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
case mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
⊢ equivClass R y = equivClass R x
Tactic:
apply Set.ext
Proof state after:
case mp.h
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
⊢ ∀ (x_1 : A), x_1 ∈ equivClass R y ↔ x_1 ∈ equivClass R x
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
case mp.h
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
⊢ ∀ (x_1 : A), x_1 ∈ equivClass R y ↔ x_1 ∈ equivClass R x
Tactic:
fix z : A
Proof state after:
case mp.h
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
⊢ z ∈ equivClass R y ↔ z ∈ equivClass R x
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
case mp.h
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
⊢ z ∈ equivClass R y ↔ z ∈ equivClass R x
Tactic:
apply Iff.intro
Proof state after:
case mp.h.mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
⊢ z ∈ equivClass R y → z ∈ equivClass R x

case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
⊢ z ∈ equivClass R x → z ∈ equivClass R y
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
case mp.h.mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
⊢ z ∈ equivClass R y → z ∈ equivClass R x
Tactic:
assume h3 : z ∈ equivClass R y
Proof state after:
case mp.h.mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : z ∈ equivClass R y
⊢ z ∈ equivClass R x
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
case mp.h.mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : z ∈ equivClass R y
⊢ z ∈ equivClass R x
Tactic:
define
Proof state after:
case mp.h.mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : z ∈ equivClass R y
⊢ R z x
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
case mp.h.mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : z ∈ equivClass R y
⊢ R z x
Tactic:
define at h3
Proof state after:
case mp.h.mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : R z y
⊢ R z x
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
case mp.h.mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : R z y
⊢ R z x
Tactic:
show R z x from Rtrans z y x h3 h2
Proof state after:
no goals
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
⊢ z ∈ equivClass R x → z ∈ equivClass R y
Tactic:
assume h3 : z ∈ equivClass R x
Proof state after:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : z ∈ equivClass R x
⊢ z ∈ equivClass R y
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : z ∈ equivClass R x
⊢ z ∈ equivClass R y
Tactic:
define
Proof state after:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : z ∈ equivClass R x
⊢ R z y
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : z ∈ equivClass R x
⊢ R z y
Tactic:
define at h3
Proof state after:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : R z x
⊢ R z y
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : R z x
⊢ R z y
Tactic:
have h4 : R x y := Rsymm y x h2
Proof state after:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : R z x
h4 : R x y
⊢ R z y
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : R z x
h4 : R x y
⊢ R z y
Tactic:
show R z y from Rtrans z x y h3 h4
Proof state after:
no goals
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
case mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
⊢ equivClass R y = equivClass R x → y ∈ equivClass R x
Tactic:
assume h2 :
  equivClass R y = equivClass R x
Proof state after:
case mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : equivClass R y = equivClass R x
⊢ y ∈ equivClass R x
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
case mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : equivClass R y = equivClass R x
⊢ y ∈ equivClass R x
Tactic:
rewrite [←h2]
Proof state after:
case mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : equivClass R y = equivClass R x
⊢ y ∈ equivClass R y
Theorem: HTPI.Lemma_4_5_5_2
Proof state before:
case mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : equivClass R y = equivClass R x
⊢ y ∈ equivClass R y
Tactic:
show y ∈ equivClass R y from Lemma_4_5_5_1 R h y
Proof state after:
no goals