awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a : α
inst_3 : MulLeftStrictMono α
h h₁ : a = a
⊢ a = a * 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a : α
inst_3 : MulLeftStrictMono α
c : α
h : 1 < c → a < a * c
⊢ 1 < c → a ≠ a * c

Tactic:
rw [← (self_le_mul_right a c).lt_iff_ne]

Premises used: self_le_mul_right, LE.le.lt_iff_ne
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a : α
inst_3 : MulLeftStrictMono α
c : α
⊢ 1 < c → a < a * c

Tactic:
apply lt_mul_of_one_lt_right'

Premises used: lt_mul_of_one_lt_right'
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Semigroup α
inst_1 : LE α
inst_2 : CanonicallyOrderedMul α
a b c : α
hbc : (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
obtain :
  ∀ (c : α) (hbc : b ≤ b * c),
    LE.le.{u} (α := α) ((fun (x1 x2 : α) ↦ x1 * x2) a b) ((fun (x1 x2 : α) ↦ x1 * x2) a (b * c))
⊢ LE.le.{u} (α := α) ((fun (x1 x2 : α) ↦ x1 * x2) a b) ((fun (x1 x2 : α) ↦ x1 * x2) a c)

Tactic:
obtain ⟨c, hc, rfl⟩ := exists_mul_of_le hbc

Premises used: rfl, ExistsMulOfLE.exists_mul_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Semigroup α
inst_1 : LE α
inst_2 : CanonicallyOrderedMul α
a b c : α
hbc : b ≤ b * c
rw : ∃ (c_1 : α), (fun (x1 x2 : α) ↦ x1 * x2) a (b * c) = (fun (x1 x2 : α) ↦ x1 * x2) a b * c_1
⊢ LE.le.{u} (α := α) ((fun (x1 x2 : α) ↦ x1 * x2) a b) ((fun (x1 x2 : α) ↦ x1 * x2) a (b * c))

Tactic:
rw [le_iff_exists_mul]

Premises used: le_iff_exists_mul
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Semigroup α
inst_1 : LE α
inst_2 : CanonicallyOrderedMul α
a b c : α
hbc : b ≤ b * c
⊢ ∃ (c_1 : α), (fun (x1 x2 : α) ↦ x1 * x2) a (b * c) = (fun (x1 x2 : α) ↦ x1 * x2) a b * c_1

Tactic:
⟨c, (mul_assoc _ _ _).symm⟩

Premises used: mul_assoc, Exists.intro, Eq.symm
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Semigroup α
inst_1 : LE α
inst_2 : CanonicallyOrderedMul α
a b c : α
hbc : b ≤ b * c
⊢ ∃ (c_1 : α), (fun (x1 x2 : α) ↦ x1 * x2) a (b * c) = (fun (x1 x2 : α) ↦ x1 * x2) a b * c_1

Tactic:
exact ⟨c, (mul_assoc _ _ _).symm⟩
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a b : α
⊢ 1 < a * b ↔ 1 < a ∨ 1 < b

Tactic:
simp only [one_lt_iff_ne_one, Ne, mul_eq_one, not_and_or]

Premises used: Ne, mul_eq_one, not_and_or, one_lt_iff_ne_one
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Monoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedMul α
a b c : α
inl : ∀ (hb : a ≤ b), min a (b * c) = min a (min a b * min a c)
inr : ∀ (hb : b ≤ a), min a (b * c) = min a (min a b * min a c)
⊢ min a (b * c) = min a (min a b * min a c)

Tactic:
rcases le_total a b with hb | hb

Premises used: le_total
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Monoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedMul α
a b c : α
hb : a ≤ b
⊢ min a (b * c) = min a (min a b * min a c)

Tactic:
simp [hb, le_mul_right]

Premises used: le_mul_right
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Monoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
inr : ∀ (hc : a ≤ c), min a (b * c) = min a (min a b * min a c)
inr₁ : ∀ (hc : c ≤ a), min a (b * c) = min a (min a b * min a c)
⊢ min a (b * c) = min a (min a b * min a c)

Tactic:
rcases le_total a c with hc | hc

Premises used: le_total
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Monoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
hc : a ≤ c
⊢ min a (b * c) = min a (min a b * min a c)

Tactic:
simp [hc, le_mul_left]

Premises used: le_mul_left
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Monoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
hc : c ≤ a
⊢ min a (b * c) = min a (min a b * min a c)

Tactic:
simp [hb, hc]
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Monoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedMul α
a b c : α
⊢ min (a * b) c = min (min a c * min b c) c

Tactic:
simpa [min_comm _ c] using min_mul_distrib c a b

Premises used: min_comm, min_mul_distrib
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Monoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedMul α
inst_3 : OrderBot α
⊢ Eq.{u + 1} (α := α) ⊥ 1

Tactic:
bot_eq_one

Premises used: bot_eq_one
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α_1 : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
a b : α
h : a ≤ b
c : α
rw : a + c ≤ b + c
⊢ c + a ≤ c + b

Tactic:
rw [add_comm c, add_comm c]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α_1 : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
a b : α
h : a ≤ b
c : α
⊢ a + c ≤ b + c

Tactic:
add_le_add_left a b h c
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α_1 : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
a b : α
h : a ≤ b
c : α
⊢ a + c ≤ b + c

Tactic:
exact add_le_add_left a b h c
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
a b : α
h : a ≤ b
c : α
rw : a * c ≤ b * c
⊢ c * a ≤ c * b

Tactic:
rw [mul_comm c, mul_comm c]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
a b : α
h : a ≤ b
c : α
⊢ a * c ≤ b * c

Tactic:
mul_le_mul_left a b h c
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
a b : α
h : a ≤ b
c : α
⊢ a * c ≤ b * c

Tactic:
exact mul_le_mul_left a b h c
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α_1 : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
add_le_add_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
toIsOrderedAddMonoid : IsOrderedAddMonoid α := ⋯
le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
a b c : α
h : b + a ≤ c + a
⊢ a + b ≤ a + c

Tactic:
rw [add_comm _ a, add_comm _ a] at h

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α_1 : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
add_le_add_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
toIsOrderedAddMonoid : IsOrderedAddMonoid α := ⋯
le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
a b c : α
h : a + b ≤ a + c
⊢ b ≤ c

Tactic:
le_of_add_le_add_left a b c h
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α_1 : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
add_le_add_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
toIsOrderedAddMonoid : IsOrderedAddMonoid α := ⋯
le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
a b c : α
h : a + b ≤ a + c
⊢ b ≤ c

Tactic:
exact le_of_add_le_add_left a b c h
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
mul_le_mul_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b
toIsOrderedMonoid : IsOrderedMonoid α := ⋯
le_of_mul_le_mul_left : ∀ (a b c : α), a * b ≤ a * c → b ≤ c
a b c : α
h : b * a ≤ c * a
⊢ a * b ≤ a * c

Tactic:
rw [mul_comm _ a, mul_comm _ a] at h

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
mul_le_mul_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b
toIsOrderedMonoid : IsOrderedMonoid α := ⋯
le_of_mul_le_mul_left : ∀ (a b c : α), a * b ≤ a * c → b ≤ c
a b c : α
h : a * b ≤ a * c
⊢ b ≤ c

Tactic:
le_of_mul_le_mul_left a b c h
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
mul_le_mul_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b
toIsOrderedMonoid : IsOrderedMonoid α := ⋯
le_of_mul_le_mul_left : ∀ (a b c : α), a * b ≤ a * c → b ≤ c
a b c : α
h : a * b ≤ a * c
⊢ b ≤ c

Tactic:
exact le_of_mul_le_mul_left a b c h
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
⊢ MulRightReflectLT α

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b : α
h : a ≤ b
c : α
inl : ∀ (h : a ≤ a), a * c ≤ a * c
inr : ∀ (h : a < b), a * c ≤ b * c
⊢ a * c ≤ b * c

Tactic:
obtain rfl | h := eq_or_lt_of_le h

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a c : α
h : a ≤ a
⊢ a * c ≤ a * c

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b : α
h_1 : a ≤ b
c : α
h : a < b
⊢ a * c ≤ b * c

Tactic:
simpa [mul_comm] using (hmul _ _ _ h).le

Premises used: LT.lt.le, mul_comm
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b c : α
h : a * b ≤ a * c
contrapose! : ∀ (h : c < b), a * c < a * b
⊢ b ≤ c

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b c : α
h : c < b
⊢ a * c < a * b

Tactic:
hmul _ _ _ h
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b c : α
h : c < b
⊢ a * c < a * b

Tactic:
exact hmul _ _ _ h
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
h : 1 ≤ a * a
contrapose! : ∀ (h : a < 1), a * a < 1
⊢ 1 ≤ a

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
h : a < 1
⊢ a * a < 1

Tactic:
mul_lt_one' h h

Premises used: mul_lt_one'
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
h : a < 1
⊢ a * a < 1

Tactic:
exact mul_lt_one' h h

Premises used: mul_lt_one'
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
h : 1 < a * a
contrapose! : ∀ (h : a ≤ 1), a * a ≤ 1
⊢ 1 < a

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
h : a ≤ 1
⊢ a * a ≤ 1

Tactic:
mul_le_one' h h

Premises used: mul_le_one'
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
h : a ≤ 1
⊢ a * a ≤ 1

Tactic:
exact mul_le_one' h h

Premises used: mul_le_one'
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
contrapose! : 1 < a * a ↔ 1 < a
⊢ a * a ≤ 1 ↔ a ≤ 1

Tactic:
contrapose!
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ 1 < a * a ↔ 1 < a

Tactic:
one_lt_mul_self_iff

Premises used: one_lt_mul_self_iff
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ 1 < a * a ↔ 1 < a

Tactic:
exact one_lt_mul_self_iff

Premises used: one_lt_mul_self_iff
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
contrapose! : 1 ≤ a * a ↔ 1 ≤ a
⊢ a * a < 1 ↔ a < 1

Tactic:
contrapose!
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ 1 ≤ a * a ↔ 1 ≤ a

Tactic:
one_le_mul_self_iff

Premises used: one_le_mul_self_iff
-- Module: Mathlib.Algebra.Order.Monoid.Defs
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ 1 ≤ a * a ↔ 1 ≤ a

Tactic:
exact one_le_mul_self_iff

Premises used: one_le_mul_self_iff
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : Monoid β
inst_3 : Preorder β
x x_1 : α
⊢ x ≤ x_1 → LE.le (α := α × β) ((inl α β : (a : α) → α × β) x : α × β) ((inl α β : (a : α) → α × β) x_1 : α × β)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : Monoid β
inst_3 : Preorder β
x x_1 : α
⊢ x < x_1 → LT.lt (α := α × β) ((inl α β : (a : α) → α × β) x : α × β) ((inl α β : (a : α) → α × β) x_1 : α × β)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : Monoid β
inst_3 : Preorder β
x x_1 : β
⊢ x ≤ x_1 → LE.le (α := α × β) ((inr α β : (a : β) → α × β) x : α × β) ((inr α β : (a : β) → α × β) x_1 : α × β)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : Monoid β
inst_3 : Preorder β
x x_1 : β
⊢ x < x_1 → LT.lt (α := α × β) ((inr α β : (a : β) → α × β) x : α × β) ((inr α β : (a : β) → α × β) x_1 : α × β)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : Monoid β
inst_3 : Preorder β
x x_1 : α × β
⊢ x ≤ x_1 → LE.le.{u_1} (α := α) ((fst α β : (a : α × β) → α) x : α) ((fst α β : (a : α × β) → α) x_1 : α)

Tactic:
simp +contextual [Prod.le_def]

Premises used: Prod.le_def
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : Monoid β
inst_3 : Preorder β
x x_1 : α × β
⊢ x ≤ x_1 → LE.le.{u_2} (α := β) ((snd α β : (a : α × β) → β) x : β) ((snd α β : (a : α × β) → β) x_1 : β)

Tactic:
simp +contextual [Prod.le_def]

Premises used: Prod.le_def
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : PartialOrder α
inst_2 : Monoid β
inst_3 : Preorder β
⊢ ∀ (x y : α),
    OrderHom.toFun (OrderHom.comp Prod.Lex.toLexOrderHom (↑(inl α β) : α →o α × β)) (x * y) =
      OrderHom.toFun (OrderHom.comp Prod.Lex.toLexOrderHom (↑(inl α β) : α →o α × β)) x *
        OrderHom.toFun (OrderHom.comp Prod.Lex.toLexOrderHom (↑(inl α β) : α →o α × β)) y

Tactic:
simp [← toLex_mul]

Premises used: toLex_mul
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : PartialOrder α
inst_2 : Monoid β
inst_3 : Preorder β
⊢ ∀ (x y : β),
    OrderHom.toFun (OrderHom.comp Prod.Lex.toLexOrderHom (↑(inr α β) : β →o α × β)) (x * y) =
      OrderHom.toFun (OrderHom.comp Prod.Lex.toLexOrderHom (↑(inr α β) : β →o α × β)) x *
        OrderHom.toFun (OrderHom.comp Prod.Lex.toLexOrderHom (↑(inr α β) : β →o α × β)) y

Tactic:
simp [← toLex_mul]

Premises used: toLex_mul
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : PartialOrder α
inst_2 : Monoid β
inst_3 : Preorder β
⊢ ∀ (x y : Lex (α × β)),
    ((ofLex : (a : Lex (α × β)) → α × β) (x * y)).1 =
      HMul.hMul (α := α) ((ofLex : (a : Lex (α × β)) → α × β) x).1 ((ofLex : (a : Lex (α × β)) → α × β) y).1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : PartialOrder α
inst_2 : Monoid β
inst_3 : Preorder β
⊢ Eq (α := α →*o α) (comp (fst α β) (inl α β)) (OrderMonoidHom.id α)

Tactic:
rfl

Premises used: OrderMonoidHom.id, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : PartialOrder α
inst_2 : Monoid β
inst_3 : Preorder β
⊢ Eq (α := α →*o α) (comp (fstₗ α β) (inlₗ α β)) (OrderMonoidHom.id α)

Tactic:
rfl

Premises used: OrderMonoidHom.id, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : PartialOrder α
inst_2 : Monoid β
inst_3 : Preorder β
⊢ Eq (α := α →*o β) (comp (snd α β) (inl α β)) 1

Tactic:
rfl

Premises used: OrderMonoidHom.comp, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : PartialOrder α
inst_2 : Monoid β
inst_3 : Preorder β
⊢ Eq (α := β →*o α) (comp (fst α β) (inr α β)) 1

Tactic:
rfl

Premises used: OrderMonoidHom.comp, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : PartialOrder α
inst_2 : Monoid β
inst_3 : Preorder β
⊢ Eq (α := β →*o β) (comp (snd α β) (inr α β)) (OrderMonoidHom.id β)

Tactic:
rfl

Premises used: OrderMonoidHom.id, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : PartialOrder α
inst_2 : Monoid β
inst_3 : Preorder β
m : α
n : β
⊢ HMul.hMul (α := α × β) (β := α × β) ((inl α β : (a : α) → α × β) m : α × β) ((inr α β : (a : β) → α × β) n : α × β) =
    (m, n)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : PartialOrder α
inst_2 : Monoid β
inst_3 : Preorder β
m : α
n : β
⊢ HMul.hMul (α := Lex (α × β)) (β := Lex (α × β)) ((inlₗ α β : (a : α) → Lex (α × β)) m : Lex (α × β))
      ((inrₗ α β : (a : β) → Lex (α × β)) n : Lex (α × β)) =
    (toLex : (a : α × β) → Lex (α × β)) (m, n)

Tactic:
simp [← toLex_mul]

Premises used: toLex_mul
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : PartialOrder α
inst_2 : Monoid β
inst_3 : Preorder β
m : α
n : β
⊢ Commute (S := α × β) ((inl α β : (a : α) → α × β) m : α × β) ((inr α β : (a : β) → α × β) n : α × β)

Tactic:
Commute.prod (.one_right m) (.one_left n)

Premises used: Commute.prod, Commute.one_right, Commute.one_left
-- Module: Mathlib.Algebra.Order.Monoid.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : PartialOrder α
inst_2 : Monoid β
inst_3 : Preorder β
m : α
n : β
⊢ Commute (S := Lex (α × β)) ((inlₗ α β : (a : α) → Lex (α × β)) m : Lex (α × β))
    ((inrₗ α β : (a : β) → Lex (α × β)) n : Lex (α × β))

Tactic:
Commute.prod (.one_right m) (.one_left n)

Premises used: Commute.prod, Lex, Commute.one_right, Commute.one_left
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c : M
h : ∀ (x : M), x ∈ Ico (a * c) (b * c) ↔ x ∈ map (mulRightEmbedding c) (Ico a b)
⊢ Ico (a * c) (b * c) = map (mulRightEmbedding c) (Ico a b)

Tactic:
ext x
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c x : M
h : a * c ≤ x ∧ x < b * c ↔ ∃ (a_1 : M), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = x
⊢ x ∈ Ico (a * c) (b * c) ↔ x ∈ map (mulRightEmbedding c) (Ico a b)

Tactic:
simp only [mem_Ico, mem_map, mulRightEmbedding_apply]

Premises used: mulRightEmbedding_apply, Finset.mem_map, Finset.mem_Ico
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c x : M
h : a * c ≤ x ∧ x < b * c → ∃ (a_2 : M), (a ≤ a_2 ∧ a_2 < b) ∧ a_2 * c = x
h₁ : (∃ (a_1 : M), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = x) → a * c ≤ x ∧ x < b * c
⊢ a * c ≤ x ∧ x < b * c ↔ ∃ (a_1 : M), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = x

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c x : M
h₁ : a * c ≤ x
h₂ : x < b * c
h : ∀ (d : M) (h₁ : a * c ≤ a * c * d) (h₂ : a * c * d < b * c), ∃ (a_1 : M), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = a * c * d
⊢ ∃ (a_1 : M), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = x

Tactic:
obtain ⟨d, rfl⟩ := exists_mul_of_le h₁

Premises used: rfl, ExistsMulOfLE.exists_mul_of_le
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c d : M
h₁ : a * c ≤ a * c * d
h₂ : a * c * d < b * c
⊢ a ≤ a * d

Tactic:
simpa using h₁
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c d : M
h₁ : a * c ≤ a * c * d
h₂ : a * c * d < b * c
⊢ a * d < b

Tactic:
simpa [mul_right_comm a c d] using h₂

Premises used: mul_right_comm
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c d : M
h₁ : a * c ≤ a * c * d
h₂ : a * c * d < b * c
simp_rw : a * (d * c) = a * (c * d)
⊢ a * d * c = a * c * d

Tactic:
simp_rw [mul_assoc, mul_comm]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c d : M
h₁ : a * c ≤ a * c * d
h₂ : a * c * d < b * c
⊢ ∃ (a_1 : M), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = a * c * d

Tactic:
exact ⟨a * d, ⟨by simpa using h₁, by simpa [mul_right_comm a c d] using h₂⟩,
        by simp_rw [mul_assoc, mul_comm]⟩
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c x : M
⊢ (∃ (a_1 : M), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = x) → a * c ≤ x ∧ x < b * c

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c : M
⊢ Ico (a * c) (b * c) = map (mulRightEmbedding c) (Ico a b)

Tactic:
have : (Ico (a * c) (b * c)) = (Ico a b).map (mulRightEmbedding c) := by
    ext x
    simp only [mem_Ico, mem_map, mulRightEmbedding_apply]
    constructor
    · rintro ⟨h₁, h₂⟩
      obtain ⟨d, rfl⟩ := exists_mul_of_le h₁
      exact ⟨a * d, ⟨by simpa using h₁, by simpa [mul_right_comm a c d] using h₂⟩,
        by simp_rw [mul_assoc, mul_comm]⟩
    · aesop
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c : M
this : Ico (a * c) (b * c) = map (mulRightEmbedding c) (Ico a b)
⊢ #(Ico (a * c) (b * c)) = #(Ico a b)

Tactic:
simp [this]