Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem (HTPILib/Chap8Part2.lean)

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
⊢ A ∼ B
Tactic:
obtain (R : Rel U V) (R_match_AD : matching R A D) from h3
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : matching R A D
⊢ A ∼ B

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : matching R A D
⊢ A ∼ B
Tactic:
obtain (S : Rel U V) (S_match_CB : matching S C B) from h4
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : matching R A D
S : Rel U V
S_match_CB : matching S C B
⊢ A ∼ B

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : matching R A D
S : Rel U V
S_match_CB : matching S C B
⊢ A ∼ B
Tactic:
define at R_match_AD
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : matching S C B
⊢ A ∼ B

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : matching S C B
⊢ A ∼ B
Tactic:
define at S_match_CB
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
⊢ A ∼ B

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
⊢ A ∼ B
Tactic:
set X0 : Set U := A \ C
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
⊢ A ∼ B

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
⊢ A ∼ B
Tactic:
set X : Set U := cum_rep_image R S X0
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
⊢ A ∼ B

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
⊢ A ∼ B
Tactic:
set T : Rel U V := csb_match R S X0
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
⊢ A ∼ B

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
⊢ A ∼ B
Tactic:
have Tdef : ∀ (x : U) (y : V),
    T x y ↔ (x ∈ X ∧ R x y) ∨ (x ∉ X ∧ S x y) := by
  fix x : U; fix y : V
  rfl
  done
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
⊢ A ∼ B

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
⊢ A ∼ B
Tactic:
have A_not_X_in_C : A \ X ⊆ C := by
  fix a : U
  assume h5 : a ∈ A \ X
  contradict h5.right with h6  define  apply Exists.intro 0
  define
  show a ∈ A ∧ a ∉ C from And.intro h5.left h6
  done
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ A ∼ B

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ A ∼ B
Tactic:
define
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ ∃ R, matching R A B

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ ∃ R, matching R A B
Tactic:
apply Exists.intro T
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ matching T A B

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ matching T A B
Tactic:
define
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ rel_within T A B ∧ fcnl_on T A ∧ fcnl_on (invRel T) B

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ rel_within T A B ∧ fcnl_on T A ∧ fcnl_on (invRel T) B
Tactic:
apply And.intro
State after:
case left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ rel_within T A B

case right
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ fcnl_on T A ∧ fcnl_on (invRel T) B

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
⊢ ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
Tactic:
fix x : U
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
x : U
⊢ ∀ (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
x : U
⊢ ∀ (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
Tactic:
fix y : V
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
x : U
y : V
⊢ T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
x : U
y : V
⊢ T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
Tactic:
rfl
State after:
no goals

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
⊢ A \ X ⊆ C
Tactic:
fix a : U
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
a : U
⊢ a ∈ A \ X → a ∈ C

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
a : U
⊢ a ∈ A \ X → a ∈ C
Tactic:
assume h5 : a ∈ A \ X
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
a : U
h5 : a ∈ A \ X
⊢ a ∈ C

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
a : U
h5 : a ∈ A \ X
⊢ a ∈ C
Tactic:
contradict h5.right with h6
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
a : U
h5 : a ∈ A \ X
h6 : ¬a ∈ C
⊢ a ∈ X

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
a : U
h5 : a ∈ A \ X
h6 : ¬a ∈ C
⊢ a ∈ X
Tactic:
define
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
a : U
h5 : a ∈ A \ X
h6 : ¬a ∈ C
⊢ ∃ n, a ∈ rep_common_image R S X0 n

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
a : U
h5 : a ∈ A \ X
h6 : ¬a ∈ C
⊢ ∃ n, a ∈ rep_common_image R S X0 n
Tactic:
apply Exists.intro 0
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
a : U
h5 : a ∈ A \ X
h6 : ¬a ∈ C
⊢ a ∈ rep_common_image R S X0 0

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
a : U
h5 : a ∈ A \ X
h6 : ¬a ∈ C
⊢ a ∈ rep_common_image R S X0 0
Tactic:
define
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
a : U
h5 : a ∈ A \ X
h6 : ¬a ∈ C
⊢ a ∈ A ∧ a ∉ C

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
a : U
h5 : a ∈ A \ X
h6 : ¬a ∈ C
⊢ a ∈ A ∧ a ∉ C
Tactic:
show a ∈ A ∧ a ∉ C from And.intro h5.left h6
State after:
no goals

State before:
case left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ rel_within T A B
Tactic:
define
State after:
case left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ ∀ ⦃x : U⦄ ⦃y : V⦄, T x y → x ∈ A ∧ y ∈ B

State before:
case left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ ∀ ⦃x : U⦄ ⦃y : V⦄, T x y → x ∈ A ∧ y ∈ B
Tactic:
fix a : U
State after:
case left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
⊢ ∀ ⦃y : V⦄, T a y → a ∈ A ∧ y ∈ B

State before:
case left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
⊢ ∀ ⦃y : V⦄, T a y → a ∈ A ∧ y ∈ B
Tactic:
fix b : V
State after:
case left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
b : V
⊢ T a b → a ∈ A ∧ b ∈ B

State before:
case left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
b : V
⊢ T a b → a ∈ A ∧ b ∈ B
Tactic:
assume h5 : T a b
State after:
case left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
b : V
h5 : T a b
⊢ a ∈ A ∧ b ∈ B

State before:
case left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
b : V
h5 : T a b
⊢ a ∈ A ∧ b ∈ B
Tactic:
rewrite [Tdef] at h5
State after:
case left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
b : V
h5 : a ∈ X ∧ R a b ∨ a ∉ X ∧ S a b
⊢ a ∈ A ∧ b ∈ B

State before:
case left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
b : V
h5 : a ∈ X ∧ R a b ∨ a ∉ X ∧ S a b
⊢ a ∈ A ∧ b ∈ B
Tactic:
by_cases on h5
State after:
case left.Case_1
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
b : V
h5 : a ∈ X ∧ R a b
⊢ a ∈ A ∧ b ∈ B

case left.Case_2
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
b : V
h5 : a ∉ X ∧ S a b
⊢ a ∈ A ∧ b ∈ B

State before:
case left.Case_1
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
b : V
h5 : a ∈ X ∧ R a b
⊢ a ∈ A ∧ b ∈ B
Tactic:
have h6 : a ∈ A ∧ b ∈ D := R_match_AD.left h5.right
State after:
case left.Case_1
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
b : V
h5 : a ∈ X ∧ R a b
h6 : a ∈ A ∧ b ∈ D
⊢ a ∈ A ∧ b ∈ B

State before:
case left.Case_1
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
b : V
h5 : a ∈ X ∧ R a b
h6 : a ∈ A ∧ b ∈ D
⊢ a ∈ A ∧ b ∈ B
Tactic:
show a ∈ A ∧ b ∈ B from And.intro h6.left (h2 h6.right)
State after:
no goals

State before:
case left.Case_2
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
b : V
h5 : a ∉ X ∧ S a b
⊢ a ∈ A ∧ b ∈ B
Tactic:
have h6 : a ∈ C ∧ b ∈ B := S_match_CB.left h5.right
State after:
case left.Case_2
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
b : V
h5 : a ∉ X ∧ S a b
h6 : a ∈ C ∧ b ∈ B
⊢ a ∈ A ∧ b ∈ B

State before:
case left.Case_2
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
b : V
h5 : a ∉ X ∧ S a b
h6 : a ∈ C ∧ b ∈ B
⊢ a ∈ A ∧ b ∈ B
Tactic:
show a ∈ A ∧ b ∈ B from And.intro (h1 h6.left) h6.right
State after:
no goals

State before:
case right
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ fcnl_on T A ∧ fcnl_on (invRel T) B
Tactic:
apply And.intro
State after:
case right.left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ fcnl_on T A

case right.right
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ fcnl_on (invRel T) B

State before:
case right.left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ fcnl_on T A
Tactic:
define
State after:
case right.left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, T x y

State before:
case right.left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, T x y
Tactic:
fix a : U
State after:
case right.left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
⊢ a ∈ A → ∃! y, T a y

State before:
case right.left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
⊢ a ∈ A → ∃! y, T a y
Tactic:
assume aA : a ∈ A
State after:
case right.left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
⊢ ∃! y, T a y

State before:
case right.left
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
⊢ ∃! y, T a y
Tactic:
exists_unique
State after:
case right.left.Existence
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
⊢ ∃ y, T a y

case right.left.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
⊢ ∀ (y_1 y_2 : V), T a y_1 → T a y_2 → y_1 = y_2

State before:
case right.left.Existence
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
⊢ ∃ y, T a y
Tactic:
by_cases h5 : a ∈ X
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∈ X
⊢ ∃ y, T a y

case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∉ X
⊢ ∃ y, T a y

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∈ X
⊢ ∃ y, T a y
Tactic:
obtain (b : V) (Rab : R a b) from
  fcnl_exists R_match_AD.right.left aA
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∈ X
b : V
Rab : R a b
⊢ ∃ y, T a y

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∈ X
b : V
Rab : R a b
⊢ ∃ y, T a y
Tactic:
apply Exists.intro b
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∈ X
b : V
Rab : R a b
⊢ T a b

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∈ X
b : V
Rab : R a b
⊢ T a b
Tactic:
rewrite [Tdef]
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∈ X
b : V
Rab : R a b
⊢ a ∈ X ∧ R a b ∨ a ∉ X ∧ S a b

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∈ X
b : V
Rab : R a b
⊢ a ∈ X ∧ R a b ∨ a ∉ X ∧ S a b
Tactic:
show a ∈ X ∧ R a b ∨ a ∉ X ∧ S a b from
  Or.inl (And.intro h5 Rab)
State after:
no goals

State before:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∉ X
⊢ ∃ y, T a y
Tactic:
have aC : a ∈ C := A_not_X_in_C (And.intro aA h5)
State after:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∉ X
aC : a ∈ C
⊢ ∃ y, T a y

State before:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∉ X
aC : a ∈ C
⊢ ∃ y, T a y
Tactic:
obtain (b : V) (Sab : S a b) from
  fcnl_exists S_match_CB.right.left aC
State after:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∉ X
aC : a ∈ C
b : V
Sab : S a b
⊢ ∃ y, T a y

State before:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∉ X
aC : a ∈ C
b : V
Sab : S a b
⊢ ∃ y, T a y
Tactic:
apply Exists.intro b
State after:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∉ X
aC : a ∈ C
b : V
Sab : S a b
⊢ T a b

State before:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∉ X
aC : a ∈ C
b : V
Sab : S a b
⊢ T a b
Tactic:
rewrite [Tdef]
State after:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∉ X
aC : a ∈ C
b : V
Sab : S a b
⊢ a ∈ X ∧ R a b ∨ a ∉ X ∧ S a b

State before:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
h5 : a ∉ X
aC : a ∈ C
b : V
Sab : S a b
⊢ a ∈ X ∧ R a b ∨ a ∉ X ∧ S a b
Tactic:
show a ∈ X ∧ R a b ∨ a ∉ X ∧ S a b from
  Or.inr (And.intro h5 Sab)
State after:
no goals

State before:
case right.left.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
⊢ ∀ (y_1 y_2 : V), T a y_1 → T a y_2 → y_1 = y_2
Tactic:
fix b1 : V
State after:
case right.left.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 : V
⊢ ∀ (y_2 : V), T a b1 → T a y_2 → b1 = y_2

State before:
case right.left.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 : V
⊢ ∀ (y_2 : V), T a b1 → T a y_2 → b1 = y_2
Tactic:
fix b2 : V
State after:
case right.left.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
⊢ T a b1 → T a b2 → b1 = b2

State before:
case right.left.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
⊢ T a b1 → T a b2 → b1 = b2
Tactic:
assume Tab1 : T a b1
State after:
case right.left.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
⊢ T a b2 → b1 = b2

State before:
case right.left.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
⊢ T a b2 → b1 = b2
Tactic:
assume Tab2 : T a b2
State after:
case right.left.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
⊢ b1 = b2

State before:
case right.left.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
⊢ b1 = b2
Tactic:
by_cases h5 : a ∈ X
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
h5 : a ∈ X
⊢ b1 = b2

case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
h5 : a ∉ X
⊢ b1 = b2

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
h5 : a ∈ X
⊢ b1 = b2
Tactic:
have Rab1 : R a b1 := csb_match_cri Tab1 h5
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
h5 : a ∈ X
Rab1 : R a b1
⊢ b1 = b2

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
h5 : a ∈ X
Rab1 : R a b1
⊢ b1 = b2
Tactic:
have Rab2 : R a b2 := csb_match_cri Tab2 h5
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
h5 : a ∈ X
Rab1 : R a b1
Rab2 : R a b2
⊢ b1 = b2

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
h5 : a ∈ X
Rab1 : R a b1
Rab2 : R a b2
⊢ b1 = b2
Tactic:
show b1 = b2 from
  fcnl_unique R_match_AD.right.left aA Rab1 Rab2
State after:
no goals

State before:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
h5 : a ∉ X
⊢ b1 = b2
Tactic:
have Sab1 : S a b1 := csb_match_not_cri Tab1 h5
State after:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
h5 : a ∉ X
Sab1 : S a b1
⊢ b1 = b2

State before:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
h5 : a ∉ X
Sab1 : S a b1
⊢ b1 = b2
Tactic:
have Sab2 : S a b2 := csb_match_not_cri Tab2 h5
State after:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
h5 : a ∉ X
Sab1 : S a b1
Sab2 : S a b2
⊢ b1 = b2

State before:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
h5 : a ∉ X
Sab1 : S a b1
Sab2 : S a b2
⊢ b1 = b2
Tactic:
have aC : a ∈ C := A_not_X_in_C (And.intro aA h5)
State after:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
h5 : a ∉ X
Sab1 : S a b1
Sab2 : S a b2
aC : a ∈ C
⊢ b1 = b2

State before:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
a : U
aA : a ∈ A
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
h5 : a ∉ X
Sab1 : S a b1
Sab2 : S a b2
aC : a ∈ C
⊢ b1 = b2
Tactic:
show b1 = b2 from
  fcnl_unique S_match_CB.right.left aC Sab1 Sab2
State after:
no goals

State before:
case right.right
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ fcnl_on (invRel T) B
Tactic:
define
State after:
case right.right
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ ∀ ⦃x : V⦄, x ∈ B → ∃! y, invRel T x y

State before:
case right.right
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
⊢ ∀ ⦃x : V⦄, x ∈ B → ∃! y, invRel T x y
Tactic:
fix b : V
State after:
case right.right
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
⊢ b ∈ B → ∃! y, invRel T b y

State before:
case right.right
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
⊢ b ∈ B → ∃! y, invRel T b y
Tactic:
assume bB : b ∈ B
State after:
case right.right
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
⊢ ∃! y, invRel T b y

State before:
case right.right
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
⊢ ∃! y, invRel T b y
Tactic:
obtain (c : U) (Scb : S c b) from
  fcnl_exists S_match_CB.right.right bB
State after:
case right.right
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
⊢ ∃! y, invRel T b y

State before:
case right.right
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
⊢ ∃! y, invRel T b y
Tactic:
have cC : c ∈ C := (S_match_CB.left Scb).left
State after:
case right.right
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
⊢ ∃! y, invRel T b y

State before:
case right.right
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
⊢ ∃! y, invRel T b y
Tactic:
exists_unique
State after:
case right.right.Existence
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
⊢ ∃ y, invRel T b y

case right.right.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
⊢ ∀ (y_1 y_2 : U), invRel T b y_1 → invRel T b y_2 → y_1 = y_2

State before:
case right.right.Existence
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
⊢ ∃ y, invRel T b y
Tactic:
by_cases h5 : c ∈ X
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : c ∈ X
⊢ ∃ y, invRel T b y

case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : c ∉ X
⊢ ∃ y, invRel T b y

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : c ∈ X
⊢ ∃ y, invRel T b y
Tactic:
define at h5
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
⊢ ∃ y, invRel T b y

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
⊢ ∃ y, invRel T b y
Tactic:
obtain (n : Nat) (h6 : c ∈ rep_common_image R S X0 n) from h5
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h6 : c ∈ rep_common_image R S X0 n
⊢ ∃ y, invRel T b y

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h6 : c ∈ rep_common_image R S X0 n
⊢ ∃ y, invRel T b y
Tactic:
have h7 : n ≠ 0 := by
  by_contra h7
  rewrite [h7] at h6
  define at h6       show False from h6.right cC
  done
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h6 : c ∈ rep_common_image R S X0 n
h7 : n ≠ 0
⊢ ∃ y, invRel T b y

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h6 : c ∈ rep_common_image R S X0 n
h7 : n ≠ 0
⊢ ∃ y, invRel T b y
Tactic:
obtain (m : Nat) (h8 : n = m + 1) from
  exists_eq_add_one_of_ne_zero h7
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h6 : c ∈ rep_common_image R S X0 n
h7 : n ≠ 0
m : ℕ
h8 : n = m + 1
⊢ ∃ y, invRel T b y

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h6 : c ∈ rep_common_image R S X0 n
h7 : n ≠ 0
m : ℕ
h8 : n = m + 1
⊢ ∃ y, invRel T b y
Tactic:
rewrite [h8] at h6
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : c ∈ rep_common_image R S X0 (m + 1)
h8 : n = m + 1
⊢ ∃ y, invRel T b y

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : c ∈ rep_common_image R S X0 (m + 1)
h8 : n = m + 1
⊢ ∃ y, invRel T b y
Tactic:
rewrite [rep_common_image_step] at h6
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
⊢ ∃ y, invRel T b y

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
⊢ ∃ y, invRel T b y
Tactic:
obtain (a : U) (h9 : a ∈ rep_common_image R S X0 m ∧
  ∃ (y : V), R a y ∧ S c y) from h6
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
⊢ ∃ y, invRel T b y

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
⊢ ∃ y, invRel T b y
Tactic:
apply Exists.intro a
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
⊢ invRel T b a

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
⊢ invRel T b a
Tactic:
rewrite [invRel_def, Tdef]
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
⊢ a ∈ X ∧ R a b ∨ a ∉ X ∧ S a b

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
⊢ a ∈ X ∧ R a b ∨ a ∉ X ∧ S a b
Tactic:
apply Or.inl
State after:
case pos.h
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
⊢ a ∈ X ∧ R a b

State before:
case pos.h
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
⊢ a ∈ X ∧ R a b
Tactic:
obtain (y : V) (h10 : R a y ∧ S c y) from h9.right
State after:
case pos.h
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
y : V
h10 : R a y ∧ S c y
⊢ a ∈ X ∧ R a b

State before:
case pos.h
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
y : V
h10 : R a y ∧ S c y
⊢ a ∈ X ∧ R a b
Tactic:
have h11 : y = b :=
  fcnl_unique S_match_CB.right.left cC h10.right Scb
State after:
case pos.h
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
y : V
h10 : R a y ∧ S c y
h11 : y = b
⊢ a ∈ X ∧ R a b

State before:
case pos.h
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
y : V
h10 : R a y ∧ S c y
h11 : y = b
⊢ a ∈ X ∧ R a b
Tactic:
rewrite [h11] at h10
State after:
case pos.h
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
y : V
h10 : R a b ∧ S c b
h11 : y = b
⊢ a ∈ X ∧ R a b

State before:
case pos.h
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
y : V
h10 : R a b ∧ S c b
h11 : y = b
⊢ a ∈ X ∧ R a b
Tactic:
apply And.intro _ h10.left
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
y : V
h10 : R a b ∧ S c b
h11 : y = b
⊢ a ∈ X

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
y : V
h10 : R a b ∧ S c b
h11 : y = b
⊢ a ∈ X
Tactic:
define
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
y : V
h10 : R a b ∧ S c b
h11 : y = b
⊢ ∃ n, a ∈ rep_common_image R S X0 n

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h7 : n ≠ 0
m : ℕ
h6 : ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S c y
h8 : n = m + 1
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
y : V
h10 : R a b ∧ S c b
h11 : y = b
⊢ ∃ n, a ∈ rep_common_image R S X0 n
Tactic:
show ∃ (n : Nat), a ∈ rep_common_image R S X0 n from
  Exists.intro m h9.left
State after:
no goals

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h6 : c ∈ rep_common_image R S X0 n
⊢ n ≠ 0
Tactic:
by_contra h7
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h6 : c ∈ rep_common_image R S X0 n
h7 : n = 0
⊢ False

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h6 : c ∈ rep_common_image R S X0 n
h7 : n = 0
⊢ False
Tactic:
rewrite [h7] at h6
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h6 : c ∈ rep_common_image R S X0 0
h7 : n = 0
⊢ False

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h6 : c ∈ rep_common_image R S X0 0
h7 : n = 0
⊢ False
Tactic:
define at h6
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h6 : c ∈ A ∧ c ∉ C
h7 : n = 0
⊢ False

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : ∃ n, c ∈ rep_common_image R S X0 n
n : ℕ
h6 : c ∈ A ∧ c ∉ C
h7 : n = 0
⊢ False
Tactic:
show False from h6.right cC
State after:
no goals

State before:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : c ∉ X
⊢ ∃ y, invRel T b y
Tactic:
apply Exists.intro c
State after:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : c ∉ X
⊢ invRel T b c

State before:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : c ∉ X
⊢ invRel T b c
Tactic:
rewrite [invRel_def, Tdef]
State after:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : c ∉ X
⊢ c ∈ X ∧ R c b ∨ c ∉ X ∧ S c b

State before:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : c ∉ X
⊢ c ∈ X ∧ R c b ∨ c ∉ X ∧ S c b
Tactic:
show c ∈ X ∧ R c b ∨ c ∉ X ∧ S c b from
  Or.inr (And.intro h5 Scb)
State after:
no goals

State before:
case right.right.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
⊢ ∀ (y_1 y_2 : U), invRel T b y_1 → invRel T b y_2 → y_1 = y_2
Tactic:
fix a1 : U
State after:
case right.right.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 : U
⊢ ∀ (y_2 : U), invRel T b a1 → invRel T b y_2 → a1 = y_2

State before:
case right.right.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 : U
⊢ ∀ (y_2 : U), invRel T b a1 → invRel T b y_2 → a1 = y_2
Tactic:
fix a2 : U
State after:
case right.right.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
⊢ invRel T b a1 → invRel T b a2 → a1 = a2

State before:
case right.right.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
⊢ invRel T b a1 → invRel T b a2 → a1 = a2
Tactic:
assume Ta1b : T a1 b
State after:
case right.right.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
⊢ invRel T b a2 → a1 = a2

State before:
case right.right.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
⊢ invRel T b a2 → a1 = a2
Tactic:
assume Ta2b : T a2 b
State after:
case right.right.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
⊢ a1 = a2

State before:
case right.right.Uniqueness
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
⊢ a1 = a2
Tactic:
by_cases h5 : a1 ∈ X
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∈ X
⊢ a1 = a2

case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∉ X
⊢ a1 = a2

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∈ X
⊢ a1 = a2
Tactic:
have h6 : a2 ∈ X := csb_cri_of_cri Ta1b Ta2b h5
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∈ X
h6 : a2 ∈ X
⊢ a1 = a2

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∈ X
h6 : a2 ∈ X
⊢ a1 = a2
Tactic:
have Ra1b : R a1 b := csb_match_cri Ta1b h5
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∈ X
h6 : a2 ∈ X
Ra1b : R a1 b
⊢ a1 = a2

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∈ X
h6 : a2 ∈ X
Ra1b : R a1 b
⊢ a1 = a2
Tactic:
have Ra2b : R a2 b := csb_match_cri Ta2b h6
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∈ X
h6 : a2 ∈ X
Ra1b : R a1 b
Ra2b : R a2 b
⊢ a1 = a2

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∈ X
h6 : a2 ∈ X
Ra1b : R a1 b
Ra2b : R a2 b
⊢ a1 = a2
Tactic:
have h7 : b ∈ D := (R_match_AD.left Ra1b).right
State after:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∈ X
h6 : a2 ∈ X
Ra1b : R a1 b
Ra2b : R a2 b
h7 : b ∈ D
⊢ a1 = a2

State before:
case pos
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∈ X
h6 : a2 ∈ X
Ra1b : R a1 b
Ra2b : R a2 b
h7 : b ∈ D
⊢ a1 = a2
Tactic:
show a1 = a2 from
  fcnl_unique R_match_AD.right.right h7 Ra1b Ra2b
State after:
no goals

State before:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∉ X
⊢ a1 = a2
Tactic:
have h6 : a2 ∉ X := by
  by_contra h6
  show False from h5 (csb_cri_of_cri Ta2b Ta1b h6)
  done
State after:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∉ X
h6 : a2 ∉ X
⊢ a1 = a2

State before:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∉ X
h6 : a2 ∉ X
⊢ a1 = a2
Tactic:
have Sa1b : S a1 b := csb_match_not_cri Ta1b h5
State after:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∉ X
h6 : a2 ∉ X
Sa1b : S a1 b
⊢ a1 = a2

State before:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∉ X
h6 : a2 ∉ X
Sa1b : S a1 b
⊢ a1 = a2
Tactic:
have Sa2b : S a2 b := csb_match_not_cri Ta2b h6
State after:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∉ X
h6 : a2 ∉ X
Sa1b : S a1 b
Sa2b : S a2 b
⊢ a1 = a2

State before:
case neg
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∉ X
h6 : a2 ∉ X
Sa1b : S a1 b
Sa2b : S a2 b
⊢ a1 = a2
Tactic:
show a1 = a2 from
  fcnl_unique S_match_CB.right.right bB Sa1b Sa2b
State after:
no goals

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∉ X
⊢ a2 ∉ X
Tactic:
by_contra h6
State after:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∉ X
h6 : a2 ∈ X
⊢ False

State before:
U V : Type
A C : Set U
B D : Set V
h1 : C ⊆ A
h2 : D ⊆ B
h3 : A ∼ D
h4 : C ∼ B
R : Rel U V
R_match_AD : rel_within R A D ∧ fcnl_on R A ∧ fcnl_on (invRel R) D
S : Rel U V
S_match_CB : rel_within S C B ∧ fcnl_on S C ∧ fcnl_on (invRel S) B
X0 : Set U := A \ C
X : Set U := cum_rep_image R S X0
T : Rel U V := csb_match R S X0
Tdef : ∀ (x : U) (y : V), T x y ↔ x ∈ X ∧ R x y ∨ x ∉ X ∧ S x y
A_not_X_in_C : A \ X ⊆ C
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∉ X
h6 : a2 ∈ X
⊢ False
Tactic:
show False from h5 (csb_cri_of_cri Ta2b Ta1b h6)
State after:
no goals