mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Nat.Factorization.Basic
Nat.factorization_le_factorization_mul_right : ∀ {a b : ℕ}, a ≠ 0 → b.factorization ≤ (a * b).factorization
-- Std.Internal.UV.DNS
/-- Asynchronously resolves a hostname and service to an array of socket addresses.
 -/
Std.Internal.UV.DNS.getAddrInfo : String → String → UInt8 → IO (IO.Promise (Except IO.Error (Array Std.Net.IPAddr)))
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.absolutelyContinuous_variation_transpose : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G),
  (μ.transpose B).variation.AbsolutelyContinuous μ.variation
-- Mathlib.Topology.Algebra.ConstMulAction
AddUnits.continuousConstVAdd : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddMonoid M] [inst_2 : AddAction M α]
  [ContinuousConstVAdd M α], ContinuousConstVAdd (AddUnits M) α
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.posFittingComp_eq_bot_of_isNilpotent : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [LieModule.IsNilpotent L M], LieModule.posFittingComp R L M = ⊥
-- Mathlib.Tactic.GRewrite.Elab
/-- Merge `lctx` into the local contexts in `tree`.
This is used to let `tree` know about bound variables that the term has been unified with.  -/
_private.Mathlib.Tactic.GRewrite.Elab.0.Mathlib.Tactic.GRewrite.updateInfoTree : Lean.LocalContext → Lean.Elab.InfoTree → Lean.Elab.InfoTree
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the reverse direction of `Equiv.Perm.sameCycle_pow_left`. -/
Equiv.Perm.SameCycle.pow_left : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℕ}, f.SameCycle x y → f.SameCycle ((f ^ n) x) y
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.toAddCommGroup : {α : Type u} → [I : Lean.Grind.Ring α] → Lean.Grind.AddCommGroup α
-- Mathlib.Data.Num.Lemmas
Num.cast_add : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] (m n : Num), ↑(m + n) = ↑m + ↑n
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.Nonempty.of_vadd_left : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α} {t : Set β}, (s +ᵥ t).Nonempty → s.Nonempty
-- Mathlib.Algebra.MvPolynomial.Cardinal
MvPolynomial.cardinalMk_eq_max : ∀ {σ R : Type u} [inst : CommSemiring R] [Nonempty σ] [Nontrivial R],
  Cardinal.mk (MvPolynomial σ R) = max (max (Cardinal.mk R) (Cardinal.mk σ)) Cardinal.aleph0
-- Mathlib.Computability.Partrec
Computable.vector_head : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Computable List.Vector.head
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
CochainComplex.homologyMap_comp_eq_zero_of_distTriang_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)),
  DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    ∀ (n : ℤ) {Z : C} (h : HomologicalComplex.homology T.obj₃ n ⟶ Z),
      CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap T.mor₁ n)
          (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap T.mor₂ n) h) =
        CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.Ring.Parity
Nat.odd_pow_iff : ∀ {n e : ℕ}, e ≠ 0 → (Odd (n ^ e) ↔ Odd n)
-- Mathlib.FieldTheory.RatFunc.Basic
/-- `FractionRing.liftAlgebra` specialized to `R⟮X⟯`.

This is a scoped instance because it creates a diamond when `L = R⟮X⟯`.  -/
RatFunc.liftAlgebra : (R : Type u_1) →
  (L : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : Field L] →
        [inst_2 : IsDomain R] →
          [inst_3 : Algebra (Polynomial R) L] → [FaithfulSMul (Polynomial R) L] → Algebra (RatFunc R) L
-- Mathlib.Data.Finset.Slice
Finset.sum_card_slice : ∀ {α : Type u_1} (𝒜 : Finset (Finset α)) [inst : Fintype α], ∑ r ≤ Fintype.card α, (𝒜.slice r).card = 𝒜.card
-- Mathlib.Tactic.ClickSuggestions.Util
/-- The ongoing computations.  -/
Mathlib.Tactic.ClickSuggestions.State.status : Mathlib.Tactic.ClickSuggestions.State → Std.HashMap String ℕ
-- Mathlib.Combinatorics.SimpleGraph.Partition
SimpleGraph.Partition.mk.sizeOf_spec : ∀ {V : Type u} {G : SimpleGraph V} [inst : SizeOf V] (parts : Set (Set V)) (isPartition : Setoid.IsPartition parts)
  (independent : ∀ s ∈ parts, IsAntichain G.Adj s),
  sizeOf { parts := parts, isPartition := isPartition, independent := independent } = 1 + sizeOf isPartition
-- Mathlib.Data.ENat.Basic
instBotENat : Bot ℕ∞
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_eq_some_getKey : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α} (h : a ∈ m), m.getKey? a = some (m.getKey a h)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.coord_repr_symm : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (i : ι) (f : ι →₀ R), (b.coord i) (b.repr.symm f) = f i
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsMonHom.instNormalId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G : C} [inst_2 : CategoryTheory.GrpObj G], CategoryTheory.IsMonHom.Normal (CategoryTheory.CategoryStruct.id G)
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_38 : HSub Std.Time.Week.Offset Std.Time.Second.Offset Std.Time.Second.Offset
-- Mathlib.Combinatorics.Additive.Convolution
Finset.univ_addConvolution : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] [inst_2 : Fintype G] (B : Finset G) (a : G),
  Finset.univ.addConvolution B a = B.card
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.π_comp_H2Iso_hom_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : (groupCohomology.shortComplexH2 A).moduleCatLeftHomologyData.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.π A 2)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.H2Iso A).hom h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₂ A).hom
      (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH2 A).moduleCatLeftHomologyData.π h)
-- Mathlib.Analysis.Normed.Module.Convex
NormedSpace.instPathConnectedSpace : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E], PathConnectedSpace E
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_eval_cast : ∀ (R : Type u) [inst : Ring R] (n : ℕ) (k : ℤ),
  ↑(Polynomial.eval k (descPochhammer ℤ n)) = Polynomial.eval (↑k) (descPochhammer R n)
-- Mathlib.Topology.Order.LocalExtr
Filter.EventuallyEq.isLocalMin_iff : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f g : α → β} {a : α},
  f =ᶠ[nhds a] g → (IsLocalMin f a ↔ IsLocalMin g a)
-- Init.Data.String.Basic
/-- Given a position in `s.sliceTo p₀`, obtain the corresponding position in `s`.  -/
String.Slice.Pos.ofSliceTo : {s : String.Slice} → {p₀ : s.Pos} → (s.sliceTo p₀).Pos → s.Pos
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inlCompInrCompInverseAssociator_inv_app_down_down : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (X : D),
  ((CategoryTheory.sum.inlCompInrCompInverseAssociator C D E).inv.app X).down.down =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (Sum.inl (Sum.inr X))).down.down
      (CategoryTheory.CategoryStruct.id (Sum.inl (Sum.inr X))).down.down
-- Mathlib.Order.Filter.Pi
Filter.instNeBotForallPi : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} [∀ (i : ι), (f i).NeBot], (Filter.pi f).NeBot
-- Mathlib.SetTheory.ZFC.Cardinal
/-- `ZFSet.card x` is equal to the cardinality of `x` as a set of `ZFSet`s.  -/
ZFSet.cardinalMk_coe_sort : ∀ {x : ZFSet.{u}}, Cardinal.mk ↥x = Cardinal.lift.{u + 1, u} x.card
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.divSubtractShift.match_1.splitter : {w : ℕ} →
  (motive : BitVec.DivModArgs w → Sort u_1) →
    (args : BitVec.DivModArgs w) → ((n d : BitVec w) → motive { n := n, d := d }) → motive args
-- Mathlib.Algebra.Squarefree.Basic
Squarefree.pow_dvd_of_pow_dvd : ∀ {R : Type u_1} [inst : Monoid R] {x y : R} {n : ℕ}, Squarefree y → x ^ n ∣ y → x ^ n ∣ x
-- Lean.Meta.Tactic.Grind.Anchor
_private.Lean.Meta.Tactic.Grind.Anchor.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
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.sum_mul_sum : ∀ {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [inst : NonUnitalNonAssocSemiring R] (s : Finset ι) (t : Finset κ)
  (f : ι → R) (g : κ → R), (∑ i ∈ s, f i) * ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i * g j
-- Init.Data.List.Count
List.count_cons_of_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {b a : α}, b ≠ a → ∀ {l : List α}, List.count a (b :: l) = List.count a l
-- Mathlib.Analysis.Normed.Ring.Basic
/-- Non-unital seminormed commutative ring structure on the product of two non-unital seminormed
commutative rings, using the sup norm.  -/
Prod.nonUnitalSeminormedCommRing : {α : Type u_2} →
  {β : Type u_3} →
    [NonUnitalSeminormedCommRing α] → [NonUnitalSeminormedCommRing β] → NonUnitalSeminormedCommRing (α × β)
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.intros : Lean.MVarId → Array Lean.FVarId → Lean.Meta.TransparencyMode → Aesop.Script.TacticBuilder
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.lift'_symm_apply_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : MulZeroOneClass β] (F : WithZero α →*₀ β) (x : α),
  (WithZero.lift'.symm F) x = F ↑x
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.instTransForallIsLittleOIsTheta : {α : Type u_1} →
  {E : Type u_3} →
    {F' : Type u_7} →
      {G' : Type u_8} →
        [inst : Norm E] →
          [inst_1 : SeminormedAddCommGroup F'] →
            [inst_2 : SeminormedAddCommGroup G'] →
              {l : Filter α} → Trans (Asymptotics.IsLittleO l) (Asymptotics.IsTheta l) (Asymptotics.IsLittleO l)
-- Init.Data.List.Lemmas
List.foldr_filter : ∀ {α : Type u_1} {β : Type u_2} {p : α → Bool} {f : α → β → β} {l : List α} {init : β},
  List.foldr f init (List.filter p l) = List.foldr (fun x y => if p x = true then f x y else y) init l
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.hom_neg_apply : ∀ {M N : AddMagmaCat} (e : M ≅ N) (s : ↑N),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.isEquivalenceMap₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L)
  (β : R.comp G ⟶ F.comp R') [F.IsEquivalence] [G.Faithful] [G.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β],
  (CategoryTheory.StructuredArrow.map₂ α β).IsEquivalence
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Fork.op.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Fork f g),
  c.op =
    (CategoryTheory.Limits.Cocone.precompose (CategoryTheory.Limits.parallelPairOpIso f g).hom).obj
      (CategoryTheory.Limits.Cocone.whisker CategoryTheory.Limits.walkingParallelPairOpEquiv.functor
        (CategoryTheory.Limits.Cone.op c))
-- Mathlib.Algebra.Order.Hom.Basic
GroupNormClass.toGroupSeminormClass : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : Group α} {inst_1 : AddCommMonoid β}
  {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : GroupNormClass F α β], GroupSeminormClass F α β
-- Mathlib.Algebra.Homology.ModelCategory.Injective
CochainComplex.Plus.modelCategoryQuillen.weakEquivalence_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {X Y : CochainComplex.Plus C} (f : X ⟶ Y), HomotopicalAlgebra.WeakEquivalence f ↔ QuasiIso f.hom
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.contains.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (t : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k' : α) →
                (v : β k') →
                  (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v l r)) →
            motive t
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.fmod.match_1.splitter : (motive : ℤ → ℤ → Sort u_1) →
  (x x_1 : ℤ) →
    ((x : ℤ) → motive 0 x) →
      ((m n : ℕ) → (m = 0 → False) → motive (Int.ofNat m) (Int.ofNat n)) →
        ((m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n)) →
          ((m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n)) →
            ((m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)) → motive x x_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k a : α}, a ∈ Std.DTreeMap.Internal.Impl.erase! k t ↔ compare k a ≠ Ordering.eq ∧ a ∈ t
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Transport a subalgebra via an algebra homomorphism.  -/
Subalgebra.map : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Semiring B] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → Subalgebra R A → Subalgebra R B
-- Init.Data.UInt.Bitwise
UInt8.toUInt32_and : ∀ (a b : UInt8), (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.mem_sphere' : ∀ {P : Type u_2} [inst : MetricSpace P] {p : P} {s : EuclideanGeometry.Sphere P}, p ∈ s ↔ dist s.center p = s.radius
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The multifork attached to a presheaf `F : Cᵒᵖ ⥤ A`, `S : C` and `E : PreOneHypercover S`.  -/
CategoryTheory.PreOneHypercover.multifork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
        {S : C} →
          (E : CategoryTheory.PreOneHypercover S) →
            (F : CategoryTheory.Functor Cᵒᵖ A) → CategoryTheory.Limits.Multifork (E.multicospanIndex F)
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A non-unital seminormed ring is a not-necessarily-unital ring
endowed with a seminorm which satisfies the inequality `‖x y‖ ≤ ‖x‖ ‖y‖`.  -/
NonUnitalSeminormedRing : Type u_5 → Type u_5
-- Init.Prelude
/-- A synthesized token without position information.  -/
Lean.SourceInfo.none : Lean.SourceInfo
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.t1Space_iff_isField : ∀ {R : Type u} [inst : CommSemiring R] [IsDomain R], T1Space (PrimeSpectrum R) ↔ IsField R
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.mk : (carrier : Type u) → [str : Mul carrier] → MagmaCat
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.length_toList : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF → (Std.DTreeMap.Internal.Impl.Const.toList t).length = t.size
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.asIsoHomologyι.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [inst_2 : S.HasHomology], S.asIsoHomologyι hg = S.asIsoHomologyι hg
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Constructor for natural transformations between parallel pairs.  -/
CategoryTheory.Limits.parallelPairHomMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C} →
      (p :
          F.obj CategoryTheory.Limits.WalkingParallelPair.zero ⟶ G.obj CategoryTheory.Limits.WalkingParallelPair.zero) →
        (q :
            F.obj CategoryTheory.Limits.WalkingParallelPair.one ⟶ G.obj CategoryTheory.Limits.WalkingParallelPair.one) →
          autoParam
              (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) q =
                CategoryTheory.CategoryStruct.comp p (G.map CategoryTheory.Limits.WalkingParallelPairHom.left))
              CategoryTheory.Limits.parallelPairHomMk._auto_1 →
            autoParam
                (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) q =
                  CategoryTheory.CategoryStruct.comp p (G.map CategoryTheory.Limits.WalkingParallelPairHom.right))
                CategoryTheory.Limits.parallelPairHomMk._auto_3 →
              (F ⟶ G)
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.instLawfulMonadLiftBindFunctionBindMonadLiftOfLawfulMonadLiftTOfLawfulMonad : ∀ {m : Type u → Type v} [inst : Monad m] {n : Type u → Type w} [inst_1 : Monad n] [inst_2 : MonadLiftT m n]
  [LawfulMonadLiftT m n] [LawfulMonad n], Std.Internal.LawfulMonadLiftBindFunction fun γ δ f x => monadLift x >>= f
-- Mathlib.Analysis.Asymptotics.Lemmas
ContinuousAt.isLittleO : ∀ {F : Type u_4} [inst : Norm F] {α : Type u_17} {E : Type u_18} [inst_1 : NormedRing E] [inst_2 : One F]
  [NormOneClass F] [inst_4 : TopologicalSpace α] {f : α → E} {x : α},
  ContinuousAt f x → (fun x_1 => f x_1 - f x) =o[nhds x] fun x => 1
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α} {k : α}, k ∉ m → l.contains k = false → (m.insertMany l).get? k = none
-- Mathlib.CategoryTheory.Functor.Derived.Adjunction
/-- Auxiliary definition for `Adjunction.derived`.  -/
CategoryTheory.Adjunction.derived' : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                {G : CategoryTheory.Functor C₁ C₂} →
                  {F : CategoryTheory.Functor C₂ C₁} →
                    (adj : G ⊣ F) →
                      {L₁ : CategoryTheory.Functor C₁ D₁} →
                        {L₂ : CategoryTheory.Functor C₂ D₂} →
                          (W₁ : CategoryTheory.MorphismProperty C₁) →
                            (W₂ : CategoryTheory.MorphismProperty C₂) →
                              [inst_4 : L₁.IsLocalization W₁] →
                                [inst_5 : L₂.IsLocalization W₂] →
                                  {G' : CategoryTheory.Functor D₁ D₂} →
                                    {F' : CategoryTheory.Functor D₂ D₁} →
                                      (α : L₁.comp G' ⟶ G.comp L₂) →
                                        (β : F.comp L₁ ⟶ L₂.comp F') →
                                          [G'.IsLeftDerivedFunctor α W₁] →
                                            [F'.IsRightDerivedFunctor β W₂] →
                                              (η : CategoryTheory.Functor.id D₁ ⟶ G'.comp F') →
                                                (ε : F'.comp G' ⟶ CategoryTheory.Functor.id D₂) →
                                                  autoParam
                                                      (∀ (X₁ : C₁),
                                                        CategoryTheory.CategoryStruct.comp (η.app (L₁.obj X₁))
                                                            (F'.map (α.app X₁)) =
                                                          CategoryTheory.CategoryStruct.comp (L₁.map (adj.unit.app X₁))
                                                            (β.app (G.obj X₁)))
                                                      CategoryTheory.Adjunction.derived'._auto_1 →
                                                    autoParam
                                                        (∀ (X₂ : C₂),
                                                          CategoryTheory.CategoryStruct.comp (G'.map (β.app X₂))
                                                              (ε.app (L₂.obj X₂)) =
                                                            CategoryTheory.CategoryStruct.comp (α.app (F.obj X₂))
                                                              (L₂.map (adj.counit.app X₂)))
                                                        CategoryTheory.Adjunction.derived'._auto_3 →
                                                      (G' ⊣ F')
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_pow_of_smul_comm : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
  [inst_3 : DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (n : ℕ),
  MulOpposite.op x.fst • x.snd = x.fst • x.snd → (x ^ n).snd = n • x.fst ^ n.pred • x.snd
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_of_isEmpty : ∀ {ι : Type u_1} {M : Type u_3} {f : ι → M} [inst : AddCommMonoid M] [IsEmpty ι] (s : Finset ι), ∑ i ∈ s, f i = 0
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- The circleMap is real analytic.  -/
analyticOnNhd_circleMap : ∀ (c : ℂ) (R : ℝ), AnalyticOnNhd ℝ (circleMap c R) Set.univ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a : α} {fallback : β},
      Std.DTreeMap.Raw.Const.getD (t.erase k) a fallback =
        if cmp k a = Ordering.eq then fallback else Std.DTreeMap.Raw.Const.getD t a fallback
-- Mathlib.Algebra.Group.End
MulAut.instGroup.eq_1 : ∀ (M : Type u_2) [inst : Mul M],
  MulAut.instGroup M =
    { mul := fun g h => MulEquiv.trans h g, mul_assoc := ⋯, one := MulEquiv.refl M, one_mul := ⋯, mul_one := ⋯,
      npow_zero := ⋯, npow_succ := ⋯, inv := MulEquiv.symm, div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯,
      zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Aesop.Stats.Report
Aesop.sortedMedianD : {α : Type u_1} → α → Array α → α
-- Lean.Meta.LazyDiscrTree
/-- Create a new trie with the given lazy entry.  -/
Lean.Meta.LazyDiscrTree.newTrie : {m : Type → Type u_1} →
  {α : Type} →
    [Monad m] →
      [MonadState (Array (Lean.Meta.LazyDiscrTree.Trie α)) m] →
        Lean.Meta.LazyDiscrTree.LazyEntry α → m Lean.Meta.LazyDiscrTree.TrieIndex
-- Mathlib.Data.Multiset.Basic
Multiset.coe_subsingletonEquiv : ∀ {α : Type u_1} [inst : Subsingleton α], ⇑(Multiset.subsingletonEquiv α) = Multiset.ofList
-- Mathlib.Topology.Germ
/-- Map the germ of functions `X × Y → Z` at `p = (x,y) ∈ X × Y` to the corresponding germ
of functions `X → Z` at `x ∈ X`  -/
Filter.Germ.sliceLeft : {X : Type u_1} →
  {Y : Type u_2} →
    {Z : Type u_3} →
      [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → {p : X × Y} → (nhds p).Germ Z → (nhds p.1).Germ Z
-- Std.Data.DHashMap.Internal.WF
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.interSmallerₘ : {α : Type u} →
  {β : α → Type v} →
    [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Raw α β → Std.DHashMap.Internal.Raw₀ α β