PANIC ...contains rhs

Stream: mathlib4

[Joël Riou]

Around the marked lines https://github.com/leanprover-community/mathlib4/pull/2534/files#diff-dbac9e254ec82565831843ba6c9b622e4a210161ec9c7f4ce6d99d8e04d8571aR140-R144 in a PR about CategoryTheory.Category.Pairwise, the Lean server produces an error PANIC at _private.Lean.Meta.Match.MatchEqs.0.Lean.Meta.Match.SimpH.substRHS Lean.Meta.Match.MatchEqs:167:2: assertion violation: ( __do_lift._@.Lean.Meta.Match.MatchEqs._hyg.2199.0 ).xs.contains rhs. I have no idea what this means. See https://github.com/leanprover-community/mathlib4/actions/runs/4301463837/jobs/7498718508 for the full output

[Adam Topaz]

some issue with hygiene, maybe?

[Adam Topaz]

it seems that the inductive type defining homs is the root of the issue, or maybe just diagramMap?

[Adam Topaz]

maybe not... turning off hygiene doesn't resolve the error.

[Matthew Ballard]

Does explicitly filling the other fields of the functor help?

[Adam Topaz]

yeah, filling in the fields as

def diagram : Pairwise ι ⥤ α where
  obj := diagramObj U
  map f := diagramMap U f
  map_id := fun _ => rfl
  map_comp := fun _ _ => rfl

gets rid of the error.
It looks like an application of simp (either via aesop_cat or directly) is causing the error somehow

[Matthew Ballard]

Maybe it should be contains??

[Joël Riou]

Thanks! It seems it was aesop_cat which was causing the error. Filling the proofs for this definition (and another in the end of the file) fixes the problem.

[Kevin Buzzard]

I was also seeing PANICs which were conjecturally tracked down to aesop_cat in a recent thread.

[Jannis Limperg]

See #mathlib4 > PSA: using Aesop for auto-params; fix is on the way.

[Adam Topaz]

In this case, it's not aesop specifically, it's simp.
E.g. this gives the same error

def diagram : Pairwise ι ⥤ α where
  obj := diagramObj U
  map f := diagramMap U f
  map_id := fun _ => by
    simp
    rfl
  map_comp := fun _ _ => rfl

[Adam Topaz]

dsimp is fine though :shrug:

[Adam Topaz]

I'll extract a mwe

[Adam Topaz]

okay, the last by simp gives the same error in the following not-so-minimal code:

import Mathlib

namespace Test

inductive Pairwise (ι : Type v)
  | single : ι → Pairwise ι
  | pair : ι → ι → Pairwise ι

variable {ι : Type v}

namespace Pairwise

inductive Hom : Pairwise ι → Pairwise ι → Type v
  | id_single : ∀ i, Hom (single i) (single i)
  | id_pair : ∀ i j, Hom (pair i j) (pair i j)
  | left : ∀ i j, Hom (pair i j) (single i)
  | right : ∀ i j, Hom (pair i j) (single j)

open Hom CategoryTheory

def id : ∀ o : Pairwise ι, Hom o o
  | single i => id_single i
  | pair i j => id_pair i j

variable {α : Type v} (U : ι → α) [SemilatticeInf α]

@[simp]
def diagramObj : Pairwise ι → α
  | single i => U i
  | pair i j => U i ⊓ U j

@[simp]
def diagramMap : ∀ {o₁ o₂ : Pairwise ι} (_ : Hom o₁ o₂), diagramObj U o₁ ⟶ diagramObj U o₂
  | _, _, id_single _ => 𝟙 _
  | _, _, id_pair _ _ => 𝟙 _
  | _, _, left _ _ => homOfLE inf_le_left
  | _, _, right _ _ => homOfLE inf_le_right

set_option hygiene false in
lemma diagramMap_id :
  diagramMap U (Pairwise.id x : Hom x x) = 𝟙 _ := by simp

end Pairwise
end Test

[Adam Topaz]

OTOH, rfl works just fine