awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
rw : (⇑(n • f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) (Int.ofNat n) (⇑f : (a : α) → β)
rw₁ : (⇑(n • f) : (a : α) → β) = HSMul.hSMul (α := ℤ) (β := (a : α) → β) (↑n : ℤ) (⇑f : (a : α) → β)
rw₂ :
  HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) =
    HSMul.hSMul (α := ℤ) (β := (a : α) → β) (↑n : ℤ) (⇑f : (a : α) → β)
rw₃ rw₄ : HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β)
⊢ (⇑(zsmulRec (fun (x1 : ℕ) (x2 : α →ᵇ β) ↦ x1 • x2) (Int.ofNat n) f) : (a : α) → β) =
    HSMul.hSMul (β := (a : α) → β) (Int.ofNat n) (⇑f : (a : α) → β)

Tactic:
rw [zsmulRec, Int.ofNat_eq_natCast, coe_nsmul, natCast_zsmul]

Premises used: Int.ofNat_eq_natCast, zsmulRec, nsmulRec, BoundedContinuousFunction.coe_nsmul, natCast_zsmul
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
rw : (⇑(-(n.succ • f)) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) (Int.negSucc n) (⇑f : (a : α) → β)
rw₁ : (⇑(-(n.succ • f)) : (a : α) → β) = -HSMul.hSMul (β := (a : α) → β) (n + 1) (⇑f : (a : α) → β)
rw₂ : -(⇑(n.succ • f) : (a : α) → β) = -HSMul.hSMul (β := (a : α) → β) (n + 1) (⇑f : (a : α) → β)
rw₃ rw₄ :
  -HSMul.hSMul (β := (a : α) → β) n.succ (⇑f : (a : α) → β) = -HSMul.hSMul (β := (a : α) → β) (n + 1) (⇑f : (a : α) → β)
⊢ (⇑(zsmulRec (fun (x1 : ℕ) (x2 : α →ᵇ β) ↦ x1 • x2) (Int.negSucc n) f) : (a : α) → β) =
    HSMul.hSMul (β := (a : α) → β) (Int.negSucc n) (⇑f : (a : α) → β)

Tactic:
rw [zsmulRec, negSucc_zsmul, coe_neg, coe_nsmul]

Premises used: BoundedContinuousFunction.coe_neg, zsmulRec, negSucc_zsmul, nsmulRec, BoundedContinuousFunction.coe_nsmul
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f_1 g : α →ᵇ β
x : α
C : ℝ
n : ℤ
f : α →ᵇ β
⊢ ∃ (C : ℝ), ∀ (x y : α), dist ((n • f.toContinuousMap).toFun x) ((n • f.toContinuousMap).toFun y) ≤ C

Tactic:
simpa using (zsmulRec (· • ·) n f).map_bounded'

Premises used: zsmulRec, HSMul.hSMul, BoundedContinuousFunction.map_bounded'
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
r : ℤ
f : α →ᵇ β
⊢ (⇑(r • f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) r (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
r : ℤ
f : α →ᵇ β
v : α
⊢ (r • f : (a : α) → β) v = HSMul.hSMul (β := β) r ((f : (a : α) → β) v : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f_1 g_1 : α →ᵇ β
x : α
C : ℝ
f g : α →ᵇ β
⊢ dist f g = ‖-f + g‖

Tactic:
simp only [norm_eq, dist_eq, dist_eq_norm_neg_add, add_apply, neg_apply]

Premises used: BoundedContinuousFunction.dist_eq, BoundedContinuousFunction.norm_eq, dist_eq_norm_neg_add, BoundedContinuousFunction.add_apply, BoundedContinuousFunction.neg_apply
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ‖f‖₊ = nndist f 0

Tactic:
rfl

Premises used: NNReal.mk, rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
x : α
⊢ nnnorm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ ‖f‖₊

Tactic:
norm_coe_le_norm _ _

Premises used: BoundedContinuousFunction.norm_coe_le_norm
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
x y : α
⊢ nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ 2 * ‖f‖₊

Tactic:
dist_le_two_norm _ _ _

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

Tactic:
norm_le C.prop

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

Tactic:
norm_const_le _

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

Tactic:
Subtype.ext <| norm_const_eq _

Premises used: NNReal, BoundedContinuousFunction.norm_const_eq, Subtype.ext
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
simp_rw :
  ⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) =
    (↑(⨆ (x : α), nnnorm.{v} (E := β) ((f : (a : α) → β) x : β)) : ℝ)
simp_rw₁ :
  Eq (α := ℝ) (⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β))
    (⨆ (i : α), (↑(nnnorm.{v} (E := β) ((f : (a : α) → β) i : β)) : ℝ))
⊢ Eq (α := ℝ) (⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β))
    (↑(⨆ (x : α), nnnorm.{v} (E := β) ((f : (a : α) → β) x : β)) : ℝ)

Tactic:
simp_rw [val_eq_coe, NNReal.coe_iSup, coe_nnnorm]

Premises used: NNReal.coe_iSup, NNReal.val_eq_coe, coe_nnnorm
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ‖f‖ₑ = ⨆ (x : α), enorm.{v} (E := β) ((f : (a : α) → β) x : β)

Tactic:
simpa only [← edist_zero_right] using edist_eq_iSup

Premises used: BoundedContinuousFunction.edist_eq_iSup, edist_zero_right
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
rw : ‖HSub.hSub (α := β) (β := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)‖ ≤ ‖f - g‖
⊢ ‖HSub.hSub (α := β) (β := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)‖ ≤ dist f g

Tactic:
rw [dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
⊢ ‖HSub.hSub (α := β) (β := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)‖ ≤ ‖f - g‖

Tactic:
(f - g).norm_coe_le_norm x

Premises used: setOf, HSub.hSub, BoundedContinuousFunction.norm_coe_le_norm
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
⊢ ‖HSub.hSub (α := β) (β := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)‖ ≤ ‖f - g‖

Tactic:
exact (f - g).norm_coe_le_norm x

Premises used: HSub.hSub, BoundedContinuousFunction.norm_coe_le_norm
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
x : α
f g : α →ᵇ ℝ
⊢ (f : (a : α) → ℝ) x ≤ HAdd.hAdd (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) (dist f g)

Tactic:
sub_le_iff_le_add'.1 <| (abs_le.1 <| @dist_coe_le_dist _ _ _ _ f g x).2

Premises used: abs_le, BoundedContinuousFunction.dist_coe_le_dist, sub_le_iff_le_add', And.right, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : TopologicalSpace γ
f : α →ᵇ β
g : C(γ, α)
rw : 1 * dist f 0 ≤ ‖f‖
rw₁ : dist f 0 ≤ ‖f‖
rw₂ rw₃ : ‖f‖ ≤ ‖f‖
⊢ (↑1 : ℝ) * dist f 0 ≤ ‖f‖

Tactic:
rw [NNReal.coe_one, one_mul, dist_zero_right]

Premises used: NNReal.coe_one, dist_zero_right, one_mul
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f_1 g : α →ᵇ β
x : α
C : ℝ
inst_2 : NormedField 𝕜
inst_3 : NormedSpace 𝕜 β
c : 𝕜
f : α →ᵇ β
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
norm_ofNormedAddCommGroup_le _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) ?_

Premises used: mul_nonneg, setOf, norm_nonneg, BoundedContinuousFunction.norm_ofNormedAddCommGroup_le
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f_1 g : α →ᵇ β
x : α
C : ℝ
inst_2 : NormedField 𝕜
inst_3 : NormedSpace 𝕜 β
c : 𝕜
f : α →ᵇ β
refine : ∀ (x : α), ‖HSMul.hSMul (β := (a : α) → β) c (⇑f.toContinuousMap : (a : α) → β) x‖ ≤ ‖c‖ * ‖f‖
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
refine norm_ofNormedAddCommGroup_le _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) ?_

Premises used: mul_nonneg, norm_nonneg, BoundedContinuousFunction.norm_ofNormedAddCommGroup_le
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f_1 g : α →ᵇ β
x : α
C : ℝ
inst_2 : NormedField 𝕜
inst_3 : NormedSpace 𝕜 β
c : 𝕜
f : α →ᵇ β
⊢ ∀ (x : α), ‖HSMul.hSMul (β := (a : α) → β) c (⇑f.toContinuousMap : (a : α) → β) x‖ ≤ ‖c‖ * ‖f‖

Tactic:
fun x =>
      norm_smul c (f x) ▸ mul_le_mul_of_nonneg_left (f.norm_coe_le_norm _) (norm_nonneg _)

Premises used: norm_smul, Eq.rec, BoundedContinuousFunction.norm_coe_le_norm, Eq.symm, mul_le_mul_of_nonneg_left, DFunLike.coe, norm_nonneg
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f_1 g : α →ᵇ β
x : α
C : ℝ
inst_2 : NormedField 𝕜
inst_3 : NormedSpace 𝕜 β
c : 𝕜
f : α →ᵇ β
⊢ ∀ (x : α), ‖HSMul.hSMul (β := (a : α) → β) c (⇑f.toContinuousMap : (a : α) → β) x‖ ≤ ‖c‖ * ‖f‖

Tactic:
exact fun x =>
      norm_smul c (f x) ▸ mul_le_mul_of_nonneg_left (f.norm_coe_le_norm _) (norm_nonneg _)
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f_1 g_1 : α →ᵇ β
x : α
C : ℝ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 β
inst_4 : SeminormedAddCommGroup γ
inst_5 : NormedSpace 𝕜 γ
g_2 : β →L[𝕜] γ
f g : α →ᵇ β
h :
  ∀ (x : α),
    Eq.{w + 1} (α := γ)
      ((ofNormedAddCommGroup
              (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g_2 : (a : β) → γ) (⇑(f + g) : (a : α) → β)) ⋯
              (‖g_2‖ * ‖f + g‖) ⋯ :
            (a : α) → γ)
          x :
        γ)
      ((ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g_2 : (a : β) → γ) (⇑f : (a : α) → β)) ⋯
                (‖g_2‖ * ‖f‖) ⋯ +
              ofNormedAddCommGroup
                (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g_2 : (a : β) → γ) (⇑g : (a : α) → β)) ⋯ (‖g_2‖ * ‖g‖)
                ⋯ :
            (a : α) → γ)
          x :
        γ)
⊢ ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g_2 : (a : β) → γ) (⇑(f + g) : (a : α) → β)) ⋯
      (‖g_2‖ * ‖f + g‖) ⋯ =
    ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g_2 : (a : β) → γ) (⇑f : (a : α) → β)) ⋯
        (‖g_2‖ * ‖f‖) ⋯ +
      ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g_2 : (a : β) → γ) (⇑g : (a : α) → β)) ⋯
        (‖g_2‖ * ‖g‖) ⋯

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f_1 g_1 : α →ᵇ β
x : α
C : ℝ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 β
inst_4 : SeminormedAddCommGroup γ
inst_5 : NormedSpace 𝕜 γ
g_2 : β →L[𝕜] γ
f g : α →ᵇ β
x_1 : α
⊢ Eq.{w + 1} (α := γ)
    ((ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g_2 : (a : β) → γ) (⇑(f + g) : (a : α) → β))
            ⋯ (‖g_2‖ * ‖f + g‖) ⋯ :
          (a : α) → γ)
        x_1 :
      γ)
    ((ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g_2 : (a : β) → γ) (⇑f : (a : α) → β)) ⋯
              (‖g_2‖ * ‖f‖) ⋯ +
            ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g_2 : (a : β) → γ) (⇑g : (a : α) → β))
              ⋯ (‖g_2‖ * ‖g‖) ⋯ :
          (a : α) → γ)
        x_1 :
      γ)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f_1 g_1 : α →ᵇ β
x : α
C : ℝ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 β
inst_4 : SeminormedAddCommGroup γ
inst_5 : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
c : 𝕜
f : α →ᵇ β
h :
  ∀ (x : α),
    Eq.{w + 1} (α := γ)
      ((ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g : (a : β) → γ) (⇑(c • f) : (a : α) → β))
              ⋯ (‖g‖ * ‖c • f‖) ⋯ :
            (a : α) → γ)
          x :
        γ)
      ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
              (ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β))
                ⋯ (‖g‖ * ‖f‖) ⋯) :
            (a : α) → γ)
          x :
        γ)
⊢ ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g : (a : β) → γ) (⇑(c • f) : (a : α) → β)) ⋯
      (‖g‖ * ‖c • f‖) ⋯ =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)) ⋯
        (‖g‖ * ‖f‖) ⋯)

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f_1 g_1 : α →ᵇ β
x : α
C : ℝ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 β
inst_4 : SeminormedAddCommGroup γ
inst_5 : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
c : 𝕜
f : α →ᵇ β
x_1 : α
⊢ Eq.{w + 1} (α := γ)
    ((ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g : (a : β) → γ) (⇑(c • f) : (a : α) → β)) ⋯
            (‖g‖ * ‖c • f‖) ⋯ :
          (a : α) → γ)
        x_1 :
      γ)
    ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
            (ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)) ⋯
              (‖g‖ * ‖f‖) ⋯) :
          (a : α) → γ)
        x_1 :
      γ)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f_1 g_1 : α →ᵇ β
x_1 : α
C : ℝ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 β
inst_4 : SeminormedAddCommGroup γ
inst_5 : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
f : α →ᵇ β
x : α
⊢ norm.{w} (E := γ) (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β) x) ≤ ‖g‖ * ‖f‖

Tactic:
g.le_opNorm_of_le (f.norm_coe_le_norm x)

Premises used: ContinuousLinearMap.le_opNorm_of_le, BoundedContinuousFunction.norm_coe_le_norm
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f_1 g_1 : α →ᵇ β
x_1 : α
C : ℝ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 β
inst_4 : SeminormedAddCommGroup γ
inst_5 : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
f : α →ᵇ β
x : α
⊢ norm.{w} (E := γ) (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β) x) ≤ ‖g‖ * ‖f‖

Tactic:
exact g.le_opNorm_of_le (f.norm_coe_le_norm x)

Premises used: ContinuousLinearMap.le_opNorm_of_le, BoundedContinuousFunction.norm_coe_le_norm
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 β
inst_4 : SeminormedAddCommGroup γ
inst_5 : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
f : α →ᵇ β
x : α
⊢ Eq.{w + 1} (α := γ)
    ((((ContinuousLinearMap.compLeftContinuousBounded α g : (a : α →ᵇ β) → α →ᵇ γ) f : α →ᵇ γ) : (a : α) → γ) x : γ)
    ((g : (a : β) → γ) ((f : (a : α) → β) x : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
f g : α →ᵇ R
⊢ 0 ≤ ‖f‖ * ‖g‖

Tactic:
positivity
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
⊢ ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)

Tactic:
simpa [DFunLike.ext_iff, mul_eq_zero] using h

Premises used: DFunLike.ext_iff, mul_eq_zero
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
⊢ ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)

Tactic:
have hfg : ∀ x, f x = 0 ∨ g x = 0 := by simpa [DFunLike.ext_iff, mul_eq_zero] using h
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
x : α
inl :
  ∀ (h : Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R)),
    norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
      max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
inr :
  ∀ (h : Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)),
    norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
      max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
⊢ norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
    max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))

Tactic:
obtain (h | h) := hfg x
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h_1 : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
x : α
h : Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R)
⊢ norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
    max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))

Tactic:
simp [h]
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h_1 : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
x : α
h : Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
⊢ norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
    max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))

Tactic:
simp [h]
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
⊢ ∀ (x : α),
    norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
      max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))

Tactic:
have hfg' x : ‖(f + g) x‖ = max ‖f x‖ ‖g x‖ := by obtain (h | h) := hfg x <;> simp [h]
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
hfg' :
  ∀ (x : α),
    norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
      max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
c : ℝ
hc : 0 ≤ c
simp_rw : (∀ (x : α), norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) ≤ c) ↔ max ‖f‖ ‖g‖ ≤ c
simp_rw₁ :
  (∀ (x : α), max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R)) ≤ c) ↔
    max ‖f‖ ‖g‖ ≤ c
simp_rw₂ :
  (∀ (x : α), norm.{u_1} (E := R) ((f : (a : α) → R) x : R) ≤ c ∧ norm.{u_1} (E := R) ((g : (a : α) → R) x : R) ≤ c) ↔
    ‖f‖ ≤ c ∧ ‖g‖ ≤ c
simp_rw₃ :
  (∀ (x : α), norm.{u_1} (E := R) ((f : (a : α) → R) x : R) ≤ c ∧ norm.{u_1} (E := R) ((g : (a : α) → R) x : R) ≤ c) ↔
    (∀ (x : α), norm.{u_1} (E := R) ((f : (a : α) → R) x : R) ≤ c) ∧
      ∀ (x : α), norm.{u_1} (E := R) ((g : (a : α) → R) x : R) ≤ c
⊢ ‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c

Tactic:
simp_rw [norm_le hc, hfg', max_le_iff, norm_le hc, forall_and]

Premises used: BoundedContinuousFunction.norm_le, max_le_iff, forall_and
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
hfg' :
  ∀ (x : α),
    norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
      max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
⊢ ∀ (c : ℝ) (hc : 0 ≤ c), ‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c

Tactic:
have key (c : ℝ) (hc : 0 ≤ c) : ‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c := by
    simp_rw [norm_le hc, hfg', max_le_iff, norm_le hc, forall_and]
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
hfg' :
  ∀ (x : α),
    norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
      max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
key : ∀ (c : ℝ) (hc : 0 ≤ c), ‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c
hc : 0 ≤ max ‖f‖ ‖g‖
⊢ ‖f + g‖ ≤ max ‖f‖ ‖g‖

Tactic:
rw [key]
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
hfg' :
  ∀ (x : α),
    norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
      max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
key : ∀ (c : ℝ) (hc : 0 ≤ c), ‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c
⊢ 0 ≤ max ‖f‖ ‖g‖

Tactic:
positivity
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_1
inst_1 : NonUnitalSeminormedRing R
inst_2 : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (0 : R) ∨ Eq.{u_1 + 1} (α := R) ((g : (a : α) → R) x : R) (0 : R)
hfg' :
  ∀ (x : α),
    norm.{u_1} (E := R) ((f + g : (a : α) → R) x : R) =
      max (norm.{u_1} (E := R) ((f : (a : α) → R) x : R)) (norm.{u_1} (E := R) ((g : (a : α) → R) x : R))
key : ∀ (c : ℝ) (hc : 0 ≤ c), ‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c
hc : 0 ≤ ‖f + g‖
⊢ max ‖f‖ ‖g‖ ≤ ‖f + g‖

Tactic:
rw [← key]