case intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
⊢ {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
⊢ {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
obtain ⟨t, ht, htsymm, htr⟩ := comp_symm_mem_uniformity_sets hr
case intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
⊢ {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
case intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
⊢ {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
choose U hU T hT hb using fun a ha =>
  exists_mem_nhds_ball_subset_of_mem_nhds ((hf a ha).preimage_mem_nhds <| mem_nhds_left _ ht)
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
⊢ {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
case intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
⊢ {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
obtain ⟨fs, hsU⟩ := hs.elim_nhds_subcover' U hU
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
⊢ (⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s)) ⊆ {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ r}
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
⊢ {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
apply mem_of_superset ((biInter_finset_mem fs).2 fun a _ => hT a a.2)
case intro.intro.intro.intro.mk
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s)
h₁ : (a₁, a₂).fst ∈ s
⊢ (f (a₁, a₂).fst, f (a₁, a₂).snd) ∈ r
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
⊢ (⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s)) ⊆ {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ r}
rintro ⟨a₁, a₂⟩ h h₁
case intro.intro.intro.intro.mk.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s)
h₁ : (a₁, a₂).fst ∈ s
a : ↑s
ha : a ∈ fs
haU : (a₁, a₂).fst ∈ U ↑a (_ : ↑a ∈ s)
⊢ (f (a₁, a₂).fst, f (a₁, a₂).snd) ∈ r
case intro.intro.intro.intro.mk
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s)
h₁ : (a₁, a₂).fst ∈ s
⊢ (f (a₁, a₂).fst, f (a₁, a₂).snd) ∈ r
obtain ⟨a, ha, haU⟩ := Set.mem_iUnion₂.1 (hsU h₁)
case intro.intro.intro.intro.mk.intro.intro.a
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s)
h₁ : (a₁, a₂).fst ∈ s
a : ↑s
ha : a ∈ fs
haU : (a₁, a₂).fst ∈ U ↑a (_ : ↑a ∈ s)
⊢ (f (a₁, a₂).fst, f (a₁, a₂).snd) ∈ t ○ t
case intro.intro.intro.intro.mk.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s)
h₁ : (a₁, a₂).fst ∈ s
a : ↑s
ha : a ∈ fs
haU : (a₁, a₂).fst ∈ U ↑a (_ : ↑a ∈ s)
⊢ (f (a₁, a₂).fst, f (a₁, a₂).snd) ∈ r
apply htr
case intro.intro.intro.intro.mk.intro.intro.a.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s)
h₁ : (a₁, a₂).fst ∈ s
a : ↑s
ha : a ∈ fs
haU : (a₁, a₂).fst ∈ U ↑a (_ : ↑a ∈ s)
⊢ (a₁, a₂).fst ∈ ball (a₁, a₂).fst (T ↑a (_ : ↑a ∈ s))

case intro.intro.intro.intro.mk.intro.intro.a.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s)
h₁ : (a₁, a₂).fst ∈ s
a : ↑s
ha : a ∈ fs
haU : (a₁, a₂).fst ∈ U ↑a (_ : ↑a ∈ s)
⊢ (a₁, a₂).snd ∈ ball (a₁, a₂).fst (T ↑a (_ : ↑a ∈ s))
case intro.intro.intro.intro.mk.intro.intro.a
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s)
h₁ : (a₁, a₂).fst ∈ s
a : ↑s
ha : a ∈ fs
haU : (a₁, a₂).fst ∈ U ↑a (_ : ↑a ∈ s)
⊢ (f (a₁, a₂).fst, f (a₁, a₂).snd) ∈ t ○ t
refine' ⟨f a, htsymm.mk_mem_comm.1 (hb _ _ _ haU _), hb _ _ _ haU _⟩
no goals
case intro.intro.intro.intro.mk.intro.intro.a.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s)
h₁ : (a₁, a₂).fst ∈ s
a : ↑s
ha : a ∈ fs
haU : (a₁, a₂).fst ∈ U ↑a (_ : ↑a ∈ s)
⊢ (a₁, a₂).fst ∈ ball (a₁, a₂).fst (T ↑a (_ : ↑a ∈ s))

case intro.intro.intro.intro.mk.intro.intro.a.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.42994
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s)
h₁ : (a₁, a₂).fst ∈ s
a : ↑s
ha : a ∈ fs
haU : (a₁, a₂).fst ∈ U ↑a (_ : ↑a ∈ s)
⊢ (a₁, a₂).snd ∈ ball (a₁, a₂).fst (T ↑a (_ : ↑a ∈ s))
exacts [mem_ball_self _ (hT a a.2), mem_iInter₂.1 h a ha]