Skip to content

Commit 43dc3a9

Browse files
committed
chore(AlgebraicGeometry): remove use of erw in ι_glueMorphisms (leanprover-community#32633)
1 parent 8d2e6ec commit 43dc3a9

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Mathlib/AlgebraicGeometry/Gluing.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -453,7 +453,7 @@ theorem ι_glueMorphisms (𝒰 : OpenCover.{v} X) {Y : Scheme} (f : ∀ x, 𝒰.
453453
PreZeroHypercover.pullback₁_X, ulift_X, ulift_f, PreZeroHypercover.pullback₁_f]
454454
simp_rw [pullback.condition_assoc, ← ulift_f, ← ι_fromGlued, Category.assoc, glueMorphisms,
455455
IsIso.hom_inv_id_assoc, ulift_f, hf]
456-
erw [Multicoequalizer.π_desc]
456+
simp [CategoryTheory.GlueData.ι]
457457

458458
end Cover
459459

0 commit comments

Comments
 (0)