Theorem: HTPI.one_one_on_of_one_one (HTPILib/Chap8Part2.lean)

State before:
U V : Type
f : U → V
h : one_to_one f
A : Set U
⊢ one_one_on f A
Tactic:
define
State after:
U V : Type
f : U → V
h : one_to_one f
A : Set U
⊢ ∀ ⦃x1 x2 : U⦄, x1 ∈ A → x2 ∈ A → f x1 = f x2 → x1 = x2

State before:
U V : Type
f : U → V
h : one_to_one f
A : Set U
⊢ ∀ ⦃x1 x2 : U⦄, x1 ∈ A → x2 ∈ A → f x1 = f x2 → x1 = x2
Tactic:
fix x1 : U
State after:
U V : Type
f : U → V
h : one_to_one f
A : Set U
x1 : U
⊢ ∀ ⦃x2 : U⦄, x1 ∈ A → x2 ∈ A → f x1 = f x2 → x1 = x2

State before:
U V : Type
f : U → V
h : one_to_one f
A : Set U
x1 : U
⊢ ∀ ⦃x2 : U⦄, x1 ∈ A → x2 ∈ A → f x1 = f x2 → x1 = x2
Tactic:
fix x2 : U
State after:
U V : Type
f : U → V
h : one_to_one f
A : Set U
x1 x2 : U
⊢ x1 ∈ A → x2 ∈ A → f x1 = f x2 → x1 = x2

State before:
U V : Type
f : U → V
h : one_to_one f
A : Set U
x1 x2 : U
⊢ x1 ∈ A → x2 ∈ A → f x1 = f x2 → x1 = x2
Tactic:
assume h1 : x1 ∈ A
State after:
U V : Type
f : U → V
h : one_to_one f
A : Set U
x1 x2 : U
h1 : x1 ∈ A
⊢ x2 ∈ A → f x1 = f x2 → x1 = x2

State before:
U V : Type
f : U → V
h : one_to_one f
A : Set U
x1 x2 : U
h1 : x1 ∈ A
⊢ x2 ∈ A → f x1 = f x2 → x1 = x2
Tactic:
assume h2 : x2 ∈ A
State after:
U V : Type
f : U → V
h : one_to_one f
A : Set U
x1 x2 : U
h1 : x1 ∈ A
h2 : x2 ∈ A
⊢ f x1 = f x2 → x1 = x2

State before:
U V : Type
f : U → V
h : one_to_one f
A : Set U
x1 x2 : U
h1 : x1 ∈ A
h2 : x2 ∈ A
⊢ f x1 = f x2 → x1 = x2
Tactic:
show f x1 = f x2 → x1 = x2 from h x1 x2
State after:
no goals