awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst : PseudoMetricSpace 𝕜
inst_1 : TopologicalSpace α
inst_2 : PseudoMetricSpace β
inst_3 : Zero 𝕜
inst_4 : Zero β
inst_5 : SMul 𝕜 β
inst_6 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α →ᵇ β
b : ℝ
hb : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ b
x y : α
hbc : dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ b
⊢ dist c 0 * dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ dist c 0 * b

Tactic:
gcongr
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst : PseudoMetricSpace 𝕜
inst_1 : TopologicalSpace α
inst_2 : PseudoMetricSpace β
inst_3 : Zero 𝕜
inst_4 : Zero β
inst_5 : SMul 𝕜 β
inst_6 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α →ᵇ β
b : ℝ
hb : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ b
x y : α
⊢ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ b

Tactic:
apply hb
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
𝕜 : Type u_2
inst : PseudoMetricSpace 𝕜
inst_1 : TopologicalSpace α
inst_2 : PseudoMetricSpace β
inst_3 : Zero 𝕜
inst_4 : Zero β
inst_5 : SMul 𝕜 β
inst_6 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α →ᵇ β
⊢ Eq (α := (a : α) → β) (⇑(c • f) : (a : α) → β) fun (x : α) ↦ HSMul.hSMul (β := β) c ((f : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
𝕜 : Type u_2
inst : PseudoMetricSpace 𝕜
inst_1 : TopologicalSpace α
inst_2 : PseudoMetricSpace β
inst_3 : Zero 𝕜
inst_4 : Zero β
inst_5 : SMul 𝕜 β
inst_6 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α →ᵇ β
x : α
⊢ (c • f : (a : α) → β) x = HSMul.hSMul (β := β) c ((f : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst : PseudoMetricSpace 𝕜
inst_1 : TopologicalSpace α
inst_2 : PseudoMetricSpace β
inst_3 : Zero 𝕜
inst_4 : Zero β
inst_5 : SMul 𝕜 β
inst_6 : IsBoundedSMul 𝕜 β
c : 𝕜
f₁ f₂ : α →ᵇ β
rw : ∀ (x : α), dist.{v} (α := β) ((c • f₁ : (a : α) → β) x : β) ((c • f₂ : (a : α) → β) x : β) ≤ dist c 0 * dist f₁ f₂
⊢ dist (c • f₁) (c • f₂) ≤ dist c 0 * dist f₁ f₂

Tactic:
rw [dist_le (mul_nonneg dist_nonneg dist_nonneg)]

Premises used: mul_nonneg, BoundedContinuousFunction.dist_le, dist_nonneg
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst : PseudoMetricSpace 𝕜
inst_1 : TopologicalSpace α
inst_2 : PseudoMetricSpace β
inst_3 : Zero 𝕜
inst_4 : Zero β
inst_5 : SMul 𝕜 β
inst_6 : IsBoundedSMul 𝕜 β
c : 𝕜
f₁ f₂ : α →ᵇ β
x : α
⊢ dist.{v} (α := β) ((c • f₁ : (a : α) → β) x : β) ((c • f₂ : (a : α) → β) x : β) ≤ dist c 0 * dist f₁ f₂

Tactic:
(dist_smul_pair c (f₁ x) (f₂ x)).trans ?_

Premises used: LE.le.trans, DFunLike.coe, dist_smul_pair
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst : PseudoMetricSpace 𝕜
inst_1 : TopologicalSpace α
inst_2 : PseudoMetricSpace β
inst_3 : Zero 𝕜
inst_4 : Zero β
inst_5 : SMul 𝕜 β
inst_6 : IsBoundedSMul 𝕜 β
c : 𝕜
f₁ f₂ : α →ᵇ β
x : α
refine : dist c 0 * dist.{v} (α := β) ((f₁ : (a : α) → β) x : β) ((f₂ : (a : α) → β) x : β) ≤ dist c 0 * dist f₁ f₂
⊢ dist.{v} (α := β) ((c • f₁ : (a : α) → β) x : β) ((c • f₂ : (a : α) → β) x : β) ≤ dist c 0 * dist f₁ f₂

Tactic:
refine (dist_smul_pair c (f₁ x) (f₂ x)).trans ?_

Premises used: LE.le.trans, DFunLike.coe, dist_smul_pair
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst : PseudoMetricSpace 𝕜
inst_1 : TopologicalSpace α
inst_2 : PseudoMetricSpace β
inst_3 : Zero 𝕜
inst_4 : Zero β
inst_5 : SMul 𝕜 β
inst_6 : IsBoundedSMul 𝕜 β
c : 𝕜
f₁ f₂ : α →ᵇ β
x : α
hbc : dist.{v} (α := β) ((f₁ : (a : α) → β) x : β) ((f₂ : (a : α) → β) x : β) ≤ dist f₁ f₂
⊢ dist c 0 * dist.{v} (α := β) ((f₁ : (a : α) → β) x : β) ((f₂ : (a : α) → β) x : β) ≤ dist c 0 * dist f₁ f₂

Tactic:
gcongr
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst : PseudoMetricSpace 𝕜
inst_1 : TopologicalSpace α
inst_2 : PseudoMetricSpace β
inst_3 : Zero 𝕜
inst_4 : Zero β
inst_5 : SMul 𝕜 β
inst_6 : IsBoundedSMul 𝕜 β
c : 𝕜
f₁ f₂ : α →ᵇ β
x : α
⊢ dist.{v} (α := β) ((f₁ : (a : α) → β) x : β) ((f₂ : (a : α) → β) x : β) ≤ dist f₁ f₂

Tactic:
apply dist_coe_le_dist

Premises used: BoundedContinuousFunction.dist_coe_le_dist
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst : PseudoMetricSpace 𝕜
inst_1 : TopologicalSpace α
inst_2 : PseudoMetricSpace β
inst_3 : Zero 𝕜
inst_4 : Zero β
inst_5 : SMul 𝕜 β
inst_6 : IsBoundedSMul 𝕜 β
c₁ c₂ : 𝕜
f : α →ᵇ β
⊢ 0 ≤ dist c₁ c₂ * dist f 0

Tactic:
positivity
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst : PseudoMetricSpace 𝕜
inst_1 : TopologicalSpace α
inst_2 : PseudoMetricSpace β
inst_3 : Zero 𝕜
inst_4 : Zero β
inst_5 : SMul 𝕜 β
inst_6 : IsBoundedSMul 𝕜 β
c₁ c₂ : 𝕜
f : α →ᵇ β
rw : ∀ (x : α), dist.{v} (α := β) ((c₁ • f : (a : α) → β) x : β) ((c₂ • f : (a : α) → β) x : β) ≤ dist c₁ c₂ * dist f 0
⊢ dist (c₁ • f) (c₂ • f) ≤ dist c₁ c₂ * dist f 0

Tactic:
rw [dist_le (by positivity)]

Premises used: BoundedContinuousFunction.dist_le
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst : PseudoMetricSpace 𝕜
inst_1 : TopologicalSpace α
inst_2 : PseudoMetricSpace β
inst_3 : Zero 𝕜
inst_4 : Zero β
inst_5 : SMul 𝕜 β
inst_6 : IsBoundedSMul 𝕜 β
c₁ c₂ : 𝕜
f : α →ᵇ β
x : α
⊢ dist.{v} (α := β) ((c₁ • f : (a : α) → β) x : β) ((c₂ • f : (a : α) → β) x : β) ≤ dist c₁ c₂ * dist f 0

Tactic:
(dist_pair_smul c₁ c₂ (f x)).trans ?_

Premises used: dist_pair_smul, LE.le.trans, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst : PseudoMetricSpace 𝕜
inst_1 : TopologicalSpace α
inst_2 : PseudoMetricSpace β
inst_3 : Zero 𝕜
inst_4 : Zero β
inst_5 : SMul 𝕜 β
inst_6 : IsBoundedSMul 𝕜 β
c₁ c₂ : 𝕜
f : α →ᵇ β
x : α
refine : dist c₁ c₂ * dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) ≤ dist c₁ c₂ * dist f 0
⊢ dist.{v} (α := β) ((c₁ • f : (a : α) → β) x : β) ((c₂ • f : (a : α) → β) x : β) ≤ dist c₁ c₂ * dist f 0

Tactic:
refine (dist_pair_smul c₁ c₂ (f x)).trans ?_

Premises used: dist_pair_smul, LE.le.trans, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst : PseudoMetricSpace 𝕜
inst_1 : TopologicalSpace α
inst_2 : PseudoMetricSpace β
inst_3 : Zero 𝕜
inst_4 : Zero β
inst_5 : SMul 𝕜 β
inst_6 : IsBoundedSMul 𝕜 β
c₁ c₂ : 𝕜
f : α →ᵇ β
x : α
hbc : dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) ≤ dist f 0
⊢ dist c₁ c₂ * dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) ≤ dist c₁ c₂ * dist f 0

Tactic:
gcongr
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst : PseudoMetricSpace 𝕜
inst_1 : TopologicalSpace α
inst_2 : PseudoMetricSpace β
inst_3 : Zero 𝕜
inst_4 : Zero β
inst_5 : SMul 𝕜 β
inst_6 : IsBoundedSMul 𝕜 β
c₁ c₂ : 𝕜
f : α →ᵇ β
x : α
⊢ dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) ≤ dist f 0

Tactic:
apply dist_coe_le_dist (g := 0)

Premises used: BoundedContinuousFunction.dist_coe_le_dist
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
⊢ nndist (α := ℝ≥0) ((f : (a : α) → ℝ≥0) x : ℝ≥0) (((0 : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0) ≤ nndist f 0

Tactic:
have key : nndist (f x) ((0 : α →ᵇ ℝ≥0) x) ≤ nndist f 0 := @dist_coe_le_dist α ℝ≥0 _ _ f 0 x
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
key : nndist (α := ℝ≥0) ((f : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0) ≤ nndist f 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (key : (f : (a : α) → ℝ≥0) x ≤ nndist f 0), (f : (a : α) → ℝ≥0) x ≤ nndist f 0
⊢ (f : (a : α) → ℝ≥0) x ≤ nndist f 0

Tactic:
rwa [NNReal.nndist_zero_eq_val' (f x)] at key

Premises used: NNReal.nndist_zero_eq_val', DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ‖f‖ = dist f 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ‖f‖ = sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C}

Tactic:
simp [norm_def, BoundedContinuousFunction.dist_eq]

Premises used: BoundedContinuousFunction.dist_eq, BoundedContinuousFunction.norm_def
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
h : Nonempty α
obtain : ∀ (a : α), ‖f‖ = sInf {C : ℝ | ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C}
⊢ ‖f‖ = sInf {C : ℝ | ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C}

Tactic:
obtain ⟨a⟩ := h
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
rw :
  Eq (α := ℝ) (sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C})
    (sInf {C : ℝ | ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C})
⊢ ‖f‖ = sInf {C : ℝ | ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C}

Tactic:
rw [norm_eq]

Premises used: BoundedContinuousFunction.norm_eq
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
e_a :
  Eq (α := ℝ → Prop) (fun (C : ℝ) ↦ 0 ≤ C ∧ ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C) fun (C : ℝ) ↦
    ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C
⊢ Eq (α := ℝ) (sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C})
    (sInf {C : ℝ | ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C})

Tactic:
congr
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
e_a :
  ∀ (x : ℝ),
    (0 ≤ x ∧ ∀ (x_1 : α), norm.{v} (E := β) ((f : (a : α) → β) x_1 : β) ≤ x) ↔
      ∀ (x_1 : α), norm.{v} (E := β) ((f : (a : α) → β) x_1 : β) ≤ x
⊢ Eq (α := ℝ → Prop) (fun (C : ℝ) ↦ 0 ≤ C ∧ ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C) fun (C : ℝ) ↦
    ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
x : ℝ
e_a : (∀ (x_1 : α), norm.{v} (E := β) ((f : (a : α) → β) x_1 : β) ≤ x) → 0 ≤ x
⊢ (0 ≤ x ∧ ∀ (x_1 : α), norm.{v} (E := β) ((f : (a : α) → β) x_1 : β) ≤ x) ↔
    ∀ (x_1 : α), norm.{v} (E := β) ((f : (a : α) → β) x_1 : β) ≤ x

Tactic:
simp only [and_iff_right_iff_imp]

Premises used: and_iff_right_iff_imp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
x : ℝ
⊢ (∀ (x_1 : α), norm.{v} (E := β) ((f : (a : α) → β) x_1 : β) ≤ x) → 0 ≤ x

Tactic:
fun h' => le_trans (norm_nonneg (f a)) (h' a)

Premises used: DFunLike.coe, norm_nonneg, le_trans
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
x : ℝ
⊢ (∀ (x_1 : α), norm.{v} (E := β) ((f : (a : α) → β) x_1 : β) ≤ x) → 0 ≤ x

Tactic:
exact fun h' => le_trans (norm_nonneg (f a)) (h' a)

Premises used: DFunLike.coe, norm_nonneg, le_trans
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
inst_2 : IsEmpty α
⊢ ‖f‖ = 0

Tactic:
dist_zero_of_empty

Premises used: BoundedContinuousFunction.dist_zero_of_empty
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
x : α
⊢ norm.{v} (E := β) ((f : (a : α) → β) x : β) = dist.{v} (α := β) ((f : (a : α) → β) x : β) ((0 : (a : α) → β) x : β)

Tactic:
simp [dist_zero_right]

Premises used: dist_zero_right
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ -‖f‖ ≤ (f : (a : α) → ℝ) x

Tactic:
(abs_le.mp (norm_coe_le_norm f x)).1

Premises used: abs_le, And.left, BoundedContinuousFunction.norm_coe_le_norm, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ (f : (a : α) → ℝ) x ≤ ‖f‖

Tactic:
(abs_le.mp (norm_coe_le_norm f x)).2

Premises used: abs_le, And.right, BoundedContinuousFunction.norm_coe_le_norm, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
β : Type v
γ : Type w
inst : SeminormedAddCommGroup β
f : γ → β
C : ℝ
hC : ∀ (x : γ), ‖f x‖ ≤ C
x y : γ
⊢ dist (f x) (f y) ≤ 2 * C

Tactic:
calc
    dist (f x) (f y) ≤ ‖f x‖ + ‖f y‖ := dist_le_norm_add_norm _ _
    _ ≤ C + C := add_le_add (hC x) (hC y)
    _ = 2 * C := (two_mul _).symm

Premises used: Trans.trans, dist_le_norm_add_norm, add_le_add, two_mul, Eq.symm
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
x y : α
⊢ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ 2 * ‖f‖

Tactic:
dist_le_two_norm' f.norm_coe_le_norm x y

Premises used: BoundedContinuousFunction.norm_coe_le_norm, BoundedContinuousFunction.dist_le_two_norm'
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
C : ℝ
C0 : 0 ≤ C
⊢ ‖f‖ ≤ C ↔ ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C

Tactic:
simpa using @dist_le _ _ _ _ f 0 _ C0

Premises used: BoundedContinuousFunction.dist_le
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : Nonempty α
f : α →ᵇ β
M : ℝ
simp_rw : dist f 0 ≤ M ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) ≤ M
⊢ ‖f‖ ≤ M ↔ ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ M

Tactic:
simp_rw [norm_def, ← dist_zero_right]

Premises used: BoundedContinuousFunction.norm_def, dist_zero_right
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : Nonempty α
f : α →ᵇ β
M : ℝ
⊢ dist f 0 ≤ M ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) ≤ M

Tactic:
dist_le_iff_of_nonempty

Premises used: BoundedContinuousFunction.dist_le_iff_of_nonempty
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : Nonempty α
f : α →ᵇ β
M : ℝ
⊢ dist f 0 ≤ M ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) ≤ M

Tactic:
exact dist_le_iff_of_nonempty

Premises used: BoundedContinuousFunction.dist_le_iff_of_nonempty
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : CompactSpace α
f : α →ᵇ β
M : ℝ
M0 : 0 < M
simp_rw : dist f 0 < M ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < M
⊢ ‖f‖ < M ↔ ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) < M

Tactic:
simp_rw [norm_def, ← dist_zero_right]

Premises used: BoundedContinuousFunction.norm_def, dist_zero_right
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : CompactSpace α
f : α →ᵇ β
M : ℝ
M0 : 0 < M
⊢ dist f 0 < M ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < M

Tactic:
dist_lt_iff_of_compact M0

Premises used: BoundedContinuousFunction.dist_lt_iff_of_compact
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : CompactSpace α
f : α →ᵇ β
M : ℝ
M0 : 0 < M
⊢ dist f 0 < M ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < M

Tactic:
exact dist_lt_iff_of_compact M0

Premises used: BoundedContinuousFunction.dist_lt_iff_of_compact
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : Nonempty α
inst_3 : CompactSpace α
f : α →ᵇ β
M : ℝ
simp_rw : dist f 0 < M ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < M
⊢ ‖f‖ < M ↔ ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) < M

Tactic:
simp_rw [norm_def, ← dist_zero_right]

Premises used: BoundedContinuousFunction.norm_def, dist_zero_right
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : Nonempty α
inst_3 : CompactSpace α
f : α →ᵇ β
M : ℝ
⊢ dist f 0 < M ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < M

Tactic:
dist_lt_iff_of_nonempty_compact

Premises used: BoundedContinuousFunction.dist_lt_iff_of_nonempty_compact
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : Nonempty α
inst_3 : CompactSpace α
f : α →ᵇ β
M : ℝ
⊢ dist f 0 < M ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < M

Tactic:
exact dist_lt_iff_of_nonempty_compact

Premises used: BoundedContinuousFunction.dist_lt_iff_of_nonempty_compact
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
b : β
⊢ norm (E := α →ᵇ β) (const α b) ≤ ‖b‖

Tactic:
(norm_le (norm_nonneg b)).2 fun _ => le_rfl

Premises used: Iff.mpr, le_rfl, BoundedContinuousFunction.norm_le, norm_nonneg
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
h : Nonempty α
b : β
⊢ norm (E := α →ᵇ β) (const α b) = ‖b‖

Tactic:
le_antisymm (norm_const_le b) <| h.elim fun x => (const α b).norm_coe_le_norm x

Premises used: Nonempty.elim, le_antisymm, BoundedContinuousFunction.const, BoundedContinuousFunction.norm_coe_le_norm, BoundedContinuousFunction.norm_const_le
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α → β
Hf : Continuous f
C : ℝ
H : ∀ (x : α), ‖f x‖ ≤ C
⊢ (⇑(ofNormedAddCommGroup f Hf C H) : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α → β
hfc : Continuous f
C : ℝ
hC : 0 ≤ C
hfC : ∀ (x : α), ‖f x‖ ≤ C
⊢ ‖ofNormedAddCommGroup f hfc C hfC‖ ≤ C

Tactic:
(norm_le hC).2 hfC

Premises used: Iff.mpr, BoundedContinuousFunction.norm_le
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
inst_2 : SeminormedAddCommGroup β
f : α → β
C : ℝ
H : ∀ (x : α), ‖f x‖ ≤ C
⊢ (⇑(ofNormedAddCommGroupDiscrete f C H) : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ Eq (α := (a : α) → ℝ) (⇑f.normComp : (a : α) → ℝ) (Function.comp.{u + 1, v + 1, 1} (β := β) norm (⇑f : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ‖f.normComp‖ = ‖f‖

Tactic:
simp only [norm_eq, coe_normComp, norm_norm, Function.comp]

Premises used: BoundedContinuousFunction.coe_normComp, Function.comp, BoundedContinuousFunction.norm_eq, norm_norm
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ BddAbove (range.{0, u + 1} (ι := α) (Function.comp.{u + 1, v + 1, 1} (β := β) norm (⇑f : (a : α) → β)))

Tactic:
(@isBounded_range _ _ _ _ f.normComp).bddAbove

Premises used: BoundedContinuousFunction.isBounded_range, BoundedContinuousFunction.normComp, Bornology.IsBounded.bddAbove
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
simp_rw : dist f 0 = ⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β)
simp_rw₁ :
  Eq (α := ℝ) (⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((0 : (a : α) → β) x : β))
    (⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β))
simp_rw₂ :
  Eq (α := ℝ) (⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 x : β))
    (⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β))
simp_rw₃ :
  Eq (α := ℝ) (⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β))
    (⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β))
⊢ ‖f‖ = ⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β)

Tactic:
simp_rw [norm_def, dist_eq_iSup, coe_zero, Pi.zero_apply, dist_zero_right]

Premises used: BoundedContinuousFunction.dist_eq_iSup, Pi.zero_apply, BoundedContinuousFunction.norm_def, BoundedContinuousFunction.coe_zero, dist_zero_right
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
inst_2 : Nonempty α
inst_3 : One β
inst_4 : NormOneClass β
⊢ norm (E := α →ᵇ β) 1 = 1

Tactic:
simp only [norm_eq_iSup_norm, coe_one, Pi.one_apply, norm_one, ciSup_const]

Premises used: BoundedContinuousFunction.coe_one, Pi.one_apply, NormOneClass.norm_one, ciSup_const, BoundedContinuousFunction.norm_eq_iSup_norm
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ Eq (α := (a : α) → β) (⇑(-f) : (a : α) → β) (-(⇑f : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
x : α
⊢ Eq.{v + 1} (α := β) ((-f : (a : α) → β) x : β) (-(f : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : CompactSpace α
f : C(α, β)
⊢ mkOfCompact (-f) = -mkOfCompact f

Tactic:
rfl

Premises used: BoundedContinuousFunction.mkOfCompact, BoundedContinuousFunction.ofNormedAddCommGroup, rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : CompactSpace α
f g : C(α, β)
⊢ mkOfCompact (f - g) = mkOfCompact f - mkOfCompact g

Tactic:
rfl

Premises used: BoundedContinuousFunction.mkOfCompact, rfl