awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : Preorder α
inst_2 : ZeroLEOneClass α
inst_3 : AddLeftMono α
⊢ 0 ≤ HAdd.hAdd (α := α) 2 1

Tactic:
exact add_nonneg zero_le_two zero_le_one

Premises used: add_nonneg, zero_le_one, zero_le_two
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : Preorder α
inst_2 : ZeroLEOneClass α
inst_3 : AddLeftMono α
rw : 0 ≤ HAdd.hAdd (α := α) 3 1
⊢ LE.le.{u_1} (α := α) 0 4

Tactic:
rw [← three_add_one_eq_four]

Premises used: three_add_one_eq_four
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : Preorder α
inst_2 : ZeroLEOneClass α
inst_3 : AddLeftMono α
⊢ 0 ≤ HAdd.hAdd (α := α) 3 1

Tactic:
add_nonneg zero_le_three zero_le_one

Premises used: zero_le_three, add_nonneg, zero_le_one
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : Preorder α
inst_2 : ZeroLEOneClass α
inst_3 : AddLeftMono α
⊢ 0 ≤ HAdd.hAdd (α := α) 3 1

Tactic:
exact add_nonneg zero_le_three zero_le_one

Premises used: zero_le_three, add_nonneg, zero_le_one
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : LE α
inst_2 : ZeroLEOneClass α
inst_3 : AddLeftMono α
bc : LE.le.{u_1} (α := α) 0 1
⊢ HAdd.hAdd (α := α) 1 0 ≤ HAdd.hAdd (α := α) 1 1

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : LE α
inst_2 : ZeroLEOneClass α
inst_3 : AddLeftMono α
⊢ LE.le.{u_1} (α := α) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : LE α
inst_2 : ZeroLEOneClass α
inst_3 : AddLeftMono α
⊢ LE.le.{u_1} (α := α) 0 1

Tactic:
exact zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : LE α
inst_2 : ZeroLEOneClass α
inst_3 : AddRightMono α
bc : LE.le.{u_1} (α := α) 0 1
⊢ HAdd.hAdd (α := α) 0 1 ≤ HAdd.hAdd (α := α) 1 1

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : LE α
inst_2 : ZeroLEOneClass α
inst_3 : AddRightMono α
⊢ LE.le.{u_1} (α := α) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : LE α
inst_2 : ZeroLEOneClass α
inst_3 : AddRightMono α
⊢ LE.le.{u_1} (α := α) 0 1

Tactic:
exact zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftMono α
⊢ LT.lt.{u_1} (α := α) 0 2

Tactic:
zero_lt_one.trans_le one_le_two

Premises used: zero_lt_one, LT.lt.trans_le, one_le_two
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftMono α
rw : 0 < HAdd.hAdd (α := α) 2 1
⊢ LT.lt.{u_1} (α := α) 0 3

Tactic:
rw [← two_add_one_eq_three]

Premises used: two_add_one_eq_three
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftMono α
⊢ 0 < HAdd.hAdd (α := α) 2 1

Tactic:
lt_add_of_lt_of_nonneg zero_lt_two zero_le_one

Premises used: lt_add_of_lt_of_nonneg, zero_le_one, zero_lt_two
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftMono α
⊢ 0 < HAdd.hAdd (α := α) 2 1

Tactic:
exact lt_add_of_lt_of_nonneg zero_lt_two zero_le_one

Premises used: lt_add_of_lt_of_nonneg, zero_le_one, zero_lt_two
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftMono α
rw : 0 < HAdd.hAdd (α := α) 3 1
⊢ LT.lt.{u_1} (α := α) 0 4

Tactic:
rw [← three_add_one_eq_four]

Premises used: three_add_one_eq_four
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftMono α
⊢ 0 < HAdd.hAdd (α := α) 3 1

Tactic:
lt_add_of_lt_of_nonneg zero_lt_three zero_le_one

Premises used: lt_add_of_lt_of_nonneg, zero_lt_three, zero_le_one
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftMono α
⊢ 0 < HAdd.hAdd (α := α) 3 1

Tactic:
exact lt_add_of_lt_of_nonneg zero_lt_three zero_le_one

Premises used: lt_add_of_lt_of_nonneg, zero_lt_three, zero_le_one
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftMono α
⊢ LT.lt.{u_1} (α := α) 0 2

Tactic:
zero_lt_two

Premises used: zero_lt_two
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftMono α
⊢ LT.lt.{u_1} (α := α) 0 3

Tactic:
zero_lt_three

Premises used: zero_lt_three
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftMono α
⊢ LT.lt.{u_1} (α := α) 0 4

Tactic:
zero_lt_four

Premises used: zero_lt_four
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftMono α
⊢ NeZero.{u_1} (R := α) 2

Tactic:
⟨zero_lt_two.ne'⟩

Premises used: NeZero.mk, LT.lt.ne', zero_lt_two
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftMono α
⊢ NeZero.{u_1} (R := α) 3

Tactic:
⟨zero_lt_three.ne'⟩

Premises used: NeZero.mk, zero_lt_three, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftMono α
⊢ NeZero.{u_1} (R := α) 4

Tactic:
⟨zero_lt_four.ne'⟩

Premises used: NeZero.mk, LT.lt.ne', zero_lt_four
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftStrictMono α
rw : 1 < HAdd.hAdd (α := α) 1 1
⊢ LT.lt.{u_1} (α := α) 1 2

Tactic:
rw [← one_add_one_eq_two]

Premises used: one_add_one_eq_two
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftStrictMono α
⊢ 1 < HAdd.hAdd (α := α) 1 1

Tactic:
lt_add_one _

Premises used: lt_add_one
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftStrictMono α
⊢ 1 < HAdd.hAdd (α := α) 1 1

Tactic:
exact lt_add_one _

Premises used: lt_add_one
-- Module: Mathlib.Algebra.Order.Monoid.PNat
Goal:
x : ℕ+
⊢ Membership.mem (γ := Submonoid ℕ) (nonZeroDivisors ℕ) (↑x : ℕ)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.PNat
Goal:
x : ↥(nonZeroDivisors ℕ)
⊢ 0 < (↑x : ℕ)

Tactic:
simp [Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.Algebra.Order.Monoid.PNat
Goal:
⊢ ∀ (x y : ℕ+),
    Subtype.mk (p := fun (x : ℕ) ↦ Membership.mem (γ := Submonoid ℕ) (nonZeroDivisors ℕ) x) (↑(x * y) : ℕ) ⋯ =
      Subtype.mk (p := fun (x : ℕ) ↦ Membership.mem (γ := Submonoid ℕ) (nonZeroDivisors ℕ) x) (↑x : ℕ) ⋯ *
        Subtype.mk (p := fun (x : ℕ) ↦ Membership.mem (γ := Submonoid ℕ) (nonZeroDivisors ℕ) x) (↑y : ℕ) ⋯

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.PNat
Goal:
⊢ ∀ {a b : ℕ+},
    Subtype.mk (p := fun (x : ℕ) ↦ Membership.mem (γ := Submonoid ℕ) (nonZeroDivisors ℕ) x) (↑a : ℕ) ⋯ ≤
        Subtype.mk (p := fun (x : ℕ) ↦ Membership.mem (γ := Submonoid ℕ) (nonZeroDivisors ℕ) x) (↑b : ℕ) ⋯ ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Prod
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedCancelMonoid α
inst_3 : CommMonoid β
inst_4 : Preorder β
inst_5 : IsOrderedCancelMonoid β
⊢ IsOrderedCancelMonoid (α × β)

Tactic:
{ le_of_mul_le_mul_left :=
      fun _ _ _ h ↦ ⟨le_of_mul_le_mul_left' h.1, le_of_mul_le_mul_left' h.2⟩ }

Premises used: IsOrderedCancelMonoid._proof_1, And.right, And.left, And.intro, Prod, le_of_mul_le_mul_left', IsOrderedCancelMonoid.mk
-- Module: Mathlib.Algebra.Order.Monoid.Prod
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
inst_2 : Mul α
inst_3 : Mul β
inst_4 : ExistsMulOfLE α
inst_5 : ExistsMulOfLE β
⊢ ExistsMulOfLE (α × β)

Tactic:
⟨fun h =>
    let ⟨c, hc⟩ := exists_mul_of_le h.1
    let ⟨d, hd⟩ := exists_mul_of_le h.2
    ⟨(c, d), Prod.ext hc hd⟩⟩

Premises used: HMul.hMul, _private.0.Prod.instExistsMulOfLE.match_2, Exists, Prod.mk, ExistsMulOfLE.mk, _private.0.Prod.instExistsMulOfLE.match_1, And.right, And.left, Prod.ext, Exists.intro, Eq, ExistsMulOfLE.exists_mul_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Prod
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
inst_3 : CommMonoid β
inst_4 : Preorder β
inst_5 : IsOrderedMonoid β
x x_1 : Lex (α × β)
hxy_1 : x ≤ x_1
z : Lex (α × β)
hxy :
  Eq.{u_1 + 1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) x).1 ((ofLex : (a : Lex (α × β)) → α × β) x_1).1 ∧
    LE.le.{u_2} (α := β) ((ofLex : (a : Lex (α × β)) → α × β) x).2 ((ofLex : (a : Lex (α × β)) → α × β) x_1).2
⊢ Eq.{u_1 + 1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) (x * z)).1
    ((ofLex : (a : Lex (α × β)) → α × β) (x_1 * z)).1

Tactic:
simp only [ofLex_mul, fst_mul, hxy.1]

Premises used: Prod.fst_mul, And.left, ofLex_mul
-- Module: Mathlib.Algebra.Order.Monoid.Submonoid
Goal:
M : Type u_1
S : Type u_2
inst : SetLike S M
inst_1 : CommMonoid M
inst_2 : Preorder M
inst_3 : IsOrderedMonoid M
inst_4 : SubmonoidClass S M
s : S
⊢ IsOrderedMonoid.{u_1} ↥s

Tactic:
Function.Injective.isOrderedMonoid Subtype.val (fun _ _ => rfl) .rfl

Premises used: Iff.rfl, Function.Injective.isOrderedMonoid, Subtype.val, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Submonoid
Goal:
M : Type u_1
S : Type u_2
inst : SetLike S M
inst_1 : CommMonoid M
inst_2 : Preorder M
inst_3 : IsOrderedCancelMonoid M
inst_4 : SubmonoidClass S M
s : S
⊢ IsOrderedCancelMonoid.{u_1} ↥s

Tactic:
Function.Injective.isOrderedCancelMonoid Subtype.val (fun _ _ => rfl) .rfl

Premises used: Iff.rfl, Function.Injective.isOrderedCancelMonoid, Subtype.val, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Submonoid
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
S : Submonoid M
⊢ IsOrderedMonoid.{u_1} ↥S

Tactic:
Function.Injective.isOrderedMonoid Subtype.val (fun _ _ => rfl) .rfl

Premises used: Iff.rfl, Function.Injective.isOrderedMonoid, Subtype.val, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Submonoid
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
S : Submonoid M
⊢ IsOrderedCancelMonoid.{u_1} ↥S

Tactic:
Function.Injective.isOrderedCancelMonoid Subtype.val (fun _ _ => rfl) .rfl

Premises used: Iff.rfl, Function.Injective.isOrderedCancelMonoid, Subtype.val, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Submonoid
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
⊢ Membership.mem (γ := Submonoid M) (oneLE M) a ↔ 1 ≤ a

Tactic:
Iff.rfl

Premises used: Set.Ici, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Order.Monoid.ToMulBot
Goal:
α : Type u
inst : Add α
⊢ Eq.{u + 1} (α := Multiplicative (WithBot α))
    ((toMulBot : (a : WithZero (Multiplicative α)) → Multiplicative (WithBot α)) 0 : Multiplicative (WithBot α))
    ((Multiplicative.ofAdd : (a : WithBot α) → Multiplicative (WithBot α)) ⊥ : Multiplicative (WithBot α))

Tactic:
rfl

Premises used: Multiplicative, rfl
-- Module: Mathlib.Algebra.Order.Monoid.ToMulBot
Goal:
α : Type u
inst : Add α
x : Multiplicative α
⊢ Eq (α := Multiplicative (WithBot α))
    ((toMulBot : (a : WithZero (Multiplicative α)) → Multiplicative (WithBot α)) (↑x : WithZero (Multiplicative α)) :
      Multiplicative (WithBot α))
    ((Multiplicative.ofAdd : (a : WithBot α) → Multiplicative (WithBot α))
        ((↑((Multiplicative.toAdd : (a : Multiplicative α) → α) x) : WithBot α) : WithBot α) :
      Multiplicative (WithBot α))

Tactic:
rfl

Premises used: WithBot.some, Multiplicative, WithZero.coe, rfl
-- Module: Mathlib.Algebra.Order.Monoid.ToMulBot
Goal:
α : Type u
inst : Add α
⊢ Eq.{u + 1} (α := WithZero (Multiplicative α))
    ((MulEquiv.symm toMulBot : (a : Multiplicative (WithBot α)) → WithZero (Multiplicative α))
        ((Multiplicative.ofAdd : (a : WithBot α) → Multiplicative (WithBot α)) ⊥ : Multiplicative (WithBot α)) :
      WithZero (Multiplicative α))
    (0 : WithZero (Multiplicative α))

Tactic:
rfl

Premises used: Multiplicative, rfl
-- Module: Mathlib.Algebra.Order.Monoid.ToMulBot
Goal:
α : Type u
inst : Add α
x : α
⊢ Eq (α := WithZero (Multiplicative α))
    ((MulEquiv.symm toMulBot : (a : Multiplicative (WithBot α)) → WithZero (Multiplicative α))
        ((Multiplicative.ofAdd : (a : WithBot α) → Multiplicative (WithBot α)) (↑x : WithBot α) :
          Multiplicative (WithBot α)) :
      WithZero (Multiplicative α))
    ((↑((Multiplicative.ofAdd : (a : α) → Multiplicative α) x) : WithZero (Multiplicative α)) :
      WithZero (Multiplicative α))

Tactic:
rfl

Premises used: WithBot.some, Multiplicative, WithZero.coe, rfl
-- Module: Mathlib.Algebra.Order.Monoid.ToMulBot
Goal:
α : Type u
inst : Add α
inst_1 : Preorder α
⊢ StrictMono.{u, u} (α := WithZero (Multiplicative α)) (β := Multiplicative (WithBot α))
    (⇑toMulBot : (a : WithZero (Multiplicative α)) → Multiplicative (WithBot α))

Tactic:
fun _ _ => id

Premises used: StrictMono, id, Multiplicative
-- Module: Mathlib.Algebra.Order.Monoid.ToMulBot
Goal:
α : Type u
inst : Add α
inst_1 : Preorder α
a b : WithZero (Multiplicative α)
⊢ LE.le (α := Multiplicative (WithBot α))
      ((toMulBot : (a : WithZero (Multiplicative α)) → Multiplicative (WithBot α)) a : Multiplicative (WithBot α))
      ((toMulBot : (a : WithZero (Multiplicative α)) → Multiplicative (WithBot α)) b : Multiplicative (WithBot α)) ↔
    a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl, Multiplicative
-- Module: Mathlib.Algebra.Order.Monoid.ToMulBot
Goal:
α : Type u
inst : Add α
inst_1 : Preorder α
a b : WithZero (Multiplicative α)
⊢ LT.lt (α := Multiplicative (WithBot α))
      ((toMulBot : (a : WithZero (Multiplicative α)) → Multiplicative (WithBot α)) a : Multiplicative (WithBot α))
      ((toMulBot : (a : WithZero (Multiplicative α)) → Multiplicative (WithBot α)) b : Multiplicative (WithBot α)) ↔
    a < b

Tactic:
Iff.rfl

Premises used: Iff.rfl, Multiplicative
-- Module: Mathlib.Algebra.Order.Monoid.TypeTags
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedAddMonoid α
⊢ IsOrderedMonoid.{u_1} (Multiplicative α)

Tactic:
{ mul_le_mul_left := @IsOrderedAddMonoid.add_le_add_left α _ _ _ }

Premises used: Multiplicative, IsOrderedMonoid._proof_1, IsOrderedMonoid.mk, IsOrderedAddMonoid.add_le_add_left
-- Module: Mathlib.Algebra.Order.Monoid.TypeTags
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
⊢ IsOrderedAddMonoid.{u_1} (Additive α)

Tactic:
{ add_le_add_left := @IsOrderedMonoid.mul_le_mul_left α _ _ _ }

Premises used: IsOrderedMonoid.mul_le_mul_left, Additive, IsOrderedAddMonoid._proof_1, IsOrderedAddMonoid.mk
-- Module: Mathlib.Algebra.Order.Monoid.TypeTags
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedCancelAddMonoid α
⊢ IsOrderedCancelMonoid.{u_1} (Multiplicative α)

Tactic:
{ le_of_mul_le_mul_left := @IsOrderedCancelAddMonoid.le_of_add_le_add_left α _ _ _ }

Premises used: IsOrderedCancelAddMonoid.le_of_add_le_add_left, IsOrderedCancelMonoid._proof_1, Multiplicative, IsOrderedCancelMonoid.mk
-- Module: Mathlib.Algebra.Order.Monoid.TypeTags
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedCancelMonoid α
⊢ IsOrderedCancelAddMonoid.{u_1} (Additive α)

Tactic:
{ le_of_add_le_add_left := @IsOrderedCancelMonoid.le_of_mul_le_mul_left α _ _ _ }

Premises used: Additive, IsOrderedCancelAddMonoid.mk, IsOrderedCancelMonoid.le_of_mul_le_mul_left, IsOrderedCancelAddMonoid._proof_1
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LE α
inst_2 : MulLeftMono α
b c : α
bc : b ≤ c
a : α
⊢ a * b ≤ a * c

Tactic:
CovariantClass.elim _ bc

Premises used: CovariantClass.elim
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LE α
inst_2 : MulLeftReflectLE α
a b c : α
bc : a * b ≤ a * c
⊢ b ≤ c

Tactic:
MulLeftReflectLE.le_of_mul_le_mul_left' bc

Premises used: MulLeftReflectLE.le_of_mul_le_mul_left'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LE α
i : MulRightMono α
b c : α
bc : b ≤ c
a : α
⊢ b * a ≤ c * a

Tactic:
i.elim a bc

Premises used: CovariantClass.elim
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LE α
inst_2 : MulRightReflectLE α
a b c : α
bc : b * a ≤ c * a
⊢ b ≤ c

Tactic:
MulRightReflectLE.le_of_mul_le_mul_right' bc

Premises used: MulRightReflectLE.le_of_mul_le_mul_right'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LE α
inst_2 : MulLeftMono α
inst_3 : MulLeftReflectLE α
a b c : α
⊢ a * b ≤ a * c ↔ b ≤ c

Tactic:
rel_iff_cov' ‹MulLeftMono α›.elim fun _ ↦ MulLeftReflectLE.le_of_mul_le_mul_left'

Premises used: MulLeftReflectLE.le_of_mul_le_mul_left', CovariantClass.elim, rel_iff_cov'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LE α
inst_2 : MulRightMono α
inst_3 : MulRightReflectLE α
a b c : α
⊢ b * a ≤ c * a ↔ b ≤ c

Tactic:
rel_iff_cov' ‹MulRightMono α›.elim fun _ ↦ MulRightReflectLE.le_of_mul_le_mul_right'

Premises used: MulRightReflectLE.le_of_mul_le_mul_right', CovariantClass.elim, rel_iff_cov'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
inst_3 : MulLeftReflectLT α
a b c : α
⊢ a * b < a * c ↔ b < c

Tactic:
rel_iff_cov α α (· * ·) (· < ·) a

Premises used: HMul.hMul, rel_iff_cov, LT.lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LT α
inst_2 : MulRightStrictMono α
inst_3 : MulRightReflectLT α
a b c : α
⊢ b * a < c * a ↔ b < c

Tactic:
rel_iff_cov α α (swap (· * ·)) (· < ·) a

Premises used: HMul.hMul, Function.swap, rel_iff_cov, LT.lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
b c : α
bc : b < c
a : α
⊢ a * b < a * c

Tactic:
CovariantClass.elim _ bc

Premises used: CovariantClass.elim
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LT α
inst_2 : MulLeftReflectLT α
a b c : α
bc : a * b < a * c
⊢ b < c

Tactic:
ContravariantClass.elim _ bc

Premises used: ContravariantClass.elim
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LT α
i : MulRightStrictMono α
b c : α
bc : b < c
a : α
⊢ b * a < c * a

Tactic:
i.elim a bc

Premises used: CovariantClass.elim
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LT α
i : MulRightReflectLT α
a b c : α
bc : b * a < c * a
⊢ b < c

Tactic:
i.elim a bc

Premises used: ContravariantClass.elim
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a : α
⊢ Monotone (β := α) fun (x : α) ↦ a * x

Tactic:
fun _ _ h ↦ mul_le_mul_right h _

Premises used: Monotone, mul_le_mul_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulRightMono α
a : α
⊢ Monotone (β := α) fun (x : α) ↦ x * a

Tactic:
fun _ _ h ↦ mul_le_mul_left h _

Premises used: Monotone, mul_le_mul_left
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
a : α
⊢ StrictMono (β := α) fun (x : α) ↦ a * x

Tactic:
fun _ _ h ↦ mul_lt_mul_right h _

Premises used: StrictMono, mul_lt_mul_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulRightStrictMono α
a : α
⊢ StrictMono (β := α) fun (x : α) ↦ x * a

Tactic:
fun _ _ h ↦ mul_lt_mul_left h _

Premises used: StrictMono, mul_lt_mul_left
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
h₁ : a < b
h₂ : c < d
⊢ a * c < b * d

Tactic:
calc
    a * c < a * d := mul_lt_mul_right h₂ a
    _ < b * d := mul_lt_mul_left h₁ d

Premises used: Trans.trans, mul_lt_mul_right, mul_lt_mul_left
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightMono α
a b c d : α
h₁ : a ≤ b
h₂ : c < d
⊢ a * c < b * d

Tactic:
(mul_le_mul_left h₁ _).trans_lt (mul_lt_mul_right h₂ b)

Premises used: mul_lt_mul_right, mul_le_mul_left, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightStrictMono α
a b c d : α
h₁ : a < b
h₂ : c ≤ d
⊢ a * c < b * d

Tactic:
(mul_le_mul_right h₂ _).trans_lt (mul_lt_mul_left h₁ d)

Premises used: mul_le_mul_right, mul_lt_mul_left, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightMono α
a b c d : α
h₁ : a < b
h₂ : c < d
⊢ a * c < b * d

Tactic:
mul_lt_mul_of_le_of_lt h₁.le h₂

Premises used: LT.lt.le, mul_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightStrictMono α
a b c d : α
h₁ : a < b
h₂ : c < d
⊢ a * c < b * d

Tactic:
mul_lt_mul_of_lt_of_le h₁ h₂.le

Premises used: LT.lt.le, mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b c d : α
h₁ : a ≤ b
h₂ : c ≤ d
grw : b * c ≤ b * d
grw₁ grw₂ : b * d ≤ b * d
⊢ a * c ≤ b * d

Tactic:
grw [h₁, h₂]
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b c d e f : α
h₁ : a ≤ d
h₂ : b ≤ e
h₃ : c ≤ f
⊢ a * b * c ≤ d * e * f

Tactic:
mul_le_mul' (mul_le_mul' h₁ h₂) h₃

Premises used: mul_le_mul'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b c d : α
h : a * b < c
hle : d ≤ b
⊢ a * d < c

Tactic:
(mul_le_mul_right hle a).trans_lt h

Premises used: mul_le_mul_right, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b c d : α
h : a * b ≤ c
hle : d ≤ b
⊢ a * d ≤ c

Tactic:
@act_rel_of_rel_of_act_rel _ _ _ (· ≤ ·) _ _ a _ _ _ hle h

Premises used: act_rel_of_rel_of_act_rel