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

Goal state before:
pp: case mk.mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b✝ : M
inst✝ : MulArchimedean M
a : M
ha : a ≠ 1
b : M
hb : b ≠ 1
⊢ mk a ha = mk b hb

Tactic:
simpa using

Goal state after:
case mk.mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b✝ : M
inst✝ : MulArchimedean M
a : M
ha : a ≠ 1
b : M
hb : b ≠ 1
⊢ MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
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
inst✝ : Nontrivial M
x : M
hx : x ≠ 1
⊢ ↑(mk x hx) ≠ ⊤

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a b : M
inst✝ : Nontrivial M
x : M
hx : x ≠ 1
⊢ ¬x = 1
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
ha : 0 < a
⊢ GaloisConnection (fun x ↦ a • x) fun x ↦ x / a

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
ha : 0 < a
⊢ GaloisConnection (fun x ↦ a * x) fun x ↦ x / a
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMulZeroClass α β
inst✝ : FloorDiv α β
f✝ : ι →₀ β
a _a : α
ha : 0 < _a
f _g : ι →₀ β
i : ι
⊢ ((fun x ↦ _a • x) f) i ≤ _g i ↔ f i ≤ ((fun x ↦ mapRange (fun x ↦ x ⌊/⌋ _a) ⋯ x) _g) i

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMulZeroClass α β
inst✝ : FloorDiv α β
f✝ : ι →₀ β
a _a : α
ha : 0 < _a
f _g : ι →₀ β
i : ι
⊢ _a • f i ≤ _g i ↔ f i ≤ _g i ⌊/⌋ _a
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMulZeroClass α β
inst✝ : CeilDiv α β
f✝ : ι →₀ β
a _a : α
ha : 0 < _a
f _g : ι →₀ β
i : ι
⊢ ((fun x ↦ mapRange (fun x ↦ x ⌈/⌉ _a) ⋯ x) f) i ≤ _g i ↔ f i ≤ ((fun x ↦ _a • x) _g) i

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMulZeroClass α β
inst✝ : CeilDiv α β
f✝ : ι →₀ β
a _a : α
ha : 0 < _a
f _g : ι →₀ β
i : ι
⊢ f i ⌈/⌉ _a ≤ _g i ↔ f i ≤ _a • _g i
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
α : Type u_2
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b
x✝ : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : ¬a = 1
hb : ¬b = 1
⊢ mk ↑⟨a, ha⟩ ⋯ = mk ↑⟨b, hb⟩ ⋯

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
α : Type u_2
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b
x✝ : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : ¬a = 1
hb : ¬b = 1
⊢ MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case refine_2.mk
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b : M
α : Type u_2
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b
x✝ : FiniteMulArchimedeanClass M
a : M
hA : MulArchimedeanClass.mk a ≠ ⊤
⊢ MulArchimedeanClass.lift (fun b ↦ if h : b = 1 then ⊤ else ↑(f ⟨b, h⟩)) ⋯ (MulArchimedeanClass.mk a) ≠ ⊤

Tactic:
simpa using

Goal state after:
case refine_2.mk
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b : M
α : Type u_2
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b
x✝ : FiniteMulArchimedeanClass M
a : M
hA : MulArchimedeanClass.mk a ≠ ⊤
⊢ ¬a = 1
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case mk.mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b✝ : M
α : Type u_2
inst✝ : PartialOrder α
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ ≤ mk ↑b ⋯ → f a ≤ f b
a : M
ha : a ≠ 1
b : M
hb : b ≠ 1
hAB : mk a ha ≤ mk b hb
⊢ lift f ⋯ (mk a ha) ≤ lift f ⋯ (mk b hb)

Tactic:
| mk b hb
     => 

Goal state after:
case mk.mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b✝ : M
α : Type u_2
inst✝ : PartialOrder α
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ ≤ mk ↑b ⋯ → f a ≤ f b
a : M
ha : a ≠ 1
b : M
hb : b ≠ 1
hAB : mk a ha ≤ mk b hb
⊢ lift f ⋯ (mk a ha) ≤ lift f ⋯ (mk b hb)
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case mk.mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b✝ : M
α : Type u_2
inst✝ : PartialOrder α
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ ≤ mk ↑b ⋯ → f a ≤ f b
a : M
ha : a ≠ 1
b : M
hb : b ≠ 1
hAB : mk a ha ≤ mk b hb
⊢ lift f ⋯ (mk a ha) ≤ lift f ⋯ (mk b hb)

Tactic:
simpa using

Goal state after:
case mk.mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b✝ : M
α : Type u_2
inst✝ : PartialOrder α
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ ≤ mk ↑b ⋯ → f a ≤ f b
a : M
ha : a ≠ 1
b : M
hb : b ≠ 1
hAB : mk a ha ≤ mk b hb
⊢ f ⟨a, ha⟩ ≤ f ⟨b, hb⟩
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
n : ℕ∞
hn₀ : n ≠ 0
hn : n ≠ ⊤
⊢ ⌈r⌉ₑ < n ↔ r ≤ ↑n - 1

Tactic:
simpa using

Goal state after:
r : ℝ≥0∞
n : ℕ∞
hn₀ : n ≠ 0
hn : n ≠ ⊤
⊢ ⌈r⌉ₑ < n ↔ r ≤ ↑n - 1
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r s : ℝ≥0∞
hrs : r ≤ s
⊢ ⌊r⌋ₑ ≤ ⌊s⌋ₑ

Tactic:
simpa using

Goal state after:
r s : ℝ≥0∞
hrs : r ≤ s
⊢ ↑⌊r⌋ₑ ≤ s
Module: Mathlib.Algebra.Order.Floor.Extended

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

Tactic:
simpa using

Goal state after:
r s : ℝ≥0∞
hrs : r ≤ s
⊢ r ≤ ↑⌈s⌉ₑ
Module: Mathlib.Algebra.Order.Floor.Extended

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

Tactic:
simpa using

Goal state after:
⊢ ⌊0⌋ₑ = 0
Module: Mathlib.Algebra.Order.Floor.Extended

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

Tactic:
simpa using

Goal state after:
⊢ ⌈0⌉ₑ = 0
Module: Mathlib.Algebra.Order.Floor.Extended

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

Tactic:
simpa using

Goal state after:
⊢ ⌊1⌋ₑ = 1
Module: Mathlib.Algebra.Order.Floor.Extended

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

Tactic:
simpa using

Goal state after:
⊢ ⌈1⌉ₑ = 1
Module: Mathlib.Algebra.Order.Floor.Extended

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

Tactic:
simpa using

Goal state after:
r : ℝ≥0∞
⊢ ⌈r⌉ₑ = 0 ↔ r = 0
Module: Mathlib.Algebra.Order.Floor.Extended

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

Tactic:
simpa using

Goal state after:
r : ℝ≥0
⊢ ↑⌈r⌉₊ ≤ ↑⌊r⌋₊ + 1
Module: Mathlib.Algebra.Order.Floor.Extended

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

Tactic:
simpa using

Goal state after:
r : ℝ≥0
⊢ ↑⌈r⌉₊ < ↑r + 1
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:
simpa using

Goal state after:
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : DenselyOrdered α
a b : α
h : ∀ (ε : α), 1 < ε → a / ε ≤ b
ε : α
ε1 : ε < 1
⊢ a * ε ≤ b
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:
simpa using

Goal state after:
H : Type u_1
inst✝² : CommGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedMonoid H
a✝ a : H
⊢ 1 ≤ a → a ≤ 1 → a = 1
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:
simpa using

Goal state after:
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), 1 ≤ a ∨ a ≤ 1
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:
simpa using

Goal state after:
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
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:
simpa using

Goal state after:
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
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:
simpa using

Goal state after:
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 ∈ C
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:
simpa using

Goal state after:
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
⊢ b / a ∈ C ∨ a / b ∈ C
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:
simpa using

Goal state after:
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
⊢ b / a ∈ C
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:
simpa using

Goal state after:
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 ≤ y
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:
simpa using

Goal state after:
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 < x
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: case right
M : Type u_2
inst✝³ : LinearOrder M
inst✝² : DenselyOrdered M
x : M
inst✝¹ : CommGroup M
inst✝ : IsOrderedCancelMonoid M
hx : x < 1
n : ℕ
y : M
hy : 1 < y
hy' : y ^ n < x⁻¹
⊢ x < y⁻¹ ^ n

Tactic:
simpa using

Goal state after:
case right
M : Type u_2
inst✝³ : LinearOrder M
inst✝² : DenselyOrdered M
x : M
inst✝¹ : CommGroup M
inst✝ : IsOrderedCancelMonoid M
hx : x < 1
n : ℕ
y : M
hy : 1 < y
hy' : y ^ n < x⁻¹
⊢ x < (y ^ n)⁻¹
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 : M
hx : x ∈ ↑(closure ↑s)
⊢ ∃ i, x ∈ f i

Tactic:
simpa using

Goal state after:
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 : M
hx : x ∈ ↑(closure ↑s)
⊢ ∃ i, x ∈ f i
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 ∈ s, x

Tactic:
calc
    _ ≤ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + #s) := by
      grw [← sum_inter_add_sum_sdiff r s, ← sum_le_card_nsmul _ _ _ fun x mx ↦ ?_]
      rw [mem_sdiff, mem_Ico] at mx; exact mx.1.2.le
    _ = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + #s) := by
      rw [inter_comm, card_sdiff_comm]
      rw [Int.card_Ico, add_sub_cancel_left, Int.toNat_natCast]
    _ ≤ _ := by
      grw [← sum_inter_add_sum_sdiff s r, card_nsmul_le_sum _ _ _ fun x mx ↦ ?_]
      grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
⊢ Monotone (↑((WithZero.map' (toLexMulEquiv (αˣ × βˣ)).toMonoidHom).comp (MonoidWithZeroHom.inl α β))).toFun

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
⊢ Monotone (⇑(WithZero.map' ↑(toLexMulEquiv (αˣ × βˣ))) ∘ ⇑(MonoidWithZeroHom.inl α β))
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
⊢ Monotone (↑((WithZero.map' (toLexMulEquiv (αˣ × βˣ)).toMonoidHom).comp (MonoidWithZeroHom.inr α β))).toFun

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
⊢ Monotone (⇑(WithZero.map' ↑(toLexMulEquiv (αˣ × βˣ))) ∘ ⇑(MonoidWithZeroHom.inr α β))
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

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

Tactic:
simpa using

Goal state after:
case coe.coe
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
a✝¹ a✝ : Lex (αˣ × βˣ)
⊢ a✝¹ ≤ a✝ → (ofLex a✝¹).1 ≤ (ofLex a✝).1
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
⊢ 0 < |k|

Tactic:
simpa using

Goal state after:
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
⊢ ¬k = 0
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
⊢ Ico (a + 1) b = Ioo a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
⊢ Ico (a + 1) b = Ioo a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a : α
ha : ¬IsMax a
b : α
⊢ Icc (a + 1) b = Ioc a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a : α
ha : ¬IsMax a
b : α
⊢ Icc (a + 1) b = Ioc a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico a (b + 1) = Icc a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico a (b + 1) = Icc a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ioo a (b + 1) = Ioc a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico (a + 1) (b + 1) = Ioc a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico (a + 1) (b + 1) = Ioc a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a ≤ b
⊢ insert a (Icc (a + 1) b) = Icc a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a ≤ b
⊢ insert a (Icc (a + 1) b) = Icc a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a ≤ b + 1
⊢ insert (b + 1) (Icc a b) = Icc a (b + 1)

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a ≤ b + 1
⊢ insert (succ b) (Icc a b) = Icc a (succ b)
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ insert b (Ico a b) = Ico a (b + 1)

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ insert b (Ico a b) = Ico a (b + 1)
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a < b
⊢ insert a (Ico (a + 1) b) = Ico a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a < b
⊢ insert a (Ico (a + 1) b) = Ico a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ insert (b + 1) (Ioc a b) = Ioc a (b + 1)

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ insert (b + 1) (Ioc a b) = Ioc a (b + 1)
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a < b
⊢ insert (a + 1) (Ioc (a + 1) b) = Ioc a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a < b
⊢ insert (a + 1) (Ioc (a + 1) b) = Ioc a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Icc (a + 1) b = Ioc a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Icc (a + 1) b = Ioc a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ico a (b + 1) = Icc a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ico a (b + 1) = Icc a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ioo a (b + 1) = Ioc a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ico (a + 1) (b + 1) = Ioc a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ico (a + 1) (b + 1) = Ioc a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
a b : α
inst✝ : NoMaxOrder α
h : a ≤ b
⊢ insert b (Ico a b) = Ico a (b + 1)

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
a b : α
inst✝ : NoMaxOrder α
h : a ≤ b
⊢ insert b (Ico a b) = Ico a (b + 1)
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

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

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
⊢ Ioc a (b - 1) = Ioo a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
b : α
hb : ¬IsMin b
a : α
⊢ Icc a (b - 1) = Ico a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
b : α
hb : ¬IsMin b
a : α
⊢ Icc a (b - 1) = Ico a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

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

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (a - 1) b = Icc a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioo (a - 1) b = Ico a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioo (a - 1) b = Ico a b