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
s t : UpperSet (MulArchimedeanClass M)
hst : s ≤ t
hs : s ≠ ⊤
ht : t ≠ ⊤
inr inr₁ inr₂ inr₃ : s ≤ t
⊢ subgroup t ≤ subgroup s

Tactic:
rwa [subgroup_strictAntiOn.le_iff_ge ht.lt_top hs.lt_top]

Premises used: MulArchimedeanClass.subgroup_strictAntiOn, StrictAntiOn.le_iff_ge, Ne.lt_top
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
c : MulArchimedeanClass M
hA : c ≠ ⊤
⊢ a ∈ c.ballSubgroup ↔ c < mk a

Tactic:
simp [hA]
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
c : MulArchimedeanClass M
⊢ a ∈ c.closedBallSubgroup ↔ c ≤ mk a

Tactic:
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} (α := Subgroup M) (subgroup ⊤) ⊥

Tactic:
subgroup_eq_bot M

Premises used: MulArchimedeanClass.subgroup_eq_bot
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
h : Eq.{u_1 + 1} (α := UpperSet (MulArchimedeanClass M)) (UpperSet.Ioi ⊤) ⊤
⊢ Eq.{u_1 + 1} (α := Subgroup M) (ballSubgroup ⊤) ⊥

Tactic:
convert! subgroup_eq_bot M

Premises used: MulArchimedeanClass.subgroup_eq_bot
-- 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} (α := UpperSet (MulArchimedeanClass M)) (UpperSet.Ioi ⊤) ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
h : ∀ (x : M), Membership.mem (γ := Subgroup M) (closedBallSubgroup ⊤) x ↔ Membership.mem (γ := Subgroup M) ⊥ x
⊢ Eq.{u_1 + 1} (α := Subgroup M) (closedBallSubgroup ⊤) ⊥

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x : M
⊢ Membership.mem (γ := Subgroup M) (closedBallSubgroup ⊤) x ↔ Membership.mem (γ := Subgroup M) ⊥ x

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 : MulArchimedeanClass M
_ : ∀ ⦃b : MulArchimedeanClass M⦄, a ≤ b → b.ballSubgroup ≤ a.ballSubgroup
⊢ ∀ ⦃b : MulArchimedeanClass M⦄, a ≤ b → b.ballSubgroup ≤ a.ballSubgroup

Tactic:
_
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : MulArchimedeanClass M
h : a ≤ b
⊢ b.ballSubgroup ≤ a.ballSubgroup

Tactic:
subgroup_antitone <| (UpperSet.Ioi_strictMono _).monotone h

Premises used: StrictMono.monotone, Set.Mem, UpperSet.Ioi_strictMono, MulArchimedeanClass.subgroup_antitone
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : MulArchimedeanClass M
h : a ≤ b
⊢ b.ballSubgroup ≤ a.ballSubgroup

Tactic:
exact subgroup_antitone <| (UpperSet.Ioi_strictMono _).monotone h

Premises used: StrictMono.monotone, UpperSet.Ioi_strictMono, MulArchimedeanClass.subgroup_antitone
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
h : a ≠ 1
⊢ Eq (α := MulArchimedeanClass M) (↑(mk a h) : MulArchimedeanClass M) (MulArchimedeanClass.mk a)

Tactic:
rfl

Premises used: MulArchimedeanClass.mk, rfl, 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
ha : a ≠ 1
b : M
hb : b ≠ 1
⊢ LE.le (α := FiniteMulArchimedeanClass M) (mk a ha) (mk b hb) ↔
    LE.le (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)

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 : M
ha : a ≠ 1
b : M
hb : b ≠ 1
⊢ LT.lt (α := FiniteMulArchimedeanClass M) (mk a ha) (mk b hb) ↔
    LT.lt (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)

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
hb : b ≠ 1
hab : a * b ≠ 1
⊢ LE.le (α := FiniteMulArchimedeanClass M) (min (mk a ha) (mk b hb)) (mk (a * b) hab)

Tactic:
MulArchimedeanClass.min_le_mk_mul a b

Premises used: MulArchimedeanClass.min_le_mk_mul, MulArchimedeanClass.mk, toAntisymmetrization
-- 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
ha : a ≠ 1
⊢ a⁻¹ ≠ 1

Tactic:
simp [ha]
-- 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 : a ≠ 1
⊢ Eq (α := FiniteMulArchimedeanClass M) (mk a⁻¹ ⋯) (mk a ha)

Tactic:
Subtype.ext (MulArchimedeanClass.mk_inv a)

Premises used: MulArchimedeanClass.mk_inv, Subtype.ext
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
motive : FiniteMulArchimedeanClass M → Prop
mk : ∀ (a : M) (ha : a ≠ 1), motive (FiniteMulArchimedeanClass.mk a ha)
⊢ ∀ (x : FiniteMulArchimedeanClass M), motive x

Tactic:
simpa [FiniteMulArchimedeanClass, MulArchimedeanClass.forall]

Premises used: MulArchimedeanClass.forall, FiniteMulArchimedeanClass
-- 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 : MulArchimedean M
A B : FiniteMulArchimedeanClass M
mk : ∀ (a : M) (ha : a ≠ 1), FiniteMulArchimedeanClass.mk a ha = B
⊢ A = B

Tactic:
induction A using ind with | mk a ha

Premises used: FiniteMulArchimedeanClass.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
inst_3 : MulArchimedean M
B : FiniteMulArchimedeanClass M
a : M
ha : a ≠ 1
mk :
  ∀ (b : M) (hb : b ≠ 1),
    Eq (α := FiniteMulArchimedeanClass M) (FiniteMulArchimedeanClass.mk a ha) (FiniteMulArchimedeanClass.mk b hb)
⊢ FiniteMulArchimedeanClass.mk a ha = B

Tactic:
induction B using ind with | mk b hb

Premises used: FiniteMulArchimedeanClass.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
inst_3 : MulArchimedean M
a : M
ha : a ≠ 1
b : M
hb : b ≠ 1
⊢ Eq (α := FiniteMulArchimedeanClass M) (mk a ha) (mk b hb)

Tactic:
simpa [mk] using MulArchimedeanClass.mk_eq_mk_of_mulArchimedean ha hb

Premises used: MulArchimedeanClass.mk_eq_mk_of_mulArchimedean, FiniteMulArchimedeanClass.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
inst_3 : Nontrivial M
obtain : ∀ (x : M) (hx : x ≠ 1), Nonempty.{u_1 + 1} (FiniteMulArchimedeanClass M)
⊢ Nonempty.{u_1 + 1} (FiniteMulArchimedeanClass M)

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
⊢ Ne (α := MulArchimedeanClass M) (↑(mk x hx) : MulArchimedeanClass M) ⊤

Tactic:
simpa using hx
-- 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
⊢ Nonempty.{u_1 + 1} (FiniteMulArchimedeanClass M)

Tactic:
exact ⟨mk x hx, by simpa using hx⟩
-- 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
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
refine_1 :
  ∀ (a b : M) (h' : Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)),
    Eq.{u_2 + 1} (α := WithTop α)
      ((fun (b : M) ↦
          (if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α) : WithTop α))
        a)
      ((fun (b : M) ↦
          (if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α) : WithTop α))
        b)
refine_2 :
  Ne.{u_2 + 1} (α := WithTop α)
    (MulArchimedeanClass.lift
      (fun (b : M) ↦ if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α)) ⋯ A)
    ⊤
⊢ α

Tactic:
refine (MulArchimedeanClass.lift
    (fun b ↦ if h : b = 1 then ⊤ else WithTop.some (f ⟨b, h⟩)) (fun a b h' ↦ ?_) A).untop ?_

Premises used: MulArchimedeanClass.lift, WithTop.some, dite, Subtype.mk, WithTop.untop, Top.top, OfNat.ofNat, Eq
-- 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
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)
pos : ∀ (ha : a = 1) (hb : b = 1), Eq.{u_2 + 1} (α := WithTop α) ⊤ ⊤
neg : ∀ (ha : a = 1) (hb : ¬b = 1), ⊤ = (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b hb)) : WithTop α)
pos₁ : ∀ (ha : ¬a = 1) (hb : b = 1), (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) a ha)) : WithTop α) = ⊤
neg₁ :
  ∀ (ha : ¬a = 1) (hb : ¬b = 1),
    (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) a ha)) : WithTop α) =
      (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b hb)) : WithTop α)
⊢ Eq.{u_2 + 1} (α := WithTop α)
    (if h : a = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) a h)) : WithTop α))
    (if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α))

Tactic:
split_ifs with ha hb hb
-- 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
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)
ha : a = 1
hb : b = 1
⊢ Eq.{u_2 + 1} (α := WithTop α) ⊤ ⊤

Tactic:
rfl
-- 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
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)
ha : a = 1
hb : ¬b = 1
⊢ ⊤ = (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b hb)) : WithTop α)

Tactic:
(hb (MulArchimedeanClass.mk_eq_top_iff.mp (ha ▸ h').symm)).elim

Premises used: False.elim, Iff.mp, 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
a_1 b_1 : M
α : Type u_2
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)
ha : a = 1
hb : ¬b = 1
⊢ ⊤ = (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b hb)) : WithTop α)

Tactic:
exact (hb (MulArchimedeanClass.mk_eq_top_iff.mp (ha ▸ h').symm)).elim

Premises used: False.elim, Iff.mp, 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
a_1 b_1 : M
α : Type u_2
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)
ha : ¬a = 1
hb : b = 1
⊢ Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) ⊤

Tactic:
apply hb ▸ h'
-- 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
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)
ha : ¬a = 1
hb : b = 1
⊢ (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) a ha)) : WithTop α) = ⊤

Tactic:
exact (ha (MulArchimedeanClass.mk_eq_top_iff.mp (by apply hb ▸ h'))).elim

Premises used: False.elim, Iff.mp, 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
a_1 b_1 : M
α : Type u_2
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)
ha : ¬a = 1
hb : ¬b = 1
⊢ Eq (α := FiniteMulArchimedeanClass M) (mk (↑(Subtype.mk (p := fun (a : M) ↦ a ≠ 1) a ha) : M) ⋯)
    (mk (↑(Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b hb) : M) ⋯)

Tactic:
simpa [mk] using h'

Premises used: FiniteMulArchimedeanClass.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
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)
ha : ¬a = 1
hb : ¬b = 1
neg neg₁ :
  (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b hb)) : WithTop α) =
    (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b hb)) : WithTop α)
⊢ (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) a ha)) : WithTop α) =
    (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b hb)) : WithTop α)

Tactic:
rw [h ⟨a, ha⟩ ⟨b, hb⟩ (by simpa [mk] using h')]

Premises used: Subtype.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
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
refine_2 :
  ∀ (a : M) (hA : Ne (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) ⊤),
    Ne.{u_2 + 1} (α := WithTop α)
      (MulArchimedeanClass.lift
        (fun (b : M) ↦ if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α)) ⋯
        (MulArchimedeanClass.mk a))
      ⊤
⊢ Ne.{u_2 + 1} (α := WithTop α)
    (MulArchimedeanClass.lift
      (fun (b : M) ↦ if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α)) ⋯ A)
    ⊤

Tactic:
induction A using MulArchimedeanClass.ind with | mk a

Premises used: FiniteMulArchimedeanClass.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
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
a : M
hA : Ne (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) ⊤
⊢ Ne.{u_2 + 1} (α := WithTop α)
    (MulArchimedeanClass.lift
      (fun (b : M) ↦ if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α)) ⋯
      (MulArchimedeanClass.mk a))
    ⊤

Tactic:
simpa using MulArchimedeanClass.mk_eq_top_iff.not.mp hA

Premises used: Iff.not, Iff.mp, 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
α : Type u_2
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
a : M
ha : a ≠ 1
⊢ lift f h (mk a ha) = f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) a ha)

Tactic:
simp [lift, mk, ha]

Premises used: FiniteMulArchimedeanClass.lift, FiniteMulArchimedeanClass.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 : { a : M // a ≠ 1 } → α
h :
  ∀ (a b : { a : M // a ≠ 1 }),
    LE.le (α := FiniteMulArchimedeanClass M) (FiniteMulArchimedeanClass.mk (↑a : M) ⋯)
        (FiniteMulArchimedeanClass.mk (↑b : M) ⋯) →
      f a ≤ f b
A B : FiniteMulArchimedeanClass M
hAB : A ≤ B
mk :
  ∀ (a : M) (ha : a ≠ 1) (hAB : FiniteMulArchimedeanClass.mk a ha ≤ B),
    lift f ⋯ (FiniteMulArchimedeanClass.mk a ha) ≤ lift f ⋯ B
⊢ lift f ⋯ A ≤ lift f ⋯ B

Tactic:
induction A using ind with | mk a ha

Premises used: FiniteMulArchimedeanClass.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 : { a : M // a ≠ 1 } → α
h :
  ∀ (a b : { a : M // a ≠ 1 }),
    LE.le (α := FiniteMulArchimedeanClass M) (FiniteMulArchimedeanClass.mk (↑a : M) ⋯)
        (FiniteMulArchimedeanClass.mk (↑b : M) ⋯) →
      f a ≤ f b
B : FiniteMulArchimedeanClass M
a : M
ha : a ≠ 1
hAB : FiniteMulArchimedeanClass.mk a ha ≤ B
mk :
  ∀ (b : M) (hb : b ≠ 1)
    (hAB :
      LE.le (α := FiniteMulArchimedeanClass M) (FiniteMulArchimedeanClass.mk a ha) (FiniteMulArchimedeanClass.mk b hb)),
    lift f ⋯ (FiniteMulArchimedeanClass.mk a ha) ≤ lift f ⋯ (FiniteMulArchimedeanClass.mk b hb)
⊢ lift f ⋯ (FiniteMulArchimedeanClass.mk a ha) ≤ lift f ⋯ B

Tactic:
induction B using ind with | mk b hb

Premises used: FiniteMulArchimedeanClass.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 : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), LE.le (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a ≤ f b
a : M
ha : a ≠ 1
b : M
hb : b ≠ 1
hAB : LE.le (α := FiniteMulArchimedeanClass M) (mk a ha) (mk b hb)
⊢ lift f ⋯ (mk a ha) ≤ lift f ⋯ (mk b hb)

Tactic:
simpa using h ⟨a, ha⟩ ⟨b, hb⟩ hAB

Premises used: Subtype.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 : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), LE.le (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a ≤ f b
a : M
ha : a ≠ 1
⊢ (liftOrderHom f h : (a : FiniteMulArchimedeanClass M) → α) (mk a ha) = f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) a ha)

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

Premises used: Eq.ge, Eq.le, FiniteMulArchimedeanClass.lift, WithTop.untop, le_antisymm, FiniteMulArchimedeanClass.lift_mk
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
A : FiniteMulArchimedeanClass M
⊢ (withTopOrderIso M : (a : WithTop (FiniteMulArchimedeanClass M)) → MulArchimedeanClass M)
      (↑A : WithTop (FiniteMulArchimedeanClass M)) =
    (↑A : MulArchimedeanClass M)

Tactic:
WithTop.subtypeOrderIso_apply_coe A

Premises used: WithTop.subtypeOrderIso_apply_coe
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
h : a ≠ 1
⊢ Eq (α := WithTop (FiniteMulArchimedeanClass M))
    ((OrderIso.symm (withTopOrderIso M) : (a : MulArchimedeanClass M) → WithTop (FiniteMulArchimedeanClass M))
        (MulArchimedeanClass.mk a) :
      WithTop (FiniteMulArchimedeanClass M))
    ((↑(mk a h) : WithTop (FiniteMulArchimedeanClass M)) : WithTop (FiniteMulArchimedeanClass M))

Tactic:
WithTop.subtypeOrderIso_symm_apply (MulArchimedeanClass.mk_eq_top_iff.ne.mpr h)

Premises used: Iff.mpr, WithTop.subtypeOrderIso_symm_apply, Iff.ne, MulArchimedeanClass.mk_eq_top_iff, FiniteMulArchimedeanClass.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
N : Type u_2
inst_3 : CommGroup N
inst_4 : LinearOrder N
inst_5 : IsOrderedMonoid N
e : OrderIso.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)
⊢ ∀ (a : MulArchimedeanClass M),
    a ≠ ⊤ ↔
      Ne.{u_2 + 1} (α := MulArchimedeanClass N)
        (((↑e : MulArchimedeanClass M ≃ MulArchimedeanClass N) : (a : MulArchimedeanClass M) → MulArchimedeanClass N)
            a :
          MulArchimedeanClass N)
        (⊤ : MulArchimedeanClass N)

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
N : Type u_2
inst_3 : CommGroup N
inst_4 : LinearOrder N
inst_5 : IsOrderedMonoid N
e : OrderIso.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)
⊢ ∀ {a b : FiniteMulArchimedeanClass M},
    LE.le.{u_2} (α := FiniteMulArchimedeanClass N)
        ((((↑e : MulArchimedeanClass M ≃ MulArchimedeanClass N).subtypeEquiv (p := fun (a : MulArchimedeanClass M) ↦
                  a ≠ ⊤) (q := fun (b : MulArchimedeanClass N) ↦ b ≠ ⊤) ⋯ :
                Equiv.{u_1 + 1, u_2 + 1} { a : MulArchimedeanClass M // a ≠ ⊤ }
                  { b : MulArchimedeanClass N // b ≠ ⊤ }) :
              (a : FiniteMulArchimedeanClass M) → FiniteMulArchimedeanClass N)
            a :
          FiniteMulArchimedeanClass N)
        ((((↑e : MulArchimedeanClass M ≃ MulArchimedeanClass N).subtypeEquiv (p := fun (a : MulArchimedeanClass M) ↦
                  a ≠ ⊤) (q := fun (b : MulArchimedeanClass N) ↦ b ≠ ⊤) ⋯ :
                Equiv.{u_1 + 1, u_2 + 1} { a : MulArchimedeanClass M // a ≠ ⊤ }
                  { b : MulArchimedeanClass N // b ≠ ⊤ }) :
              (a : FiniteMulArchimedeanClass M) → FiniteMulArchimedeanClass N)
            b :
          FiniteMulArchimedeanClass N) ↔
      a ≤ b

Tactic:
simp
-- 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
e : OrderIso.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)
a : FiniteMulArchimedeanClass M
⊢ Eq.{u_2 + 1} (α := MulArchimedeanClass N)
    ((↑((congrOrderIso e : (a : FiniteMulArchimedeanClass M) → FiniteMulArchimedeanClass N) a) :
        MulArchimedeanClass N) :
      MulArchimedeanClass N)
    ((e : (a : MulArchimedeanClass M) → MulArchimedeanClass N) (↑a : MulArchimedeanClass M) : MulArchimedeanClass N)

Tactic:
rfl

Premises used: rfl