chore (Int.Cast.Defs): delete last line (#6710)

The last line is `open Nat` which came from an incomplete deletion of content from this fild. We delete the line.
leanprover-community · Aug 21, 2023 · a2e5641 · a2e5641
1 parent 20d6b8e
commit a2e5641
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/Mathlib/Data/Int/Cast/Defs.lean b/Mathlib/Data/Int/Cast/Defs.lean
@@ -64,4 +64,3 @@ class AddCommGroupWithOne (R : Type u)
 #align add_comm_group_with_one.to_add_group_with_one AddCommGroupWithOne.toAddGroupWithOne
 #align add_comm_group_with_one.to_add_comm_monoid_with_one AddCommGroupWithOne.toAddCommMonoidWithOne
 
-open Nat