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 : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
⊢ 0 ≤ c⁻¹

Tactic:
exact Right.inv_nonneg.2 hc

Premises used: Iff.mpr, 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₀
h : 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₀
h : a < b
hc : 0 < c
⊢ a * c⁻¹ < b * c⁻¹

Tactic:
mul_lt_mul_of_pos_right h (Right.inv_pos.2 hc)

Premises used: Iff.mpr, mul_lt_mul_of_pos_right, 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 c : G₀
h : a < b
hc : 0 < c
⊢ a * c⁻¹ < b * c⁻¹

Tactic:
exact mul_lt_mul_of_pos_right h (Right.inv_pos.2 hc)

Premises used: Iff.mpr, mul_lt_mul_of_pos_right, Right.inv_pos
-- 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 : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
rw : 1 ≤ a * b⁻¹ ↔ b ≤ a
rw₁ : 1 * b ≤ a ↔ b ≤ a
rw₂ rw₃ : b ≤ a ↔ b ≤ a
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Tactic:
rw [inv_le_iff_one_le_mul₀' ha, le_mul_inv_iff₀ hb, one_mul]

Premises used: le_mul_inv_iff₀, inv_le_iff_one_le_mul₀', one_mul
-- 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 : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
rw : 1 < a * b⁻¹ ↔ b < a
rw₁ : 1 * b < a ↔ b < a
rw₂ rw₃ : b < a ↔ b < a
⊢ a⁻¹ < b⁻¹ ↔ b < a

Tactic:
rw [inv_lt_iff_one_lt_mul₀' ha, lt_mul_inv_iff₀ hb, one_mul]

Premises used: lt_mul_inv_iff₀, inv_lt_iff_one_lt_mul₀', one_mul
-- 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 : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
hba : b ≤ a
⊢ a⁻¹ ≤ b⁻¹

Tactic:
(inv_le_inv₀ (hb.trans_le hba) hb).2 hba

Premises used: Iff.mpr, LT.lt.trans_le, inv_le_inv₀
-- 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 : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
hba : b < a
⊢ a⁻¹ < b⁻¹

Tactic:
(inv_lt_inv₀ (hb.trans hba) hb).2 hba

Premises used: Iff.mpr, LT.lt.trans, inv_lt_inv₀
-- 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 : MulPosReflectLT G₀
⊢ StrictAntiOn (β := G₀) (fun (x : G₀) ↦ x⁻¹) {r : G₀ | 0 < r}

Tactic:
fun ⦃_⦄ ha ⦃_⦄ _ h ↦ inv_strictAnti₀ (Set.mem_setOf.mp ha) h

Premises used: StrictAntiOn, Set.mem_setOf, Iff.mp, inv_strictAnti₀
-- 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 : MulPosReflectLT G₀
⊢ AntitoneOn (β := G₀) (fun (x : G₀) ↦ x⁻¹) {r : G₀ | 0 < r}

Tactic:
strictAntiOn_inv_pos.antitoneOn

Premises used: StrictAntiOn.antitoneOn, strictAntiOn_inv_pos
-- 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 : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
rw : b⁻¹ ≤ a⁻¹⁻¹ ↔ b⁻¹ ≤ a
rw₁ rw₂ : b⁻¹ ≤ a ↔ b⁻¹ ≤ a
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Tactic:
rw [← inv_le_inv₀ hb (inv_pos.2 ha), inv_inv]

Premises used: Iff.mpr, inv_pos, inv_inv, inv_le_inv₀
-- 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 : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
rw : b⁻¹ < a⁻¹⁻¹ ↔ b⁻¹ < a
rw₁ rw₂ : b⁻¹ < a ↔ b⁻¹ < a
⊢ a⁻¹ < b ↔ b⁻¹ < a

Tactic:
rw [← inv_lt_inv₀ hb (inv_pos.2 ha), inv_inv]

Premises used: Iff.mpr, inv_pos, inv_inv, inv_lt_inv₀
-- 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 : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
h : a⁻¹ ≤ b
⊢ b⁻¹ ≤ a

Tactic:
(inv_le_comm₀ ha <| (inv_pos.2 ha).trans_le h).1 h

Premises used: Iff.mpr, inv_pos, LT.lt.trans_le, inv_le_comm₀, Iff.mp
-- 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 : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
h : a⁻¹ < b
⊢ b⁻¹ < a

Tactic:
(inv_lt_comm₀ ha <| (inv_pos.2 ha).trans h).1 h

Premises used: Iff.mpr, inv_pos, inv_lt_comm₀, Iff.mp, LT.lt.trans
-- 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 : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
rw : b⁻¹⁻¹ ≤ a⁻¹ ↔ b ≤ a⁻¹
rw₁ rw₂ : b ≤ a⁻¹ ↔ b ≤ a⁻¹
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹

Tactic:
rw [← inv_le_inv₀ (inv_pos.2 hb) ha, inv_inv]

Premises used: Iff.mpr, inv_pos, inv_inv, inv_le_inv₀
-- 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 : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
rw : b⁻¹⁻¹ < a⁻¹ ↔ b < a⁻¹
rw₁ rw₂ : b < a⁻¹ ↔ b < a⁻¹
⊢ a < b⁻¹ ↔ b < a⁻¹

Tactic:
rw [← inv_lt_inv₀ (inv_pos.2 hb) ha, inv_inv]

Premises used: Iff.mpr, inv_pos, inv_inv, inv_lt_inv₀
-- 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 : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
h : a ≤ b⁻¹
⊢ b ≤ a⁻¹

Tactic:
(le_inv_comm₀ ha <| inv_pos.1 <| ha.trans_le h).1 h

Premises used: le_inv_comm₀, inv_pos, LT.lt.trans_le, Iff.mp
-- 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 : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
h : a < b⁻¹
⊢ b < a⁻¹

Tactic:
(lt_inv_comm₀ ha <| inv_pos.1 <| ha.trans h).1 h

Premises used: inv_pos, lt_inv_comm₀, Iff.mp, LT.lt.trans
-- 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 : MulPosReflectLT G₀
a b c : G₀
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a / b ≤ a / c ↔ c ≤ b

Tactic:
simp only [div_eq_mul_inv, mul_le_mul_iff_right₀ ha, inv_le_inv₀ hb hc]

Premises used: div_eq_mul_inv, mul_le_mul_iff_right₀, inv_le_inv₀
-- 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 : MulPosReflectLT G₀
a b c : G₀
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a / b < a / c ↔ c < b

Tactic:
lt_iff_lt_of_le_iff_le' (div_le_div_iff_of_pos_left ha hc hb)
    (div_le_div_iff_of_pos_left ha hb hc)

Premises used: div_le_div_iff_of_pos_left, lt_iff_lt_of_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₀
inst_3 : MulPosReflectLT G₀
a b c : G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
rw : a * b⁻¹ ≤ a * c⁻¹
⊢ a / b ≤ a / c

Tactic:
rw [div_eq_mul_inv, 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 : PosMulReflectLT G₀
inst_3 : MulPosReflectLT G₀
a b c : G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
ha₁ : 0 ≤ a
hbc : 0 < c
⊢ a * b⁻¹ ≤ a * c⁻¹

Tactic:
gcongr
-- 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 : MulPosReflectLT G₀
a b c : G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ 0 ≤ a

Tactic:
ha
-- 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 : MulPosReflectLT G₀
a b c : G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ 0 < c

Tactic:
hc
-- 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 : MulPosReflectLT G₀
a b c : G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ 0 ≤ a

Tactic:
exacts [ha, hc]
-- 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 : MulPosReflectLT G₀
a b c : G₀
ha : 0 < a
hc : 0 < c
h : c < b
⊢ a / b < a / c

Tactic:
(div_lt_div_iff_of_pos_left ha (hc.trans h) hc).mpr h

Premises used: Iff.mpr, div_lt_div_iff_of_pos_left, LT.lt.trans
-- 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 : MulPosReflectLT G₀
a b c d : G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
rw : a * b⁻¹ ≤ c * d⁻¹
⊢ a / b ≤ c / d

Tactic:
rw [div_eq_mul_inv, 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 : PosMulReflectLT G₀
inst_3 : MulPosReflectLT G₀
a b c d : G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
c0 : 0 ≤ b⁻¹
b0 : 0 ≤ c
h₂ : 0 < d
⊢ a * b⁻¹ ≤ c * d⁻¹

Tactic:
gcongr
-- 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 : MulPosReflectLT G₀
a b c d : G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ 0 ≤ b⁻¹

Tactic:
inv_nonneg.2 <| hd.le.trans hdb

Premises used: Iff.mpr, LT.lt.le, inv_nonneg, LE.le.trans
-- 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 : MulPosReflectLT G₀
a b c d : G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ 0 ≤ c

Tactic:
hc
-- 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 : MulPosReflectLT G₀
a b c d : G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ 0 < d

Tactic:
hd
-- 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 : MulPosReflectLT G₀
a b c d : G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ 0 ≤ b⁻¹

Tactic:
exacts [inv_nonneg.2 <| hd.le.trans hdb, hc, hd]

Premises used: Iff.mpr, LT.lt.le, inv_nonneg, LE.le.trans
-- 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 : MulPosReflectLT G₀
a b c d : G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
rw : a * b⁻¹ < c * d⁻¹
⊢ a / b < c / d

Tactic:
rw [div_eq_mul_inv, 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 : PosMulReflectLT G₀
inst_3 : MulPosReflectLT G₀
a b c d : G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd hb : 0 < d
⊢ b⁻¹ ≤ d⁻¹

Tactic:
gcongr
-- 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 : MulPosReflectLT G₀
a b c d : G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
⊢ 0 < d

Tactic:
assumption
-- 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 : MulPosReflectLT G₀
a b c d : G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
apply : 0 < b⁻¹
⊢ a * b⁻¹ < c * d⁻¹

Tactic:
apply mul_lt_mul hac (by gcongr; assumption) _ hc

Premises used: mul_lt_mul
-- 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 : MulPosReflectLT G₀
a b c d : G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
⊢ 0 < b⁻¹

Tactic:
inv_pos.2 (hd.trans_le hdb)

Premises used: Iff.mpr, inv_pos, LT.lt.trans_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 : MulPosReflectLT G₀
a b c d : G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
⊢ 0 < b⁻¹

Tactic:
exact inv_pos.2 (hd.trans_le hdb)

Premises used: Iff.mpr, inv_pos, LT.lt.trans_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 : MulPosReflectLT G₀
a b c d : G₀
hac : a ≤ c
hdb : d < b
hc : 0 < c
hd : 0 < d
rw : a * b⁻¹ < c * d⁻¹
⊢ a / b < c / d

Tactic:
rw [div_eq_mul_inv, 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 : PosMulReflectLT G₀
inst_3 : MulPosReflectLT G₀
a b c d : G₀
hac : a ≤ c
hdb : d < b
hc : 0 < c
hd : 0 < d
⊢ a * b⁻¹ < c * d⁻¹

Tactic:
mul_lt_mul' hac ((inv_lt_inv₀ (hd.trans hdb) hd).2 hdb)
    (inv_nonneg.2 <| hd.le.trans hdb.le) hc

Premises used: Iff.mpr, LT.lt.le, mul_lt_mul', inv_nonneg, LT.lt.trans, LE.le.trans, inv_lt_inv₀
-- 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 : MulPosReflectLT G₀
a b c d : G₀
hac : a ≤ c
hdb : d < b
hc : 0 < c
hd : 0 < d
⊢ a * b⁻¹ < c * d⁻¹

Tactic:
exact mul_lt_mul' hac ((inv_lt_inv₀ (hd.trans hdb) hd).2 hdb)
    (inv_nonneg.2 <| hd.le.trans hdb.le) hc

Premises used: Iff.mpr, LT.lt.le, mul_lt_mul', inv_nonneg, LT.lt.trans, LE.le.trans, inv_lt_inv₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a : G₀
inst_2 : PosMulMono G₀
⊢ PosMulReflectLT G₀

Tactic:
have := PosMulMono.toPosMulReflectLT (α := G₀)
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a : G₀
inst_2 : PosMulMono G₀
this : PosMulReflectLT G₀
⊢ a⁻¹ < 0 ↔ a < 0

Tactic:
simp only [← not_le, inv_nonneg]

Premises used: not_le, inv_nonneg
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a : G₀
inst_2 : PosMulMono G₀
this : PosMulReflectLT G₀
⊢ a⁻¹ ≤ 0 ↔ a ≤ 0

Tactic:
simp only [← not_lt, inv_pos]

Premises used: inv_pos, not_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a : G₀
inst_2 : PosMulMono G₀
⊢ 1 / a < 0 ↔ a < 0

Tactic:
one_div a ▸ inv_neg''

Premises used: Eq.rec, inv_neg'', one_div, Eq.symm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a : G₀
inst_2 : PosMulMono G₀
⊢ 1 / a ≤ 0 ↔ a ≤ 0

Tactic:
one_div a ▸ inv_nonpos

Premises used: Eq.rec, one_div, inv_nonpos, Eq.symm
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a b : G₀
inst_2 : PosMulMono G₀
ha : 0 ≤ a
hb : b ≤ 0
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 : LinearOrder G₀
a b : G₀
inst_2 : PosMulMono G₀
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b⁻¹ ≤ 0

Tactic:
mul_nonpos_of_nonneg_of_nonpos ha (inv_nonpos.2 hb)

Premises used: Iff.mpr, mul_nonpos_of_nonneg_of_nonpos, inv_nonpos
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a b : G₀
inst_2 : PosMulMono G₀
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b⁻¹ ≤ 0

Tactic:
exact mul_nonpos_of_nonneg_of_nonpos ha (inv_nonpos.2 hb)

Premises used: Iff.mpr, mul_nonpos_of_nonneg_of_nonpos, inv_nonpos
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a b : G₀
inst_2 : PosMulMono G₀
h : a / b < 0
ha : 0 ≤ a
⊢ b < 0

Tactic:
have := PosMulMono.toPosMulReflectLT (α := G₀)
  lt_of_not_ge fun hb ↦ (div_nonneg ha hb).not_gt h

Premises used: lt_of_not_ge, LE.le.not_gt, PosMulMono.toPosMulReflectLT, div_nonneg
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a b : G₀
inst_2 : PosMulMono G₀
h : a / b < 0
hb : 0 ≤ b
⊢ a < 0

Tactic:
have := PosMulMono.toPosMulReflectLT (α := G₀)
  lt_of_not_ge fun ha ↦ (div_nonneg ha hb).not_gt h

Premises used: lt_of_not_ge, LE.le.not_gt, PosMulMono.toPosMulReflectLT, div_nonneg
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a : G₀
inst_2 : PosMulStrictMono G₀
inst_3 : ZeroLEOneClass G₀
simp_rw : ¬1 ≤ a⁻¹ ↔ a ≤ 0 ∨ ¬a ≤ 1
simp_rw₁ : ¬(0 < a ∧ a ≤ 1) ↔ a ≤ 0 ∨ ¬a ≤ 1
simp_rw₂ : ¬0 < a ∨ ¬a ≤ 1 ↔ a ≤ 0 ∨ ¬a ≤ 1
⊢ a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a

Tactic:
simp_rw [← not_le, one_le_inv_iff₀, not_and_or, not_lt]

Premises used: not_le, one_le_inv_iff₀, not_lt, not_and_or
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a : G₀
inst_2 : PosMulStrictMono G₀
inst_3 : ZeroLEOneClass G₀
⊢ a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a

Tactic:
simp only [← not_lt, one_lt_inv_iff₀, not_and_or]

Premises used: one_lt_inv_iff₀, not_lt, not_and_or
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a : G₀
inst_2 : PosMulStrictMono G₀
inst_3 : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a ≠ 1
inl : ∀ (ha₁ : a < 1), Injective.{1, u_3 + 1} (β := G₀) fun (n : ℤ) ↦ a ^ n
inr : ∀ (ha₁ : 1 < a), Injective.{1, u_3 + 1} (β := G₀) fun (n : ℤ) ↦ a ^ n
⊢ Injective.{1, u_3 + 1} (β := G₀) fun (n : ℤ) ↦ a ^ n

Tactic:
obtain ha₁ | ha₁ := ha₁.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a : G₀
inst_2 : PosMulStrictMono G₀
inst_3 : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁_1 : a ≠ 1
ha₁ : a < 1
⊢ Injective.{1, u_3 + 1} (β := G₀) fun (n : ℤ) ↦ a ^ n

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

Premises used: StrictAnti.injective, zpow_right_strictAnti₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a : G₀
inst_2 : PosMulStrictMono G₀
inst_3 : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁_1 : a ≠ 1
ha₁ : a < 1
⊢ Injective.{1, u_3 + 1} (β := G₀) fun (n : ℤ) ↦ a ^ n

Tactic:
exact (zpow_right_strictAnti₀ ha₀ ha₁).injective

Premises used: StrictAnti.injective, zpow_right_strictAnti₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a : G₀
inst_2 : PosMulStrictMono G₀
inst_3 : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁_1 : a ≠ 1
ha₁ : 1 < a
⊢ Injective.{1, u_3 + 1} (β := G₀) fun (n : ℤ) ↦ a ^ n

Tactic:
(zpow_right_strictMono₀ ha₁).injective

Premises used: StrictMono.injective, zpow_right_strictMono₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a : G₀
inst_2 : PosMulStrictMono G₀
inst_3 : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁_1 : a ≠ 1
ha₁ : 1 < a
⊢ Injective.{1, u_3 + 1} (β := G₀) fun (n : ℤ) ↦ a ^ n

Tactic:
exact (zpow_right_strictMono₀ ha₁).injective

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

Tactic:
(zpow_right_injective₀ ha₀ ha₁).eq_iff

Premises used: Function.Injective.eq_iff, zpow_right_injective₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a : G₀
inst_2 : PosMulStrictMono G₀
inst_3 : ZeroLEOneClass G₀
ha₀ : 0 ≤ a
ha₁ : a ≠ 1
n : ℤ
inl : ∀ (ha₀ : LE.le.{u_3} (α := G₀) 0 0) (ha₁ : Ne.{u_3 + 1} (α := G₀) 0 1), HPow.hPow (α := G₀) 0 n = 1 ↔ n = 0
inr : ∀ (ha₀ : 0 < a), a ^ n = 1 ↔ n = 0
⊢ a ^ n = 1 ↔ n = 0

Tactic:
obtain rfl | ha₀ := ha₀.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 : LinearOrder G₀
inst_2 : PosMulStrictMono G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha₀ : LE.le.{u_3} (α := G₀) 0 0
ha₁ : Ne.{u_3 + 1} (α := G₀) 0 1
⊢ HPow.hPow (α := G₀) 0 n = 1 ↔ n = 0

Tactic:
zero_zpow_eq_one₀

Premises used: zero_zpow_eq_one₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
inst_2 : PosMulStrictMono G₀
inst_3 : ZeroLEOneClass G₀
n : ℤ
ha₀ : LE.le.{u_3} (α := G₀) 0 0
ha₁ : Ne.{u_3 + 1} (α := G₀) 0 1
⊢ HPow.hPow (α := G₀) 0 n = 1 ↔ n = 0

Tactic:
exact zero_zpow_eq_one₀

Premises used: zero_zpow_eq_one₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a : G₀
inst_2 : PosMulStrictMono G₀
inst_3 : ZeroLEOneClass G₀
ha₀_1 : 0 ≤ a
ha₁ : a ≠ 1
n : ℤ
ha₀ : 0 < a
⊢ a ^ n = 1 ↔ n = 0

Tactic:
simpa using zpow_right_inj₀ ha₀ ha₁ (n := 0)

Premises used: zpow_right_inj₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a b : G₀
n : ℤ
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosMono G₀
ha : 0 ≤ a
hb : 0 ≤ b
hn : 0 < n
⊢ a ^ n ≤ b ^ n ↔ a ≤ b

Tactic:
(zpow_left_strictMonoOn₀ (G₀ := G₀) hn).le_iff_le ha hb

Premises used: zpow_left_strictMonoOn₀, StrictMonoOn.le_iff_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a b : G₀
n : ℤ
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosMono G₀
ha : 0 ≤ a
hb : 0 ≤ b
hn : 0 < n
⊢ a ^ n < b ^ n ↔ a < b

Tactic:
(zpow_left_strictMonoOn₀ (G₀ := G₀) hn).lt_iff_lt ha hb

Premises used: zpow_left_strictMonoOn₀, StrictMonoOn.lt_iff_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
inst_2 : PosMulStrictMono G₀
inst_3 : MulPosMono G₀
n : ℕ
h : Ne (α := ℤ) (↑(n + 1) : ℤ) 0
⊢ Set.InjOn (β := G₀) (fun (a : G₀) ↦ HPow.hPow (β := ℤ) a (↑(n + 1) : ℤ)) {a : G₀ | 0 ≤ a}

Tactic:
simpa using mod_cast (pow_left_strictMonoOn₀ n.succ_ne_zero).injOn

Premises used: StrictMonoOn.injOn, Nat.succ_ne_zero, pow_left_strictMonoOn₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
inst_2 : PosMulStrictMono G₀
inst_3 : MulPosMono G₀
n : ℕ
h : Int.negSucc n ≠ 0
⊢ Set.InjOn (β := G₀) (fun (a : G₀) ↦ a ^ Int.negSucc n) {a : G₀ | 0 ≤ a}

Tactic:
simpa using inv_injective.comp_injOn (pow_left_strictMonoOn₀ n.succ_ne_zero).injOn

Premises used: StrictMonoOn.injOn, Function.Injective.comp_injOn, Nat.succ_ne_zero, pow_left_strictMonoOn₀, inv_injective
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a b : G₀
n : ℤ
inst_2 : PosMulStrictMono G₀
inst_3 : MulPosMono G₀
ha : 0 ≤ a
hb : 0 ≤ b
hn : n ≠ 0
⊢ a ^ n = b ^ n ↔ a = b

Tactic:
(zpow_left_injOn₀ hn).eq_iff ha hb

Premises used: zpow_left_injOn₀, Set.InjOn.eq_iff