mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
ConditionallyCompletePartialOrder.mk : {α : Type u_3} →
  [toConditionallyCompletePartialOrderSup : ConditionallyCompletePartialOrderSup α] →
    [toInfSet : InfSet α] →
      (∀ (s : Set α), DirectedOn (fun x1 x2 => x1 ≥ x2) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)) →
        ConditionallyCompletePartialOrder α
-- Aesop.Check
Aesop.Check.proofReconstruction : Aesop.Check
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.addSubgroupOf_mono : ∀ {G : Type u_1} [inst : AddGroup G] {H₁ H₂ : AddSubgroup G} (H₃ : AddSubgroup G),
  H₁ ≤ H₂ → H₁.addSubgroupOf H₃ ≤ H₂.addSubgroupOf H₃
-- Mathlib.Topology.Algebra.InfiniteSum.Real
summable_prod_of_nonneg : ∀ {α : Type u_3} {β : Type u_4} {f : α × β → ℝ},
  0 ≤ f → (Summable f ↔ (∀ (x : α), Summable fun y => f (x, y)) ∧ Summable fun x => ∑' (y : β), f (x, y))
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
CategoryTheory.Limits.PreservesCofilteredLimitsOfSize.preserves_cofiltered_limits : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D}
  [self : CategoryTheory.Limits.PreservesCofilteredLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] (J : Type w)
  [inst_2 : CategoryTheory.Category.{w', w} J] [CategoryTheory.IsCofiltered J],
  CategoryTheory.Limits.PreservesLimitsOfShape J F
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- Implementation of `SheafConditionPairwiseIntersections.coneEquiv`.  -/
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        (F : TopCat.Presheaf C X) →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U).comp
                  (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U) ≅
                CategoryTheory.Functor.id
                  (CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U))
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.map_of_preservesRightHomologyOf : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C},
  S.Exact →
    ∀ (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [F.PreservesRightHomologyOf S]
      [(S.map F).HasHomology], (S.map F).Exact
-- Mathlib.Probability.Moments.IntegrableExpMul
ProbabilityTheory.rpow_abs_le_mul_max_exp : ∀ (x : ℝ) {t p : ℝ}, 0 ≤ p → t ≠ 0 → |x| ^ p ≤ (p / |t|) ^ p * max (Real.exp (t * x)) (Real.exp (-t * x))
-- Lean.Setup
Lean.instReprImport : Repr Lean.Import
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  {P : PresheafOfModules R₀} {F : SheafOfModules R}
  (g : P ⟶ (PresheafOfModules.restrictScalars α).obj ((SheafOfModules.forget R).obj F)),
  (SheafOfModules.toSheaf R).map ((PresheafOfModules.sheafificationHomEquiv α).symm g) =
    ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf
          ((SheafOfModules.toSheaf R).obj F)).symm
      ((PresheafOfModules.toPresheaf R₀).map g)
-- Mathlib.Analysis.Normed.Lp.lpSpace
memℓp_infty : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
  BddAbove (Set.range fun i => ‖f i‖) → Memℓp f ⊤
-- Mathlib.Order.Antisymmetrization
AntisymmRel.symmGen_congr : ∀ {α : Type u_1} {a b c d : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b →
    AntisymmRel (fun x1 x2 => x1 ≤ x2) c d →
      (Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a c ↔ Relation.SymmGen (fun x1 x2 => x1 ≤ x2) b d)
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.apply_ofBijective_symm_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [inst_4 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_5 : RingHomInvPair σ₂₁ σ₁₂] {h : Function.Bijective ⇑f} (x : M₂), f ((LinearEquiv.ofBijective f h).symm x) = x
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The sum of measurable functions is measurable.  -/
Measurable.tsum : ∀ {X : Type u_6} {E : Type u_7} {ι : Type u_8} [inst : MeasurableSpace X] [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace E] [SecondCountableTopology E]
  [inst_5 : MeasurableSpace E] [BorelSpace E] [MeasurableAdd₂ E] [Countable ι] {L : SummationFilter ι} [L.NeBot]
  [L.filter.IsCountablyGenerated] {f : ι → X → E},
  (∀ (i : ι), Measurable (f i)) → Measurable fun x => ∑'[L] (i : ι), f i x
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `differentiableOn_add_const_iff`. -/
DifferentiableOn.add_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} (c : F), DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 (fun y => f y + c) s
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.coe_disjUnion : ∀ {α : Type u_1} {n m : ℕ} {s : ↑(Set.powersetCard α m)} {t : ↑(Set.powersetCard α n)} {hst : Disjoint ↑s ↑t},
  ↑(Set.powersetCard.disjUnion hst) = (↑s).disjUnion (↑t) hst
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.sub.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.gt) → (Unit → motive Ordering.eq) → motive x
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- Composition of `BasedNatTrans`, given by composition of the underlying natural
transformations.  -/
CategoryTheory.BasedNatTrans.comp : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {𝒳 : CategoryTheory.BasedCategory 𝒮} →
      {𝒴 : CategoryTheory.BasedCategory 𝒮} →
        {F G H : CategoryTheory.BasedFunctor 𝒳 𝒴} →
          CategoryTheory.BasedNatTrans F G → CategoryTheory.BasedNatTrans G H → CategoryTheory.BasedNatTrans F H
-- Mathlib.FieldTheory.AbelRuffini
gal_X_pow_sub_one_isSolvable : ∀ {F : Type u_1} [inst : Field F] (n : ℕ), Group.IsSolvable (Polynomial.X ^ n - 1).Gal
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.toSubmonoid_injective : ∀ {R : Type u} [inst : NonAssocRing R], Function.Injective fun s => s.toSubmonoid
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.toContinuousAffineEquiv_refl : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P],
  (AffineIsometryEquiv.refl 𝕜 P).toContinuousAffineEquiv = ContinuousAffineEquiv.refl 𝕜 P
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Cycle.formPerm_apply_mem_eq_next : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (h : s.Nodup) (x : α) (hx : x ∈ s),
  (s.formPerm h) x = s.next h x hx
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.restrictionGEIso_inv_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (i : ℕ),
  h.restrictionGEIso.inv.f i =
    (HomologicalComplex.restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).inv
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.mono : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s t : Set α},
  t ⊆ s → eVariationOn f t ≤ eVariationOn f s
-- Init.Data.List.ToArray
Array.forIn'.loop.congr_simp : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α)
  (f f_1 : (a : α) → a ∈ as → β → m (ForInStep β)),
  f = f_1 →
    ∀ (i i_1 : ℕ) (e_i : i = i_1) (h : i ≤ as.size) (b b_1 : β),
      b = b_1 → Array.forIn'.loop as f i h b = Array.forIn'.loop as f_1 i_1 ⋯ b_1
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
/-- Put the same topological space structure on `Mᵈᵃᵃ` as on the original space.  -/
DomAddAct.instTopologicalSpace : {M : Type u_1} → [TopologicalSpace M] → TopologicalSpace Mᵈᵃᵃ
-- Lean.Elab.Command
_private.Lean.Elab.Command.0.Lean.Elab.Command.getVarDecls : Lean.Elab.Command.State → Array Lean.Syntax
-- Mathlib.GroupTheory.ArchimedeanDensely
LinearOrderedAddCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Nontrivial G] {g : G},
  ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G ≃+o ℤ)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
/-- The abelian group structure on `L.obj X ⟶ L.obj Y` when `L : C ⥤ D` is a localization
functor, `C` is preadditive and there is a left calculus of fractions.  -/
CategoryTheory.Localization.Preadditive.addCommGroup' : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [CategoryTheory.Preadditive C] →
          (L : CategoryTheory.Functor C D) →
            (W : CategoryTheory.MorphismProperty C) →
              [L.IsLocalization W] → [W.HasLeftCalculusOfFractions] → (X Y : C) → AddCommGroup (L.obj X ⟶ L.obj Y)
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (y, x - y)` sends `μ × ν` to `ν × μ`.  -/
MeasureTheory.measurePreserving_prod_sub_swap : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddRightInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.2, z.1 - z.2)) (μ.prod ν) (ν.prod μ)
-- Mathlib.NumberTheory.KummerDedekind
KummerDedekind.quotMapEquivQuotQuotMap_symm_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} {I : Ideal R}
  [inst_3 : IsDomain R] [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDedekindDomain S]
  [inst_6 : Module.IsTorsionFree R S] (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x)
  (Q : Polynomial R),
  (KummerDedekind.quotMapEquivQuotQuotMap hx hx').symm
      ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
        (Polynomial.map (Ideal.Quotient.mk I) Q)) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((Polynomial.aeval x) Q)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_and_epi_g_iff_g_is_cokernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex C) [CategoryTheory.Balanced C] [S.HasHomology],
  S.Exact ∧ CategoryTheory.Epi S.g ↔
    Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯))
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instMulAction : {α : Type u_1} →
  {β : Type u_2} → {l : Filter α} → {M : Type u_5} → [inst : Monoid M] → [MulAction M β] → MulAction M (l.Germ β)
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_transpose : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : Field R] [inst_2 : Fintype m]
  (A : Matrix m n R), A.transpose.rank = A.rank
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapNatIso_unitIso_hom_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S S' : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.mapNatIso i).unitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Lean.Meta.Tactic.SolveByElim
/-- Trying calling `intro` if no lemmas apply.  -/
Lean.Meta.SolveByElim.SolveByElimConfig.intro : Lean.Meta.SolveByElim.SolveByElimConfig → Bool
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instIsFractionRing : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : CommRing R] (v : Valuation R Γ₀)
  {S : Type u_4} [inst_2 : CommSemiring S] [inst_3 : Algebra R S] [i : IsFractionRing R S], IsFractionRing (WithVal v) S
-- Std.Data.ExtDTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `fallback` if `n` is at least `t.size`.  -/
Std.ExtDTreeMap.entryAtIdxD : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → ℕ → (a : α) × β a → (a : α) × β a
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.iSup_filtration : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E]
  {i : WithTop (Module.rank F E).ord.ToType},
  Order.IsSuccPrelimit i → ⨆ j, Field.Emb.Cardinal.filtration ↑j = Field.Emb.Cardinal.filtration i
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.continuous_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α], Continuous fun x => {x}
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.impImpSimp.sizeOf_spec : ∀ (x : Lean.Name) (p : Mathlib.Tactic.ITauto.Proof),
  sizeOf (Mathlib.Tactic.ITauto.Proof.impImpSimp x p) = 1 + sizeOf x + sizeOf p
-- Mathlib.Topology.ContinuousOn
ContinuousOn.image_closure : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  ContinuousOn f (closure s) → f '' closure s ⊆ closure (f '' s)
-- Mathlib.Topology.Algebra.Field
Subfield.le_topologicalClosure : ∀ {α : Type u_2} [inst : Field α] [inst_1 : TopologicalSpace α] [inst_2 : IsTopologicalDivisionRing α] (s : Subfield α),
  s ≤ s.topologicalClosure
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_singletonZeroHom : ∀ {α : Type u_2} [inst : Zero α], ⇑Finset.singletonZeroHom = singleton
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
CategoryTheory.Functor.mapDerivedCategoryFactors_inv_app_mapDerivedCategorySingleFunctor_hom_app : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.Abelian C₁]
  [inst_2 : HasDerivedCategory C₁] {C₂ : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂]
  [inst_4 : CategoryTheory.Abelian C₂] [inst_5 : HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂)
  [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] (X : C₁),
  CategoryTheory.CategoryStruct.comp
      (F.mapDerivedCategoryFactors.inv.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X))
      ((F.mapDerivedCategorySingleFunctor 0).hom.app X) =
    DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).hom.app X)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_alter_of_beq_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' : α} {f : Option (β k) → Option (β k)}, m.WF → (k == k') = false → (m.alter k f).contains k' = m.contains k'
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
GrpCat.toAddGrp_map : ∀ {x x_1 : GrpCat} (f : x ⟶ x_1), GrpCat.toAddGrp.map f = AddGrpCat.ofHom (MonoidHom.toAdditive (GrpCat.Hom.hom f))
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback.comp_diagonal_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : C}
  (h : CategoryTheory.Limits.pullback.diagonalObj g ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal g) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f g)
          (CategoryTheory.CategoryStruct.comp f g) g g f f (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)
        h)
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.adj_inj : ∀ {V : Type u_2} {G H : Digraph V}, G.Adj = H.Adj ↔ G = H
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.getIsLinearOrderInst : Lean.Meta.Grind.Arith.Linear.LinearM Lean.Expr
-- Mathlib.Topology.Order
/-- The open sets of the least topology containing a collection of basic sets.  -/
TopologicalSpace.GenerateOpen : {α : Type u} → Set (Set α) → Set α → Prop
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.BorelCantelli.process_difference_le : ∀ {Ω : Type u_2} (s : ℕ → Set Ω) (ω : Ω) (n : ℕ),
  |MeasureTheory.BorelCantelli.process s (n + 1) ω - MeasureTheory.BorelCantelli.process s n ω| ≤ ↑1
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Adjunction.mapGrp_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.Monoidal],
  a.mapGrp.unit =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapGrpIdIso.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapGrpNatTrans a.unit)
        CategoryTheory.Functor.mapGrpCompIso.hom)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_11.splitter : (w : ℕ) →
  (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
    (motive : Std.Tactic.BVDecide.BVExpr.Return aig w → Sort u_1) →
      (x : Std.Tactic.BVDecide.BVExpr.Return aig w) →
        ((aig_1 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
            (rhs : aig_1.RefVec w) →
              (hraig : aig.decls.size ≤ { aig := aig_1, vec := rhs }.aig.decls.size) →
                (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑⟨{ aig := aig_1, vec := rhs }, hraig⟩).aig) →
                  motive { result := ⟨{ aig := aig_1, vec := rhs }, hraig⟩, cache := cache }) →
          motive x
-- Lean.Elab.Term.TermElabM
/-- Execute `x` and return `some` if no new errors were recorded or exceptions were thrown. Otherwise, return `none`.  -/
Lean.Elab.Term.commitIfNoErrors? : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM (Option α)
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LeftLinear.instIsIsoδₗ : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'] [inst_6 : F.LeftLinear C] (c : C) (d : D),
  CategoryTheory.IsIso (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c d)
-- Mathlib.Order.CompleteLattice.Basic
/-- **Alias** of `sInf_upperBounds_eq_sSup`. -/
sInf_upperBounds_eq_csSup : ∀ {α : Type u_1} [inst : CompleteLattice α] (s : Set α), sInf (upperBounds s) = sSup s
-- Mathlib.Tactic.Convert
Convert.ExpensiveConfig.mk.sizeOf_spec : ∀ (toConfig : Congr!.Config), sizeOf { toConfig := toConfig } = 1 + sizeOf toConfig
-- Mathlib.ModelTheory.Basic
/-- The homomorphism sends related elements to related elements  -/
FirstOrder.Language.Equiv.map_rel' : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (self : L.Equiv M N) {n : ℕ} (r : L.Relations n) (x : Fin n → M),
  FirstOrder.Language.Structure.RelMap r (self.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] {f : α → ENNReal}
  (s : Set α),
  AEMeasurable f (μ.restrict s) →
    ∀ (g : α → ENNReal),
      (∀ᵐ (x : α) ∂μ.restrict s, f x < ⊤) → ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- For each match alternative, the names to use for the pattern variables.
Each ends with `hNames?.filterMap id` exactly.  -/
Lean.PrettyPrinter.Delaborator.AppMatchState.varNames : Lean.PrettyPrinter.Delaborator.AppMatchState → Array (Array Lean.Name)
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.opEquivalence_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C),
  P.opEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id P.op.FullSubcategory)
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.Database.lmfdb.sizeOf_spec : sizeOf Mathlib.CrossRef.Database.lmfdb = 1
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.mk : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι} {φ : ι → Set α},
  (∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in l, x ∈ φ i) → (∀ (i : ι), MeasurableSet (φ i)) → MeasureTheory.AECover μ l φ
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- A coproduct over an index type with exactly one term is just the object over that term.  -/
CategoryTheory.Limits.coproductUniqueIso : {β : Type w} →
  {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [inst_1 : Unique β] → (f : β → C) → ∐ f ≅ f default
-- Mathlib.RingTheory.Ideal.Operations
Ideal.iInf_span_singleton : ∀ {R : Type u} [inst : CommSemiring R] {ι : Type u_2} [inst_1 : Fintype ι] {I : ι → R},
  (∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)) → ⨅ i, Ideal.span {I i} = Ideal.span {∏ i, I i}
-- Lean.Declaration
Lean.instBEqInductiveType : BEq Lean.InductiveType
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
MulActionHom.embMap.eq_1 : ∀ (G : Type u_1) (α : Type u_2) [inst : Group G] [inst_1 : MulAction G α] {m : Type u_5} {n : Type u_6} (e : m ↪ n),
  MulActionHom.embMap G α e = { toFun := fun i => e.trans i, map_smul' := ⋯ }
-- Init.Data.Array.Basic
/-- Computes the sum of the elements of an array.

Examples:
* `#[a, b, c].sum = a + (b + (c + 0))`
* `#[1, 2, 5].sum = 8`
 -/
Array.sum : {α : Type u_1} → [Add α] → [Zero α] → Array α → α
-- Mathlib.Order.SuccPred.Limit
/-- **Alias** of the reverse direction of `Order.isPredLimit_toDual_iff`. -/
Order.IsSuccLimit.dual : ∀ {α : Type u_1} {a : α} [inst : Preorder α], Order.IsSuccLimit a → Order.IsPredLimit (OrderDual.toDual a)
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.addCommSemigroup.eq_1 : ∀ {M : Type u_4} [inst : AddCommSemigroup M] (c : AddCon M),
  c.addCommSemigroup = Function.Surjective.addCommSemigroup Quotient.mk'' ⋯ ⋯