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

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

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

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
State after:
U : Type
A : Set U
x1 x2 : U
⊢ x1 ∈ A → x2 ∈ A → id x1 = id x2 → x1 = x2

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
State after:
U : Type
A : Set U
x1 x2 : U
h1 : x1 ∈ A
⊢ x2 ∈ A → id x1 = id x2 → x1 = x2

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
State after:
U : Type
A : Set U
x1 x2 : U
h1 : x1 ∈ A
h2 : x2 ∈ A
⊢ id x1 = id x2 → x1 = x2

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
State after:
U : Type
A : Set U
x1 x2 : U
h1 : x1 ∈ A
h2 : x2 ∈ A
h3 : id x1 = id x2
⊢ x1 = x2

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