α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : b ∈ approx (↑f) i a
⊢ ∃ i, b ∈ approx (↑f) i a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : b ∈ approx (↑f) i a
⊢ b ∈ Part.fix (↑f) a
rw [mem_iff f]
no goals
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : b ∈ approx (↑f) i a
⊢ ∃ i, b ∈ approx (↑f) i a
exact ⟨_, hh⟩