ext: not a structure or a lemma proving `x = y`.

Stream: mathlib4

[Johan Commelin]

-- Mathlib/LinearAlgebra/Matrix/Hermitian.lean:41
def IsHermitian (A : Matrix n n α) : Prop := Aᴴ = A

instance (A : Matrix n n α) [Decidable (Aᴴ = A)] : Decidable (IsHermitian A) :=
  inferInstanceAs <| Decidable (_ = _)

theorem IsHermitian.eq {A : Matrix n n α} (h : A.IsHermitian) : Aᴴ = A := h

protected theorem IsHermitian.isSelfAdjoint {A : Matrix n n α} (h : A.IsHermitian) :
    IsSelfAdjoint A := h

-- @[ext] -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): incorrect `ext`, not a structure or a lemma proving `x = y`.
theorem IsHermitian.ext {A : Matrix n n α} : (∀ i j, star (A j i) = A i j) → A.IsHermitian := by
  intro h; ext i j; exact h i j

(https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/LinearAlgebra/Matrix/Hermitian.lean#L41)

• Should @[ext] work with a more aggressive reducibility level?
• Or should IsHermitian be an abbrev (which actually isn't enough to make @[ext] happy)?
• Or should we just decide that this is not in scope for ext?

[Andrew Yang]

I personally think this is out of scope. We could easily add a separate lemma in the form of an equality, which is a lot less confusing IMO.

[Johan Commelin]

@Anne Baanen indicated the same on #23524. I'm also leaning that way.

[Johan Commelin]

So let's declare it out of scope