awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2)
dist :
  Dist.dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((h₂ : (a : δ) → β) (↑x : δ) : β) =
    Dist.dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) (↑x : δ) : β) ((extend f g₂ h₂ : (a : δ) → β) (↑x : δ) : β)
⊢ Dist.dist.{v} (α := β)
      ((h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ :
            (a : (↑(range (⇑f : (a : α) → δ))ᶜ : Type u_2)) → β)
          x :
        β)
      ((h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ :
            (a : (↑(range (⇑f : (a : α) → δ))ᶜ : Type u_2)) → β)
          x :
        β) ≤
    Dist.dist (extend f g₁ h₁) (extend f g₂ h₂)

Tactic:
calc
      dist (h₁ x) (h₂ x) = dist (extend f g₁ h₁ x) (extend f g₂ h₂ x) := by
        rw [extend_apply' x.coe_prop, extend_apply' x.coe_prop]
      _ ≤ _ := dist_coe_le_dist _

Premises used: BoundedContinuousFunction.extend, BoundedContinuousFunction.dist_coe_le_dist, Dist.dist, Subtype.val, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
h : δ →ᵇ β
g₁ g₂ : α →ᵇ β
⊢ dist (extend f g₁ h) (extend f g₂ h) = dist g₁ g₂

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
s : Set α
hs : IsClopen s
⊢ ∀ a ∈ frontier s, Eq (α := ℝ) (1 a) 0

Tactic:
simp [hs]
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β
x_1 : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
pos : ∀ (hx : x ∈ s), dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
neg : ∀ (hx : x ∉ s), dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
⊢ dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β
x_1 : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∈ s
pos : ∀ (hy : y ∈ s), dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
neg : ∀ (hy : y ∉ s), dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
⊢ dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1

Tactic:
by_cases hy : y ∈ s
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β
x_1 : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∉ s
pos : ∀ (hy : y ∈ s), dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
neg : ∀ (hy : y ∉ s), dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
⊢ dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1

Tactic:
by_cases hy : y ∈ s
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β
x_1 : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1

Tactic:
simp [hx, hy]
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β
x_1 : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∈ s
hy : y ∉ s
⊢ dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1

Tactic:
simp [hx, hy]
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β
x_1 : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∉ s
hy : y ∈ s
⊢ dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1

Tactic:
simp [hx, hy]
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β
x_1 : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∉ s
hy : y ∉ s
⊢ dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1

Tactic:
simp [hx, hy]
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : One β
⊢ Eq (α := (a : α) → β) (⇑1 : (a : α) → β) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : One β
inst_3 : CompactSpace α
⊢ Eq (α := α →ᵇ β) (mkOfCompact 1) 1

Tactic:
rfl

Premises used: BoundedContinuousFunction.mkOfCompact, BoundedContinuousFunction.const, rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : One β
f : α →ᵇ β
⊢ (∀ (x : α), Eq.{v + 1} (α := β) ((f : (a : α) → β) x : β) (1 : β)) ↔ f = 1

Tactic:
(@DFunLike.ext_iff _ _ _ _ f 1).symm

Premises used: DFunLike.ext_iff, Iff.symm
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : One β
inst_3 : TopologicalSpace γ
f : C(γ, α)
⊢ Eq (α := γ →ᵇ β) (compContinuous 1 f) 1

Tactic:
rfl

Premises used: ContinuousMap.comp, BoundedContinuousFunction.compContinuous, BoundedContinuousFunction.const, ContinuousMap.const, rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
R : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace R
inst_2 : Mul R
inst_3 : BoundedMul R
inst_4 : ContinuousMul R
f g : α →ᵇ R
⊢ (⇑(f * g) : (a : α) → R) = HMul.hMul (α := (a : α) → R) (⇑f : (a : α) → R) (⇑g : (a : α) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
R : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace R
inst_2 : Mul R
inst_3 : BoundedMul R
inst_4 : ContinuousMul R
f g : α →ᵇ R
x : α
⊢ (f * g : (a : α) → R) x = HMul.hMul (α := R) (β := R) ((f : (a : α) → R) x : R) ((g : (a : α) → R) x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : AddMonoid β
inst_3 : BoundedAdd β
inst_4 : ContinuousAdd β
f : α →ᵇ β
rw : (⇑0 : (a : α) → β) = HSMul.hSMul (α := ℕ) (β := (a : α) → β) 0 (⇑f : (a : α) → β)
rw₁ : Eq (α := (a : α) → β) (⇑0 : (a : α) → β) 0
rw₂ rw₃ : Eq (α := (a : α) → β) 0 0
⊢ (⇑(nsmulRec 0 f) : (a : α) → β) = HSMul.hSMul (α := ℕ) (β := (a : α) → β) 0 (⇑f : (a : α) → β)

Tactic:
rw [nsmulRec, zero_smul, coe_zero]

Premises used: zero_smul, nsmulRec, BoundedContinuousFunction.coe_zero
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : AddMonoid β
inst_3 : BoundedAdd β
inst_4 : ContinuousAdd β
f : α →ᵇ β
n : ℕ
rw : (⇑(nsmulRec n f + f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) (n + 1) (⇑f : (a : α) → β)
rw₁ : (⇑(nsmulRec n f + f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) + (⇑f : (a : α) → β)
rw₂ :
  HAdd.hAdd (α := (a : α) → β) (⇑(nsmulRec n f) : (a : α) → β) (⇑f : (a : α) → β) =
    HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) + (⇑f : (a : α) → β)
rw₃ rw₄ :
  HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) + (⇑f : (a : α) → β) =
    HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) + (⇑f : (a : α) → β)
⊢ (⇑(nsmulRec (n + 1) f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) (n + 1) (⇑f : (a : α) → β)

Tactic:
rw [nsmulRec, succ_nsmul, coe_add, coe_nsmulRec _ n]

Premises used: BoundedContinuousFunction.coe_add, nsmulRec, succ_nsmul
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
R : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace R
inst_2 : Monoid R
inst_3 : BoundedMul R
inst_4 : ContinuousMul R
f : α →ᵇ R
n : ℕ
obtain :
  ∀ (C : ℝ)
    (hC :
      ∀ ⦃x : R⦄,
        Membership.mem (γ := Set R) ((fun (x : R) ↦ x ^ n) '' range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → R)) x →
          ∀ ⦃y : R⦄,
            Membership.mem (γ := Set R) ((fun (x : R) ↦ x ^ n) '' range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → R)) y →
              dist x y ≤ C),
    ∃ (C : ℝ),
      ∀ (x y : α),
        dist (HPow.hPow (α := R) ((f : (a : α) → R) x : R) n) (HPow.hPow (α := R) ((f : (a : α) → R) y : R) n) ≤ C
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist (HPow.hPow (α := R) ((f : (a : α) → R) x : R) n) (HPow.hPow (α := R) ((f : (a : α) → R) y : R) n) ≤ C

Tactic:
obtain ⟨C, hC⟩ := Metric.isBounded_iff.mp <| isBounded_pow (isBounded_range f) n

Premises used: BoundedContinuousFunction.isBounded_range, Metric.isBounded_iff, Iff.mp, isBounded_pow
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
R : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace R
inst_2 : Monoid R
inst_3 : BoundedMul R
inst_4 : ContinuousMul R
f : α →ᵇ R
n : ℕ
C : ℝ
hC :
  ∀ ⦃x : R⦄,
    Membership.mem (γ := Set R) ((fun (x : R) ↦ x ^ n) '' range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → R)) x →
      ∀ ⦃y : R⦄,
        Membership.mem (γ := Set R) ((fun (x : R) ↦ x ^ n) '' range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → R)) y →
          dist x y ≤ C
x y : α
⊢ Membership.mem (γ := Set R) ((fun (x : R) ↦ x ^ n) '' range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → R))
    (HPow.hPow (α := R) ((f : (a : α) → R) x : R) n)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
R : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace R
inst_2 : Monoid R
inst_3 : BoundedMul R
inst_4 : ContinuousMul R
f : α →ᵇ R
n : ℕ
C : ℝ
hC :
  ∀ ⦃x : R⦄,
    Membership.mem (γ := Set R) ((fun (x : R) ↦ x ^ n) '' range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → R)) x →
      ∀ ⦃y : R⦄,
        Membership.mem (γ := Set R) ((fun (x : R) ↦ x ^ n) '' range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → R)) y →
          dist x y ≤ C
x y : α
⊢ Membership.mem (γ := Set R) ((fun (x : R) ↦ x ^ n) '' range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → R))
    (HPow.hPow (α := R) ((f : (a : α) → R) y : R) n)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
R : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace R
inst_2 : Monoid R
inst_3 : BoundedMul R
inst_4 : ContinuousMul R
f : α →ᵇ R
n : ℕ
C : ℝ
hC :
  ∀ ⦃x : R⦄,
    Membership.mem (γ := Set R) ((fun (x : R) ↦ x ^ n) '' range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → R)) x →
      ∀ ⦃y : R⦄,
        Membership.mem (γ := Set R) ((fun (x : R) ↦ x ^ n) '' range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → R)) y →
          dist x y ≤ C
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist (HPow.hPow (α := R) ((f : (a : α) → R) x : R) n) (HPow.hPow (α := R) ((f : (a : α) → R) y : R) n) ≤ C

Tactic:
exact ⟨C, fun x y ↦ hC (by simp) (by simp)⟩
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
R : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace R
inst_2 : Monoid R
inst_3 : BoundedMul R
inst_4 : ContinuousMul R
n : ℕ
f : α →ᵇ R
⊢ (⇑(f ^ n) : (a : α) → R) = HPow.hPow (α := (a : α) → R) (⇑f : (a : α) → R) n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
R : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace R
inst_2 : Monoid R
inst_3 : BoundedMul R
inst_4 : ContinuousMul R
n : ℕ
f : α →ᵇ R
x : α
⊢ (f ^ n : (a : α) → R) x = HPow.hPow (α := R) ((f : (a : α) → R) x : R) n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
R : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace R
inst_2 : Monoid R
inst_3 : BoundedMul R
inst_4 : ContinuousMul R
x y : α →ᵇ R
h :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := R) (((x * y).toContinuousMap : (a : α) → R) a : R)
      ((x.toContinuousMap * y.toContinuousMap : (a : α) → R) a : R)
⊢ (x * y).toContinuousMap = x.toContinuousMap * y.toContinuousMap

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
R : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace R
inst_2 : Monoid R
inst_3 : BoundedMul R
inst_4 : ContinuousMul R
x y : α →ᵇ R
a : α
⊢ Eq.{u_2 + 1} (α := R) (((x * y).toContinuousMap : (a : α) → R) a : R)
    ((x.toContinuousMap * y.toContinuousMap : (a : α) → R) a : R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
R : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace R
ι : Type u_3
s : Finset ι
inst_2 : CommMonoid R
inst_3 : BoundedMul R
inst_4 : ContinuousMul R
f : ι → α →ᵇ R
⊢ Eq (α := (a : α) → R) (⇑(∏ i ∈ s, f i) : (a : α) → R) (∏ i ∈ s, (⇑(f i) : (a : α) → R))

Tactic:
map_prod coeFnMonoidHom f s

Premises used: map_prod, BoundedContinuousFunction.coeFnMonoidHom
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
R : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace R
ι : Type u_3
s : Finset ι
inst_2 : CommMonoid R
inst_3 : BoundedMul R
inst_4 : ContinuousMul R
f : ι → α →ᵇ R
a : α
⊢ Eq.{u_2 + 1} (α := R) ((∏ i ∈ s, f i : (a : α) → R) a : R) (∏ i ∈ s, (f i : (a : α) → R) a : R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : CompactSpace α
inst_3 : Add β
inst_4 : BoundedAdd β
inst_5 : ContinuousAdd β
f g : C(α, β)
⊢ mkOfCompact (f + g) = mkOfCompact f + mkOfCompact g

Tactic:
rfl

Premises used: BoundedContinuousFunction.mkOfCompact, rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Add β
inst_3 : BoundedAdd β
inst_4 : ContinuousAdd β
inst_5 : TopologicalSpace γ
f g : α →ᵇ β
h : C(γ, α)
⊢ (g + f).compContinuous h = g.compContinuous h + f.compContinuous h

Tactic:
rfl

Premises used: ContinuousMap.comp, BoundedContinuousFunction.compContinuous, rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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 : α
C : ℝ
⊢ 0 ≤ (↑(LipschitzAdd.C β) : ℝ)

Tactic:
have C_nonneg := (LipschitzAdd.C β).coe_nonneg
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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 : α
C : ℝ
C_nonneg : 0 ≤ (↑(LipschitzAdd.C β) : ℝ)
rw : ∀ (x y : (α →ᵇ β) × (α →ᵇ β)), dist (x.1 + x.2) (y.1 + y.2) ≤ (↑(LipschitzAdd.C β) : ℝ) * dist x y
⊢ LipschitzWith (β := α →ᵇ β) (LipschitzAdd.C β) fun (p : (α →ᵇ β) × (α →ᵇ β)) ↦ p.1 + p.2

Tactic:
rw [lipschitzWith_iff_dist_le_mul]

Premises used: lipschitzWith_iff_dist_le_mul
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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 : α
C : ℝ
C_nonneg : 0 ≤ (↑(LipschitzAdd.C β) : ℝ)
f₁ g₁ f₂ g₂ : α →ᵇ β
rw :
  ∀ (x : α),
    dist.{v} (α := β) (((f₁, g₁).1 + (f₁, g₁).2 : (a : α) → β) x : β) (((f₂, g₂).1 + (f₂, g₂).2 : (a : α) → β) x : β) ≤
      (↑(LipschitzAdd.C β) : ℝ) * dist (f₁, g₁) (f₂, g₂)
⊢ dist ((f₁, g₁).1 + (f₁, g₁).2) ((f₂, g₂).1 + (f₂, g₂).2) ≤ (↑(LipschitzAdd.C β) : ℝ) * dist (f₁, g₁) (f₂, g₂)

Tactic:
rw [dist_le (mul_nonneg C_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
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₁, g₁).1 + (f₁, g₁).2 : (a : α) → β) x : β) (((f₂, g₂).1 + (f₂, g₂).2 : (a : α) → β) x : β) ≤
    (↑(LipschitzAdd.C β) : ℝ) * dist (f₁, g₁) (f₂, g₂)

Tactic:
le_trans (lipschitz_with_lipschitz_const_add ⟨f₁ x, g₁ x⟩ ⟨f₂ x, g₂ x⟩) ?_

Premises used: Prod.mk, DFunLike.coe, lipschitz_with_lipschitz_const_add, le_trans
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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 : α
refine :
  (↑(LipschitzAdd.C β) : ℝ) *
      dist.{v} (α := β × β) (((f₁ : (a : α) → β) x, (g₁ : (a : α) → β) x) : β × β)
        (((f₂ : (a : α) → β) x, (g₂ : (a : α) → β) x) : β × β) ≤
    (↑(LipschitzAdd.C β) : ℝ) * dist (f₁, g₁) (f₂, g₂)
⊢ dist.{v} (α := β) (((f₁, g₁).1 + (f₁, g₁).2 : (a : α) → β) x : β) (((f₂, g₂).1 + (f₂, g₂).2 : (a : α) → β) x : β) ≤
    (↑(LipschitzAdd.C β) : ℝ) * dist (f₁, g₁) (f₂, g₂)

Tactic:
refine le_trans (lipschitz_with_lipschitz_const_add ⟨f₁ x, g₁ x⟩ ⟨f₂ x, g₂ x⟩) ?_

Premises used: Prod.mk, DFunLike.coe, lipschitz_with_lipschitz_const_add, le_trans
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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) : β × β)
      (((f₂ : (a : α) → β) x, (g₂ : (a : α) → β) x) : β × β) ≤
    dist (f₁, g₁) (f₂, g₂)
⊢ (↑(LipschitzAdd.C β) : ℝ) *
      dist.{v} (α := β × β) (((f₁ : (a : α) → β) x, (g₁ : (a : α) → β) x) : β × β)
        (((f₂ : (a : α) → β) x, (g₂ : (a : α) → β) x) : β × β) ≤
    (↑(LipschitzAdd.C β) : ℝ) * dist (f₁, g₁) (f₂, g₂)

Tactic:
gcongr
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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
hbc₁ :
  dist.{v} (α := β) (((f₁ : (a : α) → β) x, (g₁ : (a : α) → β) x).2 : β)
      (((f₂ : (a : α) → β) x, (g₂ : (a : α) → β) x).2 : β) ≤
    dist (f₁, g₁).2 (f₂, g₂).2
⊢ dist.{v} (α := β × β) (((f₁ : (a : α) → β) x, (g₁ : (a : α) → β) x) : β × β)
      (((f₂ : (a : α) → β) x, (g₂ : (a : α) → β) x) : β × β) ≤
    dist (f₁, g₁) (f₂, g₂)

Tactic:
apply max_le_max

Premises used: max_le_max
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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).1 : β)
      (((f₂ : (a : α) → β) x, (g₂ : (a : α) → β) x).1 : β) ≤
    dist (f₁, g₁).1 (f₂, g₂).1

Tactic:
dist_coe_le_dist x

Premises used: setOf, BoundedContinuousFunction.dist_coe_le_dist
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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).1 : β)
      (((f₂ : (a : α) → β) x, (g₂ : (a : α) → β) x).1 : β) ≤
    dist (f₁, g₁).1 (f₂, g₂).1

Tactic:
exact dist_coe_le_dist x

Premises used: BoundedContinuousFunction.dist_coe_le_dist
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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).2 : β)
      (((f₂ : (a : α) → β) x, (g₂ : (a : α) → β) x).2 : β) ≤
    dist (f₁, g₁).2 (f₂, g₂).2

Tactic:
dist_coe_le_dist x

Premises used: setOf, BoundedContinuousFunction.dist_coe_le_dist
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
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).2 : β)
      (((f₂ : (a : α) → β) x, (g₂ : (a : α) → β) x).2 : β) ≤
    dist (f₁, g₁).2 (f₂, g₂).2

Tactic:
exact dist_coe_le_dist x

Premises used: BoundedContinuousFunction.dist_coe_le_dist
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_2
inst_1 : PseudoMetricSpace R
inst_2 : Sub R
inst_3 : BoundedSub R
inst_4 : ContinuousSub R
f g : α →ᵇ R
x : α
⊢ (f - g : (a : α) → R) x = HSub.hSub (α := R) (β := R) ((f : (a : α) → R) x : R) ((g : (a : α) → R) x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
inst : TopologicalSpace α
R : Type u_2
inst_1 : PseudoMetricSpace R
inst_2 : Sub R
inst_3 : BoundedSub R
inst_4 : ContinuousSub R
f g : α →ᵇ R
⊢ (⇑(f - g) : (a : α) → R) = HSub.hSub (α := (a : α) → R) (⇑f : (a : α) → R) (⇑g : (a : α) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_2
inst_1 : PseudoMetricSpace β
inst_2 : NatCast β
n : ℕ
x : α
⊢ Eq.{u_2 + 1} (α := β) (((↑n : α →ᵇ β) : (a : α) → β) x : β) ((↑n : β) : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_2
inst_1 : PseudoMetricSpace β
inst_2 : IntCast β
m : ℤ
x : α
⊢ Eq.{u_2 + 1} (α := β) (((↑m : α →ᵇ β) : (a : α) → β) x : β) ((↑m : β) : β)

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 : α →ᵇ β
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

Tactic:
(dist_smul_pair c (f x) (f y)).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 : α →ᵇ β
b : ℝ
hb : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ b
x y : α
refine : dist c 0 * dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ dist c 0 * b
⊢ dist ((c • f.toContinuousMap).toFun x) ((c • f.toContinuousMap).toFun y) ≤ dist c 0 * b

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

Premises used: LE.le.trans, DFunLike.coe, dist_smul_pair