Rw makes 2 goals

Stream: lean4

[Marcus Rossel]

In the following proof ...

def invertible (f : α → β) : Prop :=
  ∃ (g : β → α), (g ∘ f = id) ∧ (f ∘ g = id)

theorem invertibleIffBijective {f : α → β} : invertible f ↔ Function.bijective f := by
  simp only [Function.bijective, Function.injective, Function.surjective, invertible]
  split
  focus
    intro h
    split
    focus
      intro a₁ a₂ he
      match h with
      | ⟨g, ⟨h, _⟩⟩ =>
        have h₁ : id a₁ = a₁ := id.def a₁
        have h₂ : id a₂ = a₂ := id.def a₂
        rw [←h] at h₁ h₂
        simp only [Function.comp] at h₁ h₂
        rw [he] at h₁
        rw [h₁] at h₂
        exact h₂
    focus
      intro b
      match h with
      | ⟨g, ⟨_, h⟩⟩ =>
        exists (g b)
        rw [←(id.def b)] -- HERE
  focus
     sorry

... on the line with the HERE, the rewrite produces two identical goals. It goes from ...

α : Sort u_1
β : Sort u_2
f : α → β
h✝ : ∃ (g : β → α), g ∘ f = id ∧ f ∘ g = id
b : β
g : β → α
x✝ : g ∘ f = id
h : f ∘ g = id
⊢ f (g b) = b

... to ...

α : Sort u_1
β : Sort u_2
f : α → β
h✝ : ∃ (g : β → α), g ∘ f = id ∧ f ∘ g = id
b : β
g : β → α
x✝ : g ∘ f = id
h : f ∘ g = id
⊢ f (g (id b)) = id b

α : Sort u_1
β : Sort u_2
f : α → β
h✝ : ∃ (g : β → α), g ∘ f = id ∧ f ∘ g = id
b : β
g : β → α
x✝ : g ∘ f = id
h : f ∘ g = id
⊢ f (g (id b)) = id b

Is this intended? And if so, why is this happening?