internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Cantor's_theorem
Proof state before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
⊢ False
Tactic:
have h3 : unique_val_on_N R := h2.left
Proof state after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
⊢ False
Theorem: HTPI.Cantor's_theorem
Proof state before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
⊢ False
Tactic:
have h4 : nat_rel_onto R (𝒫 (Univ Nat)) := h2.right
Proof state after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : nat_rel_onto R (𝒫 Univ ℕ)
⊢ False
Theorem: HTPI.Cantor's_theorem
Proof state before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : nat_rel_onto R (𝒫 Univ ℕ)
⊢ False
Tactic:
set D : Set Nat := {n : Nat | ∃ (X : Set Nat), R n X ∧ n ∉ X}
Proof state after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : nat_rel_onto R (𝒫 Univ ℕ)
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
⊢ False
Theorem: HTPI.Cantor's_theorem
Proof state before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : nat_rel_onto R (𝒫 Univ ℕ)
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
⊢ False
Tactic:
have h5 : D ∈ 𝒫 (Univ Nat) := set_elt_powerset_univ D
Proof state after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : nat_rel_onto R (𝒫 Univ ℕ)
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
⊢ False
Theorem: HTPI.Cantor's_theorem
Proof state before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : nat_rel_onto R (𝒫 Univ ℕ)
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
⊢ False
Tactic:
define at h4
Proof state after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
⊢ False
Theorem: HTPI.Cantor's_theorem
Proof state before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
⊢ False
Tactic:
obtain (n : Nat) (h6 : R n D) from h4 h5
Proof state after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
⊢ False
Theorem: HTPI.Cantor's_theorem
Proof state before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
⊢ False
Tactic:
by_cases h7 : n ∈ D
Proof state after:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∈ D
⊢ False

case neg
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∉ D
⊢ False
Theorem: HTPI.Cantor's_theorem
Proof state before:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∈ D
⊢ False
Tactic:
contradict h7
Proof state after:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∈ D
⊢ n ∉ D
Theorem: HTPI.Cantor's_theorem
Proof state before:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∈ D
⊢ n ∉ D
Tactic:
define at h7
Proof state after:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
⊢ n ∉ D
Theorem: HTPI.Cantor's_theorem
Proof state before:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
⊢ n ∉ D
Tactic:
obtain (X : Set Nat) (h8 : R n X ∧ n ∉ X) from h7
Proof state after:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
X : Set ℕ
h8 : R n X ∧ n ∉ X
⊢ n ∉ D
Theorem: HTPI.Cantor's_theorem
Proof state before:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
X : Set ℕ
h8 : R n X ∧ n ∉ X
⊢ n ∉ D
Tactic:
define at h3
Proof state after:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set ℕ⦄, R n x1 → R n x2 → x1 = x2
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
X : Set ℕ
h8 : R n X ∧ n ∉ X
⊢ n ∉ D
Theorem: HTPI.Cantor's_theorem
Proof state before:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set ℕ⦄, R n x1 → R n x2 → x1 = x2
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
X : Set ℕ
h8 : R n X ∧ n ∉ X
⊢ n ∉ D
Tactic:
have h9 : D = X := h3 h6 h8.left
Proof state after:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set ℕ⦄, R n x1 → R n x2 → x1 = x2
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
X : Set ℕ
h8 : R n X ∧ n ∉ X
h9 : D = X
⊢ n ∉ D
Theorem: HTPI.Cantor's_theorem
Proof state before:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set ℕ⦄, R n x1 → R n x2 → x1 = x2
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
X : Set ℕ
h8 : R n X ∧ n ∉ X
h9 : D = X
⊢ n ∉ D
Tactic:
rewrite [h9]
Proof state after:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set ℕ⦄, R n x1 → R n x2 → x1 = x2
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
X : Set ℕ
h8 : R n X ∧ n ∉ X
h9 : D = X
⊢ n ∉ X
Theorem: HTPI.Cantor's_theorem
Proof state before:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set ℕ⦄, R n x1 → R n x2 → x1 = x2
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
X : Set ℕ
h8 : R n X ∧ n ∉ X
h9 : D = X
⊢ n ∉ X
Tactic:
show n ∉ X from h8.right
Proof state after:
no goals
Theorem: HTPI.Cantor's_theorem
Proof state before:
case neg
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∉ D
⊢ False
Tactic:
contradict h7
Proof state after:
case neg
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∉ D
⊢ n ∈ D
Theorem: HTPI.Cantor's_theorem
Proof state before:
case neg
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∉ D
⊢ n ∈ D
Tactic:
define
Proof state after:
case neg
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∉ D
⊢ ∃ X, R n X ∧ n ∉ X
Theorem: HTPI.Cantor's_theorem
Proof state before:
case neg
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∉ D
⊢ ∃ X, R n X ∧ n ∉ X
Tactic:
show ∃ (X : Set Nat), R n X ∧ n ∉ X from
  Exists.intro D (And.intro h6 h7)
Proof state after:
no goals
Theorem: HTPI.rep_common_image_step
Proof state before:
U V : Type
R S : Rel U V
X0 : Set U
m : ℕ
a : U
⊢ a ∈ rep_common_image R S X0 (m + 1) ↔ ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S a y
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.csb_match_cri
Proof state before:
U V : Type
R S : Rel U V
X0 : Set U
x : U
y : V
h1 : csb_match R S X0 x y
h2 : x ∈ cum_rep_image R S X0
⊢ R x y
Tactic:
by_cases on h1
Proof state after:
case Case_1
U V : Type
R S : Rel U V
X0 : Set U
x : U
y : V
h2 : x ∈ cum_rep_image R S X0
h1 : x ∈ cum_rep_image R S X0 ∧ R x y
⊢ R x y

case Case_2
U V : Type
R S : Rel U V
X0 : Set U
x : U
y : V
h2 : x ∈ cum_rep_image R S X0
h1 : x ∉ cum_rep_image R S X0 ∧ S x y
⊢ R x y
Theorem: HTPI.csb_match_cri
Proof state before:
case Case_1
U V : Type
R S : Rel U V
X0 : Set U
x : U
y : V
h2 : x ∈ cum_rep_image R S X0
h1 : x ∈ cum_rep_image R S X0 ∧ R x y
⊢ R x y
Tactic:
show R x y from h1.right
Proof state after:
no goals
Theorem: HTPI.csb_match_cri
Proof state before:
case Case_2
U V : Type
R S : Rel U V
X0 : Set U
x : U
y : V
h2 : x ∈ cum_rep_image R S X0
h1 : x ∉ cum_rep_image R S X0 ∧ S x y
⊢ R x y
Tactic:
show R x y from absurd h2 h1.left
Proof state after:
no goals
Theorem: HTPI.csb_match_not_cri
Proof state before:
U V : Type
R S : Rel U V
X0 : Set U
x : U
y : V
h1 : csb_match R S X0 x y
h2 : x ∉ cum_rep_image R S X0
⊢ S x y
Tactic:
by_cases on h1
Proof state after:
case Case_1
U V : Type
R S : Rel U V
X0 : Set U
x : U
y : V
h2 : x ∉ cum_rep_image R S X0
h1 : x ∈ cum_rep_image R S X0 ∧ R x y
⊢ S x y

case Case_2
U V : Type
R S : Rel U V
X0 : Set U
x : U
y : V
h2 : x ∉ cum_rep_image R S X0
h1 : x ∉ cum_rep_image R S X0 ∧ S x y
⊢ S x y
Theorem: HTPI.csb_match_not_cri
Proof state before:
case Case_1
U V : Type
R S : Rel U V
X0 : Set U
x : U
y : V
h2 : x ∉ cum_rep_image R S X0
h1 : x ∈ cum_rep_image R S X0 ∧ R x y
⊢ S x y
Tactic:
show S x y from absurd h1.left h2
Proof state after:
no goals
Theorem: HTPI.csb_match_not_cri
Proof state before:
case Case_2
U V : Type
R S : Rel U V
X0 : Set U
x : U
y : V
h2 : x ∉ cum_rep_image R S X0
h1 : x ∉ cum_rep_image R S X0 ∧ S x y
⊢ S x y
Tactic:
show S x y from h1.right
Proof state after:
no goals
Theorem: HTPI.csb_cri_of_cri
Proof state before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
⊢ x2 ∈ cum_rep_image R S X0
Tactic:
have h4 : R x1 y := csb_match_cri h1 h3
Proof state after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
h4 : R x1 y
⊢ x2 ∈ cum_rep_image R S X0
Theorem: HTPI.csb_cri_of_cri
Proof state before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
h4 : R x1 y
⊢ x2 ∈ cum_rep_image R S X0
Tactic:
by_contra h5
Proof state after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
⊢ False
Theorem: HTPI.csb_cri_of_cri
Proof state before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
⊢ False
Tactic:
have h6 : S x2 y := csb_match_not_cri h2 h5
Proof state after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
⊢ False
Theorem: HTPI.csb_cri_of_cri
Proof state before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
⊢ False
Tactic:
contradict h5
Proof state after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
⊢ x2 ∈ cum_rep_image R S X0
Theorem: HTPI.csb_cri_of_cri
Proof state before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
⊢ x2 ∈ cum_rep_image R S X0
Tactic:
define at h3
Proof state after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
⊢ x2 ∈ cum_rep_image R S X0
Theorem: HTPI.csb_cri_of_cri
Proof state before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
⊢ x2 ∈ cum_rep_image R S X0
Tactic:
define
Proof state after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
⊢ ∃ n, x2 ∈ rep_common_image R S X0 n
Theorem: HTPI.csb_cri_of_cri
Proof state before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
⊢ ∃ n, x2 ∈ rep_common_image R S X0 n
Tactic:
obtain (n : Nat) (h7 : x1 ∈ rep_common_image R S X0 n) from h3
Proof state after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ ∃ n, x2 ∈ rep_common_image R S X0 n
Theorem: HTPI.csb_cri_of_cri
Proof state before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ ∃ n, x2 ∈ rep_common_image R S X0 n
Tactic:
apply Exists.intro (n + 1)
Proof state after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ x2 ∈ rep_common_image R S X0 (n + 1)
Theorem: HTPI.csb_cri_of_cri
Proof state before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ x2 ∈ rep_common_image R S X0 (n + 1)
Tactic:
rewrite [rep_common_image_step]
Proof state after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ ∃ x ∈ rep_common_image R S X0 n, ∃ y, R x y ∧ S x2 y
Theorem: HTPI.csb_cri_of_cri
Proof state before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ ∃ x ∈ rep_common_image R S X0 n, ∃ y, R x y ∧ S x2 y
Tactic:
apply Exists.intro x1
Proof state after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ x1 ∈ rep_common_image R S X0 n ∧ ∃ y, R x1 y ∧ S x2 y
Theorem: HTPI.csb_cri_of_cri
Proof state before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ x1 ∈ rep_common_image R S X0 n ∧ ∃ y, R x1 y ∧ S x2 y
Tactic:
apply And.intro h7
Proof state after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ ∃ y, R x1 y ∧ S x2 y
Theorem: HTPI.csb_cri_of_cri
Proof state before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ ∃ y, R x1 y ∧ S x2 y
Tactic:
show ∃ (y : V), R x1 y ∧ S x2 y from Exists.intro y (And.intro h4 h6)
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
⊢ A ∼ B
Tactic:
obtain (R : Rel U V) (R_match_AD : matching R A D) from h3
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 : matching R A D
⊢ A ∼ B
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 : matching R A D
⊢ A ∼ B
Tactic:
obtain (S : Rel U V) (S_match_CB : matching S C B) from h4
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 : matching R A D
S : Rel U V
S_match_CB : matching S C B
⊢ A ∼ B
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 : matching R A D
S : Rel U V
S_match_CB : matching S C B
⊢ A ∼ B
Tactic:
define at R_match_AD
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 : matching S C B
⊢ A ∼ B
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 : matching S C B
⊢ A ∼ B
Tactic:
define at S_match_CB
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
⊢ A ∼ B
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
⊢ A ∼ B
Tactic:
set X0 : Set U := A \ C
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
⊢ A ∼ B
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
⊢ A ∼ B
Tactic:
set X : Set U := cum_rep_image R S X0
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
⊢ A ∼ B
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
⊢ A ∼ B
Tactic:
set T : Rel U V := csb_match R S X0
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
⊢ A ∼ B