chore: Reduce imports to Data.Finset.Image (#12832)

Mathlib/Algebra/Group/Nat.lean

@@ -26,7 +26,7 @@ namespace Nat
 
 /-! ### Instances -/
 
-instance instAddCommMonoid : AddCommMonoid ℕ where
+instance instAddCancelCommMonoid : AddCancelCommMonoid ℕ where
   add := Nat.add
   add_assoc := Nat.add_assoc
   zero := Nat.zero
@@ -36,6 +36,7 @@ instance instAddCommMonoid : AddCommMonoid ℕ where
   nsmul m n := m * n
   nsmul_zero := Nat.zero_mul
   nsmul_succ := succ_mul
+  add_left_cancel _ _ _ := Nat.add_left_cancel
 
 instance instCommMonoid : CommMonoid ℕ where
   mul := Nat.mul
@@ -54,6 +55,7 @@ instance instCommMonoid : CommMonoid ℕ where
 These also prevent non-computable instances being used to construct these instances non-computably.
 -/
 
+instance instAddCommMonoid    : AddCommMonoid ℕ    := by infer_instance
 instance instAddMonoid        : AddMonoid ℕ        := by infer_instance
 instance instMonoid           : Monoid ℕ           := by infer_instance
 instance instCommSemigroup    : CommSemigroup ℕ    := by infer_instance

Mathlib/Data/Finset/Card.lean

@@ -26,6 +26,12 @@ This defines the cardinality of a `Finset` and provides induction principles for
 * `Finset.Nonempty.strong_induction`
 -/
 
+-- TODO: After #12845,
+-- assert_not_exists Ring
+-- TODO: After #11855,
+-- assert_not_exists MonoidWithZero
+-- TODO: After a lot more work,
+-- assert_not_exists OrderedCommMonoid
 
 open Function Multiset Nat
 
@@ -68,7 +74,7 @@ theorem card_mono : Monotone (@card α) := by apply card_le_card
 
 @[simp] lemma card_eq_zero : s.card = 0 ↔ s = ∅ := card_eq_zero.trans val_eq_zero
 lemma card_ne_zero : s.card ≠ 0 ↔ s.Nonempty := card_eq_zero.ne.trans nonempty_iff_ne_empty.symm
-lemma card_pos : 0 < s.card ↔ s.Nonempty := pos_iff_ne_zero.trans card_ne_zero
+lemma card_pos : 0 < s.card ↔ s.Nonempty := Nat.pos_iff_ne_zero.trans card_ne_zero
 #align finset.card_eq_zero Finset.card_eq_zero
 #align finset.card_pos Finset.card_pos
 
@@ -281,7 +287,7 @@ theorem card_image_of_injective [DecidableEq β] (s : Finset α) (H : Injective
 
 theorem fiber_card_ne_zero_iff_mem_image (s : Finset α) (f : α → β) [DecidableEq β] (y : β) :
     (s.filter fun x => f x = y).card ≠ 0 ↔ y ∈ s.image f := by
-  rw [← pos_iff_ne_zero, card_pos, fiber_nonempty_iff_mem_image]
+  rw [← Nat.pos_iff_ne_zero, card_pos, fiber_nonempty_iff_mem_image]
 #align finset.fiber_card_ne_zero_iff_mem_image Finset.fiber_card_ne_zero_iff_mem_image
 
 lemma card_filter_le_iff (s : Finset α) (P : α → Prop) [DecidablePred P] (n : ℕ) :
@@ -492,7 +498,7 @@ lemma cast_card_union [AddGroupWithOne R] :
 
 theorem card_sdiff (h : s ⊆ t) : card (t \ s) = t.card - s.card := by
   suffices card (t \ s) = card (t \ s ∪ s) - s.card by rwa [sdiff_union_of_subset h] at this
-  rw [card_union_of_disjoint sdiff_disjoint, add_tsub_cancel_right]
+  rw [card_union_of_disjoint sdiff_disjoint, Nat.add_sub_cancel_right]
 #align finset.card_sdiff Finset.card_sdiff
 
 lemma cast_card_sdiff [AddGroupWithOne R] (h : s ⊆ t) : ((t \ s).card : R) = t.card - s.card := by
@@ -505,13 +511,13 @@ theorem card_sdiff_add_card_eq_card {s t : Finset α} (h : s ⊆ t) : card (t \
 theorem le_card_sdiff (s t : Finset α) : t.card - s.card ≤ card (t \ s) :=
   calc
     card t - card s ≤ card t - card (s ∩ t) :=
-      tsub_le_tsub_left (card_le_card (inter_subset_left s t)) _
+      Nat.sub_le_sub_left (card_le_card (inter_subset_left s t)) _
     _ = card (t \ (s ∩ t)) := (card_sdiff (inter_subset_right s t)).symm
     _ ≤ card (t \ s) := by rw [sdiff_inter_self_right t s]
 #align finset.le_card_sdiff Finset.le_card_sdiff
 
 theorem card_le_card_sdiff_add_card : s.card ≤ (s \ t).card + t.card :=
-  tsub_le_iff_right.1 <| le_card_sdiff _ _
+  Nat.sub_le_iff_le_add.1 <| le_card_sdiff _ _
 #align finset.card_le_card_sdiff_add_card Finset.card_le_card_sdiff_add_card
 
 theorem card_sdiff_add_card : (s \ t).card + t.card = (s ∪ t).card := by
@@ -550,9 +556,7 @@ theorem exists_intermediate_set {A B : Finset α} (i : ℕ) (h₁ : i + card B 
     clear h₁
     induction' k with k ih generalizing A
     · exact ⟨A, h₂, Subset.refl _, h.symm⟩
-    obtain ⟨a, ha⟩ : (A \ B).Nonempty := by
-      rw [← card_pos, card_sdiff h₂, ← h, Nat.add_right_comm, add_tsub_cancel_right, Nat.add_succ]
-      apply Nat.succ_pos
+    obtain ⟨a, ha⟩ : (A \ B).Nonempty := by rw [← card_pos, card_sdiff h₂]; omega
     have z : i + card B + k = card (erase A a) := by
       rw [card_erase_of_mem (mem_sdiff.1 ha).1, ← h,
         Nat.add_sub_assoc (Nat.one_le_iff_ne_zero.mpr k.succ_ne_zero), ← pred_eq_sub_one,
@@ -582,8 +586,8 @@ theorem exists_subset_or_subset_of_two_mul_lt_card [DecidableEq α] {X Y : Finse
   have h₁ : (X ∩ (Y \ X)).card = 0 := Finset.card_eq_zero.mpr (Finset.inter_sdiff_self X Y)
   have h₂ : (X ∪ Y).card = X.card + (Y \ X).card := by
     rw [← card_union_add_card_inter X (Y \ X), Finset.union_sdiff_self_eq_union, h₁, add_zero]
-  rw [h₂, two_mul] at hXY
-  rcases lt_or_lt_of_add_lt_add hXY with (h | h)
+  rw [h₂, Nat.two_mul] at hXY
+  obtain h | h : n < X.card ∨ n < (Y \ X).card := by contrapose! hXY; omega
   · exact ⟨X, h, Or.inl (Finset.Subset.refl X)⟩
   · exact ⟨Y \ X, h, Or.inr (Finset.sdiff_subset Y X)⟩
 #align finset.exists_subset_or_subset_of_two_mul_lt_card Finset.exists_subset_or_subset_of_two_mul_lt_card
@@ -607,7 +611,7 @@ theorem exists_eq_insert_iff [DecidableEq α] {s t : Finset α} :
     exact ⟨subset_insert _ _, (card_insert_of_not_mem ha).symm⟩
   · rintro ⟨hst, h⟩
     obtain ⟨a, ha⟩ : ∃ a, t \ s = {a} :=
-      card_eq_one.1 (by rw [card_sdiff hst, ← h, add_tsub_cancel_left])
+      card_eq_one.1 (by rw [card_sdiff hst, ← h, Nat.add_sub_cancel_left])
     refine'
       ⟨a, fun hs => (_ : a ∉ {a}) <| mem_singleton_self _, by
         rw [insert_eq, ← ha, sdiff_union_of_subset hst]⟩
@@ -697,7 +701,7 @@ theorem card_eq_succ : s.card = n + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s 
   ⟨fun h =>
     let ⟨a, has⟩ := card_pos.mp (h.symm ▸ Nat.zero_lt_succ _ : 0 < s.card)
     ⟨a, s.erase a, s.not_mem_erase a, insert_erase has, by
-      simp only [h, card_erase_of_mem has, add_tsub_cancel_right]⟩,
+      simp only [h, card_erase_of_mem has, Nat.add_sub_cancel_right]⟩,
     fun ⟨a, t, hat, s_eq, n_eq⟩ => s_eq ▸ n_eq ▸ card_insert_of_not_mem hat⟩
 #align finset.card_eq_succ Finset.card_eq_succ
 
@@ -812,7 +816,8 @@ def strongDownwardInduction {p : Finset α → Sort*} {n : ℕ}
     ∀ s : Finset α, s.card ≤ n → p s
   | s =>
     H s fun {t} ht h =>
-      have : n - t.card < n - s.card := (tsub_lt_tsub_iff_left_of_le ht).2 (Finset.card_lt_card h)
+      have := Finset.card_lt_card h
+      have : n - t.card < n - s.card := by omega
       strongDownwardInduction H t ht
   termination_by s => n - s.card
 #align finset.strong_downward_induction Finset.strongDownwardInduction

Mathlib/Data/Finset/Fold.lean

@@ -3,6 +3,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import Mathlib.Algebra.Order.Monoid.MinMax
 import Mathlib.Algebra.Order.Monoid.WithTop
 import Mathlib.Data.Finset.Image
 import Mathlib.Data.Multiset.Fold

Mathlib/Data/Finset/Image.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Minchao Wu, Mario Carneiro
 -/
 import Mathlib.Algebra.Group.Embedding
-import Mathlib.Algebra.Order.Ring.Nat
-import Mathlib.Algebra.Order.Ring.Int
 import Mathlib.Data.Fin.Basic
 import Mathlib.Data.Finset.Union
 
@@ -29,8 +27,15 @@ choosing between `insert` and `Finset.cons`, or between `Finset.union` and `Fins
 * `Finset.subtype`: `s.subtype p` is the finset of `Subtype p` whose elements belong to `s`.
 * `Finset.fin`:`s.fin n` is the finset of all elements of `s` less than `n`.
 
+## TODO
+
+Move the material about `Finset.range` so that the `Mathlib.Algebra.Group.Embedding` import can be
+removed.
 -/
 
+-- TODO
+-- assert_not_exists OrderedCommMonoid
+-- assert_not_exists Ring
 
 variable {α β γ : Type*}
 
@@ -290,23 +295,11 @@ theorem attach_map_val {s : Finset α} : s.attach.map (Embedding.subtype _) = s
 #align finset.attach_map_val Finset.attach_map_val
 
 theorem disjoint_range_addLeftEmbedding (a b : ℕ) :
-    Disjoint (range a) (map (addLeftEmbedding a) (range b)) := by
-  refine' disjoint_iff_inf_le.mpr _
-  intro k hk
-  simp only [exists_prop, mem_range, inf_eq_inter, mem_map, addLeftEmbedding, mem_inter]
-    at hk
-  obtain ⟨a, _, ha⟩ := hk.2
-  simpa [← ha] using hk.1
+    Disjoint (range a) (map (addLeftEmbedding a) (range b)) := by simp [disjoint_left]; omega
 #align finset.disjoint_range_add_left_embedding Finset.disjoint_range_addLeftEmbedding
 
 theorem disjoint_range_addRightEmbedding (a b : ℕ) :
-    Disjoint (range a) (map (addRightEmbedding a) (range b)) := by
-  refine' disjoint_iff_inf_le.mpr _
-  intro k hk
-  simp only [exists_prop, mem_range, inf_eq_inter, mem_map, addRightEmbedding, mem_inter]
-    at hk
-  obtain ⟨a, _, ha⟩ := hk.2
-  simpa [← ha] using hk.1
+    Disjoint (range a) (map (addRightEmbedding a) (range b)) := by simp [disjoint_left]; omega
 #align finset.disjoint_range_add_right_embedding Finset.disjoint_range_addRightEmbedding
 
 theorem map_disjiUnion {f : α ↪ β} {s : Finset α} {t : β → Finset γ} {h} :

Mathlib/Data/Finset/Lattice.lean

@@ -3,6 +3,9 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import Mathlib.Algebra.GroupPower.CovariantClass
+import Mathlib.Algebra.Order.Group.Nat
+import Mathlib.Algebra.Order.Ring.Defs
 import Mathlib.Data.Finset.Fold
 import Mathlib.Data.Finset.Option
 import Mathlib.Data.Finset.Pi
@@ -1597,8 +1600,7 @@ theorem min'_lt_max' {i j} (H1 : i ∈ s) (H2 : j ∈ s) (H3 : i ≠ j) :
 `min'_lt_max'` which is sometimes more convenient.
 -/
 theorem min'_lt_max'_of_card (h₂ : 1 < card s) :
-    s.min' (Finset.card_pos.mp <| lt_trans zero_lt_one h₂) <
-      s.max' (Finset.card_pos.mp <| lt_trans zero_lt_one h₂) := by
+    s.min' (Finset.card_pos.1 <| by omega) < s.max' (Finset.card_pos.1 <| by omega) := by
   rcases one_lt_card.1 h₂ with ⟨a, ha, b, hb, hab⟩
   exact s.min'_lt_max' ha hb hab
 #align finset.min'_lt_max'_of_card Finset.min'_lt_max'_of_card

Mathlib/Data/Finset/Prod.lean

@@ -337,11 +337,7 @@ theorem diag_card : (diag s).card = s.card := by
 
 @[simp]
 theorem offDiag_card : (offDiag s).card = s.card * s.card - s.card :=
-  suffices (diag s).card + (offDiag s).card = s.card * s.card by
-    conv_rhs => { rw [← s.diag_card] }
-    simp only [diag_card] at *
-    rw [tsub_eq_of_eq_add_rev]
-    rw [this]
+  suffices (diag s).card + (offDiag s).card = s.card * s.card by rw [s.diag_card] at this; omega
   by rw [← card_product, diag, offDiag]
      conv_rhs => rw [← filter_card_add_filter_neg_card_eq_card (fun a => a.1 = a.2)]
 #align finset.off_diag_card Finset.offDiag_card

Mathlib/Data/Nat/Interval.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Data.Nat.Cast.Order
 import Mathlib.Order.Interval.Finset.Basic
 import Mathlib.Order.Interval.Multiset
 import Mathlib.Algebra.Order.Interval.Finset
@@ -122,12 +121,8 @@ theorem card_uIcc : (uIcc a b).card = (b - a : ℤ).natAbs + 1 := by
   refine' (card_Icc _ _).trans (Int.ofNat.inj _)
   change ((↑) : ℕ → ℤ) _ = _
   rw [sup_eq_max, inf_eq_min, Int.ofNat_sub]
-  · rw [add_comm, Int.ofNat_add, add_sub_assoc]
-    -- Porting note: `norm_cast` puts a `Int.subSubNat` in the goal
-    -- norm_cast
-    change _ = ↑(Int.natAbs (b - a) + 1)
-    push_cast
-    rw [max_sub_min_eq_abs, add_comm]
+  · change _ = ↑(Int.natAbs (b - a) + 1)
+    omega
   · exact min_le_max.trans le_self_add
 #align nat.card_uIcc Nat.card_uIcc
 

Mathlib/Data/Set/Enumerate.lean

@@ -3,7 +3,8 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import Mathlib.Algebra.Order.Ring.Nat
+import Mathlib.Algebra.Group.Basic
+import Mathlib.Algebra.Group.Nat
 import Mathlib.Data.Set.Basic
 import Mathlib.Tactic.Common
 

Mathlib/Order/SuccPred/LinearLocallyFinite.lean

@@ -4,11 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
 import Mathlib.Data.Countable.Basic
-import Mathlib.Data.Nat.Cast.Order
 import Mathlib.Logic.Encodable.Basic
-import Mathlib.Order.Hom.Basic
-import Mathlib.Order.Interval.Finset.Defs
 import Mathlib.Order.SuccPred.Basic
+import Mathlib.Order.Interval.Finset.Defs
 
 #align_import order.succ_pred.linear_locally_finite from "leanprover-community/mathlib"@"2705404e701abc6b3127da906f40bae062a169c9"
 
@@ -219,15 +217,13 @@ theorem iterate_pred_toZ (i : ι) (hi : i < i0) : pred^[(-toZ i0 i).toNat] i0 =
   exact Nat.find_spec (exists_pred_iterate_of_le hi.le)
 #align iterate_pred_to_Z iterate_pred_toZ
 
-theorem toZ_nonneg (hi : i0 ≤ i) : 0 ≤ toZ i0 i := by
-  rw [toZ_of_ge hi]
-  exact Nat.cast_nonneg _
+lemma toZ_nonneg (hi : i0 ≤ i) : 0 ≤ toZ i0 i := by rw [toZ_of_ge hi]; exact Int.natCast_nonneg _
 #align to_Z_nonneg toZ_nonneg
 
 theorem toZ_neg (hi : i < i0) : toZ i0 i < 0 := by
   refine' lt_of_le_of_ne _ _
-  · rw [toZ_of_lt hi, neg_nonpos]
-    exact Nat.cast_nonneg _
+  · rw [toZ_of_lt hi]
+    omega
   · by_contra h
     have h_eq := iterate_pred_toZ i hi
     rw [← h_eq, h] at hi
@@ -244,8 +240,9 @@ theorem toZ_iterate_pred_ge (n : ℕ) : -(n : ℤ) ≤ toZ i0 (pred^[n] i0) := b
   rcases le_or_lt i0 (pred^[n] i0) with h | h
   · have h_eq : pred^[n] i0 = i0 := le_antisymm (pred_iterate_le _ _) h
     rw [h_eq, toZ_of_eq]
-    simp only [Right.neg_nonpos_iff, Nat.cast_nonneg]
-  · rw [toZ_of_lt h, neg_le_neg_iff]
+    omega
+  · rw [toZ_of_lt h]
+    refine Int.neg_le_neg ?_
     norm_cast
     exact Nat.find_min' _ rfl
 #align to_Z_iterate_pred_ge toZ_iterate_pred_ge
@@ -257,7 +254,7 @@ theorem toZ_iterate_succ_of_not_isMax (n : ℕ) (hn : ¬IsMax (succ^[n] i0)) :
   by_cases hmn : m = n
   · nth_rw 2 [← hmn]
     rw [Int.toNat_eq_max, toZ_of_ge (le_succ_iterate _ _), max_eq_left]
-    exact Nat.cast_nonneg _
+    exact Int.natCast_nonneg _
   suffices IsMax (succ^[n] i0) from absurd this hn
   exact isMax_iterate_succ_of_eq_of_ne h_eq.symm (Ne.symm hmn)
 #align to_Z_iterate_succ_of_not_is_max toZ_iterate_succ_of_not_isMax
@@ -277,7 +274,7 @@ theorem toZ_iterate_pred_of_not_isMin (n : ℕ) (hn : ¬IsMin (pred^[n] i0)) :
   · nth_rw 2 [← hmn]
     rw [Int.toNat_eq_max, toZ_of_lt this, max_eq_left, neg_neg]
     rw [neg_neg]
-    exact Nat.cast_nonneg _
+    exact Int.natCast_nonneg _
   · suffices IsMin (pred^[n.succ] i0) from absurd this hn
     exact isMin_iterate_pred_of_eq_of_ne h_eq.symm (Ne.symm hmn)
 #align to_Z_iterate_pred_of_not_is_min toZ_iterate_pred_of_not_isMin
@@ -290,7 +287,7 @@ theorem le_of_toZ_le {j : ι} (h_le : toZ i0 i ≤ toZ i0 j) : i ≤ j := by
   · exact hi.le.trans hj
   · rw [← iterate_pred_toZ i hi, ← iterate_pred_toZ j hj]
     refine' Monotone.antitone_iterate_of_map_le pred_mono (pred_le _) (Int.toNat_le_toNat _)
-    exact neg_le_neg h_le
+    exact Int.neg_le_neg h_le
 #align le_of_to_Z_le le_of_toZ_le
 
 theorem toZ_mono {i j : ι} (h_le : i ≤ j) : toZ i0 i ≤ toZ i0 j := by
@@ -398,7 +395,7 @@ noncomputable def orderIsoIntOfLinearSuccPredArch [NoMaxOrder ι] [NoMinOrder ι
       exact Int.toNat_of_nonneg hn
     · 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]
+      simp only [hn.le, Int.toNat_of_nonneg, Int.neg_nonneg_of_nonpos, Int.neg_neg]
   map_rel_iff' := by intro i j; exact toZ_le_iff i j
 #align order_iso_int_of_linear_succ_pred_arch orderIsoIntOfLinearSuccPredArch
 

Mathlib/RingTheory/Prime.lean

@@ -5,6 +5,7 @@ Authors: Chris Hughes
 -/
 import Mathlib.Algebra.Associated
 import Mathlib.Algebra.BigOperators.Basic
+import Mathlib.Algebra.Order.Group.Abs
 import Mathlib.Algebra.Ring.Divisibility.Basic
 
 #align_import ring_theory.prime from "leanprover-community/mathlib"@"008205aa645b3f194c1da47025c5f110c8406eab"