mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Augment
CochainComplex.augment_d_zero_one : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : CochainComplex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0),
  (C.augment f w).d 0 1 = f
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `(α ≫ η ≫ ηs) ◫ (β ≫ θ ≫ θs)`  -/
Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp.mkEvalHorizontalCompConsCons : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp m] →
    Mathlib.Tactic.BicategoryLike.Structural →
      Mathlib.Tactic.BicategoryLike.Structural →
        Mathlib.Tactic.BicategoryLike.WhiskerLeft →
          Mathlib.Tactic.BicategoryLike.WhiskerLeft →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr →
                Mathlib.Tactic.BicategoryLike.NormalExpr →
                  Mathlib.Tactic.BicategoryLike.NormalExpr →
                    Mathlib.Tactic.BicategoryLike.NormalExpr →
                      Mathlib.Tactic.BicategoryLike.NormalExpr →
                        Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
/-- Use `support_getElem_eq_getVert` to rewrite in the reverse direction.  -/
SimpleGraph.Walk.getVert_eq_support_getElem : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {n : ℕ} (p : G.Walk u v) (h : n ≤ p.length), p.getVert n = p.support[n]
-- Mathlib.RingTheory.Localization.Away.AdjoinRoot
IsLocalization.Away.finitePresentation : ∀ {R : Type u_1} [inst : CommRing R] (r : R) {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization.Away r S], Algebra.FinitePresentation R S
-- Mathlib.Order.Filter.Partial
Filter.tendsto_iff_rtendsto : ∀ {α : Type u} {β : Type v} (l₁ : Filter α) (l₂ : Filter β) (f : α → β),
  Filter.Tendsto f l₁ l₂ ↔ Filter.RTendsto (Function.graph f) l₁ l₂
-- Mathlib.Algebra.Order.CauSeq.BigOperators
IsCauSeq.of_decreasing_bounded : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] [Archimedean α] (f : ℕ → α)
  {a : α} {m : ℕ}, (∀ n ≥ m, |f n| ≤ a) → (∀ n ≥ m, f n.succ ≤ f n) → IsCauSeq abs f
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageMap.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      [inst_1 : CategoryTheory.Limits.HasImage f.hom] →
        [inst_2 : CategoryTheory.Limits.HasImage g.hom] →
          {sq : f ⟶ g} →
            (map : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom) →
              autoParam
                  (CategoryTheory.CategoryStruct.comp map (CategoryTheory.Limits.image.ι g.hom) =
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom)
                      (CategoryTheory.Arrow.Hom.right sq))
                  CategoryTheory.Limits.ImageMap.map_ι._autoParam →
                CategoryTheory.Limits.ImageMap sq
-- Lean.DefEqAttrib
_private.Lean.DefEqAttrib.0.Lean.withEqLhsRhs : {α : Type} → Lean.Expr → (Lean.Expr → Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.coprodMap_apply : ∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} {N : Type u_6} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : AddCommMonoid N]
  [inst_4 : Module R N] [inst_5 : DecidableEq ι] [inst_6 : (x : N) → Decidable (x ≠ 0)] (f : (i : ι) → M i →ₗ[R] N)
  (x : Π₀ (i : ι), M i), (DFinsupp.coprodMap f) x = (DFinsupp.mapRange (fun i => ⇑(f i)) ⋯ x).sum fun x => id
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.universalFactorizationMapPresentation_jacobian : ∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k),
  (MvPolynomial.universalFactorizationMapPresentation R n m k hn).jacobian =
    (-1) ^ n *
      (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (Polynomial.freeMonic R m)).resultant
        (Polynomial.map Algebra.TensorProduct.includeRight.toRingHom (Polynomial.freeMonic R k))
-- Lean.Parser.Command
Lean.Parser.Command.openRenamingItem.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Set.Finite.Lattice
Set.Finite.biInf_iSup_eq : ∀ {α : Type u} {ι : Type v} {κ : ι → Sort w} [Nonempty ((a : ι) → κ a)] [inst : Order.Frame α] {s : Set ι},
  s.Finite → ∀ {f : (a : ι) → κ a → α}, ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSubgraph.isNonloopAt_eqOn : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, H ≤ G → Set.EqOn H.IsNonloopAt G.IsNonloopAt H.edgeSet
-- Init.Data.Vector.Lemmas
Vector.contains_eq_mem : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {as : Vector α n},
  as.contains a = decide (a ∈ as)
-- Init.Data.String.Lemmas.Order
String.Pos.sliceFrom_le_sliceFrom_iff : ∀ {s : String} {p₀ q r : s.Pos} {h₁ : p₀ ≤ q} {h₂ : p₀ ≤ r}, p₀.sliceFrom q h₁ ≤ p₀.sliceFrom r h₂ ↔ q ≤ r
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- Global sections of a sheaf of types correspond to sections of the underlying presheaf.  -/
CategoryTheory.Sheaf.ΓObjEquivSections : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : CategoryTheory.HasWeakSheafify J (Type w)] →
        [inst_2 : CategoryTheory.HasGlobalSectionsFunctor J (Type w)] →
          (F : CategoryTheory.Sheaf J (Type w)) → (CategoryTheory.Sheaf.Γ J (Type w)).obj F ≃ ↑F.obj.sections
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.applyAttributes : Lean.Name → Array Lean.Elab.Attribute → Lean.Elab.TermElabM Unit
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_sub_norm_compl_sub_single : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α],
  0 < p.toReal →
    ∀ (f : ↥(lp E p)) (s : Finset α),
      ‖f‖ ^ p.toReal - ‖f - ∑ i ∈ s, lp.single p i (↑f i)‖ ^ p.toReal = ∑ i ∈ s, ‖↑f i‖ ^ p.toReal
-- Mathlib.Topology.Order.Lattice
ContinuousAt.finset_inf_apply : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeInf L] [inst_3 : OrderTop L] [ContinuousInf L] {s : Finset ι} {f : ι → X → L} {x : X},
  (∀ i ∈ s, ContinuousAt (f i) x) → ContinuousAt (fun a => s.inf fun x => f x a) x
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_lt_add_iff_right : ∀ {α : Type u} [inst : Add α] {x y z : WithTop α} [inst_1 : LT α] [AddRightStrictMono α] [AddRightReflectLT α],
  z ≠ ⊤ → (x + z < y + z ↔ x < y)
-- Mathlib.Topology.Maps.Basic
IsOpenMap.preimage_closure_eq_closure_preimage : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → Continuous f → ∀ (s : Set Y), f ⁻¹' closure s = closure (f ⁻¹' s)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.dist_eq_iSup : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
  {f g : C(α, β)}, dist f g = ⨆ x, dist (f x) (g x)
-- Mathlib.Analysis.SpecialFunctions.CompareExp
/-- We say that `l : Filter ℂ` is an *exponential comparison filter* if the real part tends to
infinity along `l` and the imaginary part grows subexponentially compared to the real part. These
properties guarantee that `(fun z ↦ z ^ a₁ * exp (b₁ * z)) =o[l] (fun z ↦ z ^ a₂ * exp (b₂ * z))`
for any complex `a₁`, `a₂` and real `b₁ < b₂`.

In particular, the second property is automatically satisfied if the imaginary part is bounded along
`l`.  -/
Complex.IsExpCmpFilter : Filter ℂ → Prop
-- Lean.Data.DeclarationRange
Lean.instDecidableEqDeclarationRange.decEq : (x x_1 : Lean.DeclarationRange) → Decidable (x = x_1)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.ModObj.leftSMul_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} [inst_3 : CategoryTheory.ModObj M X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ModObj.leftSMul M X)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X X) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd M X) h
-- Init.Data.Int.LemmasAux
Int.sub_min_sub_right : ∀ (a b c : ℤ), min (a - c) (b - c) = min a b - c
-- Batteries.Recycling.RBTree.Alter
/-- The balance invariant for a path. `path.Balanced c₀ n₀ c n` means that `path` is a red-black tree
with balance invariant `c₀, n₀`, but it has a "hole" where a tree with balance invariant `c, n`
has been removed. The defining property is `Balanced.fill`: if `path.Balanced c₀ n₀ c n` and you
fill the hole with a tree satisfying `t.Balanced c n`, then `(path.fill t).Balanced c₀ n₀` .
 -/
RBTree.RBNode.Path.Balanced : RBTree.RBColor → ℕ → {α : Type u_1} → RBTree.RBNode.Path α → RBTree.RBColor → ℕ → Prop
-- Mathlib.Topology.Algebra.OpenSubgroup
AddSubgroup.isOpen_of_openAddSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousAdd G] (H : AddSubgroup G)
  {U : OpenAddSubgroup G}, ↑U ≤ H → IsOpen ↑H
-- Mathlib.Logic.Basic
beq_ext_iff : ∀ {α : Type u_1} {inst1 inst2 : BEq α}, inst1 = inst2 ↔ ∀ (x y : α), (x == y) = (x == y)
-- Mathlib.Data.Num.Lemmas
PosNum.natSize.eq_3 : ∀ (n : PosNum), n.bit1.natSize = n.natSize.succ
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.HasUnifEigenvalue.exists_hasUnifEigenvector : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k : ℕ∞}, f.HasUnifEigenvalue μ k → ∃ v, f.HasUnifEigenvector μ k v
-- Mathlib.Order.Preorder.Chain
IsChain.empty : ∀ {α : Type u_1} {r : α → α → Prop}, IsChain r ∅
-- Init.Data.Fin.Lemmas
Fin.zero_lt_one : ∀ {n : ℕ}, 0 < 1
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.counit_eq_algHom_toLinearMap : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Bialgebra S A] [inst_5 : Bialgebra R B] [inst_6 : Algebra R A]
  [inst_7 : Algebra R S] [inst_8 : IsScalarTower R S A],
  CoalgebraStruct.counit =
    ((↑(Algebra.TensorProduct.rid R S S)).comp
        (Algebra.TensorProduct.map (Bialgebra.counitAlgHom S A) (Bialgebra.counitAlgHom R B))).toLinearMap
-- Mathlib.Topology.Homotopy.Product
_private.Mathlib.Topology.Homotopy.Product.0.Path.Homotopic.«term_⬝_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J J_1 : CategoryTheory.GrothendieckTopology C) (e_J : J = J_1)
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)], J.MayerVietorisSquare = J_1.MayerVietorisSquare
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.isClosedUnderCokernels_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C),
  P.IsClosedUnderCokernels ↔ (CategoryTheory.MorphismProperty.ofObjectProperty P P).cokernels ≤ P
-- Mathlib.Algebra.GradedMulAction
GradedMonoid.GMulAction.toGSMul : {ιA : Type u_1} →
  {ιM : Type u_3} →
    {A : ιA → Type u_4} →
      {M : ιM → Type u_5} →
        {inst : AddMonoid ιA} →
          {inst_1 : VAdd ιA ιM} →
            {inst_2 : GradedMonoid.GMonoid A} → [self : GradedMonoid.GMulAction A M] → GradedMonoid.GSMul A M
-- Mathlib.LinearAlgebra.Finsupp.Pi
/-- The linear map `(X → M) →ₗ[R] (Y → M)` induced by a map `X → Y` between finite types.  -/
FunOnFinite.linearMap : (R : Type u_5) →
  (M : Type u_6) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {X : Type u_7} → {Y : Type u_8} → [Finite X] → [Finite Y] → (X → Y) → (X → M) →ₗ[R] Y → M
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.instHasLimitOfHasLimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  [CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor J C), CategoryTheory.Limits.HasLimit F
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.prod_symm_apply_proj : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F₁ : Type u_2} [inst_1 : TopologicalSpace F₁] {E₁ : B → Type u_3}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [inst_3 : TopologicalSpace F₂]
  {E₂ : B → Type u_5} [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj)
  [inst_5 : (x : B) → Zero (E₁ x)] [inst_6 : (x : B) → Zero (E₂ x)] (p : B × F₁ × F₂), (↑(e₁.prod e₂).symm p).proj = p.1
-- Init.Sym.Lemmas
Lean.Sym.Int8.eq_eq_false : ∀ (a b : Int8), decide (a = b) = false → (a = b) = False
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbol : Type
-- Mathlib.Data.Finset.Sum
Finset.toLeft_map_sumComm : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)}, (Finset.map (Equiv.sumComm α β).toEmbedding u).toLeft = u.toRight
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.toHom_comp_inj : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] (h : L.Embedding N P) (f g : L.Hom M N), h.toHom.comp f = h.toHom.comp g ↔ f = g
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- Given a natural isomorphism between `F ⋙ H` and `G ⋙ H` for a fully faithful functor `H`, we
can 'cancel' it to give a natural iso between `F` and `G`.
 -/
CategoryTheory.Functor.fullyFaithfulCancelRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {F G : CategoryTheory.Functor C D} →
              (H : CategoryTheory.Functor D E) → [H.Full] → [H.Faithful] → (F.comp H ≅ G.comp H) → (F ≅ G)
-- Mathlib.Data.TypeVec
/-- `prod` is functorial  -/
TypeVec.prod.map : {n : ℕ} → {α α' β β' : TypeVec.{u} n} → α.Arrow β → α'.Arrow β' → (α.prod α').Arrow (β.prod β')
-- Mathlib.Analysis.Complex.Trigonometric
Real.tan_inv_eq_cot : ∀ (x : ℝ), (Real.tan x)⁻¹ = x.cot
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.insert_setBlack : ∀ {α : Type u_1} {cmp : α → α → Ordering} {v : α} {t : RBTree.RBNode α},
  (RBTree.RBNode.insert cmp t v).setBlack = (RBTree.RBNode.ins cmp v t).setBlack
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
/-- The canonical map from `WeakSpace 𝕜 E` to `E` is an open map.  -/
isOpenMap_toWeakSpace_symm : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E],
  IsOpenMap ⇑(toWeakSpace 𝕜 E).symm
-- Mathlib.Analysis.Calculus.DSlope
dslope.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 → E) (a : 𝕜), dslope f a = Function.update (slope f a) a (deriv f a)
-- Init.Data.UInt.Lemmas
UInt64.toUSize_toUInt16 : ∀ (n : UInt64), n.toUInt16.toUSize = n.toUSize % 65536
-- Init.Core
eq_iff_iff : ∀ {a b : Prop}, a = b ↔ (a ↔ b)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.lintegral_prod_swap : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] (f : α × β → ENNReal),
  ∫⁻ (z : β × α), f z.swap ∂ν.prod μ = ∫⁻ (z : α × β), f z ∂μ.prod ν
-- Mathlib.Algebra.Group.Shrink
Shrink.instAddCommSemigroup.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : AddCommSemigroup α],
  Shrink.instAddCommSemigroup = (equivShrink α).symm.addCommSemigroup
-- Mathlib.Tactic.Sat.FromLRAT
/-- Parse a list of integers terminated by 0  -/
Mathlib.Tactic.Sat.Parser.parseInts : optParam (Array ℤ) #[] → Std.Internal.Parsec.String.Parser (Array ℤ)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.AffineScheme.forgetToScheme_preservesLimits : CategoryTheory.Limits.PreservesLimits AlgebraicGeometry.AffineScheme.forgetToScheme
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.combine.eq_1 : ∀ (p₁ p₂ : Int.Internal.Linear.Poly),
  p₁.combine p₂ = Int.Internal.Linear.Poly.combine' Int.Internal.Linear.hugeFuel p₁ p₂
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.liftₐ_comp : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Semiring B] [inst_4 : Algebra R₁ B] (I : Ideal A) [inst_5 : I.IsTwoSided] (f : A →ₐ[R₁] B)
  (hI : ∀ a ∈ I, f a = 0), (Ideal.Quotient.liftₐ I f hI).comp (Ideal.Quotient.mkₐ R₁ I) = f
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.left_triangle_components : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F H : CategoryTheory.Functor C V} (G : CategoryTheory.Functor C V)
  [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  (ℌ :
    CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F
      (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H)
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F H],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id F) ℌ.coev_app) ℌ.ev_app =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G)
-- Std.Sync.CancellationContext
/-- Counts the number of alive (non-cancelled) tokens in the context tree, including
this context and all its descendants.
 -/
Std.CancellationContext.countAliveTokens : Std.CancellationContext → BaseIO ℕ
-- Init.Prelude
/-- References  -/
Lean.Macro.MethodsRefPointed : NonemptyType
-- Mathlib.GroupTheory.MonoidLocalization.Cardinality
Localization.cardinalMk_le : ∀ {M : Type u} [inst : CommMonoid M] (S : Submonoid M), Cardinal.mk (Localization S) ≤ Cardinal.mk M
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddLocalization.addEquivOfQuotient.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N),
  AddLocalization.addEquivOfQuotient f = (AddLocalization.addMonoidOf S).addEquivOfLocalizations f
-- Mathlib.Analysis.Convex.MetricSpace
Convexity.continuous_convexCombPair_of_isBounded : ∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X] {T : Type u_3}
  [inst_3 : TopologicalSpace T] (f : T → ℝ),
  Continuous f →
    ∀ (hf0 : ∀ (t : T), 0 ≤ f t) (hf1 : ∀ (t : T), f t ≤ 1) (x y : T → X),
      ContinuousOn x (f ⁻¹' {0}ᶜ) →
        ContinuousOn y (f ⁻¹' {1}ᶜ) →
          Bornology.IsBounded (Set.range x) →
            Bornology.IsBounded (Set.range y) →
              Continuous fun i => Convexity.convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.exp_eq_one_iff : ∀ {x : ℂ}, Complex.exp x = 1 ↔ ∃ n, x = ↑n * (2 * ↑Real.pi * Complex.I)
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : InfSet α] [inst_1 : InfSet β] [inst_2 : InfSet γ]
  [inst_3 : InfSet δ] (f : sInfHom γ δ) (g : sInfHom β γ) (h : sInfHom α β), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Data.Real.Basic
Real.ofCauchy_ratCast : ∀ (q : ℚ), { cauchy := ↑q } = ↑q
-- Std.Data.HashSet.Basic
/-- Returns `true` if the hash set contains no elements.

Note that if your `BEq` instance is not reflexive or your `Hashable` instance is not
lawful, then it is possible that this function returns `false` even though `m.contains a = false`
for all `a`.
 -/
Std.HashSet.isEmpty : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → Bool
-- Mathlib.LinearAlgebra.Prod
AddMonoidHom.mrange.congr_simp : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f f_1 : F),
  f = f_1 → AddMonoidHom.mrange f = AddMonoidHom.mrange f_1
-- Mathlib.Tactic.Polynomial.Core
/-- `polynomial_post` marks a theorem to be used by the `polynomial_nf` tactic as a postprocessing
lemma. Used only by polynomial_nf. These serve the purpose of rewriting expressions in `algebra`
normal form into a more readable form. e.g. `a • X` -> `algebraMap _ _ a * X` -> `C a * X`.  -/
Mathlib.Tactic.Polynomial.polynomialPostExt : Lean.Meta.SimpExtension
-- Mathlib.Logic.Equiv.Set
/-- Equivalence between the range of `Sum.inl : α → α ⊕ β` and `α`.  -/
Equiv.Set.rangeInl : (α : Type u_3) → (β : Type u_4) → ↑(Set.range Sum.inl) ≃ α
-- Mathlib.Algebra.Group.Submonoid.Units
/-- A subgroup of units represented as a submonoid of `M`.  -/
Subgroup.ofUnits : {M : Type u_1} → [inst : Monoid M] → Subgroup Mˣ → Submonoid M
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- Turn an element of the space of measure equipped with the Lévy-Prokhorov metric into the
corresponding measure.  -/
MeasureTheory.LevyProkhorov.toMeasure : {α : Type u_2} → MeasureTheory.LevyProkhorov α → α
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
/-- An `R`-linear homomorphism of graded algebras, denoted `𝒜 →ₐᵍ[R] ℬ`.  -/
GradedAlgHom : (R : Type u_1) →
  {A : Type u_2} →
    {B : Type u_3} →
      {ι : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : DecidableEq ι] →
                    [inst_6 : AddMonoid ι] →
                      (𝒜 : ι → Submodule R A) →
                        (ℬ : ι → Submodule R B) → [GradedAlgebra 𝒜] → [GradedAlgebra ℬ] → Type (max u_2 u_3)
-- Mathlib.Algebra.Order.Monovary
monovaryOn_inv : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [inst_3 : CommGroup β] [inst_4 : PartialOrder β] [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.star_eq_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E), star A = LinearMap.adjoint A
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.forgetToPresheafModuleCatObjMap_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ)
  (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) {Y Z : Cᵒᵖ} (f : Y ⟶ Z) (m : ↑(M.obj Y)),
  (ModuleCat.Hom.hom (PresheafOfModules.forgetToPresheafModuleCatObjMap X hX M f)) m =
    (CategoryTheory.ConcreteCategory.hom (M.map f)) m
-- Mathlib.Algebra.Group.Hom.Basic
powMonoidHom.eq_1 : ∀ {α : Type u_1} [inst : CommMonoid α] (n : ℕ),
  powMonoidHom n = { toFun := fun x => x ^ n, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Data.Multiset.Bind
Multiset.mem_product : ∀ {α : Type u_1} {β : Type v} {s : Multiset α} {t : Multiset β} {p : α × β}, p ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t
-- Lean.ResolveName
Lean.checkPrivateInPublic : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] → [Lean.MonadOptions m] → [Lean.MonadLog m] → [Lean.AddMessageContext m] → Lean.Name → m Unit