awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : IsMulCommutative α
inst_4 : PosMulMono α
⊢ MulPosMono α

Tactic:
posMulMono_iff_mulPosMono.mp ‹_›

Premises used: posMulMono_iff_mulPosMono, Iff.mp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : IsMulCommutative α
⊢ PosMulStrictMono α ↔ MulPosStrictMono α

Tactic:
simp [posMulStrictMono_iff, mulPosStrictMono_iff, mul_comm']

Premises used: mulPosStrictMono_iff, posMulStrictMono_iff, mul_comm'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : IsMulCommutative α
inst_4 : PosMulStrictMono α
⊢ MulPosStrictMono α

Tactic:
posMulStrictMono_iff_mulPosStrictMono.mp ‹_›

Premises used: posMulStrictMono_iff_mulPosStrictMono, Iff.mp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : IsMulCommutative α
⊢ PosMulReflectLE α ↔ MulPosReflectLE α

Tactic:
simp [posMulReflectLE_iff, mulPosReflectLE_iff, mul_comm']

Premises used: mulPosReflectLE_iff, mul_comm', posMulReflectLE_iff
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : IsMulCommutative α
inst_4 : PosMulReflectLE α
⊢ MulPosReflectLE α

Tactic:
posMulReflectLE_iff_mulPosReflectLE.mp ‹_›

Premises used: posMulReflectLE_iff_mulPosReflectLE, Iff.mp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : IsMulCommutative α
⊢ PosMulReflectLT α ↔ MulPosReflectLT α

Tactic:
simp [posMulReflectLT_iff, mulPosReflectLT_iff, mul_comm']

Premises used: mulPosReflectLT_iff, posMulReflectLT_iff, mul_comm'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : IsMulCommutative α
inst_4 : PosMulReflectLT α
⊢ MulPosReflectLT α

Tactic:
posMulReflectLT_iff_mulPosReflectLT.mp ‹_›

Premises used: posMulReflectLT_iff_mulPosReflectLT, Iff.mp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : LinearOrder α
⊢ PosMulStrictMono α ↔ PosMulReflectLE α

Tactic:
⟨@PosMulStrictMono.toPosMulReflectLE _ _ _ _, @PosMulReflectLE.toPosMulStrictMono _ _ _ _⟩

Premises used: Iff.intro, PosMulStrictMono.toPosMulReflectLE, PosMulReflectLE.toPosMulStrictMono
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : LinearOrder α
⊢ MulPosStrictMono α ↔ MulPosReflectLE α

Tactic:
⟨@MulPosStrictMono.toMulPosReflectLE _ _ _ _, @MulPosReflectLE.toMulPosStrictMono _ _ _ _⟩

Premises used: MulPosReflectLE.toMulPosStrictMono, Iff.intro, MulPosStrictMono.toMulPosReflectLE
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : LinearOrder α
⊢ PosMulMono α ↔ PosMulReflectLT α

Tactic:
⟨@PosMulMono.toPosMulReflectLT _ _ _ _, @PosMulReflectLT.toPosMulMono _ _ _ _⟩

Premises used: PosMulReflectLT.toPosMulMono, PosMulMono.toPosMulReflectLT, Iff.intro
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : LinearOrder α
⊢ MulPosMono α ↔ MulPosReflectLT α

Tactic:
⟨@MulPosMono.toMulPosReflectLT _ _ _ _, @MulPosReflectLT.toMulPosMono _ _ _ _⟩

Premises used: MulPosReflectLT.toMulPosMono, Iff.intro, MulPosMono.toMulPosReflectLT
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
ha : 0 < a
h : ∀ (x : G₀), Eq (α := G₀) (((mulLeft₀ a ha).symm : (a : G₀) → G₀) x : G₀) ((mulLeft₀ a⁻¹ ⋯ : (a : G₀) → G₀) x : G₀)
⊢ (mulLeft₀ a ha).symm = mulLeft₀ a⁻¹ ⋯

Tactic:
ext
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
ha : 0 < a
x : G₀
⊢ Eq (α := G₀) (((mulLeft₀ a ha).symm : (a : G₀) → G₀) x : G₀) ((mulLeft₀ a⁻¹ ⋯ : (a : G₀) → G₀) x : G₀)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a : G₀
ha : 0 < a
h : ∀ (x : G₀), Eq (α := G₀) (((mulRight₀ a ha).symm : (a : G₀) → G₀) x : G₀) ((mulRight₀ a⁻¹ ⋯ : (a : G₀) → G₀) x : G₀)
⊢ (mulRight₀ a ha).symm = mulRight₀ a⁻¹ ⋯

Tactic:
ext
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a : G₀
ha : 0 < a
x : G₀
⊢ Eq (α := G₀) (((mulRight₀ a ha).symm : (a : G₀) → G₀) x : G₀) ((mulRight₀ a⁻¹ ⋯ : (a : G₀) → G₀) x : G₀)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a : G₀
ha : 0 < a
b c : G₀
simp : b * a⁻¹ ≤ c * a⁻¹ ↔ b ≤ c
⊢ LE.le (α := G₀) ((Equiv.divRight₀ a ⋯ : (a : G₀) → G₀) b : G₀) ((Equiv.divRight₀ a ⋯ : (a : G₀) → G₀) c : G₀) ↔ b ≤ c

Tactic:
simp only [Equiv.divRight₀_apply, div_eq_mul_inv]

Premises used: div_eq_mul_inv, Equiv.divRight₀_apply
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a : G₀
ha : 0 < a
b c : G₀
⊢ b * a⁻¹ ≤ c * a⁻¹ ↔ b ≤ c

Tactic:
mul_le_mul_iff_left₀ (a := a⁻¹) (Right.inv_pos.mpr ha)

Premises used: Iff.mpr, Right.inv_pos, mul_le_mul_iff_left₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a : G₀
ha : 0 < a
b c : G₀
⊢ b * a⁻¹ ≤ c * a⁻¹ ↔ b ≤ c

Tactic:
exact mul_le_mul_iff_left₀ (a := a⁻¹) (Right.inv_pos.mpr ha)

Premises used: Iff.mpr, Right.inv_pos, mul_le_mul_iff_left₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeInf G₀
inst_2 : PosMulReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
inl : ∀ (hc : LE.le.{u_1} (α := G₀) 0 0), 0 * (a ⊓ b) = 0 * a ⊓ 0 * b
inr : ∀ (hc : 0 < c), c * (a ⊓ b) = c * a ⊓ c * b
⊢ c * (a ⊓ b) = c * a ⊓ c * b

Tactic:
obtain (rfl | hc) := hc.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeInf G₀
inst_2 : PosMulReflectLT G₀
a b : G₀
hc : LE.le.{u_1} (α := G₀) 0 0
⊢ 0 * (a ⊓ b) = 0 * a ⊓ 0 * b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeInf G₀
inst_2 : PosMulReflectLT G₀
c : G₀
hc_1 : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ c * (a ⊓ b) = c * a ⊓ c * b

Tactic:
(OrderIso.mulLeft₀ c hc).map_inf a b

Premises used: OrderIso.map_inf, OrderIso.mulLeft₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeInf G₀
inst_2 : PosMulReflectLT G₀
c : G₀
hc_1 : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ c * (a ⊓ b) = c * a ⊓ c * b

Tactic:
exact (OrderIso.mulLeft₀ c hc).map_inf a b

Premises used: OrderIso.map_inf, OrderIso.mulLeft₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
inst_2 : PosMulReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
inl : ∀ (hc : LE.le.{u_1} (α := G₀) 0 0), 0 * (a ⊔ b) = 0 * a ⊔ 0 * b
inr : ∀ (hc : 0 < c), c * (a ⊔ b) = c * a ⊔ c * b
⊢ c * (a ⊔ b) = c * a ⊔ c * b

Tactic:
obtain (rfl | hc) := hc.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
inst_2 : PosMulReflectLT G₀
a b : G₀
hc : LE.le.{u_1} (α := G₀) 0 0
⊢ 0 * (a ⊔ b) = 0 * a ⊔ 0 * b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
inst_2 : PosMulReflectLT G₀
c : G₀
hc_1 : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ c * (a ⊔ b) = c * a ⊔ c * b

Tactic:
(OrderIso.mulLeft₀ c hc).map_sup a b

Premises used: OrderIso.mulLeft₀, OrderIso.map_sup
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
inst_2 : PosMulReflectLT G₀
c : G₀
hc_1 : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ c * (a ⊔ b) = c * a ⊔ c * b

Tactic:
exact (OrderIso.mulLeft₀ c hc).map_sup a b

Premises used: OrderIso.mulLeft₀, OrderIso.map_sup
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeInf G₀
inst_2 : MulPosReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
inl : ∀ (hc : LE.le.{u_1} (α := G₀) 0 0), (a ⊓ b) * 0 = a * 0 ⊓ b * 0
inr : ∀ (hc : 0 < c), (a ⊓ b) * c = a * c ⊓ b * c
⊢ (a ⊓ b) * c = a * c ⊓ b * c

Tactic:
obtain (rfl | hc) := hc.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeInf G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
hc : LE.le.{u_1} (α := G₀) 0 0
⊢ (a ⊓ b) * 0 = a * 0 ⊓ b * 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeInf G₀
inst_2 : MulPosReflectLT G₀
c : G₀
hc_1 : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ (a ⊓ b) * c = a * c ⊓ b * c

Tactic:
(OrderIso.mulRight₀ c hc).map_inf a b

Premises used: OrderIso.map_inf, OrderIso.mulRight₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeInf G₀
inst_2 : MulPosReflectLT G₀
c : G₀
hc_1 : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ (a ⊓ b) * c = a * c ⊓ b * c

Tactic:
exact (OrderIso.mulRight₀ c hc).map_inf a b

Premises used: OrderIso.map_inf, OrderIso.mulRight₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
inst_2 : MulPosReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
inl : ∀ (hc : LE.le.{u_1} (α := G₀) 0 0), (a ⊔ b) * 0 = a * 0 ⊔ b * 0
inr : ∀ (hc : 0 < c), (a ⊔ b) * c = a * c ⊔ b * c
⊢ (a ⊔ b) * c = a * c ⊔ b * c

Tactic:
obtain (rfl | hc) := hc.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
hc : LE.le.{u_1} (α := G₀) 0 0
⊢ (a ⊔ b) * 0 = a * 0 ⊔ b * 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
inst_2 : MulPosReflectLT G₀
c : G₀
hc_1 : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ (a ⊔ b) * c = a * c ⊔ b * c

Tactic:
(OrderIso.mulRight₀ c hc).map_sup a b

Premises used: OrderIso.mulRight₀, OrderIso.map_sup
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
inst_2 : MulPosReflectLT G₀
c : G₀
hc_1 : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ (a ⊔ b) * c = a * c ⊔ b * c

Tactic:
exact (OrderIso.mulRight₀ c hc).map_sup a b

Premises used: OrderIso.mulRight₀, OrderIso.map_sup
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
x : α
hx : 0 < (↑x : WithZero α)
b : α
h : 0 < (↑b : WithZero α)
⊢ (↑x : WithZero α) * 0 < (↑x : WithZero α) * (↑b : WithZero α)

Tactic:
simpa only [mul_zero] using WithZero.zero_lt_coe _

Premises used: MulZeroClass.mul_zero, WithZero.zero_lt_coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
x : α
hx : 0 < (↑x : WithZero α)
a b : α
h : (↑a : WithZero α) < (↑b : WithZero α)
norm_cast : ∀ (h : a < b), x * a < x * b
⊢ (↑x : WithZero α) * (↑a : WithZero α) < (↑x : WithZero α) * (↑b : WithZero α)

Tactic:
norm_cast at h ⊢
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
x : α
hx : 0 < (↑x : WithZero α)
a b : α
h : a < b
⊢ x * a < x * b

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulRightStrictMono α
x : α
hx : 0 < (↑x : WithZero α)
b : α
h : 0 < (↑b : WithZero α)
⊢ 0 * (↑x : WithZero α) < (↑b : WithZero α) * (↑x : WithZero α)

Tactic:
simpa only [mul_zero] using WithZero.zero_lt_coe _

Premises used: MulZeroClass.mul_zero, WithZero.zero_lt_coe
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulRightStrictMono α
x : α
hx : 0 < (↑x : WithZero α)
a b : α
h : (↑a : WithZero α) < (↑b : WithZero α)
norm_cast : ∀ (h : a < b), a * x < b * x
⊢ (↑a : WithZero α) * (↑x : WithZero α) < (↑b : WithZero α) * (↑x : WithZero α)

Tactic:
norm_cast at h ⊢
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulRightStrictMono α
x : α
hx : 0 < (↑x : WithZero α)
a b : α
h : a < b
⊢ a * x < b * x

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
h : LE.le.{u_1} (α := WithZero α) 0 0
a b : WithZero α
h_1 : a ≤ b
⊢ 0 * a ≤ 0 * b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
x : α
h : 0 ≤ (↑x : WithZero α)
x_1 : WithZero α
h_1 : 0 ≤ x_1
⊢ (↑x : WithZero α) * 0 ≤ (↑x : WithZero α) * x_1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
x : α
h_1 : 0 ≤ (↑x : WithZero α)
a : α
h : (↑a : WithZero α) ≤ 0
⊢ (↑x : WithZero α) * (↑a : WithZero α) ≤ (↑x : WithZero α) * 0

Tactic:
simp at h
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
x : α
hx : 0 ≤ (↑x : WithZero α)
a b : α
h : (↑a : WithZero α) ≤ (↑b : WithZero α)
norm_cast : ∀ (h : a ≤ b), x * a ≤ x * b
⊢ (↑x : WithZero α) * (↑a : WithZero α) ≤ (↑x : WithZero α) * (↑b : WithZero α)

Tactic:
norm_cast at h ⊢
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
x : α
hx : 0 ≤ (↑x : WithZero α)
a b : α
h : a ≤ b
⊢ x * a ≤ x * b

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulRightMono α
h : LE.le.{u_1} (α := WithZero α) 0 0
a b : WithZero α
h_1 : a ≤ b
⊢ a * 0 ≤ b * 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulRightMono α
x : α
h : 0 ≤ (↑x : WithZero α)
x_1 : WithZero α
h_1 : 0 ≤ x_1
⊢ 0 * (↑x : WithZero α) ≤ x_1 * (↑x : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulRightMono α
x : α
h_1 : 0 ≤ (↑x : WithZero α)
a : α
h : (↑a : WithZero α) ≤ 0
⊢ (↑a : WithZero α) * (↑x : WithZero α) ≤ 0 * (↑x : WithZero α)

Tactic:
simp at h
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulRightMono α
x : α
hx : 0 ≤ (↑x : WithZero α)
a b : α
h : (↑a : WithZero α) ≤ (↑b : WithZero α)
norm_cast : ∀ (h : a ≤ b), a * x ≤ b * x
⊢ (↑a : WithZero α) * (↑x : WithZero α) ≤ (↑b : WithZero α) * (↑x : WithZero α)

Tactic:
norm_cast at h ⊢
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulRightMono α
x : α
hx : 0 ≤ (↑x : WithZero α)
a b : α
h : a ≤ b
⊢ a * x ≤ b * x

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a b : WithZero αˣ
zero :
  0 < b →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) b : α)
coe :
  ∀ (a : αˣ),
    (↑a : WithZero αˣ) < b →
      LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a : WithZero αˣ) : α)
        ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) b : α)
⊢ a < b →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) a : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) b : α)

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
b : WithZero αˣ
zero :
  LT.lt.{u_1} (α := WithZero αˣ) 0 0 →
    LT.lt.{u_1} (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
zero₁ :
  ∀ (a : αˣ),
    0 < (↑a : WithZero αˣ) →
      LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
        ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a : WithZero αˣ) : α)
⊢ 0 < b →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) b : α)

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
b : WithZero αˣ
a : αˣ
coe :
  (↑a : WithZero αˣ) < 0 →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a : WithZero αˣ) : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
coe₁ :
  ∀ (a_1 : αˣ),
    (↑a : WithZero αˣ) < (↑a_1 : WithZero αˣ) →
      LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a : WithZero αˣ) : α)
        ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a_1 : WithZero αˣ) : α)
⊢ (↑a : WithZero αˣ) < b →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a : WithZero αˣ) : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) b : α)

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
⊢ LT.lt.{u_1} (α := WithZero αˣ) 0 0 →
    LT.lt.{u_1} (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a : αˣ
⊢ 0 < (↑a : WithZero αˣ) →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a : WithZero αˣ) : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a : αˣ
⊢ (↑a : WithZero αˣ) < 0 →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a : WithZero αˣ) : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a a_1 : αˣ
⊢ (↑a : WithZero αˣ) < (↑a_1 : WithZero αˣ) →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a : WithZero αˣ) : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a_1 : WithZero αˣ) : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
⊢ StrictMono.{u_1, u_1} (α := α) (β := WithZero αˣ) (⇑(MulEquiv.symm withZeroUnitsEquiv) : (a : α) → WithZero αˣ)

Tactic:
OrderIso.withZeroUnits.symm.strictMono

Premises used: OrderIso.strictMono, OrderIso.withZeroUnits, OrderIso.symm, dite
-- Module: Mathlib.Algebra.Order.Hom.Basic
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : Group α
inst_2 : CommMagma β
inst_3 : LE β
inst_4 : SubmultiplicativeHomClass F α β
f : F
a b : α
⊢ (f : (a : α) → β) a ≤ HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (a / b) : β)

Tactic:
simpa only [mul_comm, div_mul_cancel] using map_mul_le_mul f (a / b) b

Premises used: HDiv.hDiv, mul_comm, div_mul_cancel, SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Algebra.Order.Hom.Basic
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : Group α
inst_2 : AddCommMagma β
inst_3 : LE β
inst_4 : MulLEAddHomClass F α β
f : F
a b : α
⊢ (f : (a : α) → β) a ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (a / b) : β)

Tactic:
simpa only [add_comm, div_mul_cancel] using map_mul_le_add f (a / b) b

Premises used: HDiv.hDiv, add_comm, MulLEAddHomClass.map_mul_le_add, div_mul_cancel
-- Module: Mathlib.Algebra.Order.Hom.Basic
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : Group α
inst_2 : Mul β
inst_3 : LE β
inst_4 : SubmultiplicativeHomClass F α β
f : F
a b c : α
⊢ (f : (a : α) → β) (a / c) ≤
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) (a / b) : β) ((f : (a : α) → β) (b / c) : β)

Tactic:
simpa only [div_mul_div_cancel] using map_mul_le_mul f (a / b) (b / c)

Premises used: HDiv.hDiv, div_mul_div_cancel, SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Algebra.Order.Hom.Basic
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : Group α
inst_2 : Add β
inst_3 : LE β
inst_4 : MulLEAddHomClass F α β
f : F
a b c : α
⊢ (f : (a : α) → β) (a / c) ≤
    HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) (a / b) : β) ((f : (a : α) → β) (b / c) : β)

Tactic:
simpa only [div_mul_div_cancel] using map_mul_le_add f (a / b) (b / c)

Premises used: HDiv.hDiv, MulLEAddHomClass.map_mul_le_add, div_mul_div_cancel
-- Module: Mathlib.Algebra.Order.Hom.Basic
Goal:
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst : FunLike F α β
inst_1 : AddGroup α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : AddGroupSeminormClass F α β
⊢ ZeroHomClass F α β

Tactic:
{ ‹AddGroupSeminormClass F α β› with }

Premises used: ZeroHomClass.mk, AddGroupSeminormClass.map_zero
-- Module: Mathlib.Algebra.Order.Hom.Basic
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : Group α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : GroupSeminormClass F α β
f : F
x y : α
rw : (f : (a : α) → β) (x * y⁻¹) ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y⁻¹ : β)
⊢ (f : (a : α) → β) (x / y) ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
rw [div_eq_mul_inv, ← map_inv_eq_map f y]

Premises used: div_eq_mul_inv, GroupSeminormClass.map_inv_eq_map
-- Module: Mathlib.Algebra.Order.Hom.Basic
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : Group α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : GroupSeminormClass F α β
f : F
x y : α
⊢ (f : (a : α) → β) (x * y⁻¹) ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y⁻¹ : β)

Tactic:
map_mul_le_add _ _ _

Premises used: MulLEAddHomClass.map_mul_le_add
-- Module: Mathlib.Algebra.Order.Hom.Basic
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : Group α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : GroupSeminormClass F α β
f : F
x y : α
⊢ (f : (a : α) → β) (x * y⁻¹) ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y⁻¹ : β)

Tactic:
exact map_mul_le_add _ _ _

Premises used: MulLEAddHomClass.map_mul_le_add
-- Module: Mathlib.Algebra.Order.Hom.Basic
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : Group α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : GroupSeminormClass F α β
f : F
x y : α
rw : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (y / x)⁻¹ : β) ((f : (a : α) → β) (y / x) : β)
rw₁ rw₂ : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (y / x) : β) ((f : (a : α) → β) (y / x) : β)
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (x / y) : β) ((f : (a : α) → β) (y / x) : β)

Tactic:
rw [← inv_div, map_inv_eq_map]

Premises used: GroupSeminormClass.map_inv_eq_map, inv_div