failed to synthesize Additive (Group G)

Stream: mathlib4

[Winston Yin (尹維晨)]

Why do I have to use French quotes to give Lean the instance of Additive (Group G), when Lean3 was able to synthesise it automatically?

import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.Deprecated.Submonoid

variable {G : Type _} {H : Type _} {A : Type _} {a a₁ a₂ b c : G}
variable [Group G] [AddGroup A]

structure IsAddSubgroup (s : Set A) extends IsAddSubmonoid s : Prop where
  neg_mem {a} : a ∈ s → -a ∈ s

@[to_additive]
structure IsSubgroup (s : Set G) extends IsSubmonoid s : Prop where
  inv_mem {a} : a ∈ s → a⁻¹ ∈ s

structure IsNormalAddSubgroup [AddGroup A] (s : Set A) extends IsAddSubgroup s : Prop where
  normal : ∀ n ∈ s, ∀ g : A, g + n + -g ∈ s

@[to_additive]
structure IsNormalSubgroup [Group G] (s : Set G) extends IsSubgroup s : Prop where
  normal : ∀ n ∈ s, ∀ g : G, g * n * g⁻¹ ∈ s

theorem Additive.isAddSubgroup {s : Set G} (hs : IsSubgroup s) : @IsAddSubgroup (Additive G) _ s :=
  @IsAddSubgroup.mk (Additive G) _ _ (Additive.isAddSubmonoid hs.toIsSubmonoid) hs.inv_mem

theorem Additive.isNormalAddSubgroup [Group G] {s : Set G} (hs : IsNormalSubgroup s) :
    @IsNormalAddSubgroup (Additive G) _ s :=
  @IsNormalAddSubgroup.mk (Additive G) _ _ (Additive.isAddSubgroup hs.toIsSubgroup)
    (@IsNormalSubgroup.normal _ ‹Group (Additive G)› _ hs)
    -- porting note: Lean needs help synthesising
    -- fails: (IsNormalSubgroup.normal hs)

[Winston Yin (尹維晨)]

There are a few such examples in deprecated.subgroup