awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a b c : α
rw : a * b ≤ c / b * b ↔ a * b ≤ c
rw₁ : a * b ≤ c * b⁻¹ * b ↔ a * b ≤ c
⊢ a ≤ c / b ↔ a * b ≤ c
have rw₂ : a * b ≤ c ↔ a * b ≤ c
Tactic: rw [← mul_le_mul_iff_right b, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a b c : α
⊢ a / c ≤ b ↔ a ≤ b * c
have rw : a / c * c ≤ b * c ↔ a ≤ b * c
Tactic: rw [← mul_le_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a b c : α
rw : a / c * c ≤ b * c ↔ a ≤ b * c
⊢ a / c ≤ b ↔ a ≤ b * c
have rw₁ : a * c⁻¹ * c ≤ b * c ↔ a ≤ b * c
Tactic: rw [← mul_le_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a b c : α
rw : a / c * c ≤ b * c ↔ a ≤ b * c
rw₁ : a * c⁻¹ * c ≤ b * c ↔ a ≤ b * c
⊢ a / c ≤ b ↔ a ≤ b * c
have rw₂ : a ≤ b * c ↔ a ≤ b * c
Tactic: rw [← mul_le_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
b c a : α
⊢ a / b ≤ a / c ↔ c ≤ b
have rw : a * b⁻¹ ≤ a / c ↔ c ≤ b
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_le_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_le_inv_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
b c a : α
rw : a * b⁻¹ ≤ a / c ↔ c ≤ b
⊢ a / b ≤ a / c ↔ c ≤ b
have rw₁ : a * b⁻¹ ≤ a * c⁻¹ ↔ c ≤ b
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_le_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_le_inv_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
b c a : α
rw : a * b⁻¹ ≤ a / c ↔ c ≤ b
rw₁ : a * b⁻¹ ≤ a * c⁻¹ ↔ c ≤ b
⊢ a / b ≤ a / c ↔ c ≤ b
have rw₂ : a⁻¹ * (a * b⁻¹) ≤ a⁻¹ * (a * c⁻¹) ↔ c ≤ b
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_le_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_le_inv_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
b c a : α
rw : a * b⁻¹ ≤ a / c ↔ c ≤ b
rw₁ : a * b⁻¹ ≤ a * c⁻¹ ↔ c ≤ b
rw₂ : a⁻¹ * (a * b⁻¹) ≤ a⁻¹ * (a * c⁻¹) ↔ c ≤ b
⊢ a / b ≤ a / c ↔ c ≤ b
have rw₃ : b⁻¹ ≤ a⁻¹ * (a * c⁻¹) ↔ c ≤ b
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_le_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_le_inv_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
b c a : α
rw : a * b⁻¹ ≤ a / c ↔ c ≤ b
rw₁ : a * b⁻¹ ≤ a * c⁻¹ ↔ c ≤ b
rw₂ : a⁻¹ * (a * b⁻¹) ≤ a⁻¹ * (a * c⁻¹) ↔ c ≤ b
rw₃ : b⁻¹ ≤ a⁻¹ * (a * c⁻¹) ↔ c ≤ b
⊢ a / b ≤ a / c ↔ c ≤ b
have rw₄ : b⁻¹ ≤ c⁻¹ ↔ c ≤ b
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_le_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_le_inv_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
b c a : α
rw : a * b⁻¹ ≤ a / c ↔ c ≤ b
rw₁ : a * b⁻¹ ≤ a * c⁻¹ ↔ c ≤ b
rw₂ : a⁻¹ * (a * b⁻¹) ≤ a⁻¹ * (a * c⁻¹) ↔ c ≤ b
rw₃ : b⁻¹ ≤ a⁻¹ * (a * c⁻¹) ↔ c ≤ b
rw₄ : b⁻¹ ≤ c⁻¹ ↔ c ≤ b
⊢ a / b ≤ a / c ↔ c ≤ b
have rw₅ : c ≤ b ↔ c ≤ b
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_le_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_le_inv_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
⊢ b ≤ c / a ↔ a * b ≤ c
have rw : b * a ≤ c ↔ a * b ≤ c
Tactic: rw [le_div_iff_mul_le, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
rw : b * a ≤ c ↔ a * b ≤ c
⊢ b ≤ c / a ↔ a * b ≤ c
have rw₁ : a * b ≤ c ↔ a * b ≤ c
Tactic: rw [le_div_iff_mul_le, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
⊢ a / b ≤ c ↔ a ≤ b * c
have rw : a ≤ c * b ↔ a ≤ b * c
Tactic: rw [div_le_iff_le_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
rw : a ≤ c * b ↔ a ≤ b * c
⊢ a / b ≤ c ↔ a ≤ b * c
have rw₁ : a ≤ b * c ↔ a ≤ b * c
Tactic: rw [div_le_iff_le_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
⊢ a⁻¹ ≤ b / c ↔ c ≤ a * b
have rw : c ≤ b * a ↔ c ≤ a * b
Tactic: rw [inv_le_div_iff_le_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
rw : c ≤ b * a ↔ c ≤ a * b
⊢ a⁻¹ ≤ b / c ↔ c ≤ a * b
have rw₁ : c ≤ a * b ↔ c ≤ a * b
Tactic: rw [inv_le_div_iff_le_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a / d ≤ b / c
have rw : a * c ≤ b * d
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_le_inv_mul_iff, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b : α
⊢ 1 < a / b ↔ b < a
have rw : 1 * b < a / b * b ↔ b < a
Tactic: rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b : α
rw : 1 * b < a / b * b ↔ b < a
⊢ 1 < a / b ↔ b < a
have rw₁ : b < a / b * b ↔ b < a
Tactic: rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b : α
rw : 1 * b < a / b * b ↔ b < a
rw₁ : b < a / b * b ↔ b < a
⊢ 1 < a / b ↔ b < a
have rw₂ : b < a * b⁻¹ * b ↔ b < a
Tactic: rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b : α
rw : 1 * b < a / b * b ↔ b < a
rw₁ : b < a / b * b ↔ b < a
rw₂ : b < a * b⁻¹ * b ↔ b < a
⊢ 1 < a / b ↔ b < a
have rw₃ : b < a ↔ b < a
Tactic: rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b : α
⊢ a / b < 1 ↔ a < b
have rw : a / b * b < 1 * b ↔ a < b
Tactic: rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b : α
rw : a / b * b < 1 * b ↔ a < b
⊢ a / b < 1 ↔ a < b
have rw₁ : a / b * b < b ↔ a < b
Tactic: rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b : α
rw : a / b * b < 1 * b ↔ a < b
rw₁ : a / b * b < b ↔ a < b
⊢ a / b < 1 ↔ a < b
have rw₂ : a * b⁻¹ * b < b ↔ a < b
Tactic: rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b : α
rw : a / b * b < 1 * b ↔ a < b
rw₁ : a / b * b < b ↔ a < b
rw₂ : a * b⁻¹ * b < b ↔ a < b
⊢ a / b < 1 ↔ a < b
have rw₃ : a < b ↔ a < b
Tactic: rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b c : α
⊢ a < c / b ↔ a * b < c
have rw : a * b < c / b * b ↔ a * b < c
Tactic: rw [← mul_lt_mul_iff_right b, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b c : α
rw : a * b < c / b * b ↔ a * b < c
⊢ a < c / b ↔ a * b < c
have rw₁ : a * b < c * b⁻¹ * b ↔ a * b < c
Tactic: rw [← mul_lt_mul_iff_right b, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b c : α
rw : a * b < c / b * b ↔ a * b < c
rw₁ : a * b < c * b⁻¹ * b ↔ a * b < c
⊢ a < c / b ↔ a * b < c
have rw₂ : a * b < c ↔ a * b < c
Tactic: rw [← mul_lt_mul_iff_right b, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b c : α
⊢ a / c < b ↔ a < b * c
have rw : a / c * c < b * c ↔ a < b * c
Tactic: rw [← mul_lt_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b c : α
rw : a / c * c < b * c ↔ a < b * c
⊢ a / c < b ↔ a < b * c
have rw₁ : a * c⁻¹ * c < b * c ↔ a < b * c
Tactic: rw [← mul_lt_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b c : α
rw : a / c * c < b * c ↔ a < b * c
rw₁ : a * c⁻¹ * c < b * c ↔ a < b * c
⊢ a / c < b ↔ a < b * c
have rw₂ : a < b * c ↔ a < b * c
Tactic: rw [← mul_lt_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
b c a : α
⊢ a / b < a / c ↔ c < b
have rw : a * b⁻¹ < a / c ↔ c < b
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_lt_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_lt_inv_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
b c a : α
rw : a * b⁻¹ < a / c ↔ c < b
⊢ a / b < a / c ↔ c < b
have rw₁ : a * b⁻¹ < a * c⁻¹ ↔ c < b
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_lt_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_lt_inv_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
b c a : α
rw : a * b⁻¹ < a / c ↔ c < b
rw₁ : a * b⁻¹ < a * c⁻¹ ↔ c < b
⊢ a / b < a / c ↔ c < b
have rw₂ : a⁻¹ * (a * b⁻¹) < a⁻¹ * (a * c⁻¹) ↔ c < b
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_lt_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_lt_inv_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
b c a : α
rw : a * b⁻¹ < a / c ↔ c < b
rw₁ : a * b⁻¹ < a * c⁻¹ ↔ c < b
rw₂ : a⁻¹ * (a * b⁻¹) < a⁻¹ * (a * c⁻¹) ↔ c < b
⊢ a / b < a / c ↔ c < b
have rw₃ : b⁻¹ < a⁻¹ * (a * c⁻¹) ↔ c < b
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_lt_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_lt_inv_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
b c a : α
rw : a * b⁻¹ < a / c ↔ c < b
rw₁ : a * b⁻¹ < a * c⁻¹ ↔ c < b
rw₂ : a⁻¹ * (a * b⁻¹) < a⁻¹ * (a * c⁻¹) ↔ c < b
rw₃ : b⁻¹ < a⁻¹ * (a * c⁻¹) ↔ c < b
⊢ a / b < a / c ↔ c < b
have rw₄ : b⁻¹ < c⁻¹ ↔ c < b
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_lt_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_lt_inv_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
b c a : α
rw : a * b⁻¹ < a / c ↔ c < b
rw₁ : a * b⁻¹ < a * c⁻¹ ↔ c < b
rw₂ : a⁻¹ * (a * b⁻¹) < a⁻¹ * (a * c⁻¹) ↔ c < b
rw₃ : b⁻¹ < a⁻¹ * (a * c⁻¹) ↔ c < b
rw₄ : b⁻¹ < c⁻¹ ↔ c < b
⊢ a / b < a / c ↔ c < b
have rw₅ : c < b ↔ c < b
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_lt_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_lt_inv_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c : α
⊢ a⁻¹ < b / c ↔ c < a * b
have rw : a⁻¹ < b * c⁻¹ ↔ c < a * b
Tactic: rw [div_eq_mul_inv, lt_mul_inv_iff_mul_lt, inv_mul_lt_iff_lt_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c : α
rw : a⁻¹ < b * c⁻¹ ↔ c < a * b
⊢ a⁻¹ < b / c ↔ c < a * b
have rw₁ : a⁻¹ * c < b ↔ c < a * b
Tactic: rw [div_eq_mul_inv, lt_mul_inv_iff_mul_lt, inv_mul_lt_iff_lt_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c : α
rw : a⁻¹ < b * c⁻¹ ↔ c < a * b
rw₁ : a⁻¹ * c < b ↔ c < a * b
⊢ a⁻¹ < b / c ↔ c < a * b
have rw₂ : c < a * b ↔ c < a * b
Tactic: rw [div_eq_mul_inv, lt_mul_inv_iff_mul_lt, inv_mul_lt_iff_lt_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b c : α
⊢ b < c / a ↔ a * b < c
have rw : b * a < c ↔ a * b < c
Tactic: rw [lt_div_iff_mul_lt, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b c : α
rw : b * a < c ↔ a * b < c
⊢ b < c / a ↔ a * b < c
have rw₁ : a * b < c ↔ a * b < c
Tactic: rw [lt_div_iff_mul_lt, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b c : α
⊢ a / b < c ↔ a < b * c
have rw : a < c * b ↔ a < b * c
Tactic: rw [div_lt_iff_lt_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b c : α
rw : a < c * b ↔ a < b * c
⊢ a / b < c ↔ a < b * c
have rw₁ : a < b * c ↔ a < b * c
Tactic: rw [div_lt_iff_lt_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ a / d < b / c
have rw : a * c < b * d
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_lt_inv_mul_iff, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b c d : α
⊢ a / d < b / c → a < b ∨ c < d
have contrapose! : b ≤ a ∧ d ≤ c → b / c ≤ a / d
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulRightMono α
a b : α
⊢ cmp (a / b) 1 = cmp a b
have rw : cmp (a / b * b) (1 * b) = cmp a b
Tactic: rw [← cmp_mul_right' _ _ b, one_mul, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulRightMono α
a b : α
rw : cmp (a / b * b) (1 * b) = cmp a b
⊢ cmp (a / b) 1 = cmp a b
have rw₁ : cmp (a / b * b) b = cmp a b
Tactic: rw [← cmp_mul_right' _ _ b, one_mul, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulRightMono α
a b : α
rw : cmp (a / b * b) (1 * b) = cmp a b
rw₁ : cmp (a / b * b) b = cmp a b
⊢ cmp (a / b) 1 = cmp a b
have rw₂ : cmp a b = cmp a b
Tactic: rw [← cmp_mul_right' _ _ b, one_mul, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b : α
inst_3 : MulRightMono α
⊢ a / b ≤ a⁻¹ * b ↔ a ≤ b
have rw : a * a ≤ b * b ↔ a ≤ b
Tactic: rw [div_eq_mul_inv, mul_inv_le_inv_mul_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b : α
⊢ a / b ≤ b / a ↔ a ≤ b
have rw : a / b ≤ a⁻¹ * b ↔ a ≤ b
Tactic: rw [div_eq_mul_inv b, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (goal)
Goal:
a : ℤ
⊢ a.sign * |a| = a
have rw : a.sign * (↑a.natAbs : ℤ) = a
Tactic: rw [abs_eq_natAbs, sign_mul_natAbs a]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (goal)
Goal:
a : ℤ
rw : a.sign * (↑a.natAbs : ℤ) = a
⊢ a.sign * |a| = a
have rw₁ : a = a
Tactic: rw [abs_eq_natAbs, sign_mul_natAbs a]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (goal)
Goal:
a : ℤ
⊢ a.sign * a = |a|
have rw : a.sign * a = (↑a.natAbs : ℤ)
Tactic: rw [abs_eq_natAbs, sign_mul_self_eq_natAbs]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (goal)
Goal:
a : ℤ
rw : a.sign * a = (↑a.natAbs : ℤ)
⊢ a.sign * a = |a|
have rw₁ : Eq (α := ℤ) (↑a.natAbs : ℤ) (↑a.natAbs : ℤ)
Tactic: rw [abs_eq_natAbs, sign_mul_self_eq_natAbs]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (goal)
Goal:
a : ℤ
⊢ (↑a.natAbs : ℤ) ≤ HPow.hPow (β := ℕ) a 2
have rw : (↑a.natAbs : ℤ) ≤ HMul.hMul (α := ℤ) (↑a.natAbs : ℤ) (↑a.natAbs : ℤ)
Tactic: rw [← Int.natAbs_sq a, sq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (goal)
Goal:
a : ℤ
⊢ (↑a.natAbs : ℤ) ≤ HMul.hMul (α := ℤ) (↑a.natAbs : ℤ) (↑a.natAbs : ℤ)
have norm_cast : a.natAbs ≤ a.natAbs * a.natAbs
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (goal)
Goal:
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
⊢ x = 0
have by_contra : ∀ (h : ¬x = 0), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (hypothesis)
Goal:
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
h : ¬x = 0
⊢ False
have this : m.natAbs ≤ x.natAbs
Tactic: have := Int.natAbs_le_of_dvd_ne_zero h1 h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (hypothesis)
Goal:
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
h : ¬x = 0
this : m.natAbs ≤ x.natAbs
⊢ False
have h2₁ : (↑x.natAbs : ℤ) < m
Tactic: rw [Int.abs_eq_natAbs] at h2
Cleared hypotheses: h2, h, this
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (goal)
Goal:
a b : ℤ
H1 : 0 ≤ a
H2_1 : a < |b|
n : ℕ
H2 : a < (↑-[n+1].natAbs : ℤ)
⊢ -(a / -[n+1]) = -0
have rw : a / - -[n+1] = -0
Tactic: rw [← Int.ediv_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (goal)
Goal:
a b : ℤ
H : b ≠ 0
⊢ a % b < |b|
have rw : a % |b| < |b|
Tactic: rw [← emod_abs]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (goal)
Goal:
a : ℤ
n : ℕ
⊢ |a / (↑n : ℤ)| ≤ |a|
have rw : LE.le (α := ℤ) (↑(a / (↑n : ℤ)).natAbs : ℤ) (↑a.natAbs : ℤ)
Tactic: rw [abs_eq_natAbs, abs_eq_natAbs]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (goal)
Goal:
this : ∀ (a : ℤ) (n : ℕ), |a / (↑n : ℤ)| ≤ |a|
a b : ℤ
n : ℕ
⊢ |a / -(↑n : ℤ)| ≤ |a|
have rw : |a / (↑n : ℤ)| ≤ |a|
Tactic: rw [Int.ediv_neg, abs_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (goal)
Goal:
z : ℤ
hz : z ≠ 0
⊢ |z.sign| = 1
have rw : Eq (α := ℤ) (↑z.sign.natAbs : ℤ) 1
Tactic: rw [abs_eq_natAbs, natAbs_sign_of_ne_zero hz, Int.ofNat_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (goal)
Goal:
z : ℤ
hz : z ≠ 0
rw : Eq (α := ℤ) (↑z.sign.natAbs : ℤ) 1
⊢ |z.sign| = 1
have rw₁ : Eq (α := ℤ) (↑1 : ℤ) 1
Tactic: rw [abs_eq_natAbs, natAbs_sign_of_ne_zero hz, Int.ofNat_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (goal)
Goal:
z : ℤ
hz : z ≠ 0
rw : Eq (α := ℤ) (↑z.sign.natAbs : ℤ) 1
rw₁ : Eq (α := ℤ) (↑1 : ℤ) 1
⊢ |z.sign| = 1
have rw₂ : Eq (α := ℤ) 1 1
Tactic: rw [abs_eq_natAbs, natAbs_sign_of_ne_zero hz, Int.ofNat_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (goal)
Goal:
G : Type u_1
inst : Group G
a : G
n : ℤ
⊢ a ^ |n| = 1 ↔ a ^ n = 1
have rw : HPow.hPow (β := ℤ) a (↑n.natAbs : ℤ) = 1 ↔ a ^ n = 1
Tactic: rw [← Int.natCast_natAbs, zpow_natCast, pow_natAbs_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (goal)
Goal:
G : Type u_1
inst : Group G
a : G
n : ℤ
rw : HPow.hPow (β := ℤ) a (↑n.natAbs : ℤ) = 1 ↔ a ^ n = 1
⊢ a ^ |n| = 1 ↔ a ^ n = 1
have rw₁ : a ^ n.natAbs = 1 ↔ a ^ n = 1
Tactic: rw [← Int.natCast_natAbs, zpow_natCast, pow_natAbs_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Int (goal)
Goal:
G : Type u_1
inst : Group G
a : G
n : ℤ
rw : HPow.hPow (β := ℤ) a (↑n.natAbs : ℤ) = 1 ↔ a ^ n = 1
rw₁ : a ^ n.natAbs = 1 ↔ a ^ n = 1
⊢ a ^ |n| = 1 ↔ a ^ n = 1
have rw₂ : a ^ n = 1 ↔ a ^ n = 1
Tactic: rw [← Int.natCast_natAbs, zpow_natCast, pow_natAbs_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Bounds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
inst_1 : Preorder β
inst_2 : Zero β
inst_3 : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x : β | 0 ≤ x}
hg' : BddAbove (g '' range f)
⊢ BddAbove.{u_3} (α := γ) (range fun (x : α) ↦ g (f x))
have rwa : BddAbove (range (g ∘ f))
Tactic: rwa [← Function.comp_def, Set.range_comp]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Bounds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
inst_1 : Preorder β
inst_2 : Zero β
inst_3 : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x : β | 0 ≤ x}
⊢ BddAbove.{u_3} (α := γ) (range fun (x : α) ↦ g (f x))
have suffices : BddAbove (g '' range f)
Tactic: suffices hg' : BddAbove (g '' range f) by
    rwa [← Function.comp_def, Set.range_comp]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Bounds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
inst_1 : Preorder β
inst_2 : Zero β
inst_3 : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x : β | 0 ≤ x}
⊢ BddAbove (g '' range f)
have apply : (upperBounds (range f) ∩ {x : β | 0 ≤ x}).Nonempty
Tactic: apply hg.map_bddAbove (by rintro x ⟨a, rfl⟩; exact hf0 a)
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Bounds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
inst_1 : Preorder β
inst_2 : Zero β
inst_3 : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x : β | 0 ≤ x}
⊢ (upperBounds (range f) ∩ {x : β | 0 ≤ x}).Nonempty
have obtain : ∀ (b : β) (hb : b ∈ upperBounds (range f)), (upperBounds (range f) ∩ {x : β | 0 ≤ x}).Nonempty
Tactic: obtain ⟨b, hb⟩ := hf
Cleared hypotheses: hf