# Zulip Chat Archive

## Stream: general

### Topic: Addressing mismatch issues

#### Peter Nelson (Feb 19 2021 at 22:27):

I am working with a bunch of calculations with expressions that depend on fintype, and mismatch issues are happening. From what I understand, avoiding the mismatches arising is not feasible, but I'm looking for a non-painful way to handle them.

Each individual mismatch can generally be handled with `convert rfl`

, and indeed sometimes this will kill the problems if there is more than one. But it can be hard to handle these issues when they occur in a complicated context and the pretty-printer makes differences invisible. For instance, suppose that `a`

and `a'`

are complicated expressions in `int`

, indistinguishable without diving into implicit parameters, and hiding different `fintype`

instances. Let `b`

and `b'`

be another such pair. Now `a = a'`

and `b = b'`

can be proved with `convert rfl`

(or maybe `congr'`

), but how would I prove, say, that `-b + x + a + b' + y + z - a' = x + y + z`

, where `x`

, `y`

and `z`

are themselves long and complicated enough that copy-pasting them into a proof would double its length?

This is clearly possible, but quite awkard in the middle of a proof. Of course, a proof somehow isomorphic to `rw [(by convert rfl : a = a'), (by convert rfl : b = b')], linarith`

is what I would like. But I can't do this without hundreds of characters and underscores, because `a`

and `a'`

are syntactically identical!

Unfortunately it is hard to come up with an mwe because the nature of my gripe is 'in a complicated context', but I hope I've communicated my question.

(Of course, what I would really like is a way to seamlessly replace `fintype`

with a similar typeclass that is purely propositional, in a way that doesn't involve remaking half the API from scratch, but I don't know how to do that, either).

#### Eric Wieser (Feb 20 2021 at 00:50):

If you can't rewrite with a lemma due to a mismatching fintypes instance, that usually means that the lemma is written badly, and only applies to a specific instance

#### Kevin Buzzard (Feb 20 2021 at 00:57):

I teach my mathematician students to use `set.finite`

and [finite X] where none of these problems occur. I have no interest in constructive finiteness

#### Kevin Buzzard (Feb 20 2021 at 01:04):

oh apparently mathlib doesn't have `finite X`

-- hard luck.

#### Johan Commelin (Feb 20 2021 at 07:14):

@Peter Nelson These issues sound quite similar to the issues that we have been facing in homological algebra. Where you have a complex of (say) vector spaces, indexed by `int`

or `nat`

. And now you fact the issues that `V i`

is not the same vector space as `V (i - 1 + 1)`

. Which is of course ridiculous. We are still experimenting to find the best solution.

#### Johan Commelin (Feb 20 2021 at 07:15):

But more on topic, I think that you provide another strong datapoint for the need of a propositional analogue of `fintype`

.

#### Kevin Buzzard (Feb 20 2021 at 15:12):

@Peter Nelson let's first get one thing clear -- are we talking about finite types, or finite subsets of types? We already have `set.finite`

in mathlib, which is an "I am finite" predicate on a set which does not suffer from all the constructivist problems you're seeing.

#### Peter Nelson (Feb 20 2021 at 15:21):

We're talking about finite types. I'm not using finset directly at all, except where I'm being forced to. Here is some code - one of the problems occurs in the last lemma.

(Related to the fact that I'm not using finset, what I'm trying to do here is to make the shorthand `∑ (a : X), f a`

easier to work with, since most of the `finset.sum`

API is instead written in terms of `∑ a in X, f a`

.)

```
import tactic
----------------------------------------------------------------
open_locale classical big_operators
open set
variables {α β: Type}[fintype α][add_comm_monoid β](f : α → β)
lemma set.to_finset_insert' (X : set α)(e : α) :
(X ∪ {e}).to_finset = X.to_finset ∪ {e} :=
by {ext, simp[or_comm]}
lemma fin_sum_eq (X : set α):
∑ (a : X), f a = ∑ a in X.to_finset, f a :=
let φ : X ↪ α := ⟨coe, subtype.coe_injective⟩ in (finset.sum_map (finset.univ) φ f).symm
lemma fin_sum_insert {X : set α}{e : α}:
e ∉ X → ∑ (a : X ∪ {e}), f a = (∑ (a : X), f a) + f e :=
begin
rintro he,
have hdj :disjoint X.to_finset {e},
{ rw [finset.disjoint_iff_inter_eq_empty], ext,
simp only [finset.not_mem_empty, not_and, finset.mem_singleton, iff_false, finset.mem_inter, mem_to_finset],
exact λ haX hae, false.elim (he (by {rwa ←hae})),},
-- this next claim causes instance mismatch problems if fin_sum_eq is invoked directly,
-- due to two competing instances of fintype for X ∪ {e}
have hXe : ∑ (a : (X ∪{e}) ), f a = ∑ a in (X ∪ {e}).to_finset, f a,
convert fin_sum_eq f (X ∪ {e} : set α),
rw [hXe, fin_sum_eq f (X : set α), set.to_finset_insert' X e, finset.sum_union hdj],
simp,
end
```

#### Mario Carneiro (Feb 20 2021 at 15:28):

Why don't you just use finsets here? it shouldn't be hard to have analogues of all the sets you could want with `open_locale classical`

#### Peter Nelson (Feb 20 2021 at 15:33):

The `set`

API is just more complete.

#### Mario Carneiro (Feb 20 2021 at 15:36):

Only when it comes to equality of sets. The finset API is a lot more complete when it comes to summation; you can do the summation stuff on finsets and pull back to sets for the set algebra

#### Mario Carneiro (Feb 20 2021 at 15:44):

```
lemma fin_sum_insert {X : set α}{e : α}:
e ∉ X → ∑ (a : X ∪ {e}), f a = (∑ (a : X), f a) + f e :=
begin
rintro he,
obtain ⟨X, rfl⟩ := (finite.of_fintype X).exists_finset_coe,
rw [fin_sum_eq, add_comm, ← finset.sum_insert],
convert (fin_sum_eq f _).trans _,
{ congr', ext, simp },
simpa using he,
end
```

#### Mario Carneiro (Feb 20 2021 at 15:46):

`set.to_finset`

doesn't seem to have many lemmas about it, although it does have `mem_to_finset`

which is why the `ext, simp`

works

#### Peter Nelson (Feb 20 2021 at 15:46):

so the trick is `exists_finset_coe`

?

#### Mario Carneiro (Feb 20 2021 at 15:47):

That's how you make everything use finsets

#### Peter Nelson (Feb 20 2021 at 15:48):

Good to know - thanks!

#### Peter Nelson (Feb 20 2021 at 16:09):

Unfortunately it seems like the problem cascades. Here's an attempted consequence of the above where a mismatch issue carries forward, with either of our proofs of `fin_sum_insert`

. The context is a little contrived - is is the problematic part of a proof by induction. The proof that works involves reducing to a case where a single `convert`

resolves the goal, but rewriting earlier fails.

```
def subadditive (g : set α → ℤ) :=
∀ X Y, g (X ∪ Y) ≤ g X + g Y
lemma foo (S : set (set α)){g : set α → ℤ}{X₀ : set α}(hX₀ : X₀ ∉ S)
(hg : subadditive g) (hS : g (⋃₀ S) ≤ ∑ (X : ↥S), g X):
g (⋃₀(S ∪ {X₀})) ≤ ∑ (X : ↥(S ∪ {X₀})), g X :=
begin
-- rw fin_sum_insert g hX₀,
-- Doesn't work
simp_rw [sUnion_union, sUnion_singleton] at hS ⊢,
refine le_trans (hg _ _) _,
refine le_trans (int.add_le_add_right hS (g X₀)) (le_of_eq _),
convert (fin_sum_insert g hX₀).symm,
-- works
end
```

#### Johan Commelin (Feb 20 2021 at 16:11):

So you can't use `S : finset (set \a)`

?

#### Peter Nelson (Feb 20 2021 at 16:13):

I probably could, but I would be worried that this will just move the problem further upwards. In the case I want to invoke, `S`

has type `set (set \a)`

because it's a collection of equivalence classes, so I would have to use some type of equivalence between `set`

and `finset`

to get to `finset (set \a)`

.

#### Mario Carneiro (Feb 20 2021 at 16:22):

Yes, that's `exists_finset_coe`

as you saw

#### Mario Carneiro (Feb 20 2021 at 16:23):

or `set.to_finset`

#### Johan Commelin (Feb 20 2021 at 16:25):

So I guess you can do

```
obtain \<S, rfl\> := exists_finset_coe S
```

or something like that, as first line of the proof

#### Johan Commelin (Feb 20 2021 at 16:25):

Right, as Mario suggested upstairs:

```
obtain ⟨X, rfl⟩ := (finite.of_fintype X).exists_finset_coe,
```

#### Johan Commelin (Feb 20 2021 at 16:26):

After that, the proof should be "smooth"

#### Mario Carneiro (Feb 20 2021 at 16:26):

it wasn't completely smooth, there seem to be some missing simp lemmas

#### Peter Nelson (Feb 20 2021 at 16:38):

Yeah, that last proof is something where I want things from both APIs at the same time.

#### Peter Nelson (Feb 20 2021 at 16:44):

of course, what I actually want is that `fintype`

be propositional.

#### Eric Wieser (Feb 20 2021 at 18:31):

If you use `convert ... using 1`

, does it show what doesn't match?

#### Peter Nelson (Feb 20 2021 at 20:02):

The first instance of `fintype ↥(S ∪ {X₀})`

is this :

```
(@subtype.fintype (set α) (λ (x : set α), x ∈ S)
(@set.decidable_mem (set α) S (λ (a : set α), classical.prop_decidable (S a)))
(@set.fintype α _inst_1))
(@set.fintype_pure (set α) X₀)
```

and the second is this :

```
@set.fintype_union (set α)
(λ (a b : set α),
@fintype.decidable_pi_fintype α (λ (a : α), Prop) (λ (a : α) (a b : Prop), classical.prop_decidable (a = b))
_inst_1
a
b)
S
{X₀}
(@subtype.fintype (set α) (λ (x : set α), x ∈ S)
(λ (a : set α), @set.decidable_mem (set α) S (λ (a : set α), classical.prop_decidable (S a)) a)
(@set.fintype α _inst_1))
(@set.fintype_pure (set α) X₀)
```

#### Peter Nelson (Feb 20 2021 at 20:07):

Ah, so it's actually `decidable_eq`

that is the culprit! The difference between the above is :

```
fintype.decidable_pi_fintype α (λ (a : α), Prop) (λ (a : α) (a b : Prop), classical.prop_decidable (a = b))
_inst_1
a
b
```

vs

```
classical.prop_decidable (a = b)
```

I don't know if that makes any of these problems easier to address....

#### Kevin Buzzard (Feb 20 2021 at 21:14):

What should propositional finiteness be called? `[is_finite alpha]`

?

#### Eric Wieser (Feb 20 2021 at 22:20):

My assumption is that docs#fin_sum_insert is stated poorly

#### Eric Wieser (Feb 20 2021 at 22:20):

But that link doesn't work - where is that lemma?

#### Bryan Gin-ge Chen (Feb 20 2021 at 22:22):

It was proved earlier in this thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Addressing.20mismatch.20issues/near/227098783

#### Eric Wieser (Feb 20 2021 at 22:32):

Is there a full mwe?

#### Eric Wieser (Feb 20 2021 at 22:35):

I think the lemma needs `[fintype X]`

and `[fintype (X \union {e})]`

to avoid this problem

#### Peter Nelson (Feb 20 2021 at 22:55):

This mwe is a union of things earlier, but here is all of it in one place:

```
import tactic
----------------------------------------------------------------
open_locale classical big_operators
open set
variables {α β: Type}[fintype α][add_comm_monoid β](f : α → β)
lemma set.to_finset_insert' (X : set α)(e : α) :
(X ∪ {e}).to_finset = X.to_finset ∪ {e} :=
by {ext, simp[or_comm]}
lemma fin_sum_eq (X : set α):
∑ (a : X), f a = ∑ a in X.to_finset, f a :=
let φ : X ↪ α := ⟨coe, subtype.coe_injective⟩ in (finset.sum_map (finset.univ) φ f).symm
lemma fin_sum_insert {X : set α}{e : α}:
e ∉ X → ∑ (a : X ∪ {e}), f a = (∑ (a : X), f a) + f e :=
begin
rintro he,
obtain ⟨X, rfl⟩ := (finite.of_fintype X).exists_finset_coe,
rw [fin_sum_eq, add_comm, ← finset.sum_insert],
convert (fin_sum_eq f _).trans _,
{ congr', ext, simp },
simpa using he,
end
def subadditive (g : set α → ℤ) :=
∀ X Y, g (X ∪ Y) ≤ g X + g Y
lemma foo (S : set (set α)){g : set α → ℤ}{X₀ : set α}(hX₀ : X₀ ∉ S)
(hg : subadditive g) (hS : g (⋃₀ S) ≤ ∑ (X : ↥S), g X):
g (⋃₀(S ∪ {X₀})) ≤ ∑ (X : ↥(S ∪ {X₀})), g X :=
begin
simp_rw [sUnion_union, sUnion_singleton] at hS ⊢,
--would like to rw here with fin_sum_insert but can't.
refine le_trans (hg _ _) _,
refine le_trans (int.add_le_add_right hS (g X₀)) (le_of_eq _),
convert (fin_sum_insert g hX₀).symm,
end
```

#### Eric Wieser (Feb 20 2021 at 22:58):

Thanks, I'll try my idea out myself tomorrow

#### Yakov Pechersky (Feb 21 2021 at 01:10):

Is this just not going to work because subadditive is defined in a classical context?

#### Eric Wieser (Feb 21 2021 at 14:36):

Eric Wieser said:

I think the lemma needs

`[fintype X]`

and`[fintype (X \union {e})]`

to avoid this problem

Yes, this fixes it, in conjuction with removing `fintype α`

:

```
import tactic
----------------------------------------------------------------
open_locale classical big_operators
open set
variables {α β: Type} [add_comm_monoid β](f : α → β)
lemma set.to_finset_insert' (X : set α) (e : α) [fintype ↥X] [fintype ↥(X ∪ {e})]:
(X ∪ {e}).to_finset = X.to_finset ∪ {e} :=
by {ext, simp[or_comm]}
lemma fin_sum_eq (X : set α) [fintype ↥X] :
∑ (a : X), f a = ∑ a in X.to_finset, f a :=
let φ : X ↪ α := ⟨coe, subtype.coe_injective⟩ in (finset.sum_map (finset.univ) φ f).symm
lemma fin_sum_insert {X : set α}{e : α} [fintype ↥X] [fintype ↥(X ∪ {e})]:
e ∉ X → ∑ (a : X ∪ {e}), f a = (∑ (a : X), f a) + f e :=
begin
rintro he,
unfreezingI { obtain ⟨X', rfl⟩ := finite.exists_finset_coe ⟨‹fintype ↥X›⟩ },
rw [fin_sum_eq, fin_sum_eq, add_comm, ←finset.sum_insert],
{ congr', ext, simp },
simpa using he,
end
def subadditive (g : set α → ℤ) :=
∀ X Y, g (X ∪ Y) ≤ g X + g Y
lemma foo (S : set (set α)) [fintype ↥S] {g : set α → ℤ} {X₀ : set α} [fintype ↥(S ∪ {X₀})] (hX₀ : X₀ ∉ S)
(hg : subadditive g) (hS : g (⋃₀ S) ≤ ∑ (X : ↥S), g X):
g (⋃₀(S ∪ {X₀})) ≤ ∑ (X : ↥(S ∪ {X₀})), g X :=
begin
simp_rw [sUnion_union, sUnion_singleton] at hS ⊢,
rw fin_sum_insert _ hX₀, -- rw works
sorry,
end
```

#### Eric Wieser (Feb 21 2021 at 14:37):

You should never assume a more general `fintype`

instance than the one the lemma actually requires and let the specific one be derived, because then the lemma won't match again terms which obtain the specific one via a different means

#### Peter Nelson (Feb 21 2021 at 19:23):

Thank you! What if I want to invoke `fin_sum_insert`

in the middle of a larger proof where there is already a `fintype α`

instance hanging around?

#### Eric Wieser (Feb 21 2021 at 19:38):

It should work fine

#### Eric Wieser (Feb 21 2021 at 19:40):

When you rewrite, the instances on the left-hand side of the eq / iff will already be present in the goal, while typeclass instances will try to deduce the ones on the right-hand-side

#### Peter Nelson (Feb 21 2021 at 19:52):

Ok. I've run into a curiosity that results from this solution when I'm applying it in an inductive proof. The below is the smallest example where I can reproduce the issue.

```
import tactic
----------------------------------------------------------------
open_locale classical big_operators
open set
variables {α β : Type}[add_comm_monoid β]
lemma fin_sum_empty (f : α → β) :
∑ (a : (∅ : set α)), f a = 0 :=
finset.sum_empty
lemma fin_sum_eq (f : α → β)(X : set α)[fintype X]:
∑ (a : X), f a = ∑ a in X.to_finset, f a :=
let φ : X ↪ α := ⟨coe, subtype.coe_injective⟩ in (finset.sum_map (finset.univ) φ f).symm
lemma fin_sum_insert (f : α → β){X : set α}{e : α}(he : e ∉ X)[fintype ↥X][fintype ↥(X ∪ {e})]:
∑ (a : X ∪ {e}), f a = (∑ (a : X), f a) + f e :=
begin
unfreezingI {obtain ⟨X', rfl⟩ := finite.exists_finset_coe ⟨‹fintype ↥X›⟩ },
rw [fin_sum_eq, fin_sum_eq, add_comm, ←finset.sum_insert],
{ congr', ext, simp },
simpa using he,
end
lemma induction_foo [fintype α](P : set α → Prop):
(P ∅) → (∀ (X : set α)(e : α), e ∉ X → P X → P (X ∪ {e})) → (∀ X, P X) :=
sorry
lemma fin_sum_one_eq_card [fintype α](X : set α):
∑ (a : X), (1 : α → ℤ) a = X.to_finset.card :=
begin
revert X, apply induction_foo,
{rw [to_finset_card, empty_card'], convert fin_sum_empty _, },
intros X e he hX,
-- rw fin_sum_insert _ he,
-- doesn't work
rw fin_sum_insert, swap, assumption,
--works
sorry,
end
```

In the proof of `fin_sum_one_eq_card`

, I am able to rw with `fin_sum_insert`

if I don't pass it the term `he`

, but if I pass it `he`

, the rewrite fails, even though `he`

is exactly the term it needs, and resolving the goal later using `he`

works fine . The `swap, assumption`

handles this cleanly enough in practice, but I'd still like to understand what is happening, and can't figure it out.

#### Kevin Buzzard (Feb 21 2021 at 20:03):

I don't know the answer to your question, but `convert`

works so it's some type class inference issue again. Independent of that, why have you got such a horrible `∑ (a : ↥X), 1 ↑a`

term? Why not just some over `a \in X`

? Oh! Because it's not a finset :-( I think your fabulous questions are just indicating that we need some API. We solved this with `finsum_in`

when we were doing finite groups: see here.

#### Kevin Buzzard (Feb 21 2021 at 20:05):

I totally agree with you, all this constructive stuff is hard to work with but as you can see there are now sufficiently many experts around going "no it's fine, just think about it this way and there's a trick" that we've all just got used to it and learnt the tricks. Why not just write your own API and sorry it all out? `finsum_in`

will solve all your problems. The proofs are just hacks to reduce everything to finset.sum and are very ugly but you don't care about those, you just reap the benefits.

#### Kevin Buzzard (Feb 21 2021 at 20:15):

@Peter Nelson I hesitated to introduce these new definitions because some people pointed out to me that the tools we have are enough for the job as long as you continually jump over the traps you're running into, and hence because such a nonconstructive approach is not strictly necessary (it all _can_ be done with what we have) I was just in danger of adding to the noise a la xkcd#927. However your situation I think just makes it clear that we need them. If this sort of stuff is deterring beginners then it's clear that there's an argument for it. I've suggested these before but here we go again:

```
class is_finite (X : Type u) : Prop
noncomputable def finsum {ι M} [add_comm_monoid M] (f : ι → M) : M -- zero if support infinite
noncomputable def finsum_in {ι M} [add_comm_monoid M] (s : set ι) (f : ι → M) : M -- zero if support intersect s is infinite
def fincard (X : Type u) : ℕ -- zero if X is infinite
```

Why don't you switch to these, sorry all the lemmas you need and feed them back, and we can just make the API? I've done it once before and it was quite fun, I just didn't get round to PR'ing it because some people weren't convinced this stuff was needed. In some sense they might be right -- jump through some hoops, use `convert`

and woo-hoo, it's all computable! I am losing my patience with this approach.

#### Kevin Buzzard (Feb 21 2021 at 20:17):

```
intros X e he hX,
convert fin_sum_insert _ he, -- this works
have : ↑((X ∪ {e}).to_finset.card) = ∑ (a : ↥X), (1 : α → ℤ) ↑a + (1 : α → ℤ) e, -- the goal!
sorry,
exact this, -- stupid typeclass fail
```

#### Kevin Buzzard (Feb 21 2021 at 20:18):

With my approach there will be no up-arrows

#### Jason KY. (Feb 21 2021 at 21:06):

I wonder if it is worthwhile just pr finsum. All of the APIs are already done. I don't think too many standards is an issue if we can easily convert between the standards and I feel that this has come up often enough to warrant a separate definition.

#### Peter Nelson (Feb 21 2021 at 21:47):

I like this idea. I do see the perspective of the more constructively inclined, and am even (on some level) enjoying how much these subtle issues teach me about the language. I'm grateful for all the help, patience and expertise I've been getting here.

However, I am planning to give a talk in the near future to fellows combinatorialists about how great/fun formalization is, and these types of problems are among the downsides on my mind. 'Traps' is the right word - none of the problems are insurmountable, but they are barriers to entry. Being someone very interested in theorems about finite structures, I suspect that this stuff happens more frequently for me than many others, and it would be good to have a solution that can be explained in terms an average mathematician can immediately understand.

Regarding an API, I would love to have such a thing available in mathlib. Likely not much would be needed - I suspect the existing one is all I would need to work with.

#### Eric Wieser (Feb 21 2021 at 22:22):

A linter to catch the type of `decidable`

/ `fintype`

instance problems I resolved above would likely help with avoiding some of these traps

#### Kevin Buzzard (Feb 21 2021 at 22:42):

Yes but I think the time has come now to do this -- and I'm about to sit down and do it -- because there are some people who simply never ever want to #eval anything and simply do not need the trouble which things like `fintype `

and `finset.sum`

can cause, especially if they open_locale classical on line 1 and then occasionally use types which have got decidable equality. It's just one extra hassle which doesn't need to be dealt with. Avigad told me that Isabelle has finsum and it works fine.

#### Kevin Buzzard (Feb 21 2021 at 22:45):

@Jason KY. I'll put you as co-author, I'll do it on the discord.

#### Mario Carneiro (Feb 22 2021 at 01:19):

It's not just `#eval`

, when it comes to facts about small matrices or something `dec_trivial`

can sometimes be the most powerful tool at our disposal

#### Mario Carneiro (Feb 22 2021 at 01:20):

That's not a great situation, since that approach has a host of limitations, but it is what it is

#### Mario Carneiro (Feb 22 2021 at 01:24):

That said I'm in agreement on the introduction of `fincard`

and `finsum`

FWIW. There are just a lot of lemmas that are needed to make this nice - I found at least two or three in my proof above, regarding the interaction between `set.to_finset`

and all of the finset API; with a finsum API we also need lemmas relating it to finset sum, and also copies of everything in the finset sum API.

#### Kevin Buzzard (Feb 22 2021 at 02:08):

First attempt to make a `finsum`

API is #6355. Many thanks to @Jason KY. who did most of the work.

#### Kevin Buzzard (Feb 22 2021 at 02:10):

@Peter Nelson we don't make propositional finite types because we can just use `nonempty (fintype α)`

. We don't do cardinality yet, that is some work we have prepared but haven't got into PR shape yet. This might take some time to get through the system.

#### Peter Nelson (Feb 22 2021 at 02:36):

That sounds great - I look forward to tinkering tomorrow.

Might there be a case for also adding `finmax`

to the API? It is a special case of `finsum`

(and could be defined as such), but API lemmas in which maxima are taken over subsets etc could be useful. Something I'm currently doing uses `fintype.exists_max`

+ choice to define a maximum, and I haven't run into any mismatch issues so far, but who knows what will happen in the future.

#### Peter Nelson (Feb 22 2021 at 02:47):

```
variables {α β : Type u}[linear_order β]
noncomputable def finmax (f : α → β) : β := sorry
-- some default value if no max exists, otherwise the max
lemma finmax_is_max [nonempty α][nonempty (fintype α)](f : α → β): ∀ x, f x ≤ finmax f := sorry
lemma exists_argmax [nonempty α][nonempty (fintype α)](f : α → β): ∃ x, f x = finmax f := sorry
```

etc etc

#### Mario Carneiro (Feb 22 2021 at 02:51):

That seems very near to what `supr`

already does

#### Mario Carneiro (Feb 22 2021 at 02:52):

we just need a version of `supr`

that works on any preorder

#### Peter Nelson (Feb 22 2021 at 02:54):

The existence of an argmax following from (propositional) finiteness is what I'm after. I can't see anything about finiteness in the `supr`

API, but maybe I'm missing something?

#### Mario Carneiro (Feb 22 2021 at 02:54):

finite lattices are complete

#### Peter Nelson (Feb 22 2021 at 02:56):

Is there a `fintype`

hiding there somewhere?

#### Mario Carneiro (Feb 22 2021 at 02:57):

My point is that for the `finmax`

function, you don't need any inputs except for `preorder B`

and `nonempty A`

, and it can be well defined whenever anything like it makes sense; you can then prove that it makes sense when A is finite to make use of it in your scenario

#### Mario Carneiro (Feb 22 2021 at 02:58):

there's no need to bake finiteness into the definition though

#### Mario Carneiro (Feb 22 2021 at 03:00):

actually `nonempty B`

is probably better than `nonempty A`

here, that way it can default to the zero of the codomain instead of a random value

#### Mario Carneiro (Feb 22 2021 at 03:01):

`inhabited B`

is probably better

#### Peter Nelson (Feb 22 2021 at 03:05):

Ah, it looks like `set.finite.exists_maximal_wrt`

already does what I want , without any `fintype`

. Here it is:

```
theorem set.finite.exists_maximal_wrt {α : Type u} {β : Type v} [partial_order β]
(f : α → β)(s : set α) (h : s.finite) :
s.nonempty → (∃ (a : α) (H : a ∈ s), ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a')
```

Or not quite, but it's easy to get a `linear_order`

version.

#### Peter Nelson (Mar 05 2021 at 15:49):

@Kevin Buzzard @Jason KY. I've started incorporating `finsum`

into my project, as well as rolling my own `fincard`

by finsumming ones (I'm assuming the intended implementation of `fincard`

is more principled, but mine will do for now). It's great avoiding the mismatches, and what's more, not to have to regularly descend into finset coercion hell in the first place!

I have a question about intended usage. For most of my interaction with `finsum`

, everything will be happening with `variables {\a : Type} [nonempty (fintype \a)]`

at the top of files. But this will mean that for each of the `finsum`

and `finsum_in`

lemmas that require explicit finiteness assumptions (which already each come in a few different flavours) , there will be yet another version that takes a nonempty fintype instance. For example, here are statements of a lemma I proved and its version that takes an instance.

```
lemma finsum_le_finsum [ordered_add_comm_monoid M](hfg : ∀ x, f x ≤ g x)
(hf : (function.support f).finite)(hg : (function.support g).finite):
∑ᶠ (i : α), f i ≤ ∑ᶠ (i : α), g i :=
sorry
lemma finsum_le_finsum' [ordered_add_comm_monoid M][nonempty (fintype α)]
(hfg : ∀ x, f x ≤ g x):
∑ᶠ (i : α), f i ≤ ∑ᶠ (i : α), g i :=
sorry
```

Is doing this for every such lemma a reasonable solution? I can't even think of a good naming convention.

#### Jason KY. (Mar 05 2021 at 17:09):

I think the idea is you prove the different versions if you are writing APIs (e.g. your example) while if you are simply using `finsum`

you can just stick to one version (or the most general version, i.e. the support is finite.). @Mario Carneiro suggest a naming scheme here

Last updated: Dec 20 2023 at 11:08 UTC