mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- a choice of left adjoint for `R`  -/
CategoryTheory.MonadicRightAdjoint.L : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {D : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        (R : CategoryTheory.Functor D C) → [self : CategoryTheory.MonadicRightAdjoint R] → CategoryTheory.Functor C D
-- Mathlib.Geometry.Euclidean.Inversion.Basic
ContinuousWithinAt.inversion : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {X : Type u_3} [inst_4 : TopologicalSpace X] {c x : X → P} {R : X → ℝ} {a₀ : X}
  {s : Set X},
  ContinuousWithinAt c s a₀ →
    ContinuousWithinAt R s a₀ →
      ContinuousWithinAt x s a₀ →
        x a₀ ≠ c a₀ → ContinuousWithinAt (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) s a₀
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.mk : (toPartOrd : PartOrd) → [isFintype : Fintype ↑toPartOrd] → FinPartOrd
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.cg_of_countable : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] [Countable M], FirstOrder.Language.Structure.CG L M
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
/-- Rewrite `ContinuousAlternatingMap.inCoordinates` using continuous linear equivalences.  -/
ContinuousAlternatingMap.inCoordinates_eq : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] {B₁ : Type u_3} (F₁ : Type u_4)
  [inst_1 : NormedAddCommGroup F₁] [inst_2 : NormedSpace 𝕜 F₁] {E₁ : B₁ → Type u_5}
  [inst_3 : (x : B₁) → AddCommGroup (E₁ x)] [inst_4 : (x : B₁) → Module 𝕜 (E₁ x)] [inst_5 : TopologicalSpace B₁]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_7 : (x : B₁) → TopologicalSpace (E₁ x)]
  [inst_8 : FiberBundle F₁ E₁] [inst_9 : VectorBundle 𝕜 F₁ E₁] {B₂ : Type u_6} (F₂ : Type u_7)
  [inst_10 : NormedAddCommGroup F₂] [inst_11 : NormedSpace 𝕜 F₂] {E₂ : B₂ → Type u_8}
  [inst_12 : (x : B₂) → AddCommGroup (E₂ x)] [inst_13 : (x : B₂) → Module 𝕜 (E₂ x)] [inst_14 : TopologicalSpace B₂]
  [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_16 : (x : B₂) → TopologicalSpace (E₂ x)]
  [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜 F₂ E₂] {x₀ x : B₁} {y₀ y : B₂} {ϕ : E₁ x [⋀^ι]→L[𝕜] E₂ y}
  (hx : x ∈ (trivializationAt F₁ E₁ x₀).baseSet) (hy : y ∈ (trivializationAt F₂ E₂ y₀).baseSet),
  ContinuousAlternatingMap.inCoordinates F₁ F₂ x₀ x y₀ y ϕ =
    ((↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₂ E₂ y₀) y hy)).compContinuousAlternatingMap
          ϕ).compContinuousLinearMap
      ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₁ E₁ x₀) x hx).symm
-- Mathlib.Algebra.Group.Pi.Basic
Pi.instSubtractionCommMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → SubtractionCommMonoid (f i)] → SubtractionCommMonoid ((i : I) → f i)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Finset.esymm_map_val : ∀ {R : Type u_1} [inst : CommSemiring R] {σ : Type u_2} (f : σ → R) (s : Finset σ) (n : ℕ),
  (Multiset.map f s.val).esymm n = ∑ t ∈ Finset.powersetCard n s, t.prod f
-- Mathlib.Data.Set.FiniteExhaustion
Set.FiniteExhaustion.subset_succ : ∀ {α : Type u_1} {s : Set α} (K : s.FiniteExhaustion) (n : ℕ), K n ⊆ K (n + 1)
-- Init.Control.Lawful.MonadLift.Instances
_private.Init.Control.Lawful.MonadLift.Instances.0.OptionT.bind.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.Data.Opposite
/-- If `X` is `u`-small, also `Xᵒᵖ` is `u`-small.  -/
Opposite.small : ∀ {X : Type v} [Small.{u, v} X], Small.{u, v} Xᵒᵖ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.instCategory.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.AddMon.instCategory =
    { Hom := fun M N => M.Hom N, id := CategoryTheory.AddMon.id,
      comp := fun {X Y Z} f g => CategoryTheory.AddMon.comp f g, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.isCancelAdd : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommMonoid M] {S : AddSubmonoid M} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) [IsCancelAdd M], IsCancelAdd N
-- Mathlib.Analysis.Quaternion
Quaternion.instNormedAlgebraReal : NormedAlgebra ℝ (Quaternion ℝ)
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenCoend.ι_desc_assoc : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C] {X : C} (f : (j : J) → (F.obj (Opposite.op j)).obj j ⟶ X)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp ((F.map g.op).app i) (f i) =
        CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j))
  (j : J) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenCoend.ι F j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenCoend.desc f hf) h) =
    CategoryTheory.CategoryStruct.comp (f j) h
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_ne_zero : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [H.IsFiniteRelIndex K], H.relIndex K ≠ 0
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- Restriction along the composition is isomorphic to the composition of restrictions.  -/
AlgebraicGeometry.Scheme.Modules.restrictFunctorComp : {X Y Z : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    (g : Y ⟶ Z) →
      [inst : AlgebraicGeometry.IsOpenImmersion f] →
        [inst_1 : AlgebraicGeometry.IsOpenImmersion g] →
          AlgebraicGeometry.Scheme.Modules.restrictFunctor (CategoryTheory.CategoryStruct.comp f g) ≅
            (AlgebraicGeometry.Scheme.Modules.restrictFunctor g).comp
              (AlgebraicGeometry.Scheme.Modules.restrictFunctor f)
-- Init.Data.Array.Find
Array.find?_eq_some_iff_append : ∀ {α : Type u_1} {p : α → Bool} {b : α} {xs : Array α},
  Array.find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as.push b ++ bs ∧ ∀ a ∈ as, (!p a) = true
-- Mathlib.GroupTheory.Sylow
/-- A generalization of **Sylow's first theorem**.
Every `p`-subgroup is contained in a Sylow `p`-subgroup.  -/
IsPGroup.exists_le_sylow : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {P : Subgroup G}, IsPGroup p ↥P → ∃ Q, P ≤ ↑Q
-- Lean.Parser.Extra
/-- The parser `many1Indent(p)` is equivalent to `withPosition((colGe p)+)`. This has the effect of
parsing one or more occurrences of `p`, where each subsequent `p` parse needs to be indented
the same or more than the first parse.

This parser has arity 1, and returns a list of the results from `p`.
`p` is "auto-grouped" if it is not arity 1.  -/
Lean.Parser.many1Indent : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.isoModSerre_iff_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f],
  P.isoModSerre f ↔ P.epiModSerre f
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Arg.erased.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity}, sizeOf Lean.Compiler.LCNF.Arg.erased = 1
-- Mathlib.Geometry.Euclidean.Congruence
/-- **Angle–Angle–Side (AAS) congruence**
If two triangles have two equal angles and a non-included side equal, then the triangles are
congruent. We require that one of the triangles is non-degenerate, the non-collinearity of the
other is then implied by the given equalities.  -/
EuclideanGeometry.angle_angle_side : ∀ {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [inst : NormedAddCommGroup V₁]
  [inst_1 : NormedAddCommGroup V₂] [inst_2 : InnerProductSpace ℝ V₁] [inst_3 : InnerProductSpace ℝ V₂]
  [inst_4 : MetricSpace P₁] [inst_5 : MetricSpace P₂] [inst_6 : NormedAddTorsor V₁ P₁] [inst_7 : NormedAddTorsor V₂ P₂]
  {a b c : P₁} {a' b' c' : P₂},
  ¬Collinear ℝ {a, b, c} →
    EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c' →
      EuclideanGeometry.angle b c a = EuclideanGeometry.angle b' c' a' →
        dist c a = dist c' a' → Congruent ![a, b, c] ![a', b', c']
-- Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
GenContFract.compExactValue.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] (pconts conts : GenContFract.Pair K) (fr : K),
  GenContFract.compExactValue pconts conts fr =
    if fr = 0 then conts.a / conts.b
    else (GenContFract.nextConts 1 fr⁻¹ pconts conts).a / (GenContFract.nextConts 1 fr⁻¹ pconts conts).b
-- Init.Data.Range.Polymorphic.PRange
Std.Rci.HasRcoIntersection.mk : {α : Type w} → (Std.Rci α → Std.Rco α → Std.Rco α) → Std.Rci.HasRcoIntersection α
-- Init.Data.List.Find
List.lookup_replicate_of_pos : ∀ {α : Type u_2} [inst : BEq α] {n : ℕ} {a : α} {α_1 : Type u_1} {b : α_1} {k : α},
  0 < n → List.lookup k (List.replicate n (a, b)) = if (k == a) = true then some b else none
-- Init.Data.UInt.Basic
instHModUSizeNat : HMod USize ℕ USize
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.mapBifunctor.d₂_eq_zero : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J),
  ¬c₂.Rel i₂ (c₂.next i₂) → HomologicalComplex.mapBifunctor.d₂ K₁ K₂ F c i₁ i₂ j = 0
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instMulAction : {α : Type u} →
  {β : Type v} →
    {𝕜 : Type u_2} →
      [inst : PseudoMetricSpace 𝕜] →
        [inst_1 : TopologicalSpace α] →
          [inst_2 : PseudoMetricSpace β] →
            [inst_3 : MonoidWithZero 𝕜] →
              [inst_4 : Zero β] →
                [inst_5 : MulAction 𝕜 β] → [IsBoundedSMul 𝕜 β] → MulAction 𝕜 (BoundedContinuousFunction α β)
-- Mathlib.Algebra.GroupWithZero.Action.Defs
Pi.single_apply_smul : ∀ {M₀ : Type u_2} {A : Type u_7} [inst : MonoidWithZero M₀] [inst_1 : Zero A] [inst_2 : MulActionWithZero M₀ A]
  {ι : Type u_12} [inst_3 : DecidableEq ι] (x : A) (i j : ι), Pi.single i 1 j • x = Pi.single i x j
-- Mathlib.Logic.IsEmpty.Basic
isEmpty_Prop : ∀ {p : Prop}, IsEmpty p ↔ ¬p
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
isLocalHomeomorph_circleExp : IsLocalHomeomorph ⇑Circle.exp
-- Init.Data.SInt.Lemmas
ISize.toBitVec_toInt64 : ∀ (x : ISize), x.toInt64.toBitVec = BitVec.signExtend 64 x.toBitVec
-- Mathlib.LinearAlgebra.CrossProduct
/-- Alternative form of the scalar triple product expansion of the vector triple product.  -/
cross_cross_eq_smul_sub_smul' : ∀ {R : Type u_1} [inst : CommRing R] (u v w : Fin 3 → R),
  (crossProduct u) ((crossProduct v) w) = (u ⬝ᵥ w) • v - (v ⬝ᵥ u) • w
-- Lean.Data.Lsp.Window
Lean.Lsp.instToJsonShowMessageParams : Lean.ToJson Lean.Lsp.ShowMessageParams
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.mk'_strictMono : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (p : P), StrictMono (AffineSubspace.mk' p)
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.sectionsπMonoidHom.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat) (j : J),
  GrpCat.sectionsπMonoidHom F j = { toFun := fun x => ↑x j, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.intTrace.eq_1 : ∀ (A : Type u_1) (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [inst_4 : IsIntegrallyClosed A] [inst_5 : IsDomain B] [inst_6 : IsIntegrallyClosed B] [inst_7 : Module.Finite A B]
  [inst_8 : Module.IsTorsionFree A B], Algebra.intTrace A B = Algebra.intTraceAux A (FractionRing A) (FractionRing B) B
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.isUniformEmbedding_toCloseds : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : T2Space α], IsUniformEmbedding TopologicalSpace.Compacts.toCloseds
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.closure_empty : ∀ {K : Type u} [inst : DivisionRing K], Subfield.closure ∅ = ⊥
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.condKernelUnitBorel.eq_1 : ∀ {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  [inst_1 : Nonempty Ω] (κ : ProbabilityTheory.Kernel Unit (α × Ω)) [inst_2 : ProbabilityTheory.IsFiniteKernel κ],
  κ.condKernelUnitBorel =
    ProbabilityTheory.Kernel.borelMarkovFromReal Ω
      (κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))).condKernelUnitReal
-- Mathlib.RingTheory.Polynomial.Basic
Ideal.degreeLE.eq_1 : ∀ {R : Type u} [inst : Semiring R] (I : Ideal (Polynomial R)) (n : WithBot ℕ),
  I.degreeLE n = Polynomial.degreeLE R n ⊓ I.ofPolynomial
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- Given a continuous `𝕜`-bilinear map `B : F₁ →L[𝕜] F₂ →L[𝕜] F₃`, a measure `μ` on `E`,
and a function `φ : E → F₂` which is integrable on `K`, this is the *continuous* `𝕜`-linear map
`f ↦ ∫ x, B (f x) (φ x) ∂μ` from `𝓓^{n}_{K}(E, F₁)` to `F₃`. Otherwise, this is the zero map.  -/
ContDiffMapSupportedIn.integralAgainstBilinCLM : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace ℝ E] →
          {n : ℕ∞} →
            {K : TopologicalSpace.Compacts E} →
              {m : MeasurableSpace E} →
                [OpensMeasurableSpace E] →
                  {F₁ : Type u_5} →
                    {F₂ : Type u_6} →
                      {F₃ : Type u_7} →
                        [inst_4 : NormedAddCommGroup F₁] →
                          [inst_5 : NormedSpace 𝕜 F₁] →
                            [inst_6 : NormedSpace ℝ F₁] →
                              [inst_7 : NormedAddCommGroup F₂] →
                                [inst_8 : NormedSpace 𝕜 F₂] →
                                  [inst_9 : NormedAddCommGroup F₃] →
                                    [inst_10 : NormedSpace 𝕜 F₃] →
                                      [inst_11 : SMulCommClass ℝ 𝕜 F₁] →
                                        [inst_12 : NormedSpace ℝ F₃] →
                                          [SMulCommClass ℝ 𝕜 F₃] →
                                            (F₁ →L[𝕜] F₂ →L[𝕜] F₃) →
                                              MeasureTheory.Measure E →
                                                (E → F₂) → ContDiffMapSupportedIn E F₁ n K →L[𝕜] F₃
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.symm_image_target_eq_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  ↑e.symm '' e.target = e.source
-- Init.Data.Array.Lemmas
Array.some_eq_getElem?_iff : ∀ {α : Type u_1} {b : α} {i : ℕ} {xs : Array α}, some b = xs[i]? ↔ ∃ (h : i < xs.size), xs[i] = b
-- Mathlib.Tactic.Widget.StringDiagram
/-- The penrose variable associated with a node.  -/
Mathlib.Tactic.Widget.StringDiagram.Node.toPenroseVar : Mathlib.Tactic.Widget.StringDiagram.Node → Mathlib.Tactic.Widget.StringDiagram.PenroseVar
-- Mathlib.Algebra.DirectSum.Module
/-- `curryEquiv` as a linear equiv.  -/
DirectSum.sigmaLcurryEquiv : (R : Type u) →
  [inst : Semiring R] →
    {ι : Type v} →
      {α : ι → Type u_1} →
        {δ : (i : ι) → α i → Type w} →
          [DecidableEq ι] →
            [inst_2 : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] →
              [inst_3 : (i : ι) → (j : α i) → Module R (δ i j)] →
                (DirectSum ((x : ι) × α x) fun i => δ i.fst i.snd) ≃ₗ[R]
                  DirectSum ι fun i => DirectSum (α i) fun j => δ i j
-- Init.Grind.Config
Lean.Grind.OrderConfig.mk.injEq : ∀ (toNoopConfig toNoopConfig_1 : Lean.Grind.NoopConfig),
  ({ toNoopConfig := toNoopConfig } = { toNoopConfig := toNoopConfig_1 }) = (toNoopConfig = toNoopConfig_1)
-- Mathlib.Order.Preorder.Finsupp
Finsupp.coe_le_coe : ∀ {ι : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : LE M] {f g : ι →₀ M}, ⇑f ≤ ⇑g ↔ f ≤ g
-- Lean.DocString.Parser
Lean.Doc.Parser.instOrdUnorderedListType : Ord Lean.Doc.Parser.UnorderedListType
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
CategoryTheory.ConcreteCategory.instMonoOfHomCoeHomOfPreservesMonomorphismsForget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [(CategoryTheory.forget C).PreservesMonomorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f],
  CategoryTheory.Mono (TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f))
-- Batteries.Recycling.MonadSatisfying.Basic
/-- `SatisfiesM` distributes over `<*>`, strongest postcondition version.  -/
SatisfiesM.seq_post : ∀ {m : Type u_1 → Type u_2} {α α_1 : Type u_1} {p₁ : (α → α_1) → Prop} {f : m (α → α_1)} {p₂ : α → Prop}
  [inst : Applicative m] [LawfulApplicative m] {x : m α},
  SatisfiesM p₁ f → SatisfiesM p₂ x → SatisfiesM (fun c => ∃ f a, p₁ f ∧ p₂ a ∧ c = f a) (f <*> x)
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- The underlying type.  -/
Semigrp.carrier : Semigrp → Type u
-- Mathlib.Topology.UnitInterval
Set.Icc.addNSMul_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] {a b : α} (h : a ≤ b) {δ : α},
  ↑(Set.Icc.addNSMul h δ 0) = a
-- Mathlib.Algebra.Polynomial.Degree.Units
Polynomial.Monic.natDegree_pos_of_not_isUnit : ∀ {R : Type u} [inst : CommSemiring R] {p : Polynomial R}, p.Monic → ¬IsUnit p → 0 < p.natDegree
-- Init.Data.UInt.Lemmas
USize.toUInt32_toUInt16 : ∀ (n : USize), n.toUInt16.toUInt32 = n.toUInt32 % 65536
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α},
  (Std.Internal.List.eraseKey k l).length = if Std.Internal.List.containsKey k l = true then l.length - 1 else l.length
-- Mathlib.Algebra.Module.Torsion.Basic
/-- The `S`-torsion submodule, containing all elements `x` of `M` such that `a • x = 0` for some
`a` in `S`.  -/
Submodule.torsion' : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          (S : Type u_3) →
            [inst_3 : CommMonoid S] → [inst_4 : DistribMulAction S M] → [SMulCommClass S R M] → Submodule R M
-- Mathlib.Control.ULift
PLift.map_up : ∀ {α : Sort u} {β : Sort v} (f : α → β) (a : α), PLift.map f { down := a } = { down := f a }
-- Lean.Util.ParamMinimizer
Lean.Util.ParamMinimizer.Status.precise.sizeOf_spec : sizeOf Lean.Util.ParamMinimizer.Status.precise = 1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.reverse_comp_reverse : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M}, CliffordAlgebra.reverse ∘ₗ CliffordAlgebra.reverse = LinearMap.id
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.toOption.eq_4 : ∀ {s : String.Slice},
  String.Slice.Pattern.ForwardSliceSearcher.toOption✝ String.Slice.Pattern.ForwardSliceSearcher.atEnd = none
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- The function `log⁺` equals `log` outside of the interval (-1,1).  -/
Real.posLog_eq_log : ∀ {x : ℝ}, 1 ≤ |x| → x.posLog = Real.log x
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- Supremum of the radii of balls whose centers are not yet covered at step `i`.  -/
Besicovitch.TauPackage.R : {α : Type u_1} → [MetricSpace α] → {β : Type u} → [Nonempty β] → Besicovitch.TauPackage β α → Ordinal.{u} → ℝ
-- Mathlib.SetTheory.Ordinal.Veblen
/-- **Alias** of `Ordinal.lt_epsilon_zero`.

---

`ε₀` is the limit of `0`, `ω ^ 0`, `ω ^ ω ^ 0`, …  -/
Ordinal.lt_epsilon0 : ∀ {o : Ordinal.{u}}, o < Ordinal.epsilon 0 ↔ ∃ n, o < (fun a => Ordinal.omega0 ^ a)^[n] 0
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.Hom.id_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (a : E.I₀),
  (CategoryTheory.PreZeroHypercover.Hom.id E).s₀ a = id a
-- Init.Prelude
ne_false_of_eq_true : ∀ {b : Bool}, b = true → ¬b = false
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.tensorδ_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (W X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ W X Y Z)
      (CategoryTheory.SemiCartesianMonoidalCategory.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj W X)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.SemiCartesianMonoidalCategory.fst W Y)
      (CategoryTheory.SemiCartesianMonoidalCategory.fst X Z)
-- Lean.Meta.InferType
/-- `isProofQuick e` is an "approximate" predicate which returns `LBool.true` if `e` is a proof.
 -/
Lean.Meta.isProofQuick : Lean.Expr → Lean.MetaM Lean.LBool
-- Mathlib.Topology.Order.Lattice
ContinuousAt.inf' : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] [inst_2 : Min L]
  [ContinuousInf L] {f g : X → L} {x : X}, ContinuousAt f x → ContinuousAt g x → ContinuousAt (f ⊓ g) x
-- Mathlib.Topology.Category.Profinite.Nobeling.Induction
/-- The embedding `S → (I → Bool)` where `I` is the set of clopens of `S`.  -/
Profinite.Nobeling.ι : (S : Profinite) → ↑S.toTop → { C // IsClopen C } → Bool
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedComm_of_tmul_of : ∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  (i j : ι) (a : 𝒜 i) (b : ℬ j),
  (TensorProduct.gradedComm R 𝒜 ℬ) ((DirectSum.lof R ι 𝒜 i) a ⊗ₜ[R] (DirectSum.lof R ι ℬ j) b) =
    (-1) ^ (j * i) • (DirectSum.lof R ι ℬ j) b ⊗ₜ[R] (DirectSum.lof R ι 𝒜 i) a
-- Std.Http.Internal.IndexMultiMap
/-- Retrieves the first value for the given key.
 -/
Std.Internal.IndexMultiMap.get : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] → [inst_1 : Hashable α] → (map : Std.Internal.IndexMultiMap α β) → (key : α) → key ∈ map → β
-- Mathlib.LinearAlgebra.Matrix.Echelon.Basic
/-- If column indices have a linear order, then there's at most one leading position per row.  -/
Matrix.IsLeadingEntry.unique : ∀ {m : Type u_1} {n : Type u_2} {R : Type v} {A : Matrix m n R} [inst : Zero R] [inst_1 : LinearOrder n] {i : m}
  {c₁ c₂ : n}, A.IsLeadingEntry i c₁ → A.IsLeadingEntry i c₂ → c₁ = c₂
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_min_le : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M] {f g : ι → M}
  {s : Finset ι}, ∑ i ∈ s, min (f i) (g i) ≤ min (s.sum f) (s.sum g)