awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α
this : ∀ (x : α), Membership.mem.{v, v} (α := β) (γ := Set β) (closedBall 0 (max C 1)) ((f : (a : α) → β) x : β)
⊢ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ max C 1 + max C 1

Tactic:
(dist_triangle (f x) 0 (f y)).trans
    (add_le_add (mem_closedBall.mp <| this x) (mem_closedBall'.mp <| this y))

Premises used: dist_triangle, add_le_add, Metric.mem_closedBall', Iff.mp, Metric.mem_closedBall, LE.le.trans, OfNat.ofNat, DFunLike.coe
-- 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 : α
this : ∀ (x : α), Membership.mem.{v, v} (α := β) (γ := Set β) (closedBall 0 (max C 1)) ((f : (a : α) → β) x : β)
⊢ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ max C 1 + max C 1

Tactic:
exact (dist_triangle (f x) 0 (f y)).trans
    (add_le_add (mem_closedBall.mp <| this x) (mem_closedBall'.mp <| this y))

Premises used: dist_triangle, add_le_add, Metric.mem_closedBall', Iff.mp, Metric.mem_closedBall, LE.le.trans, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →C₀ β
⊢ Bornology.IsBounded.{v} (α := β) (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β))

Tactic:
isBounded_range_iff.2 (ZeroAtInftyContinuousMap.bounded f)

Premises used: Iff.mpr, ZeroAtInftyContinuousMap.bounded, Metric.isBounded_range_iff
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →C₀ β
s : Set α
⊢ Bornology.IsBounded.{v} (α := β) ((⇑f : (a : α) → β) '' s)

Tactic:
f.isBounded_range.subset <| image_subset_range _ _

Premises used: Set.image_subset_range, Bornology.IsBounded.subset, ZeroAtInftyContinuousMap.isBounded_range
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
⊢ BoundedContinuousMapClass F α β

Tactic:
{ ‹ZeroAtInftyContinuousMapClass F α β› with
    map_bounded := fun f => ZeroAtInftyContinuousMap.bounded f }

Premises used: ZeroAtInftyContinuousMap.bounded, BoundedContinuousMapClass.mk
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f g : α →C₀ β
h : f.toBCF = g.toBCF
h₁ : ∀ (x : α), Eq.{v + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f g : α →C₀ β
h : f.toBCF = g.toBCF
x : α
⊢ Eq.{v + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
simpa only using DFunLike.congr_fun h x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f g : α →C₀ β
⊢ dist f.toBCF g.toBCF = dist f g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
ι : Type u_2
F : ι → α →C₀ β
f : α →C₀ β
l : Filter ι
⊢ Tendsto F l (𝓝 f) ↔
    TendstoUniformly.{u, v, u_2} (α := α) (β := β) (fun (i : ι) ↦ (⇑(F i) : (a : α) → β)) (⇑f : (a : α) → β) l

Tactic:
simpa only [Metric.tendsto_nhds] using
    @BoundedContinuousFunction.tendsto_iff_tendstoUniformly _ _ _ _ _ (fun i => (F i).toBCF)
      f.toBCF l

Premises used: Metric.tendsto_nhds, BoundedContinuousFunction.tendsto_iff_tendstoUniformly
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ : ∀ (x1 x2 : α →C₀ β), edist x1.toBCF x2.toBCF = edist x1 x2
⊢ Isometry (α := α →C₀ β) toBCF

Tactic:
tauto
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
⊢ IsClosed (X := α →ᵇ β) (range (ι := α →C₀ β) toBCF)

Tactic:
isClosed_iff_clusterPt.mpr fun f hf => ?_

Premises used: Iff.mpr, isClosed_iff_clusterPt
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
refine :
  ∀ (f : α →ᵇ β) (hf : ClusterPt f (𝓟 (range (ι := α →C₀ β) toBCF))),
    Membership.mem (γ := Set (α →ᵇ β)) (range (ι := α →C₀ β) toBCF) f
⊢ IsClosed (X := α →ᵇ β) (range (ι := α →C₀ β) toBCF)

Tactic:
refine isClosed_iff_clusterPt.mpr fun f hf => ?_

Premises used: Iff.mpr, isClosed_iff_clusterPt
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ClusterPt f (𝓟 (range (ι := α →C₀ β) toBCF))
⊢ ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty

Tactic:
rw [clusterPt_principal_iff] at hf

Premises used: clusterPt_principal_iff
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
⊢ Tendsto.{u, v} (β := β) (⇑f : (a : α) → β) (cocompact α) (𝓝 0)

Tactic:
Metric.tendsto_nhds.mpr fun ε hε => ?_

Premises used: Iff.mpr, Metric.tendsto_nhds
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
refine : ∀ (ε : ℝ) (hε : ε > 0), ∀ᶠ (x : α) in cocompact α, dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < ε
⊢ Tendsto.{u, v} (β := β) (⇑f : (a : α) → β) (cocompact α) (𝓝 0)

Tactic:
refine Metric.tendsto_nhds.mpr fun ε hε => ?_

Premises used: Iff.mpr, Metric.tendsto_nhds
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
ε : ℝ
hε : ε > 0
obtain :
  ∀ (g : α →C₀ β) (hg : g.toBCF ∈ ball f (ε / 2)),
    ∀ᶠ (x : α) in cocompact α, dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < ε
⊢ ∀ᶠ (x : α) in cocompact α, dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < ε

Tactic:
obtain ⟨_, hg, g, rfl⟩ := hf (ball f (ε / 2)) (ball_mem_nhds f <| half_pos hε)

Premises used: half_pos, HDiv.hDiv, Metric.ball, Metric.ball_mem_nhds, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : g.toBCF ∈ ball f (ε / 2)
⊢ ∀ᶠ (x : α) in cocompact α, dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < ε

Tactic:
(Metric.tendsto_nhds.mp (zero_at_infty g) (ε / 2) (half_pos hε)).mp
      (Eventually.of_forall fun x hx => ?_)

Premises used: half_pos, Metric.tendsto_nhds, HDiv.hDiv, Filter.Eventually.of_forall, ZeroAtInftyContinuousMapClass.zero_at_infty, Filter.Eventually.mp, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : g.toBCF ∈ ball f (ε / 2)
refine :
  ∀ (x : α) (hx : dist.{v} (α := β) ((g : (a : α) → β) x : β) (0 : β) < ε / 2),
    dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < ε
⊢ ∀ᶠ (x : α) in cocompact α, dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < ε

Tactic:
refine (Metric.tendsto_nhds.mp (zero_at_infty g) (ε / 2) (half_pos hε)).mp
      (Eventually.of_forall fun x hx => ?_)

Premises used: half_pos, Metric.tendsto_nhds, HDiv.hDiv, Filter.Eventually.of_forall, ZeroAtInftyContinuousMapClass.zero_at_infty, Filter.Eventually.mp, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : g.toBCF ∈ ball f (ε / 2)
x : α
hx : dist.{v} (α := β) ((g : (a : α) → β) x : β) (0 : β) < ε / 2
⊢ dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) ≤
    dist.{v} (α := β) ((g.toBCF : (a : α) → β) x : β) ((f : (a : α) → β) x : β) +
      dist.{v} (α := β) ((g : (a : α) → β) x : β) (0 : β)

Tactic:
dist_triangle_left _ _ _

Premises used: dist_triangle_left
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : g.toBCF ∈ ball f (ε / 2)
x : α
hx : dist.{v} (α := β) ((g : (a : α) → β) x : β) (0 : β) < ε / 2
⊢ dist.{v} (α := β) ((g.toBCF : (a : α) → β) x : β) ((f : (a : α) → β) x : β) +
      dist.{v} (α := β) ((g : (a : α) → β) x : β) (0 : β) <
    dist g.toBCF f + ε / 2

Tactic:
add_lt_add_of_le_of_lt (dist_coe_le_dist x) hx

Premises used: add_lt_add_of_le_of_lt, BoundedContinuousFunction.dist_coe_le_dist
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : g.toBCF ∈ ball f (ε / 2)
x : α
hx : dist.{v} (α := β) ((g : (a : α) → β) x : β) (0 : β) < ε / 2
grw : ε / 2 + ε / 2 ≤ ε
grw₁ grw₂ : ε ≤ ε
⊢ dist g.toBCF f + ε / 2 ≤ ε

Tactic:
grw [mem_ball.1 hg, add_halves ε]

Premises used: add_halves, Metric.mem_ball, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : g.toBCF ∈ ball f (ε / 2)
x : α
hx : Dist.dist.{v} (α := β) ((g : (a : α) → β) x : β) (0 : β) < ε / 2
dist : Dist.dist g.toBCF f + ε / 2 ≤ ε
⊢ Dist.dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < ε

Tactic:
calc
      dist (f x) 0 ≤ dist (g.toBCF x) (f x) + dist (g x) 0 := dist_triangle_left _ _ _
      _ < dist g.toBCF f + ε / 2 := add_lt_add_of_le_of_lt (dist_coe_le_dist x) hx
      _ ≤ ε := by grw [mem_ball.1 hg, add_halves ε]

Premises used: add_lt_add_of_le_of_lt, ZeroAtInftyContinuousMap.toBCF, dist_triangle_left, BoundedContinuousFunction.dist_coe_le_dist, Dist.dist, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
⊢ Tendsto.{u, v} (β := β) (⇑f : (a : α) → β) (cocompact α) (𝓝 0)

Tactic:
have : Tendsto f (cocompact α) (𝓝 0) := by
    refine Metric.tendsto_nhds.mpr fun ε hε => ?_
    obtain ⟨_, hg, g, rfl⟩ := hf (ball f (ε / 2)) (ball_mem_nhds f <| half_pos hε)
    refine (Metric.tendsto_nhds.mp (zero_at_infty g) (ε / 2) (half_pos hε)).mp
      (Eventually.of_forall fun x hx => ?_)
    calc
      dist (f x) 0 ≤ dist (g.toBCF x) (f x) + dist (g x) 0 := dist_triangle_left _ _ _
      _ < dist g.toBCF f + ε / 2 := add_lt_add_of_le_of_lt (dist_coe_le_dist x) hx
      _ ≤ ε := by grw [mem_ball.1 hg, add_halves ε]
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
this : Tendsto.{u, v} (β := β) (⇑f : (a : α) → β) (cocompact α) (𝓝 0)
⊢ Membership.mem (γ := Set (α →ᵇ β)) (range (ι := α →C₀ β) toBCF) f

Tactic:
⟨⟨f.toContinuousMap, this⟩, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, ZeroAtInftyContinuousMap.mk, Set.range, rfl, BoundedContinuousFunction.toContinuousMap
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range (ι := α →C₀ β) toBCF).Nonempty
this : Tendsto.{u, v} (β := β) (⇑f : (a : α) → β) (cocompact α) (𝓝 0)
⊢ Membership.mem (γ := Set (α →ᵇ β)) (range (ι := α →C₀ β) toBCF) f

Tactic:
exact ⟨⟨f.toContinuousMap, this⟩, rfl⟩
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero β
inst_3 : FunLike F α β
inst_4 : ZeroAtInftyContinuousMapClass F α β
f g : α →C₀ β
inst_5 : CompleteSpace β
⊢ CompleteSpace (α →C₀ β)

Tactic:
(completeSpace_iff_isComplete_range isometry_toBCF.isUniformInducing).mpr
    isClosed_range_toBCF.isComplete

Premises used: Iff.mpr, ZeroAtInftyContinuousMap.isClosed_range_toBCF, ZeroAtInftyContinuousMap.isometry_toBCF, IsClosed.isComplete, Isometry.isUniformInducing, completeSpace_iff_isComplete_range
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →C₀ β
⊢ ‖f.toBCF‖ = ‖f‖

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AddMonoid β
inst_3 : StarAddMonoid β
inst_4 : ContinuousStar β
f : α →C₀ β
⊢ Tendsto.{u, v} (β := β) (fun (x : α) ↦ star ((f : (a : α) → β) x)) (cocompact α) (𝓝 0)

Tactic:
simpa only [star_zero] using (continuous_star.tendsto (0 : β)).comp (zero_at_infty f)

Premises used: ContinuousStar.continuous_star, ZeroAtInftyContinuousMapClass.zero_at_infty, Continuous.tendsto, star_zero, Filter.Tendsto.comp, OfNat.ofNat
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AddMonoid β
inst_3 : StarAddMonoid β
inst_4 : ContinuousStar β
f : α →C₀ β
⊢ Eq (α := (a : α) → β) (⇑(star f) : (a : α) → β) (star (⇑f : (a : α) → β))

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
β : Type v
γ : Type w
δ : Type u_2
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
inst_2 : TopologicalSpace δ
inst_3 : Zero δ
f : γ →C₀ δ
g : β →co γ
⊢ Eq (α := (a : β) → δ) (⇑(f.comp g) : (a : β) → δ)
    (Function.comp.{v + 1, w + 1, u_2 + 1} (β := γ) (⇑f : (a : γ) → δ) (⇑g : (a : β) → γ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
γ : Type w
δ : Type u_2
inst : TopologicalSpace γ
inst_1 : TopologicalSpace δ
inst_2 : Zero δ
f : γ →C₀ δ
⊢ f.comp (CocompactMap.id γ) = f

Tactic:
ext fun _ => rfl

Premises used: ZeroAtInftyContinuousMap.ext, rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
δ : Type u_2
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
inst_4 : Zero δ
f : γ →C₀ δ
g : β →co γ
h : α →co β
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: ContinuousMap.comp, toContinuousMap, ZeroAtInftyContinuousMap.comp, rfl
-- Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty
Goal:
β : Type v
γ : Type w
δ : Type u_2
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
inst_2 : TopologicalSpace δ
inst_3 : Zero δ
g : β →co γ
⊢ Eq (α := β →C₀ δ) (comp 0 g) 0

Tactic:
rfl

Premises used: ContinuousMap.comp, ZeroAtInftyContinuousMap.comp, ContinuousMap.const, rfl
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ContinuousWithinAt f s x
⊢ Tendsto f (𝓝[s] x) (𝓝 (f x))

Tactic:
h

Premises used: ContinuousWithinAt
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
rw : ContinuousWithinAt f univ x ↔ Tendsto f (𝓝 x) (𝓝 (f x))
rw₁ : Tendsto f (𝓝[univ] x) (𝓝 (f x)) ↔ Tendsto f (𝓝 x) (𝓝 (f x))
rw₂ rw₃ : Tendsto f (𝓝 x) (𝓝 (f x)) ↔ Tendsto f (𝓝 x) (𝓝 (f x))
⊢ ContinuousWithinAt f univ x ↔ ContinuousAt f x

Tactic:
rw [ContinuousAt, ContinuousWithinAt, nhdsWithin_univ]

Premises used: ContinuousWithinAt, nhdsWithin_univ, ContinuousAt
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
⊢ ContinuousOn f univ ↔ Continuous[inst, inst_1] f

Tactic:
simp [continuous_iff_continuousAt, ContinuousOn, ContinuousAt, ContinuousWithinAt,
    nhdsWithin_univ]

Premises used: ContinuousWithinAt, nhdsWithin_univ, ContinuousAt, ContinuousOn, continuous_iff_continuousAt
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
s : Set α
h : x ∈ s
⊢ ContinuousWithinAt f s x ↔
    ContinuousAt (s.restrict (π := fun (a : α) ↦ β) f) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h)

Tactic:
tendsto_nhdsWithin_iff_subtype h f _

Premises used: ContinuousWithinAt, ContinuousAt, tendsto_nhdsWithin_iff_subtype, Set.restrict
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
t : Set β
h : ContinuousWithinAt f s x
ht : MapsTo f s t
⊢ Tendsto f (𝓝[s] x) (𝓝[t] f x)

Tactic:
tendsto_inf.2 ⟨h, tendsto_principal.2 <| mem_inf_of_right <| mem_principal.2 <| ht⟩

Premises used: Iff.mpr, Filter.tendsto_inf, nhdsWithin, Filter.tendsto_principal, Filter.mem_inf_of_right, Filter.mem_principal, And.intro
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ContinuousWithinAt f s x
⊢ Tendsto f (𝓝[s] x) (𝓝[f '' s] f x)

Tactic:
h.tendsto_nhdsWithin (mapsTo_image _ _)

Premises used: Set.mapsTo_image, ContinuousWithinAt.tendsto_nhdsWithin
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
ctsf : ContinuousWithinAt f s x
⊢ 𝓝[s] x ≤ comap f (𝓝[f '' s] f x)

Tactic:
ctsf.tendsto_nhdsWithin_image.le_comap

Premises used: Filter.Tendsto.le_comap, ContinuousWithinAt.tendsto_nhdsWithin_image
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
t : Set β
h : ContinuousWithinAt f s x
ht : t ∈ 𝓝 (f x)
⊢ f ⁻¹' t ∈ 𝓝[s] x

Tactic:
h ht

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
t : Set β
h : ContinuousWithinAt f s x
ht : t ∈ 𝓝[f '' s] f x
⊢ f ⁻¹' t ∈ 𝓝[s] x

Tactic:
h.tendsto_nhdsWithin (mapsTo_image _ _) ht

Premises used: Set.Mem, setOf, Set.mapsTo_image, ContinuousWithinAt.tendsto_nhdsWithin, Set.preimage
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
y : β
s t : Set β
h : ContinuousWithinAt f (f ⁻¹' s) x
ht : t ∈ 𝓝[s] y
hxy : y = f x
⊢ t ∈ 𝓝[s] f x

Tactic:
rw [hxy] at ht
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
y : β
s t : Set β
h : ContinuousWithinAt f (f ⁻¹' s) x
ht : t ∈ 𝓝[s] y
hxy : y = f x
ht₁ : t ∈ 𝓝[s] f x
⊢ y = f x

Tactic:
rw [hxy] at ht
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
y : β
s t : Set β
h : ContinuousWithinAt f (f ⁻¹' s) x
ht : t ∈ 𝓝[s] f x
hxy : y = f x
⊢ f ⁻¹' t ∈ 𝓝[f ⁻¹' s] x

Tactic:
h.preimage_mem_nhdsWithin' (nhdsWithin_mono _ (image_preimage_subset f s) ht)

Premises used: ContinuousWithinAt.preimage_mem_nhdsWithin', Set.image_preimage_subset, nhdsWithin_mono
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
y : β
s t : Set β
h : ContinuousWithinAt f (f ⁻¹' s) x
ht : t ∈ 𝓝[s] f x
hxy : y = f x
⊢ f ⁻¹' t ∈ 𝓝[f ⁻¹' s] x

Tactic:
exact h.preimage_mem_nhdsWithin' (nhdsWithin_mono _ (image_preimage_subset f s) ht)

Premises used: ContinuousWithinAt.preimage_mem_nhdsWithin', Set.image_preimage_subset, nhdsWithin_mono
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : x ∉ closure[inst] s
⊢ 𝓝[s] x = ⊥

Tactic:
rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx

Premises used: mem_closure_iff_nhdsWithin_neBot, Filter.not_neBot
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : 𝓝[s] x = ⊥
rw : Tendsto f ⊥ (𝓝 (f x))
⊢ ContinuousWithinAt f s x

Tactic:
rw [ContinuousWithinAt, hx]

Premises used: ContinuousWithinAt
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : 𝓝[s] x = ⊥
⊢ Tendsto f ⊥ (𝓝 (f x))

Tactic:
tendsto_bot

Premises used: Filter.tendsto_bot
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : 𝓝[s] x = ⊥
⊢ Tendsto f ⊥ (𝓝 (f x))

Tactic:
exact tendsto_bot

Premises used: Filter.tendsto_bot
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔
    ∀ x ∈ s, ∀ (t : Set β), IsOpen[inst_1] t → f x ∈ t → ∃ (u : Set α), IsOpen[inst] u ∧ x ∈ u ∧ u ∩ s ⊆ f ⁻¹' t

Tactic:
simp only [ContinuousOn, ContinuousWithinAt, tendsto_nhds, mem_nhdsWithin]

Premises used: ContinuousWithinAt, mem_nhdsWithin, tendsto_nhds, ContinuousOn
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
hf : ContinuousOn f s
hx : x ∈ s
⊢ ContinuousWithinAt f s x

Tactic:
hf x hx
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
ht : MapsTo f s t
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (MapsTo.restrict f s t ht)

Tactic:
hf.restrict.codRestrict _

Premises used: Subtype.map, ContinuousOn.restrict, Continuous.codRestrict, Set.codRestrict, Set.restrict, Set.MapsTo.restrict