awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : AddMonoid β
inst_3 : LipschitzAdd β
f g : α →ᵇ β
x_1 : α
C : ℝ
C_nonneg : 0 ≤ (↑(LipschitzAdd.C β) : ℝ)
f₁ g₁ f₂ g₂ : α →ᵇ β
x : α
⊢ (↑(LipschitzAdd.C β) : ℝ) *
      dist.{v} (α := β × β) (((f₁ : (a : α) → β) x, (g₁ : (a : α) → β) x) : β × β)
        (((f₂ : (a : α) → β) x, (g₂ : (a : α) → β) x) : β × β) ≤
    (↑(LipschitzAdd.C β) : ℝ) * dist (f₁, g₁) (f₂, g₂)
have hbc : dist.{v} (α := β × β) (((f₁ : (a : α) → β) x, (g₁ : (a : α) → β) x) : β × β)
    (((f₂ : (a : α) → β) x, (g₂ : (a : α) → β) x) : β × β) ≤
  dist (f₁, g₁) (f₂, g₂)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : AddMonoid β
inst_3 : LipschitzAdd β
f g : α →ᵇ β
x_1 : α
C : ℝ
C_nonneg : 0 ≤ (↑(LipschitzAdd.C β) : ℝ)
f₁ g₁ f₂ g₂ : α →ᵇ β
x : α
⊢ dist.{v} (α := β × β) (((f₁ : (a : α) → β) x, (g₁ : (a : α) → β) x) : β × β)
      (((f₂ : (a : α) → β) x, (g₂ : (a : α) → β) x) : β × β) ≤
    dist (f₁, g₁) (f₂, g₂)
have hbc : dist.{v} (α := β) (((f₁ : (a : α) → β) x, (g₁ : (a : α) → β) x).1 : β)
    (((f₂ : (a : α) → β) x, (g₂ : (a : α) → β) x).1 : β) ≤
  dist (f₁, g₁).1 (f₂, g₂).1
Tactic: apply max_le_max
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : AddMonoid β
inst_3 : LipschitzAdd β
f g : α →ᵇ β
x_1 : α
C : ℝ
C_nonneg : 0 ≤ (↑(LipschitzAdd.C β) : ℝ)
f₁ g₁ f₂ g₂ : α →ᵇ β
x : α
hbc :
  dist.{v} (α := β) (((f₁ : (a : α) → β) x, (g₁ : (a : α) → β) x).1 : β)
      (((f₂ : (a : α) → β) x, (g₂ : (a : α) → β) x).1 : β) ≤
    dist (f₁, g₁).1 (f₂, g₂).1
⊢ dist.{v} (α := β × β) (((f₁ : (a : α) → β) x, (g₁ : (a : α) → β) x) : β × β)
      (((f₂ : (a : α) → β) x, (g₂ : (a : α) → β) x) : β × β) ≤
    dist (f₁, g₁) (f₂, g₂)
have hbc₁ : dist.{v} (α := β) (((f₁ : (a : α) → β) x, (g₁ : (a : α) → β) x).2 : β)
    (((f₂ : (a : α) → β) x, (g₂ : (a : α) → β) x).2 : β) ≤
  dist (f₁, g₁).2 (f₂, g₂).2
Tactic: apply max_le_max
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 ((c • f.toContinuousMap).toFun x) ((c • f.toContinuousMap).toFun y) ≤ dist c 0 * b
have refine : dist c 0 * dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ dist c 0 * b
Tactic: refine (dist_smul_pair c (f x) (f y)).trans ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 c 0 * dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ dist c 0 * b
have hbc : dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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₂ : α →ᵇ β
⊢ dist (c • f₁) (c • f₂) ≤ dist c 0 * dist f₁ f₂
have rw : ∀ (x : α), dist.{v} (α := β) ((c • f₁ : (a : α) → β) x : β) ((c • f₂ : (a : α) → β) x : β) ≤ dist c 0 * dist f₁ f₂
Tactic: rw [dist_le (mul_nonneg dist_nonneg dist_nonneg)]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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₂
have refine : dist c 0 * dist.{v} (α := β) ((f₁ : (a : α) → β) x : β) ((f₂ : (a : α) → β) x : β) ≤ dist c 0 * dist f₁ f₂
Tactic: refine (dist_smul_pair c (f₁ x) (f₂ x)).trans ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 c 0 * dist.{v} (α := β) ((f₁ : (a : α) → β) x : β) ((f₂ : (a : α) → β) x : β) ≤ dist c 0 * dist f₁ f₂
have hbc : dist.{v} (α := β) ((f₁ : (a : α) → β) x : β) ((f₂ : (a : α) → β) x : β) ≤ dist f₁ f₂
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 : α →ᵇ β
⊢ dist (c₁ • f) (c₂ • f) ≤ dist c₁ c₂ * dist f 0
have rw : ∀ (x : α), dist.{v} (α := β) ((c₁ • f : (a : α) → β) x : β) ((c₂ • f : (a : α) → β) x : β) ≤ dist c₁ c₂ * dist f 0
Tactic: rw [dist_le (by positivity)]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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
have refine : dist c₁ c₂ * dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) ≤ dist c₁ c₂ * dist f 0
Tactic: refine (dist_pair_smul c₁ c₂ (f x)).trans ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
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 c₁ c₂ * dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) ≤ dist c₁ c₂ * dist f 0
have hbc : dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) ≤ dist f 0
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (hypothesis)
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
⊢ (f : (a : α) → ℝ≥0) x ≤ nndist f 0
have key : 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
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
key : nndist (α := ℝ≥0) ((f : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0) ≤ nndist f 0
⊢ (f : (a : α) → ℝ≥0) x ≤ nndist f 0
have rwa : ∀ (key : (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
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
h : Nonempty α
⊢ ‖f‖ = sInf {C : ℝ | ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C}
have obtain : ∀ (a : α), ‖f‖ = sInf {C : ℝ | ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C}
Tactic: obtain ⟨a⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
⊢ ‖f‖ = sInf {C : ℝ | ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C}
have rw : Eq (α := ℝ) (sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C})
  (sInf {C : ℝ | ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C})
Tactic: rw [norm_eq]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
⊢ Eq (α := ℝ) (sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C})
    (sInf {C : ℝ | ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ C})
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
x : ℝ
⊢ (0 ≤ x ∧ ∀ (x_1 : α), norm.{v} (E := β) ((f : (a : α) → β) x_1 : β) ≤ x) ↔
    ∀ (x_1 : α), norm.{v} (E := β) ((f : (a : α) → β) x_1 : β) ≤ x
have e_a : (∀ (x_1 : α), norm.{v} (E := β) ((f : (a : α) → β) x_1 : β) ≤ x) → 0 ≤ x
Tactic: simp only [and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : Nonempty α
f : α →ᵇ β
M : ℝ
⊢ ‖f‖ ≤ M ↔ ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ M
have simp_rw : dist f 0 ≤ M ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) ≤ M
Tactic: simp_rw [norm_def, ← dist_zero_right]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : CompactSpace α
f : α →ᵇ β
M : ℝ
M0 : 0 < M
⊢ ‖f‖ < M ↔ ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) < M
have simp_rw : dist f 0 < M ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < M
Tactic: simp_rw [norm_def, ← dist_zero_right]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : Nonempty α
inst_3 : CompactSpace α
f : α →ᵇ β
M : ℝ
⊢ ‖f‖ < M ↔ ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) < M
have simp_rw : dist f 0 < M ↔ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β) < M
Tactic: simp_rw [norm_def, ← dist_zero_right]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ‖f‖ = ⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β)
have simp_rw : dist f 0 = ⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β)
Tactic: simp_rw [norm_def, dist_eq_iSup, coe_zero, Pi.zero_apply, dist_zero_right]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
simp_rw : dist f 0 = ⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β)
⊢ ‖f‖ = ⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β)
have simp_rw₁ : Eq (α := ℝ) (⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((0 : (a : α) → β) x : β))
  (⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β))
Tactic: simp_rw [norm_def, dist_eq_iSup, coe_zero, Pi.zero_apply, dist_zero_right]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
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 : β))
⊢ ‖f‖ = ⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β)
have simp_rw₂ : Eq (α := ℝ) (⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 x : β))
  (⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β))
Tactic: simp_rw [norm_def, dist_eq_iSup, coe_zero, Pi.zero_apply, dist_zero_right]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
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 : β))
⊢ ‖f‖ = ⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β)
have simp_rw₃ : Eq (α := ℝ) (⨆ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) (0 : β))
  (⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β))
Tactic: simp_rw [norm_def, dist_eq_iSup, coe_zero, Pi.zero_apply, dist_zero_right]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
⊢ (⇑(zsmulRec (fun (x1 : ℕ) (x2 : α →ᵇ β) ↦ x1 • x2) (Int.ofNat n) f) : (a : α) → β) =
    HSMul.hSMul (β := (a : α) → β) (Int.ofNat n) (⇑f : (a : α) → β)
have rw : (⇑(n • f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) (Int.ofNat n) (⇑f : (a : α) → β)
Tactic: rw [zsmulRec, Int.ofNat_eq_natCast, coe_nsmul, natCast_zsmul]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
rw : (⇑(n • f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) (Int.ofNat n) (⇑f : (a : α) → β)
⊢ (⇑(zsmulRec (fun (x1 : ℕ) (x2 : α →ᵇ β) ↦ x1 • x2) (Int.ofNat n) f) : (a : α) → β) =
    HSMul.hSMul (β := (a : α) → β) (Int.ofNat n) (⇑f : (a : α) → β)
have rw₁ : (⇑(n • f) : (a : α) → β) = HSMul.hSMul (α := ℤ) (β := (a : α) → β) (↑n : ℤ) (⇑f : (a : α) → β)
Tactic: rw [zsmulRec, Int.ofNat_eq_natCast, coe_nsmul, natCast_zsmul]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
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 : α) → β)
⊢ (⇑(zsmulRec (fun (x1 : ℕ) (x2 : α →ᵇ β) ↦ x1 • x2) (Int.ofNat n) f) : (a : α) → β) =
    HSMul.hSMul (β := (a : α) → β) (Int.ofNat n) (⇑f : (a : α) → β)
have rw₂ : HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) =
  HSMul.hSMul (α := ℤ) (β := (a : α) → β) (↑n : ℤ) (⇑f : (a : α) → β)
Tactic: rw [zsmulRec, Int.ofNat_eq_natCast, coe_nsmul, natCast_zsmul]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
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 : α) → β)
⊢ (⇑(zsmulRec (fun (x1 : ℕ) (x2 : α →ᵇ β) ↦ x1 • x2) (Int.ofNat n) f) : (a : α) → β) =
    HSMul.hSMul (β := (a : α) → β) (Int.ofNat n) (⇑f : (a : α) → β)
have rw₃ : HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β)
Tactic: rw [zsmulRec, Int.ofNat_eq_natCast, coe_nsmul, natCast_zsmul]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
⊢ (⇑(zsmulRec (fun (x1 : ℕ) (x2 : α →ᵇ β) ↦ x1 • x2) (Int.negSucc n) f) : (a : α) → β) =
    HSMul.hSMul (β := (a : α) → β) (Int.negSucc n) (⇑f : (a : α) → β)
have rw : (⇑(-(n.succ • f)) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) (Int.negSucc n) (⇑f : (a : α) → β)
Tactic: rw [zsmulRec, negSucc_zsmul, coe_neg, coe_nsmul]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
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 : α) → β)
⊢ (⇑(zsmulRec (fun (x1 : ℕ) (x2 : α →ᵇ β) ↦ x1 • x2) (Int.negSucc n) f) : (a : α) → β) =
    HSMul.hSMul (β := (a : α) → β) (Int.negSucc n) (⇑f : (a : α) → β)
have rw₁ : (⇑(-(n.succ • f)) : (a : α) → β) = -HSMul.hSMul (β := (a : α) → β) (n + 1) (⇑f : (a : α) → β)
Tactic: rw [zsmulRec, negSucc_zsmul, coe_neg, coe_nsmul]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
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 : α) → β)
⊢ (⇑(zsmulRec (fun (x1 : ℕ) (x2 : α →ᵇ β) ↦ x1 • x2) (Int.negSucc n) f) : (a : α) → β) =
    HSMul.hSMul (β := (a : α) → β) (Int.negSucc n) (⇑f : (a : α) → β)
have rw₂ : -(⇑(n.succ • f) : (a : α) → β) = -HSMul.hSMul (β := (a : α) → β) (n + 1) (⇑f : (a : α) → β)
Tactic: rw [zsmulRec, negSucc_zsmul, coe_neg, coe_nsmul]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
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 : α) → β)
⊢ (⇑(zsmulRec (fun (x1 : ℕ) (x2 : α →ᵇ β) ↦ x1 • x2) (Int.negSucc n) f) : (a : α) → β) =
    HSMul.hSMul (β := (a : α) → β) (Int.negSucc n) (⇑f : (a : α) → β)
have rw₃ : -HSMul.hSMul (β := (a : α) → β) n.succ (⇑f : (a : α) → β) = -HSMul.hSMul (β := (a : α) → β) (n + 1) (⇑f : (a : α) → β)
Tactic: rw [zsmulRec, negSucc_zsmul, coe_neg, coe_nsmul]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ Eq (α := ℝ) (⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β))
    (↑(⨆ (x : α), nnnorm.{v} (E := β) ((f : (a : α) → β) x : β)) : ℝ)
have simp_rw : ⨆ (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]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
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 : β)) : ℝ)
⊢ Eq (α := ℝ) (⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β))
    (↑(⨆ (x : α), nnnorm.{v} (E := β) ((f : (a : α) → β) x : β)) : ℝ)
have simp_rw₁ : Eq (α := ℝ) (⨆ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β))
  (⨆ (i : α), (↑(nnnorm.{v} (E := β) ((f : (a : α) → β) i : β)) : ℝ))
Tactic: simp_rw [val_eq_coe, NNReal.coe_iSup, coe_nnnorm]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
⊢ ‖HSub.hSub (α := β) (β := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)‖ ≤ dist f g
have rw : ‖HSub.hSub (α := β) (β := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)‖ ≤ ‖f - g‖
Tactic: rw [dist_eq_norm]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : TopologicalSpace γ
f : α →ᵇ β
g : C(γ, α)
⊢ (↑1 : ℝ) * dist f 0 ≤ ‖f‖
have rw : 1 * dist f 0 ≤ ‖f‖
Tactic: rw [NNReal.coe_one, one_mul, dist_zero_right]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : TopologicalSpace γ
f : α →ᵇ β
g : C(γ, α)
rw : 1 * dist f 0 ≤ ‖f‖
⊢ (↑1 : ℝ) * dist f 0 ≤ ‖f‖
have rw₁ : dist f 0 ≤ ‖f‖
Tactic: rw [NNReal.coe_one, one_mul, dist_zero_right]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
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‖
⊢ (↑1 : ℝ) * dist f 0 ≤ ‖f‖
have rw₂ : ‖f‖ ≤ ‖f‖
Tactic: rw [NNReal.coe_one, one_mul, dist_zero_right]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
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‖
have refine : ∀ (x : α), ‖HSMul.hSMul (β := (a : α) → β) c (⇑f.toContinuousMap : (a : α) → β) x‖ ≤ ‖c‖ * ‖f‖
Tactic: refine norm_ofNormedAddCommGroup_le _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
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 : α →ᵇ β
⊢ 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‖) ⋯
have h : ∀ (x : α),
  Eq.{w + 1} (α := γ)
    ((ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g_2 : (a : β) → γ) (⇑(f + g) : (a : α) → β))
            sorry (‖g_2‖ * ‖f + g‖) sorry :
          (a : α) → γ)
        x :
      γ)
    ((ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g_2 : (a : β) → γ) (⇑f : (a : α) → β)) sorry
              (‖g_2‖ * ‖f‖) sorry +
            ofNormedAddCommGroup (Function.comp.{u + 1, v + 1, w + 1} (β := β) (⇑g_2 : (a : β) → γ) (⇑g : (a : α) → β))
              sorry (‖g_2‖ * ‖g‖) sorry :
          (a : α) → γ)
        x :
      γ)
Tactic: ext