need help with weird error message

Stream: new members

[Becker A.]

I have this code (with a bogus theorem, no need to fixate on that):

import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Data.Fin.Basic
import Mathlib.Data.Nat.Choose.Sum
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Fin

open Finset

theorem sum_sq_mul_sq_sum.extracted_1_1.{u_1}
  {R : Type u_1} [inst : Field R]
  {n : ℕ}
  {f : Fin n → R}
  : ∑ i, f i * ∑ i_1, f i * ∑ j ∈ univ.erase i_1, f i_1 * f j = 0
  := by
  conv in (fun i_1 => f _ * ∑ j ∈ univ.erase i_1, f i_1 * f j) => rw [] -- error here

  sorry

and I get a weird error message:

[error when printing message: unknown goal _uniq.1795]

any idea what's wrong here?

[Vlad Tsyrklevich]

I figure you probably already know this, but in case not I'll just note that using 'raw' conv like conv => enter [1, 2, i, 2, 2]; works. I don't know lean internals well enough to diagnose whether this is a conv bug--seems like it might be.

[Vlad Tsyrklevich]

Weird, reducing imports to

import Mathlib.Algebra.BigOperators.Group.Finset.Defs
import Mathlib.Algebra.Field.Defs
import Mathlib.Data.Fintype.Basic

fixes the failure

[Vlad Tsyrklevich]

(deleted) better reproducer below

[Vlad Tsyrklevich]

I further minimized this and manually bisected it. Deleting prod_congr below makes it work, or just (attr := congr). I think I'm out of my depth to determine exactly why

import Mathlib.Algebra.BigOperators.Group.Finset.Defs
--import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Data.Fintype.Basic

 import Mathlib.Algebra.BigOperators.Group.Finset.Defs
 import Mathlib.Data.Finset.Prod
 import Mathlib.Data.Finset.Sum

variable {ι κ G M : Type*} {s s₁ s₂ : Finset ι} {a : ι}

namespace Finset

variable [CommMonoid M] {f g : ι → M}

@[to_additive (attr := congr)]
theorem prod_congr (h : s₁ = s₂) : (∀ x ∈ s₂, f x = g x) → s₁.prod f = s₂.prod g := by
  rw [h]; exact fold_congr


theorem repro {n : Nat} {f : Fin n → Nat} :
    ∑ i : Fin n, ∑ j : Fin n, f i = 0 := by
  conv in (fun j : Fin n => f _) => simp -- error here

  sorry

[Becker A.]

Vlad Tsyrklevich said:

I figure you probably already know this, but in case not I'll just note that using 'raw' conv like conv => enter [1, 2, i, 2, 2]; works.

I actually did not know! I think I posted this before I discovered conv? sometime in the past 24 hours. in that case, it makes sense why you'd suspect conv.

-> do you think this is worth submitting a bug report?

[Becker A.]

Vlad Tsyrklevich said:

I think I'm out of my depth to determine exactly why

it's already a little deep for me to understand just the evidence of what's breaking and when :sweat_smile: thanks for the help!

[Vlad Tsyrklevich]

I would wait a day or two--it is the holidays and there are fewer people around at the moment. Someone may be able to better minimize or find it is already a duplicate of something else (or is not a bug at all, though I do believe it is one.)

[Aaron Liu]

definitely a bug

[Aaron Liu]

I had a PR fixing conv? I think

[Aaron Liu]

conv? is very broken

[Becker A.]

wait really? it seemed to be working for me. broken in what way?

[Kevin Buzzard]

I think Aaron just means "it's not hard to confuse it" rather than "it's always broken"

[Aaron Liu]

I mean "conv? often outputs nonsense or errors on perfectly reasonable inputs"

[Vlad Tsyrklevich]

I minimized this example to cut out mathlib and filed lean4#11877