!4#3258 ext error

Stream: mathlib4

[Jeremy Tan]

!4#3258 how do I fix the one ext error over here?

[Moritz Firsching]

This discussion might be related: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Goal.20state.20not.20updating.2C.20bugs.2C.20etc.2E
Seems like

theorem IsSymm.ext {A : Matrix n n α} : (∀ i j, A j i = A i j) → A.IsSymm :=

is not really an ext lemma anymore, even though Aᵀ = A looks like an equality, it has A.

I guess something like

@[ext]
theorem IsSymm.ext {A : Matrix n n α} {B : Matrix n n α} (h : B = Aᵀ ) (g : ∀ i j, A j i = A i j) :
    B = A := by
  ext i j
  rw [h]
  exact g i j

would work as an ext lemma, but is perhaps not super useful.
In the category theory files, sometimes an aesop rule was added instead. I don't know how to proceed here.

[Eric Wieser]

I would guess we should just remove the attribute, or even the lemma itself (with a porting note)

[Eric Wieser]

I'm pretty sure nothing uses it

[Jeremy Tan]

I've gone ahead and removed @[ext]