awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
contrapose! : a₂ < a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ < a₁ * b₁
⊢ a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ < b₂

Tactic:
contrapose!
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ < a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ < a₁ * b₁

Tactic:
fun h => mul_lt_mul_of_lt_of_le h.1 h.2

Premises used: And.right, And.left, mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ < a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ < a₁ * b₁

Tactic:
exact fun h => mul_lt_mul_of_lt_of_le h.1 h.2

Premises used: mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightMono α
a₁ a₂ b₁ b₂ : α
contrapose! : a₂ ≤ a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁
⊢ a₁ * b₁ ≤ a₂ * b₂ → a₁ < a₂ ∨ b₁ ≤ b₂

Tactic:
contrapose!
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ ≤ a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁

Tactic:
fun h => mul_lt_mul_of_le_of_lt h.1 h.2

Premises used: And.right, And.left, mul_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ ≤ a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁

Tactic:
exact fun h => mul_lt_mul_of_le_of_lt h.1 h.2

Premises used: mul_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
contrapose! : a₂ < a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁
⊢ a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂

Tactic:
contrapose!
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ < a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁

Tactic:
fun h => mul_lt_mul_of_lt_of_lt h.1 h.2

Premises used: And.right, And.left, mul_lt_mul_of_lt_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ < a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁

Tactic:
exact fun h => mul_lt_mul_of_lt_of_lt h.1 h.2

Premises used: mul_lt_mul_of_lt_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
inst_4 : MulLeftStrictMono α
inst_5 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₁ * b₁ < a₂ * b₂ ↔ a₁ < a₂ ∨ b₁ < b₂

Tactic:
⟨lt_or_lt_of_mul_lt_mul, fun h => ?_⟩

Premises used: lt_or_lt_of_mul_lt_mul, Iff.intro
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
inst_4 : MulLeftStrictMono α
inst_5 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
refine : ∀ (h : a₁ < a₂ ∨ b₁ < b₂), a₁ * b₁ < a₂ * b₂
⊢ a₁ * b₁ < a₂ * b₂ ↔ a₁ < a₂ ∨ b₁ < b₂

Tactic:
refine ⟨lt_or_lt_of_mul_lt_mul, fun h => ?_⟩
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
inst_4 : MulLeftStrictMono α
inst_5 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h : a₁ < a₂ ∨ b₁ < b₂
inl : ∀ (ha' : a₁ < a₂), a₁ * b₁ < a₂ * b₂
inr : ∀ (hb' : b₁ < b₂), a₁ * b₁ < a₂ * b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
rcases h with ha' | hb'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
inst_4 : MulLeftStrictMono α
inst_5 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
ha' : a₁ < a₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
mul_lt_mul_of_lt_of_le ha' hb

Premises used: mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
inst_4 : MulLeftStrictMono α
inst_5 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
ha' : a₁ < a₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
exact mul_lt_mul_of_lt_of_le ha' hb

Premises used: mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
inst_4 : MulLeftStrictMono α
inst_5 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
hb' : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
mul_lt_mul_of_le_of_lt ha hb'

Premises used: mul_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
inst_4 : MulLeftStrictMono α
inst_5 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
hb' : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
exact mul_lt_mul_of_le_of_lt ha hb'

Premises used: mul_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : MulOneClass α
inst_2 : MulLeftMono α
a b : α
hb : 1 ≤ b
⊢ min a b ≤ a * b

Tactic:
min_le_iff.2 <| Or.inl <| le_mul_of_one_le_right' hb

Premises used: Iff.mpr, min_le_iff, Or.inl, le_mul_of_one_le_right'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : MulOneClass α
inst_2 : MulRightMono α
a b : α
ha : 1 ≤ a
⊢ min a b ≤ a * b

Tactic:
min_le_iff.2 <| Or.inr <| le_mul_of_one_le_left' ha

Premises used: Iff.mpr, min_le_iff, le_mul_of_one_le_left', Or.inr
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : MulOneClass α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
ha : 1 ≤ a
hb : 1 ≤ b
⊢ max a b ≤ a * b

Tactic:
max_le_iff.2 ⟨le_mul_of_one_le_right' hb, le_mul_of_one_le_left' ha⟩

Premises used: Iff.mpr, max_le_iff, le_mul_of_one_le_left', And.intro, le_mul_of_one_le_right'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
Goal:
α : Type u
inst : LE α
inst_1 : Mul α
c : MulLeftMono α
⊢ MulLeftMono.{u} αᵒᵈ

Tactic:
⟨c.1.flip⟩

Premises used: CovariantClass.mk, CovariantClass.elim, Covariant.flip
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
Goal:
α : Type u
inst : LE α
inst_1 : Mul α
c : MulRightMono α
⊢ MulRightMono.{u} αᵒᵈ

Tactic:
⟨c.1.flip⟩

Premises used: CovariantClass.mk, CovariantClass.elim, Covariant.flip
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
Goal:
α : Type u
inst : LT α
inst_1 : Mul α
c : MulLeftReflectLT α
⊢ MulLeftReflectLT.{u} αᵒᵈ

Tactic:
⟨c.1.flip⟩

Premises used: Contravariant.flip, ContravariantClass.mk, ContravariantClass.elim
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
Goal:
α : Type u
inst : LT α
inst_1 : Mul α
c : MulLeftStrictMono α
⊢ MulLeftStrictMono.{u} αᵒᵈ

Tactic:
⟨c.1.flip⟩

Premises used: CovariantClass.mk, CovariantClass.elim, Covariant.flip
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
Goal:
α : Type u
inst : LT α
inst_1 : Mul α
c : MulRightReflectLT α
⊢ MulRightReflectLT.{u} αᵒᵈ

Tactic:
⟨c.1.flip⟩

Premises used: Contravariant.flip, ContravariantClass.mk, ContravariantClass.elim
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
Goal:
α : Type u
inst : LT α
inst_1 : Mul α
c : MulRightStrictMono α
⊢ MulRightStrictMono.{u} αᵒᵈ

Tactic:
⟨c.1.flip⟩

Premises used: CovariantClass.mk, CovariantClass.elim, Covariant.flip
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
ha : 1 ≤ a
⊢ 1 ≤ HPow.hPow (β := ℕ) a 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
ha : 1 ≤ a
k : ℕ
rw : 1 ≤ a ^ k * a
⊢ 1 ≤ a ^ (k + 1)

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
ha : 1 ≤ a
k : ℕ
⊢ 1 ≤ a ^ k * a

Tactic:
one_le_mul (one_le_pow_of_le ha k) ha

Premises used: Left.one_le_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
ha : 1 ≤ a
k : ℕ
⊢ 1 ≤ a ^ k * a

Tactic:
exact one_le_mul (one_le_pow_of_le ha k) ha

Premises used: Left.one_le_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
ha : a ≤ 1
n : ℕ
⊢ a ^ n ≤ 1

Tactic:
one_le_pow_of_le (M := Mᵒᵈ) ha n

Premises used: Left.one_le_pow_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
n : ℕ
h : a < 1
hn : n ≠ 0
rcases : ∀ (k : ℕ) (hn : k.succ ≠ 0), a ^ k.succ < 1
⊢ a ^ n < 1

Tactic:
rcases Nat.exists_eq_succ_of_ne_zero hn with ⟨k, rfl⟩

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
h : a < 1
k : ℕ
hn : k.succ ≠ 0
rw : a * a ^ k < 1
⊢ a ^ k.succ < 1

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
h : a < 1
k : ℕ
hn : k.succ ≠ 0
⊢ a * a ^ k < 1

Tactic:
mul_lt_one_of_lt_of_le h (pow_le_one_of_le h.le _)

Premises used: LT.lt.le, Left.mul_lt_one_of_lt_of_le, Left.pow_le_one_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
h : a < 1
k : ℕ
hn : k.succ ≠ 0
⊢ a * a ^ k < 1

Tactic:
exact mul_lt_one_of_lt_of_le h (pow_le_one_of_le h.le _)

Premises used: LT.lt.le, Left.mul_lt_one_of_lt_of_le, Left.pow_le_one_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
ha : 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.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
ha : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ n * a

Tactic:
le_mul_of_one_le_right' ha

Premises used: le_mul_of_one_le_right'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
ha : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ n * a

Tactic:
exact le_mul_of_one_le_right' ha

Premises used: le_mul_of_one_le_right'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
n m : ℕ
ha : 1 ≤ a
h : n ≤ m
⊢ a ^ n ≤ a ^ m

Tactic:
pow_right_monotone ha h

Premises used: pow_right_monotone
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
n m : ℕ
ha : a ≤ 1
h : n ≤ m
⊢ a ^ m ≤ a ^ n

Tactic:
pow_le_pow_right' (M := Mᵒᵈ) ha h

Premises used: pow_le_pow_right'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
ha : 1 < a
k : ℕ
hk : k ≠ 0
⊢ 1 < a ^ k

Tactic:
pow_lt_one' (M := Mᵒᵈ) ha hk

Premises used: pow_lt_one'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
n : ℕ
ha : 1 ≤ a
hn : n ≠ 0
⊢ a ≤ a ^ n

Tactic:
simpa using pow_le_pow_right' ha (Nat.one_le_iff_ne_zero.2 hn)

Premises used: Iff.mpr, Nat.one_le_iff_ne_zero, pow_le_pow_right'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
a : M
ha : 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.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
a : M
ha : 1 < a
n : ℕ
⊢ a ^ n < a ^ n * a

Tactic:
lt_mul_of_one_lt_right' (a ^ n) ha

Premises used: lt_mul_of_one_lt_right', HPow.hPow
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
a : M
ha : 1 < a
n : ℕ
⊢ a ^ n < a ^ n * a

Tactic:
exact lt_mul_of_one_lt_right' (a ^ n) ha

Premises used: lt_mul_of_one_lt_right', HPow.hPow
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
a : M
n m : ℕ
ha : 1 < a
h : n < m
⊢ a ^ n < a ^ m

Tactic:
pow_right_strictMono' ha h

Premises used: pow_right_strictMono'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
x : M
hx : 1 ≤ x
n : ℕ
rw : 1 ≤ x ^ n * x
⊢ 1 ≤ x ^ (n + 1)

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ n * x

Tactic:
Right.one_le_mul (Right.one_le_pow_of_le hx) hx

Premises used: Right.one_le_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ n * x

Tactic:
exact Right.one_le_mul (Right.one_le_pow_of_le hx) hx

Premises used: Right.one_le_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
x : M
hx : x ≤ 1
n : ℕ
⊢ x ^ n ≤ 1

Tactic:
Right.one_le_pow_of_le (M := Mᵒᵈ) hx

Premises used: Right.one_le_pow_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
n : ℕ
x : M
hn : 0 < n
h : x < 1
rcases : ∀ (k : ℕ) (hn : 0 < k.succ), x ^ k.succ < 1
⊢ x ^ n < 1

Tactic:
rcases Nat.exists_eq_succ_of_ne_zero hn.ne' with ⟨k, rfl⟩

Premises used: LT.lt.ne', Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
x : M
h : x < 1
k : ℕ
hn : 0 < k.succ
rw : x ^ k * x < 1
⊢ x ^ k.succ < 1

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
x : M
h : x < 1
k : ℕ
hn : 0 < k.succ
⊢ x ^ k * x < 1

Tactic:
mul_lt_one_of_le_of_lt (pow_le_one_of_le h.le) h

Premises used: LT.lt.le, Right.mul_lt_one_of_le_of_lt, Right.pow_le_one_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
x : M
h : x < 1
k : ℕ
hn : 0 < k.succ
⊢ x ^ k * x < 1

Tactic:
exact mul_lt_one_of_le_of_lt (pow_le_one_of_le h.le) h

Premises used: LT.lt.le, Right.mul_lt_one_of_le_of_lt, Right.pow_le_one_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
h : Ne (α := ℕ) 1 0
⊢ HPow.hPow (β := ℕ) a 1 ≤ b ^ HSub.hSub (α := ℕ) 1 1 * a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
rw rw₁ : a ^ (n + 1) * a = a ^ (n + 1) * a
⊢ a ^ (n + 2) = a ^ (n + 1) * a

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
⊢ n + 1 ≠ 0

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
grw : b ^ (n + 1 - 1) * a * a ≤ b ^ n * a * a
⊢ a ^ (n + 1) * a ≤ b ^ n * a * a

Tactic:
grw [pow_le_pow_mul_of_sq_le_mul hab (by lia)]
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
⊢ b ^ (n + 1 - 1) * a * a ≤ b ^ n * a * a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
rw : b ^ n * (a * a) = b ^ n * HPow.hPow (β := ℕ) a 2
rw₁ rw₂ : b ^ n * (a * a) = b ^ n * (a * a)
⊢ b ^ n * a * a = b ^ n * HPow.hPow (β := ℕ) a 2

Tactic:
rw [mul_assoc, sq]

Premises used: mul_assoc, sq
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
grw grw₁ : b ^ n * (b * a) ≤ b ^ n * (b * a)
⊢ b ^ n * HPow.hPow (β := ℕ) a 2 ≤ b ^ n * (b * a)

Tactic:
grw [hab]
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
rw : b ^ n * b * a = b ^ (n + 1) * a
rw₁ rw₂ : b ^ (n + 1) * a = b ^ (n + 1) * a
⊢ b ^ n * (b * a) = b ^ (n + 1) * a

Tactic:
rw [← mul_assoc, ← pow_succ]

Premises used: pow_succ, mul_assoc
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
a₁ : a ^ (n + 2) = a ^ (n + 1) * a
a₂ : a ^ (n + 1) * a ≤ b ^ n * a * a
a₃ : b ^ n * a * a = b ^ n * HPow.hPow (β := ℕ) a 2
a₄ : b ^ n * HPow.hPow (β := ℕ) a 2 ≤ b ^ n * (b * a)
a₅ : b ^ n * (b * a) = b ^ (n + 1) * a
⊢ a ^ (n + 2) ≤ b ^ (n + 2 - 1) * a

Tactic:
calc
      a ^ (n + 2) = a ^ (n + 1) * a := by rw [pow_succ]
      _ ≤ b ^ n * a * a := by grw [pow_le_pow_mul_of_sq_le_mul hab (by lia)]; simp
      _ = b ^ n * a ^ 2 := by rw [mul_assoc, sq]
      _ ≤ b ^ n * (b * a) := by grw [hab]
      _ = b ^ (n + 1) * a := by rw [← mul_assoc, ← pow_succ]

Premises used: HMul.hMul, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
β : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : Preorder β
inst_3 : MulLeftStrictMono M
inst_4 : MulRightStrictMono M
f : β → M
hf : StrictMono f
h : Ne (α := ℕ) 1 0
⊢ StrictMono.{u_1, u_3} (β := M) fun (x : β) ↦ HPow.hPow (β := ℕ) (f x) 1

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
β : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : Preorder β
inst_3 : MulLeftStrictMono M
inst_4 : MulRightStrictMono M
f : β → M
hf : StrictMono f
n : ℕ
h : n.succ.succ ≠ 0
⊢ StrictMono.{u_1, u_3} (β := M) fun (x : β) ↦ f x ^ n.succ.succ

Tactic:
simpa only [pow_succ] using (hf.pow_const n.succ_ne_zero).mul' hf

Premises used: pow_succ, StrictMono.mul', Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulRightStrictMono M
n : ℕ
hn : n ≠ 0
⊢ StrictMono (β := M) fun (x : M) ↦ x ^ n

Tactic:
strictMono_id.pow_const hn

Premises used: strictMono_id, StrictMono.pow_const
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulRightStrictMono M
n : ℕ
hn : n ≠ 0
a b : M
hab : a < b
⊢ a ^ n < b ^ n

Tactic:
pow_left_strictMono hn hab

Premises used: pow_left_strictMono
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
a b : M
hab : a ≤ b
⊢ HPow.hPow (β := ℕ) a 0 ≤ HPow.hPow (β := ℕ) b 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
a b : M
hab : a ≤ b
k : ℕ
rw : a ^ k * a ≤ b ^ k * b
⊢ a ^ (k + 1) ≤ b ^ (k + 1)

Tactic:
rw [pow_succ, pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
a b : M
hab : a ≤ b
k : ℕ
⊢ a ^ k * a ≤ b ^ k * b

Tactic:
mul_le_mul' (pow_le_pow_left' hab k) hab

Premises used: mul_le_mul'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
a b : M
hab : a ≤ b
k : ℕ
⊢ a ^ k * a ≤ b ^ k * b

Tactic:
exact mul_le_mul' (pow_le_pow_left' hab k) hab

Premises used: mul_le_mul'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
β : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : Preorder β
inst_3 : MulLeftMono M
inst_4 : MulRightMono M
f : β → M
hf : Monotone f
⊢ Monotone.{u_1, u_3} (β := M) fun (a : β) ↦ HPow.hPow (β := ℕ) (f a) 0

Tactic:
simpa using monotone_const

Premises used: monotone_const
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
β : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : Preorder β
inst_3 : MulLeftMono M
inst_4 : MulRightMono M
f : β → M
hf : Monotone f
n : ℕ
simp_rw : Monotone.{u_1, u_3} (β := M) fun (a : β) ↦ f a ^ n * f a
⊢ Monotone.{u_1, u_3} (β := M) fun (a : β) ↦ f a ^ (n + 1)

Tactic:
simp_rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
β : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : Preorder β
inst_3 : MulLeftMono M
inst_4 : MulRightMono M
f : β → M
hf : Monotone f
n : ℕ
⊢ Monotone.{u_1, u_3} (β := M) fun (a : β) ↦ f a ^ n * f a

Tactic:
(Monotone.pow_const hf _).mul' hf

Premises used: Monotone.mul'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
β : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : Preorder β
inst_3 : MulLeftMono M
inst_4 : MulRightMono M
f : β → M
hf : Monotone f
n : ℕ
⊢ Monotone.{u_1, u_3} (β := M) fun (a : β) ↦ f a ^ n * f a

Tactic:
exact (Monotone.pow_const hf _).mul' hf

Premises used: Monotone.mul'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
n : ℕ
⊢ Monotone (β := M) fun (a : M) ↦ a ^ n

Tactic:
monotone_id.pow_const _

Premises used: monotone_id, Monotone.pow_const
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
a b : M
hab : a ≤ b
ht : 1 ≤ b
m n : ℕ
hmn : m ≤ n
⊢ a ^ m ≤ b ^ n

Tactic:
(pow_le_pow_left' hab _).trans (pow_le_pow_right' ht hmn)

Premises used: LE.le.trans, pow_le_pow_left', pow_le_pow_right'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Goal:
M : Type u_3
inst : Monoid M
inst_1 : SemilatticeSup M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
a b : M
n : ℕ
⊢ a ^ n ⊔ b ^ n ≤ (a ⊔ b) ^ n

Tactic:
sup_le (pow_le_pow_left' le_sup_left _) (pow_le_pow_left' le_sup_right _)

Premises used: le_sup_left, le_sup_right, sup_le, pow_le_pow_left'