Can't get aesop to apply lemma for me

Stream: new members

[Moritz R]

im trying to automate the well-definedness proof in Multiset.union with aesop, but i can't get aesop to apply Quotient.sound for me. apply Quotient.sound works though, so surely there must be a way to get aesop to do it here?

import Mathlib


instance Multiset'.Setoid (α : Type) [BEq α] : Setoid (List α) :=
{ r     := fun as bs ↦ ∀x, List.count x as = List.count x bs
  iseqv :=
    { refl  := by aesop
      symm  := by aesop
      trans := by aesop
    } }

def Multiset' (α : Type) [BEq α] : Type := Quotient (Multiset'.Setoid α)

def Multiset'.equiv_iff {α : Type} [BEq α] {as bs : List α}:
  as ≈ bs ↔ ∀x, List.count x as = List.count x bs := by rfl

set_option trace.aesop true

def Multiset'.union {α : Type} [BEq α] : Multiset' α → Multiset' α → Multiset' α :=
  Quotient.lift₂
  fun
  | l1, l2 => Quotient.mk _ (l1 ++ l2)
  (by
  intro a1 b1 a2 b2 h1 h2
  simp
  aesop (add safe apply Quotient.sound) -- apply works here...
  sorry
  )

[Kenny Lau]

@Moritz R #mwe please include enough imports on the top of your file so that it compiles by itself

[Moritz R]

should be fixed now

[Moritz R]

Any way to use aesop in lean 4 web?

[Kenny Lau]

@Moritz R well, how do you have aesop in your copy of the file where it works?

[Kevin Buzzard]

Moritz R said:

Any way to use aesop in lean 4 web?

import Aesop at the top

[Moritz R]

i thought Mathlib was imported automatically from the latest mathlib, but it isnt

[Moritz R]

i fixed the example to work on lean 4 web now

[Kevin Buzzard]

It's only imported if you import it!

[Moritz R]

I instead imported mathlib, which does that for me :D

[Moritz R]

The problem is reproducible now

[Moritz R]

If nobody knows, maybe i should ping @Jannis Limperg

[Jannis Limperg]

Interesting, this seems to be a failure of Aesop's indexing. aesop#241. No guarantees that I'll get to it soon, I'm afraid; I have very little time to spend on Aesop these days. :(