awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
x : β
⊢ (h : (a : α) → β) ((h.symm : (a : β) → α) x : α) = x

Tactic:
h.toEquiv.apply_symm_apply x

Premises used: Equiv.apply_symm_apply, UniformEquiv.toEquiv
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
x : α
⊢ (h.symm : (a : β) → α) ((h : (a : α) → β) x : β) = x

Tactic:
h.toEquiv.symm_apply_apply x

Premises used: Equiv.symm_apply_apply, UniformEquiv.toEquiv
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ Function.Bijective.{u + 1, u_1 + 1} (α := α) (β := β) (⇑h : (a : α) → β)

Tactic:
h.toEquiv.bijective

Premises used: Equiv.bijective, UniformEquiv.toEquiv
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ Function.Injective.{u + 1, u_1 + 1} (α := α) (β := β) (⇑h : (a : α) → β)

Tactic:
h.toEquiv.injective

Premises used: Equiv.injective, UniformEquiv.toEquiv
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ Function.Surjective.{u + 1, u_1 + 1} (α := α) (β := β) (⇑h : (a : α) → β)

Tactic:
h.toEquiv.surjective

Premises used: Equiv.surjective, UniformEquiv.toEquiv
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g (⇑f : (a : α) → β)
x : β
rw rw₁ : Eq.{u + 1} (α := α) ((f.symm : (a : β) → α) x : α) ((f.symm : (a : β) → α) x : α)
⊢ Eq.{u + 1} (α := α) ((f.symm : (a : β) → α) ((f : (a : α) → β) (g x) : β) : α) ((f.symm : (a : β) → α) x : α)

Tactic:
rw [hg x]
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g (⇑f : (a : α) → β)
this : g = (⇑f.symm : (a : β) → α)
⊢ Function.LeftInverse f.invFun f.toFun

Tactic:
f.left_inv

Premises used: UniformEquiv.toEquiv, Equiv.left_inv
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g (⇑f : (a : α) → β)
this : g = (⇑f.symm : (a : β) → α)
⊢ Function.LeftInverse g (⇑f : (a : α) → β)

Tactic:
convert! f.left_inv

Premises used: UniformEquiv.toEquiv, Equiv.left_inv
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g (⇑f : (a : α) → β)
this : g = (⇑f.symm : (a : β) → α)
⊢ Function.RightInverse f.invFun f.toFun

Tactic:
f.right_inv

Premises used: Equiv.right_inv, UniformEquiv.toEquiv
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g (⇑f : (a : α) → β)
this : g = (⇑f.symm : (a : β) → α)
⊢ Function.RightInverse g (⇑f : (a : α) → β)

Tactic:
convert! f.right_inv using 1

Premises used: Equiv.right_inv, UniformEquiv.toEquiv
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g (⇑f : (a : α) → β)
this : g = (⇑f.symm : (a : β) → α)
⊢ UniformContinuous.{u_1, u} (α := β) (β := α) (⇑f.symm : (a : β) → α)

Tactic:
f.symm.uniformContinuous

Premises used: UniformEquiv.symm, UniformEquiv.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g (⇑f : (a : α) → β)
this : g = (⇑f.symm : (a : β) → α)
⊢ UniformContinuous g

Tactic:
convert! f.symm.uniformContinuous

Premises used: UniformEquiv.symm, UniformEquiv.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ Eq.{u + 1} (α := α → α) (Function.comp.{u + 1, u_1 + 1, u + 1} (β := β) (⇑h.symm : (a : β) → α) (⇑h : (a : α) → β)) id

Tactic:
funext h.symm_apply_apply

Premises used: funext, UniformEquiv.symm_apply_apply
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ Eq.{u_1 + 1} (α := β → β)
    (Function.comp.{u_1 + 1, u + 1, u_1 + 1} (β := α) (⇑h : (a : α) → β) (⇑h.symm : (a : β) → α)) id

Tactic:
funext h.apply_symm_apply

Premises used: UniformEquiv.apply_symm_apply, funext
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ Eq.{u_1 + 1} (α := Set β) (range.{u_1, u + 1} (ι := α) (⇑h : (a : α) → β)) univ

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ Eq (α := (s : Set β) → Set α) (image (⇑h.symm : (a : β) → α)) (preimage (⇑h : (a : α) → β))

Tactic:
funext h.symm.toEquiv.image_eq_preimage_symm

Premises used: UniformEquiv.symm, funext, Equiv.image_eq_preimage_symm, UniformEquiv.toEquiv
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ Eq (α := (s : Set α) → Set β) (preimage (⇑h.symm : (a : β) → α)) (image (⇑h : (a : α) → β))

Tactic:
(funext h.toEquiv.image_eq_preimage_symm).symm

Premises used: funext, Equiv.image_eq_preimage_symm, Eq.symm, UniformEquiv.toEquiv
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
s : Set β
⊢ image.{u, u_1} (α := α) (⇑h : (a : α) → β) ((⇑h : (a : α) → β) ⁻¹' s) = s

Tactic:
h.toEquiv.image_preimage s

Premises used: Equiv.image_preimage, UniformEquiv.toEquiv
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
s : Set α
⊢ preimage.{u, u_1} (β := β) (⇑h : (a : α) → β) ((⇑h : (a : α) → β) '' s) = s

Tactic:
h.toEquiv.preimage_image s

Premises used: Equiv.preimage_image, UniformEquiv.toEquiv
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ IsUniformInducing.{u, u} (α := α) (β := α)
    (Function.comp.{u + 1, u_1 + 1, u + 1} (β := β) (⇑h.symm : (a : β) → α) (⇑h : (a : α) → β))

Tactic:
simp only [symm_comp_self, IsUniformInducing.id]

Premises used: IsUniformInducing.id, UniformEquiv.symm_comp_self
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ UniformSpace.comap (⇑h : (a : α) → β) inst_1 = inst

Tactic:
h.isUniformInducing.comap_uniformSpace

Premises used: IsUniformInducing.comap_uniformSpace, UniformEquiv.isUniformInducing
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ IsUniformEmbedding.{u, u_1} (α := α) (β := β) (⇑h : (a : α) → β)

Tactic:
⟨h.isUniformInducing, h.injective⟩

Premises used: UniformEquiv.injective, IsUniformEmbedding.mk, UniformEquiv.isUniformInducing
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ CompleteSpace α ↔ CompleteSpace β

Tactic:
completeSpace_congr h.isUniformEmbedding

Premises used: completeSpace_congr, UniformEquiv.isUniformEmbedding
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
f : α → β
hf : IsUniformEmbedding f
rw : UniformContinuous.{u_1, u_1} (α := (↑(range f) : Type u_1)) (Subtype.val (p := fun (x : β) ↦ x ∈ range f))
⊢ UniformContinuous (Equiv.ofInjective f ⋯).invFun

Tactic:
rw [hf.isUniformInducing.uniformContinuous_iff, Equiv.invFun_as_coe,
      Equiv.self_comp_ofInjective_symm]

Premises used: Equiv.invFun_as_coe, IsUniformEmbedding.isUniformInducing, IsUniformInducing.uniformContinuous_iff, Equiv.self_comp_ofInjective_symm
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
f : α → β
hf : IsUniformEmbedding f
⊢ UniformContinuous.{u_1, u_1} (α := (↑(range f) : Type u_1)) (Subtype.val (p := fun (x : β) ↦ x ∈ range f))

Tactic:
uniformContinuous_subtype_val

Premises used: uniformContinuous_subtype_val
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
f : α → β
hf : IsUniformEmbedding f
⊢ UniformContinuous.{u_1, u_1} (α := (↑(range f) : Type u_1)) (Subtype.val (p := fun (x : β) ↦ x ∈ range f))

Tactic:
exact uniformContinuous_subtype_val

Premises used: uniformContinuous_subtype_val
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
h₁ : α ≃ᵤ β
h₂ : γ ≃ᵤ δ
⊢ (h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm

Tactic:
rfl

Premises used: UniformEquiv.prodCongr, Prod.map, UniformEquiv.symm, Equiv.symm, Equiv.prodCongr, rfl
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
h₁ : α ≃ᵤ β
h₂ : γ ≃ᵤ δ
⊢ Eq (α := (a : α × γ) → β × δ) (⇑(h₁.prodCongr h₂) : (a : α × γ) → β × δ)
    (Prod.map (⇑h₁ : (a : α) → β) (⇑h₂ : (a : γ) → δ))

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ Eq (α := β × α ≃ᵤ α × β) (UniformEquiv.symm (prodComm α β)) (prodComm β α)

Tactic:
rfl

Premises used: Equiv.prodComm, UniformEquiv.symm, UniformEquiv.prodComm, Prod.swap, Equiv.symm, rfl
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ Eq (α := (a : α × β) → β × α) (⇑(prodComm α β) : (a : α × β) → β × α) Prod.swap

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
inst : UniformSpace α
⊢ Eq (α := (a : PUnit.{u_4 + 1} × α) → α) (⇑(punitProd α) : (a : PUnit.{u_4 + 1} × α) → α) Prod.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β_1 : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β_1
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
ι : Type u_4
ι' : Type u_5
β : ι' → Type u_6
inst_4 : (j : ι') → UniformSpace (β j)
e : ι ≃ ι'
i : ι
⊢ UniformContinuous (β := β ((e : (a : ι) → ι') i)) fun (x : (i : ι) → β ((e : (a : ι) → ι') i)) ↦
    (Equiv.piCongrLeft β e).toFun x ((e : (a : ι) → ι') i)

Tactic:
simpa only [Equiv.toFun_as_coe, Equiv.piCongrLeft_apply_apply] using
      Pi.uniformContinuous_proj _ i

Premises used: Equiv.toFun_as_coe, Pi.uniformContinuous_proj, Equiv.piCongrLeft_apply_apply
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
ι : Type u_4
X : ι → Type u_5
inst : (i : ι) → UniformSpace (X i)
⊢ Eq (α := ((i : ι) → X ((Equiv.refl ι : (a : ι) → ι) i)) ≃ᵤ ((j : ι) → X j)) (piCongrLeft (β := X) (Equiv.refl ι))
    (UniformEquiv.refl ((i : ι) → X i))

Tactic:
rfl

Premises used: Equiv.piCongrLeft, UniformEquiv.refl, Equiv.symm, Equiv.refl, UniformEquiv.piCongrLeft, rfl
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
ι : Type u_4
ι' : Type u_5
X : ι' → Type u_6
inst : (j : ι') → UniformSpace (X j)
e : ι ≃ ι'
⊢ Eq (α := (a : (j : ι') → X j) → (i : ι) → X ((e : (a : ι) → ι') i))
    (⇑(UniformEquiv.symm (piCongrLeft (β := X) e)) : (a : (j : ι') → X j) → (i : ι) → X ((e : (a : ι) → ι') i))
    fun (x1 : (j : ι') → X j) (x2 : ι) ↦ x1 ((e : (a : ι) → ι') x2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
ι : Type u_4
ι' : Type u_5
X : ι' → Type u_6
inst : (j : ι') → UniformSpace (X j)
e : ι ≃ ι'
x : (i : ι) → X ((e : (a : ι) → ι') i)
i : ι
⊢ (piCongrLeft (β := X) e : (a : (i : ι) → X ((e : (a : ι) → ι') i)) → (j : ι') → X j) x ((e : (a : ι) → ι') i) = x i

Tactic:
Equiv.piCongrLeft_apply_apply ..

Premises used: Equiv.piCongrLeft_apply_apply
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
ι : Type u_4
β₁ : ι → Type u_5
β₂ : ι → Type u_6
inst : (i : ι) → UniformSpace (β₁ i)
inst_1 : (i : ι) → UniformSpace (β₂ i)
F : (i : ι) → UniformEquiv.{u_5, u_6} (β₁ i) (β₂ i)
⊢ (piCongrRight (β₁ := β₁) (β₂ := β₂) F).symm = piCongrRight (β₁ := β₂) (β₂ := β₁) fun (i : ι) ↦ (F i).symm

Tactic:
rfl

Premises used: UniformEquiv.piCongrRight, Pi.map, UniformEquiv.symm, Equiv.piCongrRight, Equiv.symm, rfl
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
ι : Type u_4
X : ι → Type u_5
inst : (i : ι) → UniformSpace (X i)
⊢ Eq (α := ((i : ι) → X i) ≃ᵤ ((i : ι) → X i)) (piCongrRight (β₁ := X) (β₂ := X) fun (i : ι) ↦ UniformEquiv.refl (X i))
    (UniformEquiv.refl ((i : ι) → X i))

Tactic:
rfl

Premises used: UniformEquiv.piCongrRight, UniformEquiv.refl, Equiv.refl, rfl
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
⊢ IsUniformInducing (α := ULift.{v, u} α) (Equiv.toFun Equiv.ulift)

Tactic:
have hf : IsUniformInducing (@Equiv.ulift.{v, u} α).toFun := ⟨rfl⟩
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
hf : IsUniformInducing (α := ULift.{v, u} α) (Equiv.toFun Equiv.ulift)
simp_rw : UniformContinuous.{u, u} (α := α) (Equiv.toFun Equiv.ulift ∘ Equiv.invFun Equiv.ulift)
⊢ UniformContinuous (α := α) (Equiv.invFun Equiv.ulift)

Tactic:
simp_rw [hf.uniformContinuous_iff]

Premises used: IsUniformInducing.uniformContinuous_iff
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
hf : IsUniformInducing (α := ULift.{v, u} α) (Equiv.toFun Equiv.ulift)
⊢ UniformContinuous.{u, u} (α := α) (Equiv.toFun Equiv.ulift ∘ Equiv.invFun Equiv.ulift)

Tactic:
uniformContinuous_id

Premises used: uniformContinuous_id
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
hf : IsUniformInducing (α := ULift.{v, u} α) (Equiv.toFun Equiv.ulift)
⊢ UniformContinuous.{u, u} (α := α) (Equiv.toFun Equiv.ulift ∘ Equiv.invFun Equiv.ulift)

Tactic:
exact uniformContinuous_id

Premises used: uniformContinuous_id
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
p : α → Prop
q : β → Prop
e : α ≃ᵤ β
h : ∀ (a : α), p a ↔ q ((e : (a : α) → β) a)
⊢ UniformContinuous (e.subtypeEquiv (p := p) (q := q) h).toFun

Tactic:
simpa [Equiv.coe_subtypeEquiv_eq_map] using e.uniformContinuous.subtype_map _

Premises used: UniformContinuous.subtype_map, UniformEquiv.uniformContinuous, Equiv.coe_subtypeEquiv_eq_map
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
p : α → Prop
q : β → Prop
e : α ≃ᵤ β
h : ∀ (a : α), p a ↔ q ((e : (a : α) → β) a)
⊢ UniformContinuous (e.subtypeEquiv (p := p) (q := q) h).invFun

Tactic:
simpa [Equiv.coe_subtypeEquiv_eq_map] using e.symm.uniformContinuous.subtype_map _

Premises used: UniformContinuous.subtype_map, UniformEquiv.symm, UniformEquiv.uniformContinuous, Equiv.coe_subtypeEquiv_eq_map
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
f : α ≃ β
hf : IsUniformInducing.{u, u_1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ UniformContinuous (β := β) ((⇑f : (a : α) → β) ∘ f.invFun)

Tactic:
simpa using uniformContinuous_id

Premises used: uniformContinuous_id
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : CompactSpace α
f : α → β
h : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
rw rw₁ : map (Prod.map f f) (𝓤 α) = map (Prod.map f f) (𝓤 α)
⊢ map (Prod.map f f) (𝓤 α) = map (Prod.map f f) (𝓝ˢ (diagonal α))

Tactic:
rw [nhdsSet_diagonal_eq_uniformity]

Premises used: nhdsSet_diagonal_eq_uniformity
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
rw : UniformContinuous (s.restrict (π := fun (a : α) ↦ β) f)
⊢ UniformContinuousOn f s

Tactic:
rw [uniformContinuousOn_iff_restrict]

Premises used: uniformContinuousOn_iff_restrict
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
⊢ CompactSpace.{u_1} (↑s : Type u_1)

Tactic:
rw [isCompact_iff_compactSpace] at hs

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
hs₁ : CompactSpace.{u_1} (↑s : Type u_1)
⊢ ContinuousOn f s

Tactic:
rw [isCompact_iff_compactSpace] at hs

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace.{u_1} (↑s : Type u_1)
hf : ContinuousOn f s
⊢ Continuous[instTopologicalSpaceSubtype, inst_1.toTopologicalSpace] (s.restrict (π := fun (a : α) ↦ β) f)

Tactic:
rw [continuousOn_iff_continuous_restrict] at hf

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace.{u_1} (↑s : Type u_1)
hf : Continuous[instTopologicalSpaceSubtype, inst_1.toTopologicalSpace] (s.restrict (π := fun (a : α) ↦ β) f)
⊢ UniformContinuous (s.restrict (π := fun (a : α) ↦ β) f)

Tactic:
CompactSpace.uniformContinuous_of_continuous hf

Premises used: CompactSpace.uniformContinuous_of_continuous
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace.{u_1} (↑s : Type u_1)
hf : Continuous[instTopologicalSpaceSubtype, inst_1.toTopologicalSpace] (s.restrict (π := fun (a : α) ↦ β) f)
⊢ UniformContinuous (s.restrict (π := fun (a : α) ↦ β) f)

Tactic:
exact CompactSpace.uniformContinuous_of_continuous hf

Premises used: CompactSpace.uniformContinuous_of_continuous
-- 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 ∈ 𝓤 β
obtain :
  ∀ (t : Set (β × β)) (ht : t ∈ 𝓤 β) (htsymm : SetRel.IsSymm t) (htr : SetRel.comp t t ⊆ r),
    {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α
⊢ {x : α × α | x.1 ∈ s → (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 β
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
choose :
  ∀ (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}),
    {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α
⊢ {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α

Tactic:
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)

Premises used: mem_nhds_left, ContinuousAt.preimage_mem_nhds, exists_mem_nhds_ball_subset_of_mem_nhds
-- 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}
obtain :
  ∀ (fs : Finset (↑s : Type u_1)) (hsU : s ⊆ ⋃ x ∈ fs, U (↑x : α) ⋯), {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α
⊢ {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α

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

Premises used: IsCompact.elim_nhds_subcover'
-- 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 : α) ⋯
apply : Subset.{u_1} (α := Set (α × α)) (⋂ i ∈ fs, T (↑i : α) ⋯) {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ r}
⊢ {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)

Premises used: Iff.mpr, Filter.biInter_finset_mem, Subtype.val, Subtype.property, Filter.mem_of_superset
-- 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
obtain : ∀ (a : (↑s : Type u_1)) (ha : a ∈ fs) (haU : (a₁, a₂).1 ∈ U (↑a : α) ⋯), (f (a₁, a₂).1, f (a₁, a₂).2) ∈ r
⊢ (f (a₁, a₂).1, f (a₁, a₂).2) ∈ r

Tactic:
obtain ⟨a, ha, haU⟩ := Set.mem_iUnion₂.1 (hsU h₁)

Premises used: Set.mem_iUnion₂, Iff.mp