mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Quaternion
Cardinal.mk_quaternionAlgebra_of_infinite : ∀ {R : Type u_1} (c₁ c₂ c₃ : R) [Infinite R], Cardinal.mk (QuaternionAlgebra R c₁ c₂ c₃) = Cardinal.mk R
-- Mathlib.NumberTheory.MulChar.Basic
MulCharClass.mk : ∀ {F : Type u_3} {R : outParam (Type u_4)} {R' : outParam (Type u_5)} [inst : CommMonoid R]
  [inst_1 : CommMonoidWithZero R'] [inst_2 : FunLike F R R'] [toMonoidHomClass : MonoidHomClass F R R'],
  (∀ (χ : F) {a : R}, ¬IsUnit a → χ a = 0) → MulCharClass F R R'
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.AddGrp C} (f g : A ⟶ B), f.hom.hom = g.hom.hom → f = g
-- Mathlib.RingTheory.FreeCommRing
/-- The canonical map from `α` to the free commutative ring on `α`.  -/
FreeCommRing.of : {α : Type u} → α → FreeCommRing α
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.toFun_eq_coe : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  {X : LeftInvariantDerivation I G}, (↑↑X).toFun = ⇑X
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.mkUnless : Lean.Syntax → Lean.Elab.Term.Do.CodeBlock → Lean.MacroM Lean.Elab.Term.Do.CodeBlock
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The normal closure of a set `s` is the closure of all the additive conjugates of
elements of `s`. It is the smallest normal additive subgroup containing `s`.  -/
AddSubgroup.normalClosure : {G : Type u_1} → [inst : AddGroup G] → Set G → AddSubgroup G
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableSymbolTag : Hashable Lean.Lsp.SymbolTag
-- Mathlib.Logic.Relation
Relation.ReflTransGen.head : ∀ {α : Type u_1} {r : α → α → Prop} {a b c : α}, r a b → Relation.ReflTransGen r b c → Relation.ReflTransGen r a c
-- Mathlib.Algebra.Homology.HomotopyCategory
/-- The homology functor on the homotopy category is induced by
the homology functor on homological complexes.  -/
HomotopyCategory.homologyFunctorFactors : {ι : Type u_2} →
  (V : Type u) →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        (c : ComplexShape ι) →
          [inst_2 : CategoryTheory.CategoryWithHomology V] →
            (i : ι) →
              (HomotopyCategory.quotient V c).comp (HomotopyCategory.homologyFunctor V c i) ≅
                HomologicalComplex.homologyFunctor V c i
-- Mathlib.Tactic.NormDet
/-- `eval_det` normalizes determinants of matrices written using `!![...]` notation
over a commutative ring.

Examples:

```lean
example : Matrix.det (R := ℤ) !![1, 2; 3, 4] = -2 := by
  eval_det

example {R : Type*} [CommRing R] (a b c d : R) :
    Matrix.det !![a, b; c, d] = a * d - b * c := by
  eval_det
  ring
```
 -/
evalDet : Lean.ParserDescr
-- Mathlib.Tactic.Ring.Common
/-- The fallback case for exponentiating polynomials is to use `ExBase.toProd` to just build an
exponent expression. (This has a slightly different normalization than `evalPowAtom` because
the input types are different.)

* `x ^ e = (x + 0) ^ e * 1`
 -/
Mathlib.Tactic.Ring.Common.evalPowProdAtom : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          {a : Q(«$α»)} →
            {b : Q(ℕ)} →
              Mathlib.Tactic.Ring.Common.ExProd bt sα a →
                Mathlib.Tactic.Ring.Common.ExProdNat b →
                  Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExProd bt sα) q(«$a» ^ «$b»)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.one_def : ∀ {K : Type u_1} [inst : CommRing K], RatFunc.one = { toFractionRing := 1 }
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.zero_le_posForm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : LinearOrder S] [inst_7 : IsStrictOrderedRing S] [inst_8 : Algebra S R]
  [inst_9 : FaithfulSMul S R] [inst_10 : Module S M] [inst_11 : IsScalarTower S R M] [inst_12 : P.IsValuedIn S]
  [inst_13 : Fintype ι] (x : ↥(Submodule.span S (Set.range ⇑P.root))), 0 ≤ ((P.posRootForm S).posForm x) x
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddRightCancelMonoidOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : AddRightCancelMonoid Mᵃᵒᵖ], DomAddAct.instAddRightCancelMonoidOfAddOpposite = inst
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceDeclarationParams : Lean.Lsp.FileSource Lean.Lsp.DeclarationParams
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivWithinAt_pi'' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} {F' : ι → Type u_7}
  [inst_3 : (i : ι) → NormedAddCommGroup (F' i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i}
  {Φ' : E →L[𝕜] (i : ι) → F' i},
  (∀ (i : ι), HasFDerivWithinAt (fun x => Φ x i) (ContinuousLinearMap.proj i ∘SL Φ') s x) → HasFDerivWithinAt Φ Φ' s x
-- Mathlib.CategoryTheory.Monad.Equalizer
/-- The fork constructed is a limit. This shows that any coalgebra is a (coreflexive) equalizer of
cofree coalgebras.
 -/
CategoryTheory.Comonad.beckCoalgebraEqualizer : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Comonad C} →
      (X : T.Coalgebra) → CategoryTheory.Limits.IsLimit (CategoryTheory.Comonad.beckCoalgebraFork X)
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
Order.enum.congr_simp : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [inst_2 : IsRegularCardinalOrder α] (s : Set α)
  (hs : IsCofinal s), Order.enum s hs = Order.enum s hs
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Polynomial.contentIdeal_zero : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.contentIdeal 0 = ⊥
-- Mathlib.Control.Traversable.Instances
List.mem_traverse : ∀ {α' β' : Type u} {f : α' → Set β'} (l : List α') (n : List β'),
  n ∈ traverse f l ↔ List.Forall₂ (fun b a => b ∈ f a) n l
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isNClique_empty : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ}, G.IsNClique n ∅ ↔ n = 0
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.opHom_obj : ∀ (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.Functor.opHom C D).obj F = (Opposite.unop F).op
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iInter₂_sub_subset : ∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Sub α] (s : (i : ι) → κ i → Set α) (t : Set α),
  (⋂ i, ⋂ j, s i j) - t ⊆ ⋂ i, ⋂ j, s i j - t
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The restriction of `Spec.map f` to a basic open `D(r)` is isomorphic to `Spec.map` of the
localization of `f` away from `r`.  -/
AlgebraicGeometry.SpecMapRestrictBasicOpenIso : {R S : CommRingCat} →
  (f : R ⟶ S) →
    (r : ↑R) →
      CategoryTheory.Arrow.mk (AlgebraicGeometry.Spec.map f ∣_ PrimeSpectrum.basicOpen r) ≅
        CategoryTheory.Arrow.mk
          (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
_private.Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence.0.ContinuousLinearMap.diagonalStrongDualProd_apply : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ}
  {L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ} (x y : StrongDual ℝ (E × F)),
  ((ContinuousLinearMap.diagonalStrongDualProd✝ L₁ L₂) x) y =
    (L₁ (x ∘SL ContinuousLinearMap.inl ℝ E F)) (y ∘SL ContinuousLinearMap.inl ℝ E F) +
      (L₂ (x ∘SL ContinuousLinearMap.inr ℝ E F)) (y ∘SL ContinuousLinearMap.inr ℝ E F)
-- Init.Data.List.Nat.Modify
List.getElem_modify_ne : ∀ {α : Type u_1} (f : α → α) {i j : ℕ} (l : List α),
  i ≠ j → ∀ (h' : j < (l.modify i f).length), (l.modify i f)[j] = l[j]
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.XXIsoOfEq_inv_ιTotal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  {x₁ y₁ : I₁} (h₁ : x₁ = y₁) {x₂ y₂ : I₂} (h₂ : x₂ = y₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.XXIsoOfEq C c₁ c₂ K h₁ h₂).inv (K.ιTotal c₁₂ x₁ x₂ i₁₂ h) =
    K.ιTotal c₁₂ y₁ y₂ i₁₂ ⋯
-- Mathlib.Algebra.Group.Hom.Basic
OneHom.coe_mul : ∀ {M : Type u_8} {N : Type u_9} [inst : One M] [inst_1 : MulOneClass N] (f g : OneHom M N), ⇑(f * g) = ⇑f * ⇑g
-- Mathlib.CategoryTheory.MorphismProperty.Retract
CategoryTheory.MorphismProperty.IsStableUnderRetracts.monomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.MorphismProperty.monomorphisms C).IsStableUnderRetracts
-- Mathlib.Topology.Algebra.Monoid
AddSubsemigroup.addCommSemigroupTopologicalClosure.eq_1 : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddSemigroup M] [inst_2 : SeparatelyContinuousAdd M]
  [inst_3 : T2Space M] (s : AddSubsemigroup M) (hs : ∀ (x y : ↥s), x + y = y + x),
  s.addCommSemigroupTopologicalClosure hs =
    { toAddSemigroup := AddMemClass.toAddSemigroup s.topologicalClosure, add_comm := ⋯ }
-- Mathlib.Order.Filter.Defs
Filter.mem_sdiff : ∀ {α : Type u_1} {f g : Filter α} {s : Set α}, s ∈ f \ g ↔ ∀ t ∈ g, s ⊆ t → t ∈ f
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.restrictIndexHom_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {ι : Type w'}
  (f : ι → E.I₀) (x : (E.restrictIndex f).I₀),
  (E.restrictIndexHom f).h₀ x = CategoryTheory.CategoryStruct.id ((E.restrictIndex f).X x)
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
CategoryTheory.Sheaf.instAdditiveAddCommGrpCatFunctorH : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (n : ℕ),
  (CategoryTheory.Sheaf.functorH J n).Additive
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_vadd_set : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] (s : Set α) (t : Set β), ⋃ a ∈ s, a +ᵥ t = s +ᵥ t
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.isIso_ι_of_isInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {j : J} (I : CategoryTheory.Limits.IsInitial j) (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasColimit F] [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)],
  CategoryTheory.IsIso (CategoryTheory.Limits.colimit.ι F j)
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
/-- Almost sure convergence implies convergence in distribution.  -/
MeasureTheory.tendstoInDistribution_of_ae_tendsto : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {m' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'}
  [inst : MeasureTheory.IsProbabilityMeasure μ'] {mE : MeasurableSpace E} {Z : Ω' → E} {l : Filter ι}
  [inst_1 : TopologicalSpace E] [l.IsCountablyGenerated] [inst_3 : OpensMeasurableSpace E] {X : ι → Ω' → E},
  (∀ (i : ι), AEMeasurable (X i) μ') →
    AEMeasurable Z μ' →
      (∀ᵐ (ω : Ω') ∂μ', Filter.Tendsto (fun i => X i ω) l (nhds (Z ω))) →
        MeasureTheory.TendstoInDistribution X l Z (fun x => μ') μ'
-- Lean.DocString.Syntax
/-- Literal code.

Code may begin with any non-zero number of backticks. It must be terminated with the same number,
and it may not contain a sequence of backticks that is at least as long as its starting or ending
delimiters.

If the first and last characters are space, and it contains at least one non-space character, then
the resulting string has a single space stripped from each end. Thus, ``` `` `x `` ``` represents
``"`x"``, not ``" `x "``.
 -/
Lean.Doc.Syntax.code : Lean.ParserDescr
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
/-- The `q`-expansion of `E2` as a `HasSum` over `ℕ`.  -/
EisensteinSeries.hasSum_qExpansion_E2 : ∀ (z : UpperHalfPlane),
  HasSum
    (fun m =>
      (if m = 0 then 1 else -24 * ↑((ArithmeticFunction.sigma 1) m)) • Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ m)
    (EisensteinSeries.E2 z)
-- Mathlib.Order.TypeTags
/-- Attach `⊤` to a type.  -/
WithTop : Type u_2 → Type u_2
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_fst : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g),
  CategoryTheory.CategoryStruct.comp T.SpecTensorTo (CategoryTheory.Limits.pullback.fst f g) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInl) (X.fromSpecResidueField T.x)
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.instInhabited : {Ω : Type u_1} →
  {ι : Type u_2} → {m : MeasurableSpace Ω} → [inst : Preorder ι] → Inhabited (MeasureTheory.Filtration ι m)
-- Mathlib.NumberTheory.Fermat
Nat.fermatNumber_ne_one : ∀ (n : ℕ), n.fermatNumber ≠ 1
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Every cofork is isomorphic to one of the form `Cofork.ofπ _ _`.  -/
CategoryTheory.Limits.Cofork.isoCoforkOfπ : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} → (c : CategoryTheory.Limits.Cofork f g) → c ≅ CategoryTheory.Limits.Cofork.ofπ c.π ⋯
-- Mathlib.Topology.Category.TopCat.GrothendieckTopology
TopCat.instIsContinuousUliftFunctorGrothendieckTopology : TopCat.uliftFunctor.IsContinuous TopCat.grothendieckTopology TopCat.grothendieckTopology
-- Mathlib.NumberTheory.Modular
ModularGroup.isOpen_fdo : IsOpen ModularGroup.fdo
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Certify the upper-tail sum in one `BirdDet.stepEntry` application:

```
sumFrom n (i + 1) fun k => (stepEntry n A)^[t] F i k * get n A k j
```
 -/
Mathlib.Tactic.Determinant.certTail : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} → ℕ → ℕ → ℕ → ℕ → Mathlib.Tactic.Determinant.CertM rα (Mathlib.Tactic.Determinant.Cert rα)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.instConditionallyCompleteLinearOrderBot : ConditionallyCompleteLinearOrderBot Ordinal.{u_1}
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instExistsAddOfLE : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : Add β] [inst_1 : LE β] [ExistsAddOfLE β],
  ExistsAddOfLE (l.Germ β)
-- Mathlib.SetTheory.Ordinal.Notation
NONote.NF : ∀ (o : NONote), (↑o).NF
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.mem_sup_left : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {S T : Submodule R M} {x : M}, x ∈ S → x ∈ S ⊔ T
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.isGroupLikeElem_single_one : ∀ {R : Type u_1} {A : Type u_3} {G : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  (g : G), IsGroupLikeElem R (AddMonoidAlgebra.single g 1)
-- Init.Data.Format.Basic
/-- A representation of a set of strings, in which the placement of newlines and indentation differ.

Given a specific line width, specified in columns, the string that uses the fewest lines can be
selected.

The pretty-printing algorithm is based on Wadler's paper
[_A Prettier Printer_](https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf).
 -/
Std.Format : Type
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_ite_of_true : ∀ {ι : Type u_1} {M : Type u_3} {s : Finset ι} [inst : AddCommMonoid M] {p : ι → Prop} [inst_1 : DecidablePred p],
  (∀ x ∈ s, p x) → ∀ (f g : ι → M), (∑ x ∈ s, if p x then f x else g x) = ∑ x ∈ s, f x
-- Mathlib.RingTheory.Jacobson.Radical
Ring.jacobson_quotient_jacobson : ∀ (R : Type u_1) [inst : Ring R], Ring.jacobson (R ⧸ Ring.jacobson R) = ⊥
-- Init.Data.List.ToArray
Array.prod.eq_1 : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] (as : Array α), as.prod = Array.foldr (fun x1 x2 => x1 * x2) 1 as
-- Init.Data.Array.Lemmas
Array.getElem?_set : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.size) {v : α} {j : ℕ},
  (xs.set i v h)[j]? = if i = j then some v else xs[j]?
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable f μ → (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ) → 0 ≤ᵐ[μ] f
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.iCyclesNatTrans_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  (S : CategoryTheory.ShortComplex C), (CategoryTheory.ShortComplex.iCyclesNatTrans C).app S = S.iCycles
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.isoInv_hom_id_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory}
  (e : X ≅ Y), CategoryTheory.CategoryStruct.comp e.inv.hom e.hom.hom = CategoryTheory.CategoryStruct.id Y.obj
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.fg_of_fg_toSubalgebra : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : IntermediateField F E),
  S.FG → S.FG
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.lift_symm_apply_coe : ∀ {R : Type u_2} {a b : R} [inst : CommSemiring R] {A : Type u_3} [inst_1 : Ring A] [inst_2 : Algebra R A]
  (f : QuadraticAlgebra R a b →ₐ[R] A), ↑(QuadraticAlgebra.lift.symm f) = f QuadraticAlgebra.omega
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      (src tgt : C) → CategoryTheory.Subobject (src ⨯ tgt) → CategoryTheory.Dial C
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Adjunction.strongEpi_map_of_isEquivalence : ∀ {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] {F : CategoryTheory.Functor C D} {A B : C} [F.IsEquivalence]
  (f : A ⟶ B) [_h : CategoryTheory.StrongEpi f], CategoryTheory.StrongEpi (F.map f)
-- Mathlib.Topology.Instances.EReal.Lemmas
ContinuousOn.ereal_toENNReal : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s : Set α} {f : α → EReal},
  ContinuousOn f s → ContinuousOn (fun x => (f x).toENNReal) s
-- Mathlib.Data.EReal.Basic
EReal.forall : ∀ {p : EReal → Prop}, (∀ (r : EReal), p r) ↔ p ⊥ ∧ p ⊤ ∧ ∀ (r : ℝ), p ↑r
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.LaxTrans.associator_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H I : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B),
  (CategoryTheory.Lax.LaxTrans.associator η θ ι).hom.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.collect : Lean.Syntax → Lean.Elab.Term.CollectPatternVars.M Lean.Syntax
-- Mathlib.Order.Category.PartOrd
PartOrd.coe_of : ∀ (X : Type u) [inst : PartialOrder X], ↑{ carrier := X, str := inst } = X
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.left.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (a a_1 : C), (CategoryTheory.Join.left a = CategoryTheory.Join.left a_1) = (a = a_1)
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- The relation on `FreeAddMonoid (M × N)` that generates a congruence whose quotient is
the tensor product.  -/
TensorProduct.Eqv : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_7) →
      (N : Type u_8) →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [Module R M] → [Module R N] → FreeAddMonoid (M × N) → FreeAddMonoid (M × N) → Prop
-- Mathlib.Geometry.Convex.Set
Convexity.subtypeVal_convexCombPair : ∀ {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) (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b)
  (hab : a + b = 1) (x y : ↑s),
  ↑(Convexity.convexCombPair a b ha hb hab x y) = Convexity.convexCombPair a b ha hb hab ↑x ↑y
-- Init.Data.Nat.Lemmas
/-- Tail-recursive `Bool` loop: `true` iff `f i h` holds for every `i < n`
(short-circuits on the first `false`). Used at runtime by `decidableBallLT` via `@[csimp]`.  -/
Nat.allLTTR : (n : ℕ) → ((i : ℕ) → i < n → Bool) → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace_index : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) [inst : h.IsProper] (s : h.ι), ⋯.index ⋯ = h.index s
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toList_rcc : ∀ {m n fallback : ℤ} {i : ℕ}, (m...=n).toList.getD i fallback = if i < (n + 1 - m).toNat then m + ↑i else fallback
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPosAssignment.eq_2 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg.addPosAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both
-- Mathlib.Condensed.Light.Monoidal
LightCondensed.instSymmetricCategoryLightCondMod : (R : Type u) → [inst : CommRing R] → CategoryTheory.SymmetricCategory (LightCondMod R)
-- Mathlib.Data.DFinsupp.Multiset
DFinsupp.toMultiset_lt_toMultiset : ∀ {α : Type u_1} [inst : DecidableEq α] {f g : Π₀ (_a : α), ℕ}, DFinsupp.toMultiset f < DFinsupp.toMultiset g ↔ f < g
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.hom_ext_iff : ∀ {X Y : CommGrpCat} {f g : X ⟶ Y}, f = g ↔ CommGrpCat.Hom.hom f = CommGrpCat.Hom.hom g
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instCommMonoid : {α : Type u_1} → [inst : CommGroup α] → [inst_1 : Preorder α] → [IsOrderedMonoid α] → CommMonoid (LowerSet α)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instVAddCommClass : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : VAdd M X] [inst_2 : ContinuousConstVAdd M X]
  {N : Type u_3} [inst_3 : VAdd N X] [inst_4 : ContinuousConstVAdd N X] [VAddCommClass M N X],
  VAddCommClass M N (SeparationQuotient X)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → ∀ {fallback : α}, t.getKeyD t.maxKey! fallback = t.maxKey!
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y}
  [inst_2 : CategoryTheory.IsSplitMono f] {c : CategoryTheory.Limits.CokernelCofork f}
  (i : CategoryTheory.Limits.IsColimit c), (CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).inl = f
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.min!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t₁.Equiv t₂ → t₁.min! = t₂.min!
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instSub : {α : Type u_1} → [inst : AddCommGroup α] → [inst_1 : Preorder α] → [IsOrderedAddMonoid α] → Sub (UpperSet α)