awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
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∞)
⊢ HolderWith (C * ‖a‖₊) r (a • f) ↔ HolderWith C r f
have 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∞)
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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
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∞)
⊢ HolderWith (C * ‖a‖₊) r (a • f) ↔ HolderWith C r f
have 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∞)
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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
have refine : ∀ (h : 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⟩⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (hypothesis)
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 < ∞
⊢ MemHolder r f
have h₁ : ∃ (i : ℝ≥0) (_ : HolderWith i r f), (↑i : ℝ≥0∞) < ∞
Tactic: simp_rw [eHolderNorm, iInf_lt_top] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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∞) < ∞
⊢ MemHolder r f
have let : ∀ (C : ℝ≥0) (hC : HolderWith C r f), (↑C : ℝ≥0∞) < ∞ → MemHolder r f
Tactic: let ⟨C, hC, _⟩ := h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
have rw : eHolderNorm r f = ∞ ↔ ¬eHolderNorm r f ≠ ∞
Tactic: rw [← eHolderNorm_ne_top, not_not]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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 ≠ ∞
⊢ eHolderNorm r f = ∞ ↔ ¬MemHolder r f
have rw₁ : eHolderNorm r f = ∞ ↔ eHolderNorm r f = ∞
Tactic: rw [← eHolderNorm_ne_top, not_not]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ eHolderNorm r (Function.const X c) = 0
have rw : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ℝ≥0) (_ : HolderWith i r (Function.const X c)), (↑i : ℝ≥0∞) < b
Tactic: rw [eHolderNorm, ← ENNReal.bot_eq_zero, iInf₂_eq_bot]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
have rw : (↑(nnHolderNorm r (Function.const X c)) : ℝ≥0∞) ≤ eHolderNorm r (Function.const X c)
Tactic: rw [← nonpos_iff_eq_zero, ← ENNReal.coe_le_coe, ENNReal.coe_zero, ← eHolderNorm_const X r c]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
hX : IsEmpty X
⊢ eHolderNorm r f = 0
have rw : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ℝ≥0) (_ : HolderWith i r f), (↑i : ℝ≥0∞) < b
Tactic: rw [eHolderNorm, ← ENNReal.bot_eq_zero, iInf₂_eq_bot]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
⊢ MemHolder s f
have obtain : ∀ (C : ℝ≥0) (hf : HolderWith C r f), MemHolder s f
Tactic: obtain ⟨C, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
⊢ MemHolder s f
have obtain : ∀ (C' : ℝ≥0) (hC' : ∀ (a b : X), edist a b ≤ (↑C' : ℝ≥0∞)), MemHolder s f
Tactic: obtain ⟨C', hC'⟩ := Metric.boundedSpace_iff_edist.1 hX
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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∞)
⊢ MemHolder s f
have obtain : ∀ (C : ℝ≥0) (hX : ∀ (x y : X), edist x y ≤ (↑C : ℝ≥0∞)), MemHolder s f
Tactic: obtain ⟨C, hX⟩ := hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (hypothesis)
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 ⋯
⊢ MemHolder s f
have this₁ : BoundedSpace X
Tactic: have := Metric.boundedSpace_iff_edist.2 ⟨C, hX⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
⊢ ∃ (C : ℝ≥0), HolderOnWith C s f A
have 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)
Tactic: simp_rw [← HolderWith.restrict_iff] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (hypothesis)
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)
⊢ ∃ (C : ℝ≥0), HolderWith C s (A.restrict (π := fun (a : X) ↦ Y) f)
have this : BoundedSpace.{u_3} (↑A : Type u_3)
Tactic: have : BoundedSpace A := boundedSpace_val_set_iff.2 hA
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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∞)
⊢ ∃ (C : ℝ≥0), HolderOnWith C s f A
have 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)
Tactic: simp_rw [← HolderWith.restrict_iff] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (hypothesis)
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 ⋯
⊢ ∃ (C : ℝ≥0), HolderWith C s (A.restrict (π := fun (a : X) ↦ Y) f)
have this₁ : 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⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
⊢ ∃ (C : ℝ≥0), HolderOnWith C s f A
have obtain : ∀ (C₁ : ℝ≥0) (hf₁ : HolderOnWith C₁ r f A), ∃ (C : ℝ≥0), HolderOnWith C s f A
Tactic: obtain ⟨C₁, hf₁⟩ := hf₁
Cleared hypotheses: hf₁
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
⊢ ∃ (C : ℝ≥0), HolderOnWith C s f A
have obtain : ∀ (C₂ : ℝ≥0) (hf₂ : HolderOnWith C₂ t f A), ∃ (C : ℝ≥0), HolderOnWith C s f A
Tactic: obtain ⟨C₂, hf₂⟩ := hf₂
Cleared hypotheses: hf₂
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
⊢ MemHolder s f
have 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
Tactic: simp_rw [MemHolder, ← holderOnWith_univ] at *
Cleared hypotheses: hf₁, hf₂
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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₂
have mp : eHolderNorm r f = 0 → ∀ (x₁ x₂ : X), f x₁ = f x₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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₂
⊢ eHolderNorm r f = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂
have mpr : (∀ (x₁ x₂ : X), f x₁ = f x₂) → eHolderNorm r f = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
⊢ f x₁ = f x₂
have pos : ∀ (hx : x₁ = x₂), f x₁ = f x₂
Tactic: by_cases hx : x₁ = x₂
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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₂
⊢ f x₁ = f x₂
have neg : ∀ (hx : ¬x₁ = x₂), f x₁ = f x₂
Tactic: by_cases hx : x₁ = x₂
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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₂
⊢ f x₁ = f x₂
have pos : f x₂ = f x₂
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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₂
⊢ f x₁ = f x₂
have neg : ∀ (h : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ℝ≥0) (_ : HolderWith i r f), (↑i : ℝ≥0∞) < b) (x₁ x₂ : X) (hx : ¬x₁ = x₂),
  f x₁ = f x₂
Tactic: rw [eHolderNorm, ← ENNReal.bot_eq_zero, iInf₂_eq_bot] at h
Cleared hypotheses: h, x₁, x₂, hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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₂
⊢ f x₁ = f x₂
have neg : edist (f x₁) (f x₂) ≤ 0
Tactic: rw [← edist_eq_zero, ← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
have neg : ∀ (b : ℝ≥0∞) (hb : 0 < b), edist (f x₁) (f x₂) < b
Tactic: refine le_of_forall_gt fun b hb => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
⊢ edist (f x₁) (f x₂) < b
have neg : ∀ (C : ℝ≥0) (hC : HolderWith C r f) (hC' : (↑C : ℝ≥0∞) < b / edist x₁ x₂ ^ (↑r : ℝ)), 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)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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₂
⊢ eHolderNorm r f = 0
have mpr : ∀ (hX : IsEmpty X), eHolderNorm r f = 0
Tactic: rcases isEmpty_or_nonempty X with hX | hX
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
⊢ eHolderNorm r f = 0
have mpr₁ : ∀ (hX : Nonempty X), eHolderNorm r f = 0
Tactic: rcases isEmpty_or_nonempty X with hX | hX
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
⊢ eHolderNorm r f = 0
have mpr : eHolderNorm r f = eHolderNorm r (Function.const X (f hX.some))
Tactic: rw [← eHolderNorm_const X r (f hX.some)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
⊢ eHolderNorm r f = eHolderNorm r (Function.const X (f hX.some))
have mpr : f = Function.const X (f hX.some)
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
⊢ edist (f x₁) (f x₂) ≤ (↑(nnHolderNorm r f) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
have pos : ∀ (hx : x₁ = x₂), edist (f x₁) (f x₂) ≤ (↑(nnHolderNorm r f) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
Tactic: by_cases hx : x₁ = x₂
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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 : ℝ)
⊢ edist (f x₁) (f x₂) ≤ (↑(nnHolderNorm r f) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
have neg : ∀ (hx : ¬x₁ = x₂), edist (f x₁) (f x₂) ≤ (↑(nnHolderNorm r f) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
Tactic: by_cases hx : x₁ = x₂
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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 : ℝ)
have neg : edist (f x₁) (f x₂) ≤ (⨅ (C : ℝ≥0), ⨅ (_ : HolderWith C r f), (↑C : ℝ≥0∞)) * edist x₁ x₂ ^ (↑r : ℝ)
Tactic: rw [nnHolderNorm, eHolderNorm, coe_toNNReal]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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 : ℝ)
⊢ edist (f x₁) (f x₂) ≤ (↑(nnHolderNorm r f) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
have neg₁ : Ne (α := ℝ≥0∞) (⨅ (C : ℝ≥0), ⨅ (_ : HolderWith C r f), (↑C : ℝ≥0∞)) ∞
Tactic: rw [nnHolderNorm, eHolderNorm, coe_toNNReal]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (hypothesis)
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₂) ≤ (⨅ (C : ℝ≥0), ⨅ (_ : HolderWith C r f), (↑C : ℝ≥0∞)) * edist x₁ x₂ ^ (↑r : ℝ)
have h₁ : 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)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (hypothesis)
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 (f x₁) (f x₂) ≤ (⨅ (C : ℝ≥0), ⨅ (_ : HolderWith C r f), (↑C : ℝ≥0∞)) * edist x₁ x₂ ^ (↑r : ℝ)
have h₂ : edist x₁ x₂ ^ (↑r : ℝ) ≠ ∞
Tactic: have h₂ : edist x₁ x₂ ^ (r : ℝ) ≠ ∞ := by
    simp [(edist_lt_top x₁ x₂).ne]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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₂) ≤ (⨅ (C : ℝ≥0), ⨅ (_ : HolderWith C r f), (↑C : ℝ≥0∞)) * edist x₁ x₂ ^ (↑r : ℝ)
have neg : edist (f x₁) (f x₂) / edist x₁ x₂ ^ (↑r : ℝ) ≤ ⨅ (C : ℝ≥0), ⨅ (_ : HolderWith C r f), (↑C : ℝ≥0∞)
Tactic: rw [← ENNReal.div_le_iff h₁ h₂]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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∞)
have neg : ∀ (C : ℝ≥0) (hC : HolderWith C r f), edist (f x₁) (f x₂) / edist x₁ x₂ ^ (↑r : ℝ) ≤ (↑C : ℝ≥0∞)
Tactic: refine le_iInf₂ fun C hC => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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₂) / edist x₁ x₂ ^ (↑r : ℝ) ≤ (↑C : ℝ≥0∞)
have neg : edist (f x₁) (f x₂) ≤ (↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
Tactic: rw [ENNReal.div_le_iff h₁ h₂]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
⊢ (↑(nnHolderNorm r f) : ℝ≥0∞) = eHolderNorm r f
have rw : eHolderNorm r f ≠ ∞
Tactic: rw [nnHolderNorm, coe_toNNReal]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
⊢ nnHolderNorm r f ≤ C
have rw : eHolderNorm r f ≤ (↑C : ℝ≥0∞)
Tactic: rw [← ENNReal.coe_le_coe, hf.memHolder.coe_nnHolderNorm_eq_eHolderNorm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
⊢ nnHolderNorm r f = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂
have rw : (↑(nnHolderNorm r f) : ℝ≥0∞) = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂
Tactic: rw [← ENNReal.coe_eq_zero, hf.coe_nnHolderNorm_eq_eHolderNorm, eHolderNorm_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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₂
⊢ nnHolderNorm r f = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂
have rw₁ : eHolderNorm r f = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂
Tactic: rw [← ENNReal.coe_eq_zero, hf.coe_nnHolderNorm_eq_eHolderNorm, eHolderNorm_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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₂
⊢ nnHolderNorm r f = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂
have rw₂ : (∀ (x₁ x₂ : X), f x₁ = f x₂) ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂
Tactic: rw [← ENNReal.coe_eq_zero, hf.coe_nnHolderNorm_eq_eHolderNorm, eHolderNorm_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (goal)
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
have refine : MemHolder r (c • f) → ∀ (h : ℝ≥0) (hh : HolderWith h r (c • f)), HolderWith (h * ‖c‖₊⁻¹) r f
Tactic: refine ⟨fun ⟨h, hh⟩ => ⟨h * ‖c‖₊⁻¹, ?_⟩, .smul⟩