awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
m : α
n : β
hm : m ≠ 0
hn : n ≠ 0
rw :
  HMul.hMul (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((↑((OrderMonoidHom.inlₗ αˣ βˣ : (a : αˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm)) :
          WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((inr α β : (a : β) → WithZero (Lex (αˣ × βˣ))) n : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) =
    (↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) : WithZero (Lex (αˣ × βˣ)))
rw₁ :
  HMul.hMul (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((↑((OrderMonoidHom.inlₗ αˣ βˣ : (a : αˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm)) :
          WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((↑((OrderMonoidHom.inrₗ αˣ βˣ : (a : βˣ) → Lex (αˣ × βˣ)) (Units.mk0 n hn)) :
          WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) =
    (↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) : WithZero (Lex (αˣ × βˣ)))
rw₂ :
  (↑(HMul.hMul (α := Lex (Prod.{u_1, u_2} αˣ βˣ)) (β := Lex (Prod.{u_1, u_2} αˣ βˣ))
          ((OrderMonoidHom.inlₗ αˣ βˣ : (a : αˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm) : Lex (Prod.{u_1, u_2} αˣ βˣ))
          ((OrderMonoidHom.inrₗ αˣ βˣ : (a : βˣ) → Lex (αˣ × βˣ)) (Units.mk0 n hn) : Lex (Prod.{u_1, u_2} αˣ βˣ))) :
      WithZero (Lex (αˣ × βˣ))) =
    (↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) : WithZero (Lex (αˣ × βˣ)))
rw₃ rw₄ :
  Eq (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
      WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
      WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
⊢ HMul.hMul (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((inl α β : (a : α) → WithZero (Lex (αˣ × βˣ))) m : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((inr α β : (a : β) → WithZero (Lex (αˣ × βˣ))) n : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) =
    (↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) : WithZero (Lex (αˣ × βˣ)))

Tactic:
rw [inl_eq_coe_inlₗ hm, inr_eq_coe_inrₗ hn,
      ← WithZero.coe_mul, OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex]

Premises used: OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex, LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ, LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ, WithZero.coe_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
⊢ StrictMono (α := ValueGroup₀ f) (β := WithZero Bˣ) (⇑(orderMonoidWithZeroHom f) : (a : ValueGroup₀ f) → WithZero Bˣ)

Tactic:
map'_strictMono (Subtype.strictMono_coe _)

Premises used: WithZero.map'_strictMono, Set.Mem, setOf, Subtype.strictMono_coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
x y : ValueGroup₀ f
hxy : x < y
⊢ LT.lt (α := WithZero Bˣ) ((orderMonoidWithZeroHom f : (a : ValueGroup₀ f) → WithZero Bˣ) x : WithZero Bˣ)
    ((orderMonoidWithZeroHom f : (a : ValueGroup₀ f) → WithZero Bˣ) y : WithZero Bˣ)

Tactic:
rw [← monoidWithZeroHom_strictMono.lt_iff_lt] at hxy

Premises used: StrictMono.lt_iff_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
x y : ValueGroup₀ f
hxy :
  LT.lt (α := WithZero Bˣ) ((orderMonoidWithZeroHom f : (a : ValueGroup₀ f) → WithZero Bˣ) x : WithZero Bˣ)
    ((orderMonoidWithZeroHom f : (a : ValueGroup₀ f) → WithZero Bˣ) y : WithZero Bˣ)
⊢ LT.lt (α := B) ((embedding : (a : ValueGroup₀ f) → B) x : B) ((embedding : (a : ValueGroup₀ f) → B) y : B)

Tactic:
simpa using (OrderEmbedding.lt_iff_lt (OrderIso.withZeroUnits.toOrderEmbedding)).mpr hxy

Premises used: Iff.mpr, OrderIso.toOrderEmbedding, OrderIso.withZeroUnits, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
⊢ IsOrderedMonoid.{u_2} (ValueGroup₀ f)

Tactic:
Function.Injective.isOrderedMonoid embedding (map_mul _) embedding_strictMono.le_iff_le

Premises used: map_mul, MonoidWithZeroHom.ValueGroup₀.embedding, Function.Injective.isOrderedMonoid, StrictMono.le_iff_le, DFunLike.coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a : ValueGroup₀ f
ha : 0 < a
b c : ValueGroup₀ f
hbc : b < c
simp :
  ∀ (ha : LT.lt (α := B) ((embedding : (a : ValueGroup₀ f) → B) 0 : B) ((embedding : (a : ValueGroup₀ f) → B) a : B))
    (hbc : LT.lt (α := B) ((embedding : (a : ValueGroup₀ f) → B) b : B) ((embedding : (a : ValueGroup₀ f) → B) c : B)),
    HMul.hMul (α := B) (β := B) ((embedding : (a : ValueGroup₀ f) → B) a : B)
        ((embedding : (a : ValueGroup₀ f) → B) b : B) <
      HMul.hMul (α := B) (β := B) ((embedding : (a : ValueGroup₀ f) → B) a : B)
        ((embedding : (a : ValueGroup₀ f) → B) c : B)
⊢ a * b < a * c

Tactic:
simp only [← (embedding_strictMono (f := f)).lt_iff_lt, map_mul] at *

Premises used: StrictMono.lt_iff_lt, map_mul, MonoidWithZeroHom.ValueGroup₀.embedding_strictMono
-- Module: Mathlib.Algebra.Order.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a b c : ValueGroup₀ f
ha : LT.lt (α := B) ((embedding : (a : ValueGroup₀ f) → B) 0 : B) ((embedding : (a : ValueGroup₀ f) → B) a : B)
hbc : LT.lt (α := B) ((embedding : (a : ValueGroup₀ f) → B) b : B) ((embedding : (a : ValueGroup₀ f) → B) c : B)
⊢ HMul.hMul (α := B) (β := B) ((embedding : (a : ValueGroup₀ f) → B) a : B)
      ((embedding : (a : ValueGroup₀ f) → B) b : B) <
    HMul.hMul (α := B) (β := B) ((embedding : (a : ValueGroup₀ f) → B) a : B)
      ((embedding : (a : ValueGroup₀ f) → B) c : B)

Tactic:
(mul_lt_mul_iff_of_pos_left ha).mpr hbc

Premises used: Iff.mpr, mul_lt_mul_iff_of_pos_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a b c : ValueGroup₀ f
ha : LT.lt (α := B) ((embedding : (a : ValueGroup₀ f) → B) 0 : B) ((embedding : (a : ValueGroup₀ f) → B) a : B)
hbc : LT.lt (α := B) ((embedding : (a : ValueGroup₀ f) → B) b : B) ((embedding : (a : ValueGroup₀ f) → B) c : B)
⊢ HMul.hMul (α := B) (β := B) ((embedding : (a : ValueGroup₀ f) → B) a : B)
      ((embedding : (a : ValueGroup₀ f) → B) b : B) <
    HMul.hMul (α := B) (β := B) ((embedding : (a : ValueGroup₀ f) → B) a : B)
      ((embedding : (a : ValueGroup₀ f) → B) c : B)

Tactic:
exact (mul_lt_mul_iff_of_pos_left ha).mpr hbc

Premises used: Iff.mpr, mul_lt_mul_iff_of_pos_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
x : ValueGroup₀ f
⊢ 0 ≤ x

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a : (ValueGroup₀ f)ˣ
rw :
  ((embedding : (a : ValueGroup₀ f) → B)
      (((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) 0) :
    B)
| (0 : B)

Tactic:
rw [← map_zero f, ← ValueGroup₀.embedding_restrict₀ (0 : A)]

Premises used: map_zero, MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a : (ValueGroup₀ f)ˣ
conv_lhs :
  LT.lt (α := B)
    ((embedding : (a : ValueGroup₀ f) → B)
        (((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) 0) :
      B)
    ((embedding : (a : ValueGroup₀ f) → B) (↑a : ValueGroup₀ f) : B)
⊢ LT.lt (α := B) (0 : B) ((embedding : (a : ValueGroup₀ f) → B) (↑a : ValueGroup₀ f) : B)

Tactic:
conv_lhs => rw [← map_zero f, ← ValueGroup₀.embedding_restrict₀ (0 : A)]

Premises used: map_zero, MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a : (ValueGroup₀ f)ˣ
rw : ((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) 0 < (↑a : ValueGroup₀ f)
⊢ LT.lt (α := B)
    ((embedding : (a : ValueGroup₀ f) → B)
        (((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) 0) :
      B)
    ((embedding : (a : ValueGroup₀ f) → B) (↑a : ValueGroup₀ f) : B)

Tactic:
rw [embedding_strictMono.lt_iff_lt]

Premises used: StrictMono.lt_iff_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a : (ValueGroup₀ f)ˣ
⊢ ((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) 0 < (↑a : ValueGroup₀ f)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Range
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a : (ValueGroup₀ f)ˣ
⊢ Ne (α := B) ((embedding : (a : ValueGroup₀ f) → B) (↑a : ValueGroup₀ f) : B) (0 : B)

Tactic:
(embedding_unit_pos a).ne.symm

Premises used: MonoidWithZeroHom.ValueGroup₀.embedding_unit_pos, Ne.symm, LT.lt.ne
-- Module: Mathlib.Algebra.Order.GroupWithZero.Submonoid
Goal:
α : Type u_1
inst : MulZeroOneClass α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
a : α
⊢ Membership.mem (γ := Submonoid α) (pos α) a ↔ 0 < a

Tactic:
Iff.rfl

Premises used: Set.Ioi, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Order.GroupWithZero.Synonym
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
h : NoZeroDivisors α
⊢ NoZeroDivisors.{u_1} (Lex α)

Tactic:
h

Premises used: Lex
-- Module: Mathlib.Algebra.Order.GroupWithZero.Synonym
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
h : IsLeftCancelMulZero α
⊢ IsLeftCancelMulZero.{u_1} (Lex α)

Tactic:
h

Premises used: Lex
-- Module: Mathlib.Algebra.Order.GroupWithZero.Synonym
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
h : IsRightCancelMulZero α
⊢ IsRightCancelMulZero.{u_1} (Lex α)

Tactic:
h

Premises used: Lex
-- Module: Mathlib.Algebra.Order.GroupWithZero.Synonym
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
h : IsCancelMulZero α
⊢ IsCancelMulZero.{u_1} (Lex α)

Tactic:
h

Premises used: Lex
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : Preorder α
inst_2 : PosMulStrictMono α
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b

Tactic:
simpa only [mul_zero] using mul_lt_mul_of_pos_left hb ha

Premises used: mul_lt_mul_of_pos_left, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : Preorder α
inst_2 : PosMulStrictMono α
ha : 0 < a
hb : b < 0
⊢ a * b < 0

Tactic:
simpa only [mul_zero] using mul_lt_mul_of_pos_left hb ha

Premises used: mul_lt_mul_of_pos_left, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : Preorder α
inst_2 : PosMulStrictMono α
inst_3 : PosMulReflectLT α
h : 0 < a
⊢ 0 < a * b ↔ 0 < b

Tactic:
simpa using mul_lt_mul_iff_right₀ (b := 0) h

Premises used: mul_lt_mul_iff_right₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : Preorder α
inst_2 : MulPosStrictMono α
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b

Tactic:
simpa only [zero_mul] using mul_lt_mul_of_pos_right ha hb

Premises used: MulZeroClass.zero_mul, mul_lt_mul_of_pos_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : Preorder α
inst_2 : MulPosStrictMono α
ha : a < 0
hb : 0 < b
⊢ a * b < 0

Tactic:
simpa only [zero_mul] using mul_lt_mul_of_pos_right ha hb

Premises used: MulZeroClass.zero_mul, mul_lt_mul_of_pos_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : Preorder α
inst_2 : MulPosStrictMono α
inst_3 : MulPosReflectLT α
h : 0 < b
⊢ 0 < a * b ↔ 0 < a

Tactic:
simpa using mul_lt_mul_iff_left₀ (b := 0) h

Premises used: mul_lt_mul_iff_left₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : Preorder α
inst_2 : PosMulMono α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b

Tactic:
simpa only [mul_zero] using mul_le_mul_of_nonneg_left hb ha

Premises used: MulZeroClass.mul_zero, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : Preorder α
inst_2 : PosMulMono α
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b ≤ 0

Tactic:
simpa only [mul_zero] using mul_le_mul_of_nonneg_left hb ha

Premises used: MulZeroClass.mul_zero, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : Preorder α
inst_2 : MulPosMono α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b

Tactic:
simpa only [zero_mul] using mul_le_mul_of_nonneg_right ha hb

Premises used: MulZeroClass.zero_mul, mul_le_mul_of_nonneg_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : Preorder α
inst_2 : MulPosMono α
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b ≤ 0

Tactic:
simpa only [zero_mul] using mul_le_mul_of_nonneg_right ha hb

Premises used: MulZeroClass.zero_mul, mul_le_mul_of_nonneg_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : Preorder α
inst_2 : PosMulReflectLT α
h : 0 < a * b
ha : 0 ≤ a
⊢ 0 < b

Tactic:
lt_of_mul_lt_mul_left ((mul_zero a).symm ▸ h : a * 0 < a * b) ha

Premises used: lt_of_mul_lt_mul_left, Eq.rec, MulZeroClass.mul_zero, Eq.symm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : Preorder α
inst_2 : MulPosReflectLT α
h : 0 < a * b
hb : 0 ≤ b
⊢ 0 < a

Tactic:
lt_of_mul_lt_mul_right ((zero_mul b).symm ▸ h : 0 * b < a * b) hb

Premises used: MulZeroClass.zero_mul, Eq.rec, lt_of_mul_lt_mul_right, Eq.symm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : Preorder α
inst_2 : PosMulReflectLT α
inst_3 : MulPosReflectLT α
hab : 0 < a * b
⊢ 0 < a ↔ 0 < b

Tactic:
⟨pos_of_mul_pos_right hab ∘ le_of_lt, pos_of_mul_pos_left hab ∘ le_of_lt⟩

Premises used: pos_of_mul_pos_left, le_of_lt, Function.comp, Iff.intro, pos_of_mul_pos_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : Preorder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosMono α
h₁ : a < b
h₂ : c < d
a0 : 0 ≤ a
c0 : 0 ≤ c
⊢ a * c < b * d

Tactic:
mul_lt_mul_of_le_of_lt_of_nonneg_of_pos h₁.le h₂ c0 (a0.trans_lt h₁)

Premises used: mul_lt_mul_of_le_of_lt_of_nonneg_of_pos, LT.lt.le, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : Preorder α
inst_2 : PosMulMono α
inst_3 : MulPosStrictMono α
h₁ : a < b
h₂ : c < d
a0 : 0 ≤ a
c0 : 0 ≤ c
⊢ a * c < b * d

Tactic:
mul_lt_mul_of_lt_of_le_of_nonneg_of_pos h₁ h₂.le a0 (c0.trans_lt h₂)

Premises used: LT.lt.le, mul_lt_mul_of_lt_of_le_of_nonneg_of_pos, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : Preorder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
ha : 0 ≤ a
hab : a ≤ b
⊢ a * a ≤ b * b

Tactic:
mul_le_mul hab hab ha <| ha.trans hab

Premises used: mul_le_mul, LE.le.trans
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h : CovariantClass α>0 α (fun (x : α>0) (y : α) ↦ (↑x : α) * y) fun (x1 x2 : α) ↦ x1 ≤ x2
a : α
ha : 0 ≤ a
b c : α
hbc : b ≤ c
inl : ∀ (ha : 0 = a), a * b ≤ a * c
inr : ∀ (ha : 0 < a), a * b ≤ a * c
⊢ a * b ≤ a * c

Tactic:
obtain ha | ha := ha.eq_or_lt

Premises used: LE.le.eq_or_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h : CovariantClass α>0 α (fun (x : α>0) (y : α) ↦ (↑x : α) * y) fun (x1 x2 : α) ↦ x1 ≤ x2
a : α
ha_1 : 0 ≤ a
b c : α
hbc : b ≤ c
ha : 0 = a
⊢ a * b ≤ a * c

Tactic:
simp [← ha]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h : CovariantClass α>0 α (fun (x : α>0) (y : α) ↦ (↑x : α) * y) fun (x1 x2 : α) ↦ x1 ≤ x2
a : α
ha_1 : 0 ≤ a
b c : α
hbc : b ≤ c
ha : 0 < a
⊢ a * b ≤ a * c

Tactic:
@CovariantClass.elim α>0 α (fun x y => x * y) (· ≤ ·) _ ⟨_, ha⟩ _ _ hbc

Premises used: CovariantClass.elim, Subtype.mk
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h : CovariantClass α>0 α (fun (x : α>0) (y : α) ↦ (↑x : α) * y) fun (x1 x2 : α) ↦ x1 ≤ x2
a : α
ha_1 : 0 ≤ a
b c : α
hbc : b ≤ c
ha : 0 < a
⊢ a * b ≤ a * c

Tactic:
exact @CovariantClass.elim α>0 α (fun x y => x * y) (· ≤ ·) _ ⟨_, ha⟩ _ _ hbc
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h : CovariantClass α>0 α (fun (x : α>0) (y : α) ↦ y * (↑x : α)) fun (x1 x2 : α) ↦ x1 ≤ x2
a : α
ha : 0 ≤ a
b c : α
hbc : b ≤ c
inl : ∀ (ha : 0 = a), b * a ≤ c * a
inr : ∀ (ha : 0 < a), b * a ≤ c * a
⊢ b * a ≤ c * a

Tactic:
obtain ha | ha := ha.eq_or_lt

Premises used: LE.le.eq_or_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h : CovariantClass α>0 α (fun (x : α>0) (y : α) ↦ y * (↑x : α)) fun (x1 x2 : α) ↦ x1 ≤ x2
a : α
ha_1 : 0 ≤ a
b c : α
hbc : b ≤ c
ha : 0 = a
⊢ b * a ≤ c * a

Tactic:
simp [← ha]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h : CovariantClass α>0 α (fun (x : α>0) (y : α) ↦ y * (↑x : α)) fun (x1 x2 : α) ↦ x1 ≤ x2
a : α
ha_1 : 0 ≤ a
b c : α
hbc : b ≤ c
ha : 0 < a
⊢ b * a ≤ c * a

Tactic:
@CovariantClass.elim α>0 α (fun x y => y * x) (· ≤ ·) _ ⟨_, ha⟩ _ _ hbc

Premises used: CovariantClass.elim, Subtype.mk
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h : CovariantClass α>0 α (fun (x : α>0) (y : α) ↦ y * (↑x : α)) fun (x1 x2 : α) ↦ x1 ≤ x2
a : α
ha_1 : 0 ≤ a
b c : α
hbc : b ≤ c
ha : 0 < a
⊢ b * a ≤ c * a

Tactic:
exact @CovariantClass.elim α>0 α (fun x y => y * x) (· ≤ ·) _ ⟨_, ha⟩ _ _ hbc
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h_1 : ContravariantClass α>0 α (fun (x : α>0) (y : α) ↦ (↑x : α) * y) fun (x1 x2 : α) ↦ x1 < x2
a : { x : α // 0 ≤ x }
b c : α
h :
  (fun (x1 x2 : α) ↦ x1 < x2) ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ (↑x : α) * y) a b)
    ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ (↑x : α) * y) a c)
inl : ∀ (ha : 0 = (↑a : α)), b < c
inr : ∀ (ha : 0 < (↑a : α)), b < c
⊢ b < c

Tactic:
obtain ha | ha := a.prop.eq_or_lt

Premises used: LE.le.eq_or_lt, Subtype.prop
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h_1 : ContravariantClass α>0 α (fun (x : α>0) (y : α) ↦ (↑x : α) * y) fun (x1 x2 : α) ↦ x1 < x2
a : { x : α // 0 ≤ x }
b c : α
h :
  (fun (x1 x2 : α) ↦ x1 < x2) ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ (↑x : α) * y) a b)
    ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ (↑x : α) * y) a c)
ha : 0 = (↑a : α)
⊢ b < c

Tactic:
simp [← ha] at h
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h_1 : ContravariantClass α>0 α (fun (x : α>0) (y : α) ↦ (↑x : α) * y) fun (x1 x2 : α) ↦ x1 < x2
a : { x : α // 0 ≤ x }
b c : α
h :
  (fun (x1 x2 : α) ↦ x1 < x2) ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ (↑x : α) * y) a b)
    ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ (↑x : α) * y) a c)
ha : 0 < (↑a : α)
⊢ b < c

Tactic:
@ContravariantClass.elim α>0 α (fun x y => x * y) (· < ·) _ ⟨_, ha⟩ _ _ h

Premises used: Subtype.mk, ContravariantClass.elim
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h_1 : ContravariantClass α>0 α (fun (x : α>0) (y : α) ↦ (↑x : α) * y) fun (x1 x2 : α) ↦ x1 < x2
a : { x : α // 0 ≤ x }
b c : α
h :
  (fun (x1 x2 : α) ↦ x1 < x2) ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ (↑x : α) * y) a b)
    ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ (↑x : α) * y) a c)
ha : 0 < (↑a : α)
⊢ b < c

Tactic:
exact @ContravariantClass.elim α>0 α (fun x y => x * y) (· < ·) _ ⟨_, ha⟩ _ _ h
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h_1 : ContravariantClass α>0 α (fun (x : α>0) (y : α) ↦ y * (↑x : α)) fun (x1 x2 : α) ↦ x1 < x2
a : { x : α // 0 ≤ x }
b c : α
h :
  (fun (x1 x2 : α) ↦ x1 < x2) ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ y * (↑x : α)) a b)
    ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ y * (↑x : α)) a c)
inl : ∀ (ha : 0 = (↑a : α)), b < c
inr : ∀ (ha : 0 < (↑a : α)), b < c
⊢ b < c

Tactic:
obtain ha | ha := a.prop.eq_or_lt

Premises used: LE.le.eq_or_lt, Subtype.prop
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h_1 : ContravariantClass α>0 α (fun (x : α>0) (y : α) ↦ y * (↑x : α)) fun (x1 x2 : α) ↦ x1 < x2
a : { x : α // 0 ≤ x }
b c : α
h :
  (fun (x1 x2 : α) ↦ x1 < x2) ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ y * (↑x : α)) a b)
    ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ y * (↑x : α)) a c)
ha : 0 = (↑a : α)
⊢ b < c

Tactic:
simp [← ha] at h
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h_1 : ContravariantClass α>0 α (fun (x : α>0) (y : α) ↦ y * (↑x : α)) fun (x1 x2 : α) ↦ x1 < x2
a : { x : α // 0 ≤ x }
b c : α
h :
  (fun (x1 x2 : α) ↦ x1 < x2) ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ y * (↑x : α)) a b)
    ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ y * (↑x : α)) a c)
ha : 0 < (↑a : α)
⊢ b < c

Tactic:
@ContravariantClass.elim α>0 α (fun x y => y * x) (· < ·) _ ⟨_, ha⟩ _ _ h

Premises used: Subtype.mk, ContravariantClass.elim
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h_1 : ContravariantClass α>0 α (fun (x : α>0) (y : α) ↦ y * (↑x : α)) fun (x1 x2 : α) ↦ x1 < x2
a : { x : α // 0 ≤ x }
b c : α
h :
  (fun (x1 x2 : α) ↦ x1 < x2) ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ y * (↑x : α)) a b)
    ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ y * (↑x : α)) a c)
ha : 0 < (↑a : α)
⊢ b < c

Tactic:
exact @ContravariantClass.elim α>0 α (fun x y => y * x) (· < ·) _ ⟨_, ha⟩ _ _ h
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
⊢ PosMulMono α

Tactic:
posMulMono_iff_covariant_pos.2 (covariantClass_le_of_lt _ _ _)

Premises used: Iff.mpr, posMulMono_iff_covariant_pos, covariantClass_le_of_lt