std4#120 `ext?` and `ext!?`

Stream: PR reviews

[Jon Eugster]

std4#120 implements two additions to ext, which I believe are both useful for debugging ext. The PR resides in Std because that's where ext lies but a review by any mathlib maintainer/contributor would be highly welcomed!

• ext? prints a "Try this:" suggesting which ext-lemmas have been used.
• ext!? forces ext to ignore the DiscTree and tries to apply all ext-lemmas. It prints the same "Try this:" alongside with a warning about any ext-lemmas ext!? applied that ext couldn't.

Here's a preview, which can be found in test/ext.lean:

theorem test (c₁ c₂ : C) (h : c₁.a = c₂.a) (h' :  c₁.b = c₂.b )
    (h'' :  c₁.c = c₂.c ) : c₁ = c₂ := by
  ext?
  -- Try this:
  -- · apply extCtoB
  --   intros
  --   sorry
  --   sorry
  --   apply extBtoA
  --   sorry
  --   sorry
  repeat admit

def D := C

theorem test₂ (c₁ c₂ : D) (h : c₁.a = c₂.a) (h' :  c₁.b = c₂.b )
    (h'' :  c₁.c = c₂.c ) : c₁ = c₂ := by
  ext!?
  -- Try this: [yada yada]
  --
  -- Warning: `extCtoB` applied, which is written in terms of type `C`.
  -- If you want `ext` to find it, please make a copy of this
  -- lemma in terms of type `D`.
  repeat admit

[Scott Morrison]

Left some more comments.