eliminators in term mode

Stream: general

[Kevin Buzzard]

Is there some black magic I can do to make list.rec work for me in term mode without the @? Why are there problems here? The tactic mode proof indicates that I've given all the information required for Lean to take things from here. No doubt I could add some type annotations -- but my point is that in the tactic mode proof these are not necessary, so why isn't there some @elab_as_eliminator stuff doing the same work for me in term mode?

import data.list.basic

-- this works fine
theorem prod_map_hom {α β γ : Type*} [monoid β] [monoid γ] (L : list α) (f : α → β) (g : β →* γ) :
  (L.map (g ∘ f)).prod = g ((L.map f).prod) :=
begin
  induction L with b L hL,
  { exact g.map_one.symm},
  { simp [g.map_mul, hL]}
end

-- this works fine
theorem prod_map_hom' {α β γ : Type*} [monoid β] [monoid γ] (L : list α) (f : α → β) (g : β →* γ) :
  (L.map (g ∘ f)).prod = g ((L.map f).prod) :=
@list.rec _ (λ L, (L.map (g ∘ f)).prod = g ((L.map f).prod))
  g.map_one.symm (λ _ _ IH, by simp [g.map_mul, IH]) L

-- this doesn't work
theorem prod_map_hom'' {α β γ : Type*} [monoid β] [monoid γ] (L : list α) (f : α → β) (g : β →* γ) :
  (L.map (g ∘ f)).prod = g ((L.map f).prod) :=
L.rec g.map_one.symm (λ _ _ IH, by simp [g.map_mul, IH])
/-
type mismatch at application
  list.rec _
term
  eq.symm (monoid_hom.map_one g)
has type
  1 = ⇑g 1 : Prop
but is expected to have type
  ?m_1 list.nil : Sort ?
-/

[Mario Carneiro]

the black magic is so not skip the last argument

[Mario Carneiro]

even if the result looks like an eta redex

[Reid Barton]

But it's there in L.rec right?

[Mario Carneiro]

oh and also don't use projection notation

[Mario Carneiro]

theorem prod_map_hom'' {α β γ : Type*} [monoid β] [monoid γ] (L : list α) (f : α → β) (g : β →* γ) :
  (L.map (g ∘ f)).prod = g ((L.map f).prod) :=
list.rec g.map_one.symm (λ _ _ IH, by simp [g.map_mul, IH]) L

[Mario Carneiro]

projection notation doesn't work on the built in recursors rec, rec_on and cases_on for some reason