[Merged by Bors] - feat: FastSubsingleton and FastIsEmpty to speed up congr!/convert

Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean

@@ -972,6 +972,7 @@ variable {F K}
 
 lemma map_baseChange [Algebra F K] [IsScalarTower R F K] [Algebra F L] [IsScalarTower R F L]
     (χ : K →ₐ[F] L) (P : W⟮F⟯) : map W χ (baseChange W F K P) = baseChange W F L P := by
+  have : Subsingleton (F →ₐ[F] L) := inferInstance
   convert map_map W (Algebra.ofId F K) χ P
 
 end Point

Mathlib/Analysis/Calculus/ParametricIntegral.lean

@@ -106,8 +106,8 @@ theorem hasFDerivAt_integral_of_dominated_loc_of_lip' {F' : α → H →L[𝕜]
   /- Discard the trivial case where `E` is not complete, as all integrals vanish. -/
   by_cases hE : CompleteSpace E; swap
   · rcases subsingleton_or_nontrivial H with hH|hH
-    · convert hasFDerivAt_of_subsingleton _ _
-      exact hH
+    · have : Subsingleton (H →L[𝕜] E) := inferInstance
+      convert hasFDerivAt_of_subsingleton _ x₀
     · have : ¬(CompleteSpace (H →L[𝕜] E)) := by
         simpa [SeparatingDual.completeSpace_continuousLinearMap_iff] using hE
       simp only [integral, hE, ↓reduceDite, this]

Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

@@ -134,32 +134,32 @@ def isColimitOfPreserves (F : C ⥤ D) {c : Cocone K} (t : IsColimit c) [Preserv
 
 instance preservesLimit_subsingleton (K : J ⥤ C) (F : C ⥤ D) :
     Subsingleton (PreservesLimit K F) := by
-  constructor; rintro ⟨a⟩ ⟨b⟩; congr!
+  constructor; rintro ⟨a⟩ ⟨b⟩; congr!; apply Subsingleton.elim
 #align category_theory.limits.preserves_limit_subsingleton CategoryTheory.Limits.preservesLimit_subsingleton
 
 instance preservesColimit_subsingleton (K : J ⥤ C) (F : C ⥤ D) :
     Subsingleton (PreservesColimit K F) := by
-  constructor; rintro ⟨a⟩ ⟨b⟩; congr!
+  constructor; rintro ⟨a⟩ ⟨b⟩; congr!; apply Subsingleton.elim
 #align category_theory.limits.preserves_colimit_subsingleton CategoryTheory.Limits.preservesColimit_subsingleton
 
 instance preservesLimitsOfShape_subsingleton (J : Type w) [Category.{w'} J] (F : C ⥤ D) :
     Subsingleton (PreservesLimitsOfShape J F) := by
-  constructor; rintro ⟨a⟩ ⟨b⟩; congr!
+  constructor; rintro ⟨a⟩ ⟨b⟩; congr!; apply Subsingleton.elim
 #align category_theory.limits.preserves_limits_of_shape_subsingleton CategoryTheory.Limits.preservesLimitsOfShape_subsingleton
 
 instance preservesColimitsOfShape_subsingleton (J : Type w) [Category.{w'} J] (F : C ⥤ D) :
     Subsingleton (PreservesColimitsOfShape J F) := by
-  constructor; rintro ⟨a⟩ ⟨b⟩; congr!
+  constructor; rintro ⟨a⟩ ⟨b⟩; congr!; apply Subsingleton.elim
 #align category_theory.limits.preserves_colimits_of_shape_subsingleton CategoryTheory.Limits.preservesColimitsOfShape_subsingleton
 
 instance preserves_limits_subsingleton (F : C ⥤ D) :
     Subsingleton (PreservesLimitsOfSize.{w', w} F) := by
-  constructor; rintro ⟨a⟩ ⟨b⟩; congr; funext; congr!
+  constructor; rintro ⟨a⟩ ⟨b⟩; congr; funext; congr!; apply Subsingleton.elim
 #align category_theory.limits.preserves_limits_subsingleton CategoryTheory.Limits.preserves_limits_subsingleton
 
 instance preserves_colimits_subsingleton (F : C ⥤ D) :
     Subsingleton (PreservesColimitsOfSize.{w', w} F) := by
-  constructor; rintro ⟨a⟩ ⟨b⟩; congr; funext; congr!
+  constructor; rintro ⟨a⟩ ⟨b⟩; congr; funext; congr!; apply Subsingleton.elim
 #align category_theory.limits.preserves_colimits_subsingleton CategoryTheory.Limits.preserves_colimits_subsingleton
 
 instance idPreservesLimits : PreservesLimitsOfSize.{w', w} (𝟭 C) where
@@ -460,32 +460,32 @@ def isColimitOfReflects (F : C ⥤ D) {c : Cocone K} (t : IsColimit (F.mapCocone
 #align category_theory.limits.is_colimit_of_reflects CategoryTheory.Limits.isColimitOfReflects
 
 instance reflectsLimit_subsingleton (K : J ⥤ C) (F : C ⥤ D) : Subsingleton (ReflectsLimit K F) := by
-  constructor; rintro ⟨a⟩ ⟨b⟩; congr!
+  constructor; rintro ⟨a⟩ ⟨b⟩; congr!; apply Subsingleton.elim
 #align category_theory.limits.reflects_limit_subsingleton CategoryTheory.Limits.reflectsLimit_subsingleton
 
 instance
   reflectsColimit_subsingleton (K : J ⥤ C) (F : C ⥤ D) : Subsingleton (ReflectsColimit K F) := by
-  constructor; rintro ⟨a⟩ ⟨b⟩; congr!
+  constructor; rintro ⟨a⟩ ⟨b⟩; congr!; apply Subsingleton.elim
 #align category_theory.limits.reflects_colimit_subsingleton CategoryTheory.Limits.reflectsColimit_subsingleton
 
 instance reflectsLimitsOfShape_subsingleton (J : Type w) [Category.{w'} J] (F : C ⥤ D) :
     Subsingleton (ReflectsLimitsOfShape J F) := by
-  constructor; rintro ⟨a⟩ ⟨b⟩; congr!
+  constructor; rintro ⟨a⟩ ⟨b⟩; congr!; apply Subsingleton.elim
 #align category_theory.limits.reflects_limits_of_shape_subsingleton CategoryTheory.Limits.reflectsLimitsOfShape_subsingleton
 
 instance reflectsColimitsOfShape_subsingleton (J : Type w) [Category.{w'} J] (F : C ⥤ D) :
     Subsingleton (ReflectsColimitsOfShape J F) := by
-  constructor; rintro ⟨a⟩ ⟨b⟩; congr!
+  constructor; rintro ⟨a⟩ ⟨b⟩; congr!; apply Subsingleton.elim
 #align category_theory.limits.reflects_colimits_of_shape_subsingleton CategoryTheory.Limits.reflectsColimitsOfShape_subsingleton
 
 instance
   reflects_limits_subsingleton (F : C ⥤ D) : Subsingleton (ReflectsLimitsOfSize.{w', w} F) := by
-  constructor; rintro ⟨a⟩ ⟨b⟩; congr; funext; congr!
+  constructor; rintro ⟨a⟩ ⟨b⟩; congr; funext; congr!; apply Subsingleton.elim
 #align category_theory.limits.reflects_limits_subsingleton CategoryTheory.Limits.reflects_limits_subsingleton
 
 instance reflects_colimits_subsingleton (F : C ⥤ D) :
     Subsingleton (ReflectsColimitsOfSize.{w', w} F) := by
-  constructor; rintro ⟨a⟩ ⟨b⟩; congr; funext; congr!
+  constructor; rintro ⟨a⟩ ⟨b⟩; congr; funext; congr!; apply Subsingleton.elim
 #align category_theory.limits.reflects_colimits_subsingleton CategoryTheory.Limits.reflects_colimits_subsingleton
 
 -- see Note [lower instance priority]

Mathlib/CategoryTheory/Limits/Shapes/CommSq.lean

@@ -271,6 +271,7 @@ open ZeroObject
 theorem of_hasBinaryProduct [HasBinaryProduct X Y] [HasZeroObject C] [HasZeroMorphisms C] :
     IsPullback Limits.prod.fst Limits.prod.snd (0 : X ⟶ 0) (0 : Y ⟶ 0) := by
   convert @of_is_product _ _ X Y 0 _ (limit.isLimit _) HasZeroObject.zeroIsTerminal
+    <;> apply Subsingleton.elim
 #align category_theory.is_pullback.of_has_binary_product CategoryTheory.IsPullback.of_hasBinaryProduct
 
 variable {X Y}
@@ -403,6 +404,7 @@ open ZeroObject
 theorem of_hasBinaryCoproduct [HasBinaryCoproduct X Y] [HasZeroObject C] [HasZeroMorphisms C] :
     IsPushout (0 : 0 ⟶ X) (0 : 0 ⟶ Y) coprod.inl coprod.inr := by
   convert @of_is_coproduct _ _ 0 X Y _ (colimit.isColimit _) HasZeroObject.zeroIsInitial
+    <;> apply Subsingleton.elim
 #align category_theory.is_pushout.of_has_binary_coproduct CategoryTheory.IsPushout.of_hasBinaryCoproduct
 
 variable {X Y}
@@ -557,6 +559,7 @@ open ZeroObject
 theorem of_isBilimit {b : BinaryBicone X Y} (h : b.IsBilimit) :
     IsPullback b.fst b.snd (0 : X ⟶ 0) (0 : Y ⟶ 0) := by
   convert IsPullback.of_is_product' h.isLimit HasZeroObject.zeroIsTerminal
+    <;> apply Subsingleton.elim
 #align category_theory.is_pullback.of_is_bilimit CategoryTheory.IsPullback.of_isBilimit
 
 @[simp]
@@ -769,6 +772,7 @@ open ZeroObject
 theorem of_isBilimit {b : BinaryBicone X Y} (h : b.IsBilimit) :
     IsPushout (0 : 0 ⟶ X) (0 : 0 ⟶ Y) b.inl b.inr := by
   convert IsPushout.of_is_coproduct' h.isColimit HasZeroObject.zeroIsInitial
+    <;> apply Subsingleton.elim
 #align category_theory.is_pushout.of_is_bilimit CategoryTheory.IsPushout.of_isBilimit
 
 @[simp]

Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean

@@ -548,7 +548,7 @@ theorem hasZeroObject_of_hasInitial_object [HasZeroMorphisms C] [HasInitial C] :
   refine' ⟨⟨⊥_ C, fun X => ⟨⟨⟨0⟩, by aesop_cat⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩⟩⟩
   calc
     f = f ≫ 𝟙 _ := (Category.comp_id _).symm
-    _ = f ≫ 0 := by congr!
+    _ = f ≫ 0 := by congr!; apply Subsingleton.elim
     _ = 0 := HasZeroMorphisms.comp_zero _ _
 #align category_theory.limits.has_zero_object_of_has_initial_object CategoryTheory.Limits.hasZeroObject_of_hasInitial_object
 
@@ -558,7 +558,7 @@ theorem hasZeroObject_of_hasTerminal_object [HasZeroMorphisms C] [HasTerminal C]
   refine' ⟨⟨⊤_ C, fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨0⟩, by aesop_cat⟩⟩⟩⟩
   calc
     f = 𝟙 _ ≫ f := (Category.id_comp _).symm
-    _ = 0 ≫ f := by congr!
+    _ = 0 ≫ f := by congr!; apply Subsingleton.elim
     _ = 0 := zero_comp
 #align category_theory.limits.has_zero_object_of_has_terminal_object CategoryTheory.Limits.hasZeroObject_of_hasTerminal_object
 

Mathlib/CategoryTheory/Limits/Shapes/ZeroObjects.lean

@@ -268,6 +268,7 @@ instance {X : C} (f : X ⟶ 0) : Epi f where left_cancellation g h _ := by ext
 
 instance zero_to_zero_isIso (f : (0 : C) ⟶ 0) : IsIso f := by
   convert show IsIso (𝟙 (0 : C)) by infer_instance
+  apply Subsingleton.elim
 #align category_theory.limits.has_zero_object.zero_to_zero_is_iso CategoryTheory.Limits.HasZeroObject.zero_to_zero_isIso
 
 /-- A zero object is in particular initial. -/

Mathlib/CategoryTheory/Limits/VanKampen.lean

@@ -764,6 +764,7 @@ theorem isPullback_initial_to_of_cofan_isVanKampen [HasInitial C] {ι : Type*} {
     Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
   clear_value f
   subst this
+  have : ∀ i, Subsingleton (⊥_ C ⟶ (Discrete.functor f).obj i) := inferInstance
   convert isPullback_of_cofan_isVanKampen hc i.as j.as
   exact (if_neg (mt (Discrete.ext _ _) hi.symm)).symm
 

Mathlib/CategoryTheory/Preadditive/Biproducts.lean

@@ -671,11 +671,11 @@ instance subsingleton_preadditive_of_hasBinaryBiproducts {C : Type u} [Category.
   allEq := fun a b => by
     apply Preadditive.ext; funext X Y; apply AddCommGroup.ext; funext f g
     have h₁ := @biprod.add_eq_lift_id_desc _ _ a _ _ f g
-      (by convert (inferInstance : HasBinaryBiproduct X X))
+      (by convert (inferInstance : HasBinaryBiproduct X X); apply Subsingleton.elim)
     have h₂ := @biprod.add_eq_lift_id_desc _ _ b _ _ f g
-      (by convert (inferInstance : HasBinaryBiproduct X X))
+      (by convert (inferInstance : HasBinaryBiproduct X X); apply Subsingleton.elim)
     refine' h₁.trans (Eq.trans _ h₂.symm)
-    congr!
+    congr! 2 <;> apply Subsingleton.elim
 #align category_theory.subsingleton_preadditive_of_has_binary_biproducts CategoryTheory.subsingleton_preadditive_of_hasBinaryBiproducts
 
 end

Mathlib/CategoryTheory/Sites/CoverLifting.lean

@@ -179,7 +179,7 @@ theorem getSection_commute {Y Z : StructuredArrow (op U) G.op} (f : Y ⟶ Z) :
   apply getSection_is_unique
   intro V' fV' hV'
   have eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op := by
-    convert f.w
+    convert f.w using 1
     erw [Category.id_comp]
   rw [eq] at hV'
   convert getSection_isAmalgamation ℱ hS hx Y (fV' ≫ f.right.unop) _ using 1

Mathlib/Data/Finset/Antidiagonal.lean

@@ -75,7 +75,7 @@ instance [AddMonoid A] : Subsingleton (HasAntidiagonal A) :=
 -- 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!
+    H1.antidiagonal = H2.antidiagonal := by congr!; apply Subsingleton.elim
 
 theorem swap_mem_antidiagonal [AddCommMonoid A] [HasAntidiagonal A] {n : A} {xy : A × A}:
     xy.swap ∈ antidiagonal n ↔ xy ∈ antidiagonal n := by

Mathlib/Data/Fintype/Basic.lean

@@ -439,6 +439,8 @@ instance subsingleton (α : Type*) : Subsingleton (Fintype α) :=
   ⟨fun ⟨s₁, h₁⟩ ⟨s₂, h₂⟩ => by congr; simp [Finset.ext_iff, h₁, h₂]⟩
 #align fintype.subsingleton Fintype.subsingleton
 
+instance (α : Type*) : Lean.Meta.FastSubsingleton (Fintype α) := {}
+
 /-- Given a predicate that can be represented by a finset, the subtype
 associated to the predicate is a fintype. -/
 protected def subtype {p : α → Prop} (s : Finset α) (H : ∀ x : α, x ∈ s ↔ p x) :

Mathlib/Lean/Meta/CongrTheorems.lean

@@ -5,6 +5,7 @@ Authors: Kyle Miller
 -/
 import Lean.Meta.Tactic.Cleanup
 import Mathlib.Lean.Meta
+import Mathlib.Logic.IsEmpty
 
 /-!
 # Additions to `Lean.Meta.CongrTheorems`
@@ -90,6 +91,79 @@ where
     -- We have no more tricks.
     failure
 
+universe u v
+
+/-- A version of `Subsingleton` with few instances. It should fail fast. -/
+class FastSubsingleton (α : Sort u) : Prop where
+  /-- The subsingleton instance. -/
+  [inst : Subsingleton α]
+
+/-- A version of `IsEmpty` with few instances. It should fail fast. -/
+class FastIsEmpty (α : Sort u) : Prop where
+  [inst : IsEmpty α]
+
+protected theorem FastSubsingleton.elim {α : Sort u} [h : FastSubsingleton α] : (a b : α) → a = b :=
+  h.inst.allEq
+
+instance (priority := 100) {α : Type u} [inst : FastIsEmpty α] : FastSubsingleton α where
+  inst := have := inst.inst; inferInstance
+
+instance {p : Prop} : FastSubsingleton p := {}
+
+instance {p : Prop} : FastSubsingleton (Decidable p) := {}
+
+instance : FastSubsingleton (Fin 1) := {}
+
+instance : FastSubsingleton PUnit := {}
+
+instance : FastIsEmpty Empty := {}
+
+instance : FastIsEmpty False := {}
+
+instance : FastIsEmpty (Fin 0) := {}
+
+instance {α : Sort u} [inst : FastIsEmpty α] {β : (x : α) → Sort v} :
+    FastSubsingleton ((x : α) → β x) where
+  inst.allEq _ _ := funext fun a => (inst.inst.false a).elim
+
+instance {α : Sort u} {β : (x : α) → Sort v} [inst : ∀ x, FastSubsingleton (β x)] :
+    FastSubsingleton ((x : α) → β x) where
+  inst := have := λ x => (inst x).inst; inferInstance
+
+/--
+Runs `mx` in a context where all local `Subsingleton` and `IsEmpty` instances
+have associated `FastSubsingleton` and `FastIsEmpty` instances.
+The function passed to `mx` eliminates these instances from expressions,
+since they are only locally valid inside this context.
+-/
+def withSubsingletonAsFast {α : Type} [Inhabited α] (mx : (Expr → Expr) → MetaM α) : MetaM α := do
+  let insts1 := (← getLocalInstances).filter fun inst => inst.className == ``Subsingleton
+  let insts2 := (← getLocalInstances).filter fun inst => inst.className == ``IsEmpty
+  let mkInst (f : Name) (inst : Expr) : MetaM Expr := do
+    forallTelescopeReducing (← inferType inst) fun args _ => do
+      mkLambdaFVars args <| ← mkAppOptM f #[none, mkAppN inst args]
+  let vals := (← insts1.mapM fun inst => mkInst ``FastSubsingleton.mk inst.fvar)
+    ++ (← insts2.mapM fun inst => mkInst ``FastIsEmpty.mk inst.fvar)
+  let tys ← vals.mapM inferType
+  withLocalDeclsD (tys.map fun ty => (`inst, fun _ => pure ty)) fun args =>
+    withNewLocalInstances args 0 do
+      let elim (e : Expr) : Expr := e.replaceFVars args vals
+      mx elim
+
+/-- Like `subsingletonElim` but uses `FastSubsingleton` to fail fast. -/
+def fastSubsingletonElim (mvarId : MVarId) : MetaM Bool :=
+  mvarId.withContext do
+    let res ← observing? do
+      mvarId.checkNotAssigned `fastSubsingletonElim
+      let tgt ← withReducible mvarId.getType'
+      let some (_, lhs, rhs) := tgt.eq? | failure
+      -- Note: `mkAppM` uses `withNewMCtxDepth`, which prevents `Sort _` from specializing to `Prop`
+      let pf ← withSubsingletonAsFast fun elim =>
+        elim <$> mkAppM ``FastSubsingleton.elim #[lhs, rhs]
+      mvarId.assign pf
+      return true
+    return res.getD false
+
 /--
 `mkRichHCongr fType funInfo fixedFun fixedParams forceHEq`
 create a congruence lemma to prove that `Eq/HEq (f a₁ ... aₙ) (f' a₁' ... aₙ')`.
@@ -267,7 +341,7 @@ where
     if ← mvarId.proofIrrelHeq then return
     -- Make the goal be an eq and then try `Subsingleton.elim`
     let mvarId ← mvarId.heqOfEq
-    if ← mvarId.subsingletonElim then return
+    if ← fastSubsingletonElim mvarId then return
     -- We have no more tricks.
     throwError "was not able to solve for proof"
   /-- Driver for `trySolveCore`. -/

Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean

@@ -71,6 +71,7 @@ theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂
       = (associated (R := A) Q₁).tmul (associated (R := R) Q₂) := by
   rw [QuadraticForm.tmul, tensorDistrib, BilinForm.tmul]
   dsimp
+  have : Subsingleton (Invertible (2 : A)) := inferInstance
   convert associated_left_inverse A ((associated_isSymm A Q₁).tmul (associated_isSymm R Q₂))
 
 theorem polarBilin_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) :

Mathlib/MeasureTheory/Integral/Lebesgue.lean

@@ -630,7 +630,9 @@ theorem lintegral_zero_measure {m : MeasurableSpace α} (f : α → ℝ≥0∞)
 
 @[simp]
 theorem lintegral_of_isEmpty {α} [MeasurableSpace α] [IsEmpty α] (μ : Measure α) (f : α → ℝ≥0∞) :
-    ∫⁻ x, f x ∂μ = 0 := by convert lintegral_zero_measure f
+    ∫⁻ x, f x ∂μ = 0 := by
+  have : Subsingleton (Measure α) := inferInstance
+  convert lintegral_zero_measure f
 
 theorem set_lintegral_empty (f : α → ℝ≥0∞) : ∫⁻ x in ∅, f x ∂μ = 0 := by
   rw [Measure.restrict_empty, lintegral_zero_measure]

Mathlib/NumberTheory/Cyclotomic/Basic.lean

@@ -154,6 +154,7 @@ theorem trans (C : Type w) [CommRing C] [Algebra A C] [Algebra B C] [IsScalarTow
 
 @[nontriviality]
 theorem subsingleton_iff [Subsingleton B] : IsCyclotomicExtension S A B ↔ S = { } ∨ S = {1} := by
+  have : Subsingleton (Subalgebra A B) := inferInstance
   constructor
   · rintro ⟨hprim, -⟩
     rw [← subset_singleton_iff_eq]

Mathlib/Order/Birkhoff.lean

@@ -249,7 +249,7 @@ variable [DecidableEq α]
 
 @[simp] lemma birkhoffSet_apply (a : α) :
     birkhoffSet a = OrderIso.lowerSetSupIrred a := by
-  simp [birkhoffSet]; convert rfl
+  simp [birkhoffSet]; have : Subsingleton (OrderBot α) := inferInstance; convert rfl
 
 end OrderEmbedding
 

Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

@@ -291,6 +291,7 @@ theorem int_cyclotomic_unique {n : ℕ} {P : ℤ[X]} (h : map (Int.castRingHom 
 theorem map_cyclotomic (n : ℕ) {R S : Type*} [Ring R] [Ring S] (f : R →+* S) :
     map f (cyclotomic n R) = cyclotomic n S := by
   rw [← map_cyclotomic_int n R, ← map_cyclotomic_int n S, map_map]
+  have : Subsingleton (ℤ →+* S) := inferInstance
   congr!
 #align polynomial.map_cyclotomic Polynomial.map_cyclotomic
 

Mathlib/RingTheory/UniqueFactorizationDomain.lean

@@ -1487,6 +1487,7 @@ theorem prod_factors [Nontrivial α] (s : FactorSet α) : s.prod.factors = s :=
 
 @[nontriviality]
 theorem factors_subsingleton [Subsingleton α] {a : Associates α} : a.factors = ⊤ := by
+  have : Subsingleton (Associates α) := inferInstance
   convert factors_zero
 #align associates.factors_subsingleton Associates.factors_subsingleton