-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
@[to_additive (attr := simp)]
lemma smul_Icc (a b c : α) : a • Icc b c = Icc (a * b) (a * c)

Proof state:
case h.mp
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
⊢ x ∈ a • Icc b c → x ∈ Icc (a * b) (a * c)

Tactic:
rintro ⟨y, ⟨hby, hyc⟩, rfl⟩

Result:
case h.mp.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c y : α
hby : b ≤ y
hyc : y ≤ c
⊢ (fun x => a • x) y ∈ Icc (a * b) (a * c)

Proof state:
case h
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
⊢ x ∈ a • Icc b c ↔ x ∈ Icc (a * b) (a * c)

Tactic:
constructor

Result:
case h.mp
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
⊢ x ∈ a • Icc b c → x ∈ Icc (a * b) (a * c)

case h.mpr
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
⊢ x ∈ Icc (a * b) (a * c) → x ∈ a • Icc b c

Proof state:
case h.mp.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c y : α
hby : b ≤ y
hyc : y ≤ c
⊢ (fun x => a • x) y ∈ Icc (a * b) (a * c)

Tactic:
exact ⟨mul_le_mul_left' hby _, mul_le_mul_left' hyc _⟩

Result:
no goals

Proof state:
case h.mpr
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
⊢ x ∈ Icc (a * b) (a * c) → x ∈ a • Icc b c

Tactic:
rintro ⟨habx, hxac⟩

Result:
case h.mpr.intro
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
habx : a * b ≤ x
hxac : x ≤ a * c
⊢ x ∈ a • Icc b c

Proof state:
case h.mpr.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c y : α
hy : 1 ≤ y
habx : a * b ≤ a * b * y
hxac : a * b * y ≤ a * c
⊢ a * b * y ∈ a • Icc b c

Tactic:
refine ⟨b * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, (mul_assoc ..).symm⟩

Result:
case h.mpr.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c y : α
hy : 1 ≤ y
habx : a * b ≤ a * b * y
hxac : a * b * y ≤ a * c
⊢ b * y ≤ c

Proof state:
case h.mpr.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c y : α
hy : 1 ≤ y
habx : a * b ≤ a * b * y
hxac : a * b * y ≤ a * c
⊢ b * y ≤ c

Tactic:
rwa [mul_assoc, mul_le_mul_iff_left] at hxac

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c : α
⊢ a • Icc b c = Icc (a * b) (a * c)

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
⊢ x ∈ a • Icc b c ↔ x ∈ Icc (a * b) (a * c)

Proof state:
case h.mpr.intro
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c x : α
habx : a * b ≤ x
hxac : x ≤ a * c
⊢ x ∈ a • Icc b c

Tactic:
obtain ⟨y, hy, rfl⟩ := exists_one_le_mul_of_le habx

Result:
case h.mpr.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c y : α
hy : 1 ≤ y
habx : a * b ≤ a * b * y
hxac : a * b * y ≤ a * c
⊢ a * b * y ∈ a • Icc b c