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 : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : (↑s : ℝ) ≤ (↑r : ℝ)
ht : 0 < s
hr : 0 < (↑r : ℝ)
θ₁ : ℝ≥0 := NNReal.mk ((↑s : ℝ) / (↑r : ℝ)) ⋯
θ₂ : ℝ≥0 := NNReal.mk (1 - (↑s : ℝ) / (↑r : ℝ)) ⋯
⊢ θ₁ + θ₂ = 1
have a : (↑(θ₁ + θ₂) : ℝ) = (↑1 : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (hypothesis)
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 : ℝ)) ⋯
⊢ HolderOnWith (C * D ^ ((↑r : ℝ) - (↑s : ℝ))) s f A
have hθ : θ₁ + θ₂ = 1
Tactic: have hθ : θ₁ + θ₂ = 1 := by ext; simp [θ₁, θ₂]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
hsr : (↑s : ℝ) ≤ (↑r : ℝ)
ht : 0 < s
hr : 0 < (↑r : ℝ)
θ₁ : ℝ≥0 := NNReal.mk ((↑s : ℝ) / (↑r : ℝ)) ⋯
θ₂ : ℝ≥0 := NNReal.mk (1 - (↑s : ℝ) / (↑r : ℝ)) ⋯
hθ : θ₁ + θ₂ = 1
⊢ r * θ₁ + 0 * θ₂ = s
have a : (↑(r * θ₁ + 0 * θ₂) : ℝ) = (↑s : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (hypothesis)
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
⊢ HolderOnWith (C * D ^ ((↑r : ℝ) - (↑s : ℝ))) s f A
have hθt : r * θ₁ + 0 * θ₂ = s
Tactic: have hθt : r * θ₁ + 0 * θ₂ = s := by ext; simp [θ₁, mul_div_cancel₀ _ hr.ne']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
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 : ℝ)) ^ (↑θ₂ : ℝ)
have simp : C * D ^ ((↑r : ℝ) - (↑s : ℝ)) = C * D ^ ((↑r : ℝ) * (↑θ₂ : ℝ))
Tactic: simp (discharger := positivity) only [NNReal.mul_rpow, ← mul_assoc,
      ← NNReal.rpow_add_of_nonneg, ← NNReal.rpow_mul, ← NNReal.coe_add, hθ, NNReal.coe_one,
      NNReal.rpow_one]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
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 * D ^ ((↑r : ℝ) * (↑θ₂ : ℝ))
have e_a : (↑r : ℝ) - (↑s : ℝ) = (↑r : ℝ) * (↑θ₂ : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (hypothesis)
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
⊢ HolderOnWith (C * D ^ ((↑r : ℝ) - (↑s : ℝ))) s f A
have hθC : 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']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
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 * D ^ ((↑r : ℝ) - (↑s : ℝ))) s f A
have inr : HolderOnWith (C ^ (↑θ₁ : ℝ) * (C * D ^ (↑r : ℝ)) ^ (↑θ₂ : ℝ)) (r * θ₁ + 0 * θ₂) f A
Tactic: rw [hθC, ← hθt]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
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 : ℝ)
have grw : edist (f x) (f y) ≤ (↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)
Tactic: grw [← hC]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
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 (r * t₁ + s * t₂) f A
have h : C = C ^ (↑t₁ : ℝ) * C ^ (↑t₂ : ℝ)
Tactic: convert! hf₁.interpolate hf₂ ht
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
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} (a • r + b • s)
have rw : Membership.mem (γ := Set ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f A} (r * a + s * b)
Tactic: rw [smul_eq_mul, smul_eq_mul, ← mul_comm r, ← mul_comm s]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (hypothesis)
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₂) t f A
have hf₃ : HolderOnWith (max C₁ C₂) r f A
Tactic: replace hf₁ := hf₁.mono_const (le_max_left C₁ C₂)
Cleared hypotheses: hf₁
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (hypothesis)
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₂) t f A
have hf₃ : HolderOnWith (max C₁ C₂) s f A
Tactic: replace hf₂ := hf₂.mono_const (le_max_right C₁ C₂)
Cleared hypotheses: hf₂
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
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 | HolderWith C r f}
have simp_rw : Convex ℝ≥0 (E := ℝ≥0) {r : ℝ≥0 | HolderOnWith C r f univ}
Tactic: simp_rw [← holderOnWith_univ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
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 : ℝ)
have rw : edist (f x) (f y) ≤ (↑C : ℝ≥0∞) * (↑d : ℝ≥0∞) ^ (↑r : ℝ)
Tactic: rw [← ENNReal.coe_le_coe, ← edist_nndist, ENNReal.coe_mul,
    ENNReal.coe_rpow_of_nonneg _ r.coe_nonneg]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
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
⊢ edist (f x) (f y) ≤ (↑C : ℝ≥0∞) * (↑d : ℝ≥0∞) ^ (↑r : ℝ)
have apply : edist x y ≤ (↑d : ℝ≥0∞)
Tactic: apply hf.edist_le_of_le hx hy
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
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
⊢ edist x y ≤ (↑d : ℝ≥0∞)
have rwa : (↑(nndist x y) : ℝ≥0∞) ≤ (↑d : ℝ≥0∞)
Tactic: rwa [edist_nndist, ENNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
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
⊢ dist (f x) (f y) ≤ (↑C : ℝ) * d ^ (↑r : ℝ)
have lift : ∀ (d : ℝ≥0) (hd : dist x y ≤ (↑d : ℝ)), dist (f x) (f y) ≤ (↑C : ℝ) * (↑d : ℝ) ^ (↑r : ℝ)
Tactic: lift d to ℝ≥0 using dist_nonneg.trans hd
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
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 : ℝ)
⊢ dist (f x) (f y) ≤ (↑C : ℝ) * (↑d : ℝ) ^ (↑r : ℝ)
have rw : ∀ (hd : (↑(nndist x y) : ℝ) ≤ (↑d : ℝ)), (↑(nndist (f x) (f y)) : ℝ) ≤ (↑C : ℝ) * (↑d : ℝ) ^ (↑r : ℝ)
Tactic: rw [dist_nndist] at hd ⊢
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (hypothesis)
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 : ℝ)
have hd₁ : nndist x y ≤ d
Tactic: norm_cast at hd ⊢
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
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₂
have refine_1 : ∀ (h : HolderWith 0 r f) (x₁ x₂ : X), f x₁ = f x₂
Tactic: refine ⟨fun h x₁ x₂ => ?_, fun h x₁ x₂ => h x₁ x₂ ▸ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
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₂
⊢ HolderWith 0 r f ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂
have refine_2 : ∀ (h : ∀ (x₁ x₂ : X), f x₁ = f x₂) (x₁ x₂ : X), edist (f x₁) (f x₁) ≤ (↑0 : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
Tactic: refine ⟨fun h x₁ x₂ => ?_, fun h x₁ x₂ => h x₁ x₂ ▸ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (hypothesis)
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
⊢ f x₁ = f x₂
have h₁ : edist (f x₁) (f x₂) ≤ (↑0 : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
Tactic: specialize h x₁ x₂
Cleared hypotheses: h
-- 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 C' r : ℝ≥0
f g : X → Y
hf : HolderWith C r f
hg : HolderWith C' r g
x₁ x₂ : X
⊢ edist ((f + g) x₁) ((f + g) x₂) ≤ (↑(C + C') : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
have simp : edist (f x₁ + g x₁) (f x₂ + g x₂) ≤ ((↑C : ℝ≥0∞) + (↑C' : ℝ≥0∞)) * edist x₁ x₂ ^ (↑r : ℝ)
Tactic: simp only [Pi.add_apply, ENNReal.coe_add]
-- 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 C' r : ℝ≥0
f g : X → Y
hf : HolderWith C r f
hg : HolderWith C' r g
x₁ x₂ : X
⊢ edist (f x₁ + g x₁) (f x₂ + g x₂) ≤ ((↑C : ℝ≥0∞) + (↑C' : ℝ≥0∞)) * edist x₁ x₂ ^ (↑r : ℝ)
have grw : (↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ) + (↑C' : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ) ≤
  ((↑C : ℝ≥0∞) + (↑C' : ℝ≥0∞)) * edist x₁ x₂ ^ (↑r : ℝ)
Tactic: grw [edist_add_add_le, hf x₁ x₂, hg x₁ x₂]
-- 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 C' r : ℝ≥0
f g : X → Y
hf : HolderWith C r f
hg : HolderWith C' r g
x₁ x₂ : X
⊢ (↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ) + (↑C' : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ) ≤
    ((↑C : ℝ≥0∞) + (↑C' : ℝ≥0∞)) * edist x₁ x₂ ^ (↑r : ℝ)
have 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 : ℝ)
Tactic: rw [add_mul]
-- 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 : 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 : ℝ)
have refine : ‖a‖₊ • edist (f x₁) (f x₂) ≤ (↑(C * ‖a‖₊) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
Tactic: refine edist_smul_le _ _ _ |>.trans ?_
-- 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 : SeminormedAddCommGroup α
inst_3 : SMulZeroClass α Y
inst_4 : IsBoundedSMul α Y
a : α
hf : HolderWith C r f
x₁ x₂ : X
⊢ ‖a‖₊ • edist (f x₁) (f x₂) ≤ (↑(C * ‖a‖₊) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
have rw : (↑‖a‖₊ : ℝ≥0∞) * edist (f x₁) (f x₂) ≤ (↑‖a‖₊ : ℝ≥0∞) * ((↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ))
Tactic: rw [ENNReal.coe_mul, ENNReal.smul_def, smul_eq_mul, mul_comm (C : ℝ≥0∞), mul_assoc]
-- 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 : SeminormedAddCommGroup α
inst_3 : SMulZeroClass α Y
inst_4 : IsBoundedSMul α Y
a : α
hf : HolderWith C r f
x₁ x₂ : X
⊢ (↑‖a‖₊ : ℝ≥0∞) * edist (f x₁) (f x₂) ≤ (↑‖a‖₊ : ℝ≥0∞) * ((↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ))
have bc : edist (f x₁) (f x₂) ≤ (↑C : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
Tactic: gcongr
-- 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
⊢ HolderWith (C * ‖a‖₊) r (a • f) ↔ HolderWith C r f
have 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 : ℝ)
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 : ℝ)
⊢ HolderWith (C * ‖a‖₊) r (a • f) ↔ HolderWith C r f
have 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 : ℝ)
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 : ℝ)
⊢ HolderWith (C * ‖a‖₊) r (a • f) ↔ HolderWith C r f
have 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 : ℝ)
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 : ℝ)
⊢ HolderWith (C * ‖a‖₊) r (a • f) ↔ HolderWith C r f
have 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 : ℝ)
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 : ℝ)
⊢ HolderWith (C * ‖a‖₊) r (a • f) ↔ HolderWith C r f
have 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 : ℝ)
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 : ℝ)
⊢ HolderWith (C * ‖a‖₊) r (a • f) ↔ HolderWith C r f
have 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 : ℝ)
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 : ℝ)
⊢ 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]