Lemma not working for ```rw``` when outside a proof

Stream: lean4

[Sophie Morel]

I'm asking this question here, because it looks like more of a Lean question than a math question per se.

I'm trying to shorten a proof by extracting a lemma that is used twice in it, rather than copy-pasting code. Except that if I state and prove the lemma outside of my bigger proof, rw refuses to take it (so does erw), with a did not find instance of the pattern error. But it should be the same statement, shouldn't it ?
Here is a MWE:

import Mathlib.Tactic
import Mathlib.LinearAlgebra.Multilinear.Basic

variable {ι : Type*} {R : Type*} {M₁ : ι → Type*} {M₂ : Type*} (s : Set ι) [DecidableEq ι]
[(i : ι) → Decidable (i ∈ s)] (x : (i : ι) → M₁ i)

-- This is my rewriting lemma.
lemma truc (z : (i : s) → M₁ i) (i : s) (c : M₁ i) :
    (fun j ↦ if h : j ∈ s then Function.update z i c ⟨j, h⟩ else x j) =
    Function.update (fun j => if h : j ∈ s then z ⟨j, h⟩ else x j) i c := by
  ext j
  by_cases h : j = i.1
  . rw [h, Function.update_same]
    simp only [Subtype.coe_prop, Function.update_same, dite_eq_ite, ite_true]
  . rw [Function.update_noteq h]
    by_cases h' : j ∈ s
    . simp only [h', ne_eq, dite_true]
      have h'' : ¬ ⟨j, h'⟩ = i :=
        fun he => by apply_fun (fun x => x.1) at he; exact h he
      rw [Function.update_noteq h'']
    . simp only [h', ne_eq, dite_false]


variable [Semiring R] [∀ i, AddCommMonoid (M₁ i)] [AddCommMonoid M₂]
[∀ i, Module R (M₁ i)] [Module R M₂]

def toMultilinearMap_set (f : MultilinearMap R M₁ M₂) (x : (i : ι) → M₁ i)
    (s : Set ι) [(i : ι) → Decidable (i ∈ s)] :
    MultilinearMap R (fun (i : s) => M₁ i) M₂ where
  toFun z := f (fun i ↦ if h : i ∈ s then z ⟨i, h⟩ else x i)
  map_add' z i a b := by
    simp only
-- This is apparently the exact same thing as the rewriting lemma, except it is now a `have` statement inside the proof.
    have machin : ∀ (c : M₁ i),
        (fun j ↦ if h : j ∈ s then Function.update z i c ⟨j, h⟩ else x j) =
        Function.update (fun j => if h : j ∈ s then z ⟨j, h⟩ else x j) i c := by
      intro c; ext j
      by_cases h : j = i.1
      . rw [h, Function.update_same]
        simp only [Subtype.coe_prop, Function.update_same, dite_eq_ite, ite_true]
      . rw [Function.update_noteq h]
        by_cases h' : j ∈ s
        . simp only [h', ne_eq, dite_true]
          have h'' : ¬ ⟨j, h'⟩ = i :=
            fun he => by apply_fun (fun x => x.1) at he; exact h he
          rw [Function.update_noteq h'']
        . simp only [h', ne_eq, dite_false]
 -- End of rewriting lemma.
    rw [machin b]  -- This works !
    rw [truc (ι := ι) (M₁ := M₁) s x z i a] -- This does not. :-(
    -- Error message : tactic 'rewrite' failed, did not find instance of the pattern in the target expression
    --                 fun j ↦ if h : j ∈ s then Function.update z i ?c { val := j, property := h } else x j
  map_smul' := sorry

[Ruben Van de Velde]

map_add' puts a DecidableEq ↑s hypothesis in your context

[Ruben Van de Velde]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Multilinear/Basic.html#Implementation-notes has some background

[Ruben Van de Velde]

This works:

import Mathlib.Tactic
import Mathlib.LinearAlgebra.Multilinear.Basic

variable {ι : Type*} {R : Type*} {M₁ : ι → Type*} {M₂ : Type*} (s : Set ι) [DecidableEq ι]
[(i : ι) → Decidable (i ∈ s)] (x : (i : ι) → M₁ i)

-- This is my rewriting lemma.
lemma truc (z : (i : s) → M₁ i) (i : s) (c : M₁ i) :
    (fun j ↦ if h : j ∈ s then Function.update z i c ⟨j, h⟩ else x j) =
    Function.update (fun j => if h : j ∈ s then z ⟨j, h⟩ else x j) i c := by
  ext j
  by_cases h : j = i.1
  . rw [h, Function.update_same]
    simp only [Subtype.coe_prop, Function.update_same, dite_eq_ite, ite_true]
  . rw [Function.update_noteq h]
    by_cases h' : j ∈ s
    . simp only [h', ne_eq, dite_true]
      have h'' : ¬ ⟨j, h'⟩ = i :=
        fun he => by apply_fun (fun x => x.1) at he; exact h he
      rw [Function.update_noteq h'']
    . simp only [h', ne_eq, dite_false]


variable [Semiring R] [∀ i, AddCommMonoid (M₁ i)] [AddCommMonoid M₂]
[∀ i, Module R (M₁ i)] [Module R M₂]

def toMultilinearMap_set (f : MultilinearMap R M₁ M₂) (x : (i : ι) → M₁ i)
    (s : Set ι) [(i : ι) → Decidable (i ∈ s)] :
    MultilinearMap R (fun (i : s) => M₁ i) M₂ where
  toFun z := f (fun i ↦ if h : i ∈ s then z ⟨i, h⟩ else x i)
  map_add' z i a b := by
    simp only
    rename_i inst
    obtain rfl := Subsingleton.elim inst Subtype.instDecidableEqSubtype
    rw [truc (ι := ι) (M₁ := M₁) s x z i a]
    sorry
  map_smul' := sorry

[Ruben Van de Velde]

Or:

import Mathlib.Tactic
import Mathlib.LinearAlgebra.Multilinear.Basic

variable {ι : Type*} {R : Type*} {M₁ : ι → Type*} {M₂ : Type*} (s : Set ι) [DecidableEq ι]
[(i : ι) → Decidable (i ∈ s)] (x : (i : ι) → M₁ i)

-- This is my rewriting lemma.
lemma truc
    [DecidableEq ↑s] -- Redundant hypothesis, but makes the lemma more general
    (z : (i : s) → M₁ i) (i : s) (c : M₁ i) :
    (fun j ↦ if h : j ∈ s then Function.update z i c ⟨j, h⟩ else x j) =
    Function.update (fun j => if h : j ∈ s then z ⟨j, h⟩ else x j) i c := by
  ext j
  by_cases h : j = i.1
  . rw [h, Function.update_same]
    simp only [Subtype.coe_prop, Function.update_same, dite_eq_ite, ite_true]
  . rw [Function.update_noteq h]
    by_cases h' : j ∈ s
    . simp only [h', ne_eq, dite_true]
      have h'' : ¬ ⟨j, h'⟩ = i :=
        fun he => by apply_fun (fun x => x.1) at he; exact h he
      rw [Function.update_noteq h'']
    . simp only [h', ne_eq, dite_false]


variable [Semiring R] [∀ i, AddCommMonoid (M₁ i)] [AddCommMonoid M₂]
[∀ i, Module R (M₁ i)] [Module R M₂]

def toMultilinearMap_set (f : MultilinearMap R M₁ M₂) (x : (i : ι) → M₁ i)
    (s : Set ι) [(i : ι) → Decidable (i ∈ s)] :
    MultilinearMap R (fun (i : s) => M₁ i) M₂ where
  toFun z := f (fun i ↦ if h : i ∈ s then z ⟨i, h⟩ else x i)
  map_add' z i a b := by
    simp only
    rw [truc (ι := ι) (M₁ := M₁) s x z i a]
    sorry
  map_smul' := sorry

[Sophie Morel]

Ruben Van de Velde said:

https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Multilinear/Basic.html#Implementation-notes has some background

Ooooh, that's what they meant ! To be honest, I would not have known what to do even with that. Thank you very much !