awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
b c : G₀
hbc : b ≤ c
ha : LE.le.{u_2} (α := G₀) 0 0
⊢ (fun (x : G₀) ↦ 0 * x) '' Icc b c = Icc (0 * b) (0 * c)

Tactic:
simp [(nonempty_Icc.2 hbc).image_const]

Premises used: Iff.mpr, Set.Nonempty.image_const, Set.nonempty_Icc
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
ha_1 : 0 ≤ a
hbc : b ≤ c
ha : 0 < a
⊢ (fun (x : G₀) ↦ a * x) '' Icc b c = Icc (a * b) (a * c)

Tactic:
image_mul_left_Icc' ha b c

Premises used: Set.image_mul_left_Icc'
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
ha_1 : 0 ≤ a
hbc : b ≤ c
ha : 0 < a
⊢ (fun (x : G₀) ↦ a * x) '' Icc b c = Icc (a * b) (a * c)

Tactic:
exact image_mul_left_Icc' ha b c

Premises used: Set.image_mul_left_Icc'
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
h : 0 < a
b c : G₀
⊢ (fun (x : G₀) ↦ a * x) '' Ioo b c = Ioo (a * b) (a * c)

Tactic:
(OrderIso.mulLeft₀ a h).image_Ioo b c

Premises used: OrderIso.mulLeft₀, OrderIso.image_Ioo
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
h : 0 < a
b c : G₀
⊢ (fun (x : G₀) ↦ a * x) '' Ico b c = Ico (a * b) (a * c)

Tactic:
(OrderIso.mulLeft₀ a h).image_Ico b c

Premises used: OrderIso.image_Ico, OrderIso.mulLeft₀
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
h : 0 < a
b c : G₀
⊢ (fun (x : G₀) ↦ a * x) '' Ioc b c = Ioc (a * b) (a * c)

Tactic:
(OrderIso.mulLeft₀ a h).image_Ioc b c

Premises used: OrderIso.mulLeft₀, OrderIso.image_Ioc
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
ha : 0 < a
rw : Ioi (a * 0) = Ioi 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set G₀) (Ioi 0) (Ioi 0)
⊢ Eq.{u_2 + 1} (α := Set G₀) ((fun (x : G₀) ↦ a * x) '' Ioi 0) (Ioi 0)

Tactic:
rw [image_mul_left_Ioi ha, mul_zero]

Premises used: Set.image_mul_left_Ioi, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosReflectLT G₀
a : G₀
ha : 0 < a
h : ∀ (x : G₀), x ∈ (Ioo 0 a)⁻¹ ↔ x ∈ Ioi a⁻¹
⊢ (Ioo 0 a)⁻¹ = Ioi a⁻¹

Tactic:
ext x
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosReflectLT G₀
a : G₀
ha : 0 < a
x : G₀
⊢ x ∈ (Ioo 0 a)⁻¹ ↔ x ∈ Ioi a⁻¹

Tactic:
⟨fun h ↦ inv_lt_of_inv_lt₀ (inv_pos.1 h.1) h.2,
         fun h ↦ ⟨inv_pos.2 <| (inv_pos.2 ha).trans h, inv_lt_of_inv_lt₀ ha h⟩⟩

Premises used: Iff.mpr, inv_lt_of_inv_lt₀, inv_pos, And.right, And.left, And.intro, Iff.intro, Iff.mp, LT.lt.trans
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosReflectLT G₀
a : G₀
ha : 0 < a
x : G₀
⊢ x ∈ (Ioo 0 a)⁻¹ ↔ x ∈ Ioi a⁻¹

Tactic:
exact ⟨fun h ↦ inv_lt_of_inv_lt₀ (inv_pos.1 h.1) h.2,
         fun h ↦ ⟨inv_pos.2 <| (inv_pos.2 ha).trans h, inv_lt_of_inv_lt₀ ha h⟩⟩
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosReflectLT G₀
a : G₀
ha : 0 < a
rw : Ioi a = (Ioo 0 a⁻¹)⁻¹
rw₁ : Ioi a = Ioi a⁻¹⁻¹
rw₂ rw₃ : Ioi a = Ioi a
⊢ (Ioi a)⁻¹ = Ioo 0 a⁻¹

Tactic:
rw [inv_eq_iff_eq_inv, inv_Ioo_0_left (inv_pos.2 ha), inv_inv]

Premises used: Iff.mpr, inv_pos, inv_inv, Set.inv_Ioo_0_left, inv_eq_iff_eq_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
c a : G₀
h : 0 < c
⊢ (fun (x : G₀) ↦ c * x) ⁻¹' Iic a = Iic (a / c)

Tactic:
ext fun _x => (le_div_iff₀' h).symm

Premises used: Set.ext, le_div_iff₀', Iff.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
c a : G₀
h : 0 < c
⊢ (fun (x : G₀) ↦ c * x) ⁻¹' Ici a = Ici (a / c)

Tactic:
ext fun _x => (div_le_iff₀' h).symm

Premises used: Set.ext, div_le_iff₀', Iff.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
h : 0 < c
⊢ (fun (x : G₀) ↦ c * x) ⁻¹' Icc a b = Icc (a / c) (b / c)

Tactic:
simp [← Ici_inter_Iic, h]

Premises used: Set.Ici_inter_Iic
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
c a : G₀
h : 0 < c
⊢ (fun (x : G₀) ↦ c * x) ⁻¹' Iio a = Iio (a / c)

Tactic:
ext fun _x => (lt_div_iff₀' h).symm

Premises used: Set.ext, lt_div_iff₀', Iff.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
c a : G₀
h : 0 < c
⊢ (fun (x : G₀) ↦ c * x) ⁻¹' Ioi a = Ioi (a / c)

Tactic:
ext fun _x => (div_lt_iff₀' h).symm

Premises used: Set.ext, div_lt_iff₀', Iff.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
c a b : G₀
h : 0 < c
⊢ (fun (x : G₀) ↦ c * x) ⁻¹' Ioo a b = Ioo (a / c) (b / c)

Tactic:
simp [← Ioi_inter_Iio, h]

Premises used: Set.Ioi_inter_Iio
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
c a b : G₀
h : 0 < c
⊢ (fun (x : G₀) ↦ c * x) ⁻¹' Ioc a b = Ioc (a / c) (b / c)

Tactic:
simp [← Ioi_inter_Iic, h]

Premises used: Set.Ioi_inter_Iic
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
c a b : G₀
h : 0 < c
⊢ (fun (x : G₀) ↦ c * x) ⁻¹' Ico a b = Ico (a / c) (b / c)

Tactic:
simp [← Ici_inter_Iio, h]

Premises used: Set.Ici_inter_Iio
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Icc c d = Icc (a * c + b) (a * d + b)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : (fun (x : K) ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)),
    (fun (x : K) ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)

Tactic:
rwa [Set.image_image] at this

Premises used: Set.image_image
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
suffices : (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Icc c d = Icc (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)

Tactic:
suffices (· + b) '' (a * ·) '' Icc c d = Icc (a * c + b) (a * d + b) by
    rwa [Set.image_image] at this
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
rw : (fun (x : K) ↦ x + b) '' Icc (a * c) (a * d) = Icc (a * c + b) (a * d + b)
rw₁ rw₂ : Icc (a * c + b) (a * d + b) = Icc (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Icc c d = Icc (a * c + b) (a * d + b)

Tactic:
rw [image_mul_left_Icc' h, image_add_const_Icc]

Premises used: Set.image_mul_left_Icc', Set.image_add_const_Icc
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ico c d = Ico (a * c + b) (a * d + b)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : (fun (x : K) ↦ a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)),
    (fun (x : K) ↦ a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)

Tactic:
rwa [Set.image_image] at this

Premises used: Set.image_image
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
suffices : (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ico c d = Ico (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)

Tactic:
suffices (· + b) '' (a * ·) '' Ico c d = Ico (a * c + b) (a * d + b) by
    rwa [Set.image_image] at this
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
rw : (fun (x : K) ↦ x + b) '' Ico (a * c) (a * d) = Ico (a * c + b) (a * d + b)
rw₁ rw₂ : Ico (a * c + b) (a * d + b) = Ico (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ico c d = Ico (a * c + b) (a * d + b)

Tactic:
rw [image_mul_left_Ico h, image_add_const_Ico]

Premises used: Set.image_add_const_Ico, Set.image_mul_left_Ico
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ioc c d = Ioc (a * c + b) (a * d + b)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : (fun (x : K) ↦ a * x + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)),
    (fun (x : K) ↦ a * x + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ a * x + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)

Tactic:
rwa [Set.image_image] at this

Premises used: Set.image_image
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
suffices : (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ioc c d = Ioc (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ a * x + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)

Tactic:
suffices (· + b) '' (a * ·) '' Ioc c d = Ioc (a * c + b) (a * d + b) by
    rwa [Set.image_image] at this
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
rw : (fun (x : K) ↦ x + b) '' Ioc (a * c) (a * d) = Ioc (a * c + b) (a * d + b)
rw₁ rw₂ : Ioc (a * c + b) (a * d + b) = Ioc (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ioc c d = Ioc (a * c + b) (a * d + b)

Tactic:
rw [image_mul_left_Ioc h, image_add_const_Ioc]

Premises used: Set.image_mul_left_Ioc, Set.image_add_const_Ioc
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ioo c d = Ioo (a * c + b) (a * d + b)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : (fun (x : K) ↦ a * x + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)),
    (fun (x : K) ↦ a * x + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ a * x + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)

Tactic:
rwa [Set.image_image] at this

Premises used: Set.image_image
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
suffices : (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ioo c d = Ioo (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ a * x + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)

Tactic:
suffices (· + b) '' (a * ·) '' Ioo c d = Ioo (a * c + b) (a * d + b) by
    rwa [Set.image_image] at this
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
rw : (fun (x : K) ↦ x + b) '' Ioo (a * c) (a * d) = Ioo (a * c + b) (a * d + b)
rw₁ rw₂ : Ioo (a * c + b) (a * d + b) = Ioo (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ioo c d = Ioo (a * c + b) (a * d + b)

Tactic:
rw [image_mul_left_Ioo h, image_add_const_Ioo]

Premises used: Set.image_add_const_Ioo, Set.image_mul_left_Ioo
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a c : α
h : c < 0
⊢ (fun (x : α) ↦ x * c) ⁻¹' Iio a = Ioi (a / c)

Tactic:
ext fun _x => (div_lt_iff_of_neg h).symm

Premises used: Set.ext, div_lt_iff_of_neg, Iff.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a c : α
h : c < 0
⊢ (fun (x : α) ↦ x * c) ⁻¹' Ioi a = Iio (a / c)

Tactic:
ext fun _x => (lt_div_iff_of_neg h).symm

Premises used: Set.ext, lt_div_iff_of_neg, Iff.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a c : α
h : c < 0
⊢ (fun (x : α) ↦ x * c) ⁻¹' Iic a = Ici (a / c)

Tactic:
ext fun _x => (div_le_iff_of_neg h).symm

Premises used: Set.ext, div_le_iff_of_neg, Iff.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a c : α
h : c < 0
⊢ (fun (x : α) ↦ x * c) ⁻¹' Ici a = Iic (a / c)

Tactic:
ext fun _x => (le_div_iff_of_neg h).symm

Premises used: Set.ext, le_div_iff_of_neg, Iff.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun (x : α) ↦ x * c) ⁻¹' Ioo a b = Ioo (b / c) (a / c)

Tactic:
simp [← Ioi_inter_Iio, h, inter_comm]

Premises used: Set.inter_comm, Set.Ioi_inter_Iio
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun (x : α) ↦ x * c) ⁻¹' Ioc a b = Ico (b / c) (a / c)

Tactic:
simp [← Ioi_inter_Iic, ← Ici_inter_Iio, h, 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 : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun (x : α) ↦ x * c) ⁻¹' Ico a b = Ioc (b / c) (a / c)

Tactic:
simp [← Ici_inter_Iio, ← Ioi_inter_Iic, h, 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 : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun (x : α) ↦ x * c) ⁻¹' Icc a b = Icc (b / c) (a / c)

Tactic:
simp [← Ici_inter_Iic, h, inter_comm]

Premises used: Set.inter_comm, Set.Ici_inter_Iic
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a c : α
h : c < 0
⊢ (fun (x : α) ↦ c * x) ⁻¹' Iio a = Ioi (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Iio_of_neg a h

Premises used: Set.preimage_mul_const_Iio_of_neg, mul_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a c : α
h : c < 0
⊢ (fun (x : α) ↦ c * x) ⁻¹' Ioi a = Iio (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Ioi_of_neg a h

Premises used: mul_comm, Set.preimage_mul_const_Ioi_of_neg
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a c : α
h : c < 0
⊢ (fun (x : α) ↦ c * x) ⁻¹' Iic a = Ici (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Iic_of_neg a h

Premises used: Set.preimage_mul_const_Iic_of_neg, mul_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a c : α
h : c < 0
⊢ (fun (x : α) ↦ c * x) ⁻¹' Ici a = Iic (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Ici_of_neg a h

Premises used: Set.preimage_mul_const_Ici_of_neg, mul_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun (x : α) ↦ c * x) ⁻¹' Ioo a b = Ioo (b / c) (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Ioo_of_neg a b h

Premises used: Set.preimage_mul_const_Ioo_of_neg, mul_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun (x : α) ↦ c * x) ⁻¹' Ioc a b = Ico (b / c) (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Ioc_of_neg a b h

Premises used: Set.preimage_mul_const_Ioc_of_neg, mul_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun (x : α) ↦ c * x) ⁻¹' Ico a b = Ioc (b / c) (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Ico_of_neg a b h

Premises used: Set.preimage_mul_const_Ico_of_neg, mul_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun (x : α) ↦ c * x) ⁻¹' Icc a b = Icc (b / c) (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Icc_of_neg a b h

Premises used: mul_comm, Set.preimage_mul_const_Icc_of_neg
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a ≠ 0
b c : α
h : a < 0
⊢ (fun (x : α) ↦ x * a) ⁻¹' [[b, c]] = [[b / a, c / a]]

Tactic:
simp [← Icc_min_max, h, h.le, min_div_div_right_of_nonpos, max_div_div_right_of_nonpos]

Premises used: Set.Icc_min_max, LT.lt.le, max_div_div_right_of_nonpos, min_div_div_right_of_nonpos
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha_1 : a ≠ 0
b c : α
ha : 0 < a
⊢ (fun (x : α) ↦ x * a) ⁻¹' [[b, c]] = [[b / a, c / a]]

Tactic:
simp [← Icc_min_max, ha, ha.le, min_div_div_right, max_div_div_right]

Premises used: max_div_div_right, Set.Icc_min_max, LT.lt.le, min_div_div_right
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a ≠ 0
b c : α
⊢ (fun (x : α) ↦ a * x) ⁻¹' [[b, c]] = [[b / a, c / a]]

Tactic:
simp only [← preimage_mul_const_uIcc ha, mul_comm]

Premises used: Set.preimage_mul_const_uIcc, mul_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a ≠ 0
b c : α
⊢ (fun (x : α) ↦ x / a) ⁻¹' [[b, c]] = [[b * a, c * a]]

Tactic:
simp only [div_eq_mul_inv, preimage_mul_const_uIcc (inv_ne_zero ha), inv_inv]

Premises used: Set.preimage_mul_const_uIcc, div_eq_mul_inv, inv_inv, inv_ne_zero
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hU : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} U
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
inl : ∀ (aU : α) (haU : U = Ioi aU), Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} V
inr : ∀ (aU : α) (haU : U = Iio aU), Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} V
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} V

Tactic:
obtain ⟨aU, (haU | haU)⟩ := hU
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
inl : ∃ (a_1 : α), (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi a_1 ∨ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio a_1
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} V

Tactic:
simp only [hV, haU, mem_setOf_eq]

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
inr : ∃ (a_1 : α), (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi a_1 ∨ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio a_1
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} V

Tactic:
simp only [hV, haU, mem_setOf_eq]

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
h : (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)
⊢ ∃ (a_1 : α), (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi a_1 ∨ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio a_1

Tactic:
use a⁻¹ * aU
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
h : (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)
⊢ ∃ (a_1 : α), (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi a_1 ∨ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio a_1

Tactic:
use a⁻¹ * aU
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
h :
  ∀ (hb : a < 0), (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)
h₁ :
  ∀ (hb : 0 < a), (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)
⊢ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)

Tactic:
rcases lt_or_gt_of_ne hb with (hb | hb)

Premises used: lt_or_gt_of_ne