mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- Interpret a `CatCommSqOver` as a functor to the categorical pullback.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor A B) →
              (G : CategoryTheory.Functor C B) →
                (X : Type u₄) →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    CategoryTheory.Functor (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
                      (CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G))
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Specialize.imp_stateful : ∀ {σs : List (Type u)} {P P' Q R : Std.Do.SPred σs}, (P ∧ (Q → R) ⊣⊢ₛ P' ∧ Q) → P ∧ (Q → R) ⊢ₛ P ∧ R
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor for additive groups is faithful.  -/
AddGrpCat.instFaithfulUliftFunctor : AddGrpCat.uliftFunctor.Faithful
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.obj_zero_map_μ_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) {m : M}
  {X Y : C} (f : X ⟶ (F.obj m).obj Y) [inst_3 : F.Monoidal] {Z : C}
  (h :
    (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj m (CategoryTheory.MonoidalCategoryStruct.tensorUnit M))).obj
        Y ⟶
      Z),
  CategoryTheory.CategoryStruct.comp ((F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit M)).map f)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.LaxMonoidal.μ F m (CategoryTheory.MonoidalCategoryStruct.tensorUnit M)).app Y) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.η F).app X)
      (CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor m).inv).app Y)
          h))
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.comp_hom_assoc : ∀ {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} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {X_1 Y Z : F.DescentData' sq sq₃} (f_1 : X_1 ⟶ Y) (g : Y ⟶ Z) (i : ι) {Z_1 : ↑(F.obj { as := Opposite.op (X i) })}
  (h : Z.obj i ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp f_1 g).hom i) h =
    CategoryTheory.CategoryStruct.comp (f_1.hom i) (CategoryTheory.CategoryStruct.comp (g.hom i) h)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.trajContent.congr_simp : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (κ κ_1 : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))) (e_κ : κ = κ_1)
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {a : ℕ} (x₀ x₀_1 : (i : ↥(Finset.Iic a)) → X ↑i),
  x₀ = x₀_1 → ProbabilityTheory.Kernel.trajContent κ x₀ = ProbabilityTheory.Kernel.trajContent κ_1 x₀_1
-- Lean.Elab.DeclModifiers
Lean.Elab.ExpandDeclIdResult.mk.inj : ∀ {shortName declName : Lean.Name} {levelNames : List Lean.Name}
  {docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)} {shortName_1 declName_1 : Lean.Name}
  {levelNames_1 : List Lean.Name} {docString?_1 : Option (Lean.TSyntax `Lean.Parser.Command.docComment)},
  { shortName := shortName, declName := declName, levelNames := levelNames, docString? := docString? } =
      { shortName := shortName_1, declName := declName_1, levelNames := levelNames_1, docString? := docString?_1 } →
    shortName = shortName_1 ∧ declName = declName_1 ∧ levelNames = levelNames_1 ∧ docString? = docString?_1
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.mem_bot : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {x : R}, x ∈ ⊥ ↔ x = 0
-- Std.Http.Protocol.H1
/-- Upper bound for unread input retained in memory at once.

This caps buffered body bytes and parser lookahead (start-line/headers/chunk
metadata) so a stalled consumer cannot accumulate unbounded pending input.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.maxBufferedInputBytes : Std.Http.Protocol.H1.Config → ℕ
-- Mathlib.Algebra.Ring.Pi
Pi.ring : {I : Type u} → {f : I → Type v} → [(i : I) → Ring (f i)] → Ring ((i : I) → f i)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.hasRightHomology_of_epi_of_isIso_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasRightHomology] [CategoryTheory.Epi φ.τ₁]
  [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃], S₂.HasRightHomology
-- Mathlib.Tactic.CongrExclamation
CongrState.mk.sizeOf_spec : ∀ (goals : Array Lean.MVarId) (patterns : List (Lean.TSyntax `rintroPat)),
  sizeOf { goals := goals, patterns := patterns } = 1 + sizeOf goals + sizeOf patterns
-- Mathlib.RingTheory.HahnSeries.Basic
/-- The equivalence between iterated Hahn series and Hahn series on the lex product.  -/
HahnSeries.iterateEquiv : {Γ : Type u_1} →
  {Γ' : Type u_2} →
    {R : Type u_3} →
      [inst : PartialOrder Γ] →
        [inst_1 : Zero R] → [inst_2 : PartialOrder Γ'] → HahnSeries Γ (HahnSeries Γ' R) ≃ HahnSeries (Lex (Γ × Γ')) R
-- Mathlib.Topology.Algebra.OpenSubgroup
/-- If a subgroup of a topological group has `1` in its interior, then it is open.  -/
Subgroup.isOpen_of_one_mem_interior : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousMul G] (H : Subgroup G),
  1 ∈ interior ↑H → IsOpen ↑H
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.ext_iff : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {φ₁ φ₂ : A →ₗc[R] B}, φ₁ = φ₂ ↔ ∀ (x : A), φ₁ x = φ₂ x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int8.reduceLT : Lean.Meta.Simp.Simproc
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.fullSubcategory_leftUnitor_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [inst_3 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)]
  (X : P.FullSubcategory),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.obj).hom
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.supSet : {V : Type u_2} → SupSet (Digraph V)
-- Mathlib.Geometry.Convex.Set
Convexity.subtypeVal_sConvexComb : ∀ {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] (s : Set X) (hs : Convexity.IsConvexSet R s) (w : Convexity.StdSimplex R ↑s),
  ↑(Convexity.sConvexComb w) = Convexity.iConvexComb w Subtype.val
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.clift_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoid.Coprod.clift AddMonoid.Coprod.mk ⋯ ⋯ ⋯ ⋯ = AddMonoidHom.id (AddMonoid.Coprod M N)
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `wbtw_const_vsub_iff`. -/
Wbtw.const_vsub : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P} (p : P), Wbtw R x y z → Wbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.zsmul : ∀ {S : Type u_2} [inst : AddGroup S] [inst_1 : Mul S] (t : RingCon S) (z : ℤ) {x y : S}, t x y → t (z • x) (z • y)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_add : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : AddMonoid α] [inst_1 : StarAddMonoid α] (M N : Matrix m n α),
  (M + N).conjTranspose = M.conjTranspose + N.conjTranspose
-- Lean.Language.Basic
/-- Composes two `SnapshotTreeTransform`s, applying `inner` first and then `outer`.  -/
Lean.Language.SnapshotTreeTransform.compose : Lean.Language.SnapshotTreeTransform → Lean.Language.SnapshotTreeTransform → Lean.Language.SnapshotTreeTransform
-- Lean.Elab.DocString
/-- If `true`, suggestions are provided for code elements.
 -/
_private.Lean.Elab.DocString.0.Lean.Doc.doc.verso.suggestions : Lean.Option Bool
-- Mathlib.Analysis.RCLike.Basic
/-- The imaginary part as an additive monoid homomorphism  -/
RCLike.im : {K : semiOutParam (Type u_1)} → [self : RCLike K] → K →+ ℝ
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_atTop_isGLB : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α] [inst_2 : Preorder α]
  [InfConvergenceClass α] {f : ι → α} {a : α},
  Antitone f → IsGLB (Set.range f) a → Filter.Tendsto f Filter.atTop (nhds a)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- `CommRing` instance for `type`  -/
Lean.Meta.Grind.Arith.CommRing.CommRing.commRingInst : Lean.Meta.Grind.Arith.CommRing.CommRing → Lean.Expr
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withBotWithTop_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  (f : LatticeHom β γ) (g : LatticeHom α β), (f.comp g).withBotWithTop = f.withBotWithTop.comp g.withBotWithTop
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.supportSet_subset_zeroLocus : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens), I.supportSet ⊆ X.zeroLocus ↑(I.ideal U)
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.ExactAt.unop : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K : HomologicalComplex Vᵒᵖ c} {i : ι},
  K.ExactAt i → K.unop.ExactAt i
-- Std.Data.HashMap.Raw
/-- Computes the union of the given hash maps, inserting smaller hash map into a bigger hash map. In the case of clashes of keys, entries from the left argument, are replaced with entries from the right argument.  -/
Std.HashMap.Raw.union : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Std.HashMap.Raw α β → Std.HashMap.Raw α β → Std.HashMap.Raw α β
-- Init.Data.Int.Lemmas
Int.mul_eq_mul_right_iff : ∀ {a b c : ℤ}, c ≠ 0 → (a * c = b * c ↔ a = b)
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instIntCastOfNatIntOfHasDetPlusMinusOneFinNatReal : {Γ : Subgroup (GL (Fin 2) ℝ)} → [Γ.HasDetPlusMinusOne] → IntCast (ModularForm Γ 0)
-- Mathlib.Algebra.BigOperators.Finprod
/-- The sum of `f i` over `i ∈ {a}` equals `f a`.  -/
finsum_mem_singleton : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {a : α}, ∑ᶠ (i : α) (_ : i ∈ {a}), f i = f a
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.restrictIndepMatroid_Indep : ∀ {α : Type u_1} (M : Matroid α) (R I : Set α), (M.restrictIndepMatroid R).Indep I = (M.Indep I ∧ I ⊆ R)
-- Init.Data.SInt.Bitwise
Int32.not_eq_neg_sub : ∀ (a : Int32), ~~~a = -a - 1
-- Mathlib.Analysis.Analytic.CPolynomialDef
CPolynomialAt.eventually_cpolynomialAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E},
  CPolynomialAt 𝕜 f x → ∀ᶠ (y : E) in nhds x, CPolynomialAt 𝕜 f y
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.iSup_eq_closure : ∀ {G : Type u_1} [inst : Group G] {ι : Sort u_2} (p : ι → Subgroup G), ⨆ i, p i = Subgroup.closure (⋃ i, ↑(p i))
-- Mathlib.Algebra.Order.Group.Cyclic
/-- Given an additive subgroup of an additive cyclic linearly ordered
commutative group, this is a negative generator of the subgroup.  -/
LinearOrderedAddCommGroup.Subgroup.negGen : {G : Type u_1} →
  [inst : AddCommGroup G] →
    [inst_1 : LinearOrder G] →
      [IsOrderedAddMonoid G] → (H : AddSubgroup G) → [Nontrivial ↥H] → [hH : IsAddCyclic ↥H] → G
-- Mathlib.Tactic.FunProp.Mor
Mathlib.Meta.FunProp.Mor.Arg.mk.inj : ∀ {expr : Lean.Expr} {coe : Option Lean.Expr} {expr_1 : Lean.Expr} {coe_1 : Option Lean.Expr},
  { expr := expr, coe := coe } = { expr := expr_1, coe := coe_1 } → expr = expr_1 ∧ coe = coe_1
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
/-- `simplicialInsert` just adds one to the length.  -/
SimplexCategoryGenRel.simplicialInsert_length : ∀ (a : ℕ) (L : List ℕ), (SimplexCategoryGenRel.simplicialInsert a L).length = L.length + 1
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_intCast : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (n : ℤ), F⟮↑n⟯ = ⊥
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_eq_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} [inst_2 : Zero α]
  [IsBotZeroClass α] (hs : s.Nonempty), s.sup' hs f = 0 ↔ ∀ i ∈ s, f i = 0
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkCoinductiveAux₁.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : CochainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 1 ⟶ Q.X 0) (one : P.X 2 ⟶ Q.X 1)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one)
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X (n + 1) ⟶ Q.X n) ×'
            (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) +
                  CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') →
        (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) +
              CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f''),
  Homotopy.mkCoinductiveAux₁ e zero one comm_one succ 0 = ⟨zero, ⟨one, comm_one⟩⟩
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_left_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G]
  [inst_4 : (G.sheafPushforwardContinuous A J K).IsEquivalence] [inst_5 : CategoryTheory.HasWeakSheafify J A]
  {P₁ P₂ : CategoryTheory.Functor Dᵒᵖ A} (f : P₁ ⟶ P₂) {Q : CategoryTheory.Sheaf K A}
  (g : (CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q)
  {Z : CategoryTheory.Functor Dᵒᵖ A} (h : Q.obj ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence J K G)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A).map f) g))
      h =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence J K G) g) h)
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `none` if the
map is empty.
 -/
Std.DTreeMap.Raw.Const.maxEntry? : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → Option (α × β)
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.lift_mk : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N],
  TensorProduct.lift (TensorProduct.mk R M N) = LinearMap.id
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β] (f : α →*₀o β), (OrderMonoidWithZeroHom.id β).comp f = f
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Attempts to find the value with key `k : α` in `t` and panics if there is no such key.
 -/
RBTree.RBSet.findP! : {α : Type u_1} → {cmp : α → α → Ordering} → [Inhabited α] → RBTree.RBSet α cmp → (α → Ordering) → α
-- Std.Time.Duration
Std.Time.Duration.instHAdd : HAdd Std.Time.Duration Std.Time.Duration Std.Time.Duration
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.support_cycleBypass_sublist_support : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [inst : DecidableEq V] (w : G.Walk v v),
  w.cycleBypass.support.Sublist w.support
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.isNPowInst : Lean.Expr → Lean.Meta.Grind.Arith.FieldNormNum.M✝ Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.relStructSuccEquivMulStruct_apply_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin n}
  (h : f.RelStruct g i.succ), (SSet.PtSimplex.relStructSuccEquivMulStruct h).map = h.map
-- Init.Data.Array.Bootstrap
_private.Init.Data.Array.Bootstrap.0.Array.forIn'.loop.match_3.eq_2 : ∀ {α : Type u_1} (as : Array α) (motive : (i : ℕ) → i ≤ as.size → Sort u_2) (i : ℕ) (h : i + 1 ≤ as.size)
  (h_1 : (x : 0 ≤ as.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ as.size) → motive i.succ h),
  (match i.succ, h with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_2 i h
-- Mathlib.Order.Notation
/-- Heyting implication 

Conventions for notations in identifiers:

 * The recommended spelling of `⇨` in identifiers is `himp`. -/
«term_⇨_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.instQuasiSoberElemZeroLocus : ∀ {R : Type u} [inst : CommSemiring R] (I : Set R), QuasiSober ↑(PrimeSpectrum.zeroLocus I)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- When an instance of `[HasDerivedCategory.{w'} C]` is available, this is the additive
bijection between `Ext.{w} X Y n` and a type of morphisms in the derived category.  -/
CategoryTheory.Abelian.Ext.homAddEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {X Y : C} →
          [inst_3 : HasDerivedCategory C] →
            {n : ℕ} →
              CategoryTheory.Abelian.Ext X Y n ≃+
                CategoryTheory.ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X)
                  ((DerivedCategory.singleFunctor C 0).obj Y) ↑n
-- Init.Grind.Module.Basic
/-- Scalar multiplication by zero is zero.  -/
Lean.Grind.NatModule.zero_nsmul : ∀ {M : Type u} [self : Lean.Grind.NatModule M] (a : M), 0 • a = 0
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Multipliable.of_add_one_of_neg_add_one : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M] {f : ℤ → M},
  (Multipliable fun n => f (↑n + 1)) → (Multipliable fun n => f (-(↑n + 1))) → Multipliable f
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.comp_toSpanSingleton : ∀ {R : Type u_1} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂) (x : M),
  f ∘ₗ LinearMap.toSpanSingleton R M x = LinearMap.toSpanSingleton R M₂ (f x)
-- Mathlib.Analysis.Normed.Group.Pointwise
add_ball : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E),
  s + Metric.ball x δ = x +ᵥ Metric.thickening δ s
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
/-- The symmetric monoidal structure on `Module R`.  -/
SemimoduleCat.MonoidalCategory.symmetricCategory : {R : Type u} → [inst : CommSemiring R] → CategoryTheory.SymmetricCategory (SemimoduleCat R)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.ext_iff : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Abelian C}
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} {x y : S₁.Hom S₂},
  x = y ↔ x.f₀ = y.f₀ ∧ x.f₁ = y.f₁ ∧ x.f₂ = y.f₂ ∧ x.f₃ = y.f₃
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.dist_def : ∀ {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} [inst : Encodable ι]
  [inst_1 : (i : ι) → PseudoMetricSpace (Y i)] (x y : Metric.PiNatEmbed X Y f),
  dist x y = ∑' (i : ι), min (2⁻¹ ^ Encodable.encode i) (dist (f i x.ofPiNat) (f i y.ofPiNat))
-- Mathlib.Analysis.LConvolution
/-- Scoped notation for the additive convolution of functions with respect to `volume`.  -/
MeasureTheory.«term_⋆ₗ_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.llr_smul_right : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν →
    ∀ (c : ENNReal),
      c ≠ 0 → c ≠ ⊤ → MeasureTheory.llr μ (c • ν) =ᵐ[μ] fun x => MeasureTheory.llr μ ν x - Real.log c.toReal
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
ordinaryHypergeometricSeries_norm_div_succ_norm : ∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] (a b c : 𝕂) (n : ℕ),
  (∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c) →
    ‖ordinaryHypergeometricCoefficient a b c n‖ / ‖ordinaryHypergeometricCoefficient a b c n.succ‖ =
      ‖a + ↑n‖⁻¹ * ‖b + ↑n‖⁻¹ * ‖c + ↑n‖ * ‖1 + ↑n‖
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.support_leadingTerm : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (p : MvPolynomial σ R)
  [inst_1 : Decidable (p = 0)], (m.leadingTerm p).support = if p = 0 then ∅ else {m.degree p}
-- Mathlib.Analysis.Normed.MulAction
NormSMulClass.norm_smul : ∀ {α : Type u_3} {β : Type u_4} {inst : Norm α} {inst_1 : Norm β} {inst_2 : SMul α β} [self : NormSMulClass α β] (r : α)
  (x : β), ‖r • x‖ = ‖r‖ * ‖x‖
-- Mathlib.Order.Hom.Set
StrictMono.orderIso_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] (f : α → β) (h_mono : StrictMono f)
  (a : α), (StrictMono.orderIso f h_mono) a = ⟨f a, ⋯⟩
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.zero_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N X : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] (f : M ⟶ N)
  [CategoryTheory.IsAddMonHom f], CategoryTheory.CategoryStruct.comp 0 f = 0