internlm/Lean-Github huggingface dataset:
Theorem: HTPI.image_id
Proof state before:
case h.mp
U : Type
A : Set U
x : U
⊢ x ∈ image id A → x ∈ A
Tactic:
assume h1 : x ∈ image id A
Proof state after:
case h.mp
U : Type
A : Set U
x : U
h1 : x ∈ image id A
⊢ x ∈ A
Theorem: HTPI.image_id
Proof state before:
case h.mp
U : Type
A : Set U
x : U
h1 : x ∈ image id A
⊢ x ∈ A
Tactic:
obtain (y : U) (h2 : y ∈ A ∧ id y = x) from h1
Proof state after:
case h.mp
U : Type
A : Set U
x : U
h1 : x ∈ image id A
y : U
h2 : y ∈ A ∧ id y = x
⊢ x ∈ A
Theorem: HTPI.image_id
Proof state before:
case h.mp
U : Type
A : Set U
x : U
h1 : x ∈ image id A
y : U
h2 : y ∈ A ∧ id y = x
⊢ x ∈ A
Tactic:
rewrite [←h2.right]
Proof state after:
case h.mp
U : Type
A : Set U
x : U
h1 : x ∈ image id A
y : U
h2 : y ∈ A ∧ id y = x
⊢ id y ∈ A
Theorem: HTPI.image_id
Proof state before:
case h.mp
U : Type
A : Set U
x : U
h1 : x ∈ image id A
y : U
h2 : y ∈ A ∧ id y = x
⊢ id y ∈ A
Tactic:
show id y ∈ A from h2.left
Proof state after:
no goals
Theorem: HTPI.image_id
Proof state before:
case h.mpr
U : Type
A : Set U
x : U
⊢ x ∈ A → x ∈ image id A
Tactic:
assume h1 : x ∈ A
Proof state after:
case h.mpr
U : Type
A : Set U
x : U
h1 : x ∈ A
⊢ x ∈ image id A
Theorem: HTPI.image_id
Proof state before:
case h.mpr
U : Type
A : Set U
x : U
h1 : x ∈ A
⊢ x ∈ image id A
Tactic:
apply Exists.intro x
Proof state after:
case h.mpr
U : Type
A : Set U
x : U
h1 : x ∈ A
⊢ x ∈ A ∧ id x = x
Theorem: HTPI.image_id
Proof state before:
case h.mpr
U : Type
A : Set U
x : U
h1 : x ∈ A
⊢ x ∈ A ∧ id x = x
Tactic:
apply And.intro h1
Proof state after:
case h.mpr
U : Type
A : Set U
x : U
h1 : x ∈ A
⊢ id x = x
Theorem: HTPI.image_id
Proof state before:
case h.mpr
U : Type
A : Set U
x : U
h1 : x ∈ A
⊢ id x = x
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.inv_inv
Proof state before:
U V : Type
R : Rel U V
⊢ invRel (invRel R) = R
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.inv_match
Proof state before:
U V : Type
R : Rel U V
A : Set U
B : Set V
h : matching R A B
⊢ matching (invRel R) B A
Tactic:
define
Proof state after:
U V : Type
R : Rel U V
A : Set U
B : Set V
h : matching R A B
⊢ rel_within (invRel R) B A ∧ fcnl_on (invRel R) B ∧ fcnl_on (invRel (invRel R)) A
Theorem: HTPI.inv_match
Proof state before:
U V : Type
R : Rel U V
A : Set U
B : Set V
h : matching R A B
⊢ rel_within (invRel R) B A ∧ fcnl_on (invRel R) B ∧ fcnl_on (invRel (invRel R)) A
Tactic:
define at h
Proof state after:
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ rel_within (invRel R) B A ∧ fcnl_on (invRel R) B ∧ fcnl_on (invRel (invRel R)) A
Theorem: HTPI.inv_match
Proof state before:
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ rel_within (invRel R) B A ∧ fcnl_on (invRel R) B ∧ fcnl_on (invRel (invRel R)) A
Tactic:
apply And.intro
Proof state after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ rel_within (invRel R) B A

case right
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ fcnl_on (invRel R) B ∧ fcnl_on (invRel (invRel R)) A
Theorem: HTPI.inv_match
Proof state before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ rel_within (invRel R) B A
Tactic:
define
Proof state after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ ∀ ⦃x : V⦄ ⦃y : U⦄, invRel R x y → x ∈ B ∧ y ∈ A
Theorem: HTPI.inv_match
Proof state before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ ∀ ⦃x : V⦄ ⦃y : U⦄, invRel R x y → x ∈ B ∧ y ∈ A
Tactic:
fix y : V
Proof state after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
⊢ ∀ ⦃y_1 : U⦄, invRel R y y_1 → y ∈ B ∧ y_1 ∈ A
Theorem: HTPI.inv_match
Proof state before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
⊢ ∀ ⦃y_1 : U⦄, invRel R y y_1 → y ∈ B ∧ y_1 ∈ A
Tactic:
fix x : U
Proof state after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
x : U
⊢ invRel R y x → y ∈ B ∧ x ∈ A
Theorem: HTPI.inv_match
Proof state before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
x : U
⊢ invRel R y x → y ∈ B ∧ x ∈ A
Tactic:
assume h1 : invRel R y x
Proof state after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
x : U
h1 : invRel R y x
⊢ y ∈ B ∧ x ∈ A
Theorem: HTPI.inv_match
Proof state before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
x : U
h1 : invRel R y x
⊢ y ∈ B ∧ x ∈ A
Tactic:
define at h1
Proof state after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
x : U
h1 : R x y
⊢ y ∈ B ∧ x ∈ A
Theorem: HTPI.inv_match
Proof state before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
x : U
h1 : R x y
⊢ y ∈ B ∧ x ∈ A
Tactic:
have h2 : x ∈ A ∧ y ∈ B := h.left h1
Proof state after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
x : U
h1 : R x y
h2 : x ∈ A ∧ y ∈ B
⊢ y ∈ B ∧ x ∈ A
Theorem: HTPI.inv_match
Proof state before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
x : U
h1 : R x y
h2 : x ∈ A ∧ y ∈ B
⊢ y ∈ B ∧ x ∈ A
Tactic:
show y ∈ B ∧ x ∈ A from And.intro h2.right h2.left
Proof state after:
no goals
Theorem: HTPI.inv_match
Proof state before:
case right
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ fcnl_on (invRel R) B ∧ fcnl_on (invRel (invRel R)) A
Tactic:
rewrite [inv_inv]
Proof state after:
case right
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ fcnl_on (invRel R) B ∧ fcnl_on R A
Theorem: HTPI.inv_match
Proof state before:
case right
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ fcnl_on (invRel R) B ∧ fcnl_on R A
Tactic:
show fcnl_on (invRel R) B ∧ fcnl_on R A from
  And.intro h.right.right h.right.left
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_3_2
Proof state before:
U V : Type
A : Set U
B : Set V
h : A ∼ B
⊢ B ∼ A
Tactic:
obtain (R : Rel U V) (h1 : matching R A B) from h
Proof state after:
U V : Type
A : Set U
B : Set V
h : A ∼ B
R : Rel U V
h1 : matching R A B
⊢ B ∼ A
Theorem: HTPI.Theorem_8_1_3_2
Proof state before:
U V : Type
A : Set U
B : Set V
h : A ∼ B
R : Rel U V
h1 : matching R A B
⊢ B ∼ A
Tactic:
apply Exists.intro (invRel R)
Proof state after:
U V : Type
A : Set U
B : Set V
h : A ∼ B
R : Rel U V
h1 : matching R A B
⊢ matching (invRel R) B A
Theorem: HTPI.Theorem_8_1_3_2
Proof state before:
U V : Type
A : Set U
B : Set V
h : A ∼ B
R : Rel U V
h1 : matching R A B
⊢ matching (invRel R) B A
Tactic:
show matching (invRel R) B A from inv_match h1
Proof state after:
no goals
Theorem: HTPI.fcnl_exists
Proof state before:
U V : Type
R : Rel U V
A : Set U
x : U
h1 : fcnl_on R A
h2 : x ∈ A
⊢ ∃ y, R x y
Tactic:
define at h1
Proof state after:
U V : Type
R : Rel U V
A : Set U
x : U
h1 : ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
h2 : x ∈ A
⊢ ∃ y, R x y
Theorem: HTPI.fcnl_exists
Proof state before:
U V : Type
R : Rel U V
A : Set U
x : U
h1 : ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
h2 : x ∈ A
⊢ ∃ y, R x y
Tactic:
obtain (y : V) (h3 : R x y)
  (h4 : ∀ (y_1 y_2 : V), R x y_1 → R x y_2 → y_1 = y_2) from h1 h2
Proof state after:
U V : Type
R : Rel U V
A : Set U
x : U
h1 : ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
h2 : x ∈ A
y : V
h3 : R x y
h4 : ∀ (y_1 y_2 : V), R x y_1 → R x y_2 → y_1 = y_2
⊢ ∃ y, R x y
Theorem: HTPI.fcnl_exists
Proof state before:
U V : Type
R : Rel U V
A : Set U
x : U
h1 : ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
h2 : x ∈ A
y : V
h3 : R x y
h4 : ∀ (y_1 y_2 : V), R x y_1 → R x y_2 → y_1 = y_2
⊢ ∃ y, R x y
Tactic:
show ∃ (y : V), R x y from Exists.intro y h3
Proof state after:
no goals
Theorem: HTPI.fcnl_unique
Proof state before:
U V : Type
R : Rel U V
A : Set U
x : U
y1 y2 : V
h1 : fcnl_on R A
h2 : x ∈ A
h3 : R x y1
h4 : R x y2
⊢ y1 = y2
Tactic:
define at h1
Proof state after:
U V : Type
R : Rel U V
A : Set U
x : U
y1 y2 : V
h1 : ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
h2 : x ∈ A
h3 : R x y1
h4 : R x y2
⊢ y1 = y2
Theorem: HTPI.fcnl_unique
Proof state before:
U V : Type
R : Rel U V
A : Set U
x : U
y1 y2 : V
h1 : ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
h2 : x ∈ A
h3 : R x y1
h4 : R x y2
⊢ y1 = y2
Tactic:
obtain (z : V) (h5 : R x z)
  (h6 : ∀ (y_1 y_2 : V), R x y_1 → R x y_2 → y_1 = y_2) from h1 h2
Proof state after:
U V : Type
R : Rel U V
A : Set U
x : U
y1 y2 : V
h1 : ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
h2 : x ∈ A
h3 : R x y1
h4 : R x y2
z : V
h5 : R x z
h6 : ∀ (y_1 y_2 : V), R x y_1 → R x y_2 → y_1 = y_2
⊢ y1 = y2
Theorem: HTPI.fcnl_unique
Proof state before:
U V : Type
R : Rel U V
A : Set U
x : U
y1 y2 : V
h1 : ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
h2 : x ∈ A
h3 : R x y1
h4 : R x y2
z : V
h5 : R x z
h6 : ∀ (y_1 y_2 : V), R x y_1 → R x y_2 → y_1 = y_2
⊢ y1 = y2
Tactic:
show y1 = y2 from h6 y1 y2 h3 h4
Proof state after:
no goals
Theorem: HTPI.compRel_def
Proof state before:
U V W : Type
S : Rel V W
R : Rel U V
u : U
w : W
⊢ compRel S R u w ↔ ∃ x, R u x ∧ S x w
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.inv_comp
Proof state before:
U V W : Type
R : Rel U V
S : Rel V W
⊢ invRel (compRel S R) = RelFromExt (inv (comp (extension S) (extension R)))
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.inv_comp
Proof state before:
U V W : Type
R : Rel U V
S : Rel V W
⊢ RelFromExt (inv (comp (extension S) (extension R))) = RelFromExt (comp (inv (extension R)) (inv (extension S)))
Tactic:
rw [Theorem_4_2_5_5]
Proof state after:
no goals
Theorem: HTPI.inv_comp
Proof state before:
U V W : Type
R : Rel U V
S : Rel V W
⊢ RelFromExt (comp (inv (extension R)) (inv (extension S))) = compRel (invRel R) (invRel S)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.comp_fcnl
Proof state before:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ fcnl_on (compRel S R) A
Tactic:
define
Proof state after:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, compRel S R x y
Theorem: HTPI.comp_fcnl
Proof state before:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, compRel S R x y
Tactic:
define at h1
Proof state after:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : matching S B C
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, compRel S R x y
Theorem: HTPI.comp_fcnl
Proof state before:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : matching S B C
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, compRel S R x y
Tactic:
define at h2
Proof state after:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, compRel S R x y
Theorem: HTPI.comp_fcnl
Proof state before:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, compRel S R x y
Tactic:
fix a : U
Proof state after:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
⊢ a ∈ A → ∃! y, compRel S R a y
Theorem: HTPI.comp_fcnl
Proof state before:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
⊢ a ∈ A → ∃! y, compRel S R a y
Tactic:
assume h3 : a ∈ A
Proof state after:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
⊢ ∃! y, compRel S R a y
Theorem: HTPI.comp_fcnl
Proof state before:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
⊢ ∃! y, compRel S R a y
Tactic:
obtain (b : V) (h4 : R a b) from fcnl_exists h1.right.left h3
Proof state after:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
⊢ ∃! y, compRel S R a y
Theorem: HTPI.comp_fcnl
Proof state before:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
⊢ ∃! y, compRel S R a y
Tactic:
have h5 : a ∈ A ∧ b ∈ B := h1.left h4
Proof state after:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
⊢ ∃! y, compRel S R a y
Theorem: HTPI.comp_fcnl
Proof state before:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
⊢ ∃! y, compRel S R a y
Tactic:
obtain (c : W) (h6 : S b c) from fcnl_exists h2.right.left h5.right
Proof state after:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
⊢ ∃! y, compRel S R a y
Theorem: HTPI.comp_fcnl
Proof state before:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
⊢ ∃! y, compRel S R a y
Tactic:
exists_unique
Proof state after:
case Existence
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
⊢ ∃ y, compRel S R a y

case Uniqueness
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
⊢ ∀ (y_1 y_2 : W), compRel S R a y_1 → compRel S R a y_2 → y_1 = y_2
Theorem: HTPI.comp_fcnl
Proof state before:
case Existence
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
⊢ ∃ y, compRel S R a y
Tactic:
apply Exists.intro c
Proof state after:
case Existence
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
⊢ compRel S R a c
Theorem: HTPI.comp_fcnl
Proof state before:
case Existence
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
⊢ compRel S R a c
Tactic:
rewrite [compRel_def]
Proof state after:
case Existence
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
⊢ ∃ x, R a x ∧ S x c
Theorem: HTPI.comp_fcnl
Proof state before:
case Existence
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
⊢ ∃ x, R a x ∧ S x c
Tactic:
show ∃ (x : V), R a x ∧ S x c from Exists.intro b (And.intro h4 h6)
Proof state after:
no goals
Theorem: HTPI.comp_fcnl
Proof state before:
case Uniqueness
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
⊢ ∀ (y_1 y_2 : W), compRel S R a y_1 → compRel S R a y_2 → y_1 = y_2
Tactic:
fix c1 : W
Proof state after:
case Uniqueness
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
c1 : W
⊢ ∀ (y_2 : W), compRel S R a c1 → compRel S R a y_2 → c1 = y_2
Theorem: HTPI.comp_fcnl
Proof state before:
case Uniqueness
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
c1 : W
⊢ ∀ (y_2 : W), compRel S R a c1 → compRel S R a y_2 → c1 = y_2
Tactic:
fix c2 : W
Proof state after:
case Uniqueness
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
c1 c2 : W
⊢ compRel S R a c1 → compRel S R a c2 → c1 = c2
Theorem: HTPI.comp_fcnl
Proof state before:
case Uniqueness
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
c1 c2 : W
⊢ compRel S R a c1 → compRel S R a c2 → c1 = c2
Tactic:
assume h7 : compRel S R a c1
Proof state after:
case Uniqueness
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
c1 c2 : W
h7 : compRel S R a c1
⊢ compRel S R a c2 → c1 = c2
Theorem: HTPI.comp_fcnl
Proof state before:
case Uniqueness
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
c1 c2 : W
h7 : compRel S R a c1
⊢ compRel S R a c2 → c1 = c2
Tactic:
assume h8 : compRel S R a c2
Proof state after:
case Uniqueness
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
c1 c2 : W
h7 : compRel S R a c1
h8 : compRel S R a c2
⊢ c1 = c2
Theorem: HTPI.comp_fcnl
Proof state before:
case Uniqueness
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
c1 c2 : W
h7 : compRel S R a c1
h8 : compRel S R a c2
⊢ c1 = c2
Tactic:
rewrite [compRel_def] at h7
Proof state after:
case Uniqueness
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
c1 c2 : W
h7 : ∃ x, R a x ∧ S x c1
h8 : compRel S R a c2
⊢ c1 = c2
Theorem: HTPI.comp_fcnl
Proof state before:
case Uniqueness
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
c1 c2 : W
h7 : ∃ x, R a x ∧ S x c1
h8 : compRel S R a c2
⊢ c1 = c2
Tactic:
rewrite [compRel_def] at h8
Proof state after:
case Uniqueness
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
c1 c2 : W
h7 : ∃ x, R a x ∧ S x c1
h8 : ∃ x, R a x ∧ S x c2
⊢ c1 = c2
Theorem: HTPI.comp_fcnl
Proof state before:
case Uniqueness
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
c1 c2 : W
h7 : ∃ x, R a x ∧ S x c1
h8 : ∃ x, R a x ∧ S x c2
⊢ c1 = c2
Tactic:
obtain (b1 : V) (h9 : R a b1 ∧ S b1 c1) from h7
Proof state after:
case Uniqueness
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
c1 c2 : W
h7 : ∃ x, R a x ∧ S x c1
h8 : ∃ x, R a x ∧ S x c2
b1 : V
h9 : R a b1 ∧ S b1 c1
⊢ c1 = c2
Theorem: HTPI.comp_fcnl
Proof state before:
case Uniqueness
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
c1 c2 : W
h7 : ∃ x, R a x ∧ S x c1
h8 : ∃ x, R a x ∧ S x c2
b1 : V
h9 : R a b1 ∧ S b1 c1
⊢ c1 = c2
Tactic:
obtain (b2 : V) (h10 : R a b2 ∧ S b2 c2) from h8
Proof state after:
case Uniqueness
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : rel_within S B C ∧ fcnl_on S B ∧ fcnl_on (invRel S) C
a : U
h3 : a ∈ A
b : V
h4 : R a b
h5 : a ∈ A ∧ b ∈ B
c : W
h6 : S b c
c1 c2 : W
h7 : ∃ x, R a x ∧ S x c1
h8 : ∃ x, R a x ∧ S x c2
b1 : V
h9 : R a b1 ∧ S b1 c1
b2 : V
h10 : R a b2 ∧ S b2 c2
⊢ c1 = c2