mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.PNat.Factors
PrimeMultiset.coePNat_ofPrime : ∀ (p : Nat.Primes), (PrimeMultiset.ofPrime p).toPNatMultiset = {↑p}
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
/-- `F` creates all finite colimits.  -/
CategoryTheory.Limits.CreatesFiniteColimits.createsFiniteColimits : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {D : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        {F : CategoryTheory.Functor C D} →
          [self : CategoryTheory.Limits.CreatesFiniteColimits F] →
            (J : Type) →
              [inst_2 : CategoryTheory.SmallCategory J] →
                [CategoryTheory.FinCategory J] → CategoryTheory.CreatesColimitsOfShape J F
-- Lean.Elab.Arg
Lean.Elab.Term.expandApp : Lean.Syntax → Lean.MetaM (Lean.Syntax × Array Lean.Elab.Term.NamedArg × Array Lean.Elab.Term.Arg × Bool)
-- Mathlib.Logic.Function.Basic
/-- An involution commutes across an equality. Compare to `Function.Injective.eq_iff`.  -/
Function.Involutive.eq_iff : ∀ {α : Sort u} {f : α → α}, Function.Involutive f → ∀ {x y : α}, f x = y ↔ x = f y
-- Mathlib.Data.Sym.Sym2
Sym2.mk_isDiag_iff : ∀ {α : Type u_1} {x y : α}, s(x, y).IsDiag ↔ x = y
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.toList_prependMap_eq_append : ∀ {α : Type u} {β : α → Type v} (t : Std.DTreeMap.Internal.Impl α β) (it : Std.DTreeMap.Internal.Zipper α β),
  (Std.DTreeMap.Internal.Zipper.prependMap t it).toList = t.toList ++ it.toList
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
/-- The isomorphism between `MvPolynomial (Option ι) R` and the polynomial ring over
the algebra generated by an algebraically independent family.  -/
AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin : {ι : Type u} →
  {R : Type u_2} →
    {A : Type v} →
      {x : ι → A} →
        [inst : CommRing R] →
          [inst_1 : CommRing A] →
            [inst_2 : Algebra R A] →
              AlgebraicIndependent R x → MvPolynomial (Option ι) R ≃+* Polynomial ↥(Algebra.adjoin R (Set.range x))
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
ContinuousLinearMap.coe_restrictScalarsₗ : ∀ {A : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {R : Type u_4} {S : Type u_5} [inst : Semiring A] [inst_1 : Semiring R]
  [inst_2 : Semiring S] [inst_3 : AddCommMonoid M₁] [inst_4 : Module A M₁] [inst_5 : Module R M₁]
  [inst_6 : TopologicalSpace M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module A M₂] [inst_9 : Module R M₂]
  [inst_10 : TopologicalSpace M₂] [inst_11 : LinearMap.CompatibleSMul M₁ M₂ R A] [inst_12 : Module S M₂]
  [inst_13 : ContinuousConstSMul S M₂] [inst_14 : SMulCommClass A S M₂] [inst_15 : SMulCommClass R S M₂]
  [inst_16 : ContinuousAdd M₂],
  ⇑(ContinuousLinearMap.restrictScalarsₗ A M₁ M₂ R S) = ContinuousLinearMap.restrictScalars R
-- Mathlib.Order.Bounds.Basic
upperBounds_insert : ∀ {α : Type u_1} [inst : Preorder α] (a : α) (s : Set α), upperBounds (insert a s) = Set.Ici a ∩ upperBounds s
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- If `x` is an algebraic element of field `K`, then its minimal polynomial has degree
`[K(x) : K]`.  -/
IntermediateField.adjoin.finrank : ∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {x : L},
  IsIntegral K x → Module.finrank K ↥K⟮x⟯ = (minpoly K x).natDegree
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.IsUniversalColimit.map_reflective : ∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] {Gl : CategoryTheory.Functor C D}
  {Gr : CategoryTheory.Functor D C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful] {F : CategoryTheory.Functor J D}
  {c : CategoryTheory.Limits.Cocone (F.comp Gr)},
  CategoryTheory.IsUniversalColimit c →
    ∀ [∀ (X : D) (f : X ⟶ Gl.obj c.pt), CategoryTheory.Limits.HasPullback (Gr.map f) (adj.unit.app c.pt)]
      [∀ (X : D) (f : X ⟶ Gl.obj c.pt),
          CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (Gr.map f) (adj.unit.app c.pt)) Gl],
      CategoryTheory.IsUniversalColimit (Gl.mapCocone c)
-- Mathlib.Data.PFun
PFun.lift_injective : ∀ {α : Type u_1} {β : Type u_2}, Function.Injective PFun.lift
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.IsUniversal.of_subsingleton : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [Subsingleton V], G.IsUniversal v
-- Mathlib.Computability.PartrecCode
/-- The interpretation of a `Nat.Partrec.Code` as a partial function.
* `Nat.Partrec.Code.zero`: The constant zero function.
* `Nat.Partrec.Code.succ`: The successor function.
* `Nat.Partrec.Code.left`: Left unpairing of a pair of ℕ (encoded by `Nat.pair`)
* `Nat.Partrec.Code.right`: Right unpairing of a pair of ℕ (encoded by `Nat.pair`)
* `Nat.Partrec.Code.pair`: Pairs the outputs of argument codes using `Nat.pair`.
* `Nat.Partrec.Code.comp`: Composition of two argument codes.
* `Nat.Partrec.Code.prec`: Primitive recursion. Given an argument of the form `Nat.pair a n`:
  * If `n = 0`, returns `eval cf a`.
  * If `n = succ k`, returns `eval cg (pair a (pair k (eval (prec cf cg) (pair a k))))`
* `Nat.Partrec.Code.rfind'`: Minimization starting at a provided value. Given an argument of the
  form `Nat.pair a m`, returns the least `n ≥ m` such that `eval cf (pair a n) = 0`, if such an `n`
  exists and if `eval cf (pair a k)` terminates for all `m ≤ k ≤ n`.
 -/
Nat.Partrec.Code.eval : Nat.Partrec.Code → ℕ →. ℕ
-- Mathlib.RingTheory.Localization.Away.Basic
/-- The sheaf condition for the structure sheaf on `Spec R`
for a covering of the whole prime spectrum by basic opens.  -/
Localization.existsUnique_algebraMap_eq_of_span_eq_top : ∀ {R : Type u_1} [inst : CommSemiring R] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (f : (a : ↑s) → Localization.Away ↑a),
      (∀ (a b : ↑s),
          (IsLocalization.Away.awayToAwayRight ↑a ↑b) (f a) = (IsLocalization.Away.awayToAwayLeft ↑b ↑a) (f b)) →
        ∃! r, ∀ (a : ↑s), (algebraMap R (Localization.Away ↑a)) r = f a
-- Mathlib.Order.Basic
Pi.sdiff_def : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → SDiff (π i)] (x y : (i : ι) → π i), x \ y = fun i => x i \ y i
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk_prodMk : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ι → Type u_8}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k l : ι),
        i ≠ k →
          i ≠ l →
            j ≠ k → j ≠ l → ProbabilityTheory.Kernel.IndepFun (fun a => (f i a, f j a)) (fun a => (f k a, f l a)) κ μ
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_hom_nonempty : ∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] {l : List M} {F : Type u_8}
  [inst_2 : FunLike F M N] [MulHomClass F M N] (f : F), l ≠ [] → (List.map (⇑f) l).prod = f l.prod
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rcc_succ_right_eq_append_map : ∀ {m n : ℕ}, m ≤ n + 1 → (m...=n + 1).toArray = #[m] ++ Array.map (fun x => x + 1) (m...=n).toArray
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- The canonical natural transformation `𝟭 (Arrow C) ⟶ functor f`.  -/
CategoryTheory.SmallObject.ε : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) →
          [inst_1 : CategoryTheory.Limits.HasPushouts C] →
            [inst_2 :
                ∀ {X S : C} (πX : X ⟶ S),
                  CategoryTheory.Limits.HasColimitsOfShape
                    (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] →
              CategoryTheory.Functor.id (CategoryTheory.Arrow C) ⟶ CategoryTheory.SmallObject.functor f
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flattenAfter.match_1.eq_2 : ∀ {α α₂ β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m (Std.IterM m β)]
  {it₁ : Std.IterM m (Std.IterM m β)} (motive : it₁.Step → Sort u_3) (it₁' : Std.IterM m (Std.IterM m β))
  (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁'))
  (h_1 :
    (it₁' : Std.IterM m (Std.IterM m β)) →
      (it₂' : Std.IterM m β) →
        (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' it₂')) → motive ⟨Std.IterStep.yield it₁' it₂', h⟩)
  (h_2 :
    (it₁' : Std.IterM m (Std.IterM m β)) →
      (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it₁', h⟩ with
    | ⟨Std.IterStep.yield it₁' it₂', h⟩ => h_1 it₁' it₂' h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it₁' h
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.top_induce_pair_connected_of_adj : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Adj u v → (⊤.induce {u, v}).Connected
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
/-- The inclusion functor `BifibrantObject C ⥤ FibrantObject C`.  -/
HomotopicalAlgebra.BifibrantObject.ιFibrantObject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C] →
      [inst_2 : CategoryTheory.Limits.HasInitial C] →
        [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C] →
          [inst_4 : CategoryTheory.Limits.HasTerminal C] →
            CategoryTheory.Functor (HomotopicalAlgebra.BifibrantObject C) (HomotopicalAlgebra.FibrantObject C)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioi_union_Iio_of_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, b < a → Set.Ioi b ∪ Set.Iio a = Set.univ
-- Std.Data.HashSet.Lemmas
Std.HashSet.ofList_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {hd : α} {tl : List α},
  Std.HashSet.ofList (hd :: tl) = (∅.insert hd).insertMany tl
-- Std.Data.DHashMap.Basic
/-- Two hash maps are equivalent in the sense of `Equiv` iff
all the keys and values are equal.
 -/
Std.DHashMap.«term_~m_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.symm_bijective : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁}, Function.Bijective Path.Homotopy.symm
-- Init.Prelude
/-- The word size of the current platform may be 64 or 32 bits.
 -/
System.Platform.numBits_eq : System.Platform.numBits = 32 ∨ System.Platform.numBits = 64
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.Aesop.phase.quot : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.Notation
/-- Attempt to find the trivial model on a normed space.  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findModelInner.fromNormedSpace : Lean.Expr → Lean.Elab.TermElabM Manifold.Elab.FindModelResult
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.inclusion_apply : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I₁ I₂ : LieIdeal R L}
  (h : I₁ ≤ I₂) (x : ↥I₁), (LieIdeal.inclusion h) x = ⟨↑x, ⋯⟩
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_uIcc_succ : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∑ i ∈ Finset.uIcc a.succ b.succ, f i = ∑ i ∈ Finset.uIcc a b, f i.succ
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.p_descOpcycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁)
  {A : C} (x : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ A)
  (hx : CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) x = 0),
  CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n₁) (X.descOpcycles f g n₀ n₁ hn₁ x hx) = x
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubmonoid.multiples_le_zmultiples : ∀ {G : Type u_2} [inst : AddGroup G] (g : G), AddSubmonoid.multiples g ≤ (AddSubgroup.zmultiples g).toAddSubmonoid
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.instInhabitedConfig : Inhabited Lean.Meta.Sym.Simp.Config
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.domDomRestrict_aux_right : ∀ {ι : Sort u_2} [inst : DecidableEq ι] (P : ι → Prop) [inst_1 : DecidablePred P] {M₁ : ι → Type u_1}
  [inst_2 : DecidableEq { a // ¬P a }] (x : (i : { a // P a }) → M₁ ↑i) (z : (i : { a // ¬P a }) → M₁ ↑i)
  (i : { a // ¬P a }) (c : M₁ ↑i),
  (fun j => if h : P j then x ⟨j, h⟩ else Function.update z i c ⟨j, h⟩) =
    Function.update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) c
-- Mathlib.Logic.Equiv.Defs
Equiv.arrowCongr'_apply : ∀ {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (hα : α₁ ≃ α₂) (hβ : β₁ ≃ β₂) (f : α₁ → β₁) (a : α₂),
  (hα.arrowCongr' hβ) f a = hβ (f (hα.symm a))
-- Mathlib.Data.Sym.Sym2
Sym2.inductionOn₂ : ∀ {α : Type u_1} {β : Type u_2} {f : Sym2 α → Sym2 β → Prop} (i : Sym2 α) (j : Sym2 β),
  (∀ (a₁ a₂ : α) (b₁ b₂ : β), f s(a₁, a₂) s(b₁, b₂)) → f i j
-- Std.Do.WP.Monad
Std.Do.State.instWPMonad : {σ : Type u_1} → Std.Do.WPMonad (StateM σ) (Std.Do.PostShape.arg σ Std.Do.PostShape.pure)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_le_minKey!_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, t.erase k ≠ ∅ → (cmp t.minKey! (t.erase k).minKey!).isLE = true
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Header.binders : Lean.Elab.Deriving.Header → Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)
-- Mathlib.Analysis.Analytic.Basic
AnalyticAt.eventually_continuousAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E},
  AnalyticAt 𝕜 f x → ∀ᶠ (y : E) in nhds x, ContinuousAt f y
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_left_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b),
  (F.mapComp (CategoryTheory.CategoryStruct.id a) f).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a).hom (F.map f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom
        (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv))
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
/-- The (degenerate) subsimplex of `Λ[n+2, i]` concentrated in vertex `k`.  -/
SSet.horn.const : (n : ℕ) → (i : Fin (n + 3)) → Fin (n + 3) → (m : SimplexCategoryᵒᵖ) → ↑((SSet.horn (n + 2) i).obj m)
-- Mathlib.CategoryTheory.NatTrans
/-- `NatTrans.mk'` is the dual of `NatTrans.mk`, which we need for `to_dual`.
Please avoid using this directly.  -/
CategoryTheory.NatTrans.mk' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor C D} →
          (app : (X : C) → G.obj X ⟶ F.obj X) →
            (∀ ⦃X Y : C⦄ (f : Y ⟶ X),
                CategoryTheory.CategoryStruct.comp (app Y) (F.map f) =
                  CategoryTheory.CategoryStruct.comp (G.map f) (app X)) →
              CategoryTheory.NatTrans G F
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.eq_of_true : ∀ {a b : Prop}, a → b → a = b
-- Mathlib.CategoryTheory.GuitartExact.Opposite
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence_counitIso : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  {X₃ : C₃ᵒᵖ} {X₂ : C₂ᵒᵖ} (g : B.op.obj X₃ ⟶ R.op.obj X₂),
  (w.structuredArrowRightwardsOpEquivalence g).counitIso =
    CategoryTheory.Iso.refl
      ((CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.inverse w g).comp
        (CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor w g))
-- Batteries.Data.Random.MersenneTwister
/-- Twist value (`r`).  -/
Batteries.Random.MersenneTwister.Config.maskBits : (self : Batteries.Random.MersenneTwister.Config) → Fin self.wordSize
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
/-- Fixed points of iSup of subgroups is intersection  -/
fixedPoints_subgroup_iSup : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α] {ι : Sort u_3} {P : ι → Subgroup M},
  MulAction.fixedPoints (↥(iSup P)) α = ⋂ i, MulAction.fixedPoints (↥(P i)) α
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftUnshift_units_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n' a : ℤ}
  (γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ)
  (hn : n + a = n') (x : Rˣ), (x • γ).leftUnshift n hn = x • γ.leftUnshift n hn
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.map_preimage : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Full] {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (F.preimage f) = f
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  [inst_2 : SizeOf C] [inst_3 : SizeOf D] (d : {X : Dᵒᵖ} → ↑(R.obj X) →+ ↑(M.obj X))
  (d_mul :
    autoParam (∀ {X : Dᵒᵖ} (a b : ↑(R.obj X)), d (a * b) = a • d b + b • d a)
      PresheafOfModules.Derivation.d_mul._autoParam)
  (d_map :
    autoParam
      (∀ {X Y : Dᵒᵖ} (f : X ⟶ Y) (x : ↑(R.obj X)),
        d ((CategoryTheory.ConcreteCategory.hom (R.map f)) x) = (CategoryTheory.ConcreteCategory.hom (M.map f)) (d x))
      PresheafOfModules.Derivation.d_map._autoParam)
  (d_app :
    autoParam (∀ {X : Cᵒᵖ} (a : ↑(S.obj X)), d ((CategoryTheory.ConcreteCategory.hom (φ.app X)) a) = 0)
      PresheafOfModules.Derivation.d_app._autoParam),
  sizeOf { d := d, d_mul := d_mul, d_map := d_map, d_app := d_app } = 1
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_eq : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [hE : CompleteSpace E] (f : α → E) (hf : MeasureTheory.Integrable f μ),
  ∫ (a : α), f a ∂μ = MeasureTheory.L1.integral (MeasureTheory.Integrable.toL1 f hf)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_mem_of_nonempty : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  s.Nonempty → s.sup f ∈ f '' ↑s
-- Lean.Level
_private.Lean.Level.0.Lean.Level.normLtAux.match_1.eq_3 : ∀ (motive : Lean.Level → ℕ → Lean.Level → ℕ → Sort u_1) (l₁₁ l₁₂ : Lean.Level) (k₁ : ℕ) (l₂₁ l₂₂ : Lean.Level) (k₂ : ℕ)
  (h_1 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁.succ k₁ l₂ k₂)
  (h_2 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁ k₁ l₂.succ k₂)
  (h_3 :
    (l₁ l₁₁ l₁₂ : Lean.Level) →
      l₁ = l₁₁.max l₁₂ →
        (k₁ : ℕ) → (l₂ l₂₁ l₂₂ : Lean.Level) → l₂ = l₂₁.max l₂₂ → (k₂ : ℕ) → motive (l₁₁.max l₁₂) k₁ (l₂₁.max l₂₂) k₂)
  (h_4 :
    (l₁ l₁₁ l₁₂ : Lean.Level) →
      l₁ = l₁₁.imax l₁₂ →
        (k₁ : ℕ) →
          (l₂ l₂₁ l₂₂ : Lean.Level) → l₂ = l₂₁.imax l₂₂ → (k₂ : ℕ) → motive (l₁₁.imax l₁₂) k₁ (l₂₁.imax l₂₂) k₂)
  (h_5 :
    (n₁ : Lean.Name) →
      (k₁ : ℕ) → (n₂ : Lean.Name) → (k₂ : ℕ) → motive (Lean.Level.param n₁) k₁ (Lean.Level.param n₂) k₂)
  (h_6 :
    (n₁ : Lean.LMVarId) →
      (k₁ : ℕ) → (n₂ : Lean.LMVarId) → (k₂ : ℕ) → motive (Lean.Level.mvar n₁) k₁ (Lean.Level.mvar n₂) k₂)
  (h_7 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁ k₁ l₂ k₂),
  (match l₁₁.max l₁₂, k₁, l₂₁.max l₂₂, k₂ with
    | l₁.succ, k₁, l₂, k₂ => h_1 l₁ k₁ l₂ k₂
    | l₁, k₁, l₂.succ, k₂ => h_2 l₁ k₁ l₂ k₂
    | l₁@h:(l₁₁.max l₁₂), k₁, l₂@h_8:(l₂₁.max l₂₂), k₂ => h_3 l₁ l₁₁ l₁₂ h k₁ l₂ l₂₁ l₂₂ h_8 k₂
    | l₁@h:(l₁₁.imax l₁₂), k₁, l₂@h_8:(l₂₁.imax l₂₂), k₂ => h_4 l₁ l₁₁ l₁₂ h k₁ l₂ l₂₁ l₂₂ h_8 k₂
    | Lean.Level.param n₁, k₁, Lean.Level.param n₂, k₂ => h_5 n₁ k₁ n₂ k₂
    | Lean.Level.mvar n₁, k₁, Lean.Level.mvar n₂, k₂ => h_6 n₁ k₁ n₂ k₂
    | l₁, k₁, l₂, k₂ => h_7 l₁ k₁ l₂ k₂) =
    h_3 (l₁₁.max l₁₂) l₁₁ l₁₂ ⋯ k₁ (l₂₁.max l₂₂) l₂₁ l₂₂ ⋯ k₂
-- Mathlib.RingTheory.LocalRing.Quotient
_private.Mathlib.RingTheory.LocalRing.Quotient.0.IsLocalRing.termPS : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.Hom
Algebra.smul_units_def : ∀ {R : Type u} (A : Type v) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (f : A →ₐ[R] A)
  (x : Aˣ), f • x = (Units.map ↑f) x
-- Mathlib.Data.Multiset.Defs
Multiset.instCoeList : {α : Type u_1} → Coe (List α) (Multiset α)
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.inr_triangleδ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ) (CochainComplex.mappingCone.triangle φ).mor₃ = 0
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.core.inj : ∀ {e : Lean.Expr} {lhs rhs : Lean.Grind.CommRing.Expr} {e_1 : Lean.Expr} {lhs_1 rhs_1 : Lean.Grind.CommRing.Expr},
  Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.core e lhs rhs =
      Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.core e_1 lhs_1 rhs_1 →
    e = e_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.exs.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} (_n : ℕ) (φ : L.BoundedFormula α (_n + 1)), φ.exs = φ.ex.exs
-- Init.Data.Nat.Lemmas
Nat.mul_right_cancel : ∀ {n m k : ℕ}, 0 < m → n * m = k * m → n = k
-- Init.Data.Slice.Array.Lemmas
Array.size_mkSlice_rio : ∀ {α : Type u_1} {xs : Array α} {hi : ℕ}, Std.Slice.size (Std.Rio.Sliceable.mkSlice xs *...hi) = min hi xs.size
-- Mathlib.NumberTheory.SelbergSieve
SelbergSieve.mk.sizeOf_spec : ∀ (toBoundingSieve : BoundingSieve) (level : ℝ) (one_le_level : 1 ≤ level),
  sizeOf { toBoundingSieve := toBoundingSieve, level := level, one_le_level := one_le_level } =
    1 + sizeOf toBoundingSieve + sizeOf level + sizeOf one_le_level
-- Mathlib.Order.Defs.Unbundled
/-- `MaximalFor P f i` means that `f i` is maximal over all `i` satisfying `P`.  -/
MaximalFor : {ι : Sort u_1} → {α : Type u_2} → [LE α] → (ι → Prop) → (ι → α) → ι → Prop
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableAt.clm_postcomp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {f : M → F₂ →L[𝕜] F₃} {x : M},
  MDiffAt f x → (MDiffAt fun y => ContinuousLinearMap.postcomp F₁ (f y)) x