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
β : 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:
exact multiset_image_add hna g t.val

Premises used: Finset.val, IsNonarchimedean.multiset_image_add
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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
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)
⊢ ∃ (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)

Premises used: HSub.hSub, Multiset.card, Multiset.powersetCard, IsNonarchimedean.multiset_image_add
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
rw : b ∈ powersetCard (s.card - m) s
⊢ b ≤ s ∧ b.card = s.card - m

Tactic:
rw [← mem_powersetCard]

Premises used: Multiset.mem_powersetCard
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 ∈ powersetCard (s.card - m) s

Tactic:
hb_in (card_pos.mp
      (card_powersetCard (s.card - m) s ▸ Nat.choose_pos ((card s).sub_le m)))

Premises used: HSub.hSub, Eq.rec, Nat.sub_le, Multiset.card_powersetCard, Nat.choose_pos, Multiset.card_pos, Iff.mp, Multiset.card, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 ∈ powersetCard (s.card - m) s

Tactic:
exact hb_in (card_pos.mp
      (card_powersetCard (s.card - m) s ▸ Nat.choose_pos ((card s).sub_le m)))

Premises used: HSub.hSub, Eq.rec, Nat.sub_le, Multiset.card_powersetCard, Nat.choose_pos, Multiset.card_pos, Iff.mp, Multiset.card, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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

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)))
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
hb : b ≤ s ∧ b.card = s.card - m
⊢ ∃ (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:
⟨b, hb.2, fun x hx ↦ mem_of_le hb.left hx, hb_le⟩

Premises used: Multiset.mem_of_le, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
hb : b ≤ s ∧ b.card = s.card - m
⊢ ∃ (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:
exact ⟨b, hb.2, fun x hx ↦ mem_of_le hb.left hx, hb_le⟩
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 : ℕ
set :
  let 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)
⊢ ∃ (u : ↥(powersetCard (#s - m) s)),
    LE.le.{u_1} (α := R) ((f : (a : α) → R) (∑ t ∈ powersetCard (#s - m) s, ∏ i ∈ t, -b i) : R)
      ((f : (a : α) → R) (∏ i ∈ (↑u : Finset β), -b i) : R)

Tactic:
set g := fun t : Finset β ↦ t.prod fun i : β ↦ - b i

Premises used: Finset.prod, Neg.neg
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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
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)
⊢ ∃ (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)

Premises used: IsNonarchimedean.finset_image_add, HSub.hSub, Finset.powersetCard, Finset.card
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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_1 : β → α
m : ℕ
g : (t : Finset β) → α := fun (t : Finset β) ↦ ∏ i ∈ t, -b_1 i
b : Finset β
hb_in : (powersetCard (#s - m) s).Nonempty → b ∈ 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) : 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_1 i) : R)

Tactic:
⟨⟨b, hb_in (powersetCard_nonempty.mpr (Nat.sub_le s.card m))⟩, hb⟩

Premises used: Iff.mpr, Nat.sub_le, Subtype.mk, Exists.intro, Finset.powersetCard_nonempty, Finset.card
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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_1 : β → α
m : ℕ
g : (t : Finset β) → α := fun (t : Finset β) ↦ ∏ i ∈ t, -b_1 i
b : Finset β
hb_in : (powersetCard (#s - m) s).Nonempty → b ∈ 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) : 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_1 i) : R)

Tactic:
exact ⟨⟨b, hb_in (powersetCard_nonempty.mpr (Nat.sub_le s.card m))⟩, hb⟩
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
Goal:
R : Type u_1
inst : LinearOrder R
α : Type u_2
β : Type u_3
inst_1 : AddCommMonoid α
f : α → R
nonarch : IsNonarchimedean f
s : Finset β
l : β → α
i : β
⊢ f (∑ i ∈ {i}, l i) ≤ sup' {i} ⋯ fun (i : β) ↦ f (l i)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 : f (l i + ∑ i ∈ s, l i) ≤ f (l i) ∨ ∃ a ∈ s, f (l i + ∑ i ∈ s, l i) ≤ f (l a)
⊢ f (∑ i ∈ Finset.cons i s h, l i) ≤ (Finset.cons i s h).sup' ⋯ fun (i : β) ↦ f (l i)

Tactic:
simp only [sum_cons, le_sup'_iff, mem_cons, exists_eq_or_imp]

Premises used: Finset.le_sup'_iff, Finset.sum_cons, exists_eq_or_imp, Finset.mem_cons
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 : 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) ∨ ∃ a ∈ s, f (l i + ∑ i ∈ s, l i) ≤ f (l a)

Tactic:
rw [← le_sup'_iff hs]

Premises used: Finset.le_sup'_iff
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
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)
⊢ 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₂

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

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 α
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)
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:
exact .inl h₁
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
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:
.inr <| le_trans h₂ hind

Premises used: 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 α
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)
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:
exact .inr <| le_trans h₂ hind

Premises used: 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 α
f : α → R
nonarch : IsNonarchimedean f
s : Finset β
hnonempty : s.Nonempty
l : β → α
singleton : ∀ (i : β), f (∑ i ∈ {i}, l i) ≤ sup' {i} ⋯ fun (i : β) ↦ f (l i)
cons :
  ∀ (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 ∈ Finset.cons i s h, l i) ≤ (Finset.cons i s h).sup' ⋯ fun (i : β) ↦ f (l i)
⊢ f (∑ i ∈ s, l i) ≤ s.sup' hnonempty fun (i : β) ↦ f (l i)

Tactic:
induction hnonempty using Nonempty.cons_induction with
  | singleton i => simp
  | cons i s _ hs hind =>
    simp only [sum_cons, le_sup'_iff, mem_cons, exists_eq_or_imp]
    rw [← le_sup'_iff hs]
    rcases le_max_iff.mp <| nonarch (l i) (∑ i ∈ s, l i) with h₁ | h₂
    · exact .inl h₁
    · exact .inr <| le_trans h₂ hind

Premises used: Finset.le_sup'_iff, Finset.sum_cons, Finset.cons, exists_eq_or_imp, Iff.mp, Singleton.singleton, le_max_iff, Finset.mem_cons
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
α : Type u_2
β : Type u_3
F : Type u_4
inst_2 : AddCommGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
nonarch : IsNonarchimedean.{u_1, u_2} (R := R) (α := α) (⇑f : (a : α) → R)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)
w : β
h : k ∈ s
⊢ s.Nonempty

Tactic:
use k
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
α : Type u_2
β : Type u_3
F : Type u_4
inst_2 : AddCommGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
nonarch : IsNonarchimedean.{u_1, u_2} (R := R) (α := α) (⇑f : (a : α) → R)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)
⊢ s.Nonempty

Tactic:
have : s.Nonempty := by use k
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
α : Type u_2
β : Type u_3
F : Type u_4
inst_2 : AddCommGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
nonarch : IsNonarchimedean.{u_1, u_2} (R := R) (α := α) (⇑f : (a : α) → R)
s : Finset β
l : β → α
a k : β
hk : Membership.mem (γ := Finset β) {a} k
hmax :
  ∀ (j : β),
    Membership.mem (γ := Finset β) {a} j →
      j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ {a}, l i) : R) ((f : (a : α) → R) (l k) : R)

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
α : Type u_2
β : Type u_3
F : Type u_4
inst_2 : AddCommGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
nonarch : IsNonarchimedean.{u_1, u_2} (R := R) (α := α) (⇑f : (a : α) → R)
s_1 : Finset β
l : β → α
a : β
s : Finset β
h : a ∉ s
hs : s.Nonempty
h_1 :
  ∀ {k : β} (hk : k ∈ s)
    (hmax : ∀ j ∈ s, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ s, l i) : R) ((f : (a : α) → R) (l k) : R)
k : β
hk : k ∈ cons a s h
hmax : ∀ j ∈ cons a s h, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)
pos :
  ∀ (ha : k = a), Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ cons a s h, l i) : R) ((f : (a : α) → R) (l k) : R)
neg :
  ∀ (ha : ¬k = a), Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ cons a s h, l i) : R) ((f : (a : α) → R) (l k) : R)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ cons a s h, l i) : R) ((f : (a : α) → R) (l k) : R)

Tactic:
by_cases ha : k = a
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
α : Type u_2
β : Type u_3
F : Type u_4
inst_2 : AddCommGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
nonarch : IsNonarchimedean.{u_1, u_2} (R := R) (α := α) (⇑f : (a : α) → R)
s_1 : Finset β
l : β → α
a : β
s : Finset β
h : a ∉ s
hs : s.Nonempty
h_1 :
  ∀ {k : β} (hk : k ∈ s)
    (hmax : ∀ j ∈ s, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ s, l i) : R) ((f : (a : α) → R) (l k) : R)
k : β
hk : k ∈ cons a s h
hmax : ∀ j ∈ cons a s h, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)
ha : k = a
pos : Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (l a + ∑ x ∈ s, l x) : R) ((f : (a : α) → R) (l a) : R)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ cons a s h, l i) : R) ((f : (a : α) → R) (l k) : R)

Tactic:
rw [sum_cons, ha]

Premises used: Finset.sum_cons
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
α : Type u_2
β : Type u_3
F : Type u_4
inst_2 : AddCommGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
nonarch : IsNonarchimedean.{u_1, u_2} (R := R) (α := α) (⇑f : (a : α) → R)
s_1 : Finset β
l : β → α
a : β
s : Finset β
h : a ∉ s
hs : s.Nonempty
h_1 :
  ∀ {k : β} (hk : k ∈ s)
    (hmax : ∀ j ∈ s, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ s, l i) : R) ((f : (a : α) → R) (l k) : R)
k : β
hk : k ∈ cons a s h
hmax : ∀ j ∈ cons a s h, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)
ha : k = a
pos : LT.lt.{u_1} (α := R) ((f : (a : α) → R) (∑ x ∈ s, l x) : R) ((f : (a : α) → R) (l a) : R)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (l a + ∑ x ∈ s, l x) : R) ((f : (a : α) → R) (l a) : R)

Tactic:
apply add_eq_left_of_lt nonarch

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
α : Type u_2
β : Type u_3
F : Type u_4
inst_2 : AddCommGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
nonarch : IsNonarchimedean.{u_1, u_2} (R := R) (α := α) (⇑f : (a : α) → R)
s_1 : Finset β
l : β → α
a : β
s : Finset β
h : a ∉ s
hs : s.Nonempty
h_1 :
  ∀ {k : β} (hk : k ∈ s)
    (hmax : ∀ j ∈ s, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ s, l i) : R) ((f : (a : α) → R) (l k) : R)
k : β
hk : k ∈ cons a s h
hmax : ∀ j ∈ cons a s h, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)
ha : k = a
pos : LT.lt.{u_1} (α := R) (s.sup' hs fun (i : β) ↦ (f : (a : α) → R) (l i) : R) ((f : (a : α) → R) (l a) : R)
⊢ LT.lt.{u_1} (α := R) ((f : (a : α) → R) (∑ x ∈ s, l x) : R) ((f : (a : α) → R) (l a) : R)

Tactic:
grw [apply_sum_le_sup nonarch hs]

Premises used: IsNonarchimedean.apply_sum_le_sup
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
α : Type u_2
β : Type u_3
F : Type u_4
inst_2 : AddCommGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
nonarch : IsNonarchimedean.{u_1, u_2} (R := R) (α := α) (⇑f : (a : α) → R)
s_1 : Finset β
l : β → α
a : β
s : Finset β
h : a ∉ s
hs : s.Nonempty
h_1 :
  ∀ {k : β} (hk : k ∈ s)
    (hmax : ∀ j ∈ s, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ s, l i) : R) ((f : (a : α) → R) (l k) : R)
k : β
hk : k ∈ cons a s h
hmax : ∀ j ∈ cons a s h, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)
ha : k = a
⊢ LT.lt.{u_1} (α := R) (s.sup' hs fun (i : β) ↦ (f : (a : α) → R) (l i) : R) ((f : (a : α) → R) (l a) : R)

Tactic:
grind [sup'_lt_iff]

Premises used: Finset.sup'_lt_iff