awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 = Ico (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
-- 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 (a / c) (a / b)

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) '' Iic b = Iic (a * b)

Tactic:
simp [mul_comm]

Premises used: mul_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 = Iio (a * b)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- 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
-- 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
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ Inv.inv '' Ici a = Iic a⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ Inv.inv '' Iic a = Ici a⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ Inv.inv '' Ioi a = Iio a⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ Inv.inv '' Iio a = Ioi a⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ Inv.inv '' Icc a b = Icc b⁻¹ a⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ Inv.inv '' Ico a b = Ioc b⁻¹ a⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ Inv.inv '' Ioc a b = Ico b⁻¹ a⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ Inv.inv '' Ioo a b = Ioo b⁻¹ a⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ ∀ (a_1 : Set α),
    Eq (α := Set α) (((fun (x : α) ↦ a * x) ∘ fun (x : α) ↦ x⁻¹) '' a_1)
      ((fun (x : α) ↦ a * x) '' (fun (x : α) ↦ x⁻¹) '' a_1)

Tactic:
have := image_comp (fun x => a * x) fun x => x⁻¹
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
this :
  ∀ (a_1 : Set α),
    Eq (α := Set α) ((fun (x : α) ↦ a * x⁻¹) '' a_1) ((fun (x : α) ↦ a * x) '' (fun (x : α) ↦ x⁻¹) '' a_1)
⊢ (fun (x : α) ↦ a / x) '' Ici b = Iic (a / b)

Tactic:
simp [div_eq_mul_inv, this, mul_comm]

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

Tactic:
simp [div_eq_mul_inv, this, mul_comm]

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

Tactic:
simp [div_eq_mul_inv, this, mul_comm]

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

Tactic:
simp [div_eq_mul_inv, this, mul_comm]

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

Tactic:
have := image_comp (fun x => a * x) fun x => x⁻¹
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
this :
  ∀ (a_1 : Set α),
    Eq (α := Set α) ((fun (x : α) ↦ a * x⁻¹) '' a_1) ((fun (x : α) ↦ a * x) '' (fun (x : α) ↦ x⁻¹) '' a_1)
⊢ (fun (x : α) ↦ a / x) '' Icc b c = Icc (a / c) (a / b)

Tactic:
simp [div_eq_mul_inv, this, mul_comm]

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

Tactic:
simp [div_eq_mul_inv, this, mul_comm]

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

Tactic:
simp [div_eq_mul_inv, this, mul_comm]

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

Tactic:
simp [div_eq_mul_inv, this, mul_comm]

Premises used: div_eq_mul_inv, mul_comm
-- 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) '' 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) '' 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) '' 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 : α
⊢ BijOn (fun (x : α) ↦ x * a) (Iic b) (Iic (b * a))

Tactic:
image_mul_const_Iic a b ▸ (mul_left_injective _).injOn.bijOn_image

Premises used: Function.Injective.injOn, Eq.rec, Set.InjOn.bijOn_image, Set.image_mul_const_Iic, mul_left_injective
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ BijOn (fun (x : α) ↦ x * a) (Iio b) (Iio (b * a))

Tactic:
image_mul_const_Iio a b ▸ (mul_left_injective _).injOn.bijOn_image

Premises used: Function.Injective.injOn, Eq.rec, Set.InjOn.bijOn_image, mul_left_injective, Set.image_mul_const_Iio
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ [[a, b]]⁻¹ = [[a⁻¹, b⁻¹]]

Tactic:
simp only [uIcc, inv_Icc, inv_sup, inv_inf]

Premises used: inv_sup, Set.inv_Icc, inv_inf, Set.uIcc
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c : α
⊢ (fun (x : α) ↦ a + x) ⁻¹' [[b, c]] = [[b - a, c - a]]

Tactic:
simp only [← Icc_min_max, preimage_const_add_Icc, min_sub_sub_right, max_sub_sub_right]

Premises used: Set.preimage_const_add_Icc, Set.Icc_min_max, min_sub_sub_right, max_sub_sub_right
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c : α
⊢ (fun (x : α) ↦ x + a) ⁻¹' [[b, c]] = [[b - a, c - a]]

Tactic:
simpa only [add_comm] using preimage_const_add_uIcc a b c

Premises used: add_comm, Set.preimage_const_add_uIcc
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c : α
⊢ (fun (x : α) ↦ x - a) ⁻¹' [[b, c]] = [[b + a, c + a]]

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c : α
simp_rw : Icc (a - max b c) (a - min b c) = Icc (min (a - b) (a - c)) (max (a - b) (a - c))
⊢ (fun (x : α) ↦ a - x) ⁻¹' [[b, c]] = [[a - b, a - c]]

Tactic:
simp_rw [← Icc_min_max, preimage_const_sub_Icc]

Premises used: Set.Icc_min_max, Set.preimage_const_sub_Icc
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c : α
⊢ Icc (a - max b c) (a - min b c) = Icc (min (a - b) (a - c)) (max (a - b) (a - c))

Tactic:
simp only [sub_eq_add_neg, min_add_add_left, max_add_add_left, min_neg_neg, max_neg_neg]

Premises used: max_neg_neg, sub_eq_add_neg, max_add_add_left, min_neg_neg, min_add_add_left
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c : α
⊢ (fun (x : α) ↦ a + x) '' [[b, c]] = [[a + b, a + c]]

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c : α
⊢ (fun (x : α) ↦ x + a) '' [[b, c]] = [[b + a, c + a]]

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c : α
⊢ ∀ (a_1 : Set α),
    Eq (α := Set α) (((fun (x : α) ↦ a + x) ∘ fun (x : α) ↦ -x) '' a_1)
      ((fun (x : α) ↦ a + x) '' (fun (x : α) ↦ -x) '' a_1)

Tactic:
have := image_comp (fun x => a + x) fun x => -x
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c : α
this :
  ∀ (a_1 : Set α), Eq (α := Set α) ((fun (x : α) ↦ a + -x) '' a_1) ((fun (x : α) ↦ a + x) '' (fun (x : α) ↦ -x) '' a_1)
⊢ (fun (x : α) ↦ a - x) '' [[b, c]] = [[a - b, a - c]]

Tactic:
simp [sub_eq_add_neg, this, add_comm]

Premises used: sub_eq_add_neg, add_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c : α
⊢ (fun (x : α) ↦ x - a) '' [[b, c]] = [[b - a, c - a]]

Tactic:
simp [sub_eq_add_neg, add_comm]

Premises used: sub_eq_add_neg, add_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
⊢ Neg.neg '' [[a, b]] = [[-a, -b]]

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
rw : max c d - min c d ≤ max a b - min a b
⊢ |d - c| ≤ |b - a|

Tactic:
rw [← max_sub_min_eq_abs, ← max_sub_min_eq_abs]

Premises used: max_sub_min_eq_abs
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
⊢ min a b ≤ min c d ∧ max c d ≤ max a b

Tactic:
rw [uIcc_subset_uIcc_iff_le] at h

Premises used: Set.uIcc_subset_uIcc_iff_le
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : min a b ≤ min c d ∧ max c d ≤ max a b
⊢ max c d - min c d ≤ max a b - min a b

Tactic:
sub_le_sub h.2 h.1

Premises used: And.right, And.left, sub_le_sub
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : min a b ≤ min c d ∧ max c d ≤ max a b
⊢ max c d - min c d ≤ max a b - min a b

Tactic:
exact sub_le_sub h.2 h.1

Premises used: And.right, And.left, sub_le_sub
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c : α
h : c ∈ [[a, b]]
⊢ |c - a| ≤ |b - a|

Tactic:
abs_sub_le_of_uIcc_subset_uIcc <| uIcc_subset_uIcc_left h

Premises used: Set.uIcc_subset_uIcc_left, Set.abs_sub_le_of_uIcc_subset_uIcc
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c : α
h : c ∈ [[a, b]]
⊢ |b - c| ≤ |b - a|

Tactic:
abs_sub_le_of_uIcc_subset_uIcc <| uIcc_subset_uIcc_right h

Premises used: Set.uIcc_subset_uIcc_right, Set.abs_sub_le_of_uIcc_subset_uIcc
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
c a : G₀
h : 0 < c
⊢ (fun (x : G₀) ↦ x * c) ⁻¹' Iic a = Iic (a / c)

Tactic:
simpa only [division_def] using (OrderIso.mulRight₀ c h).preimage_Iic a

Premises used: OrderIso.mulRight₀, division_def, OrderIso.preimage_Iic
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
c a : G₀
h : 0 < c
⊢ (fun (x : G₀) ↦ x * c) ⁻¹' Ici a = Ici (a / c)

Tactic:
simpa only [division_def] using (OrderIso.mulRight₀ c h).preimage_Ici a

Premises used: OrderIso.mulRight₀, division_def, OrderIso.preimage_Ici
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
c a : G₀
h : 0 < c
⊢ (fun (x : G₀) ↦ x * c) ⁻¹' Ioi a = Ioi (a / c)

Tactic:
simpa only [division_def] using (OrderIso.mulRight₀ c h).preimage_Ioi a

Premises used: OrderIso.mulRight₀, division_def, OrderIso.preimage_Ioi
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
c a : G₀
h : 0 < c
⊢ (fun (x : G₀) ↦ x * c) ⁻¹' Iio a = Iio (a / c)

Tactic:
simpa only [division_def] using (OrderIso.mulRight₀ c h).preimage_Iio a

Premises used: OrderIso.mulRight₀, OrderIso.preimage_Iio, division_def
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
c a b : G₀
h : 0 < c
⊢ (fun (x : G₀) ↦ x * c) ⁻¹' 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 : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
c a b : G₀
h : 0 < c
⊢ (fun (x : G₀) ↦ x * c) ⁻¹' 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 : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
c a b : G₀
h : 0 < c
⊢ (fun (x : G₀) ↦ x * c) ⁻¹' 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 : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
c a b : G₀
h : 0 < c
⊢ (fun (x : G₀) ↦ x * c) ⁻¹' 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:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
c a b : G₀
h : 0 < c
⊢ (fun (x : G₀) ↦ x * c) '' Icc a b = Icc (a * c) (b * c)

Tactic:
(OrderIso.mulRight₀ c h).image_Icc a b

Premises used: OrderIso.image_Icc, OrderIso.mulRight₀
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
inl : 0 = c → (fun (x : G₀) ↦ x * c) '' Icc a b = Icc (a * c) (b * c)
inr : 0 < c → (fun (x : G₀) ↦ x * c) '' Icc a b = Icc (a * c) (b * c)
⊢ (fun (x : G₀) ↦ x * c) '' Icc a b = Icc (a * c) (b * c)

Tactic:
cases eq_or_lt_of_le hc

Premises used: eq_or_lt_of_le
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
h : 0 = c
inl : ∀ (hc : LE.le.{u_2} (α := G₀) 0 0), (fun (x : G₀) ↦ x * 0) '' Icc a b = Icc (a * 0) (b * 0)
⊢ (fun (x : G₀) ↦ x * c) '' Icc a b = Icc (a * c) (b * c)

Tactic:
subst c
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
hab : a ≤ b
hc : LE.le.{u_2} (α := G₀) 0 0
⊢ (fun (x : G₀) ↦ x * 0) '' Icc a b = Icc (a * 0) (b * 0)

Tactic:
simp [(nonempty_Icc.2 hab).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 : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
h : 0 < c
⊢ (fun (x : G₀) ↦ x * c) '' Icc a b = Icc (a * c) (b * c)

Tactic:
image_mul_right_Icc' a b ‹0 < c›

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

Tactic:
exact image_mul_right_Icc' a b ‹0 < c›

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

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

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

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

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

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

Premises used: OrderIso.mulRight₀, 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₀
h : 0 < a
b : G₀
⊢ (fun (x : G₀) ↦ a * x) '' Ici b = Ici (a * b)

Tactic:
(OrderIso.mulLeft₀ a h).image_Ici b

Premises used: OrderIso.image_Ici, 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 : G₀
⊢ (fun (x : G₀) ↦ a * x) '' Iic b = Iic (a * b)

Tactic:
(OrderIso.mulLeft₀ a h).image_Iic b

Premises used: OrderIso.image_Iic, 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 : G₀
⊢ (fun (x : G₀) ↦ a * x) '' Ioi b = Ioi (a * b)

Tactic:
(OrderIso.mulLeft₀ a h).image_Ioi b

Premises used: OrderIso.mulLeft₀, OrderIso.image_Ioi
-- 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 : G₀
⊢ (fun (x : G₀) ↦ a * x) '' Iio b = Iio (a * b)

Tactic:
(OrderIso.mulLeft₀ a h).image_Iio b

Premises used: OrderIso.image_Iio, 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) '' Icc b c = Icc (a * b) (a * c)

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

Premises used: OrderIso.image_Icc, 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 b c : G₀
ha : 0 ≤ a
hbc : b ≤ c
inl : ∀ (ha : LE.le.{u_2} (α := G₀) 0 0), (fun (x : G₀) ↦ 0 * x) '' Icc b c = Icc (0 * b) (0 * c)
inr : ∀ (ha : 0 < a), (fun (x : G₀) ↦ a * x) '' Icc b c = Icc (a * b) (a * c)
⊢ (fun (x : G₀) ↦ a * x) '' Icc b c = Icc (a * b) (a * c)

Tactic:
rcases ha.eq_or_lt with rfl | ha

Premises used: LE.le.eq_or_lt, rfl