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
a b : M
N : Type u_2
inst_3 : CommGroup N
inst_4 : LinearOrder N
inst_5 : IsOrderedMonoid N
f : M →*o N
h : LE.le (α := MulArchimedeanClass M) (mk a) (mk b)
⊢ LE.le.{u_2} (α := MulArchimedeanClass N)
    (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
          (a : MulArchimedeanClass M) → MulArchimedeanClass N)
        (mk a) :
      MulArchimedeanClass N)
    (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
          (a : MulArchimedeanClass M) → MulArchimedeanClass N)
        (mk b) :
      MulArchimedeanClass N)

Tactic:
exact OrderHomClass.monotone _ h

Premises used: OrderHomClass.monotone
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
N : Type u_2
inst_3 : CommGroup N
inst_4 : LinearOrder N
inst_5 : IsOrderedMonoid N
f : M →*o N
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
a b : MulArchimedeanClass M
mk :
  ∀ (a : M),
    Eq.{u_2 + 1} (α := MulArchimedeanClass N)
        (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
              (a : MulArchimedeanClass M) → MulArchimedeanClass N)
            (MulArchimedeanClass.mk a) :
          MulArchimedeanClass N)
        (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
              (a : MulArchimedeanClass M) → MulArchimedeanClass N)
            b :
          MulArchimedeanClass N) →
      MulArchimedeanClass.mk a = b
⊢ Eq.{u_2 + 1} (α := MulArchimedeanClass N)
      (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
            (a : MulArchimedeanClass M) → MulArchimedeanClass N)
          a :
        MulArchimedeanClass N)
      (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
            (a : MulArchimedeanClass M) → MulArchimedeanClass N)
          b :
        MulArchimedeanClass N) →
    a = b

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
N : Type u_2
inst_3 : CommGroup N
inst_4 : LinearOrder N
inst_5 : IsOrderedMonoid N
f : M →*o N
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
b : MulArchimedeanClass M
a : M
mk :
  ∀ (b : M),
    Eq.{u_2 + 1} (α := MulArchimedeanClass N)
        (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
              (a : MulArchimedeanClass M) → MulArchimedeanClass N)
            (MulArchimedeanClass.mk a) :
          MulArchimedeanClass N)
        (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
              (a : MulArchimedeanClass M) → MulArchimedeanClass N)
            (MulArchimedeanClass.mk b) :
          MulArchimedeanClass N) →
      Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)
⊢ Eq.{u_2 + 1} (α := MulArchimedeanClass N)
      (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
            (a : MulArchimedeanClass M) → MulArchimedeanClass N)
          (MulArchimedeanClass.mk a) :
        MulArchimedeanClass N)
      (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
            (a : MulArchimedeanClass M) → MulArchimedeanClass N)
          b :
        MulArchimedeanClass N) →
    MulArchimedeanClass.mk a = b

Tactic:
induction b using ind with | mk b

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
N : Type u_2
inst_3 : CommGroup N
inst_4 : LinearOrder N
inst_5 : IsOrderedMonoid N
f : M →*o N
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
a b : M
mk :
  ((∃ (m : ℕ), LE.le.{u_2} (α := N) ((f : (a : M) → N) |b|ₘ : N) ((f : (a : M) → N) (|a|ₘ ^ m) : N)) ∧
      ∃ (n : ℕ), LE.le.{u_2} (α := N) ((f : (a : M) → N) |a|ₘ : N) ((f : (a : M) → N) (|b|ₘ ^ n) : N)) →
    (∃ (m : ℕ), |b|ₘ ≤ |a|ₘ ^ m) ∧ ∃ (n : ℕ), |a|ₘ ≤ |b|ₘ ^ n
⊢ Eq.{u_2 + 1} (α := MulArchimedeanClass N)
      (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
            (a : MulArchimedeanClass M) → MulArchimedeanClass N)
          (MulArchimedeanClass.mk a) :
        MulArchimedeanClass N)
      (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
            (a : MulArchimedeanClass M) → MulArchimedeanClass N)
          (MulArchimedeanClass.mk b) :
        MulArchimedeanClass N) →
    Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)

Tactic:
simp_rw [orderHom_mk, mk_eq_mk, ← map_mabs, ← map_pow]

Premises used: MulArchimedeanClass.mk_eq_mk, map_pow, map_mabs, MulArchimedeanClass.orderHom_mk
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
N : Type u_2
inst_3 : CommGroup N
inst_4 : LinearOrder N
inst_5 : IsOrderedMonoid N
f : M →*o N
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
a b : M
⊢ StrictMono.{u_1, u_2} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
obtain hmono := (OrderHomClass.monotone f).strictMono_of_injective h

Premises used: OrderHomClass.monotone, Monotone.strictMono_of_injective
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
N : Type u_2
inst_3 : CommGroup N
inst_4 : LinearOrder N
inst_5 : IsOrderedMonoid N
f : M →*o N
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
a b : M
hmono : StrictMono.{u_1, u_2} (α := M) (β := N) (⇑f : (a : M) → N)
m : ℕ
hm : LE.le.{u_2} (α := N) ((f : (a : M) → N) |b|ₘ : N) ((f : (a : M) → N) (|a|ₘ ^ m) : N)
n : ℕ
hn : LE.le.{u_2} (α := N) ((f : (a : M) → N) |a|ₘ : N) ((f : (a : M) → N) (|b|ₘ ^ n) : N)
⊢ (∃ (m : ℕ), |b|ₘ ≤ |a|ₘ ^ m) ∧ ∃ (n : ℕ), |a|ₘ ≤ |b|ₘ ^ n

Tactic:
⟨⟨m, hmono.le_iff_le.mp hm⟩, ⟨n, hmono.le_iff_le.mp hn⟩⟩

Premises used: And.intro, Exists.intro, Iff.mp, StrictMono.le_iff_le
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
N : Type u_2
inst_3 : CommGroup N
inst_4 : LinearOrder N
inst_5 : IsOrderedMonoid N
f : M →*o N
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
a b : M
hmono : StrictMono.{u_1, u_2} (α := M) (β := N) (⇑f : (a : M) → N)
m : ℕ
hm : LE.le.{u_2} (α := N) ((f : (a : M) → N) |b|ₘ : N) ((f : (a : M) → N) (|a|ₘ ^ m) : N)
n : ℕ
hn : LE.le.{u_2} (α := N) ((f : (a : M) → N) |a|ₘ : N) ((f : (a : M) → N) (|b|ₘ ^ n) : N)
⊢ (∃ (m : ℕ), |b|ₘ ≤ |a|ₘ ^ m) ∧ ∃ (n : ℕ), |a|ₘ ≤ |b|ₘ ^ n

Tactic:
exact ⟨⟨m, hmono.le_iff_le.mp hm⟩, ⟨n, hmono.le_iff_le.mp hn⟩⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
N : Type u_2
inst_3 : CommGroup N
inst_4 : LinearOrder N
inst_5 : IsOrderedMonoid N
f : M →*o N
rw :
  Eq.{u_2 + 1} (α := MulArchimedeanClass N)
    (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
          (a : MulArchimedeanClass M) → MulArchimedeanClass N)
        (mk 1) :
      MulArchimedeanClass N)
    (⊤ : MulArchimedeanClass N)
rw₁ :
  Eq.{u_2 + 1} (α := MulArchimedeanClass N)
    (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
          (a : MulArchimedeanClass M) → MulArchimedeanClass N)
        (mk 1) :
      MulArchimedeanClass N)
    (mk 1 : MulArchimedeanClass N)
rw₂ :
  Eq.{u_2 + 1} (α := MulArchimedeanClass N) (mk ((f : (a : M) → N) 1) : MulArchimedeanClass N)
    (mk 1 : MulArchimedeanClass N)
rw₃ rw₄ : Eq.{u_2 + 1} (α := MulArchimedeanClass N) (mk 1) (mk 1)
⊢ Eq.{u_2 + 1} (α := MulArchimedeanClass N)
    (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
        (a : MulArchimedeanClass M) → MulArchimedeanClass N)
      ⊤)
    ⊤

Tactic:
rw [← mk_one, ← mk_one, orderHom_mk, map_one]

Premises used: MulArchimedeanClass.mk_one, map_one, MulArchimedeanClass.orderHom_mk
-- 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
α : Type u_2
inst_3 : PartialOrder α
f : M → α
h : ∀ (a b : M), LE.le (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b) → f a ≤ f b
A B : MulArchimedeanClass M
hle : A ≤ B
mk : ∀ (a : M) (hle : MulArchimedeanClass.mk a ≤ B), lift f ⋯ (MulArchimedeanClass.mk a) ≤ lift f ⋯ B
⊢ lift f ⋯ A ≤ lift f ⋯ B

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 : M
α : Type u_2
inst_3 : PartialOrder α
f : M → α
h : ∀ (a b : M), LE.le (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b) → f a ≤ f b
B : MulArchimedeanClass M
a : M
hle : MulArchimedeanClass.mk a ≤ B
mk :
  ∀ (b : M) (hle : LE.le (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)),
    lift f ⋯ (MulArchimedeanClass.mk a) ≤ lift f ⋯ (MulArchimedeanClass.mk b)
⊢ lift f ⋯ (MulArchimedeanClass.mk a) ≤ lift f ⋯ B

Tactic:
induction B using ind with | mk b

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_1 : M
α : Type u_2
inst_3 : PartialOrder α
f : M → α
h : ∀ (a b : M), LE.le (α := MulArchimedeanClass M) (mk a) (mk b) → f a ≤ f b
a b : M
hle : LE.le (α := MulArchimedeanClass M) (mk a) (mk b)
⊢ lift f ⋯ (mk a) ≤ lift f ⋯ (mk b)

Tactic:
simpa using h a b (mk_le_mk.mp hle)

Premises used: Iff.mp, 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
α : Type u_2
inst_3 : PartialOrder α
f : M → α
h : ∀ (a b : M), LE.le (α := MulArchimedeanClass M) (mk a) (mk b) → f a ≤ f b
a : M
⊢ (liftOrderHom f h : (a : MulArchimedeanClass M) → α) (mk a) = f a

Tactic:
lift_mk f (fun a b heq ↦ le_antisymm (h a b heq.le) (h b a heq.ge)) a

Premises used: Eq.ge, Eq.le, MulArchimedeanClass.lift, MulArchimedeanClass.lift_mk, le_antisymm
-- 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_1 : M
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : a ∈ mk ⁻¹' (↑s : Set (MulArchimedeanClass M))
hb : b ∈ mk ⁻¹' (↑s : Set (MulArchimedeanClass M))
⊢ mk a ∈ (↑s : Set (MulArchimedeanClass M))

Tactic:
rw [Set.mem_preimage] at ha hb ⊢

Premises used: Set.mem_preimage
-- 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_1 : M
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : a ∈ mk ⁻¹' (↑s : Set (MulArchimedeanClass M))
hb : b ∈ mk ⁻¹' (↑s : Set (MulArchimedeanClass M))
ha₁ : mk a ∈ (↑s : Set (MulArchimedeanClass M))
⊢ mk b ∈ (↑s : Set (MulArchimedeanClass M))

Tactic:
rw [Set.mem_preimage] at ha hb ⊢

Premises used: Set.mem_preimage
-- 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_1 : M
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : mk a ∈ (↑s : Set (MulArchimedeanClass M))
hb : mk b ∈ (↑s : Set (MulArchimedeanClass M))
inl : ∀ (h : LE.le (α := MulArchimedeanClass M) (mk a) (mk (a * b))), mk (a * b) ∈ (↑s : Set (MulArchimedeanClass M))
inr : ∀ (h : LE.le (α := MulArchimedeanClass M) (mk b) (mk (a * b))), mk (a * b) ∈ (↑s : Set (MulArchimedeanClass M))
⊢ mk (a * b) ∈ (↑s : Set (MulArchimedeanClass M))

Tactic:
obtain h | h := min_le_iff.mp (min_le_mk_mul a b)

Premises used: min_le_iff, MulArchimedeanClass.min_le_mk_mul, Iff.mp
-- 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_1 : M
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : mk a ∈ (↑s : Set (MulArchimedeanClass M))
hb : mk b ∈ (↑s : Set (MulArchimedeanClass M))
h : LE.le (α := MulArchimedeanClass M) (mk a) (mk (a * b))
⊢ mk (a * b) ∈ (↑s : Set (MulArchimedeanClass M))

Tactic:
s.upper h ha

Premises used: UpperSet.upper
-- 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_1 : M
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : mk a ∈ (↑s : Set (MulArchimedeanClass M))
hb : mk b ∈ (↑s : Set (MulArchimedeanClass M))
h : LE.le (α := MulArchimedeanClass M) (mk a) (mk (a * b))
⊢ mk (a * b) ∈ (↑s : Set (MulArchimedeanClass M))

Tactic:
exact s.upper h ha

Premises used: UpperSet.upper
-- 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_1 : M
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : mk a ∈ (↑s : Set (MulArchimedeanClass M))
hb : mk b ∈ (↑s : Set (MulArchimedeanClass M))
h : LE.le (α := MulArchimedeanClass M) (mk b) (mk (a * b))
⊢ mk (a * b) ∈ (↑s : Set (MulArchimedeanClass M))

Tactic:
s.upper h hb

Premises used: UpperSet.upper
-- 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_1 : M
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : mk a ∈ (↑s : Set (MulArchimedeanClass M))
hb : mk b ∈ (↑s : Set (MulArchimedeanClass M))
h : LE.le (α := MulArchimedeanClass M) (mk b) (mk (a * b))
⊢ mk (a * b) ∈ (↑s : Set (MulArchimedeanClass M))

Tactic:
exact s.upper h hb

Premises used: UpperSet.upper
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
hst : s < t
⊢ (↑(subsemigroup t) : Set M) ⊂ (↑(subsemigroup s) : Set M)

Tactic:
Set.ssubset_iff_subset_ne.mpr ⟨fun _ h ↦ hst.le h, ?_⟩

Premises used: Iff.mpr, Set.ssubset_iff_subset_ne, LT.lt.le, And.intro
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
hst : s < t
refine : (↑(subsemigroup t) : Set M) ≠ (↑(subsemigroup s) : Set M)
⊢ (↑(subsemigroup t) : Set M) ⊂ (↑(subsemigroup s) : Set M)

Tactic:
refine Set.ssubset_iff_subset_ne.mpr ⟨fun _ h ↦ hst.le h, ?_⟩

Premises used: Iff.mpr, Set.ssubset_iff_subset_ne, LT.lt.le, And.intro
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
hst : s < t
contrapose! : ∀ (heq : (↑(subsemigroup t) : Set M) = (↑(subsemigroup s) : Set M)), t ≤ s
⊢ (↑(subsemigroup t) : Set M) ≠ (↑(subsemigroup s) : Set M)

Tactic:
contrapose! hst with heq
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
heq : (↑(subsemigroup t) : Set M) = (↑(subsemigroup s) : Set M)
hab : t = s
⊢ t ≤ s

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
heq : (↑(subsemigroup t) : Set M) = (↑(subsemigroup s) : Set M)
⊢ t = s

Tactic:
simpa [MulArchimedeanClass.mk_surjective, MulArchimedeanClass.subsemigroup] using heq

Premises used: MulArchimedeanClass.subsemigroup, 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
s : UpperSet (MulArchimedeanClass M)
hs : ¬s = ⊤
obtain :
  ∀ (u : MulArchimedeanClass M) (hu : u ∈ (↑s : Set (MulArchimedeanClass M))), mk 1 ∈ (↑s : Set (MulArchimedeanClass M))
⊢ mk 1 ∈ (↑s : Set (MulArchimedeanClass M))

Tactic:
obtain ⟨u, hu⟩ := UpperSet.coe_nonempty.mpr hs

Premises used: Iff.mpr, UpperSet.coe_nonempty
-- 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
s : UpperSet (MulArchimedeanClass M)
hs : ¬s = ⊤
u : MulArchimedeanClass M
hu : u ∈ (↑s : Set (MulArchimedeanClass M))
⊢ u ≤ ⊤

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
s : UpperSet (MulArchimedeanClass M)
hs : ¬s = ⊤
u : MulArchimedeanClass M
hu : u ∈ (↑s : Set (MulArchimedeanClass M))
⊢ mk 1 ∈ (↑s : Set (MulArchimedeanClass M))

Tactic:
simpa using s.upper (by simp) hu

Premises used: UpperSet.upper
-- 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
s : UpperSet (MulArchimedeanClass M)
hs : ¬s = ⊤
⊢ ∀ {x : M}, x ∈ (subsemigroup s).carrier → x⁻¹ ∈ (subsemigroup s).carrier

Tactic:
simp [subsemigroup]

Premises used: MulArchimedeanClass.subsemigroup
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
hs : s ≠ ⊤
⊢ (↑(subsemigroup s) : Set M) = (↑(subgroup s) : Set M)

Tactic:
simp [subgroup, hs]

Premises used: MulArchimedeanClass.subgroup
-- 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} (α := Subgroup M) (subgroup ⊤) ⊥

Tactic:
simp [subgroup]

Premises used: MulArchimedeanClass.subgroup
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
s : UpperSet (MulArchimedeanClass M)
hs : s ≠ ⊤
⊢ a ∈ subgroup s ↔ mk a ∈ s

Tactic:
simp [subgroup, subsemigroup, hs]

Premises used: MulArchimedeanClass.subsemigroup, MulArchimedeanClass.subgroup
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
hs : Membership.mem (γ := Set (UpperSet (MulArchimedeanClass M))) (Set.Iio ⊤) s
t : UpperSet (MulArchimedeanClass M)
ht : Membership.mem (γ := Set (UpperSet (MulArchimedeanClass M))) (Set.Iio ⊤) t
hst : s < t
rw : (↑(subgroup t) : Set M) ⊂ (↑(subsemigroup s) : Set M)
⊢ (↑(subgroup t) : Set M) ⊂ (↑(subgroup s) : Set M)

Tactic:
rw [← subsemigroup_eq_subgroup_of_ne_top (Set.mem_Iio.mp hs).ne_top]

Premises used: Set.mem_Iio, LT.lt.ne_top, MulArchimedeanClass.subsemigroup_eq_subgroup_of_ne_top, Iff.mp
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
hs : Membership.mem (γ := Set (UpperSet (MulArchimedeanClass M))) (Set.Iio ⊤) s
t : UpperSet (MulArchimedeanClass M)
ht : Membership.mem (γ := Set (UpperSet (MulArchimedeanClass M))) (Set.Iio ⊤) t
hst : s < t
rw : (↑(subsemigroup t) : Set M) ⊂ (↑(subsemigroup s) : Set M)
⊢ (↑(subgroup t) : Set M) ⊂ (↑(subsemigroup s) : Set M)

Tactic:
rw [← subsemigroup_eq_subgroup_of_ne_top (Set.mem_Iio.mp ht).ne_top]

Premises used: Set.mem_Iio, LT.lt.ne_top, MulArchimedeanClass.subsemigroup_eq_subgroup_of_ne_top, Iff.mp
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
hs : Membership.mem (γ := Set (UpperSet (MulArchimedeanClass M))) (Set.Iio ⊤) s
t : UpperSet (MulArchimedeanClass M)
ht : Membership.mem (γ := Set (UpperSet (MulArchimedeanClass M))) (Set.Iio ⊤) t
hst : s < t
⊢ (↑(subsemigroup t) : Set M) ⊆ (↑(subsemigroup s) : Set M)

Tactic:
simpa [subsemigroup] using hst.le

Premises used: MulArchimedeanClass.subsemigroup, LT.lt.le
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
hs : Membership.mem (γ := Set (UpperSet (MulArchimedeanClass M))) (Set.Iio ⊤) s
t : UpperSet (MulArchimedeanClass M)
ht : Membership.mem (γ := Set (UpperSet (MulArchimedeanClass M))) (Set.Iio ⊤) t
hst : s < t
refine : (↑(subsemigroup t) : Set M) ≠ (↑(subsemigroup s) : Set M)
⊢ (↑(subsemigroup t) : Set M) ⊂ (↑(subsemigroup s) : Set M)

Tactic:
refine Set.ssubset_iff_subset_ne.mpr ⟨by simpa [subsemigroup] using hst.le, ?_⟩

Premises used: Iff.mpr, Set.ssubset_iff_subset_ne, And.intro
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
hs : Membership.mem (γ := Set (UpperSet (MulArchimedeanClass M))) (Set.Iio ⊤) s
t : UpperSet (MulArchimedeanClass M)
ht : Membership.mem (γ := Set (UpperSet (MulArchimedeanClass M))) (Set.Iio ⊤) t
hst : s < t
contrapose! : ∀ (heq : (↑(subsemigroup t) : Set M) = (↑(subsemigroup s) : Set M)), t ≤ s
⊢ (↑(subsemigroup t) : Set M) ≠ (↑(subsemigroup s) : Set M)

Tactic:
contrapose! hst with heq
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
hs : Membership.mem (γ := Set (UpperSet (MulArchimedeanClass M))) (Set.Iio ⊤) s
t : UpperSet (MulArchimedeanClass M)
ht : Membership.mem (γ := Set (UpperSet (MulArchimedeanClass M))) (Set.Iio ⊤) t
heq : (↑(subsemigroup t) : Set M) = (↑(subsemigroup s) : Set M)
hab : t = s
⊢ t ≤ s

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
hs : Membership.mem (γ := Set (UpperSet (MulArchimedeanClass M))) (Set.Iio ⊤) s
t : UpperSet (MulArchimedeanClass M)
ht : Membership.mem (γ := Set (UpperSet (MulArchimedeanClass M))) (Set.Iio ⊤) t
heq : (↑(subsemigroup t) : Set M) = (↑(subsemigroup s) : Set M)
⊢ t = s

Tactic:
simpa [mk_surjective, subsemigroup] using heq

Premises used: MulArchimedeanClass.subsemigroup, 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
s t : UpperSet (MulArchimedeanClass M)
hst : s ≤ t
inl : ∀ (hst : ⊤ ≤ t), subgroup t ≤ subgroup ⊤
inr : ∀ (hs : s ≠ ⊤), subgroup t ≤ subgroup s
⊢ subgroup t ≤ subgroup s

Tactic:
obtain rfl | hs := eq_or_ne s ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
t : UpperSet (MulArchimedeanClass M)
hst : ⊤ ≤ t
inl inl₁ : LE.le.{u_1} (α := Subgroup M) (subgroup ⊤) (subgroup ⊤)
⊢ subgroup t ≤ subgroup ⊤

Tactic:
rw [eq_top_iff.mpr hst]

Premises used: Iff.mpr, 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
s t : UpperSet (MulArchimedeanClass M)
hst : s ≤ t
hs : s ≠ ⊤
inr : ∀ (hst : s ≤ ⊤), subgroup ⊤ ≤ subgroup s
inr₁ : ∀ (ht : t ≠ ⊤), subgroup t ≤ subgroup s
⊢ subgroup t ≤ subgroup s

Tactic:
obtain rfl | ht := eq_or_ne t ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
hs : s ≠ ⊤
hst : s ≤ ⊤
⊢ subgroup ⊤ ≤ subgroup s

Tactic:
simp