internlm/Lean-Github huggingface dataset:
Theorem: HTPI.equinum_image
Proof state before:
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
⊢ A ∼ image f A
Tactic:
define
Proof state after:
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
⊢ ∃ R, matching R A (image f A)
Theorem: HTPI.equinum_image
Proof state before:
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
⊢ ∃ R, matching R A (image f A)
Tactic:
set R : Rel U V := RelWithinFromFunc f A
Proof state after:
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ ∃ R, matching R A (image f A)
Theorem: HTPI.equinum_image
Proof state before:
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ ∃ R, matching R A (image f A)
Tactic:
apply Exists.intro R
Proof state after:
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ matching R A (image f A)
Theorem: HTPI.equinum_image
Proof state before:
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ matching R A (image f A)
Tactic:
define
Proof state after:
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ rel_within R A (image f A) ∧ fcnl_on R A ∧ fcnl_on (invRel R) (image f A)
Theorem: HTPI.equinum_image
Proof state before:
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ rel_within R A (image f A) ∧ fcnl_on R A ∧ fcnl_on (invRel R) (image f A)
Tactic:
apply And.intro
Proof state after:
case left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ rel_within R A (image f A)

case right
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ fcnl_on R A ∧ fcnl_on (invRel R) (image f A)
Theorem: HTPI.equinum_image
Proof state before:
case left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ rel_within R A (image f A)
Tactic:
define
Proof state after:
case left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ ∀ ⦃x : U⦄ ⦃y : V⦄, R x y → x ∈ A ∧ y ∈ image f A
Theorem: HTPI.equinum_image
Proof state before:
case left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ ∀ ⦃x : U⦄ ⦃y : V⦄, R x y → x ∈ A ∧ y ∈ image f A
Tactic:
fix x : U
Proof state after:
case left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
⊢ ∀ ⦃y : V⦄, R x y → x ∈ A ∧ y ∈ image f A
Theorem: HTPI.equinum_image
Proof state before:
case left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
⊢ ∀ ⦃y : V⦄, R x y → x ∈ A ∧ y ∈ image f A
Tactic:
fix y : V
Proof state after:
case left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
y : V
⊢ R x y → x ∈ A ∧ y ∈ image f A
Theorem: HTPI.equinum_image
Proof state before:
case left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
y : V
⊢ R x y → x ∈ A ∧ y ∈ image f A
Tactic:
assume h3 : R x y
Proof state after:
case left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
y : V
h3 : R x y
⊢ x ∈ A ∧ y ∈ image f A
Theorem: HTPI.equinum_image
Proof state before:
case left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
y : V
h3 : R x y
⊢ x ∈ A ∧ y ∈ image f A
Tactic:
define at h3
Proof state after:
case left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
y : V
h3 : x ∈ A ∧ f x = y
⊢ x ∈ A ∧ y ∈ image f A
Theorem: HTPI.equinum_image
Proof state before:
case left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
y : V
h3 : x ∈ A ∧ f x = y
⊢ x ∈ A ∧ y ∈ image f A
Tactic:
apply And.intro h3.left
Proof state after:
case left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
y : V
h3 : x ∈ A ∧ f x = y
⊢ y ∈ image f A
Theorem: HTPI.equinum_image
Proof state before:
case left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
y : V
h3 : x ∈ A ∧ f x = y
⊢ y ∈ image f A
Tactic:
define
Proof state after:
case left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
y : V
h3 : x ∈ A ∧ f x = y
⊢ ∃ x ∈ A, f x = y
Theorem: HTPI.equinum_image
Proof state before:
case left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
y : V
h3 : x ∈ A ∧ f x = y
⊢ ∃ x ∈ A, f x = y
Tactic:
show ∃ x ∈ A, f x = y from Exists.intro x h3
Proof state after:
no goals
Theorem: HTPI.equinum_image
Proof state before:
case right
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ fcnl_on R A ∧ fcnl_on (invRel R) (image f A)
Tactic:
apply And.intro
Proof state after:
case right.left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ fcnl_on R A

case right.right
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ fcnl_on (invRel R) (image f A)
Theorem: HTPI.equinum_image
Proof state before:
case right.left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ fcnl_on R A
Tactic:
define
Proof state after:
case right.left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
Theorem: HTPI.equinum_image
Proof state before:
case right.left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
Tactic:
fix x : U
Proof state after:
case right.left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
⊢ x ∈ A → ∃! y, R x y
Theorem: HTPI.equinum_image
Proof state before:
case right.left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
⊢ x ∈ A → ∃! y, R x y
Tactic:
assume h3 : x ∈ A
Proof state after:
case right.left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
⊢ ∃! y, R x y
Theorem: HTPI.equinum_image
Proof state before:
case right.left
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
⊢ ∃! y, R x y
Tactic:
exists_unique
Proof state after:
case right.left.Existence
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
⊢ ∃ y, R x y

case right.left.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
⊢ ∀ (y_1 y_2 : V), R x y_1 → R x y_2 → y_1 = y_2
Theorem: HTPI.equinum_image
Proof state before:
case right.left.Existence
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
⊢ ∃ y, R x y
Tactic:
apply Exists.intro (f x)
Proof state after:
case right.left.Existence
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
⊢ R x (f x)
Theorem: HTPI.equinum_image
Proof state before:
case right.left.Existence
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
⊢ R x (f x)
Tactic:
define
Proof state after:
case right.left.Existence
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
⊢ x ∈ A ∧ f x = f x
Theorem: HTPI.equinum_image
Proof state before:
case right.left.Existence
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
⊢ x ∈ A ∧ f x = f x
Tactic:
apply And.intro h3
Proof state after:
case right.left.Existence
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
⊢ f x = f x
Theorem: HTPI.equinum_image
Proof state before:
case right.left.Existence
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
⊢ f x = f x
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.equinum_image
Proof state before:
case right.left.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
⊢ ∀ (y_1 y_2 : V), R x y_1 → R x y_2 → y_1 = y_2
Tactic:
fix y1 : V
Proof state after:
case right.left.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
y1 : V
⊢ ∀ (y_2 : V), R x y1 → R x y_2 → y1 = y_2
Theorem: HTPI.equinum_image
Proof state before:
case right.left.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
y1 : V
⊢ ∀ (y_2 : V), R x y1 → R x y_2 → y1 = y_2
Tactic:
fix y2 : V
Proof state after:
case right.left.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
y1 y2 : V
⊢ R x y1 → R x y2 → y1 = y2
Theorem: HTPI.equinum_image
Proof state before:
case right.left.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
y1 y2 : V
⊢ R x y1 → R x y2 → y1 = y2
Tactic:
assume h4 : R x y1
Proof state after:
case right.left.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
y1 y2 : V
h4 : R x y1
⊢ R x y2 → y1 = y2
Theorem: HTPI.equinum_image
Proof state before:
case right.left.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
y1 y2 : V
h4 : R x y1
⊢ R x y2 → y1 = y2
Tactic:
assume h5 : R x y2
Proof state after:
case right.left.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
y1 y2 : V
h4 : R x y1
h5 : R x y2
⊢ y1 = y2
Theorem: HTPI.equinum_image
Proof state before:
case right.left.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
y1 y2 : V
h4 : R x y1
h5 : R x y2
⊢ y1 = y2
Tactic:
define at h4
Proof state after:
case right.left.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
y1 y2 : V
h4 : x ∈ A ∧ f x = y1
h5 : R x y2
⊢ y1 = y2
Theorem: HTPI.equinum_image
Proof state before:
case right.left.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
y1 y2 : V
h4 : x ∈ A ∧ f x = y1
h5 : R x y2
⊢ y1 = y2
Tactic:
define at h5
Proof state after:
case right.left.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
y1 y2 : V
h4 : x ∈ A ∧ f x = y1
h5 : x ∈ A ∧ f x = y2
⊢ y1 = y2
Theorem: HTPI.equinum_image
Proof state before:
case right.left.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
y1 y2 : V
h4 : x ∈ A ∧ f x = y1
h5 : x ∈ A ∧ f x = y2
⊢ y1 = y2
Tactic:
rewrite [h4.right] at h5
Proof state after:
case right.left.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
y1 y2 : V
h4 : x ∈ A ∧ f x = y1
h5 : x ∈ A ∧ y1 = y2
⊢ y1 = y2
Theorem: HTPI.equinum_image
Proof state before:
case right.left.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
x : U
h3 : x ∈ A
y1 y2 : V
h4 : x ∈ A ∧ f x = y1
h5 : x ∈ A ∧ y1 = y2
⊢ y1 = y2
Tactic:
show y1 = y2 from h5.right
Proof state after:
no goals
Theorem: HTPI.equinum_image
Proof state before:
case right.right
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ fcnl_on (invRel R) (image f A)
Tactic:
define
Proof state after:
case right.right
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ ∀ ⦃x : V⦄, x ∈ image f A → ∃! y, invRel R x y
Theorem: HTPI.equinum_image
Proof state before:
case right.right
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
⊢ ∀ ⦃x : V⦄, x ∈ image f A → ∃! y, invRel R x y
Tactic:
fix y : V
Proof state after:
case right.right
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
⊢ y ∈ image f A → ∃! y_1, invRel R y y_1
Theorem: HTPI.equinum_image
Proof state before:
case right.right
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
⊢ y ∈ image f A → ∃! y_1, invRel R y y_1
Tactic:
assume h3 : y ∈ image f A
Proof state after:
case right.right
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
⊢ ∃! y_1, invRel R y y_1
Theorem: HTPI.equinum_image
Proof state before:
case right.right
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
⊢ ∃! y_1, invRel R y y_1
Tactic:
obtain (x : U) (h4 : x ∈ A ∧ f x = y) from h3
Proof state after:
case right.right
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
⊢ ∃! y_1, invRel R y y_1
Theorem: HTPI.equinum_image
Proof state before:
case right.right
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
⊢ ∃! y_1, invRel R y y_1
Tactic:
exists_unique
Proof state after:
case right.right.Existence
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
⊢ ∃ y_1, invRel R y y_1

case right.right.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
⊢ ∀ (y_1 y_2 : U), invRel R y y_1 → invRel R y y_2 → y_1 = y_2
Theorem: HTPI.equinum_image
Proof state before:
case right.right.Existence
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
⊢ ∃ y_1, invRel R y y_1
Tactic:
apply Exists.intro x
Proof state after:
case right.right.Existence
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
⊢ invRel R y x
Theorem: HTPI.equinum_image
Proof state before:
case right.right.Existence
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
⊢ invRel R y x
Tactic:
define
Proof state after:
case right.right.Existence
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
⊢ x ∈ A ∧ f x = y
Theorem: HTPI.equinum_image
Proof state before:
case right.right.Existence
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
⊢ x ∈ A ∧ f x = y
Tactic:
show x ∈ A ∧ f x = y from h4
Proof state after:
no goals
Theorem: HTPI.equinum_image
Proof state before:
case right.right.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
⊢ ∀ (y_1 y_2 : U), invRel R y y_1 → invRel R y y_2 → y_1 = y_2
Tactic:
fix x1 : U
Proof state after:
case right.right.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
x1 : U
⊢ ∀ (y_2 : U), invRel R y x1 → invRel R y y_2 → x1 = y_2
Theorem: HTPI.equinum_image
Proof state before:
case right.right.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
x1 : U
⊢ ∀ (y_2 : U), invRel R y x1 → invRel R y y_2 → x1 = y_2
Tactic:
fix x2 : U
Proof state after:
case right.right.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
x1 x2 : U
⊢ invRel R y x1 → invRel R y x2 → x1 = x2
Theorem: HTPI.equinum_image
Proof state before:
case right.right.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
x1 x2 : U
⊢ invRel R y x1 → invRel R y x2 → x1 = x2
Tactic:
assume h5 : invRel R y x1
Proof state after:
case right.right.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
x1 x2 : U
h5 : invRel R y x1
⊢ invRel R y x2 → x1 = x2
Theorem: HTPI.equinum_image
Proof state before:
case right.right.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
x1 x2 : U
h5 : invRel R y x1
⊢ invRel R y x2 → x1 = x2
Tactic:
assume h6 : invRel R y x2
Proof state after:
case right.right.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
x1 x2 : U
h5 : invRel R y x1
h6 : invRel R y x2
⊢ x1 = x2
Theorem: HTPI.equinum_image
Proof state before:
case right.right.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
x1 x2 : U
h5 : invRel R y x1
h6 : invRel R y x2
⊢ x1 = x2
Tactic:
define at h5
Proof state after:
case right.right.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
x1 x2 : U
h5 : x1 ∈ A ∧ f x1 = y
h6 : invRel R y x2
⊢ x1 = x2
Theorem: HTPI.equinum_image
Proof state before:
case right.right.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
x1 x2 : U
h5 : x1 ∈ A ∧ f x1 = y
h6 : invRel R y x2
⊢ x1 = x2
Tactic:
define at h6
Proof state after:
case right.right.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
x1 x2 : U
h5 : x1 ∈ A ∧ f x1 = y
h6 : x2 ∈ A ∧ f x2 = y
⊢ x1 = x2
Theorem: HTPI.equinum_image
Proof state before:
case right.right.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
x1 x2 : U
h5 : x1 ∈ A ∧ f x1 = y
h6 : x2 ∈ A ∧ f x2 = y
⊢ x1 = x2
Tactic:
rewrite [←h6.right] at h5
Proof state after:
case right.right.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
x1 x2 : U
h5 : x1 ∈ A ∧ f x1 = f x2
h6 : x2 ∈ A ∧ f x2 = y
⊢ x1 = x2
Theorem: HTPI.equinum_image
Proof state before:
case right.right.Uniqueness
U V : Type
A : Set U
B : Set V
f : U → V
h1 : one_one_on f A
h2 : image f A = B
R : Rel U V := RelWithinFromFunc f A
y : V
h3 : y ∈ image f A
x : U
h4 : x ∈ A ∧ f x = y
x1 x2 : U
h5 : x1 ∈ A ∧ f x1 = f x2
h6 : x2 ∈ A ∧ f x2 = y
⊢ x1 = x2
Tactic:
show x1 = x2 from h1 h5.left h6.left h5.right
Proof state after:
no goals
Theorem: HTPI.id_one_one_on
Proof state before:
U : Type
A : Set U
⊢ one_one_on id A
Tactic:
define
Proof state after:
U : Type
A : Set U
⊢ ∀ ⦃x1 x2 : U⦄, x1 ∈ A → x2 ∈ A → id x1 = id x2 → x1 = x2
Theorem: HTPI.id_one_one_on
Proof state before:
U : Type
A : Set U
⊢ ∀ ⦃x1 x2 : U⦄, x1 ∈ A → x2 ∈ A → id x1 = id x2 → x1 = x2
Tactic:
fix x1 : U
Proof state after:
U : Type
A : Set U
x1 : U
⊢ ∀ ⦃x2 : U⦄, x1 ∈ A → x2 ∈ A → id x1 = id x2 → x1 = x2
Theorem: HTPI.id_one_one_on
Proof state before:
U : Type
A : Set U
x1 : U
⊢ ∀ ⦃x2 : U⦄, x1 ∈ A → x2 ∈ A → id x1 = id x2 → x1 = x2
Tactic:
fix x2 : U
Proof state after:
U : Type
A : Set U
x1 x2 : U
⊢ x1 ∈ A → x2 ∈ A → id x1 = id x2 → x1 = x2
Theorem: HTPI.id_one_one_on
Proof state before:
U : Type
A : Set U
x1 x2 : U
⊢ x1 ∈ A → x2 ∈ A → id x1 = id x2 → x1 = x2
Tactic:
assume h1 : x1 ∈ A
Proof state after:
U : Type
A : Set U
x1 x2 : U
h1 : x1 ∈ A
⊢ x2 ∈ A → id x1 = id x2 → x1 = x2
Theorem: HTPI.id_one_one_on
Proof state before:
U : Type
A : Set U
x1 x2 : U
h1 : x1 ∈ A
⊢ x2 ∈ A → id x1 = id x2 → x1 = x2
Tactic:
assume h2 : x2 ∈ A
Proof state after:
U : Type
A : Set U
x1 x2 : U
h1 : x1 ∈ A
h2 : x2 ∈ A
⊢ id x1 = id x2 → x1 = x2
Theorem: HTPI.id_one_one_on
Proof state before:
U : Type
A : Set U
x1 x2 : U
h1 : x1 ∈ A
h2 : x2 ∈ A
⊢ id x1 = id x2 → x1 = x2
Tactic:
assume h3 : id x1 = id x2
Proof state after:
U : Type
A : Set U
x1 x2 : U
h1 : x1 ∈ A
h2 : x2 ∈ A
h3 : id x1 = id x2
⊢ x1 = x2
Theorem: HTPI.id_one_one_on
Proof state before:
U : Type
A : Set U
x1 x2 : U
h1 : x1 ∈ A
h2 : x2 ∈ A
h3 : id x1 = id x2
⊢ x1 = x2
Tactic:
show x1 = x2 from h3
Proof state after:
no goals
Theorem: HTPI.image_id
Proof state before:
U : Type
A : Set U
⊢ image id A = A
Tactic:
apply Set.ext
Proof state after:
case h
U : Type
A : Set U
⊢ ∀ (x : U), x ∈ image id A ↔ x ∈ A
Theorem: HTPI.image_id
Proof state before:
case h
U : Type
A : Set U
⊢ ∀ (x : U), x ∈ image id A ↔ x ∈ A
Tactic:
fix x : U
Proof state after:
case h
U : Type
A : Set U
x : U
⊢ x ∈ image id A ↔ x ∈ A
Theorem: HTPI.image_id
Proof state before:
case h
U : Type
A : Set U
x : U
⊢ x ∈ image id A ↔ x ∈ A
Tactic:
apply Iff.intro
Proof state after:
case h.mp
U : Type
A : Set U
x : U
⊢ x ∈ image id A → x ∈ A

case h.mpr
U : Type
A : Set U
x : U
⊢ x ∈ A → x ∈ image id A