mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Quiver.Arborescence
/-- The length of a path is at least the length of the shortest path  -/
Quiver.shortest_path_spec : ∀ {V : Type u} [inst : Quiver V] (r : V) [inst_1 : Quiver.RootedConnected r] {a : V} (p : Quiver.Path r a),
  (Quiver.shortestPath r a).length ≤ p.length
-- Mathlib.MeasureTheory.Group.Measure
/-- A convenience wrapper for `MeasureTheory.Measure.isHaarMeasure_map`.
 -/
ContinuousMulEquiv.isHaarMeasure_map : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [BorelSpace G] [IsTopologicalGroup G] {H : Type u_3}
  [inst_6 : Group H] [inst_7 : TopologicalSpace H] [inst_8 : MeasurableSpace H] [BorelSpace H] [IsTopologicalGroup H]
  (e : G ≃ₜ* H), (MeasureTheory.Measure.map (⇑e) μ).IsHaarMeasure
-- Init.Data.Range.Polymorphic.IntLemmas
Int.isSome_getElem?_toList_roo_eq : ∀ {m n : ℤ} {i : ℕ}, ((m<...n).toList[i]?.isSome = true) = (i < (n - (m + 1)).toNat)
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommSum_cons : ∀ {α : Type u_3} [inst : AddMonoid α] (s : Multiset α) (a : α) (comm : {x | x ∈ a ::ₘ s}.Pairwise AddCommute),
  (a ::ₘ s).noncommSum comm = a + s.noncommSum ⋯
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
quadraticCharFun_zero : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F], quadraticCharFun F 0 = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.unitOfList_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {k : α}, Std.TreeMap.Raw.unitOfList [k] cmp = ∅.insertIfNew k ()
-- Init.Data.Iterators.Basic
Std.IterM.TerminationMeasures.Productive.mk.sizeOf_spec : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] [inst_1 : SizeOf α]
  [inst_2 : (a : Type w) → SizeOf (m a)] [inst_3 : SizeOf β] (it : Std.IterM m β), sizeOf { it := it } = 1 + sizeOf it
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists'.ofList.match_1.splitter : {α : Type u_1} →
  (motive : List (Lists α) → Sort u_2) →
    (x : List (Lists α)) → (Unit → motive []) → ((a : Lists α) → (l : List (Lists α)) → motive (a :: l)) → motive x
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_40 : HSub Std.Time.Week.Offset Std.Time.Hour.Offset Std.Time.Hour.Offset
-- Mathlib.Algebra.Order.Module.Defs
PosMulStrictMono.toPosSMulStrictMono : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Mul α] [inst_2 : Preorder α] [PosMulStrictMono α], PosSMulStrictMono α α
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.ofArrows_of_unique : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} [inst_1 : Unique ι] {Y : ι → C}
  (f : (i : ι) → Y i ⟶ X), CategoryTheory.Presieve.ofArrows Y f = CategoryTheory.Presieve.singleton (f default)
-- Init.Data.Array.Find
Array.find?_flatMap_eq_none_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} {p : β → Bool},
  Array.find? p (Array.flatMap f xs) = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, (!p y) = true
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.binomial_one : ∀ {α : Type u_1} {f : α → ℕ} {a b : α} [inst : DecidableEq α], a ≠ b → f a = 1 → Nat.multinomial {a, b} f = (f b).succ
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.Saturate.below.top : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.Coverage C}
  {motive : (X : C) → (a : CategoryTheory.Sieve X) → K.Saturate X a → Prop} (X : C),
  CategoryTheory.Coverage.Saturate.below ⋯
-- Mathlib.Data.Prod.Lex
/-- Variant of `Prod.Lex.le_iff` for partial orders.  -/
Prod.Lex.le_iff' : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β] {x y : Lex (α × β)},
  x ≤ y ↔ (ofLex x).1 ≤ (ofLex y).1 ∧ ((ofLex x).1 = (ofLex y).1 → (ofLex x).2 ≤ (ofLex y).2)
-- Mathlib.AlgebraicGeometry.Sites.MorphismProperty
/-- The precoverage on `Scheme` induced by `P` is given by jointly surjective families of
`P`-morphisms.  -/
AlgebraicGeometry.Scheme.precoverage : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme → CategoryTheory.Precoverage AlgebraicGeometry.Scheme
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b c : EInt) (hab : a ≤ b)
  (hbc : b ≤ c) (j : C),
  ((t.triangleω₁δ a b c hab hbc).obj j).mor₁ =
    (t.eTruncGE.obj a).map ((t.eTruncLT.map (CategoryTheory.homOfLE hbc)).app j)
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.transIsThetaIsEquivalent : {α : Type u_1} →
  {β : Type u_2} →
    {β₂ : Type u_3} →
      [inst : NormedAddCommGroup β] →
        [inst_1 : Norm β₂] →
          {l : Filter α} → Trans (Asymptotics.IsTheta l) (Asymptotics.IsEquivalent l) (Asymptotics.IsTheta l)
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Extract the isomorphism between
`colim (uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G))` and
`(G.obj (colim K₁)).obj (colim K₂)` from a `PreservesColimit₂` instance, provided the relevant
colimits exist.  -/
CategoryTheory.Limits.PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ : {J₁ : Type u_1} →
  {J₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] →
        {C₁ : Type u_3} →
          {C₂ : Type u_4} →
            {C : Type u_5} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] →
                    (K₁ : CategoryTheory.Functor J₁ C₁) →
                      (K₂ : CategoryTheory.Functor J₂ C₂) →
                        (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) →
                          [inst_5 : CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G] →
                            [inst_6 : CategoryTheory.Limits.HasColimit K₁] →
                              [inst_7 : CategoryTheory.Limits.HasColimit K₂] →
                                CategoryTheory.Limits.colimit
                                    (CategoryTheory.Functor.uncurry.obj
                                      ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) ≅
                                  (G.obj (CategoryTheory.Limits.colimit K₁)).obj (CategoryTheory.Limits.colimit K₂)
-- Init.Data.UInt.Lemmas
USize.ofInt_neg : ∀ (x : ℤ), USize.ofInt (-x) = -USize.ofInt x
-- Mathlib.CategoryTheory.GradedObject
/-- The projection of a graded object to its `i`-th component.  -/
CategoryTheory.GradedObject.eval : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {β : Type w} → β → CategoryTheory.Functor (CategoryTheory.GradedObject β C) C
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.BuiltinSimprocs.keys : Lean.Meta.Simp.BuiltinSimprocs → Std.HashMap Lean.Name (Array Lean.Meta.SimpTheoremKey)
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
tangentBundleCore_indexAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_6)
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (x : M),
  (tangentBundleCore I M).indexAt x = achart H x
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.Hom.stalkMap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  {X Y : AlgebraicGeometry.PresheafedSpace C} (α : X.Hom Y) (x : ↑↑X),
  α.stalkMap x =
    CategoryTheory.CategoryStruct.comp
      ((TopCat.Presheaf.stalkFunctor C ((CategoryTheory.ConcreteCategory.hom α.base) x)).map α.c)
      (TopCat.Presheaf.stalkPushforward C α.base X.presheaf x)
-- Mathlib.Data.Fin.FlagRange
Flag.rangeFin_carrier : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {n : ℕ} (f : Fin (n + 1) → α) (h0 : f 0 = ⊥)
  (hlast : f (Fin.last n) = ⊤) (hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ),
  ↑(Flag.rangeFin f h0 hlast hcovBy) = Set.range f
-- Mathlib.Data.Complex.Basic
Complex.normSq_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], Complex.normSq (OfNat.ofNat n) = OfNat.ofNat n * OfNat.ofNat n
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.FunIndInfo.funName : Lean.Meta.FunIndInfo → Lean.Name
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.takeWhile_go_succ : ∀ {α : Type u_1} {r : Array α} (p : α → Bool) (a : α) (l : List α) (i : ℕ),
  Array.takeWhile.go✝ p (a :: l).toArray (i + 1) r = Array.takeWhile.go✝ p l.toArray i r
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X)
  (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex),
  CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f →
    ∀ (F : CategoryTheory.Functor C D) [inst_5 : F.Additive],
      CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).inv
          (F.leftDerivedToHomotopyCategory.map f) =
        CategoryTheory.CategoryStruct.comp
          (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp
                (HomotopyCategory.quotient D (ComplexShape.down ℕ))).map
            φ)
          (Q.isoLeftDerivedToHomotopyCategoryObj F).inv
-- Lean.LocalContext
Lean.LocalDecl.cdecl.inj : ∀ {index : ℕ} {fvarId : Lean.FVarId} {userName : Lean.Name} {type : Lean.Expr} {bi : Lean.BinderInfo}
  {kind : Lean.LocalDeclKind} {index_1 : ℕ} {fvarId_1 : Lean.FVarId} {userName_1 : Lean.Name} {type_1 : Lean.Expr}
  {bi_1 : Lean.BinderInfo} {kind_1 : Lean.LocalDeclKind},
  Lean.LocalDecl.cdecl index fvarId userName type bi kind =
      Lean.LocalDecl.cdecl index_1 fvarId_1 userName_1 type_1 bi_1 kind_1 →
    index = index_1 ∧ fvarId = fvarId_1 ∧ userName = userName_1 ∧ type = type_1 ∧ bi = bi_1 ∧ kind = kind_1
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.cases.inj : ∀ {target : Aesop.CasesTarget} {md : Lean.Meta.TransparencyMode} {isRecursiveType : Bool}
  {ctorNames : Array Aesop.CtorNames} {target_1 : Aesop.CasesTarget} {md_1 : Lean.Meta.TransparencyMode}
  {isRecursiveType_1 : Bool} {ctorNames_1 : Array Aesop.CtorNames},
  Aesop.RuleTacDescr.cases target md isRecursiveType ctorNames =
      Aesop.RuleTacDescr.cases target_1 md_1 isRecursiveType_1 ctorNames_1 →
    target = target_1 ∧ md = md_1 ∧ isRecursiveType = isRecursiveType_1 ∧ ctorNames = ctorNames_1
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.addMonoidHomCongrRightEquiv.eq_1 : ∀ {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [inst : AddZeroClass M] [inst_1 : AddMonoid N₁]
  [inst_2 : AddMonoid N₂] (e : N₁ ≃+ N₂),
  e.addMonoidHomCongrRightEquiv =
    { toFun := e.toAddMonoidHom.comp, invFun := e.symm.toAddMonoidHom.comp, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Module.Presentation.DirectSum
Module.Relations.Solution.directSumEquiv_symm_apply_var : ∀ {A : Type u} [inst : Ring A] {ι : Type w} {relations : ι → Module.Relations A} {N : Type v} [inst_1 : AddCommGroup N]
  [inst_2 : Module A N] (t : (i : ι) → (relations i).Solution N) (x : (Module.Relations.directSum relations).G),
  (Module.Relations.Solution.directSumEquiv.symm t).var x =
    match x with
    | ⟨i, g⟩ => (t i).var g
-- Lean.Elab.Command.Scope
/-- The current namespace. The top-level namespace is represented by `Name.anonymous`.  -/
Lean.Elab.Command.Scope.currNamespace : Lean.Elab.Command.Scope → Lean.Name
-- Mathlib.Topology.Algebra.Module.Star
StarModule.decomposeProdAdjointL_symm_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2] [inst_8 : TopologicalSpace A] [inst_9 : IsTopologicalAddGroup A] [inst_10 : ContinuousStar A]
  [inst_11 : ContinuousConstSMul R A] (a : ↥(selfAdjoint A) × ↥(skewAdjoint A)),
  (StarModule.decomposeProdAdjointL R A).symm a =
    (selfAdjoint.submodule R A).subtype a.1 + (skewAdjoint.submodule R A).subtype a.2
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) (y : ↥Y) (z : ↑(Y.presheaf.stalk (e.hom (e.inv y)))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap e.inv y))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap e.hom (e.inv y))) z) =
    (CategoryTheory.ConcreteCategory.hom (Y.presheaf.stalkCongr ⋯).hom) z
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_of_mem_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β}, a ∈ m.insert k v → (k == a) = false → a ∈ m
-- Mathlib.Probability.IdentDistribIndep
/-- If `X` and `Y` are independent random variables on `Ω`, `Z` and `W` are independent random
variables on `Ω'`, such that `X` and `Z` are identically distributed and `Y` and `W` are identically
distributed, then the pairs `(X, Y)`  and `(Z, W)` are identically distributed.  -/
ProbabilityTheory.IdentDistrib.prodMk : ∀ {Ω : Type u_1} {Ω' : Type u_2} {E : Type u_4} {F : Type u_5} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
  {mE : MeasurableSpace E} {mF : MeasurableSpace F} {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'}
  [MeasureTheory.IsFiniteMeasure μ] {X : Ω → E} {Y : Ω → F} {Z : Ω' → E} {W : Ω' → F},
  ProbabilityTheory.IdentDistrib X Z μ ν →
    ProbabilityTheory.IdentDistrib Y W μ ν →
      ProbabilityTheory.IndepFun X Y μ →
        ProbabilityTheory.IndepFun Z W ν →
          ProbabilityTheory.IdentDistrib (fun ω => (X ω, Y ω)) (fun ω' => (Z ω', W ω')) μ ν
-- Mathlib.Algebra.QuadraticDiscriminant
/-- If a polynomial of degree 2 is always positive, then its discriminant is negative,
at least when the coefficient of the quadratic term is nonzero.
 -/
discrim_lt_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {a b c : K},
  a ≠ 0 → (∀ (x : K), 0 < a * (x * x) + b * x + c) → discrim a b c < 0
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.toIso_inv_ι : ∀ (X : AlgebraicGeometry.Scheme),
  CategoryTheory.CategoryStruct.comp X.topIso.inv ⊤.ι = CategoryTheory.CategoryStruct.id X
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderCoproducts.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C},
  autoParam (∀ (J : Type w), W.IsStableUnderCoproductsOfShape J)
      CategoryTheory.MorphismProperty.IsStableUnderCoproducts.isStableUnderCoproductsOfShape._autoParam →
    CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{w, v, u} W
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- The Haar measure is regular.  -/
MeasureTheory.Measure.regular_haarMeasure : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G},
  (MeasureTheory.Measure.haarMeasure K₀).Regular
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.bounds_nonempty : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F},
  ∃ c, c ∈ {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖}
-- Mathlib.Topology.Algebra.ConstMulAction
IsUnit.tendsto_const_smul_iff : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [ContinuousConstSMul M α] {f : β → α} {l : Filter β} {a : α} {c : M},
  IsUnit c → (Filter.Tendsto (fun x => c • f x) l (nhds (c • a)) ↔ Filter.Tendsto f l (nhds a))
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.map_nil : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V},
  SimpleGraph.Walk.map f SimpleGraph.Walk.nil = SimpleGraph.Walk.nil
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.instIsLeftAdjointSheafSheafFiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A], Φ.sheafFiber.IsLeftAdjoint
-- Mathlib.Algebra.Group.ULift
ULift.commMonoid : {α : Type u} → [CommMonoid α] → CommMonoid (ULift.{u_1, u} α)
-- Mathlib.Dynamics.BirkhoffSum.Basic
birkhoffSum.eq_1 : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (f : α → α) (g : α → M) (n : ℕ) (x : α),
  birkhoffSum f g n x = ∑ k ∈ Finset.range n, g (f^[k] x)
-- Init.Data.List.Sort.Basic
/-- Given an ordering relation `le : α → α → Bool`,
construct the lexicographic ordering on `α × Nat`.
which first compares the first components using `le`,
but if these are equivalent (in the sense `le a.2 b.2 && le b.2 a.2`)
then compares the second components using `≤`.

This function is only used in stating the stability properties of `mergeSort`.
 -/
List.zipIdxLE : {α : Type u_1} → (α → α → Bool) → α × ℕ → α × ℕ → Bool
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
CategoryTheory.InjectiveResolution.instIsStrictlyGECochainComplexOfNatInt_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.InjectiveResolution X),
  R.cochainComplex.IsStrictlyGE 0
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
/-- If `M` is square and has nonzero determinant, then `M` as a bilinear form on `n → R` is
nondegenerate. The "iff" implication, `nondegenerate_iff_det_ne_zero`, is proved in a later file.

See also `BilinForm.nondegenerateOfDetNeZero'` and `BilinForm.nondegenerateOfDetNeZero`.
 -/
Matrix.nondegenerate_of_det_ne_zero : ∀ {m : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : Fintype m] [inst_2 : DecidableEq m] {M : Matrix m m R}
  [NoZeroDivisors R], M.det ≠ 0 → M.Nondegenerate
-- Mathlib.Algebra.Order.ZeroLEOne
ZeroLEOneClass.factZeroLtOne : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1], Fact (0 < 1)
-- Mathlib.Analysis.Normed.Module.Basic
/-- A structure encapsulating minimal axioms needed to defined a seminormed vector space, as found
in textbooks. This is meant to be used to easily define `SeminormedSpace E` instances from
scratch on a type with no preexisting distance or topology.  -/
SeminormedSpace.Core : (𝕜 : Type u_6) → (E : Type u_7) → [inst : NormedField 𝕜] → [inst_1 : AddCommGroup E] → [Norm E] → [Module 𝕜 E] → Prop
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.integrable : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {m : MeasurableSpace E} [OpensMeasurableSpace E]
  {μ : MeasureTheory.Measure E} [μ_finite : MeasureTheory.IsFiniteMeasure (μ.restrict ↑K)]
  (f : ContDiffMapSupportedIn E F n K), MeasureTheory.Integrable (⇑f) μ
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.max_ult' : ∀ {w : ℕ} (a : BitVec w), (-1#w).ult a = false
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.compLeft_h₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (ψ : S₃ ⟶ S₁), (h.compLeft ψ).h₂ = CategoryTheory.CategoryStruct.comp ψ.τ₃ h.h₂
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.instInhabitedIndGroupInst.default : Lean.Elab.Structural.IndGroupInst
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.instIsProbabilityMeasureForallInfinitePiNat : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → MeasureTheory.Measure (X n))
  [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)],
  MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.infinitePiNat μ)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- `Set α` is a `CommSemigroup` under pointwise operations if `α` is.  -/
Set.commSemigroup : {α : Type u_2} → [CommSemigroup α] → CommSemigroup (Set α)
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- If `b` is odd, then `J(-2 | b)` is given by `χ₈' b`.  -/
jacobiSym.at_neg_two : ∀ {b : ℕ}, Odd b → jacobiSym (-2) b = ZMod.χ₈' ↑b
-- Mathlib.MeasureTheory.Measure.Hausdorff
Isometry.map_hausdorffMeasure : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
  [inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] {f : X → Y} {d : ℝ},
  Isometry f →
    0 ≤ d ∨ Function.Surjective f →
      MeasureTheory.Measure.map f (MeasureTheory.Measure.hausdorffMeasure d) =
        (MeasureTheory.Measure.hausdorffMeasure d).restrict (Set.range f)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.symm_apply_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁), e.symm (e x) = x
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.mem_dilatransvections_iff_rank_quotient : ∀ {V : Type u_2} [inst : AddCommGroup V] {K : Type u_3} [inst_1 : DivisionRing K] [inst_2 : Module K V] {e : V ≃ₗ[K] V},
  e ∈ LinearEquiv.dilatransvections K V ↔ Module.rank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
-- Lean.Meta.Structure
/-- Given an expression `e` that's either a native projection or a registered projection
function, gives the object being projected.
Checks that the parameters are defeq to `params`, that the projection index is equal to `idx`,
and, if `x?` is provided, that the object being projected is equal to it.
 -/
_private.Lean.Meta.Structure.0.Lean.Meta.etaStruct?.getProjectedExpr : Lean.Name → Lean.Name → Array Lean.Expr → ℕ → Lean.Expr → Option Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Init.Data.Vector.Monadic
Vector.findSomeM?_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] [LawfulMonad m] {f : α → Option β}
  {xs : Vector α n}, Vector.findSomeM? (fun x => pure (f x)) xs = pure (Vector.findSome? f xs)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_erase : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k a : α}, (m.erase k).contains a = (!k == a && m.contains a)
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_uIcc_castSucc : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∑ i ∈ Finset.uIcc a.castSucc b.castSucc, f i = ∑ i ∈ Finset.uIcc a b, f i.castSucc