apply? failing

Stream: lean4

[Siddhartha Gadgil]

In the following example, if the last line of the proof is replaced by exact? we get an error and apply? has many suggestions, but none that close the goal. Is this just a case of depth of search? If so, is there some configuration change available?

import Mathlib

theorem isom_bijective :
      ∀ {G : Type u_11} {H : Type u_12} [Group G] [Group H] (ϕ : G ≃* H),
        Function.Bijective (⇑ϕ.toMonoidHom : G → H) :=
    by
    intro G H inst₁ inst₂ ϕ
    apply MulEquiv.bijective

[Siddhartha Gadgil]

I have reduced the import to just the file containing the theorem, Mathlib.Algebra.Group.Equiv.Defs, and things still fail. Is this a bug?

[Kim Morrison]

Have you looked at the output of set_option trace.Tactic.librarySearch and set_option trace.Tactic.librarySearch.lemmas?

[Siddhartha Gadgil]

Just tried, and it seems the correct function was found and rejected. Pasting the output from the infoview:

[Tactic.librarySearch] :cross_mark: Function.Bijective ⇑ϕ.toMonoidHom ▼
[] :cross_mark: trying EquivLike.bijective
[] :check: trying Function.bijective_iff_existsUnique with mpr
[] :check: trying Function.Bijective.of_comp_iff' with mp
[] :check: trying Function.bijective_iff_has_inverse with mpr
[] :cross_mark: trying Function.bijective_of_subsingleton
[] :check: trying Function.Bijective.of_comp_iff with mp
[] :cross_mark: trying Function.Involutive.bijective
[] :check: trying Unique.bijective
[] :check: trying EquivLike.bijective_comp with mp
[] :check: trying EquivLike.comp_bijective with mp
[] :check: trying Equiv.bijective_comp with mp
[] :check: trying Equiv.comp_bijective with mp

[Siddhartha Gadgil]

Oops, sorry. That is a different function.

[Siddhartha Gadgil]

But it seems that 12 functions were tried, 9 leading to the next step and some internal barrier was hit (was it constantsPerImportTask?)

[Kim Morrison]

That looks like MulEquiv.bijective isn't even on the list. Does it show up under the lemmas trace option?

[Siddhartha Gadgil]

I got that list with

set_option trace.Tactic.librarySearch true
set_option trace.Tactic.librarySearch.lemmas true

[Floris van Doorn]

You have to unfold semireducible definitions to apply the lemma MulEquiv.bijective. I forgot if library_search tries to unify up to semireducible defeq? And even if it does, maybe the discrimination tree keys are not computed up to semireducible defeq?

[Floris van Doorn]

    intro G H inst₁ inst₂ ϕ
    simp
    exact?

does work

[Siddhartha Gadgil]

Wow. Thanks.