awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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₀
ha : 0 ≤ a ^ n
⊢ a ^ n * a ≤ a ^ n * 1

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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₀
⊢ 0 ≤ a ^ n

Tactic:
pow_nonneg ha₀ n

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

Tactic:
exact pow_nonneg ha₀ n

Premises used: pow_nonneg
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
inst_2 : PosMulMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
m n : ℕ
hmn : m ≤ n
⊢ a ^ n ≤ a ^ m

Tactic:
pow_right_anti₀ ha₀ ha₁ hmn

Premises used: pow_right_anti₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
n : ℕ
inst_2 : PosMulMono M₀
h₀ : 0 ≤ a
h₁ : a ≤ 1
hn : n ≠ 0
⊢ a ^ n ≤ a

Tactic:
(pow_one a).subst (pow_le_pow_of_le_one h₀ h₁ (Nat.pos_of_ne_zero hn))

Premises used: Eq.subst, pow_le_pow_of_le_one, Nat.pos_of_ne_zero, pow_one
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
inst_2 : PosMulMono M₀
h₀ : 0 ≤ a
h₁ : a ≤ 1
⊢ HPow.hPow (β := ℕ) a 2 ≤ a

Tactic:
pow_le_of_le_one h₀ h₁ two_ne_zero

Premises used: two_ne_zero, pow_le_of_le_one
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
inst_2 : PosMulMono M₀
n : ℕ
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ a ^ n ≤ 1

Tactic:
pow_zero a ▸ pow_right_anti₀ ha₀ ha₁ (Nat.zero_le n)

Premises used: Nat.zero_le, Eq.rec, pow_zero, pow_right_anti₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a b : M₀
inst_2 : ZeroLEOneClass M₀
inst_3 : PosMulMono M₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ 1 ≤ a * b

Tactic:
ha.trans <| le_mul_of_one_le_right (zero_le_one.trans ha) hb

Premises used: zero_le_one, le_mul_of_one_le_right, LE.le.trans
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a b : M₀
inst_2 : ZeroLEOneClass M₀
inst_3 : MulPosMono M₀
ha : 1 ≤ a
hb : 1 < b
⊢ 1 < a * b

Tactic:
hb.trans_le <| le_mul_of_one_le_left (zero_le_one.trans hb.le) ha

Premises used: le_mul_of_one_le_left, LT.lt.le, zero_le_one, LT.lt.trans_le, LE.le.trans
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a b : M₀
inst_2 : ZeroLEOneClass M₀
inst_3 : PosMulMono M₀
ha : 1 < a
hb : 1 ≤ b
⊢ 1 < a * b

Tactic:
ha.trans_le <| le_mul_of_one_le_right (zero_le_one.trans ha.le) hb

Premises used: LT.lt.le, zero_le_one, LT.lt.trans_le, le_mul_of_one_le_right, LE.le.trans
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a b : M₀
inst_2 : PosMulMono M₀
ha₀ : 0 ≤ a
ha : a < 1
hb : b ≤ 1
⊢ a * b < 1

Tactic:
(mul_le_of_le_one_right ha₀ hb).trans_lt ha

Premises used: mul_le_of_le_one_right, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a b : M₀
inst_2 : MulPosMono M₀
ha : a ≤ 1
hb₀ : 0 ≤ b
hb : b < 1
⊢ a * b < 1

Tactic:
(mul_le_of_le_one_left hb₀ ha).trans_lt hb

Premises used: mul_le_of_le_one_left, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a b : M₀
inst_2 : ZeroLEOneClass M₀
inst_3 : PosMulMono M₀
inst_4 : MulPosMono M₀
ha : 1 ≤ a
hb : 1 < b
⊢ 1 < a * b

Tactic:
one_lt_mul ha hb

Premises used: one_lt_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a b : M₀
inst_2 : ZeroLEOneClass M₀
inst_3 : PosMulMono M₀
inst_4 : MulPosMono M₀
ha : 1 < a
hb : 1 ≤ b
⊢ 1 < a * b

Tactic:
one_lt_mul_of_lt_of_le ha hb

Premises used: one_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a b : M₀
inst_2 : ZeroLEOneClass M₀
inst_3 : PosMulMono M₀
inst_4 : MulPosMono M₀
ha : 1 ≤ a
hb : 1 < b
⊢ 1 < a * b

Tactic:
exacts [one_lt_mul ha hb, one_lt_mul_of_lt_of_le ha hb]

Premises used: one_lt_mul, one_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a b : M₀
inst_2 : MulPosMono M₀
ha : a ≤ 1
hb₀ : 0 ≤ b
hb rwa rwa₁ rwa₂ rwa₃ : b ≤ 1
⊢ 1 * b ≤ 1

Tactic:
rwa [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
rw : a * a ^ n < 1
⊢ a ^ (n + 1) < 1

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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 * a ^ n < 1

Tactic:
mul_lt_one_of_nonneg_of_lt_one_left h₀ h₁ (pow_le_one₀ h₀ h₁.le)

Premises used: mul_lt_one_of_nonneg_of_lt_one_left, LT.lt.le, pow_le_one₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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 * a ^ n < 1

Tactic:
exact mul_lt_one_of_nonneg_of_lt_one_left h₀ h₁ (pow_le_one₀ h₀ h₁.le)

Premises used: mul_lt_one_of_nonneg_of_lt_one_left, LT.lt.le, pow_le_one₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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 : ℕ
rw : a ^ n ≤ a ^ n * a
⊢ a ^ n ≤ a ^ (n + 1)

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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 * a

Tactic:
le_mul_of_one_le_right (pow_nonneg (zero_le_one.trans h) _) h

Premises used: pow_nonneg, zero_le_one, le_mul_of_one_le_right, LE.le.trans
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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 * a

Tactic:
exact le_mul_of_one_le_right (pow_nonneg (zero_le_one.trans h) _) h

Premises used: pow_nonneg, zero_le_one, le_mul_of_one_le_right, LE.le.trans
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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 : ℕ
⊢ 1 ≤ a ^ n

Tactic:
pow_zero a ▸ pow_right_mono₀ ha n.zero_le

Premises used: Nat.zero_le, Eq.rec, pow_zero, pow_right_mono₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
rw : 1 < a * a ^ n
⊢ 1 < a ^ (n + 1)

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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 * a ^ n

Tactic:
one_lt_mul_of_lt_of_le ha (one_le_pow₀ ha.le)

Premises used: one_le_pow₀, LT.lt.le, one_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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 * a ^ n

Tactic:
exact one_lt_mul_of_lt_of_le ha (one_le_pow₀ ha.le)

Premises used: one_le_pow₀, LT.lt.le, one_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
inr : ∀ (a0 : 0 ≤ a) (a1 : a ≤ 1) (mn : m ≤ n), a ^ n ≤ a ^ m
⊢ a ^ n ≤ a ^ m

Tactic:
obtain ⟨a1, nm⟩ | ⟨a0, a1, mn⟩ := h
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
m n : ℕ
inst_2 : ZeroLEOneClass M₀
inst_3 : PosMulMono M₀
a1 : 1 ≤ a
nm : n ≤ m
⊢ a ^ n ≤ a ^ m

Tactic:
pow_right_mono₀ a1 nm

Premises used: pow_right_mono₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
m n : ℕ
inst_2 : ZeroLEOneClass M₀
inst_3 : PosMulMono M₀
a1 : 1 ≤ a
nm : n ≤ m
⊢ a ^ n ≤ a ^ m

Tactic:
exact pow_right_mono₀ a1 nm

Premises used: pow_right_mono₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
m n : ℕ
inst_2 : ZeroLEOneClass M₀
inst_3 : PosMulMono M₀
a0 : 0 ≤ a
a1 : a ≤ 1
mn : m ≤ n
⊢ a ^ n ≤ a ^ m

Tactic:
pow_le_pow_of_le_one a0 a1 mn

Premises used: pow_le_pow_of_le_one
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
m n : ℕ
inst_2 : ZeroLEOneClass M₀
inst_3 : PosMulMono M₀
a0 : 0 ≤ a
a1 : a ≤ 1
mn : m ≤ n
⊢ a ^ n ≤ a ^ m

Tactic:
exact pow_le_pow_of_le_one a0 a1 mn

Premises used: pow_le_pow_of_le_one
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
m n : ℕ
inst_2 : ZeroLEOneClass M₀
inst_3 : PosMulMono M₀
ha : 1 ≤ a
hmn : m ≤ n
⊢ a ^ m ≤ a ^ n

Tactic:
pow_right_mono₀ ha hmn

Premises used: pow_right_mono₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
n : ℕ
inst_2 : ZeroLEOneClass M₀
inst_3 : PosMulMono M₀
ha : 1 ≤ a
hn : n ≠ 0
⊢ a ≤ a ^ n

Tactic:
simpa only [pow_one] using pow_le_pow_right₀ ha <| Nat.pos_iff_ne_zero.2 hn

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, pow_le_pow_right₀, pow_one
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
n : ℕ
inst_2 : ZeroLEOneClass M₀
inst_3 : PosMulMono M₀
ha : 1 ≤ a
hn : 0 < n
⊢ a ≤ a ^ n

Tactic:
le_self_pow₀ ha hn.ne'

Premises used: LT.lt.ne', le_self_pow₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a b : M₀
inst_2 : PosMulMono M₀
inst_3 : MulPosMono M₀
ha : 0 ≤ a
hab : a ≤ b
⊢ HPow.hPow (β := ℕ) a 0 ≤ HPow.hPow (β := ℕ) b 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a b : M₀
inst_2 : PosMulMono M₀
inst_3 : MulPosMono M₀
ha : 0 ≤ a
hab : a ≤ b
⊢ HPow.hPow (β := ℕ) a 1 ≤ HPow.hPow (β := ℕ) b 1

Tactic:
simpa using hab
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a b : M₀
inst_2 : PosMulMono M₀
inst_3 : MulPosMono M₀
ha : 0 ≤ a
hab : a ≤ b
n : ℕ
⊢ a ^ (n + 2) ≤ b ^ (n + 2)

Tactic:
simpa only [pow_succ']
      using mul_le_mul hab (pow_le_pow_left₀ ha hab _) (pow_succ_nonneg ha _) (ha.trans hab)

Premises used: pow_succ_nonneg, mul_le_mul, LE.le.trans, pow_succ'
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
n : ℕ
inst_2 : PosMulMono M₀
inst_3 : MulPosMono M₀
⊢ MonotoneOn (β := M₀) (fun (a : M₀) ↦ a ^ n) {x : M₀ | 0 ≤ x}

Tactic:
fun _a ha _b _ hab ↦ pow_le_pow_left₀ ha hab _

Premises used: pow_le_pow_left₀, MonotoneOn
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
inst_2 : PosMulMono M₀
ha : 0 ≤ a
⊢ Monotone (β := M₀) fun (x : M₀) ↦ a * x

Tactic:
fun _ _ h ↦ mul_le_mul_of_nonneg_left h ha

Premises used: Monotone, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
inst_2 : MulPosMono M₀
ha : 0 ≤ a
⊢ Monotone (β := M₀) fun (x : M₀) ↦ x * a

Tactic:
fun _ _ h ↦ mul_le_mul_of_nonneg_right h ha

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

Tactic:
(monotone_mul_right_of_nonneg ha).comp hf

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

Tactic:
(monotone_mul_left_of_nonneg ha).comp hf

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

Tactic:
(monotone_mul_right_of_nonneg ha).comp_antitone hf

Premises used: monotone_mul_right_of_nonneg, Monotone.comp_antitone
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
inst_2 : Preorder α
f : α → M₀
inst_3 : PosMulMono M₀
hf : Antitone f
ha : 0 ≤ a
⊢ Antitone.{u_1, u_2} (β := M₀) fun (x : α) ↦ a * f x

Tactic:
(monotone_mul_left_of_nonneg ha).comp_antitone hf

Premises used: Monotone.comp_antitone, monotone_mul_left_of_nonneg
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a b : M₀
inst_2 : PosMulStrictMono M₀
inst_3 : MulPosMono M₀
ha : 0 ≤ a
hab : a < b
⊢ a * a < b * b

Tactic:
mul_lt_mul' hab.le hab ha <| ha.trans_lt hab

Premises used: LT.lt.le, mul_lt_mul', LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
inst_2 : PosMulStrictMono M₀
inst_3 : MulPosMono M₀
⊢ StrictMonoOn (β := M₀) (fun (x : M₀) ↦ x * x) {x : M₀ | 0 ≤ x}

Tactic:
fun _ hx _ _ hxy ↦ mul_self_lt_mul_self hx hxy

Premises used: mul_self_lt_mul_self, StrictMonoOn
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
rw : 0 < c * d
⊢ a * b < c * d

Tactic:
rw [← b0, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
⊢ 0 < c * d

Tactic:
mul_pos (h3.trans_lt h1) (h4.trans_lt h2)

Premises used: mul_pos, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
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
⊢ 0 < c * d

Tactic:
exact mul_pos (h3.trans_lt h1) (h4.trans_lt h2)

Premises used: mul_pos, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a b : M₀
inst_2 : MulPosStrictMono M₀
ha : 0 < a
hb : 1 < b
⊢ a < b * a

Tactic:
simpa using mul_lt_mul_of_pos_right hb ha

Premises used: mul_lt_mul_of_pos_right
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a b : M₀
inst_2 : PosMulStrictMono M₀
ha : 0 < a
hb : 1 < b
⊢ a < a * b

Tactic:
simpa using mul_lt_mul_of_pos_left hb ha

Premises used: 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 : ZeroLEOneClass M₀
inst_3 : MulPosStrictMono M₀
ha : 1 < a
⊢ a < a * a

Tactic:
lt_mul_left (ha.trans_le' zero_le_one) ha

Premises used: LT.lt.trans_le', zero_le_one, lt_mul_left
-- 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
⊢ 0 < HPow.hPow (β := ℕ) a 2

Tactic:
simpa only [sq] using mul_pos ha ha

Premises used: sq, mul_pos
-- 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
⊢ 0 < a ^ HAdd.hAdd (α := ℕ) 0 1

Tactic:
simpa using ha
-- 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₀
inst_3 : ZeroLEOneClass M₀
ha : 0 < a
⊢ Nontrivial M₀

Tactic:
nontriviality
-- 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₀
inst_3 : ZeroLEOneClass M₀
ha : 0 < a
inst_4 : Nontrivial M₀
rw : LT.lt.{u_2} (α := M₀) 0 1
⊢ 0 < HPow.hPow (β := ℕ) a 0

Tactic:
rw [pow_zero]

Premises used: pow_zero
-- 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₀
inst_3 : ZeroLEOneClass M₀
ha : 0 < a
inst_4 : Nontrivial M₀
⊢ LT.lt.{u_2} (α := M₀) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one
-- 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₀
inst_3 : ZeroLEOneClass M₀
ha : 0 < a
inst_4 : Nontrivial M₀
⊢ LT.lt.{u_2} (α := M₀) 0 1

Tactic:
exact zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a b : M₀
inst_2 : PosMulStrictMono M₀
inst_3 : MulPosMono M₀
hab : a < b
ha : 0 ≤ a
h : Ne (α := ℕ) 1 0
⊢ HPow.hPow (β := ℕ) a 1 < HPow.hPow (β := ℕ) b 1

Tactic:
simpa using hab
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a b : M₀
inst_2 : PosMulStrictMono M₀
inst_3 : MulPosMono M₀
hab : a < b
ha : 0 ≤ a
n : ℕ
h : n + 2 ≠ 0
⊢ a ^ (n + 2) < b ^ (n + 2)

Tactic:
simpa only [pow_succ] using mul_lt_mul_of_le_of_lt_of_nonneg_of_pos
      (pow_le_pow_left₀ ha hab.le _) hab ha (pow_succ_pos (ha.trans_lt hab) _)

Premises used: mul_lt_mul_of_le_of_lt_of_nonneg_of_pos, pow_succ, pow_le_pow_left₀, LT.lt.le, pow_succ_pos, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
n : ℕ
inst_2 : PosMulStrictMono M₀
inst_3 : MulPosMono M₀
hn : n ≠ 0
⊢ StrictMonoOn (β := M₀) (fun (x : M₀) ↦ x ^ n) {a : M₀ | 0 ≤ a}

Tactic:
fun _a ha _b _ hab ↦ pow_lt_pow_left₀ hab ha hn

Premises used: pow_lt_pow_left₀, StrictMonoOn
-- 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₀
inst_3 : ZeroLEOneClass M₀
h : 1 < a
n : ℕ
⊢ a ^ n < a ^ (n + 1)

Tactic:
simpa only [one_mul, pow_succ] using lt_mul_right (pow_pos (zero_le_one.trans_lt h) _) h

Premises used: pow_pos, pow_succ, lt_mul_right, zero_le_one, LE.le.trans_lt, one_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a : M₀
m n : ℕ
inst_2 : PosMulStrictMono M₀
inst_3 : ZeroLEOneClass M₀
h : 1 < a
hmn : m < n
⊢ a ^ m < a ^ n

Tactic:
pow_right_strictMono₀ h hmn

Premises used: pow_right_strictMono₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a : M₀
m n : ℕ
inst_2 : PosMulStrictMono M₀
inst_3 : ZeroLEOneClass M₀
h : 1 < a
⊢ a ^ n < a ^ m ↔ n < m

Tactic:
(pow_right_strictMono₀ h).lt_iff_lt

Premises used: StrictMono.lt_iff_lt, pow_right_strictMono₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a : M₀
m n : ℕ
inst_2 : PosMulStrictMono M₀
inst_3 : ZeroLEOneClass M₀
h : 1 < a
⊢ a ^ n ≤ a ^ m ↔ n ≤ m

Tactic:
(pow_right_strictMono₀ h).le_iff_le

Premises used: StrictMono.le_iff_le, pow_right_strictMono₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a : M₀
m : ℕ
inst_2 : PosMulStrictMono M₀
inst_3 : ZeroLEOneClass M₀
h : 1 < a
hm : 1 < m
⊢ a < a ^ m

Tactic:
simpa only [pow_one] using pow_lt_pow_right₀ h hm

Premises used: pow_lt_pow_right₀, pow_one
-- 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₀
h₀ : 0 < a
h₁ : a < 1
n : ℕ
⊢ ZeroLEOneClass M₀

Tactic:
have : ZeroLEOneClass M₀ := ⟨(h₀.trans h₁).le⟩
-- 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₀
h₀ : 0 < a
h₁ : a < 1
n : ℕ
this : ZeroLEOneClass M₀
⊢ a ^ (n + 1) < a ^ n

Tactic:
simpa only [pow_succ, mul_one] using mul_lt_mul_of_pos_left h₁ (pow_pos h₀ n)

Premises used: pow_pos, pow_succ, mul_lt_mul_of_pos_left, mul_one
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a : M₀
m n : ℕ
inst_2 : PosMulStrictMono M₀
ha₀ : 0 < a
ha₁ : a < 1
⊢ a ^ m ≤ a ^ n ↔ n ≤ m

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

Premises used: pow_right_strictAnti₀, StrictAnti.le_iff_ge
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a : M₀
m n : ℕ
inst_2 : PosMulStrictMono M₀
h₀ : 0 < a
h₁ : a < 1
⊢ a ^ m < a ^ n ↔ n < m

Tactic:
(pow_right_strictAnti₀ h₀ h₁).lt_iff_gt

Premises used: pow_right_strictAnti₀, StrictAnti.lt_iff_gt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a : M₀
m n : ℕ
inst_2 : PosMulStrictMono M₀
h₀ : 0 < a
h₁ : a < 1
hmn : m < n
⊢ a ^ n < a ^ m

Tactic:
(pow_lt_pow_iff_right_of_lt_one₀ h₀ h₁).2 hmn

Premises used: Iff.mpr, pow_lt_pow_iff_right_of_lt_one₀
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : PartialOrder M₀
a : M₀
n : ℕ
inst_2 : PosMulStrictMono M₀
h₀ : 0 < a
h₁ : a < 1
hn : 1 < n
⊢ a ^ n < a

Tactic:
simpa only [pow_one] using pow_lt_pow_right_of_lt_one₀ h₀ h₁ hn

Premises used: pow_one, pow_lt_pow_right_of_lt_one₀