awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
x y : α
h_lt : LT.lt.{u_1} (α := R) ((f : (a : α) → R) y : R) ((f : (a : α) → R) x : R)
h : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) x : R)
h1 : LE.le.{u_1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) x : R)
⊢ LT.lt.{u_1} (α := R) (max ((f : (a : α) → R) (x + y)) ((f : (a : α) → R) (-y)) : R)
    (max ((f : (a : α) → R) x) ((f : (a : α) → R) x) : R)
have rw : LT.lt.{u_1} (α := R) (max ((f : (a : α) → R) (x + y)) ((f : (a : α) → R) y) : R) ((f : (a : α) → R) x : R)
Tactic: rw [max_self, map_neg_eq_map]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
x y : α
h_lt : LT.lt.{u_1} (α := R) ((f : (a : α) → R) y : R) ((f : (a : α) → R) x : R)
h : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) x : R)
h1 : LE.le.{u_1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) x : R)
⊢ LT.lt.{u_1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) x : R)
have f₁ : Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) (x + y + -y) : R)
Tactic: calc
    f x = f (x + y + -y) := by simp
    _   ≤ max (f (x + y)) (f (-y)) := hna (x + y) (-y)
    _   < max (f x) (f x) := by
      rw [max_self, map_neg_eq_map]
      apply max_lt (lt_of_le_of_ne h1 h) h_lt
    _   = f x := max_self (f x)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
x y : α
h_lt : LT.lt.{u_1} (α := R) ((f : (a : α) → R) y : R) ((f : (a : α) → R) x : R)
h : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) x : R)
h1 : LE.le.{u_1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) x : R)
f₁ : Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) (x + y + -y) : R)
⊢ LT.lt.{u_1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) x : R)
have f₂ : LT.lt.{u_1} (α := R) (max ((f : (a : α) → R) (x + y)) ((f : (a : α) → R) (-y)) : R)
  (max ((f : (a : α) → R) x) ((f : (a : α) → R) x) : R)
Tactic: calc
    f x = f (x + y + -y) := by simp
    _   ≤ max (f (x + y)) (f (-y)) := hna (x + y) (-y)
    _   < max (f x) (f x) := by
      rw [max_self, map_neg_eq_map]
      apply max_lt (lt_of_le_of_ne h1 h) h_lt
    _   = f x := max_self (f x)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
x y : α
hne : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) y : R)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) (max ((f : (a : α) → R) x) ((f : (a : α) → R) y) : R)
have inl : ∀ (h_lt : LT.lt.{u_1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) y : R)),
  Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) (max ((f : (a : α) → R) x) ((f : (a : α) → R) y) : R)
Tactic: rcases hne.lt_or_gt with h_lt | h_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
x y : α
hne : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) y : R)
inl :
  ∀ (h_lt : LT.lt.{u_1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) y : R)),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) (max ((f : (a : α) → R) x) ((f : (a : α) → R) y) : R)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) (max ((f : (a : α) → R) x) ((f : (a : α) → R) y) : R)
have inr : ∀ (h_lt : LT.lt.{u_1} (α := R) ((f : (a : α) → R) y : R) ((f : (a : α) → R) x : R)),
  Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) (max ((f : (a : α) → R) x) ((f : (a : α) → R) y) : R)
Tactic: rcases hne.lt_or_gt with h_lt | h_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
x y : α
hne : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) y : R)
h_lt : LT.lt.{u_1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) y : R)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) (max ((f : (a : α) → R) x) ((f : (a : α) → R) y) : R)
have inl : Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) y : R) (max ((f : (a : α) → R) x) ((f : (a : α) → R) y) : R)
Tactic: rw [add_eq_right_of_lt hna h_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
x y : α
hne : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) y : R)
h_lt : LT.lt.{u_1} (α := R) ((f : (a : α) → R) y : R) ((f : (a : α) → R) x : R)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) (max ((f : (a : α) → R) x) ((f : (a : α) → R) y) : R)
have inr : Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) (max ((f : (a : α) → R) x) ((f : (a : α) → R) y) : R)
Tactic: rw [add_eq_left_of_lt hna h_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
α : Type u_2
β : Type u_3
inst_1 : AddCommMonoid α
inst_2 : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
a : β
s : Multiset β
h : ∀ (hs : s ≠ 0), ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)
hs : a ::ₘ s ≠ 0
⊢ ∃ b ∈ a ::ₘ s, f (Multiset.map g (a ::ₘ s)).sum ≤ f (g b)
have cons : f (g a + (Multiset.map g s).sum) ≤ f (g a) ∨ ∃ a_1 ∈ s, f (g a + (Multiset.map g s).sum) ≤ f (g a_1)
Tactic: simp only [Multiset.mem_cons, Multiset.map_cons, Multiset.sum_cons, exists_eq_or_imp]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
α : Type u_2
β : Type u_3
inst_1 : AddCommMonoid α
inst_2 : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
a : β
s : Multiset β
h : ∀ (hs : s ≠ 0), ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)
hs : a ::ₘ s ≠ 0
⊢ f (g a + (Multiset.map g s).sum) ≤ f (g a) ∨ ∃ a_1 ∈ s, f (g a + (Multiset.map g s).sum) ≤ f (g a_1)
have pos : ∀ (h1 : s = 0), f (g a + (Multiset.map g s).sum) ≤ f (g a) ∨ ∃ a_1 ∈ s, f (g a + (Multiset.map g s).sum) ≤ f (g a_1)
Tactic: by_cases h1 : s = 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
α : Type u_2
β : Type u_3
inst_1 : AddCommMonoid α
inst_2 : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
a : β
s : Multiset β
h : ∀ (hs : s ≠ 0), ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)
hs : a ::ₘ s ≠ 0
pos :
  ∀ (h1 : s = 0), f (g a + (Multiset.map g s).sum) ≤ f (g a) ∨ ∃ a_1 ∈ s, f (g a + (Multiset.map g s).sum) ≤ f (g a_1)
⊢ f (g a + (Multiset.map g s).sum) ≤ f (g a) ∨ ∃ a_1 ∈ s, f (g a + (Multiset.map g s).sum) ≤ f (g a_1)
have neg : ∀ (h1 : ¬s = 0), f (g a + (Multiset.map g s).sum) ≤ f (g a) ∨ ∃ a_1 ∈ s, f (g a + (Multiset.map g s).sum) ≤ f (g a_1)
Tactic: by_cases h1 : s = 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
α : Type u_2
β : Type u_3
inst_1 : AddCommMonoid α
inst_2 : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
a : β
s : Multiset β
h : ∀ (hs : s ≠ 0), ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)
hs : a ::ₘ s ≠ 0
h1 : ¬s = 0
⊢ f (g a + (Multiset.map g s).sum) ≤ f (g a) ∨ ∃ a_1 ∈ s, f (g a + (Multiset.map g s).sum) ≤ f (g a_1)
have neg : ∀ (w : β) (h2 : w ∈ s) (h3 : f (Multiset.map g s).sum ≤ f (g w)),
  f (g a + (Multiset.map g s).sum) ≤ f (g a) ∨ ∃ a_1 ∈ s, f (g a + (Multiset.map g s).sum) ≤ f (g a_1)
Tactic: obtain ⟨w, h2, h3⟩ := h h1
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
α : Type u_2
β : Type u_3
inst_1 : AddCommMonoid α
inst_2 : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
a : β
s : Multiset β
h : ∀ (hs : s ≠ 0), ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)
hs : a ::ₘ s ≠ 0
h1 : ¬s = 0
w : β
h2 : w ∈ s
h3 : f (Multiset.map g s).sum ≤ f (g w)
⊢ f (g a + (Multiset.map g s).sum) ≤ f (g a) ∨ ∃ a_1 ∈ s, f (g a + (Multiset.map g s).sum) ≤ f (g a_1)
have neg : ∀ (h4 : f (g a + (Multiset.map g s).sum) ≤ f (g a)),
  f (g a + (Multiset.map g s).sum) ≤ f (g a) ∨ ∃ a_1 ∈ s, f (g a + (Multiset.map g s).sum) ≤ f (g a_1)
Tactic: rcases le_max_iff.mp <| hna (g a) (Multiset.map g s).sum with h4 | h4
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
α : Type u_2
β : Type u_3
inst_1 : AddCommMonoid α
inst_2 : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
a : β
s : Multiset β
h : ∀ (hs : s ≠ 0), ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)
hs : a ::ₘ s ≠ 0
h1 : ¬s = 0
w : β
h2 : w ∈ s
h3 : f (Multiset.map g s).sum ≤ f (g w)
neg :
  ∀ (h4 : f (g a + (Multiset.map g s).sum) ≤ f (g a)),
    f (g a + (Multiset.map g s).sum) ≤ f (g a) ∨ ∃ a_1 ∈ s, f (g a + (Multiset.map g s).sum) ≤ f (g a_1)
⊢ f (g a + (Multiset.map g s).sum) ≤ f (g a) ∨ ∃ a_1 ∈ s, f (g a + (Multiset.map g s).sum) ≤ f (g a_1)
have neg₁ : ∀ (h4 : f (g a + (Multiset.map g s).sum) ≤ f (Multiset.map g s).sum),
  f (g a + (Multiset.map g s).sum) ≤ f (g a) ∨ ∃ a_1 ∈ s, f (g a + (Multiset.map g s).sum) ≤ f (g a_1)
Tactic: rcases le_max_iff.mp <| hna (g a) (Multiset.map g s).sum with h4 | h4
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
α : Type u_2
β : Type u_3
inst_1 : AddCommMonoid α
inst_2 : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
s : Multiset β
hs : s ≠ 0
⊢ ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)
have empty : ∀ (hs : Ne.{u_3 + 1} (α := Multiset β) 0 0),
  ∃ (b : β), Membership.mem (γ := Multiset β) 0 b ∧ f (Multiset.map g 0).sum ≤ f (g b)
Tactic: induction s using Multiset.induction_on with
  | empty => contradiction
  | cons a s h =>
    simp only [Multiset.mem_cons, Multiset.map_cons, Multiset.sum_cons, exists_eq_or_imp]
    by_cases h1 : s = 0
    · simp [h1]
    · obtain ⟨w, h2, h3⟩ := h h1
      rcases le_max_iff.mp <| hna (g a) (Multiset.map g s).sum with h4 | h4
      · exact .inl h4
      · exact .inr ⟨w, h2, le_trans h4 h3⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
α : Type u_2
β : Type u_3
inst_1 : AddCommMonoid α
inst_2 : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
s : Multiset β
hs : s ≠ 0
empty :
  ∀ (hs : Ne.{u_3 + 1} (α := Multiset β) 0 0),
    ∃ (b : β), Membership.mem (γ := Multiset β) 0 b ∧ f (Multiset.map g 0).sum ≤ f (g b)
⊢ ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)
have cons : ∀ (a : β) (s : Multiset β) (h : ∀ (hs : s ≠ 0), ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)) (hs : a ::ₘ s ≠ 0),
  ∃ b ∈ a ::ₘ s, f (Multiset.map g (a ::ₘ s)).sum ≤ f (g b)
Tactic: induction s using Multiset.induction_on with
  | empty => contradiction
  | cons a s h =>
    simp only [Multiset.mem_cons, Multiset.map_cons, Multiset.sum_cons, exists_eq_or_imp]
    by_cases h1 : s = 0
    · simp [h1]
    · obtain ⟨w, h2, h3⟩ := h h1
      rcases le_max_iff.mp <| hna (g a) (Multiset.map g s).sum with h4 | h4
      · exact .inl h4
      · exact .inr ⟨w, h2, le_trans h4 h3⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
α : Type u_2
β : Type u_3
inst_1 : AddCommMonoid α
inst_2 : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
t : Finset β
ht : t.Nonempty
⊢ ∃ b ∈ t, f (t.sum g) ≤ f (g b)
have hs : t.val ≠ 0
Tactic: apply multiset_image_add_of_nonempty hna
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
β : Type u_4
inst_2 : AddCommMonoid α
inst_3 : FunLike F α R
inst_4 : ZeroHomClass F α R
inst_5 : NonnegHomClass F α R
inst_6 : Nonempty β
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
g : β → α
a : β
s : Multiset β
h :
  ∃ (b : β),
    (s ≠ 0 → b ∈ s) ∧ LE.le.{u_1} (α := R) ((f : (a : α) → R) (Multiset.map g s).sum : R) ((f : (a : α) → R) (g b) : R)
⊢ ∃ (b : β),
    (a ::ₘ s ≠ 0 → b ∈ a ::ₘ s) ∧
      LE.le.{u_1} (α := R) ((f : (a : α) → R) (Multiset.map g (a ::ₘ s)).sum : R) ((f : (a : α) → R) (g b) : R)
have cons : ∀ (b : β) (hb1 : b ∈ a ::ₘ s)
  (hb2 : LE.le.{u_1} (α := R) ((f : (a : α) → R) (Multiset.map g (a ::ₘ s)).sum : R) ((f : (a : α) → R) (g b) : R)),
  ∃ (b : β),
    (a ::ₘ s ≠ 0 → b ∈ a ::ₘ s) ∧
      LE.le.{u_1} (α := R) ((f : (a : α) → R) (Multiset.map g (a ::ₘ s)).sum : R) ((f : (a : α) → R) (g b) : R)
Tactic: obtain ⟨b, hb1, hb2⟩ := multiset_image_add_of_nonempty (s := a ::ₘ s)
      hna g Multiset.cons_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
β : Type u_4
inst_2 : AddCommMonoid α
inst_3 : FunLike F α R
inst_4 : ZeroHomClass F α R
inst_5 : NonnegHomClass F α R
inst_6 : Nonempty β
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
g : β → α
s : Multiset β
⊢ ∃ (b : β),
    (s ≠ 0 → b ∈ s) ∧ LE.le.{u_1} (α := R) ((f : (a : α) → R) (Multiset.map g s).sum : R) ((f : (a : α) → R) (g b) : R)
have empty : ∃ (b : β),
  (Ne.{u_4 + 1} (α := Multiset β) 0 0 → Membership.mem (γ := Multiset β) 0 b) ∧
    LE.le.{u_1} (α := R) ((f : (a : α) → R) (Multiset.map g 0).sum : R) ((f : (a : α) → R) (g b) : R)
Tactic: induction s using Multiset.induction_on with
  | empty => simp
  | cons a s h =>
    obtain ⟨b, hb1, hb2⟩ := multiset_image_add_of_nonempty (s := a ::ₘ s)
      hna g Multiset.cons_ne_zero
    exact ⟨b, fun _ ↦ hb1, hb2⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
β : Type u_4
inst_2 : AddCommMonoid α
inst_3 : FunLike F α R
inst_4 : ZeroHomClass F α R
inst_5 : NonnegHomClass F α R
inst_6 : Nonempty β
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
g : β → α
s : Multiset β
empty :
  ∃ (b : β),
    (Ne.{u_4 + 1} (α := Multiset β) 0 0 → Membership.mem (γ := Multiset β) 0 b) ∧
      LE.le.{u_1} (α := R) ((f : (a : α) → R) (Multiset.map g 0).sum : R) ((f : (a : α) → R) (g b) : R)
⊢ ∃ (b : β),
    (s ≠ 0 → b ∈ s) ∧ LE.le.{u_1} (α := R) ((f : (a : α) → R) (Multiset.map g s).sum : R) ((f : (a : α) → R) (g b) : R)
have cons : ∀ (a : β) (s : Multiset β)
  (h :
    ∃ (b : β),
      (s ≠ 0 → b ∈ s) ∧
        LE.le.{u_1} (α := R) ((f : (a : α) → R) (Multiset.map g s).sum : R) ((f : (a : α) → R) (g b) : R)),
  ∃ (b : β),
    (a ::ₘ s ≠ 0 → b ∈ a ::ₘ s) ∧
      LE.le.{u_1} (α := R) ((f : (a : α) → R) (Multiset.map g (a ::ₘ s)).sum : R) ((f : (a : α) → R) (g b) : R)
Tactic: induction s using Multiset.induction_on with
  | empty => simp
  | cons a s h =>
    obtain ⟨b, hb1, hb2⟩ := multiset_image_add_of_nonempty (s := a ::ₘ s)
      hna g Multiset.cons_ne_zero
    exact ⟨b, fun _ ↦ hb1, hb2⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
β : Type u_4
inst_2 : AddCommMonoid α
inst_3 : FunLike F α R
inst_4 : ZeroHomClass F α R
inst_5 : NonnegHomClass F α R
inst_6 : Nonempty β
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
g : β → α
t : Finset β
⊢ ∃ (b : β), (t.Nonempty → b ∈ t) ∧ LE.le.{u_1} (α := R) ((f : (a : α) → R) (t.sum g) : R) ((f : (a : α) → R) (g b) : R)
have h1 : t.Nonempty ↔ t.val ≠ 0
Tactic: have h1 : t.Nonempty ↔ t.val ≠ 0 := by simp [Finset.nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
β : Type u_4
inst_2 : AddCommMonoid α
inst_3 : FunLike F α R
inst_4 : ZeroHomClass F α R
inst_5 : NonnegHomClass F α R
inst_6 : Nonempty β
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
g : β → α
t : Finset β
h1 : t.Nonempty ↔ t.val ≠ 0
⊢ ∃ (b : β), (t.Nonempty → b ∈ t) ∧ LE.le.{u_1} (α := R) ((f : (a : α) → R) (t.sum g) : R) ((f : (a : α) → R) (g b) : R)
have rw : ∃ (b : β), (t.val ≠ 0 → b ∈ t) ∧ LE.le.{u_1} (α := R) ((f : (a : α) → R) (t.sum g) : R) ((f : (a : α) → R) (g b) : R)
Tactic: rw [h1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst_3 : CommRing α
inst_4 : FunLike F α R
inst_5 : AddGroupSeminormClass F α R
f : F
hf_na : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
s : Multiset α
m : ℕ
g : (t : Multiset α) → α := fun (t : Multiset α) ↦ t.prod
⊢ ∃ (t : Multiset α),
    t.card = s.card - m ∧
      (∀ x ∈ t, x ∈ s) ∧
        LE.le.{u_1} (α := R) ((f : (a : α) → R) (map prod (powersetCard (s.card - m) s)).sum : R)
          ((f : (a : α) → R) t.prod : R)
have obtain : ∀ (b : Multiset α) (hb_in : powersetCard (s.card - m) s ≠ 0 → b ∈ powersetCard (s.card - m) s)
  (hb_le :
    LE.le.{u_1} (α := R) ((f : (a : α) → R) (map g (powersetCard (s.card - m) s)).sum : R)
      ((f : (a : α) → R) (g b) : R)),
  ∃ (t : Multiset α),
    t.card = s.card - m ∧
      (∀ x ∈ t, x ∈ s) ∧
        LE.le.{u_1} (α := R) ((f : (a : α) → R) (map prod (powersetCard (s.card - m) s)).sum : R)
          ((f : (a : α) → R) t.prod : R)
Tactic: obtain ⟨b, hb_in, hb_le⟩ := hf_na.multiset_image_add g (powersetCard (card s - m) s)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst_3 : CommRing α
inst_4 : FunLike F α R
inst_5 : AddGroupSeminormClass F α R
f : F
hf_na : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
s : Multiset α
m : ℕ
g : (t : Multiset α) → α := fun (t : Multiset α) ↦ t.prod
b : Multiset α
hb_in : powersetCard (s.card - m) s ≠ 0 → b ∈ powersetCard (s.card - m) s
hb_le :
  LE.le.{u_1} (α := R) ((f : (a : α) → R) (map g (powersetCard (s.card - m) s)).sum : R) ((f : (a : α) → R) (g b) : R)
⊢ b ≤ s ∧ b.card = s.card - m
have rw : b ∈ powersetCard (s.card - m) s
Tactic: rw [← mem_powersetCard]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst_3 : CommRing α
inst_4 : FunLike F α R
inst_5 : AddGroupSeminormClass F α R
f : F
hf_na : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
s : Multiset α
m : ℕ
g : (t : Multiset α) → α := fun (t : Multiset α) ↦ t.prod
b : Multiset α
hb_in : powersetCard (s.card - m) s ≠ 0 → b ∈ powersetCard (s.card - m) s
hb_le :
  LE.le.{u_1} (α := R) ((f : (a : α) → R) (map g (powersetCard (s.card - m) s)).sum : R) ((f : (a : α) → R) (g b) : R)
⊢ ∃ (t : Multiset α),
    t.card = s.card - m ∧
      (∀ x ∈ t, x ∈ s) ∧
        LE.le.{u_1} (α := R) ((f : (a : α) → R) (map prod (powersetCard (s.card - m) s)).sum : R)
          ((f : (a : α) → R) t.prod : R)
have hb : b ≤ s ∧ b.card = s.card - m
Tactic: have hb : b ≤ s ∧ card b = card s - m := by
    rw [← mem_powersetCard]
    exact hb_in (card_pos.mp
      (card_powersetCard (s.card - m) s ▸ Nat.choose_pos ((card s).sub_le m)))
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
β : Type u_4
inst_3 : CommRing α
inst_4 : FunLike F α R
inst_5 : AddGroupSeminormClass F α R
f : F
hf_na : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
s : Finset β
b : β → α
m : ℕ
g : (t : Finset β) → α := fun (t : Finset β) ↦ ∏ i ∈ t, -b i
⊢ ∃ (u : ↥(powersetCard (#s - m) s)),
    LE.le.{u_1} (α := R) ((f : (a : α) → R) ((powersetCard (#s - m) s).sum g) : R)
      ((f : (a : α) → R) (∏ i ∈ (↑u : Finset β), -b i) : R)
have obtain : ∀ (b_1 : Finset β) (hb_in : (powersetCard (#s - m) s).Nonempty → b_1 ∈ powersetCard (#s - m) s)
  (hb : LE.le.{u_1} (α := R) ((f : (a : α) → R) ((powersetCard (#s - m) s).sum g) : R) ((f : (a : α) → R) (g b_1) : R)),
  ∃ (u : ↥(powersetCard (#s - m) s)),
    LE.le.{u_1} (α := R) ((f : (a : α) → R) ((powersetCard (#s - m) s).sum g) : R)
      ((f : (a : α) → R) (∏ i ∈ (↑u : Finset β), -b i) : R)
Tactic: obtain ⟨b, hb_in, hb⟩ := hf_na.finset_image_add g (powersetCard (s.card - m) s)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
α : Type u_2
β : Type u_3
inst_1 : AddCommMonoid α
f : α → R
nonarch : IsNonarchimedean f
s_1 : Finset β
l : β → α
i : β
s : Finset β
h : i ∉ s
hs : s.Nonempty
hind : f (∑ i ∈ s, l i) ≤ s.sup' hs fun (i : β) ↦ f (l i)
⊢ f (∑ i ∈ cons i s h, l i) ≤ (cons i s h).sup' ⋯ fun (i : β) ↦ f (l i)
have cons : f (l i + ∑ i ∈ s, l i) ≤ f (l i) ∨ ∃ a ∈ s, f (l i + ∑ i ∈ s, l i) ≤ f (l a)
Tactic: simp only [sum_cons, le_sup'_iff, mem_cons, exists_eq_or_imp]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
α : Type u_2
β : Type u_3
inst_1 : AddCommMonoid α
f : α → R
nonarch : IsNonarchimedean f
s_1 : Finset β
l : β → α
i : β
s : Finset β
h : i ∉ s
hs : s.Nonempty
hind : f (∑ i ∈ s, l i) ≤ s.sup' hs fun (i : β) ↦ f (l i)
⊢ f (l i + ∑ i ∈ s, l i) ≤ f (l i) ∨ ∃ a ∈ s, f (l i + ∑ i ∈ s, l i) ≤ f (l a)
have cons : f (l i + ∑ i ∈ s, l i) ≤ f (l i) ∨ f (l i + ∑ i ∈ s, l i) ≤ s.sup' hs fun (a : β) ↦ f (l a)
Tactic: rw [← le_sup'_iff hs]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
α : Type u_2
β : Type u_3
inst_1 : AddCommMonoid α
f : α → R
nonarch : IsNonarchimedean f
s_1 : Finset β
l : β → α
i : β
s : Finset β
h : i ∉ s
hs : s.Nonempty
hind : f (∑ i ∈ s, l i) ≤ s.sup' hs fun (i : β) ↦ f (l i)
⊢ f (l i + ∑ i ∈ s, l i) ≤ f (l i) ∨ f (l i + ∑ i ∈ s, l i) ≤ s.sup' hs fun (a : β) ↦ f (l a)
have cons : ∀ (h₁ : f (l i + ∑ i ∈ s, l i) ≤ f (l i)),
  f (l i + ∑ i ∈ s, l i) ≤ f (l i) ∨ f (l i + ∑ i ∈ s, l i) ≤ s.sup' hs fun (a : β) ↦ f (l a)
Tactic: rcases le_max_iff.mp <| nonarch (l i) (∑ i ∈ s, l i) with h₁ | h₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
α : Type u_2
β : Type u_3
inst_1 : AddCommMonoid α
f : α → R
nonarch : IsNonarchimedean f
s_1 : Finset β
l : β → α
i : β
s : Finset β
h : i ∉ s
hs : s.Nonempty
hind : f (∑ i ∈ s, l i) ≤ s.sup' hs fun (i : β) ↦ f (l i)
cons :
  ∀ (h₁ : f (l i + ∑ i ∈ s, l i) ≤ f (l i)),
    f (l i + ∑ i ∈ s, l i) ≤ f (l i) ∨ f (l i + ∑ i ∈ s, l i) ≤ s.sup' hs fun (a : β) ↦ f (l a)
⊢ f (l i + ∑ i ∈ s, l i) ≤ f (l i) ∨ f (l i + ∑ i ∈ s, l i) ≤ s.sup' hs fun (a : β) ↦ f (l a)
have cons₁ : ∀ (h₂ : f (l i + ∑ i ∈ s, l i) ≤ f (∑ i ∈ s, l i)),
  f (l i + ∑ i ∈ s, l i) ≤ f (l i) ∨ f (l i + ∑ i ∈ s, l i) ≤ s.sup' hs fun (a : β) ↦ f (l a)
Tactic: rcases le_max_iff.mp <| nonarch (l i) (∑ i ∈ s, l i) with h₁ | h₂