internlm/Lean-Github huggingface dataset:
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
b2 : V
h10 : R a b2 ∧ S b2 c2
⊢ c1 = c2
Tactic:
have h11 : b1 = b := fcnl_unique h1.right.left h3 h9.left h4
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
h11 : b1 = b
⊢ 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
b2 : V
h10 : R a b2 ∧ S b2 c2
h11 : b1 = b
⊢ c1 = c2
Tactic:
have h12 : b2 = b := fcnl_unique h1.right.left h3 h10.left h4
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
h11 : b1 = b
h12 : b2 = b
⊢ 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
b2 : V
h10 : R a b2 ∧ S b2 c2
h11 : b1 = b
h12 : b2 = b
⊢ c1 = c2
Tactic:
rewrite [h11] at h9
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 b ∧ S b c1
b2 : V
h10 : R a b2 ∧ S b2 c2
h11 : b1 = b
h12 : b2 = b
⊢ 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 b ∧ S b c1
b2 : V
h10 : R a b2 ∧ S b2 c2
h11 : b1 = b
h12 : b2 = b
⊢ c1 = c2
Tactic:
rewrite [h12] at h10
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 b ∧ S b c1
b2 : V
h10 : R a b ∧ S b c2
h11 : b1 = b
h12 : b2 = b
⊢ 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 b ∧ S b c1
b2 : V
h10 : R a b ∧ S b c2
h11 : b1 = b
h12 : b2 = b
⊢ c1 = c2
Tactic:
show c1 = c2 from
  fcnl_unique h2.right.left h5.right h9.right h10.right
Proof state after:
no goals
Theorem: HTPI.comp_match
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
⊢ matching (compRel S R) A C
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
⊢ rel_within (compRel S R) A C ∧ fcnl_on (compRel S R) A ∧ fcnl_on (invRel (compRel S R)) C
Theorem: HTPI.comp_match
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
⊢ rel_within (compRel S R) A C ∧ fcnl_on (compRel S R) A ∧ fcnl_on (invRel (compRel S R)) C
Tactic:
apply And.intro
Proof state after:
case left
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
⊢ rel_within (compRel S R) A C

case right
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 ∧ fcnl_on (invRel (compRel S R)) C
Theorem: HTPI.comp_match
Proof state before:
case left
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
⊢ rel_within (compRel S R) A C
Tactic:
define
Proof state after:
case left
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⦄ ⦃y : W⦄, compRel S R x y → x ∈ A ∧ y ∈ C
Theorem: HTPI.comp_match
Proof state before:
case left
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⦄ ⦃y : W⦄, compRel S R x y → x ∈ A ∧ y ∈ C
Tactic:
fix a : U
Proof state after:
case left
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
a : U
⊢ ∀ ⦃y : W⦄, compRel S R a y → a ∈ A ∧ y ∈ C
Theorem: HTPI.comp_match
Proof state before:
case left
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
a : U
⊢ ∀ ⦃y : W⦄, compRel S R a y → a ∈ A ∧ y ∈ C
Tactic:
fix c : W
Proof state after:
case left
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
a : U
c : W
⊢ compRel S R a c → a ∈ A ∧ c ∈ C
Theorem: HTPI.comp_match
Proof state before:
case left
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
a : U
c : W
⊢ compRel S R a c → a ∈ A ∧ c ∈ C
Tactic:
assume h3 : compRel S R a c
Proof state after:
case left
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
a : U
c : W
h3 : compRel S R a c
⊢ a ∈ A ∧ c ∈ C
Theorem: HTPI.comp_match
Proof state before:
case left
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
a : U
c : W
h3 : compRel S R a c
⊢ a ∈ A ∧ c ∈ C
Tactic:
rewrite [compRel_def] at h3
Proof state after:
case left
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
a : U
c : W
h3 : ∃ x, R a x ∧ S x c
⊢ a ∈ A ∧ c ∈ C
Theorem: HTPI.comp_match
Proof state before:
case left
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
a : U
c : W
h3 : ∃ x, R a x ∧ S x c
⊢ a ∈ A ∧ c ∈ C
Tactic:
obtain (b : V) (h4 : R a b ∧ S b c) from h3
Proof state after:
case left
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
a : U
c : W
h3 : ∃ x, R a x ∧ S x c
b : V
h4 : R a b ∧ S b c
⊢ a ∈ A ∧ c ∈ C
Theorem: HTPI.comp_match
Proof state before:
case left
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
a : U
c : W
h3 : ∃ x, R a x ∧ S x c
b : V
h4 : R a b ∧ S b c
⊢ a ∈ A ∧ c ∈ C
Tactic:
have h5 : a ∈ A ∧ b ∈ B := h1.left h4.left
Proof state after:
case left
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
a : U
c : W
h3 : ∃ x, R a x ∧ S x c
b : V
h4 : R a b ∧ S b c
h5 : a ∈ A ∧ b ∈ B
⊢ a ∈ A ∧ c ∈ C
Theorem: HTPI.comp_match
Proof state before:
case left
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
a : U
c : W
h3 : ∃ x, R a x ∧ S x c
b : V
h4 : R a b ∧ S b c
h5 : a ∈ A ∧ b ∈ B
⊢ a ∈ A ∧ c ∈ C
Tactic:
have h6 : b ∈ B ∧ c ∈ C := h2.left h4.right
Proof state after:
case left
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
a : U
c : W
h3 : ∃ x, R a x ∧ S x c
b : V
h4 : R a b ∧ S b c
h5 : a ∈ A ∧ b ∈ B
h6 : b ∈ B ∧ c ∈ C
⊢ a ∈ A ∧ c ∈ C
Theorem: HTPI.comp_match
Proof state before:
case left
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
a : U
c : W
h3 : ∃ x, R a x ∧ S x c
b : V
h4 : R a b ∧ S b c
h5 : a ∈ A ∧ b ∈ B
h6 : b ∈ B ∧ c ∈ C
⊢ a ∈ A ∧ c ∈ C
Tactic:
show a ∈ A ∧ c ∈ C from And.intro h5.left h6.right
Proof state after:
no goals
Theorem: HTPI.comp_match
Proof state before:
case right
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 ∧ fcnl_on (invRel (compRel S R)) C
Tactic:
apply And.intro
Proof state after:
case right.left
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

case right.right
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 (invRel (compRel S R)) C
Theorem: HTPI.comp_match
Proof state before:
case right.left
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:
show fcnl_on (compRel S R) A from comp_fcnl h1 h2
Proof state after:
no goals
Theorem: HTPI.comp_match
Proof state before:
case right.right
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 (invRel (compRel S R)) C
Tactic:
rewrite [inv_comp]
Proof state after:
case right.right
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 (invRel R) (invRel S)) C
Theorem: HTPI.comp_match
Proof state before:
case right.right
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 (invRel R) (invRel S)) C
Tactic:
have h3 : matching (invRel R) B A := inv_match h1
Proof state after:
case right.right
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
h3 : matching (invRel R) B A
⊢ fcnl_on (compRel (invRel R) (invRel S)) C
Theorem: HTPI.comp_match
Proof state before:
case right.right
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
h3 : matching (invRel R) B A
⊢ fcnl_on (compRel (invRel R) (invRel S)) C
Tactic:
have h4 : matching (invRel S) C B := inv_match h2
Proof state after:
case right.right
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
h3 : matching (invRel R) B A
h4 : matching (invRel S) C B
⊢ fcnl_on (compRel (invRel R) (invRel S)) C
Theorem: HTPI.comp_match
Proof state before:
case right.right
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
h3 : matching (invRel R) B A
h4 : matching (invRel S) C B
⊢ fcnl_on (compRel (invRel R) (invRel S)) C
Tactic:
show fcnl_on (compRel (invRel R) (invRel S)) C from comp_fcnl h4 h3
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_3_3
Proof state before:
U V W : Type
A : Set U
B : Set V
C : Set W
h1 : A ∼ B
h2 : B ∼ C
⊢ A ∼ C
Tactic:
obtain (R : Rel U V) (h3 : matching R A B) from h1
Proof state after:
U V W : Type
A : Set U
B : Set V
C : Set W
h1 : A ∼ B
h2 : B ∼ C
R : Rel U V
h3 : matching R A B
⊢ A ∼ C
Theorem: HTPI.Theorem_8_1_3_3
Proof state before:
U V W : Type
A : Set U
B : Set V
C : Set W
h1 : A ∼ B
h2 : B ∼ C
R : Rel U V
h3 : matching R A B
⊢ A ∼ C
Tactic:
obtain (S : Rel V W) (h4 : matching S B C) from h2
Proof state after:
U V W : Type
A : Set U
B : Set V
C : Set W
h1 : A ∼ B
h2 : B ∼ C
R : Rel U V
h3 : matching R A B
S : Rel V W
h4 : matching S B C
⊢ A ∼ C
Theorem: HTPI.Theorem_8_1_3_3
Proof state before:
U V W : Type
A : Set U
B : Set V
C : Set W
h1 : A ∼ B
h2 : B ∼ C
R : Rel U V
h3 : matching R A B
S : Rel V W
h4 : matching S B C
⊢ A ∼ C
Tactic:
apply Exists.intro (compRel S R)
Proof state after:
U V W : Type
A : Set U
B : Set V
C : Set W
h1 : A ∼ B
h2 : B ∼ C
R : Rel U V
h3 : matching R A B
S : Rel V W
h4 : matching S B C
⊢ matching (compRel S R) A C
Theorem: HTPI.Theorem_8_1_3_3
Proof state before:
U V W : Type
A : Set U
B : Set V
C : Set W
h1 : A ∼ B
h2 : B ∼ C
R : Rel U V
h3 : matching R A B
S : Rel V W
h4 : matching S B C
⊢ matching (compRel S R) A C
Tactic:
show matching (compRel S R) A C from comp_match h3 h4
Proof state after:
no goals
Theorem: HTPI.I_def
Proof state before:
k n : ℕ
⊢ k ∈ I n ↔ k < n
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.denum_def
Proof state before:
U : Type
A : Set U
⊢ denum A ↔ Univ ℕ ∼ A
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.numElts_def
Proof state before:
U : Type
A : Set U
n : ℕ
⊢ numElts A n ↔ I n ∼ A
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.finite_def
Proof state before:
U : Type
A : Set U
⊢ finite A ↔ ∃ n, numElts A n
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.fcnl_on_empty
Proof state before:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
⊢ fcnl_on R A
Tactic:
define
Proof state after:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
Theorem: HTPI.fcnl_on_empty
Proof state before:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
Tactic:
fix a : U
Proof state after:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
a : U
⊢ a ∈ A → ∃! y, R a y
Theorem: HTPI.fcnl_on_empty
Proof state before:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
a : U
⊢ a ∈ A → ∃! y, R a y
Tactic:
assume h2 : a ∈ A
Proof state after:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
a : U
h2 : a ∈ A
⊢ ∃! y, R a y
Theorem: HTPI.fcnl_on_empty
Proof state before:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
a : U
h2 : a ∈ A
⊢ ∃! y, R a y
Tactic:
contradict h1 with h3
Proof state after:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
a : U
h2 : a ∈ A
h3 : ¬∃! y, R a y
⊢ ∃ x, x ∈ A
Theorem: HTPI.fcnl_on_empty
Proof state before:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
a : U
h2 : a ∈ A
h3 : ¬∃! y, R a y
⊢ ∃ x, x ∈ A
Tactic:
show ∃ (x : U), x ∈ A from Exists.intro a h2
Proof state after:
no goals
Theorem: HTPI.empty_match
Proof state before:
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ matching (emptyRel U V) A B
Tactic:
define
Proof state after:
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ rel_within (emptyRel U V) A B ∧ fcnl_on (emptyRel U V) A ∧ fcnl_on (invRel (emptyRel U V)) B
Theorem: HTPI.empty_match
Proof state before:
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ rel_within (emptyRel U V) A B ∧ fcnl_on (emptyRel U V) A ∧ fcnl_on (invRel (emptyRel U V)) B
Tactic:
apply And.intro
Proof state after:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ rel_within (emptyRel U V) A B

case right
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ fcnl_on (emptyRel U V) A ∧ fcnl_on (invRel (emptyRel U V)) B
Theorem: HTPI.empty_match
Proof state before:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ rel_within (emptyRel U V) A B
Tactic:
define
Proof state after:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ ∀ ⦃x : U⦄ ⦃y : V⦄, emptyRel U V x y → x ∈ A ∧ y ∈ B
Theorem: HTPI.empty_match
Proof state before:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ ∀ ⦃x : U⦄ ⦃y : V⦄, emptyRel U V x y → x ∈ A ∧ y ∈ B
Tactic:
fix a : U
Proof state after:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
⊢ ∀ ⦃y : V⦄, emptyRel U V a y → a ∈ A ∧ y ∈ B
Theorem: HTPI.empty_match
Proof state before:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
⊢ ∀ ⦃y : V⦄, emptyRel U V a y → a ∈ A ∧ y ∈ B
Tactic:
fix b : V
Proof state after:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
b : V
⊢ emptyRel U V a b → a ∈ A ∧ b ∈ B
Theorem: HTPI.empty_match
Proof state before:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
b : V
⊢ emptyRel U V a b → a ∈ A ∧ b ∈ B
Tactic:
assume h3 : emptyRel U V a b
Proof state after:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
b : V
h3 : emptyRel U V a b
⊢ a ∈ A ∧ b ∈ B
Theorem: HTPI.empty_match
Proof state before:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
b : V
h3 : emptyRel U V a b
⊢ a ∈ A ∧ b ∈ B
Tactic:
by_contra h4
Proof state after:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
b : V
h3 : emptyRel U V a b
h4 : ¬(a ∈ A ∧ b ∈ B)
⊢ False
Theorem: HTPI.empty_match
Proof state before:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
b : V
h3 : emptyRel U V a b
h4 : ¬(a ∈ A ∧ b ∈ B)
⊢ False
Tactic:
define at h3
Proof state after:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
b : V
h3 : False
h4 : ¬(a ∈ A ∧ b ∈ B)
⊢ False
Theorem: HTPI.empty_match
Proof state before:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
b : V
h3 : False
h4 : ¬(a ∈ A ∧ b ∈ B)
⊢ False
Tactic:
show False from h3
Proof state after:
no goals
Theorem: HTPI.empty_match
Proof state before:
case right
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ fcnl_on (emptyRel U V) A ∧ fcnl_on (invRel (emptyRel U V)) B
Tactic:
apply And.intro
Proof state after:
case right.left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ fcnl_on (emptyRel U V) A

case right.right
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ fcnl_on (invRel (emptyRel U V)) B
Theorem: HTPI.empty_match
Proof state before:
case right.left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ fcnl_on (emptyRel U V) A
Tactic:
show fcnl_on (emptyRel U V) A from fcnl_on_empty (emptyRel U V) h1
Proof state after:
no goals
Theorem: HTPI.empty_match
Proof state before:
case right.right
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ fcnl_on (invRel (emptyRel U V)) B
Tactic:
show fcnl_on (invRel (emptyRel U V)) B from
  fcnl_on_empty (invRel (emptyRel U V)) h2
Proof state after:
no goals
Theorem: HTPI.I_0_empty
Proof state before:
⊢ empty (I 0)
Tactic:
define
Proof state after:
⊢ ¬∃ x, x ∈ I 0
Theorem: HTPI.I_0_empty
Proof state before:
⊢ ¬∃ x, x ∈ I 0
Tactic:
by_contra h1
Proof state after:
h1 : ∃ x, x ∈ I 0
⊢ False
Theorem: HTPI.I_0_empty
Proof state before:
h1 : ∃ x, x ∈ I 0
⊢ False
Tactic:
obtain (x : Nat) (h2 : x ∈ I 0) from h1
Proof state after:
h1 : ∃ x, x ∈ I 0
x : ℕ
h2 : x ∈ I 0
⊢ False
Theorem: HTPI.I_0_empty
Proof state before:
h1 : ∃ x, x ∈ I 0
x : ℕ
h2 : x ∈ I 0
⊢ False
Tactic:
define at h2
Proof state after:
h1 : ∃ x, x ∈ I 0
x : ℕ
h2 : x < 0
⊢ False
Theorem: HTPI.I_0_empty
Proof state before:
h1 : ∃ x, x ∈ I 0
x : ℕ
h2 : x < 0
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.zero_elts_iff_empty
Proof state before:
U : Type
A : Set U
⊢ numElts A 0 ↔ empty A
Tactic:
apply Iff.intro
Proof state after:
case mp
U : Type
A : Set U
⊢ numElts A 0 → empty A

case mpr
U : Type
A : Set U
⊢ empty A → numElts A 0
Theorem: HTPI.zero_elts_iff_empty
Proof state before:
case mp
U : Type
A : Set U
⊢ numElts A 0 → empty A
Tactic:
assume h1 : numElts A 0
Proof state after:
case mp
U : Type
A : Set U
h1 : numElts A 0
⊢ empty A
Theorem: HTPI.zero_elts_iff_empty
Proof state before:
case mp
U : Type
A : Set U
h1 : numElts A 0
⊢ empty A
Tactic:
define
Proof state after:
case mp
U : Type
A : Set U
h1 : numElts A 0
⊢ ¬∃ x, x ∈ A
Theorem: HTPI.zero_elts_iff_empty
Proof state before:
case mp
U : Type
A : Set U
h1 : numElts A 0
⊢ ¬∃ x, x ∈ A
Tactic:
by_contra h2
Proof state after:
case mp
U : Type
A : Set U
h1 : numElts A 0
h2 : ∃ x, x ∈ A
⊢ False
Theorem: HTPI.zero_elts_iff_empty
Proof state before:
case mp
U : Type
A : Set U
h1 : numElts A 0
h2 : ∃ x, x ∈ A
⊢ False
Tactic:
obtain (x : U) (h3 : x ∈ A) from h2
Proof state after:
case mp
U : Type
A : Set U
h1 : numElts A 0
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
⊢ False
Theorem: HTPI.zero_elts_iff_empty
Proof state before:
case mp
U : Type
A : Set U
h1 : numElts A 0
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
⊢ False
Tactic:
define at h1
Proof state after:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
⊢ False
Theorem: HTPI.zero_elts_iff_empty
Proof state before:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
⊢ False
Tactic:
obtain (R : Rel Nat U) (h4 : matching R (I 0) A) from h1
Proof state after:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
R : Rel ℕ U
h4 : matching R (I 0) A
⊢ False
Theorem: HTPI.zero_elts_iff_empty
Proof state before:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
R : Rel ℕ U
h4 : matching R (I 0) A
⊢ False
Tactic:
define at h4
Proof state after:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
R : Rel ℕ U
h4 : rel_within R (I 0) A ∧ fcnl_on R (I 0) ∧ fcnl_on (invRel R) A
⊢ False
Theorem: HTPI.zero_elts_iff_empty
Proof state before:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
R : Rel ℕ U
h4 : rel_within R (I 0) A ∧ fcnl_on R (I 0) ∧ fcnl_on (invRel R) A
⊢ False
Tactic:
obtain (j : Nat) (h5 : invRel R x j) from
  fcnl_exists h4.right.right h3
Proof state after:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
R : Rel ℕ U
h4 : rel_within R (I 0) A ∧ fcnl_on R (I 0) ∧ fcnl_on (invRel R) A
j : ℕ
h5 : invRel R x j
⊢ False
Theorem: HTPI.zero_elts_iff_empty
Proof state before:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
R : Rel ℕ U
h4 : rel_within R (I 0) A ∧ fcnl_on R (I 0) ∧ fcnl_on (invRel R) A
j : ℕ
h5 : invRel R x j
⊢ False
Tactic:
define at h5
Proof state after:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
R : Rel ℕ U
h4 : rel_within R (I 0) A ∧ fcnl_on R (I 0) ∧ fcnl_on (invRel R) A
j : ℕ
h5 : R j x
⊢ False
Theorem: HTPI.zero_elts_iff_empty
Proof state before:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
R : Rel ℕ U
h4 : rel_within R (I 0) A ∧ fcnl_on R (I 0) ∧ fcnl_on (invRel R) A
j : ℕ
h5 : R j x
⊢ False
Tactic:
have h6 : j ∈ I 0 ∧ x ∈ A := h4.left h5
Proof state after:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
R : Rel ℕ U
h4 : rel_within R (I 0) A ∧ fcnl_on R (I 0) ∧ fcnl_on (invRel R) A
j : ℕ
h5 : R j x
h6 : j ∈ I 0 ∧ x ∈ A
⊢ False
Theorem: HTPI.zero_elts_iff_empty
Proof state before:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
R : Rel ℕ U
h4 : rel_within R (I 0) A ∧ fcnl_on R (I 0) ∧ fcnl_on (invRel R) A
j : ℕ
h5 : R j x
h6 : j ∈ I 0 ∧ x ∈ A
⊢ False
Tactic:
contradict I_0_empty
Proof state after:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
R : Rel ℕ U
h4 : rel_within R (I 0) A ∧ fcnl_on R (I 0) ∧ fcnl_on (invRel R) A
j : ℕ
h5 : R j x
h6 : j ∈ I 0 ∧ x ∈ A
⊢ ∃ x, x ∈ I 0
Theorem: HTPI.zero_elts_iff_empty
Proof state before:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
R : Rel ℕ U
h4 : rel_within R (I 0) A ∧ fcnl_on R (I 0) ∧ fcnl_on (invRel R) A
j : ℕ
h5 : R j x
h6 : j ∈ I 0 ∧ x ∈ A
⊢ ∃ x, x ∈ I 0
Tactic:
show ∃ (x : Nat), x ∈ I 0 from Exists.intro j h6.left
Proof state after:
no goals