tactic#transport not solving any goals

Stream: general

[Eric Wieser]

Any idea why transport leaves all the goals unsolved here?

import tactic.transport
import algebra.monoid_algebra

noncomputable theory

variables (k : Type*) (G : Type*) [add_monoid G] [semiring k]

@[derive add_comm_monoid]
def my_add_monoid_algebra := G →₀ k

variables {k G}

def of_add' : my_add_monoid_algebra k G ≃+ monoid_algebra k (multiplicative G) :=
(finsupp.dom_congr multiplicative.of_add)

@[simp] def of_add'_apply (f : my_add_monoid_algebra k G) :
  of_add' f = f.map_domain multiplicative.of_add := rfl

@[simp] def of_add'_symm_apply (f : monoid_algebra k (multiplicative G)) :
  of_add'.symm f = f.map_domain multiplicative.of_add.symm := rfl

-- mathlib#4651
@[simp] def of_add_symm_eq_to_add : (@multiplicative.of_add G).symm = multiplicative.to_add := rfl
@[simp] def to_add_symm_eq_of_add : (@multiplicative.of_add G).symm = multiplicative.to_add := rfl

instance : semiring (my_add_monoid_algebra k G) :=
by transport (infer_instance : semiring (monoid_algebra k (multiplicative G))) using of_add'

[Bryan Gin-ge Chen]

(deleted)