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
n : ℕ
a : G
ha : a ≤ 1
inl : 1 ≤ a⁻¹ ^ n
⊢ |a ^ n|ₘ = |a|ₘ ^ n

Tactic:
rw [mabs_of_le_one ha, ← mabs_inv, ← inv_pow, mabs_of_one_le]

Premises used: mabs_of_one_le, inv_pow, mabs_of_le_one, mabs_inv
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ 1 ≤ a⁻¹ ^ n

Tactic:
one_le_pow_of_one_le' (one_le_inv'.2 ha) n

Premises used: Iff.mpr, one_le_pow_of_one_le', one_le_inv'
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ 1 ≤ a⁻¹ ^ n

Tactic:
exact one_le_pow_of_one_le' (one_le_inv'.2 ha) n

Premises used: Iff.mpr, one_le_pow_of_one_le', one_le_inv'
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
n : ℕ
a : G
ha : 1 ≤ a
inr : |a ^ n|ₘ = a ^ n
inr₁ inr₂ : a ^ n = a ^ n
⊢ |a ^ n|ₘ = |a|ₘ ^ n

Tactic:
rw [mabs_of_one_le ha, mabs_of_one_le (one_le_pow_of_one_le' ha n)]

Premises used: mabs_of_one_le, one_le_pow_of_one_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 : G
hab : a ≤ b
inl : ∀ (ha : 1 ≤ a), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
inr : ∀ (ha : a < 1), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
obtain ha | ha := 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 b : G
hab : a ≤ b
ha : 1 ≤ a
inl : ∀ (hb : 1 ≤ b), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
inl₁ : ∀ (hb : b < 1), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
obtain hb | hb := le_or_gt 1 b

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 b : G
hab : a ≤ b
ha : a < 1
inr : ∀ (hb : 1 ≤ b), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
inr₁ : ∀ (hb : b < 1), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
obtain hb | hb := le_or_gt 1 b

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 b : G
hab : a ≤ b
ha : 1 ≤ a
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
simp [ha, hb, mabs_of_one_le, one_le_mul ha hb]

Premises used: mabs_of_one_le, one_le_mul
-- 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
hab : a ≤ b
ha : 1 ≤ a
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
(lt_irrefl (1 : G) <| ha.trans_lt <| hab.trans_lt hb).elim

Premises used: lt_irrefl, False.elim, OfNat.ofNat, LE.le.trans_lt
-- 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
hab : a ≤ b
ha : 1 ≤ a
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
exact (lt_irrefl (1 : G) <| ha.trans_lt <| hab.trans_lt hb).elim

Premises used: lt_irrefl, False.elim, OfNat.ofNat, LE.le.trans_lt
-- 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
hab : a ≤ b
ha : a < 1
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
simp [ha.le, hb.le, mabs_of_le_one, mul_le_one', mul_comm]

Premises used: LT.lt.le, mabs_of_le_one, mul_comm, mul_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 b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
⊢ (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)

Tactic:
simp [ha.le, ha.not_ge, hb, mabs_of_le_one, mabs_of_one_le]

Premises used: mabs_of_one_le, LT.lt.le, mabs_of_le_one, LT.lt.not_ge
-- 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
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
⊢ (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)

Tactic:
have : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔
    (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1) := by
    simp [ha.le, ha.not_ge, hb, mabs_of_le_one, mabs_of_one_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 : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : b ≤ 1
⊢ |a * b|ₘ = a⁻¹ * b

Tactic:
simp only [h.antisymm hb, mabs_of_lt_one ha, mul_one]

Premises used: mabs_of_lt_one, LE.le.antisymm, mul_one
-- 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
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
inr : ∀ (h : |a * b|ₘ = a⁻¹ * b), b ≤ 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
refine this.mp ⟨fun h ↦ ?_, fun h ↦ by simp only [h.antisymm hb, mabs_of_lt_one ha, mul_one]⟩

Premises used: Iff.intro, 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 b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
inr : ∀ (ab : a * b ≤ 1), b ≤ 1
inr₁ : ∀ (ab : 1 < a * b), b ≤ 1
⊢ b ≤ 1

Tactic:
obtain ab | ab := le_or_gt (a * b) 1

Premises used: HMul.hMul, 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 b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : a * b ≤ 1
⊢ b ≤ 1

Tactic:
(eq_one_of_inv_eq' ?_).le

Premises used: Eq.le, eq_one_of_inv_eq'
-- 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
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : a * b ≤ 1
inr : b⁻¹ = b
⊢ b ≤ 1

Tactic:
refine (eq_one_of_inv_eq' ?_).le

Premises used: Eq.le, eq_one_of_inv_eq'
-- 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
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : a * b ≤ 1
inr : ∀ (h : (a * b)⁻¹ = a⁻¹ * b) (ab : a * b ≤ 1), b⁻¹ = b
inr₁ : ∀ (h : b⁻¹ * a⁻¹ = a⁻¹ * b) (ab : a * b ≤ 1), b⁻¹ = b
inr₂ : ∀ (h : a⁻¹ * b⁻¹ = a⁻¹ * b) (ab : a * b ≤ 1), b⁻¹ = b
inr₃ inr₄ inr₅ inr₆ : ∀ (h : b⁻¹ = b) (ab : a * b ≤ 1), b⁻¹ = b
⊢ b⁻¹ = b

Tactic:
rwa [mabs_of_le_one ab, mul_inv_rev, mul_comm, mul_right_inj] at h

Premises used: mabs_of_le_one, mul_right_inj, mul_comm, mul_inv_rev
-- 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
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : 1 < a * b
⊢ a = a⁻¹

Tactic:
rw [mabs_of_one_lt ab, mul_left_inj] at h

Premises used: mul_left_inj, mabs_of_one_lt
-- 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
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : 1 < a * b
h₁ : a = a⁻¹
⊢ 1 < a * b

Tactic:
rw [mabs_of_one_lt ab, mul_left_inj] at h

Premises used: mul_left_inj, mabs_of_one_lt
-- 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
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : a = a⁻¹
ab : 1 < a * b
⊢ LT.lt.{u_1} (α := G) 1 1

Tactic:
rw [eq_one_of_inv_eq' h.symm] at ha

Premises used: Eq.symm, eq_one_of_inv_eq'
-- 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
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : a = a⁻¹
ab : 1 < a * b
ha₁ : LT.lt.{u_1} (α := G) 1 1
⊢ 1 ≤ b

Tactic:
rw [eq_one_of_inv_eq' h.symm] at ha

Premises used: Eq.symm, eq_one_of_inv_eq'
-- 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
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : a = a⁻¹
ab : 1 < a * b
ha₁ : LT.lt.{u_1} (α := G) 1 1
hb₁ : 1 ≤ b
⊢ (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)

Tactic:
rw [eq_one_of_inv_eq' h.symm] at ha

Premises used: Eq.symm, eq_one_of_inv_eq'
-- 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
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : a = a⁻¹
ab : 1 < a * b
ha₁ : LT.lt.{u_1} (α := G) 1 1
hb₁ : 1 ≤ b
this₁ : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
⊢ a = a⁻¹

Tactic:
rw [eq_one_of_inv_eq' h.symm] at ha

Premises used: Eq.symm, eq_one_of_inv_eq'
-- 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
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : a = a⁻¹
ab : 1 < a * b
ha₁ : LT.lt.{u_1} (α := G) 1 1
hb₁ : 1 ≤ b
this₁ : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h₁ : a = a⁻¹
⊢ 1 < a * b

Tactic:
rw [eq_one_of_inv_eq' h.symm] at ha

Premises used: Eq.symm, eq_one_of_inv_eq'
-- 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
hab : a ≤ b
ha : LT.lt.{u_1} (α := G) 1 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : a = a⁻¹
ab : 1 < a * b
⊢ b ≤ 1

Tactic:
cases ha.false

Premises used: LT.lt.false
-- 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
inl : ∀ (ab : a ≤ b), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
inr : ∀ (ab : b ≤ a), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
obtain ab | ab := le_total a b

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 : G
ab : a ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
mabs_mul_eq_mul_mabs_le ab

Premises used: _private.0.mabs_mul_eq_mul_mabs_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 : G
ab : a ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
exact mabs_mul_eq_mul_mabs_le ab

Premises used: _private.0.mabs_mul_eq_mul_mabs_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 : G
ab : b ≤ a
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
simpa only [mul_comm, and_comm] using mabs_mul_eq_mul_mabs_le ab

Premises used: _private.0.mabs_mul_eq_mul_mabs_le, and_comm, mul_comm
-- 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
rw : a ≤ b ∧ a⁻¹ ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b
rw₁ : a⁻¹ ≤ b ∧ a ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b
rw₂ rw₃ : b⁻¹ ≤ a ∧ a ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b
⊢ |a|ₘ ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b

Tactic:
rw [mabs_le', and_comm, inv_le']

Premises used: inv_le', mabs_le', and_comm
-- 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
rw : a ≤ b ∨ a ≤ b⁻¹ ↔ b ≤ a⁻¹ ∨ a ≤ b
rw₁ : a ≤ b⁻¹ ∨ a ≤ b ↔ b ≤ a⁻¹ ∨ a ≤ b
rw₂ rw₃ : b ≤ a⁻¹ ∨ a ≤ b ↔ b ≤ a⁻¹ ∨ a ≤ b
⊢ a ≤ |b|ₘ ↔ b ≤ a⁻¹ ∨ a ≤ b

Tactic:
rw [le_mabs, or_comm, le_inv']

Premises used: le_mabs, le_inv', or_comm
-- 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
⊢ b⁻¹ ≤ a

Tactic:
(mabs_le.mp h).1

Premises used: mabs_le, And.left, 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 b : G
h : |a|ₘ ≤ b
⊢ a ≤ b

Tactic:
(mabs_le.mp h).2

Premises used: mabs_le, And.right, 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 b : G
⊢ |a|ₘ ≤ |b|ₘ * |b * a|ₘ

Tactic:
simpa using mabs_mul_le b⁻¹ (b * a)

Premises used: HMul.hMul, mabs_mul_le, Inv.inv
-- 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
rw : |a * b⁻¹|ₘ ≤ |a|ₘ * |b⁻¹|ₘ
⊢ |a / b|ₘ ≤ |a|ₘ * |b|ₘ

Tactic:
rw [div_eq_mul_inv, ← mabs_inv b]

Premises used: div_eq_mul_inv, mabs_inv
-- 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
⊢ |a * b⁻¹|ₘ ≤ |a|ₘ * |b⁻¹|ₘ

Tactic:
mabs_mul_le a _

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 : G
⊢ |a * b⁻¹|ₘ ≤ |a|ₘ * |b⁻¹|ₘ

Tactic:
exact mabs_mul_le a _

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 c : G
rw : c⁻¹ ≤ a / b ∧ a / b ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
rw₁ : b ≤ a * c ∧ a / b ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
rw₂ : b ≤ a * c ∧ a ≤ b * c ↔ a ≤ b * c ∧ b / a ≤ c
rw₃ : a ≤ b * c ∧ b ≤ a * c ↔ a ≤ b * c ∧ b / a ≤ c
rw₄ rw₅ : a ≤ b * c ∧ b ≤ a * c ↔ a ≤ b * c ∧ b ≤ a * c
⊢ |a / b|ₘ ≤ c ↔ a / b ≤ c ∧ b / a ≤ c

Tactic:
rw [mabs_le, inv_le_div_iff_le_mul, div_le_iff_le_mul', and_comm, div_le_iff_le_mul']

Premises used: mabs_le, and_comm, div_le_iff_le_mul', inv_le_div_iff_le_mul
-- 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
rw : c⁻¹ < a / b ∧ a / b < c ↔ a / b < c ∧ b / a < c
rw₁ : b < a * c ∧ a / b < c ↔ a / b < c ∧ b / a < c
rw₂ : b < a * c ∧ a < b * c ↔ a < b * c ∧ b / a < c
rw₃ : a < b * c ∧ b < a * c ↔ a < b * c ∧ b / a < c
rw₄ rw₅ : a < b * c ∧ b < a * c ↔ a < b * c ∧ b < a * c
⊢ |a / b|ₘ < c ↔ a / b < c ∧ b / a < c

Tactic:
rw [mabs_lt, inv_lt_div_iff_lt_mul', div_lt_iff_lt_mul', and_comm, div_lt_iff_lt_mul']

Premises used: div_lt_iff_lt_mul', and_comm, mabs_lt, inv_lt_div_iff_lt_mul'
-- 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
h : |a / b|ₘ ≤ c
⊢ b / c ≤ a

Tactic:
div_le_comm.1 <| (mabs_div_le_iff.1 h).2

Premises used: div_le_comm, And.right, Iff.mp, 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 c : G
h : |a / b|ₘ ≤ c
⊢ a / c ≤ b

Tactic:
div_le_of_mabs_div_le_left (mabs_div_comm a b ▸ h)

Premises used: mabs_div_comm, Eq.rec, div_le_of_mabs_div_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
h : |a / b|ₘ < c
⊢ b / c < a

Tactic:
div_lt_comm.1 <| (mabs_div_lt_iff.1 h).2

Premises used: And.right, div_lt_comm, Iff.mp, mabs_div_lt_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 c : G
h : |a / b|ₘ < c
⊢ a / c < b

Tactic:
div_lt_of_mabs_div_lt_left (mabs_div_comm a b ▸ h)

Premises used: mabs_div_comm, Eq.rec, div_lt_of_mabs_div_lt_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 : G
rw rw₁ : |a|ₘ = |a|ₘ
⊢ |a|ₘ = |a / b * b|ₘ

Tactic:
rw [div_mul_cancel]

Premises used: div_mul_cancel
-- 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
⊢ |a|ₘ / |b|ₘ ≤ |a * b|ₘ

Tactic:
mabs_inv b ▸ div_inv_eq_mul a b ▸ mabs_div_mabs_le_mabs_div a b⁻¹

Premises used: Eq.rec, Inv.inv, mabs_inv, div_inv_eq_mul, mabs_div_mabs_le_mabs_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 : G
rw : |b|ₘ / |a|ₘ ≤ |b / a|ₘ
⊢ |b|ₘ / |a|ₘ ≤ |a / b|ₘ

Tactic:
rw [mabs_div_comm]

Premises used: mabs_div_comm
-- 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
⊢ |b|ₘ / |a|ₘ ≤ |b / a|ₘ

Tactic:
apply mabs_div_mabs_le_mabs_div

Premises used: mabs_div_mabs_le_mabs_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 n : G
one_le_a : 1 ≤ a
a_le_n : a ≤ n
one_le_b : 1 ≤ b
b_le_n : b ≤ n
rw : a ≤ n * b ∧ b ≤ n * a
⊢ |a / b|ₘ ≤ n

Tactic:
rw [mabs_div_le_iff, div_le_iff_le_mul, div_le_iff_le_mul]

Premises used: div_le_iff_le_mul, 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 n : G
one_le_a : 1 ≤ a
a_le_n : a ≤ n
one_le_b : 1 ≤ b
b_le_n : b ≤ n
⊢ a ≤ n * b ∧ b ≤ n * a

Tactic:
⟨le_mul_of_le_of_one_le a_le_n one_le_b, le_mul_of_le_of_one_le b_le_n one_le_a⟩

Premises used: le_mul_of_le_of_one_le, And.intro
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b n : G
one_le_a : 1 ≤ a
a_le_n : a ≤ n
one_le_b : 1 ≤ b
b_le_n : b ≤ n
⊢ a ≤ n * b ∧ b ≤ n * a

Tactic:
exact ⟨le_mul_of_le_of_one_le a_le_n one_le_b, le_mul_of_le_of_one_le b_le_n one_le_a⟩
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b n : G
one_le_a : 1 ≤ a
a_lt_n : a < n
one_le_b : 1 ≤ b
b_lt_n : b < n
rw : a < n * b ∧ b < n * a
⊢ |a / b|ₘ < n

Tactic:
rw [mabs_div_lt_iff, div_lt_iff_lt_mul, div_lt_iff_lt_mul]

Premises used: mabs_div_lt_iff, div_lt_iff_lt_mul
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b n : G
one_le_a : 1 ≤ a
a_lt_n : a < n
one_le_b : 1 ≤ b
b_lt_n : b < n
⊢ a < n * b ∧ b < n * a

Tactic:
⟨lt_mul_of_lt_of_one_le a_lt_n one_le_b, lt_mul_of_lt_of_one_le b_lt_n one_le_a⟩

Premises used: And.intro, lt_mul_of_lt_of_one_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 n : G
one_le_a : 1 ≤ a
a_lt_n : a < n
one_le_b : 1 ≤ b
b_lt_n : b < n
⊢ a < n * b ∧ b < n * a

Tactic:
exact ⟨lt_mul_of_lt_of_one_le a_lt_n one_le_b, lt_mul_of_lt_of_one_le b_lt_n one_le_a⟩
-- 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
hb : 1 ≤ b
⊢ |a|ₘ = b ↔ a = b ∨ a = b⁻¹

Tactic:
⟨eq_or_eq_inv_of_mabs_eq, ?_⟩

Premises used: eq_or_eq_inv_of_mabs_eq, Iff.intro
-- 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
hb : 1 ≤ b
refine : a = b ∨ a = b⁻¹ → |a|ₘ = b
⊢ |a|ₘ = b ↔ a = b ∨ a = b⁻¹

Tactic:
refine ⟨eq_or_eq_inv_of_mabs_eq, ?_⟩
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
hb : 1 ≤ a
⊢ |a|ₘ = a

Tactic:
simp only [mabs_inv, mabs_of_one_le hb]

Premises used: mabs_of_one_le, mabs_inv
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
b : G
hb : 1 ≤ b
⊢ |b⁻¹|ₘ = b

Tactic:
simp only [mabs_inv, mabs_of_one_le hb]

Premises used: mabs_of_one_le, mabs_inv
-- 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
hab : a ≤ b
hbc : b ≤ c
⊢ b ≤ max |a|ₘ |c|ₘ

Tactic:
simp [hbc.trans (le_mabs_self c)]

Premises used: le_mabs_self, LE.le.trans
-- 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
hab : a ≤ b
hbc : b ≤ c
⊢ b⁻¹ ≤ max |a|ₘ |c|ₘ

Tactic:
simp [(inv_le_inv_iff.mpr hab).trans (inv_le_mabs a)]

Premises used: Iff.mpr, inv_le_mabs, inv_le_inv_iff, LE.le.trans
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
a b : G
⊢ min |a|ₘ |b|ₘ ≤ |max a b|ₘ

Tactic:
(le_total a b).elim (fun h => (min_le_right _ _).trans_eq <| congr_arg _ (max_eq_right h).symm)
    fun h => (min_le_left _ _).trans_eq <| congr_arg _ (max_eq_left h).symm

Premises used: LE.le.trans_eq, max_eq_left, le_total, congr_arg, max_eq_right, min_le_left, min_le_right, Or.elim, Eq.symm, mabs
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
a b : G
⊢ min |a|ₘ |b|ₘ ≤ |min a b|ₘ

Tactic:
(le_total a b).elim (fun h => (min_le_left _ _).trans_eq <| congr_arg _ (min_eq_left h).symm)
    fun h => (min_le_right _ _).trans_eq <| congr_arg _ (min_eq_right h).symm

Premises used: LE.le.trans_eq, le_total, min_eq_right, congr_arg, min_le_left, min_eq_left, min_le_right, Or.elim, Eq.symm, mabs
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
a b : G
⊢ |max a b|ₘ ≤ max |a|ₘ |b|ₘ

Tactic:
(le_total a b).elim (fun h => (congr_arg _ <| max_eq_right h).trans_le <| le_max_right _ _)
    fun h => (congr_arg _ <| max_eq_left h).trans_le <| le_max_left _ _

Premises used: le_max_right, Eq.trans_le, max_eq_left, le_total, congr_arg, max_eq_right, Or.elim, le_max_left, mabs
-- Module: Mathlib.Algebra.Order.Group.Abs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
a b : G
⊢ |min a b|ₘ ≤ max |a|ₘ |b|ₘ

Tactic:
(le_total a b).elim (fun h => (congr_arg _ <| min_eq_left h).trans_le <| le_max_left _ _) fun h =>
    (congr_arg _ <| min_eq_right h).trans_le <| le_max_right _ _

Premises used: le_max_right, Eq.trans_le, le_total, min_eq_right, congr_arg, min_eq_left, Or.elim, le_max_left, mabs
-- 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:
div_eq_one.1 <| mabs_eq_one.1 h

Premises used: mabs_eq_one, div_eq_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 b c : G
rw rw₁ : |a / c|ₘ = |a / c|ₘ
⊢ |a / c|ₘ = |a / b * (b / c)|ₘ

Tactic:
rw [div_mul_div_cancel]

Premises used: div_mul_div_cancel