fix

Author: kim-em

Mathlib/AlgebraicGeometry/Morphisms/FlatRank.lean

@@ -266,6 +266,7 @@ lemma Scheme.Hom.finrank_eq_one_of_isIso (f : X ⟶ Y) [IsIso f] : finrank f = 1
   · exact RingHom.Finite.id R
   · exact RingHom.Flat.id ↑R
 
+set_option backward.defeqAttrib.useBackward true in
 /-- A finite flat locally finitely presented morphism is an isomorphism if and only if
 its rank is constant equal to `1`. -/
 nonrec lemma Scheme.Hom.isIso_iff_finrank_eq : IsIso f ↔ finrank f = 1 := by