simps and match and destruction of a subtype with a metavar

Stream: general

[Yakov Pechersky]

In #26941, I proposed changing the construction of docs#WithZero.lift' to use recZeroCoe directly. I ran into this while working with a more complex construction mapping a valuation's value group with zero to a different type. This construction is via composition with WithZero.withZeroUnitsEquiv, which is simps tagged.

Somehow, when using simp in a downstream proof where I am constructing a Units on the fly with a deferred proof obligation metavariable, there is a match match ↑⟨y, ⋯⟩ with that doesn't get simplified. This happens when lift' is defined via an explicit match. If, instead, lift' used recZeroCoe, then the match does get simplified.

This seems to be some complex interaction with simps, because any simpler goals of the same nature don't seem to have this issue. The "MWE" is below, showing the different goal states for the existing and proposed new definition.

Do any simp and simps experts understand what's going on?

import Mathlib.Algebra.GroupWithZero.WithZero
import Mathlib.Algebra.GroupWithZero.Range
import Mathlib.Algebra.Order.GroupWithZero.WithZero

variable {G H : Type*} [CommGroupWithZero G] [LinearOrderedCommGroupWithZero H] (f : G →*₀ H)

open MonoidWithZeroHom

@[simps!]
def foo : WithZero (valueGroup f) →*₀ WithZero Hˣ :=
  WithZero.map' (valueGroup f).subtype

/--
info: theorem _example.extracted_1.{u_2, u_1} {G : Type u_1} {H : Type u_2} [inst : CommGroupWithZero G]
  [inst_1 : LinearOrderedCommGroupWithZero H] (f : G →*₀ H) (x : H) (y : Hˣ) :
  WithZero.recZeroCoe 0 Units.val
      (match ↑⟨y, ⋯⟩ with
      | none => 0
      | some a => ↑↑a) =
    x := sorry
-/
#guard_msgs (info) in
example {G : Type*} [Group G] (s : Subgroup G) (x : H) (y : Hˣ) :
    ∃ y : WithZero (valueGroup f),
      (WithZero.withZeroUnitsEquiv.toMonoidHom.comp (foo f).toMonoidHom) y = x := by
  refine ⟨WithZero.coe ⟨y, ?_⟩, ?_⟩
  · sorry
  · simp
    extract_goal
    sorry

@[simps! symm_apply_apply]
nonrec def lift'' {α β : Type*} [MulOneClass α] [MulZeroOneClass β] :
    (α →* β) ≃ (WithZero α →*₀ β) where
  toFun f :=
    { toFun := WithZero.recZeroCoe 0 f
      map_zero' := rfl
      map_one' := by simp
      map_mul' := fun
        | 0, _ => (zero_mul _).symm
        | (_ : α), 0 => (mul_zero _).symm
        | (_ : α), (_ : α) => map_mul f _ _ }
  invFun F := F.toMonoidHom.comp WithZero.coeMonoidHom

def map'' {α β : Type*} [MulOneClass α] [MulOneClass β] (f : α →* β) :
    WithZero α →*₀ WithZero β :=
  lift'' (WithZero.coeMonoidHom.comp f)

@[simps!]
def fooAgain : WithZero (valueGroup f) →*₀ WithZero Hˣ :=
  map'' (valueGroup f).subtype

/--
info: theorem _example.extracted_1.{u_2, u_1} {G : Type u_1} {H : Type u_2} [inst : CommGroupWithZero G]
  [inst_1 : LinearOrderedCommGroupWithZero H] (f : G →*₀ H) (x : H) (y : Hˣ) : ↑y = x := sorry
-/
#guard_msgs (info) in
example {G : Type*} [Group G] (s : Subgroup G) (x : H) (y : Hˣ) :
    ∃ y : WithZero (valueGroup f),
      (WithZero.withZeroUnitsEquiv.toMonoidHom.comp (fooAgain f).toMonoidHom) y = x := by
  refine ⟨WithZero.coe ⟨y, ?_⟩, ?_⟩
  · sorry
  · simp
    extract_goal
    sorry