Nonsense autocomplete of `cases with`

Stream: general

[Eric Wieser]

If I type the following:

import Mathlib.Algebra.Category.MonCat.Colimits

open CategoryTheory

example {J : Type v} [inst : SmallCategory J] (F : J ⥤ MonCat) (s : Cocone F)
    (x y) (r : MonCat.Colimits.Relation F x y) : true := by
  cases r with

then the "Generate an explicit pattern match" action generates the following nonsense:

  cases r with
  | J => sorry
  | inst._@.Mathlib.Algebra.Category.MonCat.Colimits._hyg.119 => sorry
  | F => sorry
  | refl x => sorry
  | symm x y _ => sorry
  | trans x y z _ _ => sorry
  | map j j' f x => sorry
  | mul j x y => sorry
  | one j => sorry
  | mul_1 x x' y _ => sorry
  | mul_2 x y y' _ => sorry
  | mul_assoc x y z => sorry
  | one_mul x => sorry
  | mul_one x => sorry

[Eric Wieser]

In particular, it seems to have generated cases for the arguments of Relation:

MonCat.Colimits.Relation.{v} {J : Type v} [inst✝ : SmallCategory J] (F : J ⥤ MonCat)
  (a✝a✝¹ : MonCat.Colimits.Prequotient F) : Prop

[Mario Carneiro]

can you make a MWE?

[Eric Wieser]

You mean a mathlib-free one?

[Eric Wieser]

inductive Relation (n : ℕ) : ℕ → ℕ → Prop
| ohno : Relation n 1 1
| anyway : Relation n 2 2

example {x y z} (r : Relation x y z) : true := by
  cases r with

[Eric Wieser]

Or even

inductive Relation (n : ℕ) : ℕ → ℕ → Prop

example {x y z} (r : Relation x y z) : true := by
  cases r with

[Kevin Buzzard]

Also https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20How.20do.20I.20refer.20to.20hypothesis.20created.20by.20tactics.3F/near/390993766