mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : PrimeSpectrum R)
  (q : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p})),
  ↑((PrimeSpectrum.preimageOrderIsoFiber R S p) q).asIdeal =
    ⇑(Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (Algebra.ofId R S) ⋯)
          (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯) ⁻¹'
      {0}
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.isPreconnected_iff_of_equivalence : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  (e : J ≌ K), CategoryTheory.IsPreconnected J ↔ CategoryTheory.IsPreconnected K
-- Lean.Meta.AppBuilder
/-- Similar to `mkAppM`, but takes an `Expr` instead of a constant name.  -/
Lean.Meta.mkAppM' : Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Logic.Equiv.PartialEquiv
/-- The proposition that `invFun` is a left-inverse of `toFun` on `source`.  -/
PartialEquiv.left_inv' : ∀ {α : Type u_5} {β : Type u_6} (self : PartialEquiv α β) ⦃x : α⦄, x ∈ self.source → self.invFun (↑self x) = x
-- Lean.Parser.Term
Lean.Parser.Term.binop.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- The closure of a submodule has the same orthogonal complement and the submodule itself.  -/
Submodule.orthogonal_closure : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E), K.topologicalClosureᗮ = Kᗮ
-- Mathlib.Order.Filter.CountablyGenerated
Filter.map.isCountablyGenerated : ∀ {α : Type u_1} {β : Type u_2} (l : Filter α) [l.IsCountablyGenerated] (f : α → β),
  (Filter.map f l).IsCountablyGenerated
-- Mathlib.Analysis.Normed.Module.FiniteDimension
ProperSpace.of_locallyCompact_module : ∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] (V : Type u_1) [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [IsTopologicalAddGroup V] [T2Space V] [Nontrivial V] [LocallyCompactSpace V]
  [inst_8 : Module 𝕜 V] [ContinuousSMul 𝕜 V], ProperSpace 𝕜
-- Mathlib.Algebra.Quandle
ShelfHom.mk : {S₁ : Type u_1} →
  {S₂ : Type u_2} →
    [inst : Shelf S₁] →
      [inst_1 : Shelf S₂] →
        (toFun : S₁ → S₂) → (∀ {x y : S₁}, toFun (Shelf.act x y) = Shelf.act (toFun x) (toFun y)) → ShelfHom S₁ S₂
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Asymptotics.isBigO_pow_pow_cobounded_of_le : ∀ {R : Type u_1} [inst : NormedRing R] [NormMulClass R] {p q : ℕ},
  p ≤ q → (fun x => x ^ p) =O[Bornology.cobounded R] fun x => x ^ q
-- Mathlib.Analysis.Convex.Basic
/-- The convex sets form an additive submonoid under pointwise addition.  -/
convexAddSubmonoid : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : Semiring 𝕜] → [PartialOrder 𝕜] → [inst_2 : AddCommMonoid E] → [Module 𝕜 E] → AddSubmonoid (Set E)
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCard_self : ∀ {α : Type u_1} (s : Multiset α), Multiset.powersetCard s.card s = {s}
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
_private.Mathlib.RingTheory.Coalgebra.CoassocSimps.0.CoassocSimps.«termλ⁻¹» : Lean.ParserDescr
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.app_surjective_of_stalkFunctor_map_bijective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  {F G : TopCat.Sheaf C X} (f : F ⟶ G) (U : TopologicalSpace.Opens ↑X),
  (∀ x ∈ U, Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f.hom))) →
    Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op U)))
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.withMDataExpr : {α : Type} →
  [Inhabited α] →
    {m : Type → Type} → [Monad m] → [MonadReaderOf Lean.SubExpr m] → [MonadWithReaderOf Lean.SubExpr m] → m α → m α
-- Batteries.Data.UnionFind.Basic
/-- Root of a union-find node.  -/
Batteries.UnionFind.rootN : {n : ℕ} → (self : Batteries.UnionFind) → Fin n → n = self.size → Fin n
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.Icc_coe : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Icc ↑b ↑a = WithBot.some '' Set.Icc b a
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.mk.injEq : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B] (toRingEquiv : A ≃+* B)
  (map_star' : ∀ (a : A), toRingEquiv.toFun (star a) = star (toRingEquiv.toFun a)) (toRingEquiv_1 : A ≃+* B)
  (map_star'_1 : ∀ (a : A), toRingEquiv_1.toFun (star a) = star (toRingEquiv_1.toFun a)),
  ({ toRingEquiv := toRingEquiv, map_star' := map_star' } =
      { toRingEquiv := toRingEquiv_1, map_star' := map_star'_1 }) =
    (toRingEquiv = toRingEquiv_1)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoCycles₁_inv_comp_iCycles_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ((Fin 1 → G) →₀ ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₁ A).inv
      (CategoryTheory.CategoryStruct.comp (groupHomology.iCycles A 1) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.i
        (groupHomology.chainsIso₁ A).inv)
      h
-- Mathlib.Order.Filter.Map
Filter.comap_top : ∀ {α : Type u_1} {β : Type u_2} {m : α → β}, Filter.comap m ⊤ = ⊤
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.mul_left : ∀ {α : Type u_1} {M : Type u_4} [inst : MulZeroClass M] {f : α → M},
  Function.HasFiniteSupport f → ∀ (g : α → M), Function.HasFiniteSupport (f * g)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.neg.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.neg = { neg := fun a => ⟨-↑a, ⋯⟩ }
-- Init.Data.List.Range
List.range_succ : ∀ {n : ℕ}, List.range n.succ = List.range n ++ [n]
-- Mathlib.Algebra.DirectSum.Module
DirectSum.linearEquivFunOnFintype_apply : ∀ (R : Type u) [inst : Semiring R] (ι : Type v) (M : ι → Type w) [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Fintype ι] (a : Π₀ (i : ι), (fun i => M i) i) (i : ι),
  (DirectSum.linearEquivFunOnFintype R ι M) a i = a i
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.attachLift : {α : Type w} → {m : Type w → Type w'} → [MonadAttach m] → m α → Std.Iterators.PostconditionT m α
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
measurableEmbedding_subLeft : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [MeasurableAdd G] [MeasurableNeg G] (g : G),
  MeasurableEmbedding fun x => g - x
-- Std.Http.Protocol.H1.Config
/-- Maximum length of request URI (default: 8192 bytes).
 -/
Std.Http.Protocol.H1.Config.maxUriLength : Std.Http.Protocol.H1.Config → ℕ
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.symm_preimage_preimage : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) (S : Set B), ⇑e.symm ⁻¹' ⇑e ⁻¹' S = S
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
MeasureTheory.Lp.finStronglyMeasurable : ∀ {α : Type u_1} {G : Type u_2} {p : ENNReal} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup G] (f : ↥(MeasureTheory.Lp G p μ)),
  p ≠ 0 → p ≠ ⊤ → MeasureTheory.FinStronglyMeasurable (↑↑f) μ
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_unitIso : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (X₂ : C₂),
  (CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence Φ X₂).unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (Φ.LeftResolution X₂)ᵒᵖ)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z)
  (g : Y ⟶ Z) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f],
  CategoryTheory.Limits.HasLimit
    ((CategoryTheory.Limits.cospan f g).comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.isoOfEq_inv : ∀ (X : AlgebraicGeometry.Scheme) {U V : X.Opens} (e : U = V), (X.isoOfEq e).inv = X.homOfLE ⋯
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.instInhabited : {R : Type u} → [inst : CommRing R] → Inhabited (CommAlgCat R)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- A constructor for natural isomorphisms of functors `X ⥤ CategoricalPullback`: to
construct such an isomorphism, it suffices to produce isomorphisms after whiskering with
the projections, and compatible with the canonical 2-commutative square .  -/
CategoryTheory.Limits.CategoricalPullback.mkNatIso : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {X : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    {J K : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)} →
                      (e₁ :
                          J.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G) ≅
                            K.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G)) →
                        (e₂ :
                            J.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G) ≅
                              K.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G)) →
                          autoParam
                              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight e₁.hom F)
                                  (CategoryTheory.CategoryStruct.comp
                                    (K.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
                                    (CategoryTheory.CategoryStruct.comp
                                      (K.whiskerLeft
                                        (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                                            (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
                                      (K.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv)) =
                                CategoryTheory.CategoryStruct.comp
                                  (J.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
                                  (CategoryTheory.CategoryStruct.comp
                                    (J.whiskerLeft
                                      (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                                          (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
                                    (CategoryTheory.CategoryStruct.comp
                                      (J.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv
                                      (CategoryTheory.Functor.whiskerRight e₂.hom G))))
                              CategoryTheory.Limits.CategoricalPullback.mkNatIso._auto_1 →
                            (J ≅ K)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
/-- The map between `Ext` induced by `LocalizerMorphism.smallShiftedHomMap`.  -/
CategoryTheory.Abelian.Ext.mapExactFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {D : Type u'} →
        [inst_2 : CategoryTheory.Category.{v', u'} D] →
          [inst_3 : CategoryTheory.Abelian D] →
            (F : CategoryTheory.Functor C D) →
              [F.Additive] →
                [CategoryTheory.Limits.PreservesFiniteLimits F] →
                  [CategoryTheory.Limits.PreservesFiniteColimits F] →
                    [inst_7 : CategoryTheory.HasExt C] →
                      [inst_8 : CategoryTheory.HasExt D] →
                        {X Y : C} →
                          {n : ℕ} → CategoryTheory.Abelian.Ext X Y n → CategoryTheory.Abelian.Ext (F.obj X) (F.obj Y) n
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.GSemiring.toGNonUnitalNonAssocSemiring : {ι : Type u_1} →
  {A : ι → Type u_2} →
    {inst : AddMonoid ι} →
      {inst_1 : (i : ι) → AddCommMonoid (A i)} → [self : DirectSum.GSemiring A] → DirectSum.GNonUnitalNonAssocSemiring A
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget.start : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {len : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget aig len → ℕ
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccAboveEquiv_apply : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), (finSuccAboveEquiv p) i = ⟨p.succAbove i, ⋯⟩
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.fstₗ_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β] (p : Lex (α × β)), (OrderAddMonoidHom.fstₗ α β) p = (ofLex p).1
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instNonUnitalNonAssocCommRingOfNonUnitalRingHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → NonUnitalNonAssocCommRing (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] →
                      NonUnitalNonAssocCommRing (DirectLimit G f)
-- Mathlib.CategoryTheory.Sites.Equivalence
/-- Transport `HasSheafify` along an equivalence of sites.  -/
CategoryTheory.Equivalence.hasSheafify : ∀ {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] [CategoryTheory.Functor.IsDenseSubsite K J e.inverse]
  [CategoryTheory.HasSheafify K A], CategoryTheory.HasSheafify J A
-- Mathlib.Combinatorics.Enumerative.Composition
/-- The canonical increasing bijection between `Fin (c.length + 1)` and `c.boundaries` is
exactly `c.boundary`.  -/
Composition.orderEmbOfFin_boundaries : ∀ {n : ℕ} (c : Composition n), c.boundaries.orderEmbOfFin ⋯ = c.boundary
-- Mathlib.Topology.Sets.Opens
/-- If `α` has a basis consisting of compact opens, then an open set in `α` is compact open iff
it is a finite union of some elements in the basis  -/
TopologicalSpace.Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion : ∀ {α : Type u_2} [inst : TopologicalSpace α] {ι : Type u_5} (b : ι → TopologicalSpace.Opens α),
  TopologicalSpace.Opens.IsBasis (Set.range b) →
    (∀ (i : ι), IsCompact ↑(b i)) → ∀ (U : Set α), IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, ↑(b i)
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.Isocrystal.toModule : {p : ℕ} →
  {inst : Fact (Nat.Prime p)} →
    {k : Type u_1} →
      {inst_1 : CommRing k} →
        {inst_2 : CharP k p} →
          {inst_3 : PerfectRing k p} →
            {V : Type u_2} →
              {inst_4 : AddCommGroup V} →
                [self : WittVector.Isocrystal p k V] → Module (FractionRing (WittVector p k)) V
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f)
  (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).inv.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp
        ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X))
        (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X) h))
-- Mathlib.Analysis.Calculus.FDeriv.Comp
HasFDerivWithinAt.comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {f' : E →L[𝕜] F} (x : E) {s : Set E}
  {g : F → G} {g' : F →L[𝕜] G} {t : Set F},
  HasFDerivWithinAt g g' t (f x) →
    HasFDerivWithinAt f f' s x → Set.MapsTo f s t → HasFDerivWithinAt (g ∘ f) (g' ∘SL f') s x
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.CategoryOfElements.CreatesLimitsAux.π_liftedConeElement' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor C (Type w)} {I : Type u₁}
  [inst_1 : CategoryTheory.Category.{v₁, u₁} I] [inst_2 : Small.{w, u₁} I] (F : CategoryTheory.Functor I A.Elements)
  (i : I),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.limit.π ((F.comp (CategoryTheory.CategoryOfElements.π A)).comp A) i))
      (CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement' F) =
    (F.obj i).snd
-- Mathlib.Algebra.Group.Basic
div_pow : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α) (n : ℕ), (a / b) ^ n = a ^ n / b ^ n
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.Hom.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {M N : CategoryTheory.Comon C} {x y : M.Hom N}, x.hom = y.hom → x = y
-- Init.PropLemmas
not_exists_of_forall_not : ∀ {α : Sort u_1} {p : α → Prop}, (∀ (x : α), ¬p x) → ¬∃ x, p x
-- Mathlib.GroupTheory.HNNExtension
/-- Multiplying `t^u` by a `NormalWord`, `w` and putting the result in normal form.  -/
HNNExtension.NormalWord.unitsSMul : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      ↥A ≃* ↥B →
        {d : HNNExtension.NormalWord.TransversalPair G A B} → ℤˣ → HNNExtension.NormalWord d → HNNExtension.NormalWord d
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_all_liftAt_one_self : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} [Nonempty M] {n : ℕ}
  {φ : L.BoundedFormula α n} {v : α → M} {xs : Fin n → M},
  (FirstOrder.Language.BoundedFormula.liftAt 1 n φ).all.Realize v xs ↔ φ.Realize v xs
-- Init.Core
instInhabitedForInStep : {a : Type u_1} → [Inhabited a] → Inhabited (ForInStep a)
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.mul_int : ∀ {p x : ℝ} {m : ℤ}, LiouvilleWith p x → m ≠ 0 → LiouvilleWith p (x * ↑m)
-- Lean.Meta.SizeOf
_private.Lean.Meta.SizeOf.0.Lean.Meta.isInductiveHypothesis : Array Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbitRel.Quotient.orbit_mk : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (a : α),
  MulAction.orbitRel.Quotient.orbit (Quotient.mk'' a) = MulAction.orbit G a
-- Mathlib.GroupTheory.Finiteness
/-- An equivalent expression of `AddMonoid.FG` in terms of `Set.Finite` instead of `Finset`.  -/
AddMonoid.fg_iff : ∀ {M : Type u_1} [inst : AddMonoid M], AddMonoid.FG M ↔ ∃ S, AddSubmonoid.closure S = ⊤ ∧ S.Finite
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.fpowerSeries.eq_1 : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E),
  f.fpowerSeries x 0 = ContinuousMultilinearMap.uncurry0 𝕜 E (f x)
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
/-- `ContinuousLinearMap.coprod` as a `ContinuousLinearEquiv`.  -/
ContinuousLinearMap.coprodEquivL : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {G : Type u_4} →
        (S : Type u_5) →
          [inst : NormedField 𝕜] →
            [inst_1 : Semiring S] →
              [inst_2 : AddCommGroup E] →
                [inst_3 : Module 𝕜 E] →
                  [inst_4 : TopologicalSpace E] →
                    [IsTopologicalAddGroup E] →
                      [inst_6 : AddCommGroup F] →
                        [inst_7 : Module 𝕜 F] →
                          [inst_8 : TopologicalSpace F] →
                            [IsTopologicalAddGroup F] →
                              [inst_10 : AddCommGroup G] →
                                [inst_11 : Module 𝕜 G] →
                                  [inst_12 : TopologicalSpace G] →
                                    [inst_13 : IsTopologicalAddGroup G] →
                                      [ContinuousConstSMul 𝕜 G] →
                                        [inst_15 : Module S G] →
                                          [inst_16 : SMulCommClass 𝕜 S G] →
                                            [inst_17 : ContinuousConstSMul S G] →
                                              ((E →L[𝕜] G) × (F →L[𝕜] G)) ≃L[S] E × F →L[𝕜] G
-- Mathlib.CategoryTheory.EpiMono
/-- `section_` composed with `f` is the identity  -/
CategoryTheory.SplitEpi.id_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.SplitEpi f)
  {Z : C} (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp self.section_ (CategoryTheory.CategoryStruct.comp f h) = h
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.multicospanShapeEnd_R : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J],
  (CategoryTheory.Limits.multicospanShapeEnd J).R = CategoryTheory.Arrow J
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  AlgebraicGeometry.Scheme.Hom.appTop hU.isoSpec.inv =
    CategoryTheory.CategoryStruct.comp U.topIso.hom
      (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.val_mkUnits : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {u : ℚ_[p]} (h : ‖u‖ = 1), ↑(PadicInt.mkUnits h) = ⟨u, ⋯⟩
-- Mathlib.RingTheory.Extension.Generators
/-- The assignment of each variable to a value in `S`.  -/
Algebra.Generators.val : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Generators R S ι → ι → S
-- Std.Net.Addr
Std.Net.SocketAddressV6.instToString : ToString Std.Net.SocketAddressV6
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsBasis.encard_eq_eRk : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → I.encard = M.eRk X