awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : 0 ≤ a / b
inl : 0 * a / (0 * b) ≤ a / b
inr : ∀ (hc : c ≠ 0), c * a / (c * b) ≤ a / b
⊢ c * a / (c * b) ≤ a / b

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
h : 0 ≤ a / b
⊢ 0 * a / (0 * b) ≤ a / b

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : 0 ≤ a / b
hc : c ≠ 0
inr inr₁ : a / b ≤ a / b
⊢ c * a / (c * b) ≤ a / b

Tactic:
rw [mul_div_mul_left _ _ hc]

Premises used: mul_div_mul_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : a / b ≤ 0
inl : a / b ≤ 0 * a / (0 * b)
inr : ∀ (hc : c ≠ 0), a / b ≤ c * a / (c * b)
⊢ a / b ≤ c * a / (c * b)

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
h : a / b ≤ 0
⊢ a / b ≤ 0 * a / (0 * b)

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : a / b ≤ 0
hc : c ≠ 0
inr inr₁ : a / b ≤ a / b
⊢ a / b ≤ c * a / (c * b)

Tactic:
rw [mul_div_mul_left _ _ hc]

Premises used: mul_div_mul_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : c * a ≤ b ↔ a * c ≤ b
rw₁ rw₂ : a * c ≤ b ↔ a * c ≤ b
⊢ a ≤ c⁻¹ * b ↔ a * c ≤ b

Tactic:
rw [le_inv_mul_iff₀ hc, mul_comm]

Premises used: le_inv_mul_iff₀, mul_comm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : b ≤ c * a ↔ b ≤ a * c
rw₁ rw₂ : b ≤ a * c ↔ b ≤ a * c
⊢ c⁻¹ * b ≤ a ↔ b ≤ a * c

Tactic:
rw [inv_mul_le_iff₀ hc, mul_comm]

Premises used: inv_mul_le_iff₀, mul_comm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : a * c ≤ b ↔ c * a ≤ b
rw₁ rw₂ : c * a ≤ b ↔ c * a ≤ b
⊢ a ≤ b * c⁻¹ ↔ c * a ≤ b

Tactic:
rw [le_mul_inv_iff₀ hc, mul_comm]

Premises used: le_mul_inv_iff₀, mul_comm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : b ≤ a * c ↔ b ≤ c * a
rw₁ rw₂ : b ≤ c * a ↔ b ≤ c * a
⊢ b * c⁻¹ ≤ a ↔ b ≤ c * a

Tactic:
rw [mul_inv_le_iff₀ hc, mul_comm]

Premises used: mul_inv_le_iff₀, mul_comm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
rw : a ≤ c / d * b ↔ a * d ≤ c * b
rw₁ : a ≤ c * b / d ↔ a * d ≤ c * b
rw₂ rw₃ : a * d ≤ c * b ↔ a * d ≤ c * b
⊢ a / b ≤ c / d ↔ a * d ≤ c * b

Tactic:
rw [div_le_iff₀ hb, ← mul_div_right_comm, le_div_iff₀ hd]

Premises used: div_le_iff₀, mul_div_right_comm, le_div_iff₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : a * c ≤ b ↔ c * a ≤ b
rw₁ rw₂ : c * a ≤ b ↔ c * a ≤ b
⊢ a ≤ b / c ↔ c * a ≤ b

Tactic:
rw [le_div_iff₀ hc, mul_comm]

Premises used: mul_comm, le_div_iff₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : b ≤ a * c ↔ b ≤ c * a
rw₁ rw₂ : b ≤ c * a ↔ b ≤ c * a
⊢ b / c ≤ a ↔ b ≤ c * a

Tactic:
rw [div_le_iff₀ hc, mul_comm]

Premises used: div_le_iff₀, mul_comm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
ha : 0 < a
hc : 0 < c
rw : a ≤ b / c ↔ c * a ≤ b
rw₁ rw₂ : c * a ≤ b ↔ c * a ≤ b
⊢ a ≤ b / c ↔ c ≤ b / a

Tactic:
rw [le_div_iff₀ ha, le_div_iff₀' hc]

Premises used: le_div_iff₀', le_div_iff₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
rw : a ≤ c * b ↔ a / c ≤ b
rw₁ rw₂ : a ≤ c * b ↔ a ≤ c * b
⊢ a / b ≤ c ↔ a / c ≤ b

Tactic:
rw [div_le_iff₀ hb, div_le_iff₀' hc]

Premises used: div_le_iff₀, div_le_iff₀'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : c * a < b ↔ a * c < b
rw₁ rw₂ : a * c < b ↔ a * c < b
⊢ a < c⁻¹ * b ↔ a * c < b

Tactic:
rw [lt_inv_mul_iff₀ hc, mul_comm]

Premises used: lt_inv_mul_iff₀, mul_comm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : b < c * a ↔ b < a * c
rw₁ rw₂ : b < a * c ↔ b < a * c
⊢ c⁻¹ * b < a ↔ b < a * c

Tactic:
rw [inv_mul_lt_iff₀ hc, mul_comm]

Premises used: inv_mul_lt_iff₀, mul_comm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : a * c < b ↔ c * a < b
rw₁ rw₂ : c * a < b ↔ c * a < b
⊢ a < b * c⁻¹ ↔ c * a < b

Tactic:
rw [lt_mul_inv_iff₀ hc, mul_comm]

Premises used: lt_mul_inv_iff₀, mul_comm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : b < a * c ↔ b < c * a
rw₁ rw₂ : b < c * a ↔ b < c * a
⊢ b * c⁻¹ < a ↔ b < c * a

Tactic:
rw [mul_inv_lt_iff₀ hc, mul_comm]

Premises used: mul_inv_lt_iff₀, mul_comm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
rw : a < c / d * b ↔ a * d < c * b
rw₁ : a < c * b / d ↔ a * d < c * b
rw₂ rw₃ : a * d < c * b ↔ a * d < c * b
⊢ a / b < c / d ↔ a * d < c * b

Tactic:
rw [div_lt_iff₀ hb, ← mul_div_right_comm, lt_div_iff₀ hd]

Premises used: lt_div_iff₀, div_lt_iff₀, mul_div_right_comm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : a * c < b ↔ c * a < b
rw₁ rw₂ : c * a < b ↔ c * a < b
⊢ a < b / c ↔ c * a < b

Tactic:
rw [lt_div_iff₀ hc, mul_comm]

Premises used: lt_div_iff₀, mul_comm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : b < a * c ↔ b < c * a
rw₁ rw₂ : b < c * a ↔ b < c * a
⊢ b / c < a ↔ b < c * a

Tactic:
rw [div_lt_iff₀ hc, mul_comm]

Premises used: div_lt_iff₀, mul_comm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
ha : 0 < a
hc : 0 < c
rw : a < b / c ↔ c * a < b
rw₁ rw₂ : c * a < b ↔ c * a < b
⊢ a < b / c ↔ c < b / a

Tactic:
rw [lt_div_iff₀ ha, lt_div_iff₀' hc]

Premises used: lt_div_iff₀', lt_div_iff₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
rw : a < c * b ↔ a / c < b
rw₁ rw₂ : a < c * b ↔ a < c * b
⊢ a / b < c ↔ a / c < b

Tactic:
rw [div_lt_iff₀ hb, div_lt_iff₀' hc]

Premises used: div_lt_iff₀, div_lt_iff₀'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : PosMulReflectLT α
⊢ ContravariantClass α>0 α (fun (x : α>0) (y : α) ↦ (↑x : α) * y) fun (x1 x2 : α) ↦ x1 < x2

Tactic:
⟨fun a _ _ bc => @ContravariantClass.elim α≥0 α (fun x y => x * y) (· < ·) _ ⟨_, a.2.le⟩ _ _ bc⟩

Premises used: LT.lt.le, Subtype.mk, ContravariantClass.mk, ContravariantClass.elim, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : MulPosReflectLT α
⊢ ContravariantClass α>0 α (fun (x : α>0) (y : α) ↦ y * (↑x : α)) fun (x1 x2 : α) ↦ x1 < x2

Tactic:
⟨fun a _ _ bc => @ContravariantClass.elim α≥0 α (fun x y => y * x) (· < ·) _ ⟨_, a.2.le⟩ _ _ bc⟩

Premises used: LT.lt.le, Subtype.mk, ContravariantClass.mk, ContravariantClass.elim, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c : α
inst_3 : PosMulMono α
hbc : b ≤ c
ha : 0 ≤ a
⊢ a * b ≤ a * c

Tactic:
PosMulMono.mul_le_mul_of_nonneg_left ha hbc

Premises used: PosMulMono.mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c : α
inst_3 : MulPosMono α
hbc : b ≤ c
ha : 0 ≤ a
⊢ b * a ≤ c * a

Tactic:
MulPosMono.mul_le_mul_of_nonneg_right ha hbc

Premises used: MulPosMono.mul_le_mul_of_nonneg_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c : α
inst_3 : PosMulStrictMono α
hbc : b < c
ha : 0 < a
⊢ a * b < a * c

Tactic:
PosMulStrictMono.mul_lt_mul_of_pos_left ha hbc

Premises used: PosMulStrictMono.mul_lt_mul_of_pos_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c : α
inst_3 : MulPosStrictMono α
hbc : b < c
ha : 0 < a
⊢ b * a < c * a

Tactic:
MulPosStrictMono.mul_lt_mul_of_pos_right ha hbc

Premises used: MulPosStrictMono.mul_lt_mul_of_pos_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c : α
inst_3 : PosMulReflectLT α
h : a * b < a * c
a0 : 0 ≤ a
⊢ b < c

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

Premises used: Subtype.mk, ContravariantClass.elim
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c : α
inst_3 : MulPosReflectLT α
h : b * a < c * a
a0 : 0 ≤ a
⊢ b < c

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

Premises used: Subtype.mk, ContravariantClass.elim
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c : α
inst_3 : PosMulReflectLE α
bc : a * b ≤ a * c
a0 : 0 < a
⊢ b ≤ c

Tactic:
@ContravariantClass.elim α>0 α (fun x y => x * y) (· ≤ ·) _ ⟨a, a0⟩ _ _ bc

Premises used: Subtype.mk, ContravariantClass.elim
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c : α
inst_3 : MulPosReflectLE α
bc : b * a ≤ c * a
a0 : 0 < a
⊢ b ≤ c

Tactic:
@ContravariantClass.elim α>0 α (fun x y => y * x) (· ≤ ·) _ ⟨a, a0⟩ _ _ bc

Premises used: Subtype.mk, ContravariantClass.elim
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : PosMulMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
rw : f a * f b ≤ f a * f c
⊢ a * b ≤ a * c

Tactic:
rw [← le, mul, mul]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : PosMulMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
rwa : f 0 ≤ f a
rwa₁ rwa₂ rwa₃ rwa₄ : 0 ≤ a
⊢ 0 ≤ f a

Tactic:
rwa [← zero, le]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : PosMulMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ f a * f b ≤ f a * f c

Tactic:
exact mul_le_mul_of_nonneg_left (le.2 hbc) (by rwa [← zero, le])

Premises used: Iff.mpr, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : MulPosMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
rw : f b * f a ≤ f c * f a
⊢ b * a ≤ c * a

Tactic:
rw [← le, mul, mul]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : MulPosMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
rwa : f 0 ≤ f a
rwa₁ rwa₂ rwa₃ rwa₄ : 0 ≤ a
⊢ 0 ≤ f a

Tactic:
rwa [← zero, le]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : MulPosMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ f b * f a ≤ f c * f a

Tactic:
exact mul_le_mul_of_nonneg_right (le.2 hbc) (by rwa [← zero, le])

Premises used: Iff.mpr, mul_le_mul_of_nonneg_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
rw : f a * f b < f a * f c
⊢ a * b < a * c

Tactic:
rw [← lt, mul, mul]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
rwa : f 0 < f a
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < a
⊢ 0 < f a

Tactic:
rwa [← zero, lt]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ f a * f b < f a * f c

Tactic:
exact mul_lt_mul_of_pos_left (lt.2 hbc) (by rwa [← zero, lt])

Premises used: Iff.mpr, mul_lt_mul_of_pos_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
rw : f b * f a < f c * f a
⊢ b * a < c * a

Tactic:
rw [← lt, mul, mul]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
rwa : f 0 < f a
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < a
⊢ 0 < f a

Tactic:
rwa [← zero, lt]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ f b * f a < f c * f a

Tactic:
exact mul_lt_mul_of_pos_right (lt.2 hbc) (by rwa [← zero, lt])

Premises used: Iff.mpr, mul_lt_mul_of_pos_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c : α
inst_3 : PosMulMono α
inst_4 : PosMulReflectLE α
a0 : 0 < a
⊢ a * b ≤ a * c ↔ b ≤ c

Tactic:
@rel_iff_cov α>0 α (fun x y => x * y) (· ≤ ·) _ _ ⟨a, a0⟩ _ _

Premises used: HMul.hMul, Subtype, rel_iff_cov, LE.le, Subtype.mk, LT.lt, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c : α
inst_3 : MulPosMono α
inst_4 : MulPosReflectLE α
a0 : 0 < a
⊢ b * a ≤ c * a ↔ b ≤ c

Tactic:
@rel_iff_cov α>0 α (fun x y => y * x) (· ≤ ·) _ _ ⟨a, a0⟩ _ _

Premises used: HMul.hMul, Subtype, rel_iff_cov, LE.le, Subtype.mk, LT.lt, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
h₁ : a ≤ b
h₂ : c ≤ d
a0 : 0 ≤ a
d0 : 0 ≤ d
⊢ a * c ≤ b * d

Tactic:
(mul_le_mul_of_nonneg_left h₂ a0).trans (mul_le_mul_of_nonneg_right h₁ d0)

Premises used: mul_le_mul_of_nonneg_right, LE.le.trans, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
h₁ : a ≤ b
h₂ : c ≤ d
c0 : 0 ≤ c
b0 : 0 ≤ b
⊢ a * c ≤ b * d

Tactic:
(mul_le_mul_of_nonneg_right h₁ c0).trans (mul_le_mul_of_nonneg_left h₂ b0)

Premises used: mul_le_mul_of_nonneg_right, LE.le.trans, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : PosMulStrictMono α
inst_4 : MulPosMono α
h₁ : a ≤ b
h₂ : c < d
a0 : 0 < a
d0 : 0 ≤ d
⊢ a * c < b * d

Tactic:
(mul_lt_mul_of_pos_left h₂ a0).trans_le (mul_le_mul_of_nonneg_right h₁ d0)

Premises used: mul_lt_mul_of_pos_left, mul_le_mul_of_nonneg_right, LT.lt.trans_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : PosMulStrictMono α
inst_4 : MulPosMono α
h₁ : a ≤ b
h₂ : c < d
c0 : 0 ≤ c
b0 : 0 < b
⊢ a * c < b * d

Tactic:
(mul_le_mul_of_nonneg_right h₁ c0).trans_lt (mul_lt_mul_of_pos_left h₂ b0)

Premises used: mul_lt_mul_of_pos_left, mul_le_mul_of_nonneg_right, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : PosMulMono α
inst_4 : MulPosStrictMono α
h₁ : a < b
h₂ : c ≤ d
a0 : 0 ≤ a
d0 : 0 < d
⊢ a * c < b * d

Tactic:
(mul_le_mul_of_nonneg_left h₂ a0).trans_lt (mul_lt_mul_of_pos_right h₁ d0)

Premises used: mul_lt_mul_of_pos_right, LE.le.trans_lt, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : PosMulMono α
inst_4 : MulPosStrictMono α
h₁ : a < b
h₂ : c ≤ d
c0 : 0 < c
b0 : 0 ≤ b
⊢ a * c < b * d

Tactic:
(mul_lt_mul_of_pos_right h₁ c0).trans_le (mul_le_mul_of_nonneg_left h₂ b0)

Premises used: mul_lt_mul_of_pos_right, LT.lt.trans_le, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : PosMulStrictMono α
inst_4 : MulPosStrictMono α
h₁ : a < b
h₂ : c < d
a0 : 0 < a
d0 : 0 < d
⊢ a * c < b * d

Tactic:
(mul_lt_mul_of_pos_left h₂ a0).trans (mul_lt_mul_of_pos_right h₁ d0)

Premises used: mul_lt_mul_of_pos_left, mul_lt_mul_of_pos_right, LT.lt.trans
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : PosMulStrictMono α
inst_4 : MulPosStrictMono α
h₁ : a < b
h₂ : c < d
c0 : 0 < c
b0 : 0 < b
⊢ a * c < b * d

Tactic:
(mul_lt_mul_of_pos_right h₁ c0).trans (mul_lt_mul_of_pos_left h₂ b0)

Premises used: mul_lt_mul_of_pos_left, mul_lt_mul_of_pos_right, LT.lt.trans
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : PosMulMono α
h : a * b ≤ c
hle : d ≤ b
a0 : 0 ≤ a
⊢ a * d ≤ c

Tactic:
(mul_le_mul_of_nonneg_left hle a0).trans h

Premises used: LE.le.trans, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : PosMulMono α
h : a * b < c
hle : d ≤ b
a0 : 0 ≤ a
⊢ a * d < c

Tactic:
(mul_le_mul_of_nonneg_left hle a0).trans_lt h

Premises used: LE.le.trans_lt, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : PosMulMono α
h : a ≤ b * c
hle : c ≤ d
b0 : 0 ≤ b
⊢ a ≤ b * d

Tactic:
h.trans (mul_le_mul_of_nonneg_left hle b0)

Premises used: LE.le.trans, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : PosMulMono α
h : a < b * c
hle : c ≤ d
b0 : 0 ≤ b
⊢ a < b * d

Tactic:
h.trans_le (mul_le_mul_of_nonneg_left hle b0)

Premises used: LT.lt.trans_le, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : MulPosMono α
h : a * b ≤ c
hle : d ≤ a
b0 : 0 ≤ b
⊢ d * b ≤ c

Tactic:
(mul_le_mul_of_nonneg_right hle b0).trans h

Premises used: mul_le_mul_of_nonneg_right, LE.le.trans
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : MulPosMono α
h : a * b < c
hle : d ≤ a
b0 : 0 ≤ b
⊢ d * b < c

Tactic:
(mul_le_mul_of_nonneg_right hle b0).trans_lt h

Premises used: mul_le_mul_of_nonneg_right, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : MulPosMono α
h : a ≤ b * c
hle : b ≤ d
c0 : 0 ≤ c
⊢ a ≤ d * c

Tactic:
h.trans (mul_le_mul_of_nonneg_right hle c0)

Premises used: mul_le_mul_of_nonneg_right, LE.le.trans
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
a b c d : α
inst_3 : MulPosMono α
h : a < b * c
hle : b ≤ d
c0 : 0 ≤ c
⊢ a < d * c

Tactic:
h.trans_le (mul_le_mul_of_nonneg_right hle c0)

Premises used: mul_le_mul_of_nonneg_right, LT.lt.trans_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : IsMulCommutative α
⊢ PosMulMono α ↔ MulPosMono α

Tactic:
simp [posMulMono_iff, mulPosMono_iff, mul_comm']

Premises used: mulPosMono_iff, posMulMono_iff, mul_comm'