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
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 ι)
ih₂ : Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
⊢ s.min' hs ∈ Finset.cons i s hi

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 ι)
ih₂ : Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
hminmem₁ : s.min' hs ∈ Finset.cons i s hi
⊢ Eq (α := MulArchimedeanClass M) (mk (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)))
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:
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_1 : i ∉ s
hs : s.Nonempty
hi : s.min' hs ∉ s
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_1) : Set ι)
ih : Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
hminmem : s.min' hs ∈ Finset.cons i s hi_1
h : Eq (α := MulArchimedeanClass M) (mk (a i)) (mk (a (s.min' hs)))
eq : i = s.min' hs
⊢ False

Tactic:
hi (Finset.min'_mem _ hs)

Premises used: 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_1 : i ∉ s
hs : s.Nonempty
hi : s.min' hs ∉ s
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_1) : Set ι)
ih : Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
hminmem : s.min' hs ∈ Finset.cons i s hi_1
h : Eq (α := MulArchimedeanClass M) (mk (a i)) (mk (a (s.min' hs)))
eq : i = s.min' hs
⊢ False

Tactic:
exact hi (Finset.min'_mem _ hs)

Premises used: 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
⊢ Ne (α := MulArchimedeanClass M) (mk (a i)) (mk (a (s.min' hs)))

Tactic:
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)
-- 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 (a (s.min' hs)))
⊢ Ne (α := MulArchimedeanClass M) (mk (a i)) (mk (∏ i ∈ s, a i))

Tactic:
rw [← ih] at hne
-- 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))
cons :
  ∀ (hlt : LT.lt (α := MulArchimedeanClass M) (mk (a i)) (mk (∏ i ∈ s, a i))),
    Eq (α := MulArchimedeanClass M) (mk (a i * ∏ x ∈ s, a x)) (mk (a ((Finset.cons i s hi).min' ⋯)))
cons₁ :
  ∀ (hlt : LT.lt (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a i))),
    Eq (α := MulArchimedeanClass M) (mk (a i * ∏ x ∈ s, a x)) (mk (a ((Finset.cons i s hi).min' ⋯)))
⊢ Eq (α := MulArchimedeanClass M) (mk (a i * ∏ x ∈ s, a x)) (mk (a ((Finset.cons i s hi).min' ⋯)))

Tactic:
obtain hlt | hlt := lt_or_gt_of_ne hne

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

Tactic:
rw [mk_mul_eq_mk_left hlt]

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

Tactic:
congr
-- 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 (a i)) (mk (∏ i ∈ s, a i))
⊢ i ∈ Finset.cons i s hi

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
hne : Ne (α := MulArchimedeanClass M) (mk (a i)) (mk (∏ i ∈ s, a i))
hlt : LT.lt (α := MulArchimedeanClass M) (mk (a i)) (mk (∏ i ∈ s, a i))
apply : ∀ y ∈ Finset.cons i s hi, i ≤ y
⊢ i = (Finset.cons i s hi).min' ⋯

Tactic:
apply le_antisymm (Finset.le_min' _ _ _ ?_) (Finset.min'_le _ _ (by simp))

Premises used: Finset.min'_le, le_antisymm, Finset.le_min'
-- 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 (a i)) (mk (∏ i ∈ s, a i))
y : ι
hy : y ∈ Finset.cons i s hi
inl :
  ∀ (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 y)) (mk (∏ i ∈ s, a i))) (hy : y ∈ Finset.cons y s hi), y ≤ y
inr : ∀ (hmem : y ∈ s), i ≤ y
⊢ i ≤ 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 (a y)) (mk (∏ i ∈ s, a i))
hy : y ∈ Finset.cons y s hi
⊢ y ≤ y

Tactic:
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
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 (a i)) (mk (∏ i ∈ s, a i))
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
⊢ i ≤ y

Tactic:
(lt_of_lt_of_le ?_ (Finset.min'_le _ _ hmem)).le

Premises used: Finset.min'_le, LT.lt.le, lt_of_lt_of_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 (a i)) (mk (∏ i ∈ s, a i))
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
inr : i < s.min' ⋯
⊢ i ≤ y

Tactic:
refine (lt_of_lt_of_le ?_ (Finset.min'_le _ _ hmem)).le

Premises used: Finset.min'_le, LT.lt.le, lt_of_lt_of_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 (a i)) (mk (∏ i ∈ s, a i))
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
⊢ 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
hne : Ne (α := MulArchimedeanClass M) (mk (a i)) (mk (∏ i ∈ s, a i))
hlt : LT.lt (α := MulArchimedeanClass M) (mk (a i)) (mk (∏ i ∈ s, a i))
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
inr : LT.lt (α := MulArchimedeanClass M) ((mk ∘ a) i) ((mk ∘ a) (s.min' hs))
⊢ i < s.min' ⋯

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

Premises used: 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
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 (a i)) (mk (∏ i ∈ s, a i))
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
inr :
  ∀ (hlt : LT.lt (α := MulArchimedeanClass M) (mk (a i)) (mk (a (s.min' hs)))) (y : ι) (hy : y ∈ Finset.cons i s hi)
    (hmem : y ∈ s), LT.lt (α := MulArchimedeanClass M) ((mk ∘ a) i) ((mk ∘ a) (s.min' hs))
⊢ LT.lt (α := MulArchimedeanClass M) ((mk ∘ a) i) ((mk ∘ a) (s.min' hs))

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
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 (a i)) (mk (a (s.min' hs)))
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
⊢ LT.lt (α := MulArchimedeanClass M) ((mk ∘ a) i) ((mk ∘ a) (s.min' hs))

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
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 (a i)) (mk (a (s.min' hs)))
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
⊢ LT.lt (α := MulArchimedeanClass M) ((mk ∘ a) i) ((mk ∘ a) (s.min' hs))

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

Tactic:
rw [mul_comm, mk_mul_eq_mk_left hlt, ih]

Premises used: mul_comm, 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
ι : 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))
cons : s.min' hs = (Finset.cons i s hi).min' ⋯
⊢ Eq (α := MulArchimedeanClass M) (mk (a (s.min' hs))) (mk (a ((Finset.cons i s hi).min' ⋯)))

Tactic:
congr 2
-- 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))
⊢ s.min' hs = (Finset.cons i s hi).min' ⋯

Tactic:
le_antisymm (Finset.le_min' _ _ _ ?_) (Finset.min'_le _ _ hminmem)

Premises used: Finset.min'_le, le_antisymm, Finset.le_min'
-- 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))
cons : ∀ y ∈ Finset.cons i s hi, s.min' hs ≤ y
⊢ s.min' hs = (Finset.cons i s hi).min' ⋯

Tactic:
refine le_antisymm (Finset.le_min' _ _ _ ?_) (Finset.min'_le _ _ hminmem)

Premises used: Finset.min'_le, le_antisymm, Finset.le_min'