bicategory_coherence — Mathlib

Lean4
/-- Coherence tactic for bicategories. -/
def bicategory_coherence (g : MVarId) : TermElabM Unit :=
  g.withContext do
    withOptions (fun opts => synthInstance.maxSize.set opts (max 256 (synthInstance.maxSize.get opts))) do
        let thms :=
          [``BicategoricalCoherence.iso, ``Iso.trans, ``Iso.symm, ``Iso.refl, ``Bicategory.whiskerRightIso,
                ``Bicategory.whiskerLeftIso].foldl
            (·.addDeclToUnfoldCore ·) { }
        let (ty, _) ← dsimp (← g.getType) (← Simp.mkContext (simpTheorems := #[thms]))
        let some (_, lhs, rhs) := (← whnfR ty).eq? |
          exception g "Not an equation of morphisms."
        let lift_lhs ← mkLiftMap₂LiftExpr lhs
        let lift_rhs ← mkLiftMap₂LiftExpr rhs
        let g₁ ← g.change (← mkEq lift_lhs lift_rhs)
        let [g₂] ← g₁.applyConst ``congrArg |
          exception g "congrArg failed in coherence"
        let [] ← g₂.applyConst ``Subsingleton.elim |
          exception g "This shouldn't happen; Subsingleton.elim does not create goals."
Похожие утверждения