mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.norm_nonneg : ∀ (A : Type u_1) {E : Type u_2} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : Norm E] [CStarModule A E] {x : E}, 0 ≤ ‖x‖
-- Mathlib.Order.Bounds.Basic
bbdBelow_range_right_of_inf : ∀ {ι : Sort u_4} {α : Type u_5} [inst : SemilatticeInf α] {f g : ι → α},
  BddBelow (Set.range fun x => f x ⊓ g x) → BddBelow (Set.range g)
-- Mathlib.Logic.Equiv.Defs
Equiv.piUnique_symm_apply : ∀ {α : Sort u} [inst : Unique α] (β : α → Sort u_1), ⇑(Equiv.piUnique β).symm = uniqueElim
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleIcc_def_le : ∀ {n : ℕ} {i j : Fin n} (hij : i ≤ j),
  i.cycleIcc j = ((j - i).castLT ⋯).cycleRange.extendDomain (Fin.natAdd_castLEEmb ⋯).toEquivRange
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGT.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α)
  (x_3 : Std.DTreeMap.Internal.Impl.leaf.Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.gt),
  Std.DTreeMap.Internal.Impl.Const.getEntryGT k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.instAdd.eq_1 : ∀ {E : Type u_3} [inst : Group E],
  GroupNorm.instAdd =
    {
      add := fun p q =>
        let __src := p.toGroupSeminorm + q.toGroupSeminorm;
        { toGroupSeminorm := __src, eq_one_of_map_eq_zero' := ⋯ } }
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
GenContFract.squashSeq.eq_1 : ∀ {K : Type u_1} [inst : DivisionRing K] (s : Stream'.Seq (GenContFract.Pair K)) (n : ℕ),
  GenContFract.squashSeq s n =
    match (s.get? n, s.get? (n + 1)) with
    | (some gp_n, some gp_succ_n) =>
      Stream'.Seq.zipWith (fun n' gp => if n' = n then { a := gp_n.a, b := gp_n.b + gp_succ_n.a / gp_succ_n.b } else gp)
        Stream'.Seq.nats s
    | x => s
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_congr : ∀ {r s : ENNReal}, (∀ (n : ℕ∞), ↑n ≤ r ↔ ↑n ≤ s) → ⌊r⌋ₑ = ⌊s⌋ₑ
-- Mathlib.Algebra.Homology.Precylinder
HomologicalComplex.precylinder_i₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} [inst_2 : DecidableRel c.Rel] (K : HomologicalComplex C c)
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder],
  K.precylinder.i₀ = HomologicalComplex.cylinder.ι₀ K
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.uliftYonedaMap.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C),
  CategoryTheory.uliftYonedaMap F X =
    { app := fun x => TypeCat.ofHom fun f => { down := F.map f.down }, naturality := ⋯ }
-- Mathlib.Topology.Compactness.Compact
instNeBotCocompactOfNoncompactSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [NoncompactSpace X], (Filter.cocompact X).NeBot
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.IsSheaf.amalgamate_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {E : A} {X : C} {P : CategoryTheory.Functor Cᵒᵖ A}
  (hP : CategoryTheory.Presheaf.IsSheaf J P) (S : J.Cover X) (x : (I : S.Arrow) → E ⟶ P.obj (Opposite.op I.Y))
  (hx :
    ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂),
      CategoryTheory.CategoryStruct.comp (x I₁) (P.map r.g₁.op) =
        CategoryTheory.CategoryStruct.comp (x I₂) (P.map r.g₂.op))
  (I : S.Arrow), CategoryTheory.CategoryStruct.comp (hP.amalgamate S x hx) (P.map I.f.op) = x I
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        k ∉ m₂ → Std.DTreeMap.Raw.Const.getD (m₁ ∪ m₂) k fallback = Std.DTreeMap.Raw.Const.getD m₁ k fallback
-- Mathlib.Algebra.Polynomial.Div
Polynomial.natDegree_modByMonic_lt : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R) {q : Polynomial R}, q.Monic → q ≠ 1 → (p %ₘ q).natDegree < q.natDegree
-- Lean.Meta.Basic
Lean.Meta.instInhabitedDefEqCacheKey : Inhabited Lean.Meta.DefEqCacheKey
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isRat_neg : ∀ {α : Type u_1} [inst : Ring α] {f : α → α} {a : α} {n n' : ℤ} {d : ℕ},
  f = Neg.neg → Mathlib.Meta.NormNum.IsRat a n d → n.neg = n' → Mathlib.Meta.NormNum.IsRat (-a) n' d
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.exp_log_of_neg : ∀ {x : ℝ}, x < 0 → Real.exp (Real.log x) = -x
-- Init.Prelude
instDecidableLtBitVec : {w : ℕ} → (x y : BitVec w) → Decidable (x < y)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
PosMulReflectLE.toPosMulReflectLT : ∀ {α : Type u_1} [inst : MulZeroClass α] [inst_1 : PartialOrder α] [PosMulReflectLE α], PosMulReflectLT α
-- Mathlib.Algebra.Order.Sub.Defs
tsub_zero : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommMonoid α] [inst_2 : Sub α] [OrderedSub α] (a : α), a - 0 = a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- If `G` is an additive monoid object, then `Hom(-, G)` as a presheaf of additive monoids
is represented by `G`.  -/
CategoryTheory.yonedaAddGrpObjRepresentableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (G : C) →
        [inst_2 : CategoryTheory.AddGrpObj G] →
          ((CategoryTheory.yonedaAddGrpObj G).comp (CategoryTheory.forget AddGrpCat)).RepresentableBy G
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.IsStackFor.essSurj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {S : C}
  {R : CategoryTheory.Presieve S}, F.IsStackFor R → (F.toDescentData fun f => f.obj.hom).EssSurj
-- Init.Data.Ord.Basic
Ordering.then_self : ∀ {o : Ordering}, o.then o = o
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_neg : ∀ (a : UInt64), (-a).toUInt8 = -a.toUInt8
-- Mathlib.Algebra.Group.Conj
isConj_one_right : ∀ {α : Type u} [inst : Monoid α] {a : α}, IsConj 1 a ↔ a = 1
-- Mathlib.Tactic.Simps.Basic
Simps.ProjectionRule.rename.injEq : ∀ (oldName : Lean.Name) (oldStx : Lean.Syntax) (newName : Lean.Name) (newStx : Lean.Syntax) (oldName_1 : Lean.Name)
  (oldStx_1 : Lean.Syntax) (newName_1 : Lean.Name) (newStx_1 : Lean.Syntax),
  (Simps.ProjectionRule.rename oldName oldStx newName newStx =
      Simps.ProjectionRule.rename oldName_1 oldStx_1 newName_1 newStx_1) =
    (oldName = oldName_1 ∧ oldStx = oldStx_1 ∧ newName = newName_1 ∧ newStx = newStx_1)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.map_mul : ∀ {α β : Type u} (f : α → β) (x y : FreeGroup α), f <$> (x * y) = f <$> x * f <$> y
-- Lean.Parser.Extension
Lean.Parser.withOpenDeclFnCore : Lean.Syntax → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Condensed.Discrete.Module
CompHausLike.LocallyConstantModule.functorToPresheaves_obj_map : ∀ {P : TopCat → Prop} (R : Type (max u w)) [inst : Ring R] (X : ModuleCat R) {X_1 Y : (CompHausLike P)ᵒᵖ} (f : X_1 ⟶ Y),
  ((CompHausLike.LocallyConstantModule.functorToPresheaves R).obj X).map f =
    ModuleCat.ofHom (LocallyConstant.comapₗ R (TopCat.Hom.hom f.unop.hom))
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.of_map : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] {φ : MvPolynomial σ R}
  {n : ℕ} {f : R →+* S}, Function.Injective ⇑f → ((MvPolynomial.map f) φ).IsHomogeneous n → φ.IsHomogeneous n
-- Mathlib.CategoryTheory.Limits.Types.Limits
/-- The limit of a functor `F : J ⥤ Type _` is naturally isomorphic to `F.sections`.  -/
CategoryTheory.Limits.Types.limNatIsoSectionsFunctor : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] → CategoryTheory.Limits.lim ≅ CategoryTheory.Functor.sectionsFunctor J
-- Lean.Meta.CongrTheorems
Lean.Meta.instBEqCongrArgKind : BEq Lean.Meta.CongrArgKind
-- Mathlib.Data.Finite.Defs
Infinite.mk : ∀ {α : Sort u_3}, ¬Finite α → Infinite α
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedArg.default : Lean.IR.Arg
-- Mathlib.RingTheory.Extension.Basic
/-- The action of `R` on `P.Cotangent` for an `R`-extension `P → S`.  -/
Algebra.Extension.Cotangent.val_smul'' : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (r : R) (x : P.Cotangent), (r • x).val = r • x.val
-- Aesop.RuleSet.Member
Aesop.instInhabitedLocalRuleSetMember : Inhabited Aesop.LocalRuleSetMember
-- Mathlib.Computability.MyhillNerode
/-- The *left quotient* of `x` is the set of suffixes `y` such that `x ++ y` is in `L`.  -/
Language.leftQuotient : {α : Type u} → Language α → List α → Language α
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_union_of_disjoint : ∀ {α : Type u_1} {M : Type u_4} [inst : MulOneClass M] {s t : Set α},
  Disjoint s t → ∀ (f : α → M), (s ∪ t).mulIndicator f = fun a => s.mulIndicator f a * t.mulIndicator f a
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso_hom_app_hom_apply_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F X : CategoryTheory.Functor C V)
  (a :
    (((CategoryTheory.Functor.whiskeringLeft (C × C) C V).obj (CategoryTheory.MonoidalCategory.tensor C)).comp
          (((CategoryTheory.Functor.whiskeringLeft (C × CategoryTheory.Discrete PUnit.{1}) (C × C) V).obj
                ((CategoryTheory.Functor.id C).prod
                  (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))).comp
            (CategoryTheory.coyoneda.obj
              (Opposite.op
                (CategoryTheory.MonoidalCategory.externalProduct F
                  (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))))))).obj
      X)
  (X_1 : C),
  ((CategoryTheory.ConcreteCategory.hom
            ((CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso F).hom.app X))
          a).app
      X_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X_1)).inv
      (((CategoryTheory.CategoryStruct.comp
                (CategoryTheory.prod.rightUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv.toIso.hom
                (TypeCat.ofHom fun g =>
                  CategoryTheory.CategoryStruct.comp g
                    (((CategoryTheory.Functor.whiskeringLeft C C V).map
                          (CategoryTheory.NatIso.ofComponents
                              (fun x => CategoryTheory.MonoidalCategoryStruct.rightUnitor x) ⋯).hom).app
                      X))).hom'
            a).app
        X_1)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.delta_naturality : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Comonad C) ⦃X Y : C⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (T.map f) (T.δ.app Y) =
    CategoryTheory.CategoryStruct.comp (T.δ.app X) (T.map (T.map f))
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.AuxLemmas.lemmas : Lean.Meta.AuxLemmas → Lean.PHashMap Lean.Meta.AuxLemmaKey (Lean.Name × List Lean.Name)
-- Mathlib.Algebra.MvPolynomial.Counit
/-- `MvPolynomial.counitNat A` is the natural surjective ring homomorphism
`MvPolynomial A ℕ →+* A` obtained by `X a ↦ a`.

See `MvPolynomial.ACounit` for a “relative” variant for algebras over a base ring
and `MvPolynomial.counit` for the “absolute” variant with `A = ℤ`.  -/
MvPolynomial.counitNat : (A : Type u_1) → [inst : CommSemiring A] → MvPolynomial A ℕ →+* A
-- Mathlib.RingTheory.FractionalIdeal.Operations
/-- `FractionalIdeal.span_finset R₁ s f` is the fractional ideal of `R₁` generated by `f '' s`.  -/
FractionalIdeal.spanFinset : (R₁ : Type u_3) →
  [inst : CommRing R₁] →
    {K : Type u_4} →
      [inst_1 : Field K] →
        [inst_2 : Algebra R₁ K] →
          [IsFractionRing R₁ K] → {ι : Type u_5} → Finset ι → (ι → K) → FractionalIdeal (nonZeroDivisors R₁) K
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableWithinAt_of_subsingleton : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E} [Subsingleton E], DifferentiableWithinAt 𝕜 f s x
-- Lean.Meta.Sym.Pattern
/-- Attempts to match expression `e` against pattern `p` using purely syntactic matching.

Returns `some result` if matching succeeds, where `result` contains:
- `us`: Level assignments for the pattern's universe variables
- `args`: Expression assignments for the pattern's bound variables

Matching fails if:
- The term contains metavariables (use `unify?` instead)
- Structural mismatch after reducible unfolding

Instance arguments are synthesized (or assigned by unification). Any that cannot be resolved are
reported in `MatchUnifyResult.unresolvedInsts` rather than silently left as loose metavariables in
`args`. Proof arguments are skipped via proof irrelevance.
 -/
Lean.Meta.Sym.Pattern.match? : Lean.Meta.Sym.Pattern → Lean.Expr → optParam Bool true → Lean.Meta.Sym.SymM (Option Lean.Meta.Sym.MatchUnifyResult)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.of_pow : ∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S]
  {l : Filter α} [NormOneClass S] {f : α → S} {g : α → R} {n : ℕ}, (f ^ n) =o[l] (g ^ n) → n ≠ 0 → f =o[l] g
-- Mathlib.CategoryTheory.Category.Pointed
/-- compatibility with the distinguished points  -/
Pointed.Hom.map_point : ∀ {X Y : Pointed} (self : X.Hom Y), self.toFun X.point = Y.point
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_le_length_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  l.length ≤ (Std.Internal.List.insertEntry k v l).length
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.mem_functorPushforward_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} {Y : D} {S : CategoryTheory.Sieve X} {e : C ≌ D} {f : Y ⟶ e.functor.obj X},
  (CategoryTheory.Sieve.functorPushforward e.functor S).arrows f ↔
    S.arrows (CategoryTheory.CategoryStruct.comp (e.inverse.map f) (e.unitInv.app X))
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mrange.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F),
  AddMonoidHom.mrange f = (AddSubmonoid.map f ⊤).copy (Set.range ⇑f) ⋯
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.mul_param_zpow : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [inst : TopologicalSpace β] [inst_1 : Field β]
  [inst_2 : LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β],
  Filter.Tendsto k l Filter.atTop →
    Asymptotics.SuperpolynomialDecay l k f → ∀ (z : ℤ), Asymptotics.SuperpolynomialDecay l k fun a => f a * k a ^ z
-- Init.Data.List.MinMax
List.min_cons_cons_nil : ∀ {α : Type u_1} [inst : Min α] {a b : α}, [a, b].min ⋯ = a ⊓ b
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.re_im : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : Zero R], a.im.re = 0
-- Init.Data.Hashable
/-- An opaque (low-level) hash operation used to implement hashing for pointers.  -/
hash64 : UInt64 → UInt64
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rco_succ_right_eq_append : ∀ {m n : ℤ}, m ≤ n → (m...n + 1).toList = (m...n).toList ++ [n]
-- Mathlib.CategoryTheory.Category.ULift
/-- The equivalence between `C` and `ULiftHom (ULift C)`.  -/
CategoryTheory.ULiftHomULiftCategory.equiv : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → C ≌ CategoryTheory.ULiftHom (ULift.{u', u} C)
-- Lean.Server.References
/-- Determines the `RefIdent` for the `Info` `i` of an identifier in `module` and
whether it is a declaration.
 -/
Lean.Server.identOf : Lean.Elab.ContextInfo → Lean.Elab.Info → Option (Lean.Lsp.RefIdent × Bool)
-- Mathlib.Algebra.Algebra.Pi
AlgEquiv.piCongrLeft_symm_apply : ∀ {R : Type u_3} {ι : Type u_4} {A₁ : ι → Type u_5} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A₁ i)]
  [inst_2 : (i : ι) → Algebra R (A₁ i)] {ι' : Type u_8} (e : ι' ≃ ι) (x : (i : ι) → A₁ i),
  (AlgEquiv.piCongrLeft R A₁ e).symm x = (Equiv.piCongrLeft A₁ e).symm x
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.toSheafify_plusPlusIsoSheafify_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w)
  [inst_1 : CategoryTheory.Category.{t, 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] {FD : D → D → Type u_1}
  {CD : D → Type t} [inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_5 : CategoryTheory.ConcreteCategory D FD]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [inst_7 : (CategoryTheory.forget D).ReflectsIsomorphisms]
  [inst_8 :
    ∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  (P : CategoryTheory.Functor Cᵒᵖ D),
  CategoryTheory.CategoryStruct.comp (J.toSheafify P) (CategoryTheory.plusPlusIsoSheafify J D P).hom =
    CategoryTheory.toSheafify J P
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.tanh_injective : Function.Injective Real.tanh
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Multipliable.tprod_le_tprod_of_inj : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {g : κ → α} (e : ι → κ),
  Function.Injective e →
    (∀ c ∉ Set.range e, 1 ≤ g c) → (∀ (i : ι), f i ≤ g (e i)) → Multipliable f → Multipliable g → tprod f ≤ tprod g
-- Std.Http.Protocol.H1.Reader
/-- State that it has completed and cannot process more data.
 -/
Std.Http.Protocol.H1.Reader.State.closed : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader.State dir
-- Mathlib.Algebra.Ring.CentroidHom
/-- Commutativity of centroid homomorphisms with left multiplication.  -/
CentroidHom.map_mul_left' : ∀ {α : Type u_6} [inst : NonUnitalNonAssocSemiring α] (self : CentroidHom α) (a b : α),
  (↑self.toAddMonoidHom).toFun (a * b) = a * (↑self.toAddMonoidHom).toFun b
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_inter_mulSupport_eq' : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) (s t : Set α),
  (∀ x ∈ Function.mulSupport f, x ∈ s ↔ x ∈ t) → ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
-- Mathlib.RingTheory.LaurentSeries
/-- The algebra isomorphism between `K⟦X⟧` and the unit ball inside the `X`-adic completion of
`K⟮X⟯`.  -/
LaurentSeries.powerSeriesAlgEquiv : (K : Type u_2) →
  [inst : Field K] →
    PowerSeries K ≃ₐ[K] ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers (RatFunc K) (Polynomial.idealX K))
-- Mathlib.Data.Part
Part.left_dom_of_mul_dom : ∀ {α : Type u_1} [inst : Mul α] {a b : Part α}, (a * b).Dom → a.Dom
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {k : α}, (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k)
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
/-- A subsemiring `S` of `R` determines a subsemiring `S.op` of the opposite ring `Rᵐᵒᵖ`.  -/
Subsemiring.opEquiv : {R : Type u_2} → [inst : NonAssocSemiring R] → Subsemiring R ≃o Subsemiring Rᵐᵒᵖ
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- Bound `abv (a - b)` from above  -/
AbsoluteValue.sub_le_add : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing S] [inst_1 : PartialOrder S] [IsOrderedRing S] [inst_3 : Ring R]
  (abv : AbsoluteValue R S) [NoZeroDivisors S] (a b : R), abv (a - b) ≤ abv a + abv b
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Multipliable.tprod_finsetProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} [T2Space α] [ContinuousMul α] [L.NeBot] {f : γ → β → α} {s : Finset γ},
  (∀ i ∈ s, Multipliable (f i) L) → ∏'[L] (b : β), ∏ i ∈ s, f i b = ∏ i ∈ s, ∏'[L] (b : β), f i b
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_filter_key : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → Bool} {k fallback : α},
  (Std.ExtTreeMap.filter (fun k x => f k) t).getKeyD k fallback = (Option.filter f (t.getKey? k)).getD fallback
-- Mathlib.Topology.Homeomorph.Lemmas
/-- A homeomorphism `h : X ≃ₜ Y` lifts to a homeomorphism between subtypes corresponding to
predicates `p : X → Prop` and `q : Y → Prop` so long as `p = q ∘ h`.  -/
Homeomorph.subtype : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {p : X → Prop} → {q : Y → Prop} → (h : X ≃ₜ Y) → (∀ (x : X), p x ↔ q (h x)) → { x // p x } ≃ₜ { y // q y }
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.WalkingParallelFamily.one.sizeOf_spec : ∀ {J : Type w} [inst : SizeOf J], sizeOf CategoryTheory.Limits.WalkingParallelFamily.one = 1
-- Init.Data.SInt.Lemmas
Int8.le_iff_toBitVec_sle : ∀ {a b : Int8}, a ≤ b ↔ a.toBitVec.sle b.toBitVec = true
-- Init.Data.SInt.Basic
/-- Converts an arbitrary-precision integer to a 64-bit integer, wrapping on overflow or underflow.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Int.toInt64 48 = 48`
* `Int.toInt64 (-40_000) = -40_000`
* `Int.toInt64 2_147_483_648 = 2_147_483_648`
* `Int.toInt64 (-2_147_483_649) = -2_147_483_649`
* `Int.toInt64 9_223_372_036_854_775_808 = -9_223_372_036_854_775_808`
* `Int.toInt64 (-9_223_372_036_854_775_809) = 9_223_372_036_854_775_807`
 -/
Int.toInt64 : ℤ → Int64
-- Lean.ResolveName
/-- Returns `true` if `name` is a reserved name.
 -/
Lean.isReservedName : Lean.Environment → Lean.Name → Bool
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- Expresses the integral over `Ioi 0` of `t ^ (a - 1) * exp (-(r * t))` in terms of the Gamma
function, for complex `a`.  -/
Complex.integral_cpow_mul_exp_neg_mul_Ioi : ∀ {a : ℂ} {r : ℝ},
  0 < a.re → 0 < r → ∫ (t : ℝ) in Set.Ioi 0, ↑t ^ (a - 1) * Complex.exp (-(↑r * ↑t)) = (1 / ↑r) ^ a * Complex.Gamma a
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.map_vadd' : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_4} {V₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (self : P₁ ≃ᵃ[k] P₂) (p : P₁) (v : V₁),
  self.toEquiv (v +ᵥ p) = self.linear v +ᵥ self.toEquiv p
-- Mathlib.RingTheory.Valuation.Quotient
Valuation.self_le_supp_comap : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : CommRing R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (J : Ideal R)
  (v : Valuation (R ⧸ J) Γ₀), J ≤ (Valuation.comap (Ideal.Quotient.mk J) v).supp
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_erase_eq_of_not_compare_eq_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (∀ {km : α}, t.min? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).min? = t.min?
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.natDegree_T : ∀ (R : Type u_1) [inst : CommRing R] [IsDomain R] [NeZero 2] (n : ℤ), (Polynomial.Chebyshev.T R n).natDegree = n.natAbs
-- Mathlib.Order.Hom.Basic
OrderIso.apply_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) (x : β), e (e.symm x) = x