awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a : M₀
inst_2 : PosMulStrictMono M₀
ha : 0 < a
⊢ StrictMono (β := M₀) fun (x : M₀) ↦ a * x

Tactic:
fun _ _ b_lt_c ↦ mul_lt_mul_of_pos_left b_lt_c ha

Premises used: StrictMono, mul_lt_mul_of_pos_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a : M₀
inst_2 : MulPosStrictMono M₀
ha : 0 < a
⊢ StrictMono (β := M₀) fun (x : M₀) ↦ x * a

Tactic:
fun _ _ b_lt_c ↦ mul_lt_mul_of_pos_right b_lt_c ha

Premises used: StrictMono, mul_lt_mul_of_pos_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a : M₀
inst_2 : Preorder α
f : α → M₀
inst_3 : MulPosStrictMono M₀
hf : StrictMono f
ha : 0 < a
⊢ StrictMono.{u_1, u_2} (β := M₀) fun (x : α) ↦ f x * a

Tactic:
(strictMono_mul_right_of_pos ha).comp hf

Premises used: strictMono_mul_right_of_pos, StrictMono.comp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a : M₀
inst_2 : Preorder α
f : α → M₀
inst_3 : PosMulStrictMono M₀
hf : StrictMono f
ha : 0 < a
⊢ StrictMono.{u_1, u_2} (β := M₀) fun (x : α) ↦ a * f x

Tactic:
(strictMono_mul_left_of_pos ha).comp hf

Premises used: strictMono_mul_left_of_pos, StrictMono.comp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a : M₀
inst_2 : Preorder α
f : α → M₀
inst_3 : MulPosStrictMono M₀
hf : StrictAnti f
ha : 0 < a
⊢ StrictAnti.{u_1, u_2} (β := M₀) fun (x : α) ↦ f x * a

Tactic:
(strictMono_mul_right_of_pos ha).comp_strictAnti hf

Premises used: strictMono_mul_right_of_pos, StrictMono.comp_strictAnti
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a : M₀
inst_2 : Preorder α
f : α → M₀
inst_3 : PosMulStrictMono M₀
hf : StrictAnti f
ha : 0 < a
⊢ StrictAnti.{u_1, u_2} (β := M₀) fun (x : α) ↦ a * f x

Tactic:
(strictMono_mul_left_of_pos ha).comp_strictAnti hf

Premises used: strictMono_mul_left_of_pos, StrictMono.comp_strictAnti
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
inst_2 : Preorder α
f g : α → M₀
inst_3 : PosMulMono M₀
inst_4 : MulPosStrictMono M₀
hf : StrictMono f
hg : Monotone g
hf₀ : ∀ (x : α), 0 ≤ f x
hg₀ : ∀ (x : α), 0 < g x
⊢ StrictMono (f * g)

Tactic:
fun _ _ h ↦ mul_lt_mul (hf h) (hg h.le) (hg₀ _) (hf₀ _)

Premises used: StrictMono, mul_lt_mul, LT.lt.le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
inst_2 : Preorder α
f g : α → M₀
inst_3 : PosMulStrictMono M₀
inst_4 : MulPosMono M₀
hf : Monotone f
hg : StrictMono g
hf₀ : ∀ (x : α), 0 < f x
hg₀ : ∀ (x : α), 0 ≤ g x
⊢ StrictMono (f * g)

Tactic:
fun _ _ h ↦ mul_lt_mul' (hf h.le) (hg h) (hg₀ _) (hf₀ _)

Premises used: StrictMono, LT.lt.le, mul_lt_mul'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
inst_2 : Preorder α
f g : α → M₀
inst_3 : PosMulStrictMono M₀
inst_4 : MulPosStrictMono M₀
hf : StrictMono f
hg : StrictMono g
hf₀ : ∀ (x : α), 0 ≤ f x
hg₀ : ∀ (x : α), 0 ≤ g x
⊢ StrictMono (f * g)

Tactic:
fun _ _ h ↦ mul_lt_mul'' (hf h) (hg h) (hf₀ _) (hg₀ _)

Premises used: StrictMono, mul_lt_mul''
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : LinearOrder M₀
inst_2 : PosMulStrictMono M₀
a b : M₀
n : ℕ
inst_3 : MulPosMono M₀
ha : 0 ≤ a
hb : 0 ≤ b
hn : n ≠ 0
⊢ a ^ n ≤ b ^ n ↔ a ≤ b

Tactic:
(pow_left_strictMonoOn₀ hn).le_iff_le ha hb

Premises used: pow_left_strictMonoOn₀, StrictMonoOn.le_iff_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : LinearOrder M₀
inst_2 : PosMulStrictMono M₀
a b : M₀
n : ℕ
inst_3 : MulPosMono M₀
ha : 0 ≤ a
hb : 0 ≤ b
hn : n ≠ 0
⊢ a ^ n < b ^ n ↔ a < b

Tactic:
(pow_left_strictMonoOn₀ hn).lt_iff_lt ha hb

Premises used: pow_left_strictMonoOn₀, StrictMonoOn.lt_iff_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : LinearOrder M₀
inst_2 : PosMulStrictMono M₀
a b : M₀
n : ℕ
inst_3 : MulPosMono M₀
ha : 0 ≤ a
hb : 0 ≤ b
hn : n ≠ 0
⊢ a ^ n = b ^ n ↔ a = b

Tactic:
(pow_left_strictMonoOn₀ hn).eq_iff_eq ha hb

Premises used: StrictMonoOn.eq_iff_eq, pow_left_strictMonoOn₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
inr : ∀ (ha₁ : 1 < a), Injective.{1, u_2 + 1} (β := M₀) fun (x : ℕ) ↦ a ^ x
⊢ Injective.{1, u_2 + 1} (β := M₀) fun (x : ℕ) ↦ a ^ x

Tactic:
obtain ha₁ | ha₁ := ha₁.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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₁_1 : a ≠ 1
ha₁ : a < 1
⊢ Injective.{1, u_2 + 1} (β := M₀) fun (x : ℕ) ↦ a ^ x

Tactic:
(pow_right_strictAnti₀ ha₀ ha₁).injective

Premises used: pow_right_strictAnti₀, StrictAnti.injective
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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₁_1 : a ≠ 1
ha₁ : a < 1
⊢ Injective.{1, u_2 + 1} (β := M₀) fun (x : ℕ) ↦ a ^ x

Tactic:
exact (pow_right_strictAnti₀ ha₀ ha₁).injective

Premises used: pow_right_strictAnti₀, StrictAnti.injective
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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₁_1 : a ≠ 1
ha₁ : 1 < a
⊢ Injective.{1, u_2 + 1} (β := M₀) fun (x : ℕ) ↦ a ^ x

Tactic:
(pow_right_strictMono₀ ha₁).injective

Premises used: StrictMono.injective, pow_right_strictMono₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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₁_1 : a ≠ 1
ha₁ : 1 < a
⊢ Injective.{1, u_2 + 1} (β := M₀) fun (x : ℕ) ↦ a ^ x

Tactic:
exact (pow_right_strictMono₀ ha₁).injective

Premises used: StrictMono.injective, pow_right_strictMono₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : LinearOrder M₀
inst_2 : PosMulStrictMono M₀
a : M₀
m n : ℕ
inst_3 : ZeroLEOneClass M₀
ha₀ : 0 < a
ha₁ : a ≠ 1
⊢ a ^ m = a ^ n ↔ m = n

Tactic:
(pow_right_injective₀ ha₀ ha₁).eq_iff

Premises used: Function.Injective.eq_iff, pow_right_injective₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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

Tactic:
⟨fun h ↦ ?_, pow_le_one₀ ha⟩

Premises used: Iff.intro, pow_le_one₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
refine : ∀ (h : a ^ n ≤ 1), a ≤ 1
⊢ a ^ n ≤ 1 ↔ a ≤ 1

Tactic:
refine ⟨fun h ↦ ?_, pow_le_one₀ ha⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
contrapose! : ∀ (h : 1 < a), 1 < a ^ n
⊢ a ≤ 1

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
⊢ 1 < a ^ n

Tactic:
one_lt_pow₀ h hn

Premises used: one_lt_pow₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
⊢ 1 < a ^ n

Tactic:
exact one_lt_pow₀ h hn

Premises used: one_lt_pow₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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

Tactic:
⟨fun h ↦ ?_, fun h ↦ one_le_pow₀ h⟩

Premises used: one_le_pow₀, Iff.intro
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
refine : ∀ (h : 1 ≤ a ^ n), 1 ≤ a
⊢ 1 ≤ a ^ n ↔ 1 ≤ a

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ one_le_pow₀ h⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
contrapose! : ∀ (h : a < 1), a ^ n < 1
⊢ 1 ≤ a

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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 < 1
⊢ a ^ n < 1

Tactic:
pow_lt_one₀ ha h hn

Premises used: pow_lt_one₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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 < 1
⊢ a ^ n < 1

Tactic:
exact pow_lt_one₀ ha h hn

Premises used: pow_lt_one₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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

Tactic:
lt_iff_lt_of_le_iff_le (one_le_pow_iff_of_nonneg ha hn)

Premises used: one_le_pow_iff_of_nonneg, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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

Tactic:
simp only [← not_le, pow_le_one_iff_of_nonneg ha hn]

Premises used: not_le, pow_le_one_iff_of_nonneg
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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

Tactic:
simp only [le_antisymm_iff, pow_le_one_iff_of_nonneg ha hn, one_le_pow_iff_of_nonneg ha hn]

Premises used: one_le_pow_iff_of_nonneg, pow_le_one_iff_of_nonneg, le_antisymm_iff
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
⊢ HPow.hPow (β := ℕ) a 2 ≤ 1 ↔ a ≤ 1

Tactic:
pow_le_one_iff_of_nonneg ha (Nat.succ_ne_zero _)

Premises used: Nat.succ_ne_zero, pow_le_one_iff_of_nonneg
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
⊢ HPow.hPow (β := ℕ) a 2 < 1 ↔ a < 1

Tactic:
pow_lt_one_iff_of_nonneg ha (Nat.succ_ne_zero _)

Premises used: pow_lt_one_iff_of_nonneg, Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
⊢ 1 ≤ HPow.hPow (β := ℕ) a 2 ↔ 1 ≤ a

Tactic:
one_le_pow_iff_of_nonneg ha (Nat.succ_ne_zero _)

Premises used: one_le_pow_iff_of_nonneg, Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
⊢ 1 < HPow.hPow (β := ℕ) a 2 ↔ 1 < a

Tactic:
one_lt_pow_iff_of_nonneg ha (Nat.succ_ne_zero _)

Premises used: one_lt_pow_iff_of_nonneg, Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : LinearOrder M₀
inst_2 : PosMulStrictMono M₀
a b : M₀
inst_3 : MulPosMono M₀
n : ℕ
hb : 0 ≤ b
h : a ^ n < b ^ n
⊢ a < b

Tactic:
lt_of_not_ge fun hn => not_lt_of_ge (pow_le_pow_left₀ hb hn _) h

Premises used: lt_of_not_ge, pow_le_pow_left₀, not_lt_of_ge
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : LinearOrder M₀
inst_2 : PosMulStrictMono M₀
a b : M₀
n : ℕ
inst_3 : MulPosMono M₀
hn : n ≠ 0
hb : 0 ≤ b
h : a ^ n ≤ b ^ n
⊢ a ≤ b

Tactic:
le_of_not_gt fun h1 => not_le_of_gt (pow_lt_pow_left₀ h1 hb hn) h

Premises used: le_of_not_gt, pow_lt_pow_left₀, not_le_of_gt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : LinearOrder M₀
inst_2 : PosMulStrictMono M₀
a b : M₀
inst_3 : MulPosMono M₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2 ↔ a = b

Tactic:
simp [ha, hb]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
simp : HPow.hPow (β := ℕ) a 2 < HPow.hPow (β := ℕ) b 2 → a < b
⊢ a * a < b * b → a < b

Tactic:
simp only [← sq]

Premises used: sq
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
⊢ HPow.hPow (β := ℕ) a 2 < HPow.hPow (β := ℕ) b 2 → a < b

Tactic:
lt_of_pow_lt_pow_left₀ _ hb

Premises used: lt_of_pow_lt_pow_left₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
⊢ HPow.hPow (β := ℕ) a 2 < HPow.hPow (β := ℕ) b 2 → a < b

Tactic:
exact lt_of_pow_lt_pow_left₀ _ hb

Premises used: lt_of_pow_lt_pow_left₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : LinearOrder M₀
inst_2 : PosMulStrictMono M₀
a b : M₀
inst_3 : MulPosMono M₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ HPow.hPow (β := ℕ) a 2 < HPow.hPow (β := ℕ) b 2 ↔ a < b

Tactic:
pow_lt_pow_iff_left₀ ha hb two_ne_zero

Premises used: two_ne_zero, pow_lt_pow_iff_left₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : LinearOrder M₀
inst_2 : PosMulStrictMono M₀
a b : M₀
inst_3 : MulPosMono M₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ HPow.hPow (β := ℕ) a 2 ≤ HPow.hPow (β := ℕ) b 2 ↔ a ≤ b

Tactic:
pow_le_pow_iff_left₀ ha hb two_ne_zero

Premises used: pow_le_pow_iff_left₀, two_ne_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MonoidWithZero α
inst_1 : PartialOrder α
inst_2 : IsLeftCancelMulZero α
⊢ PosMulMono α ↔ PosMulStrictMono α

Tactic:
⟨(·.toPosMulStrictMono), (·.toPosMulMono)⟩

Premises used: PosMulStrictMono.toPosMulMono, Iff.intro, PosMulMono.toPosMulStrictMono
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MonoidWithZero α
inst_1 : PartialOrder α
inst_2 : IsRightCancelMulZero α
⊢ MulPosMono α ↔ MulPosStrictMono α

Tactic:
⟨(·.toMulPosStrictMono), (·.toMulPosMono)⟩

Premises used: MulPosMono.toMulPosStrictMono, MulPosStrictMono.toMulPosMono, Iff.intro
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MonoidWithZero α
inst_1 : PartialOrder α
inst_2 : IsLeftCancelMulZero α
⊢ PosMulReflectLE α ↔ PosMulReflectLT α

Tactic:
⟨(·.toPosMulReflectLT), (·.toPosMulReflectLE)⟩

Premises used: PosMulReflectLT.toPosMulReflectLE, Iff.intro, PosMulReflectLE.toPosMulReflectLT
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MonoidWithZero α
inst_1 : PartialOrder α
inst_2 : IsRightCancelMulZero α
⊢ MulPosReflectLE α ↔ MulPosReflectLT α

Tactic:
⟨(·.toMulPosReflectLT), (·.toMulPosReflectLE)⟩

Premises used: MulPosReflectLE.toMulPosReflectLT, Iff.intro, MulPosReflectLT.toMulPosReflectLE
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
hb : 0 ≤ b
inl : 0 * (0⁻¹ * b) ≤ b
inr : ∀ (ha : a ≠ 0), a * (a⁻¹ * b) ≤ b
⊢ a * (a⁻¹ * b) ≤ b

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
b : G₀
hb : 0 ≤ b
⊢ 0 * (0⁻¹ * b) ≤ b

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

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
hb : b ≤ 0
inl : b ≤ 0 * (0⁻¹ * b)
inr : ∀ (ha : a ≠ 0), b ≤ a * (a⁻¹ * b)
⊢ b ≤ a * (a⁻¹ * b)

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
b : G₀
hb : b ≤ 0
⊢ b ≤ 0 * (0⁻¹ * b)

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

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
hb : 0 ≤ b
inl : 0⁻¹ * (0 * b) ≤ b
inr : ∀ (ha : a ≠ 0), a⁻¹ * (a * b) ≤ b
⊢ a⁻¹ * (a * b) ≤ b

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
b : G₀
hb : 0 ≤ b
⊢ 0⁻¹ * (0 * b) ≤ b

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

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
hb : b ≤ 0
inl : b ≤ 0⁻¹ * (0 * b)
inr : ∀ (ha : a ≠ 0), b ≤ a⁻¹ * (a * b)
⊢ b ≤ a⁻¹ * (a * b)

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
b : G₀
hb : b ≤ 0
⊢ b ≤ 0⁻¹ * (0 * b)

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

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
ha : 0 ≤ a
inl : a * 0 * 0⁻¹ ≤ a
inr : ∀ (hb : b ≠ 0), a * b * b⁻¹ ≤ a
⊢ a * b * b⁻¹ ≤ a

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a : G₀
ha : 0 ≤ a
⊢ a * 0 * 0⁻¹ ≤ a

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

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
ha : a ≤ 0
inl : a ≤ a * 0 * 0⁻¹
inr : ∀ (hb : b ≠ 0), a ≤ a * b * b⁻¹
⊢ a ≤ a * b * b⁻¹

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a : G₀
ha : a ≤ 0
⊢ a ≤ a * 0 * 0⁻¹

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

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
ha : 0 ≤ a
inl : a * 0⁻¹ * 0 ≤ a
inr : ∀ (hb : b ≠ 0), a * b⁻¹ * b ≤ a
⊢ a * b⁻¹ * b ≤ a

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a : G₀
ha : 0 ≤ a
⊢ a * 0⁻¹ * 0 ≤ a

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

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
ha : a ≤ 0
inl : a ≤ a * 0⁻¹ * 0
inr : ∀ (hb : b ≠ 0), a ≤ a * b⁻¹ * b
⊢ a ≤ a * b⁻¹ * b

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a : G₀
ha : a ≤ 0
⊢ a ≤ a * 0⁻¹ * 0

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

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
inr : ∀ (hc : c ≠ 0), a * c / (b * c) ≤ a / b
⊢ a * c / (b * c) ≤ a / b

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
h : 0 ≤ a / b
⊢ a * 0 / (b * 0) ≤ a / b

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : 0 ≤ a / b
hc : c ≠ 0
inr inr₁ : a / b ≤ a / b
⊢ a * c / (b * c) ≤ a / b

Tactic:
rw [mul_div_mul_right _ _ hc]

Premises used: mul_div_mul_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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)
inr : ∀ (hc : c ≠ 0), a / b ≤ a * c / (b * c)
⊢ a / b ≤ a * c / (b * c)

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b : G₀
h : a / b ≤ 0
⊢ a / b ≤ a * 0 / (b * 0)

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : Preorder G₀
a b c : G₀
h : a / b ≤ 0
hc : c ≠ 0
inr inr₁ : a / b ≤ a / b
⊢ a / b ≤ a * c / (b * c)

Tactic:
rw [mul_div_mul_right _ _ hc]

Premises used: mul_div_mul_right