mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Lemmas
/-- Simpler variant of `getElem?_filter` when `LawfulEqCmp` is available.  -/
Std.TreeMap.getElem?_filter' : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {f : α → β → Bool} {k : α}, (Std.TreeMap.filter f t)[k]? = Option.filter (f k) t[k]?
-- Mathlib.Algebra.Module.Congruence.Defs
/-- The quotient by a congruence relation preserving scalar multiplication.  -/
SMulCon.Quotient : {S : Type u_2} → (M : Type u_3) → [inst : SMul S M] → SMulCon S M → Type u_3
-- Mathlib.MeasureTheory.PiSystem
/-- A Dynkin system contains the empty set.  -/
MeasurableSpace.DynkinSystem.has_empty : ∀ {α : Type u_4} (self : MeasurableSpace.DynkinSystem α), self.Has ∅
-- Std.Http.Server.Handler
Std.Http.Server.instHandlerStatelessHandler : Std.Http.Server.Handler Std.Http.Server.StatelessHandler
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The left object of a costructured arrow.  -/
CategoryTheory.CostructuredArrow.left : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor C D} → {T : D} → CategoryTheory.CostructuredArrow S T → C
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.evalEquiv_symm_apply : ∀ (S : CategoryTheory.Functor Type uᵒᵖ (Type u))
  (hs : CategoryTheory.Presheaf.IsSheaf CategoryTheory.typesGrothendieckTopology S) (α : Type u)
  (f : α ⟶ S.obj (Opposite.op PUnit.{u + 1})),
  (CategoryTheory.evalEquiv S hs α).symm f = CategoryTheory.typesGlue S ⋯ α ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.fromBlocks₁₁ : ∀ {m : Type u_1} {n : Type u_2} {R' : Type u_4} [inst : CommRing R'] [inst_1 : PartialOrder R'] [inst_2 : StarRing R']
  [inst_3 : Fintype m] [StarOrderedRing R'] [Finite n] [inst_6 : DecidableEq m] {A : Matrix m m R'} (B : Matrix m n R')
  (D : Matrix n n R'),
  A.PosDef →
    ∀ [Invertible A], (Matrix.fromBlocks A B B.conjTranspose D).PosSemidef ↔ (D - B.conjTranspose * A⁻¹ * B).PosSemidef
-- Std.Http.Data.Version
/-- Converts `String` to the corresponding `Version`, panics if invalid.
 -/
Std.Http.Version.ofString! : String → Std.Http.Version
-- Mathlib.Analysis.Normed.Lp.ProdLp
IsometryEquiv.withLpProdComm_apply : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β] (x : WithLp p (α × β)),
  (IsometryEquiv.withLpProdComm p α β) x = WithLp.toLp p (x.snd, x.fst)
-- Mathlib.Algebra.Order.Floor.Semifield
Mathlib.Meta.NormNum.IsInt.natFloor : ∀ {R : Type u_3} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R] (r : R)
  (m : ℕ), Mathlib.Meta.NormNum.IsInt r (Int.negOfNat m) → Mathlib.Meta.NormNum.IsNat ⌊r⌋₊ 0
-- Std.Time.Zoned.Database.PosixTz
_private.Std.Time.Zoned.Database.PosixTz.0.Std.Time.TimeZone.posixParseJulianSpec : Std.Internal.Parsec.String.Parser Std.Time.TimeZone.TransitionSpec
-- Mathlib.Data.Set.Lattice
Set.iInter_plift_down : ∀ {α : Type u_1} {ι : Sort u_5} (f : ι → Set α), ⋂ i, f i.down = ⋂ i, f i
-- Mathlib.Data.PFun
/-- Evaluate a partial function to return an `Option`  -/
PFun.evalOpt : {α : Type u_1} → {β : Type u_2} → (f : α →. β) → [D : DecidablePred fun x => x ∈ f.Dom] → α → Option β
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableAt.const_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a : E → 𝔸},
  DifferentiableAt 𝕜 a x → ∀ (b : 𝔸), DifferentiableAt 𝕜 (fun y => b * a y) x
-- Init.Data.List.ToArray
List.sum_toArray : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] (l : List α), l.toArray.sum = l.sum
-- Init.Data.Option.Basic
/-- Applies a function in some applicative functor to an optional value, returning `none` with no
effects if the value is missing.

This is an alias for `Option.mapM`, which already works for applicative functors.
 -/
Option.mapA : {m : Type u_1 → Type u_2} → {α : Type u_3} → {β : Type u_1} → [Applicative m] → (α → m β) → Option α → m (Option β)
-- Mathlib.Data.Set.Basic
Set.univ_union : ∀ {α : Type u} (s : Set α), Set.univ ∪ s = Set.univ
-- Lean.Meta.Tactic.Simp.Main
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.unfold?.unfoldDeclToUnfold? : Lean.Expr → Lean.Name → Lean.Meta.SimpM (Option Lean.Expr)
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α]
  {l : List α} {k : α}, k ∈ m → (m.insertMany l).get! k = m.get! k
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.instOrderTop : {α : Type u_2} → {β : Type u_3} → [inst : InfSet α] → {x : CompleteLattice β} → OrderTop (sInfHom α β)
-- Mathlib.Combinatorics.Enumerative.Schroder
Nat.smallSchroder_succ_eq_largeSchroder_div_two : ∀ {n : ℕ}, n ≠ 0 → (n + 1).smallSchroder = n.largeSchroder / 2
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
_private.Mathlib.NumberTheory.EllipticDivisibilitySequence.0.complEDS'.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_2 ()
-- Mathlib.LinearAlgebra.Dimension.Finite
Submodule.one_le_finrank_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] [StrongRankCondition R] {S : Submodule R M} [Module.Finite R ↥S],
  1 ≤ Module.finrank R ↥S ↔ S ≠ ⊥
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.Adj.not_isIsolated_left : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Adj u v → ¬G.IsIsolated u
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_ric_eq_fallback : ∀ {n i fallback : ℕ}, n < i → (*...=n).toArray.getD i fallback = fallback
-- Mathlib.Algebra.CubicDiscriminant
Cubic.b_eq_three_roots : ∀ {F : Type u_3} {K : Type u_4} {P : Cubic F} [inst : Field F] [inst_1 : Field K] {φ : F →+* K} {x y z : K},
  P.a ≠ 0 → (Cubic.map φ P).roots = {x, y, z} → φ P.b = φ P.a * -(x + y + z)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.single_one_one : ∀ {k : Type u_1} {G : Type u_2} [inst : One G] [inst_1 : AddMonoidWithOne k], SkewMonoidAlgebra.single 1 1 = 1
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_obj_left_right_as : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  (Y : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag T) X),
  ((CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor X).obj Y).left.right.as = PUnit.unit
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
/-- If `G` preserves colimits, we have an isomorphism from the image of the colimit of a functor `F`
to the colimit of the functor `F ⋙ G`.
 -/
CategoryTheory.preservesColimitIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {J : Type w} →
            [inst_2 : CategoryTheory.Category.{w', w} J] →
              (F : CategoryTheory.Functor J C) →
                [inst_3 : CategoryTheory.Limits.PreservesColimit F G] →
                  [inst_4 : CategoryTheory.Limits.HasColimit F] →
                    G.obj (CategoryTheory.Limits.colimit F) ≅ CategoryTheory.Limits.colimit (F.comp G)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Descend a collection of morphisms to a morphism from the pushout.  -/
CategoryTheory.Limits.WidePushout.desc : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {B : C} →
        {objs : J → C} →
          {arrows : (j : J) → B ⟶ objs j} →
            [inst_1 : CategoryTheory.Limits.HasWidePushout B objs arrows] →
              {X : C} →
                (f : B ⟶ X) →
                  (fs : (j : J) → objs j ⟶ X) →
                    (∀ (j : J), CategoryTheory.CategoryStruct.comp (arrows j) (fs j) = f) →
                      (CategoryTheory.Limits.widePushout B objs arrows ⟶ X)
-- Std.Do.WP.SimpLemmas
Std.Do.WP.throw_Except : ∀ {ε α : Type u_1} {e : ε} {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε Std.Do.PostShape.pure)},
  (Std.Do.wp (MonadExceptOf.throw e)).apply Q = Q.2.1 e
-- Mathlib.Analysis.Meromorphic.Basic
/-- In a complete space, a function which is meromorphic at a point is analytic at all nearby
points. The completeness assumption can be dispensed with if one assumes that `f` is meromorphic
on a set around `x`, see `MeromorphicOn.eventually_analyticAt`.  -/
MeromorphicAt.eventually_analyticAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} [CompleteSpace E] {f : 𝕜 → E},
  MeromorphicAt f x → ∀ᶠ (y : 𝕜) in nhdsWithin x {x}ᶜ, AnalyticAt 𝕜 f y
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_apply_smul_mem_of_le_comap : ∀ {R : Type u} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {q : Submodule R M} {m : M},
  m ∈ q → ∀ (p : Polynomial R) (f : Module.End R M), q ≤ Submodule.comap f q → ((Polynomial.aeval f) p) m ∈ q
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.FirstByte.oneMore : ByteArray.utf8DecodeChar?.FirstByte
-- Lean.Language.Basic
Lean.Language.instTypeNameSnapshotLeaf : TypeName Lean.Language.SnapshotLeaf
-- Mathlib.CategoryTheory.Adjunction.Additive
CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.Additive] (X : Cᵒᵖ) (Y : D)
  (a : ULift.{max v₁ v₂, v₁} (Opposite.unop X ⟶ G.obj Y)),
  (CategoryTheory.ConcreteCategory.hom ((adj.compPreadditiveYonedaIso.hom.app Y).app X)) a =
    { down := (adj.homEquiv (Opposite.unop X) Y).symm (AddEquiv.ulift a) }
-- Init.Data.Int.Lemmas
Int.sub_eq_zero_of_eq : ∀ {a b : ℤ}, a = b → a - b = 0
-- Mathlib.Algebra.Ring.Defs
LeftDistribClass.mk : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R], (∀ (a b c : R), a * (b + c) = a * b + a * c) → LeftDistribClass R
-- Mathlib.RingTheory.Bialgebra.Equiv
/-- Bialgebra equivalences are transitive.  -/
BialgEquiv.trans : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      {C : Type u₁} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Semiring C] →
                [inst_4 : Algebra R A] →
                  [inst_5 : Algebra R B] →
                    [inst_6 : Algebra R C] →
                      [inst_7 : CoalgebraStruct R A] →
                        [inst_8 : CoalgebraStruct R B] →
                          [inst_9 : CoalgebraStruct R C] → (A ≃ₐc[R] B) → (B ≃ₐc[R] C) → A ≃ₐc[R] C
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.log_rnDeriv_tilted_left_self : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.SigmaFinite μ],
  MeasureTheory.Integrable (fun x => Real.exp (f x)) μ →
    (fun x => Real.log ((μ.tilted f).rnDeriv μ x).toReal) =ᵐ[μ] fun x => f x - Real.log (∫ (x : α), Real.exp (f x) ∂μ)
-- Mathlib.Data.Nat.Cast.Basic
Pi.natCast_apply : ∀ {α : Type u_1} {π : α → Type u_3} [inst : (a : α) → NatCast (π a)] (n : ℕ) (a : α), ↑n a = ↑n
-- Init.Data.Array.Zip
Array.zip_eq_zip_take_min : ∀ {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β},
  as.zip bs = (as.take (min as.size bs.size)).zip (bs.take (min as.size bs.size))
-- Mathlib.Order.Basic
le_of_forall_le : ∀ {α : Type u_2} [inst : Preorder α] {a b : α}, (∀ c ≤ a, c ≤ b) → a ≤ b
-- Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
/-- Let `γ` and `γ'` be integral curves defined on `Ioo a b` and `Ioo a' b'`, respectively. Then,
`piecewise (Ioo a b) γ γ'` is equal to `γ` and `γ'` in their respective domains.
`Set.piecewise_eqOn` shows the equality for `γ` by definition, while this lemma shows the equality
for `γ'` by the uniqueness of integral curves.  -/
eqOn_piecewise_of_isMIntegralCurveOn_Ioo : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] [T2Space M] {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ : ℝ}
  [BoundarylessManifold I M],
  (ContMDiff I I.tangent 1 fun x => ⟨x, v x⟩) →
    ∀ {a b a' b' : ℝ},
      IsMIntegralCurveOn γ v (Set.Ioo a b) →
        IsMIntegralCurveOn γ' v (Set.Ioo a' b') →
          t₀ ∈ Set.Ioo a b ∩ Set.Ioo a' b' → γ t₀ = γ' t₀ → Set.EqOn ((Set.Ioo a b).piecewise γ γ') γ' (Set.Ioo a' b')
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.radius_nonneg_of_mem : ∀ {P : Type u_2} [inst : MetricSpace P] {s : EuclideanGeometry.Sphere P} {p : P}, p ∈ s → 0 ≤ s.radius
-- Mathlib.Algebra.Group.Prod
AddEquiv.uniqueProd_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : Unique N] (a : N × M),
  AddEquiv.uniqueProd a = a.2
-- Init.Grind.AC
Lean.Grind.AC.simp_middle_cert : Lean.Grind.AC.Seq →
  Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Init.Data.BitVec.Bitblast
BitVec.sshiftRightRec.eq_def : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (n : ℕ),
  x.sshiftRightRec y n =
    have shiftAmt := y &&& BitVec.twoPow w₂ n;
    match n with
    | 0 => x.sshiftRight' shiftAmt
    | n.succ => (x.sshiftRightRec y n).sshiftRight' shiftAmt
-- Mathlib.Algebra.Lie.Abelian
trivial_lie_zero : ∀ (L : Type v) (M : Type w) [inst : Bracket L M] [inst_1 : Zero M] [LieModule.IsTrivial L M] (x : L) (m : M), ⁅x, m⁆ = 0
-- Mathlib.Topology.Algebra.LinearTopology
/-- If a ring `R` is linearly ordered as a left *and* right module over itself,
then it has a basis of neighborhoods of zero made of *two-sided* ideals.

This is usually called a *linearly topologized ring*, but we do not add a specific spelling:
you should use `[IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R]` instead.  -/
IsLinearTopology.hasBasis_twoSidedIdeal : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R],
  (nhds 0).HasBasis (fun I => ↑I ∈ nhds 0) fun I => ↑I
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_zero_right_iff : ∀ {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [inst : SeminormedAddCommGroup F'] [inst_1 : NormedAddCommGroup E'']
  {c : ℝ} {f'' : α → E''} {l : Filter α}, (Asymptotics.IsBigOWith c l f'' fun _x => 0) ↔ f'' =ᶠ[l] 0
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.instIsAffineHomιBasicOpen : ∀ {X : AlgebraicGeometry.Scheme} (r : ↑(X.presheaf.obj (Opposite.op ⊤))),
  AlgebraicGeometry.IsAffineHom (X.basicOpen r).ι
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable
value `∞` instead, use `Metric.hausdorffEDist`, which takes values in `ℝ≥0∞`).  -/
Metric.hausdorffDist_empty : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, Metric.hausdorffDist s ∅ = 0
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafLeftAdjointSheafToPresheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasSheafify J A],
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.sheafToPresheaf J A).leftAdjoint
-- Std.Sat.CNF.RelabelFin
Std.Sat.CNF.unsat_relabelFin : ∀ {f : Std.Sat.CNF ℕ}, f.relabelFin.Unsat ↔ f.Unsat
-- Mathlib.Algebra.Star.UnitaryStarAlgAut
Unitary.toAlgEquiv_conjStarAlgAut : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] {S : Type u_3} [inst_2 : CommSemiring S]
  [inst_3 : Algebra S R] (u : ↥(unitary R)),
  ((Unitary.conjStarAlgAut S R) u).toAlgEquiv = MulSemiringAction.toAlgEquiv S R (ConjAct.toConjAct (Unitary.toUnits u))
-- Init.Control.Lawful.Instances
ReaderT.run_read : ∀ {m : Type u_1 → Type u_2} {ρ : Type u_1} [inst : Monad m] (ctx : ρ), ReaderT.read.run ctx = pure ctx
-- Mathlib.Algebra.CharP.Algebra
/-- If `R →+* A` is injective, then `R` is of exponential characteristic `p` if and only if `A` is
also of exponential characteristic `p`. Similar to `RingHom.charZero_iff`.  -/
RingHom.expChar_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring A] (f : R →+* A),
  Function.Injective ⇑f → ∀ (p : ℕ), ExpChar R p ↔ ExpChar A p
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctorIso_inv_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'}
  {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) p)
  {β : ι' → ι} {p'' : (j : ι') → X' j ⟶ X (β j)}
  (w' : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p'' j) (f (β j)) = CategoryTheory.CategoryStruct.comp (f' j) p)
  (X_1 : F.DescentData f) (i : ι'),
  ((CategoryTheory.Pseudofunctor.DescentData.pullFunctorIso F w w').inv.app X_1).hom i =
    X_1.hom (CategoryTheory.CategoryStruct.comp (p' i) (f (α i))) (p'' i) (p' i) ⋯ ⋯
-- Aesop.Util.Basic
Aesop.aesop.smallErrorMessages : Lean.Option Bool
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.comp_assoc_of_second_deg_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y Z T : C} {a₁ a₃ a₁₃ : ℕ} (α : CategoryTheory.Abelian.Ext X Y a₁)
  (β : CategoryTheory.Abelian.Ext Y Z 0) (γ : CategoryTheory.Abelian.Ext Z T a₃) (h₁₃ : a₁ + a₃ = a₁₃),
  (α.comp β ⋯).comp γ h₁₃ = α.comp (β.comp γ ⋯) h₁₃
-- Mathlib.Data.List.Cycle
List.prev_head_eq_getLast : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (hl : l ≠ []), l.prev (l.head hl) ⋯ = l.getLast hl
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.IsStrictCut.toIsCut : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} [self : RBTree.RBNode.IsStrictCut cmp cut],
  RBTree.RBNode.IsCut cmp cut
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
/-- **Monotone convergence theorem** for a supremum over a directed family and indexed by a
countable type.  -/
MeasureTheory.lintegral_iSup_directed : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable β]
  {f : β → α → ENNReal},
  (∀ (b : β), AEMeasurable (f b) μ) →
    Directed (fun x1 x2 => x1 ≤ x2) f → ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.restrictPreimage_source : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty),
  (e.restrictPreimage hs).source = Subtype.val ⁻¹' e.toPretrivialization.source
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.right.sizeOf_spec : ∀ {J : CategoryTheory.Limits.MultispanShape} (a : J.R),
  sizeOf (CategoryTheory.Limits.WalkingMultispan.right a) = 1 + sizeOf a
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.ZNum.zNeg.match_1.splitter : (motive : ZNum → Sort u_1) →
  (x : ZNum) →
    (Unit → motive ZNum.zero) → ((a : PosNum) → motive (ZNum.pos a)) → ((a : PosNum) → motive (ZNum.neg a)) → motive x
-- Mathlib.Order.Category.HeytAlg
HeytAlg.hom_ext_iff : ∀ {X Y : HeytAlg} {f g : X ⟶ Y}, f = g ↔ HeytAlg.Hom.hom f = HeytAlg.Hom.hom g
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- A splitting of an additive group extension as a (set-theoretic) section.  -/
AddGroupExtension.Splitting.toSection : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] →
        [inst_1 : AddGroup E] → [inst_2 : AddGroup G] → {S : AddGroupExtension N E G} → S.Splitting → S.Section
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.dec : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    ℕ →
      Bool →
        Bool →
          Option ℕ →
            Lean.Compiler.LCNF.Code pu →
              autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_17 →
                Lean.Compiler.LCNF.Code pu
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_congr_fun_ae : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} {s : Set α},
  MeasurableSet s → (∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.Hom.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {d e : CategoryTheory.Factorisation f}
  (h h_1 : d.mid ⟶ e.mid) (e_h : h = h_1) (ι_h : CategoryTheory.CategoryStruct.comp d.ι h = e.ι)
  (h_π : CategoryTheory.CategoryStruct.comp h e.π = d.π),
  { h := h, ι_h := ι_h, h_π := h_π } = { h := h_1, ι_h := ⋯, h_π := ⋯ }
-- Mathlib.Algebra.Order.GroupWithZero.Basic
inv_mul_lt_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀},
  0 < a → (a⁻¹ * b < 1 ↔ b < a)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- An alternate form of the congruence relation on `M × S`, `M` a `CommMonoid` and `S` a
submonoid of `M`, whose quotient is the localization of `M` at `S`.  -/
Localization.r' : {M : Type u_1} → [inst : CommMonoid M] → (S : Submonoid M) → Con (M × ↥S)
-- Std.Http.Internal.IndexMultiMap
/-- Retrieves the first value for the given key, or `none` if the key is absent.
 -/
Std.Internal.IndexMultiMap.get? : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.Internal.IndexMultiMap α β → α → Option β
-- Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
/-- The vector measure with density `f` with respect to a vector measure `μ`, associating to a
measurable set the mass `∫ᵛ x in s, f x ∂[B; μ]`.
If `f` is not integrable, we use the junk value `0`.  -/
MeasureTheory.VectorMeasure.withDensity : {X : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {G : Type u_4} →
        {mX : MeasurableSpace X} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : NormedSpace ℝ E] →
              [inst_2 : NormedAddCommGroup F] →
                [inst_3 : NormedSpace ℝ F] →
                  [inst_4 : NormedAddCommGroup G] →
                    [inst_5 : NormedSpace ℝ G] →
                      MeasureTheory.VectorMeasure X F → (X → E) → (E →L[ℝ] F →L[ℝ] G) → MeasureTheory.VectorMeasure X G
-- Mathlib.Data.Finsupp.Defs
Finsupp.onFinset_apply : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {s : Finset α} {f : α → M} {hf : ∀ (a : α), f a ≠ 0 → a ∈ s} {a : α},
  (Finsupp.onFinset s f hf) a = f a
-- Lean.Elab.PreDefinition.TerminationMeasure
_private.Lean.Elab.PreDefinition.TerminationMeasure.0.Array.map_unattach.match_1.splitter : {α : Type u_1} →
  {P : α → Prop} → (motive : Subtype P → Sort u_2) → (x : Subtype P) → ((x : α) → (h : P x) → motive ⟨x, h⟩) → motive x
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
/-- `subst_hom_lift p f φ` tries to substitute `f` with `p(φ)` by using `p.IsHomLift f φ`  -/
CategoryTheory.tacticSubst_hom_lift___ : Lean.ParserDescr
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.of_isZero : ∀ (ctx : Nat.Internal.Linear.Context) {p : Nat.Internal.Linear.Poly},
  p.isZero = true → Nat.Internal.Linear.Poly.denote ctx p = 0