internlm/Lean-Github huggingface dataset:
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
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
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
Rab1 : R a b1
⊢ b1 = b2
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
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
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
Rab1 : R a b1
Rab2 : R a b2
⊢ b1 = b2
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
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
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
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
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
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
h5 : a ∉ X
Sab1 : S a b1
⊢ b1 = b2
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
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
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
b1 b2 : V
Tab1 : T a b1
Tab2 : T a b2
h5 : a ∉ X
Sab1 : S a b1
Sab2 : S a b2
⊢ b1 = b2
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
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)
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
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
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
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
Proof state after:
no goals
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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