Skip to content

Commit

Permalink
fixing the build
Browse files Browse the repository at this point in the history
  • Loading branch information
joelriou committed Aug 18, 2024
1 parent ae4bc09 commit b3c0c79
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion Mathlib/CategoryTheory/Limits/Fubini.lean
Original file line number Diff line number Diff line change
Expand Up @@ -513,7 +513,6 @@ theorem limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π {j} {k} :
dsimp [Equivalence.counit]
rw [← prod_id, G.map_id]
simp
sorry

-- Porting note: Added type annotation `limit (_ ⋙ lim) ⟶ _`
@[simp]
Expand Down

0 comments on commit b3c0c79

Please sign in to comment.