internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : (a, c) ∈ comp S R
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
Tactic:
define at h3
Proof state after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
Tactic:
obtain (b : B) (h4 : (a, b) ∈ R ∧ (b, c) ∈ S) from h3
Proof state after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h4 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h4 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
Tactic:
apply Exists.intro b
Proof state after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h4 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ (a, b) ∈ R ∧ (b, d) ∈ comp T S
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h4 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ (a, b) ∈ R ∧ (b, d) ∈ comp T S
Tactic:
apply And.intro h4.left
Proof state after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h4 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ (b, d) ∈ comp T S
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h4 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ (b, d) ∈ comp T S
Tactic:
define
Proof state after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h4 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h4 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
Tactic:
show ∃ (x : C), (b, x) ∈ S ∧ (x, d) ∈ T from
  Exists.intro c (And.intro h4.right h2.right)
Proof state after:
no goals
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
⊢ (a, d) ∈ comp (comp T S) R → (a, d) ∈ comp T (comp S R)
Tactic:
assume h1 : (a, d) ∈ comp (comp T S) R
Proof state after:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : (a, d) ∈ comp (comp T S) R
⊢ (a, d) ∈ comp T (comp S R)
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : (a, d) ∈ comp (comp T S) R
⊢ (a, d) ∈ comp T (comp S R)
Tactic:
define
Proof state after:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : (a, d) ∈ comp (comp T S) R
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : (a, d) ∈ comp (comp T S) R
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Tactic:
define at h1
Proof state after:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Tactic:
obtain (b : B) (h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S) from h1
Proof state after:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Tactic:
have h3 : (b, d) ∈ comp T S := h2.right
Proof state after:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : (b, d) ∈ comp T S
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : (b, d) ∈ comp T S
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Tactic:
define at h3
Proof state after:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Tactic:
obtain (c : C) (h4 : (b, c) ∈ S ∧ (c, d) ∈ T) from h3
Proof state after:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
c : C
h4 : (b, c) ∈ S ∧ (c, d) ∈ T
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
c : C
h4 : (b, c) ∈ S ∧ (c, d) ∈ T
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Tactic:
apply Exists.intro c
Proof state after:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
c : C
h4 : (b, c) ∈ S ∧ (c, d) ∈ T
⊢ (a, c) ∈ comp S R ∧ (c, d) ∈ T
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
c : C
h4 : (b, c) ∈ S ∧ (c, d) ∈ T
⊢ (a, c) ∈ comp S R ∧ (c, d) ∈ T
Tactic:
apply And.intro _ h4.right
Proof state after:
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
c : C
h4 : (b, c) ∈ S ∧ (c, d) ∈ T
⊢ (a, c) ∈ comp S R
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
c : C
h4 : (b, c) ∈ S ∧ (c, d) ∈ T
⊢ (a, c) ∈ comp S R
Tactic:
define
Proof state after:
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
c : C
h4 : (b, c) ∈ S ∧ (c, d) ∈ T
⊢ ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
c : C
h4 : (b, c) ∈ S ∧ (c, d) ∈ T
⊢ ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
Tactic:
show ∃ (x : B), (a, x) ∈ R ∧ (x, c) ∈ S from
  Exists.intro b (And.intro h2.left h4.left)
Proof state after:
no goals
Theorem: HTPI.inv_def
Proof state before:
A B : Type
R : Set (A × B)
a : A
b : B
⊢ (b, a) ∈ inv R ↔ (a, b) ∈ R
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_4_2_5_5
Proof state before:
A B C : Type
R : Set (A × B)
S : Set (B × C)
⊢ inv (comp S R) = comp (inv R) (inv S)
Tactic:
apply Set.ext
Proof state after:
case h
A B C : Type
R : Set (A × B)
S : Set (B × C)
⊢ ∀ (x : C × A), x ∈ inv (comp S R) ↔ x ∈ comp (inv R) (inv S)
Theorem: HTPI.Theorem_4_2_5_5
Proof state before:
case h
A B C : Type
R : Set (A × B)
S : Set (B × C)
⊢ ∀ (x : C × A), x ∈ inv (comp S R) ↔ x ∈ comp (inv R) (inv S)
Tactic:
fix (c, a) : C × A
Proof state after:
case h
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
⊢ (c, a) ∈ inv (comp S R) ↔ (c, a) ∈ comp (inv R) (inv S)
Theorem: HTPI.Theorem_4_2_5_5
Proof state before:
case h
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
⊢ (c, a) ∈ inv (comp S R) ↔ (c, a) ∈ comp (inv R) (inv S)
Tactic:
apply Iff.intro
Proof state after:
case h.mp
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
⊢ (c, a) ∈ inv (comp S R) → (c, a) ∈ comp (inv R) (inv S)

case h.mpr
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
⊢ (c, a) ∈ comp (inv R) (inv S) → (c, a) ∈ inv (comp S R)
Theorem: HTPI.Theorem_4_2_5_5
Proof state before:
case h.mp
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
⊢ (c, a) ∈ inv (comp S R) → (c, a) ∈ comp (inv R) (inv S)
Tactic:
assume h1 : (c, a) ∈ inv (comp S R)
Proof state after:
case h.mp
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : (c, a) ∈ inv (comp S R)
⊢ (c, a) ∈ comp (inv R) (inv S)
Theorem: HTPI.Theorem_4_2_5_5
Proof state before:
case h.mp
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : (c, a) ∈ inv (comp S R)
⊢ (c, a) ∈ comp (inv R) (inv S)
Tactic:
define at h1
Proof state after:
case h.mp
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
⊢ (c, a) ∈ comp (inv R) (inv S)
Theorem: HTPI.Theorem_4_2_5_5
Proof state before:
case h.mp
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
⊢ (c, a) ∈ comp (inv R) (inv S)
Tactic:
define
Proof state after:
case h.mp
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
⊢ ∃ x, (c, x) ∈ inv S ∧ (x, a) ∈ inv R
Theorem: HTPI.Theorem_4_2_5_5
Proof state before:
case h.mp
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
⊢ ∃ x, (c, x) ∈ inv S ∧ (x, a) ∈ inv R
Tactic:
obtain (b : B) (h2 : (a, b) ∈ R ∧ (b, c) ∈ S) from h1
Proof state after:
case h.mp
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h2 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ ∃ x, (c, x) ∈ inv S ∧ (x, a) ∈ inv R
Theorem: HTPI.Theorem_4_2_5_5
Proof state before:
case h.mp
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h2 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ ∃ x, (c, x) ∈ inv S ∧ (x, a) ∈ inv R
Tactic:
apply Exists.intro b
Proof state after:
case h.mp
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h2 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ (c, b) ∈ inv S ∧ (b, a) ∈ inv R
Theorem: HTPI.Theorem_4_2_5_5
Proof state before:
case h.mp
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h2 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ (c, b) ∈ inv S ∧ (b, a) ∈ inv R
Tactic:
rewrite [inv_def, inv_def]
Proof state after:
case h.mp
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h2 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ (b, c) ∈ S ∧ (a, b) ∈ R
Theorem: HTPI.Theorem_4_2_5_5
Proof state before:
case h.mp
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h2 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ (b, c) ∈ S ∧ (a, b) ∈ R
Tactic:
show (b, c) ∈ S ∧ (a, b) ∈ R from And.intro h2.right h2.left
Proof state after:
no goals
Theorem: HTPI.Theorem_4_2_5_5
Proof state before:
case h.mpr
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
⊢ (c, a) ∈ comp (inv R) (inv S) → (c, a) ∈ inv (comp S R)
Tactic:
assume h1 : (c, a) ∈ comp (inv R) (inv S)
Proof state after:
case h.mpr
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : (c, a) ∈ comp (inv R) (inv S)
⊢ (c, a) ∈ inv (comp S R)
Theorem: HTPI.Theorem_4_2_5_5
Proof state before:
case h.mpr
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : (c, a) ∈ comp (inv R) (inv S)
⊢ (c, a) ∈ inv (comp S R)
Tactic:
define at h1
Proof state after:
case h.mpr
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (c, x) ∈ inv S ∧ (x, a) ∈ inv R
⊢ (c, a) ∈ inv (comp S R)
Theorem: HTPI.Theorem_4_2_5_5
Proof state before:
case h.mpr
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (c, x) ∈ inv S ∧ (x, a) ∈ inv R
⊢ (c, a) ∈ inv (comp S R)
Tactic:
define
Proof state after:
case h.mpr
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (c, x) ∈ inv S ∧ (x, a) ∈ inv R
⊢ ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
Theorem: HTPI.Theorem_4_2_5_5
Proof state before:
case h.mpr
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (c, x) ∈ inv S ∧ (x, a) ∈ inv R
⊢ ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
Tactic:
obtain (b : B) (h2 : (c, b) ∈ inv S ∧ (b, a) ∈ inv R) from h1
Proof state after:
case h.mpr
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (c, x) ∈ inv S ∧ (x, a) ∈ inv R
b : B
h2 : (c, b) ∈ inv S ∧ (b, a) ∈ inv R
⊢ ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
Theorem: HTPI.Theorem_4_2_5_5
Proof state before:
case h.mpr
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (c, x) ∈ inv S ∧ (x, a) ∈ inv R
b : B
h2 : (c, b) ∈ inv S ∧ (b, a) ∈ inv R
⊢ ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
Tactic:
apply Exists.intro b
Proof state after:
case h.mpr
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (c, x) ∈ inv S ∧ (x, a) ∈ inv R
b : B
h2 : (c, b) ∈ inv S ∧ (b, a) ∈ inv R
⊢ (a, b) ∈ R ∧ (b, c) ∈ S
Theorem: HTPI.Theorem_4_2_5_5
Proof state before:
case h.mpr
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (c, x) ∈ inv S ∧ (x, a) ∈ inv R
b : B
h2 : (c, b) ∈ inv S ∧ (b, a) ∈ inv R
⊢ (a, b) ∈ R ∧ (b, c) ∈ S
Tactic:
rewrite [inv_def, inv_def] at h2
Proof state after:
case h.mpr
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (c, x) ∈ inv S ∧ (x, a) ∈ inv R
b : B
h2 : (b, c) ∈ S ∧ (a, b) ∈ R
⊢ (a, b) ∈ R ∧ (b, c) ∈ S
Theorem: HTPI.Theorem_4_2_5_5
Proof state before:
case h.mpr
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (c, x) ∈ inv S ∧ (x, a) ∈ inv R
b : B
h2 : (b, c) ∈ S ∧ (a, b) ∈ R
⊢ (a, b) ∈ R ∧ (b, c) ∈ S
Tactic:
show (a, b) ∈ R ∧ (b, c) ∈ S from And.intro h2.right h2.left
Proof state after:
no goals
Theorem: HTPI.ext_def
Proof state before:
A B : Type
R : Rel A B
a : A
b : B
⊢ (a, b) ∈ extension R ↔ R a b
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_4_3_4_2
Proof state before:
A : Type
R : BinRel A
⊢ symmetric R ↔ extension R = inv (extension R)
Tactic:
apply Iff.intro
Proof state after:
case mp
A : Type
R : BinRel A
⊢ symmetric R → extension R = inv (extension R)

case mpr
A : Type
R : BinRel A
⊢ extension R = inv (extension R) → symmetric R
Theorem: HTPI.Theorem_4_3_4_2
Proof state before:
case mp
A : Type
R : BinRel A
⊢ symmetric R → extension R = inv (extension R)
Tactic:
assume h1 : symmetric R
Proof state after:
case mp
A : Type
R : BinRel A
h1 : symmetric R
⊢ extension R = inv (extension R)
Theorem: HTPI.Theorem_4_3_4_2
Proof state before:
case mp
A : Type
R : BinRel A
h1 : symmetric R
⊢ extension R = inv (extension R)
Tactic:
define at h1
Proof state after:
case mp
A : Type
R : BinRel A
h1 : ∀ (x y : A), R x y → R y x
⊢ extension R = inv (extension R)
Theorem: HTPI.Theorem_4_3_4_2
Proof state before:
case mp
A : Type
R : BinRel A
h1 : ∀ (x y : A), R x y → R y x
⊢ extension R = inv (extension R)
Tactic:
apply Set.ext
Proof state after:
case mp.h
A : Type
R : BinRel A
h1 : ∀ (x y : A), R x y → R y x
⊢ ∀ (x : A × A), x ∈ extension R ↔ x ∈ inv (extension R)
Theorem: HTPI.Theorem_4_3_4_2
Proof state before:
case mp.h
A : Type
R : BinRel A
h1 : ∀ (x y : A), R x y → R y x
⊢ ∀ (x : A × A), x ∈ extension R ↔ x ∈ inv (extension R)
Tactic:
fix (a, b) : A × A
Proof state after:
case mp.h
A : Type
R : BinRel A
h1 : ∀ (x y : A), R x y → R y x
a b : A
⊢ (a, b) ∈ extension R ↔ (a, b) ∈ inv (extension R)
Theorem: HTPI.Theorem_4_3_4_2
Proof state before:
case mp.h
A : Type
R : BinRel A
h1 : ∀ (x y : A), R x y → R y x
a b : A
⊢ (a, b) ∈ extension R ↔ (a, b) ∈ inv (extension R)
Tactic:
show (a, b) ∈ extension R ↔ (a, b) ∈ inv (extension R) from
  calc (a, b) ∈ extension R
    _ ↔ R a b := by rfl
    _ ↔ R b a := Iff.intro (h1 a b) (h1 b a)
    _ ↔ (a, b) ∈ inv (extension R) := by rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_4_3_4_2
Proof state before:
A : Type
R : BinRel A
h1 : ∀ (x y : A), R x y → R y x
a b : A
⊢ (a, b) ∈ extension R ↔ R a b
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_4_3_4_2
Proof state before:
A : Type
R : BinRel A
h1 : ∀ (x y : A), R x y → R y x
a b : A
⊢ R b a ↔ (a, b) ∈ inv (extension R)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_4_3_4_2
Proof state before:
case mpr
A : Type
R : BinRel A
⊢ extension R = inv (extension R) → symmetric R
Tactic:
assume h1 : extension R = inv (extension R)
Proof state after:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
⊢ symmetric R
Theorem: HTPI.Theorem_4_3_4_2
Proof state before:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
⊢ symmetric R
Tactic:
define
Proof state after:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
⊢ ∀ (x y : A), R x y → R y x
Theorem: HTPI.Theorem_4_3_4_2
Proof state before:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
⊢ ∀ (x y : A), R x y → R y x
Tactic:
fix a : A
Proof state after:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
a : A
⊢ ∀ (y : A), R a y → R y a
Theorem: HTPI.Theorem_4_3_4_2
Proof state before:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
a : A
⊢ ∀ (y : A), R a y → R y a
Tactic:
fix b : A
Proof state after:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
a b : A
⊢ R a b → R b a
Theorem: HTPI.Theorem_4_3_4_2
Proof state before:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
a b : A
⊢ R a b → R b a
Tactic:
assume h2 : R a b
Proof state after:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
a b : A
h2 : R a b
⊢ R b a
Theorem: HTPI.Theorem_4_3_4_2
Proof state before:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
a b : A
h2 : R a b
⊢ R b a
Tactic:
rewrite [←ext_def R, h1, inv_def, ext_def] at h2
Proof state after:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
a b : A
h2 : R b a
⊢ R b a
Theorem: HTPI.Theorem_4_3_4_2
Proof state before:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
a b : A
h2 : R b a
⊢ R b a
Tactic:
show R b a from h2
Proof state after:
no goals
Theorem: HTPI.RelFromExt_def
Proof state before:
A B : Type
R : Set (A × B)
a : A
b : B
⊢ RelFromExt R a b ↔ (a, b) ∈ R
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_4_4_6_2
Proof state before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : partial_order R
h2 : smallestElt R b B
⊢ minimalElt R b B ∧ ∀ (c : A), minimalElt R c B → b = c
Tactic:
define at h1
Proof state after:
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : smallestElt R b B
⊢ minimalElt R b B ∧ ∀ (c : A), minimalElt R c B → b = c
Theorem: HTPI.Theorem_4_4_6_2
Proof state before:
A : Type
R : BinRel A
B : Set A
b : A
h1 : reflexive R ∧ transitive R ∧ antisymmetric R
h2 : smallestElt R b B
⊢ minimalElt R b B ∧ ∀ (c : A), minimalElt R c B → b = c
Tactic:
define at h2
Proof state after:
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
⊢ minimalElt R b B ∧ ∀ (c : A), minimalElt R c B → b = c
Theorem: HTPI.Theorem_4_4_6_2
Proof state before:
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
⊢ minimalElt R b B ∧ ∀ (c : A), minimalElt R c B → b = c
Tactic:
apply And.intro
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
⊢ minimalElt R b B

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 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
⊢ minimalElt R b B
Tactic:
define
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
⊢ b ∈ B ∧ ¬∃ 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
⊢ b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
Tactic:
apply And.intro h2.left
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 ∈ 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 ∈ B, R x b ∧ x ≠ b
Tactic:
quant_neg
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), ¬(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), ¬(x ∈ B ∧ R x b ∧ x ≠ b)
Tactic:
fix x : A
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
⊢ ¬(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
⊢ ¬(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
⊢ 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
⊢ x ∉ B ∨ ¬(R x b ∧ x ≠ b)
Tactic:
or_right with 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
⊢ ¬(R x b ∧ x ≠ b)