DTT hell: How to debug when equal things aren't equal?

Stream: lean4

[Joey Eremondi]

I'm wondering a few things:

1. How do I debug a case where two things should be equal, but aren't. I've got a situation where two things in the goal are exactly equal except for parts that are in Prop, so I'm not sure why rfl isn't working on them.
2. Is there a way to avoid DTT hell when dealing with over-categories? I'm trying to prove a lemma about Grothendieck Topologies on over-categories. Is there a better solution than pattern-matching when going between properties of arrows in the base and over-categories?

Here's a working example, maybe not too minimal but at least self-contained. It's trying to formalize part of C2.2.17 from Sketches of an Elephant. At the end I get an error trying to unify (hₖs (CommaMorphism.mk θ rt) (_ : R.arrows (CommaMorphism.mk θ rt))).left and (hₖs (CommaMorphism.mk θ rt) inR).left which are (as far as I can see) equal except for Prop-valued proofs.

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Functor.Basic
import Mathlib.CategoryTheory.Comma.Over
import Mathlib.CategoryTheory.Sites.Over
import Mathlib.CategoryTheory.Sites.Sieves

open CategoryTheory
variable {C : Type u} [cat : Category.{v'}  C]


def baseFamily {U V W : C} {f : V ⟶ U} {g : W ⟶ U}
  (R : Sieve (Over.mk f))
  (hₖs : Presieve.FamilyOfElements (yoneda.obj (Over.mk g)) R.arrows)
  : Presieve.FamilyOfElements (C := C)
      (yoneda.obj W)
      (Sieve.overEquiv (Over.mk f) R).arrows
    := by
      intros k hk in_hₖs
      let inR := (Sieve.overEquiv_iff R hk).mp in_hₖs
      let sliceArrow := hₖs _ inR
      apply sliceArrow.left


def baseArrowsIff {U V : C} {f : V ⟶ U}
  (R : Sieve (Over.mk f : Over U))
  {Y : Over U}
  (θ : Y ⟶ Over.mk f)
  : R.arrows θ ↔ (Sieve.overEquiv (Over.mk f) R) θ.left := by
    have unfld :  R.arrows = (Sieve.overEquiv (Over.mk f)).symm (Sieve.overEquiv (Over.mk f) R) := by aesop
    rw [unfld]
    apply Sieve.overEquiv_symm_iff

def overPreserveAmalg {U V W : C}  {g : W ⟶ U} {h : V ⟶ W}
(R : Sieve (Over.mk (h ≫ g)))
{hₖs : Presieve.FamilyOfElements (yoneda.obj (Over.mk g)) R.arrows}
    (isAmalg : Presieve.FamilyOfElements.IsAmalgamation (baseFamily R hₖs) h )
    : Presieve.FamilyOfElements.IsAmalgamation hₖs (Over.homMk h) := by
    simp [Presieve.FamilyOfElements.IsAmalgamation, baseFamily] at isAmalg
    simp [Presieve.FamilyOfElements.IsAmalgamation, baseFamily]
    intros Y θ inR
    simp_all [Over.homMk, CostructuredArrow.homMk]
    let ⟨θ, rt, eq⟩ := θ
    let inRbase := (baseArrowsIff R _).mp inR
    let lem := isAmalg θ inRbase
    apply Over.OverMorphism.ext
    simp
    apply Eq.trans lem
    simp [Presieve.FamilyOfElements] at hₖs
    have eqrt {x : _} :  x = rt := by aesop_cat
    have eqinR {x : _} :  x = inR := by aesop_cat
    simp [eqrt, eqinR]
    apply Eq.refl

[Kyle Miller]

One trick is to use convert in place of exact or congr! in place of rfl. These try to tear through expressions, reducing the issue to the parts that aren't obviously defeq. (They can also sometimes prove equalities that aren't true by defeq.)

[Andrew Yang]

In this case, the structure morphism of Y/U are different on the two sides. It is θ ≫ h ≫ g on the LHS and Y.hom on the RHS.