awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ
hd : dist x y ≤ d
⊢ dist (f x) (f y) ≤ (↑C : ℝ) * d ^ (↑r : ℝ)

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

Premises used: HolderWith.holderOnWith, Set.univ, Set.mem_univ, 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
⊢ dist (f x) (f y) ≤ (↑C : ℝ) * dist x y ^ (↑r : ℝ)

Tactic:
hf.dist_le_of_le le_rfl

Premises used: le_rfl, HolderWith.dist_le_of_le
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : MetricSpace Y
r : ℝ≥0
f : X → Y
⊢ HolderWith 0 r f ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂

Tactic:
⟨fun h x₁ x₂ => ?_, fun h x₁ x₂ => h x₁ x₂ ▸ ?_⟩

Premises used: Eq.rec, Iff.intro
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : MetricSpace Y
r : ℝ≥0
f : X → Y
refine_1 : ∀ (h : HolderWith 0 r f) (x₁ x₂ : X), f x₁ = f x₂
refine_2 : ∀ (h : ∀ (x₁ x₂ : X), f x₁ = f x₂) (x₁ x₂ : X), edist (f x₁) (f x₁) ≤ (↑0 : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
⊢ HolderWith 0 r f ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂

Tactic:
refine ⟨fun h x₁ x₂ => ?_, fun h x₁ x₂ => h x₁ x₂ ▸ ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : MetricSpace Y
r : ℝ≥0
f : X → Y
h : HolderWith 0 r f
x₁ x₂ : X
⊢ edist (f x₁) (f x₂) ≤ (↑0 : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
specialize h x₁ x₂
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : MetricSpace Y
r : ℝ≥0
f : X → Y
x₁ x₂ : X
h : edist (f x₁) (f x₂) ≤ (↑0 : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
⊢ f x₁ = f x₂

Tactic:
simp [ENNReal.coe_zero, zero_mul, nonpos_iff_eq_zero, edist_eq_zero] at h

Premises used: MulZeroClass.zero_mul, ENNReal.coe_zero, edist_eq_zero, nonpos_iff_eq_zero
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : MetricSpace Y
r : ℝ≥0
f : X → Y
x₁ x₂ : X
h : f x₁ = f x₂
⊢ f x₁ = f x₂

Tactic:
assumption
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : MetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
x₁ x₂ : X
⊢ edist (f x₁) (f x₁) ≤ (↑0 : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
simp only [edist_self, ENNReal.coe_zero, zero_mul, le_refl]

Premises used: le_refl, MulZeroClass.zero_mul, PseudoEMetricSpace.edist_self, ENNReal.coe_zero
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : SeminormedAddCommGroup Y
C C' r : ℝ≥0
f g : X → Y
hf : HolderWith C r f
hg : HolderWith C' r g
x₁ x₂ : X
simp : edist (f x₁ + g x₁) (f x₂ + g x₂) ≤ ((↑C : ℝ≥0∞) + (↑C' : ℝ≥0∞)) * edist x₁ x₂ ^ (↑r : ℝ)
⊢ edist ((f + g) x₁) ((f + g) x₂) ≤ (↑(C + C') : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
simp only [Pi.add_apply, ENNReal.coe_add]

Premises used: ENNReal.coe_add, Pi.add_apply
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : SeminormedAddCommGroup Y
C C' r : ℝ≥0
f g : X → Y
hf : HolderWith C r f
hg : HolderWith C' r g
x₁ x₂ : X
grw :
  (↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ) + (↑C' : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ) ≤
    ((↑C : ℝ≥0∞) + (↑C' : ℝ≥0∞)) * edist x₁ x₂ ^ (↑r : ℝ)
⊢ edist (f x₁ + g x₁) (f x₂ + g x₂) ≤ ((↑C : ℝ≥0∞) + (↑C' : ℝ≥0∞)) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
grw [edist_add_add_le, hf x₁ x₂, hg x₁ x₂]

Premises used: edist_add_add_le
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : SeminormedAddCommGroup Y
C C' r : ℝ≥0
f g : X → Y
hf : HolderWith C r f
hg : HolderWith C' r g
x₁ x₂ : X
rw rw₁ :
  (↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ) + (↑C' : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ) ≤
    (↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ) + (↑C' : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
⊢ (↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ) + (↑C' : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ) ≤
    ((↑C : ℝ≥0∞) + (↑C' : ℝ≥0∞)) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
rw [add_mul]

Premises used: add_mul
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : SeminormedAddCommGroup Y
C r : ℝ≥0
f : X → Y
α : Type u_4
inst_2 : SeminormedAddCommGroup α
inst_3 : SMulZeroClass α Y
inst_4 : IsBoundedSMul α Y
a : α
hf : HolderWith C r f
x₁ x₂ : X
⊢ edist ((a • f) x₁) ((a • f) x₂) ≤ (↑(C * ‖a‖₊) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
edist_smul_le _ _ _ |>.trans ?_

Premises used: LE.le.trans, edist_smul_le
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : SeminormedAddCommGroup Y
C r : ℝ≥0
f : X → Y
α : Type u_4
inst_2 : SeminormedAddCommGroup α
inst_3 : SMulZeroClass α Y
inst_4 : IsBoundedSMul α Y
a : α
hf : HolderWith C r f
x₁ x₂ : X
refine : ‖a‖₊ • edist (f x₁) (f x₂) ≤ (↑(C * ‖a‖₊) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
⊢ edist ((a • f) x₁) ((a • f) x₂) ≤ (↑(C * ‖a‖₊) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
refine edist_smul_le _ _ _ |>.trans ?_

Premises used: LE.le.trans, edist_smul_le
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : SeminormedAddCommGroup Y
C r : ℝ≥0
f : X → Y
α : Type u_4
inst_2 : SeminormedAddCommGroup α
inst_3 : SMulZeroClass α Y
inst_4 : IsBoundedSMul α Y
a : α
hf : HolderWith C r f
x₁ x₂ : X
rw : (↑‖a‖₊ : ℝ≥0∞) * edist (f x₁) (f x₂) ≤ (↑‖a‖₊ : ℝ≥0∞) * ((↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ))
⊢ ‖a‖₊ • edist (f x₁) (f x₂) ≤ (↑(C * ‖a‖₊) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
rw [ENNReal.coe_mul, ENNReal.smul_def, smul_eq_mul, mul_comm (C : ℝ≥0∞), mul_assoc]

Premises used: ENNReal.ofNNReal, ENNReal.smul_def, mul_assoc, ENNReal.coe_mul, mul_comm, smul_eq_mul
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : SeminormedAddCommGroup Y
C r : ℝ≥0
f : X → Y
α : Type u_4
inst_2 : SeminormedAddCommGroup α
inst_3 : SMulZeroClass α Y
inst_4 : IsBoundedSMul α Y
a : α
hf : HolderWith C r f
x₁ x₂ : X
bc : edist (f x₁) (f x₂) ≤ (↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
⊢ (↑‖a‖₊ : ℝ≥0∞) * edist (f x₁) (f x₂) ≤ (↑‖a‖₊ : ℝ≥0∞) * ((↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ))

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : SeminormedAddCommGroup Y
C r : ℝ≥0
f : X → Y
α : Type u_4
inst_2 : SeminormedAddCommGroup α
inst_3 : SMulZeroClass α Y
inst_4 : IsBoundedSMul α Y
a : α
hf : HolderWith C r f
x₁ x₂ : X
⊢ edist (f x₁) (f x₂) ≤ (↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
hf x₁ x₂
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : SeminormedAddCommGroup Y
C r : ℝ≥0
f : X → Y
α : Type u_4
inst_2 : SeminormedAddCommGroup α
inst_3 : SMulZeroClass α Y
inst_4 : IsBoundedSMul α Y
a : α
hf : HolderWith C r f
x₁ x₂ : X
⊢ edist (f x₁) (f x₂) ≤ (↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
exact hf x₁ x₂
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : SeminormedAddCommGroup Y
C r : ℝ≥0
f : X → Y
α : Type u_4
inst_2 : SeminormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
a : α
ha : ‖a‖₊ ≠ 0
simp_rw :
  (∀ (x y : X), edist ((a • f) x) ((a • f) y) ≤ (↑(C * ‖a‖₊) : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ↔
    ∀ (x y : X), edist (f x) (f y) ≤ (↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ)
simp_rw₁ :
  (∀ (x y : X), edist ((a • f) x) ((a • f) y) ≤ (↑C : ℝ≥0∞) * (↑‖a‖₊ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ↔
    ∀ (x y : X), edist (f x) (f y) ≤ (↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ)
simp_rw₂ :
  (∀ (x y : X), edist (a • f x) (a • f y) ≤ (↑C : ℝ≥0∞) * (↑‖a‖₊ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ↔
    ∀ (x y : X), edist (f x) (f y) ≤ (↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ)
simp_rw₃ :
  (∀ (x y : X), ‖a‖₊ • edist (f x) (f y) ≤ (↑C : ℝ≥0∞) * (↑‖a‖₊ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ↔
    ∀ (x y : X), edist (f x) (f y) ≤ (↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ)
simp_rw₄ :
  (∀ (x y : X), (↑‖a‖₊ : ℝ≥0∞) • edist (f x) (f y) ≤ (↑C : ℝ≥0∞) * (↑‖a‖₊ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ↔
    ∀ (x y : X), edist (f x) (f y) ≤ (↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ)
simp_rw₅ :
  (∀ (x y : X), (↑‖a‖₊ : ℝ≥0∞) * edist (f x) (f y) ≤ (↑C : ℝ≥0∞) * (↑‖a‖₊ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ↔
    ∀ (x y : X), edist (f x) (f y) ≤ (↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ)
simp_rw₆ :
  (∀ (x y : X), (↑‖a‖₊ : ℝ≥0∞) * edist (f x) (f y) ≤ (↑‖a‖₊ : ℝ≥0∞) * (↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ↔
    ∀ (x y : X), edist (f x) (f y) ≤ edist x y ^ (↑r : ℝ) * (↑C : ℝ≥0∞)
simp_rw₇ :
  (∀ (x y : X), (↑‖a‖₊ : ℝ≥0∞) * edist (f x) (f y) ≤ (↑‖a‖₊ : ℝ≥0∞) * ((↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ))) ↔
    ∀ (x y : X), edist (f x) (f y) ≤ edist x y ^ (↑r : ℝ) * (↑C : ℝ≥0∞)
simp_rw₈ :
  (∀ (x y : X), edist (f x) (f y) ≤ (↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ↔
    ∀ (x y : X), edist (f x) (f y) ≤ edist x y ^ (↑r : ℝ) * (↑C : ℝ≥0∞)
⊢ HolderWith (C * ‖a‖₊) r (a • f) ↔ HolderWith C r f

Tactic:
simp_rw [HolderWith, ENNReal.coe_mul, Pi.smul_apply, edist_smul₀, ENNReal.smul_def, smul_eq_mul,
    mul_comm (C : ℝ≥0∞), mul_assoc,
    ENNReal.mul_le_mul_iff_right (ENNReal.coe_ne_zero.mpr ha) ENNReal.coe_ne_top, mul_comm]

Premises used: Iff.mpr, ENNReal.ofNNReal, ENNReal.smul_def, mul_assoc, edist_smul₀, ENNReal.coe_ne_zero, ENNReal.coe_mul, ENNReal.mul_le_mul_iff_right, HolderWith, mul_comm, smul_eq_mul, ENNReal.coe_ne_top, Pi.smul_apply
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C : ℝ≥0
hf : HolderWith C r f
⊢ MemHolder r f

Tactic:
⟨C, hf⟩

Premises used: MemHolder, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ eHolderNorm r f < ∞ ↔ MemHolder r f

Tactic:
⟨fun h => ?_,
    fun hf => let ⟨C, hC⟩ := hf; iInf_lt_top.2 ⟨C, iInf_lt_top.2 ⟨hC, coe_lt_top⟩⟩⟩

Premises used: Iff.mpr, _private.0.eHolderNorm_lt_top.match_1, eHolderNorm, LT.lt, Iff.intro, Exists.intro, Top.top, iInf_lt_top, ENNReal.coe_lt_top
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
refine : ∀ (h : eHolderNorm r f < ∞), MemHolder r f
⊢ eHolderNorm r f < ∞ ↔ MemHolder r f

Tactic:
refine ⟨fun h => ?_,
    fun hf => let ⟨C, hC⟩ := hf; iInf_lt_top.2 ⟨C, iInf_lt_top.2 ⟨hC, coe_lt_top⟩⟩⟩
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
h : eHolderNorm r f < ∞
⊢ ∃ (i : ℝ≥0) (_ : HolderWith i r f), (↑i : ℝ≥0∞) < ∞

Tactic:
simp_rw [eHolderNorm, iInf_lt_top] at h

Premises used: eHolderNorm, iInf_lt_top
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∃ (i : ℝ≥0) (_ : HolderWith i r f), (↑i : ℝ≥0∞) < ∞
let : ∀ (C : ℝ≥0) (hC : HolderWith C r f), (↑C : ℝ≥0∞) < ∞ → MemHolder r f
⊢ MemHolder r f

Tactic:
let ⟨C, hC, _⟩ := h
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∃ (i : ℝ≥0) (_ : HolderWith i r f), (↑i : ℝ≥0∞) < ∞
C : ℝ≥0
hC : HolderWith C r f
h_1 : (↑C : ℝ≥0∞) < ∞
⊢ MemHolder r f

Tactic:
⟨C, hC⟩

Premises used: MemHolder, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∃ (i : ℝ≥0) (_ : HolderWith i r f), (↑i : ℝ≥0∞) < ∞
C : ℝ≥0
hC : HolderWith C r f
h_1 : (↑C : ℝ≥0∞) < ∞
⊢ MemHolder r f

Tactic:
exact ⟨C, hC⟩
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
rw : eHolderNorm r f = ∞ ↔ ¬eHolderNorm r f ≠ ∞
rw₁ rw₂ : eHolderNorm r f = ∞ ↔ eHolderNorm r f = ∞
⊢ eHolderNorm r f = ∞ ↔ ¬MemHolder r f

Tactic:
rw [← eHolderNorm_ne_top, not_not]

Premises used: Classical.not_not, eHolderNorm_ne_top
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ (↑(nnHolderNorm r f) : ℝ≥0∞) ≤ eHolderNorm r f

Tactic:
coe_toNNReal_le_self

Premises used: ENNReal.coe_toNNReal_le_self, nnHolderNorm
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
rw : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ℝ≥0) (_ : HolderWith i r (Function.const X c)), (↑i : ℝ≥0∞) < b
⊢ eHolderNorm r (Function.const X c) = 0

Tactic:
rw [eHolderNorm, ← ENNReal.bot_eq_zero, iInf₂_eq_bot]

Premises used: ENNReal.bot_eq_zero, eHolderNorm, iInf₂_eq_bot
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ℝ≥0) (_ : HolderWith i r (Function.const X c)), (↑i : ℝ≥0∞) < b

Tactic:
fun C' hC' => ⟨0, .const, hC'⟩

Premises used: Exists.intro, HolderWith.const, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ℝ≥0) (_ : HolderWith i r (Function.const X c)), (↑i : ℝ≥0∞) < b

Tactic:
exact fun C' hC' => ⟨0, .const, hC'⟩
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : Zero Y
r : ℝ≥0
⊢ eHolderNorm.{u_1, u_2} (X := X) (Y := Y) r 0 = 0

Tactic:
eHolderNorm_const X r 0

Premises used: eHolderNorm_const, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
rw : (↑(nnHolderNorm r (Function.const X c)) : ℝ≥0∞) ≤ eHolderNorm r (Function.const X c)
⊢ nnHolderNorm r (Function.const X c) = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← ENNReal.coe_le_coe, ENNReal.coe_zero, ← eHolderNorm_const X r c]

Premises used: ENNReal.coe_le_coe, eHolderNorm_const, ENNReal.coe_zero, nonpos_iff_eq_zero
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ (↑(nnHolderNorm r (Function.const X c)) : ℝ≥0∞) ≤ eHolderNorm r (Function.const X c)

Tactic:
coe_nnHolderNorm_le_eHolderNorm

Premises used: coe_nnHolderNorm_le_eHolderNorm
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ (↑(nnHolderNorm r (Function.const X c)) : ℝ≥0∞) ≤ eHolderNorm r (Function.const X c)

Tactic:
exact coe_nnHolderNorm_le_eHolderNorm

Premises used: coe_nnHolderNorm_le_eHolderNorm
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : Zero Y
r : ℝ≥0
⊢ nnHolderNorm.{u_1, u_2} (X := X) (Y := Y) r 0 = 0

Tactic:
nnHolderNorm_const X r 0

Premises used: nnHolderNorm_const, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
hX : IsEmpty X
rw : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ℝ≥0) (_ : HolderWith i r f), (↑i : ℝ≥0∞) < b
⊢ eHolderNorm r f = 0

Tactic:
rw [eHolderNorm, ← ENNReal.bot_eq_zero, iInf₂_eq_bot]

Premises used: ENNReal.bot_eq_zero, eHolderNorm, iInf₂_eq_bot
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
hX : IsEmpty X
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ℝ≥0) (_ : HolderWith i r f), (↑i : ℝ≥0∞) < b

Tactic:
fun ε hε => ⟨0, .of_isEmpty, hε⟩

Premises used: HolderWith.of_isEmpty, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
hX : IsEmpty X
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ℝ≥0) (_ : HolderWith i r f), (↑i : ℝ≥0∞) < b

Tactic:
exact fun ε hε => ⟨0, .of_isEmpty, hε⟩
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C : ℝ≥0
hf : HolderWith C r f
⊢ eHolderNorm r f ≤ (↑C : ℝ≥0∞)

Tactic:
iInf₂_le C hf

Premises used: iInf₂_le, eHolderNorm
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ MemHolder r (Function.const X c)

Tactic:
(HolderWith.const (C := 0)).memHolder

Premises used: HolderWith.memHolder, HolderWith.const
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ MemHolder.{u_1, u_2} (Y := Y) r fun (x : X) ↦ c

Tactic:
memHolder_const

Premises used: memHolder_const
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
inst_2 : Zero Y
⊢ MemHolder.{u_1, u_2} (X := X) (Y := Y) r 0

Tactic:
memHolder_const

Premises used: memHolder_const
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
Y : Type u_2
inst : PseudoEMetricSpace Y
r : ℝ≥0
X : Type u_3
inst_1 : PseudoMetricSpace X
hX : BoundedSpace X
f : X → Y
s : ℝ≥0
hf : MemHolder r f
hs : s ≤ r
obtain : ∀ (C : ℝ≥0) (hf : HolderWith C r f), MemHolder s f
⊢ MemHolder s f

Tactic:
obtain ⟨C, hf⟩ := hf
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
Y : Type u_2
inst : PseudoEMetricSpace Y
r : ℝ≥0
X : Type u_3
inst_1 : PseudoMetricSpace X
hX : BoundedSpace X
f : X → Y
s : ℝ≥0
hs : s ≤ r
C : ℝ≥0
hf : HolderWith C r f
obtain : ∀ (C' : ℝ≥0) (hC' : ∀ (a b : X), edist a b ≤ (↑C' : ℝ≥0∞)), MemHolder s f
⊢ MemHolder s f

Tactic:
obtain ⟨C', hC'⟩ := Metric.boundedSpace_iff_edist.1 hX

Premises used: Iff.mp, Metric.boundedSpace_iff_edist
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
Y : Type u_2
inst : PseudoEMetricSpace Y
r : ℝ≥0
X : Type u_3
inst_1 : PseudoMetricSpace X
hX : BoundedSpace X
f : X → Y
s : ℝ≥0
hs : s ≤ r
C : ℝ≥0
hf : HolderWith C r f
C' : ℝ≥0
hC' : ∀ (a b : X), edist a b ≤ (↑C' : ℝ≥0∞)
⊢ MemHolder s f

Tactic:
⟨C * C' ^ (r - s : ℝ),
    holderOnWith_univ.1 <| (holderOnWith_univ.2 hf).of_le (fun x _ y _ ↦ hC' x y) hs⟩

Premises used: Iff.mpr, holderOnWith_univ, HMul.hMul, MemHolder, HSub.hSub, HPow.hPow, Exists.intro, Iff.mp, HolderOnWith.of_le, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
Y : Type u_2
inst : PseudoEMetricSpace Y
r : ℝ≥0
X : Type u_3
inst_1 : PseudoMetricSpace X
hX : BoundedSpace X
f : X → Y
s : ℝ≥0
hs : s ≤ r
C : ℝ≥0
hf : HolderWith C r f
C' : ℝ≥0
hC' : ∀ (a b : X), edist a b ≤ (↑C' : ℝ≥0∞)
⊢ MemHolder s f

Tactic:
exact ⟨C * C' ^ (r - s : ℝ),
    holderOnWith_univ.1 <| (holderOnWith_univ.2 hf).of_le (fun x _ y _ ↦ hC' x y) hs⟩
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
s : ℝ≥0
hf : MemHolder r f
hs : s ≤ r
hX : ∃ (C : ℝ≥0), ∀ (x y : X), edist x y ≤ (↑C : ℝ≥0∞)
obtain : ∀ (C : ℝ≥0) (hX : ∀ (x y : X), edist x y ≤ (↑C : ℝ≥0∞)), MemHolder s f
⊢ MemHolder s f

Tactic:
obtain ⟨C, hX⟩ := hX
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
s : ℝ≥0
hf : MemHolder r f
hs : s ≤ r
C : ℝ≥0
hX : ∀ (x y : X), edist x y ≤ (↑C : ℝ≥0∞)
this : PseudoMetricSpace X := PseudoEMetricSpace.toPseudoMetricSpace ⋯
⊢ BoundedSpace X

Tactic:
have := Metric.boundedSpace_iff_edist.2 ⟨C, hX⟩
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
s : ℝ≥0
hf : MemHolder r f
hs : s ≤ r
C : ℝ≥0
hX : ∀ (x y : X), edist x y ≤ (↑C : ℝ≥0∞)
this_1 : PseudoMetricSpace X := PseudoEMetricSpace.toPseudoMetricSpace ⋯
this : BoundedSpace X
⊢ MemHolder s f

Tactic:
hf.of_le hs

Premises used: MemHolder.of_le
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
s : ℝ≥0
hf : MemHolder r f
hs : s ≤ r
C : ℝ≥0
hX : ∀ (x y : X), edist x y ≤ (↑C : ℝ≥0∞)
this_1 : PseudoMetricSpace X := PseudoEMetricSpace.toPseudoMetricSpace ⋯
this : BoundedSpace X
⊢ MemHolder s f

Tactic:
exact hf.of_le hs

Premises used: MemHolder.of_le
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
Y : Type u_2
inst : PseudoEMetricSpace Y
r : ℝ≥0
X : Type u_3
inst_1 : PseudoMetricSpace X
f : X → Y
s : ℝ≥0
A : Set X
hf : ∃ (C : ℝ≥0), HolderOnWith C r f A
hs : s ≤ r
hA : Bornology.IsBounded A
simp_rw :
  ∀ (hf : ∃ (C : ℝ≥0), HolderWith C r (A.restrict (π := fun (a : X) ↦ Y) f)),
    ∃ (C : ℝ≥0), HolderWith C s (A.restrict (π := fun (a : X) ↦ Y) f)
⊢ ∃ (C : ℝ≥0), HolderOnWith C s f A

Tactic:
simp_rw [← HolderWith.restrict_iff] at *

Premises used: HolderWith.restrict_iff
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
Y : Type u_2
inst : PseudoEMetricSpace Y
r : ℝ≥0
X : Type u_3
inst_1 : PseudoMetricSpace X
f : X → Y
s : ℝ≥0
A : Set X
hs : s ≤ r
hA : Bornology.IsBounded A
hf : ∃ (C : ℝ≥0), HolderWith C r (A.restrict (π := fun (a : X) ↦ Y) f)
⊢ BoundedSpace.{u_3} (↑A : Type u_3)

Tactic:
have : BoundedSpace A := boundedSpace_val_set_iff.2 hA
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
Y : Type u_2
inst : PseudoEMetricSpace Y
r : ℝ≥0
X : Type u_3
inst_1 : PseudoMetricSpace X
f : X → Y
s : ℝ≥0
A : Set X
hs : s ≤ r
hA : Bornology.IsBounded A
hf : ∃ (C : ℝ≥0), HolderWith C r (A.restrict (π := fun (a : X) ↦ Y) f)
this : BoundedSpace.{u_3} (↑A : Type u_3)
⊢ ∃ (C : ℝ≥0), HolderWith C s (A.restrict (π := fun (a : X) ↦ Y) f)

Tactic:
MemHolder.of_le hf hs

Premises used: MemHolder, MemHolder.of_le
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
Y : Type u_2
inst : PseudoEMetricSpace Y
r : ℝ≥0
X : Type u_3
inst_1 : PseudoMetricSpace X
f : X → Y
s : ℝ≥0
A : Set X
hs : s ≤ r
hA : Bornology.IsBounded A
hf : ∃ (C : ℝ≥0), HolderWith C r (A.restrict (π := fun (a : X) ↦ Y) f)
this : BoundedSpace.{u_3} (↑A : Type u_3)
⊢ ∃ (C : ℝ≥0), HolderWith C s (A.restrict (π := fun (a : X) ↦ Y) f)

Tactic:
exact MemHolder.of_le hf hs

Premises used: MemHolder.of_le
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
D s : ℝ≥0
A : Set X
hf : ∃ (C : ℝ≥0), HolderOnWith C r f A
hs : s ≤ r
hA : ∀ ⦃x : X⦄, x ∈ A → ∀ ⦃y : X⦄, y ∈ A → edist x y ≤ (↑D : ℝ≥0∞)
simp_rw :
  ∀ (hf : ∃ (C : ℝ≥0), HolderWith C r (A.restrict (π := fun (a : X) ↦ Y) f)),
    ∃ (C : ℝ≥0), HolderWith C s (A.restrict (π := fun (a : X) ↦ Y) f)
⊢ ∃ (C : ℝ≥0), HolderOnWith C s f A

Tactic:
simp_rw [← HolderWith.restrict_iff] at *

Premises used: HolderWith.restrict_iff
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
D s : ℝ≥0
A : Set X
hs : s ≤ r
hA : ∀ ⦃x : X⦄, x ∈ A → ∀ ⦃y : X⦄, y ∈ A → edist x y ≤ (↑D : ℝ≥0∞)
hf : ∃ (C : ℝ≥0), HolderWith C r (A.restrict (π := fun (a : X) ↦ Y) f)
this : PseudoMetricSpace (↑A : Type u_1) := PseudoEMetricSpace.toPseudoMetricSpace ⋯
⊢ BoundedSpace.{u_1} (↑A : Type u_1)

Tactic:
have : BoundedSpace A := Metric.boundedSpace_iff_edist.2 ⟨D, fun x y ↦ hA x.2 y.2⟩