Theorem: HTPI.equinum_image (HTPILib/Chap8Part1.lean)

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 ∼ B
Tactic:
rewrite [←h2]
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
⊢ A ∼ image f A

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
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)

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
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)

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
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)

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
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)

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
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)

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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)

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
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

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
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

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
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

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
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

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)
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)

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
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals