!4#4047 Analysis.Normed.Group.SemiNormedGroup

Stream: mathlib4

[Nikolas Kuhn]

I ran into some issues in porting this file. It seems like the definition of SemiNormedGroup₁ now allows morphisms to be norm-non-increasing up to a constant, while the description says that morphisms should be norm-non-increasing. This also makes a theorem at the end of the file fail.
It might be good for someone experienced with this file to take a look @Johan Commelin @Riccardo Brasca
This is also my first time porting, so please excuse the probably numerous blunders...
PR here: https://github.com/leanprover-community/mathlib4/pull/4047

[Eric Wieser]

Porting from mathlib3 to mathlib4 shouldn't result in a true statement becoming false. By "now allows", are you comparing mathlib3 with mathlib4, or code with docs?

[Eric Wieser]

I've commented on the problem; you should be _very_ wary of changing defs and instances when porting, as doing so can change whether later results are true

[Nikolas Kuhn]

Ah great, thanks! Yeah, now it makes sense. I'll roll it back to there and try again.

[Nikolas Kuhn]

There seems to be a missing coercion from Homs inSemiNormedGroup₁ to NormedAddGroupHom which is needed in this Lemma:

-- If `coe_fn_coe_base` fires before `coe_comp`, `coe_comp'` puts us back in normal form.
@[simp]
theorem coe_comp' {M N K : SemiNormedGroup₁} (f : M ⟶ N) (g : N ⟶ K) :
    ((f ≫ g) : NormedAddGroupHom M K) = (↑g : NormedAddGroupHom N K).comp ↑f :=
  rfl
#align SemiNormedGroup₁.coe_comp' SemiNormedGroup₁.coe_comp'

Should this coercion be added manually, and if so as what type of instance?

[Nikolas Kuhn]

This is another result that doesn't work anymore due to missing coercions

theorem coe_id (V : SemiNormedGroup) : (𝟙 V : V → V) = id :=
  rfl

This gives the error

type mismatch
  𝟙 V
has type
  V ⟶ V : Type ?u.11927
but is expected to have type
  ↑V → ↑V : Type ?u.11893

unless I manually add a CoeFun instance before (which I now believe one shouldn't do?).

[Kevin Buzzard]

docs4#SemiNormedGroup

[Kevin Buzzard]

lololol
instance.png
Surely someone should actually do something about this?

[Eric Wieser]

I assume asking Henrik Böving to make this display nicely would be an #xy problem!

[Kevin Buzzard]

I started a new thread in #lean4 here , I don't want to derail this one.