awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
inl : ∀ (h : d ≤ b), |b / d|ₘ ≤ max (c / d) (d / a)
inr : ∀ (h : b ≤ d), |b / d|ₘ ≤ max (c / d) (d / a)
⊢ |b / d|ₘ ≤ max (c / d) (d / a)

Tactic:
rcases le_total d b with h | h

Premises used: le_total
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : d ≤ b
inl : b / d ≤ max (c / d) (d / a)
⊢ |b / d|ₘ ≤ max (c / d) (d / a)

Tactic:
rw [mabs_of_one_le <| one_le_div'.mpr h]

Premises used: Iff.mpr, mabs_of_one_le, one_le_div'
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : d ≤ b
⊢ b / d ≤ max (c / d) (d / a)

Tactic:
le_max_of_le_left <| div_le_div_right' hcd _

Premises used: div_le_div_right', le_max_of_le_left
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : d ≤ b
⊢ b / d ≤ max (c / d) (d / a)

Tactic:
exact le_max_of_le_left <| div_le_div_right' hcd _

Premises used: div_le_div_right', le_max_of_le_left
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : b ≤ d
inr : d / b ≤ max (c / d) (d / a)
⊢ |b / d|ₘ ≤ max (c / d) (d / a)

Tactic:
rw [mabs_of_le_one <| div_le_one'.mpr h, inv_div]

Premises used: Iff.mpr, div_le_one', mabs_of_le_one, inv_div
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : b ≤ d
⊢ d / b ≤ max (c / d) (d / a)

Tactic:
le_max_of_le_right <| div_le_div_left' hac _

Premises used: div_le_div_left', le_max_of_le_right
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : b ≤ d
⊢ d / b ≤ max (c / d) (d / a)

Tactic:
exact le_max_of_le_right <| div_le_div_left' hac _

Premises used: div_le_div_left', le_max_of_le_right
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
grw : |a * b|ₘ * |c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ
grw₁ grw₂ : |a|ₘ * |b|ₘ * |c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ
⊢ |a * b * c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ

Tactic:
grw [mabs_mul_le, mabs_mul_le]

Premises used: mabs_mul_le
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b lb ub : G
hal : lb ≤ a
hau : a ≤ ub
hbl : lb ≤ b
hbu : b ≤ ub
⊢ |a / b|ₘ ≤ ub / lb

Tactic:
mabs_div_le_iff.2 ⟨div_le_div'' hau hbl, div_le_div'' hbu hal⟩

Premises used: Iff.mpr, div_le_div'', And.intro, mabs_div_le_iff
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
h : |a / b|ₘ ≤ 1
⊢ a = b

Tactic:
eq_of_mabs_div_eq_one (le_antisymm h (one_le_mabs (a / b)))

Premises used: HDiv.hDiv, le_antisymm, eq_of_mabs_div_eq_one, one_le_mabs
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
x y : G
h : ∀ (ε : G), ε > 1 → |x / y|ₘ < ε
⊢ x = y

Tactic:
eq_of_mabs_div_le_one <| le_of_forall_gt h

Premises used: eq_of_mabs_div_le_one, le_of_forall_gt
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : DenselyOrdered G
x y : G
h : ∀ (ε : G), ε > 1 → |x / y|ₘ ≤ ε
⊢ x = y

Tactic:
eq_of_mabs_div_le_one <| forall_gt_imp_ge_iff_le_of_dense.mp h

Premises used: forall_gt_imp_ge_iff_le_of_dense, eq_of_mabs_div_le_one, Iff.mp
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
rw : LE.le.{u_1} (α := G) |1|ₘ 1
rw₁ rw₂ : LE.le.{u_1} (α := G) 1 1
⊢ |a / a|ₘ ≤ 1

Tactic:
rw [div_self', mabs_one]

Premises used: mabs_one, div_self'
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
⊢ 1 < |a / b|ₘ ↔ a ≠ b

Tactic:
not_le.symm.trans mabs_div_le_one.not

Premises used: not_le, Iff.not, Iff.trans, Iff.symm, mabs_div_le_one
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
rw : max a a⁻¹ = a ↔ 1 ≤ a
rw₁ : a⁻¹ ≤ a ↔ 1 ≤ a
rw₂ rw₃ : 1 ≤ a ↔ 1 ≤ a
⊢ |a|ₘ = a ↔ 1 ≤ a

Tactic:
rw [mabs_eq_max_inv, max_eq_left_iff, inv_le_self_iff]

Premises used: inv_le_self_iff, max_eq_left_iff, mabs_eq_max_inv
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
rw : max a a⁻¹ = a⁻¹ ↔ a ≤ 1
rw₁ : a ≤ a⁻¹ ↔ a ≤ 1
rw₂ rw₃ : a ≤ 1 ↔ a ≤ 1
⊢ |a|ₘ = a⁻¹ ↔ a ≤ 1

Tactic:
rw [mabs_eq_max_inv, max_eq_right_iff, le_inv_self_iff]

Premises used: max_eq_right_iff, mabs_eq_max_inv, le_inv_self_iff
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
inl : 1 ≤ a → |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1
inr : a < 1 → |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1
⊢ |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1

Tactic:
cases le_or_gt 1 a

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
h : 1 ≤ a
⊢ |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1

Tactic:
simp [*, le_of_lt]

Premises used: le_of_lt
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
h : a < 1
⊢ |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1

Tactic:
simp [*, le_of_lt]

Premises used: le_of_lt
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
symm : |a|ₘ = max a 1 * max a⁻¹ 1
⊢ max a 1 * max a⁻¹ 1 = |a|ₘ

Tactic:
symm
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
inl : ∀ (ha : 1 ≤ a), |a|ₘ = max a 1 * max a⁻¹ 1
inr : ∀ (ha : a ≤ 1), |a|ₘ = max a 1 * max a⁻¹ 1
⊢ |a|ₘ = max a 1 * max a⁻¹ 1

Tactic:
rcases le_total 1 a with (ha | ha)

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
ha : 1 ≤ a
⊢ |a|ₘ = max a 1 * max a⁻¹ 1

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
ha : a ≤ 1
⊢ |a|ₘ = max a 1 * max a⁻¹ 1

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
H : Type u_2
inst_3 : MulOneClass H
inst_4 : LE H
inst_5 : MulLeftMono H
inst_6 : MulRightMono H
f : G → H
a : G
h₁ : 1 ≤ f a
h₂ : 1 ≤ f (-a)
⊢ f |a| ≤ f a * f (-a)

Tactic:
(le_total a 0).rec (fun ha => (abs_of_nonpos ha).symm ▸ le_mul_of_one_le_left' h₁) fun ha =>
    (abs_of_nonneg ha).symm ▸ le_mul_of_one_le_right' h₂

Premises used: Or.rec, le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
H : Type u_2
inst_3 : MulOneClass H
inst_4 : LE H
inst_5 : MulLeftMono H
inst_6 : MulRightMono H
f : G → H
h : ∀ (x : G), 1 ≤ f x
a : G
⊢ f |a| ≤ f a * f (-a)

Tactic:
apply_abs_le_mul_of_one_le' (h _) (h _)

Premises used: apply_abs_le_mul_of_one_le'
-- Module: Mathlib.Algebra.Order.Group.Action.End
Goal:
α : Type u_1
r : α → α → Prop
f : r →r r
a : α
⊢ f • a = (f : (a : α) → α) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Action.End
Goal:
α : Type u_1
r : α → α → Prop
f : r ↪r r
a : α
⊢ f • a = (f : (a : α) → α) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Action.End
Goal:
α : Type u_1
r : α → α → Prop
f : r ≃r r
a : α
⊢ f • a = (f : (a : α) → α) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Action.Flag
Goal:
α : Type u_1
inst : Preorder α
e : α ≃o α
s : Flag α
⊢ (↑(e • s) : Set α) = e • (↑s : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Action
Goal:
M : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : Preorder α
inst_2 : CovariantClass M α HSMul.hSMul LE.le
m : M
⊢ Monotone (α := α) (HSMul.hSMul m)

Tactic:
fun _ _ => CovariantClass.elim _

Premises used: Monotone, CovariantClass.elim
-- Module: Mathlib.Algebra.Order.Group.Action
Goal:
M : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : Preorder α
inst_2 : CovariantClass M α HSMul.hSMul LE.le
m : M
a b : α
h : a ≤ b
⊢ m • a ≤ m • b

Tactic:
smul_mono_right _ h

Premises used: smul_mono_right
-- Module: Mathlib.Algebra.Order.Group.Action
Goal:
M : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : SemilatticeInf α
inst_2 : CovariantClass M α HSMul.hSMul LE.le
m : M
a₁ a₂ : α
⊢ m • (a₁ ⊓ a₂) ≤ m • a₁ ⊓ m • a₂

Tactic:
(smul_mono_right _).map_inf_le _ _

Premises used: smul_mono_right, Monotone.map_inf_le
-- Module: Mathlib.Algebra.Order.Group.Action
Goal:
ι : Sort u_1
M : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : CompleteLattice α
inst_2 : CovariantClass M α HSMul.hSMul LE.le
m : M
t : ι → α
⊢ m • iInf t ≤ ⨅ (i : ι), m • t i

Tactic:
le_iInf fun _ => smul_mono_right _ (iInf_le _ _)

Premises used: le_iInf, smul_mono_right, iInf_le
-- Module: Mathlib.Algebra.Order.Group.Action
Goal:
M : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : Preorder α
inst_2 : CovariantClass M α HSMul.hSMul LT.lt
m : M
⊢ StrictMono (α := α) (HSMul.hSMul m)

Tactic:
fun _ _ => CovariantClass.elim _

Premises used: StrictMono, CovariantClass.elim
-- Module: Mathlib.Algebra.Order.Group.Action
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
zero : a ≤ HSMul.hSMul.{u_4, u_5, u_5} (α := G) 1 a
zero₁ zero₂ : a ≤ a
⊢ a ≤ HPow.hPow (β := ℕ) g 0 • a

Tactic:
rw [pow_zero, one_smul]

Premises used: pow_zero, one_smul
-- Module: Mathlib.Algebra.Order.Group.Action
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
hn : a ≤ g ^ n • a
succ : a ≤ g • g ^ n • a
⊢ a ≤ g ^ (n + 1) • a

Tactic:
rw [pow_succ', mul_smul]

Premises used: SemigroupAction.mul_smul, pow_succ'
-- Module: Mathlib.Algebra.Order.Group.Action
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
hn : a ≤ g ^ n • a
⊢ a ≤ g • g ^ n • a

Tactic:
h.trans (smul_mono_right g hn)

Premises used: smul_mono_right, LE.le.trans
-- Module: Mathlib.Algebra.Order.Group.Action
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
hn : a ≤ g ^ n • a
⊢ a ≤ g • g ^ n • a

Tactic:
exact h.trans (smul_mono_right g hn)

Premises used: smul_mono_right, LE.le.trans
-- Module: Mathlib.Algebra.Order.Group.Action
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
zero : a ≤ HPow.hPow (β := ℕ) g 0 • a
succ : ∀ (n : ℕ) (hn : a ≤ g ^ n • a), a ≤ g ^ (n + 1) • a
⊢ a ≤ g ^ n • a

Tactic:
induction n with
  | zero => rw [pow_zero, one_smul]
  | succ n hn =>
    rw [pow_succ', mul_smul]
    exact h.trans (smul_mono_right g hn)

Premises used: pow_zero, one_smul, SemigroupAction.mul_smul, pow_succ'
-- Module: Mathlib.Algebra.Order.Group.Action
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
zero : HSMul.hSMul.{u_4, u_5, u_5} (α := G) 1 a ≤ a
zero₁ zero₂ : a ≤ a
⊢ HPow.hPow (β := ℕ) g 0 • a ≤ a

Tactic:
rw [pow_zero, one_smul]

Premises used: pow_zero, one_smul
-- Module: Mathlib.Algebra.Order.Group.Action
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
hn : g ^ n • a ≤ a
succ : g • g ^ n • a ≤ a
⊢ g ^ (n + 1) • a ≤ a

Tactic:
rw [pow_succ', mul_smul]

Premises used: SemigroupAction.mul_smul, pow_succ'
-- Module: Mathlib.Algebra.Order.Group.Action
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
hn : g ^ n • a ≤ a
⊢ g • g ^ n • a ≤ a

Tactic:
(smul_mono_right g hn).trans h

Premises used: smul_mono_right, LE.le.trans
-- Module: Mathlib.Algebra.Order.Group.Action
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
hn : g ^ n • a ≤ a
⊢ g • g ^ n • a ≤ a

Tactic:
exact (smul_mono_right g hn).trans h

Premises used: smul_mono_right, LE.le.trans
-- Module: Mathlib.Algebra.Order.Group.Action
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
zero : HPow.hPow (β := ℕ) g 0 • a ≤ a
succ : ∀ (n : ℕ) (hn : g ^ n • a ≤ a), g ^ (n + 1) • a ≤ a
⊢ g ^ n • a ≤ a

Tactic:
induction n with
  | zero => rw [pow_zero, one_smul]
  | succ n hn =>
    rw [pow_succ', mul_smul]
    exact (smul_mono_right g hn).trans h

Premises used: pow_zero, one_smul, SemigroupAction.mul_smul, pow_succ'
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : 1 < a
⊢ StrictMono.{0, u_1} (β := α) fun (n : ℤ) ↦ a ^ n

Tactic:
strictMono_int_of_lt_succ fun n ↦ ?_

Premises used: strictMono_int_of_lt_succ
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : 1 < a
refine : ∀ (n : ℤ), a ^ n < a ^ (n + 1)
⊢ StrictMono.{0, u_1} (β := α) fun (n : ℤ) ↦ a ^ n

Tactic:
refine strictMono_int_of_lt_succ fun n ↦ ?_

Premises used: strictMono_int_of_lt_succ
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : 1 < a
n : ℤ
rw : a ^ n < a ^ n * a
⊢ a ^ n < a ^ (n + 1)

Tactic:
rw [zpow_add_one]

Premises used: zpow_add_one
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
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.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
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.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : a < 1
⊢ StrictAnti.{0, u_1} (β := α) fun (n : ℤ) ↦ a ^ n

Tactic:
strictAnti_int_of_succ_lt fun n ↦ ?_

Premises used: strictAnti_int_of_succ_lt
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : a < 1
refine : ∀ (n : ℤ), a ^ (n + 1) < a ^ n
⊢ StrictAnti.{0, u_1} (β := α) fun (n : ℤ) ↦ a ^ n

Tactic:
refine strictAnti_int_of_succ_lt fun n ↦ ?_

Premises used: strictAnti_int_of_succ_lt
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : a < 1
n : ℤ
rw : a ^ n * a < a ^ n
⊢ a ^ (n + 1) < a ^ n

Tactic:
rw [zpow_add_one]

Premises used: zpow_add_one
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : a < 1
n : ℤ
⊢ a ^ n * a < a ^ n

Tactic:
mul_lt_of_lt_one_right' (a ^ n) ha

Premises used: mul_lt_of_lt_one_right', HPow.hPow
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : a < 1
n : ℤ
⊢ a ^ n * a < a ^ n

Tactic:
exact mul_lt_of_lt_one_right' (a ^ n) ha

Premises used: mul_lt_of_lt_one_right', HPow.hPow
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : 1 < a
m n : ℤ
⊢ a ^ m = a ^ n ↔ m = n

Tactic:
(zpow_right_strictMono ha).injective.eq_iff

Premises used: zpow_right_strictMono, Function.Injective.eq_iff, StrictMono.injective
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : 1 ≤ a
⊢ Monotone.{0, u_1} (β := α) fun (n : ℤ) ↦ a ^ n

Tactic:
monotone_int_of_le_succ fun n ↦ ?_

Premises used: monotone_int_of_le_succ
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : 1 ≤ a
refine : ∀ (n : ℤ), a ^ n ≤ a ^ (n + 1)
⊢ Monotone.{0, u_1} (β := α) fun (n : ℤ) ↦ a ^ n

Tactic:
refine monotone_int_of_le_succ fun n ↦ ?_

Premises used: monotone_int_of_le_succ
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : 1 ≤ a
n : ℤ
rw : a ^ n ≤ a ^ n * a
⊢ a ^ n ≤ a ^ (n + 1)

Tactic:
rw [zpow_add_one]

Premises used: zpow_add_one
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
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.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
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.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
m n : ℤ
a : α
ha : 1 ≤ a
h : m ≤ n
⊢ a ^ m ≤ a ^ n

Tactic:
zpow_right_mono ha h

Premises used: zpow_right_mono
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
m n : ℤ
a : α
ha : 1 < a
h : m < n
⊢ a ^ m < a ^ n

Tactic:
zpow_right_strictMono ha h

Premises used: zpow_right_strictMono
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
m n : ℤ
a : α
ha : 1 < a
⊢ a ^ m ≤ a ^ n ↔ m ≤ n

Tactic:
(zpow_right_strictMono ha).le_iff_le

Premises used: zpow_right_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
m n : ℤ
a : α
ha : 1 < a
⊢ a ^ m < a ^ n ↔ m < n

Tactic:
(zpow_right_strictMono ha).lt_iff_lt

Premises used: zpow_right_strictMono, StrictMono.lt_iff_lt
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
hn : 0 < n
a b : α
hab : a < b
rw : 1 < (b / a) ^ n
⊢ LT.lt.{u_1} (α := α) ((fun (x : α) ↦ x ^ n) a) ((fun (x : α) ↦ x ^ n) b)

Tactic:
rw [← one_lt_div', ← div_zpow]

Premises used: div_zpow, one_lt_div'
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
hn : 0 < n
a b : α
hab : a < b
⊢ 1 < (b / a) ^ n

Tactic:
one_lt_zpow (one_lt_div'.2 hab) hn

Premises used: Iff.mpr, one_lt_zpow, one_lt_div'
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
hn : 0 < n
a b : α
hab : a < b
⊢ 1 < (b / a) ^ n

Tactic:
exact one_lt_zpow (one_lt_div'.2 hab) hn

Premises used: Iff.mpr, one_lt_zpow, one_lt_div'
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
rw : 1 ≤ (b / a) ^ n
⊢ LE.le.{u_1} (α := α) ((fun (x : α) ↦ x ^ n) a) ((fun (x : α) ↦ x ^ n) b)

Tactic:
rw [← one_le_div', ← div_zpow]

Premises used: div_zpow, one_le_div'
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ 1 ≤ (b / a) ^ n

Tactic:
one_le_zpow (one_le_div'.2 hab) hn

Premises used: Iff.mpr, one_le_div', one_le_zpow
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ 1 ≤ (b / a) ^ n

Tactic:
exact one_le_zpow (one_le_div'.2 hab) hn

Premises used: Iff.mpr, one_le_div', one_le_zpow
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
a b : α
hn : 0 ≤ n
h : a ≤ b
⊢ a ^ n ≤ b ^ n

Tactic:
zpow_left_mono α hn h

Premises used: zpow_left_mono
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
a b : α
hn : 0 < n
h : a < b
⊢ a ^ n < b ^ n

Tactic:
zpow_left_strictMono α hn h

Premises used: zpow_left_strictMono
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
a b : α
hn : 0 < n
⊢ a ^ n ≤ b ^ n ↔ a ≤ b

Tactic:
(zpow_left_strictMono α hn).le_iff_le

Premises used: zpow_left_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
a b : α
hn : 0 < n
⊢ a ^ n < b ^ n ↔ a < b

Tactic:
(zpow_left_strictMono α hn).lt_iff_lt

Premises used: StrictMono.lt_iff_lt, zpow_left_strictMono
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
rcases : ∀ (a : α) (ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x), False
⊢ False

Tactic:
rcases exists_zpow_surjective α with ⟨a, ha⟩

Premises used: exists_zpow_surjective
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
inl : ∀ (hlt : a < 1), False
inr : ∀ (ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ HPow.hPow (α := α) 1 x), False
inr₁ : ∀ (hlt : 1 < a), False
⊢ False

Tactic:
rcases lt_trichotomy a 1 with hlt | rfl | hlt

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
hlt : a < 1
inl : ∀ (b : α) (hab : a < b) (hb : b < 1), False
⊢ False

Tactic:
rcases exists_between hlt with ⟨b, hab, hb⟩

Premises used: exists_between