feat: subsingleton tactic (#12525)

The `subsingleton` tactic tries to close equality goals by arguing that the underlying type is a subsingleton type. It might be via a `Subsingleton` instance (via `Subsingleton.elim`), but it also handles some cases where morally the types are subsingletons; for example, it can prove that two `BEq` instances are equal if they both have `LawfulBEq` instances. For heterogeneous equality, it tries the `HEq` version of proof irrelevance.

This tactic avoids the issue where
```lean
example (α : Sort _) (x y : α) : x = y := by apply Subsingleton.elim
```
is a "proof" that every type is trivial. Changing this to `by subsingleton` prevents it from assigning the universe level metavariable in `Sort _` to `0`.

This tactic can accept a list of instances `subsingleton [inst1, inst2, ...]` to do something like `have := inst1; have := inst2; ...; subsingleton`, but it elaborates them in a lenient way (like `simp` arguments), and they can even be universe polymorphic. For example, `subsingleton [CharP.CharOne.subsingleton]` is allowed even though the type of `CharP.CharOne.subsingleton` is `Subsingleton ?R` with a number of pending instance problems.

This PR also eliminates a number of uses of `Subsingleton.elim`, either by switching a `congr` to `congr!` or by using this new tactic.

Author: kmill

Mathlib.lean

@@ -4023,6 +4023,7 @@ import Mathlib.Tactic.Simps.NotationClass
 import Mathlib.Tactic.SlimCheck
 import Mathlib.Tactic.SplitIfs
 import Mathlib.Tactic.Spread
+import Mathlib.Tactic.Subsingleton
 import Mathlib.Tactic.Substs
 import Mathlib.Tactic.SuccessIfFailWithMsg
 import Mathlib.Tactic.SudoSetOption

Mathlib/Algebra/BigOperators/Fin.lean

@@ -342,8 +342,7 @@ def finFunctionFinEquiv {m n : ℕ} : (Fin n → Fin m) ≃ Fin (m ^ n) :=
     fun a => by
       dsimp
       induction' n with n ih
-      · haveI : Subsingleton (Fin (m ^ 0)) := (finCongr <| pow_zero _).subsingleton
-        exact Subsingleton.elim _ _
+      · subsingleton [(finCongr <| pow_zero _).subsingleton]
       simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
       ext
       simp_rw [Fin.sum_univ_succ, Fin.val_zero, Fin.val_succ, pow_zero, Nat.div_one,
@@ -398,9 +397,9 @@ def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃
       intro a; revert a; dsimp only [Fin.val_mk]
       refine Fin.consInduction ?_ ?_ n
       · intro a
-        haveI : Subsingleton (Fin (∏ i : Fin 0, i.elim0)) :=
+        have : Subsingleton (Fin (∏ i : Fin 0, i.elim0)) :=
           (finCongr <| prod_empty).subsingleton
-        exact Subsingleton.elim _ _
+        subsingleton
       · intro n x xs ih a
         simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
         ext

Mathlib/Algebra/BigOperators/Group/Finset.lean

@@ -2324,7 +2324,7 @@ theorem prod_empty {α β : Type*} [CommMonoid β] [IsEmpty α] [Fintype α] (f
 @[to_additive]
 theorem prod_subsingleton {α β : Type*} [CommMonoid β] [Subsingleton α] [Fintype α] (f : α → β)
     (a : α) : ∏ x : α, f x = f a := by
-  haveI : Unique α := uniqueOfSubsingleton a
+  have : Unique α := uniqueOfSubsingleton a
   rw [prod_unique f, Subsingleton.elim default a]
 #align fintype.prod_subsingleton Fintype.prod_subsingleton
 #align fintype.sum_subsingleton Fintype.sum_subsingleton

Mathlib/Algebra/Category/Grp/Zero.lean

@@ -31,7 +31,7 @@ theorem isZero_of_subsingleton (G : Grp) [Subsingleton G] : IsZero G := by
     have : x = 1 := Subsingleton.elim _ _
     rw [this, map_one, map_one]
   · ext
-    apply Subsingleton.elim
+    subsingleton
 set_option linter.uppercaseLean3 false in
 #align Group.is_zero_of_subsingleton Grp.isZero_of_subsingleton
 set_option linter.uppercaseLean3 false in
@@ -52,7 +52,7 @@ theorem isZero_of_subsingleton (G : CommGrp) [Subsingleton G] : IsZero G := by
     have : x = 1 := Subsingleton.elim _ _
     rw [this, map_one, map_one]
   · ext
-    apply Subsingleton.elim
+    subsingleton
 set_option linter.uppercaseLean3 false in
 #align CommGroup.is_zero_of_subsingleton CommGrp.isZero_of_subsingleton
 set_option linter.uppercaseLean3 false in

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -206,7 +206,7 @@ theorem isZero_of_subsingleton (M : ModuleCat R) [Subsingleton M] : IsZero M whe
     simp⟩⟩
   unique_from X := ⟨⟨⟨(0 : X →ₗ[R] M)⟩, fun f => by
     ext x
-    apply Subsingleton.elim⟩⟩
+    subsingleton⟩⟩
 #align Module.is_zero_of_subsingleton ModuleCat.isZero_of_subsingleton
 
 instance : HasZeroObject (ModuleCat.{v} R) :=

Mathlib/Algebra/DirectLimit.lean

@@ -200,7 +200,7 @@ def map (g : (i : ι) → G i →ₗ[R] G' i) (hg : ∀ i j h, g j ∘ₗ f i j
     DirectLimit G f →ₗ[R] DirectLimit G' f' :=
   lift _ _ _ _ (fun i ↦ of _ _ _ _ _ ∘ₗ g i) fun i j h g ↦ by
     cases isEmpty_or_nonempty ι
-    · exact Subsingleton.elim _ _
+    · subsingleton
     · have eq1 := LinearMap.congr_fun (hg i j h) g
       simp only [LinearMap.coe_comp, Function.comp_apply] at eq1 ⊢
       rw [eq1, of_f]
@@ -213,7 +213,7 @@ def map (g : (i : ι) → G i →ₗ[R] G' i) (hg : ∀ i j h, g j ∘ₗ f i j
 
 @[simp] lemma map_id [IsDirected ι (· ≤ ·)] :
     map (fun i ↦ LinearMap.id) (fun _ _ _ ↦ rfl) = LinearMap.id (R := R) (M := DirectLimit G f) :=
-  DFunLike.ext _ _ fun x ↦ (isEmpty_or_nonempty ι).elim (fun _ ↦ Subsingleton.elim _ _) fun _ ↦
+  DFunLike.ext _ _ fun x ↦ (isEmpty_or_nonempty ι).elim (by subsingleton) fun _ ↦
     x.induction_on fun i g ↦ by simp
 
 lemma map_comp [IsDirected ι (· ≤ ·)]
@@ -225,7 +225,7 @@ lemma map_comp [IsDirected ι (· ≤ ·)]
     (map (fun i ↦ g₂ i ∘ₗ g₁ i) fun i j h ↦ by
         rw [LinearMap.comp_assoc, hg₁ i, ← LinearMap.comp_assoc, hg₂ i, LinearMap.comp_assoc] :
       DirectLimit G f →ₗ[R] DirectLimit G'' f'') :=
-  DFunLike.ext _ _ fun x ↦ (isEmpty_or_nonempty ι).elim (fun _ ↦ Subsingleton.elim _ _) fun _ ↦
+  DFunLike.ext _ _ fun x ↦ (isEmpty_or_nonempty ι).elim (by subsingleton) fun _ ↦
     x.induction_on fun i g ↦ by simp
 
 open LinearEquiv LinearMap in
@@ -473,7 +473,7 @@ def map (g : (i : ι) → G i →+ G' i)
     DirectLimit G f →+ DirectLimit G' f' :=
   lift _ _ _ (fun i ↦ (of _ _ _).comp (g i)) fun i j h g ↦ by
     cases isEmpty_or_nonempty ι
-    · exact Subsingleton.elim _ _
+    · subsingleton
     · have eq1 := DFunLike.congr_fun (hg i j h) g
       simp only [AddMonoidHom.coe_comp, Function.comp_apply] at eq1 ⊢
       rw [eq1, of_f]
@@ -486,7 +486,7 @@ def map (g : (i : ι) → G i →+ G' i)
 
 @[simp] lemma map_id [IsDirected ι (· ≤ ·)] :
     map (fun i ↦ AddMonoidHom.id _) (fun _ _ _ ↦ rfl) = AddMonoidHom.id (DirectLimit G f) :=
-  DFunLike.ext _ _ fun x ↦ (isEmpty_or_nonempty ι).elim (fun _ ↦ Subsingleton.elim _ _) fun _ ↦
+  DFunLike.ext _ _ fun x ↦ (isEmpty_or_nonempty ι).elim (by subsingleton) fun _ ↦
     x.induction_on fun i g ↦ by simp
 
 lemma map_comp [IsDirected ι (· ≤ ·)]
@@ -499,7 +499,7 @@ lemma map_comp [IsDirected ι (· ≤ ·)]
       rw [AddMonoidHom.comp_assoc, hg₁ i, ← AddMonoidHom.comp_assoc, hg₂ i,
         AddMonoidHom.comp_assoc] :
       DirectLimit G f →+ DirectLimit G'' f'') :=
-  DFunLike.ext _ _ fun x ↦ (isEmpty_or_nonempty ι).elim (fun _ ↦ Subsingleton.elim _ _) fun _ ↦
+  DFunLike.ext _ _ fun x ↦ (isEmpty_or_nonempty ι).elim (by subsingleton) fun _ ↦
     x.induction_on fun i g ↦ by simp
 
 /--

Mathlib/Algebra/Group/Units.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.Group.Commute.Defs
 import Mathlib.Logic.Unique
 import Mathlib.Tactic.Nontriviality
 import Mathlib.Tactic.Lift
+import Mathlib.Tactic.Subsingleton
 
 #align_import algebra.group.units from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"
 
@@ -672,7 +673,7 @@ theorem isUnit_iff_exists_and_exists [Monoid M] {a : M} :
 
 @[to_additive (attr := nontriviality)]
 theorem isUnit_of_subsingleton [Monoid M] [Subsingleton M] (a : M) : IsUnit a :=
-  ⟨⟨a, a, Subsingleton.elim _ _, Subsingleton.elim _ _⟩, rfl⟩
+  ⟨⟨a, a, by subsingleton, by subsingleton⟩, rfl⟩
 #align is_unit_of_subsingleton isUnit_of_subsingleton
 #align is_add_unit_of_subsingleton isAddUnit_of_subsingleton
 
@@ -683,7 +684,7 @@ instance [Monoid M] : CanLift M Mˣ Units.val IsUnit :=
 /-- A subsingleton `Monoid` has a unique unit. -/
 @[to_additive "A subsingleton `AddMonoid` has a unique additive unit."]
 instance [Monoid M] [Subsingleton M] : Unique Mˣ where
-  uniq a := Units.val_eq_one.mp <| Subsingleton.elim (a : M) 1
+  uniq _ := Units.val_eq_one.mp (by subsingleton)
 
 @[to_additive (attr := simp)]
 protected theorem Units.isUnit [Monoid M] (u : Mˣ) : IsUnit (u : M) :=
@@ -735,8 +736,7 @@ lemma IsUnit.exists_left_inv {a : M} (h : IsUnit a) : ∃ b, b * a = 1 := by
 #align is_unit.pow IsUnit.pow
 #align is_add_unit.nsmul IsAddUnit.nsmul
 
-theorem units_eq_one [Unique Mˣ] (u : Mˣ) : u = 1 :=
-  Subsingleton.elim u 1
+theorem units_eq_one [Unique Mˣ] (u : Mˣ) : u = 1 := by subsingleton
 #align units_eq_one units_eq_one
 
 @[to_additive] lemma isUnit_iff_eq_one [Unique Mˣ] {x : M} : IsUnit x ↔ x = 1 :=

Mathlib/Algebra/Homology/HomologicalComplex.lean

@@ -317,8 +317,8 @@ theorem isZero_zero [HasZeroObject V] : IsZero (zero : HomologicalComplex V c) :
   refine ⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩
   all_goals
     ext
-    dsimp [zero]
-    apply Subsingleton.elim
+    dsimp only [zero]
+    subsingleton
 #align homological_complex.is_zero_zero HomologicalComplex.isZero_zero
 
 instance [HasZeroObject V] : HasZeroObject (HomologicalComplex V c) :=

Mathlib/Algebra/Lie/Engel.lean

@@ -166,8 +166,7 @@ theorem LieAlgebra.isEngelian_of_subsingleton [Subsingleton L] : LieAlgebra.IsEn
   intro M _i1 _i2 _i3 _i4 _h
   use 1
   suffices (⊤ : LieIdeal R L) = ⊥ by simp [this]
-  haveI := (LieSubmodule.subsingleton_iff R L L).mpr inferInstance
-  apply Subsingleton.elim
+  subsingleton [(LieSubmodule.subsingleton_iff R L L).mpr inferInstance]
 #align lie_algebra.is_engelian_of_subsingleton LieAlgebra.isEngelian_of_subsingleton
 
 theorem Function.Surjective.isEngelian {f : L →ₗ⁅R⁆ L₂} (hf : Function.Surjective f)

Mathlib/Algebra/Order/Antidiag/Prod.lean

@@ -64,17 +64,17 @@ attribute [simp] mem_antidiagonal
 variable {A : Type*}
 
 /-- All `HasAntidiagonal` instances are equal -/
-instance [AddMonoid A] : Subsingleton (HasAntidiagonal A) :=
-  ⟨by
+instance [AddMonoid A] : Subsingleton (HasAntidiagonal A) where
+  allEq := by
     rintro ⟨a, ha⟩ ⟨b, hb⟩
     congr with n xy
-    rw [ha, hb]⟩
+    rw [ha, hb]
 
 -- The goal of this lemma is to allow to rewrite antidiagonal
 -- when the decidability instances obsucate Lean
 lemma hasAntidiagonal_congr (A : Type*) [AddMonoid A]
     [H1 : HasAntidiagonal A] [H2 : HasAntidiagonal A] :
-    H1.antidiagonal = H2.antidiagonal := by congr!; apply Subsingleton.elim
+    H1.antidiagonal = H2.antidiagonal := by congr!; subsingleton
 
 theorem swap_mem_antidiagonal [AddCommMonoid A] [HasAntidiagonal A] {n : A} {xy : A × A}:
     xy.swap ∈ antidiagonal n ↔ xy ∈ antidiagonal n := by

Mathlib/Algebra/PUnitInstances.lean

@@ -87,10 +87,10 @@ instance normalizedGCDMonoid : NormalizedGCDMonoid PUnit where
   normUnit_zero := rfl
   normUnit_mul := by intros; rfl
   normUnit_coe_units := by intros; rfl
-  gcd_dvd_left _ _ := ⟨unit, Subsingleton.elim _ _⟩
-  gcd_dvd_right _ _ := ⟨unit, Subsingleton.elim _ _⟩
-  dvd_gcd {_ _} _ _ _ := ⟨unit, Subsingleton.elim _ _⟩
-  gcd_mul_lcm _ _ := ⟨1, Subsingleton.elim _ _⟩
+  gcd_dvd_left _ _ := ⟨unit, by subsingleton⟩
+  gcd_dvd_right _ _ := ⟨unit, by subsingleton⟩
+  dvd_gcd {_ _} _ _ _ := ⟨unit, by subsingleton⟩
+  gcd_mul_lcm _ _ := ⟨1, by subsingleton⟩
   lcm_zero_left := by intros; rfl
   lcm_zero_right := by intros; rfl
   normalize_gcd := by intros; rfl
@@ -112,7 +112,7 @@ theorem norm_unit_eq {x : PUnit} : normUnit x = 1 :=
 #align punit.norm_unit_eq PUnit.norm_unit_eq
 
 instance canonicallyOrderedAddCommMonoid : CanonicallyOrderedAddCommMonoid PUnit where
-  exists_add_of_le {_ _} _ := ⟨unit, Subsingleton.elim _ _⟩
+  exists_add_of_le {_ _} _ := ⟨unit, by subsingleton⟩
   add_le_add_left _ _ _ _ := trivial
   le_self_add _ _ := trivial
 
@@ -150,23 +150,23 @@ instance instIsScalarTowerOfSMul [SMul R S] : IsScalarTower R S PUnit :=
 
 instance smulWithZero [Zero R] : SMulWithZero R PUnit where
   __ := PUnit.smul
-  smul_zero _ := Subsingleton.elim _ _
-  zero_smul _ := Subsingleton.elim _ _
+  smul_zero := by subsingleton
+  zero_smul := by subsingleton
 
 instance mulAction [Monoid R] : MulAction R PUnit where
   __ := PUnit.smul
-  one_smul _ := Subsingleton.elim _ _
-  mul_smul _ _ _ := Subsingleton.elim _ _
+  one_smul := by subsingleton
+  mul_smul := by subsingleton
 
 instance distribMulAction [Monoid R] : DistribMulAction R PUnit where
   __ := PUnit.mulAction
-  smul_zero _ := Subsingleton.elim _ _
-  smul_add _ _ _ := Subsingleton.elim _ _
+  smul_zero := by subsingleton
+  smul_add := by subsingleton
 
 instance mulDistribMulAction [Monoid R] : MulDistribMulAction R PUnit where
   __ := PUnit.mulAction
-  smul_mul _ _ _ := Subsingleton.elim _ _
-  smul_one _ := Subsingleton.elim _ _
+  smul_mul := by subsingleton
+  smul_one := by subsingleton
 
 instance mulSemiringAction [Semiring R] : MulSemiringAction R PUnit :=
   { PUnit.distribMulAction, PUnit.mulDistribMulAction with }
@@ -176,7 +176,7 @@ instance mulActionWithZero [MonoidWithZero R] : MulActionWithZero R PUnit :=
 
 instance module [Semiring R] : Module R PUnit where
   __ := PUnit.distribMulAction
-  add_smul _ _ _ := Subsingleton.elim _ _
-  zero_smul _ := Subsingleton.elim _ _
+  add_smul := by subsingleton
+  zero_smul := by subsingleton
 
 end PUnit

Mathlib/AlgebraicTopology/CechNerve.lean

@@ -378,12 +378,11 @@ def wideCospan.limitCone [Finite ι] (X : C) : LimitCone (wideCospan ι X) where
             cases f
             · cases i
               all_goals dsimp; simp
-            · dsimp
-              simp only [terminal.comp_from]
-              exact Subsingleton.elim _ _ } }
+            · simp only [Functor.const_obj_obj, Functor.const_obj_map, terminal.comp_from]
+              subsingleton } }
   isLimit :=
     { lift := fun s => Limits.Pi.lift fun j => s.π.app (some j)
-      fac := fun s j => Option.casesOn j (Subsingleton.elim _ _) fun j => limit.lift_π _ _
+      fac := fun s j => Option.casesOn j (by subsingleton) fun j => limit.lift_π _ _
       uniq := fun s f h => by
         dsimp
         ext j

Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

@@ -198,7 +198,7 @@ protected noncomputable def extraDegeneracy (Δ : SimplexCategory) :
     (shift (objEquiv _ _ f))
   s'_comp_ε := by
     dsimp
-    apply Subsingleton.elim
+    subsingleton
   s₀_comp_δ₁ := by
     dsimp
     ext1 x

Mathlib/CategoryTheory/Filtered/Basic.lean

@@ -97,9 +97,7 @@ class IsFiltered extends IsFilteredOrEmpty C : Prop where
 instance (priority := 100) isFilteredOrEmpty_of_semilatticeSup (α : Type u) [SemilatticeSup α] :
     IsFilteredOrEmpty α where
   cocone_objs X Y := ⟨X ⊔ Y, homOfLE le_sup_left, homOfLE le_sup_right, trivial⟩
-  cocone_maps X Y f g := ⟨Y, 𝟙 _, by
-    apply ULift.ext
-    apply Subsingleton.elim⟩
+  cocone_maps X Y f g := ⟨Y, 𝟙 _, by subsingleton⟩
 #align category_theory.is_filtered_or_empty_of_semilattice_sup CategoryTheory.isFilteredOrEmpty_of_semilatticeSup
 
 instance (priority := 100) isFiltered_of_semilatticeSup_nonempty (α : Type u) [SemilatticeSup α]
@@ -111,9 +109,7 @@ instance (priority := 100) isFilteredOrEmpty_of_directed_le (α : Type u) [Preor
   cocone_objs X Y :=
     let ⟨Z, h1, h2⟩ := exists_ge_ge X Y
     ⟨Z, homOfLE h1, homOfLE h2, trivial⟩
-  cocone_maps X Y f g := ⟨Y, 𝟙 _, by
-    apply ULift.ext
-    apply Subsingleton.elim⟩
+  cocone_maps X Y f g := ⟨Y, 𝟙 _, by subsingleton⟩
 #align category_theory.is_filtered_or_empty_of_directed_le CategoryTheory.isFilteredOrEmpty_of_directed_le
 
 instance (priority := 100) isFiltered_of_directed_le_nonempty (α : Type u) [Preorder α]
@@ -126,10 +122,8 @@ example (α : Type u) [SemilatticeSup α] [OrderBot α] : IsFiltered α := by in
 example (α : Type u) [SemilatticeSup α] [OrderTop α] : IsFiltered α := by infer_instance
 
 instance : IsFiltered (Discrete PUnit) where
-  cocone_objs X Y := ⟨⟨PUnit.unit⟩, ⟨⟨by trivial⟩⟩, ⟨⟨Subsingleton.elim _ _⟩⟩, trivial⟩
-  cocone_maps X Y f g := ⟨⟨PUnit.unit⟩, ⟨⟨by trivial⟩⟩, by
-    apply ULift.ext
-    apply Subsingleton.elim⟩
+  cocone_objs X Y := ⟨⟨PUnit.unit⟩, ⟨⟨by trivial⟩⟩, ⟨⟨by subsingleton⟩⟩, trivial⟩
+  cocone_maps X Y f g := ⟨⟨PUnit.unit⟩, ⟨⟨by trivial⟩⟩, by subsingleton⟩
 
 namespace IsFiltered
 
@@ -568,7 +562,7 @@ instance (priority := 100) isCofilteredOrEmpty_of_semilatticeInf (α : Type u) [
   cone_objs X Y := ⟨X ⊓ Y, homOfLE inf_le_left, homOfLE inf_le_right, trivial⟩
   cone_maps X Y f g := ⟨X, 𝟙 _, by
     apply ULift.ext
-    apply Subsingleton.elim⟩
+    subsingleton⟩
 #align category_theory.is_cofiltered_or_empty_of_semilattice_inf CategoryTheory.isCofilteredOrEmpty_of_semilatticeInf
 
 instance (priority := 100) isCofiltered_of_semilatticeInf_nonempty (α : Type u) [SemilatticeInf α]
@@ -582,7 +576,7 @@ instance (priority := 100) isCofilteredOrEmpty_of_directed_ge (α : Type u) [Pre
     ⟨Z, homOfLE hX, homOfLE hY, trivial⟩
   cone_maps X Y f g := ⟨X, 𝟙 _, by
     apply ULift.ext
-    apply Subsingleton.elim⟩
+    subsingleton⟩
 #align category_theory.is_cofiltered_or_empty_of_directed_ge CategoryTheory.isCofilteredOrEmpty_of_directed_ge
 
 instance (priority := 100) isCofiltered_of_directed_ge_nonempty (α : Type u) [Preorder α]
@@ -595,10 +589,10 @@ example (α : Type u) [SemilatticeInf α] [OrderBot α] : IsCofiltered α := by
 example (α : Type u) [SemilatticeInf α] [OrderTop α] : IsCofiltered α := by infer_instance
 
 instance : IsCofiltered (Discrete PUnit) where
-  cone_objs X Y := ⟨⟨PUnit.unit⟩, ⟨⟨by trivial⟩⟩, ⟨⟨Subsingleton.elim _ _⟩⟩, trivial⟩
+  cone_objs X Y := ⟨⟨PUnit.unit⟩, ⟨⟨by trivial⟩⟩, ⟨⟨by subsingleton⟩⟩, trivial⟩
   cone_maps X Y f g := ⟨⟨PUnit.unit⟩, ⟨⟨by trivial⟩⟩, by
     apply ULift.ext
-    apply Subsingleton.elim⟩
+    subsingleton⟩
 
 namespace IsCofiltered
 

Mathlib/CategoryTheory/Filtered/Final.lean

@@ -182,7 +182,7 @@ theorem Functor.final_iff_of_isFiltered [IsFilteredOrEmpty C] :
   · intro d c s s'
     have : colimit.ι (F ⋙ coyoneda.obj (op d)) c s = colimit.ι (F ⋙ coyoneda.obj (op d)) c s' := by
       apply (Final.colimitCompCoyonedaIso F d).toEquiv.injective
-      exact Subsingleton.elim _ _
+      subsingleton
     obtain ⟨c', t₁, t₂, h⟩ := (Types.FilteredColimit.colimit_eq_iff.{v₁, v₁, v₁} _).mp this
     refine ⟨IsFiltered.coeq t₁ t₂, t₁ ≫ IsFiltered.coeqHom t₁ t₂, ?_⟩
     conv_rhs => rw [IsFiltered.coeq_condition t₁ t₂]

Mathlib/CategoryTheory/Functor/Flat.lean

@@ -218,7 +218,7 @@ noncomputable def preservesFiniteLimitsIffFlat [HasFiniteLimits C] (F : C ⥤ D)
     dsimp only [preservesFiniteLimitsOfPreservesFiniteLimitsOfSize]
     congr
     -- Porting note: this next line wasn't needed in lean 3
-    apply Subsingleton.elim
+    subsingleton
 
 #align category_theory.preserves_finite_limits_iff_flat CategoryTheory.preservesFiniteLimitsIffFlat
 
@@ -319,15 +319,15 @@ noncomputable def preservesFiniteLimitsIffLanPreservesFiniteLimits (F : C ⥤ D)
     -- indicates that it was doing the same as `dsimp only`
     dsimp only [preservesFiniteLimitsOfPreservesFiniteLimitsOfSize]; congr
     -- Porting note: next line wasn't necessary in lean 3
-    apply Subsingleton.elim
+    subsingleton
   right_inv x := by
     -- cases x; -- Porting note: not necessary in lean 4
     dsimp only [lanPreservesFiniteLimitsOfPreservesFiniteLimits,
       lanPreservesFiniteLimitsOfFlat,
       preservesFiniteLimitsOfPreservesFiniteLimitsOfSize]
     congr
     -- Porting note: next line wasn't necessary in lean 3
-    apply Subsingleton.elim
+    subsingleton
 set_option linter.uppercaseLean3 false in
 #align category_theory.preserves_finite_limits_iff_Lan_preserves_finite_limits CategoryTheory.preservesFiniteLimitsIffLanPreservesFiniteLimits