awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
U : (a : α) → (ha : a ∈ s) → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → (ha : 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 : Type u_1)
hsU : s ⊆ ⋃ x ∈ fs, U (↑x : α) ⋯
a₁ a₂ : α
h : Membership.mem (γ := Set (α × α)) (⋂ i ∈ fs, T (↑i : α) ⋯) (a₁, a₂)
h₁ : (a₁, a₂).1 ∈ s
a : (↑s : Type u_1)
ha : a ∈ fs
haU : (a₁, a₂).1 ∈ U (↑a : α) ⋯
a₃ : (f (a₁, a₂).1, f (a₁, a₂).2) ∈ SetRel.comp t t
⊢ (f (a₁, a₂).1, f (a₁, a₂).2) ∈ r

Tactic:
apply htr
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
U : (a : α) → (ha : a ∈ s) → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → (ha : 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 : Type u_1)
hsU : s ⊆ ⋃ x ∈ fs, U (↑x : α) ⋯
a₁ a₂ : α
h : Membership.mem (γ := Set (α × α)) (⋂ i ∈ fs, T (↑i : α) ⋯) (a₁, a₂)
h₁ : (a₁, a₂).1 ∈ s
a : (↑s : Type u_1)
ha : a ∈ fs
haU : (a₁, a₂).1 ∈ U (↑a : α) ⋯
⊢ (f (a₁, a₂).1, f (a₁, a₂).2) ∈ SetRel.comp t t

Tactic:
⟨f a, SetRel.symm t <| hb _ _ _ haU ?_, hb _ _ _ haU ?_⟩

Premises used: Set.Mem, setOf, SetRel.symm, SetRel.comp, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
U : (a : α) → (ha : a ∈ s) → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → (ha : 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 : Type u_1)
hsU : s ⊆ ⋃ x ∈ fs, U (↑x : α) ⋯
a₁ a₂ : α
h : Membership.mem (γ := Set (α × α)) (⋂ i ∈ fs, T (↑i : α) ⋯) (a₁, a₂)
h₁ : (a₁, a₂).1 ∈ s
a : (↑s : Type u_1)
ha : a ∈ fs
haU : (a₁, a₂).1 ∈ U (↑a : α) ⋯
a₃ : (a₁, a₂).1 ∈ ball (a₁, a₂).1 (T (↑a : α) ⋯)
a₄ : (a₁, a₂).2 ∈ ball (a₁, a₂).1 (T (↑a : α) ⋯)
⊢ (f (a₁, a₂).1, f (a₁, a₂).2) ∈ SetRel.comp t t

Tactic:
refine ⟨f a, SetRel.symm t <| hb _ _ _ haU ?_, hb _ _ _ haU ?_⟩
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
U : (a : α) → (ha : a ∈ s) → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → (ha : 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 : Type u_1)
hsU : s ⊆ ⋃ x ∈ fs, U (↑x : α) ⋯
a₁ a₂ : α
h : Membership.mem (γ := Set (α × α)) (⋂ i ∈ fs, T (↑i : α) ⋯) (a₁, a₂)
h₁ : (a₁, a₂).1 ∈ s
a : (↑s : Type u_1)
ha : a ∈ fs
haU : (a₁, a₂).1 ∈ U (↑a : α) ⋯
⊢ (a₁, a₂).1 ∈ ball (a₁, a₂).1 (T (↑a : α) ⋯)

Tactic:
mem_ball_self _ (hT a a.2)

Premises used: UniformSpace.mem_ball_self, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
U : (a : α) → (ha : a ∈ s) → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → (ha : 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 : Type u_1)
hsU : s ⊆ ⋃ x ∈ fs, U (↑x : α) ⋯
a₁ a₂ : α
h : Membership.mem (γ := Set (α × α)) (⋂ i ∈ fs, T (↑i : α) ⋯) (a₁, a₂)
h₁ : (a₁, a₂).1 ∈ s
a : (↑s : Type u_1)
ha : a ∈ fs
haU : (a₁, a₂).1 ∈ U (↑a : α) ⋯
⊢ (a₁, a₂).2 ∈ ball (a₁, a₂).1 (T (↑a : α) ⋯)

Tactic:
mem_iInter₂.1 h a ha

Premises used: Set.Mem, setOf, Set.mem_iInter₂, UniformSpace.ball, Set.preimage, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
U : (a : α) → (ha : a ∈ s) → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → (ha : 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 : Type u_1)
hsU : s ⊆ ⋃ x ∈ fs, U (↑x : α) ⋯
a₁ a₂ : α
h : Membership.mem (γ := Set (α × α)) (⋂ i ∈ fs, T (↑i : α) ⋯) (a₁, a₂)
h₁ : (a₁, a₂).1 ∈ s
a : (↑s : Type u_1)
ha : a ∈ fs
haU : (a₁, a₂).1 ∈ U (↑a : α) ⋯
⊢ (a₁, a₂).1 ∈ ball (a₁, a₂).1 (T (↑a : α) ⋯)

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

Premises used: Set.mem_iInter₂, UniformSpace.mem_ball_self, Iff.mp, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
obtain :
  ∀ (t : Set (β × β)) (ht : t ∈ 𝓤 β) (htsymm : SetRel.IsSymm t) (htr : SetRel.comp t t ⊆ r),
    {x : α × α | (f x.1, f x.2) ∈ r} ∈ 𝓤 α
⊢ {x : α × α | (f x.1, f x.2) ∈ r} ∈ 𝓤 α

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

Premises used: comp_symm_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
obtain :
  ∀ (s : Set α) (hs : IsCompact s) (hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}), {x : α × α | (f x.1, f x.2) ∈ r} ∈ 𝓤 α
⊢ {x : α × α | (f x.1, f x.2) ∈ r} ∈ 𝓤 α

Tactic:
obtain ⟨s, hs, hst⟩ := mem_cocompact.1 (hx <| mem_nhds_left _ ht)

Premises used: mem_nhds_left, Iff.mp, Filter.mem_cocompact
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}
f₁ :
  Subset.{u_1} (α := Set (α × α)) (SetRel.symmetrize {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r})
    {x : α × α | (f x.1, f x.2) ∈ r}
⊢ {x : α × α | (f x.1, f x.2) ∈ r} ∈ 𝓤 α

Tactic:
apply
      mem_of_superset
        (symmetrize_mem_uniformity <|
          (hs.uniformContinuousAt_of_continuousAt f fun _ _ => h_cont.continuousAt) <|
            symmetrize_mem_uniformity hr)

Premises used: IsCompact.uniformContinuousAt_of_continuousAt, symmetrize_mem_uniformity, Continuous.continuousAt, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}
b₁ b₂ : α
h :
  Membership.mem (γ := Set (α × α)) (SetRel.symmetrize {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r})
    (b₁, b₂)
pos : ∀ (h₁ : b₁ ∈ s), Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)
neg : ∀ (h₁ : b₁ ∉ s), Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)
⊢ Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)

Tactic:
by_cases h₁ : b₁ ∈ s
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}
b₁ b₂ : α
h :
  Membership.mem (γ := Set (α × α)) (SetRel.symmetrize {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r})
    (b₁, b₂)
h₁ : b₁ ∈ s
⊢ Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)

Tactic:
(h.1 h₁).1

Premises used: Set.Mem, setOf, And.left
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}
b₁ b₂ : α
h :
  Membership.mem (γ := Set (α × α)) (SetRel.symmetrize {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r})
    (b₁, b₂)
h₁ : b₁ ∈ s
⊢ Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)

Tactic:
exact (h.1 h₁).1

Premises used: And.left
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}
b₁ b₂ : α
h :
  Membership.mem (γ := Set (α × α)) (SetRel.symmetrize {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r})
    (b₁, b₂)
h₁ : b₁ ∉ s
pos : ∀ (h₂ : b₂ ∈ s), Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)
neg : ∀ (h₂ : b₂ ∉ s), Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)
⊢ Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)

Tactic:
by_cases h₂ : b₂ ∈ s
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}
b₁ b₂ : α
h :
  Membership.mem (γ := Set (α × α)) (SetRel.symmetrize {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r})
    (b₁, b₂)
h₁ : b₁ ∉ s
h₂ : b₂ ∈ s
⊢ Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)

Tactic:
(h.2 h₂).2

Premises used: Set.Mem, SetRel.inv, setOf, And.right, Set.preimage, Prod.swap
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}
b₁ b₂ : α
h :
  Membership.mem (γ := Set (α × α)) (SetRel.symmetrize {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r})
    (b₁, b₂)
h₁ : b₁ ∉ s
h₂ : b₂ ∈ s
⊢ Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)

Tactic:
exact (h.2 h₂).2

Premises used: And.right
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}
b₁ b₂ : α
h :
  Membership.mem (γ := Set (α × α)) (SetRel.symmetrize {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r})
    (b₁, b₂)
h₁ : b₁ ∉ s
h₂ : b₂ ∉ s
neg : (f (b₁, b₂).1, f (b₁, b₂).2) ∈ SetRel.comp t t
⊢ Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)

Tactic:
apply htr
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}
b₁ b₂ : α
h :
  Membership.mem (γ := Set (α × α)) (SetRel.symmetrize {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r})
    (b₁, b₂)
h₁ : b₁ ∉ s
h₂ : b₂ ∉ s
⊢ (f (b₁, b₂).1, f (b₁, b₂).2) ∈ SetRel.comp t t

Tactic:
⟨x, SetRel.symm t <| hst h₁, hst h₂⟩

Premises used: Set.Mem, setOf, SetRel.symm, SetRel.comp, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}
b₁ b₂ : α
h :
  Membership.mem (γ := Set (α × α)) (SetRel.symmetrize {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r})
    (b₁, b₂)
h₁ : b₁ ∉ s
h₂ : b₂ ∉ s
⊢ (f (b₁, b₂).1, f (b₁, b₂).2) ∈ SetRel.comp t t

Tactic:
exact ⟨x, SetRel.symm t <| hst h₁, hst h₂⟩
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
inst_2 : One β
h1 : HasCompactMulSupport f
h2 : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
⊢ UniformContinuous f

Tactic:
h2.uniformContinuous_of_tendsto_cocompact h1.is_one_at_infty

Premises used: HasCompactMulSupport.is_one_at_infty, Continuous.uniformContinuous_of_tendsto_cocompact
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : LocallyCompactSpace α
inst_3 : CompactSpace β
inst_4 : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (SProd.sprod (β := Set β) U univ)
rcases : ∀ (K : Set α) (hxK : K ∈ 𝓝 x) (hKU : K ⊆ U) (hK : IsCompact K), TendstoUniformly f (f x) (𝓝 x)
⊢ TendstoUniformly f (f x) (𝓝 x)

Tactic:
rcases LocallyCompactSpace.local_compact_nhds _ _ hxU with ⟨K, hxK, hKU, hK⟩

Premises used: LocallyCompactSpace.local_compact_nhds
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : LocallyCompactSpace α
inst_3 : CompactSpace β
inst_4 : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (SProd.sprod (β := Set β) U univ)
K : Set α
hxK : K ∈ 𝓝 x
hKU : K ⊆ U
hK : IsCompact K
⊢ UniformContinuousOn (↿f) (SProd.sprod (β := Set β) K univ)

Tactic:
have : UniformContinuousOn ↿f (K ×ˢ univ) :=
    IsCompact.uniformContinuousOn_of_continuous (hK.prod isCompact_univ)
      (h.mono <| prod_mono hKU Subset.rfl)
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : LocallyCompactSpace α
inst_3 : CompactSpace β
inst_4 : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (SProd.sprod (β := Set β) U univ)
K : Set α
hxK : K ∈ 𝓝 x
hKU : K ⊆ U
hK : IsCompact K
this : UniformContinuousOn (↿f) (SProd.sprod (β := Set β) K univ)
⊢ TendstoUniformly f (f x) (𝓝 x)

Tactic:
this.tendstoUniformly hxK

Premises used: UniformContinuousOn.tendstoUniformly
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : LocallyCompactSpace α
inst_3 : CompactSpace β
inst_4 : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (SProd.sprod (β := Set β) U univ)
K : Set α
hxK : K ∈ 𝓝 x
hKU : K ⊆ U
hK : IsCompact K
this : UniformContinuousOn (↿f) (SProd.sprod (β := Set β) K univ)
⊢ TendstoUniformly f (f x) (𝓝 x)

Tactic:
exact this.tendstoUniformly hxK

Premises used: UniformContinuousOn.tendstoUniformly
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : WeaklyLocallyCompactSpace α
inst_3 : CompactSpace β
inst_4 : UniformSpace γ
f : α → β → γ
h : Continuous[instTopologicalSpaceProd, inst_4.toTopologicalSpace] ↿f
x : α
⊢ TendstoUniformly f (f x) (𝓝 x)

Tactic:
let ⟨K, hK, hxK⟩ := exists_compact_mem_nhds x
  have : UniformContinuousOn ↿f (K ×ˢ univ) :=
    IsCompact.uniformContinuousOn_of_continuous (hK.prod isCompact_univ) h.continuousOn
  this.tendstoUniformly hxK

Premises used: Continuous.continuousOn, IsCompact.prod, WeaklyLocallyCompactSpace.exists_compact_mem_nhds, nhds, IsCompact.uniformContinuousOn_of_continuous, TendstoUniformly, isCompact_univ, UniformContinuousOn.tendstoUniformly, _private.0.Continuous.tendstoUniformly.match_1
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
he : ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ (x : β), Membership.mem (γ := Set β) ∅ x → (f p x, f q x) ∈ u
hmono :
  ∀ ⦃s_1 t : Set β⦄,
    s_1 ⊆ t →
      (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1, (f p x, f q x) ∈ u
hunion :
  ∀ ⦃s_1 t : Set β⦄,
    (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1, (f p x, f q x) ∈ u) →
      (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1 ∪ t, (f p x, f q x) ∈ u
hnhds : ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
⊢ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ k, (f p x, f q x) ∈ u

Tactic:
apply hk.induction_on (p := fun t ↦ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u)

Premises used: IsCompact.induction_on
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
⊢ ∀ (p : α), Membership.mem (γ := Set α) univ p → ∀ (x : β), Membership.mem (γ := Set β) ∅ x → (f p x, f q x) ∈ u

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
⊢ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ (x : β), Membership.mem (γ := Set β) ∅ x → (f p x, f q x) ∈ u

Tactic:
exact ⟨univ, univ_mem, by simp⟩
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t' t : Set β
ht't : t' ⊆ t
hmono :
  ∀ (v : Set α) (v_mem : v ∈ 𝓝[s] q) (hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u),
    ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t', (f p x, f q x) ∈ u
⊢ (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t', (f p x, f q x) ∈ u

Tactic:
⟨v, v_mem, hv⟩
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t' t : Set β
ht't : t' ⊆ t
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
⊢ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t', (f p x, f q x) ∈ u

Tactic:
⟨v, v_mem, fun p hp x hx ↦ hv p hp x (ht't hx)⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t' t : Set β
ht't : t' ⊆ t
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
⊢ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t', (f p x, f q x) ∈ u

Tactic:
exact ⟨v, v_mem, fun p hp x hx ↦ hv p hp x (ht't hx)⟩
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t t' : Set β
hunion :
  ∀ (v : Set α) (v_mem : v ∈ 𝓝[s] q) (hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u),
    (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t', (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t ∪ t', (f p x, f q x) ∈ u
⊢ (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) →
    (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t', (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t ∪ t', (f p x, f q x) ∈ u

Tactic:
⟨v, v_mem, hv⟩
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
hunion :
  ∀ (v' : Set α) (v'_mem : v' ∈ 𝓝[s] q) (hv' : ∀ p ∈ v', ∀ x ∈ t', (f p x, f q x) ∈ u),
    ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t ∪ t', (f p x, f q x) ∈ u
⊢ (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t', (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t ∪ t', (f p x, f q x) ∈ u

Tactic:
⟨v', v'_mem, hv'⟩
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
v' : Set α
v'_mem : v' ∈ 𝓝[s] q
hv' : ∀ p ∈ v', ∀ x ∈ t', (f p x, f q x) ∈ u
⊢ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t ∪ t', (f p x, f q x) ∈ u

Tactic:
⟨v ∩ v', inter_mem v_mem v'_mem, fun p hp x hx ↦ ?_⟩

Premises used: Filter.inter_mem, Inter.inter, And.intro, Exists.intro