awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a⁻¹ * b < 1 ↔ b < a
have rw₁ : b < a ↔ b < a
Tactic: rw [inv_mul_lt_iff₀ ha, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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 ≤ HPow.hPow (β := ℤ) a (↑n : ℤ)
have rw : 0 ≤ a ^ n
Tactic: rw [zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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 ≤ HPow.hPow (β := ℤ) a (-(↑(n + 1) : ℤ))
have rw : 0 ≤ a ^ (n + 1)
Tactic: rw [zpow_neg, inv_nonneg, zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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 < HPow.hPow (β := ℤ) a (↑n : ℤ)
have rw : 0 < a ^ n
Tactic: rw [zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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 < HPow.hPow (β := ℤ) a (-(↑(n + 1) : ℤ))
have rw : 0 < a ^ (n + 1)
Tactic: rw [zpow_neg, inv_pos, zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
have refine : ∀ (n : ℤ), a ^ n ≤ a ^ (n + 1)
Tactic: refine monotone_int_of_le_succ fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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 + 1)
have rw : a ^ n ≤ a ^ n * a
Tactic: rw [zpow_add_one₀ (zero_lt_one.trans_le ha).ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
have refine : ∀ (n : ℤ), a ^ (n + 1) ≤ a ^ n
Tactic: refine antitone_int_of_succ_le fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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 + 1) ≤ a ^ n
have rw : a ^ n * a ≤ a ^ n
Tactic: rw [zpow_add_one₀ ha₀.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
have refine : ∀ (n : ℤ), a ^ n < a ^ (n + 1)
Tactic: refine strictMono_int_of_lt_succ fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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 + 1)
have rw : a ^ n < a ^ n * a
Tactic: rw [zpow_add_one₀ (zero_lt_one.trans ha).ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
have refine : ∀ (n : ℤ), a ^ (n + 1) < a ^ n
Tactic: refine strictAnti_int_of_succ_lt fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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 + 1) < a ^ n
have rw : a ^ n * a < a ^ n
Tactic: rw [zpow_add_one₀ ha₀.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosMono G₀
n : ℤ
hn : 0 ≤ n
⊢ MonotoneOn (β := G₀) (fun (a : G₀) ↦ a ^ n) {a : G₀ | 0 ≤ a}
have lift : ∀ (n : ℕ), MonotoneOn (β := G₀) (fun (a : G₀) ↦ HPow.hPow (β := ℤ) a (↑n : ℤ)) {a : G₀ | 0 ≤ a}
Tactic: lift n to ℕ using hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosMono G₀
n : ℤ
hn : 0 < n
⊢ StrictMonoOn (β := G₀) (fun (a : G₀) ↦ a ^ n) {a : G₀ | 0 ≤ a}
have lift : ∀ (n : ℕ) (hn : LT.lt (α := ℤ) 0 (↑n : ℤ)),
  StrictMonoOn (β := G₀) (fun (a : G₀) ↦ HPow.hPow (β := ℤ) a (↑n : ℤ)) {a : G₀ | 0 ≤ a}
Tactic: lift n to ℕ using hn.le
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a : G₀
⊢ 0 < a⁻¹ ↔ 0 < a
have suffices : ∀ (a : G₀), 0 < a → 0 < a⁻¹
Tactic: suffices ∀ a : G₀, 0 < a → 0 < a⁻¹ from ⟨fun h ↦ inv_inv a ▸ this _ h, this a⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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⁻¹
have apply : 0 * a < a⁻¹ * a
Tactic: apply lt_of_mul_lt_mul_right _ ha.le
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
have apply : 0 * a * a < a⁻¹ * a * a
Tactic: apply lt_of_mul_lt_mul_right _ ha.le
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
have rw : a * b⁻¹ ≤ 0
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ b * c⁻¹ ↔ a * c ≤ b
have rw : a * c ≤ b * c⁻¹ * c ↔ a * c ≤ b
Tactic: rw [← mul_le_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a ≤ b * c⁻¹ ↔ a * c ≤ b
have rw₁ : a * c ≤ b ↔ a * c ≤ b
Tactic: rw [← mul_le_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b * c⁻¹ ≤ a ↔ b ≤ a * c
have rw : b * c⁻¹ * c ≤ a * c ↔ b ≤ a * c
Tactic: rw [← mul_le_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ b * c⁻¹ ≤ a ↔ b ≤ a * c
have rw₁ : b ≤ a * c ↔ b ≤ a * c
Tactic: rw [← mul_le_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < b * c⁻¹ ↔ a * c < b
have rw : a * c < b * c⁻¹ * c ↔ a * c < b
Tactic: rw [← mul_lt_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a < b * c⁻¹ ↔ a * c < b
have rw₁ : a * c < b ↔ a * c < b
Tactic: rw [← mul_lt_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b * c⁻¹ < a ↔ b < a * c
have rw : b * c⁻¹ * c < a * c ↔ b < a * c
Tactic: rw [← mul_lt_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ b * c⁻¹ < a ↔ b < a * c
have rw₁ : b < a * c ↔ b < a * c
Tactic: rw [← mul_lt_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ b / c ↔ a * c ≤ b
have rw : a ≤ b * c⁻¹ ↔ a * c ≤ b
Tactic: rw [div_eq_mul_inv, le_mul_inv_iff₀ hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a ≤ b / c ↔ a * c ≤ b
have rw₁ : a * c ≤ b ↔ a * c ≤ b
Tactic: rw [div_eq_mul_inv, le_mul_inv_iff₀ hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b / c ≤ a ↔ b ≤ a * c
have rw : b * c⁻¹ ≤ a ↔ b ≤ a * c
Tactic: rw [div_eq_mul_inv, mul_inv_le_iff₀ hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ b / c ≤ a ↔ b ≤ a * c
have rw₁ : b ≤ a * c ↔ b ≤ a * c
Tactic: rw [div_eq_mul_inv, mul_inv_le_iff₀ hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < b / c ↔ a * c < b
have rw : a < b * c⁻¹ ↔ a * c < b
Tactic: rw [div_eq_mul_inv, lt_mul_inv_iff₀ hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a < b / c ↔ a * c < b
have rw₁ : a * c < b ↔ a * c < b
Tactic: rw [div_eq_mul_inv, lt_mul_inv_iff₀ hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b / c < a ↔ b < a * c
have rw : b * c⁻¹ < a ↔ b < a * c
Tactic: rw [div_eq_mul_inv, mul_inv_lt_iff₀ hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ b / c < a ↔ b < a * c
have rw₁ : b < a * c ↔ b < a * c
Tactic: rw [div_eq_mul_inv, mul_inv_lt_iff₀ hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a / c ≤ b / c ↔ a ≤ b
have rw : a ≤ b / c * c ↔ a ≤ b
Tactic: rw [div_le_iff₀ hc, div_mul_cancel₀ _ hc.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a / c ≤ b / c ↔ a ≤ b
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [div_le_iff₀ hc, div_mul_cancel₀ _ hc.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a / c < b / c ↔ a < b
have rw : a < b / c * c ↔ a < b
Tactic: rw [div_lt_iff₀ hc, div_mul_cancel₀ _ hc.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a / c < b / c ↔ a < b
have rw₁ : a < b ↔ a < b
Tactic: rw [div_lt_iff₀ hc, div_mul_cancel₀ _ hc.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ ≤ b ↔ 1 ≤ b * a
have rw : a⁻¹ ≤ b ↔ 1 * a⁻¹ ≤ b
Tactic: rw [← mul_inv_le_iff₀ ha, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a⁻¹ ≤ b ↔ 1 ≤ b * a
have rw₁ : a⁻¹ ≤ b ↔ a⁻¹ ≤ b
Tactic: rw [← mul_inv_le_iff₀ ha, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ < b ↔ 1 < b * a
have rw : a⁻¹ < b ↔ 1 * a⁻¹ < b
Tactic: rw [← mul_inv_lt_iff₀ ha, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a⁻¹ < b ↔ 1 < b * a
have rw₁ : a⁻¹ < b ↔ a⁻¹ < b
Tactic: rw [← mul_inv_lt_iff₀ ha, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ 1 ≤ a / b ↔ b ≤ a
have rw : 1 * b ≤ a ↔ b ≤ a
Tactic: rw [le_div_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ 1 ≤ a / b ↔ b ≤ a
have rw₁ : b ≤ a ↔ b ≤ a
Tactic: rw [le_div_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ 1 < a / b ↔ b < a
have rw : 1 * b < a ↔ b < a
Tactic: rw [lt_div_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ 1 < a / b ↔ b < a
have rw₁ : b < a ↔ b < a
Tactic: rw [lt_div_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ a / b ≤ 1 ↔ a ≤ b
have rw : a ≤ 1 * b ↔ a ≤ b
Tactic: rw [div_le_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a / b ≤ 1 ↔ a ≤ b
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [div_le_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ a / b < 1 ↔ a < b
have rw : a < 1 * b ↔ a < b
Tactic: rw [div_lt_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a / b < 1 ↔ a < b
have rw₁ : a < b ↔ a < b
Tactic: rw [div_lt_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
have inl : ∀ (hc : LE.le.{u_3} (α := G₀) 0 0) (h : a ≤ b * 0⁻¹), a * 0 ≤ b
Tactic: obtain rfl | hc := hc.eq_or_lt
Cleared hypotheses: c, hc, h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a * c ≤ b
have inr : ∀ (hc : 0 < c), a * c ≤ b
Tactic: obtain rfl | hc := hc.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a * c ≤ b
have inr : ∀ (h : a * c ≤ b) (hc : 0 < c), a * c ≤ b
Tactic: rwa [le_mul_inv_iff₀ hc] at h
Cleared hypotheses: h, hc
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
have inl : ∀ (hb : LE.le.{u_3} (α := G₀) 0 0) (h : a ≤ c * 0), a * 0⁻¹ ≤ c
Tactic: obtain rfl | hb := hb.eq_or_lt
Cleared hypotheses: b, hb, h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a * b⁻¹ ≤ c
have inr : ∀ (hb : 0 < b), a * b⁻¹ ≤ c
Tactic: obtain rfl | hb := hb.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a / c ≤ b / c
have rw : a * c⁻¹ ≤ b * c⁻¹
Tactic: rw [div_eq_mul_inv a c, div_eq_mul_inv b c]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a * c⁻¹ ≤ b * c⁻¹
have ha : 0 ≤ c⁻¹
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
have rw : a * c⁻¹ < b * c⁻¹
Tactic: rw [div_eq_mul_inv a c, div_eq_mul_inv b c]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a
have rw : 1 ≤ a * b⁻¹ ↔ b ≤ a
Tactic: rw [inv_le_iff_one_le_mul₀' ha, le_mul_inv_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a
have rw₁ : 1 * b ≤ a ↔ b ≤ a
Tactic: rw [inv_le_iff_one_le_mul₀' ha, le_mul_inv_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a
have rw₂ : b ≤ a ↔ b ≤ a
Tactic: rw [inv_le_iff_one_le_mul₀' ha, le_mul_inv_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a⁻¹ < b⁻¹ ↔ b < a
have rw : 1 < a * b⁻¹ ↔ b < a
Tactic: rw [inv_lt_iff_one_lt_mul₀' ha, lt_mul_inv_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a⁻¹ < b⁻¹ ↔ b < a
have rw₁ : 1 * b < a ↔ b < a
Tactic: rw [inv_lt_iff_one_lt_mul₀' ha, lt_mul_inv_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a⁻¹ < b⁻¹ ↔ b < a
have rw₂ : b < a ↔ b < a
Tactic: rw [inv_lt_iff_one_lt_mul₀' ha, lt_mul_inv_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a
have rw : b⁻¹ ≤ a⁻¹⁻¹ ↔ b⁻¹ ≤ a
Tactic: rw [← inv_le_inv₀ hb (inv_pos.2 ha), inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a
have rw₁ : b⁻¹ ≤ a ↔ b⁻¹ ≤ a
Tactic: rw [← inv_le_inv₀ hb (inv_pos.2 ha), inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a⁻¹ < b ↔ b⁻¹ < a
have rw : b⁻¹ < a⁻¹⁻¹ ↔ b⁻¹ < a
Tactic: rw [← inv_lt_inv₀ hb (inv_pos.2 ha), inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a⁻¹ < b ↔ b⁻¹ < a
have rw₁ : b⁻¹ < a ↔ b⁻¹ < a
Tactic: rw [← inv_lt_inv₀ hb (inv_pos.2 ha), inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹
have rw : b⁻¹⁻¹ ≤ a⁻¹ ↔ b ≤ a⁻¹
Tactic: rw [← inv_le_inv₀ (inv_pos.2 hb) ha, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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⁻¹
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹
have rw₁ : b ≤ a⁻¹ ↔ b ≤ a⁻¹
Tactic: rw [← inv_le_inv₀ (inv_pos.2 hb) ha, inv_inv]