Theorem: HTPI.comp_fcnl (HTPILib/Chap8Part1.lean)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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