Theorem: idx_set_inter_rev (meetings/ex2.lean)

State before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
⊢ ⋂ i ∈ I, A i ⊆ ⋂ j ∈ J, A j
Tactic:
simp only [Set.subset_iInter_iff]
State after:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
⊢ ∀ i ∈ J, ⋂ i ∈ I, A i ⊆ A i

State before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
⊢ ∀ i ∈ J, ⋂ i ∈ I, A i ⊆ A i
Tactic:
intros x hx b hb
State after:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : α
hx : x ∈ J
b : β
hb : b ∈ ⋂ i ∈ I, A i
⊢ b ∈ A x

State before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : α
hx : x ∈ J
b : β
hb : b ∈ ⋂ i ∈ I, A i
⊢ b ∈ A x
Tactic:
simp at hb
State after:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : α
hx : x ∈ J
b : β
hb : ∀ i ∈ I, b ∈ A i
⊢ b ∈ A x

State before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : α
hx : x ∈ J
b : β
hb : ∀ i ∈ I, b ∈ A i
⊢ b ∈ A x
Tactic:
specialize hb x
State after:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : α
hx : x ∈ J
b : β
hb : x ∈ I → b ∈ A x
⊢ b ∈ A x

State before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : α
hx : x ∈ J
b : β
hb : x ∈ I → b ∈ A x
⊢ b ∈ A x
Tactic:
exact hb (hsub hx)
State after:
no goals