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
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
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
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
⊢ ∃ 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 : ∃ 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
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
a : U
h9 : a ∈ rep_common_image R S X0 m ∧ ∃ y, R a y ∧ S c y
⊢ invRel T b a
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 : ∃ 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]
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
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
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 : ∃ 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof state after:
no goals
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
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
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
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
b : V
bB : b ∈ B
c : U
Scb : S c b
cC : c ∈ C
h5 : c ∉ X
⊢ invRel T b c
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
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]
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
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
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
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)
Proof state after:
no goals
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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
Theorem: HTPI.Cantor_Schroeder_Bernstein_theorem
Proof 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
Proof 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