refl failure without intros

Stream: general

[Oliver Nash]

Is there an easy explanation for why the following fails if I drop the intros from the proof of map_mul?

universes u v w

variables {α : Type u} {β : Type v} {γ : Type w} [monoid β] [comm_monoid γ]

@[to_additive]
lemma hom_prod (s : finset α) (b : β) (g : α → β →* γ) :
  s.prod (λ a, g a b) = (s.prod g) b :=
begin
let evb : (β →* γ) → γ := λ h, h b,
haveI : is_monoid_hom evb := {
  map_one := rfl,
  map_mul := by { intros, refl, }, },
rw finset.prod_hom s evb,
end

[Oliver Nash]

The error I see if I replace map_mul := by { intros, refl, } with map_mul := rfl is:

type mismatch at field 'map_mul'
  rfl
has type
  ?m_2 = ?m_2
but is expected to have type
  ∀ (x y : β →* γ), evb (x * y) = evb x * evb y

[Patrick Massot]

Why would it work?

[Oliver Nash]

Erm, good question!

[Patrick Massot]

in

example : ∀ n : ℕ, n = n :=
begin
  sorry
end

would you expect refl to close the goal?

[Patrick Massot]

hint: you shouldn't.

[Oliver Nash]

Oh dear, I would have expected it to close that goal :embarrassed:

[Oliver Nash]

Thank you for providing such a simplified example. Is there a simple explanation for when I should expect refl to work, or somewhere I should look to read more?

[Patrick Massot]

You should expect it to work when the goal is x = x, maybe in disguise.

[Oliver Nash]

Till now I had regarded it as a way to close goals that are just definitional equalities once you unfold sufficiently (or something along those lines).

[Patrick Massot]

Yes, exactly.

[Oliver Nash]

Right, that has been my approximate understanding.

[Patrick Massot]

And ∀ n : ℕ, n = n is not of that form.

[Oliver Nash]

But I'm fairly sure it has been able to succeed in the past when there was a universal qualifier "in the way".

[Oliver Nash]

Understood, perhaps my memory misleads me.

[Oliver Nash]

Hmm, I suppose it does. There does not seem to be anything more to this.

[Oliver Nash]

Thank you!

[Patrick Massot]

If you are frustrated to have to type two tactics to close this goal you can probably try tauto

[Oliver Nash]

Right ho, I'll use that.

[Patrick Massot]

I hope Mario has a good zulip filtering preventing him from seeing such suggestions...

[Oliver Nash]

You mean my original message (which I now realise was perhaps wasting people's time) or the suggestion to use tauto?

[Patrick Massot]

Seriously, the right proof here is lambda _ _, rfl

[Patrick Massot]

I meant the suggestion to use tauto

[Oliver Nash]

Oh I see.

[Patrick Massot]

You are not wasting people's time. Everybody answering questions here is volunteer, and has been asking elementary questions before.

[Oliver Nash]

Well, I can believe tauto might be too heavyweight alright!

[Oliver Nash]

Thanks for the encouragement, and again for the clarifications.

[Mario Carneiro]

I like the proof \lam _, rfl

[Mario Carneiro]

Note that refl already has problems with guessing the number of arguments because it is equivalent to apply *refl where *refl is some reflexivity lemma

[Mario Carneiro]

and the apply bug causes issues in cases like le_refl when le is defined as a pi

[Mario Carneiro]

maybe this is your recollection

[Oliver Nash]

Thank you @Mario Carneiro I suspect this is the case. I appreciate this further information.

[Jesse Michael Han]

this is also by cc