awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
p : MulArchimedeanClass M → Prop
⊢ (∀ (A : MulArchimedeanClass M), p A) ↔ ∀ (a : M), p (mk a)

Tactic:
Quotient.forall

Premises used: Quotient.forall, MulArchimedeanClass.mk, Antisymmetrization, MulArchimedeanClass, MulArchimedeanOrder, toAntisymmetrization
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := M) (β := MulArchimedeanClass M) mk

Tactic:
Quotient.mk_surjective

Premises used: MulArchimedeanClass.mk, Antisymmetrization, Quotient.mk_surjective, MulArchimedeanClass, MulArchimedeanOrder, toAntisymmetrization
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
⊢ Eq.{u_1 + 1} (α := Set (MulArchimedeanClass M)) (Set.range mk) Set.univ

Tactic:
Set.range_eq_univ.mpr (mk_surjective M)

Premises used: Iff.mpr, Set.range_eq_univ, MulArchimedeanClass.mk_surjective
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
rw :
  (AntisymmRel.setoid (MulArchimedeanOrder M) fun (x1 x2 : MulArchimedeanOrder M) ↦ x1 ≤ x2 :
        MulArchimedeanOrder M → MulArchimedeanOrder M → Prop)
      ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)
      ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) b : MulArchimedeanOrder M) ↔
    (∃ (m : ℕ), |b|ₘ ≤ |a|ₘ ^ m) ∧ ∃ (n : ℕ), |a|ₘ ≤ |b|ₘ ^ n
⊢ Eq (α := MulArchimedeanClass M)
      (⟦(MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a⟧ :
        Quotient (α := MulArchimedeanOrder M)
          (AntisymmRel.setoid (MulArchimedeanOrder M) fun (x1 x2 : MulArchimedeanOrder M) ↦ x1 ≤ x2))
      (⟦(MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) b⟧ :
        Quotient (α := MulArchimedeanOrder M)
          (AntisymmRel.setoid (MulArchimedeanOrder M) fun (x1 x2 : MulArchimedeanOrder M) ↦ x1 ≤ x2)) ↔
    (∃ (m : ℕ), |b|ₘ ≤ |a|ₘ ^ m) ∧ ∃ (n : ℕ), |a|ₘ ≤ |b|ₘ ^ n

Tactic:
rw [Quotient.eq]

Premises used: Quotient.eq
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
⊢ (AntisymmRel.setoid (MulArchimedeanOrder M) fun (x1 x2 : MulArchimedeanOrder M) ↦ x1 ≤ x2 :
        MulArchimedeanOrder M → MulArchimedeanOrder M → Prop)
      ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)
      ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) b : MulArchimedeanOrder M) ↔
    (∃ (m : ℕ), |b|ₘ ≤ |a|ₘ ^ m) ∧ ∃ (n : ℕ), |a|ₘ ≤ |b|ₘ ^ n

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
α : Type u_2
f : M → α
h : ∀ (a b : M), Eq (α := MulArchimedeanClass M) (mk a) (mk b) → f a = f b
a : M
unfold : Quotient.lift f ⋯ (mk a) = f a
⊢ lift f h (mk a) = f a

Tactic:
unfold lift

Premises used: MulArchimedeanClass.lift
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
α : Type u_2
f : M → α
h : ∀ (a b : M), Eq (α := MulArchimedeanClass M) (mk a) (mk b) → f a = f b
a : M
⊢ Quotient.lift f ⋯ (mk a) = f a

Tactic:
Quotient.lift_mk f (fun _ _ h' ↦ h _ _ <| mk_eq_mk.mpr h') a

Premises used: Iff.mpr, MulArchimedeanClass.mk_eq_mk, Quotient.lift_mk
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
α : Type u_2
f : M → α
h : ∀ (a b : M), Eq (α := MulArchimedeanClass M) (mk a) (mk b) → f a = f b
a : M
⊢ Quotient.lift f ⋯ (mk a) = f a

Tactic:
exact Quotient.lift_mk f (fun _ _ h' ↦ h _ _ <| mk_eq_mk.mpr h') a

Premises used: Iff.mpr, MulArchimedeanClass.mk_eq_mk, Quotient.lift_mk
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
α : Type u_2
f : M → M → α
h :
  ∀ (a₁ b₁ a₂ b₂ : M),
    Eq (α := MulArchimedeanClass M) (mk a₁) (mk b₁) →
      Eq (α := MulArchimedeanClass M) (mk a₂) (mk b₂) → f a₁ a₂ = f b₁ b₂
a b : M
unfold : Quotient.lift₂ f ⋯ (mk a) (mk b) = f a b
⊢ lift₂ f h (mk a) (mk b) = f a b

Tactic:
unfold lift₂

Premises used: MulArchimedeanClass.lift₂
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
α : Type u_2
f : M → M → α
h :
  ∀ (a₁ b₁ a₂ b₂ : M),
    Eq (α := MulArchimedeanClass M) (mk a₁) (mk b₁) →
      Eq (α := MulArchimedeanClass M) (mk a₂) (mk b₂) → f a₁ a₂ = f b₁ b₂
a b : M
⊢ Quotient.lift₂ f ⋯ (mk a) (mk b) = f a b

Tactic:
Quotient.lift₂_mk f (fun _ _ _ _ h₁ h₂ ↦ h _ _ _ _ (mk_eq_mk.mpr h₁) (mk_eq_mk.mpr h₂)) a b

Premises used: Iff.mpr, Quotient.lift₂_mk, MulArchimedeanClass.mk_eq_mk
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
α : Type u_2
f : M → M → α
h :
  ∀ (a₁ b₁ a₂ b₂ : M),
    Eq (α := MulArchimedeanClass M) (mk a₁) (mk b₁) →
      Eq (α := MulArchimedeanClass M) (mk a₂) (mk b₂) → f a₁ a₂ = f b₁ b₂
a b : M
⊢ Quotient.lift₂ f ⋯ (mk a) (mk b) = f a b

Tactic:
exact Quotient.lift₂_mk f (fun _ _ _ _ h₁ h₂ ↦ h _ _ _ _ (mk_eq_mk.mpr h₁) (mk_eq_mk.mpr h₂)) a b

Premises used: Iff.mpr, Quotient.lift₂_mk, MulArchimedeanClass.mk_eq_mk
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
A : MulArchimedeanClass M
⊢ mk A.out = A

Tactic:
Quotient.out_eq' A

Premises used: Quotient.out_eq', Quot.out, Quotient.out, MulArchimedeanClass.mk, Antisymmetrization, MulArchimedeanClass.out, Classical.choose, MulArchimedeanClass, toAntisymmetrization
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
⊢ |a|ₘ ≤ HPow.hPow (β := ℕ) |a⁻¹|ₘ 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
⊢ |a⁻¹|ₘ ≤ HPow.hPow (β := ℕ) |a|ₘ 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
rw : Eq (α := MulArchimedeanClass M) (mk (a / b)⁻¹) (mk (b / a))
rw₁ rw₂ : Eq (α := MulArchimedeanClass M) (mk (b / a)) (mk (b / a))
⊢ Eq (α := MulArchimedeanClass M) (mk (a / b)) (mk (b / a))

Tactic:
rw [← mk_inv, inv_div]

Premises used: MulArchimedeanClass.mk_inv, inv_div
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
⊢ |a|ₘ ≤ HPow.hPow (β := ℕ) |(|a|ₘ)|ₘ 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
⊢ |(|a|ₘ)|ₘ ≤ HPow.hPow (β := ℕ) |a|ₘ 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
inst_3 : Subsingleton M
⊢ Subsingleton.{u_1 + 1} (MulArchimedeanClass M)

Tactic:
inferInstanceAs (Subsingleton (Antisymmetrization ..))

Premises used: _private.0.MulArchimedeanClass.instSubsingleton._proof_1
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
⊢ LE.le (α := MulArchimedeanClass M) (mk a) (mk b) ↔ ∃ (n : ℕ), |b|ₘ ≤ |a|ₘ ^ n

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
⊢ LT.lt (α := MulArchimedeanClass M) (mk a) (mk b) ↔ ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
ha : a ≠ 1
⊢ LE.le (α := MulArchimedeanClass M) (mk a) (mk b) ↔ ∃ (n : ℕ), |b|ₘ < |a|ₘ ^ n

Tactic:
⟨fun ⟨n, hn⟩ ↦ ⟨n + 1, hn.trans_lt ?_⟩, fun ⟨n, hn⟩ ↦ ?_⟩

Premises used: Exists, _private.0.MulArchimedeanClass.mk_le_mk_iff_lt.match_2, LE.le, MulArchimedeanClass.mk, HPow.hPow, HAdd.hAdd, LT.lt, Iff.intro, Exists.intro, OfNat.ofNat, LE.le.trans_lt, mabs, _private.0.MulArchimedeanClass.mk_le_mk_iff_lt.match_1
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
ha : a ≠ 1
refine_1 :
  LE.le (α := MulArchimedeanClass M) (mk a) (mk b) →
    ∀ (n : ℕ)
      (hn :
        |(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
              ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) b : MulArchimedeanOrder M)|ₘ ≤
          HPow.hPow (α := M)
            (|(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
                  ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)|ₘ :
              M)
            n),
      HPow.hPow (α := M)
          (|(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
                ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)|ₘ :
            M)
          n <
        |a|ₘ ^ (n + 1)
refine_2 :
  (∃ (n : ℕ), |b|ₘ < |a|ₘ ^ n) → ∀ (n : ℕ) (hn : |b|ₘ < |a|ₘ ^ n), LE.le (α := MulArchimedeanClass M) (mk a) (mk b)
⊢ LE.le (α := MulArchimedeanClass M) (mk a) (mk b) ↔ ∃ (n : ℕ), |b|ₘ < |a|ₘ ^ n

Tactic:
refine ⟨fun ⟨n, hn⟩ ↦ ⟨n + 1, hn.trans_lt ?_⟩, fun ⟨n, hn⟩ ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
ha : a ≠ 1
h : LE.le (α := MulArchimedeanClass M) (mk a) (mk b)
n : ℕ
hn :
  |(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
        ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) b : MulArchimedeanOrder M)|ₘ ≤
    HPow.hPow (α := M)
      (|(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
            ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)|ₘ :
        M)
      n
refine_1 :
  HPow.hPow (α := M)
      (|(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
            ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)|ₘ :
        M)
      n <
    |a|ₘ ^ n * |a|ₘ
⊢ HPow.hPow (α := M)
      (|(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
            ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)|ₘ :
        M)
      n <
    |a|ₘ ^ (n + 1)

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
ha : a ≠ 1
h : LE.le (α := MulArchimedeanClass M) (mk a) (mk b)
n : ℕ
hn :
  |(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
        ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) b : MulArchimedeanOrder M)|ₘ ≤
    HPow.hPow (α := M)
      (|(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
            ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)|ₘ :
        M)
      n
⊢ HPow.hPow (α := M)
      (|(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
            ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)|ₘ :
        M)
      n <
    |a|ₘ ^ n * |a|ₘ

Tactic:
lt_mul_of_one_lt_right' _ (one_lt_mabs.mpr ha)

Premises used: Iff.mpr, one_lt_mabs, lt_mul_of_one_lt_right'
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
ha : a ≠ 1
h : LE.le (α := MulArchimedeanClass M) (mk a) (mk b)
n : ℕ
hn :
  |(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
        ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) b : MulArchimedeanOrder M)|ₘ ≤
    HPow.hPow (α := M)
      (|(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
            ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)|ₘ :
        M)
      n
⊢ HPow.hPow (α := M)
      (|(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
            ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)|ₘ :
        M)
      n <
    |a|ₘ ^ n * |a|ₘ

Tactic:
exact lt_mul_of_one_lt_right' _ (one_lt_mabs.mpr ha)

Premises used: Iff.mpr, one_lt_mabs, lt_mul_of_one_lt_right'
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
ha : a ≠ 1
h : ∃ (n : ℕ), |b|ₘ < |a|ₘ ^ n
n : ℕ
hn : |b|ₘ < |a|ₘ ^ n
⊢ LE.le (α := MulArchimedeanClass M) (mk a) (mk b)

Tactic:
⟨n, hn.le⟩

Premises used: LT.lt.le, Exists.intro
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
ha : a ≠ 1
h : ∃ (n : ℕ), |b|ₘ < |a|ₘ ^ n
n : ℕ
hn : |b|ₘ < |a|ₘ ^ n
⊢ LE.le (α := MulArchimedeanClass M) (mk a) (mk b)

Tactic:
exact ⟨n, hn.le⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
A : MulArchimedeanClass M
mk : ∀ (a : M), LE.le (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk 1)
⊢ A ≤ MulArchimedeanClass.mk 1

Tactic:
induction A using ind with | mk a

Premises used: MulArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a_1 b a : M
mk : ∃ (n : ℕ), |1|ₘ ≤ |a|ₘ ^ n
⊢ LE.le (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk 1)

Tactic:
rw [mk_le_mk]

Premises used: MulArchimedeanClass.mk_le_mk
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a_1 b a : M
⊢ |1|ₘ ≤ HPow.hPow (β := ℕ) |a|ₘ 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a_1 b a : M
⊢ ∃ (n : ℕ), |1|ₘ ≤ |a|ₘ ^ n

Tactic:
exact ⟨1, by simp⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
⊢ Eq.{u_1 + 1} (α := MulArchimedeanClass M) (mk 1) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
⊢ Eq (α := MulArchimedeanClass M) (mk a) ⊤ → a = 1

Tactic:
simp [← mk_one, mk_eq_mk]

Premises used: MulArchimedeanClass.mk_eq_mk, MulArchimedeanClass.mk_one
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
⊢ a = 1 → Eq (α := MulArchimedeanClass M) (mk a) ⊤

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
rw : Eq (α := MulArchimedeanClass M) (mk a) ⊤ ↔ a = 1
rw₁ rw₂ : a = 1 ↔ a = 1
⊢ Eq (α := MulArchimedeanClass M) ⊤ (mk a) ↔ a = 1

Tactic:
rw [eq_comm, mk_eq_top_iff]

Premises used: eq_comm, MulArchimedeanClass.mk_eq_top_iff
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
rw : Eq.{u_1 + 1} (α := MulArchimedeanClass M) (mk (out ⊤)) ⊤
rw₁ rw₂ : Eq.{u_1 + 1} (α := MulArchimedeanClass M) ⊤ ⊤
⊢ Eq.{u_1 + 1} (α := M) (out ⊤) 1

Tactic:
rw [← mk_eq_top_iff, mk_out]

Premises used: MulArchimedeanClass.mk_eq_top_iff, MulArchimedeanClass.mk_out
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
inst_3 : Nontrivial M
obtain : ∀ (x : M) (hx : x ≠ 1), ∃ (x : MulArchimedeanClass M) (y : MulArchimedeanClass M), x ≠ y
⊢ ∃ (x : MulArchimedeanClass M) (y : MulArchimedeanClass M), x ≠ y

Tactic:
obtain ⟨x, hx⟩ := exists_ne (1 : M)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
inst_3 : Nontrivial M
x : M
hx : x ≠ 1
⊢ ∃ (x : MulArchimedeanClass M) (y : MulArchimedeanClass M), x ≠ y

Tactic:
⟨mk x, ⊤, mk_eq_top_iff.ne.mpr hx⟩

Premises used: Iff.mpr, MulArchimedeanClass.mk, Iff.ne, Exists.intro, MulArchimedeanClass.mk_eq_top_iff, Top.top
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
inst_3 : Nontrivial M
x : M
hx : x ≠ 1
⊢ ∃ (x : MulArchimedeanClass M) (y : MulArchimedeanClass M), x ≠ y

Tactic:
exact ⟨mk x, ⊤, mk_eq_top_iff.ne.mpr hx⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Ici 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Ici 1) b
hab : a ≤ b
contrapose! : ∀ (hab : LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)), b < a
⊢ LE.le (α := MulArchimedeanClass M) (mk b) (mk a)

Tactic:
contrapose! hab
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Ici 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Ici 1) b
hab : LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)
⊢ ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ

Tactic:
rw [mk_lt_mk] at hab

Premises used: MulArchimedeanClass.mk_lt_mk
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Ici 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Ici 1) b
hab : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
⊢ HPow.hPow (β := ℕ) |b|ₘ 1 < |a|ₘ

Tactic:
obtain h := hab 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Ici 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Ici 1) b
hab : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
h : HPow.hPow (β := ℕ) |b|ₘ 1 < |a|ₘ
⊢ HPow.hPow (β := ℕ) b 1 < a

Tactic:
rw [mabs_eq_self.mpr ha, mabs_eq_self.mpr hb] at h

Premises used: Iff.mpr, mabs_eq_self
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Ici 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Ici 1) b
hab : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
h : HPow.hPow (β := ℕ) b 1 < a
⊢ b < a

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Iic 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Iic 1) b
hab : a ≤ b
contrapose! : ∀ (hab : LT.lt (α := MulArchimedeanClass M) (mk b) (mk a)), b < a
⊢ LE.le (α := MulArchimedeanClass M) (mk a) (mk b)

Tactic:
contrapose! hab
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Iic 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Iic 1) b
hab : LT.lt (α := MulArchimedeanClass M) (mk b) (mk a)
⊢ ∀ (n : ℕ), |a|ₘ ^ n < |b|ₘ

Tactic:
rw [mk_lt_mk] at hab

Premises used: MulArchimedeanClass.mk_lt_mk
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Iic 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Iic 1) b
hab : ∀ (n : ℕ), |a|ₘ ^ n < |b|ₘ
⊢ HPow.hPow (β := ℕ) |a|ₘ 1 < |b|ₘ

Tactic:
obtain h := hab 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Iic 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Iic 1) b
hab : ∀ (n : ℕ), |a|ₘ ^ n < |b|ₘ
h : HPow.hPow (β := ℕ) |a|ₘ 1 < |b|ₘ
⊢ HPow.hPow (β := ℕ) a⁻¹ 1 < b⁻¹

Tactic:
rw [mabs_eq_inv_self.mpr ha, mabs_eq_inv_self.mpr hb] at h

Premises used: Iff.mpr, mabs_eq_inv_self
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Iic 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Iic 1) b
hab : ∀ (n : ℕ), |a|ₘ ^ n < |b|ₘ
h : HPow.hPow (β := ℕ) a⁻¹ 1 < b⁻¹
⊢ b < a

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h : |a|ₘ ≤ |b|ₘ
rw : LE.le (α := MulArchimedeanClass M) (mk |b|ₘ) (mk |a|ₘ)
⊢ LE.le (α := MulArchimedeanClass M) (mk b) (mk a)

Tactic:
rw [← mk_mabs a, ← mk_mabs]

Premises used: MulArchimedeanClass.mk_mabs
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h : |a|ₘ ≤ |b|ₘ
⊢ 1 ≤ |a|ₘ

Tactic:
have ha := one_le_mabs a
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h : |a|ₘ ≤ |b|ₘ
ha : 1 ≤ |a|ₘ
⊢ LE.le (α := MulArchimedeanClass M) (mk |b|ₘ) (mk |a|ₘ)

Tactic:
mk_antitoneOn ha (ha.trans h) h

Premises used: MulArchimedeanClass.mk_antitoneOn, LE.le.trans
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h : |a|ₘ ≤ |b|ₘ
ha : 1 ≤ |a|ₘ
⊢ LE.le (α := MulArchimedeanClass M) (mk |b|ₘ) (mk |a|ₘ)

Tactic:
exact mk_antitoneOn ha (ha.trans h) h

Premises used: MulArchimedeanClass.mk_antitoneOn, LE.le.trans
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
⊢ |x|ₘ ≤ max |y|ₘ |z|ₘ

Tactic:
have H := mabs_le_max_mabs_mabs hy hz
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ max |y|ₘ |z|ₘ
⊢ |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ

Tactic:
rw [← mabs_of_one_le (le_max_of_le_left (one_le_mabs y))] at H

Premises used: mabs_of_one_le, le_max_of_le_left, one_le_mabs
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
apply : LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk (max |y|ₘ |z|ₘ))
⊢ LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk x)

Tactic:
apply (mk_le_mk_of_mabs H).trans'

Premises used: MulArchimedeanClass.mk_le_mk_of_mabs, LE.le.trans'
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
inl : ∀ (h : |y|ₘ ≤ |z|ₘ), LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk (max |y|ₘ |z|ₘ))
inr : ∀ (h : |z|ₘ ≤ |y|ₘ), LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk (max |y|ₘ |z|ₘ))
⊢ LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk (max |y|ₘ |z|ₘ))

Tactic:
obtain h | h := le_total |y|ₘ |z|ₘ

Premises used: le_total, mabs