!4#2994

Stream: mathlib4

[Jeremy Tan]

!4#2994 I've managed to remove all deterministic timeouts but there are still several places where surprisingly Lean can't close goals, please help

[Jeremy Tan]

Another problem lies at L352:

theorem inv_apply {R : Type u} [CommMonoidWithZero R] (χ : MulChar R R') (a : R) :
    χ⁻¹ a = χ (Ring.inverse a) := by
  by_cases ha : IsUnit a
  · rw [inv_apply_eq_inv]
    have h := IsUnit.map χ ha
    apply_fun (χ a * ·) using IsUnit.mul_right_injective h -- here
    rw [Ring.mul_inverse_cancel _ h, ← map_mul, Ring.mul_inverse_cancel _ ha, MulChar.map_one]
  · revert ha
    nontriviality R
    intro ha
    -- `nontriviality R` by itself doesn't do it
    rw [map_nonunit _ ha, Ring.inverse_non_unit a ha, MulChar.map_zero χ]

Knowing that apply_fun was recently augmented, how can it not see that the given function can be applied? (And how do I get h to appear to Lean for the using part?)

[Jeremy Tan]

I've taken it as far as I can, though