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

State before:
U : Type
A : Set U
⊢ image id A = A
Tactic:
apply Set.ext
State after:
case h
U : Type
A : Set U
⊢ ∀ (x : U), x ∈ image id A ↔ x ∈ A

State before:
case h
U : Type
A : Set U
⊢ ∀ (x : U), x ∈ image id A ↔ x ∈ A
Tactic:
fix x : U
State after:
case h
U : Type
A : Set U
x : U
⊢ x ∈ image id A ↔ x ∈ A

State before:
case h
U : Type
A : Set U
x : U
⊢ x ∈ image id A ↔ x ∈ A
Tactic:
apply Iff.intro
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

State before:
case h.mp
U : Type
A : Set U
x : U
⊢ x ∈ image id A → x ∈ A
Tactic:
assume h1 : x ∈ image id A
State after:
case h.mp
U : Type
A : Set U
x : U
h1 : x ∈ image id A
⊢ x ∈ A

State before:
case h.mp
U : Type
A : Set U
x : U
h1 : x ∈ image id A
⊢ x ∈ A
Tactic:
obtain (y : U) (h2 : y ∈ A ∧ id y = x) from h1
State after:
case h.mp
U : Type
A : Set U
x : U
h1 : x ∈ image id A
y : U
h2 : y ∈ A ∧ id y = x
⊢ x ∈ A

State before:
case h.mp
U : Type
A : Set U
x : U
h1 : x ∈ image id A
y : U
h2 : y ∈ A ∧ id y = x
⊢ x ∈ A
Tactic:
rewrite [←h2.right]
State after:
case h.mp
U : Type
A : Set U
x : U
h1 : x ∈ image id A
y : U
h2 : y ∈ A ∧ id y = x
⊢ id y ∈ A

State before:
case h.mp
U : Type
A : Set U
x : U
h1 : x ∈ image id A
y : U
h2 : y ∈ A ∧ id y = x
⊢ id y ∈ A
Tactic:
show id y ∈ A from h2.left
State after:
no goals

State before:
case h.mpr
U : Type
A : Set U
x : U
⊢ x ∈ A → x ∈ image id A
Tactic:
assume h1 : x ∈ A
State after:
case h.mpr
U : Type
A : Set U
x : U
h1 : x ∈ A
⊢ x ∈ image id A

State before:
case h.mpr
U : Type
A : Set U
x : U
h1 : x ∈ A
⊢ x ∈ image id A
Tactic:
apply Exists.intro x
State after:
case h.mpr
U : Type
A : Set U
x : U
h1 : x ∈ A
⊢ x ∈ A ∧ id x = x

State before:
case h.mpr
U : Type
A : Set U
x : U
h1 : x ∈ A
⊢ x ∈ A ∧ id x = x
Tactic:
apply And.intro h1
State after:
case h.mpr
U : Type
A : Set U
x : U
h1 : x ∈ A
⊢ id x = x

State before:
case h.mpr
U : Type
A : Set U
x : U
h1 : x ∈ A
⊢ id x = x
Tactic:
rfl
State after:
no goals