mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The tensor product of two isomorphisms is an isomorphism.  -/
CategoryTheory.MonoidalCategory.tensorIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y X' Y' : C} →
        (X ≅ Y) →
          (X' ≅ Y') →
            (CategoryTheory.MonoidalCategoryStruct.tensorObj X X' ≅
              CategoryTheory.MonoidalCategoryStruct.tensorObj Y Y')
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} [inst_1 : SizeOf C]
  (obj : (X : Cᵒᵖ) → ModuleCat ↑(R.obj X))
  (map : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → obj X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (obj Y))
  (map_id :
    autoParam
      (∀ (X : Cᵒᵖ),
        map (CategoryTheory.CategoryStruct.id X) =
          (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.id X))) ⋯).inv.app
            (obj X))
      PresheafOfModules.map_id._autoParam)
  (map_comp :
    autoParam
      (∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
        map (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (map f)
            (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (map g))
              ((ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                      (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.comp f g))) ⋯).inv.app
                (obj Z))))
      PresheafOfModules.map_comp._autoParam),
  sizeOf { obj := obj, map := map, map_id := map_id, map_comp := map_comp } = 1
-- Mathlib.Tactic.Ring.Common
/-- This cache contains data required by the `ring` tactic during execution.  -/
Mathlib.Tactic.Ring.Common.Cache : {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Type
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.refl_partialEquiv : ∀ {X : Type u_1} [inst : TopologicalSpace X], (PartialHomeomorph.refl X).toPartialEquiv = PartialEquiv.refl X
-- Mathlib.Algebra.Ring.Subring.Basic
/-- Closure of a subring `S` equals `S`.  -/
Subring.closure_eq : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R), Subring.closure ↑s = s
-- Mathlib.Order.Cofinal
/-- A cofinal subset of a cofinal subset is cofinal.  -/
IsCofinal.trans : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {t : Set ↑s}, IsCofinal s → IsCofinal t → IsCofinal (Subtype.val '' t)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roo_add_right_eq_map : ∀ {m n : ℤ}, (m<...m + 1 + n).toList = List.map (fun x => x + m + 1) (0...n).toList
-- Mathlib.Topology.LocallyClosed
coborder_inter_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, coborder s ∩ closure s = s
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.IsPerfPair.ext_iff : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_5} {inst : AddCommGroup M} {inst_1 : AddCommGroup N} {inst_2 : CommRing R}
  {inst_3 : Module R M} {inst_4 : Module R N} {p : M →ₗ[R] N →ₗ[R] R} {x y : p.IsPerfPair}, x = y ↔ True
-- Mathlib.Algebra.Group.Basic
neg_sub_left : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a b : α), -a - b = -(b + a)
-- Mathlib.Algebra.Module.Torsion.Basic
/-- The `a`-torsion submodule as an `(R ⧸ R ∙ a)`-module.  -/
Submodule.instModuleQuotientTorsionBy : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (a : R) → Module (R ⧸ R ∙ a) ↥(Submodule.torsionBy R M a)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_middle : Bool →
  Lean.Grind.AC.Seq →
    Lean.Grind.AC.Seq → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstrProof
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- **Alias** of `IsAlgClosed.surjective_domRestrict_of_isAlgebraic`.

---

If E/L/K is a tower of field extensions with E/L algebraic, and if M is an algebraically
closed extension of K, then any embedding of L/K into M/K extends to an embedding of E/K.
Known as the extension lemma in https://math.stackexchange.com/a/687914.  -/
IsAlgClosed.surjective_restrictDomain_of_isAlgebraic : ∀ {K : Type u} [inst : Field K] {L : Type v} {M : Type w} [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : Field M]
  [inst_4 : Algebra K M] [IsAlgClosed M] {E : Type u_1} [inst_6 : Field E] [inst_7 : Algebra K E] [inst_8 : Algebra L E]
  [inst_9 : IsScalarTower K L E] [Algebra.IsAlgebraic L E], Function.Surjective fun φ => AlgHom.domRestrict L φ
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0` and `+` is an additive group, if it admits a
surjective map that preserves `0` and `+` to an additive group.  -/
Function.Surjective.addGroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₂] →
      [inst_1 : Zero M₂] →
        [inst_2 : SMul ℕ M₂] →
          [inst_3 : Neg M₂] →
            [inst_4 : Sub M₂] →
              [inst_5 : SMul ℤ M₂] →
                [inst_6 : AddGroup M₁] →
                  (f : M₁ → M₂) →
                    Function.Surjective f →
                      f 0 = 0 →
                        (∀ (x y : M₁), f (x + y) = f x + f y) →
                          (∀ (x : M₁), f (-x) = -f x) →
                            (∀ (x y : M₁), f (x - y) = f x - f y) →
                              (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) →
                                (∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) → AddGroup M₂
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
/-- Construct limit data for a binary product in `AddGrpCat`, using `AddGrpCat.of (G × H)`  -/
AddGrpCat.binaryProductLimitCone : (G H : AddGrpCat) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair G H)
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- Simple graphs contain a copy of a `completeEquipartiteGraph (r + 1) t` iff there exists
`s : Finset V` of size `#s = t` and `K : G.CompleteEquipartiteSubgraph r t` such that the
vertices in `s` are adjacent to the vertices in `K`.  -/
SimpleGraph.completeEquipartiteGraph_succ_isContained_iff : ∀ {V : Type u_1} {G : SimpleGraph V} {r t : ℕ},
  (SimpleGraph.completeEquipartiteGraph (r + 1) t).IsContained G ↔
    ∃ K s, s.card = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
_private.Mathlib.AlgebraicGeometry.Morphisms.Flat.0.CategoryTheory.Pairwise.diagramMap.match_1.eq_4 : ∀ {ι : Type u_1} (motive : (x x_1 : CategoryTheory.Pairwise ι) → (x ⟶ x_1) → Sort u_2) (i j : ι)
  (h_1 :
    (i : ι) →
      motive (CategoryTheory.Pairwise.single i) (CategoryTheory.Pairwise.single i)
        (CategoryTheory.Pairwise.Hom.id_single i))
  (h_2 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.pair i j)
        (CategoryTheory.Pairwise.Hom.id_pair i j))
  (h_3 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single i)
        (CategoryTheory.Pairwise.Hom.left i j))
  (h_4 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single j)
        (CategoryTheory.Pairwise.Hom.right i j)),
  (match CategoryTheory.Pairwise.pair i j, CategoryTheory.Pairwise.single j, CategoryTheory.Pairwise.Hom.right i j with
    | .(CategoryTheory.Pairwise.single i), .(CategoryTheory.Pairwise.single i),
      CategoryTheory.Pairwise.Hom.id_single i => h_1 i
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.pair i j),
      CategoryTheory.Pairwise.Hom.id_pair i j => h_2 i j
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.single i), CategoryTheory.Pairwise.Hom.left i j =>
      h_3 i j
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.single j), CategoryTheory.Pairwise.Hom.right i j =>
      h_4 i j) =
    h_4 i j
-- Mathlib.Algebra.Group.Units.Basic
AddLeftCancelMonoid.add_eq_zero : ∀ {α : Type u} [inst : AddLeftCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α}, a + b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.lintegral_nnnorm_le : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] (μ : MeasureTheory.Measure X) {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] (f : BoundedContinuousFunction X E), ∫⁻ (x : X), ↑‖f x‖₊ ∂μ ≤ ↑‖f‖₊ * μ Set.univ
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.neg : {R : Type u_1} →
  [inst : Ring R] →
    {R₂ : Type u_2} →
      [inst_1 : Ring R₂] →
        {M : Type u_4} →
          [inst_2 : TopologicalSpace M] →
            [inst_3 : AddCommGroup M] →
              {M₂ : Type u_5} →
                [inst_4 : TopologicalSpace M₂] →
                  [inst_5 : AddCommGroup M₂] →
                    [inst_6 : Module R M] →
                      [inst_7 : Module R₂ M₂] → {σ₁₂ : R →+* R₂} → [IsTopologicalAddGroup M₂] → Neg (M →SL[σ₁₂] M₂)
-- Mathlib.Analysis.Calculus.Implicit
/-- The function given by `x ↦ (leftFun x, rightFun x)`.  -/
ImplicitFunctionData.prodFun : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [inst_3 : CompleteSpace E] →
            {F : Type u_3} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : CompleteSpace F] →
                    {G : Type u_4} →
                      [inst_7 : NormedAddCommGroup G] →
                        [inst_8 : NormedSpace 𝕜 G] →
                          [inst_9 : CompleteSpace G] → ImplicitFunctionData 𝕜 E F G → E → F × G
-- Mathlib.Tactic.Sat.FromLRAT
/-- A macro for producing SAT proofs from CNF / LRAT files.
These files are commonly used in the SAT community for writing proofs.

The input to the `from_lrat` term syntax is two string expressions with
the statement (written in CNF format) and the proof (in LRAT format).
For example:
```
def foo := from_lrat
  "p cnf 2 4  1 2 0  -1 2 0  1 -2 0  -1 -2 0"
  "5 -2 0 4 3 0  5 d 3 4 0  6 1 0 5 1 0  6 d 1 0  7 0 5 2 6 0"
```
produces a theorem:
```
foo : ∀ (a a_1 : Prop), (¬a ∧ ¬a_1 ∨ a ∧ ¬a_1) ∨ ¬a ∧ a_1 ∨ a ∧ a_1
```

* You can use this term after `have :=` or in `def foo :=` to produce the term
  without constraining the type.
* You can use it when a specific type is expected, but it currently does not
  pay any attention to the shape of the goal and always produces the same theorem,
  so you can only use this to do alpha renaming.
* You can use the `include_str` macro in place of the two strings
  to load CNF / LRAT files from disk.
 -/
Mathlib.Tactic.Sat.termFrom_lrat___ : Lean.ParserDescr
-- Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
MonoidAlgebra.instIsLeftCancelMulZeroOfIsCancelAddOfUniqueProds : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [IsCancelAdd R] [IsLeftCancelMulZero R] [inst_3 : Mul A]
  [UniqueProds A], IsLeftCancelMulZero (MonoidAlgebra R A)
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- We say that a function `f : ℂ → E` is integrable on the circle with center `c` and radius `R` if
the function `f ∘ circleMap c R` is integrable on `[0, 2π]`.

Note that the actual function used in the definition of `circleIntegral` is
`(deriv (circleMap c R) θ) • f (circleMap c R θ)`. Integrability of this function is equivalent
to integrability of `f ∘ circleMap c R` whenever `R ≠ 0`.  -/
CircleIntegrable : {E : Type u_1} → [NormedAddCommGroup E] → (ℂ → E) → ℂ → ℝ → Prop
-- Init.Data.BitVec.Bitblast
/-- Subtracting `x` from the all ones bitvector is equivalent to taking its complement  -/
BitVec.allOnes_sub_eq_not : ∀ {w : ℕ} (x : BitVec w), BitVec.allOnes w - x = ~~~x
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.FixPoint.merge : Lean.FVarIdSet → Lean.FVarIdSet → Lean.Elab.Term.MutualClosure.FixPoint.M Lean.FVarIdSet
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
PositiveLinearMap.gnsNonUnitalStarAlgHom.eq_1 : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] (f : A →ₚ[ℂ] ℂ)
  [inst_2 : StarOrderedRing A],
  f.gnsNonUnitalStarAlgHom =
    { toFun := fun a => (f.leftMulMapPreGNS a).completion, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯,
      map_star' := ⋯ }
-- Mathlib.Topology.Algebra.Order.Group
LinearOrderedAddCommGroup.toIsTopologicalAddGroup : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [inst_2 : LinearOrder G] [IsOrderedAddMonoid G]
  [OrderTopology G], IsTopologicalAddGroup G
-- Batteries.Data.Float.Basic
/-- Calculates the number of trailing bits in a `UInt64`. Requires `v ≠ 0`.  -/
Float.toRatParts'.trailingZeros : UInt64 → UInt8 → UInt8
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.rightInvOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), Set.RightInvOn (↑e.symm) (↑e) e.target
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- In the space `ℝ`, the Hausdorff measure coincides exactly with the Lebesgue measure.  -/
MeasureTheory.hausdorffMeasure_real : MeasureTheory.Measure.hausdorffMeasure 1 = MeasureTheory.volume
-- Mathlib.NumberTheory.ModularForms.Derivative
/-- Serre derivative is equivariant under the slash action. More precisely,
$\partial_k (F ∣[k] γ) = (\partial_k F) ∣[k + 2] \gamma$ for all $\gamma \in SL(2, \mathbb{Z})$.
 -/
Derivative.serreDerivative_slash_equivariant : ∀ {k : ℤ} {F : UpperHalfPlane → ℂ},
  MDiff F →
    ∀ {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ},
      SlashAction.map (k + 2) γ (Derivative.serreDerivative (↑k) F) =
        Derivative.serreDerivative (↑k) (SlashAction.map k γ F)
-- Mathlib.Lean.Expr.Basic
/-- Return `some n` if `e` is one of the following
- a nat literal (numeral)
- `Nat.zero`
- `Nat.succ x` where `isNumeral x`
- `OfNat.ofNat _ x _` where `isNumeral x`  -/
Lean.Expr.numeral? : Lean.Expr → Option ℕ
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.inv_j : ∀ {n : Type u_1} {R : Type u₂} [inst : CommRing R] (t : Matrix.TransvectionStruct n R), t.inv.j = t.j
-- Mathlib.Data.Num.Lemmas
PosNum.size.eq_2 : ∀ (n : PosNum), n.bit0.size = n.size.succ
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.sparsePairs.eq_1 : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : DecidableEq α] {A : Finset α}
  (P : Finpartition A) (G : SimpleGraph α) [inst_3 : DecidableRel G.Adj] (ε : 𝕜),
  P.sparsePairs G ε =
    {x ∈ P.parts.offDiag |
      match x with
      | (u, v) => ↑(G.edgeDensity u v) < ε}
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
FreeSimplexQuiver.homRel.δ_comp_σ_of_gt : ∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)},
  j.castSucc < i →
    FreeSimplexQuiver.homRel
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i.succ))
        ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ j.castSucc)))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ j))
        ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i)))
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.restrictedYonedaObj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A)
  (s : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ),
  (CategoryTheory.OverPresheafAux.restrictedYonedaObj η).obj s =
    CategoryTheory.OverPresheafAux.OverArrows η (Opposite.unop s).hom
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.instInhabitedDecreasingBy.default : Lean.Elab.DecreasingBy
-- Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
/-- If `s` has the unique differential property, `f` is differentiable on `s` and its derivative
at every point of `s` has dense range, then `f '' s` has the unique differential property.  -/
UniqueMDiffOn.image_denseRange : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {s : Set M},
  UniqueMDiff[s] → ∀ {f : M → M'}, MDiff[s] f → (∀ x ∈ s, DenseRange ⇑(mfderiv[s] f x)) → UniqueMDiff[f '' s]
-- Init.Data.List.Lemmas
List.getD.eq_1 : ∀ {α : Type u_1} (as : List α) (i : ℕ) (fallback : α), as.getD i fallback = as[i]?.getD fallback
-- Mathlib.RingTheory.Localization.Integral
/-- If `R → S` is an integral extension, `M` is a submonoid of `R`,
`Rₘ` is the localization of `R` at `M`,
and `Sₘ` is the localization of `S` at the image of `M` under the extension map,
then the induced map `Rₘ → Sₘ` is also an integral extension  -/
isIntegral_localization : ∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {Rₘ : Type u_3} {Sₘ : Type u_4} [inst_3 : CommRing Rₘ] [inst_4 : CommRing Sₘ] [inst_5 : Algebra R Rₘ]
  [inst_6 : IsLocalization M Rₘ] [inst_7 : Algebra S Sₘ] [inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
  [Algebra.IsIntegral R S], (IsLocalization.map Sₘ (algebraMap R S) ⋯).IsIntegral
-- Mathlib.CategoryTheory.Core
CategoryTheory.Iso.coreComp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor C D} (α : F ≅ G) (β : G ≅ H), (α ≪≫ β).core = α.core ≪≫ β.core
-- Lean.PrettyPrinter
/-- Pretty-prints a declaration `c` as `c.{<levels>} <params> : <type>`.  -/
Lean.PrettyPrinter.ppSignature : Lean.Name → Lean.MetaM Lean.FormatWithInfos
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey!_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.maxKey! ∈ t
-- Init.Grind.Module.Basic
Lean.Grind.AddCommMonoid.toZero : {M : Type u} → [self : Lean.Grind.AddCommMonoid M] → Zero M
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Linear equivalence between linear maps `M₂ →ₗ[R] M₃`
and one-multilinear maps `MultilinearMap R (fun _ : ι ↦ M₂) M₃`.  -/
MultilinearMap.ofSubsingletonₗ : (R : Type uR) →
  (S : Type uS) →
    {ι : Type uι} →
      (M₂ : Type v₂) →
        (M₃ : Type v₃) →
          [inst : Semiring R] →
            [inst_1 : AddCommMonoid M₂] →
              [inst_2 : Module R M₂] →
                [inst_3 : Semiring S] →
                  [inst_4 : AddCommMonoid M₃] →
                    [inst_5 : Module S M₃] →
                      [inst_6 : Module R M₃] →
                        [inst_7 : SMulCommClass R S M₃] →
                          [Subsingleton ι] → ι → (M₂ →ₗ[R] M₃) ≃ₗ[S] MultilinearMap R (fun x => M₂) M₃
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_left_split_dvd_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → ℤ → Bool
-- Mathlib.Analysis.Convex.Side
Affine.Simplex.wSameSide_affineSpan_faceOpposite_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {n : ℕ}
  [inst_6 : NeZero n] (s : Affine.Simplex R P n) {w₁ w₂ : Fin (n + 1) → R},
  ∑ j, w₁ j = 1 →
    ∑ j, w₂ j = 1 →
      ∀ {i : Fin (n + 1)},
        (affineSpan R (Set.range (s.faceOpposite i).points)).WSameSide
            ((Finset.affineCombination R Finset.univ s.points) w₁)
            ((Finset.affineCombination R Finset.univ s.points) w₂) ↔
          SignType.sign (w₁ i) = SignType.sign (w₂ i) ∨ w₁ i = 0 ∨ w₂ i = 0
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.binomial_spec : ∀ {α : Type u_1} {f : α → ℕ} {a b : α} [inst : DecidableEq α],
  a ≠ b → (f a).factorial * (f b).factorial * Nat.multinomial {a, b} f = (f a + f b).factorial
-- Init.Data.Int.DivMod.Lemmas
Int.sub_mul_bmod_self_left : ∀ (a : ℤ) (b : ℕ) (c : ℤ), (a - ↑b * c).bmod b = a.bmod b
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_5 : HSub Std.Time.Nanosecond.Offset Std.Time.Week.Offset Std.Time.Nanosecond.Offset
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.snd_one : ∀ {ι : Type u_1} (A : ι → Type u_2) [inst : Zero ι] [inst_1 : GradedMonoid.GOne A], Sigma.snd 1 = GradedMonoid.GOne.one
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.coeff_single_smul_vadd : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : PartialOrder Γ']
  [inst_2 : VAdd Γ Γ'] [inst_3 : IsOrderedCancelVAdd Γ Γ'] [inst_4 : AddCommMonoid V] [inst_5 : MulZeroClass R]
  [inst_6 : SMulWithZero R V] {r : R} {x : HahnModule Γ' R V} {a : Γ'} {b : Γ},
  ((HahnModule.of R).symm ((HahnSeries.single b) r • x)).coeff (b +ᵥ a) = r • ((HahnModule.of R).symm x).coeff a
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.hasTrivialRadical_of_no_solvable_ideals : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  (∀ (I : LieIdeal R L), LieAlgebra.IsSolvable ↥I → I = ⊥) → LieAlgebra.HasTrivialRadical R L
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
      {A : C} →
        (toPrepathObject : HomotopicalAlgebra.PrepathObject A) →
          autoParam (HomotopicalAlgebra.WeakEquivalence toPrepathObject.ι)
              HomotopicalAlgebra.PathObject.weakEquivalence_ι._autoParam →
            HomotopicalAlgebra.PathObject A
-- Mathlib.Topology.AlexandrovDiscrete
nhdsKer_subset_iff_mem_nhdsSet : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {s t : Set α}, nhdsKer s ⊆ t ↔ t ∈ nhdsSet s
-- Lean.Data.Name
Lean.Name.cmp : Lean.Name → Lean.Name → Ordering
-- Mathlib.Topology.MetricSpace.Bounded
Metric.isBounded_Icc : ∀ {α : Type u} [inst : PseudoMetricSpace α] [inst_1 : Preorder α] [CompactIccSpace α] (a b : α),
  Bornology.IsBounded (Set.Icc a b)
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.theta_one : Chebyshev.theta 1 = 0
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
/-- The topology of compact convergence on `E →L[𝕜] F`.  -/
CompactConvergenceCLM : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (𝕜₁ →+* 𝕜₂) →
          (E : Type u_4) →
            (F : Type u_5) →
              [inst_2 : AddCommGroup E] →
                [Module 𝕜₁ E] →
                  [inst : AddCommGroup F] →
                    [Module 𝕜₂ F] → [TopologicalSpace E] → [TopologicalSpace F] → Type (max u_4 u_5)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.eval_X : ∀ {K : Type u} [inst : Field K] {L : Type u} [inst_1 : Field L] (f : K →+* L) (a : L), RatFunc.eval f a RatFunc.X = a
-- Lean.Data.Lsp.Client
Lean.Lsp.Registration.id : Lean.Lsp.Registration → String
-- Mathlib.GroupTheory.Divisible
/-- A `Monoid A` is `α`-rootable iff the `pow _ n` function is surjective, i.e. the constructive version
implies the textbook approach.
 -/
rootableByOfPowLeftSurj : (A : Type u_1) →
  (α : Type u_2) →
    [inst : Monoid A] →
      [inst_1 : Pow A α] → [inst_2 : Zero α] → (∀ {n : α}, n ≠ 0 → Function.Surjective fun a => a ^ n) → RootableBy A α
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.lTensor_comp_mapL : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] {A : Type u_6} [inst_9 : NormedAddCommGroup A]
  [inst_10 : InnerProductSpace 𝕜 A] (f : E →L[𝕜] F) (g₁ : G →L[𝕜] H) (g₂ : A →L[𝕜] G),
  ContinuousLinearMap.lTensor F g₁ ∘SL TensorProduct.mapL f g₂ = TensorProduct.mapL f (g₁ ∘SL g₂)
-- Mathlib.Data.Complex.Basic
Complex.mul_inv_cancel : ∀ {z : ℂ}, z ≠ 0 → z * z⁻¹ = 1