awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : PseudoEMetricSpace Z
s : Set X
Cg rg : ℝ≥0
g : Y → Z
t : Set Y
hg : HolderOnWith Cg rg g t
Cf rf : ℝ≥0
f : X → Y
hf : HolderOnWith Cf rf f s
hst : MapsTo f s t
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ edist ((g ∘ f) x) ((g ∘ f) y) ≤ (↑Cg : ℝ≥0∞) * ((↑Cf : ℝ≥0∞) * edist x y ^ (↑rf : ℝ)) ^ (↑rg : ℝ)

Tactic:
hg.edist_le_of_le (hst hx) (hst hy) (hf.edist_le hx hy)

Premises used: HolderOnWith.edist_le, HolderOnWith.edist_le_of_le
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : PseudoEMetricSpace Z
s : Set X
Cg rg : ℝ≥0
g : Y → Z
t : Set Y
hg : HolderOnWith Cg rg g t
Cf rf : ℝ≥0
f : X → Y
hf : HolderOnWith Cf rf f s
hst : MapsTo f s t
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ edist ((g ∘ f) x) ((g ∘ f) y) ≤ (↑Cg : ℝ≥0∞) * ((↑Cf : ℝ≥0∞) * edist x y ^ (↑rf : ℝ)) ^ (↑rg : ℝ)

Tactic:
exact hg.edist_le_of_le (hst hx) (hst hy) (hf.edist_le hx hy)

Premises used: HolderOnWith.edist_le, HolderOnWith.edist_le_of_le
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : PseudoEMetricSpace Z
Cg rg : ℝ≥0
g : Y → Z
t : Set Y
hg : HolderOnWith Cg rg g t
Cf rf : ℝ≥0
f : X → Y
hf : HolderWith Cf rf f
ht : ∀ (x : X), f x ∈ t
⊢ HolderWith (Cg * Cf ^ (↑rg : ℝ)) (rg * rf) (g ∘ f)

Tactic:
holderOnWith_univ.mp <| hg.comp (hf.holderOnWith univ) fun x _ => ht x

Premises used: holderOnWith_univ, HolderOnWith.comp, HolderWith.holderOnWith, Set.univ, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
⊢ UniformContinuousOn f s

Tactic:
EMetric.uniformContinuousOn_iff.2 fun ε εpos => ?_

Premises used: Iff.mpr, EMetric.uniformContinuousOn_iff
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
refine :
  ∀ (ε : ℝ≥0∞) (εpos : ε > 0), ∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
⊢ UniformContinuousOn f s

Tactic:
refine EMetric.uniformContinuousOn_iff.2 fun ε εpos => ?_

Premises used: Iff.mpr, EMetric.uniformContinuousOn_iff
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
⊢ Tendsto (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) (𝓝 0) (𝓝 0)

Tactic:
have : Tendsto (fun d : ℝ≥0∞ => (C : ℝ≥0∞) * d ^ (r : ℝ)) (𝓝 0) (𝓝 0) :=
    ENNReal.tendsto_const_mul_rpow_nhds_zero_of_pos ENNReal.coe_ne_top h0
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) (𝓝 0) (𝓝 0)
rcases :
  ∀ (δ : ℝ≥0∞) (δ0 : 0 < δ)
    (H :
      Iio δ ⊆
        preimage (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ x < ε) x}),
    ∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
⊢ ∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε

Tactic:
rcases ENNReal.nhds_zero_basis.mem_iff.1 (this (gt_mem_nhds εpos)) with ⟨δ, δ0, H⟩

Premises used: gt_mem_nhds, Filter.HasBasis.mem_iff, ENNReal.nhds_zero_basis, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : Iio δ ⊆ preimage (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ x < ε) x}
⊢ ∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε

Tactic:
⟨δ, δ0, fun hx y hy h => (hf.edist_le hx hy).trans_lt (H h)⟩

Premises used: And.intro, Exists.intro, HolderOnWith.edist_le, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : Iio δ ⊆ preimage (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ x < ε) x}
⊢ ∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε

Tactic:
exact ⟨δ, δ0, fun hx y hy h => (hf.edist_le hx hy).trans_lt (H h)⟩
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
⊢ ContinuousOn f s

Tactic:
(hf.uniformContinuousOn h0).continuousOn

Premises used: UniformContinuousOn.continuousOn, HolderOnWith.uniformContinuousOn
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s t : Set X
hf : HolderOnWith C r f s
ht : t ⊆ s
⊢ HolderOnWith C r f t

Tactic:
fun _ hx _ hy => hf.edist_le (ht hx) (ht hy)

Premises used: HolderOnWith, HolderOnWith.edist_le
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
d : ℝ≥0∞
hd : ediam s ≤ d
⊢ ediam (f '' s) ≤ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)

Tactic:
ediam_image_le_iff.2 fun _ hx _ hy =>
    hf.edist_le_of_le hx hy <| (edist_le_ediam_of_mem hx hy).trans hd

Premises used: Iff.mpr, Metric.edist_le_ediam_of_mem, Metric.ediam_image_le_iff, LE.le.trans, HolderOnWith.edist_le_of_le
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
⊢ ediam (f '' s) ≤ (↑C : ℝ≥0∞) * ediam s ^ (↑r : ℝ)

Tactic:
hf.ediam_image_le_of_le le_rfl

Premises used: le_rfl, HolderOnWith.ediam_image_le_of_le
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s t : Set X
hf : HolderOnWith C r f s
ht : t ⊆ s
⊢ ediam (f '' t) ≤ (↑C : ℝ≥0∞) * ediam t ^ (↑r : ℝ)

Tactic:
(hf.mono ht).ediam_image_le

Premises used: HolderOnWith.ediam_image_le, HolderOnWith.mono
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s t : Set X
hf : HolderOnWith C r f s
ht : t ⊆ s
d : ℝ≥0∞
hd : ediam t ≤ d
⊢ ediam (f '' t) ≤ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)

Tactic:
(hf.mono ht).ediam_image_le_of_le hd

Premises used: HolderOnWith.ediam_image_le_of_le, HolderOnWith.mono
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s t : Set X
hf : HolderOnWith C r f s
d : ℝ≥0∞
hd : ediam t ≤ d
⊢ ediam (f '' (t ∩ s)) ≤ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)

Tactic:
hf.ediam_image_le_of_subset_of_le inter_subset_right <|
    (ediam_mono inter_subset_left).trans hd

Premises used: HolderOnWith.ediam_image_le_of_subset_of_le, Set.inter_subset_left, Metric.ediam_mono, LE.le.trans, Set.inter_subset_right
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
t : Set X
⊢ ediam (f '' (t ∩ s)) ≤ (↑C : ℝ≥0∞) * ediam t ^ (↑r : ℝ)

Tactic:
hf.ediam_image_inter_le_of_le le_rfl

Premises used: le_rfl, HolderOnWith.ediam_image_inter_le_of_le
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C₁ C₂ s t₁ t₂ : ℝ≥0
A : Set X
hf₁ : HolderOnWith C₁ r f A
hf₂ : HolderOnWith C₂ s f A
ht : t₁ + t₂ = 1
x : X
hx : x ∈ A
y : X
hy : y ∈ A
⊢ edist (f x) (f y) = edist (f x) (f y) ^ (↑t₁ : ℝ) * edist (f x) (f y) ^ (↑t₂ : ℝ)

Tactic:
simp [← ENNReal.rpow_add_of_nonneg, ← NNReal.coe_add, ht]

Premises used: NNReal.coe_add, ENNReal.rpow_add_of_nonneg
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C₁ C₂ s t₁ t₂ : ℝ≥0
A : Set X
hf₁ : HolderOnWith C₁ r f A
hf₂ : HolderOnWith C₂ s f A
ht : t₁ + t₂ = 1
x : X
hx : x ∈ A
y : X
hy : y ∈ A
h₁ : 0 ≤ (↑t₁ : ℝ)
nth_grw :
  ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * edist (f x) (f y) ^ (↑t₂ : ℝ) ≤
    ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ)
nth_grw₁ nth_grw₂ :
  ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ) ≤
    ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ)
⊢ edist (f x) (f y) ^ (↑t₁ : ℝ) * edist (f x) (f y) ^ (↑t₂ : ℝ) ≤
    ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ)

Tactic:
nth_grw 1 [hf₁ x hx y hy, hf₂ x hx y hy]
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C₁ C₂ s t₁ t₂ : ℝ≥0
A : Set X
hf₁ : HolderOnWith C₁ r f A
hf₂ : HolderOnWith C₂ s f A
ht : t₁ + t₂ = 1
x : X
hx : x ∈ A
y : X
hy : y ∈ A
simp :
  (↑C₁ : ℝ≥0∞) ^ (↑t₁ : ℝ) * (edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) *
      ((↑C₂ : ℝ≥0∞) ^ (↑t₂ : ℝ) * (edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ)) =
    (↑C₁ : ℝ≥0∞) ^ (↑t₁ : ℝ) * (↑C₂ : ℝ≥0∞) ^ (↑t₂ : ℝ) *
      ((edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * (edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ))
⊢ ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ) =
    (↑(C₁ ^ (↑t₁ : ℝ)) : ℝ≥0∞) * (↑(C₂ ^ (↑t₂ : ℝ)) : ℝ≥0∞) * edist x y ^ ((↑r : ℝ) * (↑t₁ : ℝ) + (↑s : ℝ) * (↑t₂ : ℝ))

Tactic:
simp (discharger := positivity) only [ENNReal.mul_rpow_of_nonneg,
          ENNReal.rpow_add_of_nonneg, ENNReal.rpow_mul, ENNReal.coe_rpow_of_nonneg]

Premises used: ENNReal.rpow_mul, ENNReal.mul_rpow_of_nonneg, ENNReal.coe_rpow_of_nonneg, ENNReal.rpow_add_of_nonneg
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C₁ C₂ s t₁ t₂ : ℝ≥0
A : Set X
hf₁ : HolderOnWith C₁ r f A
hf₂ : HolderOnWith C₂ s f A
ht : t₁ + t₂ = 1
x : X
hx : x ∈ A
y : X
hy : y ∈ A
⊢ (↑C₁ : ℝ≥0∞) ^ (↑t₁ : ℝ) * (edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) *
      ((↑C₂ : ℝ≥0∞) ^ (↑t₂ : ℝ) * (edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ)) =
    (↑C₁ : ℝ≥0∞) ^ (↑t₁ : ℝ) * (↑C₂ : ℝ≥0∞) ^ (↑t₂ : ℝ) *
      ((edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * (edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ))

Tactic:
ring
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C₁ C₂ s t₁ t₂ : ℝ≥0
A : Set X
hf₁ : HolderOnWith C₁ r f A
hf₂ : HolderOnWith C₂ s f A
ht : t₁ + t₂ = 1
x : X
hx : x ∈ A
y : X
hy : y ∈ A
calc : edist (f x) (f y) = edist (f x) (f y) ^ (↑t₁ : ℝ) * edist (f x) (f y) ^ (↑t₂ : ℝ)
calc₁ :
  edist (f x) (f y) ^ (↑t₁ : ℝ) * edist (f x) (f y) ^ (↑t₂ : ℝ) ≤
    ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ)
calc₂ :
  ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ) =
    (↑(C₁ ^ (↑t₁ : ℝ) * C₂ ^ (↑t₂ : ℝ)) : ℝ≥0∞) * edist x y ^ (↑(r * t₁ + s * t₂) : ℝ)
⊢ edist (f x) (f y) ≤ (↑(C₁ ^ (↑t₁ : ℝ) * C₂ ^ (↑t₂ : ℝ)) : ℝ≥0∞) * edist x y ^ (↑(r * t₁ + s * t₂) : ℝ)

Tactic:
calc edist (f x) (f y)
      = (edist (f x) (f y)) ^ (t₁ : ℝ) * (edist (f x) (f y)) ^ (t₂ : ℝ) := by
        simp [← ENNReal.rpow_add_of_nonneg, ← NNReal.coe_add, ht]
    _ ≤ (C₁ * (edist x y) ^ (r : ℝ)) ^ (t₁ : ℝ) * (C₂ * (edist x y) ^ (s : ℝ)) ^ (t₂ : ℝ) := by
        nth_grw 1 [hf₁ x hx y hy, hf₂ x hx y hy]
    _ = ↑(C₁ ^ (t₁ : ℝ) * C₂ ^ (t₂ : ℝ)) * (edist x y) ^ (↑(r * t₁ + s * t₂) : ℝ) := by
        push_cast
        simp (discharger := positivity) only [ENNReal.mul_rpow_of_nonneg,
          ENNReal.rpow_add_of_nonneg, ENNReal.rpow_mul, ENNReal.coe_rpow_of_nonneg]
        ring

Premises used: ENNReal.ofNNReal, HMul.hMul, HPow.hPow, HAdd.hAdd, EDist.edist, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
x : X
hx : x ∈ A
y : X
hy : y ∈ A
simp : edist (f x) (f y) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞)
⊢ edist (f x) (f y) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞) * edist x y ^ (↑0 : ℝ)

Tactic:
simp only [NNReal.coe_zero, ENNReal.rpow_zero, mul_one]

Premises used: NNReal.coe_zero, ENNReal.rpow_zero, mul_one
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
x : X
hx : x ∈ A
y : X
hy : y ∈ A
⊢ 0 ≤ (↑r : ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
x : X
hx : x ∈ A
y : X
hy : y ∈ A
grw : (↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞)
grw₁ : (↑C : ℝ≥0∞) * (↑D : ℝ≥0∞) ^ (↑r : ℝ) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞)
grw₂ : (↑C : ℝ≥0∞) * (↑D : ℝ≥0∞) ^ (↑r : ℝ) ≤ (↑C : ℝ≥0∞) * (↑(D ^ (↑r : ℝ)) : ℝ≥0∞)
grw₃ grw₄ : (↑C : ℝ≥0∞) * (↑D : ℝ≥0∞) ^ (↑r : ℝ) ≤ (↑C : ℝ≥0∞) * (↑D : ℝ≥0∞) ^ (↑r : ℝ)
⊢ edist (f x) (f y) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞)

Tactic:
grw [hf x hx y hy, hA x hx y hy, ENNReal.coe_mul, ENNReal.coe_rpow_of_nonneg _ (by simp)]

Premises used: ENNReal.coe_rpow_of_nonneg, ENNReal.coe_mul
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : s ≤ r
inl : ∀ (hsr : 0 ≤ r), HolderOnWith (C * D ^ ((↑r : ℝ) - (↑0 : ℝ))) 0 f A
inr : ∀ (ht : 0 < s), HolderOnWith (C * D ^ ((↑r : ℝ) - (↑s : ℝ))) s f A
⊢ HolderOnWith (C * D ^ ((↑r : ℝ) - (↑s : ℝ))) s f A

Tactic:
obtain rfl | ht := eq_zero_or_pos s

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : 0 ≤ r
⊢ HolderOnWith (C * D ^ ((↑r : ℝ) - (↑0 : ℝ))) 0 f A

Tactic:
simpa using hf.holderOnWith_zero_of_bounded hA

Premises used: HolderOnWith.holderOnWith_zero_of_bounded
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : s ≤ r
ht : 0 < s
⊢ 0 < r

Tactic:
have hr : 0 < r := ht.trans_le hsr
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : s ≤ r
ht : 0 < s
hr : 0 < r
⊢ (↑s : ℝ) ≤ (↑r : ℝ)

Tactic:
rw [← NNReal.coe_le_coe] at hsr

Premises used: NNReal.coe_le_coe
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : s ≤ r
ht : 0 < s
hr : 0 < r
hsr₁ : (↑s : ℝ) ≤ (↑r : ℝ)
⊢ 0 < s

Tactic:
rw [← NNReal.coe_le_coe] at hsr

Premises used: NNReal.coe_le_coe
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : s ≤ r
ht : 0 < s
hr : 0 < r
hsr₁ : (↑s : ℝ) ≤ (↑r : ℝ)
ht₁ : 0 < s
⊢ 0 < r

Tactic:
rw [← NNReal.coe_le_coe] at hsr

Premises used: NNReal.coe_le_coe
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : (↑s : ℝ) ≤ (↑r : ℝ)
ht : 0 < s
hr : 0 < r
⊢ 0 < (↑r : ℝ)

Tactic:
rw [← NNReal.coe_pos] at hr

Premises used: NNReal.coe_pos
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : (↑s : ℝ) ≤ (↑r : ℝ)
ht : 0 < s
hr : 0 < (↑r : ℝ)
⊢ 0 ≤ (↑s : ℝ) / (↑r : ℝ)

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : (↑s : ℝ) ≤ (↑r : ℝ)
ht : 0 < s
hr : 0 < (↑r : ℝ)
θ₁ : ℝ≥0 := NNReal.mk ((↑s : ℝ) / (↑r : ℝ)) ⋯
⊢ 0 ≤ (↑r : ℝ)

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : (↑s : ℝ) ≤ (↑r : ℝ)
ht : 0 < s
hr : 0 < (↑r : ℝ)
θ₁ : ℝ≥0 := NNReal.mk ((↑s : ℝ) / (↑r : ℝ)) ⋯
⊢ 0 ≤ 1 - (↑s : ℝ) / (↑r : ℝ)

Tactic:
simpa using div_le_one_of_le₀ hsr (by positivity)

Premises used: div_le_one_of_le₀
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : (↑s : ℝ) ≤ (↑r : ℝ)
ht : 0 < s
hr : 0 < (↑r : ℝ)
θ₁ : ℝ≥0 := NNReal.mk ((↑s : ℝ) / (↑r : ℝ)) ⋯
θ₂ : ℝ≥0 := NNReal.mk (1 - (↑s : ℝ) / (↑r : ℝ)) ⋯
a : (↑(θ₁ + θ₂) : ℝ) = (↑1 : ℝ)
⊢ θ₁ + θ₂ = 1

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : (↑s : ℝ) ≤ (↑r : ℝ)
ht : 0 < s
hr : 0 < (↑r : ℝ)
θ₁ : ℝ≥0 := NNReal.mk ((↑s : ℝ) / (↑r : ℝ)) ⋯
θ₂ : ℝ≥0 := NNReal.mk (1 - (↑s : ℝ) / (↑r : ℝ)) ⋯
⊢ (↑(θ₁ + θ₂) : ℝ) = (↑1 : ℝ)

Tactic:
simp [θ₁, θ₂]
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : (↑s : ℝ) ≤ (↑r : ℝ)
ht : 0 < s
hr : 0 < (↑r : ℝ)
θ₁ : ℝ≥0 := NNReal.mk ((↑s : ℝ) / (↑r : ℝ)) ⋯
θ₂ : ℝ≥0 := NNReal.mk (1 - (↑s : ℝ) / (↑r : ℝ)) ⋯
⊢ θ₁ + θ₂ = 1

Tactic:
have hθ : θ₁ + θ₂ = 1 := by ext; simp [θ₁, θ₂]
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : (↑s : ℝ) ≤ (↑r : ℝ)
ht : 0 < s
hr : 0 < (↑r : ℝ)
θ₁ : ℝ≥0 := NNReal.mk ((↑s : ℝ) / (↑r : ℝ)) ⋯
θ₂ : ℝ≥0 := NNReal.mk (1 - (↑s : ℝ) / (↑r : ℝ)) ⋯
hθ : θ₁ + θ₂ = 1
a : (↑(r * θ₁ + 0 * θ₂) : ℝ) = (↑s : ℝ)
⊢ r * θ₁ + 0 * θ₂ = s

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : (↑s : ℝ) ≤ (↑r : ℝ)
ht : 0 < s
hr : 0 < (↑r : ℝ)
θ₁ : ℝ≥0 := NNReal.mk ((↑s : ℝ) / (↑r : ℝ)) ⋯
θ₂ : ℝ≥0 := NNReal.mk (1 - (↑s : ℝ) / (↑r : ℝ)) ⋯
hθ : θ₁ + θ₂ = 1
⊢ (↑(r * θ₁ + 0 * θ₂) : ℝ) = (↑s : ℝ)

Tactic:
simp [θ₁, mul_div_cancel₀ _ hr.ne']

Premises used: mul_div_cancel₀, LT.lt.ne'
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : (↑s : ℝ) ≤ (↑r : ℝ)
ht : 0 < s
hr : 0 < (↑r : ℝ)
θ₁ : ℝ≥0 := NNReal.mk ((↑s : ℝ) / (↑r : ℝ)) ⋯
θ₂ : ℝ≥0 := NNReal.mk (1 - (↑s : ℝ) / (↑r : ℝ)) ⋯
hθ : θ₁ + θ₂ = 1
⊢ r * θ₁ + 0 * θ₂ = s

Tactic:
have hθt : r * θ₁ + 0 * θ₂ = s := by ext; simp [θ₁, mul_div_cancel₀ _ hr.ne']
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : (↑s : ℝ) ≤ (↑r : ℝ)
ht : 0 < s
hr : 0 < (↑r : ℝ)
θ₁ : ℝ≥0 := NNReal.mk ((↑s : ℝ) / (↑r : ℝ)) ⋯
θ₂ : ℝ≥0 := NNReal.mk (1 - (↑s : ℝ) / (↑r : ℝ)) ⋯
hθ : θ₁ + θ₂ = 1
hθt : r * θ₁ + 0 * θ₂ = s
simp : C * D ^ ((↑r : ℝ) - (↑s : ℝ)) = C * D ^ ((↑r : ℝ) * (↑θ₂ : ℝ))
⊢ C * D ^ ((↑r : ℝ) - (↑s : ℝ)) = C ^ (↑θ₁ : ℝ) * (C * D ^ (↑r : ℝ)) ^ (↑θ₂ : ℝ)

Tactic:
simp (discharger := positivity) only [NNReal.mul_rpow, ← mul_assoc,
      ← NNReal.rpow_add_of_nonneg, ← NNReal.rpow_mul, ← NNReal.coe_add, hθ, NNReal.coe_one,
      NNReal.rpow_one]

Premises used: NNReal.coe_add, mul_assoc, NNReal.rpow_mul, NNReal.coe_one, NNReal.rpow_add_of_nonneg, NNReal.rpow_one, NNReal.mul_rpow
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : (↑s : ℝ) ≤ (↑r : ℝ)
ht : 0 < s
hr : 0 < (↑r : ℝ)
θ₁ : ℝ≥0 := NNReal.mk ((↑s : ℝ) / (↑r : ℝ)) ⋯
θ₂ : ℝ≥0 := NNReal.mk (1 - (↑s : ℝ) / (↑r : ℝ)) ⋯
hθ : θ₁ + θ₂ = 1
hθt : r * θ₁ + 0 * θ₂ = s
e_a : (↑r : ℝ) - (↑s : ℝ) = (↑r : ℝ) * (↑θ₂ : ℝ)
⊢ C * D ^ ((↑r : ℝ) - (↑s : ℝ)) = C * D ^ ((↑r : ℝ) * (↑θ₂ : ℝ))

Tactic:
congr
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : (↑s : ℝ) ≤ (↑r : ℝ)
ht : 0 < s
hr : 0 < (↑r : ℝ)
θ₁ : ℝ≥0 := NNReal.mk ((↑s : ℝ) / (↑r : ℝ)) ⋯
θ₂ : ℝ≥0 := NNReal.mk (1 - (↑s : ℝ) / (↑r : ℝ)) ⋯
hθ : θ₁ + θ₂ = 1
hθt : r * θ₁ + 0 * θ₂ = s
⊢ (↑r : ℝ) - (↑s : ℝ) = (↑r : ℝ) * (↑θ₂ : ℝ)

Tactic:
simp [mul_sub, θ₂, mul_div_cancel₀ _ hr.ne']

Premises used: mul_sub, mul_div_cancel₀, LT.lt.ne'