refine_struct not working as advertised? about mathlib HOT 8 CLOSED

def my_foo {α} (x : semigroup α) (y : group α) : true := trivial

example {α : Type} : true :=
begin
  refine_struct (@my_foo α { .. } { .. } ),
    -- 9 goals
    -- case semigroup, mul
    -- α : Type
    -- ⊢ α → α → α

    -- case semigroup, mul_assoc
    -- α : Type
    -- ⊢ ∀ (a b c : α), a * b * c = a * (b * c)

    -- case group, mul
    -- α : Type
    -- ⊢ α → α → α

    -- case group, mul_assoc
    -- α : Type
    -- ⊢ ∀ (a b c : α), a * b * c = a * (b * c)

    -- case group, one
    -- α : Type
    -- ⊢ α

    -- case group, one_mul
    -- α : Type
    -- ⊢ ∀ (a : α), 1 * a = a

    -- case group, mul_one
    -- α : Type
    -- ⊢ ∀ (a : α), a * 1 = a

    -- case group, inv
    -- α : Type
    -- ⊢ α → α

    -- case group, mul_left_inv
    -- α : Type
    -- ⊢ ∀ (a : α), a⁻¹ * a = 1

end