internlm/Lean-Github huggingface dataset:
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 a2 : U
⊢ invRel T b a1 → invRel T b a2 → a1 = a2
Tactic:
assume Ta1b : T a1 b
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
Ta1b : T a1 b
⊢ invRel T b a2 → a1 = a2
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 a2 : U
Ta1b : T a1 b
⊢ invRel T b a2 → a1 = a2
Tactic:
assume Ta2b : T a2 b
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
Ta1b : T a1 b
Ta2b : T a2 b
⊢ a1 = a2
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 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
⊢ a1 = a2
Tactic:
by_cases h5 : a1 ∈ 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
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
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
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
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
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∈ X
h6 : a2 ∈ X
⊢ a1 = a2
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
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
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
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∈ X
h6 : a2 ∈ X
Ra1b : R a1 b
⊢ a1 = a2
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
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
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
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
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
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
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
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
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
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
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
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
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
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∉ X
h6 : a2 ∉ X
⊢ a1 = a2
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
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
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
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∉ X
h6 : a2 ∉ X
Sa1b : S a1 b
⊢ a1 = a2
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
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
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
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
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
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
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
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∉ X
⊢ a2 ∉ X
Tactic:
by_contra 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
a1 a2 : U
Ta1b : T a1 b
Ta2b : T a2 b
h5 : a1 ∉ X
h6 : a2 ∈ X
⊢ 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
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)
Proof state after:
no goals
Theorem: HTPI.graph_def
Proof state before:
A B : Type
f : A → B
a : A
b : B
⊢ (a, b) ∈ graph f ↔ f a = b
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.func_from_graph_rtl
Proof state before:
A B : Type
F : Set (A × B)
⊢ is_func_graph F → ∃ f, graph f = F
Tactic:
assume h1 : is_func_graph F
Proof state after:
A B : Type
F : Set (A × B)
h1 : is_func_graph F
⊢ ∃ f, graph f = F
Theorem: HTPI.func_from_graph_rtl
Proof state before:
A B : Type
F : Set (A × B)
h1 : is_func_graph F
⊢ ∃ f, graph f = F
Tactic:
define at h1
Proof state after:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
⊢ ∃ f, graph f = F
Theorem: HTPI.func_from_graph_rtl
Proof state before:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
⊢ ∃ f, graph f = F
Tactic:
have h2 : ∀ (x : A), ∃ (y : B), (x, y) ∈ F := by
  fix x : A
  obtain (y : B) (h3 : (x, y) ∈ F)
    (h4 : ∀ (y1 y2 : B), (x, y1) ∈ F → (x, y2) ∈ F → y1 = y2) from h1 x
  show ∃ (y : B), (x, y) ∈ F from Exists.intro y h3
  done
Proof state after:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
⊢ ∃ f, graph f = F
Theorem: HTPI.func_from_graph_rtl
Proof state before:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
⊢ ∃ f, graph f = F
Tactic:
set f : A → B := fun (x : A) => Classical.choose (h2 x)
Proof state after:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
⊢ ∃ f, graph f = F
Theorem: HTPI.func_from_graph_rtl
Proof state before:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
⊢ ∃ f, graph f = F
Tactic:
apply Exists.intro f
Proof state after:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
⊢ graph f = F
Theorem: HTPI.func_from_graph_rtl
Proof state before:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
⊢ graph f = F
Tactic:
apply Set.ext
Proof state after:
case h
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
⊢ ∀ (x : A × B), x ∈ graph f ↔ x ∈ F
Theorem: HTPI.func_from_graph_rtl
Proof state before:
case h
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
⊢ ∀ (x : A × B), x ∈ graph f ↔ x ∈ F
Tactic:
fix (x, y) : A × B
Proof state after:
case h
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
⊢ (x, y) ∈ graph f ↔ (x, y) ∈ F
Theorem: HTPI.func_from_graph_rtl
Proof state before:
case h
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
⊢ (x, y) ∈ graph f ↔ (x, y) ∈ F
Tactic:
have h3 : (x, f x) ∈ F := Classical.choose_spec (h2 x)
Proof state after:
case h
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
⊢ (x, y) ∈ graph f ↔ (x, y) ∈ F
Theorem: HTPI.func_from_graph_rtl
Proof state before:
case h
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
⊢ (x, y) ∈ graph f ↔ (x, y) ∈ F
Tactic:
apply Iff.intro
Proof state after:
case h.mp
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
⊢ (x, y) ∈ graph f → (x, y) ∈ F

case h.mpr
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
⊢ (x, y) ∈ F → (x, y) ∈ graph f
Theorem: HTPI.func_from_graph_rtl
Proof state before:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
⊢ ∀ (x : A), ∃ y, (x, y) ∈ F
Tactic:
fix x : A
Proof state after:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
x : A
⊢ ∃ y, (x, y) ∈ F
Theorem: HTPI.func_from_graph_rtl
Proof state before:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
x : A
⊢ ∃ y, (x, y) ∈ F
Tactic:
obtain (y : B) (h3 : (x, y) ∈ F)
  (h4 : ∀ (y1 y2 : B), (x, y1) ∈ F → (x, y2) ∈ F → y1 = y2) from h1 x
Proof state after:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
x : A
y : B
h3 : (x, y) ∈ F
h4 : ∀ (y_1 y_2 : B), (x, y_1) ∈ F → (x, y_2) ∈ F → y_1 = y_2
⊢ ∃ y, (x, y) ∈ F
Theorem: HTPI.func_from_graph_rtl
Proof state before:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
x : A
y : B
h3 : (x, y) ∈ F
h4 : ∀ (y_1 y_2 : B), (x, y_1) ∈ F → (x, y_2) ∈ F → y_1 = y_2
⊢ ∃ y, (x, y) ∈ F
Tactic:
show ∃ (y : B), (x, y) ∈ F from Exists.intro y h3
Proof state after:
no goals
Theorem: HTPI.func_from_graph_rtl
Proof state before:
case h.mp
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
⊢ (x, y) ∈ graph f → (x, y) ∈ F
Tactic:
assume h4 : (x, y) ∈ graph f
Proof state after:
case h.mp
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : (x, y) ∈ graph f
⊢ (x, y) ∈ F
Theorem: HTPI.func_from_graph_rtl
Proof state before:
case h.mp
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : (x, y) ∈ graph f
⊢ (x, y) ∈ F
Tactic:
define at h4
Proof state after:
case h.mp
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : f x = y
⊢ (x, y) ∈ F
Theorem: HTPI.func_from_graph_rtl
Proof state before:
case h.mp
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : f x = y
⊢ (x, y) ∈ F
Tactic:
rewrite [h4] at h3
Proof state after:
case h.mp
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, y) ∈ F
h4 : f x = y
⊢ (x, y) ∈ F
Theorem: HTPI.func_from_graph_rtl
Proof state before:
case h.mp
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, y) ∈ F
h4 : f x = y
⊢ (x, y) ∈ F
Tactic:
show (x, y) ∈ F from h3
Proof state after:
no goals
Theorem: HTPI.func_from_graph_rtl
Proof state before:
case h.mpr
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
⊢ (x, y) ∈ F → (x, y) ∈ graph f
Tactic:
assume h4 : (x, y) ∈ F
Proof state after:
case h.mpr
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : (x, y) ∈ F
⊢ (x, y) ∈ graph f