mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (Ico a b)⁻¹ = Ioc b⁻¹ a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (Ioc a b)⁻¹ = Ico b⁻¹ a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (Ioo a b)⁻¹ = Ioo b⁻¹ a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a * x) ⁻¹' Icc b c = Icc (b / a) (c / a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a * x) ⁻¹' Ico b c = Ico (b / a) (c / a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a * x) ⁻¹' Ioc b c = Ioc (b / a) (c / a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
⊢ s ^ 0 ∈ f ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a * x) ⁻¹' Ioo b c = Ioo (b / a) (c / a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x * a) ⁻¹' Icc b c = Icc (b / a) (c / a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x * a) ⁻¹' Ico b c = Ico (b / a) (c / a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x * a) ⁻¹' Ioc b c = Ioc (b / a) (c / a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x * a) ⁻¹' Ioo b c = Ioo (b / a) (c / a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x / a) ⁻¹' Ici b = Ici (b * a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x / a) ⁻¹' Ioi b = Ioi (b * a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x / a) ⁻¹' Iic b = Iic (b * a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x / a) ⁻¹' Iio b = Iio (b * a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x / a) ⁻¹' Icc b c = Icc (b * a) (c * a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x / a) ⁻¹' Ico b c = Ico (b * a) (c * a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
n : ℕ
⊢ s ^ (n + 1) ∈ f ^ (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x / a) ⁻¹' Ioc b c = Ioc (b * a) (c * a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x / a) ⁻¹' Ioo b c = Ioo (b * a) (c * a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a / x) ⁻¹' Icc b c = Icc (a / c) (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a / x) ⁻¹' Ico b c = Ioc (a / c) (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a / x) ⁻¹' Ioc b c = Ico (a / c) (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a / x) ⁻¹' Ioo b c = Ioo (a / c) (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ
hn : n ≠ 0
⊢ ⊥ ^ n = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ a * x) '' Iic b = Iic (a * b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ a * x) '' Iio b = Iio (a * b)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
⊢ IsUniformInducing
    ⇑((ofFun 𝔖).symm.trans
        ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x * a) '' Iic b = Iic (b * a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x * a) '' Iio b = Iio (b * a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ Inv.inv '' Ici a = Iic a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ Inv.inv '' Iic a = Ici a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ Inv.inv '' Ioi a = Iio a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ Inv.inv '' Iio a = Ioi a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ Inv.inv '' Icc a b = Icc b⁻¹ a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ Inv.inv '' Ico a b = Ioc b⁻¹ a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ Inv.inv '' Ioc a b = Ico b⁻¹ a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ Inv.inv '' Ioo a b = Ioo b⁻¹ a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ a / x) '' Ici b = Iic (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
⊢ f * ⊤ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ a / x) '' Iic b = Ici (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ a / x) '' Ioi b = Iio (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ a / x) '' Iio b = Ioi (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
⊢ ⊤ * f = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a / x) '' Icc b c = Icc (a / c) (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a / x) '' Ico b c = Ioc (a / c) (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ⊤ ^ (n + 2) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a / x) '' Ioc b c = Ico (a / c) (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a / x) '' Ioo b c = Ioo (a / c) (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x / a) '' Ici b = Ici (b / a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x / a) '' Iic b = Iic (b / a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x / a) '' Ioi b = Ioi (b / a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x / a) '' Iio b = Iio (b / a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x / a) '' Icc b c = Icc (b / a) (c / a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x / a) '' Ico b c = Ico (b / a) (c / a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x / a) '' Ioc b c = Ioc (b / a) (c / a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x / a) '' Ioo b c = Ioo (b / a) (c / a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ [[a, b]]⁻¹ = [[a⁻¹, b⁻¹]]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ (fun x ↦ a + x) ⁻¹' [[b, c]] = [[b - a, c - a]]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ (fun x ↦ x + a) ⁻¹' [[b, c]] = [[b - a, c - a]]

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ IsUniformInducing ⇑(Equiv.piComm fun a ↦ δ)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ (fun x ↦ x - a) ⁻¹' [[b, c]] = [[b + a, c + a]]

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
⊢ f * g = 1 ↔ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ (fun x ↦ a - x) ⁻¹' [[b, c]] = [[a - b, a - c]]

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
a b : α
hab : a * b = 1
h : pure a * pure b = 1
⊢ (pure a)⁻¹ = pure b

Tactic:
rw [inv_pure, inv_eq_of_mul_eq_one_right hab]

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g s t : Filter α
h : s * t = 1
⊢ s⁻¹ = t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ (fun x ↦ a + x) '' [[b, c]] = [[a + b, a + c]]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ (fun x ↦ x + a) '' [[b, c]] = [[b + a, c + a]]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ (fun x ↦ a - x) '' [[b, c]] = [[a - b, a - c]]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ (fun x ↦ x - a) '' [[b, c]] = [[b - a, c - a]]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b : α
⊢ Neg.neg '' [[a, b]] = [[-a, -b]]

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
f : Filter α
⊢ IsUnit f ↔ ∃ a, f = pure a ∧ IsUnit a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
h : IsCoherentWith 𝔖
⊢ IsClosed[topologicalSpace α β 𝔖] {f | Continuous[inst✝, inst✝¹.toTopologicalSpace] ((toFun 𝔖) f)}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
⊢ |d - c| ≤ |b - a|

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Group α
f g : Filter α
⊢ 1 ≤ f / g ↔ ¬Disjoint f g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
c a : G₀
h : 0 < c
⊢ (fun x ↦ x * c) ⁻¹' Iic a = Iic (a / c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Group α
f : Filter α
h : f.NeBot
⊢ 1 ≤ f / f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Group α
f : Filter α
⊢ IsUnit f ↔ ∃ a, f = pure a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
c a : G₀
h : 0 < c
⊢ (fun x ↦ x * c) ⁻¹' Ici a = Ici (a / c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
c a : G₀
h : 0 < c
⊢ (fun x ↦ x * c) ⁻¹' Ioi a = Ioi (a / c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
c a : G₀
h : 0 < c
⊢ (fun x ↦ x * c) ⁻¹' Iio a = Iio (a / c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SMul α β
a : α
b : β
⊢ pure a • pure b = pure (a • b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
c a b : G₀
h : 0 < c
⊢ (fun x ↦ x * c) ⁻¹' Icc a b = Icc (a / c) (b / c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
c a b : G₀
h : 0 < c
⊢ (fun x ↦ x * c) ⁻¹' Ioo a b = Ioo (a / c) (b / c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
c a b : G₀
h : 0 < c
⊢ (fun x ↦ x * c) ⁻¹' Ioc a b = Ioc (a / c) (b / c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : VSub α β
a b : β
⊢ pure a -ᵥ pure b = pure (a -ᵥ b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
c a b : G₀
h : 0 < c
⊢ (fun x ↦ x * c) ⁻¹' Ico a b = Ico (a / c) (b / c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
b : β
f : Filter γ
⊢ (a • b) • f = a • b • f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
⊢ (fun x ↦ x * c) '' Icc a b = Icc (a * c) (b * c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
f : Filter β
g : Filter γ
⊢ (a • f) • g = a • f • g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝¹ : Monoid α
inst✝ : MulAction α β
f : Filter β
⊢ map (fun x2 ↦ 1 • x2) f = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
ha : 0 ≤ a
hbc : b ≤ c
⊢ (fun x ↦ a * x) '' Icc b c = Icc (a * b) (a * c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝¹ : Monoid α
inst✝ : MulAction α β
a b : α
f : Filter β
⊢ (a * b) • f = a • b • f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a : G₀
ha : 0 < a
⊢ (fun x ↦ a * x) '' Ioi 0 = Ioi 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝¹ : Monoid α
inst✝ : MulAction α β
f : Filter β
⊢ 1 • f = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a : G₀
ha : 0 < a
⊢ (Ioo 0 a)⁻¹ = Ioi a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Monoid α
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction α β
x✝ : α
⊢ pure (x✝ • 0) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MulDistribMulAction α β
x✝ : α
⊢ {x✝ • 1} = 1

Tactic:
by

Goal state after: