last fix

leanprover-community · Feb 3, 2023 · c5c1fcb · c5c1fcb
1 parent 705b2ec
commit c5c1fcb
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/Order/SuccPred/LinearLocallyFinite.lean b/Mathlib/Order/SuccPred/LinearLocallyFinite.lean
@@ -374,7 +374,7 @@ variable [SuccOrder ι] [PredOrder ι] [IsSuccArchimedean ι]
 noncomputable def orderIsoRangeToZOfLinearSuccPredArch [hι : Nonempty ι] :
     ι ≃o Set.range (toZ hι.some) where
   toEquiv := Equiv.ofInjective _ injective_toZ
-  map_rel_iff' := toZ_le_iff
+  map_rel_iff' := by intro i j ; exact toZ_le_iff i j
 set_option linter.uppercaseLean3 false in
 #align order_iso_range_to_Z_of_linear_succ_pred_arch orderIsoRangeToZOfLinearSuccPredArch
 
@@ -405,7 +405,7 @@ noncomputable def orderIsoIntOfLinearSuccPredArch [NoMaxOrder ι] [NoMinOrder ι
     · simp_rw [if_neg (not_le.mpr hn)]
       rw [toZ_iterate_pred]
       simp only [hn.le, Int.toNat_of_nonneg, Right.nonneg_neg_iff, neg_neg]
-  map_rel_iff' := toZ_le_iff
+  map_rel_iff' := by intro i j ; exact toZ_le_iff i j
 #align order_iso_int_of_linear_succ_pred_arch orderIsoIntOfLinearSuccPredArch
 
 /-- If the order has a bot but no top, `to_Z` defines an `order_iso` between `ι` and `ℕ`. -/