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

State before:
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
h3 : image f (Univ U) = Univ V
⊢ Univ U ∼ Univ V
Tactic:
show Univ U ∼ Univ V from
  equinum_image (one_one_on_of_one_one h1 (Univ U)) h3
State after:
no goals

State before:
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
⊢ image f (Univ U) = Univ V
Tactic:
apply Set.ext
State after:
case h
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
⊢ ∀ (x : V), x ∈ image f (Univ U) ↔ x ∈ Univ V

State before:
case h
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
⊢ ∀ (x : V), x ∈ image f (Univ U) ↔ x ∈ Univ V
Tactic:
fix v : V
State after:
case h
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
⊢ v ∈ image f (Univ U) ↔ v ∈ Univ V

State before:
case h
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
⊢ v ∈ image f (Univ U) ↔ v ∈ Univ V
Tactic:
apply Iff.intro
State after:
case h.mp
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
⊢ v ∈ image f (Univ U) → v ∈ Univ V

case h.mpr
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
⊢ v ∈ Univ V → v ∈ image f (Univ U)

State before:
case h.mp
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
⊢ v ∈ image f (Univ U) → v ∈ Univ V
Tactic:
assume h3 : v ∈ image f (Univ U)
State after:
case h.mp
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ image f (Univ U)
⊢ v ∈ Univ V

State before:
case h.mp
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ image f (Univ U)
⊢ v ∈ Univ V
Tactic:
show v ∈ Univ V from elt_Univ v
State after:
no goals

State before:
case h.mpr
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
⊢ v ∈ Univ V → v ∈ image f (Univ U)
Tactic:
assume h3 : v ∈ Univ V
State after:
case h.mpr
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ Univ V
⊢ v ∈ image f (Univ U)

State before:
case h.mpr
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ Univ V
⊢ v ∈ image f (Univ U)
Tactic:
obtain (u : U) (h4 : f u = v) from h2 v
State after:
case h.mpr
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ Univ V
u : U
h4 : f u = v
⊢ v ∈ image f (Univ U)

State before:
case h.mpr
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ Univ V
u : U
h4 : f u = v
⊢ v ∈ image f (Univ U)
Tactic:
apply Exists.intro u
State after:
case h.mpr
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ Univ V
u : U
h4 : f u = v
⊢ u ∈ Univ U ∧ f u = v

State before:
case h.mpr
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ Univ V
u : U
h4 : f u = v
⊢ u ∈ Univ U ∧ f u = v
Tactic:
apply And.intro _ h4
State after:
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ Univ V
u : U
h4 : f u = v
⊢ u ∈ Univ U

State before:
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ Univ V
u : U
h4 : f u = v
⊢ u ∈ Univ U
Tactic:
show u ∈ Univ U from elt_Univ u
State after:
no goals