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

State before:
U : Type
A : Set U
⊢ A ∈ 𝒫 Univ U
Tactic:
fix x : U
State after:
U : Type
A : Set U
x : U
⊢ x ∈ A → x ∈ Univ U

State before:
U : Type
A : Set U
x : U
⊢ x ∈ A → x ∈ Univ U
Tactic:
assume h : x ∈ A
State after:
U : Type
A : Set U
x : U
h : x ∈ A
⊢ x ∈ Univ U

State before:
U : Type
A : Set U
x : U
h : x ∈ A
⊢ x ∈ Univ U
Tactic:
show x ∈ Univ U from elt_Univ x
State after:
no goals