mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.toCycles_Ψ_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 j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.toCycles_Ψ._auto_1) {Z : C}
  (h : X.opcycles f₁ f₂ n₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.toCycles f₂ f₃ f₂₃ h₂₃ n₀)
      (CategoryTheory.CategoryStruct.comp (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁) h) =
    CategoryTheory.CategoryStruct.comp (X.δ f₁ f₂₃ n₀ n₁ hn₁)
      (CategoryTheory.CategoryStruct.comp (X.pOpcycles f₁ f₂ n₁) h)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.enum_lt_fin : ∀ {n : ℕ} (x : Fin n), (Ordinal.enum LT.lt) ⟨↑↑x, ⋯⟩ = x
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_nonneg : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  0 ≤ ProbabilityTheory.mgf X μ t
-- Mathlib.Order.RelSeries
RelSeries.snoc_length : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newLast : α) (rel : (p.last, newLast) ∈ r),
  (p.snoc newLast rel).length = p.length + 1
-- Mathlib.RingTheory.Unramified.Finite
Algebra.FormallyUnramified.finite_of_free_aux : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (I : Type u_4)
  [inst_3 : DecidableEq I] (b : Module.Basis I R S) (f : I →₀ S) (x : S) (a : I → I →₀ R),
  (a = fun i => b.repr (b i * x)) →
    (1 ⊗ₜ[R] x * f.sum fun i y => y ⊗ₜ[R] b i) =
      ∑ k ∈ f.support.biUnion fun i => (a i).support,
        (b.repr (f.sum fun i y => (a i) k • y)).sum fun j c => c • b j ⊗ₜ[R] b k
-- Mathlib.NumberTheory.WellApproximable
approxAddOrderOf.image_nsmul_subset_of_coprime : ∀ {A : Type u_1} [inst : SeminormedAddCommGroup A] {m n : ℕ} (δ : ℝ),
  0 < m → n.Coprime m → (fun y => m • y) '' approxAddOrderOf A n δ ⊆ approxAddOrderOf A n (↑m * δ)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.id_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData),
  (CategoryTheory.ShortComplex.LeftHomologyMapData.id h).φH = CategoryTheory.CategoryStruct.id h.H
-- Mathlib.Algebra.Category.MonCat.Adjunctions
/-- The free functor `Type u ⥤ MonCat` sending a type `X` to the free monoid on `X`.  -/
MonCat.free : CategoryTheory.Functor (Type u) MonCat
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The fundamental property of the adjoint.  -/
LinearMap.adjoint_inner_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (x : E) (y : F),
  inner 𝕜 ((LinearMap.adjoint A) y) x = inner 𝕜 y (A x)
-- Init.PropLemmas
and_iff_left : ∀ {b a : Prop}, b → (a ∧ b ↔ a)
-- Mathlib.Algebra.Category.Grp.Basic
/-- Build a `MulEquiv` from an isomorphism in the category `GrpCat`.  -/
CategoryTheory.Iso.groupIsoToMulEquiv : {X Y : GrpCat} → (X ≅ Y) → ↑X ≃* ↑Y
-- Mathlib.LinearAlgebra.Pi
LinearMap.lsum_apply : ∀ (R : Type u) {M : Type v} {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (S : Type u_1) [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : Fintype ι] [inst_7 : Semiring S] [inst_8 : Module S M] [inst_9 : SMulCommClass R S M]
  (f : (i : ι) → φ i →ₗ[R] M), (LinearMap.lsum R φ S) f = ∑ i, f i ∘ₗ LinearMap.proj i
-- Aesop.Search.Expansion.Norm
Aesop.NormSeqResult : Type
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.neg_smul_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R) {u : R},
  IsUnit u → W'.neg (u • P) ≈ W'.neg P
-- Mathlib.Algebra.Group.Subsemigroup.Membership
AddSubsemigroup.mem_iSup_of_mem : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Add M] {S : ι → AddSubsemigroup M} (i : ι) {x : M}, x ∈ S i → x ∈ iSup S
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.valuation_surjective : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  Function.Surjective ⇑(IsDedekindDomain.HeightOneSpectrum.valuation K v)
-- Init.Data.Array.Lemmas
Array.getElem?_size : ∀ {α : Type u_1} {xs : Array α}, xs[xs.size]? = none
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcHom_id : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a),
  (cfcHom ha) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instHAddOffset_4 : HAdd Std.Time.WallTime Std.Time.Second.Offset Std.Time.WallTime
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.InternalConsumers.toList_filterMap : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Option γ} (it : Std.IterM m β),
  (Std.IterM.filterMap f it).toList = (fun x => List.filterMap f x) <$> it.toList
-- Mathlib.CategoryTheory.Sites.PreservesLimits
instPreservesLimitsOfShapeSheafTypeUliftYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : J.Subcanonical] {K : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} K],
  CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J)
-- Mathlib.Algebra.Ring.Action.Submonoid
FixedPoints.mem_addSubgroup : ∀ (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst_1 : AddGroup α] [inst_2 : DistribMulAction M α] (a : α),
  a ∈ FixedPoints.addSubgroup M α ↔ ∀ (m : M), m • a = a
-- Init.Data.Int.DivMod.Basic
Int.divExact_eq_ediv : ∀ {x y : ℤ} (h : y ∣ x), x.divExact y h = x / y
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.ofSubsingleton_apply_apply : ∀ (R : Type u_1) [inst : Semiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} [inst_5 : Subsingleton ι] (i : ι) (f : M →ₗ[R] N)
  (x : ι → M), ((AlternatingMap.ofSubsingleton R M N i) f) x = f (x i)
-- Mathlib.Order.Interval.Finset.Defs
Set.toFinset_Ici : ∀ {α : Type u_3} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : α) [inst_2 : Fintype ↑(Set.Ici a)],
  (Set.Ici a).toFinset = Finset.Ici a
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- The canonical isomorphism between `(Fork.ofι ι w).op` and `Cofork.ofπ ι.op w'`.  -/
CategoryTheory.Limits.Fork.ofιOpIsoOfπ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y P : C} →
      {f g : X ⟶ Y} →
        (ι ι' : P ⟶ X) →
          (w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g) →
            (w' : CategoryTheory.CategoryStruct.comp f.op ι'.op = CategoryTheory.CategoryStruct.comp g.op ι'.op) →
              ι = ι' → ((CategoryTheory.Limits.Fork.ofι ι w).op ≅ CategoryTheory.Limits.Cofork.ofπ ι'.op w')
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
/-- position of the argument we are recursing on, among all parameters  -/
Lean.Elab.Structural.RecArgInfo.recArgPos : Lean.Elab.Structural.RecArgInfo → ℕ
-- Mathlib.Analysis.Convex.Jensen
/-- Canonical form of the **strict Jensen's inequality**.  -/
StrictConvexOn.map_sum_lt_iff_of_pos' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConvexOn 𝕜 s f →
    (∀ i ∈ t, 0 < w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) → (f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i) ↔ ∃ j ∈ t, p j ≠ ∑ i ∈ t, w i • p i)
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
/-- If `H' : D' ⥤ V` is a pointwise left Kan extension along `L : D ⥤ D'` at `d : D'` and
if tensoring left with an object preserves colimits in `V`,
then `K ⊠ H' : D' × E ⥤ V` is a pointwise left Kan extension along `(𝟭 E) × L` at `(e, d)` for
every `e`.  -/
CategoryTheory.MonoidalCategory.ExternalProduct.isPointwiseLeftKanExtensionAtExtensionUnitRight : {V : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {D : Type u₂} →
        {D' : Type u₃} →
          {E : Type u₄} →
            [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} D'] →
                [inst_4 : CategoryTheory.Category.{v₄, u₄} E] →
                  {H : CategoryTheory.Functor D V} →
                    {L : CategoryTheory.Functor D D'} →
                      (H' : CategoryTheory.Functor D' V) →
                        (α : H ⟶ L.comp H') →
                          (K : CategoryTheory.Functor E V) →
                            (d : D') →
                              (CategoryTheory.Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d →
                                (e : E) →
                                  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow L d)
                                        (CategoryTheory.MonoidalCategory.tensorLeft (K.obj e))] →
                                    (CategoryTheory.Functor.LeftExtension.mk
                                          (CategoryTheory.MonoidalCategory.externalProduct K H')
                                          (CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitRight H' α
                                            K)).IsPointwiseLeftKanExtensionAt
                                      (e, d)
-- Mathlib.GroupTheory.Nilpotent
Subgroup.isNilpotent_of_lowerCentralSeries_eq_bot : ∀ {G : Type u_1} [inst : Group G] {S : Subgroup G} {n : ℕ}, S.lowerCentralSeries n = ⊥ → Group.IsNilpotent ↥S
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- Given `a, b ∈ A` and `v b ≤ v a` we can find `y : A` such that `y * a` is close to `b` by
the valuation `v`.  -/
IsDedekindDomain.HeightOneSpectrum.exists_intValuation_mul_sub_lt : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {a b : R},
  v.intValuation b ≤ v.intValuation a → ∀ (γ : Multiplicative ℤ), ∃ y, v.intValuation (b - y * a) < ↑γ
-- Mathlib.Data.PNat.Xgcd
PNat.gcd_rel_left' : ∀ (a b : ℕ+), a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.weightedSMul_null : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {s : Set α}, μ s = 0 → MeasureTheory.weightedSMul μ s = 0
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
/-- The associated pre-`0`-hypercover family to a precoverage.  -/
CategoryTheory.Precoverage.preZeroHypercoverFamily : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Precoverage C → CategoryTheory.PreZeroHypercoverFamily C
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.restrictPreimage'_apply : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) (s : Set B)
  [inst_3 : Nonempty (↑s → F → ↑(proj ⁻¹' s))] (z : ↑(proj ⁻¹' s)),
  ↑(e.restrictPreimage' s) z = (⟨proj ↑z, ⋯⟩, (↑e.toPretrivialization ↑z).2)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flattenAfter.match_3.eq_3 : ∀ {α₂ β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₂ m β] (it₂ : Std.IterM m β)
  (motive : it₂.Step → Sort u_3) (h : it₂.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it₂' : Std.IterM m β) →
      (out : β) → (h : it₂.IsPlausibleStep (Std.IterStep.yield it₂' out)) → motive ⟨Std.IterStep.yield it₂' out, h⟩)
  (h_2 :
    (it₂' : Std.IterM m β) → (h : it₂.IsPlausibleStep (Std.IterStep.skip it₂')) → motive ⟨Std.IterStep.skip it₂', h⟩)
  (h_3 : (h : it₂.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it₂' out, h⟩ => h_1 it₂' out h
    | ⟨Std.IterStep.skip it₂', h⟩ => h_2 it₂' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Finset.mem_bipartiteAbove : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {t : Finset β} {a : α} [inst : DecidablePred (r a)] {b : β},
  b ∈ Finset.bipartiteAbove r t a ↔ b ∈ t ∧ r a b
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
Mathlib.Tactic.BicategoryCoherence.liftHom₂RightUnitorHom : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      (f : a ⟶ b) →
        [inst_1 : Mathlib.Tactic.BicategoryCoherence.LiftHom f] →
          Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.Bicategory.rightUnitor f).hom
-- Std.Sync.Semaphore
/-- Creates a new semaphore with `permits` initially available permits.
 -/
Std.Semaphore.new : ℕ → BaseIO Std.Semaphore
-- Mathlib.RepresentationTheory.Basic
Representation.norm_ofDistribMulAction_eq : ∀ {k : Type u_1} {A : Type u_3} [inst : Semiring k] [inst_1 : AddCommMonoid A] [inst_2 : Module k A] {G : Type u_4}
  [inst_3 : Group G] [inst_4 : Fintype G] [inst_5 : DistribMulAction G A] [inst_6 : SMulCommClass G k A] (x : A),
  (Representation.ofDistribMulAction k G A).norm x = ∑ g, g • x
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.step_negRev_iff : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)},
  FreeAddGroup.Red.Step (FreeAddGroup.negRev L₁) (FreeAddGroup.negRev L₂) ↔ FreeAddGroup.Red.Step L₁ L₂
-- Lean.Meta.LetToHave
/-- If we don't need full typechecking, returns `e`, otherwise evaluates `m`.  -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.whenCheck : Lean.Expr → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝ → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Break.runK.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Lean.ReservedNameAction
/-- Register a new function that is invoked when trying to resolve a reserved name.
 -/
Lean.registerReservedNameAction : Lean.ReservedNameAction → IO Unit
-- Mathlib.CategoryTheory.Sites.Equivalence
/-- An auxiliary definition for the sheafification adjunction.  -/
CategoryTheory.Equivalence.transportIsoSheafToPresheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (K : CategoryTheory.GrothendieckTopology D) →
            (e : C ≌ D) →
              (A : Type u₃) →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} A] →
                  [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse] →
                    (CategoryTheory.Equivalence.sheafCongr J K e A).functor.comp
                        ((CategoryTheory.sheafToPresheaf K A).comp e.op.congrLeft.inverse) ≅
                      CategoryTheory.sheafToPresheaf J A
-- Mathlib.Topology.Algebra.Polynomial
/-- The coefficients of the monic polynomials of bounded degree with bounded roots are
uniformly bounded.  -/
Polynomial.coeff_bdd_of_roots_le : ∀ {F : Type u_3} {K : Type u_4} [inst : CommRing F] [inst_1 : NormedField K] {B : ℝ} {d : ℕ} (f : F →+* K)
  {p : Polynomial F},
  p.Monic →
    (Polynomial.map f p).Splits →
      p.natDegree ≤ d →
        (∀ z ∈ (Polynomial.map f p).roots, ‖z‖ ≤ B) →
          ∀ (i : ℕ), ‖(Polynomial.map f p).coeff i‖ ≤ max B 1 ^ d * ↑(d.choose (d / 2))
-- Mathlib.Topology.MetricSpace.PiNat
/-- Given a point `x` in a product space `Π (n : ℕ), E n`, and `s` a subset of this space, then
`shortestPrefixDiff x s` if the smallest `n` for which there is no element of `s` having the same
prefix of length `n` as `x`. If there is no such `n`, then use `0` by convention.  -/
PiNat.shortestPrefixDiff : {E : ℕ → Type u_2} → ((n : ℕ) → E n) → Set ((n : ℕ) → E n) → ℕ
-- Init.Data.List.Perm
List.Perm.countP_congr : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₁.Perm l₂ → ∀ {p p' : α → Bool}, (∀ x ∈ l₁, p x = p' x) → List.countP p l₁ = List.countP p' l₂
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.PromiseCheckedResult.mk.sizeOf_spec : ∀ (mainEnv asyncEnv : Lean.Environment) (checkedEnvPromise : IO.Promise Lean.Kernel.Environment),
  sizeOf { mainEnv := mainEnv, asyncEnv := asyncEnv, checkedEnvPromise := checkedEnvPromise } =
    1 + sizeOf mainEnv + sizeOf asyncEnv + sizeOf checkedEnvPromise
-- Aesop.Rule.Forward
Aesop.instInhabitedForwardRulePriority : Inhabited Aesop.ForwardRulePriority
-- Lean.Expr
Lean.Expr.dbgToString : Lean.Expr → String
-- Mathlib.Algebra.Polynomial.Div
Polynomial.modByMonic_zero : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R), p %ₘ 0 = p
-- Mathlib.Algebra.Category.ModuleCat.EnoughInjectives
instEnoughInjectivesModuleCatInt : CategoryTheory.EnoughInjectives (ModuleCat ℤ)
-- Mathlib.Order.Filter.AtTopBot.Map
OrderIso.map_atBot : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β),
  Filter.map (⇑e) Filter.atBot = Filter.atBot
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {fallback v : β}, Std.ExtDTreeMap.Const.getD (t.insert k v) k fallback = v
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.eq_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y : C} {f g : W ⟶ X} {i : X ⟶ Y}
  [CategoryTheory.Mono i], CategoryTheory.CommSq f g i i → f = g
-- Init.GrindInstances.Ring.UInt
Lean.Grind.instPowUInt64UintOfNatNat : Lean.Grind.ToInt.Pow UInt64 (Lean.Grind.IntInterval.uint 64)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.shrinkFunctor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] {X : C}
  (S : CategoryTheory.Sieve X) (Y : Cᵒᵖ),
  (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).obj Y = {f | S.arrows (CategoryTheory.shrinkYonedaObjObjEquiv f)}
-- Mathlib.Algebra.GroupWithZero.Commute
Commute.inv_right₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a b : G₀}, Commute a b → Commute a b⁻¹
-- Mathlib.Topology.Constructions
/-- **Alias** of `Pi.continuous_domRestrict`. -/
Pi.continuous_restrict : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] (S : Set ι), Continuous S.domRestrict
-- Mathlib.Order.SuccPred.Basic
Order.pred_lt_iff_eq_or_gt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α],
  Order.pred b < a ↔ a = b ∨ b < a
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_mul_cancel_of_dvd : ∀ {a b : ℤ}, b ∣ a → a / b * b = a
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.isoComp_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.MonoFactorisation f) {X' : C} (g : X' ⟶ X), (F.isoComp g).I = F.I
-- Mathlib.Data.Matrix.Mul
Matrix.op_smul_one_eq_diagonal : ∀ {m : Type u_2} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : DecidableEq m] (a : α),
  MulOpposite.op a • 1 = Matrix.diagonal fun x => a
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a fallback : α} {v : β}, (m.insert k v).getKeyD a fallback = if (k == a) = true then k else m.getKeyD a fallback
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.funMap_unify_equiv : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] (G : ι → Type w) [inst_1 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] {n : ℕ} (F : L.Functions n)
  (x : Fin n → FirstOrder.Language.Structure.Sigma f) (i j : ι) (hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x)))
  (hj : j ∈ upperBounds (Set.range (Sigma.fst ∘ x))),
  FirstOrder.Language.Structure.Sigma.mk f i
      (FirstOrder.Language.Structure.funMap F (FirstOrder.Language.DirectLimit.unify f x i hi)) ≈
    FirstOrder.Language.Structure.Sigma.mk f j
      (FirstOrder.Language.Structure.funMap F (FirstOrder.Language.DirectLimit.unify f x j hj))
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- If `a < b`, then an isomorphism `T.obj₂ ≅ T'.obj₂` extends to an isomorphism `T ≅ T'`
of distinguished triangles when for a t-structure, both `T.obj₁` and `T'.obj₁` are `≤ a` and
both `T.obj₃` and `T'.obj₃` are `≥ b`.  -/
CategoryTheory.Triangulated.TStructure.triangle_iso_exists : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) {T T' : CategoryTheory.Pretriangulated.Triangle C},
  T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
      ∀ (e : T.obj₂ ≅ T'.obj₂) (a b : ℤ),
        t.IsLE T.obj₁ a →
          t.IsGE T.obj₃ b →
            t.IsLE T'.obj₁ a →
              t.IsGE T'.obj₃ b →
                autoParam (a < b) CategoryTheory.Triangulated.TStructure.triangle_iso_exists._auto_1 →
                  ∃ e', e'.hom.hom₂ = e.hom
-- Lean.Parser.Do
/-- A `doSeq` is a sequence of `doElem`, the main argument after the `do` keyword and other
do elements that take blocks. It can either have the form `"{" (doElem ";"?)* "}"` or
`many1Indent (doElem ";"?)`, where `many1Indent` ensures that all the items are at
the same or higher indentation level as the first line.  -/
Lean.Parser.Term.doSeq : Lean.Parser.Parser
-- Mathlib.Data.Complex.Basic
Complex.I_mul : ∀ (z : ℂ), Complex.I * z = { re := -z.im, im := z.re }
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.ordConnectedComponent_ordConnectedProj : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Set α) (x : ↑s),
  s.ordConnectedComponent (s.ordConnectedProj x) = s.ordConnectedComponent ↑x
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsAEKolmogorovProcess.aestronglyMeasurable_edist : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E},
  ProbabilityTheory.IsAEKolmogorovProcess X P p q M →
    ∀ {s t : T}, MeasureTheory.AEStronglyMeasurable (fun ω => edist (X s ω) (X t ω)) P
-- Mathlib.Data.List.Forall2
List.SublistForall₂.is_trans : ∀ {α : Type u_1} {Rₐ : α → α → Prop} [IsTrans α Rₐ], IsTrans (List α) (List.SublistForall₂ Rₐ)
-- Mathlib.Algebra.Field.Opposite
MulOpposite.instSemifield : {α : Type u_1} → [Semifield α] → Semifield αᵐᵒᵖ