french brackets and structure instances

Stream: mathlib4

[Matthew Ballard]

The following gives me a no goals error on the french brackets

import Mathlib.Analysis.Normed.Field.Basic

example [NonUnitalRing R] [NonUnitalSeminormedRing S]
    [NonUnitalRingHomClass F R S] (f : F) : NonUnitalSeminormedRing R :=
  { ‹NonUnitalRing R›, SeminormedAddCommGroup.induced R S f with
    norm_mul := fun x y => by
      show ‖f (x * y)‖ ≤ ‖f x‖ * ‖f y‖
      exact (map_mul f x y).symm ▸ norm_mul_le (f x) (f y) }

has this kind of behavior been seen before?

[Damiano Testa]

Does Mathlib.Normed exist?

[Kevin Buzzard]

This works fine on mathlib master:

import Mathlib.Analysis.Normed.Field.Basic
set_option autoImplicit true

example [NonUnitalRing R] [NonUnitalSeminormedRing S] [FunLike F R S]
    [NonUnitalRingHomClass F R S] (f : F) : NonUnitalSeminormedRing R :=
  { ‹NonUnitalRing R›, SeminormedAddCommGroup.induced R S f with
    norm_mul := fun x y => by
      show ‖f (x * y)‖ ≤ ‖f x‖ * ‖f y‖
      exact (map_mul f x y).symm ▸ norm_mul_le (f x) (f y) }

[Kyle Miller]

I can confirm it didn't work and now it works on mathlib master -- @Matthew Ballard I suspect the difference is lean4#2478?

[Matthew Ballard]

It might have been working with an old toolchain…

[Matthew Ballard]

I thought it didn’t work on anything

[Matthew Ballard]

Huh, must have been on the wrong toolchain when I thought I was testing current master

[Kyle Miller]

By the way, what "no goals" means for french brackets is that unification solved for this metavariable. It's because it's defined by

macro_rules | `(‹$type›) => `((by assumption : $type))

and "no goals" is what a tactic like assumption reports if there's no main goal.

I've seen the error for plain by notation too. I feel like this should probably not happen, since I thought by was supposed to set up a synthetic opaque metavariable, which can't be solved for by unification by default.