Replacing `sorry` by proof changing required indentation

Stream: lean4

[Joseph Myers]

In #29418 I have an example of code that with sorry can be expressed as

  · convert (Finset.orderEmbOfFin_zero _ _).symm
    · sorry
    · omega

but if I try to replace that sorry with a particular (valid) proof

  · convert (Finset.orderEmbOfFin_zero _ _).symm
    · rw [eq_comm]
      convert Finset.min'_pair i j
    · omega

then this doesn't work and instead Lean expects the indentation to be

  · convert (Finset.orderEmbOfFin_zero _ _).symm
    · rw [eq_comm]
      · convert Finset.min'_pair i j
      · omega

which is logically wrong since it's definitely the convert that introduces the second goal that omega resolves, not the rw. Can someone explain what's going on here? (The proof may get replaced by a simpler one that avoids this issue, but it can be seen in the original commit of this PR.)

[Robin Arnez]

Might be lean4#10172 again

[Ruben Van de Velde]

Sounds like it, that's annoying

[Kyle Miller]

PR fixing 10172: lean4#10306