-- 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 pos.refine_1
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
⊢ ↑(nnHolderNorm r f * ‖c‖₊) ≤ ↑‖c‖₊ * eHolderNorm r f

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

Result:
no goals

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 ((c • f) x₁) ((c • f) x₂) ≤ ↑(nnHolderNorm r (c • f)) * edist x₁ x₂ ^ ↑r

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

Result:
no goals

Proof state:
case pos
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
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Tactic:
rw [nnnorm_eq_zero] at hc

Result:
case pos
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
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Proof state:
case pos
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
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Tactic:
simp [hc]

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 = ⊤
h : MemHolder r (c • f)
⊢ False

Tactic:
have := h.smul (c := c⁻¹)

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 (c⁻¹ • c • f)
⊢ False

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
⊢ eHolderNorm r f ≤ eHolderNorm r (c • f) / ↑‖c‖₊

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

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
⊢ eHolderNorm r f ≤ ↑(nnHolderNorm r (c • f) / ‖c‖₊)

Proof state:
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 : α
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Tactic:
by_cases hc : ‖c‖₊ = 0

Result:
case pos
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
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

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
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Proof state:
case pos
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:
refine le_antisymm ((hf.holderWith.smul c).eHolderNorm_le.trans ?_) <| mul_le_of_le_div' ?_

Result:
case pos.refine_1
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
⊢ ↑(nnHolderNorm r f * ‖c‖₊) ≤ ↑‖c‖₊ * eHolderNorm r f

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
⊢ eHolderNorm r f ≤ eHolderNorm r (c • f) / ↑‖c‖₊

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 = ⊤
⊢ ¬MemHolder r (c • f)

Tactic:
intro h

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)
⊢ False

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
⊢ eHolderNorm r f ≤ ↑(nnHolderNorm r (c • f) / ‖c‖₊)

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

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 (f x₁) (f x₂) ≤ ↑(nnHolderNorm r (c • f) / ‖c‖₊) * edist x₁ x₂ ^ ↑r

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
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Tactic:
by_cases hf : MemHolder r f

Result:
case pos
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

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

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 = ⊤
⊢ ¬MemHolder r (c • f)

Tactic:
rw [nnnorm_eq_zero] at hc

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)