mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
⊢ ↑s ⊆ ↑(Finset.cons i s hi)

Tactic:
simp

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
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
h : mk (a i) = mk (a (s.min' hs))
⊢ i ∈ ↑(Finset.cons i s hi)

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
⊢ 1 1 = 1

Tactic:
simp

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
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (a i) < mk (∏ i ∈ s, a i)
⊢ i ∈ Finset.cons i s hi

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → ArithmeticFunction R
hf : ∀ i ∈ ∅, (f i).IsMultiplicative
⊢ (∏ i ∈ ∅, f i).IsMultiplicative

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
⊢ (f ^ 0).IsMultiplicative

Tactic:
simp

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
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (a i) < mk (∏ i ∈ s, a i)
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
⊢ i ∈ ↑(Finset.cons i s hi)

Tactic:
simp

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
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
s : Finset ι
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
y : ι
hi : y ∉ s
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons y s hi)
hminmem : s.min' hs ∈ Finset.cons y s hi
hne : mk (a y) ≠ mk (∏ i ∈ s, a i)
hlt : mk (∏ i ∈ s, a i) < mk (a y)
hy : y ∈ Finset.cons y s hi
⊢ y ∈ ↑(Finset.cons y s hi)

Tactic:
simp

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 b : M
s : UpperSet (MulArchimedeanClass M)
hs : ¬s = ⊤
u : MulArchimedeanClass M
hu : u ∈ ↑s
⊢ u ≤ ⊤

Tactic:
simp

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

Goal state before:
pp: case inr.inl
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
hs : s ≠ ⊤
hst : s ≤ ⊤
⊢ subgroup ⊤ ≤ subgroup s

Tactic:
simp

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 : MulArchimedeanClass M
⊢ a ∈ c.closedBallSubgroup ↔ c ≤ mk a

Tactic:
simp

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

Goal state before:
pp: case e'_5
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
⊢ UpperSet.Ioi ⊤ = ⊤

Tactic:
simp

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
x✝ : M
⊢ x✝ ∈ ⊤.closedBallSubgroup ↔ x✝ ∈ ⊥

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMulZeroClass α β
inst✝ : FloorDiv α β
b : β
⊢ b ⌊/⌋ 0 = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMulZeroClass α β
inst✝ : CeilDiv α β
b : β
⊢ b ⌈/⌉ 0 = 0

Tactic:
simp

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

Goal state before:
pp: case inl
K : Type u_2
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
a : K
⊢ ⌊a / ↑0⌋₊ = ⌊a⌋₊ / 0

Tactic:
simp

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

Goal state before:
pp: case top
⊢ ⌊∞⌋ₑ = ⊤ ↔ ∞ = ∞

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case top
⊢ ⌈∞⌉ₑ = ⊤ ↔ ∞ = ∞

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case top
⊢ ⌊∞⌋ₑ < ⊤ ↔ ∞ < ∞

Tactic:
simp

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

Goal state before:
pp: case coe
x✝ : ℝ≥0
⊢ ⌊↑x✝⌋ₑ < ⊤ ↔ ↑x✝ < ∞

Tactic:
simp

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

Goal state before:
pp: case top
⊢ ⌈∞⌉ₑ < ⊤ ↔ ∞ < ∞

Tactic:
simp

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

Goal state before:
pp: case coe
x✝ : ℝ≥0
⊢ ⌈↑x✝⌉ₑ < ⊤ ↔ ↑x✝ < ∞

Tactic:
simp

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

Goal state before:
pp: case top.top
⊢ ⌈∞⌉ₑ ≤ ⊤ ↔ ∞ ≤ ↑⊤

Tactic:
simp

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

Goal state before:
pp: case top.coe
a✝ : ℕ
⊢ ⌈∞⌉ₑ ≤ ↑a✝ ↔ ∞ ≤ ↑↑a✝

Tactic:
simp

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

Goal state before:
pp: case coe.top
x✝ : ℝ≥0
⊢ ⌈↑x✝⌉ₑ ≤ ⊤ ↔ ↑x✝ ≤ ↑⊤

Tactic:
simp

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

Goal state before:
pp: case coe.coe
x✝ : ℝ≥0
a✝ : ℕ
⊢ ⌈↑x✝⌉ₑ ≤ ↑a✝ ↔ ↑x✝ ≤ ↑↑a✝

Tactic:
simp

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 b : M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
e : MulArchimedeanClass M ≃o MulArchimedeanClass N
⊢ ∀ (a : MulArchimedeanClass M), a ≠ ⊤ ↔ ↑e a ≠ ⊤

Tactic:
simp

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 b : M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
e : MulArchimedeanClass M ≃o MulArchimedeanClass N
⊢ ∀ {a b : FiniteMulArchimedeanClass M}, ((↑e).subtypeEquiv ⋯) a ≤ ((↑e).subtypeEquiv ⋯) b ↔ a ≤ b

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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
⊢ n / d = ↑(n / d)

Tactic:
Nat.cast_id

Goal state after:
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
⊢ n / d = n / d
Module: Mathlib.Algebra.Order.Floor.Extended

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: a : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Ioi a ↔ x✝ ∈ Ioi ⌊a⌋ₑ

Tactic:
simp

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

Goal state before:
pp: a : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Iio a ↔ x✝ ∈ Iio ⌈a⌉ₑ

Tactic:
simp

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

Goal state before:
pp: a : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Iic a ↔ x✝ ∈ Iic ⌊a⌋ₑ

Tactic:
simp

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

Goal state before:
pp: a : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Ici a ↔ x✝ ∈ Ici ⌈a⌉ₑ

Tactic:
simp

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

Goal state before:
pp: a b : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Icc a b ↔ x✝ ∈ Icc ⌈a⌉ₑ ⌊b⌋ₑ

Tactic:
simp

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

Goal state before:
pp: a b : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Ico a b ↔ x✝ ∈ Ico ⌈a⌉ₑ ⌈b⌉ₑ

Tactic:
simp

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

Goal state before:
pp: a b : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Ioc a b ↔ x✝ ∈ Ioc ⌊a⌋ₑ ⌊b⌋ₑ

Tactic:
simp

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

Goal state before:
pp: a b : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Ioo a b ↔ x✝ ∈ Ioo ⌊a⌋ₑ ⌈b⌉ₑ

Tactic:
simp

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:
simp

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:
simp

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

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ range #s
⊢ c - ↑x ∈ Ioc (c - ↑(#s)) c

Tactic:
rw [mem_Ioc]

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ range #s
⊢ c - ↑(#s) < c - ↑x ∧ c - ↑x ≤ c
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:
simp

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:
simp

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✝ → (inr α β) x✝¹ ≤ (inr α β) x✝

Tactic:
simp

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✝ → (inr α β) x✝¹ < (inr α β) x✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : PartialOrder α
inst✝¹ : Monoid β
inst✝ : Preorder β
⊢ ∀ (x y : Lex (α × β)), (ofLex (x * y)).1 = (ofLex x).1 * (ofLex y).1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : PartialOrder α
inst✝¹ : Monoid β
inst✝ : Preorder β
m : α
n : β
⊢ (inl α β) m * (inr α β) n = (m, n)

Tactic:
simp

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

Goal state before:
pp: case zero.zero
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
⊢ 0 ≤ 0 →
    (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun 0 ≤
      (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun 0

Tactic:
simp

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

Goal state before:
pp: case zero.coe
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
a✝ : Lex (αˣ × βˣ)
⊢ 0 ≤ ↑a✝ →
    (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun 0 ≤
      (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun ↑a✝

Tactic:
simp

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

Goal state before:
pp: case coe.zero
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
a✝ : Lex (αˣ × βˣ)
⊢ ↑a✝ ≤ 0 →
    (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun ↑a✝ ≤
      (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun 0

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
⊢ ((fst α β).comp (inl α β)) 0 = (OrderMonoidWithZeroHom.id α) 0

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
w✝ : αˣ
⊢ ((fst α β).comp (inl α β)) ↑w✝ = (OrderMonoidWithZeroHom.id α) ↑w✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
m : αˣ
hm : ↑m ≠ 0
⊢ (inl α β) ↑m = ↑((OrderMonoidHom.inlₗ αˣ βˣ) (Units.mk0 (↑m) hm))

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
n : βˣ
hn : ↑n ≠ 0
⊢ (inr α β) ↑n = ↑((OrderMonoidHom.inrₗ αˣ βˣ) (Units.mk0 (↑n) hn))

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
⊢ 0 < 1

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ 0 ≤ |a|

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this✝ : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
this : n • |a| = (n • 1) • |a|
⊢ 0 ≤ |a|

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α →o β
⊢ ⇑f '' ↑⊥ ⊆ ↑(map f ⊥)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioc (a - 1) b = Icc a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_left_eq_Icc a b

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t : NonemptyInterval α
h : s * t = 1
⊢ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1

Tactic:
rw [NonemptyInterval.ext_iff, Prod.ext_iff] at h
    have := (mul_le_mul_iff_of_ge s.fst_le_snd t.fst_le_snd).1 (h.2.trans h.1.symm).le
    refine ⟨s.fst, t.fst, ?_, ?_, h.1⟩ <;> apply NonemptyInterval.ext <;> dsimp [pure]
    · nth_rw 2 [this.1]
    · nth_rw 2 [this.2]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: case bot
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
t : Interval α
⊢ ⊥ * t = 1 ↔ ∃ a b, ⊥ = pure a ∧ t = pure b ∧ a * b = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: case coe.bot
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a✝ : NonemptyInterval α
⊢ ↑a✝ * ⊥ = 1 ↔ ∃ a b, ↑a✝ = pure a ∧ ⊥ = pure b ∧ a * b = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s t : Interval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
⊢ ∀ (x : Interval α), - -x = x

Tactic:
rintro (_ | s) <;> first | rfl | exact congr_arg WithBot.some (neg_neg _)

Goal state after:
Module: Mathlib.Data.Finset.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
x : α × α
⊢ x.swap ∈ mulAntidiagonal hs ht a ↔ x ∈ mulAntidiagonal ht hs a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: α : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
x✝ : Interval α
⊢ (⊥ + x✝).length ≤ ⊥.length + x✝.length

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: α : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
x✝ : Interval α
⊢ (x✝ + ⊥).length ≤ x✝.length + ⊥.length

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
⊢ (Function.support 0).IsPWO

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero S
f : ZeroHom R S
x✝ : Γ
⊢ (map 0 f).coeff x✝ = coeff 0 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
i : Γ
hi : i < order 0
⊢ coeff 0 i = 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a b : Γ
r : R
⊢ { coeff := ⇑0, isPWO_support' := ⋯ } = 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case inl
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
⊢ (embDomain f 0).orderTop = WithTop.map (⇑f) (orderTop 0)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
⊢ x.orderTop = ↑(x.orderTop.untop ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : PartialOrder Γ
V : Type u_8
inst✝² : Zero V
inst✝¹ : SMulZeroClass R V
inst✝ : DecidableLT Γ
c : Γ
r : R
x : V⟦Γ⟧
x✝ : Γ
⊢ ((truncLT c) (r • x)).coeff x✝ = (r • (truncLT c) x).coeff x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : AddMonoid S
f : R →+ S
x y : R⟦Γ⟧
x✝ : Γ
⊢ ((x + y).map f).coeff x✝ = (x.map f + y.map f).coeff x✝

Tactic:
simp

Goal state after: