mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Filter.tendsto_of_seq_tendsto : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {k : Filter α} {l : Filter β} [k.IsCountablyGenerated],
  (∀ (x : ℕ → α), Filter.Tendsto x Filter.atTop k → Filter.Tendsto (f ∘ x) Filter.atTop l) → Filter.Tendsto f k l
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_hom' : ∀ {ι : Type u_2} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (s : Multiset ι)
  {F : Type u_8} [inst_2 : FunLike F M N] [AddMonoidHomClass F M N] (f : F) (g : ι → M),
  (Multiset.map (fun i => f (g i)) s).sum = f (Multiset.map g s).sum
-- Mathlib.Data.Nat.GCD.Basic
Nat.div_lcm_eq_div_gcd : ∀ {n m k : ℕ}, m ∣ k → n ∣ k → (k / m).lcm (k / n) = k / m.gcd n
-- Mathlib.GroupTheory.OrderOfElement
mod_addOrderOf_zsmul : ∀ {G : Type u_1} [inst : AddGroup G] (x : G) (z : ℤ), (z % ↑(addOrderOf x)) • x = z • x
-- Mathlib.Algebra.Group.End
Equiv.inv_mulLeft : ∀ {α : Type u_4} [inst : Group α] (a : α), (Equiv.mulLeft a)⁻¹ = Equiv.mulLeft a⁻¹
-- Mathlib.Data.Set.Lattice
Set.iUnion₂_mono : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s t : (i : ι) → κ i → Set α},
  (∀ (i : ι) (j : κ i), s i j ⊆ t i j) → ⋃ i, ⋃ j, s i j ⊆ ⋃ i, ⋃ j, t i j
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.anyM.match_1.splitter : (motive : Bool → Sort u_1) → (__do_lift : Bool) → (Unit → motive true) → (Unit → motive false) → motive __do_lift
-- Mathlib.RingTheory.Valuation.LocalSubring
bijective_rangeRestrict_comp_of_valuationRing : ∀ {R : Type u_1} {S : Type u_2} {K : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Field K]
  [inst_3 : IsDomain R] [ValuationRing R] [IsLocalRing S] [inst_6 : Algebra R K] [IsFractionRing R K] (f : R →+* S)
  (g : S →+* K), g.comp f = algebraMap R K → ∀ [IsLocalHom f], Function.Bijective ⇑(g.rangeRestrict.comp f)
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.FredholmPackage.eq_equiv : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] {u : E →L[𝕜] F} (self : u.FredholmPackage),
  u = self.decCodom.X₁.subtypeL ∘SL ↑self.equiv ∘SL self.decDom.proj
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
/-- In this version of the lemma, the inclusion homs `iUV` can be specified directly by the user,
which can be more convenient in practice.
 -/
TopCat.Sheaf.existsUnique_gluing' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.HasLimitsOfSize.{x, x, v_1, u_1} C] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] {X : TopCat}
  (F : TopCat.Sheaf C X) {ι : Type u_4} (U : ι → TopologicalSpace.Opens ↑X) (V : TopologicalSpace.Opens ↑X)
  (iUV : (i : ι) → U i ⟶ V),
  V ≤ iSup U →
    ∀ (sf : (i : ι) → CategoryTheory.ToType (F.obj.obj (Opposite.op (U i)))),
      TopCat.Presheaf.IsCompatible F.obj U sf →
        ∃! s, ∀ (i : ι), (CategoryTheory.ConcreteCategory.hom (F.obj.map (iUV i).op)) s = sf i
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
Finset.centroid.eq_1 : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (p : ι → P),
  Finset.centroid k s p = (Finset.affineCombination k s p) (Finset.centroidWeights k s)
-- Mathlib.Data.EReal.Basic
EReal.preimage_coe_Ioo_bot_top : Real.toEReal ⁻¹' Set.Ioo ⊥ ⊤ = Set.univ
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAdd.eq_1 : ∀ {α : Type u_1} [inst : Add α], Lex.instAdd = inst
-- Mathlib.Data.List.Basic
List.replicate_left_injective : ∀ {α : Type u} (a : α), Function.Injective fun x => List.replicate x a
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
/-- The **Gelfand transform** is an algebra homomorphism (over `𝕜`) from a topological `𝕜`-algebra
`A` into the `𝕜`-algebra of continuous `𝕜`-valued functions on the `characterSpace 𝕜 A`.
The character space itself consists of all algebra homomorphisms from `A` to `𝕜`.  -/
WeakDual.gelfandTransform : (𝕜 : Type u_1) →
  (A : Type u_2) →
    [inst : CommRing 𝕜] →
      [NoZeroDivisors 𝕜] →
        [inst_2 : TopologicalSpace 𝕜] →
          [inst_3 : IsTopologicalRing 𝕜] →
            [inst_4 : TopologicalSpace A] →
              [inst_5 : Semiring A] → [inst_6 : Algebra 𝕜 A] → A →ₐ[𝕜] C(↑(WeakDual.characterSpace 𝕜 A), 𝕜)
-- Mathlib.Algebra.Ring.Semiconj
SemiconjBy.sub_right : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {a x y x' y' : R},
  SemiconjBy a x y → SemiconjBy a x' y' → SemiconjBy a (x - x') (y - y')
-- Mathlib.RingTheory.Polynomial.HilbertPoly
/-- For any field `F` and natural numbers `d` and `k`, `Polynomial.preHilbertPoly F d k`
is defined as `(d.factorial : F)⁻¹ • ((ascPochhammer F d).comp (X - (C (k : F)) + 1))`.
This is the most basic form of Hilbert polynomials. `Polynomial.preHilbertPoly ℚ d 0`
is exactly the Hilbert polynomial of the polynomial ring `ℚ[X_0,...,X_d]` viewed as
a graded module over itself. In fact, `Polynomial.preHilbertPoly F d k` is the
same as `Polynomial.hilbertPoly ((X : F[X]) ^ k) (d + 1)` for any field `F` and
`d k : ℕ` (see the lemma `Polynomial.hilbertPoly_X_pow_succ`). See also the lemma
`Polynomial.preHilbertPoly_eq_choose_sub_add`, which states that if `CharZero F`,
then for any `d k n : ℕ` with `k ≤ n`, `(Polynomial.preHilbertPoly F d k).eval (n : F)`
equals `(n - k + d).choose d`.
 -/
Polynomial.preHilbertPoly : (F : Type u_1) → [inst : Field F] → ℕ → ℕ → Polynomial F
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.lift.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : IsAdicComplete I N]
  (f f_1 : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤) (e_f : f = f_1)
  (h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m),
  IsAdicComplete.lift I f h = IsAdicComplete.lift I f_1 ⋯
-- Mathlib.Order.Filter.Pointwise
Filter.HasBasis.div : ∀ {α : Type u_2} [inst : Div α] {f g : Filter α} {ιf : Type u_7} {ιg : Type u_8} {pf : ιf → Prop} {sf : ιf → Set α}
  {pg : ιg → Prop} {sg : ιg → Set α},
  f.HasBasis pf sf → g.HasBasis pg sg → (f / g).HasBasis (fun i => pf i.1 ∧ pg i.2) fun i => sf i.1 / sg i.2
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- The global section functor for `𝒪_{Spec R}` modules  -/
AlgebraicGeometry.moduleSpecΓFunctor : {R : CommRingCat} → CategoryTheory.Functor (AlgebraicGeometry.Spec (CommRingCat.of ↑R)).Modules (ModuleCat ↑R)
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
ContDiffWithinAt.exp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E}
  {n : WithTop ℕ∞}, ContDiffWithinAt ℝ n f s x → ContDiffWithinAt ℝ n (fun x => Real.exp (f x)) s x
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.isIso_toPlus_of_isSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  (P : CategoryTheory.Functor Cᵒᵖ D) [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D],
  CategoryTheory.Presheaf.IsSheaf J P → CategoryTheory.IsIso (J.toPlus P)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.snd_equivOfRightInverse : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_3} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {M₂ : Type u_4} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂]
  [inst_7 : IsTopologicalAddGroup M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : Function.RightInverse ⇑f₂ ⇑f₁) (x : M),
  ↑((ContinuousLinearEquiv.equivOfRightInverse f₁ f₂ h) x).2 = x - f₂ (f₁ x)
-- Mathlib.Order.Grade
covBy_iff_lt_covBy_grade : ∀ {𝕆 : Type u_1} {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : Preorder α] [inst_2 : GradeOrder 𝕆 α] {a b : α},
  a ⋖ b ↔ a < b ∧ grade 𝕆 a ⋖ grade 𝕆 b
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivativeFinsupp_C : ∀ {R : Type u} [inst : Semiring R] (r : R), Polynomial.derivativeFinsupp (Polynomial.C r) = fun₀ | 0 => Polynomial.C r
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
Lean.Meta.Grind.Arith.CommRing.getNatCastFn : {m : Type → Type} →
  [MonadLiftT Lean.MetaM m] →
    [Monad m] → [Lean.Meta.Sym.Arith.MonadCanon m] → [Lean.Meta.Grind.Arith.CommRing.MonadRing m] → m Lean.Expr
-- Mathlib.Tactic.Order.Preprocessing
Mathlib.Tactic.Order.le_of_not_lt_le : ∀ {α : Type u} [inst : Preorder α] {x y : α}, ¬x < y → x ≤ y → y ≤ x
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.mk : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} →
          (pt : C) →
            (π : (j : J) → pt ⟶ F j) →
              (ι : (j : J) → F j ⟶ pt) →
                autoParam
                    (∀ (j j' : J),
                      CategoryTheory.CategoryStruct.comp (ι j) (π j') =
                        if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
                    CategoryTheory.Limits.Bicone.ι_π._autoParam →
                  CategoryTheory.Limits.Bicone F
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Balanced.dec : {α : Type u_1} → DecidablePred Ordnode.Balanced
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.cast_toNat_of_aleph0_le : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → ↑(Cardinal.toNat c) = 0
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.isValueTransition : Lean.Meta.Match.Problem → Bool
-- Mathlib.Algebra.Module.Submodule.Defs
/-- The actual `Submodule` obtained from an element of a `SMulMemClass` and `AddSubmonoidClass`.  -/
Submodule.ofClass : {S : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : SetLike S M] → [AddSubmonoidClass S M] → [SMulMemClass S R M] → S → Submodule R M
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.CofanMapObjFun.ιMapObj_iso_inv_assoc : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  {X : CategoryTheory.GradedObject I C} {p : I → J} {j : J} [inst_1 : X.HasMap p] {c : X.CofanMapObjFun p j}
  (hc : CategoryTheory.Limits.IsColimit c) (i : I) (hi : p i = j) {Z : C} (h : c.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hi)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.CofanMapObjFun.iso hc).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj c ⟨i, hi⟩) h
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
/-- A functor `D ⥤ HomologicalComplex C c` preserves limits of shape `J`
if for any `i`, `G ⋙ eval C c i` does.  -/
HomologicalComplex.preservesLimitsOfShape_of_eval : ∀ {C : Type u_1} {ι : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u_4} [inst_3 : CategoryTheory.Category.{v_3, u_4} D]
  (G : CategoryTheory.Functor D (HomologicalComplex C c)),
  (∀ (i : ι), CategoryTheory.Limits.PreservesLimitsOfShape J (G.comp (HomologicalComplex.eval C c i))) →
    CategoryTheory.Limits.PreservesLimitsOfShape J G
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.rat_ofNat_smul_1 : ∀ {d : ℕ} {R : Type u_3} {A : Type u_4} [inst : Field R] [inst_1 : Field A] [inst_2 : Algebra R A] {a : A}
  [inst_3 : d.AtLeastTwo], (-1 / OfNat.ofNat d) • a = -1 / OfNat.ofNat d * a
-- Mathlib.Data.Set.Insert
Set.empty_ssubset_singleton : ∀ {α : Type u_1} {a : α}, ∅ ⊂ {a}
-- Lean.Data.Lsp.Basic
/-- Changes to existing resources.  -/
Lean.Lsp.WorkspaceEdit.changes? : Lean.Lsp.WorkspaceEdit → Option (Std.TreeMap Lean.Lsp.DocumentUri Lean.Lsp.TextEditBatch compare)
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
List.cycleOf_formPerm : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α},
  l.Nodup → 2 ≤ l.length → ∀ (x : { x // x ∈ l }), l.attach.formPerm.cycleOf x = l.attach.formPerm
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
/-- An arbitrarily chosen index such that `V ≤ U i`.
 -/
TopCat.Presheaf.SheafCondition.OpensLeCover.index : {X : TopCat} → {ι : Type u_2} → {U : ι → TopologicalSpace.Opens ↑X} → TopCat.Presheaf.SheafCondition.OpensLeCover U → ι
-- Mathlib.Topology.Separation.Hausdorff
/-- The universal property of the largest T2 quotient of a topological space `X`: any continuous
map from `X` to a T2 space `Y` uniquely factors through `T2Quotient X`. This declaration builds the
factored map. Its continuity is `T2Quotient.continuous_lift`, the fact that it indeed factors the
original map is `T2Quotient.lift_mk` and uniqueness is `T2Quotient.unique_lift`.  -/
T2Quotient.lift : {X : Type u_3} →
  {Y : Type u_4} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → [T2Space Y] → {f : X → Y} → Continuous f → T2Quotient X → Y
-- Mathlib.Data.Num.Basic
/-- The absolute value of a `ZNum` as a `Num`.  -/
ZNum.abs : ZNum → Num
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.canonical_H : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.RightHomologyData.canonical S).H = S.homology
-- Mathlib.Order.Lattice
ULift.instSemilatticeInf.eq_1 : ∀ {α : Type u} [inst : SemilatticeInf α],
  ULift.instSemilatticeInf = Function.Injective.semilatticeInf ULift.down ⋯ ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Localization.Prod
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁.congr_simp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ W₂_1 : CategoryTheory.MorphismProperty C₂} (e_W₂ : W₂ = W₂_1) {E : Type u₅}
  [inst_2 : CategoryTheory.Category.{v₅, u₅} E] (F F_1 : CategoryTheory.Functor (C₁ × C₂) E) (e_F : F = F_1)
  [inst_3 : W₂.ContainsIdentities] (hF : (W₁.prod W₂).IsInvertedBy F),
  CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁ F hF =
    CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁ F_1 ⋯
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Submodule.toLinearMap_orthogonalProjectionOnto_eq_projectionOnto : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection], ↑K.orthogonalProjectionOnto = K.projectionOnto Kᗮ ⋯
-- Init.Data.Array.Count
Array.countP_replicate : ∀ {α : Type u_1} {p : α → Bool} {a : α} {n : ℕ}, Array.countP p (Array.replicate n a) = if p a = true then n else 0
-- Init.Prelude
instDecidableNot : {p : Prop} → [dp : Decidable p] → Decidable ¬p
-- Mathlib.Order.Heyting.Basic
himp_le_himp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b c d : α}, a ≤ b → c ≤ d → b ⇨ c ≤ a ⇨ d
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The circumcenter of a simplex.  -/
Affine.Simplex.circumcenter : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] → [inst_3 : NormedAddTorsor V P] → {n : ℕ} → Affine.Simplex ℝ P n → P
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.nnnorm_inr : ∀ {R : Type u_3} {M : Type u_4} [inst : SeminormedRing R] [inst_1 : SeminormedAddCommGroup M] (m : M),
  ‖TrivSqZeroExt.inr m‖₊ = ‖m‖₊
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
DerivedCategory.triangleOfSESδ.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact),
  DerivedCategory.triangleOfSESδ hS = DerivedCategory.triangleOfSESδ hS
-- Mathlib.CategoryTheory.MarkovCategory.Positive
CategoryTheory.PositiveCategory.toMarkovCategory : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      [self : CategoryTheory.PositiveCategory C] → CategoryTheory.MarkovCategory C
-- Mathlib.Util.Notation3
/-- Given an expression, generate a matcher for it.
The `boundFVars` hash map records which state variables certain fvars correspond to.
The `localFVars` hash map records which local variable the matcher should use for an exact
expression match.

If it succeeds generating a matcher, returns
1. a list of keys that should be used for the `delab` attribute
   when defining the elaborator
2. a `Term` that represents a `Matcher` for the given expression `e`.  -/
Mathlib.Notation3.exprToMatcher : Std.HashMap Lean.FVarId Lean.Name →
  Std.HashMap Lean.FVarId Lean.Term →
    Lean.Expr → OptionT Lean.Elab.TermElabM (List Mathlib.Notation3.DelabKey × Lean.Term)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsEquivalenceOfRingEquiv_additive : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (e : R ≃+* S),
  (ModuleCat.restrictScalarsEquivalenceOfRingEquiv e).functor.Additive
-- Init.Data.String.Pattern.Basic
/-- Provides simple pattern matching capabilities from the end of a `Slice`.
 -/
String.Slice.Pattern.BackwardPattern : {ρ : Type} → ρ → Type
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.finTwoArrow_apply : ∀ (α : Type u_4) [inst : UniformSpace α], ⇑(UniformEquiv.finTwoArrow α) = fun f => (f 0, f 1)
-- Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Matrix.IsHermitian.cfc.eq_1 : ∀ {n : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n 𝕜}
  (hA : A.IsHermitian) (f : ℝ → ℝ),
  hA.cfc f =
    ((Unitary.conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary)
      (Matrix.diagonal (RCLike.ofReal ∘ f ∘ hA.eigenvalues))
-- Lean.DocString.Parser
Lean.Doc.Parser.BlockCtxt.mk.sizeOf_spec : ∀ (minIndent : ℕ) (maxDirective : Option ℕ) (inLists : List Lean.Doc.Parser.InList) (docStartPosition : Lean.Position)
  (baseColumn : ℕ),
  sizeOf
      { minIndent := minIndent, maxDirective := maxDirective, inLists := inLists, docStartPosition := docStartPosition,
        baseColumn := baseColumn } =
    1 + sizeOf minIndent + sizeOf maxDirective + sizeOf inLists + sizeOf docStartPosition + sizeOf baseColumn
-- Mathlib.Tactic.Translate.Core
/-- If `changeNumeral := true`, then try to translate the number `1` to `0`.  -/
Mathlib.Tactic.Translate.TranslateData.changeNumeral : Mathlib.Tactic.Translate.TranslateData → Bool
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_subtypeCongr : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {p : α → Prop} [inst_2 : DecidablePred p]
  (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a }),
  Equiv.Perm.sign (ep.subtypeCongr en) = Equiv.Perm.sign ep * Equiv.Perm.sign en
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- Since the vector space is empty the ring is commutative.  -/
CliffordAlgebraRing.instCommRingCliffordAlgebraUnitOfNatQuadraticForm : {R : Type u_1} → [inst : CommRing R] → CommRing (CliffordAlgebra 0)
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsAddTorsion.extension_closed`.

---

Torsion additive groups are closed under extensions.  -/
AddIsTorsion.extension_closed : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] {N : AddSubgroup G} [inst_1 : AddGroup H] {f : G →+ H},
  N = f.ker → IsAddTorsion H → IsAddTorsion ↥N → IsAddTorsion G
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.rename_comp_expand : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (p : ℕ) (f : σ → τ),
  (MvPolynomial.rename f).comp (MvPolynomial.expand p) = (MvPolynomial.expand p).comp (MvPolynomial.rename f)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.sin_mul_sum_sin : ∀ (n : ℕ) (a b : ℝ),
  Real.sin (a / 2) * ∑ i ∈ Finset.range n, Real.sin (a * ↑i + b) =
    Real.sin (↑n * a / 2) * Real.sin ((↑n - 1) * a / 2 + b)
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.bot_eq_top_iff_isEmpty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], ⊥ = ⊤ ↔ IsEmpty C
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.indexing_modeTarget_ : Lean.ParserDescr
-- Init.Data.Char.Lemmas
Char.ne_of_lt : ∀ {a b : Char}, a < b → a ≠ b
-- Aesop.Builder.Unfold
Aesop.RuleBuilder.unfold : Aesop.RuleBuilder
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.integral_eq_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ↥(α →₁ₛ[μ] ℝ)},
  0 ≤ᵐ[μ] ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) →
    MeasureTheory.L1.SimpleFunc.integral f =
      (∫⁻ (a : α), ENNReal.ofReal ((MeasureTheory.Lp.simpleFunc.toSimpleFunc f) a) ∂μ).toReal
-- Mathlib.Logic.Equiv.Defs
Equiv.permCongr_refl : ∀ {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β'), e.permCongr (Equiv.refl α') = Equiv.refl β'
-- Init.Data.BitVec.Lemmas
BitVec.umod_self : ∀ {w : ℕ} {x : BitVec w}, x % x = 0#w
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.instIsFilteredForall : ∀ {α : Type w} {I : α → Type u₁} [inst : (i : α) → CategoryTheory.Category.{v₁, u₁} (I i)]
  [∀ (i : α), CategoryTheory.IsFiltered (I i)], CategoryTheory.IsFiltered ((i : α) → I i)
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.MonadicityInternal.counitCofork_pt : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (B : D),
  (CategoryTheory.Monad.MonadicityInternal.counitCofork adj B).pt = B
-- Mathlib.RingTheory.Finiteness.Defs
/-- A submodule of `M` is finitely generated if it is the span of a finite subset of `M`.  -/
Submodule.FG : {R : Type u_1} →
  {M : Type u_2} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → Prop
-- Init.PropLemmas
forall_eq_or_imp' : ∀ {α : Sort u_1} {P Q : α → Prop} {a' : α}, (∀ (a : α), a' = a ∨ Q a → P a) ↔ P a' ∧ ∀ (a : α), Q a → P a
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Config.mk : ℕ → Lean.Meta.Sym.DSimp.Config
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart_def : ∀ {α : Type u_2} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α),
  μ.singularPart ν = if h : μ.HaveLebesgueDecomposition ν then (Classical.choose ⋯).1 else 0
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mk'.sizeOf_spec : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : SizeOf ι] [inst_2 : (a : ι) → SizeOf (β a)]
  (toFun : (i : ι) → β i) (support' : Trunc { s // ∀ (i : ι), i ∈ s ∨ toFun i = 0 }),
  sizeOf { toFun := toFun, support' := support' } = 1 + sizeOf support'
-- Mathlib.Algebra.Polynomial.OfFn
/-- `ofFn n v` is the polynomial whose coefficients are the entries of the vector `v`.  -/
Polynomial.ofFn : {R : Type u_1} → [inst : Semiring R] → [DecidableEq R] → (n : ℕ) → (Fin n → R) →ₗ[R] Polynomial R
-- Mathlib.Data.Sign.Defs
SignType.noConfusionType : Sort v✝ → SignType → SignType → Sort v✝
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
/-- Turning `p : Submodule R M` into an `S`-submodule gives the same module structure
as turning it into a type and adding a module structure.  -/
Submodule.restrictScalarsEquiv : (S : Type u_1) →
  (R : Type u_2) →
    (M : Type u_3) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Semiring S] →
            [inst_3 : Module S M] →
              [inst_4 : Module R M] →
                [inst_5 : SMul S R] →
                  [inst_6 : IsScalarTower S R M] → (p : Submodule R M) → ↥(Submodule.restrictScalars S p) ≃ₗ[R] ↥p