awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b : α
this : MulRightMono α
y : α
hya : y ∈ Iic a
z : α
hzb : z ∈ Iio b
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Iio (a * b)

Tactic:
mul_lt_mul_of_le_of_lt hya hzb

Premises used: Set.Mem, setOf, mul_lt_mul_of_le_of_lt, Set.Iio
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b : α
this : MulRightMono α
y : α
hya : y ∈ Iic a
z : α
hzb : z ∈ Iio b
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Iio (a * b)

Tactic:
exact mul_lt_mul_of_le_of_lt hya hzb

Premises used: mul_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b : α
⊢ MulLeftMono α

Tactic:
have := mulLeftMono_of_mulLeftStrictMono α
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b : α
this : MulLeftMono α
y : α
hya : y ∈ Iio a
z : α
hzb : z ∈ Iic b
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Iio (a * b)

Tactic:
mul_lt_mul_of_lt_of_le hya hzb

Premises used: Set.Mem, setOf, Set.Iio, mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b : α
this : MulLeftMono α
y : α
hya : y ∈ Iio a
z : α
hzb : z ∈ Iic b
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Iio (a * b)

Tactic:
exact mul_lt_mul_of_lt_of_le hya hzb

Premises used: mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b : α
this : MulLeftMono α
y : α
hya : y ∈ Ioi a
z : α
hzb : z ∈ Ici b
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Ioi (a * b)

Tactic:
mul_lt_mul_of_lt_of_le hya hzb

Premises used: Set.Ioi, Set.Mem, setOf, mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b : α
this : MulLeftMono α
y : α
hya : y ∈ Ioi a
z : α
hzb : z ∈ Ici b
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Ioi (a * b)

Tactic:
exact mul_lt_mul_of_lt_of_le hya hzb

Premises used: mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b : α
this : MulRightMono α
y : α
hya : y ∈ Ici a
z : α
hzb : z ∈ Ioi b
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Ioi (a * b)

Tactic:
mul_lt_mul_of_le_of_lt hya hzb

Premises used: Set.Ioi, Set.Mem, setOf, mul_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b : α
this : MulRightMono α
y : α
hya : y ∈ Ici a
z : α
hzb : z ∈ Ioi b
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Ioi (a * b)

Tactic:
exact mul_lt_mul_of_le_of_lt hya hzb

Premises used: mul_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c : α
h : ∀ (x : α), x ∈ a • Icc b c ↔ x ∈ Icc (a * b) (a * c)
⊢ a • Icc b c = Icc (a * b) (a * c)

Tactic:
ext x
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c x : α
h : x ∈ a • Icc b c → x ∈ Icc (a * b) (a * c)
h₁ : x ∈ Icc (a * b) (a * c) → x ∈ a • Icc b c
⊢ x ∈ a • Icc b c ↔ x ∈ Icc (a * b) (a * c)

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c y : α
hby : b ≤ y
hyc : y ≤ c
h : a * y ∈ Icc (a * b) (a * c)
⊢ (fun (x : α) ↦ a • x) y ∈ Icc (a * b) (a * c)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c y : α
hby : b ≤ y
hyc : y ≤ c
h : a * b ≤ a * y
h₁ : a * y ≤ a * c
⊢ a * y ∈ Icc (a * b) (a * c)

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c y : α
hby : b ≤ y
hyc : y ≤ c
⊢ a * b ≤ a * y

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c y : α
hby : b ≤ y
hyc : y ≤ c
⊢ a * y ≤ a * c

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c x : α
habx : a * b ≤ x
hxac : x ≤ a * c
h : ∀ (y : α) (hy : 1 ≤ y) (habx : a * b ≤ a * b * y) (hxac : a * b * y ≤ a * c), a * b * y ∈ a • Icc b c
⊢ x ∈ a • Icc b c

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

Premises used: exists_one_le_mul_of_le, rfl
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : 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:
⟨b * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, (mul_assoc ..).symm⟩

Premises used: HMul.hMul, Set.Mem, mul_assoc, setOf, And.intro, Exists.intro, Set.image, le_mul_of_one_le_right', Eq.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c y : α
hy : 1 ≤ y
habx : a * b ≤ a * b * y
hxac : a * b * y ≤ a * c
h : b * y ≤ c
⊢ a * b * y ∈ a • Icc b c

Tactic:
refine ⟨b * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, (mul_assoc ..).symm⟩
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c y : α
hy : 1 ≤ y
habx : a * b ≤ a * b * y
hxac : a * b * y ≤ a * c
h : ∀ (hxac : a * (b * y) ≤ a * c), b * y ≤ c
h₁ h₂ h₃ h₄ : ∀ (hxac : b * y ≤ c), b * y ≤ c
⊢ b * y ≤ c

Tactic:
rwa [mul_assoc, mul_le_mul_iff_left] at hxac

Premises used: mul_assoc, mul_le_mul_iff_left
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ Icc a b * Icc c d = Icc (a * c) (b * d)

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

Premises used: _private.0.Set.Icc_mul_Icc.match_1, HMul.hMul, Set.Icc_mul_Icc_subset', Membership.mem, Set.Icc, HasSubset.Subset.antisymm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
refine : ∀ x ∈ Icc (a * c) (b * d), ∀ (hacx : a * c ≤ x) (hxbd : x ≤ b * d), x ∈ Icc a b * Icc c d
⊢ Icc a b * Icc c d = Icc (a * c) (b * d)

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

Premises used: Set.Icc_mul_Icc_subset', HasSubset.Subset.antisymm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
x : α
h : x ∈ Icc (a * c) (b * d)
hacx : a * c ≤ x
hxbd : x ≤ b * d
inl : ∀ (hxbc : x ≤ b * c), x ∈ Icc a b * Icc c d
inr : ∀ (hbcx : b * c ≤ x), x ∈ Icc a b * Icc c d
⊢ x ∈ Icc a b * Icc c d

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

Premises used: HMul.hMul, le_total
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
x : α
h : x ∈ Icc (a * c) (b * d)
hacx : a * c ≤ x
hxbd : x ≤ b * d
hxbc : x ≤ b * c
inl :
  ∀ (y : α) (hy : 1 ≤ y),
    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
⊢ x ∈ Icc a b * Icc c d

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

Premises used: exists_one_le_mul_of_le, rfl
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
h : 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:
⟨a * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, c, left_mem_Icc.2 hcd, mul_right_comm ..⟩

Premises used: Iff.mpr, HMul.hMul, Set.Mem, setOf, Set.left_mem_Icc, mul_right_comm, Set.image2, And.intro, Exists.intro, le_mul_of_one_le_right'
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
h : 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
inl : a * y ≤ b
⊢ 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 ..⟩
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
h : 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
inl : ∀ (hxbc : a * y * c ≤ b * c), a * y ≤ b
inl₁ inl₂ inl₃ inl₄ : ∀ (hxbc : a * y ≤ b), a * y ≤ b
⊢ a * y ≤ b

Tactic:
rwa [mul_right_comm, mul_le_mul_iff_right] at hxbc

Premises used: mul_le_mul_iff_right, mul_right_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
x : α
h : x ∈ Icc (a * c) (b * d)
hacx : a * c ≤ x
hxbd : x ≤ b * d
hbcx : b * c ≤ x
inr :
  ∀ (y : α) (hy : 1 ≤ y),
    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
⊢ x ∈ Icc a b * Icc c d

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

Premises used: exists_one_le_mul_of_le, rfl
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
h : 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:
⟨b, right_mem_Icc.2 hab, c * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, (mul_assoc ..).symm⟩

Premises used: Iff.mpr, Set.right_mem_Icc, HMul.hMul, Set.Mem, mul_assoc, setOf, Set.image2, And.intro, Exists.intro, le_mul_of_one_le_right', Eq.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
h : 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
inr : c * y ≤ d
⊢ 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⟩
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
h : 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
inr : ∀ (hxbd : b * (c * y) ≤ b * d) (hbcx : b * c ≤ b * c * y), c * y ≤ d
inr₁ inr₂ inr₃ inr₄ : ∀ (hxbd : c * y ≤ d) (hbcx : b * c ≤ b * c * y), c * y ≤ d
⊢ c * y ≤ d

Tactic:
rwa [mul_assoc, mul_le_mul_iff_left] at hxbd

Premises used: mul_assoc, mul_le_mul_iff_left
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ (Ici a)⁻¹ = Iic a⁻¹

Tactic:
ext fun _x ↦ le_inv'

Premises used: Set.ext, le_inv'
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ (Iic a)⁻¹ = Ici a⁻¹

Tactic:
ext fun _x ↦ inv_le'

Premises used: inv_le', Set.ext
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ (Ioi a)⁻¹ = Iio a⁻¹

Tactic:
ext fun _x ↦ lt_inv'

Premises used: Set.ext, lt_inv'
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ (Iio a)⁻¹ = Ioi a⁻¹

Tactic:
ext fun _x ↦ inv_lt'

Premises used: inv_lt', Set.ext
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (Icc a b)⁻¹ = Icc b⁻¹ a⁻¹

Tactic:
simp [← Ici_inter_Iic, inter_comm]

Premises used: Set.inter_comm, Set.Ici_inter_Iic
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (Ico a b)⁻¹ = Ioc b⁻¹ a⁻¹

Tactic:
simp [← Ici_inter_Iio, ← Ioi_inter_Iic, inter_comm]

Premises used: Set.Ioi_inter_Iic, Set.Ici_inter_Iio, Set.inter_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (Ioc a b)⁻¹ = Ico b⁻¹ a⁻¹

Tactic:
simp [← Ioi_inter_Iic, ← Ici_inter_Iio, inter_comm]

Premises used: Set.Ioi_inter_Iic, Set.Ici_inter_Iio, Set.inter_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (Ioo a b)⁻¹ = Ioo b⁻¹ a⁻¹

Tactic:
simp [← Ioi_inter_Iio, inter_comm]

Premises used: Set.inter_comm, Set.Ioi_inter_Iio
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ a * x) ⁻¹' Ici b = Ici (b / a)

Tactic:
ext fun _x => div_le_iff_le_mul'.symm

Premises used: Set.ext, div_le_iff_le_mul', Iff.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ a * x) ⁻¹' Ioi b = Ioi (b / a)

Tactic:
ext fun _x => div_lt_iff_lt_mul'.symm

Premises used: Set.ext, div_lt_iff_lt_mul', Iff.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ a * x) ⁻¹' Iic b = Iic (b / a)

Tactic:
ext fun _x => le_div_iff_mul_le'.symm

Premises used: Set.ext, le_div_iff_mul_le', Iff.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ a * x) ⁻¹' Iio b = Iio (b / a)

Tactic:
ext fun _x => lt_div_iff_mul_lt'.symm

Premises used: Set.ext, lt_div_iff_mul_lt', Iff.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ a * x) ⁻¹' Icc b c = Icc (b / a) (c / a)

Tactic:
simp [← Ici_inter_Iic]

Premises used: Set.Ici_inter_Iic
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ a * x) ⁻¹' Ico b c = Ico (b / a) (c / a)

Tactic:
simp [← Ici_inter_Iio]

Premises used: Set.Ici_inter_Iio
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ a * x) ⁻¹' Ioc b c = Ioc (b / a) (c / a)

Tactic:
simp [← Ioi_inter_Iic]

Premises used: Set.Ioi_inter_Iic
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ a * x) ⁻¹' Ioo b c = Ioo (b / a) (c / a)

Tactic:
simp [← Ioi_inter_Iio]

Premises used: Set.Ioi_inter_Iio
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ x * a) ⁻¹' Ici b = Ici (b / a)

Tactic:
ext fun _x => div_le_iff_le_mul.symm

Premises used: Set.ext, div_le_iff_le_mul, Iff.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ x * a) ⁻¹' Ioi b = Ioi (b / a)

Tactic:
ext fun _x => div_lt_iff_lt_mul.symm

Premises used: Set.ext, Iff.symm, div_lt_iff_lt_mul
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ x * a) ⁻¹' Iic b = Iic (b / a)

Tactic:
ext fun _x => le_div_iff_mul_le.symm

Premises used: Set.ext, Iff.symm, le_div_iff_mul_le
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ x * a) ⁻¹' Iio b = Iio (b / a)

Tactic:
ext fun _x => lt_div_iff_mul_lt.symm

Premises used: Set.ext, lt_div_iff_mul_lt, Iff.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ x * a) ⁻¹' Icc b c = Icc (b / a) (c / a)

Tactic:
simp [← Ici_inter_Iic]

Premises used: Set.Ici_inter_Iic
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ x * a) ⁻¹' Ico b c = Ico (b / a) (c / a)

Tactic:
simp [← Ici_inter_Iio]

Premises used: Set.Ici_inter_Iio
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ x * a) ⁻¹' Ioc b c = Ioc (b / a) (c / a)

Tactic:
simp [← Ioi_inter_Iic]

Premises used: Set.Ioi_inter_Iic
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ x * a) ⁻¹' Ioo b c = Ioo (b / a) (c / a)

Tactic:
simp [← Ioi_inter_Iio]

Premises used: Set.Ioi_inter_Iio
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ x / a) ⁻¹' Ici b = Ici (b * a)

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ x / a) ⁻¹' Ioi b = Ioi (b * a)

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ x / a) ⁻¹' Iic b = Iic (b * a)

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ x / a) ⁻¹' Iio b = Iio (b * a)

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ x / a) ⁻¹' Icc b c = Icc (b * a) (c * a)

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ x / a) ⁻¹' Ico b c = Ico (b * a) (c * a)

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ x / a) ⁻¹' Ioc b c = Ioc (b * a) (c * a)

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ x / a) ⁻¹' Ioo b c = Ioo (b * a) (c * a)

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ a / x) ⁻¹' Ici b = Iic (a / b)

Tactic:
ext fun _x => le_div_comm

Premises used: Set.ext, le_div_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ a / x) ⁻¹' Iic b = Ici (a / b)

Tactic:
ext fun _x => div_le_comm

Premises used: Set.ext, div_le_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ a / x) ⁻¹' Ioi b = Iio (a / b)

Tactic:
ext fun _x => lt_div_comm

Premises used: Set.ext, lt_div_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ a / x) ⁻¹' Iio b = Ioi (a / b)

Tactic:
ext fun _x => div_lt_comm

Premises used: Set.ext, div_lt_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ a / x) ⁻¹' Icc b c = Icc (a / c) (a / b)

Tactic:
simp [← Ici_inter_Iic, inter_comm]

Premises used: Set.inter_comm, Set.Ici_inter_Iic
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ a / x) ⁻¹' Ico b c = Ioc (a / c) (a / b)

Tactic:
simp [← Ioi_inter_Iic, ← Ici_inter_Iio, inter_comm]

Premises used: Set.Ioi_inter_Iic, Set.Ici_inter_Iio, Set.inter_comm