awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ C * D ^ ((↑r : ℝ) - (↑s : ℝ)) = C ^ (↑θ₁ : ℝ) * (C * D ^ (↑r : ℝ)) ^ (↑θ₂ : ℝ)

Tactic:
have hθC : C * D ^ (r - s : ℝ) = C ^ (θ₁ : ℝ) * (C * D ^ (r : ℝ)) ^ (θ₂ : ℝ) := by
    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]
    congr
    simp [mul_sub, θ₂, 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
hθC : C * D ^ ((↑r : ℝ) - (↑s : ℝ)) = C ^ (↑θ₁ : ℝ) * (C * D ^ (↑r : ℝ)) ^ (↑θ₂ : ℝ)
inr : HolderOnWith (C ^ (↑θ₁ : ℝ) * (C * D ^ (↑r : ℝ)) ^ (↑θ₂ : ℝ)) (r * θ₁ + 0 * θ₂) f A
⊢ HolderOnWith (C * D ^ ((↑r : ℝ) - (↑s : ℝ))) s f A

Tactic:
rw [hθC, ← hθt]
-- 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
hθC : C * D ^ ((↑r : ℝ) - (↑s : ℝ)) = C ^ (↑θ₁ : ℝ) * (C * D ^ (↑r : ℝ)) ^ (↑θ₂ : ℝ)
⊢ HolderOnWith (C ^ (↑θ₁ : ℝ) * (C * D ^ (↑r : ℝ)) ^ (↑θ₂ : ℝ)) (r * θ₁ + 0 * θ₂) f A

Tactic:
hf.interpolate (hf.holderOnWith_zero_of_bounded hA) hθ

Premises used: HolderOnWith.interpolate, 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
hr : 0 < (↑r : ℝ)
θ₁ : ℝ≥0 := NNReal.mk ((↑s : ℝ) / (↑r : ℝ)) ⋯
θ₂ : ℝ≥0 := NNReal.mk (1 - (↑s : ℝ) / (↑r : ℝ)) ⋯
hθ : θ₁ + θ₂ = 1
hθt : r * θ₁ + 0 * θ₂ = s
hθC : C * D ^ ((↑r : ℝ) - (↑s : ℝ)) = C ^ (↑θ₁ : ℝ) * (C * D ^ (↑r : ℝ)) ^ (↑θ₂ : ℝ)
⊢ HolderOnWith (C ^ (↑θ₁ : ℝ) * (C * D ^ (↑r : ℝ)) ^ (↑θ₂ : ℝ)) (r * θ₁ + 0 * θ₂) f A

Tactic:
exact hf.interpolate (hf.holderOnWith_zero_of_bounded hA) hθ

Premises used: HolderOnWith.interpolate, 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₁ C₂ : ℝ≥0
A : Set X
hf : HolderOnWith C₁ r f A
hC : C₁ ≤ C₂
x : X
hx : x ∈ A
y : X
hy : y ∈ A
grw : edist (f x) (f y) ≤ (↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)
⊢ edist (f x) (f y) ≤ (↑C₂ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)

Tactic:
grw [← hC]
-- 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₂ : ℝ≥0
A : Set X
hf : HolderOnWith C₁ r f A
hC : C₁ ≤ C₂
x : X
hx : x ∈ A
y : X
hy : y ∈ A
⊢ edist (f x) (f y) ≤ (↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)

Tactic:
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₂ : ℝ≥0
A : Set X
hf : HolderOnWith C₁ r f A
hC : C₁ ≤ C₂
x : X
hx : x ∈ A
y : X
hy : y ∈ A
⊢ edist (f x) (f y) ≤ (↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)

Tactic:
exact 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 s t₁ t₂ : ℝ≥0
A : Set X
hf₁ : HolderOnWith C r f A
hf₂ : HolderOnWith C s f A
ht : t₁ + t₂ = 1
⊢ HolderOnWith (C ^ (↑t₁ : ℝ) * C ^ (↑t₂ : ℝ)) (r * t₁ + s * t₂) f A

Tactic:
hf₁.interpolate hf₂ ht

Premises used: HolderOnWith.interpolate
-- 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 s t₁ t₂ : ℝ≥0
A : Set X
hf₁ : HolderOnWith C r f A
hf₂ : HolderOnWith C s f A
ht : t₁ + t₂ = 1
h : C = C ^ (↑t₁ : ℝ) * C ^ (↑t₂ : ℝ)
⊢ HolderOnWith C (r * t₁ + s * t₂) f A

Tactic:
convert! hf₁.interpolate hf₂ ht

Premises used: HolderOnWith.interpolate
-- 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 s t₁ t₂ : ℝ≥0
A : Set X
hf₁ : HolderOnWith C r f A
hf₂ : HolderOnWith C s f A
ht : t₁ + t₂ = 1
⊢ C = C ^ (↑t₁ : ℝ) * C ^ (↑t₂ : ℝ)

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

Premises used: NNReal.coe_add, NNReal.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
f : X → Y
C : ℝ≥0
A : Set X
r : ℝ≥0
hr : Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} r
s : ℝ≥0
hs : Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} s
_ :
  ∀ ⦃a b : ℝ≥0⦄,
    0 ≤ a → 0 ≤ b → a + b = 1 → Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} (a • r + b • s)
⊢ ∀ ⦃a b : ℝ≥0⦄,
    0 ≤ a → 0 ≤ b → a + b = 1 → Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} (a • r + b • s)

Tactic:
_
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
f : X → Y
C : ℝ≥0
A : Set X
r : ℝ≥0
hr : Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} r
s : ℝ≥0
hs : Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} s
a : ℝ≥0
_ :
  ∀ ⦃b : ℝ≥0⦄,
    0 ≤ a → 0 ≤ b → a + b = 1 → Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} (a • r + b • s)
⊢ ∀ ⦃b : ℝ≥0⦄,
    0 ≤ a → 0 ≤ b → a + b = 1 → Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} (a • r + b • s)

Tactic:
_
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
f : X → Y
C : ℝ≥0
A : Set X
r : ℝ≥0
hr : Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} r
s : ℝ≥0
hs : Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} s
a b : ℝ≥0
_ : 0 ≤ a → 0 ≤ b → a + b = 1 → Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} (a • r + b • s)
⊢ 0 ≤ a → 0 ≤ b → a + b = 1 → Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} (a • r + b • s)

Tactic:
_
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
f : X → Y
C : ℝ≥0
A : Set X
r : ℝ≥0
hr : Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} r
s : ℝ≥0
hs : Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} s
a b : ℝ≥0
h : 0 ≤ a
_ : 0 ≤ b → a + b = 1 → Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} (a • r + b • s)
⊢ 0 ≤ b → a + b = 1 → Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} (a • r + b • s)

Tactic:
_
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
f : X → Y
C : ℝ≥0
A : Set X
r : ℝ≥0
hr : Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} r
s : ℝ≥0
hs : Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} s
a b : ℝ≥0
h : 0 ≤ a
h_1 : 0 ≤ b
ht : a + b = 1
rw : Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} (r * a + s * b)
⊢ Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} (a • r + b • s)

Tactic:
rw [smul_eq_mul, smul_eq_mul, ← mul_comm r, ← mul_comm s]

Premises used: mul_comm, smul_eq_mul
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
f : X → Y
C : ℝ≥0
A : Set X
r : ℝ≥0
hr : Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} r
s : ℝ≥0
hs : Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} s
a b : ℝ≥0
h : 0 ≤ a
h_1 : 0 ≤ b
ht : a + b = 1
⊢ Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} (r * a + s * b)

Tactic:
hr.interpolate_const hs ht

Premises used: Set.Mem, setOf, HolderOnWith.interpolate_const, HolderOnWith
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
f : X → Y
C : ℝ≥0
A : Set X
r : ℝ≥0
hr : Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} r
s : ℝ≥0
hs : Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} s
a b : ℝ≥0
h : 0 ≤ a
h_1 : 0 ≤ b
ht : a + b = 1
⊢ Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} (r * a + s * b)

Tactic:
exact hr.interpolate_const hs ht

Premises used: HolderOnWith.interpolate_const
-- 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 : ℝ≥0
A : Set X
hf₁ : HolderOnWith C₁ r f A
hf₂ : HolderOnWith C₂ s f A
hrt : r ≤ t
hts : t ≤ s
⊢ HolderOnWith (max C₁ C₂) r f A

Tactic:
replace hf₁ := hf₁.mono_const (le_max_left C₁ C₂)
-- 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 : ℝ≥0
A : Set X
hf₂ : HolderOnWith C₂ s f A
hrt : r ≤ t
hts : t ≤ s
hf₁ : HolderOnWith (max C₁ C₂) r f A
⊢ HolderOnWith (max C₁ C₂) s f A

Tactic:
replace hf₂ := hf₂.mono_const (le_max_right C₁ C₂)
-- 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 : ℝ≥0
A : Set X
hrt : r ≤ t
hts : t ≤ s
hf₁ : HolderOnWith (max C₁ C₂) r f A
hf₂ : HolderOnWith (max C₁ C₂) s f A
⊢ HolderOnWith (max C₁ C₂) t f A

Tactic:
convex_setOf_holderOnWith f (max C₁ C₂) A |>.segment_subset hf₁ hf₂
    (NNReal.Icc_subset_segment ⟨hrt, hts⟩)

Premises used: Set.Mem, setOf, Max.max, And.intro, HolderOnWith, convex_setOf_holderOnWith, Convex.segment_subset, NNReal.Icc_subset_segment
-- 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 : ℝ≥0
A : Set X
hrt : r ≤ t
hts : t ≤ s
hf₁ : HolderOnWith (max C₁ C₂) r f A
hf₂ : HolderOnWith (max C₁ C₂) s f A
⊢ HolderOnWith (max C₁ C₂) t f A

Tactic:
exact convex_setOf_holderOnWith f (max C₁ C₂) A |>.segment_subset hf₁ hf₂
    (NNReal.Icc_subset_segment ⟨hrt, hts⟩)

Premises used: Max.max, And.intro, convex_setOf_holderOnWith, Convex.segment_subset, NNReal.Icc_subset_segment
-- 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
⊢ HolderWith C r (s.restrict (π := fun (a : X) ↦ Y) f) ↔ HolderOnWith C r f s

Tactic:
simp [HolderWith, HolderOnWith]

Premises used: HolderWith, HolderOnWith
-- 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
h : HolderWith C r f
x y : X
⊢ edist (f x) (f y) ≤ (↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ)

Tactic:
h x y
-- 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
h : HolderWith C r f
x y : X
d : ℝ≥0∞
hd : edist x y ≤ d
⊢ edist (f x) (f y) ≤ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)

Tactic:
(h.holderOnWith univ).edist_le_of_le trivial trivial hd

Premises used: trivial, HolderWith.holderOnWith, Set.univ, 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
hg : HolderWith Cg rg g
Cf rf : ℝ≥0
f : X → Y
hf : HolderWith Cf rf f
⊢ HolderWith (Cg * Cf ^ (↑rg : ℝ)) (rg * rf) (g ∘ f)

Tactic:
(hg.holderOnWith univ).comp_holderWith hf fun _ => trivial

Premises used: trivial, HolderWith.holderOnWith, Set.univ, HolderOnWith.comp_holderWith
-- 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
hg : HolderWith Cg rg g
Cf rf : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith Cf rf f s
⊢ HolderOnWith (Cg * Cf ^ (↑rg : ℝ)) (rg * rf) (g ∘ f) s

Tactic:
(hg.holderOnWith univ).comp hf fun _ _ => trivial

Premises used: HolderOnWith.comp, trivial, HolderWith.holderOnWith, Set.univ
-- 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
hf : HolderWith C r f
h0 : 0 < r
⊢ UniformContinuous f

Tactic:
uniformContinuousOn_univ.mp <| (hf.holderOnWith univ).uniformContinuousOn h0

Premises used: HolderWith.holderOnWith, Set.univ, uniformContinuousOn_univ, HolderOnWith.uniformContinuousOn, 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
hf : HolderWith C r f
h0 : 0 < r
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    f

Tactic:
(hf.uniformContinuous h0).continuous

Premises used: UniformContinuous.continuous, HolderWith.uniformContinuous
-- 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
hf : HolderWith C r f
s : Set X
⊢ ediam (f '' s) ≤ (↑C : ℝ≥0∞) * ediam s ^ (↑r : ℝ)

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

Premises used: Iff.mpr, HolderWith.edist_le_of_le, Metric.edist_le_ediam_of_mem, Metric.ediam_image_le_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
y : Y
x₁ x₂ : X
⊢ edist (Function.const X y x₁) (Function.const X y x₂) ≤ (↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
simp only [Function.const_apply, edist_self, zero_le]

Premises used: Function.const_apply, zero_le, PseudoEMetricSpace.edist_self
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
inst_2 : Zero Y
⊢ HolderWith.{u_1, u_2} (X := X) (Y := Y) C r 0

Tactic:
.const

Premises used: HolderWith.const
-- 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
inst_2 : IsEmpty X
⊢ HolderWith C r f

Tactic:
isEmptyElim

Premises used: isEmptyElim, HolderWith
-- 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
C' : ℝ≥0
hf : HolderWith C r f
h : C ≤ C'
x₁ x₂ : X
⊢ (↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ) ≤ (↑C' : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
gcongr
-- 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
hf₁ : HolderWith C₁ r f
hf₂ : HolderWith C₂ s f
ht : t₁ + t₂ = 1
⊢ HolderWith (C₁ ^ (↑t₁ : ℝ) * C₂ ^ (↑t₂ : ℝ)) (r * t₁ + s * t₂) f

Tactic:
holderOnWith_univ.1 ((holderOnWith_univ.2 hf₁).interpolate (holderOnWith_univ.2 hf₂) ht)

Premises used: Iff.mpr, holderOnWith_univ, HolderOnWith.interpolate, Iff.mp
-- 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
h : ∀ (x y : X), edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderWith C r f
⊢ HolderWith (C * D ^ (↑r : ℝ)) 0 f

Tactic:
holderOnWith_univ.1 ((holderOnWith_univ.2 hf).holderOnWith_zero_of_bounded (fun x _ y _ ↦ h x y))

Premises used: Iff.mpr, holderOnWith_univ, HolderOnWith.holderOnWith_zero_of_bounded, Iff.mp
-- 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
h : ∀ (x y : X), edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderWith C r f
hsr : s ≤ r
⊢ HolderWith (C * D ^ ((↑r : ℝ) - (↑s : ℝ))) s f

Tactic:
holderOnWith_univ.1 ((holderOnWith_univ.2 hf).of_le (fun x _ y _ ↦ h x y) hsr)

Premises used: Iff.mpr, holderOnWith_univ, Iff.mp, HolderOnWith.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 s t₁ t₂ : ℝ≥0
hf₁ : HolderWith C r f
hf₂ : HolderWith C s f
ht : t₁ + t₂ = 1
⊢ HolderWith C (r * t₁ + s * t₂) f

Tactic:
holderOnWith_univ.1 ((holderOnWith_univ.2 hf₁).interpolate_const (holderOnWith_univ.2 hf₂) ht)

Premises used: Iff.mpr, holderOnWith_univ, HolderOnWith.interpolate_const, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
f : X → Y
C : ℝ≥0
simp_rw : Convex ℝ≥0 (E := ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f univ}
⊢ Convex ℝ≥0 (E := ℝ≥0) {r : ℝ≥0 | HolderWith C r f}

Tactic:
simp_rw [← holderOnWith_univ]

Premises used: holderOnWith_univ
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
f : X → Y
C : ℝ≥0
⊢ Convex ℝ≥0 (E := ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f univ}

Tactic:
convex_setOf_holderOnWith f C _

Premises used: convex_setOf_holderOnWith
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
f : X → Y
C : ℝ≥0
⊢ Convex ℝ≥0 (E := ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f univ}

Tactic:
exact convex_setOf_holderOnWith f C _

Premises used: convex_setOf_holderOnWith
-- 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 : ℝ≥0
hf₁ : HolderWith C₁ r f
hf₂ : HolderWith C₂ s f
hrt : r ≤ t
hts : t ≤ s
⊢ HolderWith (max C₁ C₂) t f

Tactic:
holderOnWith_univ.1 ((holderOnWith_univ.2 hf₁).of_le_of_le (holderOnWith_univ.2 hf₂) hrt hts)

Premises used: Iff.mpr, holderOnWith_univ, HolderOnWith.of_le_of_le, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
rw : edist (f x) (f y) ≤ (↑C : ℝ≥0∞) * (↑d : ℝ≥0∞) ^ (↑r : ℝ)
⊢ nndist (f x) (f y) ≤ C * d ^ (↑r : ℝ)

Tactic:
rw [← ENNReal.coe_le_coe, ← edist_nndist, ENNReal.coe_mul,
    ENNReal.coe_rpow_of_nonneg _ r.coe_nonneg]

Premises used: ENNReal.coe_rpow_of_nonneg, ENNReal.coe_le_coe, ENNReal.coe_mul, NNReal.coe_nonneg, edist_nndist
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
apply : edist x y ≤ (↑d : ℝ≥0∞)
⊢ edist (f x) (f y) ≤ (↑C : ℝ≥0∞) * (↑d : ℝ≥0∞) ^ (↑r : ℝ)

Tactic:
apply hf.edist_le_of_le hx hy

Premises used: HolderOnWith.edist_le_of_le
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
rwa : (↑(nndist x y) : ℝ≥0∞) ≤ (↑d : ℝ≥0∞)
rwa₁ rwa₂ rwa₃ rwa₄ : nndist x y ≤ d
⊢ edist x y ≤ (↑d : ℝ≥0∞)

Tactic:
rwa [edist_nndist, ENNReal.coe_le_coe]

Premises used: ENNReal.coe_le_coe, edist_nndist
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
⊢ nndist (f x) (f y) ≤ C * nndist x y ^ (↑r : ℝ)

Tactic:
hf.nndist_le_of_le hx hy le_rfl

Premises used: le_rfl, HolderOnWith.nndist_le_of_le
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ
hd : dist x y ≤ d
⊢ 0 ≤ d

Tactic:
dist_nonneg.trans hd

Premises used: dist_nonneg, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ
hd : dist x y ≤ d
lift : ∀ (d : ℝ≥0) (hd : dist x y ≤ (↑d : ℝ)), dist (f x) (f y) ≤ (↑C : ℝ) * (↑d : ℝ) ^ (↑r : ℝ)
⊢ dist (f x) (f y) ≤ (↑C : ℝ) * d ^ (↑r : ℝ)

Tactic:
lift d to ℝ≥0 using dist_nonneg.trans hd

Premises used: dist_nonneg, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : dist x y ≤ (↑d : ℝ)
rw : ∀ (hd : (↑(nndist x y) : ℝ) ≤ (↑d : ℝ)), (↑(nndist (f x) (f y)) : ℝ) ≤ (↑C : ℝ) * (↑d : ℝ) ^ (↑r : ℝ)
⊢ dist (f x) (f y) ≤ (↑C : ℝ) * (↑d : ℝ) ^ (↑r : ℝ)

Tactic:
rw [dist_nndist] at hd ⊢

Premises used: dist_nndist
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : (↑(nndist x y) : ℝ) ≤ (↑d : ℝ)
⊢ nndist x y ≤ d

Tactic:
norm_cast at hd ⊢
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
⊢ nndist (f x) (f y) ≤ C * d ^ (↑r : ℝ)

Tactic:
hf.nndist_le_of_le hx hy hd

Premises used: HolderOnWith.nndist_le_of_le
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
⊢ nndist (f x) (f y) ≤ C * d ^ (↑r : ℝ)

Tactic:
exact hf.nndist_le_of_le hx hy hd

Premises used: HolderOnWith.nndist_le_of_le
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
⊢ dist (f x) (f y) ≤ (↑C : ℝ) * dist x y ^ (↑r : ℝ)

Tactic:
hf.dist_le_of_le hx hy le_rfl

Premises used: le_rfl, HolderOnWith.dist_le_of_le
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ≥0
hd : nndist x y ≤ d
⊢ nndist (f x) (f y) ≤ C * d ^ (↑r : ℝ)

Tactic:
(hf.holderOnWith univ).nndist_le_of_le (mem_univ x) (mem_univ y) hd

Premises used: HolderWith.holderOnWith, HolderOnWith.nndist_le_of_le, Set.univ, Set.mem_univ
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
⊢ nndist (f x) (f y) ≤ C * nndist x y ^ (↑r : ℝ)

Tactic:
hf.nndist_le_of_le le_rfl

Premises used: le_rfl, HolderWith.nndist_le_of_le