awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
inst_2 : ZeroLEOneClass M₀
n : ℕ
⊢ HPow.hPow (α := M₀) 0 (n + 1) ≤ 1
have rw : LE.le.{u_2} (α := M₀) 0 1
Tactic: rw [zero_pow n.succ_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (hypothesis)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
inst_2 : PosMulMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n : ℕ
⊢ a ^ (n + 1) ≤ a ^ n
have this : ZeroLEOneClass M₀
Tactic: have : ZeroLEOneClass M₀ := ⟨ha₀.trans ha₁⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
inst_2 : PosMulMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n : ℕ
this : ZeroLEOneClass M₀
⊢ a ^ (n + 1) ≤ a ^ n
have rw : a ^ n * a ≤ a ^ n * 1
Tactic: rw [← mul_one (a ^ n), pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
inst_2 : PosMulMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n : ℕ
this : ZeroLEOneClass M₀
⊢ a ^ n * a ≤ a ^ n * 1
have ha : 0 ≤ a ^ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
inst_2 : PosMulMono M₀
h₀ : 0 ≤ a
h₁ : a < 1
n : ℕ
h : n + 1 ≠ 0
⊢ a ^ (n + 1) < 1
have rw : a * a ^ n < 1
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
inst_2 : ZeroLEOneClass M₀
inst_3 : PosMulMono M₀
h : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ (n + 1)
have rw : a ^ n ≤ a ^ n * a
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
inst_2 : ZeroLEOneClass M₀
inst_3 : PosMulMono M₀
ha : 1 < a
n : ℕ
h : n + 1 ≠ 0
⊢ 1 < a ^ (n + 1)
have rw : 1 < a * a ^ n
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
m n : ℕ
inst_2 : ZeroLEOneClass M₀
inst_3 : PosMulMono M₀
h : 1 ≤ a ∧ n ≤ m ∨ 0 ≤ a ∧ a ≤ 1 ∧ m ≤ n
⊢ a ^ n ≤ a ^ m
have inl : ∀ (a1 : 1 ≤ a) (nm : n ≤ m), a ^ n ≤ a ^ m
Tactic: obtain ⟨a1, nm⟩ | ⟨a0, a1, mn⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
m n : ℕ
inst_2 : ZeroLEOneClass M₀
inst_3 : PosMulMono M₀
h : 1 ≤ a ∧ n ≤ m ∨ 0 ≤ a ∧ a ≤ 1 ∧ m ≤ n
inl : ∀ (a1 : 1 ≤ a) (nm : n ≤ m), a ^ n ≤ a ^ m
⊢ a ^ n ≤ a ^ m
have inr : ∀ (a0 : 0 ≤ a) (a1 : a ≤ 1) (mn : m ≤ n), a ^ n ≤ a ^ m
Tactic: obtain ⟨a1, nm⟩ | ⟨a0, a1, mn⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a b c d : M₀
inst_2 : PosMulMono M₀
inst_3 : PosMulStrictMono M₀
inst_4 : MulPosStrictMono M₀
inst_5 : DecidableLE M₀
h1 : a < c
h2 : b < d
h3 : 0 ≤ a
h4 : 0 ≤ b
b0 : 0 = b
⊢ a * b < c * d
have rw : 0 < c * d
Tactic: rw [← b0, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (hypothesis)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a : M₀
inst_2 : PosMulStrictMono M₀
inst_3 : ZeroLEOneClass M₀
ha : 0 < a
⊢ 0 < HPow.hPow (β := ℕ) a 0
have inst : Nontrivial M₀
Tactic: nontriviality
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a : M₀
inst_2 : PosMulStrictMono M₀
inst_3 : ZeroLEOneClass M₀
ha : 0 < a
inst_4 : Nontrivial M₀
⊢ 0 < HPow.hPow (β := ℕ) a 0
have rw : LT.lt.{u_2} (α := M₀) 0 1
Tactic: rw [pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (hypothesis)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a : M₀
inst_2 : PosMulStrictMono M₀
h₀ : 0 < a
h₁ : a < 1
n : ℕ
⊢ a ^ (n + 1) < a ^ n
have this : ZeroLEOneClass M₀
Tactic: have : ZeroLEOneClass M₀ := ⟨(h₀.trans h₁).le⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : LinearOrder M₀
inst_2 : PosMulStrictMono M₀
a : M₀
inst_3 : ZeroLEOneClass M₀
ha₀ : 0 < a
ha₁ : a ≠ 1
⊢ Injective.{1, u_2 + 1} (β := M₀) fun (x : ℕ) ↦ a ^ x
have inl : ∀ (ha₁ : a < 1), Injective.{1, u_2 + 1} (β := M₀) fun (x : ℕ) ↦ a ^ x
Tactic: obtain ha₁ | ha₁ := ha₁.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : LinearOrder M₀
inst_2 : PosMulStrictMono M₀
a : M₀
inst_3 : ZeroLEOneClass M₀
ha₀ : 0 < a
ha₁ : a ≠ 1
inl : ∀ (ha₁ : a < 1), Injective.{1, u_2 + 1} (β := M₀) fun (x : ℕ) ↦ a ^ x
⊢ Injective.{1, u_2 + 1} (β := M₀) fun (x : ℕ) ↦ a ^ x
have inr : ∀ (ha₁ : 1 < a), Injective.{1, u_2 + 1} (β := M₀) fun (x : ℕ) ↦ a ^ x
Tactic: obtain ha₁ | ha₁ := ha₁.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : LinearOrder M₀
inst_2 : PosMulStrictMono M₀
a : M₀
n : ℕ
inst_3 : ZeroLEOneClass M₀
ha : 0 ≤ a
hn : n ≠ 0
⊢ a ^ n ≤ 1 ↔ a ≤ 1
have refine : ∀ (h : a ^ n ≤ 1), a ≤ 1
Tactic: refine ⟨fun h ↦ ?_, pow_le_one₀ ha⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : LinearOrder M₀
inst_2 : PosMulStrictMono M₀
a : M₀
n : ℕ
inst_3 : ZeroLEOneClass M₀
ha : 0 ≤ a
hn : n ≠ 0
h : a ^ n ≤ 1
⊢ a ≤ 1
have contrapose! : ∀ (h : 1 < a), 1 < a ^ n
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : LinearOrder M₀
inst_2 : PosMulStrictMono M₀
a : M₀
n : ℕ
inst_3 : ZeroLEOneClass M₀
ha : 0 ≤ a
hn : n ≠ 0
⊢ 1 ≤ a ^ n ↔ 1 ≤ a
have refine : ∀ (h : 1 ≤ a ^ n), 1 ≤ a
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ one_le_pow₀ h⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : LinearOrder M₀
inst_2 : PosMulStrictMono M₀
a : M₀
n : ℕ
inst_3 : ZeroLEOneClass M₀
ha : 0 ≤ a
hn : n ≠ 0
h : 1 ≤ a ^ n
⊢ 1 ≤ a
have contrapose! : ∀ (h : a < 1), a ^ n < 1
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : LinearOrder M₀
inst_2 : PosMulStrictMono M₀
a b : M₀
inst_3 : MulPosMono M₀
hb : 0 ≤ b
⊢ a * a < b * b → a < b
have simp : HPow.hPow (β := ℕ) a 2 < HPow.hPow (β := ℕ) b 2 → a < b
Tactic: simp only [← sq]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
hb : 0 ≤ b
⊢ a * (a⁻¹ * b) ≤ b
have inl : 0 * (0⁻¹ * b) ≤ b
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
hb : 0 ≤ b
inl : 0 * (0⁻¹ * b) ≤ b
⊢ a * (a⁻¹ * b) ≤ b
have inr : ∀ (ha : a ≠ 0), a * (a⁻¹ * b) ≤ b
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
hb : b ≤ 0
⊢ b ≤ a * (a⁻¹ * b)
have inl : b ≤ 0 * (0⁻¹ * b)
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
hb : b ≤ 0
inl : b ≤ 0 * (0⁻¹ * b)
⊢ b ≤ a * (a⁻¹ * b)
have inr : ∀ (ha : a ≠ 0), b ≤ a * (a⁻¹ * b)
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
hb : 0 ≤ b
⊢ a⁻¹ * (a * b) ≤ b
have inl : 0⁻¹ * (0 * b) ≤ b
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
hb : 0 ≤ b
inl : 0⁻¹ * (0 * b) ≤ b
⊢ a⁻¹ * (a * b) ≤ b
have inr : ∀ (ha : a ≠ 0), a⁻¹ * (a * b) ≤ b
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
hb : b ≤ 0
⊢ b ≤ a⁻¹ * (a * b)
have inl : b ≤ 0⁻¹ * (0 * b)
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
hb : b ≤ 0
inl : b ≤ 0⁻¹ * (0 * b)
⊢ b ≤ a⁻¹ * (a * b)
have inr : ∀ (ha : a ≠ 0), b ≤ a⁻¹ * (a * b)
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
ha : 0 ≤ a
⊢ a * b * b⁻¹ ≤ a
have inl : a * 0 * 0⁻¹ ≤ a
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
ha : 0 ≤ a
inl : a * 0 * 0⁻¹ ≤ a
⊢ a * b * b⁻¹ ≤ a
have inr : ∀ (hb : b ≠ 0), a * b * b⁻¹ ≤ a
Tactic: obtain rfl | hb := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
ha : a ≤ 0
⊢ a ≤ a * b * b⁻¹
have inl : a ≤ a * 0 * 0⁻¹
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
ha : a ≤ 0
inl : a ≤ a * 0 * 0⁻¹
⊢ a ≤ a * b * b⁻¹
have inr : ∀ (hb : b ≠ 0), a ≤ a * b * b⁻¹
Tactic: obtain rfl | hb := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
ha : 0 ≤ a
⊢ a * b⁻¹ * b ≤ a
have inl : a * 0⁻¹ * 0 ≤ a
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
ha : 0 ≤ a
inl : a * 0⁻¹ * 0 ≤ a
⊢ a * b⁻¹ * b ≤ a
have inr : ∀ (hb : b ≠ 0), a * b⁻¹ * b ≤ a
Tactic: obtain rfl | hb := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
ha : a ≤ 0
⊢ a ≤ a * b⁻¹ * b
have inl : a ≤ a * 0⁻¹ * 0
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
ha : a ≤ 0
inl : a ≤ a * 0⁻¹ * 0
⊢ a ≤ a * b⁻¹ * b
have inr : ∀ (hb : b ≠ 0), a ≤ a * b⁻¹ * b
Tactic: obtain rfl | hb := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : 0 ≤ a / b
⊢ a * c / (b * c) ≤ a / b
have inl : a * 0 / (b * 0) ≤ 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 : GroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : 0 ≤ a / b
inl : a * 0 / (b * 0) ≤ a / b
⊢ a * c / (b * c) ≤ a / b
have inr : ∀ (hc : c ≠ 0), a * c / (b * c) ≤ 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 : GroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : 0 ≤ a / b
hc : c ≠ 0
⊢ a * c / (b * c) ≤ a / b
have inr : a / b ≤ a / b
Tactic: rw [mul_div_mul_right _ _ hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : a / b ≤ 0
⊢ a / b ≤ a * c / (b * c)
have inl : a / b ≤ a * 0 / (b * 0)
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 : GroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : a / b ≤ 0
inl : a / b ≤ a * 0 / (b * 0)
⊢ a / b ≤ a * c / (b * c)
have inr : ∀ (hc : c ≠ 0), a / b ≤ a * c / (b * c)
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 : GroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : a / b ≤ 0
hc : c ≠ 0
⊢ a / b ≤ a * c / (b * c)
have inr : a / b ≤ a / b
Tactic: rw [mul_div_mul_right _ _ hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
inst_2 : ZeroLEOneClass G₀
a : G₀
⊢ a / a ≤ 1
have inl : 0 / 0 ≤ 1
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
inst_2 : ZeroLEOneClass G₀
a : G₀
inl : 0 / 0 ≤ 1
⊢ a / a ≤ 1
have inr : ∀ (ha : a ≠ 0), a / a ≤ 1
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
inst_2 : ZeroLEOneClass G₀
a : G₀
⊢ a⁻¹ * a ≤ 1
have inl : HMul.hMul (α := G₀) 0⁻¹ 0 ≤ 1
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
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
⊢ a⁻¹ * a ≤ 1
have inr : ∀ (ha : a ≠ 0), a⁻¹ * a ≤ 1
Tactic: obtain rfl | ha := eq_or_ne a 0
-- 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₀
⊢ 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 : PosMulReflectLT G₀
a_1 a : G₀
ha : 0 < a
⊢ 0 < a⁻¹
have apply : a * 0 < a * a⁻¹
Tactic: apply lt_of_mul_lt_mul_left _ 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 : PosMulReflectLT G₀
a_1 a : G₀
ha : 0 < a
⊢ a * 0 < a * a⁻¹
have apply : a * (a * 0) < a * (a * a⁻¹)
Tactic: apply lt_of_mul_lt_mul_left _ 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 : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ 0 < a / b
have rw : 0 < a * b⁻¹
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 : PosMulReflectLT G₀
a b : G₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a / b
have rw : 0 ≤ a * b⁻¹
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 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ c⁻¹ * b ↔ c * a ≤ b
have rw : c * a ≤ c * (c⁻¹ * b) ↔ c * a ≤ b
Tactic: rw [← mul_le_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ 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 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : c * a ≤ c * (c⁻¹ * b) ↔ c * a ≤ b
⊢ a ≤ c⁻¹ * b ↔ c * a ≤ b
have rw₁ : c * a ≤ b ↔ c * a ≤ b
Tactic: rw [← mul_le_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ 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 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ c⁻¹ * b ≤ a ↔ b ≤ c * a
have rw : c * (c⁻¹ * b) ≤ c * a ↔ b ≤ c * a
Tactic: rw [← mul_le_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ 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 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : c * (c⁻¹ * b) ≤ c * a ↔ b ≤ c * a
⊢ c⁻¹ * b ≤ a ↔ b ≤ c * a
have rw₁ : b ≤ c * a ↔ b ≤ c * a
Tactic: rw [← mul_le_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ 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 : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ 1 ≤ a⁻¹ * b ↔ a ≤ b
have rw : a * 1 ≤ b ↔ a ≤ b
Tactic: rw [le_inv_mul_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 b : G₀
ha : 0 < a
rw : a * 1 ≤ b ↔ a ≤ b
⊢ 1 ≤ a⁻¹ * b ↔ a ≤ b
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [le_inv_mul_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 b : G₀
ha : 0 < a
⊢ a⁻¹ * b ≤ 1 ↔ b ≤ a
have rw : b ≤ a * 1 ↔ b ≤ a
Tactic: rw [inv_mul_le_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 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_le_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 b : G₀
ha : 0 < a
⊢ a⁻¹ ≤ b ↔ 1 ≤ a * b
have rw : a⁻¹ ≤ b ↔ a⁻¹ * 1 ≤ b
Tactic: rw [← inv_mul_le_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 b : G₀
ha : 0 < a
rw : a⁻¹ ≤ b ↔ a⁻¹ * 1 ≤ b
⊢ a⁻¹ ≤ b ↔ 1 ≤ a * b
have rw₁ : a⁻¹ ≤ b ↔ a⁻¹ ≤ b
Tactic: rw [← inv_mul_le_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 b c : G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c⁻¹ * b
⊢ c * a ≤ b
have inl : ∀ (hc : LE.le.{u_3} (α := G₀) 0 0) (h : a ≤ 0⁻¹ * b), 0 * a ≤ 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 : 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
⊢ c * a ≤ b
have inr : ∀ (hc : 0 < c), c * a ≤ 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 : PosMulReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc_1 : 0 ≤ c
h : a ≤ c⁻¹ * b
hc : 0 < c
⊢ c * a ≤ b
have inr : ∀ (h : c * a ≤ b) (hc : 0 < c), c * a ≤ b
Tactic: rwa [le_inv_mul_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 : PosMulReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b * c
⊢ b⁻¹ * a ≤ c
have inl : ∀ (hb : LE.le.{u_3} (α := G₀) 0 0) (h : a ≤ 0 * c), 0⁻¹ * a ≤ 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 : 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
⊢ b⁻¹ * a ≤ c
have inr : ∀ (hb : 0 < b), b⁻¹ * a ≤ 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 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < c⁻¹ * b ↔ c * a < b
have rw : c * a < c * (c⁻¹ * b) ↔ c * a < b
Tactic: rw [← mul_lt_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ 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 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : c * a < c * (c⁻¹ * b) ↔ c * a < b
⊢ a < c⁻¹ * b ↔ c * a < b
have rw₁ : c * a < b ↔ c * a < b
Tactic: rw [← mul_lt_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ 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 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ c⁻¹ * b < a ↔ b < c * a
have rw : c * (c⁻¹ * b) < c * a ↔ b < c * a
Tactic: rw [← mul_lt_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ 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 : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
rw : c * (c⁻¹ * b) < c * a ↔ b < c * a
⊢ c⁻¹ * b < a ↔ b < c * a
have rw₁ : b < c * a ↔ b < c * a
Tactic: rw [← mul_lt_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ 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 : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ < b ↔ 1 < a * b
have rw : a⁻¹ < b ↔ a⁻¹ * 1 < b
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 b : G₀
ha : 0 < a
rw : a⁻¹ < b ↔ a⁻¹ * 1 < b
⊢ a⁻¹ < b ↔ 1 < a * b
have rw₁ : a⁻¹ < b ↔ a⁻¹ < b
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 b : G₀
ha : 0 < a
⊢ 1 < a⁻¹ * b ↔ a < b
have rw : a * 1 < b ↔ a < b
Tactic: rw [lt_inv_mul_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 b : G₀
ha : 0 < a
rw : a * 1 < b ↔ a < b
⊢ 1 < a⁻¹ * b ↔ a < b
have rw₁ : a < b ↔ a < b
Tactic: rw [lt_inv_mul_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 b : G₀
ha : 0 < a
⊢ a⁻¹ * b < 1 ↔ b < a
have rw : b < a * 1 ↔ b < a
Tactic: rw [inv_mul_lt_iff₀ ha, mul_one]