solve_by_elim going in circles

Stream: mathlib4

[Patrick Massot]

I don't know whether this qualifies as a bug, but I've been surprised by the following behavior of solve_by_elim @Scott Morrison

import Mathlib.Tactic.SolveByElim

def injective {α β : Type _} (f : α → β) := ∀ (x y : α), f x = f y → x = y

/- Hand-written proof -/
example {α β γ} {f : α → β} {g : β → γ} (hf : injective f) (hg : injective g) :
  injective (g ∘ f) :=
fun x y h ↦ hf x y (hg (f x) (f y) h)

/- solve_by_elim generates a proof that contains the hand-written proof as a strict subterm -/
example {α β γ} {f : α → β} {g : β → γ} (hf : injective f) (hg : injective g) :
  injective (g ∘ f) :=
by
  intros x y h
  show_term solve_by_elim
  --  exact hf x y (congrArg f (hf x y (hg (f x) (f y) h)))

Here solve_by_elim uses assumptions hf and hg to prove x = y (which was the end goal) then deduces f x = f y using congrArg, and then uses hf again to re-derive the end goal.

[Alex J. Best]

This is as library lemmas are always applied before context lemmas in solve by elim it seems.
I'm not sure the effects of reversing this but #5809 will at least fix your proof, lets see if mathlib builds, and if there is a non-negligable effect on bench

[Alex J. Best]

As is maybe to be expected, the benchmark results dont show a clear gain or less, they seem to imply one file got "significantly" faster and two slower, but there doesn't seem to be too much in it, but a net win in total instruction sizes.

[Patrick Massot]

I'm not sure I understand the link with my question but thanks for investigating!