-- Mathlib/Topology/MetricSpace/HolderNorm.lean
lemma eHolderNorm_smul {α} [NormedDivisionRing α] [Module α Y] [BoundedSMul α Y] (c : α) :
    eHolderNorm r (c • f) = ‖c‖₊ * eHolderNorm r f

Proof state:
case neg
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedDivisionRing α
inst✝¹ : Module α Y
inst✝ : BoundedSMul α Y
c : α
hc : ¬c = 0
hf : eHolderNorm r f = ⊤
h : MemHolder r (c • f)
this : MemHolder r (c⁻¹ • c • f)
⊢ False

Tactic:
rw [inv_smul_smul₀ hc] at this

Result:
case neg
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedDivisionRing α
inst✝¹ : Module α Y
inst✝ : BoundedSMul α Y
c : α
hc : ¬c = 0
hf : eHolderNorm r f = ⊤
h : MemHolder r (c • f)
this : MemHolder r f
⊢ False

Proof state:
case neg
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedDivisionRing α
inst✝¹ : Module α Y
inst✝ : BoundedSMul α Y
c : α
hc : ¬‖c‖₊ = 0
hf : ¬MemHolder r f
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Tactic:
rw [← eHolderNorm_eq_top] at hf

Result:
case neg
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedDivisionRing α
inst✝¹ : Module α Y
inst✝ : BoundedSMul α Y
c : α
hc : ¬‖c‖₊ = 0
hf : eHolderNorm r f = ⊤
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Proof state:
case neg
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedDivisionRing α
inst✝¹ : Module α Y
inst✝ : BoundedSMul α Y
c : α
hc : ¬c = 0
hf : eHolderNorm r f = ⊤
h : MemHolder r (c • f)
this : MemHolder r f
⊢ False

Tactic:
exact this.eHolderNorm_lt_top.ne hf

Result:
no goals

Proof state:
case neg
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedDivisionRing α
inst✝¹ : Module α Y
inst✝ : BoundedSMul α Y
c : α
hc : ¬‖c‖₊ = 0
hf : eHolderNorm r f = ⊤
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

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

Result:
case neg
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedDivisionRing α
inst✝¹ : Module α Y
inst✝ : BoundedSMul α Y
c : α
hc : ¬‖c‖₊ = 0
hf : eHolderNorm r f = ⊤
⊢ ¬MemHolder r (c • f)

Proof state:
case pos.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedDivisionRing α
inst✝¹ : Module α Y
inst✝ : BoundedSMul α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
x₁ x₂ : X
⊢ edist (f x₁) (f x₂) ≤ ↑(nnHolderNorm r (c • f) / ‖c‖₊) * 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]

Result:
case pos.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedDivisionRing α
inst✝¹ : Module α Y
inst✝ : BoundedSMul α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
x₁ x₂ : X
⊢ edist ((c • f) x₁) ((c • f) x₂) ≤ ↑(nnHolderNorm r (c • f)) * edist x₁ x₂ ^ ↑r