Polynomial.algebraMap_apply

Stream: mathlib4

[Bolton Bailey]

Can docs#Polynomial.algebraMap_apply be made simp? Seems like it would potentially some proofs one-shot-simps, like the ones in the Equiv file in the PR.

[Bolton Bailey]

What is happening in Mathlib/RingTheory/Polynomial/Basic.lean? When correcting the bug I try to simp, but it stops simplifying at the goal C r = (killCompl _) (C r). What is the underscore? Why does it matter? Shouldn't docs#MvPolynomial.algHom_C clear it?

[Bolton Bailey]

MWE:

import Mathlib.Data.MvPolynomial.CommRing

universe u v w

namespace MvPolynomial

lemma mwe {R : Type u} (σ) [CommRing R] {r : R} (s: Finset σ) : C r = (@killCompl { x // x ∈ s } σ R CommRing.toCommSemiring (fun a ↦ ↑a) Subtype.coe_injective) (C r) := by
  -- simp -- no progress
  rw [MvPolynomial.algHom_C (@killCompl { x // x ∈ s } σ R CommRing.toCommSemiring (fun a ↦ ↑a) Subtype.coe_injective) r]
  -- Did not find instance of the pattern in the target expression

[Bolton Bailey]

What I don't understand is why the infoview shows a hole. I have specified all my arguments, right?