False negative: |- (∑' (n :Nat), _ ^ n) =

[nomeata]

The query |- (∑' (n : Nat), _ ^ n) = _ doesn’t work, while |- (∑' (n : _), _ ^ n) = _ works.

Something with type classes, because it says

Found 40 definitions mentioning HPow.hPow, tsum and Eq. Of these, 7 match your pattern(s).

but

Found 0 definitions mentioning instPowNat, instTopologicalSpaceNat, Nat.addCommMonoid, HPow.hPow, tsum, Nat, instHPow and Eq. Of these, 0 match your pattern(s).

[nomeata]

These work:

|- (∑' (n :  _), _ ^ n) = (_ : Real)
|- (∑' (n :  _), @HPow.hPow Real Nat Real _ _ n) = _

These don’t

|- (∑' (n :  _), (_ ^ n : Real)) = (_ : Real)
|- (∑' (n :  _), ((_:Real) ^ (n : Nat) : Real)) = _

[nomeata]

Ah, maybe this is due to https://github.com/leanprover/lean4/issues/2220 somehow.

[nomeata]

yay, this got fixed along with https://github.com/leanprover/lean4/issues/2220!