awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : CocompactMap α β
s : Set β
hs : IsCompact s
h's : IsClosed s
t : Set α
ht : IsCompact t
hts : ((⇑f : (a : α) → β) ⁻¹' s)ᶜᶜ ⊆ t
⊢ IsCompact.{u_1} (X := α) ((⇑f : (a : α) → β) ⁻¹' s)

Tactic:
exact
    ht.of_isClosed_subset (h's.preimage <| map_continuous f) (by simpa using hts)

Premises used: IsCompact.of_isClosed_subset, IsClosed.preimage, ContinuousMapClass.map_continuous
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : T2Space β
f : CocompactMap α β
s : Set β
hs : IsCompact s
⊢ IsCompact.{u_1} (X := α) ((⇑f : (a : α) → β) ⁻¹' s)

Tactic:
isCompact_preimage_of_isClosed f hs hs.isClosed

Premises used: CocompactMap.isCompact_preimage_of_isClosed, IsCompact.isClosed
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
⊢ Tendsto (⇑f : (a : α) → β) (cocompact α) (cocompact β)

Tactic:
CocompactMap.tendsto_of_forall_preimage fun K hK => ?_

Premises used: CocompactMap.tendsto_of_forall_preimage
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
refine : ∀ (K : Set β) (hK : IsCompact K), IsCompact.{u_1} (X := α) ((⇑f : (a : α) → β) ⁻¹' K)
⊢ Tendsto (⇑f : (a : α) → β) (cocompact α) (cocompact β)

Tactic:
refine CocompactMap.tendsto_of_forall_preimage fun K hK => ?_

Premises used: CocompactMap.tendsto_of_forall_preimage
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
K : Set β
hK : IsCompact K
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑f.symm : (a : β) → α) '' K) ((⇑f.toEquiv : (a : α) → β) ⁻¹' K)

Tactic:
have := f.toEquiv.image_symm_eq_preimage K
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
K : Set β
hK : IsCompact K
this : Eq.{u_1 + 1} (α := Set α) ((⇑f.symm : (a : β) → α) '' K) ((⇑f : (a : α) → β) ⁻¹' K)
rw : IsCompact.{u_1} (X := α) ((⇑f.symm : (a : β) → α) '' K)
⊢ IsCompact.{u_1} (X := α) ((⇑f : (a : α) → β) ⁻¹' K)

Tactic:
rw [← this]
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
K : Set β
hK : IsCompact K
this : Eq.{u_1 + 1} (α := Set α) ((⇑f.symm : (a : β) → α) '' K) ((⇑f : (a : α) → β) ⁻¹' K)
⊢ IsCompact.{u_1} (X := α) ((⇑f.symm : (a : β) → α) '' K)

Tactic:
hK.image f.symm.continuous

Premises used: Homeomorph.continuous, Homeomorph.symm, IsCompact.image
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
K : Set β
hK : IsCompact K
this : Eq.{u_1 + 1} (α := Set α) ((⇑f.symm : (a : β) → α) '' K) ((⇑f : (a : α) → β) ⁻¹' K)
⊢ IsCompact.{u_1} (X := α) ((⇑f.symm : (a : β) → α) '' K)

Tactic:
exact hK.image f.symm.continuous

Premises used: Homeomorph.continuous, Homeomorph.symm, IsCompact.image
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E
f : C(α, β)
h : ∀ (a : α), Eq.{u_2 + 1} (α := β) (((mkOfCompact f).toContinuousMap : (a : α) → β) a : β) ((f : (a : α) → β) a : β)
⊢ (mkOfCompact f).toContinuousMap = f

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E
f : C(α, β)
a : α
⊢ Eq.{u_2 + 1} (α := β) (((mkOfCompact f).toContinuousMap : (a : α) → β) a : β) ((f : (a : α) → β) a : β)

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E
f : α →ᵇ β
h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((mkOfCompact f.toContinuousMap : (a : α) → β) x : β) ((f : (a : α) → β) x : β)
⊢ mkOfCompact f.toContinuousMap = f

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E
f : α →ᵇ β
x : α
⊢ Eq.{u_2 + 1} (α := β) ((mkOfCompact f.toContinuousMap : (a : α) → β) x : β) ((f : (a : α) → β) x : β)

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
simp :
  ∀ (s : Set (C(α, β) × C(α, β))),
    (∃ (i : Prod.{u_1, u_2} (Set α) (Set (β × β))),
        (IsCompact i.1 ∧ ∃ (i_1 : ℝ), 0 < i_1 ∧ {p : β × β | dist p.1 p.2 ≤ i_1} ⊆ i.2) ∧
          {fg : C(α, β) × C(α, β) |
              ∀ x ∈ i.1, Membership.mem (α := β × β) i.2 (((fg.1 : (a : α) → β) x, (fg.2 : (a : α) → β) x) : β × β)} ⊆
            s) ↔
      ∃ (t : Set ((α →ᵇ β) × (α →ᵇ β))),
        (∃ (i : ℝ), 0 < i ∧ {p : (α →ᵇ β) × (α →ᵇ β) | dist p.1 p.2 ≤ i} ⊆ t) ∧
          ∀ (x y : C(α, β)),
            Membership.mem (α := (α →ᵇ β) × (α →ᵇ β)) t
                (((equivBoundedOfCompact α β : (a : C(α, β)) → α →ᵇ β) x,
                    (equivBoundedOfCompact α β : (a : C(α, β)) → α →ᵇ β) y) :
                  (α →ᵇ β) × (α →ᵇ β)) →
              (x, y) ∈ s
⊢ ∀ (s : Set (C(α, β) × C(α, β))),
    Membership.mem (γ := Filter (C(α, β) × C(α, β))) (uniformity C(α, β)) s ↔
      ∃ (t : Set ((α →ᵇ β) × (α →ᵇ β))),
        Membership.mem (γ := Filter ((α →ᵇ β) × (α →ᵇ β))) (uniformity (α →ᵇ β)) t ∧
          ∀ (x y : C(α, β)),
            Membership.mem (α := (α →ᵇ β) × (α →ᵇ β)) t
                (((equivBoundedOfCompact α β : (a : C(α, β)) → α →ᵇ β) x,
                    (equivBoundedOfCompact α β : (a : C(α, β)) → α →ᵇ β) y) :
                  (α →ᵇ β) × (α →ᵇ β)) →
              (x, y) ∈ s

Tactic:
simp only [hasBasis_compactConvergenceUniformity.mem_iff, uniformity_basis_dist_le.mem_iff]

Premises used: Filter.HasBasis.mem_iff, ContinuousMap.hasBasis_compactConvergenceUniformity, Metric.uniformity_basis_dist_le
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
⊢ ∀ (s : Set (C(α, β) × C(α, β))),
    (∃ (i : Prod.{u_1, u_2} (Set α) (Set (β × β))),
        (IsCompact i.1 ∧ ∃ (i_1 : ℝ), 0 < i_1 ∧ {p : β × β | dist p.1 p.2 ≤ i_1} ⊆ i.2) ∧
          {fg : C(α, β) × C(α, β) |
              ∀ x ∈ i.1, Membership.mem (α := β × β) i.2 (((fg.1 : (a : α) → β) x, (fg.2 : (a : α) → β) x) : β × β)} ⊆
            s) ↔
      ∃ (t : Set ((α →ᵇ β) × (α →ᵇ β))),
        (∃ (i : ℝ), 0 < i ∧ {p : (α →ᵇ β) × (α →ᵇ β) | dist p.1 p.2 ≤ i} ⊆ t) ∧
          ∀ (x y : C(α, β)),
            Membership.mem (α := (α →ᵇ β) × (α →ᵇ β)) t
                (((equivBoundedOfCompact α β : (a : C(α, β)) → α →ᵇ β) x,
                    (equivBoundedOfCompact α β : (a : C(α, β)) → α →ᵇ β) y) :
                  (α →ᵇ β) × (α →ᵇ β)) →
              (x, y) ∈ s

Tactic:
fun s =>
        ⟨fun ⟨⟨a, b⟩, ⟨_, ⟨ε, hε, hb⟩⟩, hs⟩ =>
          ⟨{ p | ∀ x, (p.1 x, p.2 x) ∈ b }, ⟨ε, hε, fun _ h x => hb ((dist_le hε.le).mp h x)⟩,
            fun f g h => hs fun x _ => h x⟩,
          fun ⟨_, ⟨ε, hε, ht⟩, hs⟩ =>
          ⟨⟨Set.univ, { p | dist p.1 p.2 ≤ ε }⟩, ⟨isCompact_univ, ⟨ε, hε, fun _ h => h⟩⟩,
            fun ⟨f, g⟩ h => hs _ _ (ht ((dist_le hε.le).mpr fun x => h x (mem_univ x)))⟩⟩

Premises used: Iff.mpr, _private.0.ContinuousMap.isUniformInducing_equivBoundedOfCompact.match_4, BoundedContinuousFunction.dist_le, Set.univ, setOf, Membership.mem, Exists, LT.lt.le, Prod.mk, HasSubset.Subset, LE.le, Prod.fst, And, _private.0.ContinuousMap.isUniformInducing_equivBoundedOfCompact.match_3, isCompact_univ, And.intro, LT.lt, Iff.intro, Exists.intro, Iff.mp, Set.mem_univ, Dist.dist, OfNat.ofNat, Prod.snd, IsCompact, _private.0.ContinuousMap.isUniformInducing_equivBoundedOfCompact.match_2
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
⊢ ∀ (s : Set (C(α, β) × C(α, β))),
    (∃ (i : Prod.{u_1, u_2} (Set α) (Set (β × β))),
        (IsCompact i.1 ∧ ∃ (i_1 : ℝ), 0 < i_1 ∧ {p : β × β | dist p.1 p.2 ≤ i_1} ⊆ i.2) ∧
          {fg : C(α, β) × C(α, β) |
              ∀ x ∈ i.1, Membership.mem (α := β × β) i.2 (((fg.1 : (a : α) → β) x, (fg.2 : (a : α) → β) x) : β × β)} ⊆
            s) ↔
      ∃ (t : Set ((α →ᵇ β) × (α →ᵇ β))),
        (∃ (i : ℝ), 0 < i ∧ {p : (α →ᵇ β) × (α →ᵇ β) | dist p.1 p.2 ≤ i} ⊆ t) ∧
          ∀ (x y : C(α, β)),
            Membership.mem (α := (α →ᵇ β) × (α →ᵇ β)) t
                (((equivBoundedOfCompact α β : (a : C(α, β)) → α →ᵇ β) x,
                    (equivBoundedOfCompact α β : (a : C(α, β)) → α →ᵇ β) y) :
                  (α →ᵇ β) × (α →ᵇ β)) →
              (x, y) ∈ s

Tactic:
exact fun s =>
        ⟨fun ⟨⟨a, b⟩, ⟨_, ⟨ε, hε, hb⟩⟩, hs⟩ =>
          ⟨{ p | ∀ x, (p.1 x, p.2 x) ∈ b }, ⟨ε, hε, fun _ h x => hb ((dist_le hε.le).mp h x)⟩,
            fun f g h => hs fun x _ => h x⟩,
          fun ⟨_, ⟨ε, hε, ht⟩, hs⟩ =>
          ⟨⟨Set.univ, { p | dist p.1 p.2 ≤ ε }⟩, ⟨isCompact_univ, ⟨ε, hε, fun _ h => h⟩⟩,
            fun ⟨f, g⟩ h => hs _ _ (ht ((dist_le hε.le).mpr fun x => h x (mem_univ x)))⟩⟩
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
⊢ IsUniformEmbedding (α := C(α, β)) (β := α →ᵇ β) (⇑(equivBoundedOfCompact α β) : (a : C(α, β)) → α →ᵇ β)

Tactic:
{ isUniformInducing_equivBoundedOfCompact α β with
    injective := (equivBoundedOfCompact α β).injective }

Premises used: ContinuousMap.isUniformInducing_equivBoundedOfCompact, ContinuousMap.equivBoundedOfCompact, IsUniformEmbedding.mk, Equiv.injective
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
f g : C(α, β)
⊢ dist (mkOfCompact f) (mkOfCompact g) = dist f g

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
f g : α →ᵇ β
⊢ dist f.toContinuousMap g.toContinuousMap = dist f g

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
f g : C(α, β)
x : α
⊢ dist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ dist f g

Tactic:
simp only [← dist_mkOfCompact, dist_coe_le_dist, ← mkOfCompact_apply]

Premises used: BoundedContinuousFunction.mkOfCompact_apply, BoundedContinuousFunction.dist_coe_le_dist, BoundedContinuousFunction.dist_mkOfCompact
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
f g : C(α, β)
C : ℝ
C0 : 0 ≤ C
⊢ dist f g ≤ C ↔ ∀ (x : α), dist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C

Tactic:
simp only [← dist_mkOfCompact, BoundedContinuousFunction.dist_le C0, mkOfCompact_apply]

Premises used: BoundedContinuousFunction.dist_le, BoundedContinuousFunction.mkOfCompact_apply, BoundedContinuousFunction.dist_mkOfCompact
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
f g : C(α, β)
C : ℝ
inst_3 : Nonempty α
⊢ dist f g ≤ C ↔ ∀ (x : α), dist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C

Tactic:
simp only [← dist_mkOfCompact, BoundedContinuousFunction.dist_le_iff_of_nonempty,
    mkOfCompact_apply]

Premises used: BoundedContinuousFunction.mkOfCompact_apply, BoundedContinuousFunction.dist_le_iff_of_nonempty, BoundedContinuousFunction.dist_mkOfCompact
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
f g : C(α, β)
C : ℝ
inst_3 : Nonempty α
⊢ dist f g < C ↔ ∀ (x : α), dist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C

Tactic:
simp only [← dist_mkOfCompact, dist_lt_iff_of_nonempty_compact, mkOfCompact_apply]

Premises used: BoundedContinuousFunction.mkOfCompact_apply, BoundedContinuousFunction.dist_lt_iff_of_nonempty_compact, BoundedContinuousFunction.dist_mkOfCompact
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
f g : C(α, β)
C : ℝ
inst_3 : Nonempty α
w : ∀ (x : α), dist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C
⊢ dist f g < C

Tactic:
dist_lt_iff_of_nonempty.2 w

Premises used: Iff.mpr, ContinuousMap.dist_lt_iff_of_nonempty
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
f g : C(α, β)
C : ℝ
C0 : 0 < C
rw :
  (∀ (x : α), dist.{u_2} (α := β) ((mkOfCompact f : (a : α) → β) x : β) ((mkOfCompact g : (a : α) → β) x : β) < C) ↔
    ∀ (x : α), dist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C
⊢ dist f g < C ↔ ∀ (x : α), dist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C

Tactic:
rw [← dist_mkOfCompact, dist_lt_iff_of_compact C0]

Premises used: BoundedContinuousFunction.dist_mkOfCompact, BoundedContinuousFunction.dist_lt_iff_of_compact
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
f g : C(α, β)
C : ℝ
C0 : 0 < C
⊢ (∀ (x : α), dist.{u_2} (α := β) ((mkOfCompact f : (a : α) → β) x : β) ((mkOfCompact g : (a : α) → β) x : β) < C) ↔
    ∀ (x : α), dist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C

Tactic:
simp only [mkOfCompact_apply]

Premises used: BoundedContinuousFunction.mkOfCompact_apply
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
f g : C(α, β)
⊢ dist f g = ⨆ (x : α), dist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
simp [← isometryEquivBoundedOfCompact α β |>.dist_eq f g,
    BoundedContinuousFunction.dist_eq_iSup]

Premises used: BoundedContinuousFunction.dist_eq_iSup, IsometryEquiv.dist_eq, ContinuousMap.isometryEquivBoundedOfCompact
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
f g : C(α, β)
⊢ nndist f g = ⨆ (x : α), nndist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
simp [← isometryEquivBoundedOfCompact α β |>.nndist_eq f g,
    BoundedContinuousFunction.nndist_eq_iSup]

Premises used: BoundedContinuousFunction.nndist_eq_iSup, ContinuousMap.isometryEquivBoundedOfCompact, IsometryEquiv.nndist_eq
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
f g : C(α, β)
⊢ edist f g = ⨆ (x : α), edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
simp [← isometryEquivBoundedOfCompact α β |>.edist_eq f g,
    BoundedContinuousFunction.edist_eq_iSup]

Premises used: IsometryEquiv.edist_eq, BoundedContinuousFunction.edist_eq_iSup, ContinuousMap.isometryEquivBoundedOfCompact
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E
f_1 g_1 : C(α, β)
C : ℝ
R : Type u_4
inst_4 : Zero R
inst_5 : Zero β
inst_6 : PseudoMetricSpace R
inst_7 : SMul R β
inst_8 : IsBoundedSMul R β
r : R
f g : C(α, β)
⊢ dist (r • f) (r • g) ≤ dist r 0 * dist f g

Tactic:
simpa only [← dist_mkOfCompact] using dist_smul_pair r (mkOfCompact f) (mkOfCompact g)

Premises used: BoundedContinuousFunction.mkOfCompact, BoundedContinuousFunction.dist_mkOfCompact, dist_smul_pair
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E
f_1 g : C(α, β)
C : ℝ
R : Type u_4
inst_4 : Zero R
inst_5 : Zero β
inst_6 : PseudoMetricSpace R
inst_7 : SMul R β
inst_8 : IsBoundedSMul R β
r₁ r₂ : R
f : C(α, β)
⊢ dist (r₁ • f) (r₂ • f) ≤ dist r₁ r₂ * dist f 0

Tactic:
simpa only [← dist_mkOfCompact] using dist_pair_smul r₁ r₂ (mkOfCompact f)

Premises used: dist_pair_smul, BoundedContinuousFunction.mkOfCompact, BoundedContinuousFunction.dist_mkOfCompact
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
f : C(α, E)
⊢ ‖mkOfCompact f‖ = ‖f‖

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
f : α →ᵇ E
⊢ ‖f.toContinuousMap‖ = ‖f‖

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E
x y : C(α, E)
rw : dist x y = ‖mkOfCompact (-x + y)‖
rw₁ : dist (mkOfCompact x) (mkOfCompact y) = ‖mkOfCompact (-x + y)‖
rw₂ : ‖-mkOfCompact x + mkOfCompact y‖ = ‖mkOfCompact (-x + y)‖
rw₃ : ‖-mkOfCompact x + mkOfCompact y‖ = ‖mkOfCompact (-x) + mkOfCompact y‖
rw₄ rw₅ : ‖-mkOfCompact x + mkOfCompact y‖ = ‖-mkOfCompact x + mkOfCompact y‖
⊢ dist x y = ‖-x + y‖

Tactic:
rw [← norm_mkOfCompact, ← dist_mkOfCompact, dist_eq_norm_neg_add,
    mkOfCompact_add, mkOfCompact_neg]

Premises used: BoundedContinuousFunction.mkOfCompact_add, dist_eq_norm_neg_add, BoundedContinuousFunction.mkOfCompact_neg, BoundedContinuousFunction.norm_mkOfCompact, BoundedContinuousFunction.dist_mkOfCompact
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
E_1 : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E_1
inst_4 : Nonempty α
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : Nontrivial E
⊢ NontrivialTopology C(α, E)

Tactic:
simpa [nontrivialTopology_iff_exists_norm_ne_zero] using exists_ne (0 : C(α, E))

Premises used: exists_ne, nontrivialTopology_iff_exists_norm_ne_zero, OfNat.ofNat
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E
inst_4 : Nonempty α
inst_5 : One E
inst_6 : NormOneClass E
⊢ norm (E := C(α, E)) 1 = 1

Tactic:
simp only [← norm_mkOfCompact, mkOfCompact_one, norm_one]

Premises used: NormOneClass.norm_one, BoundedContinuousFunction.norm_mkOfCompact, BoundedContinuousFunction.mkOfCompact_one
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
f : C(α, E)
x : α
⊢ norm.{u_3} (E := E) ((f : (a : α) → E) x : E) ≤ ‖f‖

Tactic:
(mkOfCompact f).norm_coe_le_norm x

Premises used: setOf, BoundedContinuousFunction.mkOfCompact, BoundedContinuousFunction.norm_coe_le_norm
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
f : C(α, E)
x y : α
⊢ dist.{u_3} (α := E) ((f : (a : α) → E) x : E) ((f : (a : α) → E) y : E) ≤ 2 * ‖f‖

Tactic:
(mkOfCompact f).dist_le_two_norm x y

Premises used: setOf, BoundedContinuousFunction.mkOfCompact, BoundedContinuousFunction.dist_le_two_norm
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
f : C(α, E)
C : ℝ
C0 : 0 ≤ C
⊢ ‖f‖ ≤ C ↔ ∀ (x : α), norm.{u_3} (E := E) ((f : (a : α) → E) x : E) ≤ C

Tactic:
@BoundedContinuousFunction.norm_le _ _ _ _ (mkOfCompact f) _ C0

Premises used: setOf, BoundedContinuousFunction.norm_le
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
f : C(α, E)
inst_3 : Nonempty α
M : ℝ
⊢ ‖f‖ ≤ M ↔ ∀ (x : α), norm.{u_3} (E := E) ((f : (a : α) → E) x : E) ≤ M

Tactic:
@BoundedContinuousFunction.norm_le_of_nonempty _ _ _ _ _ (mkOfCompact f) _

Premises used: setOf, BoundedContinuousFunction.norm_le_of_nonempty
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
f : C(α, E)
M : ℝ
M0 : 0 < M
⊢ ‖f‖ < M ↔ ∀ (x : α), norm.{u_3} (E := E) ((f : (a : α) → E) x : E) < M

Tactic:
@BoundedContinuousFunction.norm_lt_iff_of_compact _ _ _ _ _ (mkOfCompact f) _ M0

Premises used: setOf, BoundedContinuousFunction.norm_lt_iff_of_compact
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
f : C(α, E)
M : ℝ≥0
M0 : 0 < M
⊢ ‖f‖₊ < M ↔ ∀ (x : α), NNNorm.nnnorm.{u_3} (E := E) ((f : (a : α) → E) x : E) < M

Tactic:
f.norm_lt_iff M0

Premises used: ContinuousMap.norm_lt_iff
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
f : C(α, E)
inst_3 : Nonempty α
M : ℝ
⊢ ‖f‖ < M ↔ ∀ (x : α), norm.{u_3} (E := E) ((f : (a : α) → E) x : E) < M

Tactic:
@BoundedContinuousFunction.norm_lt_iff_of_nonempty_compact _ _ _ _ _ _ (mkOfCompact f) _

Premises used: setOf, BoundedContinuousFunction.norm_lt_iff_of_nonempty_compact
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
f : C(α, E)
inst_3 : Nonempty α
M : ℝ≥0
⊢ ‖f‖₊ < M ↔ ∀ (x : α), NNNorm.nnnorm.{u_3} (E := E) ((f : (a : α) → E) x : E) < M

Tactic:
f.norm_lt_iff_of_nonempty

Premises used: ContinuousMap.norm_lt_iff_of_nonempty
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
f : C(α, ℝ)
x : α
⊢ (f : (a : α) → ℝ) x ≤ ‖f‖

Tactic:
le_trans (le_abs.mpr (Or.inl (le_refl (f x)))) (f.norm_coe_le_norm x)

Premises used: Iff.mpr, le_refl, ContinuousMap.norm_coe_le_norm, le_abs, Or.inl, DFunLike.coe, le_trans
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
f : C(α, ℝ)
x : α
⊢ -‖f‖ ≤ (f : (a : α) → ℝ) x

Tactic:
le_trans (neg_le_neg (f.norm_coe_le_norm x)) (neg_le.mp (neg_le_abs (f x)))

Premises used: ContinuousMap.norm_coe_le_norm, neg_le, neg_le_abs, Iff.mp, neg_le_neg, DFunLike.coe, le_trans
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
f : C(α, E)
⊢ ‖f‖₊ = ⨆ (x : α), NNNorm.nnnorm.{u_3} (E := E) ((f : (a : α) → E) x : E)

Tactic:
(mkOfCompact f).nnnorm_eq_iSup_nnnorm

Premises used: setOf, BoundedContinuousFunction.mkOfCompact, BoundedContinuousFunction.nnnorm_eq_iSup_nnnorm
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
f : C(α, E)
⊢ ‖f‖ = ⨆ (x : α), norm.{u_3} (E := E) ((f : (a : α) → E) x : E)

Tactic:
(mkOfCompact f).norm_eq_iSup_norm

Premises used: setOf, BoundedContinuousFunction.mkOfCompact, BoundedContinuousFunction.norm_eq_iSup_norm