Golfing a sum on a Finset subtype

Stream: general

[EdwardW]

Hia all, I've got a very simple theorem, but the proof is hideous :(

Here's the proof I have (sorry for the unnecessarily large import, but #min_imports wasn't outputting anything and tracking down what wasn't working was a giant pain). I would be very interested if there is a simple way to prove this...

import Mathlib.Analysis.Analytic.Basic

open BigOperators Nat

example {E : Type} [Semiring E] {x x' : E} (hx : Commute x x') (n : ℕ) :

    (∑ s : {s : (Finset (Fin (1 + n))) // s.card = n},

      (List.ofFn ((s.1).piecewise (fun _ ↦ x) fun _ ↦ x')).prod) = (n + 1) * x' * x ^ n := by

  conv_lhs => {

    enter [2, s]

    tactic =>

      obtain ⟨i, hi⟩ := Finset.card_eq_one.mp (by convert s.2 ▸ s.1.card_compl; simp)

      have : (1 + n) = (i + (1 + (n - i))) := by zify; rw [cast_sub (lt_one_add_iff.mp i.2)]; group

      simp_rw [this, List.ofFn_add, List.prod_append, Finset.piecewise]

      have nmem (x : Fin 1) :

          (Fin.cast (by aesop) (Fin.natAdd (↑i) (Fin.castAdd (n - ↑i) x)) ∉ s.1) :=

        Finset.mem_compl.mp (hi ▸ Finset.mem_singleton.mpr (by aesop))

      have meml (x : Fin i) : Fin.cast (by aesop) (Fin.castAdd (1 + (n - ↑i)) x) ∈ s.1 := by

        refine Finset.not_mem_compl.mp (hi ▸ Finset.not_mem_singleton.mpr (ne_eq _ _ ▸ ?_))

        by_contra h

        convert x.2.ne ?_

        apply_fun Fin.val at h

        rwa [Fin.coe_cast, Fin.coe_castAdd] at h

      have memg (x : Fin (n - i)) :

          Fin.cast (by aesop) (Fin.natAdd (↑i) (Fin.natAdd 1 x)) ∈ s.1 := by

        refine Finset.not_mem_compl.mp (hi ▸ Finset.not_mem_singleton.mpr (ne_eq _ _ ▸ ?_))

        by_contra h

        apply_fun Fin.val at h

        rw [Fin.coe_cast, Fin.coe_natAdd, Fin.coe_natAdd] at h

        aesop

      simp only [meml, ↓reduceIte, List.ofFn_const, List.prod_replicate, nmem, List.ofFn_succ,

        List.ofFn_zero, List.prod_cons, List.prod_nil, mul_one, memg]

      rw [← mul_assoc, (hx.pow_left i).eq, mul_assoc, pow_mul_pow_sub x (lt_one_add_iff.mp i.2)]

  }

  simp [one_add, mul_assoc]

[Edward van de Meent]

EdwardW said:

#min_imports wasn't outputting anything

#min_imports doesn't see examples

[Edward van de Meent]

also, it seems you're using odd spacing chars? (they seem to confuse the playground)

[Edward van de Meent]

this should have those removed...

import Mathlib.Algebra.BigOperators.Group.Finset
import Mathlib.Algebra.Order.Ring.Nat
import Mathlib.Tactic.Group
import Mathlib.Tactic.Ring.RingNF
import Mathlib.Tactic.Zify

open BigOperators Nat

def foo {E : Type} [Semiring E] {x x' : E} (hx : Commute x x') (n : ℕ) :

   (∑ s : {s : (Finset (Fin (1 + n))) // s.card = n},

      (List.ofFn ((s.1).piecewise (fun _ ↦ x) fun _ ↦ x')).prod) = (n + 1) * x' * x ^ n := by

  conv_lhs => {

    enter [2, s]

    tactic =>

      obtain ⟨i, hi⟩ := Finset.card_eq_one.mp (by convert s.2 ▸ s.1.card_compl; simp)

      have : (1 + n) = (i + (1 + (n - i))) := by zify; rw [cast_sub (lt_one_add_iff.mp i.2)]; group

      simp_rw [this, List.ofFn_add, List.prod_append, Finset.piecewise]

      have nmem (x : Fin 1) :

          (Fin.cast (by aesop) (Fin.natAdd (↑i) (Fin.castAdd (n - ↑i) x)) ∉ s.1) :=

        Finset.mem_compl.mp (hi ▸ Finset.mem_singleton.mpr (by aesop))

      have meml (x : Fin i) : Fin.cast (by aesop) (Fin.castAdd (1 + (n - ↑i)) x) ∈ s.1 := by

        refine Finset.not_mem_compl.mp (hi ▸ Finset.not_mem_singleton.mpr (ne_eq _ _ ▸ ?_))

        by_contra h

        convert x.2.ne ?_

        apply_fun Fin.val at h

        rwa [Fin.coe_cast, Fin.coe_castAdd] at h

      have memg (x : Fin (n - i)) :

          Fin.cast (by aesop) (Fin.natAdd (↑i) (Fin.natAdd 1 x)) ∈ s.1 := by

        refine Finset.not_mem_compl.mp (hi ▸ Finset.not_mem_singleton.mpr (ne_eq _ _ ▸ ?_))

        by_contra h

        apply_fun Fin.val at h

        rw [Fin.coe_cast, Fin.coe_natAdd, Fin.coe_natAdd] at h

        aesop

      simp only [meml, ↓reduceIte, List.ofFn_const, List.prod_replicate, nmem, List.ofFn_succ,

        List.ofFn_zero, List.prod_cons, List.prod_nil, mul_one, memg]

      rw [← mul_assoc, (hx.pow_left i).eq, mul_assoc, pow_mul_pow_sub x (lt_one_add_iff.mp i.2)]

  }

  simp [one_add, mul_assoc]

[EdwardW]

Edward van de Meent said:

also, it seems you're using odd spacing chars? (they seem to confuse the playground)

You mean odd as in strange? That is weird because I let vscode handle that but thanks for the fix!

[Damiano Testa]

The minImports linter can give partial information for examples, as it also inspects the syntax. You could try it by setting set_option linter.minImports true at the beginning of the file.