awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
pos : ∀ (hfg : MemHolder r f ∧ MemHolder r g), eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
neg : ∀ (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

Tactic:
by_cases hfg : MemHolder r f ∧ MemHolder r g

Premises used: MemHolder
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
hfg : MemHolder r f ∧ MemHolder r g
⊢ MemHolder r f

Tactic:
obtain ⟨hf, hg⟩ := hfg
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
hfg : MemHolder r f ∧ MemHolder r g
hf : MemHolder r f
⊢ MemHolder r g

Tactic:
obtain ⟨hf, hg⟩ := hfg
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
hf : MemHolder r f
hg : MemHolder r g
pos : nnHolderNorm r (f + g) ≤ nnHolderNorm r f + nnHolderNorm r g
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm 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]

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

Tactic:
hf.nnHolderNorm_add_le hg

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

Tactic:
exact hf.nnHolderNorm_add_le hg

Premises used: MemHolder.nnHolderNorm_add_le
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
hfg : ¬(MemHolder r f ∧ MemHolder r g)
⊢ eHolderNorm r f = ∞ ∨ eHolderNorm r g = ∞

Tactic:
rw [Classical.not_and_iff_not_or_not, ← eHolderNorm_eq_top, ← eHolderNorm_eq_top] at hfg

Premises used: eHolderNorm_eq_top, Classical.not_and_iff_not_or_not
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
hfg : eHolderNorm r f = ∞ ∨ eHolderNorm r g = ∞
neg : ∀ (h : eHolderNorm r f = ∞), eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
neg₁ : ∀ (h : eHolderNorm r g = ∞), eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g

Tactic:
obtain (h | h) := hfg
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
h : eHolderNorm r f = ∞
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g

Tactic:
simp [h]
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
h : eHolderNorm r g = ∞
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g

Tactic:
simp [h]
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
pos : ∀ (hc : ‖c‖₊ = 0), eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
neg : ∀ (hc : ¬‖c‖₊ = 0), eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
⊢ eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f

Tactic:
by_cases hc : ‖c‖₊ = 0
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ‖c‖₊ = 0
⊢ c = 0

Tactic:
rw [nnnorm_eq_zero] at hc

Premises used: nnnorm_eq_zero
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : 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

Tactic:
simp [hc]
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : 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
neg : ∀ (hf : ¬MemHolder r f), eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
⊢ eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f

Tactic:
by_cases hf : MemHolder r f

Premises used: MemHolder
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : 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

Tactic:
le_antisymm ((hf.holderWith.smul c).eHolderNorm_le.trans ?_) <| mul_le_of_le_div' ?_

Premises used: MemHolder.holderWith, le_antisymm, ENNReal.mul_le_of_le_div', LE.le.trans, HolderWith.eHolderNorm_le, HolderWith.smul
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : 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
pos₁ : eHolderNorm r f ≤ eHolderNorm r (c • f) / (↑‖c‖₊ : ℝ≥0∞)
⊢ eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f

Tactic:
refine le_antisymm ((hf.holderWith.smul c).eHolderNorm_le.trans ?_) <| mul_le_of_le_div' ?_

Premises used: MemHolder.holderWith, le_antisymm, ENNReal.mul_le_of_le_div', LE.le.trans, HolderWith.eHolderNorm_le, HolderWith.smul
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : 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
pos₂ pos₃ : (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f ≤ (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
⊢ (↑(nnHolderNorm r f * ‖c‖₊) : ℝ≥0∞) ≤ (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f

Tactic:
rw [coe_mul, hf.coe_nnHolderNorm_eq_eHolderNorm, mul_comm]

Premises used: MemHolder.coe_nnHolderNorm_eq_eHolderNorm, ENNReal.coe_mul, mul_comm
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
pos : eHolderNorm r f ≤ (↑(nnHolderNorm r (c • f) / ‖c‖₊) : ℝ≥0∞)
⊢ eHolderNorm r f ≤ eHolderNorm r (c • f) / (↑‖c‖₊ : ℝ≥0∞)

Tactic:
rw [← (hf.holderWith.smul c).memHolder.coe_nnHolderNorm_eq_eHolderNorm, ← coe_div hc]

Premises used: MemHolder.holderWith, MemHolder.coe_nnHolderNorm_eq_eHolderNorm, HolderWith.memHolder, HolderWith.smul, ENNReal.coe_div
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : 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∞)

Tactic:
HolderWith.eHolderNorm_le fun x₁ x₂ => ?_

Premises used: HolderWith.eHolderNorm_le
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
pos : ∀ (x₁ x₂ : X), edist (f x₁) (f x₂) ≤ (↑(nnHolderNorm r (c • f) / ‖c‖₊) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
⊢ eHolderNorm r f ≤ (↑(nnHolderNorm r (c • f) / ‖c‖₊) : ℝ≥0∞)

Tactic:
refine HolderWith.eHolderNorm_le fun x₁ x₂ => ?_

Premises used: HolderWith.eHolderNorm_le
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
x₁ x₂ : X
pos : edist ((c • f) x₁) ((c • f) x₂) ≤ (↑(nnHolderNorm r (c • f)) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)
⊢ edist (f x₁) (f x₂) ≤ (↑(nnHolderNorm r (c • f) / ‖c‖₊) : ℝ≥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]

Premises used: Iff.mpr, ENNReal.smul_def, ENNReal.mul_div_right_comm, ENNReal.le_div_iff_mul_le, edist_smul₀, ENNReal.coe_ne_zero, mul_comm, Or.inl, smul_eq_mul, ENNReal.coe_div, ENNReal.coe_ne_top, Pi.smul_apply
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
x₁ x₂ : X
⊢ edist ((c • f) x₁) ((c • f) x₂) ≤ (↑(nnHolderNorm r (c • f)) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
hf.smul.holderWith x₁ x₂

Premises used: MemHolder.holderWith, MemHolder.smul
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
x₁ x₂ : X
⊢ edist ((c • f) x₁) ((c • f) x₂) ≤ (↑(nnHolderNorm r (c • f)) : ℝ≥0∞) * edist x₁ x₂ ^ (↑r : ℝ)

Tactic:
exact hf.smul.holderWith x₁ x₂

Premises used: MemHolder.holderWith, MemHolder.smul
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : ¬MemHolder r f
⊢ eHolderNorm r f = ∞

Tactic:
rw [← eHolderNorm_eq_top] at hf

Premises used: eHolderNorm_eq_top
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : eHolderNorm r f = ∞
neg : ¬MemHolder r f
⊢ eHolderNorm r (c • f) = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f

Tactic:
rw [hf, mul_top <| coe_ne_zero.2 hc, eHolderNorm_eq_top, MemHolder.smul_iff hc]

Premises used: eHolderNorm_eq_top, ENNReal.mul_top, MemHolder.smul_iff
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : eHolderNorm r f = ∞
⊢ ¬c = 0

Tactic:
rw [nnnorm_eq_zero] at hc

Premises used: nnnorm_eq_zero
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : eHolderNorm r f = ∞
hc₁ : ¬c = 0
⊢ eHolderNorm r f = ∞

Tactic:
rw [nnnorm_eq_zero] at hc

Premises used: nnnorm_eq_zero
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst_2 : NormedRing α
inst_3 : Module α Y
inst_4 : NormSMulClass α Y
c : α
hc : ¬c = 0
hf : eHolderNorm r f = ∞
h : MemHolder r f
⊢ False

Tactic:
h.eHolderNorm_lt_top.ne hf

Premises used: MemHolder.eHolderNorm_lt_top, LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : 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 = ∞
h : MemHolder r f
⊢ False

Tactic:
exact h.eHolderNorm_lt_top.ne hf

Premises used: MemHolder.eHolderNorm_lt_top, LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : 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
rw₄ rw₅ : (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f = (↑‖c‖₊ : ℝ≥0∞) * eHolderNorm r f
⊢ nnHolderNorm r (c • f) = ‖c‖₊ * nnHolderNorm r f

Tactic:
rw [← ENNReal.coe_inj, coe_mul, hf.coe_nnHolderNorm_eq_eHolderNorm,
    hf.smul.coe_nnHolderNorm_eq_eHolderNorm, eHolderNorm_smul]

Premises used: MemHolder.coe_nnHolderNorm_eq_eHolderNorm, ENNReal.coe_inj, MemHolder.smul, ENNReal.coe_mul, eHolderNorm_smul
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
inst_2 : NormedSpace ℝ Y
n : ℕ
⊢ eHolderNorm r (n • f) = n • eHolderNorm r f

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

Premises used: Real, Nat.cast_smul_eq_nsmul, eHolderNorm_smul
-- Module: Mathlib.Topology.MetricSpace.HolderNorm
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
inst_2 : NormedSpace ℝ Y
n : ℕ
hf : MemHolder r f
⊢ nnHolderNorm r (n • f) = n • nnHolderNorm r f

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

Premises used: Real, MemHolder.nnHolderNorm_smul, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
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
⊢ s.einfsep = 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]

Premises used: exists_prop, iInf_lt_iff, iInf_eq_bot, Set.einfsep, bot_eq_zero
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
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
⊢ 0 < s.einfsep ↔ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y

Tactic:
rw [pos_iff_ne_zero, Ne, einfsep_zero]

Premises used: Set.einfsep_zero, Ne, pos_iff_ne_zero
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
⊢ (¬∀ 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:
simp only [not_forall, not_exists, not_lt, exists_prop, not_and]

Premises used: not_exists, exists_prop, not_lt, not_and, Classical.not_forall
-- Module: Mathlib.Topology.MetricSpace.Infsep
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 < ∞
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 < ∞
⊢ s.einfsep < ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ∞

Tactic:
simp_rw [einfsep, iInf_lt_iff, exists_prop]

Premises used: exists_prop, iInf_lt_iff, Set.einfsep
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
simp_rw : s.einfsep < ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ∞
⊢ s.einfsep ≠ ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y ≠ ∞

Tactic:
simp_rw [← lt_top_iff_ne_top, einfsep_lt_top]

Premises used: lt_top_iff_ne_top, Set.einfsep_lt_top
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
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
⊢ s.einfsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d

Tactic:
simp_rw [einfsep, iInf_lt_iff, exists_prop]

Premises used: exists_prop, iInf_lt_iff, Set.einfsep
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : s.einfsep < ∞
rcases : ∀ (w : α) (hx : w ∈ s) (w_1 : α) (hy : w_1 ∈ s) (hxy : w ≠ w_1), edist w w_1 < ∞ → s.Nontrivial
⊢ s.Nontrivial

Tactic:
rcases einfsep_lt_top.1 hs with ⟨_, hx, _, hy, hxy, _⟩

Premises used: Set.einfsep_lt_top, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : s.einfsep < ∞
w : α
hx : w ∈ s
w_1 : α
hy : w_1 ∈ s
hxy : w ≠ w_1
right : edist w w_1 < ∞
⊢ s.Nontrivial

Tactic:
⟨_, hx, _, hy, hxy⟩

Premises used: And.intro, Exists.intro, Set.Nontrivial
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : s.einfsep < ∞
w : α
hx : w ∈ s
w_1 : α
hy : w_1 ∈ s
hxy : w ≠ w_1
right : edist w w_1 < ∞
⊢ s.Nontrivial

Tactic:
exact ⟨_, hx, _, hy, hxy⟩
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : s.einfsep ≠ ∞
⊢ s.Nontrivial

Tactic:
nontrivial_of_einfsep_lt_top (lt_top_iff_ne_top.mpr hs)

Premises used: Iff.mpr, Set.nontrivial_of_einfsep_lt_top, lt_top_iff_ne_top
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : s.Subsingleton
rw : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ∞
⊢ s.einfsep = ∞

Tactic:
rw [einfsep_top]

Premises used: Set.einfsep_top
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : s.Subsingleton
⊢ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ∞

Tactic:
fun _ hx _ hy hxy => (hxy <| hs hx hy).elim

Premises used: False.elim
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : s.Subsingleton
⊢ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ∞

Tactic:
exact fun _ hx _ hy hxy => (hxy <| hs hx hy).elim
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
β : Type u_2
inst : EDist α
d : ℝ≥0∞
f : β → α
s : Set β
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)
⊢ d ≤ (f '' s).einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≠ f y → d ≤ edist (f x) (f y)

Tactic:
simp_rw [le_einfsep_iff, forall_mem_image]

Premises used: Set.le_einfsep_iff, Set.forall_mem_image
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
d : ℝ≥0∞
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ s.einfsep
⊢ d ≤ edist x y

Tactic:
le_einfsep_iff.1 hd x hx y hy hxy

Premises used: Set.le_einfsep_iff, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ s.einfsep ≤ edist x y

Tactic:
le_edist_of_le_einfsep hx hy hxy le_rfl

Premises used: le_rfl, Set.le_edist_of_le_einfsep
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
d : ℝ≥0∞
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hxy' : edist x y ≤ d
⊢ s.einfsep ≤ d

Tactic:
le_trans (einfsep_le_edist_of_mem hx hy hxy) hxy'

Premises used: Set.einfsep_le_edist_of_mem, le_trans
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
d : ℝ≥0∞
h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y
⊢ d ≤ s.einfsep

Tactic:
le_einfsep_iff.2 h

Premises used: Iff.mpr, Set.le_einfsep_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
⊢ einfsep.{u_1} (α := α) ∅ = ∞

Tactic:
subsingleton_empty.einfsep

Premises used: Set.subsingleton_empty, Set.Subsingleton.einfsep
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
x : α
⊢ einfsep (α := α) {x} = ∞

Tactic:
subsingleton_singleton.einfsep

Premises used: Set.subsingleton_singleton, Set.Subsingleton.einfsep
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
some : ∀ (val : ι), einfsep.{u_1} (α := α) (⋃ i ∈ Option.some val, s i) = ⨅ i ∈ Option.some val, (s i).einfsep
⊢ einfsep.{u_1} (α := α) (⋃ i ∈ o, s i) = ⨅ i ∈ o, (s i).einfsep

Tactic:
cases o
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
ι : Type u_3
s : ι → Set α
⊢ einfsep.{u_1} (α := α) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Option ι) none i), s i) =
    ⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Option ι) none i), (s i).einfsep

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
ι : Type u_3
s : ι → Set α
val : ι
⊢ einfsep.{u_1} (α := α) (⋃ i ∈ some val, s i) = ⨅ i ∈ some val, (s i).einfsep

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s t : Set α
hst : s ⊆ t
⊢ t.einfsep ≤ s.einfsep

Tactic:
le_einfsep fun _x hx _y hy => einfsep_le_edist_of_mem (hst hx) (hst hy)

Premises used: Set.einfsep_le_edist_of_mem, Set.le_einfsep
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
x : α
s : Set α
simp_rw : ∀ (i : α) (i_1 : i ∈ s) (i_2 : x ≠ i), (insert x s).einfsep ≤ edist x i
⊢ (insert x s).einfsep ≤ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y

Tactic:
simp_rw [le_iInf_iff]

Premises used: le_iInf_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
x : α
s : Set α
⊢ ∀ (i : α) (i_1 : i ∈ s) (i_2 : x ≠ i), (insert x s).einfsep ≤ edist x i

Tactic:
fun _ hy hxy => einfsep_le_edist_of_mem (mem_insert _ _) (mem_insert_of_mem _ hy) hxy

Premises used: Set.einfsep_le_edist_of_mem, Set.mem_insert_of_mem, Set.mem_insert
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
x : α
s : Set α
⊢ ∀ (i : α) (i_1 : i ∈ s) (i_2 : x ≠ i), (insert x s).einfsep ≤ edist x i

Tactic:
exact fun _ hy hxy => einfsep_le_edist_of_mem (mem_insert _ _) (mem_insert_of_mem _ hy) hxy

Premises used: Set.einfsep_le_edist_of_mem, Set.mem_insert_of_mem, Set.mem_insert
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
x y : α
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
⊢ min (edist x y) (edist y x) ≤ einfsep (α := α) {x, y}

Tactic:
simp_rw [le_einfsep_iff, inf_le_iff, mem_insert_iff, mem_singleton_iff]

Premises used: inf_le_iff, Set.le_einfsep_iff, Set.mem_singleton_iff, Set.mem_insert_iff