mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.AlgCat.Limits
AlgCat.semiringObj : {R : Type u} →
  [inst : CommRing R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (AlgCat R)) →
          (j : J) → Semiring ((F.comp (CategoryTheory.forget (AlgCat R))).obj j)
-- Mathlib.Algebra.MvPolynomial.SchwartzZippel
_private.Mathlib.Algebra.MvPolynomial.SchwartzZippel.0.«term_^^_» : Lean.TrailingParserDescr
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonRenameFile : Lean.FromJson Lean.Lsp.RenameFile
-- Mathlib.Topology.UniformSpace.Cauchy
/-- The construction `interUnionBalls` is used to have a relatively compact set.  -/
isCompact_closure_interUnionBalls : ∀ {α : Type u} [uniformSpace : UniformSpace α] {p : ℕ → Prop} {U : ℕ → SetRel α α},
  (uniformity α).HasBasis p U →
    ∀ [CompleteSpace α] (xs : ℕ → α) (u : ℕ → ℕ), IsCompact (closure (interUnionBalls xs u U))
-- Mathlib.Probability.Independence.Integration
ProbabilityTheory.IndepFun.integral_fun_comp_mul_comp : ∀ {Ω : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝓧 : Type u_3}
  {𝓨 : Type u_4} [inst_1 : MeasurableSpace 𝓧] [inst_2 : MeasurableSpace 𝓨] {X : Ω → 𝓧} {Y : Ω → 𝓨} {f : 𝓧 → 𝕜}
  {g : 𝓨 → 𝕜},
  ProbabilityTheory.IndepFun X Y μ →
    AEMeasurable X μ →
      AEMeasurable Y μ →
        MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map X μ) →
          MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map Y μ) →
            ∫ (ω : Ω), f (X ω) * g (Y ω) ∂μ = (∫ (ω : Ω), f (X ω) ∂μ) * ∫ (ω : Ω), g (Y ω) ∂μ
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.isoMk_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom)
            (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f)))
      CategoryTheory.Lax.OplaxTrans.isoMk._auto_1)
  (a : B), (CategoryTheory.Lax.OplaxTrans.isoMk app naturality).hom.as.app a = (app a).hom
-- Init.Data.SInt.Lemmas
ISize.toInt_toInt16 : ∀ (x : ISize), x.toInt16.toInt = x.toInt.bmod (2 ^ 16)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
/-- `DayConvolutionInternalHom F G H` asserts that `H` is the value at `G` of
an internal hom functor of `F` for the Day convolution monoidal structure.
This is phrased as the data of a limit `CategoryTheory.Wedge`
(i.e an end) on `internalHomDiagramFunctor F|>.obj G|>.obj c` and
`c`, with tip `(H.obj G).obj c` and a compatibility condition asserting that
the functoriality of `H` identifies to the functoriality of ends.  -/
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            [CategoryTheory.MonoidalClosed V] →
              CategoryTheory.Functor C V →
                CategoryTheory.Functor C V → CategoryTheory.Functor C V → Type (max (max (max u₁ u₂) v₁) v₂)
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- The subgroup defined by the class of `1` for a congruence relation on a group.
 -/
Con.subgroup : {G : Type u_1} → [inst : Group G] → Con G → Subgroup G
-- Mathlib.Algebra.GroupWithZero.Units.Equiv
Equiv.divRight₀_symm_apply : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) (x : G₀),
  (Equiv.symm (Equiv.divRight₀ a ha)) x = x * a
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.instAlgebra : {R : Type u_1} →
  [inst : Semiring R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {R₀ : Type u_3} → [inst_2 : CommSemiring R₀] → [Algebra R₀ R] → Algebra R₀ (OreLocalization S R)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- The element in `Splitting.IndexSet Δ` attached to an epimorphism `f : Δ ⟶ Δ'`.  -/
CategoryTheory.SimplicialObject.Splitting.IndexSet.mk : {Δ Δ' : SimplexCategory} →
  (f : Δ ⟶ Δ') → [CategoryTheory.Epi f] → CategoryTheory.SimplicialObject.Splitting.IndexSet (Opposite.op Δ)
-- Mathlib.Algebra.Group.Center
Set.addCentralizer_addCentralizer_comm_of_comm : ∀ {M : Type u_1} {S : Set M} [inst : Add M],
  (∀ x ∈ S, ∀ y ∈ S, x + y = y + x) →
    ∀ x ∈ S.addCentralizer.addCentralizer, ∀ y ∈ S.addCentralizer.addCentralizer, x + y = y + x
-- Mathlib.Data.Finset.SMulAntidiagonal
Set.IsWF.min_smul : ∀ {G : Type u_1} {P : Type u_2} [inst : LinearOrder G] [inst_1 : LinearOrder P] [inst_2 : SMul G P]
  [inst_3 : IsOrderedSMul G P] {s : Set G} {t : Set P} (hs : s.IsWF) (ht : t.IsWF) (hsn : s.Nonempty)
  (htn : t.Nonempty), ⋯.min ⋯ = hs.min hsn • ht.min htn
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- `HasBinaryBiproducts C` represents the existence of a bicone which is
simultaneously a limit and a colimit of the diagram `pair P Q`, for every `P Q : C`.  -/
CategoryTheory.Limits.HasBinaryBiproducts : (C : Type uC) → [inst : CategoryTheory.Category.{uC', uC} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → Prop
-- Mathlib.Algebra.Regular.Opposite
/-- **Alias** of the reverse direction of `isLeftRegular_op`. -/
IsLeftRegular.op : ∀ {R : Type u_1} [inst : Mul R] {a : R}, IsRightRegular a → IsLeftRegular (MulOpposite.op a)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The first projection functor `ShortComplex C ⥤ C`.  -/
CategoryTheory.ShortComplex.π₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.Functor (CategoryTheory.ShortComplex C) C
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.subtype_comp_codRestrict : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (b : M), f b ∈ p), p.subtype ∘ₛₗ LinearMap.codRestrict p f h = f
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
/-- The cofan given by the inclusions
`X.ιNormalizedChainComplex x : R ⟶ (X.normalizedChainComplex R).X n` for all
nondegenerate `n`-simplices `x` of a simplicial set `X`.  -/
SSet.cofanNormalizedChainComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasCoproducts C] →
      [CategoryTheory.Preadditive C] → (X : SSet) → (R : C) → (n : ℕ) → CategoryTheory.Limits.Cofan fun x => R
-- Mathlib.Data.Num.Basic
/-- The predecessor of a `Num` as an `Option Num`, where `ppred 0 = none`  -/
Num.ppred : Num → Option Num
-- Mathlib.CategoryTheory.Adjunction.Basic
_private.Mathlib.CategoryTheory.Adjunction.Basic.0.CategoryTheory.Adjunction.he'' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G_obj : D → C} (e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)),
  (∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
      (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)) →
    ∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G_obj Y),
      CategoryTheory.CategoryStruct.comp (F.map f) ((e X Y).symm g) =
        (e X' Y).symm (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.union_mul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s₁ s₂ t : Finset α}, (s₁ ∪ s₂) * t = s₁ * t ∪ s₂ * t
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.monoidal_tensorHom_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X₁ Y₁ X₂ Y₂ : CategoryTheory.Comon C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom =
    CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom
-- Init.Data.BitVec.Lemmas
BitVec.ult_eq_decide_lt : ∀ {w : ℕ} {x y : BitVec w}, x.ult y = decide (x < y)
-- Mathlib.Order.SupClosed
/-- **Alias** of the reverse direction of `supClosed_preimage_ofDual`. -/
InfClosed.dual : ∀ {α : Type u_3} [inst : Lattice α] {s : Set α}, InfClosed s → SupClosed (⇑OrderDual.ofDual ⁻¹' s)
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.IsInvertedBy.unop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {W : CategoryTheory.MorphismProperty C} {L : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ},
  W.op.IsInvertedBy L → W.IsInvertedBy L.unop
-- Mathlib.NumberTheory.NumberField.DirichletDensity
NumberField.Set.primeIdealZetaSum_def : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (s : ℝ),
  NumberField.Set.primeIdealZetaSum S s = ∑' (𝔭 : ↑S), ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSemanticTokensRangeParams : Lean.FromJson Lean.Lsp.SemanticTokensRangeParams
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C =
    {
      obj := fun A =>
        CategoryTheory.LaxMonoidalFunctor.of (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A),
      map := fun {X Y} f => { hom := { app := fun x => f.hom, naturality := ⋯ }, isMonoidal := ⋯ }, map_id := ⋯,
      map_comp := ⋯ }
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_ric_eq_mkSlice_rio : ∀ {α : Type u_1} {xs : Array α} {hi : ℕ},
  (Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rio.Sliceable.mkSlice xs *...hi + 1
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.div_right : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {s t : Set G},
  IsOpen s → IsOpen (s / t)
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.argSelfAdjoint_coe : ∀ {A : Type u_1} [inst : CStarAlgebra A] (u : ↥(unitary A)), ↑(Unitary.argSelfAdjoint u) = cfc (fun x => ↑x.arg) ↑u
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.BodyInfo.mk.sizeOf_spec : ∀ (value? : Option Lean.Expr), sizeOf { value? := value? } = 1 + sizeOf value?
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_toNat : ∀ (o : Ordinal.{u_1}), Cardinal.toNat (Cardinal.aleph o) = 0
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.invertibleAlgebraMapEquiv_symm_apply_invOf : ∀ {R : Type u1} [inst : CommRing R] (M : Type u2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R)
  (x : Invertible r), ⅟((algebraMap R (ExteriorAlgebra R M)) r) = (algebraMap R (ExteriorAlgebra R M)) ⅟r
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.GNonUnitalNonAssocSemiring.mk : {ι : Type u_1} →
  {A : ι → Type u_2} →
    [inst : Add ι] →
      [inst_1 : (i : ι) → AddCommMonoid (A i)] →
        [toGMul : GradedMonoid.GMul A] →
          (∀ {i j : ι} (a : A i), GradedMonoid.GMul.mul a 0 = 0) →
            (∀ {i j : ι} (b : A j), GradedMonoid.GMul.mul 0 b = 0) →
              (∀ {i j : ι} (a : A i) (b c : A j),
                  GradedMonoid.GMul.mul a (b + c) = GradedMonoid.GMul.mul a b + GradedMonoid.GMul.mul a c) →
                (∀ {i j : ι} (a b : A i) (c : A j),
                    GradedMonoid.GMul.mul (a + b) c = GradedMonoid.GMul.mul a c + GradedMonoid.GMul.mul b c) →
                  DirectSum.GNonUnitalNonAssocSemiring A
-- Mathlib.Order.Filter.Basic
Filter.Frequently.and_eventually : ∀ {α : Type u} {p q : α → Prop} {f : Filter α},
  (∃ᶠ (x : α) in f, p x) → (∀ᶠ (x : α) in f, q x) → ∃ᶠ (x : α) in f, p x ∧ q x
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.A_two : CartanMatrix.A 2 = !![2, -1; -1, 2]
-- Init.Data.List.Sort.Lemmas
List.merge_stable : ∀ {α : Type u_1} {le : α → α → Bool} (xs ys : List (α × ℕ)),
  (∀ (x y : α × ℕ), x ∈ xs → y ∈ ys → x.2 ≤ y.2) →
    List.map (fun x => x.1) (xs.merge ys (List.zipIdxLE le)) =
      (List.map (fun x => x.1) xs).merge (List.map (fun x => x.1) ys) le
-- Init.System.IOError
IO.Error.illegalOperation.inj : ∀ {osCode : UInt32} {details : String} {osCode_1 : UInt32} {details_1 : String},
  IO.Error.illegalOperation osCode details = IO.Error.illegalOperation osCode_1 details_1 →
    osCode = osCode_1 ∧ details = details_1
-- Init.Data.BitVec.Lemmas
BitVec.msb_replicate : ∀ {n w : ℕ} {x : BitVec w}, (BitVec.replicate n x).msb = (decide (0 < n) && x.msb)
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Whether `pp.analysis.namedArg` was set for the motive argument.  -/
Lean.PrettyPrinter.Delaborator.AppMatchState.motiveNamed : Lean.PrettyPrinter.Delaborator.AppMatchState → Bool
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- An `n`-preprimitive action is `n`-pretransitive.  -/
AddAction.IsMultiplyPreprimitive.isMultiplyPretransitive : ∀ (M : Type u_1) (α : Type u_2) {inst : AddGroup M} {inst_1 : AddAction M α} (n : ℕ)
  [self : AddAction.IsMultiplyPreprimitive M α n], AddAction.IsMultiplyPretransitive M α n
-- Mathlib.RingTheory.Unramified.Basic
Algebra.TensorProduct.lmul''.eq_1 : ∀ (R : Type uR) {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  Algebra.TensorProduct.lmul'' R =
    Algebra.TensorProduct.algHomOfLinearMapTensorProduct
      (let __spread.0 := LinearMap.mul' R S;
      { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ })
      ⋯ ⋯
-- Mathlib.Analysis.InnerProductSpace.PiL2
Module.Basis.toOrthonormalBasis.eq_1 : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (v : Module.Basis ι 𝕜 E) (hv : Orthonormal 𝕜 ⇑v),
  v.toOrthonormalBasis hv = { repr := (v.equivFun.trans (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm).isometryOfInner ⋯ }
-- Std.Data.ExtHashSet.Basic
Std.ExtHashSet.instDecidableMem : {α : Type u} →
  [inst : BEq α] →
    [inst_1 : Hashable α] →
      [inst_2 : EquivBEq α] → [inst_3 : LawfulHashable α] → {m : Std.ExtHashSet α} → {a : α} → Decidable (a ∈ m)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F] {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsColimit c) (j : J) {Z : C} (h : c.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
      (CategoryTheory.CategoryStruct.comp (hc.coconePointUniqueUpToIso (CategoryTheory.Limits.colimit.isColimit F)).inv
        h) =
    CategoryTheory.CategoryStruct.comp (c.ι.app j) h
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
/-- This function produces a subword of a word `L` by cancelling the first and last letters of `L`
as long as possible. If `L` is reduced, the resulting word will be cyclically reduced.  -/
FreeGroup.reduceCyclically : {α : Type u} → [DecidableEq α] → List (α × Bool) → List (α × Bool)
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.insert_Icc_add_one_left_eq_Icc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [SuccAddOrder α] {a b : α}, a ≤ b → insert a (Finset.Icc (a + 1) b) = Finset.Icc a b
-- Mathlib.CategoryTheory.Localization.Predicate
/-- If `L₁ : C ⥤ D₁` and `L₂ : C ⥤ D₂` are two localization functors for the
same `MorphismProperty C`, any functor `F : D₁ ⥤ D₂` equipped with an isomorphism
`L₁ ⋙ F ≅ L₂` is isomorphic to the functor of the equivalence given by `uniq`.  -/
CategoryTheory.Localization.isoUniqFunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D₁ : Type u_4} →
      {D₂ : Type u_5} →
        [inst_1 : CategoryTheory.Category.{v_4, u_4} D₁] →
          [inst_2 : CategoryTheory.Category.{v_5, u_5} D₂] →
            (L₁ : CategoryTheory.Functor C D₁) →
              (L₂ : CategoryTheory.Functor C D₂) →
                (W' : CategoryTheory.MorphismProperty C) →
                  [inst_3 : L₁.IsLocalization W'] →
                    [inst_4 : L₂.IsLocalization W'] →
                      (F : CategoryTheory.Functor D₁ D₂) →
                        (L₁.comp F ≅ L₂) → (F ≅ (CategoryTheory.Localization.uniq L₁ L₂ W').functor)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.instCoeHeadContinuousMap : {R : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      {P : Type u_4} →
        {Q : Type u_5} →
          [inst : Ring R] →
            [inst_1 : AddCommGroup V] →
              [inst_2 : Module R V] →
                [inst_3 : TopologicalSpace P] →
                  [inst_4 : AddTorsor V P] →
                    [inst_5 : AddCommGroup W] →
                      [inst_6 : Module R W] →
                        [inst_7 : TopologicalSpace Q] → [inst_8 : AddTorsor W Q] → CoeHead (P →ᴬ[R] Q) C(P, Q)
-- Mathlib.Data.Set.Pairwise.Basic
Set.PairwiseDisjoint.elim : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {s : Set ι} {f : ι → α},
  s.PairwiseDisjoint f → ∀ {i j : ι}, i ∈ s → j ∈ s → ¬Disjoint (f i) (f j) → i = j
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabMatch.elabMatchDefault : Lean.Syntax → Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.values_eq_on_of_interpolate_eq : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r r' : ι → F),
  Set.InjOn v ↑s → (Lagrange.interpolate s v) r = (Lagrange.interpolate s v) r' → ∀ i ∈ s, r i = r' i
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformGroup.of_left_right : ∀ {β : Type u_2} [inst : UniformSpace β] [inst_1 : Group β] [IsLeftUniformGroup β] [IsRightUniformGroup β],
  IsUniformGroup β
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
CategoryTheory.WalkingIso.fromIso_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y),
  (CategoryTheory.WalkingIso.fromIso e).obj CategoryTheory.WalkingIso.zero = X
-- Mathlib.MeasureTheory.Measure.WithDensity
/-- In a countable space, every measure is s-finite.  -/
MeasureTheory.instSFiniteOfCountable : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable α], MeasureTheory.SFinite μ
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Presieve.FactorsThruAlong.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (S : CategoryTheory.Presieve Y)
  (T : CategoryTheory.Presieve X) (f : Y ⟶ X),
  S.FactorsThruAlong T f =
    ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄,
      S g → ∃ W i e, T e ∧ CategoryTheory.CategoryStruct.comp i e = CategoryTheory.CategoryStruct.comp g f
-- Mathlib.Analysis.Analytic.Constructions
AnalyticAt.sub : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {x : E},
  AnalyticAt 𝕜 f x → AnalyticAt 𝕜 g x → AnalyticAt 𝕜 (f - g) x
-- Mathlib.Analysis.RCLike.Basic
RCLike.nonneg_iff : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, 0 ≤ z ↔ 0 ≤ RCLike.re z ∧ RCLike.im z = 0
-- Mathlib.Algebra.Group.Units.Basic
RightCancelMonoid.mul_eq_one : ∀ {α : Type u} [inst : RightCancelMonoid α] [Subsingleton αˣ] {a b : α}, a * b = 1 ↔ a = 1 ∧ b = 1
-- Mathlib.CategoryTheory.Skeletal
/-- A category is skeletal if isomorphic objects are equal.  -/
CategoryTheory.Skeletal : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Prop
-- Mathlib.Probability.Distributions.Uniform
MeasureTheory.pdf.IsUniform.absolutelyContinuous : ∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} {x : MeasurableSpace Ω}
  {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E},
  MeasureTheory.pdf.IsUniform X s ℙ μ → (MeasureTheory.Measure.map X ℙ).AbsolutelyContinuous μ
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.indepFun_congr : ∀ {α : Type u_1} {Ω : Type u_2} {γ : Type u_6} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_10} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace γ] {f : Ω → β} {g : Ω → γ},
  ⇑κ =ᵐ[μ] ⇑η → (ProbabilityTheory.Kernel.IndepFun f g κ μ ↔ ProbabilityTheory.Kernel.IndepFun f g η μ)
-- Std.Time.Date.Unit.Weekday
_private.Std.Time.Date.Unit.Weekday.0.Std.Time.Weekday.toOrdinal.eq_4 : Std.Time.Weekday.thursday.toOrdinal = 4
-- Mathlib.CategoryTheory.Adjunction.Lifting.Right
/-- If `L ⋙ F` has a right adjoint, the domain of `L` has coreflexive equalizers and `F` is a
comonadic functor, then `L` has a right adjoint.
This is a special case of `isLeftAdjoint_triangle_lift` which is often more useful in practice.
 -/
CategoryTheory.isLeftAdjoint_triangle_lift_comonadic : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor B A) [CategoryTheory.ComonadicLeftAdjoint F] {L : CategoryTheory.Functor C B}
  [CategoryTheory.Limits.HasCoreflexiveEqualizers C] [(L.comp F).IsLeftAdjoint], L.IsLeftAdjoint
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- The recursor for WalkingIso, which constructs a term of `∏ (x : WalkingIso), A x` from
a term of `A zero` and a term of `A one`.  -/
CategoryTheory.WalkingIso.rec : {motive : CategoryTheory.WalkingIso → Sort u_1} →
  motive CategoryTheory.WalkingIso.zero →
    motive CategoryTheory.WalkingIso.one → (a : CategoryTheory.WalkingIso) → motive a
-- Mathlib.Logic.Small.Set
small_inter_of_left : ∀ {α : Type u1} (s t : Set α) [Small.{u, u1} ↑s], Small.{u, u1} ↑(s ∩ t)
-- Mathlib.Analysis.Convex.Function
ConvexOn.comp_concaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid α] [inst_4 : PartialOrder α] [inst_5 : AddCommMonoid β]
  [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 E] [inst_8 : SMul 𝕜 α] [inst_9 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {g : β → α}, ConvexOn 𝕜 (f '' s) g → ConcaveOn 𝕜 s f → AntitoneOn g (f '' s) → ConvexOn 𝕜 s (g ∘ f)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.isZero_homology_of_isZero_X₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C),
  CategoryTheory.Limits.IsZero S.X₂ → ∀ [inst_2 : S.HasHomology], CategoryTheory.Limits.IsZero S.homology
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k a : α}
  {fallback : β},
  Std.DTreeMap.Const.getD (t.erase k) a fallback =
    if cmp k a = Ordering.eq then fallback else Std.DTreeMap.Const.getD t a fallback
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Rotating the second of two vectors by `θ` scales their Kähler form by `cos θ + sin θ * I`.  -/
Orientation.kahler_rotation_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) (θ : Real.Angle),
  (o.kahler x) ((o.rotation θ) y) = ↑θ.toCircle * (o.kahler x) y
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instPartialOrder : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} → [inst_1 : TopologicalSpace β] → [PartialOrder β] → PartialOrder (α →ₘ[μ] β)