awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ Continuous[inst, inst_1] (⇑f : (a : α) → β)

Tactic:
f.continuous_toFun

Premises used: ContinuousMap.continuous_toFun, ZeroAtInftyContinuousMap.toContinuousMap
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ Continuous[inst, inst_1] (⇑f : (a : α) → β)

Tactic:
exact f.continuous_toFun

Premises used: ContinuousMap.continuous_toFun, ZeroAtInftyContinuousMap.toContinuousMap
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = (⇑f : (a : α) → β)
simp_rw : Tendsto.{u, v} (β := β) (⇑f : (a : α) → β) (cocompact α) (𝓝 0)
⊢ Tendsto f' (cocompact α) (𝓝 0)

Tactic:
simp_rw [h]
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ Tendsto.{u, v} (β := β) (⇑f : (a : α) → β) (cocompact α) (𝓝 0)

Tactic:
f.zero_at_infty'

Premises used: ZeroAtInftyContinuousMap.zero_at_infty'
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ Tendsto.{u, v} (β := β) (⇑f : (a : α) → β) (cocompact α) (𝓝 0)

Tactic:
exact f.zero_at_infty'

Premises used: ZeroAtInftyContinuousMap.zero_at_infty'
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : α →C₀ β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : α →C₀ β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
inst_3 : IsEmpty α
f g : α →C₀ β
⊢ f = g

Tactic:
ext <| IsEmpty.elim ‹_›

Premises used: IsEmpty.elim, ZeroAtInftyContinuousMap.ext
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
inst_5 : CompactSpace α
f : C(α, β)
⊢ Tendsto.{u, v} (β := β) (⇑f : (a : α) → β) (cocompact α) (𝓝 0)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
G : Type u_2
inst_3 : FunLike G α β
inst_4 : ContinuousMapClass G α β
inst_5 : CompactSpace α
⊢ ∀ (f : G), Tendsto.{u, v} (β := β) (⇑f : (a : α) → β) (cocompact α) (𝓝 0)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
⊢ Eq (α := (a : α) → β) (⇑0 : (a : α) → β) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
inst_2 : Zero β
⊢ Eq.{v + 1} (α := β) ((0 : (a : α) → β) x : β) (0 : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
inst_2 : MulZeroClass β
inst_3 : ContinuousMul β
f g : α →C₀ β
⊢ Tendsto (HMul.hMul (α := C(α, β)) (↑f : C(α, β)) (↑g : C(α, β))).toFun (cocompact α) (𝓝 0)

Tactic:
simpa only [mul_zero] using (zero_at_infty f).mul (zero_at_infty g)

Premises used: ZeroAtInftyContinuousMapClass.zero_at_infty, MulZeroClass.mul_zero, Filter.Tendsto.mul
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : MulZeroClass β
inst_3 : ContinuousMul β
f g : α →C₀ β
⊢ (⇑(f * g) : (a : α) → β) = HMul.hMul (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
inst_2 : MulZeroClass β
inst_3 : ContinuousMul β
f g : α →C₀ β
⊢ (f * g : (a : α) → β) x = HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
inst_2 : AddZeroClass β
inst_3 : ContinuousAdd β
f g : α →C₀ β
⊢ Tendsto (HAdd.hAdd (α := C(α, β)) (↑f : C(α, β)) (↑g : C(α, β))).toFun (cocompact α) (𝓝 0)

Tactic:
simpa only [add_zero] using (zero_at_infty f).add (zero_at_infty g)

Premises used: ZeroAtInftyContinuousMapClass.zero_at_infty, Filter.Tendsto.add, add_zero
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AddZeroClass β
inst_3 : ContinuousAdd β
f g : α →C₀ β
⊢ (⇑(f + g) : (a : α) → β) = HAdd.hAdd (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
inst_2 : AddZeroClass β
inst_3 : ContinuousAdd β
f g : α →C₀ β
⊢ (f + g : (a : α) → β) x = HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
inst_2 : Zero β
R : Type u_2
inst_3 : Zero R
inst_4 : SMulWithZero R β
inst_5 : ContinuousConstSMul R β
r : R
f : α →C₀ β
⊢ Tendsto (HSMul.hSMul (β := C(α, β)) r (↑f : C(α, β))).toFun (cocompact α) (𝓝 0)

Tactic:
simpa [smul_zero] using (zero_at_infty f).const_smul r

Premises used: smul_zero, ZeroAtInftyContinuousMapClass.zero_at_infty, Filter.Tendsto.const_smul
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
R : Type u_2
inst_3 : Zero R
inst_4 : SMulWithZero R β
inst_5 : ContinuousConstSMul R β
r : R
f : α →C₀ β
⊢ (⇑(r • f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) r (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
R : Type u_2
inst_3 : Zero R
inst_4 : SMulWithZero R β
inst_5 : ContinuousConstSMul R β
r : R
f : α →C₀ β
x : α
⊢ (r • f : (a : α) → β) x = HSMul.hSMul (β := β) r ((f : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
inst_2 : AddGroup β
inst_3 : IsTopologicalAddGroup β
f_1 g f : α →C₀ β
⊢ Tendsto (ContinuousMap.toFun (-(↑f : C(α, β)))) (cocompact α) (𝓝 0)

Tactic:
simpa only [neg_zero] using (zero_at_infty f).neg

Premises used: Filter.Tendsto.neg, ZeroAtInftyContinuousMapClass.zero_at_infty, neg_zero
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AddGroup β
inst_3 : IsTopologicalAddGroup β
f : α →C₀ β
⊢ Eq (α := (a : α) → β) (⇑(-f) : (a : α) → β) (-(⇑f : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
inst_2 : AddGroup β
inst_3 : IsTopologicalAddGroup β
f : α →C₀ β
⊢ Eq.{v + 1} (α := β) ((-f : (a : α) → β) x : β) (-(f : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
inst_2 : AddGroup β
inst_3 : IsTopologicalAddGroup β
f_1 g_1 f g : α →C₀ β
⊢ Tendsto (HSub.hSub (α := C(α, β)) (↑f : C(α, β)) (↑g : C(α, β))).toFun (cocompact α) (𝓝 0)

Tactic:
simpa only [sub_zero] using (zero_at_infty f).sub (zero_at_infty g)

Premises used: sub_zero, ZeroAtInftyContinuousMapClass.zero_at_infty, Filter.Tendsto.sub
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AddGroup β
inst_3 : IsTopologicalAddGroup β
f g : α →C₀ β
⊢ (⇑(f - g) : (a : α) → β) = HSub.hSub (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
inst_2 : AddGroup β
inst_3 : IsTopologicalAddGroup β
f g : α →C₀ β
⊢ (f - g : (a : α) → β) x = HSub.hSub (α := β) (β := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
inst_2 : Zero β
R : Type u_2
inst_3 : Zero R
inst_4 : SMulWithZero R β
inst_5 : SMulWithZero.{u_2, v} Rᵐᵒᵖ β
inst_6 : ContinuousConstSMul R β
inst_7 : IsCentralScalar R β
⊢ IsCentralScalar R (α →C₀ β)

Tactic:
⟨fun _ _ => ext fun _ => op_smul_eq_smul _ _⟩

Premises used: ZeroAtInftyContinuousMap.ext, toContinuousMap, IsCentralScalar.mk, DFunLike.coe, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_2
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : IsScalarTower R β β
r : R
f g : α →C₀ β
h : ∀ (x : α), Eq.{v + 1} (α := β) (((r • f) • g : (a : α) → β) x : β) ((r • f • g : (a : α) → β) x : β)
⊢ (r • f) • g = r • f • g

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_2
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : IsScalarTower R β β
r : R
f g : α →C₀ β
x_1 : α
h :
  HMul.hMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
⊢ Eq.{v + 1} (α := β) (((r • f) • g : (a : α) → β) x_1 : β) ((r • f • g : (a : α) → β) x_1 : β)

Tactic:
simp only [smul_eq_mul, coe_mul, coe_smul, Pi.mul_apply, Pi.smul_apply]

Premises used: ZeroAtInftyContinuousMap.coe_smul, Pi.mul_apply, ZeroAtInftyContinuousMap.coe_mul, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_2
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : IsScalarTower R β β
r : R
f g : α →C₀ β
x_1 : α
h :
  HSMul.hSMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
h₁ :
  HSMul.hSMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
h₂ h₃ :
  r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
⊢ HMul.hMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)

Tactic:
rw [← smul_eq_mul, ← smul_eq_mul, smul_assoc]

Premises used: smul_assoc, smul_eq_mul
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_2
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : SMulCommClass R β β
r : R
f g : α →C₀ β
h : ∀ (x : α), Eq.{v + 1} (α := β) ((r • f • g : (a : α) → β) x : β) ((f • r • g : (a : α) → β) x : β)
⊢ r • f • g = f • r • g

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_2
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : SMulCommClass R β β
r : R
f g : α →C₀ β
x_1 : α
h :
  r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
⊢ Eq.{v + 1} (α := β) ((r • f • g : (a : α) → β) x_1 : β) ((f • r • g : (a : α) → β) x_1 : β)

Tactic:
simp only [smul_eq_mul, coe_smul, coe_mul, Pi.smul_apply, Pi.mul_apply]

Premises used: ZeroAtInftyContinuousMap.coe_smul, Pi.mul_apply, ZeroAtInftyContinuousMap.coe_mul, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_2
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : SMulCommClass R β β
r : R
f g : α →C₀ β
x_1 : α
h :
  r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
h₁ :
  r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HSMul.hSMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
h₂ h₃ :
  HSMul.hSMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β)) =
    HSMul.hSMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
⊢ r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))

Tactic:
rw [← smul_eq_mul, ← smul_eq_mul, smul_comm]

Premises used: smul_eq_mul, SMulCommClass.smul_comm
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
β : Type v
γ : Type w
inst : UniformSpace β
inst_1 : UniformSpace γ
inst_2 : Zero γ
inst_3 : FunLike F β γ
inst_4 : ZeroAtInftyContinuousMapClass F β γ
f : F
⊢ UniformContinuous.{v, w} (α := β) (β := γ) (⇑f : (a : β) → γ)

Tactic:
(map_continuous f).uniformContinuous_of_tendsto_cocompact (zero_at_infty f)

Premises used: ZeroAtInftyContinuousMapClass.zero_at_infty, ContinuousMapClass.map_continuous, Continuous.uniformContinuous_of_tendsto_cocompact
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : F
obtain :
  ∀ (K : Set α) (hK₁ : IsCompact K) (hK₂ : Kᶜ ⊆ preimage.{u, v} (β := β) (⇑f : (a : α) → β) (closedBall 0 1)),
    ∃ (C : ℝ), ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C

Tactic:
obtain ⟨K : Set α, hK₁, hK₂⟩ := mem_cocompact.mp
    (tendsto_def.mp (zero_at_infty (f : F)) _ (closedBall_mem_nhds (0 : β) zero_lt_one))

Premises used: Filter.tendsto_def, Metric.closedBall_mem_nhds, ZeroAtInftyContinuousMapClass.zero_at_infty, zero_lt_one, Iff.mp, OfNat.ofNat, Filter.mem_cocompact, Set
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ preimage.{u, v} (β := β) (⇑f : (a : α) → β) (closedBall 0 1)
obtain :
  ∀ (C : ℝ) (hC : Subset.{v} (α := Set β) ((⇑f : (a : α) → β) '' K) (closedBall 0 C)),
    ∃ (C : ℝ), ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C

Tactic:
obtain ⟨C, hC⟩ := (hK₁.image (map_continuous f)).isBounded.subset_closedBall (0 : β)

Premises used: IsCompact.isBounded, BoundedContinuousFunction.C, Bornology.IsBounded.subset_closedBall, ContinuousMapClass.map_continuous, OfNat.ofNat, IsCompact.image
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ preimage.{u, v} (β := β) (⇑f : (a : α) → β) (closedBall 0 1)
C : ℝ
hC : Subset.{v} (α := Set β) ((⇑f : (a : α) → β) '' K) (closedBall 0 C)
⊢ ∃ (C : ℝ), ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C

Tactic:
⟨max C 1 + max C 1, fun x y => ?_⟩

Premises used: HAdd.hAdd, Max.max, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ preimage.{u, v} (β := β) (⇑f : (a : α) → β) (closedBall 0 1)
C : ℝ
hC : Subset.{v} (α := Set β) ((⇑f : (a : α) → β) '' K) (closedBall 0 C)
refine : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ max C 1 + max C 1
⊢ ∃ (C : ℝ), ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C

Tactic:
refine ⟨max C 1 + max C 1, fun x y => ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ preimage.{u, v} (β := β) (⇑f : (a : α) → β) (closedBall 0 1)
C : ℝ
hC : Subset.{v} (α := Set β) ((⇑f : (a : α) → β) '' K) (closedBall 0 C)
x_1 y x : α
pos : ∀ (hx : x ∈ K), Membership.mem.{v, v} (α := β) (γ := Set β) (closedBall 0 (max C 1)) ((f : (a : α) → β) x : β)
neg : ∀ (hx : x ∉ K), Membership.mem.{v, v} (α := β) (γ := Set β) (closedBall 0 (max C 1)) ((f : (a : α) → β) x : β)
⊢ Membership.mem.{v, v} (α := β) (γ := Set β) (closedBall 0 (max C 1)) ((f : (a : α) → β) x : β)

Tactic:
by_cases hx : x ∈ K
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ preimage.{u, v} (β := β) (⇑f : (a : α) → β) (closedBall 0 1)
C : ℝ
hC : Subset.{v} (α := Set β) ((⇑f : (a : α) → β) '' K) (closedBall 0 C)
x_1 y x : α
hx : x ∈ K
⊢ Membership.mem.{v, v} (α := β) (γ := Set β) (closedBall 0 (max C 1)) ((f : (a : α) → β) x : β)

Tactic:
(mem_closedBall.mp <| hC ⟨x, hx, rfl⟩).trans (le_max_left _ _)

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Iff.mp, Metric.mem_closedBall, LE.le.trans, Metric.closedBall, le_max_left, rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ preimage.{u, v} (β := β) (⇑f : (a : α) → β) (closedBall 0 1)
C : ℝ
hC : Subset.{v} (α := Set β) ((⇑f : (a : α) → β) '' K) (closedBall 0 C)
x_1 y x : α
hx : x ∈ K
⊢ Membership.mem.{v, v} (α := β) (γ := Set β) (closedBall 0 (max C 1)) ((f : (a : α) → β) x : β)

Tactic:
exact (mem_closedBall.mp <| hC ⟨x, hx, rfl⟩).trans (le_max_left _ _)

Premises used: And.intro, Exists.intro, Iff.mp, Metric.mem_closedBall, LE.le.trans, le_max_left, rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ preimage.{u, v} (β := β) (⇑f : (a : α) → β) (closedBall 0 1)
C : ℝ
hC : Subset.{v} (α := Set β) ((⇑f : (a : α) → β) '' K) (closedBall 0 C)
x_1 y x : α
hx : x ∉ K
⊢ Membership.mem.{v, v} (α := β) (γ := Set β) (closedBall 0 (max C 1)) ((f : (a : α) → β) x : β)

Tactic:
(mem_closedBall.mp <| mem_preimage.mp (hK₂ hx)).trans (le_max_right _ _)

Premises used: le_max_right, Set.Mem, setOf, Iff.mp, Metric.mem_closedBall, LE.le.trans, Metric.closedBall, Set.mem_preimage
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ preimage.{u, v} (β := β) (⇑f : (a : α) → β) (closedBall 0 1)
C : ℝ
hC : Subset.{v} (α := Set β) ((⇑f : (a : α) → β) '' K) (closedBall 0 C)
x_1 y x : α
hx : x ∉ K
⊢ Membership.mem.{v, v} (α := β) (γ := Set β) (closedBall 0 (max C 1)) ((f : (a : α) → β) x : β)

Tactic:
exact (mem_closedBall.mp <| mem_preimage.mp (hK₂ hx)).trans (le_max_right _ _)

Premises used: le_max_right, Iff.mp, Metric.mem_closedBall, LE.le.trans, Set.mem_preimage
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ preimage.{u, v} (β := β) (⇑f : (a : α) → β) (closedBall 0 1)
C : ℝ
hC : Subset.{v} (α := Set β) ((⇑f : (a : α) → β) '' K) (closedBall 0 C)
x y : α
⊢ ∀ (x : α), Membership.mem.{v, v} (α := β) (γ := Set β) (closedBall 0 (max C 1)) ((f : (a : α) → β) x : β)

Tactic:
have : ∀ x, f x ∈ closedBall (0 : β) (max C 1) := by
    intro x
    by_cases hx : x ∈ K
    · exact (mem_closedBall.mp <| hC ⟨x, hx, rfl⟩).trans (le_max_left _ _)
    · exact (mem_closedBall.mp <| mem_preimage.mp (hK₂ hx)).trans (le_max_right _ _)