algHom_C not firing

Stream: mathlib4

[Bolton Bailey]

Here is an even simpler example of the error I got in a recent thread. Why doesn't algHom_C fire here?

import Mathlib.Data.MvPolynomial.Rename

@[simp]
theorem killCompl_C {σ τ R : Type} [CommSemiring R] {f : σ → τ} (hf : Function.Injective f) (r : R) :
    MvPolynomial.killCompl hf (MvPolynomial.C r) = MvPolynomial.C r := by
  rw [MvPolynomial.algHom_C] -- Why doesn't this work?

[Kevin Buzzard]

If my understanding is correct,MvPolynomial.algHom_C takes an input (f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R) i.e. f : X →ₐ[R] X and you're trying to apply it to an algebra hom between two different rings.

I debugged this by changing the rw to a refine (filling in the holes with ?_) and then a convert. Let me know if I've misunderstood.

[Bolton Bailey]

The ring is always R. You mean the type of variables in AlgHom_C has to be the same, whereas in my lemma it's different (τ to σ). Thanks, I don't know how I missed that.

[Bolton Bailey]

Hmm, should algHom_C hold for different variable types though?

[Bolton Bailey]

Yeah I just checked, the proof of algHom_C does go through for different variable types, and correcting this makes my proof work. Thanks for helping me catch this.

[Bolton Bailey]

I feel like when I was doing this myself I got to this stage:

import Mathlib.Data.MvPolynomial.Rename

@[simp]
theorem killCompl_C {σ τ R : Type} [CommSemiring R] {f : σ → τ} (hf : Function.Injective f) (r : R) :
    MvPolynomial.killCompl hf (MvPolynomial.C r) = MvPolynomial.C r := by
  apply MvPolynomial.algHom_C (MvPolynomial.killCompl hf) r

And I got the message

tactic 'apply' failed, failed to unify
  (MvPolynomial.killCompl ?m.769) (MvPolynomial.C r) = MvPolynomial.C r
with
  (MvPolynomial.killCompl hf) (MvPolynomial.C r) = MvPolynomial.C r

I don't get why I get this message here, and I think it's why I stopped the "specify implicits" train. Why does the first thing that it is unifying have a metavariable in it? I specify the argument right there!

[Eric Wieser]

Does using refine instead of apply help?

[Bolton Bailey]

It tells me

application type mismatch
  MvPolynomial.killCompl hf
argument
  hf
has type
  Function.Injective f : Prop
but is expected to have type
  Function.Injective ?m.663 : Prop

Which I suppose is helpful, since it would trigger me to start filling implicits again, but the implicit I feel like I have to fill is (f := f) and this doesn't change the error.

[Bolton Bailey]

I have no idea what the difference is between refine and apply for this use case, but they both look wrong.

[Bolton Bailey]

Here is the code with refine

import Mathlib.Data.MvPolynomial.Rename

@[simp]
theorem killCompl_C {σ τ R : Type} [CommSemiring R] {f : σ → τ} (hf : Function.Injective f) (r : R) :
    MvPolynomial.killCompl (f := f) hf (MvPolynomial.C r) = MvPolynomial.C r := by
  refine MvPolynomial.algHom_C (MvPolynomial.killCompl (f := f) hf) r

[Bolton Bailey]

I can even MWE it down to a mathlib-free version. Let me continue in a thread in #lean4