awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
refine_1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ diam (s ∪ t)
⊢ hausdorffDist s t ≤ diam (s ∪ t)
have refine_2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ diam (s ∪ t)
Tactic: refine hausdorffDist_le_of_mem_dist diam_nonneg ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
⊢ ∃ y ∈ t, dist x y < r
have r0 : 0 < r
Tactic: have r0 : 0 < r := lt_of_le_of_lt hausdorffDist_nonneg H
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
⊢ hausdorffEDist s t < ENNReal.ofReal r
have rwa : ∀ (H : (hausdorffEDist s t).toReal < r) (fin : hausdorffEDist s t ≠ ∞) (r0 : 0 < r),
  hausdorffEDist s t < ENNReal.ofReal r
Tactic: rwa [hausdorffDist, ← ENNReal.toReal_ofReal (le_of_lt r0),
      ENNReal.toReal_lt_toReal fin ENNReal.ofReal_ne_top] at H
Cleared hypotheses: H, fin, r0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
rwa :
  ∀ (H : (hausdorffEDist s t).toReal < r) (fin : hausdorffEDist s t ≠ ∞) (r0 : 0 < r),
    hausdorffEDist s t < ENNReal.ofReal r
⊢ hausdorffEDist s t < ENNReal.ofReal r
have rwa₁ : ∀ (H : (hausdorffEDist s t).toReal < (ENNReal.ofReal r).toReal) (fin : hausdorffEDist s t ≠ ∞) (r0 : 0 < r),
  hausdorffEDist s t < ENNReal.ofReal r
Tactic: rwa [hausdorffDist, ← ENNReal.toReal_ofReal (le_of_lt r0),
      ENNReal.toReal_lt_toReal fin ENNReal.ofReal_ne_top] at H
Cleared hypotheses: H, fin, r0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
rwa :
  ∀ (H : (hausdorffEDist s t).toReal < r) (fin : hausdorffEDist s t ≠ ∞) (r0 : 0 < r),
    hausdorffEDist s t < ENNReal.ofReal r
rwa₁ :
  ∀ (H : (hausdorffEDist s t).toReal < (ENNReal.ofReal r).toReal) (fin : hausdorffEDist s t ≠ ∞) (r0 : 0 < r),
    hausdorffEDist s t < ENNReal.ofReal r
⊢ hausdorffEDist s t < ENNReal.ofReal r
have rwa₂ : ∀ (H : hausdorffEDist s t < ENNReal.ofReal r) (fin : hausdorffEDist s t ≠ ∞) (r0 : 0 < r),
  hausdorffEDist s t < ENNReal.ofReal r
Tactic: rwa [hausdorffDist, ← ENNReal.toReal_ofReal (le_of_lt r0),
      ENNReal.toReal_lt_toReal fin ENNReal.ofReal_ne_top] at H
Cleared hypotheses: H, fin, r0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
⊢ ∃ y ∈ t, dist x y < r
have this : hausdorffEDist s t < ENNReal.ofReal r
Tactic: have : hausdorffEDist s t < ENNReal.ofReal r := by
    rwa [hausdorffDist, ← ENNReal.toReal_ofReal (le_of_lt r0),
      ENNReal.toReal_lt_toReal fin ENNReal.ofReal_ne_top] at H
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
this : hausdorffEDist s t < ENNReal.ofReal r
⊢ ∃ y ∈ t, dist x y < r
have rcases : ∀ (y : α) (hy : y ∈ t) (yr : edist x y < ENNReal.ofReal r), ∃ y ∈ t, dist x y < r
Tactic: rcases exists_edist_lt_of_hausdorffEDist_lt h this with ⟨y, hy, yr⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
this : hausdorffEDist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : edist x y < ENNReal.ofReal r
⊢ ∃ y ∈ t, dist x y < r
have yr₁ : dist x y < r
Tactic: rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff r0] at yr
Cleared hypotheses: yr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
y : α
r : ℝ
h : y ∈ t
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
⊢ ∃ x ∈ s, dist x y < r
have H₁ : hausdorffDist t s < r
Tactic: rw [hausdorffDist_comm] at H
Cleared hypotheses: H, fin
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
y : α
r : ℝ
h : y ∈ t
H : hausdorffDist t s < r
fin : hausdorffEDist s t ≠ ∞
⊢ ∃ x ∈ s, dist x y < r
have fin₁ : hausdorffEDist t s ≠ ∞
Tactic: rw [hausdorffEDist_comm] at fin
Cleared hypotheses: fin
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist s t ≠ ∞
⊢ infDist x t ≤ infDist x s + hausdorffDist s t
have refine : ∀ (h : infEDist x s = ∞), infEDist x t = ∞
Tactic: refine toReal_le_add' infEDist_le_infEDist_add_hausdorffEDist (fun h ↦ ?_) (flip absurd fin)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist s t ≠ ∞
h : infEDist x s = ∞
⊢ infEDist x t = ∞
have rw : ∀ (h : ¬s.Nonempty), ¬t.Nonempty
Tactic: rw [infEDist_eq_top_iff, ← not_nonempty_iff_eq_empty] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist s t ≠ ∞
h : ¬s.Nonempty
⊢ ¬t.Nonempty
have fin₁ : hausdorffEDist t s ≠ ∞
Tactic: rw [hausdorffEDist_comm] at fin
Cleared hypotheses: fin, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist s t ≠ ∞
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
have refine : ∀ (h : ¬hausdorffEDist s u = ∞), ¬hausdorffEDist t u = ∞
Tactic: refine toReal_le_add' hausdorffEDist_triangle (flip absurd fin) (not_imp_not.1 fun h ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist s t ≠ ∞
h : ¬hausdorffEDist s u = ∞
⊢ ¬hausdorffEDist t u = ∞
have fin₁ : hausdorffEDist t s ≠ ∞
Tactic: rw [hausdorffEDist_comm] at fin
Cleared hypotheses: fin, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist t u ≠ ∞
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
have fin₁ : hausdorffEDist u t ≠ ∞
Tactic: rw [hausdorffEDist_comm] at fin
Cleared hypotheses: fin
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist u t ≠ ∞
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
have I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s
Tactic: have I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s :=
    hausdorffDist_triangle fin
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ hausdorffDist (α := α) {x} {y} = dist x y
have rw : (hausdorffEDist (α := α) {x} {y}).toReal = dist x y
Tactic: rw [hausdorffDist, hausdorffEDist_singleton, dist_edist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
rw : (hausdorffEDist (α := α) {x} {y}).toReal = dist x y
⊢ hausdorffDist (α := α) {x} {y} = dist x y
have rw₁ : (edist x y).toReal = dist x y
Tactic: rw [hausdorffDist, hausdorffEDist_singleton, dist_edist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
rw : (hausdorffEDist (α := α) {x} {y}).toReal = dist x y
rw₁ : (edist x y).toReal = dist x y
⊢ hausdorffDist (α := α) {x} {y} = dist x y
have rw₂ : (edist x y).toReal = (edist x y).toReal
Tactic: rw [hausdorffDist, hausdorffEDist_singleton, dist_edist]
-- 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
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
x y : X
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0∞
hd : edist x y ≤ d
⊢ (↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ) ≤ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)
have bc : 0 ≤ (↑r : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Holder (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : PseudoEMetricSpace Z
s : Set X
Cg rg : ℝ≥0
g : Y → Z
t : Set Y
hg : HolderOnWith Cg rg g t
Cf rf : ℝ≥0
f : X → Y
hf : HolderOnWith Cf rf f s
hst : MapsTo f s t
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ edist ((g ∘ f) x) ((g ∘ f) y) ≤ (↑(Cg * Cf ^ (↑rg : ℝ)) : ℝ≥0∞) * edist x y ^ (↑(rg * rf) : ℝ)
have rw : edist ((g ∘ f) x) ((g ∘ f) y) ≤ (↑Cg : ℝ≥0∞) * ((↑Cf : ℝ≥0∞) * edist x y ^ (↑rf : ℝ)) ^ (↑rg : ℝ)
Tactic: rw [ENNReal.coe_mul, mul_comm rg, NNReal.coe_mul, ENNReal.rpow_mul, mul_assoc,
    ENNReal.coe_rpow_of_nonneg _ rg.coe_nonneg, ← ENNReal.mul_rpow_of_nonneg _ _ rg.coe_nonneg]
-- 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
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
⊢ UniformContinuousOn f s
have refine : ∀ (ε : ℝ≥0∞) (εpos : ε > 0), ∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
Tactic: refine EMetric.uniformContinuousOn_iff.2 fun ε εpos => ?_
-- 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
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
have this : Tendsto (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) (𝓝 0) (𝓝 0)
Tactic: have : Tendsto (fun d : ℝ≥0∞ => (C : ℝ≥0∞) * d ^ (r : ℝ)) (𝓝 0) (𝓝 0) :=
    ENNReal.tendsto_const_mul_rpow_nhds_zero_of_pos ENNReal.coe_ne_top h0
-- 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
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) (𝓝 0) (𝓝 0)
⊢ ∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
have rcases : ∀ (δ : ℝ≥0∞) (δ0 : 0 < δ)
  (H :
    Iio δ ⊆ preimage (β := ℝ≥0∞) (fun (d : ℝ≥0∞) ↦ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)) {x : ℝ≥0∞ | (fun (x : ℝ≥0∞) ↦ x < ε) x}),
  ∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
Tactic: rcases ENNReal.nhds_zero_basis.mem_iff.1 (this (gt_mem_nhds εpos)) with ⟨δ, δ0, H⟩
-- 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₂ s t₁ t₂ : ℝ≥0
A : Set X
hf₁ : HolderOnWith C₁ r f A
hf₂ : HolderOnWith C₂ s f A
ht : t₁ + t₂ = 1
x : X
hx : x ∈ A
y : X
hy : y ∈ A
⊢ edist (f x) (f y) ^ (↑t₁ : ℝ) * edist (f x) (f y) ^ (↑t₂ : ℝ) ≤
    ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ)
have h₁ : 0 ≤ (↑t₁ : ℝ)
Tactic: nth_grw 1 [hf₁ x hx y hy, hf₂ x hx y hy]
-- 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₂ s t₁ t₂ : ℝ≥0
A : Set X
hf₁ : HolderOnWith C₁ r f A
hf₂ : HolderOnWith C₂ s f A
ht : t₁ + t₂ = 1
x : X
hx : x ∈ A
y : X
hy : y ∈ A
h₁ : 0 ≤ (↑t₁ : ℝ)
⊢ edist (f x) (f y) ^ (↑t₁ : ℝ) * edist (f x) (f y) ^ (↑t₂ : ℝ) ≤
    ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ)
have nth_grw : ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * edist (f x) (f y) ^ (↑t₂ : ℝ) ≤
  ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ)
Tactic: nth_grw 1 [hf₁ x hx y hy, hf₂ x hx y hy]
-- 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₂ s t₁ t₂ : ℝ≥0
A : Set X
hf₁ : HolderOnWith C₁ r f A
hf₂ : HolderOnWith C₂ s f A
ht : t₁ + t₂ = 1
x : X
hx : x ∈ A
y : X
hy : y ∈ A
h₁ : 0 ≤ (↑t₁ : ℝ)
nth_grw :
  ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * edist (f x) (f y) ^ (↑t₂ : ℝ) ≤
    ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ)
⊢ edist (f x) (f y) ^ (↑t₁ : ℝ) * edist (f x) (f y) ^ (↑t₂ : ℝ) ≤
    ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ)
have nth_grw₁ : ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ) ≤
  ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ)
Tactic: nth_grw 1 [hf₁ x hx y hy, hf₂ x hx y hy]
-- 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₂ s t₁ t₂ : ℝ≥0
A : Set X
hf₁ : HolderOnWith C₁ r f A
hf₂ : HolderOnWith C₂ s f A
ht : t₁ + t₂ = 1
x : X
hx : x ∈ A
y : X
hy : y ∈ A
⊢ ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ) =
    (↑(C₁ ^ (↑t₁ : ℝ)) : ℝ≥0∞) * (↑(C₂ ^ (↑t₂ : ℝ)) : ℝ≥0∞) * edist x y ^ ((↑r : ℝ) * (↑t₁ : ℝ) + (↑s : ℝ) * (↑t₂ : ℝ))
have simp : (↑C₁ : ℝ≥0∞) ^ (↑t₁ : ℝ) * (edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) *
    ((↑C₂ : ℝ≥0∞) ^ (↑t₂ : ℝ) * (edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ)) =
  (↑C₁ : ℝ≥0∞) ^ (↑t₁ : ℝ) * (↑C₂ : ℝ≥0∞) ^ (↑t₂ : ℝ) *
    ((edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * (edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ))
Tactic: simp (discharger := positivity) only [ENNReal.mul_rpow_of_nonneg,
          ENNReal.rpow_add_of_nonneg, ENNReal.rpow_mul, ENNReal.coe_rpow_of_nonneg]
-- 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₂ s t₁ t₂ : ℝ≥0
A : Set X
hf₁ : HolderOnWith C₁ r f A
hf₂ : HolderOnWith C₂ s f A
ht : t₁ + t₂ = 1
x : X
hx : x ∈ A
y : X
hy : y ∈ A
⊢ edist (f x) (f y) ≤ (↑(C₁ ^ (↑t₁ : ℝ) * C₂ ^ (↑t₂ : ℝ)) : ℝ≥0∞) * edist x y ^ (↑(r * t₁ + s * t₂) : ℝ)
have calc : edist (f x) (f y) = edist (f x) (f y) ^ (↑t₁ : ℝ) * edist (f x) (f y) ^ (↑t₂ : ℝ)
Tactic: calc edist (f x) (f y)
      = (edist (f x) (f y)) ^ (t₁ : ℝ) * (edist (f x) (f y)) ^ (t₂ : ℝ) := by
        simp [← ENNReal.rpow_add_of_nonneg, ← NNReal.coe_add, ht]
    _ ≤ (C₁ * (edist x y) ^ (r : ℝ)) ^ (t₁ : ℝ) * (C₂ * (edist x y) ^ (s : ℝ)) ^ (t₂ : ℝ) := by
        nth_grw 1 [hf₁ x hx y hy, hf₂ x hx y hy]
    _ = ↑(C₁ ^ (t₁ : ℝ) * C₂ ^ (t₂ : ℝ)) * (edist x y) ^ (↑(r * t₁ + s * t₂) : ℝ) := by
        push_cast
        simp (discharger := positivity) only [ENNReal.mul_rpow_of_nonneg,
          ENNReal.rpow_add_of_nonneg, ENNReal.rpow_mul, ENNReal.coe_rpow_of_nonneg]
        ring
-- 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₂ s t₁ t₂ : ℝ≥0
A : Set X
hf₁ : HolderOnWith C₁ r f A
hf₂ : HolderOnWith C₂ s f A
ht : t₁ + t₂ = 1
x : X
hx : x ∈ A
y : X
hy : y ∈ A
calc : edist (f x) (f y) = edist (f x) (f y) ^ (↑t₁ : ℝ) * edist (f x) (f y) ^ (↑t₂ : ℝ)
⊢ edist (f x) (f y) ≤ (↑(C₁ ^ (↑t₁ : ℝ) * C₂ ^ (↑t₂ : ℝ)) : ℝ≥0∞) * edist x y ^ (↑(r * t₁ + s * t₂) : ℝ)
have calc₁ : edist (f x) (f y) ^ (↑t₁ : ℝ) * edist (f x) (f y) ^ (↑t₂ : ℝ) ≤
  ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ)
Tactic: calc edist (f x) (f y)
      = (edist (f x) (f y)) ^ (t₁ : ℝ) * (edist (f x) (f y)) ^ (t₂ : ℝ) := by
        simp [← ENNReal.rpow_add_of_nonneg, ← NNReal.coe_add, ht]
    _ ≤ (C₁ * (edist x y) ^ (r : ℝ)) ^ (t₁ : ℝ) * (C₂ * (edist x y) ^ (s : ℝ)) ^ (t₂ : ℝ) := by
        nth_grw 1 [hf₁ x hx y hy, hf₂ x hx y hy]
    _ = ↑(C₁ ^ (t₁ : ℝ) * C₂ ^ (t₂ : ℝ)) * (edist x y) ^ (↑(r * t₁ + s * t₂) : ℝ) := by
        push_cast
        simp (discharger := positivity) only [ENNReal.mul_rpow_of_nonneg,
          ENNReal.rpow_add_of_nonneg, ENNReal.rpow_mul, ENNReal.coe_rpow_of_nonneg]
        ring
-- 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₂ s t₁ t₂ : ℝ≥0
A : Set X
hf₁ : HolderOnWith C₁ r f A
hf₂ : HolderOnWith C₂ s f A
ht : t₁ + t₂ = 1
x : X
hx : x ∈ A
y : X
hy : y ∈ A
calc : edist (f x) (f y) = edist (f x) (f y) ^ (↑t₁ : ℝ) * edist (f x) (f y) ^ (↑t₂ : ℝ)
calc₁ :
  edist (f x) (f y) ^ (↑t₁ : ℝ) * edist (f x) (f y) ^ (↑t₂ : ℝ) ≤
    ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ)
⊢ edist (f x) (f y) ≤ (↑(C₁ ^ (↑t₁ : ℝ) * C₂ ^ (↑t₂ : ℝ)) : ℝ≥0∞) * edist x y ^ (↑(r * t₁ + s * t₂) : ℝ)
have calc₂ : ((↑C₁ : ℝ≥0∞) * edist x y ^ (↑r : ℝ)) ^ (↑t₁ : ℝ) * ((↑C₂ : ℝ≥0∞) * edist x y ^ (↑s : ℝ)) ^ (↑t₂ : ℝ) =
  (↑(C₁ ^ (↑t₁ : ℝ) * C₂ ^ (↑t₂ : ℝ)) : ℝ≥0∞) * edist x y ^ (↑(r * t₁ + s * t₂) : ℝ)
Tactic: calc edist (f x) (f y)
      = (edist (f x) (f y)) ^ (t₁ : ℝ) * (edist (f x) (f y)) ^ (t₂ : ℝ) := by
        simp [← ENNReal.rpow_add_of_nonneg, ← NNReal.coe_add, ht]
    _ ≤ (C₁ * (edist x y) ^ (r : ℝ)) ^ (t₁ : ℝ) * (C₂ * (edist x y) ^ (s : ℝ)) ^ (t₂ : ℝ) := by
        nth_grw 1 [hf₁ x hx y hy, hf₂ x hx y hy]
    _ = ↑(C₁ ^ (t₁ : ℝ) * C₂ ^ (t₂ : ℝ)) * (edist x y) ^ (↑(r * t₁ + s * t₂) : ℝ) := by
        push_cast
        simp (discharger := positivity) only [ENNReal.mul_rpow_of_nonneg,
          ENNReal.rpow_add_of_nonneg, ENNReal.rpow_mul, ENNReal.coe_rpow_of_nonneg]
        ring
-- 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 : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
x : X
hx : x ∈ A
y : X
hy : y ∈ A
⊢ edist (f x) (f y) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞) * edist x y ^ (↑0 : ℝ)
have simp : edist (f x) (f y) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞)
Tactic: simp only [NNReal.coe_zero, ENNReal.rpow_zero, mul_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 : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
x : X
hx : x ∈ A
y : X
hy : y ∈ A
⊢ edist (f x) (f y) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞)
have grw : (↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞)
Tactic: grw [hf x hx y hy, hA x hx y hy, ENNReal.coe_mul, ENNReal.coe_rpow_of_nonneg _ (by 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 : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
x : X
hx : x ∈ A
y : X
hy : y ∈ A
grw : (↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞)
⊢ edist (f x) (f y) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞)
have grw₁ : (↑C : ℝ≥0∞) * (↑D : ℝ≥0∞) ^ (↑r : ℝ) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞)
Tactic: grw [hf x hx y hy, hA x hx y hy, ENNReal.coe_mul, ENNReal.coe_rpow_of_nonneg _ (by 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 : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
x : X
hx : x ∈ A
y : X
hy : y ∈ A
grw : (↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞)
grw₁ : (↑C : ℝ≥0∞) * (↑D : ℝ≥0∞) ^ (↑r : ℝ) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞)
⊢ edist (f x) (f y) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞)
have grw₂ : (↑C : ℝ≥0∞) * (↑D : ℝ≥0∞) ^ (↑r : ℝ) ≤ (↑C : ℝ≥0∞) * (↑(D ^ (↑r : ℝ)) : ℝ≥0∞)
Tactic: grw [hf x hx y hy, hA x hx y hy, ENNReal.coe_mul, ENNReal.coe_rpow_of_nonneg _ (by 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 : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ (↑D : ℝ≥0∞)
hf : HolderOnWith C r f A
x : X
hx : x ∈ A
y : X
hy : y ∈ A
grw : (↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞)
grw₁ : (↑C : ℝ≥0∞) * (↑D : ℝ≥0∞) ^ (↑r : ℝ) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞)
grw₂ : (↑C : ℝ≥0∞) * (↑D : ℝ≥0∞) ^ (↑r : ℝ) ≤ (↑C : ℝ≥0∞) * (↑(D ^ (↑r : ℝ)) : ℝ≥0∞)
⊢ edist (f x) (f y) ≤ (↑(C * D ^ (↑r : ℝ)) : ℝ≥0∞)
have grw₃ : (↑C : ℝ≥0∞) * (↑D : ℝ≥0∞) ^ (↑r : ℝ) ≤ (↑C : ℝ≥0∞) * (↑D : ℝ≥0∞) ^ (↑r : ℝ)
Tactic: grw [hf x hx y hy, hA x hx y hy, ENNReal.coe_mul, ENNReal.coe_rpow_of_nonneg _ (by 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
⊢ HolderOnWith (C * D ^ ((↑r : ℝ) - (↑s : ℝ))) s f A
have inl : ∀ (hsr : 0 ≤ r), HolderOnWith (C * D ^ ((↑r : ℝ) - (↑0 : ℝ))) 0 f A
Tactic: obtain rfl | ht := eq_zero_or_pos s
Cleared hypotheses: s, hsr
-- 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
inl : ∀ (hsr : 0 ≤ r), HolderOnWith (C * D ^ ((↑r : ℝ) - (↑0 : ℝ))) 0 f A
⊢ HolderOnWith (C * D ^ ((↑r : ℝ) - (↑s : ℝ))) s f A
have inr : ∀ (ht : 0 < s), HolderOnWith (C * D ^ ((↑r : ℝ) - (↑s : ℝ))) s f A
Tactic: obtain rfl | ht := eq_zero_or_pos 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 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
⊢ HolderOnWith (C * D ^ ((↑r : ℝ) - (↑s : ℝ))) s f A
have hr : 0 < r
Tactic: have hr : 0 < r := ht.trans_le hsr
-- 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
⊢ HolderOnWith (C * D ^ ((↑r : ℝ) - (↑s : ℝ))) s f A
have hsr₁ : (↑s : ℝ) ≤ (↑r : ℝ)
Tactic: rw [← NNReal.coe_le_coe] at hsr
Cleared hypotheses: hsr, ht, hr
-- 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
⊢ HolderOnWith (C * D ^ ((↑r : ℝ) - (↑s : ℝ))) s f A
have hr₁ : 0 < (↑r : ℝ)
Tactic: rw [← NNReal.coe_pos] at hr
Cleared hypotheses: hr