Theorem: idx_set_union (meetings/ex2.lean)

State before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
⊢ ⋃ j ∈ J, A j ⊆ ⋃ i ∈ I, A i
Tactic:
intros x hx
State after:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
hx : x ∈ ⋃ j ∈ J, A j
⊢ x ∈ ⋃ i ∈ I, A i

State before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
hx : x ∈ ⋃ j ∈ J, A j
⊢ x ∈ ⋃ i ∈ I, A i
Tactic:
simp only [Set.mem_iUnion, exists_prop]
State after:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
hx : x ∈ ⋃ j ∈ J, A j
⊢ ∃ i ∈ I, x ∈ A i

State before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
hx : x ∈ ⋃ j ∈ J, A j
⊢ ∃ i ∈ I, x ∈ A i
Tactic:
simp only [Set.mem_iUnion, exists_prop] at hx
State after:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
hx : ∃ i ∈ J, x ∈ A i
⊢ ∃ i ∈ I, x ∈ A i

State before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
hx : ∃ i ∈ J, x ∈ A i
⊢ ∃ i ∈ I, x ∈ A i
Tactic:
rcases hx with ⟨j, ⟨hj, hxj⟩⟩
State after:
case intro.intro
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ ∃ i ∈ I, x ∈ A i

State before:
case intro.intro
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ ∃ i ∈ I, x ∈ A i
Tactic:
use j
State after:
case h
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ j ∈ I ∧ x ∈ A j

State before:
case h
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ j ∈ I ∧ x ∈ A j
Tactic:
constructor
State after:
case h.left
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ j ∈ I

case h.right
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ x ∈ A j

State before:
case h.left
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ j ∈ I

case h.right
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ x ∈ A j
Tactic:
exact hsub hj
State after:
case h.right
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ x ∈ A j

State before:
case h.right
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ x ∈ A j
Tactic:
exact hxj
State after:
no goals