Proof breaks when previous placeholder is filled

Stream: new members

[Michał Mrugała]

Hi, I am working on proving the following result:

def pushoutCoconeEquivBinaryCofan : PushoutCocone f g ≌ BinaryCofan (Under.mk f) (Under.mk g) where
  functor := {
    obj c := BinaryCofan.mk (Under.homMk (U := Under.mk f) c.inl rfl)
        (Under.homMk (U := Under.mk g) (V := Under.mk (f ≫ c.inl)) c.inr c.condition.symm)
    map {c1 c2} a := {
      hom := Under.homMk a.hom
      w := by
        rintro ⟨(_|_)⟩
        repeat
          ext
          exact a.w _
    }
  }
  inverse := {
    obj c := PushoutCocone.mk c.inl.right c.inr.right (c.inl.w.symm.trans c.inr.w)
    map {c1 c2} a := {
      hom := a.hom.right
      w := by rintro (_|_|_) <;> simp [← Under.comp_right]
    }
  }
  unitIso := {
    hom := {
      app c := c.eta.hom
      naturality {c1 c2} a := _ -- by ext; simp -- removable
    }
    inv := {
      app c := c.eta.inv
      naturality {c1 c2} a := by ext; simp
    }
    hom_inv_id := _
    inv_hom_id := _
  }
  counitIso := _
  functor_unitIso_comp := _

As shown the proof of naturality of inv seems to work. However, if I fill in the proof of naturality of hom or remove that field (since aesop does it) the simp call times out. How can I approach troubleshooting this?

[Aaron Liu]

This may be an instance of #lean4 > dsimp simplifies proofs, which is slow .

[Aaron Liu]

This may be an instance of #lean4 > dsimp simplifies proofs, which is slow .

[Aaron Liu]

For troubleshooting options, you can try set_option trace.Meta.Tactic.simp true

[Michał Mrugała]

On a quick skim it seems likely. dsimp also times out under the same circumstances.