Search for actual match

Stream: mathlib4

[Patrick Massot]

How do I ask Lean to find a lemma whose statement is exactly {α β : Type} (a : α) (b : β) : (a, b).1 = a? Using exact? tells me this is rfl, which I already knew and is not my question. I tried various ways to ask find/loogle but it returns many irrelevant results and then times out.

[Mario Carneiro]

grep?

[Yaël Dillies]

Maybe exact? could have a reducibility setting?

[Mario Carneiro]

it doesn't help, this is a reducible refl

[Mario Carneiro]

and unfold reducibles is the lightest reducibility setting you can set

[Ruben Van de Velde]

Try rw?

[Eric Rodriguez]

rw? suggests docs#Prod.fst_eq_iff, which isn't far

[Patrick Massot]

It's still not the right one.

[Kyle Miller]

@Patrick Massot What's the right one? I haven't found one in mathlib.

[Kyle Miller]

Here's an exact search command:

import Mathlib

namespace ExactSearch

open Lean Elab Term Command

elab "#find_exact " t:term : command => runTermElabM fun vars => do
  let e ← withSynthesize <| elabTerm t none
  let e ← Meta.mkForallFVars (usedOnly := true) vars e
  let e ← instantiateMVars e
  let e ← Elab.Term.levelMVarToParam e
  if e.hasExprMVar then
    throwError "Expression has metavariables:{indentD e}"
  logInfo m!"Searching for {e}"
  -- Look in particular for `e` with all level parameters set to 0
  let e' := e.instantiateLevelParams (← getLevelNames) (List.replicate (← getLevelNames).length .zero)
  let env ← getEnv
  let r ← env.constants.foldM (init := ({} : NameSet)) fun s n ci => do
    let ty := ci.type.instantiateLevelParams ci.levelParams (List.replicate ci.levelParams.length .zero)
    if ty == e' then
      return s.insert n
    else
      return s
  logInfo m!"All matches: {r.toList}"


variable {α β : Type _}

lemma patrick_lemma (a : α) (b : β) : (a, b).1 = a := rfl

#find_exact ∀ (a : α) (b : β), (a, b).1 = a
-- All matches: [ExactSearch.patrick_lemma]

[Kyle Miller]

Caveat: it's an exact search after setting all universe level variables to 0, since the full problem would involve checking that there's a permutation of the universe levels variables.

[Patrick Massot]

I don't know what is the right one, otherwise I wouldn't be searching for it.

[Patrick Massot]

I just assume it would be somewhere.

[Patrick Massot]

The actual context of this question is at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/New.20exotic.20simp.20failure

[Mario Carneiro]

I don't think it exists

[Damiano Testa]

I had observed something similar elsewhere. I had formed the idea that Lean generated internally a lemma that it uses to solve this equality and then discarded it. Though I cannot reproduce what I observed in your specific case...