mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r s : ℝ≥0∞
hrs : r ≤ s
⊢ ⌈r⌉ₑ ≤ ⌈s⌉ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ a / 2 < ↑⌊a⌋₊

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: n r : ℕ∞
⊢ r ≤ ⌊↑n⌋ₑ ↔ r ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: n r : ℕ∞
⊢ ⌈↑n⌉ₑ ≤ r ↔ n ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: ⊢ ⌊0⌋ₑ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 2⁻¹ < a
⊢ ↑⌈(2 - 1)⁻¹⌉₊ / 2 < a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: ⊢ ⌈0⌉ₑ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: ⊢ ⌊1⌋ₑ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: ⊢ ⌈1⌉ₑ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
⊢ 0 < ⌊r⌋ₑ ↔ 1 ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
s : UpperSet (FiniteMulArchimedeanClass M)
⊢ a ∈ subgroup s ↔ ∀ (h : a ≠ 1), mk a h ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
⊢ 0 < ⌈r⌉ₑ ↔ 0 < r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
⊢ ⌊r⌋ₑ = 0 ↔ r < 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
c : FiniteMulArchimedeanClass M
⊢ a ∈ c.ballSubgroup ↔ ∀ (h : a ≠ 1), c < mk a h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 2⁻¹ ≤ a
⊢ ↑⌈(2 - 1)⁻¹⌉₊ / 2 ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
c : FiniteMulArchimedeanClass M
⊢ a ∈ c.closedBallSubgroup ↔ ∀ (h : a ≠ 1), c ≤ mk a h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
m : ℕ
⊢ ⌊↑m⌋₊ = ↑m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
m : ℕ
⊢ IsNat r m → IsNat ⌊r⌋₊ m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
⊢ ⌈r⌉ₑ = 0 ↔ r = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
⊢ ⌈↑r⌉ₑ ≤ ⌊↑r⌋ₑ + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
m : ℕ
⊢ ↑(Int.negOfNat m) ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
m : ℕ
⊢ IsInt r (Int.negOfNat m) → IsNat ⌊r⌋₊ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r s : ℝ≥0∞
h : ∀ (n : ℕ∞), ↑n ≤ r ↔ ↑n ≤ s
⊢ ∀ (c : ℕ∞), c ≤ ⌊r⌋ₑ ↔ c ≤ ⌊s⌋ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r s : ℝ≥0∞
h : ∀ (n : ℕ∞), r ≤ ↑n ↔ s ≤ ↑n
⊢ ∀ (c : ℕ∞), ⌈r⌉ₑ ≤ c ↔ ⌈s⌉ₑ ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: x✝ : ℕ∞
⊢ ⌊∞ + ↑x✝⌋ₑ = ⌊∞⌋ₑ + x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: x✝ : ℝ≥0∞
⊢ ⌊x✝ + ↑⊤⌋ₑ = ⌊x✝⌋ₑ + ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: R : Type u_3
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : n / d = res
⊢ IsNat ⌊r⌋₊ res

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ⌊↑r + ↑↑n⌋ₑ = ⌊↑r⌋ₑ + ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: x✝ : ℕ∞
⊢ ⌈∞ + ↑x✝⌉ₑ = ⌈∞⌉ₑ + x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: x✝ : ℝ≥0∞
⊢ ⌈x✝ + ↑⊤⌉ₑ = ⌈x✝⌉ₑ + ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ⌈↑r + ↑↑n⌉ₑ = ⌈↑r⌉ₑ + ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
n : ℕ∞
⊢ ⌊↑n + r⌋ₑ = n + ⌊r⌋ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: R : Type u_3
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
n d : ℕ
hd : Invertible ↑d
⊢ ↑(Int.negOfNat n) * ⅟↑d ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
n : ℕ∞
⊢ ⌈↑n + r⌉ₑ = n + ⌈r⌉ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: ⊢ ⌊∞ - ↑⊤⌋ₑ = ⌊∞⌋ₑ - ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: R : Type u_3
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsRat r (Int.negOfNat n) d
⊢ IsNat ⌊r⌋₊ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: n : ℕ
⊢ ⌊∞ - ↑↑n⌋ₑ = ⌊∞⌋ₑ - ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
⊢ ⌊↑r - ↑⊤⌋ₑ = ⌊↑r⌋ₑ - ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ⌊↑r - ↑↑n⌋ₑ = ⌊↑r⌋ₑ - ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: ⊢ ⌈∞ - ↑⊤⌉ₑ = ⌈∞⌉ₑ - ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: n : ℕ
⊢ ⌈∞ - ↑↑n⌉ₑ = ⌈∞⌉ₑ - ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
⊢ ⌈↑r - ↑⊤⌉ₑ = ⌈↑r⌉ₑ - ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ⌈↑r - ↑↑n⌉ₑ = ⌈↑r⌉ₑ - ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
hr : r ≠ ∞
⊢ ↑⌈r⌉ₑ < r + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: x✝ : ℝ≥0∞
⊢ ⌈∞ + x✝⌉ₑ ≤ ⌈∞⌉ₑ + ⌈x✝⌉ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: x✝ : ℝ≥0∞
⊢ ⌈x✝ + ∞⌉ₑ ≤ ⌈x✝⌉ₑ + ⌈∞⌉ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: ι : Sort u_1
f : ι → ℕ∞
x✝ : ℝ≥0∞
⊢ ↑(⨆ i, f i) ≤ x✝ ↔ ⨆ i, ↑(f i) ≤ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: ι : Sort u_1
f : ι → ℕ∞
x✝ : ℝ≥0∞
⊢ x✝ ≤ ↑(⨅ i, f i) ↔ x✝ ≤ ⨅ i, ↑(f i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: a : ℝ≥0∞
⊢ toENNReal ⁻¹' Ioi a = Ioi ⌊a⌋ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: a : ℝ≥0∞
⊢ toENNReal ⁻¹' Iio a = Iio ⌈a⌉ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: a : ℝ≥0∞
⊢ toENNReal ⁻¹' Iic a = Iic ⌊a⌋ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: a : ℝ≥0∞
⊢ toENNReal ⁻¹' Ici a = Ici ⌈a⌉ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: a b : ℝ≥0∞
⊢ toENNReal ⁻¹' Icc a b = Icc ⌈a⌉ₑ ⌊b⌋ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: a b : ℝ≥0∞
⊢ toENNReal ⁻¹' Ico a b = Ico ⌈a⌉ₑ ⌈b⌉ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: a b : ℝ≥0∞
⊢ toENNReal ⁻¹' Ioc a b = Ioc ⌊a⌋ₑ ⌊b⌋ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: a b : ℝ≥0∞
⊢ toENNReal ⁻¹' Ioo a b = Ioo ⌊a⌋ₑ ⌈b⌉ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
hr : 0 < r
⊢ 0 < ⌈r⌉ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.CompleteLattice

Goal state before:
pp: ι : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : ConditionallyCompleteLattice G
inst✝¹ : Nonempty ι
f : ι → G
inst✝ : MulRightMono G
hf : BddAbove (range f)
a : G
⊢ (⨆ i, f i) / a = ⨆ i, f i / a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.CompleteLattice

Goal state before:
pp: ι : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : ConditionallyCompleteLattice G
inst✝¹ : Nonempty ι
f : ι → G
inst✝ : MulRightMono G
hf : BddBelow (range f)
a : G
⊢ (⨅ i, f i) / a = ⨅ i, f i / a

Tactic:
simp only [div_eq_mul_inv, ciInf_mul hf]

Goal state after:
Module: Mathlib.Algebra.Order.Group.CompleteLattice

Goal state before:
pp: ι : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : ConditionallyCompleteLattice G
inst✝¹ : Nonempty ι
f : ι → G
inst✝ : MulRightMono G
hf : BddBelow (range f)
a : G
⊢ (⨅ i, f i) / a = ⨅ i, f i / a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Equiv

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
x✝¹ x✝ : α
⊢ toLex.toFun (x✝¹ * x✝) = toLex.toFun x✝¹ * toLex.toFun x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Equiv

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
x✝¹ x✝ : Lex α
⊢ ofLex.toFun (x✝¹ * x✝) = ofLex.toFun x✝¹ * ofLex.toFun x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : DenselyOrdered α
a b : α
h : ∀ (ε : α), 1 < ε → a / ε ≤ b
ε : α
ε1 : ε < 1
⊢ a * ε ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : MulRightStrictMono α
a b c : α
hc : c < a * b
⊢ ∃ a', a' < a ∧ c < a' * b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : CommGroup α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : MulLeftStrictMono α
a b c : α
hc : c < a * b
⊢ ∃ b', b' < b ∧ c < a * b'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : MulRightStrictMono α
a b c : α
hc : a * b < c
⊢ ∃ a', a' > a ∧ a' * b < c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : CommGroup α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : MulLeftStrictMono α
a b c : α
hc : a * b < c
⊢ ∃ b', b' > b ∧ a * b' < c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b'
⊢ c ≤ a * b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cone

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
p q : GroupCone G
h : (fun C ↦ C.carrier) p = (fun C ↦ C.carrier) q
⊢ p = q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cone

Goal state before:
pp: H : Type u_1
inst✝² : CommGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedMonoid H
a✝ a : H
⊢ a ∈ (Submonoid.oneLE H).carrier → a⁻¹ ∈ (Submonoid.oneLE H).carrier → a = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cone

Goal state before:
pp: H✝ : Type u_1
inst✝⁵ : CommGroup H✝
inst✝⁴ : PartialOrder H✝
inst✝³ : IsOrderedMonoid H✝
a : H✝
H : Type u_2
inst✝² : CommGroup H
inst✝¹ : LinearOrder H
inst✝ : IsOrderedMonoid H
⊢ ∀ (a : H), a ∈ oneLE H ∨ a⁻¹ ∈ oneLE H

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cone

Goal state before:
pp: S : Type u_1
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : SetLike S G
C : S
inst✝ : GroupConeClass S G
a : G
⊢ a / a ∈ C

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cone

Goal state before:
pp: S : Type u_1
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : SetLike S G
C : S
inst✝ : GroupConeClass S G
a b c : G
nab : b / a ∈ C
nbc : c / b ∈ C
⊢ c / a ∈ C

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cone

Goal state before:
pp: S : Type u_1
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : SetLike S G
C : S
inst✝ : GroupConeClass S G
a b : G
nab : b / a ∈ C
nba : a / b ∈ C
⊢ (b / a)⁻¹ ∈ C

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cone

Goal state before:
pp: S : Type u_1
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : SetLike S G
C : S
inst✝ : GroupConeClass S G
a b : G
nab : b / a ∈ C
nba : a / b ∈ C
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cone

Goal state before:
pp: S : Type u_1
G : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : SetLike S G
C : S
inst✝² : GroupConeClass S G
inst✝¹ : HasMemOrInvMem C
inst✝ : DecidablePred fun x ↦ x ∈ C
a b : G
⊢ a ≤ b ∨ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cone

Goal state before:
pp: S : Type u_1
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : SetLike S G
C : S
inst✝ : GroupConeClass S G
x✝ : PartialOrder G := PartialOrder.mkOfGroupCone C
a b : G
nab : a ≤ b
c : G
⊢ a * c ≤ b * c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: M : Type u_2
inst✝⁴ : LinearOrder M
inst✝³ : DenselyOrdered M
inst✝² : CommMonoid M
inst✝¹ : ExistsMulOfLE M
inst✝ : IsOrderedCancelMonoid M
y : M
hy : 1 < y
z : M
hz : 1 < z
hx : 1 < y * z
hyx : y < y * z
hxy : y * z ≤ y ^ 2
⊢ z ^ 2 ≤ y * z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: M : Type u_2
inst✝⁴ : LinearOrder M
inst✝³ : DenselyOrdered M
x : M
inst✝² : CommMonoid M
inst✝¹ : ExistsMulOfLE M
inst✝ : IsOrderedCancelMonoid M
hx : 1 < x
⊢ ∃ y, 1 < y ∧ y ^ 2 ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: M : Type u_2
inst✝⁴ : LinearOrder M
inst✝³ : DenselyOrdered M
x : M
inst✝² : CommMonoid M
inst✝¹ : ExistsMulOfLE M
inst✝ : IsOrderedCancelMonoid M
hx : 1 < x
⊢ 1 < x ∧ x ^ 0 < x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: M : Type u_2
inst✝⁴ : LinearOrder M
inst✝³ : DenselyOrdered M
x : M
inst✝² : CommMonoid M
inst✝¹ : ExistsMulOfLE M
inst✝ : IsOrderedCancelMonoid M
hx : 1 < x
⊢ ∃ y, 1 < y ∧ y ^ 1 < x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: M : Type u_2
inst✝⁴ : LinearOrder M
inst✝³ : DenselyOrdered M
x : M
inst✝² : CommMonoid M
inst✝¹ : ExistsMulOfLE M
inst✝ : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
y : M
hy : 1 < y
hyx : y ^ (n + 1) < x
z : M
hz : 1 < z
hzy : z ^ 2 ≤ y
⊢ n + 2 ≤ 2 * (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: M : Type u_2
inst✝⁴ : LinearOrder M
inst✝³ : DenselyOrdered M
x : M
inst✝² : CommMonoid M
inst✝¹ : ExistsMulOfLE M
inst✝ : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
y : M
hy : 1 < y
hyx : y ^ (n + 1) < x
z : M
hz : 1 < z
hzy : z ^ 2 ≤ y
⊢ z ^ (2 * (n + 1)) = (z ^ 2) ^ (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: M : Type u_2
inst✝⁴ : LinearOrder M
inst✝³ : DenselyOrdered M
x : M
inst✝² : CommMonoid M
inst✝¹ : ExistsMulOfLE M
inst✝ : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
⊢ ∃ y, 1 < y ∧ y ^ (n + 2) < x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: M : Type u_2
inst✝³ : LinearOrder M
inst✝² : DenselyOrdered M
x : M
inst✝¹ : CommGroup M
inst✝ : IsOrderedCancelMonoid M
hx : x < 1
n : ℕ
⊢ ∃ y, y < 1 ∧ x < y ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH : IsCyclic ↥H
⊢ ∃ a < 1, Subgroup.zpowers a = H

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH : IsCyclic ↥H
⊢ Subgroup.genLTOne H ∈ H

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ ∑ x ∈ s, x ≤ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - ↑(#s))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - ↑(#s)) = ∑ x ∈ r ∩ s, x + #(r \ s) • (c - ↑(#s))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH✝ : IsCyclic ↥H
g : G
hg : g < 1
hH : Subgroup.zpowers g = H
⊢ g = Subgroup.genLTOne H

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Nontrivial ↥(Subgroup.zpowers g2)
⊢ IsCyclic ↥(Subgroup.zpowers g2)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Nontrivial ↥(Subgroup.zpowers g2)
h1 : IsCyclic ↥(Subgroup.zpowers g2)
⊢ Nontrivial ↥(Subgroup.zpowers g1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Nontrivial ↥(Subgroup.zpowers g2)
h1 : IsCyclic ↥(Subgroup.zpowers g2)
h2 : Nontrivial ↥(Subgroup.zpowers g1)
⊢ IsCyclic ↥(Subgroup.zpowers g1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ ∑ x ∈ r ∩ s, x + #(r \ s) • (c - ↑(#s)) ≤ ∑ x ∈ r, x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Ideal

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
⊢ I.FG

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ ∑ x ∈ s, x ≤ ∑ x ∈ Ioc (c - ↑(#s)) c, x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
⊢ g1 = g2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Ideal

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : ⨆ i, f i = closure ↑s
⊢ ∀ x ∈ s, ∃ i, x ∈ f i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Ideal

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
⊢ WellFoundedGT (SemigroupIdeal M)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ ∑ x ∈ s, x ≤ ∑ n ∈ range #s, (c - ↑n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
⊢ ∑ x ∈ r, x ≤ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + ↑(#s))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
⊢ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + ↑(#s)) = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + ↑(#s))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
⊢ ∑ x ∈ s ∩ r, x + #(s \ r) • (c + ↑(#s)) ≤ ∑ x ∈ s, x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
⊢ ∑ x ∈ Ico c (c + ↑(#s)), x ≤ ∑ x ∈ s, x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Bounds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
hg' : BddAbove (g '' range f)
⊢ BddAbove (range fun x ↦ g (f x))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
⊢ ∑ n ∈ range #s, (c + ↑n) ≤ ∑ x ∈ s, x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Bounds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
⊢ range f ⊆ {x | 0 ≤ x}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Bounds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
⊢ BddAbove (range fun x ↦ g (f x))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : Preorder α
inst✝¹ : Monoid β
inst✝ : Preorder β
x✝¹ x✝ : α
⊢ x✝¹ ≤ x✝ → (inl α β) x✝¹ ≤ (inl α β) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : Preorder α
inst✝¹ : Monoid β
inst✝ : Preorder β
x✝¹ x✝ : α
⊢ x✝¹ < x✝ → (inl α β) x✝¹ < (inl α β) x✝

Tactic:
by

Goal state after: