awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 g : X → Y
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
have pos : ∀ (hfg : MemHolder r f ∧ MemHolder r g), eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
Tactic: by_cases hfg : MemHolder r f ∧ MemHolder r g
-- 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 g : X → Y
pos : ∀ (hfg : MemHolder r f ∧ MemHolder r g), eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
have neg : ∀ (hfg : ¬(MemHolder r f ∧ MemHolder r g)), eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
Tactic: by_cases hfg : MemHolder r f ∧ MemHolder r g
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
hfg : MemHolder r f ∧ MemHolder r g
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
have hf : MemHolder r f
Tactic: obtain ⟨hf, hg⟩ := hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
hfg : MemHolder r f ∧ MemHolder r g
hf : MemHolder r f
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
have hg : MemHolder r g
Tactic: obtain ⟨hf, hg⟩ := hfg
Cleared hypotheses: hfg
-- 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 g : X → Y
hf : MemHolder r f
hg : MemHolder r g
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
have pos : nnHolderNorm r (f + g) ≤ nnHolderNorm r f + nnHolderNorm r g
Tactic: rw [← hf.coe_nnHolderNorm_eq_eHolderNorm, ← hg.coe_nnHolderNorm_eq_eHolderNorm,
      ← (hf.add hg).coe_nnHolderNorm_eq_eHolderNorm, ← coe_add, ENNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
hfg : ¬(MemHolder r f ∧ MemHolder r g)
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
have hfg₁ : eHolderNorm r f = ∞ ∨ eHolderNorm r g = ∞
Tactic: rw [Classical.not_and_iff_not_or_not, ← eHolderNorm_eq_top, ← eHolderNorm_eq_top] at hfg
Cleared hypotheses: hfg
-- 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 g : X → Y
hfg : eHolderNorm r f = ∞ ∨ eHolderNorm r g = ∞
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
have neg : ∀ (h : eHolderNorm r f = ∞), eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
Tactic: obtain (h | h) := hfg
Cleared hypotheses: hfg
-- 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 g : X → Y
hfg : eHolderNorm r f = ∞ ∨ eHolderNorm r g = ∞
neg : ∀ (h : eHolderNorm r f = ∞), eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
have neg₁ : ∀ (h : eHolderNorm r g = ∞), eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
Tactic: obtain (h | h) := hfg
Cleared hypotheses: hfg
-- 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 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
⊢ eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
have pos : ∀ (hc : ‖c‖₊ = 0), eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
Tactic: by_cases hc : ‖c‖₊ = 0
-- 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 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
pos : ∀ (hc : ‖c‖₊ = 0), eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
⊢ eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
have neg : ∀ (hc : ¬‖c‖₊ = 0), eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
Tactic: by_cases hc : ‖c‖₊ = 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (hypothesis)
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 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ‖c‖₊ = 0
⊢ eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
have hc₁ : c = 0
Tactic: rw [nnnorm_eq_zero] at hc
Cleared hypotheses: 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 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
⊢ eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
have pos : ∀ (hf : MemHolder r f), eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
Tactic: by_cases hf : MemHolder r f
-- 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 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
pos : ∀ (hf : MemHolder r f), eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
⊢ eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
have neg : ∀ (hf : ¬MemHolder r f), eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
Tactic: by_cases hf : MemHolder r f
-- 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 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
⊢ eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
have pos : (↑(nnHolderNorm r f * ‖c‖₊) : ℝ≥0∞) ≤ (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
Tactic: refine le_antisymm ((hf.holderWith.smul c).eHolderNorm_le.trans ?_) <| mul_le_of_le_div' ?_
-- 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 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
pos : (↑(nnHolderNorm r f * ‖c‖₊) : ℝ≥0∞) ≤ (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
⊢ eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
have pos₁ : eHolderNorm r f ≤ eHolderNorm r (c • f) / (↑‖c‖₊ : ℝ≥0∞)
Tactic: refine le_antisymm ((hf.holderWith.smul c).eHolderNorm_le.trans ?_) <| mul_le_of_le_div' ?_
-- 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 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
⊢ (↑(nnHolderNorm r f * ‖c‖₊) : ℝ≥0∞) ≤ (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
have pos : (↑(nnHolderNorm r f) : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) ≤ (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
Tactic: rw [coe_mul, hf.coe_nnHolderNorm_eq_eHolderNorm, mul_comm]
-- 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 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
pos : (↑(nnHolderNorm r f) : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) ≤ (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
⊢ (↑(nnHolderNorm r f * ‖c‖₊) : ℝ≥0∞) ≤ (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
have pos₁ : eHolderNorm r f * (↑‖c‖₊ : ℝ≥0∞) ≤ (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
Tactic: rw [coe_mul, hf.coe_nnHolderNorm_eq_eHolderNorm, mul_comm]
-- 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 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
pos : (↑(nnHolderNorm r f) : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) ≤ (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
pos₁ : eHolderNorm r f * (↑‖c‖₊ : ℝ≥0∞) ≤ (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
⊢ (↑(nnHolderNorm r f * ‖c‖₊) : ℝ≥0∞) ≤ (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
have pos₂ : (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f ≤ (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
Tactic: rw [coe_mul, hf.coe_nnHolderNorm_eq_eHolderNorm, mul_comm]
-- 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 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
⊢ eHolderNorm r f ≤ eHolderNorm r (c • f) / (↑‖c‖₊ : ℝ≥0∞)
have pos : eHolderNorm r f ≤ (↑(nnHolderNorm r (c • f) / ‖c‖₊) : ℝ≥0∞)
Tactic: rw [← (hf.holderWith.smul c).memHolder.coe_nnHolderNorm_eq_eHolderNorm, ← coe_div 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 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
⊢ eHolderNorm r f ≤ (↑(nnHolderNorm r (c • f) / ‖c‖₊) : ℝ≥0∞)
have pos : ∀ (x₁ x₂ : X), edist (f x₁) (f x₂) ≤ (↑(nnHolderNorm r (c • f) / ‖c‖₊) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
Tactic: refine HolderWith.eHolderNorm_le fun 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 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
x₁ x₂ : X
⊢ edist (f x₁) (f x₂) ≤ (↑(nnHolderNorm r (c • f) / ‖c‖₊) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
have pos : edist ((c • f) x₁) ((c • f) x₂) ≤ (↑(nnHolderNorm r (c • f)) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
Tactic: rw [coe_div hc, ← ENNReal.mul_div_right_comm,
        ENNReal.le_div_iff_mul_le (Or.inl <| coe_ne_zero.2 hc) <| Or.inl coe_ne_top,
        mul_comm, ← smul_eq_mul, ← ENNReal.smul_def, ← edist_smul₀, ← Pi.smul_apply,
        ← Pi.smul_apply]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (hypothesis)
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 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : ¬MemHolder r f
⊢ eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
have hf₁ : eHolderNorm r f = ∞
Tactic: rw [← eHolderNorm_eq_top] at hf
Cleared hypotheses: 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 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : eHolderNorm r f = ∞
⊢ eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
have neg : ¬MemHolder r f
Tactic: rw [hf, mul_top <| coe_ne_zero.2 hc, eHolderNorm_eq_top, MemHolder.smul_iff hc]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HolderNorm (hypothesis)
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 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : eHolderNorm r f = ∞
⊢ ¬MemHolder r f
have hc₁ : ¬c = 0
Tactic: rw [nnnorm_eq_zero] at hc
Cleared hypotheses: hc, 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 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
hf : MemHolder r f
c : α
⊢ nnHolderNorm r (c • f) = ‖c‖₊ * nnHolderNorm r f
have rw : (↑(nnHolderNorm r (c • f)) : ℝ≥0∞) = (↑(‖c‖₊ * nnHolderNorm r f) : ℝ≥0∞)
Tactic: rw [← ENNReal.coe_inj, coe_mul, hf.coe_nnHolderNorm_eq_eHolderNorm,
    hf.smul.coe_nnHolderNorm_eq_eHolderNorm, eHolderNorm_smul]
-- 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 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
hf : MemHolder r f
c : α
rw : (↑(nnHolderNorm r (c • f)) : ℝ≥0∞) = (↑(‖c‖₊ * nnHolderNorm r f) : ℝ≥0∞)
⊢ nnHolderNorm r (c • f) = ‖c‖₊ * nnHolderNorm r f
have rw₁ : (↑(nnHolderNorm r (c • f)) : ℝ≥0∞) = (↑‖c‖₊ : ℝ≥0∞) * (↑(nnHolderNorm r f) : ℝ≥0∞)
Tactic: rw [← ENNReal.coe_inj, coe_mul, hf.coe_nnHolderNorm_eq_eHolderNorm,
    hf.smul.coe_nnHolderNorm_eq_eHolderNorm, eHolderNorm_smul]
-- 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 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
hf : MemHolder r f
c : α
rw : (↑(nnHolderNorm r (c • f)) : ℝ≥0∞) = (↑(‖c‖₊ * nnHolderNorm r f) : ℝ≥0∞)
rw₁ : (↑(nnHolderNorm r (c • f)) : ℝ≥0∞) = (↑‖c‖₊ : ℝ≥0∞) * (↑(nnHolderNorm r f) : ℝ≥0∞)
⊢ nnHolderNorm r (c • f) = ‖c‖₊ * nnHolderNorm r f
have rw₂ : (↑(nnHolderNorm r (c • f)) : ℝ≥0∞) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
Tactic: rw [← ENNReal.coe_inj, coe_mul, hf.coe_nnHolderNorm_eq_eHolderNorm,
    hf.smul.coe_nnHolderNorm_eq_eHolderNorm, eHolderNorm_smul]
-- 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 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
hf : MemHolder r f
c : α
rw : (↑(nnHolderNorm r (c • f)) : ℝ≥0∞) = (↑(‖c‖₊ * nnHolderNorm r f) : ℝ≥0∞)
rw₁ : (↑(nnHolderNorm r (c • f)) : ℝ≥0∞) = (↑‖c‖₊ : ℝ≥0∞) * (↑(nnHolderNorm r f) : ℝ≥0∞)
rw₂ : (↑(nnHolderNorm r (c • f)) : ℝ≥0∞) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
⊢ nnHolderNorm r (c • f) = ‖c‖₊ * nnHolderNorm r f
have rw₃ : eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
Tactic: rw [← ENNReal.coe_inj, coe_mul, hf.coe_nnHolderNorm_eq_eHolderNorm,
    hf.smul.coe_nnHolderNorm_eq_eHolderNorm, eHolderNorm_smul]
-- 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 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
hf : MemHolder r f
c : α
rw : (↑(nnHolderNorm r (c • f)) : ℝ≥0∞) = (↑(‖c‖₊ * nnHolderNorm r f) : ℝ≥0∞)
rw₁ : (↑(nnHolderNorm r (c • f)) : ℝ≥0∞) = (↑‖c‖₊ : ℝ≥0∞) * (↑(nnHolderNorm r f) : ℝ≥0∞)
rw₂ : (↑(nnHolderNorm r (c • f)) : ℝ≥0∞) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
rw₃ : eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
⊢ nnHolderNorm r (c • f) = ‖c‖₊ * nnHolderNorm r f
have rw₄ : (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
Tactic: rw [← ENNReal.coe_inj, coe_mul, hf.coe_nnHolderNorm_eq_eHolderNorm,
    hf.smul.coe_nnHolderNorm_eq_eHolderNorm, eHolderNorm_smul]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
⊢ s.einfsep = 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
have simp_rw : Eq (α := ℝ≥0∞) (⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
Tactic: simp_rw [einfsep, ← _root_.bot_eq_zero, iInf_eq_bot, iInf_lt_iff, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
simp_rw :
  Eq (α := ℝ≥0∞) (⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
⊢ s.einfsep = 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
have simp_rw₁ : Eq (α := ℝ≥0∞) (⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) ⊥ ↔ ∀ C > ⊥, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
Tactic: simp_rw [einfsep, ← _root_.bot_eq_zero, iInf_eq_bot, iInf_lt_iff, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
simp_rw :
  Eq (α := ℝ≥0∞) (⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
simp_rw₁ :
  Eq (α := ℝ≥0∞) (⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) ⊥ ↔ ∀ C > ⊥, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
⊢ s.einfsep = 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
have simp_rw₂ : (∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : α), ⨅ (_ : i ∈ s), ⨅ y ∈ s, ⨅ (_ : i ≠ y), edist i y < b) ↔
  ∀ C > ⊥, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
Tactic: simp_rw [einfsep, ← _root_.bot_eq_zero, iInf_eq_bot, iInf_lt_iff, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
simp_rw :
  Eq (α := ℝ≥0∞) (⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
simp_rw₁ :
  Eq (α := ℝ≥0∞) (⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) ⊥ ↔ ∀ C > ⊥, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
simp_rw₂ :
  (∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : α), ⨅ (_ : i ∈ s), ⨅ y ∈ s, ⨅ (_ : i ≠ y), edist i y < b) ↔
    ∀ C > ⊥, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
⊢ s.einfsep = 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
have simp_rw₃ : (∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : α) (_ : i ∈ s) (i_1 : α) (_ : i_1 ∈ s) (_ : i ≠ i_1), edist i i_1 < b) ↔
  ∀ C > ⊥, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
Tactic: simp_rw [einfsep, ← _root_.bot_eq_zero, iInf_eq_bot, iInf_lt_iff, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
⊢ 0 < s.einfsep ↔ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y
have rw : (¬∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C) ↔ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y
Tactic: rw [pos_iff_ne_zero, Ne, einfsep_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
⊢ s.einfsep < ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ∞
have simp_rw : LT.lt (α := ℝ≥0∞) (⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ∞
Tactic: simp_rw [einfsep, iInf_lt_iff, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
simp_rw : LT.lt (α := ℝ≥0∞) (⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ∞
⊢ s.einfsep < ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ∞
have simp_rw₁ : (∃ (i : α) (_ : i ∈ s) (i_1 : α) (_ : i_1 ∈ s) (_ : i ≠ i_1), edist i i_1 < ∞) ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ∞
Tactic: simp_rw [einfsep, iInf_lt_iff, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
⊢ s.einfsep ≠ ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y ≠ ∞
have simp_rw : s.einfsep < ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ∞
Tactic: simp_rw [← lt_top_iff_ne_top, einfsep_lt_top]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
d : ℝ≥0∞
⊢ s.einfsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d
have simp_rw : ⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d
Tactic: simp_rw [einfsep, iInf_lt_iff, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
d : ℝ≥0∞
simp_rw : ⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d
⊢ s.einfsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d
have simp_rw₁ : (∃ (i : α) (_ : i ∈ s) (i_1 : α) (_ : i_1 ∈ s) (_ : i ≠ i_1), edist i i_1 < d) ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d
Tactic: simp_rw [einfsep, iInf_lt_iff, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : s.einfsep < ∞
⊢ s.Nontrivial
have rcases : ∀ (w : α) (hx : w ∈ s) (w_1 : α) (hy : w_1 ∈ s) (hxy : w ≠ w_1), edist w w_1 < ∞ → s.Nontrivial
Tactic: rcases einfsep_lt_top.1 hs with ⟨_, hx, _, hy, hxy, _⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : s.Subsingleton
⊢ s.einfsep = ∞
have rw : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ∞
Tactic: rw [einfsep_top]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
β : Type u_2
inst : EDist α
d : ℝ≥0∞
f : β → α
s : Set β
⊢ d ≤ (f '' s).einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≠ f y → d ≤ edist (f x) (f y)
have simp_rw : (∀ x ∈ f '' s, ∀ y ∈ f '' s, x ≠ y → d ≤ edist x y) ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≠ f y → d ≤ edist (f x) (f y)
Tactic: simp_rw [le_einfsep_iff, forall_mem_image]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
ι : Type u_3
o : Option ι
s : ι → Set α
⊢ einfsep.{u_1} (α := α) (⋃ i ∈ o, s i) = ⨅ i ∈ o, (s i).einfsep
have none : einfsep.{u_1} (α := α) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Option ι) none i), s i) =
  ⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Option ι) none i), (s i).einfsep
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
ι : Type u_3
o : Option ι
s : ι → Set α
none :
  einfsep.{u_1} (α := α) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Option ι) Option.none i), s i) =
    ⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Option ι) Option.none i), (s i).einfsep
⊢ einfsep.{u_1} (α := α) (⋃ i ∈ o, s i) = ⨅ i ∈ o, (s i).einfsep
have some : ∀ (val : ι), einfsep.{u_1} (α := α) (⋃ i ∈ some val, s i) = ⨅ i ∈ some val, (s i).einfsep
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
x : α
s : Set α
⊢ (insert x s).einfsep ≤ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y
have simp_rw : ∀ (i : α) (i_1 : i ∈ s) (i_2 : x ≠ i), (insert x s).einfsep ≤ edist x i
Tactic: simp_rw [le_iInf_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
x y : α
⊢ min (edist x y) (edist y x) ≤ einfsep (α := α) {x, y}
have simp_rw : ∀ (x_1 : α),
  x_1 = x ∨ x_1 = y → ∀ (y_1 : α), y_1 = x ∨ y_1 = y → x_1 ≠ y_1 → edist x y ≤ edist x_1 y_1 ∨ edist y x ≤ edist x_1 y_1
Tactic: simp_rw [le_einfsep_iff, inf_le_iff, mem_insert_iff, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
x y : α
hxy : x ≠ y
⊢ einfsep (α := α) {x, y} ≤ edist y x
have rw : einfsep (α := α) {y, x} ≤ edist y x
Tactic: rw [pair_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
⊢ s.einfsep = ⨅ (d : (↑s.offDiag : Type u_1)), uncurry edist (↑d : α × α)
have refine : ∀ (x : ℝ≥0∞), x ≤ s.einfsep ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry edist (↑d : α × α)
Tactic: refine eq_of_forall_le_iff fun _ => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
x : ℝ≥0∞
⊢ x ≤ s.einfsep ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry edist (↑d : α × α)
have simp_rw : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ edist x_1 y) ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry edist (↑d : α × α)
Tactic: simp_rw [le_einfsep_iff, le_iInf_iff, imp_forall_iff, SetCoe.forall, mem_offDiag,
    Prod.forall, uncurry_apply_pair, and_imp]