Theorem: HTPI.Example_3_3_5 (HTPILib/Chap3.lean)

State before:
U : Type
B : Set U
F : Set (Set U)
⊢ ⋃₀ F ⊆ B → F ⊆ 𝒫 B
Tactic:
assume h1 : ⋃₀ F ⊆ B
State after:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
⊢ F ⊆ 𝒫 B

State before:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
⊢ F ⊆ 𝒫 B
Tactic:
define
State after:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
⊢ ∀ ⦃a : Set U⦄, a ∈ F → a ∈ 𝒫 B

State before:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
⊢ ∀ ⦃a : Set U⦄, a ∈ F → a ∈ 𝒫 B
Tactic:
fix x : Set U
State after:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
⊢ x ∈ F → x ∈ 𝒫 B

State before:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
⊢ x ∈ F → x ∈ 𝒫 B
Tactic:
assume h2 : x ∈ F
State after:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
⊢ x ∈ 𝒫 B

State before:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
⊢ x ∈ 𝒫 B
Tactic:
define
State after:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
⊢ ∀ ⦃a : U⦄, a ∈ x → a ∈ B

State before:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
⊢ ∀ ⦃a : U⦄, a ∈ x → a ∈ B
Tactic:
fix y : U
State after:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
y : U
⊢ y ∈ x → y ∈ B

State before:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
y : U
⊢ y ∈ x → y ∈ B
Tactic:
assume h3 : y ∈ x
State after:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ y ∈ B

State before:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ y ∈ B
Tactic:
define at h1
State after:
U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄, a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ y ∈ B

State before:
U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄, a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ y ∈ B
Tactic:
apply h1 _
State after:
U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄, a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ y ∈ ⋃₀ F

State before:
U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄, a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ y ∈ ⋃₀ F
Tactic:
define
State after:
U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄, a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ ∃ t ∈ F, y ∈ t

State before:
U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄, a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ ∃ t ∈ F, y ∈ t
Tactic:
apply Exists.intro x _
State after:
U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄, a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ x ∈ F ∧ y ∈ x

State before:
U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄, a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ x ∈ F ∧ y ∈ x
Tactic:
show x ∈ F ∧ y ∈ x from And.intro h2 h3
State after:
no goals