## Stream: general

### Topic: How does congr know to apply subsingleton.elim

#### Eric Wieser (Jan 05 2021 at 12:11):

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 (Jan 05 2021 at 12:21):

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] :
: 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 (Jan 05 2021 at 12:22):

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 (Jan 05 2021 at 13:01):

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

Last updated: May 14 2021 at 03:27 UTC