mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2ComputableInPolyTime.mk.sizeOf_spec : ∀ {α β αΓ βΓ : Type} {ea : α → List αΓ} {eb : β → List βΓ} {f : α → β} [inst : SizeOf α] [inst_1 : SizeOf β]
  [inst_2 : SizeOf αΓ] [inst_3 : SizeOf βΓ] (toTM2ComputableAux : Turing.TM2ComputableAux αΓ βΓ) (time : Polynomial ℕ)
  (outputsFun :
    (a : α) →
      Turing.TM2OutputsInTime toTM2ComputableAux.tm (List.map toTM2ComputableAux.inputAlphabet.invFun (ea a))
        (some (List.map toTM2ComputableAux.outputAlphabet.invFun (eb (f a)))) (Polynomial.eval (ea a).length time)),
  sizeOf { toTM2ComputableAux := toTM2ComputableAux, time := time, outputsFun := outputsFun } =
    1 + sizeOf toTM2ComputableAux + sizeOf time
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
_private.Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps.0.ContinuousMap.Homotopy.end_path : ∀ {X₁ X₂ Y : TopCat} {f : C(↑X₁, ↑Y)} {g : C(↑X₂, ↑Y)} {x₀ x₁ : ↑X₁} {x₂ x₃ : ↑X₂} {p : Path x₀ x₁} {q : Path x₂ x₃},
  (∀ (t : ↑unitInterval), f (p t) = g (q t)) → f x₁ = g x₃
-- Mathlib.Topology.Connected.TotallyDisconnected
subsingleton_of_preconnected_totallyDisconnected : ∀ {α : Type u} [inst : TopologicalSpace α] [PreconnectedSpace α] [TotallyDisconnectedSpace α], Subsingleton α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  (t₁ ∩ t₂).getKeyD k fallback = if k ∈ t₂ then t₁.getKeyD k fallback else fallback
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Extract a lean expression from an `Atom₁` term.  -/
Mathlib.Tactic.BicategoryLike.Atom₁.e : Mathlib.Tactic.BicategoryLike.Atom₁ → Lean.Expr
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
  [inst_5 : LE β] {f g : α ≃+*o β}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- The doubling constant `σₘ[A, B]` of two finsets `A` and `B` in a group is `|A * B| / |A|`.  -/
Combinatorics.Additive.«termσₘ[_,_]» : Lean.ParserDescr
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.localTrivAt_def : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (b : B), Z.localTriv (Z.indexAt b) = Z.localTrivAt b
-- Std.Http.Data.URI.Basic
Std.Http.URI.instBEqUserInfo.beq : Std.Http.URI.UserInfo → Std.Http.URI.UserInfo → Bool
-- Mathlib.Topology.Category.Profinite.Basic
instTotallyDisconnectedSpaceCarrierToTopTrueObjProfiniteCompHausProfiniteToCompHaus : ∀ {X : Profinite}, TotallyDisconnectedSpace ↑(profiniteToCompHaus.obj X).toTop
-- Init.Data.Nat.Lemmas
Nat.le_add_pred_of_pos : ∀ {b : ℕ} (a : ℕ), b ≠ 0 → a ≤ b + (a - 1)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.alter! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [inst : Std.LawfulEqOrd α] {t : Std.DTreeMap.Internal.Impl α β} {a : α}
  {f : Option (β a) → Option (β a)}, t.WF → (Std.DTreeMap.Internal.Impl.alter! a f t).WF
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.closure.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M] (s : Set M), AddSubmonoid.closure s = sInf {S | s ⊆ ↑S}
-- Init.Data.Int.Cooper
/-- When `p ≤ a * x`, we can realize `resolve_left` as a natural number.  -/
Int.Cooper.resolve_left' : (a : ℤ) → ℤ → ℤ → (p x : ℤ) → p ≤ a * x → ℕ
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.mk.injEq : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (toCoalgHom : A →ₗc[R] B) (map_one' : toCoalgHom.toFun 1 = 1)
  (map_mul' : ∀ (x y : A), toCoalgHom.toFun (x * y) = toCoalgHom.toFun x * toCoalgHom.toFun y)
  (toCoalgHom_1 : A →ₗc[R] B) (map_one'_1 : toCoalgHom_1.toFun 1 = 1)
  (map_mul'_1 : ∀ (x y : A), toCoalgHom_1.toFun (x * y) = toCoalgHom_1.toFun x * toCoalgHom_1.toFun y),
  ({ toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' } =
      { toCoalgHom := toCoalgHom_1, map_one' := map_one'_1, map_mul' := map_mul'_1 }) =
    (toCoalgHom = toCoalgHom_1)
-- Mathlib.CategoryTheory.CommSq
/-- The horizontal composition of two commutative squares as below is a commutative square.
```
  W ---f---> X ---f'--> X'
  |          |          |
  g          h          h'
  |          |          |
  v          v          v
  Y ---i---> Z ---i'--> Z'

```
 -/
CategoryTheory.CommSq.horiz_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X X' Y Z Z' : C} {f : W ⟶ X} {f' : X ⟶ X'} {g : W ⟶ Y}
  {h : X ⟶ Z} {h' : X' ⟶ Z'} {i : Y ⟶ Z} {i' : Z ⟶ Z'},
  CategoryTheory.CommSq f g h i →
    CategoryTheory.CommSq f' h h' i' →
      CategoryTheory.CommSq (CategoryTheory.CategoryStruct.comp f f') g h' (CategoryTheory.CategoryStruct.comp i i')
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.IsPullback.of_hasBinaryProduct : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [inst_3 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.IsPullback CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd 0 0
-- Mathlib.Data.Num.ZNum
ZNum.linearOrder : LinearOrder ZNum
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_eq_some_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k k' : α},
  t.get? k = some k' ↔ ∃ (h : k ∈ t), t.get k h = k'
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.eq_unit_mul_pow_irreducible : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R] {x : R},
  x ≠ 0 → ∀ {ϖ : R}, Irreducible ϖ → ∃ n u, x = ↑u * ϖ ^ n
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.coe_zero_linearMap : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M], ↑0 = 0
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.diagram_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i j : D.J),
  D.diagram.fst (i, j) = D.f i j
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.hasDetPlusMinusOne_adjoinNegOne_iff : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_3} [inst_2 : CommRing R]
  {𝒢 : Subgroup (GL n R)}, 𝒢.adjoinNegOne.HasDetPlusMinusOne ↔ 𝒢.HasDetPlusMinusOne
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `i` is an isomorphism such that `i.hom ≫ l = f`, then any cokernel of `f` is a cokernel of
`l`.  -/
CategoryTheory.Limits.IsCokernel.ofIsoComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          {Z : C} →
            (l : Z ⟶ Y) →
              (i : X ≅ Z) →
                (h : CategoryTheory.CategoryStruct.comp i.hom l = f) →
                  {s : CategoryTheory.Limits.CokernelCofork f} →
                    CategoryTheory.Limits.IsColimit s →
                      CategoryTheory.Limits.IsColimit
                        (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.Cofork.π s) ⋯)
-- Init.Data.String.Lemmas.Iterate
String.Slice.foldr_eq_foldr_toList : ∀ {α : Type u} {f : Char → α → α} {init : α} {s : String.Slice},
  String.Slice.foldr f init s = List.foldr f init s.copy.toList
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.composePath_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : Quiver.Path X Y) (g : Quiver.Path Y Z),
  CategoryTheory.composePath (f.comp g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.composePath f) (CategoryTheory.composePath g)
-- Lean.Meta.Basic
/-- Number of times `f a =?= f b` heuristic has been used per function `f`.  -/
Lean.Meta.Diagnostics.heuristicCounter : Lean.Meta.Diagnostics → Lean.PHashMap Lean.Name ℕ
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularCompactLTTop.map_of_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [BorelSpace α] [inst_3 : MeasurableSpace β] [inst_4 : TopologicalSpace β] [BorelSpace β]
  [h : μ.InnerRegularCompactLTTop] {f : α → β}, Continuous f → (MeasureTheory.Measure.map f μ).InnerRegularCompactLTTop
-- Mathlib.Data.ENat.Basic
instAddMonoidWithOneENat : AddMonoidWithOne ℕ∞
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.nhds_eq : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α}, nhds x = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal (Metric.eball x ε)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.FullyFaithful.homNatIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X_1 : Cᵒᵖ),
  (hF.homNatIso X).inv.app X_1 = (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.inv
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.getKey_eq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (hk : k ∈ m₁) (h : m₁.Equiv m₂), m₁.getKey k hk = m₂.getKey k ⋯
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.instFiniteElemFinset : ∀ (α : Type u_1) (n : ℕ) [Finite α], Finite ↑(Set.powersetCard α n)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Orientation.rotationAux_apply : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (x : V),
  (o.rotationAux θ) x = θ.cos • x + θ.sin • o.rightAngleRotation x
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.srem_umod : ∀ {w : ℕ} (x y : BitVec w),
  x.srem y =
    bif x.getLsbD (w - 1) then bif y.getLsbD (w - 1) then -(-x % -y) else -(-x % y)
    else bif y.getLsbD (w - 1) then x % -y else x % y
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mapOfLE_valuation_apply : ∀ {K : Type u} [inst : Field K] (R S : ValuationSubring K) (h : R ≤ S) (x : K),
  (R.mapOfLE S h) (R.valuation x) = S.valuation x
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- The inverse map in `lTensor.equiv_of_rightInverse` (computably, given a right inverse)  -/
lTensor.inverse_of_rightInverse : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {P : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : AddCommGroup P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      {f : M →ₗ[R] N} →
                        {g : N →ₗ[R] P} →
                          (Q : Type u_5) →
                            [inst_7 : AddCommGroup Q] →
                              [inst_8 : Module R Q] →
                                {h : P → N} →
                                  Function.Exact ⇑f ⇑g →
                                    Function.RightInverse h ⇑g →
                                      TensorProduct R Q P →ₗ[R] TensorProduct R Q N ⧸ (LinearMap.lTensor Q f).range
-- Batteries.Recycling.RBTree.Basic
/-- `O(n₁ * (log n₁ + log n₂))`. Constructs the set of all elements of `t₁` that are not in `t₂`.
 -/
RBTree.RBMap.sdiff : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → RBTree.RBMap α β cmp → RBTree.RBMap α β cmp
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instBEqDiagnosticWith.beq : {α : Type} → [BEq α] → Lean.Lsp.DiagnosticWith α → Lean.Lsp.DiagnosticWith α → Bool
-- Mathlib.CategoryTheory.Action.Basic
/-- A functor between categories induces a functor between
the categories of `G`-actions within those categories.  -/
CategoryTheory.Functor.mapAction : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {W : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} W] →
        CategoryTheory.Functor V W →
          (G : Type u_3) → [inst_2 : Monoid G] → CategoryTheory.Functor (Action V G) (Action W G)
-- Mathlib.Data.PEquiv
PEquiv.symm_apply_eq : ∀ {α : Type u} {β : Type v} (f : α ≃. β) {x : β} {y : α}, f.symm x = some y ↔ some x = f y
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_finset_product₃ : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {γ : Type u_7} (s : Finset (α × β × γ))
  (f : α × β × γ → M),
  ∏ᶠ (abc : α × β × γ) (_ : abc ∈ s), f abc = ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
_private.Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite.0.CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.instProjectiveOppositeProjectiveSeparator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C],
  CategoryTheory.Projective
    (CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator✝ C)
-- Mathlib.RingTheory.RingHomProperties
RingHom.toMorphismProperty_respectsIso_iff : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) ↔
    (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
-- Init.Data.SInt.Lemmas
Int16.toISize_lt : ∀ {a b : Int16}, a.toISize < b.toISize ↔ a < b
-- Mathlib.Algebra.Order.Module.Defs
smul_nonneg_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [PosSMulStrictMono α β] {a : α} {b : β}, 0 ≤ a • b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
-- Init.Control.Lawful.Instances
EStateM.bind.eq_1 : ∀ {ε σ α β : Type u} (x : EStateM ε σ α) (f : α → EStateM ε σ β) (s : σ),
  x.bind f s =
    match x s with
    | EStateM.Result.ok a s => f a s
    | EStateM.Result.error e s => EStateM.Result.error e s
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.join.eq_1 : ∀ {α : Type u} (S : Stream'.WSeq (Stream'.WSeq α)),
  S.join =
    ((fun o =>
          match o with
          | none => Stream'.Seq1.ret none
          | some s => (none, s)) <$>
        S).join
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.domDomRestrict_aux : ∀ {ι : Sort u_2} [inst : DecidableEq ι] (P : ι → Prop) [inst_1 : DecidablePred P] {M₁ : ι → Type u_1}
  [inst_2 : DecidableEq { a // P a }] (x : (i : { a // P a }) → M₁ ↑i) (z : (i : { a // ¬P a }) → M₁ ↑i)
  (i : { a // P a }) (c : M₁ ↑i),
  (fun j => if h : P j then Function.update x i c ⟨j, h⟩ else z ⟨j, h⟩) =
    Function.update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) c
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.productTriangle.zero₃₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  (T : J → CategoryTheory.Pretriangulated.Triangle C) [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂]
  [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃]
  [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C],
  (∀ (j : J), CategoryTheory.CategoryStruct.comp (T j).mor₃ ((CategoryTheory.shiftFunctor C 1).map (T j).mor₁) = 0) →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Pretriangulated.productTriangle T).mor₃
        ((CategoryTheory.shiftFunctor C 1).map (CategoryTheory.Pretriangulated.productTriangle T).mor₁) =
      0
-- Mathlib.Analysis.Convex.Slope
ConvexOn.secant_mono_aux3 : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  ConvexOn 𝕜 s f → ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f x) / (z - x) ≤ (f z - f y) / (z - y)
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.Producer.mk : Std.Http.Chunk → IO.Promise Bool → Std.Http.Body.Channel.Producer✝
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanLocationLink : Lean.FromJson Lean.Lsp.LeanLocationLink
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The obvious functor `WidePullbackShape J ⥤ (WidePushoutShape J)ᵒᵖ`  -/
CategoryTheory.Limits.widePullbackShapeOp : (J : Type w) →
  CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J) (CategoryTheory.Limits.WidePushoutShape J)ᵒᵖ
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Descend a morphism `k : X ⟶ Z`, coequalized by the two morphisms `left` and `right`, along `f`.
 -/
CategoryTheory.IsRegularEpi.desc : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      (f : X ⟶ Y) →
        [inst_1 : CategoryTheory.IsRegularEpi f] →
          (k : X ⟶ Z) →
            CategoryTheory.CategoryStruct.comp (CategoryTheory.IsRegularEpi.left f) k =
                CategoryTheory.CategoryStruct.comp (CategoryTheory.IsRegularEpi.right f) k →
              (Y ⟶ Z)
-- Mathlib.Analysis.Distribution.Support
Distribution.IsVanishingOn.lineDerivOp : ∀ {E : Type u_11} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E}
  {F : Type u_12} [inst_2 : AddCommGroup F] [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace F]
  [inst_5 : IsTopologicalAddGroup F] [inst_6 : ContinuousSMul ℝ F] {f : Distribution Ω F ⊤} {s : Set E},
  Distribution.IsVanishingOn (⇑f) s → ∀ (m : E), Distribution.IsVanishingOn (⇑(LineDeriv.lineDerivOp m f)) s
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the angle between two vectors is `π / 2`, the first vector is nonzero.  -/
Orientation.left_ne_zero_of_oangle_eq_pi_div_two : ∀ {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}, o.oangle x y = ↑(Real.pi / 2) → x ≠ 0
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- The forgetful map from the type alias associated to `EnrichedOrdinaryCategory Cat C` and the
type alias associated to `EnrichedCategory Cat C` is the identity on underlying types.  -/
CategoryTheory.CatEnrichedOrdinary.toBase : {C : Type u} → CategoryTheory.CatEnrichedOrdinary C → CategoryTheory.CatEnriched C
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_le_pi_div_two : ∀ (x : ℝ), Real.arcsin x ≤ Real.pi / 2
-- Mathlib.Data.ZMod.Basic
ZMod.one_eq_zero_iff : ∀ {n : ℕ}, 1 = 0 ↔ n = 1
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- The exponential sum as an `ofScalarsSum`.  -/
NormedSpace.exp_eq_ofScalarsSum : ∀ (𝕂 : Type u_1) {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] [CharZero 𝕂],
  NormedSpace.exp = FormalMultilinearSeries.ofScalarsSum fun n => (↑n.factorial)⁻¹
-- Mathlib.Order.SymmDiff
symmDiff_left_surjective : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a : α), Function.Surjective fun x => symmDiff x a
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.add : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S] {a b : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a → MvPowerSeries.HasSubst b → MvPowerSeries.HasSubst (a + b)
-- Mathlib.Analysis.Complex.Basic
Complex.dist_conj_comm : ∀ (z w : ℂ), dist ((starRingEnd ℂ) z) w = dist z ((starRingEnd ℂ) w)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_le_size_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {f : Option (β k) → Option (β k)}, t.size - 1 ≤ (t.alter k f).size
-- Mathlib.FieldTheory.Extension
/-- Given a lift `x` and an integral element `s : E` over `x.carrier` whose conjugates over
`x.carrier` are all in `K`, we can extend the lift to a lift whose carrier contains `s`.  -/
IntermediateField.Lifts.exists_lift_of_splits' : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] (x : IntermediateField.Lifts F E K) {s : E},
  IsIntegral (↥x.carrier) s →
    (Polynomial.map x.emb.toRingHom (minpoly (↥x.carrier) s)).Splits → ∃ y, x ≤ y ∧ s ∈ y.carrier
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicator_one : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) {x : α},
  x ∈ E → (thickenedIndicator δ_pos E) x = 1
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.resLE_comp_resLE_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) {Z : AlgebraicGeometry.Scheme} (g : Y ⟶ Z) {W : Z.Opens}
  (e' : U ≤ (TopologicalSpace.Opens.map g.base).obj W) {Z_1 : AlgebraicGeometry.Scheme} (h : ↑W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.resLE f U V e)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.resLE g W U e') h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.resLE (CategoryTheory.CategoryStruct.comp f g) W V ⋯) h
-- Mathlib.NumberTheory.NumberField.House
NumberField.house_add_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (α β : K),
  NumberField.house (α + β) ≤ NumberField.house α + NumberField.house β
-- Aesop.Stats.Report
_private.Aesop.Stats.Report.0.Aesop.StatsReport.scriptsCore.fmtTimes : Array Aesop.Nanos → Std.Format
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- We have partitioned the TM2 statements into "stack actions", which require going to the end
of the stack, and all other actions, which do not. This is a modified recursor which lumps the
stack actions into one.  -/
Turing.TM2to1.stmtStRec : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} →
        {motive : Turing.TM2.Stmt Γ Λ σ → Sort l} →
          ((k : K) →
              (s : Turing.TM2to1.StAct K Γ σ k) →
                (q : Turing.TM2.Stmt Γ Λ σ) → motive q → motive (Turing.TM2to1.stRun s q)) →
            ((a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive q → motive (Turing.TM2.Stmt.load a q)) →
              ((p : σ → Bool) →
                  (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive q₁ → motive q₂ → motive (Turing.TM2.Stmt.branch p q₁ q₂)) →
                ((l : σ → Λ) → motive (Turing.TM2.Stmt.goto l)) →
                  motive Turing.TM2.Stmt.halt → (n : Turing.TM2.Stmt Γ Λ σ) → motive n
-- Init.Prelude
/-- Replaces `oldRef` with `ref`, unless `ref` has no position info.
This biases us to having a valid span to report an error on.
 -/
Lean.replaceRef : Lean.Syntax → Lean.Syntax → Lean.Syntax
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- Natural inclusion `B²(G, A) →ₗ[k] Z²(G, A)`.  -/
groupCohomology.coboundariesToCocycles₂ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u_1, u, u} k G) → ↥(groupCohomology.coboundaries₂ A) →ₗ[k] ↥(groupCohomology.cocycles₂ A)
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsPreBrownianReal.mk' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ}
  {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsPreBrownianReal._auto_1},
  (∀ (I : Finset NNReal),
      ProbabilityTheory.HasLaw (fun ω => I.restrict fun x => X x ω) (ProbabilityTheory.BrownianReal.projectiveFamily I)
        P) →
    ProbabilityTheory.IsPreBrownianReal X P
-- Mathlib.GroupTheory.Congruence.Basic
/-- The third isomorphism theorem for `AddMonoid`s.  -/
AddCon.quotientQuotientEquivQuotient : {M : Type u_1} →
  [inst : AddZeroClass M] → (c d : AddCon M) → (h : c ≤ d) → (AddCon.ker (c.map d h)).Quotient ≃+ d.Quotient