Zulip Chat Archive

Stream: lean4

Topic: Rw makes 2 goals


Marcus Rossel (Aug 03 2021 at 13:07):

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?


Last updated: Dec 20 2023 at 11:08 UTC