chore: deprecate 14 Init.Logic lemmas (#16721)

Deprecate
* `(and,or,iff)_(true,false)_iff` and `(true,false)_(and_or_iff)_iff` for the lemmas without `_iff`, which are in core
* `iff_self_iff` for `iff_self` in core
* `not_or_of_not` for `not_or_intro` in core

The vast majority of their uses are as simp/rw lemmas, for which the core versions work equally well.

Archive/Imo/Imo1994Q1.lean

@@ -77,7 +77,7 @@ theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : Finset ℕ) (hm : A.card = m + 1)
   have hf : map f (Icc 0 k) ⊆ map a.toEmbedding (Ioc (rev k) (Fin.last m)) := by
     intro x hx
     simp only [Equiv.subLeft_apply, a, rev] at h
-    simp only [mem_map, mem_Icc, mem_Ioc, Fin.zero_le, true_and_iff, Equiv.subLeft_apply,
+    simp only [mem_map, mem_Icc, mem_Ioc, Fin.zero_le, true_and, Equiv.subLeft_apply,
       Function.Embedding.coeFn_mk, exists_prop, RelEmbedding.coe_toEmbedding, f, rev] at hx ⊢
     rcases hx with ⟨i, ⟨hi, rfl⟩⟩
     have h1 : a i + a (Fin.last m - k) ≤ n := by unfold_let; linarith only [h, a.monotone hi]

Archive/Imo/Imo1998Q2.lean

@@ -104,9 +104,9 @@ theorem A_fibre_over_contestant (c : C) :
     (Finset.univ.filter fun p : JudgePair J => p.Agree r c ∧ p.Distinct) =
       ((A r).filter fun a : AgreedTriple C J => a.contestant = c).image Prod.snd := by
   ext p
-  simp only [A, Finset.mem_univ, Finset.mem_filter, Finset.mem_image, true_and_iff, exists_prop]
+  simp only [A, Finset.mem_univ, Finset.mem_filter, Finset.mem_image, exists_prop]
   constructor
-  · rintro ⟨h₁, h₂⟩; refine ⟨(c, p), ?_⟩; tauto
+  · rintro ⟨_, h₂⟩; refine ⟨(c, p), ?_⟩; tauto
   · intro h; aesop
 
 theorem A_fibre_over_contestant_card (c : C) :

Archive/MiuLanguage/DecisionSuf.lean

@@ -265,7 +265,7 @@ theorem base_case_suf (en : Miustr) (h : Decstr en) (hu : count U en = 0) : Deri
   rcases h with ⟨⟨mhead, nmtail⟩, hi⟩
   have : en ≠ nil := by
     intro k
-    simp only [k, count, countP, countP.go, if_false, zero_mod, zero_ne_one, false_or_iff,
+    simp only [k, count, countP, countP.go, if_false, zero_mod, zero_ne_one, false_or,
       reduceCtorEq] at hi
   rcases exists_cons_of_ne_nil this with ⟨y, ys, rfl⟩
   rcases mhead

Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

@@ -147,7 +147,7 @@ theorem erdos_szekeres {r s n : ℕ} {f : Fin n → α} (hn : r * s < n) (hf : I
   have : image ab univ ⊆ ran := by
     -- First some logical shuffling
     rintro ⟨x₁, x₂⟩
-    simp only [ran, mem_image, exists_prop, mem_range, mem_univ, mem_product, true_and_iff,
+    simp only [ran, mem_image, exists_prop, mem_range, mem_univ, mem_product, true_and,
       Prod.ext_iff]
     rintro ⟨i, rfl, rfl⟩
     specialize q i

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -206,7 +206,7 @@ theorem first_vote_pos :
         ((countedSequence_nonempty _ _).image _)]
     · have : List.cons (-1) '' countedSequence (p + 1) q ∩ {l : List ℤ | l.headI = 1} = ∅ := by
         ext
-        simp only [mem_inter_iff, mem_image, mem_setOf_eq, mem_empty_iff_false, iff_false_iff,
+        simp only [mem_inter_iff, mem_image, mem_setOf_eq, mem_empty_iff_false, iff_false,
           not_and, forall_exists_index, and_imp]
         rintro l _ rfl
         norm_num
@@ -262,7 +262,7 @@ theorem countedSequence_int_pos_counted_succ_succ (p q : ℕ) :
       (_ : List.cons (-1) '' countedSequence (p + 1) q ∩ {l | l.headI = 1} = ∅), union_empty] <;>
     · ext
       simp only [mem_inter_iff, mem_image, mem_setOf_eq, and_iff_left_iff_imp, mem_empty_iff_false,
-        iff_false_iff, not_and, forall_exists_index, and_imp]
+        iff_false, not_and, forall_exists_index, and_imp]
       rintro y _ rfl
       norm_num
 
@@ -289,7 +289,7 @@ theorem countedSequence_int_neg_counted_succ_succ (p q : ℕ) :
       empty_union] <;>
     · ext
       simp only [mem_inter_iff, mem_image, mem_setOf_eq, and_iff_left_iff_imp, mem_empty_iff_false,
-        iff_false_iff, not_and, forall_exists_index, and_imp]
+        iff_false, not_and, forall_exists_index, and_imp]
       rintro y _ rfl
       norm_num
 
@@ -363,7 +363,7 @@ theorem ballot_problem :
   rwa [ENNReal.toReal_eq_toReal (measure_lt_top _ _).ne] at this
   simp only [Ne, ENNReal.div_eq_top, tsub_eq_zero_iff_le, Nat.cast_le, not_le,
     add_eq_zero, Nat.cast_eq_zero, ENNReal.add_eq_top, ENNReal.natCast_ne_top, or_self_iff,
-    not_false_iff, and_true_iff]
+    not_false_iff, and_true]
   push_neg
   exact ⟨fun _ _ => by linarith, (tsub_le_self.trans_lt (ENNReal.natCast_ne_top p).lt_top).ne⟩
 

Archive/Wiedijk100Theorems/CubingACube.lean

@@ -71,7 +71,7 @@ theorem univ_pi_side (c : Cube n) : pi univ (side c) = c.toSet :=
 
 theorem toSet_subset {c c' : Cube n} : c.toSet ⊆ c'.toSet ↔ ∀ j, c.side j ⊆ c'.side j := by
   simp only [← univ_pi_side, univ_pi_subset_univ_pi_iff, (c.side_nonempty _).ne_empty, exists_false,
-    or_false_iff]
+    or_false]
 
 theorem toSet_disjoint {c c' : Cube n} :
     Disjoint c.toSet c'.toSet ↔ ∃ j, Disjoint (c.side j) (c'.side j) := by
@@ -361,7 +361,7 @@ theorem smallest_onBoundary {j} (bi : OnBoundary (mi_mem_bcubes : mi h v ∈ _)
     dsimp only [x]; rw [← bi, add_sub_assoc, add_lt_iff_neg_left, sub_lt_zero]
     apply mi_strict_minimal (Ne.symm h2i') hi'
   refine ⟨x, ⟨?_, ?_⟩, ?_⟩
-  · simp only [side, neg_lt_zero, hw, add_lt_iff_neg_left, and_true_iff, mem_Ico, sub_eq_add_neg, x]
+  · simp only [side, neg_lt_zero, hw, add_lt_iff_neg_left, and_true, mem_Ico, sub_eq_add_neg, x]
     rw [add_assoc, le_add_iff_nonneg_right, ← sub_eq_add_neg, sub_nonneg]
     apply le_of_lt (w_lt_w h v hi')
   · simp only [side, not_and_or, not_lt, not_le, mem_Ico]; left; exact hx
@@ -408,7 +408,7 @@ theorem mi_not_onBoundary (j : Fin n) : ¬OnBoundary (mi_mem_bcubes : mi h v ∈
   have i'_i'' : i' ≠ i'' := by
     rintro ⟨⟩
     have : (cs i).b ∈ (cs i').toSet := by
-      simp only [toSet, forall_iff_succ, hi.1, bottom_mem_side h2i', true_and_iff, mem_setOf_eq]
+      simp only [toSet, forall_iff_succ, hi.1, bottom_mem_side h2i', true_and, mem_setOf_eq]
       intro j₂; by_cases hj₂ : j₂ = j
       · simpa [p', side_tail, hj'.symm, hj₂] using hi''.2 j
       · simpa [p, hj₂] using hi'.2 j₂

Archive/Wiedijk100Theorems/FriendshipGraphs.lean

@@ -179,7 +179,7 @@ theorem card_of_regular (hd : G.IsRegularOfDegree d) : d + (Fintype.card V - 1)
   trans ((G.adjMatrix ℕ ^ 2) *ᵥ (fun _ => 1)) v
   · rw [adjMatrix_sq_of_regular hG hd, mulVec, dotProduct, ← insert_erase (mem_univ v)]
     simp only [sum_insert, mul_one, if_true, Nat.cast_id, eq_self_iff_true, mem_erase, not_true,
-      Ne, not_false_iff, add_right_inj, false_and_iff, of_apply]
+      Ne, not_false_iff, add_right_inj, false_and, of_apply]
     rw [Finset.sum_const_nat, card_erase_of_mem (mem_univ v), mul_one]; · rfl
     intro x hx; simp [(ne_of_mem_erase hx).symm]
   · rw [sq, ← mulVec_mulVec]

Archive/Wiedijk100Theorems/Partition.lean

@@ -206,7 +206,7 @@ theorem partialGF_prop (α : Type*) [CommSemiring α] (n : ℕ) (s : Finset ℕ)
   · dsimp only
     intro p₁ hp₁ p₂ hp₂ h
     apply Nat.Partition.ext
-    simp only [true_and_iff, mem_univ, mem_filter] at hp₁ hp₂
+    simp only [true_and, mem_univ, mem_filter] at hp₁ hp₂
     ext i
     simp only [φ, ne_eq, Multiset.mem_toFinset, not_not, smul_eq_mul, Finsupp.mk.injEq] at h
     by_cases hi : i = 0
@@ -218,7 +218,7 @@ theorem partialGF_prop (α : Type*) [CommSemiring α] (n : ℕ) (s : Finset ℕ)
     · rw [← mul_left_inj' hi]
       rw [Function.funext_iff] at h
       exact h.2 i
-  · simp only [φ, mem_filter, mem_finsuppAntidiag, mem_univ, exists_prop, true_and_iff, and_assoc]
+  · simp only [φ, mem_filter, mem_finsuppAntidiag, mem_univ, exists_prop, true_and, and_assoc]
     rintro f ⟨hf, hf₃, hf₄⟩
     have hf' : f ∈ finsuppAntidiag s n := mem_finsuppAntidiag.mpr ⟨hf, hf₃⟩
     simp only [mem_finsuppAntidiag] at hf'
@@ -266,7 +266,7 @@ theorem partialOddGF_prop [Field α] (n m : ℕ) :
   convert partialGF_prop α n
     ((range m).map mkOdd) _ (fun _ => Set.univ) (fun _ _ => trivial) using 2
   · congr
-    simp only [true_and_iff, forall_const, Set.mem_univ]
+    simp only [true_and, forall_const, Set.mem_univ]
   · rw [Finset.prod_map]
     simp_rw [num_series']
     congr! 2 with x

Counterexamples/Phillips.lean

@@ -467,14 +467,14 @@ theorem sierpinski_pathological_family (Hcont : #ℝ = aleph 1) :
   refine ⟨fun x => {y | r x y}, fun x => ?_, fun y => ?_⟩
   · have : univ \ {y | r x y} = {y | r y x} ∪ {x} := by
       ext y
-      simp only [true_and_iff, mem_univ, mem_setOf_eq, mem_insert_iff, union_singleton, mem_diff]
+      simp only [true_and, mem_univ, mem_setOf_eq, mem_insert_iff, union_singleton, mem_diff]
       rcases trichotomous_of r x y with (h | rfl | h)
-      · simp only [h, not_or, false_iff_iff, not_true]
+      · simp only [h, not_or, false_iff, not_true]
         constructor
         · rintro rfl; exact irrefl_of r y h
         · exact asymm h
-      · simp only [true_or_iff, eq_self_iff_true, iff_true_iff]; exact irrefl x
-      · simp only [h, iff_true_iff, or_true_iff]; exact asymm h
+      · simp only [true_or, eq_self_iff_true, iff_true]; exact irrefl x
+      · simp only [h, iff_true, or_true]; exact asymm h
     rw [this]
     apply Countable.union _ (countable_singleton _)
     rw [Cardinal.countable_iff_lt_aleph_one, ← Hcont]

Mathlib/Algebra/BigOperators/Group/Finset.lean

@@ -2074,7 +2074,7 @@ theorem disjoint_list_sum_left {a : Multiset α} {l : List (Multiset α)} :
     simp only [zero_disjoint, List.not_mem_nil, IsEmpty.forall_iff, forall_const, List.sum_nil]
   | cons b bs ih =>
     simp_rw [List.sum_cons, disjoint_add_left, List.mem_cons, forall_eq_or_imp]
-    simp [and_congr_left_iff, iff_self_iff, ih]
+    simp [and_congr_left_iff, ih]
 
 theorem disjoint_list_sum_right {a : Multiset α} {l : List (Multiset α)} :
     Multiset.Disjoint a l.sum ↔ ∀ b ∈ l, Multiset.Disjoint a b := by
@@ -2093,7 +2093,7 @@ theorem disjoint_sum_right {a : Multiset α} {i : Multiset (Multiset α)} :
 theorem disjoint_finset_sum_left {β : Type*} {i : Finset β} {f : β → Multiset α} {a : Multiset α} :
     Multiset.Disjoint (i.sum f) a ↔ ∀ b ∈ i, Multiset.Disjoint (f b) a := by
   convert @disjoint_sum_left _ a (map f i.val)
-  simp [and_congr_left_iff, iff_self_iff]
+  simp [and_congr_left_iff]
 
 theorem disjoint_finset_sum_right {β : Type*} {i : Finset β} {f : β → Multiset α}
     {a : Multiset α} : Multiset.Disjoint a (i.sum f) ↔ ∀ b ∈ i, Multiset.Disjoint a (f b) := by

Mathlib/Algebra/CharZero/Lemmas.lean

@@ -79,7 +79,7 @@ variable {R : Type*} [NonAssocSemiring R] [NoZeroDivisors R] [CharZero R] {a : R
 
 @[simp]
 theorem add_self_eq_zero {a : R} : a + a = 0 ↔ a = 0 := by
-  simp only [(two_mul a).symm, mul_eq_zero, two_ne_zero, false_or_iff]
+  simp only [(two_mul a).symm, mul_eq_zero, two_ne_zero, false_or]
 
 end
 

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -666,7 +666,7 @@ theorem lcm_dvd_iff [GCDMonoid α] {a b c : α} : lcm a b ∣ c ↔ a ∣ c ∧
   by_cases h : a = 0 ∨ b = 0
   · rcases h with (rfl | rfl) <;>
       simp (config := { contextual := true }) only [iff_def, lcm_zero_left, lcm_zero_right,
-        zero_dvd_iff, dvd_zero, eq_self_iff_true, and_true_iff, imp_true_iff]
+        zero_dvd_iff, dvd_zero, eq_self_iff_true, and_true, imp_true_iff]
   · obtain ⟨h1, h2⟩ := not_or.1 h
     have h : gcd a b ≠ 0 := fun H => h1 ((gcd_eq_zero_iff _ _).1 H).1
     rw [← mul_dvd_mul_iff_left h, (gcd_mul_lcm a b).dvd_iff_dvd_left, ←
@@ -1306,7 +1306,7 @@ instance (priority := 100) : NormalizedGCDMonoid G₀ where
         exact Associated.refl _
       -- Porting note(#12129): additional beta reduction needed
       · beta_reduce
-        rw [if_neg (not_and_of_not_left _ ha), one_mul, if_neg (not_or_of_not ha hb)]
+        rw [if_neg (not_and_of_not_left _ ha), one_mul, if_neg (not_or_intro ha hb)]
         exact (associated_one_iff_isUnit.mpr ((IsUnit.mk0 _ ha).mul (IsUnit.mk0 _ hb))).symm
   lcm_zero_left b := if_pos (Or.inl rfl)
   lcm_zero_right a := if_pos (Or.inr rfl)

Mathlib/Algebra/Group/Pointwise/Set.lean

@@ -1146,7 +1146,7 @@ theorem isUnit_singleton (a : α) : IsUnit ({a} : Set α) :=
 
 @[to_additive (attr := simp)]
 theorem isUnit_iff_singleton : IsUnit s ↔ ∃ a, s = {a} := by
-  simp only [isUnit_iff, Group.isUnit, and_true_iff]
+  simp only [isUnit_iff, Group.isUnit, and_true]
 
 @[to_additive (attr := simp)]
 theorem image_mul_left : (a * ·) '' t = (a⁻¹ * ·) ⁻¹' t := by

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -1717,7 +1717,7 @@ This may be easier to work with, as it avoids inequalities and negations. -/
 theorem _root_.normalizerCondition_iff_only_full_group_self_normalizing :
     NormalizerCondition G ↔ ∀ H : Subgroup G, H.normalizer = H → H = ⊤ := by
   apply forall_congr'; intro H
-  simp only [lt_iff_le_and_ne, le_normalizer, true_and_iff, le_top, Ne]
+  simp only [lt_iff_le_and_ne, le_normalizer, le_top, Ne]
   tauto
 
 variable (H)
@@ -2219,10 +2219,10 @@ instance (priority := 100) normal_ker (f : G →* M) : f.ker.Normal :=
     rw [mem_ker, map_mul, map_mul, f.mem_ker.1 hx, mul_one, map_mul_eq_one f (mul_inv_cancel y)]⟩
 
 @[to_additive (attr := simp)]
-lemma ker_fst : ker (fst G G') = .prod ⊥ ⊤ := SetLike.ext fun _ => (and_true_iff _).symm
+lemma ker_fst : ker (fst G G') = .prod ⊥ ⊤ := SetLike.ext fun _ => (iff_of_eq (and_true _)).symm
 
 @[to_additive (attr := simp)]
-lemma ker_snd : ker (snd G G') = .prod ⊤ ⊥ := SetLike.ext fun _ => (true_and_iff _).symm
+lemma ker_snd : ker (snd G G') = .prod ⊤ ⊥ := SetLike.ext fun _ => (iff_of_eq (true_and _)).symm
 
 @[simp]
 theorem coe_toAdditive_ker (f : G →* G') :
@@ -2384,7 +2384,7 @@ theorem map_le_map_iff {f : G →* N} {H K : Subgroup G} : H.map f ≤ K.map f 
 @[to_additive]
 theorem map_le_map_iff' {f : G →* N} {H K : Subgroup G} :
     H.map f ≤ K.map f ↔ H ⊔ f.ker ≤ K ⊔ f.ker := by
-  simp only [map_le_map_iff, sup_le_iff, le_sup_right, and_true_iff]
+  simp only [map_le_map_iff, sup_le_iff, le_sup_right, and_true]
 
 @[to_additive]
 theorem map_eq_map_iff {f : G →* N} {H K : Subgroup G} :

Mathlib/Algebra/Group/Subgroup/Pointwise.lean

@@ -72,7 +72,7 @@ theorem closure_toSubmonoid (S : Set G) :
         (fun x hx => Submonoid.closure_mono subset_union_left (Submonoid.subset_closure hx))
         (Submonoid.one_mem _) (fun x y hx hy => Submonoid.mul_mem _ hx hy) fun x hx => ?_
     rwa [← Submonoid.mem_closure_inv, Set.union_inv, inv_inv, Set.union_comm]
-  · simp only [true_and_iff, coe_toSubmonoid, union_subset_iff, subset_closure, inv_subset_closure]
+  · simp only [true_and, coe_toSubmonoid, union_subset_iff, subset_closure, inv_subset_closure]
 
 /-- For subgroups generated by a single element, see the simpler `zpow_induction_left`. -/
 @[to_additive (attr := elab_as_elim)

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -914,10 +914,10 @@ theorem mker_inr : mker (inr M N) = ⊥ := by
   simp [mem_mker]
 
 @[to_additive (attr := simp)]
-lemma mker_fst : mker (fst M N) = .prod ⊥ ⊤ := SetLike.ext fun _ => (and_true_iff _).symm
+lemma mker_fst : mker (fst M N) = .prod ⊥ ⊤ := SetLike.ext fun _ => (iff_of_eq (and_true _)).symm
 
 @[to_additive (attr := simp)]
-lemma mker_snd : mker (snd M N) = .prod ⊤ ⊥ := SetLike.ext fun _ => (true_and_iff _).symm
+lemma mker_snd : mker (snd M N) = .prod ⊤ ⊥ := SetLike.ext fun _ => (iff_of_eq (true_and _)).symm
 
 /-- The `MonoidHom` from the preimage of a submonoid to itself. -/
 @[to_additive (attr := simps)

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -411,8 +411,7 @@ lemma zpow_add' {m n : ℤ} (h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0) :
   · simp [hn]
   by_cases ha : a = 0
   · subst a
-    simp only [false_or_iff, eq_self_iff_true, not_true, Ne, hm, hn, false_and_iff,
-      or_false_iff] at h
+    simp only [false_or, eq_self_iff_true, not_true, Ne, hm, hn, false_and, or_false] at h
     rw [zero_zpow _ h, zero_zpow _ hm, zero_mul]
   · exact zpow_add₀ ha m n
 

Mathlib/Algebra/Lie/CartanSubalgebra.lean

@@ -107,7 +107,7 @@ end LieSubalgebra
 theorem LieIdeal.normalizer_eq_top {R : Type u} {L : Type v} [CommRing R] [LieRing L]
     [LieAlgebra R L] (I : LieIdeal R L) : (I : LieSubalgebra R L).normalizer = ⊤ := by
   ext x
-  simpa only [LieSubalgebra.mem_normalizer_iff, LieSubalgebra.mem_top, iff_true_iff] using
+  simpa only [LieSubalgebra.mem_normalizer_iff, LieSubalgebra.mem_top, iff_true] using
     fun y hy => I.lie_mem hy
 
 open LieIdeal

Mathlib/Algebra/Lie/Submodule.lean

@@ -550,7 +550,7 @@ nonrec theorem eq_bot_iff : N = ⊥ ↔ ∀ m : M, m ∈ N → m = 0 := by rw [e
 instance subsingleton_of_bot : Subsingleton (LieSubmodule R L ↑(⊥ : LieSubmodule R L M)) := by
   apply subsingleton_of_bot_eq_top
   ext ⟨x, hx⟩; change x ∈ ⊥ at hx; rw [Submodule.mem_bot] at hx; subst hx
-  simp only [true_iff_iff, eq_self_iff_true, Submodule.mk_eq_zero, LieSubmodule.mem_bot, mem_top]
+  simp only [eq_self_iff_true, Submodule.mk_eq_zero, LieSubmodule.mem_bot, mem_top]
 
 instance : IsModularLattice (LieSubmodule R L M) where
   sup_inf_le_assoc_of_le _ _ := by

Mathlib/Algebra/Module/Basic.lean

@@ -135,7 +135,7 @@ lemma support_smul_subset_right [Zero M] [SMulZeroClass R M] (f : α → R) (g :
 
 lemma support_const_smul_of_ne_zero [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M]
     (c : R) (g : α → M) (hc : c ≠ 0) : support (c • g) = support g :=
-  ext fun x ↦ by simp only [hc, mem_support, Pi.smul_apply, Ne, smul_eq_zero, false_or_iff]
+  ext fun x ↦ by simp only [hc, mem_support, Pi.smul_apply, Ne, smul_eq_zero, false_or]
 
 lemma support_smul [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] (f : α → R)
     (g : α → M) : support (f • g) = support f ∩ support g :=

Mathlib/Algebra/Module/Submodule/Map.lean

@@ -624,7 +624,7 @@ This is `LinearEquiv.ofSubmodule'` but with `map` on the right instead of `comap
 def submoduleMap (p : Submodule R M) : p ≃ₛₗ[σ₁₂] ↥(p.map (e : M →ₛₗ[σ₁₂] M₂) : Submodule R₂ M₂) :=
   { ((e : M →ₛₗ[σ₁₂] M₂).domRestrict p).codRestrict (p.map (e : M →ₛₗ[σ₁₂] M₂)) fun x =>
       ⟨x, by
-        simp only [LinearMap.domRestrict_apply, eq_self_iff_true, and_true_iff, SetLike.coe_mem,
+        simp only [LinearMap.domRestrict_apply, eq_self_iff_true, and_true, SetLike.coe_mem,
           SetLike.mem_coe]⟩ with
     invFun := fun y =>
       ⟨(e.symm : M₂ →ₛₗ[σ₂₁] M) y, by

Mathlib/Algebra/MvPolynomial/Division.lean

@@ -206,7 +206,7 @@ theorem monomial_dvd_monomial {r s : R} {i j : σ →₀ ℕ} :
 theorem monomial_one_dvd_monomial_one [Nontrivial R] {i j : σ →₀ ℕ} :
     monomial i (1 : R) ∣ monomial j 1 ↔ i ≤ j := by
   rw [monomial_dvd_monomial]
-  simp_rw [one_ne_zero, false_or_iff, dvd_rfl, and_true_iff]
+  simp_rw [one_ne_zero, false_or, dvd_rfl, and_true]
 
 @[simp]
 theorem X_dvd_X [Nontrivial R] {i j : σ} :
@@ -219,6 +219,6 @@ theorem X_dvd_X [Nontrivial R] {i j : σ} :
 theorem X_dvd_monomial {i : σ} {j : σ →₀ ℕ} {r : R} :
     (X i : MvPolynomial σ R) ∣ monomial j r ↔ r = 0 ∨ j i ≠ 0 := by
   refine monomial_dvd_monomial.trans ?_
-  simp_rw [one_dvd, and_true_iff, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero]
+  simp_rw [one_dvd, and_true, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero]
 
 end MvPolynomial

Mathlib/Algebra/MvPolynomial/Rename.lean

@@ -206,15 +206,14 @@ theorem exists_finset_rename (p : MvPolynomial σ R) :
   · rintro p q ⟨s, p, rfl⟩ ⟨t, q, rfl⟩
     refine ⟨s ∪ t, ⟨?_, ?_⟩⟩
     · refine rename (Subtype.map id ?_) p + rename (Subtype.map id ?_) q <;>
-        simp (config := { contextual := true }) only [id, true_or_iff, or_true_iff,
+        simp (config := { contextual := true }) only [id, true_or, or_true,
           Finset.mem_union, forall_true_iff]
     · simp only [rename_rename, map_add]
       rfl
   · rintro p n ⟨s, p, rfl⟩
     refine ⟨insert n s, ⟨?_, ?_⟩⟩
     · refine rename (Subtype.map id ?_) p * X ⟨n, s.mem_insert_self n⟩
-      simp (config := { contextual := true }) only [id, or_true_iff, Finset.mem_insert,
-        forall_true_iff]
+      simp (config := { contextual := true }) only [id, or_true, Finset.mem_insert, forall_true_iff]
     · simp only [rename_rename, rename_X, Subtype.coe_mk, map_mul]
       rfl
 

Mathlib/Algebra/MvPolynomial/Variables.lean

@@ -149,7 +149,7 @@ theorem vars_C_mul (a : A) (ha : a ≠ 0) (φ : MvPolynomial σ A) :
   apply exists_congr
   intro d
   apply and_congr _ Iff.rfl
-  rw [coeff_C_mul, mul_ne_zero_iff, eq_true ha, true_and_iff]
+  rw [coeff_C_mul, mul_ne_zero_iff, eq_true ha, true_and]
 
 end IsDomain
 

Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

@@ -545,7 +545,7 @@ theorem finset_sum_eq_sup_iff_disjoint [DecidableEq α] {β : Type*} {i : Finset
   · simp only [Finset.not_mem_empty, IsEmpty.forall_iff, imp_true_iff, Finset.sum_empty,
       Finset.sup_empty, bot_eq_zero, eq_self_iff_true]
   · simp_rw [Finset.sum_cons hz, Finset.sup_cons, Finset.mem_cons, Multiset.sup_eq_union,
-      forall_eq_or_imp, Ne, not_true_eq_false, IsEmpty.forall_iff, true_and_iff,
+      forall_eq_or_imp, Ne, not_true_eq_false, IsEmpty.forall_iff, true_and,
       imp_and, forall_and, ← hr, @eq_comm _ z]
     have := fun x (H : x ∈ i) => ne_of_mem_of_not_mem H hz
     simp (config := { contextual := true }) only [this, not_false_iff, true_imp_iff]