Minimization request

Stream: general

[Heather Macbeth]

If anyone wants a fun (?) weekend project: it would be great to have a minimization of the following error, produced on branch#bump/v4.15.0 but not on mathlib master. See #nightly-testing > #19314 adaptations for nightly-2024-11-20 for previous discussion.

import Mathlib.Data.NNReal.Basic
open NNReal

-- "tactic 'apply' failed, failed to assign synthesized instance"
example {n : ℕ} {p : ℝ≥0} : (↑n)⁻¹ ≤ p⁻¹ := by
  with_reducible_and_instances apply inv_anti₀
  sorry
  sorry

My guess is that it is caused by lean4#6053, but we'll see!

[Heather Macbeth]

I just spent half an hour on this, and minimized about halfway, down to

import Mathlib.Algebra.Order.Field.Defs
import Mathlib.Algebra.Order.Group.InjSurj
import Mathlib.Algebra.Ring.InjSurj

Posting at https://gist.github.com/hrmacbeth/9befbcd157e873314572bd3909ba9e63 in case anyone has time to pick up from here.

[Heather Macbeth]

De-mathlib'd and filed: lean4#6266.