awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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 : Eq (α := MulArchimedeanClass M) (mk a) (mk b)
rw :
  Eq.{u_2 + 1} (α := MulArchimedeanClass N)
    (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
          (a : MulArchimedeanClass M) → MulArchimedeanClass N)
        (mk a) :
      MulArchimedeanClass N)
    (mk ((f : (a : M) → N) b) : MulArchimedeanClass N)
⊢ Eq.{u_2 + 1} (α := MulArchimedeanClass N) (mk ((f : (a : M) → N) a) : MulArchimedeanClass N)
    (mk ((f : (a : M) → N) b) : MulArchimedeanClass N)
have rw₁ : Eq.{u_2 + 1} (α := 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: rw [← orderHom_mk, ← orderHom_mk, h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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 : Eq (α := MulArchimedeanClass M) (mk a) (mk b)
rw :
  Eq.{u_2 + 1} (α := MulArchimedeanClass N)
    (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
          (a : MulArchimedeanClass M) → MulArchimedeanClass N)
        (mk a) :
      MulArchimedeanClass N)
    (mk ((f : (a : M) → N) b) : 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 a) :
      MulArchimedeanClass N)
    (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
          (a : MulArchimedeanClass M) → MulArchimedeanClass N)
        (mk b) :
      MulArchimedeanClass N)
⊢ Eq.{u_2 + 1} (α := MulArchimedeanClass N) (mk ((f : (a : M) → N) a) : MulArchimedeanClass N)
    (mk ((f : (a : M) → N) b) : MulArchimedeanClass N)
have rw₂ : Eq.{u_2 + 1} (α := MulArchimedeanClass N)
  (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
        (a : MulArchimedeanClass M) → MulArchimedeanClass N)
      (mk b) :
    MulArchimedeanClass N)
  (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
        (a : MulArchimedeanClass M) → MulArchimedeanClass N)
      (mk b) :
    MulArchimedeanClass N)
Tactic: rw [← orderHom_mk, ← orderHom_mk, h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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) (mk ((f : (a : M) → N) a) : MulArchimedeanClass N)
    (mk ((f : (a : M) → N) b) : MulArchimedeanClass N)
have rw : 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: rw [← orderHom_mk, ← orderHom_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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
⊢ 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
have 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)
          (mk a) :
        MulArchimedeanClass N)
      (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
            (a : MulArchimedeanClass M) → MulArchimedeanClass N)
          b :
        MulArchimedeanClass N) →
    mk a = b
Tactic: induction a using ind with | mk a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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
⊢ Eq.{u_2 + 1} (α := 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)
          b :
        MulArchimedeanClass N) →
    mk a = b
have 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)
          (mk a) :
        MulArchimedeanClass N)
      (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
            (a : MulArchimedeanClass M) → MulArchimedeanClass N)
          (mk b) :
        MulArchimedeanClass N) →
    Eq (α := MulArchimedeanClass M) (mk a) (mk b)
Tactic: induction b using ind with | mk b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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
⊢ Eq.{u_2 + 1} (α := 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) →
    Eq (α := MulArchimedeanClass M) (mk a) (mk b)
have 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
Tactic: simp_rw [orderHom_mk, mk_eq_mk, ← map_mabs, ← map_pow]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
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
⊢ ((∃ (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
have hmono : StrictMono.{u_1, u_2} (α := M) (β := N) (⇑f : (a : M) → N)
Tactic: obtain hmono := (OrderHomClass.monotone f).strictMono_of_injective h
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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
⊢ Eq.{u_2 + 1} (α := MulArchimedeanClass N)
    (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
        (a : MulArchimedeanClass M) → MulArchimedeanClass N)
      ⊤)
    ⊤
have 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)
Tactic: rw [← mk_one, ← mk_one, orderHom_mk, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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)
⊢ Eq.{u_2 + 1} (α := MulArchimedeanClass N)
    (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
        (a : MulArchimedeanClass M) → MulArchimedeanClass N)
      ⊤)
    ⊤
have 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)
Tactic: rw [← mk_one, ← mk_one, orderHom_mk, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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)
⊢ Eq.{u_2 + 1} (α := MulArchimedeanClass N)
    (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
        (a : MulArchimedeanClass M) → MulArchimedeanClass N)
      ⊤)
    ⊤
have rw₂ : Eq.{u_2 + 1} (α := MulArchimedeanClass N) (mk ((f : (a : M) → N) 1) : MulArchimedeanClass N)
  (mk 1 : MulArchimedeanClass N)
Tactic: rw [← mk_one, ← mk_one, orderHom_mk, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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)
⊢ Eq.{u_2 + 1} (α := MulArchimedeanClass N)
    (((orderHom f : OrderHom.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)) :
        (a : MulArchimedeanClass M) → MulArchimedeanClass N)
      ⊤)
    ⊤
have rw₃ : Eq.{u_2 + 1} (α := MulArchimedeanClass N) (mk 1) (mk 1)
Tactic: rw [← mk_one, ← mk_one, orderHom_mk, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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) (mk a) (mk b) → f a ≤ f b
A B : MulArchimedeanClass M
hle : A ≤ B
⊢ lift f ⋯ A ≤ lift f ⋯ B
have mk : ∀ (a : M) (hle : mk a ≤ B), lift f sorry (mk a) ≤ lift f sorry B
Tactic: induction A using ind with | mk a
Cleared hypotheses: A, hle
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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) (mk a) (mk b) → f a ≤ f b
B : MulArchimedeanClass M
a : M
hle : mk a ≤ B
⊢ lift f ⋯ (mk a) ≤ lift f ⋯ B
have mk : ∀ (b : M) (hle : LE.le (α := MulArchimedeanClass M) (mk a) (mk b)), lift f sorry (mk a) ≤ lift f sorry (mk b)
Tactic: induction B using ind with | mk b
Cleared hypotheses: B, hle
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
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))
⊢ a * b ∈ mk ⁻¹' (↑s : Set (MulArchimedeanClass M))
have ha₁ : mk a ∈ (↑s : Set (MulArchimedeanClass M))
Tactic: rw [Set.mem_preimage] at ha hb ⊢
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
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))
⊢ a * b ∈ mk ⁻¹' (↑s : Set (MulArchimedeanClass M))
have hb₁ : mk b ∈ (↑s : Set (MulArchimedeanClass M))
Tactic: rw [Set.mem_preimage] at ha hb ⊢
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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))
⊢ mk (a * b) ∈ (↑s : Set (MulArchimedeanClass M))
have inl : ∀ (h : LE.le (α := MulArchimedeanClass M) (mk a) (mk (a * b))), mk (a * b) ∈ (↑s : Set (MulArchimedeanClass M))
Tactic: obtain h | h := min_le_iff.mp (min_le_mk_mul a b)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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))
⊢ mk (a * b) ∈ (↑s : Set (MulArchimedeanClass M))
have inr : ∀ (h : LE.le (α := MulArchimedeanClass M) (mk b) (mk (a * b))), mk (a * b) ∈ (↑s : Set (MulArchimedeanClass M))
Tactic: obtain h | h := min_le_iff.mp (min_le_mk_mul a b)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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)
have refine : (↑(subsemigroup t) : Set M) ≠ (↑(subsemigroup s) : Set M)
Tactic: refine Set.ssubset_iff_subset_ne.mpr ⟨fun _ h ↦ hst.le h, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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)
have contrapose! : ∀ (heq : (↑(subsemigroup t) : Set M) = (↑(subsemigroup s) : Set M)), t ≤ s
Tactic: contrapose! hst with heq
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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
have hab : t = s
Tactic: apply le_of_eq
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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 = ⊤
⊢ mk 1 ∈ (↑s : Set (MulArchimedeanClass M))
have obtain : ∀ (u : MulArchimedeanClass M) (hu : u ∈ (↑s : Set (MulArchimedeanClass M))), mk 1 ∈ (↑s : Set (MulArchimedeanClass M))
Tactic: obtain ⟨u, hu⟩ := UpperSet.coe_nonempty.mpr hs
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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
⊢ (↑(subgroup t) : Set M) ⊂ (↑(subgroup s) : Set M)
have rw : (↑(subgroup t) : Set M) ⊂ (↑(subsemigroup s) : Set M)
Tactic: rw [← subsemigroup_eq_subgroup_of_ne_top (Set.mem_Iio.mp hs).ne_top]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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
⊢ (↑(subgroup t) : Set M) ⊂ (↑(subsemigroup s) : Set M)
have rw : (↑(subsemigroup t) : Set M) ⊂ (↑(subsemigroup s) : Set M)
Tactic: rw [← subsemigroup_eq_subgroup_of_ne_top (Set.mem_Iio.mp ht).ne_top]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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)
have refine : (↑(subsemigroup t) : Set M) ≠ (↑(subsemigroup s) : Set M)
Tactic: refine Set.ssubset_iff_subset_ne.mpr ⟨by simpa [subsemigroup] using hst.le, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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)
have contrapose! : ∀ (heq : (↑(subsemigroup t) : Set M) = (↑(subsemigroup s) : Set M)), t ≤ s
Tactic: contrapose! hst with heq
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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
have hab : t = s
Tactic: apply le_of_eq
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
hst : s ≤ t
⊢ subgroup t ≤ subgroup s
have inl : ∀ (hst : ⊤ ≤ t), subgroup t ≤ subgroup ⊤
Tactic: obtain rfl | hs := eq_or_ne s ⊤
Cleared hypotheses: s, hst
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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 ⊤
⊢ subgroup t ≤ subgroup s
have inr : ∀ (hs : s ≠ ⊤), subgroup t ≤ subgroup s
Tactic: obtain rfl | hs := eq_or_ne s ⊤
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
t : UpperSet (MulArchimedeanClass M)
hst : ⊤ ≤ t
⊢ subgroup t ≤ subgroup ⊤
have inl : LE.le.{u_1} (α := Subgroup M) (subgroup ⊤) (subgroup ⊤)
Tactic: rw [eq_top_iff.mpr hst]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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 ≠ ⊤
⊢ subgroup t ≤ subgroup s
have inr : ∀ (hst : s ≤ ⊤), subgroup ⊤ ≤ subgroup s
Tactic: obtain rfl | ht := eq_or_ne t ⊤
Cleared hypotheses: t, hst
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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
⊢ subgroup t ≤ subgroup s
have inr₁ : ∀ (ht : t ≠ ⊤), subgroup t ≤ subgroup s
Tactic: obtain rfl | ht := eq_or_ne t ⊤
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
⊢ Eq.{u_1 + 1} (α := Subgroup M) (ballSubgroup ⊤) ⊥
have h : Eq.{u_1 + 1} (α := UpperSet (MulArchimedeanClass M)) (UpperSet.Ioi ⊤) ⊤
Tactic: convert! subgroup_eq_bot M
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
⊢ Eq.{u_1 + 1} (α := Subgroup M) (closedBallSubgroup ⊤) ⊥
have h : ∀ (x : M), Membership.mem (γ := Subgroup M) (closedBallSubgroup ⊤) x ↔ Membership.mem (γ := Subgroup M) ⊥ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
inst_3 : MulArchimedean M
A B : FiniteMulArchimedeanClass M
⊢ A = B
have mk : ∀ (a : M) (ha : a ≠ 1), mk a ha = B
Tactic: induction A using ind with | mk a ha
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a_1 b : M
inst_3 : MulArchimedean M
B : FiniteMulArchimedeanClass M
a : M
ha : a ≠ 1
⊢ mk a ha = B
have mk : ∀ (b : M) (hb : b ≠ 1), Eq (α := FiniteMulArchimedeanClass M) (mk a ha) (mk b hb)
Tactic: induction B using ind with | mk b hb
Cleared hypotheses: B