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
ι : Type u_2
inst_3 : LinearOrder ι
s_1 : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih_1 :
  StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑s : Set ι) →
    Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
hmono : StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑(Finset.cons i s hi) : Set ι)
ih : Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : Ne (α := MulArchimedeanClass M) (mk (a i)) (mk (∏ i ∈ s, a i))
hlt : LT.lt (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a i))
y : ι
hy : y ∈ Finset.cons i s hi
cons :
  ∀ (hi : y ∉ s) (hmono : StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑(Finset.cons y s hi) : Set ι))
    (hminmem : s.min' hs ∈ Finset.cons y s hi) (hne : Ne (α := MulArchimedeanClass M) (mk (a y)) (mk (∏ i ∈ s, a i)))
    (hlt : LT.lt (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a y))) (hy : y ∈ Finset.cons y s hi),
    s.min' hs ≤ y
cons₁ : ∀ (hmem : y ∈ s), s.min' hs ≤ y
⊢ s.min' hs ≤ y

Tactic:
obtain rfl | hmem := Finset.mem_cons.mp hy

Premises used: Iff.mp, Finset.mem_cons, rfl
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
ι : Type u_2
inst_3 : LinearOrder ι
s_1 : Finset ι
a : ι → M
s : Finset ι
hs : s.Nonempty
ih_1 :
  StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑s : Set ι) →
    Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
ih : Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
y : ι
hi : y ∉ s
hmono : StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑(Finset.cons y s hi) : Set ι)
hminmem : s.min' hs ∈ Finset.cons y s hi
hne : Ne (α := MulArchimedeanClass M) (mk (a y)) (mk (∏ i ∈ s, a i))
hlt : LT.lt (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a y))
hy : y ∈ Finset.cons y s hi
⊢ y ∈ (↑(Finset.cons y s hi) : Set ι)

Tactic:
simp
-- 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 : LinearOrder ι
s_1 : Finset ι
a : ι → M
s : Finset ι
hs : s.Nonempty
ih_1 :
  StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑s : Set ι) →
    Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
ih : Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
y : ι
hi : y ∉ s
hmono : StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑(Finset.cons y s hi) : Set ι)
hminmem : s.min' hs ∈ Finset.cons y s hi
hne : Ne (α := MulArchimedeanClass M) (mk (a y)) (mk (∏ i ∈ s, a i))
hlt : LT.lt (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a y))
hy : y ∈ Finset.cons y s hi
apply : LT.lt (α := MulArchimedeanClass M) ((mk ∘ a) (s.min' hs)) ((mk ∘ a) y)
⊢ s.min' hs ≤ y

Tactic:
apply ((hmono.lt_iff_lt hminmem (by simp)).mp ?_).le

Premises used: LT.lt.le, Iff.mp, StrictMonoOn.lt_iff_lt
-- 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 : LinearOrder ι
s_1 : Finset ι
a : ι → M
s : Finset ι
hs : s.Nonempty
ih_1 :
  StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑s : Set ι) →
    Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
ih : Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
y : ι
hi : y ∉ s
hmono : StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑(Finset.cons y s hi) : Set ι)
hminmem : s.min' hs ∈ Finset.cons y s hi
hne : Ne (α := MulArchimedeanClass M) (mk (a y)) (mk (∏ i ∈ s, a i))
hlt : LT.lt (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a y))
hy : y ∈ Finset.cons y s hi
⊢ LT.lt (α := MulArchimedeanClass M) (mk (a (s.min' hs))) (mk (a y))

Tactic:
rw [ih] at hlt
-- 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 : LinearOrder ι
s_1 : Finset ι
a : ι → M
s : Finset ι
hs : s.Nonempty
ih_1 :
  StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑s : Set ι) →
    Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
ih : Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
y : ι
hi : y ∉ s
hmono : StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑(Finset.cons y s hi) : Set ι)
hminmem : s.min' hs ∈ Finset.cons y s hi
hne : Ne (α := MulArchimedeanClass M) (mk (a y)) (mk (∏ i ∈ s, a i))
hlt : LT.lt (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a y))
hy : y ∈ Finset.cons y s hi
hlt₁ : LT.lt (α := MulArchimedeanClass M) (mk (a (s.min' hs))) (mk (a y))
⊢ y ∈ Finset.cons y s hi

Tactic:
rw [ih] at hlt
-- 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 : LinearOrder ι
s_1 : Finset ι
a : ι → M
s : Finset ι
hs : s.Nonempty
ih_1 :
  StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑s : Set ι) →
    Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
ih : Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
y : ι
hi : y ∉ s
hmono : StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑(Finset.cons y s hi) : Set ι)
hminmem : s.min' hs ∈ Finset.cons y s hi
hne : Ne (α := MulArchimedeanClass M) (mk (a y)) (mk (∏ i ∈ s, a i))
hlt : LT.lt (α := MulArchimedeanClass M) (mk (a (s.min' hs))) (mk (a y))
hy : y ∈ Finset.cons y s hi
⊢ LT.lt (α := MulArchimedeanClass M) ((mk ∘ a) (s.min' hs)) ((mk ∘ a) y)

Tactic:
hlt
-- 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 : LinearOrder ι
s_1 : Finset ι
a : ι → M
s : Finset ι
hs : s.Nonempty
ih_1 :
  StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑s : Set ι) →
    Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
ih : Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
y : ι
hi : y ∉ s
hmono : StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑(Finset.cons y s hi) : Set ι)
hminmem : s.min' hs ∈ Finset.cons y s hi
hne : Ne (α := MulArchimedeanClass M) (mk (a y)) (mk (∏ i ∈ s, a i))
hlt : LT.lt (α := MulArchimedeanClass M) (mk (a (s.min' hs))) (mk (a y))
hy : y ∈ Finset.cons y s hi
⊢ LT.lt (α := MulArchimedeanClass M) ((mk ∘ a) (s.min' hs)) ((mk ∘ a) y)

Tactic:
exact hlt
-- 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 : LinearOrder ι
s_1 : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih_1 :
  StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑s : Set ι) →
    Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
hmono : StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑(Finset.cons i s hi) : Set ι)
ih : Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : Ne (α := MulArchimedeanClass M) (mk (a i)) (mk (∏ i ∈ s, a i))
hlt : LT.lt (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a i))
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
⊢ s.min' hs ≤ y

Tactic:
Finset.min'_le _ _ hmem

Premises used: Finset.min'_le
-- 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 : LinearOrder ι
s_1 : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih_1 :
  StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑s : Set ι) →
    Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
hmono : StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑(Finset.cons i s hi) : Set ι)
ih : Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : Ne (α := MulArchimedeanClass M) (mk (a i)) (mk (∏ i ∈ s, a i))
hlt : LT.lt (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a i))
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
⊢ s.min' hs ≤ y

Tactic:
exact Finset.min'_le _ _ hmem

Premises used: Finset.min'_le
-- 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 : LinearOrder ι
s : Finset ι
hnonempty : s.Nonempty
a : ι → M
singleton :
  ∀ (i : ι),
    StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑{i} : Set ι) →
      Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ {i}, a i)) (mk (a (Finset.min' {i} ⋯)))
cons :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s) (hs : s.Nonempty)
    (ih :
      StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑s : Set ι) →
        Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))),
    StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑(Finset.cons i s hi) : Set ι) →
      Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ Finset.cons i s hi, a i)) (mk (a ((Finset.cons i s hi).min' ⋯)))
⊢ StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑s : Set ι) →
    Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hnonempty)))

Tactic:
induction hnonempty using Finset.Nonempty.cons_induction with
  | singleton i => simp
  | cons i s hi hs ih =>
    intro hmono
    obtain ih := ih (hmono.mono (by simp))
    rw [Finset.prod_cons]
    have hminmem : s.min' hs ∈ (Finset.cons i s hi) :=
      Finset.mem_cons_of_mem (Finset.min'_mem _ _)
    have hne : mk (a i) ≠ mk (a (s.min' hs)) := by
      by_contra h
      obtain eq := hmono.injOn (by simp) hminmem h
      rw [eq] at hi
      exact hi (Finset.min'_mem _ hs)
    rw [← ih] at hne
    obtain hlt | hlt := lt_or_gt_of_ne hne
    · rw [mk_mul_eq_mk_left hlt]
      congr
      apply le_antisymm (Finset.le_min' _ _ _ ?_) (Finset.min'_le _ _ (by simp))
      intro y hy
      obtain rfl | hmem := Finset.mem_cons.mp hy
      · rfl
      · refine (lt_of_lt_of_le ?_ (Finset.min'_le _ _ hmem)).le
        apply (hmono.lt_iff_lt (by simp) hminmem).mp
        rw [ih] at hlt
        exact hlt
    · rw [mul_comm, mk_mul_eq_mk_left hlt, ih]
      congr 2
      refine le_antisymm (Finset.le_min' _ _ _ ?_) (Finset.min'_le _ _ hminmem)
      intro y hy
      obtain rfl | hmem := Finset.mem_cons.mp hy
      · apply ((hmono.lt_iff_lt hminmem (by simp)).mp ?_).le
        rw [ih] at hlt
        exact hlt
      · exact Finset.min'_le _ _ hmem

Premises used: Finset.min'_le, le_antisymm, Finset.prod_cons, mul_comm, Finset.le_min', Singleton.singleton, 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
h : LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)
hpos : 1 ≤ a
⊢ HPow.hPow (β := ℕ) |b|ₘ 1 < |a|ₘ

Tactic:
obtain h := mk_lt_mk.mp h 1

Premises used: MulArchimedeanClass.mk_lt_mk, Iff.mp, 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
h_1 : LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)
hpos : 1 ≤ a
h : HPow.hPow (β := ℕ) |b|ₘ 1 < |a|ₘ
⊢ a⁻¹ < b ∧ b < a

Tactic:
rw [pow_one, mabs_lt, mabs_eq_self.mpr hpos] at h

Premises used: Iff.mpr, pow_one, mabs_lt, mabs_eq_self
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h_1 : LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)
hpos : 1 ≤ a
h : a⁻¹ < b ∧ b < a
⊢ b < a

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h_1 : LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)
hpos : 1 ≤ a
h : a⁻¹ < b ∧ b < a
⊢ b < a

Tactic:
exact h.2

Premises used: And.right
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h : LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)
hneg : a ≤ 1
⊢ HPow.hPow (β := ℕ) |b|ₘ 1 < |a|ₘ

Tactic:
obtain h := mk_lt_mk.mp h 1

Premises used: MulArchimedeanClass.mk_lt_mk, Iff.mp, 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
h_1 : LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)
hneg : a ≤ 1
h : HPow.hPow (β := ℕ) |b|ₘ 1 < |a|ₘ
⊢ a < b ∧ b < a⁻¹

Tactic:
rw [pow_one, mabs_lt, mabs_eq_inv_self.mpr hneg, inv_inv] at h

Premises used: Iff.mpr, inv_inv, pow_one, mabs_eq_inv_self, mabs_lt
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h_1 : LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)
hneg : a ≤ 1
h : a < b ∧ b < a⁻¹
⊢ a < b

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h_1 : LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)
hneg : a ≤ 1
h : a < b ∧ b < a⁻¹
⊢ a < b

Tactic:
exact h.1

Premises used: And.left
-- 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 : 1 < a
hab : LT.lt (α := MulArchimedeanClass M) (mk a) (mk (b / a))
this : a⁻¹ < b / a
⊢ 1 < b

Tactic:
simpa using this
-- 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 : 1 < a
hab : LT.lt (α := MulArchimedeanClass M) (mk a) (mk (b / a))
suffices : a⁻¹ < b / a
⊢ 1 < b

Tactic:
suffices a⁻¹ < b / a by
    simpa using this
-- 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 : 1 < a
hab : LT.lt (α := MulArchimedeanClass M) (mk a) (mk (b / a))
h : LT.lt (α := MulArchimedeanClass M) (mk a⁻¹) (mk (b / a))
hneg : a⁻¹ ≤ 1
⊢ a⁻¹ < b / a

Tactic:
apply lt_of_mk_lt_mk_of_le_one

Premises used: MulArchimedeanClass.lt_of_mk_lt_mk_of_le_one
-- 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 : 1 < a
hab : LT.lt (α := MulArchimedeanClass M) (mk a) (mk (b / a))
⊢ LT.lt (α := MulArchimedeanClass M) (mk a⁻¹) (mk (b / a))

Tactic:
simpa using hab
-- 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 : 1 < a
hab : LT.lt (α := MulArchimedeanClass M) (mk a) (mk (b / a))
⊢ a⁻¹ ≤ 1

Tactic:
simpa using ha.le

Premises used: 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
h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → Eq (α := MulArchimedeanClass M) (mk a) (mk b)
x y : M
hy : 1 < y
pos : ∀ (hx : x ≤ 1), ∃ (n : ℕ), x ≤ y ^ n
neg : ∀ (hx : 1 < x), ∃ (n : ℕ), x ≤ y ^ n
⊢ ∃ (n : ℕ), x ≤ y ^ n

Tactic:
by_cases! hx : x ≤ 1
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → Eq (α := MulArchimedeanClass M) (mk a) (mk b)
x y : M
hy : 1 < y
hx : x ≤ 1
h₁ : x ≤ HPow.hPow (β := ℕ) y 0
⊢ ∃ (n : ℕ), x ≤ y ^ n

Tactic:
use 0
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → Eq (α := MulArchimedeanClass M) (mk a) (mk b)
x y : M
hy : 1 < y
hx : x ≤ 1
⊢ x ≤ HPow.hPow (β := ℕ) y 0

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
h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → Eq (α := MulArchimedeanClass M) (mk a) (mk b)
x y : M
hy : 1 < y
hx : 1 < x
⊢ Eq (α := MulArchimedeanClass M) (mk x) (mk y)

Tactic:
have hxy : mk x = mk y := h x hx.ne.symm y hy.ne.symm
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → Eq (α := MulArchimedeanClass M) (mk a) (mk b)
x y : M
hy : 1 < y
hx : 1 < x
hxy : Eq (α := MulArchimedeanClass M) (mk x) (mk y)
neg : (∃ (m : ℕ), |y|ₘ ≤ |x|ₘ ^ m) → ∀ (m : ℕ) (hm : |x|ₘ ≤ |y|ₘ ^ m), ∃ (n : ℕ), x ≤ y ^ n
⊢ ∃ (n : ℕ), x ≤ y ^ n

Tactic:
obtain ⟨_, ⟨m, hm⟩⟩ := mk_eq_mk.mp hxy

Premises used: MulArchimedeanClass.mk_eq_mk, Iff.mp
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → Eq (α := MulArchimedeanClass M) (mk a) (mk b)
x y : M
hy : 1 < y
hx : 1 < x
hxy : Eq (α := MulArchimedeanClass M) (mk x) (mk y)
left : ∃ (m : ℕ), |y|ₘ ≤ |x|ₘ ^ m
m : ℕ
hm : |x|ₘ ≤ |y|ₘ ^ m
⊢ x ≤ y ^ m

Tactic:
rw [mabs_eq_self.mpr hx.le, mabs_eq_self.mpr hy.le] at hm

Premises used: Iff.mpr, LT.lt.le, mabs_eq_self
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → Eq (α := MulArchimedeanClass M) (mk a) (mk b)
x y : M
hy : 1 < y
hx : 1 < x
hxy : Eq (α := MulArchimedeanClass M) (mk x) (mk y)
left : ∃ (m : ℕ), |y|ₘ ≤ |x|ₘ ^ m
m : ℕ
hm : x ≤ y ^ m
⊢ ∃ (n : ℕ), x ≤ y ^ n

Tactic:
⟨m, hm⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → Eq (α := MulArchimedeanClass M) (mk a) (mk b)
x y : M
hy : 1 < y
hx : 1 < x
hxy : Eq (α := MulArchimedeanClass M) (mk x) (mk y)
left : ∃ (m : ℕ), |y|ₘ ≤ |x|ₘ ^ m
m : ℕ
hm : x ≤ y ^ m
⊢ ∃ (n : ℕ), x ≤ y ^ n

Tactic:
exact ⟨m, hm⟩
-- 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
ha : a ≠ 1
hb : b ≠ 1
⊢ 1 < |a|ₘ

Tactic:
simpa using ha
-- 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
ha : a ≠ 1
hb : b ≠ 1
⊢ ∃ (n : ℕ), |b|ₘ ≤ |a|ₘ ^ n

Tactic:
obtain hm := MulArchimedean.arch |b|ₘ (show 1 < |a|ₘ by simpa using ha)

Premises used: MulArchimedean.arch, mabs
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
inst_3 : MulArchimedean M
ha : a ≠ 1
hb : b ≠ 1
hm : ∃ (n : ℕ), |b|ₘ ≤ |a|ₘ ^ n
⊢ 1 < |b|ₘ

Tactic:
simpa using hb
-- 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
ha : a ≠ 1
hb : b ≠ 1
hm : ∃ (n : ℕ), |b|ₘ ≤ |a|ₘ ^ n
⊢ ∃ (n : ℕ), |a|ₘ ≤ |b|ₘ ^ n

Tactic:
obtain hn := MulArchimedean.arch |a|ₘ (show 1 < |b|ₘ by simpa using hb)

Premises used: MulArchimedean.arch, mabs
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
inst_3 : MulArchimedean M
ha : a ≠ 1
hb : b ≠ 1
hm : ∃ (n : ℕ), |b|ₘ ≤ |a|ₘ ^ n
hn : ∃ (n : ℕ), |a|ₘ ≤ |b|ₘ ^ n
⊢ Eq (α := MulArchimedeanClass M) (mk a) (mk b)

Tactic:
mk_eq_mk.mpr ⟨hm, hn⟩

Premises used: Iff.mpr, MulArchimedeanClass.mk_eq_mk, And.intro
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
inst_3 : MulArchimedean M
ha : a ≠ 1
hb : b ≠ 1
hm : ∃ (n : ℕ), |b|ₘ ≤ |a|ₘ ^ n
hn : ∃ (n : ℕ), |a|ₘ ≤ |b|ₘ ^ n
⊢ Eq (α := MulArchimedeanClass M) (mk a) (mk b)

Tactic:
exact mk_eq_mk.mpr ⟨hm, hn⟩

Premises used: Iff.mpr, MulArchimedeanClass.mk_eq_mk, And.intro
-- 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
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)
    (mk ((f : (a : M) → N) a) : MulArchimedeanClass N)

Tactic:
rfl

Premises used: MulArchimedeanClass.mk, Quot.map, Quotient.map', 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 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)
rw₂ 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)
⊢ Eq.{u_2 + 1} (α := MulArchimedeanClass N) (mk ((f : (a : M) → N) a) : MulArchimedeanClass N)
    (mk ((f : (a : M) → N) b) : MulArchimedeanClass N)

Tactic:
rw [← orderHom_mk, ← orderHom_mk, h]

Premises used: 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
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)
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)
⊢ LE.le.{u_2} (α := MulArchimedeanClass N) (mk ((f : (a : M) → N) a) : MulArchimedeanClass N)
    (mk ((f : (a : M) → N) b) : MulArchimedeanClass N)

Tactic:
rw [← orderHom_mk, ← orderHom_mk]

Premises used: 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
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:
OrderHomClass.monotone _ h

Premises used: OrderHomClass.monotone