mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.mk.injEq : ∀ {R : Type u} [inst : NonAssocSemiring R] (toSubmonoid : Submonoid R)
  (add_mem' : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier)
  (zero_mem' : 0 ∈ toSubmonoid.carrier) (toSubmonoid_1 : Submonoid R)
  (add_mem'_1 : ∀ {a b : R}, a ∈ toSubmonoid_1.carrier → b ∈ toSubmonoid_1.carrier → a + b ∈ toSubmonoid_1.carrier)
  (zero_mem'_1 : 0 ∈ toSubmonoid_1.carrier),
  ({ toSubmonoid := toSubmonoid, add_mem' := add_mem', zero_mem' := zero_mem' } =
      { toSubmonoid := toSubmonoid_1, add_mem' := add_mem'_1, zero_mem' := zero_mem'_1 }) =
    (toSubmonoid = toSubmonoid_1)
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- A continuous surjective monoid homomorphism of topological groups with compact codomain
is measure preserving, provided that the Haar measures on the domain and on the codomain
have the same total mass.
 -/
MonoidHom.measurePreserving : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] {H : Type u_2} [inst_5 : Group H] [inst_6 : TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H]
  [inst_9 : MeasurableSpace H] [BorelSpace H] {μ : MeasureTheory.Measure G} [μ.IsHaarMeasure]
  {ν : MeasureTheory.Measure H} [ν.IsHaarMeasure] {f : G →* H},
  Continuous ⇑f → Function.Surjective ⇑f → μ Set.univ = ν Set.univ → MeasureTheory.MeasurePreserving (⇑f) μ ν
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableAt.isBigOTVS_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} [ContinuousAdd F] [ContinuousSMul 𝕜 F],
  DifferentiableAt 𝕜 f x → (fun x_1 => f x_1 - f x) =O[𝕜; nhds x] fun x_1 => x_1 - x
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.reorder.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.reorder c = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.reorder c_1 → c = c_1
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.Seq.endsWithVar : Lean.Grind.AC.Seq → Lean.Grind.AC.Var → Bool
-- Lean.Environment
_private.Lean.Environment.0.Lean.importModulesCore.go : Lean.OLeanLevel →
  Lean.NameMap Lean.ImportArtifacts → Bool → Array Lean.Import → Bool → Bool → Bool → Bool → Lean.ImportStateM Unit
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- A vector space is a model with corners, denoted as `𝓘(𝕜, E)` within the `Manifold` namespace.  -/
Manifold.«term𝓘(_,_)» : Lean.ParserDescr
-- Lean.Syntax
Lean.Syntax.TopDown.firstChoiceOnly : Lean.Syntax.TopDown → Bool
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_inv_Ioo : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  Inv.inv '' Set.Ioo a b = Set.Ioo b⁻¹ a⁻¹
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instVAddCommClass_1 : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst_1 : VAdd N α] [VAddCommClass M N α],
  VAddCommClass M Nᵒᵈ α
-- Lean.Meta.Tactic.Grind.Internalize
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.mkDefaultSplitInfo : Lean.Expr → Lean.Meta.Grind.GrindM Lean.Meta.Grind.SplitInfo
-- Init.Data.Array.Zip
Array.zipWith_self : ∀ {α : Type u_1} {δ : Type u_2} {f : α → α → δ} {xs : Array α}, Array.zipWith f xs xs = Array.map (fun a => f a a) xs
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.map_fst_toList_eq_keys : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → List.map Sigma.fst m.toList = m.keys
-- Mathlib.Logic.Equiv.Defs
Equiv.trans_apply : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ) (a : α), (f.trans g) a = g (f a)
-- Mathlib.Data.Sum.Interval
Sum.Lex.Ici_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderTop α]
  [inst_3 : Fintype β] [inst_4 : LocallyFiniteOrderTop β] (a : α),
  Finset.Ici (Sum.inlₗ a) = Finset.map toLex.toEmbedding ((Finset.Ici a).disjSum Finset.univ)
-- Mathlib.MeasureTheory.Measure.Prod
/-- Marginal measure on `α` obtained from a measure `ρ` on `α × β`, defined by `ρ.map Prod.fst`.  -/
MeasureTheory.Measure.fst : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] → [inst_1 : MeasurableSpace β] → MeasureTheory.Measure (α × β) → MeasureTheory.Measure α
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.liftPred_const_iff : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [l.NeBot] {p : β → Prop} {x : β}, Filter.Germ.LiftPred p ↑x ↔ p x
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toMeasure_apply_eq_one_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] (p : PMF α) {s : Set α},
  MeasurableSet s → (p.toMeasure s = 1 ↔ p.support ⊆ s)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.lift_iSup_lt_of_lt_cof : ∀ {β : Type v} {f : β → Ordinal.{u}} {a : Ordinal.{u}},
  Cardinal.lift.{u, v} (Cardinal.mk β) < (Ordinal.lift.{v, u} a).cof → (∀ (i : β), f i < a) → ⨆ i, f i < a
-- Mathlib.Data.Multiset.Filter
Multiset.filter_eq_self : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Multiset α}, Multiset.filter p s = s ↔ ∀ a ∈ s, p a
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.trace_kroneckerTMul : ∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {m : Type u_10} {n : Type u_11} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β] [inst_3 : Module R α] [inst_4 : Module R β] [inst_5 : Fintype m]
  [inst_6 : Fintype n] (A : Matrix m m α) (B : Matrix n n β),
  (Matrix.kroneckerMap (TensorProduct.tmul R) A B).trace = A.trace ⊗ₜ[R] B.trace
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Functor.PreservesPairwisePullbacks.preservesLimit : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {F : CategoryTheory.Functor C D} {X : C}
  (R : CategoryTheory.Presieve X) [self : F.PreservesPairwisePullbacks R] ⦃Y Z : C⦄ ⦃f : Y ⟶ X⦄ ⦃g : Z ⟶ X⦄,
  R f → R g → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) F
-- Init.Data.List.MinMaxIdx
List.maxIdxOn?_replicate_of_pos : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.Refl fun x1 x2 => x1 ≤ x2] {n : ℕ} {a : α}
  {f : α → β}, 0 < n → List.maxIdxOn? f (List.replicate n a) = some 0
-- Aesop.Tree.Data
Aesop.RappId.one : Aesop.RappId
-- Mathlib.Computability.Ackermann
ack_pos : ∀ (m n : ℕ), 0 < ack m n
-- Std.Time.Zoned.Database.TzIf
/-- The array of abbreviation strings used by local time types.
 -/
Std.Time.TimeZone.TZif.TZifV1.abbreviations : Std.Time.TimeZone.TZif.TZifV1 → Array String
-- Mathlib.Tactic.Linter.Style
/-- The "missing end" linter emits a warning on non-closed `section`s and `namespace`s.
It allows the "outermost" `noncomputable section` to be left open (whether or not it is named).
 -/
Mathlib.Linter.linter.style.missingEnd : Lean.Option Bool
-- Mathlib.Algebra.Star.StarProjection
IsStarProjection.isSelfAdjoint : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Star R] {p : R}, IsStarProjection p → IsSelfAdjoint p
-- Mathlib.Data.ENNReal.Real
ENNReal.toNNReal_pos_iff : ∀ {a : ENNReal}, 0 < a.toNNReal ↔ 0 < a ∧ a < ⊤
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.reduce.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (t : List (α × Bool)),
  FreeGroup.reduce t =
    List.rec []
      (fun hd1 _tl1 ih =>
        List.casesOn ih [hd1] fun hd2 tl2 => if hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2 then tl2 else hd1 :: hd2 :: tl2)
      t
-- Mathlib.CategoryTheory.ConcreteCategory.Bundled
CategoryTheory.Bundled.coe_mk : ∀ {c : Type u → Type v} (α : Type u) (str : c α), ↑{ α := α, str := str } = α
-- Mathlib.CategoryTheory.Subterminal
/-- The category of subterminal objects is equivalent to the category of monomorphisms to the terminal
object (which is in turn equivalent to the subobjects of the terminal object).
 -/
CategoryTheory.subterminalsEquivMonoOverTerminal : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasTerminal C] → CategoryTheory.Subterminals C ≌ CategoryTheory.MonoOver (⊤_ C)
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- The bijection between the free group on a unique type and the integers.  -/
FreeGroup.equivIntOfUnique : {α : Type u} → [Unique α] → FreeGroup α ≃ ℤ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The opposite of a bilimit binary bicone is bilimit.  -/
CategoryTheory.Limits.BinaryBicone.IsBilimit.op : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} → {b : CategoryTheory.Limits.BinaryBicone P Q} → b.IsBilimit → b.op.IsBilimit
-- Mathlib.Data.List.Sigma
List.dlookup_eq_none : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {l : List (Sigma β)},
  List.dlookup a l = none ↔ a ∉ l.keys
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_sdiff_both : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : DecidableEq α] (a b : α),
  Finset.Icc a b \ {a, b} = Finset.Ioo a b
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.fromOpcycles_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology] (φ : S₁ ⟶ S₂)
  {Z : C} (h : S₂.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ)
      (CategoryTheory.CategoryStruct.comp S₂.fromOpcycles h) =
    CategoryTheory.CategoryStruct.comp S₁.fromOpcycles (CategoryTheory.CategoryStruct.comp φ.τ₃ h)
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_single_ne_zero : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B} (a : A) {r : R}, r ≠ 0 → AddMonoidAlgebra.supDegree D (AddMonoidAlgebra.single a r) = D a
-- Init.Data.Int.Order
Int.sub_left_lt_of_lt_add : ∀ {a b c : ℤ}, a < b + c → a - b < c
-- Lean.Meta.Tactic.Apply
/-- Close the given goal using `apply e`.
 -/
Lean.MVarId.apply : Lean.MVarId →
  Lean.Expr →
    optParam Lean.Meta.ApplyConfig { } → optParam (Option Lean.MessageData) none → Lean.MetaM (List Lean.MVarId)
-- Lean.Meta.Tactic.Apply
_private.Lean.Meta.Tactic.Apply.0.Lean.MVarId.apply.go.eq_def : ∀ (mvarId : Lean.MVarId) (cfg : Lean.Meta.ApplyConfig) (term? : Option Lean.MessageData) (targetType eType : Lean.Expr)
  (rangeNumArgs : Std.Rco ℕ) (i : ℕ),
  Lean.MVarId.apply.go✝ mvarId cfg term? targetType eType rangeNumArgs i =
    if i < rangeNumArgs.upper then do
      let s ← Lean.saveState
      let __x ← Lean.Meta.forallMetaTelescopeReducing eType (some i)
      match __x with
        | (newMVars, binderInfos, eType_1) => do
          let __do_lift ← Lean.Meta.isDefEqApply✝ cfg.approx eType_1 targetType
          if __do_lift = true then pure (newMVars, binderInfos)
            else do
              s.restore
              Lean.MVarId.apply.go✝ mvarId cfg term? targetType eType rangeNumArgs (i + 1)
    else
      have __do_jp := fun conclusionType? => Lean.Meta.throwApplyError✝ mvarId eType conclusionType? targetType term?;
      if rangeNumArgs.lower = 0 then do
        let conclusionType? ← pure none
        __do_jp conclusionType?
      else do
        let __x ← Lean.Meta.forallMetaTelescopeReducing eType (some rangeNumArgs.lower)
        match __x with
          | (fst, fst_1, r) => do
            let conclusionType? ← pure (some r)
            __do_jp conclusionType?
-- Mathlib.Data.Sym.Sym2
/-- The inverse to `Sym2.fromRel`. Given a set on `Sym2 α`, give a symmetric relation on `α`
(see `Sym2.toRel_symm`).  -/
Sym2.ToRel : {α : Type u_1} → Set (Sym2 α) → α → α → Prop
-- Mathlib.LinearAlgebra.Matrix.Circulant
/-- A circulant of `v` is symmetric iff `v` equals its reverse.  -/
Matrix.circulant_isSymm_iff : ∀ {α : Type u_1} {n : Type u_3} [inst : SubtractionMonoid n] {v : n → α},
  (Matrix.circulant v).IsSymm ↔ ∀ (i : n), v (-i) = v i
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- A heuristic procedure for detecting generalized patterns.
For example, given the theorem
```
theorem Option.pbind_some' {α β} {x : Option α} {a : α} {f : (a : α) → x = some a → Option β}
  (h : x = some a) : pbind x f = f a h
```
In the current implementation, we support only occurrences in the resulting type.
Thus, the following resulting type is generated for the example above:
```
pbind (Grind.genPattern h x (some a)) f = f a h
```
 -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.detectGeneralizedPatterns? : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
Orthonormal.map_equiv : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {ι' : Type u_5} {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E']
  {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Module.Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι'),
  v.map (hv.equiv hv' e).toLinearEquiv = v'.reindex e.symm
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.refl_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.Iso.refl X).hom = CategoryTheory.CategoryStruct.id X
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_range : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β), ↑f.range = Set.range ⇑f
-- Mathlib.NumberTheory.Divisors
Nat.cons_self_properDivisors : ∀ {n : ℕ}, n ≠ 0 → Finset.cons n n.properDivisors ⋯ = n.divisors
-- Mathlib.Tactic.ErwQuestion
/-- `erw? [r, ...]` calls `erw [r, ...]` (at hypothesis `h` if written `erw [r, ...] at h`),
and then attempts to identify any subexpression which would block the use of `rw` instead.
It does so by identifying subexpressions which are defeq, but not at reducible transparency.
 -/
Mathlib.Tactic.Erw?.erw? : Lean.ParserDescr
-- Mathlib.Logic.Equiv.Defs
/-- The map `(r ≃ s) → (r → s)` is injective.  -/
Equiv.coe_fn_injective : ∀ {α : Sort u} {β : Sort v}, Function.Injective fun e => ⇑e
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.comap_mk_nhds : ∀ {M : Type u_1} [inst : TopologicalSpace M] (x : Mᵈᵃᵃ),
  Filter.comap (⇑DomAddAct.mk) (nhds x) = nhds (DomAddAct.mk.symm x)
-- Mathlib.Algebra.Star.TransferInstance
/-- Transfer `Star` across an `Equiv`. See note [reducible non-instances].

For `star : R → R` bundled as an `Equiv`, see `Equiv.Perm.star`.  -/
Equiv.star : {R : Type u_1} → {S : Type u_2} → R ≃ S → [Star S] → Star R
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.eRank_subsingleton : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [Subsingleton R] (A : Matrix m n R), A.eRank = 1
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.functorialFactorizationData_Z_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  (f : CategoryTheory.Arrow C),
  (CategoryTheory.SmallObject.functorialFactorizationData I κ).Z.obj f = CategoryTheory.SmallObject.obj I κ f.hom
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
/-- Minimal primes are contained in zero divisors.  -/
Ideal.disjoint_nonZeroDivisors_of_mem_minimalPrimes : ∀ {R : Type u_1} [inst : CommSemiring R] {p : Ideal R}, p ∈ minimalPrimes R → Disjoint ↑p ↑(nonZeroDivisors R)
-- Mathlib.CategoryTheory.Sites.Canonical
/-- A representable functor is a sheaf for the canonical topology.  -/
CategoryTheory.Sheaf.isSheaf_of_isRepresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) [P.IsRepresentable],
  CategoryTheory.Presieve.IsSheaf (CategoryTheory.Sheaf.canonicalTopology C) P
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceCompletionItem : Lean.Lsp.FileSource Lean.Lsp.CompletionItem
-- Init.Data.Slice.List.Lemmas
_private.Init.Data.Slice.List.Lemmas.0.ListSlice.toList_internalIter : ∀ {α : Type u} {s : ListSlice α},
  (Std.Slice.Internal.iter s).toList =
    match s.internalRepresentation.stop with
    | some stop => List.take stop s.internalRepresentation.list
    | none => s.internalRepresentation.list
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.cyclesMap_neg : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology],
  CategoryTheory.ShortComplex.cyclesMap (-φ) = -CategoryTheory.ShortComplex.cyclesMap φ
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The forgetful functor from monoids to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types.  -/
MonCat.forget_preservesLimitsOfSize : ∀ [UnivLE.{v, u}], CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget MonCat)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.C_apply : ∀ {R : Type u_1} [inst : Semiring R] {r : R}, PowerSeries.C r = MvPowerSeries.C r
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Main entry point of this module:

Try to find a lexicographic ordering of the basic measures for which the recursive definition
terminates. See the module doc string for a high-level overview.

The `preDefs` are used to determine arity and types of parameters; the bodies are ignored.
 -/
Lean.Elab.WF.guessLex : Array Lean.Elab.PreDefinition →
  Lean.Elab.PreDefinition → Lean.Elab.FixedParamPerms → Lean.Meta.ArgsPacker → Lean.MetaM Lean.Elab.TerminationMeasures
-- Mathlib.Data.ENat.Basic
MonoidWithZeroHom.ENatMap_apply : ∀ {S : Type u_2} [inst : MulZeroOneClass S] [inst_1 : DecidableEq S] [inst_2 : Nontrivial S] (f : ℕ →*₀ S)
  (hf : Function.Injective ⇑f), ⇑(f.ENatMap hf) = ENat.map ⇑f
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_mono : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α], Monotone fun x => x⁺ᵐ
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.totalFunctor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂)
  [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : ∀ (K : HomologicalComplex₂ C c₁ c₂), K.HasTotal c₁₂] {X Y : HomologicalComplex₂ C c₁ c₂} (φ : X ⟶ Y),
  (HomologicalComplex₂.totalFunctor C c₁ c₂ c₁₂).map φ = HomologicalComplex₂.total.map φ c₁₂
-- Mathlib.Algebra.Category.BialgCat.Basic
/-- The underlying `BialgHom`  -/
BialgCat.Hom.toBialgHom' : {R : Type u} → [inst : CommRing R] → {V W : BialgCat R} → V.Hom W → V.carrier →ₐc[R] W.carrier
-- Init.Data.String.PosRaw
String.Pos.Raw.unoffsetBy_offsetBy : ∀ {p q : String.Pos.Raw}, (p.offsetBy q).unoffsetBy q = p
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
/-- If `R` and `S` are isomorphic as rings, then two-sided ideals of `R` and two-sided ideals of `S` are
order isomorphic.
 -/
RingEquiv.mapTwoSidedIdeal : {R : Type u_1} →
  {S : Type u_2} →
    [inst : NonUnitalNonAssocRing R] → [inst_1 : NonUnitalNonAssocRing S] → R ≃+* S → TwoSidedIdeal R ≃o TwoSidedIdeal S
-- Mathlib.CategoryTheory.Limits.Cones
/-- A natural transformation from `F` to the constant functor at `pt`  -/
CategoryTheory.Limits.Cocone.ι : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (self : CategoryTheory.Limits.Cocone F) → F ⟶ (CategoryTheory.Functor.const J).obj self.pt
-- Mathlib.Probability.Distributions.Bernoulli
/-- The **Bernoulli distribution** over an arbitrary measurable space `X`.
Given `x y : X` and `p : I` (`I` is the `unitInterval`),
it is the measure which gives mass `p` to `{x}` and `1 - p` to `{y}`.  -/
ProbabilityTheory.«termBer(_,_,_)» : Lean.ParserDescr
-- Mathlib.Logic.Relation
IsEquiv.comap : ∀ {α : Type u_1} {β : Type u_2} {r : β → β → Prop} [IsEquiv β r] (f : α → β), IsEquiv α (Function.onFun r f)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.snd_zero : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}, ProbabilityTheory.Kernel.snd 0 = 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.le_maxKey!_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, t.contains k = true → (cmp k t.maxKey!).isLE = true
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.single.congr_simp : ∀ (n : ℕ) (h : 0 < n), Composition.single n h = Composition.single n h
-- Lean.Data.Lsp.Window
Lean.Lsp.instToJsonMessageActionItem : Lean.ToJson Lean.Lsp.MessageActionItem
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.symm_apply_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₁), e.symm (e p) = p
-- Mathlib.Data.List.TFAE
List.tfae_of_cycle : ∀ {a b : Prop} {l : List Prop},
  List.IsChain (fun x1 x2 => x1 → x2) (a :: b :: l) → (l.getLastD b → a) → (a :: b :: l).TFAE
-- Std.Data.DTreeMap.Internal.Operations
/-- The tree.  -/
Std.DTreeMap.Internal.Impl.RawView.tree : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl.RawView α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Tactic.NormNum.NatFib
Mathlib.Meta.NormNum.isNat_fib : ∀ {x nx z : ℕ}, Mathlib.Meta.NormNum.IsNat x nx → Nat.fib nx = z → Mathlib.Meta.NormNum.IsNat (Nat.fib x) z
-- Mathlib.Topology.Homeomorph.Lemmas
Continuous.toEquiv_homeoOfEquivCompactToT2 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : CompactSpace X]
  [inst_3 : T2Space Y] {f : X ≃ Y} (hf : Continuous ⇑f), hf.homeoOfEquivCompactToT2.toEquiv = f
-- Mathlib.Algebra.Module.Equiv.Opposite
MulOpposite.coe_opLinearEquiv_symm_toLinearMap : ∀ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ⇑↑(MulOpposite.opLinearEquiv R).symm = MulOpposite.unop