curious difference between `exact rfl` and `apply rfl`

Stream: general

[Scott Morrison]

I would have naively expected that exact rfl and apply rfl always had identical behaviour. Curiously they don't:

example {i : ℕ} (n : ℕ) (hi : 2 ≤ i) :
  i + (n + 1).factorial < (i + n) * (i + n).factorial + (i + n).factorial :=
begin
  apply add_lt_add_of_lt_of_le,
  apply has_le.le.trans_lt,
  apply nat.le.intro,
  apply rfl,
  -- now there are 3 goals remaining
end

while

example {i : ℕ} (n : ℕ) (hi : 2 ≤ i) :
  i + (n + 1).factorial < (i + n) * (i + n).factorial + (i + n).factorial :=
begin
  apply add_lt_add_of_lt_of_le,
  apply has_le.le.trans_lt,
  apply nat.le.intro,
  exact rfl,
  -- now there are 4 goals remaining
end

After the exact rfl, the first two goals are actually duplicates (i.e. solving either solves both).

[Eric Wieser]

Does skip also collapse the two?

[Eric Wieser]

Or any other non-solving step

[Scott Morrison]

No, no effect.

[Mario Carneiro]

The two goals after the exact rfl are indeed duplicates: they are literally the same mvar, not just instantiated to a common mvar

[Eric Wieser]

This came up a month or two ago in some other tactic, didn't it?

[Mario Carneiro]

I believe this is because the unification of rfl : i + ?m_1 = ?m_2 results in assigning ?m_2 and elaborating @rfl (i + ?m_1), which causes ?m_1 to be kicked back as a subgoal; since exact runs on a focused state it doesn't realize that ?m_1 is already a goal

[Mario Carneiro]

I don't think I have seen this particular issue before, although I will remark that apply and exact often differ in the details, so I don't have the same "naive expectation" as Scott professes

[Kevin Buzzard]

convert could also occasionally leave two copies of the same mvar as goals but probably for different reasons