Exact? produces a non-accepted term

Stream: lean4

[Luna]

While doing an exercise in MIL, I attempted to use by exact? and it produced exact exists_rep 1 which fails with the following message:

failed to synthesize
OfNat (Quotient (Submodule.quotientRel I)) 1
numerals are polymorphic in Lean, but the numeral 1 cannot be used in a context where the expected type is
Quotient (Submodule.quotientRel I)
due to the absence of the instance above

From my understanding of the exact? tactic, I believe this should be a bug. The simplified code (though it still contains mathlib) is below:

import Mathlib.RingTheory.Ideal.Quotient.Basic

example {R : Type*} [Ring R] {I : Ideal R} [Ideal.IsTwoSided I] : ∃ (a : R), (Ideal.Quotient.mk I) a = 1 := by
  exact?  -- exact exists_rep 1

[Ruben Van de Velde]

That's a funny one. Unfortunately the process of turning the expression exact? finds into a lean code string (pretty printing) is not foolproof

[Damiano Testa]

In this case, replacing 1 by _ works.