Zulip Chat Archive

Stream: Is there code for X?

Topic: finset sum function.extend

Apurva Nakade (Dec 17 2023 at 16:16):

How does one show the result below?

import Mathlib.Algebra.Module.Basic
import Mathlib.Algebra.BigOperators.Basic

open BigOperators

variable {𝕜 : Type*} {E : Type*} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E]

example (t : Finset E) (g : t → 𝕜) :
  ∑ i : t, g i = ∑ i in t, Function.extend Subtype.val g 0 i := by sorry

I can't figure out how to use the i in t to simplify Function.extend.

I don't have a choice with rewriting the statement as it appears like this in a larger proof.

Thanks,

Yaël Dillies (Dec 17 2023 at 16:17):

docs#Fintype.sum_extend_by_zero

Yury G. Kudryashov (Dec 17 2023 at 16:20):

That's not exactly the same

Yury G. Kudryashov (Dec 17 2023 at 16:21):

But very close

Yaël Dillies (Dec 17 2023 at 16:22):

Yeah, that's the closest I could find

Apurva Nakade (Dec 17 2023 at 16:23):

Thanks! Maybe unfolding Function.extend reduces it to the above theorem

Yury G. Kudryashov (Dec 17 2023 at 16:24):

You can rewrite on docs#Finset.sum_coe_sort right-to-left, then apply docs#Finset.sum_congr

Yury G. Kudryashov (Dec 17 2023 at 16:24):

Then you'll have to prove ∀ i : t, g i = Function.extend Subtype.val g 0 i

Yury G. Kudryashov (Dec 17 2023 at 16:25):

This follows from docs#Function.Injective.extend_apply

Apurva Nakade (Dec 17 2023 at 16:30):

docs#Finset.sum_congr is complaining that the LHS is of type @Finset.sum k t and the RHS is of type @Finset.sum k E

Apurva Nakade (Dec 17 2023 at 16:31):

At least that's what it seems to be trying to do. If I do congr then I explicitly get a goal t = E

Ruben Van de Velde (Dec 17 2023 at 16:31):

First follow the first part of the sentence

Ruben Van de Velde (Dec 17 2023 at 16:31):

import Mathlib
import Mathlib.Algebra.BigOperators.Basic

open BigOperators

variable {𝕜 : Type*} {E : Type*} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E]

example (t : Finset E) (g : t → 𝕜) :
  ∑ i : t, g i = ∑ i in t, Function.extend Subtype.val g 0 i := by
  conv_rhs => rw [←Finset.sum_coe_sort]
  apply Finset.sum_congr rfl ?_
  rintro x -
  rw [Function.Injective.extend_apply]
  exact Subtype.val_injective

Apurva Nakade (Dec 17 2023 at 16:33):

Oh wow, thanks a lot! This was far more complicated than I expected.
I was trying out the rw [←Finset.sum_coe_sort] but couldn't get it to work

Apurva Nakade (Dec 17 2023 at 16:35):

Is conv_rhs saying that only apply the tactic to the RHS of the equation?

Last updated: Dec 20 2023 at 11:08 UTC