mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.GroupWithZero.Action.Opposite
MulOpposite.instSMulWithZero : {M : Type u_1} →
  {α : Type u_2} → [inst : MonoidWithZero M] → [inst_1 : AddMonoid α] → [SMulWithZero M α] → SMulWithZero M αᵐᵒᵖ
-- Mathlib.Data.List.Lemmas
List.mapAccumr₂.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β → γ → γ × δ) (x : List β) (x_1 : γ),
  List.mapAccumr₂ f [] x x_1 = (x_1, [])
-- Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
CategoryTheory.monoidalOfHasFiniteCoproducts.associator_inv : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] (X Y Z : C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv =
    CategoryTheory.Limits.coprod.desc
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inl)
      (CategoryTheory.Limits.coprod.desc
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl)
        CategoryTheory.Limits.coprod.inr)
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.underlying_arrow_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y Z : CategoryTheory.Subobject X} (f : Y ⟶ Z)
  {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlying.map f)
      (CategoryTheory.CategoryStruct.comp Z.arrow h) =
    CategoryTheory.CategoryStruct.comp Y.arrow h
-- Mathlib.Order.Filter.Interval
Filter.tendstoIxxClass_inf : ∀ {α : Type u_1} {l₁ l₁' l₂ l₂' : Filter α} {Ixx : α → α → Set α} [h : Filter.TendstoIxxClass Ixx l₁ l₂]
  [h' : Filter.TendstoIxxClass Ixx l₁' l₂'], Filter.TendstoIxxClass Ixx (l₁ ⊓ l₁') (l₂ ⊓ l₂')
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidt.eq_def : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f : ι → E)
  (n : ι),
  InnerProductSpace.gramSchmidt 𝕜 f n = f n - ∑ i, (𝕜 ∙ InnerProductSpace.gramSchmidt 𝕜 f ↑i).starProjection (f n)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Seed.hahnCoeff.eq_1 : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] (seed : HahnEmbedding.Seed K M R),
  seed.hahnCoeff = DirectSum.lmap seed.coeff' ∘ₗ ↑(DirectSum.decomposeLinearEquiv seed.stratum')
-- Mathlib.Order.Disjointed
disjointed_bot : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : Preorder ι]
  [inst_2 : LocallyFiniteOrderBot ι] [inst_3 : OrderBot ι] (f : ι → α), disjointed f ⊥ = f ⊥
-- Mathlib.Algebra.Group.Action.Defs
SMulDistribClass.smul_distrib_smul : ∀ {G : Type u_9} {R : Type u_10} {S : Type u_11} {inst : SMul G R} {inst_1 : SMul G S} {inst_2 : SMul R S}
  [self : SMulDistribClass G R S] (g : G) (r : R) (s : S), g • r • s = (g • r) • g • s
-- Mathlib.Algebra.Quaternion
Quaternion.imK_coe : ∀ {R : Type u_3} [inst : CommRing R] (x : R), (↑x).imK = 0
-- Mathlib.NumberTheory.FactorisationProperties
Nat.perfect_iff_not_abundant_and_not_deficient : ∀ {n : ℕ}, 0 ≠ n → (n.Perfect ↔ ¬n.Abundant ∧ ¬n.Deficient)
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.refl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  (x : M), x ≡ x [SMOD U]
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.isUnit_iff : ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, Associated a b → (IsUnit a ↔ IsUnit b)
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f` is a submersion at `x`, it maps its domain chart's target to its codomain chart's target:
`(h.domChart.extend I).target` to `(h.domChart.extend J).target`.  -/
Manifold.IsSubmersionAt.image_target_subset_target : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAt I J n f x),
  Prod.fst ∘ ⇑h.equiv '' (h.domChart.extend I).target ⊆ (h.codChart.extend J).target
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
Algebra.Extension.tensorCotangentSpace_tmul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S) (T : Type u_3) [inst_3 : CommRing T] [inst_4 : Algebra R T] (t : T)
  (x : P.CotangentSpace),
  (P.tensorCotangentSpace T) (t ⊗ₜ[R] x) =
    t • (Algebra.Extension.CotangentSpace.map (Algebra.Extension.toBaseChange T)) x
-- Mathlib.NumberTheory.Padics.PadicNumbers
instMulPadic : (p : ℕ) → [inst : Fact (Nat.Prime p)] → Mul ℚ_[p]
-- Mathlib.Analysis.Normed.Module.Basic
Subalgebra.toNormedAlgebra : {𝕜 : Type u_6} →
  {A : Type u_7} →
    [inst : SeminormedRing A] →
      [inst_1 : NormedField 𝕜] → [inst_2 : NormedAlgebra 𝕜 A] → (S : Subalgebra 𝕜 A) → NormedAlgebra 𝕜 ↥S
-- Init.Data.Int.DivMod.Lemmas
Int.neg_emod_two : ∀ (i : ℤ), -i % 2 = i % 2
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.Ici_coe : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Ici ↑a = WithBot.some '' Set.Ici a
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- Given a natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of arbitrary category,
where `G` is locally-full and cover-dense, and `ℱ', ℱ` are sheaves,
we may obtain a natural isomorphism between presheaves.
 -/
CategoryTheory.Functor.IsCoverDense.presheafIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {K : CategoryTheory.GrothendieckTopology D} →
          {A : Type u_4} →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} A] →
              {G : CategoryTheory.Functor C D} →
                [G.IsCoverDense K] →
                  [G.IsLocallyFull K] →
                    {ℱ ℱ' : CategoryTheory.Sheaf K A} → (G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) → (ℱ.obj ≅ ℱ'.obj)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.comp_symm : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (e : R ≃+* S),
  (↑e).comp ↑e.symm = RingHom.id S
-- Mathlib.Algebra.Homology.CommSq
CategoryTheory.Limits.CokernelCofork.ofπ.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {Z : C} (π π_1 : Y ⟶ Z) (e_π : π = π_1) (w : CategoryTheory.CategoryStruct.comp f π = 0),
  CategoryTheory.Limits.CokernelCofork.ofπ π w = CategoryTheory.Limits.CokernelCofork.ofπ π_1 ⋯
-- Mathlib.CategoryTheory.Opposites
/-- The isomorphism between `F.op.unop` and `F`.  -/
CategoryTheory.Functor.opUnopIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (F : CategoryTheory.Functor C D) → F.op.unop ≅ F
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.Hom.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.LaxMonoidalFunctor C D} (hom hom_1 : F.toFunctor ⟶ G.toFunctor) (e_hom : hom = hom_1)
  (isMonoidal : CategoryTheory.NatTrans.IsMonoidal hom),
  { hom := hom, isMonoidal := isMonoidal } = { hom := hom_1, isMonoidal := ⋯ }
-- Mathlib.Order.SuccPred.CompleteLinearOrder
sInf_mem_of_not_isPredPrelimit : ∀ {α : Type u_2} [inst : CompleteLinearOrder α] {s : Set α}, ¬Order.IsPredPrelimit (sInf s) → sInf s ∈ s
-- Init.Data.SInt.Lemmas
Int64.ofNat_mul : ∀ (a b : ℕ), Int64.ofNat (a * b) = Int64.ofNat a * Int64.ofNat b
-- Mathlib.Topology.Sets.Compacts
/-- Reinterpret a compact open as an open.  -/
TopologicalSpace.CompactOpens.toOpens : {α : Type u_1} → [inst : TopologicalSpace α] → TopologicalSpace.CompactOpens α → TopologicalSpace.Opens α
-- Mathlib.Order.CompleteSublattice
CompleteLatticeHom.toOrderIsoRangeOfInjective_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : CompleteLatticeHom α β)
  (hf : Function.Injective ⇑f) (a : α), (f.toOrderIsoRangeOfInjective hf) a = ⟨f a, ⋯⟩
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.antitoneOn_cos : AntitoneOn Real.cos (Set.Icc 0 Real.pi)
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasStrictFDerivAt.fun_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {ι : Type u_4} {u : Finset ι} {A : ι → E → F} {A' : ι → E →L[𝕜] F},
  (∀ i ∈ u, HasStrictFDerivAt (A i) (A' i) x) → HasStrictFDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x
-- Init.Data.String.TakeDrop
/-- Repeatedly increments a position in a string, as if by `String.Pos.Raw.next`, while the
predicate `p` returns `true` for the character at the position. Stops incrementing at
the end of the string or when `p` returns `false` for the current character.

Examples:

* `let s := "   a  "; ((0 : Pos.Raw).nextWhile s Char.isWhitespace).get s = 'a'`

* `let s := "a  "; ((0 : Pos.Raw).nextWhile s Char.isWhitespace).get s = 'a'`

* `let s := "ba  "; (Pos.Raw.nextWhile s Char.isWhitespace 0).get s = 'b'`
 -/
String.Pos.Raw.nextWhile : String → (Char → Bool) → String.Pos.Raw → String.Pos.Raw
-- Std.Tactic.Do.Syntax
/-- The discharging step in `vcgen … with`. It is a single `grind`-mode tactic (e.g. `finish`,
`intro`) so it can share `vcgen`'s internalised E-graph. The `tactic` alternative is a
lower-priority catch-all so that a non-`grind` step (e.g. `with grind`, `with simp`) still parses
and the elaborator can report a helpful error instead of a raw `expected grind` parser error.
 -/
Lean.Parser.Category.vcgenDischarge : Lean.Parser.Category
-- Init.Data.Bool
Bool.or_eq_decide : ∀ (p q : Bool), (p || q) = decide (p = true ∨ q = true)
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instIsAddApplyUpperHalfPlaneComplex : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ}, IsAddApply (ModularForm Γ k) UpperHalfPlane ℂ
-- Aesop.Forward.State
Aesop.PatSubstSource.hyp.sizeOf_spec : ∀ (fvarId : Lean.FVarId), sizeOf (Aesop.PatSubstSource.hyp fvarId) = 1 + sizeOf fvarId
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.glued.eq_1 : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰)
  [inst_5 :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.Limits.PreservesColimitsOfShape J
        (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))]
  [inst_6 : Quiver.IsThin 𝒰.I₀] [inst_7 : Small.{u, u_2} 𝒰.I₀] [inst_8 : AlgebraicGeometry.IsZariskiLocalAtTarget P],
  d.glued = CategoryTheory.MorphismProperty.Over.mk ⊤ d.relativeGluingData.toBase ⋯
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.prodMonoidal : (C₁ : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
    [CategoryTheory.MonoidalCategory C₁] →
      (C₂ : Type u₂) →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [CategoryTheory.MonoidalCategory C₂] → CategoryTheory.MonoidalCategory (C₁ × C₂)
-- Init.Data.Nat.Div.Basic
Nat.div_eq : ∀ (x y : ℕ), x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- If `L/K` is finite and normal, then `spectralNorm K L x = supr (λ (σ : Gal(L/K)), f (σ x))`.  -/
spectralNorm_eq_iSup_of_finiteDimensional_normal : ∀ (K : Type u_2) [inst : NormedField K] (L : Type u_3) [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hn : Normal K L] {f : AlgebraNorm K L},
  IsPowMul ⇑f →
    IsNonarchimedean ⇑f → (∀ (x : K), f ((algebraMap K L) x) = ‖x‖) → ∀ (x : L), spectralNorm K L x = ⨆ σ, f (σ x)
-- Mathlib.LinearAlgebra.Span.Basic
/-- There is no vector subspace between `s` and `K ∙ x ⊔ s`, `WCovBy` version.  -/
Submodule.wcovBy_span_singleton_sup : ∀ {K : Type u_3} {V : Type u_6} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (x : V)
  (s : Submodule K V), s ⩿ K ∙ x ⊔ s
-- Mathlib.Order.Filter.Finite
Filter.iInf_principal : ∀ {α : Type u} {ι : Sort w} [Finite ι] (f : ι → Set α), ⨅ i, Filter.principal (f i) = Filter.principal (⋂ i, f i)
-- Mathlib.Order.Booleanisation
Booleanisation.comp_sdiff_lift : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (a b : α),
  Booleanisation.comp a \ Booleanisation.lift b = Booleanisation.comp (a ⊔ b)
-- Std.Http.Data.Chunk
/-- An empty chunk with no data and no extensions.
 -/
Std.Http.Chunk.empty : Std.Http.Chunk
-- Mathlib.LinearAlgebra.Complex.Module
imaginaryPart_apply_coe : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  (a : A), ↑(imaginaryPart a) = -Complex.I • 2⁻¹ • (a - star a)
-- Std.Http.Server.Connection
/-- The socket address of the remote client.
 -/
Std.Http.Server.RemoteAddr.addr : Std.Http.Server.RemoteAddr → Std.Net.SocketAddress
-- Mathlib.Tactic.NormNum.Ordinal
/-- The `norm_num` extension for inequality on ordinals.  -/
Mathlib.Meta.NormNum.evalOrdinalLE : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- The transpose of an invertible matrix is invertible.  -/
Matrix.invertibleTranspose : {n : Type u_2} →
  {α : Type u_3} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] →
        [inst_2 : CommSemiring α] → (A : Matrix n n α) → [Invertible A] → Invertible A.transpose
-- Lean.Meta.Tactic.Grind.Action
Lean.Meta.Grind.Action.mbtc : Lean.Meta.Grind.Action
-- Init.MetaTypes
/-- When `true` (default: `true`), reduces `match` expressions applied to constructors.
 -/
Lean.Meta.Simp.Config.iota : Lean.Meta.Simp.Config → Bool
-- Mathlib.Algebra.BigOperators.Option
Finset.sum_eraseNone : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (f : α → M) (s : Finset (Option α)),
  ∑ x ∈ Finset.eraseNone s, f x = ∑ x ∈ s, Option.elim' 0 f x
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.measurableSet_of_null : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [μ.IsComplete],
  μ s = 0 → MeasurableSet s
-- Std.Http.Data.URI.Basic
Std.Http.URI.instInhabitedAuthority : Inhabited Std.Http.URI.Authority
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteGrp.cone.eq_1 : ∀ (P : ProfiniteGrp.{u}), P.cone = { pt := P, π := { app := ProfiniteGrp.proj, naturality := ⋯ } }
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Functor composition induces a functor on augmented cosimplicial objects.  -/
CategoryTheory.CosimplicialObject.Augmented.whiskeringObj : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : Type u_1) →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.Functor C D →
          CategoryTheory.Functor (CategoryTheory.CosimplicialObject.Augmented C)
            (CategoryTheory.CosimplicialObject.Augmented D)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.isRegular_preAleph_add_one : ∀ {o : Ordinal.{u_1}}, Ordinal.omega0 ≤ o → (Cardinal.preAleph (o + 1)).IsRegular
-- Std.Http.Server.Connection
Std.Http.Server.RemoteAddr.mk.sizeOf_spec : ∀ (addr : Std.Net.SocketAddress), sizeOf { addr := addr } = 1 + sizeOf addr
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.isCommMonObj_spec_asOver_spec : ∀ {R A : CommRingCat} [inst : Bialgebra ↑R ↑A] [Coalgebra.IsCocomm ↑R ↑A],
  CategoryTheory.IsCommMonObj ((AlgebraicGeometry.Spec A).asOver (AlgebraicGeometry.Spec R))
-- Lean.Meta.Tactic.Util
Lean.Meta.TacticResultCNM.modified : Lean.MVarId → Lean.Meta.TacticResultCNM
-- Mathlib.Logic.Equiv.Defs
Equiv.instEquivLike : {α : Sort u} → {β : Sort v} → EquivLike (α ≃ β) α β
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A shorthand for `toCoconeFunctor.obj`  -/
CategoryTheory.Limits.Bicone.toCocone : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} → CategoryTheory.Limits.Bicone F → CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor F)
-- Lean.Elab.Binders
/-- Helper function for `expandMatchAltsIntoMatch`.
 -/
_private.Lean.Elab.Binders.0.Lean.Elab.Term.expandMatchAltsIntoMatchAux : Lean.Syntax → Bool → Bool → ℕ → Array Lean.Syntax → Array Lean.Ident → Lean.MacroM Lean.Syntax
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.unop_natCast : ∀ {R : Type u_1} [inst : NatCast R] (n : ℕ), AddOpposite.unop ↑n = ↑n
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C_neg_one : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.C R (-1) = Polynomial.X
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.IsLocalizationMap.mulEquiv_comp : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] {f : M → N},
  S.IsLocalizationMap f →
    ∀ {E : Type u_4} [inst_3 : EquivLike E N P] [MulEquivClass E N P] (e : E), S.IsLocalizationMap (⇑e ∘ f)
-- Mathlib.Data.Nat.Cast.Commute
Commute.ofNat_right : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (x : α) (n : ℕ) [inst_1 : n.AtLeastTwo], Commute x (OfNat.ofNat n)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundaries₁_eq_bot_of_isTrivial : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G) [A.IsTrivial],
  groupCohomology.coboundaries₁ A = ⊥
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
/-- This naming follows the convention of `NormedSpace.expSeries_apply_eq'`.  -/
ordinaryHypergeometricSeries_apply_eq' : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (a b c : 𝕂) (x : 𝔸),
  (fun n => (ordinaryHypergeometricSeries 𝔸 a b c n) fun x_1 => x) = fun n =>
    ((↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n
-- Mathlib.AlgebraicTopology.Quasicategory.Basic
SSet.Quasicategory.hornFilling' : ∀ {S : SSet} [self : S.Quasicategory] ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : (SSet.horn (n + 2) i).toSSet ⟶ S),
  0 < i → i < Fin.last (n + 2) → ∃ σ, σ₀ = CategoryTheory.CategoryStruct.comp (SSet.horn (n + 2) i).ι σ
-- Init.Data.Float.Model.Float32
/-- Converts a `Float32.Model` to an `ISize`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float32.Model.toISize : Float32.Model → ISize
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ici_cast : ∀ {M : Type u_2} [inst : CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a : Fin n),
  ∏ i ≥ Fin.cast h a, f i = ∏ i ≥ a, f (Fin.cast h i)
-- Mathlib.Topology.Homeomorph.Lemmas
Equiv.isHomeomorph_of_discrete : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [DiscreteTopology X]
  [DiscreteTopology Y] (f : X ≃ Y), IsHomeomorph ⇑f
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
norm_jacobiTheta₂_term : ∀ (n : ℤ) (z τ : ℂ), ‖jacobiTheta₂_term n z τ‖ = Real.exp (-Real.pi * ↑n ^ 2 * τ.im - 2 * Real.pi * ↑n * z.im)
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instAddAction' : {M : Type u_1} → {α : Type u_3} → [inst : AddMonoid M] → [AddAction M α] → AddAction M (Lex α)
-- Mathlib.Algebra.Order.Sub.Basic
AddLECancellable.lt_tsub_iff_right : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [inst_2 : Sub α] [OrderedSub α] {a b c : α},
  AddLECancellable c → (a < b - c ↔ a + c < b)
-- Mathlib.MeasureTheory.Constructions.Projective
MeasureTheory.IsProjectiveLimit.isFiniteMeasure : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)]
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {μ : MeasureTheory.Measure ((i : ι) → α i)}
  [∀ (i : Finset ι), MeasureTheory.IsFiniteMeasure (P i)],
  MeasureTheory.IsProjectiveLimit μ P → MeasureTheory.IsFiniteMeasure μ
-- Batteries.Data.List.Lemmas
List.foldlIdx_const : ∀ {α : Type u_1} {xs : List α} {α_1 : Type u_2} {f : α_1 → α → α_1} {i : α_1} {s : ℕ},
  List.foldlIdx (Function.const ℕ f) i xs s = List.foldl f i xs
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Turns a `k`-module `A` with a compatible `DistribMulAction` of a monoid `G` into a
`k`-linear `G`-representation on `A`.  -/
Rep.ofDistribMulAction : (k : Type u) →
  (G : Type v) →
    [inst : Ring k] →
      [inst_1 : Monoid G] →
        (A : Type w') →
          [inst_2 : AddCommGroup A] →
            [inst_3 : Module k A] → [inst_4 : DistribMulAction G A] → [SMulCommClass G k A] → Rep.{w', u, v} k G
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.Hom.isModHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (self : M.Hom N),
  CategoryTheory.IsModHom A self.hom
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueue.initial : Array Aesop.PostponedSafeRule → Array (Aesop.IndexMatchResult Aesop.UnsafeRule) → Aesop.UnsafeQueue
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.id_comp : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M →ₚₗ[R] N), PolynomialLaw.id.comp f = f
-- Mathlib.LinearAlgebra.Matrix.Bilinear
/-- A version of `LinearMap.mulRight_mul` for matrix multiplication.  -/
mulRightLinearMap_mul : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_5} {A : Type u_6} [inst : Fintype m]
  [inst_1 : Fintype n] [inst_2 : Semiring R] [inst_3 : NonUnitalSemiring A] [inst_4 : Module R A]
  [inst_5 : IsScalarTower R A A] (a : Matrix m n A) (b : Matrix n o A),
  mulRightLinearMap l R (a * b) = mulRightLinearMap l R b ∘ₗ mulRightLinearMap l R a
-- Mathlib.Algebra.Algebra.Equiv
/-- Interpret an algebra equivalence as an algebra homomorphism.

This definition is included for symmetry with the other `to*Hom` projections.
The `simp` normal form is to use the coercion of the `AlgHomClass.coeTC` instance.  -/
AlgEquiv.toAlgHom : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] → [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → (A₁ ≃ₐ[R] A₂) → A₁ →ₐ[R] A₂
-- Mathlib.Logic.Encodable.Basic
/-- The equivalence between the encodable type `α` and `ULower α : Type`.  -/
ULower.equiv : (α : Type u_1) → [inst : Encodable α] → α ≃ ULower α
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
AEMeasurable.withDensity_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} {x : MeasurableSpace β}
  {f : α → β}, AEMeasurable f μ → ∀ (ν : MeasureTheory.Measure α), AEMeasurable f (ν.withDensity (μ.rnDeriv ν))