chore: deprecate dif_ctx_congr, move if_(ctx_)congr (#16692)

The few uses of `dif_ctx_congr` can all be replaced without increasing the line count. The other two `ite` congruence lemmas are moved to `Logic.Basic`.

Author: Parcly-Taxel

Mathlib/CategoryTheory/Preadditive/Mat.lean

@@ -184,11 +184,11 @@ instance hasFiniteBiproducts : HasFiniteBiproducts (Mat_ C) where
               ext x y
               dsimp
               simp_rw [dite_comp, comp_dite]
-              simp only [ite_self, dite_eq_ite, dif_ctx_congr, Limits.comp_zero, Limits.zero_comp,
+              simp only [ite_self, dite_eq_ite, Limits.comp_zero, Limits.zero_comp,
                 eqToHom_trans, Finset.sum_congr]
               erw [Finset.sum_sigma]
               dsimp
-              simp only [if_congr, if_true, dif_ctx_congr, Finset.sum_dite_irrel, Finset.mem_univ,
+              simp only [if_true, Finset.sum_dite_irrel, Finset.mem_univ,
                 Finset.sum_const_zero, Finset.sum_congr, Finset.sum_dite_eq']
               split_ifs with h h'
               · substs h h'

Mathlib/FieldTheory/Minpoly/Basic.lean

@@ -60,8 +60,8 @@ theorem eq_zero (hx : ¬IsIntegral A x) : minpoly A x = 0 :=
 
 theorem algHom_eq (f : B →ₐ[A] B') (hf : Function.Injective f) (x : B) :
     minpoly A (f x) = minpoly A x := by
-  refine dif_ctx_congr (isIntegral_algHom_iff _ hf) (fun _ => ?_) fun _ => rfl
-  simp_rw [← Polynomial.aeval_def, aeval_algHom, AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]
+  simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
+    AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]
 
 theorem algebraMap_eq {B} [CommRing B] [Algebra A B] [Algebra B B'] [IsScalarTower A B B']
     (h : Function.Injective (algebraMap B B')) (x : B) :

Mathlib/Init/Logic.lean

@@ -166,19 +166,7 @@ theorem imp_of_if_pos {c t e : Prop} [Decidable c] (h : ite c t e) (hc : c) : t
 theorem imp_of_if_neg {c t e : Prop} [Decidable c] (h : ite c t e) (hnc : ¬c) : e :=
   (if_neg hnc ▸ h :)
 
-theorem if_ctx_congr {α : Sort u} {b c : Prop} [dec_b : Decidable b] [dec_c : Decidable c]
-    {x y u v : α} (h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v) : ite b x y = ite c u v :=
-  match dec_b, dec_c with
-  | isFalse _,  isFalse h₂ => h_e h₂
-  | isTrue _,   isTrue h₂  => h_t h₂
-  | isFalse h₁, isTrue h₂  => absurd h₂ (Iff.mp (not_congr h_c) h₁)
-  | isTrue h₁,  isFalse h₂ => absurd h₁ (Iff.mpr (not_congr h_c) h₂)
-
-theorem if_congr {α : Sort u} {b c : Prop} [Decidable b] [Decidable c]
-    {x y u v : α} (h_c : b ↔ c) (h_t : x = u) (h_e : y = v) : ite b x y = ite c u v :=
-  if_ctx_congr h_c (fun _ ↦ h_t) (fun _ ↦ h_e)
-
--- @[congr]
+@[deprecated (since := "2024-09-11")]
 theorem dif_ctx_congr {α : Sort u} {b c : Prop} [dec_b : Decidable b] [dec_c : Decidable c]
     {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
     (h_c : b ↔ c) (h_t : ∀ h : c, x (Iff.mpr h_c h) = u h)

Mathlib/Logic/Basic.lean

@@ -952,6 +952,22 @@ theorem dite_prop_iff_and {Q : P → Prop} {R : ¬P → Prop} :
     dite P Q R ↔ (∀ h, Q h) ∧ (∀ h, R h) := by
   by_cases h : P <;> simp [h, forall_prop_of_false, forall_prop_of_true]
 
+section congr
+
+variable [Decidable Q] {x y u v : α}
+
+theorem if_ctx_congr (h_c : P ↔ Q) (h_t : Q → x = u) (h_e : ¬Q → y = v) : ite P x y = ite Q u v :=
+  match ‹Decidable P›, ‹Decidable Q› with
+  | isFalse _,  isFalse h₂ => by simp_all
+  | isTrue _,   isTrue h₂  => by simp_all
+  | isFalse h₁, isTrue h₂  => absurd h₂ (Iff.mp (not_congr h_c) h₁)
+  | isTrue h₁,  isFalse h₂ => absurd h₁ (Iff.mpr (not_congr h_c) h₂)
+
+theorem if_congr (h_c : P ↔ Q) (h_t : x = u) (h_e : y = v) : ite P x y = ite Q u v :=
+  if_ctx_congr h_c (fun _ ↦ h_t) (fun _ ↦ h_e)
+
+end congr
+
 end ite
 
 theorem not_beq_of_ne {α : Type*} [BEq α] [LawfulBEq α] {a b : α} (ne : a ≠ b) : ¬(a == b) :=

Mathlib/RingTheory/Coprime/Ideal.lean

@@ -35,7 +35,7 @@ theorem iSup_iInf_eq_top_iff_pairwise {t : Finset ι} (h : t.Nonempty) (I : ι 
   · simp only [Finset.sum_singleton, Finset.coe_singleton, Set.pairwise_singleton, iff_true_iff]
     refine fun a => ⟨fun i => if h : i = a then ⟨1, ?_⟩ else 0, ?_⟩
     · simp [h]
-    · simp only [dif_pos, dif_ctx_congr, Submodule.coe_mk, eq_self_iff_true]
+    · simp only [dif_pos, Submodule.coe_mk, eq_self_iff_true]
   intro a t hat h ih
   rw [Finset.coe_cons,
     Set.pairwise_insert_of_symmetric fun i j (h : I i ⊔ I j = ⊤) ↦ (sup_comm _ _).trans h]