-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem ediam_smul₀ (c : 𝕜) (s : Set E) : EMetric.diam (c • s) = ‖c‖₊ • EMetric.diam s

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
⊢ ‖c‖₊ • EMetric.diam s ≤ EMetric.diam (c • s)

Tactic:
have := (lipschitzWith_smul c⁻¹).ediam_image_le (c • s)

Result:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : EMetric.diam ((fun x => c⁻¹ • x) '' (c • s)) ≤ ↑‖c⁻¹‖₊ * EMetric.diam (c • s)
⊢ ‖c‖₊ • EMetric.diam s ≤ EMetric.diam (c • s)

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : EMetric.diam ((fun x => c⁻¹ • x) '' (c • s)) ≤ ↑‖c⁻¹‖₊ * EMetric.diam (c • s)
⊢ ‖c‖₊ • EMetric.diam s ≤ EMetric.diam (c • s)

Tactic:
rwa [← smul_eq_mul, ← ENNReal.smul_def, Set.image_smul, inv_smul_smul₀ hc s, nnnorm_inv,
  le_inv_smul_iff_of_pos (nnnorm_pos.2 hc)] at this

Result:
no goals

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
s : Set E
⊢ ‖0‖₊ • EMetric.diam s ≤ EMetric.diam (0 • s)

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Result:
case inl.inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
⊢ ‖0‖₊ • EMetric.diam ∅ ≤ EMetric.diam (0 • ∅)

case inl.inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
s : Set E
hs : s.Nonempty
⊢ ‖0‖₊ • EMetric.diam s ≤ EMetric.diam (0 • s)

Proof state:
case inl.inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
⊢ ‖0‖₊ • EMetric.diam ∅ ≤ EMetric.diam (0 • ∅)

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
s : Set E
⊢ EMetric.diam (c • s) = ‖c‖₊ • EMetric.diam s

Tactic:
refine le_antisymm (ediam_smul_le c s) ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
s : Set E
⊢ ‖c‖₊ • EMetric.diam s ≤ EMetric.diam (c • s)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
s : Set E
⊢ ‖c‖₊ • EMetric.diam s ≤ EMetric.diam (c • s)

Tactic:
obtain rfl | hc := eq_or_ne c 0

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
s : Set E
⊢ ‖0‖₊ • EMetric.diam s ≤ EMetric.diam (0 • s)

case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
⊢ ‖c‖₊ • EMetric.diam s ≤ EMetric.diam (c • s)

Proof state:
case inl.inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
s : Set E
hs : s.Nonempty
⊢ ‖0‖₊ • EMetric.diam s ≤ EMetric.diam (0 • s)

Tactic:
simp [zero_smul_set hs, ← Set.singleton_zero]

Result:
no goals