-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
@[to_additive]
lemma Icc_mul_Icc (hab : a ≤ b) (hcd : c ≤ d) : Icc a b * Icc c d = Icc (a * c) (b * d)

Proof state:
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
x : α
x✝ : x ∈ Icc (a * c) (b * d)
hacx : a * c ≤ x
hxbd : x ≤ b * d
⊢ x ∈ Icc a b * Icc c d

Tactic:
obtain hxbc | hbcx := le_total x (b * c)

Result:
case inl
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
x : α
x✝ : x ∈ Icc (a * c) (b * d)
hacx : a * c ≤ x
hxbd : x ≤ b * d
hxbc : x ≤ b * c
⊢ x ∈ Icc a b * Icc c d

case inr
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
x : α
x✝ : x ∈ Icc (a * c) (b * d)
hacx : a * c ≤ x
hxbd : x ≤ b * d
hbcx : b * c ≤ x
⊢ x ∈ Icc a b * Icc c d

Proof state:
case inr
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
x : α
x✝ : x ∈ Icc (a * c) (b * d)
hacx : a * c ≤ x
hxbd : x ≤ b * d
hbcx : b * c ≤ x
⊢ x ∈ Icc a b * Icc c d

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

Result:
case inr.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : b * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ b * c * y
hxbd : b * c * y ≤ b * d
hbcx : b * c ≤ b * c * y
⊢ b * c * y ∈ Icc a b * Icc c d

Proof state:
case inl.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : a * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ a * c * y
hxbd : a * c * y ≤ b * d
hxbc : a * c * y ≤ b * c
⊢ a * y ≤ b

Tactic:
rwa [mul_right_comm, mul_le_mul_iff_right] at hxbc

Result:
no goals

Proof state:
case inr.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : b * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ b * c * y
hxbd : b * c * y ≤ b * d
hbcx : b * c ≤ b * c * y
⊢ b * c * y ∈ Icc a b * Icc c d

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

Result:
case inr.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : b * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ b * c * y
hxbd : b * c * y ≤ b * d
hbcx : b * c ≤ b * c * y
⊢ c * y ≤ d

Proof state:
case inl.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : a * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ a * c * y
hxbd : a * c * y ≤ b * d
hxbc : a * c * y ≤ b * c
⊢ a * c * y ∈ Icc a b * Icc c d

Tactic:
refine ⟨a * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, c, left_mem_Icc.2 hcd, mul_right_comm ..⟩

Result:
case inl.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : a * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ a * c * y
hxbd : a * c * y ≤ b * d
hxbc : a * c * y ≤ b * c
⊢ a * y ≤ b

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

Tactic:
refine (Icc_mul_Icc_subset' _ _ _ _).antisymm fun x ⟨hacx, hxbd⟩ ↦ ?_

Result:
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
x : α
x✝ : x ∈ Icc (a * c) (b * d)
hacx : a * c ≤ x
hxbd : x ≤ b * d
⊢ x ∈ Icc a b * Icc c d

Proof state:
case inl
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
x : α
x✝ : x ∈ Icc (a * c) (b * d)
hacx : a * c ≤ x
hxbd : x ≤ b * d
hxbc : x ≤ b * c
⊢ x ∈ Icc a b * Icc c d

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

Result:
case inl.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : a * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ a * c * y
hxbd : a * c * y ≤ b * d
hxbc : a * c * y ≤ b * c
⊢ a * c * y ∈ Icc a b * Icc c d

Proof state:
case inr.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : b * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ b * c * y
hxbd : b * c * y ≤ b * d
hbcx : b * c ≤ b * c * y
⊢ c * y ≤ d

Tactic:
rwa [mul_assoc, mul_le_mul_iff_left] at hxbd

Result:
no goals