awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
R : Type u_3
K_1 : Type u_4
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
rw : ∀ (x : K), ∃ (n : ℤ), x ≤ (↑n : K)
⊢ Archimedean K

Tactic:
rw [archimedean_iff_int_le]

Premises used: archimedean_iff_int_le
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
R : Type u_3
K_1 : Type u_4
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
⊢ ∀ (x : K), ∃ (n : ℤ), x ≤ (↑n : K)

Tactic:
fun x => ⟨⌈x⌉, Int.le_ceil x⟩

Premises used: Int.le_ceil, Exists.intro, Int.ceil
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
R : Type u_3
K_1 : Type u_4
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
⊢ ∀ (x : K), ∃ (n : ℤ), x ≤ (↑n : K)

Tactic:
exact fun x => ⟨⌈x⌉, Int.le_ceil x⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : MulArchimedean M
⊢ MulArchimedean.{u_5} Mˣ

Tactic:
⟨fun x {_} h ↦ MulArchimedean.arch x.val h⟩

Premises used: Units.val, MulArchimedean.mk, MulArchimedean.arch
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Archimedean M
arch : ∀ (x : WithBot M) {y : WithBot M}, 0 < y → ∃ (n : ℕ), x ≤ n • y
⊢ Archimedean.{u_5} (WithBot M)

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Archimedean M
x : WithBot M
hxy : LT.lt.{u_5} (α := WithBot M) 0 ⊥
⊢ ∃ (n : ℕ), x ≤ HSMul.hSMul (β := WithBot M) n ⊥

Tactic:
absurd hxy bot_le.not_gt

Premises used: absurd, LE.le.not_gt, bot_le
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Archimedean M
x : WithBot M
hxy : LT.lt.{u_5} (α := WithBot M) 0 ⊥
⊢ ∃ (n : ℕ), x ≤ HSMul.hSMul (β := WithBot M) n ⊥

Tactic:
exact absurd hxy bot_le.not_gt

Premises used: absurd, LE.le.not_gt, bot_le
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Archimedean M
y : M
hxy : 0 < (↑y : WithBot M)
⊢ ∃ (n : ℕ), ⊥ ≤ n • (↑y : WithBot M)

Tactic:
⟨0, bot_le⟩

Premises used: Exists.intro, OfNat.ofNat, bot_le
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Archimedean M
y : M
hxy : 0 < (↑y : WithBot M)
⊢ ∃ (n : ℕ), ⊥ ≤ n • (↑y : WithBot M)

Tactic:
refine ⟨0, bot_le⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Archimedean M
y : M
hxy : 0 < (↑y : WithBot M)
x : M
⊢ 0 < y

Tactic:
simpa using hxy
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Archimedean M
y : M
hxy : 0 < (↑y : WithBot M)
x : M
⊢ ∃ (n : ℕ), (↑x : WithBot M) ≤ n • (↑y : WithBot M)

Tactic:
simpa [← WithBot.coe_nsmul] using (Archimedean.arch x (by simpa using hxy))

Premises used: WithBot.coe_nsmul, Archimedean.arch
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Archimedean M
x : WithBot M
y : M
hxy : 0 < (↑y : WithBot M)
arch : ∃ (n : ℕ), ⊥ ≤ n • (↑y : WithBot M)
arch₁ : ∀ (x : M), ∃ (n : ℕ), (↑x : WithBot M) ≤ n • (↑y : WithBot M)
⊢ ∃ (n : ℕ), x ≤ n • (↑y : WithBot M)

Tactic:
cases x with
    | bot => refine ⟨0, bot_le⟩
    | coe x => simpa [← WithBot.coe_nsmul] using (Archimedean.arch x (by simpa using hxy))

Premises used: WithBot.coe, WithBot.coe_nsmul, Archimedean.arch, WithBot.bot
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Archimedean M
x y : WithBot M
hxy : 0 < y
arch : ∀ (hxy : LT.lt.{u_5} (α := WithBot M) 0 ⊥), ∃ (n : ℕ), x ≤ HSMul.hSMul (β := WithBot M) n ⊥
arch₁ : ∀ (y : M) (hxy : 0 < (↑y : WithBot M)), ∃ (n : ℕ), x ≤ n • (↑y : WithBot M)
⊢ ∃ (n : ℕ), x ≤ n • y

Tactic:
cases y with
  | bot => exact absurd hxy bot_le.not_gt
  | coe y =>
    cases x with
    | bot => refine ⟨0, bot_le⟩
    | coe x => simpa [← WithBot.coe_nsmul] using (Archimedean.arch x (by simpa using hxy))

Premises used: WithBot.coe, absurd, WithBot.coe_nsmul, Archimedean.arch, WithBot.bot
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : MulArchimedean M
arch : ∀ (x : WithZero M) {y : WithZero M}, 1 < y → ∃ (n : ℕ), x ≤ y ^ n
⊢ MulArchimedean.{u_5} (WithZero M)

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : MulArchimedean M
x : WithZero M
hxy : LT.lt.{u_5} (α := WithZero M) 1 0
⊢ ∃ (n : ℕ), x ≤ HPow.hPow (α := WithZero M) 0 n

Tactic:
cases hxy.pos.false

Premises used: LT.lt.pos, LT.lt.false
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : MulArchimedean M
y : M
hxy : 1 < (↑y : WithZero M)
⊢ ∃ (n : ℕ), 0 ≤ (↑y : WithZero M) ^ n

Tactic:
⟨0, zero_le⟩

Premises used: zero_le, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : MulArchimedean M
y : M
hxy : 1 < (↑y : WithZero M)
⊢ ∃ (n : ℕ), 0 ≤ (↑y : WithZero M) ^ n

Tactic:
refine ⟨0, zero_le⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : MulArchimedean M
y : M
hxy : 1 < (↑y : WithZero M)
x : M
⊢ 1 < y

Tactic:
simpa using hxy
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : MulArchimedean M
y : M
hxy : 1 < (↑y : WithZero M)
x : M
⊢ ∃ (n : ℕ), (↑x : WithZero M) ≤ (↑y : WithZero M) ^ n

Tactic:
simpa [← WithZero.coe_pow] using (MulArchimedean.arch x (by simpa using hxy))

Premises used: WithZero.coe_pow, MulArchimedean.arch
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : MulArchimedean M
x : WithZero M
y : M
hxy : 1 < (↑y : WithZero M)
arch : ∃ (n : ℕ), 0 ≤ (↑y : WithZero M) ^ n
arch₁ : ∀ (x : M), ∃ (n : ℕ), (↑x : WithZero M) ≤ (↑y : WithZero M) ^ n
⊢ ∃ (n : ℕ), x ≤ (↑y : WithZero M) ^ n

Tactic:
cases x with
    | zero => refine ⟨0, zero_le⟩
    | coe x => simpa [← WithZero.coe_pow] using (MulArchimedean.arch x (by simpa using hxy))

Premises used: WithZero.coe_pow, WithZero.coe, MulArchimedean.arch
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : MulArchimedean M
x y : WithZero M
hxy : 1 < y
arch : ∀ (hxy : LT.lt.{u_5} (α := WithZero M) 1 0), ∃ (n : ℕ), x ≤ HPow.hPow (α := WithZero M) 0 n
arch₁ : ∀ (y : M) (hxy : 1 < (↑y : WithZero M)), ∃ (n : ℕ), x ≤ (↑y : WithZero M) ^ n
⊢ ∃ (n : ℕ), x ≤ y ^ n

Tactic:
cases y with
  | zero => cases hxy.pos.false
  | coe y =>
    cases x with
    | zero => refine ⟨0, zero_le⟩
    | coe x => simpa [← WithZero.coe_pow] using (MulArchimedean.arch x (by simpa using hxy))

Premises used: WithZero.coe_pow, WithZero.coe, LT.lt.false, MulArchimedean.arch
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
⊢ Eq.{u_1 + 1} (α := MulArchimedeanOrder M ≃ M) (Equiv.symm of) val

Tactic:
rfl

Premises used: MulArchimedeanOrder.val, Equiv.symm, Equiv.refl, rfl, MulArchimedeanOrder
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
⊢ Eq.{u_1 + 1} (α := M ≃ MulArchimedeanOrder M) (Equiv.symm val) of

Tactic:
rfl

Premises used: Equiv.symm, Equiv.refl, rfl, MulArchimedeanOrder, MulArchimedeanOrder.of
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
a : MulArchimedeanOrder M
⊢ (of : (a : M) → MulArchimedeanOrder M) ((val : (a : MulArchimedeanOrder M) → M) a : M) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
a : M
⊢ (val : (a : MulArchimedeanOrder M) → M) ((of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : Nonempty M
⊢ Nonempty.{u_1 + 1} (MulArchimedeanOrder M)

Tactic:
inferInstanceAs (Nonempty M)

Premises used: _private.0.MulArchimedeanOrder.instNonempty._proof_1
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : Subsingleton M
⊢ Subsingleton.{u_1 + 1} (MulArchimedeanOrder M)

Tactic:
inferInstanceAs (Subsingleton M)

Premises used: _private.0.MulArchimedeanOrder.instSubsingleton._proof_1
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : Group M
inst_1 : Lattice M
a b : MulArchimedeanOrder M
⊢ a ≤ b ↔
    ∃ (n : ℕ),
      |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤
        HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) n

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : Group M
inst_1 : Lattice M
a b : MulArchimedeanOrder M
⊢ a < b ↔
    ∀ (n : ℕ),
      HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n <
        |(val : (a : MulArchimedeanOrder M) → M) a|ₘ

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b : M
a : MulArchimedeanOrder M
⊢ |(val : (a : MulArchimedeanOrder M) → M) a|ₘ ≤
    HPow.hPow (α := M) (β := ℕ) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b c : MulArchimedeanOrder M
m : ℕ
hm :
  |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) m
this :
  ∀ (n : ℕ)
    (hn :
      |(val : (a : MulArchimedeanOrder M) → M) c|ₘ ≤
        HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n),
    a ≤ c
⊢ b ≤ c → a ≤ c

Tactic:
⟨n, hn⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b c : MulArchimedeanOrder M
m : ℕ
hm :
  |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) m
n : ℕ
hn :
  |(val : (a : MulArchimedeanOrder M) → M) c|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n
h :
  |(val : (a : MulArchimedeanOrder M) → M) c|ₘ ≤
    HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) (m * n)
⊢ a ≤ c

Tactic:
use m * n
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b c : MulArchimedeanOrder M
m : ℕ
hm :
  |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) m
n : ℕ
hn :
  |(val : (a : MulArchimedeanOrder M) → M) c|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n
h :
  |(val : (a : MulArchimedeanOrder M) → M) c|ₘ ≤
    HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) m ^ n
⊢ |(val : (a : MulArchimedeanOrder M) → M) c|ₘ ≤
    HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) (m * n)

Tactic:
rw [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b c : MulArchimedeanOrder M
m : ℕ
hm :
  |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) m
n : ℕ
hn :
  |(val : (a : MulArchimedeanOrder M) → M) c|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n
⊢ |(val : (a : MulArchimedeanOrder M) → M) c|ₘ ≤
    HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) m ^ n

Tactic:
hn.trans (pow_le_pow_left' hm n)

Premises used: LE.le.trans, pow_le_pow_left'
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b c : MulArchimedeanOrder M
m : ℕ
hm :
  |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) m
n : ℕ
hn :
  |(val : (a : MulArchimedeanOrder M) → M) c|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n
⊢ |(val : (a : MulArchimedeanOrder M) → M) c|ₘ ≤
    HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) m ^ n

Tactic:
exact hn.trans (pow_le_pow_left' hm n)

Premises used: LE.le.trans, pow_le_pow_left'
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b : MulArchimedeanOrder M
this :
  (∀ (n : ℕ),
      HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n <
        |(val : (a : MulArchimedeanOrder M) → M) a|ₘ) →
    ∃ (n : ℕ),
      |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤
        HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) n
⊢ (∀ (n : ℕ),
      HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n <
        |(val : (a : MulArchimedeanOrder M) → M) a|ₘ) ↔
    (∃ (n : ℕ),
        |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤
          HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) n) ∧
      ¬∃ (n : ℕ),
          |(val : (a : MulArchimedeanOrder M) → M) a|ₘ ≤
            HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n

Tactic:
simpa using this
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b : MulArchimedeanOrder M
suffices :
  (∀ (n : ℕ),
      HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n <
        |(val : (a : MulArchimedeanOrder M) → M) a|ₘ) →
    ∃ (n : ℕ),
      |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤
        HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) n
⊢ (∀ (n : ℕ),
      HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n <
        |(val : (a : MulArchimedeanOrder M) → M) a|ₘ) ↔
    (∃ (n : ℕ),
        |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤
          HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) n) ∧
      ¬∃ (n : ℕ),
          |(val : (a : MulArchimedeanOrder M) → M) a|ₘ ≤
            HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n

Tactic:
suffices (∀ (n : ℕ), |b.val|ₘ ^ n < |a.val|ₘ) → ∃ n, |b.val|ₘ ≤ |a.val|ₘ ^ n by
      simpa using this
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b : MulArchimedeanOrder M
h :
  ∀ (n : ℕ),
    HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n <
      |(val : (a : MulArchimedeanOrder M) → M) a|ₘ
⊢ HPow.hPow (α := M) (β := ℕ) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) 1 ≤
    |(val : (a : MulArchimedeanOrder M) → M) a|ₘ

Tactic:
obtain h := (h 1).le

Premises used: LT.lt.le, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b : MulArchimedeanOrder M
h_1 :
  ∀ (n : ℕ),
    HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n <
      |(val : (a : MulArchimedeanOrder M) → M) a|ₘ
h :
  HPow.hPow (α := M) (β := ℕ) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) 1 ≤
    |(val : (a : MulArchimedeanOrder M) → M) a|ₘ
⊢ |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤
    HPow.hPow (α := M) (β := ℕ) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) 1

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b : MulArchimedeanOrder M
h_1 :
  ∀ (n : ℕ),
    HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n <
      |(val : (a : MulArchimedeanOrder M) → M) a|ₘ
h :
  HPow.hPow (α := M) (β := ℕ) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) 1 ≤
    |(val : (a : MulArchimedeanOrder M) → M) a|ₘ
⊢ ∃ (n : ℕ),
    |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤
      HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) n

Tactic:
exact ⟨1, by simpa using h⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b : MulArchimedeanOrder M
inl :
  ∀
    (hab :
      LE.le (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M)
        (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M)),
    a ≤ b ∨ b ≤ a
inr :
  ∀
    (hab :
      LE.le (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M)
        (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M)),
    a ≤ b ∨ b ≤ a
⊢ a ≤ b ∨ b ≤ a

Tactic:
obtain hab | hab := le_total |a.val|ₘ |b.val|ₘ

Premises used: le_total, MulArchimedeanOrder.val, DFunLike.coe, mabs
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b : MulArchimedeanOrder M
hab :
  LE.le (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M)
⊢ |(val : (a : MulArchimedeanOrder M) → M) a|ₘ ≤
    HPow.hPow (α := M) (β := ℕ) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) 1

Tactic:
simpa using hab
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b : MulArchimedeanOrder M
hab :
  LE.le (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M)
⊢ a ≤ b ∨ b ≤ a

Tactic:
exact .inr ⟨1, by simpa using hab⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b : MulArchimedeanOrder M
hab :
  LE.le (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M)
⊢ |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤
    HPow.hPow (α := M) (β := ℕ) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) 1

Tactic:
simpa using hab
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b : MulArchimedeanOrder M
hab :
  LE.le (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M)
⊢ a ≤ b ∨ b ≤ a

Tactic:
exact .inl ⟨1, by simpa using hab⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
N : Type u_3
inst_5 : CommGroup N
inst_6 : LinearOrder N
inst_7 : IsOrderedMonoid N
f : M →*o N
a b : MulArchimedeanOrder M
n : ℕ
hn :
  |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) n
simp_rw :
  ∃ (n : ℕ),
    LE.le.{u_3} (α := N) ((f : (a : M) → N) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) : N)
      ((f : (a : M) → N) (HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) n) : N)
⊢ LE.le.{u_3} (α := MulArchimedeanOrder N)
    ((fun (a : MulArchimedeanOrder M) ↦
        ((of : (a : N) → MulArchimedeanOrder N)
            ((f : (a : M) → N) ((val : (a : MulArchimedeanOrder M) → M) a : M) : N) :
          MulArchimedeanOrder N))
      a)
    ((fun (a : MulArchimedeanOrder M) ↦
        ((of : (a : N) → MulArchimedeanOrder N)
            ((f : (a : M) → N) ((val : (a : MulArchimedeanOrder M) → M) a : M) : N) :
          MulArchimedeanOrder N))
      b)

Tactic:
simp_rw [le_def, val_of, ← map_mabs, ← map_pow]

Premises used: map_pow, map_mabs, MulArchimedeanOrder.le_def, MulArchimedeanOrder.val_of
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
N : Type u_3
inst_5 : CommGroup N
inst_6 : LinearOrder N
inst_7 : IsOrderedMonoid N
f : M →*o N
a b : MulArchimedeanOrder M
n : ℕ
hn :
  |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) n
⊢ ∃ (n : ℕ),
    LE.le.{u_3} (α := N) ((f : (a : M) → N) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) : N)
      ((f : (a : M) → N) (HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) n) : N)

Tactic:
⟨n, OrderHomClass.monotone f hn⟩

Premises used: OrderHomClass.monotone, Exists.intro
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
N : Type u_3
inst_5 : CommGroup N
inst_6 : LinearOrder N
inst_7 : IsOrderedMonoid N
f : M →*o N
a b : MulArchimedeanOrder M
n : ℕ
hn :
  |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) n
⊢ ∃ (n : ℕ),
    LE.le.{u_3} (α := N) ((f : (a : M) → N) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) : N)
      ((f : (a : M) → N) (HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) n) : N)

Tactic:
exact ⟨n, OrderHomClass.monotone f hn⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
motive : MulArchimedeanClass M → Prop
mk : ∀ (a : M), motive (MulArchimedeanClass.mk a)
⊢ ∀ (x : MulArchimedeanClass M), motive x

Tactic:
Antisymmetrization.ind _ mk

Premises used: Antisymmetrization.ind, LE.le, MulArchimedeanClass