mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finsupp.Multiset
Finsupp.count_toMultiset : ∀ {α : Type u_1} [inst : DecidableEq α] (f : α →₀ ℕ) (a : α), Multiset.count a (Finsupp.toMultiset f) = f a
-- Mathlib.Algebra.GradedMonoid
List.dProdIndex_nil : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddMonoid ι] (fι : α → ι), [].dProdIndex fι = 0
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- To give an object in the over category, it suffices to give a morphism with codomain `X`.  -/
CategoryTheory.Over.mk : {T : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} T] → {X Y : T} → (Y ⟶ X) → CategoryTheory.Over X
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.instFiniteTypeIntCoreOfFinite : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} [Finite σ], Algebra.FiniteType ℤ P.Core
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.OplaxTrans.instInhabited : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F : CategoryTheory.LaxFunctor B C} → Inhabited (CategoryTheory.Lax.OplaxTrans F F)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mk.sizeOf_spec : ∀ {K : Type u} [inst : Field K] [inst_1 : SizeOf K] (toSubring : Subring K)
  (mem_or_inv_mem' : ∀ (x : K), x ∈ toSubring.carrier ∨ x⁻¹ ∈ toSubring.carrier),
  sizeOf { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' } = 1 + sizeOf toSubring
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instHasDistribNeg : {R : Type u_1} → [inst : Mul R] → [HasDistribNeg R] → HasDistribNeg (Lex R)
-- Lean.Parser.Types
Lean.Parser.instInhabitedParser : Inhabited Lean.Parser.Parser
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
/-- `F.LaxLinear C` equips `F : D ⥤ D'` with a family of morphisms
`μₗ F : ∀ (c : C) (d : D), c ⊙ₗ F.obj d ⟶ F.obj (c ⊙ₗ d)`
that is natural in each variable and coherent with respect to left actions
of `C` on `D` and `D'`.  -/
CategoryTheory.Functor.LaxLeftLinear : {D : Type u_1} →
  {D' : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} D] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] →
        CategoryTheory.Functor D D' →
          (C : Type u_3) →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.MonoidalCategory C] →
                [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
                  [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'] → Type (max (max u_1 u_3) v_2)
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.mk : {α₁ : Type w} →
  {m : Type w → Type w'} →
    {β₁ : Type w} →
      [inst : Std.Iterator α₁ m β₁] →
        {α₂ β₂ : Type w} →
          Std.IterM m β₁ →
            Option { out // ∃ it, it.IsPlausibleOutput out } → Std.IterM m β₂ → Std.Iterators.Types.Zip α₁ m α₂ β₂
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.isCyclicallyReduced_iff : ∀ {α : Type u} {L : List (α × Bool)},
  FreeGroup.IsCyclicallyReduced L ↔ FreeGroup.IsReduced L ∧ ∀ a ∈ L.getLast?, ∀ b ∈ L.head?, a.1 = b.1 → a.2 = b.2
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.smul_mem_iff : ∀ {𝕜 : Type u_5} {M : Type u_6} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommMonoid M] [inst_4 : Module 𝕜 M] (C : PointedCone 𝕜 M) {c : 𝕜}, 0 < c → ∀ {x : M}, c • x ∈ C ↔ x ∈ C
-- Lean.Meta.MethodSpecs
/-- Array mapping field names to implementation functions.  -/
_private.Lean.Meta.MethodSpecs.0.Lean.MethodSpecsInfo.fieldImpls : Lean.MethodSpecsInfo✝ → Array (Lean.Name × Lean.Name)
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.den_one : ∀ {m : Type u_1} [inst : Fintype m] [inst_1 : DecidableEq m], Matrix.den 1 = 1
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- An almost everywhere sequential limit of almost everywhere strongly measurable functions is
almost everywhere strongly measurable.  -/
aestronglyMeasurable_of_tendsto_ae : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {ι : Type u_5} [TopologicalSpace.PseudoMetrizableSpace β] (u : Filter ι) [u.NeBot] [u.IsCountablyGenerated]
  {f : ι → α → β} {g : α → β},
  (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) →
    (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) u (nhds (g x))) → MeasureTheory.AEStronglyMeasurable g μ
-- Mathlib.Algebra.Group.Defs
IsRightCancelMul.mk : ∀ {G : Type u} [inst : Mul G], (∀ (a : G), IsRightRegular a) → IsRightCancelMul G
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeOfConeLeftOp_ι_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.leftOp) (X : J),
  (CategoryTheory.Limits.coconeOfConeLeftOp c).ι.app X = (c.π.app (Opposite.op X)).op
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instInfFiniteIndexNormalAddSubgroup.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  FiniteIndexNormalAddSubgroup.instInfFiniteIndexNormalAddSubgroup =
    {
      min := fun U V =>
        let __Subgroup := U.toAddSubgroup ⊓ V.toAddSubgroup;
        { toAddSubgroup := __Subgroup, isNormal' := ⋯, isFiniteIndex' := ⋯ } }
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKeyD_unitOfList_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α},
  l.contains k = false → (Std.DHashMap.Raw.Const.unitOfList l).getKeyD k fallback = fallback
-- Mathlib.Analysis.LocallyConvex.WeakDual
LinearMap.toSeminorm_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {f : E →ₗ[𝕜] 𝕜}
  {x : E}, f.toSeminorm x = ‖f x‖
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.hasNatPow : {α : Type u} →
  [inst : TopologicalSpace α] → {R : Type u_1} → [inst_1 : SeminormedRing R] → Pow (BoundedContinuousFunction α R) ℕ
-- Batteries.Data.Array.Scan
Array.scanr_reverse : ∀ {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : Array α},
  Array.scanr f init as.reverse = (Array.scanl (flip f) init as).reverse
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom : ∀ (R S : CommRingCat) (p : PrimeSpectrum ↑R) [inst : Algebra ↑R ↑S],
  IsLocalizedModule p.asIdeal.primeCompl (AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom R S p).toLinearMap
-- Lean.Data.Json.Stream
Lean.IO.FS.Stream.writeJson : IO.FS.Stream → Lean.Json → IO Unit
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.mk.inj : ∀ {d : ℤ} {p : Int.Internal.Linear.Poly} {h : Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof} {d_1 : ℤ}
  {p_1 : Int.Internal.Linear.Poly} {h_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof},
  { d := d, p := p, h := h } = { d := d_1, p := p_1, h := h_1 } → d = d_1 ∧ p = p_1 ∧ h = h_1
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] (f : M₁ →ₗ[R] M₂ →ₗ[R] M), IsTensorProduct f = Function.Bijective ⇑(TensorProduct.lift f)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.δ_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  (i : Fin (n + 2)), X.δ i = X.map (SimplexCategory.δ i).op
-- Mathlib.RingTheory.AdicCompletion.RingHom
IsAdicComplete.liftAlgHom.eq_1 : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (I : Ideal S) [inst_3 : IsAdicComplete I S] [inst_4 : CommRing A] [inst_5 : Algebra R A]
  (f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m),
  IsAdicComplete.liftAlgHom I f hf =
    (AlgHom.restrictScalars R ↑(AdicCompletion.ofAlgEquiv I).symm).comp (AdicCompletion.liftAlgHom I f ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.instIsRegularMonoOfIsSplitMono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsSplitMono f],
  CategoryTheory.IsRegularMono f
-- Mathlib.Condensed.Discrete.Module
/-- `functorToPresheaves` in the case of `CompHaus`.  -/
CondensedMod.LocallyConstant.functorToPresheaves : (R : Type (u + 1)) →
  [inst : Ring R] → CategoryTheory.Functor (ModuleCat R) (CategoryTheory.Functor CompHausᵒᵖ (ModuleCat R))
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.forget_reflects_isos : (CategoryTheory.forget AddCommMonCat).ReflectsIsomorphisms
-- Init.Data.SInt.Bitwise
Int64.and_comm : ∀ (a b : Int64), a &&& b = b &&& a
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.Abelian.mono_of_epi_of_epi_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ComposableArrows C 2} (φ : R₁ ⟶ R₂),
  R₁.Exact →
    R₂.Exact →
      CategoryTheory.Epi
          (R₁.map' 1 2 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6
            CategoryTheory.Abelian.mono_of_epi_of_epi_mono'._proof_1) →
        CategoryTheory.Epi
            (CategoryTheory.ComposableArrows.app' φ 0 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_2) →
          CategoryTheory.Mono
              (CategoryTheory.ComposableArrows.app' φ 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6) →
            CategoryTheory.Mono
              (CategoryTheory.ComposableArrows.app' φ 2 CategoryTheory.Abelian.mono_of_epi_of_epi_mono'._proof_1)
-- Mathlib.Analysis.Normed.Operator.NormedSpace
LinearIsometry.enorm_toContinuousLinearMap : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [NontrivialTopology E]
  [inst_7 : RingHomIsometric σ₁₂] (f : E →ₛₗᵢ[σ₁₂] F), ‖f.toContinuousLinearMap‖ₑ = 1
-- Mathlib.Combinatorics.Enumerative.Bell
Nat.bell_succ : ∀ (n : ℕ), (n + 1).bell = ∑ i ≤ n, n.choose i * (n - i).bell
-- Mathlib.Data.Set.Prod
Set.univ_pi_subset_univ_pi_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {t₁ t₂ : (i : ι) → Set (α i)},
  Set.univ.pi t₁ ⊆ Set.univ.pi t₂ ↔ (∀ (i : ι), t₁ i ⊆ t₂ i) ∨ ∃ i, t₁ i = ∅
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjHomologySelfIso c j A).hom
      (HomologicalComplex.singleObjOpcyclesSelfIso c j A).hom =
    ((HomologicalComplex.single C c j).obj A).homologyι j
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trCont.match_1.eq_5 : ∀ (motive : Turing.ToPartrec.Cont → Sort u_1) (c : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont)
  (h_1 : Unit → motive Turing.ToPartrec.Cont.halt)
  (h_2 :
    (c : Turing.ToPartrec.Code) →
      (a : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₁ c a k))
  (h_3 : (a : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₂ a k))
  (h_4 : (c : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.comp c k))
  (h_5 : (c : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.fix c k)),
  (match Turing.ToPartrec.Cont.fix c k with
    | Turing.ToPartrec.Cont.halt => h_1 ()
    | Turing.ToPartrec.Cont.cons₁ c a k => h_2 c a k
    | Turing.ToPartrec.Cont.cons₂ a k => h_3 a k
    | Turing.ToPartrec.Cont.comp c k => h_4 c k
    | Turing.ToPartrec.Cont.fix c k => h_5 c k) =
    h_5 c k
-- Init.Data.UInt.Lemmas
USize.ofBitVec_le_iff_le : ∀ {a b : BitVec System.Platform.numBits}, { toBitVec := a } ≤ { toBitVec := b } ↔ a ≤ b
-- Mathlib.Analysis.Calculus.FDeriv.Pow
fderivWithin_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {x : E}
  {s : Set E},
  UniqueDiffWithinAt 𝕜 s x →
    ∀ (n : ℕ), DifferentiableWithinAt 𝕜 f s x → fderivWithin 𝕜 (f ^ n) s x = (n • f x ^ (n - 1)) • fderivWithin 𝕜 f s x
-- Mathlib.Analysis.Meromorphic.IsolatedZeros
MeromorphicAt.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin_preperfect : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {x : 𝕜} {f g : 𝕜 → E},
  MeromorphicAt f x →
    MeromorphicAt g x → x ∈ U → Preperfect U → f =ᶠ[Filter.codiscreteWithin U] g → f =ᶠ[nhdsWithin x {x}ᶜ] g
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
cfcₙ_im_id : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [inst_6 : StarModule ℂ A]
  [inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A),
  autoParam (IsStarNormal a) cfcₙ_im_id._auto_1 → cfcₙ (fun x => ↑x.im) a = ↑(imaginaryPart a)
-- Init.Data.Nat.Lemmas
/-- See also `Nat.divModEquiv` for a similar statement as an `Equiv`.  -/
Nat.div_mod_unique : ∀ {b a d c : ℕ}, 0 < b → (a / b = d ∧ a % b = c ↔ c + b * d = a ∧ c < b)
-- Qq.MetaM
Qq.trySynthInstanceQ : {u : Lean.Level} → (α : Q(Sort u)) → Lean.MetaM (Lean.LOption Q(«$α»))
-- Mathlib.Topology.Algebra.InfiniteSum.Order
tsum_nonpos : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommMonoid α] [inst_1 : Preorder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α},
  (∀ (i : ι), f i ≤ 0) → ∑'[L] (i : ι), f i ≤ 0
-- Init.Data.List.Monadic
List.forIn'.loop.eq_def : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : List α)
  (f : (a : α) → a ∈ as → β → m (ForInStep β)) (as' : List α) (b : β) (a : ∃ bs, bs ++ as' = as),
  List.forIn'.loop as f as' b a =
    match as', b, a with
    | [], b, x => pure b
    | a :: as', b, h =>
      have this := ⋯;
      do
      let __do_lift ← f a this b
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b =>
          have this := ⋯;
          List.forIn'.loop as f as' b this
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_add_eq_mod : ∀ {w i : ℕ} {x y : BitVec w},
  BitVec.setWidth i (x + y) = (BitVec.setWidth i x + BitVec.setWidth i y) % BitVec.twoPow i w
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.not_boundaryLE_prev' : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff]
  {i j : ι}, ¬e.BoundaryLE j → c.prev j = i → ¬e.BoundaryLE i
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- The inner product of a linear combination of a set of orthonormal vectors with one of those
vectors picks out the coefficient of that vector.  -/
Orthonormal.inner_left_fintype : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : Fintype ι] {v : ι → E},
  Orthonormal 𝕜 v → ∀ (l : ι → 𝕜) (i : ι), inner 𝕜 (∑ i, l i • v i) (v i) = (starRingEnd 𝕜) (l i)
-- Plausible.Sampleable
Plausible.NoShrink.shrinkable : {α : Type u_1} → Plausible.Shrinkable (Plausible.NoShrink α)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negDblY_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.negDblY P = -P 1 ^ 4
-- Init.Control.Lawful.Instances
ExceptT.stM_eq : ∀ {m : Type u_1 → Type u_2} {ε α : Type u_1} [inst : Monad m], stM m (ExceptT ε m) α = Except ε α
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.addLeft : ∀ {R : Type u} {X : Type v} [inst : CommRing R] (a : FreeNonUnitalNonAssocAlgebra R X)
  {b c : FreeNonUnitalNonAssocAlgebra R X}, FreeLieAlgebra.Rel R X b c → FreeLieAlgebra.Rel R X (a + b) (a + c)
-- Mathlib.GroupTheory.Index
/-- If `H` and `K` are subgroups of a group `G`, then `relIndex H K : ℕ` is the index
of `H ∩ K` in `K`. The function returns `0` if the index is infinite.  -/
Subgroup.relIndex : {G : Type u_1} → [inst : Group G] → Subgroup G → Subgroup G → ℕ
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.of : {R : Type u_1} → {X : Type u_2} → X → FreeAlgebra.Pre R X
-- Mathlib.Order.Grade
GradeMinOrder.toGradeOrder : {𝕆 : Type u_5} →
  {α : Type u_6} → {inst : Preorder 𝕆} → {inst_1 : Preorder α} → [self : GradeMinOrder 𝕆 α] → GradeOrder 𝕆 α
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Relations.formula₁.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (r : L.Relations 1) (t : L.Term α), r.formula₁ t = r.formula ![t]
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.iteratedDeriv_even_cos : ∀ (n : ℕ), iteratedDeriv (2 * n) Real.cos = (-1) ^ n * Real.cos
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersion.instNormedSpaceComplement : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup E''] →
              [inst_4 : NormedSpace 𝕜 E''] →
                {H : Type u_7} →
                  [inst_5 : TopologicalSpace H] →
                    {G : Type u_9} →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {N : Type u_13} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} → (h : Manifold.IsImmersion I J n f) → NormedSpace 𝕜 h.complement
-- Mathlib.RingTheory.Ideal.Prod
Ideal.prod_bot_bot : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S], ⊥.prod ⊥ = ⊥
-- Mathlib.Condensed.Discrete.Colimit
/-- The presheaf on `Profinite` of locally constant functions to `X`.  -/
Condensed.locallyConstantPresheaf : Type (u + 1) → CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.add_assoc_flip : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.AddMonObj M],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.AddMonObj.add)
      CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M M).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add M)
        CategoryTheory.AddMonObj.add)
-- Mathlib.GroupTheory.Torsion
AddCommMonoid.mem_torsion : ∀ (G : Type u_1) [inst : AddCommMonoid G] (g : G), g ∈ AddCommMonoid.addTorsion G ↔ IsOfFinAddOrder g
-- Mathlib.Algebra.Order.Group.Synonym
toDual_inv : ∀ {α : Type u_1} [inst : Inv α] (a : α), OrderDual.toDual a⁻¹ = (OrderDual.toDual a)⁻¹
-- Mathlib.Algebra.Group.Basic
pow_iterate : ∀ {M : Type u_4} [inst : Monoid M] (k n : ℕ), (fun x => x ^ k)^[n] = fun x => x ^ k ^ n
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.some_eq_iff : ∀ {X : Type u_1} (x₁ x₂ : X), ↑x₁ = ↑x₂ ↔ x₁ = x₂
-- Lean.LocalContext
Lean.instHashableLocalDeclKind : Hashable Lean.LocalDeclKind
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
MultilinearMap.mkContinuousLinear_norm_le : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : SeminormedAddCommGroup G']
  [inst_6 : NormedSpace 𝕜 G'] [inst_7 : Fintype ι] (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') {C : ℝ},
  0 ≤ C →
    ∀ (H : ∀ (x : G) (m : (i : ι) → E i), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖),
      ‖MultilinearMap.mkContinuousLinear f C H‖ ≤ C
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.biSup_normal : ∀ {G : Type u_2} [inst : Group G] {ι : Type u_5} (s : Set ι) (H : ι → Subgroup G),
  (∀ i ∈ s, (H i).Normal) → (⨆ i ∈ s, H i).Normal
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.absolutelyContinuous_zero_iff : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.AbsolutelyContinuous 0 ↔ μ = 0
-- Init.Internal.Order.MonadTail
Lean.Order.MonadTail.mk : {m : Type u → Type v} →
  [inst : Bind m] →
    (instCCPO : (β : Type u) → [Nonempty β] → Lean.Order.CCPO (m β)) →
      (∀ {α β : Type u} {a : m α} {f₁ f₂ : α → m β} [inst_1 : Nonempty β],
          (∀ (x : α), Lean.Order.PartialOrder.rel (f₁ x) (f₂ x)) → Lean.Order.PartialOrder.rel (a >>= f₁) (a >>= f₂)) →
        Lean.Order.MonadTail m
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.List.toByteArray.match_1.splitter : (motive : List UInt8 → ByteArray → Sort u_1) →
  (x : List UInt8) →
    (x_1 : ByteArray) →
      ((r : ByteArray) → motive [] r) →
        ((b : UInt8) → (bs : List UInt8) → (r : ByteArray) → motive (b :: bs) r) → motive x x_1
-- Mathlib.RingTheory.Ideal.GoingUp
/-- If `B` is an integral `A`-algebra, `P` is a maximal ideal of `B`, then the pull back of
`P` is also a maximal ideal of `A`.  -/
Ideal.IsMaximal.under : ∀ (A : Type u_1) [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Algebra.IsIntegral A B] (P : Ideal B) [P.IsMaximal], (Ideal.under A P).IsMaximal
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insertManyIfNewUnit_list_eq_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α}, m.insertManyIfNewUnit l = List.foldl (fun acc a => acc.insertIfNew a ()) m l
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_associator_inv_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 x_2 : CategoryTheory.LaxFunctor B C} (x_3 : CategoryTheory.LaxFunctor B C) (η : x ⟶ x_1) (θ : x_1 ⟶ x_2)
  (ι : x_2 ⟶ x_3) (a : B),
  (CategoryTheory.Bicategory.associator η θ ι).inv.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
HasFDerivWithinAt.continuousMultilinear_apply_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_5} {M : ι → Type u_6}
  [inst_3 : (i : ι) → NormedAddCommGroup (M i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7}
  [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {c : E → ContinuousMultilinearMap 𝕜 M H}
  {c' : E →L[𝕜] ContinuousMultilinearMap 𝕜 M H} [inst_7 : Fintype ι],
  HasFDerivWithinAt c c' s x → ∀ (u : (i : ι) → M i), HasFDerivWithinAt (fun y => (c y) u) (c'.flipMultilinear u) s x