making `simp` work with restricted products

Stream: mathlib4

[Kevin Buzzard]

I am not competent enough to fix the following. If the components of a restricted product are isomorphic then the restricted products are isomorphic. Here's part of a proof of this.

import Mathlib.Topology.Algebra.RestrictedProduct

variable
    -- let ι be an index set.
    {ι : Type*}
    -- Let Gᵢ and Hᵢ be ι-indexed families of types
    {G H : ι → Type*}
    -- Let Cᵢ ⊆ Gᵢ and Dᵢ ⊆ Hᵢ be subsets
    {C : (i : ι) → Set (G i)} {D : (i : ι) → Set (H i)}
    -- Let φᵢ : Gᵢ → Hᵢ be a bijection
    (φ : (i : ι) → G i ≃ H i)
    {𝓕 : Filter ι}
    -- and assume φᵢ(Cᵢ) = Dᵢ for all but finitely many i
    (hφ : ∀ᶠ i in 𝓕, φ i ⁻¹' (D i) = C i)

open RestrictedProduct

set_option linter.flexible false in -- just to stop the noise
/-- The induced isomorphoism-/
def Equiv.restrictedProductCongrRight :
    (Πʳ i, [G i, C i]_[𝓕]) ≃ (Πʳ i, [H i, D i]_[𝓕]) where
  toFun x := ⟨fun i ↦ φ i (x i), sorry⟩
  invFun y := ⟨fun i ↦ (φ i).symm (y i), sorry⟩
  left_inv x := by -- this should be easy
    ext i -- goal is kind of a mess
    simp -- please tidy it up
    dsimp -- please?
    -- ⊢ ⟨fun i ↦ (φ i).symm (⟨fun i ↦ (φ i) (x i), ⋯⟩ i), ⋯⟩ i = x i
    change (φ i).symm (φ i (x i)) = x i -- this is what I want
    simp -- now simp works
  right_inv := sorry

As you can see, simp isn't doing what I want it to do, which getting rid of the fun. Does this mean there's a missing simp lemma? I can't figure out what it is though. There is no RestrictedProduct.mk because RestrictedProduct is just defined as a subtype. I attempted to define a simp lemma

section API

open RestrictedProduct

variable {ι : Type*}
variable (R : ι → Type*) (A : (i : ι) → Set (R i))
variable {𝓕 : Filter ι}

@[simp]
lemma RestrictedProduct.mk_apply (x : Π i, R i) (hx : ∀ᶠ i in 𝓕, x i ∈ A i) (i : ι) :
    (⟨x, hx⟩ : Πʳ i, [R i, A i]_[𝓕]) i = x i := rfl

end API

but this doesn't even typecheck, because I don't know how to make a term of type RestrictedProduct ..., the ⟨x, hx⟩ just makes a subtype. The id trick works:

(id ⟨x, hx⟩ : Πʳ i, [R i, A i]_[𝓕]) i = x i := rfl

but this doesn't seem to make simp fire. What lemma do I need to make simp close this goal?

[Andrew Yang]

Something like this would work

@[simp]
lemma RestrictedProduct.mk_apply {x : Π i, G i} (hx) (i) :
    letI x' : Πʳ i, [G i, C i]_[𝓕] := ⟨x, hx⟩
    x' i = x i := rfl

Or this might be better but I'm not sure (it works here at least):

abbrev RestrictedProduct.mk (x : Π i, G i) (hx : ∀ᶠ (i : ι) in 𝓕, x i ∈ C i) :
    Πʳ i, [G i, C i]_[𝓕] :=
  ⟨x, hx⟩

@[simp]
lemma RestrictedProduct.mk_apply {x : Π i, G i} (hx : ∀ᶠ (i : ι) in 𝓕, x i ∈ C i) (i) :
    RestrictedProduct.mk x hx i = x i := rfl

[Eric Wieser]

I think the missing lemma is coe_mk not mk_apply