simp / rw with full defeq

Stream: general

[Mirek Olšák]

Is it possible to make simp, or rw look for any defeq match of a given theorem with the lhs? I guess writing a simproc for this should not be too hard but I thought there already could be a standard way. The particular use case I have in mind now is the one below, although I imagine it could be useful for various reasons.

module
import Mathlib.Data.Fin.VecNotation
import Mathlib.Data.Nat.SuccPred

def Fin.const {Dom : Type} (n : Nat) (c : Dom) : Fin n → Dom :=
  match n with
  | 0 => Matrix.vecEmpty
  | n+1 => Fin.cons c (const n c)

theorem Fin.const_eq {Dom : Type} {n : ℕ} {c : Dom} :
    Fin.const n c = (fun _ ↦ c) := by
  induction n with
  | zero =>
    funext x
    apply x.elim0
  | succ n ih =>
    funext ⟨x, h⟩
    cases x with
    | zero => rfl
    | succ k =>
      exact congrFun ih ⟨k, Order.lt_add_one_iff.mp h⟩

def Multiary (Dom arity : Type) := (arity → Dom) → Dom
def Multiary.idempotent {Dom arity : Type} (f : Multiary Dom arity) : Prop :=
  ∀ x : Dom, f (fun _ ↦ x) = x

theorem Multiary.idempotent_fin {Dom : Type} {arity : ℕ}
    {f : Multiary Dom (Fin arity)} (h : f.idempotent) {x : Dom} :
    f (Fin.const arity x) = x := by
  rw [Fin.const_eq]
  exact h x

example (f : Multiary Nat (Fin 6)) (h : f.idempotent) : f ![0,0,0,0,0,0] ≠ 2 := by
  simp! [f.idempotent_fin h] -- I would like to solve the goal already with something like this
  simp [show f ![0,0,0,0,0,0] = 0 by exact f.idempotent_fin h] -- this actually solves the goal

[Jovan Gerbscheid]

I think you are looking for erw:

example (f : Multiary Nat (Fin 6)) (h : f.idempotent) : f ![0,0,0,0,0,0] ≠ 2 := by
  erw [f.idempotent_fin h]
  simp