awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : PseudoMetricSpace (↑A : Type u_1) := PseudoEMetricSpace.toPseudoMetricSpace ⋯
this : BoundedSpace.{u_1} (↑A : Type u_1)
⊢ ∃ (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:
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_1 : PseudoMetricSpace (↑A : Type u_1) := PseudoEMetricSpace.toPseudoMetricSpace ⋯
this : BoundedSpace.{u_1} (↑A : Type u_1)
⊢ ∃ (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
s t : ℝ≥0
A : Set X
hf₁ : ∃ (C : ℝ≥0), HolderOnWith C r f A
hf₂ : ∃ (C : ℝ≥0), HolderOnWith C t f A
hrs : r ≤ s
hst : s ≤ t
obtain : ∀ (C₁ : ℝ≥0) (hf₁ : HolderOnWith C₁ r f A), ∃ (C : ℝ≥0), HolderOnWith C s f A
⊢ ∃ (C : ℝ≥0), HolderOnWith C s f A

Tactic:
obtain ⟨C₁, hf₁⟩ := hf₁
-- 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 t : ℝ≥0
A : Set X
hf₂ : ∃ (C : ℝ≥0), HolderOnWith C t f A
hrs : r ≤ s
hst : s ≤ t
C₁ : ℝ≥0
hf₁ : HolderOnWith C₁ r f A
obtain : ∀ (C₂ : ℝ≥0) (hf₂ : HolderOnWith C₂ t f A), ∃ (C : ℝ≥0), HolderOnWith C s f A
⊢ ∃ (C : ℝ≥0), HolderOnWith C s f A

Tactic:
obtain ⟨C₂, hf₂⟩ := hf₂
-- 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 t : ℝ≥0
A : Set X
hrs : r ≤ s
hst : s ≤ t
C₁ : ℝ≥0
hf₁ : HolderOnWith C₁ r f A
C₂ : ℝ≥0
hf₂ : HolderOnWith C₂ t f A
⊢ ∃ (C : ℝ≥0), HolderOnWith C s f A

Tactic:
⟨max C₁ C₂, hf₁.of_le_of_le hf₂ hrs hst⟩

Premises used: HolderOnWith.of_le_of_le, Max.max, 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
s t : ℝ≥0
A : Set X
hrs : r ≤ s
hst : s ≤ t
C₁ : ℝ≥0
hf₁ : HolderOnWith C₁ r f A
C₂ : ℝ≥0
hf₂ : HolderOnWith C₂ t f A
⊢ ∃ (C : ℝ≥0), HolderOnWith C s f A

Tactic:
exact ⟨max C₁ C₂, hf₁.of_le_of_le hf₂ hrs hst⟩
-- 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 t : ℝ≥0
hf₁ : MemHolder r f
hf₂ : MemHolder t f
hrs : r ≤ s
hst : s ≤ t
simp_rw :
  ∀ (hf₁ : ∃ (C : ℝ≥0), HolderOnWith C r f univ) (hf₂ : ∃ (C : ℝ≥0), HolderOnWith C t f univ),
    ∃ (C : ℝ≥0), HolderOnWith C s f univ
⊢ MemHolder s f

Tactic:
simp_rw [MemHolder, ← holderOnWith_univ] at *

Premises used: holderOnWith_univ, MemHolder
-- 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 t : ℝ≥0
hrs : r ≤ s
hst : s ≤ t
hf₁ : ∃ (C : ℝ≥0), HolderOnWith C r f univ
hf₂ : ∃ (C : ℝ≥0), HolderOnWith C t f univ
⊢ ∃ (C : ℝ≥0), HolderOnWith C s f univ

Tactic:
HolderOnWith.exists_holderOnWith_of_le_of_le hf₁ hf₂ hrs hst

Premises used: HolderOnWith.exists_holderOnWith_of_le_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 t : ℝ≥0
hrs : r ≤ s
hst : s ≤ t
hf₁ : ∃ (C : ℝ≥0), HolderOnWith C r f univ
hf₂ : ∃ (C : ℝ≥0), HolderOnWith C t f univ
⊢ ∃ (C : ℝ≥0), HolderOnWith C s f univ

Tactic:
exact HolderOnWith.exists_holderOnWith_of_le_of_le hf₁ hf₂ hrs hst

Premises used: HolderOnWith.exists_holderOnWith_of_le_of_le
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
mp : eHolderNorm r f = 0 → ∀ (x₁ x₂ : X), f x₁ = f x₂
mpr : (∀ (x₁ x₂ : X), f x₁ = f x₂) → eHolderNorm r f = 0
⊢ eHolderNorm r f = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ eHolderNorm r f = 0 → ∀ (x₁ x₂ : X), f x₁ = f x₂

Tactic:
fun h x₁ x₂ => ?_
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
mp : ∀ (h : eHolderNorm r f = 0) (x₁ x₂ : X), f x₁ = f x₂
⊢ eHolderNorm r f = 0 → ∀ (x₁ x₂ : X), f x₁ = f x₂

Tactic:
refine fun h x₁ x₂ => ?_
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : eHolderNorm r f = 0
x₁ x₂ : X
pos : ∀ (hx : x₁ = x₂), f x₁ = f x₂
neg : ∀ (hx : ¬x₁ = x₂), f x₁ = f x₂
⊢ f x₁ = f x₂

Tactic:
by_cases hx : x₁ = x₂
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : eHolderNorm r f = 0
x₁ x₂ : X
hx : x₁ = x₂
pos pos₁ : f x₂ = f x₂
⊢ f x₁ = f x₂

Tactic:
rw [hx]
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : eHolderNorm r f = 0
x₁ x₂ : X
hx : ¬x₁ = x₂
neg :
  ∀ (h : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ℝ≥0) (_ : HolderWith i r f), (↑i : ℝ≥0∞) < b) (x₁ x₂ : X) (hx : ¬x₁ = x₂),
    f x₁ = f x₂
⊢ f x₁ = f x₂

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

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 : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ℝ≥0) (_ : HolderWith i r f), (↑i : ℝ≥0∞) < b
x₁ x₂ : X
hx : ¬x₁ = x₂
neg : edist (f x₁) (f x₂) ≤ 0
⊢ f x₁ = f x₂

Tactic:
rw [← edist_eq_zero, ← nonpos_iff_eq_zero]

Premises used: edist_eq_zero, nonpos_iff_eq_zero
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ℝ≥0) (_ : HolderWith i r f), (↑i : ℝ≥0∞) < b
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ edist (f x₁) (f x₂) ≤ 0

Tactic:
le_of_forall_gt fun b hb => ?_

Premises used: le_of_forall_gt
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ℝ≥0) (_ : HolderWith i r f), (↑i : ℝ≥0∞) < b
x₁ x₂ : X
hx : ¬x₁ = x₂
neg : ∀ (b : ℝ≥0∞) (hb : 0 < b), edist (f x₁) (f x₂) < b
⊢ edist (f x₁) (f x₂) ≤ 0

Tactic:
refine le_of_forall_gt fun b hb => ?_

Premises used: le_of_forall_gt
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ℝ≥0) (_ : HolderWith i r f), (↑i : ℝ≥0∞) < b
x₁ x₂ : X
hx : ¬x₁ = x₂
b : ℝ≥0∞
hb : 0 < b
neg : ∀ (C : ℝ≥0) (hC : HolderWith C r f) (hC' : (↑C : ℝ≥0∞) < b / edist x₁ x₂ ^ (↑r : ℝ)), edist (f x₁) (f x₂) < b
⊢ edist (f x₁) (f x₂) < b

Tactic:
obtain ⟨C, hC, hC'⟩ := h (b / edist x₁ x₂ ^ (r : ℝ))
        (ENNReal.div_pos hb.ne.symm (ENNReal.rpow_lt_top_of_nonneg zero_le_coe
          (edist_lt_top x₁ x₂).ne).ne)

Premises used: HDiv.hDiv, Ne.symm, HPow.hPow, edist_lt_top, ENNReal.div_pos, EDist.edist, NNReal.zero_le_coe, ENNReal.rpow_lt_top_of_nonneg, NNReal.toReal, LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ℝ≥0) (_ : HolderWith i r f), (↑i : ℝ≥0∞) < b
x₁ x₂ : X
hx : ¬x₁ = x₂
b : ℝ≥0∞
hb : 0 < b
C : ℝ≥0
hC : HolderWith C r f
hC' : (↑C : ℝ≥0∞) < b / edist x₁ x₂ ^ (↑r : ℝ)
⊢ edist (f x₁) (f x₂) < b

Tactic:
lt_of_le_of_lt (hC x₁ x₂) <| ENNReal.mul_lt_of_lt_div hC'

Premises used: lt_of_le_of_lt, ENNReal.mul_lt_of_lt_div
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ℝ≥0) (_ : HolderWith i r f), (↑i : ℝ≥0∞) < b
x₁ x₂ : X
hx : ¬x₁ = x₂
b : ℝ≥0∞
hb : 0 < b
C : ℝ≥0
hC : HolderWith C r f
hC' : (↑C : ℝ≥0∞) < b / edist x₁ x₂ ^ (↑r : ℝ)
⊢ edist (f x₁) (f x₂) < b

Tactic:
exact lt_of_le_of_lt (hC x₁ x₂) <| ENNReal.mul_lt_of_lt_div hC'

Premises used: lt_of_le_of_lt, ENNReal.mul_lt_of_lt_div
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
mpr : ∀ (hX : IsEmpty X), eHolderNorm r f = 0
mpr₁ : ∀ (hX : Nonempty X), eHolderNorm r f = 0
⊢ eHolderNorm r f = 0

Tactic:
rcases isEmpty_or_nonempty X with hX | hX

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
hX : IsEmpty X
⊢ eHolderNorm r f = 0

Tactic:
eHolderNorm_of_isEmpty

Premises used: eHolderNorm_of_isEmpty
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
hX : IsEmpty X
⊢ eHolderNorm r f = 0

Tactic:
exact eHolderNorm_of_isEmpty

Premises used: eHolderNorm_of_isEmpty
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
hX : Nonempty X
mpr : eHolderNorm r f = eHolderNorm r (Function.const X (f hX.some))
⊢ eHolderNorm r f = 0

Tactic:
rw [← eHolderNorm_const X r (f hX.some)]

Premises used: Nonempty.some, eHolderNorm_const
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
hX : Nonempty X
mpr : f = Function.const X (f hX.some)
⊢ eHolderNorm r f = eHolderNorm r (Function.const X (f hX.some))

Tactic:
congr
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
hX : Nonempty X
⊢ f = Function.const X (f hX.some)

Tactic:
simp [funext_iff, h _ hX.some]

Premises used: funext_iff, Nonempty.some
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
pos : ∀ (hx : x₁ = x₂), edist (f x₁) (f x₂) ≤ (↑(nnHolderNorm r f) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
neg : ∀ (hx : ¬x₁ = x₂), edist (f x₁) (f x₂) ≤ (↑(nnHolderNorm r f) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
⊢ edist (f x₁) (f x₂) ≤ (↑(nnHolderNorm r f) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
by_cases hx : x₁ = x₂
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : x₁ = x₂
⊢ edist (f x₁) (f x₂) ≤ (↑(nnHolderNorm r f) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
simp only [hx, edist_self, zero_le]

Premises used: zero_le, PseudoEMetricSpace.edist_self
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
neg : edist (f x₁) (f x₂) ≤ (⨅ (C : ℝ≥0), ⨅ (_ : HolderWith C r f), (↑C : ℝ≥0∞)) * edist x₁ x₂ ^ (↑r : ℝ)
neg₁ : Ne (α := ℝ≥0∞) (⨅ (C : ℝ≥0), ⨅ (_ : HolderWith C r f), (↑C : ℝ≥0∞)) ∞
⊢ edist (f x₁) (f x₂) ≤ (↑(nnHolderNorm r f) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
rw [nnHolderNorm, eHolderNorm, coe_toNNReal]

Premises used: ENNReal.coe_toNNReal, eHolderNorm, nnHolderNorm
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ Ne (α := ℝ≥0∞) (⨅ (C : ℝ≥0), ⨅ (_ : HolderWith C r f), (↑C : ℝ≥0∞)) ∞

Tactic:
hf.eHolderNorm_lt_top.ne

Premises used: eHolderNorm, MemHolder.eHolderNorm_lt_top, LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ Ne (α := ℝ≥0∞) (⨅ (C : ℝ≥0), ⨅ (_ : HolderWith C r f), (↑C : ℝ≥0∞)) ∞

Tactic:
exact hf.eHolderNorm_lt_top.ne

Premises used: MemHolder.eHolderNorm_lt_top, LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ Ne (α := ℝ≥0∞) (⨅ (C : ℝ≥0), ⨅ (_ : HolderWith C r f), (↑C : ℝ≥0∞)) ∞

Tactic:
on_goal 2 => exact hf.eHolderNorm_lt_top.ne

Premises used: MemHolder.eHolderNorm_lt_top, LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ edist x₁ x₂ ^ (↑r : ℝ) ≠ 0

Tactic:
have h₁ : edist x₁ x₂ ^ (r : ℝ) ≠ 0 :=
    (Ne.symm <| ne_of_lt <| ENNReal.rpow_pos (edist_pos.2 hx) (edist_lt_top x₁ x₂).ne)
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ (↑r : ℝ) ≠ 0
⊢ edist x₁ x₂ ^ (↑r : ℝ) ≠ ∞

Tactic:
simp [(edist_lt_top x₁ x₂).ne]

Premises used: edist_lt_top, LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ (↑r : ℝ) ≠ 0
⊢ edist x₁ x₂ ^ (↑r : ℝ) ≠ ∞

Tactic:
have h₂ : edist x₁ x₂ ^ (r : ℝ) ≠ ∞ := by
    simp [(edist_lt_top x₁ x₂).ne]
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ (↑r : ℝ) ≠ 0
h₂ : edist x₁ x₂ ^ (↑r : ℝ) ≠ ∞
neg : edist (f x₁) (f x₂) / edist x₁ x₂ ^ (↑r : ℝ) ≤ ⨅ (C : ℝ≥0), ⨅ (_ : HolderWith C r f), (↑C : ℝ≥0∞)
⊢ edist (f x₁) (f x₂) ≤ (⨅ (C : ℝ≥0), ⨅ (_ : HolderWith C r f), (↑C : ℝ≥0∞)) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
rw [← ENNReal.div_le_iff h₁ h₂]

Premises used: ENNReal.div_le_iff
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ (↑r : ℝ) ≠ 0
h₂ : edist x₁ x₂ ^ (↑r : ℝ) ≠ ∞
⊢ edist (f x₁) (f x₂) / edist x₁ x₂ ^ (↑r : ℝ) ≤ ⨅ (C : ℝ≥0), ⨅ (_ : HolderWith C r f), (↑C : ℝ≥0∞)

Tactic:
le_iInf₂ fun C hC => ?_

Premises used: le_iInf₂
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ (↑r : ℝ) ≠ 0
h₂ : edist x₁ x₂ ^ (↑r : ℝ) ≠ ∞
neg : ∀ (C : ℝ≥0) (hC : HolderWith C r f), edist (f x₁) (f x₂) / edist x₁ x₂ ^ (↑r : ℝ) ≤ (↑C : ℝ≥0∞)
⊢ edist (f x₁) (f x₂) / edist x₁ x₂ ^ (↑r : ℝ) ≤ ⨅ (C : ℝ≥0), ⨅ (_ : HolderWith C r f), (↑C : ℝ≥0∞)

Tactic:
refine le_iInf₂ fun C hC => ?_

Premises used: le_iInf₂
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ (↑r : ℝ) ≠ 0
h₂ : edist x₁ x₂ ^ (↑r : ℝ) ≠ ∞
C : ℝ≥0
hC : HolderWith C r f
neg : edist (f x₁) (f x₂) ≤ (↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
⊢ edist (f x₁) (f x₂) / edist x₁ x₂ ^ (↑r : ℝ) ≤ (↑C : ℝ≥0∞)

Tactic:
rw [ENNReal.div_le_iff h₁ h₂]

Premises used: ENNReal.div_le_iff
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ (↑r : ℝ) ≠ 0
h₂ : edist x₁ x₂ ^ (↑r : ℝ) ≠ ∞
C : ℝ≥0
hC : HolderWith C r f
⊢ edist (f x₁) (f x₂) ≤ (↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
hC x₁ x₂
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ (↑r : ℝ) ≠ 0
h₂ : edist x₁ x₂ ^ (↑r : ℝ) ≠ ∞
C : ℝ≥0
hC : HolderWith C r f
⊢ edist (f x₁) (f x₂) ≤ (↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
exact hC x₁ x₂
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ MemHolder r f ↔ HolderWith (nnHolderNorm r f) r f

Tactic:
⟨MemHolder.holderWith, HolderWith.memHolder⟩

Premises used: MemHolder.holderWith, HolderWith.memHolder, Iff.intro
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
rw : eHolderNorm r f ≠ ∞
⊢ (↑(nnHolderNorm r f) : ℝ≥0∞) = eHolderNorm r f

Tactic:
rw [nnHolderNorm, coe_toNNReal]

Premises used: ENNReal.coe_toNNReal, nnHolderNorm
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
⊢ eHolderNorm r f ≠ ∞

Tactic:
ne_of_lt <| lt_of_le_of_lt hf.holderWith.eHolderNorm_le <| coe_lt_top

Premises used: MemHolder.holderWith, lt_of_le_of_lt, HolderWith.eHolderNorm_le, ne_of_lt, ENNReal.coe_lt_top
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
⊢ eHolderNorm r f ≠ ∞

Tactic:
exact ne_of_lt <| lt_of_le_of_lt hf.holderWith.eHolderNorm_le <| coe_lt_top

Premises used: MemHolder.holderWith, lt_of_le_of_lt, HolderWith.eHolderNorm_le, ne_of_lt, ENNReal.coe_lt_top
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
rw : eHolderNorm r f ≤ (↑C : ℝ≥0∞)
⊢ nnHolderNorm r f ≤ C

Tactic:
rw [← ENNReal.coe_le_coe, hf.memHolder.coe_nnHolderNorm_eq_eHolderNorm]

Premises used: MemHolder.coe_nnHolderNorm_eq_eHolderNorm, ENNReal.coe_le_coe, HolderWith.memHolder
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
⊢ eHolderNorm r f ≤ (↑C : ℝ≥0∞)

Tactic:
hf.eHolderNorm_le

Premises used: HolderWith.eHolderNorm_le
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
⊢ eHolderNorm r f ≤ (↑C : ℝ≥0∞)

Tactic:
exact hf.eHolderNorm_le

Premises used: HolderWith.eHolderNorm_le
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r s : ℝ≥0
Z : Type u_3
inst_2 : MetricSpace Z
f : Z → X
g : X → Y
hf : MemHolder r f
hg : MemHolder s g
⊢ MemHolder (s * r) (g ∘ f)

Tactic:
(hg.holderWith.comp hf.holderWith).memHolder

Premises used: MemHolder.holderWith, HolderWith.memHolder, HolderWith.comp
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
rw : (↑(nnHolderNorm r f) : ℝ≥0∞) = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂
rw₁ : eHolderNorm r f = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂
rw₂ rw₃ : (∀ (x₁ x₂ : X), f x₁ = f x₂) ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂
⊢ nnHolderNorm r f = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂

Tactic:
rw [← ENNReal.coe_eq_zero, hf.coe_nnHolderNorm_eq_eHolderNorm, eHolderNorm_eq_zero]

Premises used: eHolderNorm_eq_zero, MemHolder.coe_nnHolderNorm_eq_eHolderNorm, ENNReal.coe_eq_zero
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
hf : MemHolder r f
hg : MemHolder r g
⊢ MemHolder r (f + g)

Tactic:
(hf.holderWith.add hg.holderWith).memHolder

Premises used: MemHolder.holderWith, HolderWith.add, HolderWith.memHolder
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
𝕜 : Type u_3
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 Y
inst_4 : IsBoundedSMul 𝕜 Y
c : 𝕜
hf : MemHolder r f
⊢ MemHolder r (c • f)

Tactic:
(hf.holderWith.smul c).memHolder

Premises used: MemHolder.holderWith, HolderWith.memHolder, HolderWith.smul
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
𝕜 : Type u_3
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 Y
inst_4 : NormSMulClass 𝕜 Y
c : 𝕜
hc : ‖c‖₊ ≠ 0
⊢ MemHolder r (c • f) ↔ MemHolder r f

Tactic:
⟨fun ⟨h, hh⟩ => ⟨h * ‖c‖₊⁻¹, ?_⟩, .smul⟩

Premises used: _private.0.MemHolder.smul_iff.match_1, HMul.hMul, MemHolder, NNNorm.nnnorm, MemHolder.smul, Inv.inv, Iff.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
𝕜 : Type u_3
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 Y
inst_4 : NormSMulClass 𝕜 Y
c : 𝕜
hc : ‖c‖₊ ≠ 0
refine : MemHolder r (c • f) → ∀ (h : ℝ≥0) (hh : HolderWith h r (c • f)), HolderWith (h * ‖c‖₊⁻¹) r f
⊢ MemHolder r (c • f) ↔ MemHolder r f

Tactic:
refine ⟨fun ⟨h, hh⟩ => ⟨h * ‖c‖₊⁻¹, ?_⟩, .smul⟩
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
𝕜 : Type u_3
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 Y
inst_4 : NormSMulClass 𝕜 Y
c : 𝕜
hc : ‖c‖₊ ≠ 0
h_1 : MemHolder r (c • f)
h : ℝ≥0
hh : HolderWith h r (c • f)
rw : HolderWith h r (c • f)
⊢ HolderWith (h * ‖c‖₊⁻¹) r f

Tactic:
rw [← HolderWith.smul_iff _ hc, inv_mul_cancel_right₀ hc]

Premises used: inv_mul_cancel_right₀, HolderWith.smul_iff
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
𝕜 : Type u_3
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 Y
inst_4 : NormSMulClass 𝕜 Y
c : 𝕜
hc : ‖c‖₊ ≠ 0
h_1 : MemHolder r (c • f)
h : ℝ≥0
hh : HolderWith h r (c • f)
⊢ HolderWith h r (c • f)

Tactic:
hh
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
𝕜 : Type u_3
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 Y
inst_4 : NormSMulClass 𝕜 Y
c : 𝕜
hc : ‖c‖₊ ≠ 0
h_1 : MemHolder r (c • f)
h : ℝ≥0
hh : HolderWith h r (c • f)
⊢ HolderWith h r (c • f)

Tactic:
exact hh
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
inst_2 : NormedSpace ℝ Y
n : ℕ
hf : MemHolder r f
⊢ MemHolder r (n • f)

Tactic:
simp [← Nat.cast_smul_eq_nsmul (R := ℝ), hf.smul]

Premises used: Real, MemHolder.smul, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
hf : MemHolder r f
hg : MemHolder r g
⊢ nnHolderNorm r (f + g) ≤ nnHolderNorm r f + nnHolderNorm r g

Tactic:
(hf.add hg).holderWith.nnholderNorm_le.trans (hf.holderWith.add hg.holderWith).nnholderNorm_le

Premises used: MemHolder.holderWith, HolderWith.add, MemHolder.add, HolderWith.nnholderNorm_le, LE.le.trans