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
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |y|ₘ ≤ |z|ₘ
inl : LE.le (α := MulArchimedeanClass M) (mk z) (mk y)
⊢ LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk (max |y|ₘ |z|ₘ))

Tactic:
rw [max_eq_right h, min_eq_right, mk_mabs]

Premises used: min_eq_right, max_eq_right, MulArchimedeanClass.mk_mabs
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |y|ₘ ≤ |z|ₘ
⊢ LE.le (α := MulArchimedeanClass M) (mk z) (mk y)

Tactic:
mk_le_mk_of_mabs h

Premises used: MulArchimedeanClass.mk_le_mk_of_mabs
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |y|ₘ ≤ |z|ₘ
⊢ LE.le (α := MulArchimedeanClass M) (mk z) (mk y)

Tactic:
exact mk_le_mk_of_mabs h

Premises used: MulArchimedeanClass.mk_le_mk_of_mabs
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |z|ₘ ≤ |y|ₘ
inr : LE.le (α := MulArchimedeanClass M) (mk y) (mk z)
⊢ LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk (max |y|ₘ |z|ₘ))

Tactic:
rw [max_eq_left h, min_eq_left, mk_mabs]

Premises used: max_eq_left, MulArchimedeanClass.mk_mabs, min_eq_left
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |z|ₘ ≤ |y|ₘ
⊢ LE.le (α := MulArchimedeanClass M) (mk y) (mk z)

Tactic:
mk_le_mk_of_mabs h

Premises used: MulArchimedeanClass.mk_le_mk_of_mabs
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |z|ₘ ≤ |y|ₘ
⊢ LE.le (α := MulArchimedeanClass M) (mk y) (mk z)

Tactic:
exact mk_le_mk_of_mabs h

Premises used: MulArchimedeanClass.mk_le_mk_of_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
by_contra! : ∀ (h : LT.lt (α := MulArchimedeanClass M) (mk (a * b)) (min (mk a) (mk b))), False
⊢ LE.le (α := MulArchimedeanClass M) (min (mk a) (mk b)) (mk (a * b))

Tactic:
by_contra! h
-- 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 * b)) (min (mk a) (mk b))
⊢ LT.lt (α := MulArchimedeanClass M) (mk (a * b)) (mk a) ∧ LT.lt (α := MulArchimedeanClass M) (mk (a * b)) (mk b)

Tactic:
rw [lt_min_iff] at h

Premises used: lt_min_iff
-- 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 * b)) (mk a) ∧ LT.lt (α := MulArchimedeanClass M) (mk (a * b)) (mk b)
⊢ HPow.hPow (β := ℕ) |a|ₘ 2 < |a|ₘ * |b|ₘ

Tactic:
have h1 := (mk_lt_mk.mp h.1 2).trans_le (mabs_mul_le _ _)
-- 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 * b)) (mk a) ∧ LT.lt (α := MulArchimedeanClass M) (mk (a * b)) (mk b)
h1 : HPow.hPow (β := ℕ) |a|ₘ 2 < |a|ₘ * |b|ₘ
⊢ HPow.hPow (β := ℕ) |b|ₘ 2 < |a|ₘ * |b|ₘ

Tactic:
have h2 := (mk_lt_mk.mp h.2 2).trans_le (mabs_mul_le _ _)
-- 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 * b)) (mk a) ∧ LT.lt (α := MulArchimedeanClass M) (mk (a * b)) (mk b)
h1 : HPow.hPow (β := ℕ) |a|ₘ 2 < |a|ₘ * |b|ₘ
h2 : HPow.hPow (β := ℕ) |b|ₘ 2 < |a|ₘ * |b|ₘ
⊢ |a|ₘ < |b|ₘ

Tactic:
simp only [mul_lt_mul_iff_left, mul_lt_mul_iff_right, pow_two] at h1 h2

Premises used: pow_two, mul_lt_mul_iff_left, mul_lt_mul_iff_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 * b)) (mk a) ∧ LT.lt (α := MulArchimedeanClass M) (mk (a * b)) (mk b)
h1 : HPow.hPow (β := ℕ) |a|ₘ 2 < |a|ₘ * |b|ₘ
h2 : HPow.hPow (β := ℕ) |b|ₘ 2 < |a|ₘ * |b|ₘ
h1₁ : |a|ₘ < |b|ₘ
⊢ |b|ₘ < |a|ₘ

Tactic:
simp only [mul_lt_mul_iff_left, mul_lt_mul_iff_right, pow_two] at h1 h2

Premises used: pow_two, mul_lt_mul_iff_left, mul_lt_mul_iff_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 * b)) (mk a) ∧ LT.lt (α := MulArchimedeanClass M) (mk (a * b)) (mk b)
h1 : |a|ₘ < |b|ₘ
h2 : |b|ₘ < |a|ₘ
⊢ False

Tactic:
h1.not_gt h2

Premises used: LT.lt.not_gt
-- 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 * b)) (mk a) ∧ LT.lt (α := MulArchimedeanClass M) (mk (a * b)) (mk b)
h1 : |a|ₘ < |b|ₘ
h2 : |b|ₘ < |a|ₘ
⊢ False

Tactic:
exact h1.not_gt h2

Premises used: LT.lt.not_gt
-- 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
⊢ LE.le (α := MulArchimedeanClass M) (min (mk a) (mk b)) (mk (a / b))

Tactic:
simpa [div_eq_mul_inv] using min_le_mk_mul (a := a) (b := b⁻¹)

Premises used: MulArchimedeanClass.min_le_mk_mul, div_eq_mul_inv, Inv.inv
-- 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
hab : LE.le (α := MulArchimedeanClass M) (mk a) (mk b)
⊢ LE.le (α := MulArchimedeanClass M) (mk a) (mk (a * b))

Tactic:
simpa [hab] using min_le_mk_mul (a := a) (b := b)

Premises used: MulArchimedeanClass.min_le_mk_mul
-- 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
hba : LE.le (α := MulArchimedeanClass M) (mk b) (mk a)
⊢ LE.le (α := MulArchimedeanClass M) (mk b) (mk (a * b))

Tactic:
simpa [hba] using min_le_mk_mul (a := a) (b := b)

Premises used: MulArchimedeanClass.min_le_mk_mul
-- 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
hab : LE.le (α := MulArchimedeanClass M) (mk a) (mk b)
⊢ LE.le (α := MulArchimedeanClass M) (mk a) (mk (a / b))

Tactic:
simpa [div_eq_mul_inv, hab] using mk_left_le_mk_mul (a := a) (b := b⁻¹)

Premises used: div_eq_mul_inv, MulArchimedeanClass.mk_left_le_mk_mul
-- 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
hba : LE.le (α := MulArchimedeanClass M) (mk b) (mk a)
⊢ LE.le (α := MulArchimedeanClass M) (mk b) (mk (a / b))

Tactic:
simpa [div_eq_mul_inv, hba] using mk_right_le_mk_mul (a := a) (b := b⁻¹)

Premises used: div_eq_mul_inv, MulArchimedeanClass.mk_right_le_mk_mul
-- 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 : LE.le (α := MulArchimedeanClass M) (mk a) (mk (a * b))
⊢ LE.le (α := MulArchimedeanClass M) (mk a) (mk b)

Tactic:
simpa using mk_left_le_mk_div h

Premises used: MulArchimedeanClass.mk_left_le_mk_div
-- 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
rw : LE.le (α := MulArchimedeanClass M) (mk b) (mk (b * a)) ↔ LE.le (α := MulArchimedeanClass M) (mk b) (mk a)
rw₁ rw₂ : LE.le (α := MulArchimedeanClass M) (mk b) (mk a) ↔ LE.le (α := MulArchimedeanClass M) (mk b) (mk a)
⊢ LE.le (α := MulArchimedeanClass M) (mk b) (mk (a * b)) ↔ LE.le (α := MulArchimedeanClass M) (mk b) (mk a)

Tactic:
rw [mul_comm, mk_left_le_mk_mul_iff]

Premises used: MulArchimedeanClass.mk_left_le_mk_mul_iff, mul_comm
-- 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 : LE.le (α := MulArchimedeanClass M) (mk a) (mk (a / b))
⊢ LE.le (α := MulArchimedeanClass M) (mk a) (mk b)

Tactic:
simpa using mk_left_le_mk_div h

Premises used: MulArchimedeanClass.mk_left_le_mk_div
-- 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
rw : LE.le (α := MulArchimedeanClass M) (mk b) (mk (b / a)) ↔ LE.le (α := MulArchimedeanClass M) (mk b) (mk a)
rw₁ rw₂ : LE.le (α := MulArchimedeanClass M) (mk b) (mk a) ↔ LE.le (α := MulArchimedeanClass M) (mk b) (mk a)
⊢ LE.le (α := MulArchimedeanClass M) (mk b) (mk (a / b)) ↔ LE.le (α := MulArchimedeanClass M) (mk b) (mk a)

Tactic:
rw [mk_div_comm, mk_left_le_mk_div_iff]

Premises used: MulArchimedeanClass.mk_left_le_mk_div_iff, MulArchimedeanClass.mk_div_comm
-- 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
⊢ LT.lt (α := MulArchimedeanClass M) (mk (a * b)) (mk a) ↔ LT.lt (α := MulArchimedeanClass M) (mk b) (mk a)

Tactic:
le_iff_le_iff_lt_iff_lt.1 mk_left_le_mk_mul_iff

Premises used: MulArchimedeanClass.mk_left_le_mk_mul_iff, le_iff_le_iff_lt_iff_lt, 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 b : M
⊢ LT.lt (α := MulArchimedeanClass M) (mk (a * b)) (mk b) ↔ LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)

Tactic:
le_iff_le_iff_lt_iff_lt.1 mk_right_le_mk_mul_iff

Premises used: le_iff_le_iff_lt_iff_lt, MulArchimedeanClass.mk_right_le_mk_mul_iff, 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 b : M
⊢ LT.lt (α := MulArchimedeanClass M) (mk (a / b)) (mk a) ↔ LT.lt (α := MulArchimedeanClass M) (mk b) (mk a)

Tactic:
le_iff_le_iff_lt_iff_lt.1 mk_left_le_mk_div_iff

Premises used: le_iff_le_iff_lt_iff_lt, MulArchimedeanClass.mk_left_le_mk_div_iff, 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 b : M
⊢ LT.lt (α := MulArchimedeanClass M) (mk (a / b)) (mk b) ↔ LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)

Tactic:
le_iff_le_iff_lt_iff_lt.1 mk_right_le_mk_div_iff

Premises used: le_iff_le_iff_lt_iff_lt, Iff.mp, MulArchimedeanClass.mk_right_le_mk_div_iff
-- 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)
⊢ Eq (α := MulArchimedeanClass M) (mk (a * b)) (mk a)

Tactic:
le_antisymm (mk_le_mk.mpr ⟨2, ?_⟩) (mk_left_le_mk_mul h.le)

Premises used: Iff.mpr, LT.lt.le, le_antisymm, Exists.intro, MulArchimedeanClass.mk_left_le_mk_mul, MulArchimedeanClass.mk_le_mk, 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 : LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)
refine : |a|ₘ ≤ HPow.hPow (β := ℕ) |a * b|ₘ 2
⊢ Eq (α := MulArchimedeanClass M) (mk (a * b)) (mk a)

Tactic:
refine le_antisymm (mk_le_mk.mpr ⟨2, ?_⟩) (mk_left_le_mk_mul h.le)

Premises used: Iff.mpr, LT.lt.le, le_antisymm, Exists.intro, MulArchimedeanClass.mk_left_le_mk_mul, MulArchimedeanClass.mk_le_mk, 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 : LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)
⊢ ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ

Tactic:
rw [mk_lt_mk] at h

Premises used: MulArchimedeanClass.mk_lt_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
h : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
apply : |b|ₘ * |b * a|ₘ ≤ HPow.hPow (β := ℕ) |a * b|ₘ 2
⊢ |a|ₘ ≤ HPow.hPow (β := ℕ) |a * b|ₘ 2

Tactic:
apply (mabs_mul' _ b).trans

Premises used: mabs_mul', LE.le.trans
-- 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 : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
rw : |b|ₘ ≤ |a * b|ₘ
⊢ |b|ₘ * |b * a|ₘ ≤ HPow.hPow (β := ℕ) |a * b|ₘ 2

Tactic:
rw [mul_comm b a, pow_two, mul_le_mul_iff_right]

Premises used: pow_two, mul_le_mul_iff_right, mul_comm
-- 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 : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
apply : |b|ₘ * |b|ₘ ≤ |b|ₘ * |a * b|ₘ
⊢ |b|ₘ ≤ |a * b|ₘ

Tactic:
apply le_of_mul_le_mul_left' (a := |b|ₘ)

Premises used: le_of_mul_le_mul_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 : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
rw : |b|ₘ * |b|ₘ ≤ |b|ₘ * |b * a|ₘ
⊢ |b|ₘ * |b|ₘ ≤ |b|ₘ * |a * b|ₘ

Tactic:
rw [mul_comm a b]

Premises used: mul_comm
-- 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 : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
⊢ |b|ₘ * |b|ₘ ≤ |b|ₘ * |b * a|ₘ

Tactic:
exact (pow_two |b|ₘ ▸ (h 2).le).trans (mabs_mul' a b)
-- 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 b) (mk a)
⊢ Eq (α := MulArchimedeanClass M) (mk (a * b)) (mk b)

Tactic:
mul_comm a b ▸ mk_mul_eq_mk_left h

Premises used: Eq.rec, mul_comm, MulArchimedeanClass.mk_mul_eq_mk_left, Eq.symm
-- 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)
⊢ Eq (α := MulArchimedeanClass M) (mk (a / b)) (mk a)

Tactic:
simpa [h, div_eq_mul_inv] using mk_mul_eq_mk_left (a := a) (b := b⁻¹)

Premises used: div_eq_mul_inv, MulArchimedeanClass.mk_mul_eq_mk_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 : LT.lt (α := MulArchimedeanClass M) (mk b) (mk a)
⊢ Eq (α := MulArchimedeanClass M) (mk (a / b)) (mk b)

Tactic:
simpa [h, div_eq_mul_inv] using mk_mul_eq_mk_right (a := a) (b := b⁻¹)

Premises used: div_eq_mul_inv, MulArchimedeanClass.mk_mul_eq_mk_right
-- 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 ι
a : ι → M
i : ι
⊢ StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑{i} : Set ι) →
    Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ {i}, a i)) (mk (a (Finset.min' {i} ⋯)))

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
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)))
hmono : StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑(Finset.cons i s hi) : Set ι)
⊢ (↑s : Set ι) ⊆ (↑(Finset.cons i 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
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)))
hmono : StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑(Finset.cons i s hi) : Set ι)
⊢ Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))

Tactic:
obtain ih := ih (hmono.mono (by simp))

Premises used: StrictMonoOn.mono
-- 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)))
cons : Eq (α := MulArchimedeanClass M) (mk (a i * ∏ x ∈ s, a x)) (mk (a ((Finset.cons i s hi).min' ⋯)))
⊢ Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ Finset.cons i s hi, a i)) (mk (a ((Finset.cons i s hi).min' ⋯)))

Tactic:
rw [Finset.prod_cons]

Premises used: Finset.prod_cons
-- 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)))
⊢ s.min' hs ∈ Finset.cons i s hi

Tactic:
have hminmem : s.min' hs ∈ (Finset.cons i s hi) :=
      Finset.mem_cons_of_mem (Finset.min'_mem _ _)
-- 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
by_contra : ∀ (h : Eq (α := MulArchimedeanClass M) (mk (a i)) (mk (a (s.min' hs)))), False
⊢ Ne (α := MulArchimedeanClass M) (mk (a i)) (mk (a (s.min' hs)))

Tactic:
by_contra h
-- 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
h : Eq (α := MulArchimedeanClass M) (mk (a i)) (mk (a (s.min' hs)))
⊢ i ∈ (↑(Finset.cons i 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
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
h : Eq (α := MulArchimedeanClass M) (mk (a i)) (mk (a (s.min' hs)))
⊢ i = s.min' hs

Tactic:
obtain eq := hmono.injOn (by simp) hminmem h

Premises used: StrictMonoOn.injOn
-- 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
h : Eq (α := MulArchimedeanClass M) (mk (a i)) (mk (a (s.min' hs)))
eq : i = s.min' hs
⊢ s.min' hs ∉ s

Tactic:
rw [eq] at hi
-- 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
h : Eq (α := MulArchimedeanClass M) (mk (a i)) (mk (a (s.min' hs)))
eq : i = s.min' hs
hi₁ : s.min' hs ∉ s
⊢ StrictMonoOn (β := MulArchimedeanClass M) (mk ∘ a) (↑s : Set ι) →
    Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))

Tactic:
rw [eq] at hi
-- 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
h : Eq (α := MulArchimedeanClass M) (mk (a i)) (mk (a (s.min' hs)))
eq : i = s.min' hs
hi₁ : s.min' hs ∉ s
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 ι)

Tactic:
rw [eq] at hi
-- 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
h : Eq (α := MulArchimedeanClass M) (mk (a i)) (mk (a (s.min' hs)))
eq : i = s.min' hs
hi₁ : s.min' hs ∉ s
ih₁ :
  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 ι)
⊢ Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))

Tactic:
rw [eq] at hi