How does `congr` know to apply `subsingleton.elim`

Stream: general

[Eric Wieser]

Is this hard coded? docs#subsingleton.elim doesn't have any any attributes attached, so I'm not sure how to investigate further into what tactic#congr is doing
.

[Eric Wieser]

The example in question is

import linear_algebra.tensor_product
open_locale tensor_product

example {R M N : Type*}
  [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] :
  (add_comm_monoid.nat_semimodule.to_distrib_mul_action.to_mul_action.to_has_scalar
    : has_scalar ℕ (M ⊗[R] N)) =
  tensor_product.has_scalar' :=
begin
  change _ = tensor_product.semimodule'.to_distrib_mul_action.to_mul_action.to_has_scalar,
  congr,
  apply_instance,
  apply_instance,
end

[Eric Wieser]

And I was hoping that I could train congr to solve it more easily. I can't see how to tag this with attr#congr either.

[Gabriel Ebner]

subsingleton is hard-coded into the code that creates the congruence lemmas.