-- Mathlib/Analysis/Convex/Body.lean
theorem smul_le_of_le (K : ConvexBody V) (h_zero : 0 ∈ K) {a b : ℝ≥0} (h : a ≤ b) :
    a • K ≤ b • K

Proof state:
case inl
V : Type u_1
inst✝⁴ : TopologicalSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : ContinuousAdd V
K : ConvexBody V
h_zero : 0 ∈ K
b : ℝ≥0
h : 0 ≤ b
⊢ 0 ∈ b • ↑K

Tactic:
exact Set.mem_smul_set.mpr ⟨0, h_zero, smul_zero _⟩

Result:
no goals

Proof state:
case inr
V : Type u_1
inst✝⁴ : TopologicalSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : ContinuousAdd V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
⊢ a • ↑K ⊆ b • ↑K

Tactic:
intro x hx

Result:
case inr
V : Type u_1
inst✝⁴ : TopologicalSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : ContinuousAdd V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
x : V
hx : x ∈ a • ↑K
⊢ x ∈ b • ↑K

Proof state:
case inl
V : Type u_1
inst✝⁴ : TopologicalSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : ContinuousAdd V
K : ConvexBody V
h_zero : 0 ∈ K
b : ℝ≥0
h : 0 ≤ b
⊢ 0 • ↑K ⊆ b • ↑K

Tactic:
rw [Set.zero_smul_set K.nonempty, Set.zero_subset]

Result:
case inl
V : Type u_1
inst✝⁴ : TopologicalSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : ContinuousAdd V
K : ConvexBody V
h_zero : 0 ∈ K
b : ℝ≥0
h : 0 ≤ b
⊢ 0 ∈ b • ↑K

Proof state:
case inr.intro.intro
V : Type u_1
inst✝⁴ : TopologicalSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : ContinuousAdd V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
y : V
hy : y ∈ ↑K
hx : a • y ∈ a • ↑K
⊢ a • y ∈ b • ↑K

Tactic:
rw [← Set.mem_inv_smul_set_iff₀ ha.ne', smul_smul]

Result:
case inr.intro.intro
V : Type u_1
inst✝⁴ : TopologicalSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : ContinuousAdd V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
y : V
hy : y ∈ ↑K
hx : a • y ∈ a • ↑K
⊢ y ∈ (a⁻¹ * b) • ↑K

Proof state:
case inr.intro.intro
V : Type u_1
inst✝⁴ : TopologicalSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : ContinuousAdd V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
y : V
hy : y ∈ ↑K
hx : a • y ∈ a • ↑K
⊢ 1 ≤ a⁻¹ * b

Tactic:
rwa [le_inv_mul_iff₀ ha, mul_one]

Result:
no goals

Proof state:
V : Type u_1
inst✝⁴ : TopologicalSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : ContinuousAdd V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
⊢ a • ↑K ⊆ b • ↑K

Tactic:
obtain rfl | ha := eq_zero_or_pos a

Result:
case inl
V : Type u_1
inst✝⁴ : TopologicalSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : ContinuousAdd V
K : ConvexBody V
h_zero : 0 ∈ K
b : ℝ≥0
h : 0 ≤ b
⊢ 0 • ↑K ⊆ b • ↑K

case inr
V : Type u_1
inst✝⁴ : TopologicalSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : ContinuousAdd V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
⊢ a • ↑K ⊆ b • ↑K

Proof state:
V : Type u_1
inst✝⁴ : TopologicalSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : ContinuousAdd V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
⊢ a • K ≤ b • K

Tactic:
rw [← SetLike.coe_subset_coe, coe_smul', coe_smul']

Result:
V : Type u_1
inst✝⁴ : TopologicalSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : ContinuousAdd V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
⊢ a • ↑K ⊆ b • ↑K

Proof state:
case inr
V : Type u_1
inst✝⁴ : TopologicalSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : ContinuousAdd V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
x : V
hx : x ∈ a • ↑K
⊢ x ∈ b • ↑K

Tactic:
obtain ⟨y, hy, rfl⟩ := Set.mem_smul_set.mp hx

Result:
case inr.intro.intro
V : Type u_1
inst✝⁴ : TopologicalSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : ContinuousAdd V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
y : V
hy : y ∈ ↑K
hx : a • y ∈ a • ↑K
⊢ a • y ∈ b • ↑K

Proof state:
case inr.intro.intro
V : Type u_1
inst✝⁴ : TopologicalSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : ContinuousAdd V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
y : V
hy : y ∈ ↑K
hx : a • y ∈ a • ↑K
⊢ y ∈ (a⁻¹ * b) • ↑K

Tactic:
refine Convex.mem_smul_of_zero_mem K.convex h_zero hy (?_ : 1 ≤ a⁻¹ * b)

Result:
case inr.intro.intro
V : Type u_1
inst✝⁴ : TopologicalSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : ContinuousAdd V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
y : V
hy : y ∈ ↑K
hx : a • y ∈ a • ↑K
⊢ 1 ≤ a⁻¹ * b