awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Iic 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Iic 1) b
hab : a ≤ b
⊢ LE.le (α := MulArchimedeanClass M) (mk a) (mk b)
have contrapose! : ∀ (hab : LT.lt (α := MulArchimedeanClass M) (mk b) (mk a)), b < a
Tactic: contrapose! hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Iic 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Iic 1) b
hab : LT.lt (α := MulArchimedeanClass M) (mk b) (mk a)
⊢ b < a
have hab₁ : ∀ (n : ℕ), |a|ₘ ^ n < |b|ₘ
Tactic: rw [mk_lt_mk] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Iic 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Iic 1) b
hab : ∀ (n : ℕ), |a|ₘ ^ n < |b|ₘ
⊢ b < a
have h : HPow.hPow (β := ℕ) |a|ₘ 1 < |b|ₘ
Tactic: obtain h := hab 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Iic 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Iic 1) b
hab : ∀ (n : ℕ), |a|ₘ ^ n < |b|ₘ
h : HPow.hPow (β := ℕ) |a|ₘ 1 < |b|ₘ
⊢ b < a
have h₁ : HPow.hPow (β := ℕ) a⁻¹ 1 < b⁻¹
Tactic: rw [mabs_eq_inv_self.mpr ha, mabs_eq_inv_self.mpr hb] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h : |a|ₘ ≤ |b|ₘ
⊢ LE.le (α := MulArchimedeanClass M) (mk b) (mk a)
have rw : LE.le (α := MulArchimedeanClass M) (mk |b|ₘ) (mk |a|ₘ)
Tactic: rw [← mk_mabs a, ← mk_mabs]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h : |a|ₘ ≤ |b|ₘ
⊢ LE.le (α := MulArchimedeanClass M) (mk |b|ₘ) (mk |a|ₘ)
have ha : 1 ≤ |a|ₘ
Tactic: have ha := one_le_mabs a
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
⊢ LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk x)
have H : |x|ₘ ≤ max |y|ₘ |z|ₘ
Tactic: have H := mabs_le_max_mabs_mabs hy hz
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ max |y|ₘ |z|ₘ
⊢ LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk x)
have H₁ : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
Tactic: rw [← mabs_of_one_le (le_max_of_le_left (one_le_mabs y))] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
⊢ LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk x)
have apply : LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk (max |y|ₘ |z|ₘ))
Tactic: apply (mk_le_mk_of_mabs H).trans'
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
⊢ LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk (max |y|ₘ |z|ₘ))
have inl : ∀ (h : |y|ₘ ≤ |z|ₘ), LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk (max |y|ₘ |z|ₘ))
Tactic: obtain h | h := le_total |y|ₘ |z|ₘ
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
inl : ∀ (h : |y|ₘ ≤ |z|ₘ), LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk (max |y|ₘ |z|ₘ))
⊢ LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk (max |y|ₘ |z|ₘ))
have inr : ∀ (h : |z|ₘ ≤ |y|ₘ), LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk (max |y|ₘ |z|ₘ))
Tactic: obtain h | h := le_total |y|ₘ |z|ₘ
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |y|ₘ ≤ |z|ₘ
⊢ LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk (max |y|ₘ |z|ₘ))
have inl : LE.le (α := MulArchimedeanClass M) (mk z) (mk y)
Tactic: rw [max_eq_right h, min_eq_right, mk_mabs]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |z|ₘ ≤ |y|ₘ
⊢ LE.le (α := MulArchimedeanClass M) (min (mk y) (mk z)) (mk (max |y|ₘ |z|ₘ))
have inr : LE.le (α := MulArchimedeanClass M) (mk y) (mk z)
Tactic: rw [max_eq_left h, min_eq_left, mk_mabs]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
⊢ LE.le (α := MulArchimedeanClass M) (min (mk a) (mk b)) (mk (a * b))
have by_contra! : ∀ (h : LT.lt (α := MulArchimedeanClass M) (mk (a * b)) (min (mk a) (mk b))), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h : LT.lt (α := MulArchimedeanClass M) (mk (a * b)) (min (mk a) (mk b))
⊢ False
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h : LT.lt (α := MulArchimedeanClass M) (mk (a * b)) (mk a) ∧ LT.lt (α := MulArchimedeanClass M) (mk (a * b)) (mk b)
⊢ False
have h1 : HPow.hPow (β := ℕ) |a|ₘ 2 < |a|ₘ * |b|ₘ
Tactic: have h1 := (mk_lt_mk.mp h.1 2).trans_le (mabs_mul_le _ _)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a 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|ₘ
⊢ False
have h2 : HPow.hPow (β := ℕ) |b|ₘ 2 < |a|ₘ * |b|ₘ
Tactic: have h2 := (mk_lt_mk.mp h.2 2).trans_le (mabs_mul_le _ _)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a 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|ₘ
⊢ False
have h1₁ : |a|ₘ < |b|ₘ
Tactic: simp only [mul_lt_mul_iff_left, mul_lt_mul_iff_right, pow_two] at h1 h2
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a 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|ₘ
⊢ False
have h2₁ : |b|ₘ < |a|ₘ
Tactic: simp only [mul_lt_mul_iff_left, mul_lt_mul_iff_right, pow_two] at h1 h2
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
⊢ LE.le (α := MulArchimedeanClass M) (mk b) (mk (a * b)) ↔ LE.le (α := MulArchimedeanClass M) (mk b) (mk a)
have rw : LE.le (α := MulArchimedeanClass M) (mk b) (mk (b * a)) ↔ LE.le (α := MulArchimedeanClass M) (mk b) (mk a)
Tactic: rw [mul_comm, mk_left_le_mk_mul_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
rw : LE.le (α := MulArchimedeanClass M) (mk b) (mk (b * 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)
have rw₁ : LE.le (α := MulArchimedeanClass M) (mk b) (mk a) ↔ LE.le (α := MulArchimedeanClass M) (mk b) (mk a)
Tactic: rw [mul_comm, mk_left_le_mk_mul_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
⊢ LE.le (α := MulArchimedeanClass M) (mk b) (mk (a / b)) ↔ LE.le (α := MulArchimedeanClass M) (mk b) (mk a)
have rw : LE.le (α := MulArchimedeanClass M) (mk b) (mk (b / a)) ↔ LE.le (α := MulArchimedeanClass M) (mk b) (mk a)
Tactic: rw [mk_div_comm, mk_left_le_mk_div_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
rw : LE.le (α := MulArchimedeanClass M) (mk b) (mk (b / 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)
have rw₁ : LE.le (α := MulArchimedeanClass M) (mk b) (mk a) ↔ LE.le (α := MulArchimedeanClass M) (mk b) (mk a)
Tactic: rw [mk_div_comm, mk_left_le_mk_div_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h : LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)
⊢ Eq (α := MulArchimedeanClass M) (mk (a * b)) (mk a)
have refine : |a|ₘ ≤ HPow.hPow (β := ℕ) |a * b|ₘ 2
Tactic: refine le_antisymm (mk_le_mk.mpr ⟨2, ?_⟩) (mk_left_le_mk_mul h.le)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h : LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)
⊢ |a|ₘ ≤ HPow.hPow (β := ℕ) |a * b|ₘ 2
have h₁ : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
Tactic: rw [mk_lt_mk] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
⊢ |a|ₘ ≤ HPow.hPow (β := ℕ) |a * b|ₘ 2
have apply : |b|ₘ * |b * a|ₘ ≤ HPow.hPow (β := ℕ) |a * b|ₘ 2
Tactic: apply (mabs_mul' _ b).trans
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
⊢ |b|ₘ * |b * a|ₘ ≤ HPow.hPow (β := ℕ) |a * b|ₘ 2
have rw : |b|ₘ ≤ |a * b|ₘ
Tactic: rw [mul_comm b a, pow_two, mul_le_mul_iff_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
⊢ |b|ₘ ≤ |a * b|ₘ
have apply : |b|ₘ * |b|ₘ ≤ |b|ₘ * |a * b|ₘ
Tactic: apply le_of_mul_le_mul_left' (a := |b|ₘ)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
h : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
⊢ |b|ₘ * |b|ₘ ≤ |b|ₘ * |a * b|ₘ
have rw : |b|ₘ * |b|ₘ ≤ |b|ₘ * |b * a|ₘ
Tactic: rw [mul_comm a b]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
ι : 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 ∈ Finset.cons i s hi, a i)) (mk (a ((Finset.cons i s hi).min' ⋯)))
have ih₁ : Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ s, a i)) (mk (a (s.min' hs)))
Tactic: obtain ih := ih (hmono.mono (by simp))
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
ι : 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)))
⊢ Eq (α := MulArchimedeanClass M) (mk (∏ i ∈ Finset.cons i s hi, a i)) (mk (a ((Finset.cons i s hi).min' ⋯)))
have cons : Eq (α := MulArchimedeanClass M) (mk (a i * ∏ x ∈ s, a x)) (mk (a ((Finset.cons i s hi).min' sorry)))
Tactic: rw [Finset.prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
ι : 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)))
⊢ Eq (α := MulArchimedeanClass M) (mk (a i * ∏ x ∈ s, a x)) (mk (a ((Finset.cons i s hi).min' ⋯)))
have hminmem : 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 _ _)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
ι : 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)))
⊢ False
have eq : i = s.min' hs
Tactic: obtain eq := hmono.injOn (by simp) hminmem h
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
ι : 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
⊢ False
have hi₁ : s.min' hs ∉ s
Tactic: rw [eq] at hi
Cleared hypotheses: ih_1, hmono, ih, hminmem, h, eq
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
ι : 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
⊢ Eq (α := MulArchimedeanClass M) (mk (a i * ∏ x ∈ s, a x)) (mk (a ((Finset.cons i s hi).min' ⋯)))
have hne : 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)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
ι : 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)))
⊢ Eq (α := MulArchimedeanClass M) (mk (a i * ∏ x ∈ s, a x)) (mk (a ((Finset.cons i s hi).min' ⋯)))
have hne₁ : Ne (α := MulArchimedeanClass M) (mk (a i)) (mk (∏ i ∈ s, a i))
Tactic: rw [← ih] at hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
ι : 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))
⊢ Eq (α := MulArchimedeanClass M) (mk (a i * ∏ x ∈ s, a x)) (mk (a ((Finset.cons i s hi).min' ⋯)))
have 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' sorry)))
Tactic: obtain hlt | hlt := lt_or_gt_of_ne hne
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
ι : 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' ⋯)))
⊢ Eq (α := MulArchimedeanClass M) (mk (a i * ∏ x ∈ s, a x)) (mk (a ((Finset.cons i s hi).min' ⋯)))
have 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' sorry)))
Tactic: obtain hlt | hlt := lt_or_gt_of_ne hne
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
ι : 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))
⊢ Eq (α := MulArchimedeanClass M) (mk (a i * ∏ x ∈ s, a x)) (mk (a ((Finset.cons i s hi).min' ⋯)))
have cons : Eq (α := MulArchimedeanClass M) (mk (a i)) (mk (a ((Finset.cons i s hi).min' sorry)))
Tactic: rw [mk_mul_eq_mk_left hlt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
ι : 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))
⊢ Eq (α := MulArchimedeanClass M) (mk (a i)) (mk (a ((Finset.cons i s hi).min' ⋯)))
have cons : i = (Finset.cons i s hi).min' sorry
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
ι : 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).min' ⋯
have apply : ∀ y ∈ Finset.cons i s hi, i ≤ y
Tactic: apply le_antisymm (Finset.le_min' _ _ _ ?_) (Finset.min'_le _ _ (by simp))