unapplied lambda in coercion

Stream: lean4

[Kevin Buzzard]

Does this matter? I just noticed it in the port. The LHS can be beta-reduced.

import Mathlib.CategoryTheory.Bicategory.Basic

namespace CategoryTheory

open Category Bicategory

open Bicategory

universe w₁ w₂ w₃ v₁ v₂ v₃ u₁ u₂ u₃

section

variable {B : Type u₁} [Quiver.{v₁ + 1} B] [∀ a b : B, Quiver.{w₁ + 1} (a ⟶ b)]

variable {C : Type u₂} [Quiver.{v₂ + 1} C] [∀ a b : C, Quiver.{w₂ + 1} (a ⟶ b)]

variable {D : Type u₃} [Quiver.{v₃ + 1} D] [∀ a b : D, Quiver.{w₃ + 1} (a ⟶ b)]

structure PrelaxFunctor (B : Type u₁) [Quiver.{v₁ + 1} B] [∀ a b : B, Quiver.{w₁ + 1} (a ⟶ b)]
  (C : Type u₂) [Quiver.{v₂ + 1} C] [∀ a b : C, Quiver.{w₂ + 1} (a ⟶ b)] extends
  Prefunctor B C where
  zipWith {a b : B} {f g : a ⟶ b} : (f ⟶ g) → (map f ⟶ map g)

/-- The prefunctor between the underlying quivers. -/
add_decl_doc PrelaxFunctor.toPrefunctor

namespace PrelaxFunctor

attribute [coe] CategoryTheory.PrelaxFunctor.toPrefunctor

instance hasCoeToPrefunctor : Coe (PrelaxFunctor B C) (Prefunctor B C) :=
  ⟨toPrefunctor⟩

variable (F : PrelaxFunctor B C)

-- set_option pp.all true
@[simp]
theorem to_prefunctor_obj : (F : Prefunctor B C).obj = F.obj :=
  -- ⊢ (↑F).obj = (↑F).obj
  rfl
/-
But LHS has two unapplied lambdas

⊢ @Eq.{max (u₁ + 1) (u₂ + 1)} (B → C)
  (@Prefunctor.obj.{v₁ + 1, v₂ + 1, u₁, u₂} B inst✝⁵ C inst✝³
    (@CategoryTheory.PrelaxFunctor.toPrefunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B inst✝⁵
      (fun (a b : B) => (fun (a b : B) => inst✝⁴ a b) a b) C inst✝³ (fun (a b : C) => (fun (a b : C) => inst✝² a b) a b)
      F))
  (@Prefunctor.obj.{v₁ + 1, v₂ + 1, u₁, u₂} B inst✝⁵ C inst✝³
    (@CategoryTheory.PrelaxFunctor.toPrefunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B inst✝⁵ (fun (a b : B) => inst✝⁴ a b) C inst✝³
      (fun (a b : C) => inst✝² a b) F))
-/

end PrelaxFunctor

[Chris Hughes]

The difference is only in the instance arguments right? So I think it should be fine, since those are more aggressively unfolded and checked for defeq when rewriting