awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
rw : LT.lt.{u_1} (α := R) (max ((f : (a : α) → R) (x + y)) ((f : (a : α) → R) 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)

Tactic:
rw [max_self, map_neg_eq_map]

Premises used: AddGroupSeminormClass.map_neg_eq_map, max_self
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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) ((f : (a : α) → R) x : R)

Tactic:
apply max_lt (lt_of_le_of_ne h1 h) h_lt

Premises used: max_lt, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
⊢ Eq.{u_1 + 1} (α := R) (max ((f : (a : α) → R) x) ((f : (a : α) → R) x) : R) ((f : (a : α) → R) x : R)

Tactic:
max_self (f x)

Premises used: max_self, DFunLike.coe
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
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)
⊢ LT.lt.{u_1} (α := R) ((f : (a : α) → R) x : R) ((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)

Premises used: max_self, HAdd.hAdd, Max.max, DFunLike.coe, Neg.neg
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
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)
⊢ 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

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
inl : Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) 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)

Tactic:
rw [add_eq_right_of_lt hna h_lt]

Premises used: IsNonarchimedean.add_eq_right_of_lt
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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) y : R) (max ((f : (a : α) → R) x) ((f : (a : α) → R) y) : R)

Tactic:
(max_eq_right_of_lt h_lt).symm

Premises used: max_eq_right_of_lt, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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) y : R) (max ((f : (a : α) → R) x) ((f : (a : α) → R) y) : R)

Tactic:
exact (max_eq_right_of_lt h_lt).symm

Premises used: max_eq_right_of_lt, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
inr : Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : 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)

Tactic:
rw [add_eq_left_of_lt hna h_lt]

Premises used: IsNonarchimedean.add_eq_left_of_lt
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 : R) (max ((f : (a : α) → R) x) ((f : (a : α) → R) y) : R)

Tactic:
(max_eq_left_of_lt h_lt).symm

Premises used: max_eq_left_of_lt, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 : R) (max ((f : (a : α) → R) x) ((f : (a : α) → R) y) : R)

Tactic:
exact (max_eq_left_of_lt h_lt).symm

Premises used: max_eq_left_of_lt, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 : β → α
hs : Ne.{u_3 + 1} (α := Multiset β) 0 0
⊢ ∃ (b : β), Membership.mem (γ := Multiset β) 0 b ∧ f (Multiset.map g 0).sum ≤ f (g b)

Tactic:
contradiction
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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
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)
⊢ ∃ b ∈ a ::ₘ s, f (Multiset.map g (a ::ₘ s)).sum ≤ f (g b)

Tactic:
simp only [Multiset.mem_cons, Multiset.map_cons, Multiset.sum_cons, exists_eq_or_imp]

Premises used: Multiset.map_cons, Multiset.mem_cons, exists_eq_or_imp, Multiset.sum_cons
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
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)
⊢ 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
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)

Tactic:
simp [h1]
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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
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)
⊢ 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
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
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)
⊢ 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

Premises used: Multiset.sum, Multiset.map, Iff.mp, le_max_iff
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
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:
.inl h4

Premises used: Or.inl
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
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:
exact .inl h4
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
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:
.inr ⟨w, h2, le_trans h4 h3⟩

Premises used: And.intro, Exists.intro, Or.inr, le_trans
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
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:
exact .inr ⟨w, h2, le_trans h4 h3⟩
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
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)
⊢ ∃ b ∈ s, f (Multiset.map g 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⟩

Premises used: Multiset.map_cons, Multiset.mem_cons, exists_eq_or_imp, Iff.mp, Multiset.sum_cons, le_max_iff
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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
hs : t.val ≠ 0
⊢ ∃ b ∈ t, f (t.sum g) ≤ f (g b)

Tactic:
apply multiset_image_add_of_nonempty hna

Premises used: IsNonarchimedean.multiset_image_add_of_nonempty
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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
⊢ t.val ≠ 0

Tactic:
simp_all [Finset.nonempty_iff_ne_empty]

Premises used: Finset.nonempty_iff_ne_empty
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 : β → α
⊢ ∃ (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:
simp
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
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)
⊢ ∃ (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

Premises used: IsNonarchimedean.multiset_image_add_of_nonempty, Multiset.cons_ne_zero
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 : β
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:
⟨b, fun _ ↦ hb1, hb2⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 : β
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:
exact ⟨b, fun _ ↦ hb1, hb2⟩
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
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)
⊢ ∃ (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)

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⟩
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 β
⊢ t.Nonempty ↔ t.val ≠ 0

Tactic:
simp [Finset.nonempty_iff_ne_empty]

Premises used: Finset.nonempty_iff_ne_empty
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 β
⊢ t.Nonempty ↔ t.val ≠ 0

Tactic:
have h1 : t.Nonempty ↔ t.val ≠ 0 := by simp [Finset.nonempty_iff_ne_empty]
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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
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)
⊢ ∃ (b : β), (t.Nonempty → b ∈ t) ∧ LE.le.{u_1} (α := R) ((f : (a : α) → R) (t.sum g) : R) ((f : (a : α) → R) (g b) : R)

Tactic:
rw [h1]
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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.val ≠ 0 → b ∈ t) ∧ LE.le.{u_1} (α := R) ((f : (a : α) → R) (t.sum g) : R) ((f : (a : α) → R) (g b) : R)

Tactic:
multiset_image_add hna g t.val

Premises used: Set.Mem, setOf, Finset.val, Multiset.Mem, IsNonarchimedean.multiset_image_add, Finset.sum