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₀
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₀ (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_lt_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 c : G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ a / b ≤ a / c
have rw : a * b⁻¹ ≤ a * c⁻¹
Tactic: rw [div_eq_mul_inv, 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 : PosMulReflectLT G₀
inst_3 : MulPosReflectLT G₀
a b c d : G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ a / b ≤ c / d
have rw : a * b⁻¹ ≤ c * d⁻¹
Tactic: rw [div_eq_mul_inv, 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 : PosMulReflectLT G₀
inst_3 : MulPosReflectLT G₀
a b c d : G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ a * b⁻¹ ≤ c * d⁻¹
have c0 : 0 ≤ b⁻¹
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 : 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
have rw : a * b⁻¹ < c * d⁻¹
Tactic: rw [div_eq_mul_inv, 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 : 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⁻¹
have apply : 0 < b⁻¹
Tactic: apply mul_lt_mul hac (by gcongr; assumption) _ 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 : 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
have rw : a * b⁻¹ < c * d⁻¹
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (hypothesis)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a : G₀
inst_2 : PosMulMono G₀
⊢ a⁻¹ < 0 ↔ a < 0
have this : PosMulReflectLT G₀
Tactic: have := PosMulMono.toPosMulReflectLT (α := G₀)
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (hypothesis)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : LinearOrder G₀
a : G₀
inst_2 : PosMulMono G₀
⊢ a⁻¹ ≤ 0 ↔ a ≤ 0
have this : PosMulReflectLT G₀
Tactic: have := PosMulMono.toPosMulReflectLT (α := G₀)
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
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 : LinearOrder G₀
a : G₀
inst_2 : PosMulStrictMono G₀
inst_3 : ZeroLEOneClass G₀
⊢ a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a
have simp_rw : ¬1 ≤ a⁻¹ ↔ a ≤ 0 ∨ ¬a ≤ 1
Tactic: simp_rw [← not_le, one_le_inv_iff₀, not_and_or, not_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a
have simp_rw₁ : ¬(0 < a ∧ a ≤ 1) ↔ a ≤ 0 ∨ ¬a ≤ 1
Tactic: simp_rw [← not_le, one_le_inv_iff₀, not_and_or, not_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a
have simp_rw₂ : ¬0 < a ∨ ¬a ≤ 1 ↔ a ≤ 0 ∨ ¬a ≤ 1
Tactic: simp_rw [← not_le, one_le_inv_iff₀, not_and_or, not_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ Injective.{1, u_3 + 1} (β := G₀) fun (n : ℤ) ↦ a ^ n
have inl : ∀ (ha₁ : a < 1), Injective.{1, u_3 + 1} (β := G₀) fun (n : ℤ) ↦ a ^ n
Tactic: obtain ha₁ | ha₁ := ha₁.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ Injective.{1, u_3 + 1} (β := G₀) fun (n : ℤ) ↦ a ^ n
have inr : ∀ (ha₁ : 1 < a), Injective.{1, u_3 + 1} (β := G₀) fun (n : ℤ) ↦ a ^ n
Tactic: obtain ha₁ | ha₁ := ha₁.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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 : ℤ
⊢ a ^ n = 1 ↔ n = 0
have 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
Tactic: obtain rfl | ha₀ := ha₀.eq_or_lt
Cleared hypotheses: a, ha₀, ha₁
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a ^ n = 1 ↔ n = 0
have inr : ∀ (ha₀ : 0 < a), a ^ n = 1 ↔ n = 0
Tactic: obtain rfl | ha₀ := ha₀.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : 0 ≤ a / b
⊢ c * a / (c * b) ≤ a / b
have inl : 0 * a / (0 * b) ≤ a / b
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : 0 ≤ a / b
inl : 0 * a / (0 * b) ≤ a / b
⊢ c * a / (c * b) ≤ a / b
have inr : ∀ (hc : c ≠ 0), c * a / (c * b) ≤ a / b
Tactic: obtain rfl | hc := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : 0 ≤ a / b
hc : c ≠ 0
⊢ c * a / (c * b) ≤ a / b
have inr : a / b ≤ a / b
Tactic: rw [mul_div_mul_left _ _ hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : a / b ≤ 0
⊢ a / b ≤ c * a / (c * b)
have inl : a / b ≤ 0 * a / (0 * b)
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : a / b ≤ 0
inl : a / b ≤ 0 * a / (0 * b)
⊢ a / b ≤ c * a / (c * b)
have inr : ∀ (hc : c ≠ 0), a / b ≤ c * a / (c * b)
Tactic: obtain rfl | hc := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : a / b ≤ 0
hc : c ≠ 0
⊢ a / b ≤ c * a / (c * b)
have inr : a / b ≤ a / b
Tactic: rw [mul_div_mul_left _ _ hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ c⁻¹ * b ↔ a * c ≤ b
have rw : c * a ≤ b ↔ a * c ≤ b
Tactic: rw [le_inv_mul_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : c * a ≤ b ↔ a * c ≤ b
⊢ a ≤ c⁻¹ * b ↔ a * c ≤ b
have rw₁ : a * c ≤ b ↔ a * c ≤ b
Tactic: rw [le_inv_mul_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ c⁻¹ * b ≤ a ↔ b ≤ a * c
have rw : b ≤ c * a ↔ b ≤ a * c
Tactic: rw [inv_mul_le_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : b ≤ c * a ↔ b ≤ a * c
⊢ c⁻¹ * b ≤ a ↔ b ≤ a * c
have rw₁ : b ≤ a * c ↔ b ≤ a * c
Tactic: rw [inv_mul_le_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ b * c⁻¹ ↔ c * a ≤ b
have rw : a * c ≤ b ↔ c * a ≤ b
Tactic: rw [le_mul_inv_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : a * c ≤ b ↔ c * a ≤ b
⊢ a ≤ b * c⁻¹ ↔ c * a ≤ b
have rw₁ : c * a ≤ b ↔ c * a ≤ b
Tactic: rw [le_mul_inv_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b * c⁻¹ ≤ a ↔ b ≤ c * a
have rw : b ≤ a * c ↔ b ≤ c * a
Tactic: rw [mul_inv_le_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : b ≤ a * c ↔ b ≤ c * a
⊢ b * c⁻¹ ≤ a ↔ b ≤ c * a
have rw₁ : b ≤ c * a ↔ b ≤ c * a
Tactic: rw [mul_inv_le_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
⊢ a / b ≤ c / d ↔ a * d ≤ c * b
have rw : a ≤ c / d * b ↔ a * d ≤ c * b
Tactic: rw [div_le_iff₀ hb, ← mul_div_right_comm, le_div_iff₀ hd]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
rw : a ≤ c / d * b ↔ a * d ≤ c * b
⊢ a / b ≤ c / d ↔ a * d ≤ c * b
have rw₁ : a ≤ c * b / d ↔ a * d ≤ c * b
Tactic: rw [div_le_iff₀ hb, ← mul_div_right_comm, le_div_iff₀ hd]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
rw : a ≤ c / d * b ↔ a * d ≤ c * b
rw₁ : a ≤ c * b / d ↔ a * d ≤ c * b
⊢ a / b ≤ c / d ↔ a * d ≤ c * b
have rw₂ : a * d ≤ c * b ↔ a * d ≤ c * b
Tactic: rw [div_le_iff₀ hb, ← mul_div_right_comm, le_div_iff₀ hd]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ b / c ↔ c * a ≤ b
have rw : a * c ≤ b ↔ c * a ≤ b
Tactic: rw [le_div_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : a * c ≤ b ↔ c * a ≤ b
⊢ a ≤ b / c ↔ c * a ≤ b
have rw₁ : c * a ≤ b ↔ c * a ≤ b
Tactic: rw [le_div_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b / c ≤ a ↔ b ≤ c * a
have rw : b ≤ a * c ↔ b ≤ c * a
Tactic: rw [div_le_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : b ≤ a * c ↔ b ≤ c * a
⊢ b / c ≤ a ↔ b ≤ c * a
have rw₁ : b ≤ c * a ↔ b ≤ c * a
Tactic: rw [div_le_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
ha : 0 < a
hc : 0 < c
⊢ a ≤ b / c ↔ c ≤ b / a
have rw : a ≤ b / c ↔ c * a ≤ b
Tactic: rw [le_div_iff₀ ha, le_div_iff₀' hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
ha : 0 < a
hc : 0 < c
rw : a ≤ b / c ↔ c * a ≤ b
⊢ a ≤ b / c ↔ c ≤ b / a
have rw₁ : c * a ≤ b ↔ c * a ≤ b
Tactic: rw [le_div_iff₀ ha, le_div_iff₀' hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
⊢ a / b ≤ c ↔ a / c ≤ b
have rw : a ≤ c * b ↔ a / c ≤ b
Tactic: rw [div_le_iff₀ hb, div_le_iff₀' hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
rw : a ≤ c * b ↔ a / c ≤ b
⊢ a / b ≤ c ↔ a / c ≤ b
have rw₁ : a ≤ c * b ↔ a ≤ c * b
Tactic: rw [div_le_iff₀ hb, div_le_iff₀' hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < c⁻¹ * b ↔ a * c < b
have rw : c * a < b ↔ a * c < b
Tactic: rw [lt_inv_mul_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : c * a < b ↔ a * c < b
⊢ a < c⁻¹ * b ↔ a * c < b
have rw₁ : a * c < b ↔ a * c < b
Tactic: rw [lt_inv_mul_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ c⁻¹ * b < a ↔ b < a * c
have rw : b < c * a ↔ b < a * c
Tactic: rw [inv_mul_lt_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : b < c * a ↔ b < a * c
⊢ c⁻¹ * b < a ↔ b < a * c
have rw₁ : b < a * c ↔ b < a * c
Tactic: rw [inv_mul_lt_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < b * c⁻¹ ↔ c * a < b
have rw : a * c < b ↔ c * a < b
Tactic: rw [lt_mul_inv_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : a * c < b ↔ c * a < b
⊢ a < b * c⁻¹ ↔ c * a < b
have rw₁ : c * a < b ↔ c * a < b
Tactic: rw [lt_mul_inv_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b * c⁻¹ < a ↔ b < c * a
have rw : b < a * c ↔ b < c * a
Tactic: rw [mul_inv_lt_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : b < a * c ↔ b < c * a
⊢ b * c⁻¹ < a ↔ b < c * a
have rw₁ : b < c * a ↔ b < c * a
Tactic: rw [mul_inv_lt_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
⊢ a / b < c / d ↔ a * d < c * b
have rw : a < c / d * b ↔ a * d < c * b
Tactic: rw [div_lt_iff₀ hb, ← mul_div_right_comm, lt_div_iff₀ hd]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
rw : a < c / d * b ↔ a * d < c * b
⊢ a / b < c / d ↔ a * d < c * b
have rw₁ : a < c * b / d ↔ a * d < c * b
Tactic: rw [div_lt_iff₀ hb, ← mul_div_right_comm, lt_div_iff₀ hd]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
rw : a < c / d * b ↔ a * d < c * b
rw₁ : a < c * b / d ↔ a * d < c * b
⊢ a / b < c / d ↔ a * d < c * b
have rw₂ : a * d < c * b ↔ a * d < c * b
Tactic: rw [div_lt_iff₀ hb, ← mul_div_right_comm, lt_div_iff₀ hd]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < b / c ↔ c * a < b
have rw : a * c < b ↔ c * a < b
Tactic: rw [lt_div_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : a * c < b ↔ c * a < b
⊢ a < b / c ↔ c * a < b
have rw₁ : c * a < b ↔ c * a < b
Tactic: rw [lt_div_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b / c < a ↔ b < c * a
have rw : b < a * c ↔ b < c * a
Tactic: rw [div_lt_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : b < a * c ↔ b < c * a
⊢ b / c < a ↔ b < c * a
have rw₁ : b < c * a ↔ b < c * a
Tactic: rw [div_lt_iff₀ hc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
ha : 0 < a
hc : 0 < c
⊢ a < b / c ↔ c < b / a
have rw : a < b / c ↔ c * a < b
Tactic: rw [lt_div_iff₀ ha, lt_div_iff₀' hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
ha : 0 < a
hc : 0 < c
rw : a < b / c ↔ c * a < b
⊢ a < b / c ↔ c < b / a
have rw₁ : c * a < b ↔ c * a < b
Tactic: rw [lt_div_iff₀ ha, lt_div_iff₀' hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
⊢ a / b < c ↔ a / c < b
have rw : a < c * b ↔ a / c < b
Tactic: rw [div_lt_iff₀ hb, div_lt_iff₀' hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : CommGroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
rw : a < c * b ↔ a / c < b
⊢ a / b < c ↔ a / c < b
have rw₁ : a < c * b ↔ a < c * b
Tactic: rw [div_lt_iff₀ hb, div_lt_iff₀' hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : PosMulMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ a * b ≤ a * c
have rw : f a * f b ≤ f a * f c
Tactic: rw [← le, mul, mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : PosMulMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ 0 ≤ f a
have rwa : f 0 ≤ f a
Tactic: rwa [← zero, le]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : MulPosMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ b * a ≤ c * a
have rw : f b * f a ≤ f c * f a
Tactic: rw [← le, mul, mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : MulPosMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ 0 ≤ f a
have rwa : f 0 ≤ f a
Tactic: rwa [← zero, le]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ a * b < a * c
have rw : f a * f b < f a * f c
Tactic: rw [← lt, mul, mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ 0 < f a
have rwa : f 0 < f a
Tactic: rwa [← zero, lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ b * a < c * a
have rw : f b * f a < f c * f a
Tactic: rw [← lt, mul, mul]