mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Sat.CNF.Dimacs
_private.Std.Sat.CNF.Dimacs.0.Std.Sat.CNF.DimacsState.mk.inj : ∀ {numClauses maxLit numClauses_1 maxLit_1 : ℕ},
  { numClauses := numClauses, maxLit := maxLit } = { numClauses := numClauses_1, maxLit := maxLit_1 } →
    numClauses = numClauses_1 ∧ maxLit = maxLit_1
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.sectionsMk_val_op_bot : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  (d : F.WellOrderInductionData) [inst_2 : OrderBot J] [inst_3 : WellFoundedLT J] (val₀ : F.obj (Opposite.op ⊥)),
  ↑(d.sectionsMk val₀) (Opposite.op ⊥) = val₀
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.ofContinuousMulEquiv.eq_1 : ∀ {G : ProfiniteGrp.{u}} {H : Type v} [inst : TopologicalSpace H] [inst_1 : Group H] [inst_2 : IsTopologicalGroup H]
  (e : ↑G.toProfinite.toTop ≃ₜ* H), ProfiniteGrp.ofContinuousMulEquiv e = ProfiniteGrp.of H
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ D` creates colimits, then `F.rightOp : C ⥤ Dᵒᵖ` creates limits.  -/
CategoryTheory.Limits.createsLimitsRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ D) → [CategoryTheory.CreatesColimits F] → CategoryTheory.CreatesLimits F.rightOp
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_dvd_index_of_normal : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G) [H.Normal], H.relIndex K ∣ H.index
-- Mathlib.Data.EReal.Operations
EReal.top_add_top : ⊤ + ⊤ = ⊤
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.symm_symm_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) (a : A), e.symm.symm a = e a
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.fun.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (decl : Lean.Compiler.LCNF.FunDecl pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.CodeDecl._auto_1),
  sizeOf (Lean.Compiler.LCNF.CodeDecl.fun decl h) = 1 + sizeOf decl + sizeOf h
-- Mathlib.CategoryTheory.Sites.CoverPreserving
CategoryTheory.CompatiblePreserving.apply_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D},
  CategoryTheory.CompatiblePreserving K G →
    ∀ (ℱ : CategoryTheory.Sheaf K (Type w)) {Z : C} {T : CategoryTheory.Presieve Z}
      {x : CategoryTheory.Presieve.FamilyOfElements (G.op.comp ℱ.obj) T},
      x.Compatible →
        ∀ {Y : C} {f : Y ⟶ Z} (hf : T f),
          CategoryTheory.Presieve.FamilyOfElements.functorPushforward G x (G.map f) ⋯ = x f hf
-- Mathlib.Combinatorics.Configuration
Configuration.ofField.crossProduct_eq_zero_of_dotProduct_eq_zero : ∀ {K : Type u_3} [inst : Field K] {a b c d : Fin 3 → K},
  a ⬝ᵥ c = 0 → b ⬝ᵥ c = 0 → a ⬝ᵥ d = 0 → b ⬝ᵥ d = 0 → (crossProduct a) b = 0 ∨ (crossProduct c) d = 0
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_rightUnitor_inv_snd : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] {a b : B × C}
  (f : a ⟶ b), (CategoryTheory.Bicategory.rightUnitor f).inv.2 = (CategoryTheory.Bicategory.rightUnitor f.2).inv
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.Corec.f.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (a : α) (h_1 : (a : α) → motive (Sum.inl a))
  (h_2 : (val : β) → motive (Sum.inr val)),
  (match Sum.inl a with
    | Sum.inl a => h_1 a
    | Sum.inr val => h_2 val) =
    h_1 a
-- Mathlib.Data.ENNReal.Basic
ENNReal.iInf_coe_lt_top : ∀ {ι : Sort u_2} {f : ι → NNReal}, ⨅ i, ↑(f i) < ⊤ ↔ Nonempty ι
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.lit.inj : ∀ {a a_1 : Lean.Literal}, Lean.Meta.DiscrTree.Key.lit a = Lean.Meta.DiscrTree.Key.lit a_1 → a = a_1
-- Mathlib.Data.NNReal.Defs
NNReal.mk_coe : ∀ (a : NNReal) (ha : 0 ≤ ↑a), NNReal.mk (↑a) ha = a
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.link.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (r' : Std.DTreeMap.Internal.Impl α β) (szr : ℕ) (k'' : α) (v'' : β k'')
  (l'' r'' : Std.DTreeMap.Internal.Impl α β)
  (motive :
    Std.DTreeMap.Internal.Impl.Tree α β (r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size) →
      Sort u_3)
  (ℓ : Std.DTreeMap.Internal.Impl α β) (hℓ₁ : ℓ.Balanced)
  (hℓ₂ : ℓ.size = r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size)
  (h_1 :
    (ℓ : Std.DTreeMap.Internal.Impl α β) →
      (hℓ₁ : ℓ.Balanced) →
        (hℓ₂ : ℓ.size = r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size) →
          motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ }),
  (match { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } with
    | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } => h_1 ℓ hℓ₁ hℓ₂) =
    h_1 ℓ hℓ₁ hℓ₂
-- Mathlib.Analysis.Complex.Basic
Complex.nndist_conj_comm : ∀ (z w : ℂ), nndist ((starRingEnd ℂ) z) w = nndist z ((starRingEnd ℂ) w)
-- Mathlib.Tactic.Linter.DocString
/-- Determines if a given Verso parse error should be silenced in the Verso syntax linter.
This happens when it is valid Markdown syntax that we will migrate all at once.
 -/
_private.Mathlib.Tactic.Linter.DocString.0.Mathlib.Linter.isSilencedVersoWarning : Lean.Parser.Error → Bool
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.instCharZero : ∀ (σ : Type u) (R : Type v) [inst : CommSemiring R] [CharZero R], CharZero (MvPolynomial σ R)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.Parallel.trans : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s₁ s₂ s₃ : AffineSubspace k P}, s₁.Parallel s₂ → s₂.Parallel s₃ → s₁.Parallel s₃
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.ι_D₃ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄)
  (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h)
      (HomologicalComplex.mapBifunctor₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') =
    HomologicalComplex.mapBifunctor₁₂.d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.SkeletalFunctor.instFullNonemptyFinLinOrdSkeletalFunctor : SimplexCategory.skeletalFunctor.Full
-- Mathlib.Data.Finmap
/-- Lift a permutation-respecting function on `AList` to `Finmap`.  -/
Finmap.liftOn : {α : Type u} →
  {β : α → Type v} →
    {γ : Type u_1} → Finmap β → (f : AList β → γ) → (∀ (a b : AList β), a.entries.Perm b.entries → f a = f b) → γ
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.IsArtinianScheme.toIsLocallyArtinian : ∀ {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsArtinianScheme X], AlgebraicGeometry.IsLocallyArtinian X
-- Mathlib.AlgebraicGeometry.Morphisms.Descent
AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact : ∀ (P P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [P'.IsStableUnderBaseChange]
  [P'.IsStableUnderComposition] [P.IsStableUnderBaseChange],
  @AlgebraicGeometry.IsLocalIso ⊓ @AlgebraicGeometry.Surjective ≤ P' →
    ∀ [AlgebraicGeometry.IsZariskiLocalAtTarget P],
      (∀ {R S : CommRingCat} {Y : AlgebraicGeometry.Scheme} (φ : R ⟶ S) (g : Y ⟶ AlgebraicGeometry.Spec R),
          P' (AlgebraicGeometry.Spec.map φ) →
            P (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map φ) g) → P g) →
        P.DescendsAlong (P' ⊓ @AlgebraicGeometry.QuasiCompact)
-- Mathlib.Data.Vector.Defs
/-- The tail of a vector, with an empty vector having empty tail.  -/
List.Vector.tail : {α : Type u_1} → {n : ℕ} → List.Vector α n → List.Vector α (n - 1)
-- Mathlib.Order.Sublattice
Sublattice.pi_top : ∀ {κ : Type u_5} {π : κ → Type u_6} [inst : (i : κ) → Lattice (π i)] (s : Set κ), (Sublattice.pi s fun x => ⊤) = ⊤
-- Lean.Meta.Sym.Simp.SimpM
/-- Returns `true` if this result depends on the local context (e.g., hypotheses).  -/
Lean.Meta.Sym.Simp.Result.isContextDependent : Lean.Meta.Sym.Simp.Result → Bool
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeContext.mk.sizeOf_spec : ∀ (elabs : Array Lean.Elab.Command.InductiveElabStep2) (mctx : Lean.MetavarContext) (levelParams : List Lean.Name)
  (params : Array Lean.Expr) (lctx : Lean.LocalContext) (localInsts : Lean.LocalInstances)
  (replaceIndFVars : Lean.Expr → Lean.MetaM Lean.Expr),
  sizeOf
      { elabs := elabs, mctx := mctx, levelParams := levelParams, params := params, lctx := lctx,
        localInsts := localInsts, replaceIndFVars := replaceIndFVars } =
    1 + sizeOf elabs + sizeOf mctx + sizeOf levelParams + sizeOf params + sizeOf lctx + sizeOf localInsts
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.splitMax'.match_1.eq_1 : ∀ {α : Type u_1} (motive : Ordnode α × α → Sort u_2) (r' : Ordnode α) (xm : α)
  (h_1 : (r' : Ordnode α) → (xm : α) → motive (r', xm)),
  (match (r', xm) with
    | (r', xm) => h_1 r' xm) =
    h_1 r' xm
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.inv_whiskerLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C}
  (f : Y ⟶ Z) [inst_2 : CategoryTheory.IsIso f],
  CategoryTheory.inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.inv f)
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- The right unitor isomorphism for graded objects.  -/
CategoryTheory.GradedObject.Monoidal.rightUnitor : {I : Type u} →
  [inst : AddMonoid I] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : DecidableEq I] →
            [inst_4 : CategoryTheory.Limits.HasInitial C] →
              [inst_5 :
                  ∀ (X₁ : C),
                    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                      ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] →
                (X : CategoryTheory.GradedObject I C) →
                  CategoryTheory.GradedObject.Monoidal.tensorObj X CategoryTheory.GradedObject.Monoidal.tensorUnit ≅ X
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- The completed Riemann zeta function with its poles removed, `Λ(s) + 1 / s - 1 / (s - 1)`.  -/
completedRiemannZeta₀ : ℂ → ℂ
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Summable.tsum_union_disjoint : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} [T2Space α]
  [ContinuousAdd α] {s t : Set β},
  Disjoint s t →
    Summable (f ∘ Subtype.val) →
      Summable (f ∘ Subtype.val) → ∑' (x : ↑(s ∪ t)), f ↑x = ∑' (x : ↑s), f ↑x + ∑' (x : ↑t), f ↑x
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.MethodSpecTheorem : Type
-- Mathlib.Order.BourbakiWitt
ChainCompletePartialOrder.mk : {α : Type u_4} →
  [toPartialOrder : PartialOrder α] →
    (cSup : NonemptyChain α → α) →
      (∀ (c : NonemptyChain α), ∀ x ∈ c.carrier, x ≤ cSup c) →
        (∀ (c : NonemptyChain α) (x : α), (∀ y ∈ c.carrier, y ≤ x) → cSup c ≤ x) → ChainCompletePartialOrder α
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.le_coeff : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsLinearOrder α] [Lean.Grind.OrderedAdd α] (ctx : Lean.Grind.Linarith.Context α)
  (p₁ p₂ : Lean.Grind.Linarith.Poly) (k : ℕ),
  Lean.Grind.Linarith.coeff_cert p₁ p₂ k = true →
    Lean.Grind.Linarith.Poly.denote' ctx p₁ ≤ 0 → Lean.Grind.Linarith.Poly.denote' ctx p₂ ≤ 0
-- Mathlib.Topology.SmallInductiveDimension
smallInductiveDimension_eq_bot : ∀ {X : Type u_1} [inst : TopologicalSpace X], smallInductiveDimension X = ⊥ ↔ IsEmpty X
-- Init.Data.Array.Basic
/-- Returns the array of elements in `as` for which `p` returns `true`.

Only elements from `start` (inclusive) to `stop` (exclusive) are considered. Elements outside that
range are discarded. By default, the entire array is considered.

Examples:
* `#[1, 2, 5, 2, 7, 7].filter (· > 2) = #[5, 7, 7]`
* `#[1, 2, 5, 2, 7, 7].filter (fun _ => false) = #[]`
* `#[1, 2, 5, 2, 7, 7].filter (fun _ => true) = #[1, 2, 5, 2, 7, 7]`
* `#[1, 2, 5, 2, 7, 7].filter (· > 2) (start := 3) = #[7, 7]`
* `#[1, 2, 5, 2, 7, 7].filter (fun _ => true) (start := 3) = #[2, 7, 7]`
* `#[1, 2, 5, 2, 7, 7].filter (fun _ => true) (stop := 3) = #[1, 2, 5]`
 -/
Array.filter : {α : Type u} → (α → Bool) → (as : Array α) → optParam ℕ 0 → optParam ℕ as.size → Array α
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.preimage_smul_inv₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
  a ≠ 0 → ∀ (t : Set β), (fun x => a⁻¹ • x) ⁻¹' t = a • t
-- Mathlib.Tactic.Order.ToInt
/-- Given an array `atoms : Array α`, create an expression representing a function
`f : Fin atoms.size → α` such that `f n` is defeq to `atoms[n]` for `n : Fin atoms.size`.  -/
Mathlib.Tactic.Order.ToInt.mkFinFun : {u : Lean.Level} →
  {α :
      have u := u;
      Q(Type u)} →
    Array Q(«$α») → Lean.MetaM Lean.Expr
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
SimplexCategoryGenRel.isSplitMono_toSimplexCategory_map_of_P_δ : ∀ {x y : SimplexCategoryGenRel} {m : x ⟶ y},
  SimplexCategoryGenRel.P_δ m → CategoryTheory.IsSplitMono (SimplexCategoryGenRel.toSimplexCategory.map m)
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsupp_single : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : Semiring S] [inst_6 : Algebra R S] [inst_7 : Module S M] [inst_8 : IsScalarTower R S M] (i : ι) (m : M)
  (k : κ) (n : N), (finsuppTensorFinsupp R S M N ι κ) ((fun₀ | i => m) ⊗ₜ[R] fun₀ | k => n) = fun₀ | (i, k) => m ⊗ₜ[R] n
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.insert.eq_def : ∀ (k : ℕ) (v : Nat.Internal.Linear.Var) (p : Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.insert k v p =
    match p with
    | [] => [(k, v)]
    | (k', v') :: p =>
      bif Nat.blt v v' then (k, v) :: (k', v') :: p
      else bif Nat.beq v v' then (k + k', v') :: p else (k', v') :: Nat.Internal.Linear.Poly.insert k v p
-- Std.Do.PredTrans
/-- Sequences two predicate transformers by composing them.
 -/
Std.Do.PredTrans.bind : {ps : Std.Do.PostShape} → {α β : Type u} → Std.Do.PredTrans ps α → (α → Std.Do.PredTrans ps β) → Std.Do.PredTrans ps β
-- Mathlib.CategoryTheory.Grothendieck
/-- The morphism from the pushforward to the source fiber object to the target fiber object.  -/
CategoryTheory.Grothendieck.Hom.fiber : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {X Y : CategoryTheory.Grothendieck F} → (self : X.Hom Y) → (F.map self.base).toFunctor.obj X.fiber ⟶ Y.fiber
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.ofNat : ℕ → CategoryTheory.Limits.WalkingReflexivePair
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.sigmoid_nonneg : ∀ (x : ℝ), 0 ≤ x.sigmoid
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.ker.incl_comp_lift : ∀ {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₁ V₂)
  (g : NormedAddGroupHom V₂ V₃) (h : g.comp f = 0),
  (NormedAddGroupHom.incl g.ker).comp (NormedAddGroupHom.ker.lift f g h) = f
-- Mathlib.Algebra.Tropical.Basic
Tropical.untrop_zero : ∀ {R : Type u} [inst : Top R], Tropical.untrop 0 = ⊤
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.isStackFor_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C}
  (R : CategoryTheory.Presieve S), F.IsStackFor R ↔ (F.toDescentData fun f => f.obj.hom).IsEquivalence
-- Mathlib.Data.Nat.Bits
Nat.bit_le : ∀ (b : Bool) {m n : ℕ}, m ≤ n → Nat.bit b m ≤ Nat.bit b n
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- A refl prefunctor can be promoted to a functor if it respects composition.  -/
CategoryTheory.ReflPrefunctor.toFunctor : {C D : CategoryTheory.Cat} →
  (F : CategoryTheory.ReflQuiv.of ↑C ⟶ CategoryTheory.ReflQuiv.of ↑D) →
    (∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z),
        F.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)) →
      CategoryTheory.Functor ↑C ↑D
-- Std.Data.TreeMap.Raw.Lemmas
/-- Simpler variant of `getElem?_filter` when `LawfulEqCmp` is available.  -/
Std.TreeMap.Raw.getElem?_filter' : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → Bool} {k : α}, t.WF → (Std.TreeMap.Raw.filter f t)[k]? = Option.filter (f k) t[k]?
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.map_id_apply : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} [inst_2 : Fintype X]
  [inst_3 : IsOrderedRing S] (x : ↑(stdSimplex S X)), stdSimplex.map id x = x
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearEquiv.conjContinuousAlgEquiv_trans : ∀ {𝕜 : Type u_1} {E : Type u_2} {G : Type u_4} {H : Type u_5} [inst : AddCommGroup E] [inst_1 : AddCommGroup G]
  [inst_2 : AddCommGroup H] [inst_3 : NormedField 𝕜] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 G] [inst_6 : Module 𝕜 H]
  [inst_7 : TopologicalSpace E] [inst_8 : TopologicalSpace G] [inst_9 : TopologicalSpace H]
  [inst_10 : IsTopologicalAddGroup G] [inst_11 : IsTopologicalAddGroup H] [inst_12 : ContinuousConstSMul 𝕜 G]
  [inst_13 : ContinuousConstSMul 𝕜 H] [inst_14 : IsTopologicalAddGroup E] [inst_15 : ContinuousConstSMul 𝕜 E]
  (e : E ≃L[𝕜] G) (f : G ≃L[𝕜] H),
  (e.trans f).conjContinuousAlgEquiv = e.conjContinuousAlgEquiv.trans f.conjContinuousAlgEquiv
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.invert_C : ∀ {R : Type u_3} [inst : CommSemiring R] (t : R),
  LaurentPolynomial.invert (LaurentPolynomial.C t) = LaurentPolynomial.C t
-- Mathlib.CategoryTheory.Pi.Basic
_private.Mathlib.CategoryTheory.Pi.Basic.0.CategoryTheory.Pi.sumElimCategory.match_19.splitter : {I J : Type u_1} →
  (motive : I ⊕ J → Sort u_2) → (x : I ⊕ J) → ((i : I) → motive (Sum.inl i)) → ((j : J) → motive (Sum.inr j)) → motive x
-- Lean.Parser.Do
Lean.Parser.Term.doDbgTrace.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- `PreservesFilteredColimitsOfSize_shrink.{w, w'} F` tries to obtain
`PreservesFilteredColimitsOfSize.{w, w'} F` from some other `PreservesFilteredColimitsOfSize F`.
 -/
CategoryTheory.Limits.preservesFilteredColimitsOfSize_shrink : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Analysis.Fourier.FourierTransform
Real.instFourierTransformInv : {V : Type u_1} →
  {E : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℂ E] →
        [inst : NormedAddCommGroup V] →
          [inst_1 : InnerProductSpace ℝ V] →
            [inst_2 : MeasurableSpace V] →
              [BorelSpace V] → [FiniteDimensional ℝ V] → FourierTransformInv (V → E) (V → E)
-- Mathlib.GroupTheory.Finiteness
AddSubgroup.FG.finset_sup : ∀ {G : Type u_3} [inst : AddGroup G] {ι : Type u_5} (s : Finset ι) (P : ι → AddSubgroup G),
  (∀ i ∈ s, (P i).FG) → (s.sup P).FG
-- Std.Internal.Do.Order.Instances
Std.Internal.Do.CompleteLattice.instTransRel_std : {l : Sort u_1} →
  [inst : Lean.Order.CompleteLattice l] →
    Trans (fun x1 x2 => Lean.Order.PartialOrder.rel x1 x2) (fun x1 x2 => Lean.Order.PartialOrder.rel x1 x2) fun x1 x2 =>
      Lean.Order.PartialOrder.rel x1 x2
-- Mathlib.Analysis.Calculus.ImplicitContDiff
ContDiffAt.implicitFunction_def : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁]
  [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂] [inst_5 : NormedSpace 𝕜 E₂]
  [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F]
  [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {n : WithTop ℕ∞} (cdf : ContDiffAt 𝕜 n f u) (pn : n ≠ 0)
  (if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible),
  cdf.implicitFunction pn if₂ = ⋯.implicitFunctionOfProdDomain if₂
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The iterated derivative is given by the derivative of the `n-1` iterated derivative.  -/
DifferentiableAt.iteratedFDeriv_succ_apply_left' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {n : ℕ} {m : Fin (n + 1) → E},
  DifferentiableAt 𝕜 (iteratedFDeriv 𝕜 n f) x →
    (iteratedFDeriv 𝕜 (n + 1) f x) m = (fderiv 𝕜 (fun y => (iteratedFDeriv 𝕜 n f y) (Fin.tail m)) x) (m 0)
-- Mathlib.Analysis.Normed.Group.Bounded
Filter.HasBasis.cobounded_of_norm' : ∀ {E : Type u_2} [inst : SeminormedGroup E] {ι : Sort u_5} {p : ι → Prop} {s : ι → Set ℝ},
  Filter.atTop.HasBasis p s → (Bornology.cobounded E).HasBasis p fun i => norm ⁻¹' s i
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- A measurable version of `v.limRatio ρ`. Do *not* use this definition: it is only a temporary
device to show that `v.limRatio` is almost everywhere equal to the Radon-Nikodym derivative.  -/
VitaliFamily.limRatioMeas : {α : Type u_1} →
  [inst : PseudoMetricSpace α] →
    {m0 : MeasurableSpace α} →
      {μ : MeasureTheory.Measure α} →
        VitaliFamily μ →
          [SecondCountableTopology α] →
            [BorelSpace α] →
              [MeasureTheory.IsLocallyFiniteMeasure μ] →
                {ρ : MeasureTheory.Measure α} →
                  [MeasureTheory.IsLocallyFiniteMeasure ρ] → ρ.AbsolutelyContinuous μ → α → ENNReal