Rewriting indices of sum/product

Stream: new members

[Robert Shlyakhtenko]

Hi,

Here is another very basic question which will hopefully not be difficult to answer, but would help me tremendously.

I can prove something very simple of the sort:

lemma index_rewrite (n m : Nat) (h : n = m) (f : Nat -> Nat):
  ∏ (i : Fin n), f i.val = ∏ (i : Fin m), f i.val := by rw[h]

And, unsurprisingly, this extends to something a bit more complex, like:

lemma index_rewrite (l₁ l₂ : List T) (h : l₁.length = l₂.length) (f : Nat -> Nat):
  ∏ (i : Fin l₁.length), f i.val = ∏ (i : Fin l₂.length), f i.val := by rw[h]

However, if I just have something like ∏ (i : Fin l₁.length), f i.val in my goal, and something like (h : l₁.length = l₂.length), then writing rw[h] doesn't work.

I know that there are tactics like conv and enter which would allow me to enter and modify a subexpression, but they don't seem to allow me to access the actual indices of the product.

What is the "right" way to do this?

(I could probably "have" index_rewrite and then rewrite that into my goal, but that seems like a subpar solution).

Thanks!

[Aaron Liu]

See #26835

[Luigi Massacci]

something like convert ought to work I think

[Robert Shlyakhtenko]

Here is something simple that I couldn't prove:

lemma reindex (α β : Type) (l v : List α) (b : List β) (h1 : l.length = v.length) (h2 : l.length = b.length)
  (f : α -> β -> ENNReal):
  ∏ (i : Fin l.length), f l[i] b[i] = ∏ (i : Fin v.length), f l[i] b[i]

I tried:

lemma reindex (α β : Type) (l v : List α) (b : List β) (h1 : l.length = v.length) (h2 : l.length = b.length)
  (f : α -> β -> ENNReal):
  ∏ (i : Fin l.length), f l[i] b[i] = ∏ (i : Fin v.length), f l[i] b[i] := by
   let e : Fin l.length ≃ Fin v.length := by
      rw [h1]
   apply Fintype.prod_equiv e
   intro x
   simp
   sorry

But I don't think this is a good solution, and I couldn't get it to work completely.

Thanks for the patience!

[Aaron Liu]

Use docs#finCongr instead, which doesn't put Eq.mpr into your goal state

[Robert Shlyakhtenko]

Aha, this makes it easy! Thanks!