β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
this : Set.Nonempty.some (_ : ↑x ∈ (inducedMap A).fst) ∈ ⋂ (n : ℕ), A (res (↑x) n)
⊢ Sigma.snd (inducedMap A) x ∈ A (res (↑x) n)
β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
⊢ Sigma.snd (inducedMap A) x ∈ A (res (↑x) n)
have := x.property.some_mem
β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
this : ∀ (i : ℕ), Set.Nonempty.some (_ : ↑x ∈ (inducedMap A).fst) ∈ A (res (↑x) i)
⊢ Sigma.snd (inducedMap A) x ∈ A (res (↑x) n)
β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
this : Set.Nonempty.some (_ : ↑x ∈ (inducedMap A).fst) ∈ ⋂ (n : ℕ), A (res (↑x) n)
⊢ Sigma.snd (inducedMap A) x ∈ A (res (↑x) n)
rw [mem_iInter] at this
no goals
β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
this : ∀ (i : ℕ), Set.Nonempty.some (_ : ↑x ∈ (inducedMap A).fst) ∈ A (res (↑x) i)
⊢ Sigma.snd (inducedMap A) x ∈ A (res (↑x) n)
exact this n