internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof state after:
no goals
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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]
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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)
Proof state after:
no goals
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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)
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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]
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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)
Proof state after:
no goals
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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