awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
inst_2 : ZeroLEOneClass G₀
a : G₀
inl : 0 / 0 ≤ 1
inr : ∀ (ha : a ≠ 0), a / a ≤ 1
⊢ a / a ≤ 1

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
inst_2 : ZeroLEOneClass G₀
⊢ 0 / 0 ≤ 1

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
inst_2 : ZeroLEOneClass G₀
a : G₀
ha : a ≠ 0
⊢ a / a ≤ 1

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
inst_2 : ZeroLEOneClass G₀
a : G₀
⊢ a * a⁻¹ ≤ 1

Tactic:
simpa only [div_eq_mul_inv] using div_self_le_one a

Premises used: div_self_le_one, div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
inst_2 : ZeroLEOneClass G₀
a : G₀
inl : HMul.hMul (α := G₀) 0⁻¹ 0 ≤ 1
inr : ∀ (ha : a ≠ 0), a⁻¹ * a ≤ 1
⊢ a⁻¹ * a ≤ 1

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
inst_2 : ZeroLEOneClass G₀
⊢ HMul.hMul (α := G₀) 0⁻¹ 0 ≤ 1

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
inst_2 : ZeroLEOneClass G₀
a : G₀
ha : a ≠ 0
⊢ a⁻¹ * a ≤ 1

Tactic:
simp [*]
-- 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₀
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 : PosMulReflectLT G₀
a_1 a : G₀
ha : 0 < a
apply : a * 0 < a * a⁻¹
⊢ 0 < a⁻¹

Tactic:
apply lt_of_mul_lt_mul_left _ ha.le

Premises used: lt_of_mul_lt_mul_left, 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₀
a_1 a : G₀
ha : 0 < a
apply : a * (a * 0) < a * (a * a⁻¹)
⊢ a * 0 < a * a⁻¹

Tactic:
apply lt_of_mul_lt_mul_left _ ha.le

Premises used: lt_of_mul_lt_mul_left, 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₀
a_1 a : G₀
ha : 0 < a
⊢ a * (a * 0) < 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 : PosMulReflectLT 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, inv_pos, zero_eq_inv
-- 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₀
⊢ 0 < 1 / a ↔ 0 < a

Tactic:
one_div a ▸ inv_pos

Premises used: Eq.rec, inv_pos, one_div, Eq.symm
-- 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₀
⊢ 0 ≤ 1 / a ↔ 0 ≤ a

Tactic:
one_div a ▸ inv_nonneg

Premises used: Eq.rec, inv_nonneg, one_div, Eq.symm
-- 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₀
ha : 0 < a
b c : G₀
hbc : b < c
⊢ a⁻¹ * (a * b) < a⁻¹ * (a * c)

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 : PosMulReflectLT G₀
inst_3 : MulPosMono G₀
a : G₀
ha : 0 < a
b c : G₀
h :
  LE.le.{u_3} (α := G₀)
    ((fun (x : { x : G₀ // 0 < x }) (y : G₀) ↦ y * (↑x : G₀)) (Subtype.mk (p := fun (x : G₀) ↦ 0 < x) a ha) b)
    ((fun (x : { x : G₀ // 0 < x }) (y : G₀) ↦ y * (↑x : G₀)) (Subtype.mk (p := fun (x : G₀) ↦ 0 < x) a ha) c)
⊢ b ≤ c

Tactic:
simpa [ha.ne'] using mul_le_mul_of_nonneg_right h (inv_nonneg.2 ha.le)

Premises used: Iff.mpr, LT.lt.le, LT.lt.ne', mul_le_mul_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 : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
rw : 0 < a * b⁻¹
⊢ 0 < a / b

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 : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b⁻¹

Tactic:
mul_pos ha (inv_pos.2 hb)

Premises used: Iff.mpr, inv_pos, mul_pos
-- 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₀
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b⁻¹

Tactic:
exact mul_pos ha (inv_pos.2 hb)

Premises used: Iff.mpr, inv_pos, mul_pos
-- 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₀
ha : 0 ≤ a
hb : 0 ≤ b
rw : 0 ≤ a * b⁻¹
⊢ 0 ≤ a / b

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 : PosMulReflectLT G₀
a b : G₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b⁻¹

Tactic:
mul_nonneg ha (inv_nonneg.2 hb)

Premises used: Iff.mpr, mul_nonneg, inv_nonneg
-- 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₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b⁻¹

Tactic:
exact mul_nonneg ha (inv_nonneg.2 hb)

Premises used: Iff.mpr, mul_nonneg, inv_nonneg
-- 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 c : G₀
hc : 0 < c
rw : c * a ≤ c * (c⁻¹ * b) ↔ c * a ≤ b
rw₁ rw₂ : c * a ≤ b ↔ c * a ≤ b
⊢ a ≤ c⁻¹ * b ↔ c * a ≤ b

Tactic:
rw [← mul_le_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ hc.ne']

Premises used: mul_inv_cancel_left₀, mul_le_mul_iff_of_pos_left, 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 b c : G₀
hc : 0 < c
rw : c * (c⁻¹ * b) ≤ c * a ↔ b ≤ c * a
rw₁ rw₂ : b ≤ c * a ↔ b ≤ c * a
⊢ c⁻¹ * b ≤ a ↔ b ≤ c * a

Tactic:
rw [← mul_le_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ hc.ne']

Premises used: mul_inv_cancel_left₀, mul_le_mul_iff_of_pos_left, 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 b : G₀
ha : 0 < a
rw : a * 1 ≤ b ↔ a ≤ b
rw₁ rw₂ : a ≤ b ↔ a ≤ b
⊢ 1 ≤ a⁻¹ * b ↔ a ≤ b

Tactic:
rw [le_inv_mul_iff₀ ha, mul_one]

Premises used: le_inv_mul_iff₀, mul_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 b : G₀
ha : 0 < a
rw : b ≤ a * 1 ↔ b ≤ a
rw₁ rw₂ : b ≤ a ↔ b ≤ a
⊢ a⁻¹ * b ≤ 1 ↔ b ≤ a

Tactic:
rw [inv_mul_le_iff₀ ha, mul_one]

Premises used: inv_mul_le_iff₀, mul_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 b : G₀
ha : 0 < a
rw : a⁻¹ ≤ b ↔ a⁻¹ * 1 ≤ b
rw₁ rw₂ : a⁻¹ ≤ b ↔ a⁻¹ ≤ b
⊢ a⁻¹ ≤ b ↔ 1 ≤ a * b

Tactic:
rw [← inv_mul_le_iff₀ ha, mul_one]

Premises used: inv_mul_le_iff₀, mul_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₀
ha : 0 < a
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1

Tactic:
simpa using one_le_inv_mul₀ ha (b := 1)

Premises used: one_le_inv_mul₀
-- 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₀
ha : 0 < a
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a

Tactic:
simpa using inv_mul_le_one₀ ha (b := 1)

Premises used: inv_mul_le_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 b c : G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c⁻¹ * b
inl : ∀ (hc : LE.le.{u_3} (α := G₀) 0 0) (h : a ≤ 0⁻¹ * b), 0 * a ≤ b
inr : ∀ (hc : 0 < c), c * a ≤ b
⊢ c * a ≤ 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 : PosMulReflectLT G₀
a b : G₀
hb : 0 ≤ b
hc : LE.le.{u_3} (α := G₀) 0 0
h : a ≤ 0⁻¹ * b
⊢ 0 * a ≤ 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 : PosMulReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc_1 : 0 ≤ c
h : a ≤ c⁻¹ * b
hc : 0 < c
inr inr₁ inr₂ inr₃ : ∀ (h : c * a ≤ b) (hc : 0 < c), c * a ≤ b
⊢ c * a ≤ b

Tactic:
rwa [le_inv_mul_iff₀ hc] at h

Premises used: le_inv_mul_iff₀
-- 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 c : G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b * c
inl : ∀ (hb : LE.le.{u_3} (α := G₀) 0 0) (h : a ≤ 0 * c), 0⁻¹ * a ≤ c
inr : ∀ (hb : 0 < b), b⁻¹ * a ≤ c
⊢ b⁻¹ * a ≤ 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 : PosMulReflectLT G₀
a c : G₀
hc : 0 ≤ c
hb : LE.le.{u_3} (α := G₀) 0 0
h : a ≤ 0 * c
⊢ 0⁻¹ * a ≤ 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 : PosMulReflectLT G₀
a b c : G₀
hb_1 : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b * c
hb : 0 < b
inr inr₁ inr₂ inr₃ : a ≤ b * c
⊢ b⁻¹ * a ≤ c

Tactic:
rwa [inv_mul_le_iff₀ hb]

Premises used: inv_mul_le_iff₀
-- 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 c : G₀
hc : 0 < c
rw : c * a < c * (c⁻¹ * b) ↔ c * a < b
rw₁ rw₂ : c * a < b ↔ c * a < b
⊢ a < c⁻¹ * b ↔ c * a < b

Tactic:
rw [← mul_lt_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ hc.ne']

Premises used: mul_inv_cancel_left₀, mul_lt_mul_iff_of_pos_left, 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 b c : G₀
hc : 0 < c
rw : c * (c⁻¹ * b) < c * a ↔ b < c * a
rw₁ rw₂ : b < c * a ↔ b < c * a
⊢ c⁻¹ * b < a ↔ b < c * a

Tactic:
rw [← mul_lt_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ hc.ne']

Premises used: mul_inv_cancel_left₀, mul_lt_mul_iff_of_pos_left, 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 b : G₀
ha : 0 < a
rw : a⁻¹ < b ↔ a⁻¹ * 1 < b
rw₁ rw₂ : a⁻¹ < b ↔ a⁻¹ < b
⊢ a⁻¹ < b ↔ 1 < a * b

Tactic:
rw [← inv_mul_lt_iff₀ ha, mul_one]

Premises used: inv_mul_lt_iff₀, mul_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 b : G₀
ha : 0 < a
rw : a * 1 < b ↔ a < b
rw₁ rw₂ : a < b ↔ a < b
⊢ 1 < a⁻¹ * b ↔ a < b

Tactic:
rw [lt_inv_mul_iff₀ ha, mul_one]

Premises used: lt_inv_mul_iff₀, mul_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 b : G₀
ha : 0 < a
rw : b < a * 1 ↔ b < a
rw₁ rw₂ : b < a ↔ b < a
⊢ a⁻¹ * b < 1 ↔ b < a

Tactic:
rw [inv_mul_lt_iff₀ ha, mul_one]

Premises used: inv_mul_lt_iff₀, mul_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₀
ha : 0 < a
⊢ 1 < a⁻¹ ↔ a < 1

Tactic:
simpa using one_lt_inv_mul₀ ha (b := 1)

Premises used: one_lt_inv_mul₀
-- 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₀
ha : 0 < a
⊢ a⁻¹ < 1 ↔ 1 < a

Tactic:
simpa using inv_mul_lt_one₀ ha (b := 1)

Premises used: inv_mul_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₀
ha : 1 < a
⊢ a⁻¹ < 1

Tactic:
(inv_lt_one₀ <| zero_lt_one.trans ha).2 ha

Premises used: Iff.mpr, inv_lt_one₀, zero_lt_one, 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₀
a : G₀
inst_3 : ZeroLEOneClass G₀
ha : 1 ≤ a
⊢ a⁻¹ ≤ 1

Tactic:
(inv_le_one₀ <| zero_lt_one.trans_le ha).2 ha

Premises used: Iff.mpr, zero_lt_one, LT.lt.trans_le, inv_le_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 b : G₀
inst_3 : ZeroLEOneClass G₀
h : a ≤ b
hb : 0 ≤ b
rwa rwa₁ rwa₂ rwa₃ : a ≤ b
⊢ a ≤ b * 1

Tactic:
rwa [mul_one]

Premises used: mul_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₀
ha : 0 ≤ a
n : ℕ
rw : 0 ≤ a ^ n
⊢ 0 ≤ HPow.hPow (β := ℤ) a (↑n : ℤ)

Tactic:
rw [zpow_natCast]

Premises used: zpow_natCast
-- 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
n : ℕ
⊢ 0 ≤ a ^ n

Tactic:
pow_nonneg ha _

Premises used: pow_nonneg
-- 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
n : ℕ
⊢ 0 ≤ a ^ n

Tactic:
exact pow_nonneg ha _

Premises used: pow_nonneg
-- 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
n : ℕ
rw : 0 ≤ a ^ (n + 1)
⊢ 0 ≤ HPow.hPow (β := ℤ) a (-(↑(n + 1) : ℤ))

Tactic:
rw [zpow_neg, inv_nonneg, zpow_natCast]

Premises used: zpow_natCast, inv_nonneg, zpow_neg
-- 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
n : ℕ
⊢ 0 ≤ a ^ (n + 1)

Tactic:
pow_nonneg ha _

Premises used: pow_nonneg
-- 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
n : ℕ
⊢ 0 ≤ a ^ (n + 1)

Tactic:
exact pow_nonneg ha _

Premises used: pow_nonneg
-- 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
n : ℕ
rw : 0 < a ^ n
⊢ 0 < HPow.hPow (β := ℤ) a (↑n : ℤ)

Tactic:
rw [zpow_natCast]

Premises used: zpow_natCast
-- 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
n : ℕ
⊢ 0 < a ^ n

Tactic:
pow_pos ha _

Premises used: pow_pos
-- 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
n : ℕ
⊢ 0 < a ^ n

Tactic:
exact pow_pos ha _

Premises used: pow_pos
-- 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
n : ℕ
rw : 0 < a ^ (n + 1)
⊢ 0 < HPow.hPow (β := ℤ) a (-(↑(n + 1) : ℤ))

Tactic:
rw [zpow_neg, inv_pos, zpow_natCast]

Premises used: zpow_natCast, inv_pos, zpow_neg
-- 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
n : ℕ
⊢ 0 < a ^ (n + 1)

Tactic:
pow_pos ha _

Premises used: pow_pos
-- 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
n : ℕ
⊢ 0 < a ^ (n + 1)

Tactic:
exact pow_pos ha _

Premises used: pow_pos
-- 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 : 1 ≤ a
⊢ Monotone.{0, u_3} (β := G₀) fun (n : ℤ) ↦ a ^ n

Tactic:
monotone_int_of_le_succ fun n ↦ ?_

Premises used: monotone_int_of_le_succ
-- 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 : 1 ≤ a
refine : ∀ (n : ℤ), a ^ n ≤ a ^ (n + 1)
⊢ Monotone.{0, u_3} (β := G₀) fun (n : ℤ) ↦ a ^ n

Tactic:
refine monotone_int_of_le_succ fun n ↦ ?_

Premises used: monotone_int_of_le_succ
-- 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 : 1 ≤ a
n : ℤ
rw : a ^ n ≤ a ^ n * a
⊢ a ^ n ≤ a ^ (n + 1)

Tactic:
rw [zpow_add_one₀ (zero_lt_one.trans_le ha).ne']

Premises used: zpow_add_one₀, LT.lt.ne', zero_lt_one, 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₀
a : G₀
inst_3 : ZeroLEOneClass G₀
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ n * a

Tactic:
le_mul_of_one_le_right (zpow_nonneg (zero_le_one.trans ha) _) ha

Premises used: zpow_nonneg, zero_le_one, le_mul_of_one_le_right, 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₀
a : G₀
inst_3 : ZeroLEOneClass G₀
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ n * a

Tactic:
exact le_mul_of_one_le_right (zpow_nonneg (zero_le_one.trans ha) _) ha

Premises used: zpow_nonneg, zero_le_one, le_mul_of_one_le_right, 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₀
a : G₀
inst_3 : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a ≤ 1
⊢ Antitone.{0, u_3} (β := G₀) fun (n : ℤ) ↦ a ^ n

Tactic:
antitone_int_of_succ_le fun n ↦ ?_

Premises used: antitone_int_of_succ_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₀
ha₀ : 0 < a
ha₁ : a ≤ 1
refine : ∀ (n : ℤ), a ^ (n + 1) ≤ a ^ n
⊢ Antitone.{0, u_3} (β := G₀) fun (n : ℤ) ↦ a ^ n

Tactic:
refine antitone_int_of_succ_le fun n ↦ ?_

Premises used: antitone_int_of_succ_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₀
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_le_of_le_one_right (zpow_nonneg ha₀.le _) ha₁

Premises used: mul_le_of_le_one_right, LT.lt.le, zpow_nonneg
-- 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_le_of_le_one_right (zpow_nonneg ha₀.le _) ha₁

Premises used: mul_le_of_le_one_right, LT.lt.le, zpow_nonneg
-- 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 : 1 < a
⊢ StrictMono.{0, u_3} (β := G₀) fun (n : ℤ) ↦ a ^ n

Tactic:
strictMono_int_of_lt_succ fun n ↦ ?_

Premises used: strictMono_int_of_lt_succ
-- 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 : 1 < a
refine : ∀ (n : ℤ), a ^ n < a ^ (n + 1)
⊢ StrictMono.{0, u_3} (β := G₀) fun (n : ℤ) ↦ a ^ n

Tactic:
refine strictMono_int_of_lt_succ fun n ↦ ?_

Premises used: strictMono_int_of_lt_succ
-- 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 : 1 < a
n : ℤ
rw : a ^ n < a ^ n * a
⊢ a ^ n < a ^ (n + 1)

Tactic:
rw [zpow_add_one₀ (zero_lt_one.trans ha).ne']

Premises used: zpow_add_one₀, LT.lt.ne', zero_lt_one, 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₀
a : G₀
inst_3 : ZeroLEOneClass G₀
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ n * a

Tactic:
lt_mul_of_one_lt_right (zpow_pos (zero_lt_one.trans ha) _) ha

Premises used: zpow_pos, zero_lt_one, LT.lt.trans, lt_mul_of_one_lt_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 : 1 < a
n : ℤ
⊢ a ^ n < a ^ n * a

Tactic:
exact lt_mul_of_one_lt_right (zpow_pos (zero_lt_one.trans ha) _) ha

Premises used: zpow_pos, zero_lt_one, LT.lt.trans, lt_mul_of_one_lt_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
⊢ StrictAnti.{0, u_3} (β := G₀) fun (n : ℤ) ↦ a ^ n

Tactic:
strictAnti_int_of_succ_lt fun n ↦ ?_

Premises used: strictAnti_int_of_succ_lt
-- 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
refine : ∀ (n : ℤ), a ^ (n + 1) < a ^ n
⊢ StrictAnti.{0, u_3} (β := G₀) fun (n : ℤ) ↦ a ^ n

Tactic:
refine strictAnti_int_of_succ_lt fun n ↦ ?_

Premises used: strictAnti_int_of_succ_lt