Nontransitivity of DefEq

Stream: lean4

[Chris Hughes]

I came across this nontransitivity of DefEq today that isn't anything to do with Prop or Quotients. rfl cannot prove the following lemma.

example {α : Type} (f g : α → Unit) : f = g :=
  calc f
    = fun x => f x := rfl
  _ = g := rfl

[Reid Barton]

This is supposed to be by eta for functions + eta for Unit?

[Chris Hughes]

Yes