mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.commMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : One M₁] [inst_2 : Pow M₁ ℕ] [inst_3 : CommMonoid M₂]
  (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y)
  (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n),
  Function.Injective.commMonoid f hf one mul npow =
    { toMonoid := Function.Injective.monoid f hf one mul npow, mul_comm := ⋯ }
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.hasSum_lt : ∀ {α : Type u_1} {f g : α → ENNReal} {sf sg : ENNReal} {i : α},
  (∀ (a : α), f a ≤ g a) → f i < g i → sf ≠ ⊤ → HasSum f sf → HasSum g sg → sf < sg
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.smul_apply : ∀ {ι : Type u_1} {α : Type u_2} {M : ι → Type u_5} [inst : (i : ι) → SMul α (M i)] (a : α) (f : (i : ι) → M i) (i : ι),
  (a • f) i = a • f i
-- Mathlib.Order.Filter.Prod
Filter.NeBot.prod : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, f.NeBot → g.NeBot → (f ×ˢ g).NeBot
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.instDivInvMonoid : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : DivisionRing β] →
            {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → DivInvMonoid (CauSeq.Completion.Cauchy abv)
-- Mathlib.LinearAlgebra.Prod
/-- `LinearMap.prodMap` as an `AlgHom`  -/
LinearMap.prodMapAlgHom : (R : Type u) →
  (M : Type v) →
    (M₂ : Type w) →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M] →
              [inst_4 : Module R M₂] → Module.End R M × Module.End R M₂ →ₐ[R] Module.End R (M × M₂)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesMap_opcyclesIso_hom_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃')
  (γ : CategoryTheory.ComposableArrows.mk₂ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₂ f₂' f₃'),
  autoParam (γ = CategoryTheory.ComposableArrows.homMk₂ (α.app 1) (α.app 2) (α.app 3) ⋯ ⋯)
      CategoryTheory.Abelian.SpectralObject.opcyclesMap_opcyclesIso_hom._auto_1 →
    ∀ (n₀ n₁ n₂ : ℤ)
      (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.opcyclesMap_opcyclesIso_hom._auto_3)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.opcyclesMap_opcyclesIso_hom._auto_5) {Z : C}
      (h : X.opcycles f₂' f₃' n₁ ⟶ Z),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.ShortComplex.opcyclesMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂))
          (CategoryTheory.CategoryStruct.comp (X.opcyclesIso f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂).hom h) =
        CategoryTheory.CategoryStruct.comp (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom
          (CategoryTheory.CategoryStruct.comp (X.opcyclesMap f₂ f₃ f₂' f₃' γ n₁) h)
-- Lean.Meta.NatInstTesters
Lean.Meta.Structural.isInstAddNat : Lean.Expr → Lean.MetaM Bool
-- Init.Data.SInt.Lemmas
ISize.le_total : ∀ (a b : ISize), a ≤ b ∨ b ≤ a
-- Init.Data.BitVec.Lemmas
BitVec.ofBoolListBE.eq_1 : BitVec.ofBoolListBE [] = 0#0
-- Lean.Parser.Basic
Lean.Parser.orelseFnCore : Lean.Parser.ParserFn →
  Lean.Parser.ParserFn →
    optParam Lean.Parser.OrElseOnAntiquotBehavior Lean.Parser.OrElseOnAntiquotBehavior.merge → Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The morphisms in the constructed localized category for a morphism property `W`
that has left calculus of fractions are equivalence classes of left fractions.  -/
CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.MorphismProperty C → C → C → Type (max u_1 v_1)
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.integral_map_cast_binomial : ∀ {R : Type u_1} [inst : MeasurableSpace R] [inst_1 : AddMonoidWithOne R] {n : ℕ} {p : ↑unitInterval} {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [CompleteSpace E] [MeasurableSingletonClass R] (f : R → E),
  ∫ (x : R), f x ∂MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p) =
    ∑ k ≤ n, (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • f ↑k
-- Mathlib.Algebra.Algebra.Prod
/-- Multiplying by the trivial algebra from the left does not change the structure.
This is the `AlgEquiv` version of `LinearEquiv.uniqueProd` and `RingEquiv.zeroRingProd.symm`.
 -/
AlgEquiv.uniqueProd : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] → [inst_3 : Semiring B] → [inst_4 : Algebra R B] → [Unique B] → (B × A) ≃ₐ[R] A
-- Mathlib.Algebra.Module.Submodule.Map
/-- The `LinearMap` from the preimage of a submodule to itself.

This is the linear version of `AddMonoidHom.addSubmonoidComap`
and `AddMonoidHom.addSubgroupComap`.  -/
LinearMap.submoduleComap : {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₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {σ₁₂ : R →+* R₂} → (f : M →ₛₗ[σ₁₂] M₂) → (q : Submodule R₂ M₂) → ↥(Submodule.comap f q) →ₛₗ[σ₁₂] ↥q
-- Lean.Meta.Tactic.Grind.MarkAccessible
/-- Mark used by `markAccessible`  -/
_private.Lean.Meta.Tactic.Grind.MarkAccessible.0.Lean.Meta.Grind.grindMark : String
-- Lean.Declaration
Lean.instBEqReducibilityHints.beq : Lean.ReducibilityHints → Lean.ReducibilityHints → Bool
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiable.sub : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {f g : M → E'}, MDiff f → MDiff g → MDiff (f - g)
-- Mathlib.RingTheory.Localization.Defs
/-- For any given denominator `b : M`, the map `a ↦ a / b` is an `AddMonoidHom` from `R` to
`Localization M`.  -/
Localization.mkAddMonoidHom : {R : Type u_1} → [inst : CommSemiring R] → {M : Submonoid R} → ↥M → R →+ Localization M
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- The trailing coefficient of the power of a function is the power of the trailing coefficient.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {n : ℕ} {f : 𝕜 → 𝕜},
  MeromorphicAt f x → meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
-- Mathlib.CategoryTheory.Square
/-- The image of a commutative square by a functor.  -/
CategoryTheory.Square.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        CategoryTheory.Square C → CategoryTheory.Functor C D → CategoryTheory.Square D
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.filterMap_equiv_map : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w} [EquivBEq α]
  [LawfulHashable α] {f : (a : α) → β a → γ a},
  (Std.DHashMap.filterMap (fun k v => some (f k v)) m).Equiv (Std.DHashMap.map f m)
-- Aesop.Search.Expansion.Norm
Aesop.NormStep.simp : Std.HashSet Lean.MVarId → Aesop.NormStep
-- Lean.CoreM
/-- If `diag := true`, different parts of the system collect diagnostics.
Use the `set_option diag true` to set it to true.
 -/
Lean.Core.Context.diag : Lean.Core.Context → Bool
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- The `matcherTy` instantiated with universe levels and the matcher parameters, with a position at the type of
this application prefix.  -/
Lean.PrettyPrinter.Delaborator.AppMatchState.matcherTy : Lean.PrettyPrinter.Delaborator.AppMatchState → Lean.SubExpr
-- Mathlib.Order.Hom.Basic
OrderIso.toRelIsoGT_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β),
  e.symm.toRelIsoGT = e.toRelIsoGT.symm
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryLE.match_3.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (k : α)
  (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.Ordered → (∃ a ∈ x, (compare a k).isLE = true) → Sort u_3)
  (size : ℕ) (ky : α) (y : β ky) (l r : Std.DTreeMap.Internal.Impl α β)
  (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isLE = true)
  (h_1 :
    (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
      (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isLE = true) →
        motive Std.DTreeMap.Internal.Impl.leaf x he)
  (h_2 :
    (size : ℕ) →
      (ky : α) →
        (y : β ky) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isLE = true) →
                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he),
  (match Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => h_1 x he
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he => h_2 size ky y l r ho he) =
    h_2 size ky y l r ho he
-- Std.Time.Time.Unit.Minute
/-- Creates an `Ordinal` from a natural number, ensuring the value is within bounds.
 -/
Std.Time.Minute.Ordinal.ofNat : (data : ℕ) → data ≤ 59 → Std.Time.Minute.Ordinal
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryProductCone_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w))
  (x : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair),
  (CategoryTheory.FunctorToTypes.binaryProductCone F G).π.app x =
    match x.as with
    | CategoryTheory.Limits.WalkingPair.left => CategoryTheory.FunctorToTypes.prod.fst
    | CategoryTheory.Limits.WalkingPair.right => CategoryTheory.FunctorToTypes.prod.snd
-- Mathlib.GroupTheory.QuotientGroup.Defs
Subgroup.orderIsoCon_symm_apply_coe : ∀ {G : Type u_1} [inst : Group G] (c : Con G), ↑((RelIso.symm Subgroup.orderIsoCon) c) = c.subgroup
-- Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
/-- The canonical isomorphism `X ≅ (cosk n).obj X` defined when `X` is coskeletal and the
`n`-coskeleton functor exists.  -/
CategoryTheory.SimplicialObject.isoCoskOfIsCoskeletal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.SimplicialObject C) →
      (n : ℕ) →
        [inst_1 :
            ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
              (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] →
          [X.IsCoskeletal n] → X ≅ (CategoryTheory.SimplicialObject.cosk n).obj X
-- Mathlib.MeasureTheory.Measure.Haar.Extension
/-- If `φ : A →* B` and `ψ : B →* C` define a short exact sequence of topological groups, and if
`ψ` is injective on an open set `U`, then the induced measure on `U` is bounded above by
`μC Set.univ * μA {1}` (possibly infinite).  -/
TopologicalGroup.IsSES.inducedMeasure_lt_of_injOn : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C}
  (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A] [inst_7 : IsTopologicalGroup B]
  [inst_8 : MeasurableSpace A] [inst_9 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure]
  [inst_10 : IsTopologicalGroup C] [inst_11 : LocallyCompactSpace B] [inst_12 : MeasurableSpace C]
  [inst_13 : BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsHaarMeasure] [inst_14 : T2Space B]
  [inst_15 : MeasurableSpace B] [inst_16 : BorelSpace B] {U : Set B},
  IsOpen U → ∀ [DiscreteTopology A], Set.InjOn (⇑ψ) U → (H.inducedMeasure μA μC) U ≤ μC Set.univ * μA {1}
-- Mathlib.Data.Nat.MaxPowDiv
Nat.divMaxPow_one_right : ∀ (n : ℕ), n.divMaxPow 1 = n
-- Std.Data.ExtDTreeMap.Basic
/-- Transforms an array of keys into a tree map.  -/
Std.ExtDTreeMap.Const.unitOfArray : {α : Type u} →
  Array α →
    (cmp : autoParam (α → α → Ordering) Std.ExtDTreeMap.Const.unitOfArray._auto_1) →
      Std.ExtDTreeMap α (fun x => Unit) cmp
-- Mathlib.Algebra.Module.Presentation.Finite
Module.Presentation.finite : ∀ {A : Type u} [inst : Ring A] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module A M]
  (pres : Module.Presentation A M) [Finite pres.G], Module.Finite A M
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
CategoryTheory.instFaithfulForget : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC], (CategoryTheory.forget C).Faithful
-- Init.Data.Range.Polymorphic.Fin
Fin.instLawfulUpwardEnumerableLeast? : ∀ {n : ℕ} [inst : NeZero n], Std.PRange.LawfulUpwardEnumerableLeast? (Fin n)
-- Mathlib.Algebra.Order.ToIntervalMod
/-- **Alias** of the reverse direction of `toIcoMod_inj`.

---

If `a` and `b` fall within the same cycle w.r.t. `c`, then they are congruent modulo `p`.  -/
AddCommGroup.ModEq.toIcoMod_eq_toIcoMod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b c : α}, a ≡ b [PMOD p] → toIcoMod hp c a = toIcoMod hp c b
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderTriple.holderConjugate_div_div : ∀ (p q r : ENNReal) [p.HolderTriple q r], r ≠ 0 → r ≠ ⊤ → (p / r).HolderConjugate (q / r)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.SpecialLinearGroup.mapGL_coe_matrix : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] (g : Matrix.SpecialLinearGroup n R),
  ↑((Matrix.SpecialLinearGroup.mapGL S) g) = ↑((Matrix.SpecialLinearGroup.map (algebraMap R S)) g)
-- Mathlib.Analysis.InnerProductSpace.Basic
Complex.inner : ∀ (w z : ℂ), inner ℝ w z = (z * (starRingEnd ℂ) w).re
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.instHasStrongEpiMonoFactorisations : CategoryTheory.Limits.HasStrongEpiMonoFactorisations SimplexCategory
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.matchesAt_iff_exists_isMatch : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.MatchesAt pat pos ↔
    ∃ endPos, ∃ (h : pos ≤ endPos), String.Slice.Pattern.Model.IsMatch pat (pos.sliceFrom endPos h)
-- Mathlib.Algebra.Order.Group.End
OrderHom.instMonoid : {α : Type u_1} → [inst : Preorder α] → Monoid (α →o α)
-- Mathlib.Algebra.Group.Defs
RightCancelSemigroup.mk : {G : Type u} → [toSemigroup : Semigroup G] → [toIsRightCancelMul : IsRightCancelMul G] → RightCancelSemigroup G
-- Lean.Compiler.IR.Basic
Lean.IR.AlphaEqv : Type → Type
-- Mathlib.Data.Sign.Defs
SignType.neg_one_lt_one : -1 < 1
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.volume_Ico : ∀ (x y : ↑unitInterval), MeasureTheory.volume (Set.Ico x y) = ENNReal.ofReal (↑y - ↑x)
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atTop_of_add_isBoundedUnder_le : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M]
  {l : Filter α} {f g : α → M},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l g →
    Filter.Tendsto (fun x => f x + g x) l Filter.atTop → Filter.Tendsto f l Filter.atTop
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- A collection of morphisms `P ⟶ f b` induces a morphism `P ⟶ ∏ᶜ f`.  -/
CategoryTheory.Limits.Pi.lift : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f : β → C} → [inst_1 : CategoryTheory.Limits.HasProduct f] → {P : C} → ((b : β) → P ⟶ f b) → (P ⟶ ∏ᶜ f)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_ric_eq_none : ∀ {n i : ℕ}, n < i → (*...=n).toArray[i]? = none
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.sheafifyMap_sheafifyLift_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q) (γ : Q ⟶ R) (hR : CategoryTheory.Presheaf.IsSheaf J R) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (J.sheafifyMap η) (CategoryTheory.CategoryStruct.comp (J.sheafifyLift γ hR) h) =
    CategoryTheory.CategoryStruct.comp (J.sheafifyLift (CategoryTheory.CategoryStruct.comp η γ) hR) h
-- Std.Data.HashMap.Lemmas
Std.HashMap.find?_toList_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} {v : β}, List.find? (fun a => a.1 == k) m.toList = some (k', v) ↔ m.getKey? k = some k' ∧ m[k]? = some v
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval.instFiniteOrig : ∀ {R : Type u_1} {A : Type u_3} {M : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] (a : A)
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] [Module.Finite R M], Module.Finite R (Module.AEval R M a)
-- Init.Data.Nat.Simproc
Nat.Simproc.bneEqOfEqEq : ∀ {a b c d : ℕ}, (a = b) = (c = d) → (a != b) = (c != d)
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.not_monic_zero_iff : ∀ {R : Type u} [inst : Semiring R], ¬Polynomial.Monic 0 ↔ 0 ≠ 1
-- Init.Data.List.Monadic
List.zipWithM'_eq_mapM_id_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type v} {m : Type v → Type w} [inst : Monad m] [LawfulMonad m] {f : α → β → m γ}
  {as : List α} {bs : List β}, List.zipWithM' f as bs = List.mapM id (List.zipWith f as bs)
-- Mathlib.MeasureTheory.Measure.DiracProba
MeasureTheory.diracProba_toMeasure_apply : ∀ {X : Type u_1} [inst : MeasurableSpace X] [MeasurableSingletonClass X] (x : X) (A : Set X),
  ↑(MeasureTheory.diracProba x) A = A.indicator 1 x
-- Init.Data.Array.Find
Array.isSome_findFinIdx? : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, (Array.findFinIdx? p xs).isSome = xs.any p
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimitsOfShape.mk : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C],
  autoParam (∀ (F : CategoryTheory.Functor J C), CategoryTheory.Limits.HasLimit F)
      CategoryTheory.Limits.HasLimitsOfShape.has_limit._autoParam →
    CategoryTheory.Limits.HasLimitsOfShape J C
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.transport_μ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (i : F ≅ G) (X Y : C) {Z : D}
  (h : G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ G X Y) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (i.inv.app X) (i.inv.app Y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y)
        (CategoryTheory.CategoryStruct.comp (i.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) h))
-- Batteries.Data.BinomialHeap.Basic
/-- The list of elements prior to the minimum element, encoded as a "difference list".  -/
Batteries.BinomialHeap.Imp.FindMin.before : {α : Type u_1} →
  Batteries.BinomialHeap.Imp.FindMin α → Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α
-- Mathlib.Topology.Algebra.Support
mulTSupport_mul_inv : ∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : DivisionMonoid α] (f g : X → α),
  (mulTSupport fun x => f x * (g x)⁻¹) ⊆ mulTSupport f ∪ mulTSupport g
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.σ_num : ∀ (g h : GL (Fin 2) ℝ) (z : ℂ),
  (UpperHalfPlane.σ g) (UpperHalfPlane.num h z) = UpperHalfPlane.num h ((UpperHalfPlane.σ g) z)
-- Mathlib.Data.Seq.Defs
/-- `Seq1 α` is the type of nonempty sequences.  -/
Stream'.Seq1 : Type u_1 → Type u_1
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
/-- A predicate saying that a function is harmonic on a set and is continuous on its closure. This is a
common assumption in harmonic analysis.
 -/
InnerProductSpace.HarmonicContOnCl : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      [FiniteDimensional ℝ E] →
        {F : Type u_2} → [inst : NormedAddCommGroup F] → [NormedSpace ℝ F] → (E → F) → Set E → Prop
-- Mathlib.NumberTheory.SelbergSieve
SelbergSieve.mk : BoundingSieve → (level : ℝ) → 1 ≤ level → SelbergSieve
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The initial state, evaluating function `c` on input `v`.  -/
Turing.PartrecToTM2.init : Turing.ToPartrec.Code → List ℕ → Turing.PartrecToTM2.Cfg'
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.inv_right : ∀ {α : Type u_1} {f g : Equiv.Perm α}, f.Disjoint g → f.Disjoint g⁻¹
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.Num.add.match_1.eq_3 : ∀ (motive : Num → Num → Sort u_1) (a b : PosNum) (h_1 : (a : Num) → motive Num.zero a)
  (h_2 : (b : Num) → motive b Num.zero) (h_3 : (a b : PosNum) → motive (Num.pos a) (Num.pos b)),
  (match Num.pos a, Num.pos b with
    | Num.zero, a => h_1 a
    | b, Num.zero => h_2 b
    | Num.pos a, Num.pos b => h_3 a b) =
    h_3 a b
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
CategoryTheory.Monoidal.whiskerLeft_fst : ∀ (X : CategoryTheory.Cat) {A B : CategoryTheory.Cat} (f : A ⟶ B),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).toFunctor.comp (CategoryTheory.Prod.fst ↑X ↑B) =
    CategoryTheory.Prod.fst ↑X ↑A
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RoiSliceData.mk.inj : ∀ {α : Type u} {β : α → Type v} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α β} {range : Std.Roi α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α β} {range_1 : Std.Roi α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.not_lt_norm : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsLinearOrder α] [Lean.Grind.OrderedRing α] (ctx : Lean.Grind.CommRing.Context α)
  (lhs rhs : Lean.Grind.CommRing.Expr) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.core_cert rhs lhs p = true →
    ¬Lean.Grind.CommRing.Expr.denote ctx lhs < Lean.Grind.CommRing.Expr.denote ctx rhs →
      Lean.Grind.CommRing.Poly.denote ctx p ≤ 0
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgEquiv.isTranscendenceBasis_iff : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing A'] [inst_3 : Algebra R A] [inst_4 : Algebra R A'] (e : A ≃ₐ[R] A'),
  IsTranscendenceBasis R (⇑e ∘ x) ↔ IsTranscendenceBasis R x