awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a < 1
n : ℤ
rw : a ^ n * a < a ^ n
⊢ a ^ (n + 1) < a ^ n

Tactic:
rw [zpow_add_one₀ ha₀.ne']

Premises used: zpow_add_one₀, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a < 1
n : ℤ
⊢ a ^ n * a < a ^ n

Tactic:
mul_lt_of_lt_one_right (zpow_pos ha₀ _) ha₁

Premises used: zpow_pos, mul_lt_of_lt_one_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a < 1
n : ℤ
⊢ a ^ n * a < a ^ n

Tactic:
exact mul_lt_of_lt_one_right (zpow_pos ha₀ _) ha₁

Premises used: zpow_pos, mul_lt_of_lt_one_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
m n : ℤ
ha : 1 ≤ a
hmn : m ≤ n
⊢ a ^ m ≤ a ^ n

Tactic:
zpow_right_mono₀ ha hmn

Premises used: zpow_right_mono₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
m n : ℤ
ha₀ : 0 < a
ha₁ : a ≤ 1
hmn : m ≤ n
⊢ a ^ n ≤ a ^ m

Tactic:
zpow_right_anti₀ ha₀ ha₁ hmn

Premises used: zpow_right_anti₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha : 1 ≤ a
hn : 0 ≤ n
⊢ 1 ≤ a ^ n

Tactic:
simpa using zpow_right_mono₀ ha hn

Premises used: zpow_right_mono₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a ≤ 1
hn : 0 ≤ n
⊢ a ^ n ≤ 1

Tactic:
simpa using zpow_right_anti₀ ha₀ ha₁ hn

Premises used: zpow_right_anti₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha : 1 ≤ a
hn : n ≤ 0
⊢ a ^ n ≤ 1

Tactic:
simpa using zpow_right_mono₀ ha hn

Premises used: zpow_right_mono₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a ≤ 1
hn : n ≤ 0
⊢ 1 ≤ a ^ n

Tactic:
simpa using zpow_right_anti₀ ha₀ ha₁ hn

Premises used: zpow_right_anti₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
m n : ℤ
ha : 1 < a
hmn : m < n
⊢ a ^ m < a ^ n

Tactic:
zpow_right_strictMono₀ ha hmn

Premises used: zpow_right_strictMono₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
m n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
hmn : m < n
⊢ a ^ n < a ^ m

Tactic:
zpow_right_strictAnti₀ ha₀ ha₁ hmn

Premises used: zpow_right_strictAnti₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha : 1 < a
hn : 0 < n
⊢ 1 < a ^ n

Tactic:
simpa using zpow_right_strictMono₀ ha hn

Premises used: zpow_right_strictMono₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
hn : 0 < n
⊢ a ^ n < 1

Tactic:
simpa using zpow_right_strictAnti₀ ha₀ ha₁ hn

Premises used: zpow_right_strictAnti₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha : 1 < a
hn : n < 0
⊢ a ^ n < 1

Tactic:
simpa using zpow_right_strictMono₀ ha hn

Premises used: zpow_right_strictMono₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
hn : n < 0
⊢ 1 < a ^ n

Tactic:
simpa using zpow_right_strictAnti₀ ha₀ ha₁ hn

Premises used: zpow_right_strictAnti₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
m n : ℤ
ha : 1 < a
⊢ a ^ m ≤ a ^ n ↔ m ≤ n

Tactic:
(zpow_right_strictMono₀ ha).le_iff_le

Premises used: zpow_right_strictMono₀, StrictMono.le_iff_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
m n : ℤ
ha : 1 < a
⊢ a ^ m < a ^ n ↔ m < n

Tactic:
(zpow_right_strictMono₀ ha).lt_iff_lt

Premises used: StrictMono.lt_iff_lt, zpow_right_strictMono₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
m n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
⊢ a ^ m ≤ a ^ n ↔ n ≤ m

Tactic:
(zpow_right_strictAnti₀ ha₀ ha₁).le_iff_ge

Premises used: StrictAnti.le_iff_ge, zpow_right_strictAnti₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
m n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
⊢ a ^ m < a ^ n ↔ n < m

Tactic:
(zpow_right_strictAnti₀ ha₀ ha₁).lt_iff_gt

Premises used: StrictAnti.lt_iff_gt, zpow_right_strictAnti₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha : 1 < a
⊢ 1 ≤ a ^ n ↔ 0 ≤ n

Tactic:
simp [← zpow_le_zpow_iff_right₀ ha]

Premises used: zpow_le_zpow_iff_right₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha : 1 < a
⊢ 1 < a ^ n ↔ 0 < n

Tactic:
simp [← zpow_lt_zpow_iff_right₀ ha]

Premises used: zpow_lt_zpow_iff_right₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
⊢ 1 ≤ a ^ n ↔ n ≤ 0

Tactic:
simp [← zpow_le_zpow_iff_right_of_lt_one₀ ha₀ ha₁]

Premises used: zpow_le_zpow_iff_right_of_lt_one₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
⊢ 1 < a ^ n ↔ n < 0

Tactic:
simp [← zpow_lt_zpow_iff_right_of_lt_one₀ ha₀ ha₁]

Premises used: zpow_lt_zpow_iff_right_of_lt_one₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha : 1 < a
⊢ a ^ n ≤ 1 ↔ n ≤ 0

Tactic:
simp [← zpow_le_zpow_iff_right₀ ha]

Premises used: zpow_le_zpow_iff_right₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha : 1 < a
⊢ a ^ n < 1 ↔ n < 0

Tactic:
simp [← zpow_lt_zpow_iff_right₀ ha]

Premises used: zpow_lt_zpow_iff_right₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
⊢ a ^ n ≤ 1 ↔ 0 ≤ n

Tactic:
simp [← zpow_le_zpow_iff_right_of_lt_one₀ ha₀ ha₁]

Premises used: zpow_le_zpow_iff_right_of_lt_one₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
⊢ a ^ n < 1 ↔ 0 < n

Tactic:
simp [← zpow_lt_zpow_iff_right_of_lt_one₀ ha₀ ha₁]

Premises used: zpow_lt_zpow_iff_right_of_lt_one₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosMono G₀
n : ℤ
hn : 0 ≤ n
⊢ 0 ≤ n

Tactic:
hn
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosMono G₀
n : ℤ
hn : 0 ≤ n
lift : ∀ (n : ℕ), MonotoneOn (β := G₀) (fun (a : G₀) ↦ HPow.hPow (β := ℤ) a (↑n : ℤ)) {a : G₀ | 0 ≤ a}
⊢ MonotoneOn (β := G₀) (fun (a : G₀) ↦ a ^ n) {a : G₀ | 0 ≤ a}

Tactic:
lift n to ℕ using hn
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosMono G₀
n : ℕ
⊢ MonotoneOn (β := G₀) (fun (a : G₀) ↦ HPow.hPow (β := ℤ) a (↑n : ℤ)) {a : G₀ | 0 ≤ a}

Tactic:
simpa using pow_left_monotoneOn

Premises used: pow_left_monotoneOn
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosMono G₀
n : ℤ
hn : 0 < n
⊢ 0 ≤ n

Tactic:
hn.le

Premises used: LT.lt.le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosMono G₀
n : ℤ
hn : 0 < n
lift :
  ∀ (n : ℕ) (hn : LT.lt (α := ℤ) 0 (↑n : ℤ)),
    StrictMonoOn (β := G₀) (fun (a : G₀) ↦ HPow.hPow (β := ℤ) a (↑n : ℤ)) {a : G₀ | 0 ≤ a}
⊢ StrictMonoOn (β := G₀) (fun (a : G₀) ↦ a ^ n) {a : G₀ | 0 ≤ a}

Tactic:
lift n to ℕ using hn.le

Premises used: LT.lt.le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosMono G₀
n : ℕ
hn : LT.lt (α := ℤ) 0 (↑n : ℤ)
⊢ n ≠ 0

Tactic:
lia
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosMono G₀
n : ℕ
hn : LT.lt (α := ℤ) 0 (↑n : ℤ)
⊢ StrictMonoOn (β := G₀) (fun (a : G₀) ↦ HPow.hPow (β := ℤ) a (↑n : ℤ)) {a : G₀ | 0 ≤ a}

Tactic:
simpa using pow_left_strictMonoOn₀ (by lia)

Premises used: pow_left_strictMonoOn₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b : G₀
inst_3 : MulPosMono G₀
n : ℤ
hn : 0 ≤ n
ha : 0 ≤ a
h : a ≤ b
⊢ Membership.mem (γ := Set G₀) {a : G₀ | 0 ≤ a} b

Tactic:
grind
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b : G₀
inst_3 : MulPosMono G₀
n : ℤ
hn : 0 < n
ha : 0 ≤ a
h : a < b
⊢ Membership.mem (γ := Set G₀) {a : G₀ | 0 ≤ a} b

Tactic:
grind
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a : G₀
suffices : ∀ (a : G₀), 0 < a → 0 < a⁻¹
⊢ 0 < a⁻¹ ↔ 0 < a

Tactic:
suffices ∀ a : G₀, 0 < a → 0 < a⁻¹ from ⟨fun h ↦ inv_inv a ▸ this _ h, this a⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a_1 a : G₀
ha : 0 < a
apply : 0 * a < a⁻¹ * a
⊢ 0 < a⁻¹

Tactic:
apply lt_of_mul_lt_mul_right _ ha.le

Premises used: LT.lt.le, lt_of_mul_lt_mul_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a_1 a : G₀
ha : 0 < a
apply : 0 * a * a < a⁻¹ * a * a
⊢ 0 * a < a⁻¹ * a

Tactic:
apply lt_of_mul_lt_mul_right _ ha.le

Premises used: LT.lt.le, lt_of_mul_lt_mul_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a_1 a : G₀
ha : 0 < a
⊢ 0 * a * a < a⁻¹ * a * a

Tactic:
simpa [ha.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a : G₀
ha : 0 < a
b c : G₀
hbc : b < c
⊢ b * a * a⁻¹ < c * a * a⁻¹

Tactic:
simpa [ha.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a : G₀
⊢ 0 ≤ a⁻¹ ↔ 0 ≤ a

Tactic:
simp only [le_iff_eq_or_lt, inv_pos, zero_eq_inv]

Premises used: le_iff_eq_or_lt, zero_eq_inv, Right.inv_pos
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
ha : a ≤ 0
hb : 0 ≤ b
rw : a * b⁻¹ ≤ 0
⊢ a / b ≤ 0

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b⁻¹ ≤ 0

Tactic:
mul_nonpos_of_nonpos_of_nonneg ha (Right.inv_nonneg.2 hb)

Premises used: Iff.mpr, mul_nonpos_of_nonpos_of_nonneg, Right.inv_nonneg
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b⁻¹ ≤ 0

Tactic:
exact mul_nonpos_of_nonpos_of_nonneg ha (Right.inv_nonneg.2 hb)

Premises used: Iff.mpr, mul_nonpos_of_nonpos_of_nonneg, Right.inv_nonneg
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
rw : a * c ≤ b * c⁻¹ * c ↔ a * c ≤ b
rw₁ rw₂ : a * c ≤ b ↔ a * c ≤ b
⊢ a ≤ b * c⁻¹ ↔ a * c ≤ b

Tactic:
rw [← mul_le_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']

Premises used: mul_le_mul_iff_of_pos_right, LT.lt.ne', inv_mul_cancel_right₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
rw : b * c⁻¹ * c ≤ a * c ↔ b ≤ a * c
rw₁ rw₂ : b ≤ a * c ↔ b ≤ a * c
⊢ b * c⁻¹ ≤ a ↔ b ≤ a * c

Tactic:
rw [← mul_le_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']

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

Tactic:
rw [← mul_lt_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']

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

Tactic:
rw [← mul_lt_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']

Premises used: LT.lt.ne', mul_lt_mul_iff_of_pos_right, inv_mul_cancel_right₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
rw : a ≤ b * c⁻¹ ↔ a * c ≤ b
rw₁ rw₂ : a * c ≤ b ↔ a * c ≤ b
⊢ a ≤ b / c ↔ a * c ≤ b

Tactic:
rw [div_eq_mul_inv, le_mul_inv_iff₀ hc]

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

Tactic:
rw [div_eq_mul_inv, mul_inv_le_iff₀ hc]

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

Tactic:
rw [div_eq_mul_inv, lt_mul_inv_iff₀ hc]

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

Tactic:
rw [div_eq_mul_inv, mul_inv_lt_iff₀ hc]

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

Tactic:
rw [div_le_iff₀ hc, div_mul_cancel₀ _ hc.ne']

Premises used: div_le_iff₀, div_mul_cancel₀, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
rw : a < b / c * c ↔ a < b
rw₁ rw₂ : a < b ↔ a < b
⊢ a / c < b / c ↔ a < b

Tactic:
rw [div_lt_iff₀ hc, div_mul_cancel₀ _ hc.ne']

Premises used: div_mul_cancel₀, div_lt_iff₀, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
rw : a⁻¹ ≤ b ↔ 1 * a⁻¹ ≤ b
rw₁ rw₂ : a⁻¹ ≤ b ↔ a⁻¹ ≤ b
⊢ a⁻¹ ≤ b ↔ 1 ≤ b * a

Tactic:
rw [← mul_inv_le_iff₀ ha, one_mul]

Premises used: mul_inv_le_iff₀, one_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
rw : a⁻¹ < b ↔ 1 * a⁻¹ < b
rw₁ rw₂ : a⁻¹ < b ↔ a⁻¹ < b
⊢ a⁻¹ < b ↔ 1 < b * a

Tactic:
rw [← mul_inv_lt_iff₀ ha, one_mul]

Premises used: mul_inv_lt_iff₀, one_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
rw : 1 * b ≤ a ↔ b ≤ a
rw₁ rw₂ : b ≤ a ↔ b ≤ a
⊢ 1 ≤ a / b ↔ b ≤ a

Tactic:
rw [le_div_iff₀ hb, one_mul]

Premises used: le_div_iff₀, one_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
rw : 1 * b < a ↔ b < a
rw₁ rw₂ : b < a ↔ b < a
⊢ 1 < a / b ↔ b < a

Tactic:
rw [lt_div_iff₀ hb, one_mul]

Premises used: lt_div_iff₀, one_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
rw : a ≤ 1 * b ↔ a ≤ b
rw₁ rw₂ : a ≤ b ↔ a ≤ b
⊢ a / b ≤ 1 ↔ a ≤ b

Tactic:
rw [div_le_iff₀ hb, one_mul]

Premises used: div_le_iff₀, one_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
rw : a < 1 * b ↔ a < b
rw₁ rw₂ : a < b ↔ a < b
⊢ a / b < 1 ↔ a < b

Tactic:
rw [div_lt_iff₀ hb, one_mul]

Premises used: div_lt_iff₀, one_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b * c⁻¹
inl : ∀ (hc : LE.le.{u_3} (α := G₀) 0 0) (h : a ≤ b * 0⁻¹), a * 0 ≤ b
inr : ∀ (hc : 0 < c), a * c ≤ b
⊢ 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.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
hb : 0 ≤ b
hc : LE.le.{u_3} (α := G₀) 0 0
h : a ≤ b * 0⁻¹
⊢ a * 0 ≤ b

Tactic:
simpa using hb
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc_1 : 0 ≤ c
h : a ≤ b * c⁻¹
hc : 0 < c
inr inr₁ inr₂ inr₃ : ∀ (h : a * c ≤ b) (hc : 0 < c), a * c ≤ b
⊢ a * c ≤ b

Tactic:
rwa [le_mul_inv_iff₀ hc] at h

Premises used: le_mul_inv_iff₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
inl : ∀ (hb : LE.le.{u_3} (α := G₀) 0 0) (h : a ≤ c * 0), a * 0⁻¹ ≤ c
inr : ∀ (hb : 0 < b), a * b⁻¹ ≤ c
⊢ a * b⁻¹ ≤ c

Tactic:
obtain rfl | hb := hb.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a c : G₀
hc : 0 ≤ c
hb : LE.le.{u_3} (α := G₀) 0 0
h : a ≤ c * 0
⊢ a * 0⁻¹ ≤ c

Tactic:
simp [hc]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hb_1 : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
hb : 0 < b
inr inr₁ inr₂ inr₃ : a ≤ c * b
⊢ a * b⁻¹ ≤ c

Tactic:
rwa [mul_inv_le_iff₀ hb]

Premises used: mul_inv_le_iff₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b / c
⊢ a * c ≤ b

Tactic:
mul_le_of_le_mul_inv₀ hb hc (div_eq_mul_inv b _ ▸ h)

Premises used: Eq.rec, div_eq_mul_inv, mul_le_of_le_mul_inv₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
⊢ a / b ≤ c

Tactic:
div_eq_mul_inv a _ ▸ mul_inv_le_of_le_mul₀ hb hc h

Premises used: Eq.rec, div_eq_mul_inv, Eq.symm, mul_inv_le_of_le_mul₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
inst_3 : ZeroLEOneClass G₀
h : a ≤ b
hb : 0 ≤ b
rwa rwa₁ rwa₂ rwa₃ : a ≤ b
⊢ a ≤ 1 * b

Tactic:
rwa [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
rw : a * c⁻¹ ≤ b * c⁻¹
⊢ a / c ≤ b / c

Tactic:
rw [div_eq_mul_inv a c, div_eq_mul_inv b c]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
ha : 0 ≤ c⁻¹
⊢ a * c⁻¹ ≤ b * c⁻¹

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
⊢ 0 ≤ c⁻¹

Tactic:
Right.inv_nonneg.2 hc

Premises used: Iff.mpr, Right.inv_nonneg