-- Mathlib/Topology/UniformSpace/HeineCantor.lean
theorem IsCompact.uniformContinuousAt_of_continuousAt {r : Set (β × β)} {s : Set α}
    (hs : IsCompact s) (f : α → β) (hf : ∀ a ∈ s, ContinuousAt f a) (hr : r ∈ 𝓤 β) :
    { x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ r } ∈ 𝓤 α

Proof state:
case intro.intro.intro.intro.mk.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ 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' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ x ∈ fs, U ↑x ⋯
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ i ∈ fs, T ↑i ⋯
h₁ : (a₁, a₂).1 ∈ s
a : ↑s
ha : a ∈ fs
haU : (a₁, a₂).1 ∈ U ↑a ⋯
⊢ (f (a₁, a₂).1, f (a₁, a₂).2) ∈ r

Tactic:
apply htr

Result:
case intro.intro.intro.intro.mk.intro.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ 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' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ x ∈ fs, U ↑x ⋯
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ i ∈ fs, T ↑i ⋯
h₁ : (a₁, a₂).1 ∈ s
a : ↑s
ha : a ∈ fs
haU : (a₁, a₂).1 ∈ U ↑a ⋯
⊢ (f (a₁, a₂).1, f (a₁, a₂).2) ∈ t ○ t

Proof state:
case intro.intro.intro.intro.mk.intro.intro.a.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ 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' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ x ∈ fs, U ↑x ⋯
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ i ∈ fs, T ↑i ⋯
h₁ : (a₁, a₂).1 ∈ s
a : ↑s
ha : a ∈ fs
haU : (a₁, a₂).1 ∈ U ↑a ⋯
⊢ (a₁, a₂).1 ∈ ball (a₁, a₂).1 (T ↑a ⋯)

case intro.intro.intro.intro.mk.intro.intro.a.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ 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' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ x ∈ fs, U ↑x ⋯
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ i ∈ fs, T ↑i ⋯
h₁ : (a₁, a₂).1 ∈ s
a : ↑s
ha : a ∈ fs
haU : (a₁, a₂).1 ∈ U ↑a ⋯
⊢ (a₁, a₂).2 ∈ ball (a₁, a₂).1 (T ↑a ⋯)

Tactic:
exacts [mem_ball_self _ (hT a a.2), mem_iInter₂.1 h a ha]

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ 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' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
⊢ {x | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α

Tactic:
obtain ⟨fs, hsU⟩ := hs.elim_nhds_subcover' U hU

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ 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' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ x ∈ fs, U ↑x ⋯
⊢ {x | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ 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' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ x ∈ fs, U ↑x ⋯
⊢ {x | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α

Tactic:
apply mem_of_superset ((biInter_finset_mem fs).2 fun a _ => hT a a.2)

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ 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' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ x ∈ fs, U ↑x ⋯
⊢ ⋂ i ∈ fs, T ↑i ⋯ ⊆ {x | x.1 ∈ s → (f x.1, f x.2) ∈ r}

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
⊢ {x | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α

Tactic:
obtain ⟨t, ht, htsymm, htr⟩ := comp_symm_mem_uniformity_sets hr

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
⊢ {x | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α