mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
Set.Finite.measure_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α},
  s.Finite → ∀ (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ], μ s = 0
-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- A triangulated category is a pretriangulated category which satisfies
the octahedron axiom (TR 4).  -/
CategoryTheory.IsTriangulated : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} 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] → [CategoryTheory.Pretriangulated C] → Prop
-- Mathlib.Algebra.DualNumber
/-- Scaling on the right is sent by `DualNumber.lift` to multiplication on the right  -/
DualNumber.lift_op_smul : ∀ {R : Type u_1} {B : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) })
  (a : A) (ad : DualNumber A), (DualNumber.lift fe) (MulOpposite.op a • ad) = (DualNumber.lift fe) ad * (↑fe).1 a
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.mk.sizeOf_spec : ∀ {ι : Type u_5} {B : Type u_6} [inst : TopologicalSpace B] {F : Type u_7} [inst_1 : TopologicalSpace F]
  [inst_2 : SizeOf ι] [inst_3 : SizeOf B] [inst_4 : SizeOf F] (baseSet : ι → Set B)
  (isOpen_baseSet : ∀ (i : ι), IsOpen (baseSet i)) (indexAt : B → ι)
  (mem_baseSet_at : ∀ (x : B), x ∈ baseSet (indexAt x)) (coordChange : ι → ι → B → F → F)
  (coordChange_self : ∀ (i : ι), ∀ x ∈ baseSet i, ∀ (v : F), coordChange i i x v = v)
  (continuousOn_coordChange :
    ∀ (i j : ι), ContinuousOn (fun p => coordChange i j p.1 p.2) ((baseSet i ∩ baseSet j) ×ˢ Set.univ))
  (coordChange_comp :
    ∀ (i j k : ι),
      ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k,
        ∀ (v : F), coordChange j k x (coordChange i j x v) = coordChange i k x v),
  sizeOf
      { baseSet := baseSet, isOpen_baseSet := isOpen_baseSet, indexAt := indexAt, mem_baseSet_at := mem_baseSet_at,
        coordChange := coordChange, coordChange_self := coordChange_self,
        continuousOn_coordChange := continuousOn_coordChange, coordChange_comp := coordChange_comp } =
    1
-- Mathlib.Probability.Independence.Basic
/-- The measurable space structures generated by independent pi-systems are independent.  -/
ProbabilityTheory.iIndepSets.iIndep : ∀ {Ω : Type u_1} {ι : Type u_2} {m : ι → MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  (∀ (i : ι), m i ≤ _mΩ) →
    ∀ (π : ι → Set (Set Ω)),
      (∀ (n : ι), IsPiSystem (π n)) →
        (∀ (i : ι), m i = MeasurableSpace.generateFrom (π i)) →
          ProbabilityTheory.iIndepSets π μ → ProbabilityTheory.iIndep m μ
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.WorkGroup.mk.sizeOf_spec : ∀ (fla : Std.Format.FlattenAllowability) (flb : Std.Format.FlattenBehavior) (items : List Std.Format.WorkItem✝),
  sizeOf { fla := fla, flb := flb, items := items } = 1 + sizeOf fla + sizeOf flb + sizeOf items
-- Mathlib.Data.Set.Image
Set.image_preimage_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} (s : Set β), Function.Surjective f → f '' f ⁻¹' s = s
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instCreatesLimitsOfSizeIndFunctorOppositeTypeInclusionOfHasLimits : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasLimits C] →
      CategoryTheory.CreatesLimitsOfSize.{v, v, v, max u v, max u (v + 1), max u (v + 1)}
        (CategoryTheory.Ind.inclusion C)
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.Iso.asOver_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (S : C) [inst_1 : CategoryTheory.OverClass X S]
  [inst_2 : CategoryTheory.OverClass Y S] (e : X ≅ Y) [inst_3 : CategoryTheory.HomIsOver e.hom S],
  (CategoryTheory.Iso.asOver S e).hom = CategoryTheory.OverClass.asOverHom S e.hom
-- Mathlib.Computability.Reduce
Computable.equiv₂ : ∀ (α : Type u_1) (β : Type u_2) [inst : Denumerable α] [inst_1 : Denumerable β], (Denumerable.equiv₂ α β).Computable
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb_ofFin : ∀ {n : ℕ} (x : Fin (2 ^ n)) (hi lo : ℕ), BitVec.extractLsb hi lo { toFin := x } = BitVec.ofNat (hi - lo + 1) (↑x >>> lo)
-- Mathlib.Algebra.Star.Conjneg
conjneg_conj : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R] (f : G → R),
  conjneg ((starRingEnd (G → R)) f) = (starRingEnd (G → R)) (conjneg f)
-- Lean.Elab.App
/-- `findMethod? S fName` tries the for each namespace `S'` in the resolution order for `S` to resolve the name `S'.fname`.
If it resolves to `name`, returns `(S', name)`.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.findMethod? : Lean.Name → Lean.Name → Lean.MetaM (Option (Lean.Name × Lean.Name))
-- Mathlib.Data.Finite.Prod
Set.Finite.toFinset_prod : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (hs : s.Finite) (ht : t.Finite),
  hs.toFinset ×ˢ ht.toFinset = ⋯.toFinset
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] {f : α → β → Bool} {k : α} (h : m.WF),
  (Std.HashMap.Raw.filter f m).getKey? k = (m.getKey? k).pfilter fun x h' => f x m[x]
-- Lean.Server.References
Lean.Server.References.DocumentRefInfo.mk.injEq : ∀ (location : Lean.Lsp.Location) (module : Lean.Name) (parentInfo? : Option Lean.Server.References.ParentDecl)
  (location_1 : Lean.Lsp.Location) (module_1 : Lean.Name) (parentInfo?_1 : Option Lean.Server.References.ParentDecl),
  ({ location := location, module := module, parentInfo? := parentInfo? } =
      { location := location_1, module := module_1, parentInfo? := parentInfo?_1 }) =
    (location = location_1 ∧ module = module_1 ∧ parentInfo? = parentInfo?_1)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonSnippetString : Lean.FromJson Lean.Lsp.SnippetString
-- Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Matrix.IsHermitian.cfcAux.congr_simp : ∀ {n : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n 𝕜}
  (hA : A.IsHermitian), hA.cfcAux = hA.cfcAux
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_iUnion : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {ι : Sort u_3}
  (f : ι → Set E), IntermediateField.adjoin F (⋃ i, f i) = ⨆ i, IntermediateField.adjoin F (f i)
-- Mathlib.Analysis.Real.Cardinality
/-- The cardinality of the interval $[a, ∞)$.  -/
Cardinal.mk_Ici_real : ∀ (a : ℝ), Cardinal.mk ↑(Set.Ici a) = Cardinal.continuum
-- Mathlib.Topology.Algebra.Order.Field
tendsto_inv_atTop_zero : ∀ {𝕜 : Type u_1} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜], Filter.Tendsto (fun r => r⁻¹) Filter.atTop (nhds 0)
-- Init.Control.Except
instMonadExceptOfExceptT : (m : Type u → Type v) → (ε₁ ε₂ : Type u) → [MonadExceptOf ε₁ m] → MonadExceptOf ε₁ (ExceptT ε₂ m)
-- Mathlib.Topology.Sheaves.LocallySurjective
TopCat.Presheaf.isLocallySurjective_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X : TopCat}
  {ℱ 𝒢 : TopCat.Presheaf C X} (T : ℱ ⟶ 𝒢),
  TopCat.Presheaf.IsLocallySurjective T ↔
    ∀ (U : TopologicalSpace.Opens ↑X) (t : CategoryTheory.ToType (𝒢.obj (Opposite.op U))),
      ∀ x ∈ U,
        ∃ V,
          ∃ (x_1 : V ≤ U),
            (∃ s,
                (CategoryTheory.ConcreteCategory.hom (T.app (Opposite.op V))) s =
                  TopCat.Presheaf.restrictOpen t V x_1) ∧
              x ∈ V
-- Mathlib.Data.Set.Insert
Set.insert_comm : ∀ {α : Type u_1} (a b : α) (s : Set α), insert a (insert b s) = insert b (insert a s)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.funs.eq_1 : ∀ (x y : ZFSet.{u}), x.funs y = ZFSet.sep (x.IsFunc y) (x.prod y).powerset
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- Any continuous bijection of light profinite spaces induces an isomorphism.  -/
LightProfinite.isoOfBijective : {X Y : LightProfinite} → (f : X ⟶ Y) → Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f) → (X ≅ Y)
-- Mathlib.Algebra.BigOperators.Balance
/-- The balancing of a function, namely the function minus its average.  -/
Fintype.balance : {ι : Type u_1} → {G : Type u_4} → [Fintype ι] → [inst : AddCommGroup G] → [Module ℚ≥0 G] → (ι → G) → ι → G
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.val_vadd : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] {p : SubAddAction R M} (r : R) (x : ↥p), ↑(r +ᵥ x) = r +ᵥ ↑x
-- Init.Data.Vector.Lemmas
Vector.extract_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} {h : xs.size = n} {start stop : ℕ},
  (Vector.mk xs h).extract start stop = Vector.mk (xs.extract start stop) ⋯
-- Mathlib.Topology.Neighborhoods
interior_eq_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, interior s = {x | nhds x ≤ Filter.principal s}
-- Mathlib.Tactic.FBinop
/-- `fbinop% f x y` elaborates `f x y` for `x : S α` and `y : S' β`, taking into account
any coercions that the "functors" `S` and `S'` possess.  -/
FBinopElab.prodSyntax : Lean.ParserDescr
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Term.toParserDescr.processSepBy : Lean.Syntax → Lean.Elab.Term.ToParserDescrM (Lean.Term × ℕ)
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n)`. Convert the heap to a list in arbitrary order.  -/
Batteries.BinomialHeap.toListUnordered : {α : Type u} → {le : α → α → Bool} → Batteries.BinomialHeap α le → List α
-- Mathlib.Control.Traversable.Basic
instLawfulTraversableId : LawfulTraversable Id
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
/-- The alternating face map complex, on morphisms  -/
AlgebraicTopology.AlternatingCofaceMapComplex.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : CategoryTheory.CosimplicialObject C} →
        (X ⟶ Y) →
          (AlgebraicTopology.AlternatingCofaceMapComplex.obj X ⟶ AlgebraicTopology.AlternatingCofaceMapComplex.obj Y)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn'_rio : ∀ {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred]
  [inst_4 : Std.PRange.Least? α] [inst_5 : LT α] [inst_6 : DecidableLT α] [inst_7 : Std.PRange.UpwardEnumerable α]
  [inst_8 : Std.Rxo.IsAlwaysFinite α] [inst_9 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_10 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_11 : Std.PRange.LawfulUpwardEnumerableLT α]
  {xs : Std.Rio α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
  (inv : Std.Internal.Do.Invariant xs.toList β Pred) {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur ⋯ b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn' xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
/-- The unit isomorphism of the equivalence `equivalence₁` between `A` and `B'`.  -/
AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso : {A : Type u_1} →
  {A' : Type u_2} →
    {B' : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} A] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] →
            {eA : A ≌ A'} →
              {e' : A' ≌ B'} →
                {F : CategoryTheory.Functor A B'} →
                  (eA.functor.comp e'.functor ≅ F) → (CategoryTheory.Functor.id A ≅ F.comp (e'.inverse.comp eA.inverse))
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor : ∀ {𝒮 : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮),
  (CategoryTheory.Functor.Fiber.inducedFunctor ⋯).EssSurj
-- Init.Data.Float.Model.Float
/-- Converts a `Float.Model` to an `ISize`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.toISize : Float.Model → ISize
-- Init.Data.BitVec.Basic
BitVec.instHShiftLeft : {m n : ℕ} → HShiftLeft (BitVec m) (BitVec n) (BitVec m)
-- Mathlib.CategoryTheory.Generator.Type
CategoryTheory.Types.isSeparator_punit : CategoryTheory.IsSeparator PUnit.{u + 1}
-- Mathlib.Data.Finsupp.PointwiseSMul
/-- **Alias** of `Set.SMulAntidiagonal.finite_of_finite_fst`. -/
Finsupp.finite_vaddAntidiagonal : ∀ {G : Type u_1} {P : Type u_2} {s : Set G} [inst : SMul G P] [IsLeftCancelSMul G P],
  s.Finite → ∀ (t : Set P) (p : P), (s.smulAntidiagonal t p).Finite
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.Hom.equivContinuousMap_symm_apply : ∀ (X Y : TopCat) (f : C(↑X, ↑Y)), (TopCat.Hom.equivContinuousMap X Y).symm f = TopCat.ofHom f
-- Init.Data.List.ToArray
Array.flatMap.eq_1 : ∀ {α : Type u} {β : Type u_1} (f : α → Array β) (as : Array α),
  Array.flatMap f as = Array.foldl (fun bs a => bs ++ f a) #[] as
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.instFaithfulInclusion : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C),
  (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.inclusion F).Faithful
-- Mathlib.Algebra.Polynomial.Inductions
Polynomial.divX_hom_toFun : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, Polynomial.divX_hom p = p.divX
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.FullSubcategory.comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  {X Y Z : P.FullSubcategory} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.zeroLocus.eq_1 : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (s : Set ↑(X.presheaf.obj (Opposite.op U))),
  X.zeroLocus s = X.toRingedSpace.zeroLocus s
-- Lean.Data.NameMap.Basic
Lean.NameSSet.instInhabited : Inhabited Lean.NameSSet
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.postcomposeEquivalence_inverse : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ≅ G),
  (CategoryTheory.Limits.Cone.postcomposeEquivalence α).inverse = CategoryTheory.Limits.Cone.postcompose α.inv
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ →
    ∀ {i₀ i₁ i₂ : ι} (f : i₀ ⟶ i₁) (g : i₁ ⟶ i₂) (fg : i₀ ⟶ i₂) (hfg : CategoryTheory.CategoryStruct.comp f g = fg),
      CategoryTheory.Limits.IsZero ((X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f)) →
        CategoryTheory.Limits.IsZero ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)) →
          CategoryTheory.IsIso ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg hfg))
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.varFinset.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} [inst : DecidableEq α] (x : L.Term α),
  x.varFinset =
    match x with
    | FirstOrder.Language.var i => {i}
    | FirstOrder.Language.func _f ts => Finset.univ.biUnion fun i => (ts i).varFinset
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.inv_appTop : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f],
  AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.inv f) =
    CategoryTheory.inv (AlgebraicGeometry.Scheme.Hom.appTop f)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientBot_apply : ∀ {G : Type u} [inst : AddGroup G] (a : G ⧸ (AddMonoidHom.id G).ker),
  QuotientAddGroup.quotientBot a = (QuotientAddGroup.kerLift (AddMonoidHom.id G)) a
-- Mathlib.NumberTheory.NumberField.House
/-- `asiegel K a` is the integer matrix of the coefficients of the
product of matrix elements and basis vectors.  -/
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.asiegel : (K : Type u_1) →
  [inst : Field K] →
    [NumberField K] →
      {α : Type u_2} →
        {β : Type u_3} → Matrix α β (NumberField.RingOfIntegers K) → Matrix (α × (K →+* ℂ)) (β × (K →+* ℂ)) ℤ
-- Mathlib.Data.List.Lattice
_private.Mathlib.Data.List.Lattice.0.List.bagInter.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) →
      ((x : List α) → motive [] x) →
        ((x : List α) → (x = [] → False) → motive x []) →
          ((a : α) → (l₁ l₂ : List α) → (l₂ = [] → False) → motive (a :: l₁) l₂) → motive x x_1
-- Mathlib.Order.InitialSeg
PrincipalSeg.irrefl : ∀ {α : Type u_1} {r : α → α → Prop} [IsWellOrder α r] (f : PrincipalSeg r r), False
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.alter.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Option ((a : α) × β a) → Sort u_3) →
      (x : Option ((a : α) × β a)) →
        (x = none → motive none) → ((k' : α) → (v' : β k') → x = some ⟨k', v'⟩ → motive (some ⟨k', v'⟩)) → motive x
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Multiset.pow_smul_esymm : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : Monoid S] [inst_2 : DistribMulAction S R]
  [IsScalarTower S R R] [SMulCommClass S R R] (s : S) (n : ℕ) (m : Multiset R),
  s ^ n • m.esymm n = (Multiset.map (fun x => s • x) m).esymm n
-- Mathlib.Data.Matrix.Composition
/-- An `I` by `J` matrix where each entry is a `K` by `L` matrix is equivalent to
an `I × K` by `J × L` matrix  -/
Matrix.comp : (I : Type u_1) →
  (J : Type u_2) →
    (K : Type u_3) → (L : Type u_4) → (R : Type u_5) → Matrix I J (Matrix K L R) ≃ Matrix (I × K) (J × L) R
-- Mathlib.RingTheory.Bialgebra.Hom
/-- Given `R`-algebras `A, B` with comultiplication maps `Δ_A, Δ_B` and counit maps
`ε_A, ε_B`, an `R`-bialgebra homomorphism `A →ₐc[R] B` is an `R`-algebra map `f` such that
`ε_B ∘ f = ε_A` and `(f ⊗ f) ∘ Δ_A = Δ_B ∘ f`.  -/
«term_→ₐc_» : Lean.TrailingParserDescr
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.isFlat_iff_closure_eq : ∀ {α : Type u_2} {M : Matroid α} {F : Set α}, M.IsFlat F ↔ M.closure F = F
-- Lean.Widget.UserWidget
Lean.Widget.UserWidgetDefinition.mk.inj : ∀ {name javascript name_1 javascript_1 : String},
  { name := name, javascript := javascript } = { name := name_1, javascript := javascript_1 } →
    name = name_1 ∧ javascript = javascript_1
-- Mathlib.Topology.Algebra.OpenSubgroup
Submodule.isOpen_mono : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : TopologicalSpace M]
  [IsTopologicalAddGroup M] [inst_4 : Module R M] {U P : Submodule R M}, U ≤ P → IsOpen ↑U → IsOpen ↑P
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.norm.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.norm c) = 1 + sizeOf c
-- Aesop.RuleTac.GoalDiff
/-- Is the old goal's target defeq to the new goal's target?  -/
Aesop.GoalDiff.targetChanged : Aesop.GoalDiff → Bool
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.mapBicone_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {J : Type w₁} {f : J → C}
  (b : CategoryTheory.Limits.Bicone f) (j : J), (F.mapBicone b).ι j = F.map (b.ι j)
-- Init.Data.Float.Float
instReprFloat : Repr Float
-- Mathlib.CategoryTheory.Localization.Construction
/-- If `F₁` and `F₂` are functors `W.Localization ⥤ D` and if we have
`τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂`, we shall define a natural transformation `F₁ ⟶ F₂`.
This is the `app` field of this natural transformation.  -/
CategoryTheory.Localization.Construction.NatTransExtension.app : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {D : Type uD} →
        [inst_1 : CategoryTheory.Category.{uD', uD} D] →
          {F₁ F₂ : CategoryTheory.Functor W.Localization D} →
            (W.Q.comp F₁ ⟶ W.Q.comp F₂) → (X : W.Localization) → F₁.obj X ⟶ F₂.obj X
-- Aesop.Script.Step
Aesop.Script.LazyStep.BuildInput.postGoals : {α : Type} → Aesop.Script.LazyStep.BuildInput α → α → Array Lean.MVarId
-- Mathlib.Algebra.Ring.Semiconj
SemiconjBy.add_left : ∀ {R : Type u} [inst : Distrib R] {a b x y : R}, SemiconjBy a x y → SemiconjBy b x y → SemiconjBy (a + b) x y
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.inhabited : {R : Type u} → [inst : Semiring R] → Inhabited (Polynomial R)
-- Mathlib.LinearAlgebra.Basis.Submodule
Module.Basis.restrictScalars.congr_simp : ∀ {ι : Type u_1} (R : Type u_3) {M : Type u_5} {S : Type u_7} [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : Ring S] [inst_3 : Nontrivial S] [inst_4 : AddCommGroup M] [inst_5 : Algebra R S] [inst_6 : Module S M]
  [inst_7 : Module R M] [inst_8 : IsScalarTower R S M] [inst_9 : Module.IsTorsionFree R S] (b : Module.Basis ι S M),
  Module.Basis.restrictScalars R b = Module.Basis.restrictScalars R b
-- Mathlib.Algebra.Order.Interval.Basic
instSubInterval : {α : Type u_2} →
  [inst : Preorder α] →
    [inst_1 : AddCommSemigroup α] → [inst_2 : Sub α] → [OrderedSub α] → [AddLeftMono α] → Sub (Interval α)
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
CategoryTheory.Functor.HasPointwiseRightDerivedFunctorAt.hasColimit : ∀ {C : Type u₁} {D : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  (F : CategoryTheory.Functor C H) (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [L.IsLocalization W] (X : C) [F.HasPointwiseRightDerivedFunctorAt W X], L.HasPointwiseLeftKanExtensionAt F (L.obj X)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_iInf : ∀ {α : Type u_2} [inst : TopologicalSpace α] {ι : Sort u_4} (s : ι → TopologicalSpace.Closeds α),
  ↑(⨅ i, s i) = ⋂ i, ↑(s i)
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₂₀.isPushout : CategoryTheory.IsPushout (SSet.stdSimplex.δ 1) (SSet.stdSimplex.δ 1) SSet.horn₂₀.ι₀₁ SSet.horn₂₀.ι₀₂
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A non-unital normed ring is a not-necessarily-unital ring
endowed with a norm which satisfies the inequality `‖x y‖ ≤ ‖x‖ ‖y‖`.  -/
NonUnitalNormedRing : Type u_5 → Type u_5
-- Mathlib.Algebra.Lie.SkewAdjoint
skewAdjointLieSubalgebraEquiv.eq_1 : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M) {N : Type w} [inst_3 : AddCommGroup N] [inst_4 : Module R N] (e : N ≃ₗ[R] M),
  skewAdjointLieSubalgebraEquiv B e =
    LieEquiv.ofSubalgebras (skewAdjointLieSubalgebra (LinearMap.compl₁₂ B ↑e ↑e)) (skewAdjointLieSubalgebra B) e.lieConj
      ⋯