mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.Defs
/-- Decomposition of a type `X` as a disjoint union of its orbits under a group action.
Phrased as a set union. See `MulAction.selfEquivSigmaOrbits` for the type isomorphism.  -/
MulAction.univ_eq_iUnion_orbit : ∀ (G : Type u_1) (α : Type u_2) [inst : Group G] [inst_1 : MulAction G α], Set.univ = ⋃ x, x.orbit
-- Init.Data.UInt.BasicAux
BitVec.toNat.eq_1 : ∀ {w : ℕ} (x : BitVec w), x.toNat = ↑x.toFin
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
/-- A `MorphComponents` can be precomposed with a morphism of simplicial objects.  -/
AlgebraicTopology.DoldKan.MorphComponents.preComp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X X' : CategoryTheory.SimplicialObject C} →
      {n : ℕ} →
        {Z : C} →
          AlgebraicTopology.DoldKan.MorphComponents X n Z → (X' ⟶ X) → AlgebraicTopology.DoldKan.MorphComponents X' n Z
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalAddGroup.IsSES.integrate_apply : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : AddGroup A] [inst_1 : AddGroup B]
  [inst_2 : AddGroup C] [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C]
  {φ : A →+ B} {ψ : B →+ C} (H : TopologicalAddGroup.IsSES φ ψ) [inst_6 : IsTopologicalAddGroup A]
  [inst_7 : IsTopologicalAddGroup B] [inst_8 : NormedAddCommGroup E] [inst_9 : MeasurableSpace A]
  [inst_10 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [inst_11 : NormedSpace ℝ E]
  [inst_12 : IsTopologicalAddGroup C] [inst_13 : LocallyCompactSpace B] [inst_14 : MeasurableSpace C]
  [inst_15 : BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsAddHaarMeasure]
  (f : CompactlySupportedContinuousMap B E), (H.integrate μA μC) f = ∫ (c : C), ((H.pushforward μA) f) c ∂μC
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The pseudofunctor from `Schemeᵒᵖ` to the bicategory of adjunctions which sends
a scheme `X` to the category `X.Modules` of sheaves of modules over `X`.
(This contains both the covariant and the contravariant functorialities of
these categories.)  -/
AlgebraicGeometry.Scheme.Modules.pseudofunctor : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ)
  (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)
-- Mathlib.Algebra.Group.Basic
div_eq_of_eq_mul' : ∀ {G : Type u_3} [inst : CommGroup G] {a b c : G}, a = b * c → a / b = c
-- Lean.Elab.AssertExists
/-- `#import_path Foo` prints the transitive import chain that brings the declaration `Foo`
into the current file's scope.

This is useful for understanding why a particular declaration is available,
especially when debugging unexpected dependencies.
 -/
Lean.Elab.Command.elabImportPath : Lean.Elab.Command.CommandElab
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolResult : Type
-- Mathlib.Analysis.Meromorphic.Basic
/-- Finite sums of meromorphic functions are meromorphic.  -/
MeromorphicAt.sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {s : Finset ι} {G : ι → 𝕜 → E} {x : 𝕜},
  (∀ σ ∈ s, MeromorphicAt (G σ) x) → MeromorphicAt (∑ n ∈ s, G n) x
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.coe_injective_iff : ∀ {a₁ a₂ : Complex.UnitDisc}, a₁ = a₂ ↔ ↑a₁ = ↑a₂
-- Init.Data.UInt.Lemmas
UInt32.ofNat_add : ∀ (a b : ℕ), UInt32.ofNat (a + b) = UInt32.ofNat a + UInt32.ofNat b
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_singleton_eq_self`. -/
Set.diff_singleton_eq_self : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∉ s → s \ {a} = s
-- Std.Data.DTreeMap.Internal.Model
/-- General tree-traversal function. Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.explore : {α : Type u} →
  {β : α → Type v} →
    {γ : Type w} →
      [inst : Ord α] →
        (k : α → Ordering) →
          γ → (γ → Std.DTreeMap.Internal.Impl.ExplorationStep α β k → γ) → Std.DTreeMap.Internal.Impl α β → γ
-- Mathlib.RingTheory.Ideal.Over
Ideal.Quotient.algEquivOfEqComap_apply : ∀ {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  [inst_3 : Algebra A B] [inst_4 : Algebra A C] {P : Ideal B} {Q : Ideal C} (p : Ideal A) [inst_5 : Q.LiesOver p]
  [inst_6 : P.LiesOver p] {E : Type u_7} [inst_7 : EquivLike E B C] [inst_8 : AlgEquivClass E A B C] (σ : E)
  (h : P = Ideal.comap σ Q) (x : B),
  (Ideal.Quotient.algEquivOfEqComap p σ h) ((Ideal.Quotient.mk P) x) = (Ideal.Quotient.mk Q) (σ x)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.MeasureTheory.Constructions.Projective
/-- Auxiliary lemma for `measure_univ_eq`.  -/
MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq_of_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)]
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {I J : Finset ι},
  MeasureTheory.IsProjectiveMeasureFamily P → J ⊆ I → (P I) Set.univ = (P J) Set.univ
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
AddAction.IsPretransitive.of_embedding_congr : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {H : Type u_3} {β : Type u_4}
  [inst_2 : AddGroup H] [inst_3 : AddAction H β] {σ : G → H} {f : α →ₑ[σ] β} {n : Type u_5},
  Function.Surjective σ →
    Function.Bijective ⇑f → (AddAction.IsPretransitive G (n ↪ α) ↔ AddAction.IsPretransitive H (n ↪ β))
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
/-- The triangle in the standard simplex with vertices `k`, `k+1`, and `k+2`.

This constructor assumes `0 < i < n`,
which is the type of horn that occurs in the horn-filling condition of quasicategories.  -/
SSet.horn.primitiveTriangle : {n : ℕ} →
  (i : Fin (n + 4)) →
    0 < i → i < Fin.last (n + 3) → (k : ℕ) → k < n + 2 → (SSet.horn (n + 3) i).toSSet.obj (Opposite.op { len := 2 })
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash : Lean.Grind.Linarith.Expr → UInt64
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.ext' : ∀ {Δ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ), A = ⟨A.fst, ⟨A.e, ⋯⟩⟩
-- Mathlib.Tactic.NormNum.Core
/-- Read a `norm_num` extension from a declaration of the right type.  -/
Mathlib.Meta.NormNum.mkNormNumExt : Lean.Name → Lean.ImportM Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Algebra.Group.Finsupp
Finsupp.coe_add : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (f g : ι →₀ M), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- A predicate saying that `C` is "small" enough to satisfy the inductive hypothesis.  -/
Profinite.NobelingProof.contained : {I : Type u} → Set (I → Bool) → [inst : LinearOrder I] → [WellFoundedLT I] → Ordinal.{u} → Prop
-- Mathlib.Algebra.Group.End
/-- Monoid hom from the group of multiplicative automorphisms to the group of permutations.  -/
MulAut.toPerm : (M : Type u_2) → [inst : Mul M] → MulAut M →* Equiv.Perm M
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ZeroExtend
Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {newWidth : ℕ} → (aig : Std.Sat.AIG α) → aig.ExtendTarget newWidth → Std.Sat.AIG.RefVecEntry α newWidth
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pos.skip?_eq_map_skipPrefix? : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String.Slice} {pos : s.Pos},
  pos.skip? pat = Option.map String.Slice.Pos.ofSliceFrom ((s.sliceFrom pos).skipPrefix? pat)
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
/-- (Implementation).
Every cone over `F(U) ⟶ F(U ⊓ V)` and `F(V) ⟶ F(U ⊓ V)` factors through `F(U ⊔ V)`.
 -/
TopCat.Sheaf.interUnionPullbackConeLift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : TopCat} →
      (F : TopCat.Sheaf C X) →
        (U V : TopologicalSpace.Opens ↑X) →
          (s :
              CategoryTheory.Limits.PullbackCone (F.obj.map (CategoryTheory.homOfLE ⋯).op)
                (F.obj.map (CategoryTheory.homOfLE ⋯).op)) →
            s.pt ⟶ F.obj.obj (Opposite.op (U ⊔ V))
-- Std.Data.Iterators.Lemmas.Producers.Monadic.List
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.List.0.Std.Types.ListIterator.stepAsHetT_iterM.match_1.eq_1 : ∀ {β : Type u_1} (motive : List β → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (x : β) → (xs : List β) → motive (x :: xs)),
  (match [] with
    | [] => h_1 ()
    | x :: xs => h_2 x xs) =
    h_1 ()
-- Mathlib.Algebra.Homology.QuasiIso
isoOfQuasiIsoAt_hom : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L)
  (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [inst_4 : QuasiIsoAt f i],
  (isoOfQuasiIsoAt f i).hom = HomologicalComplex.homologyMap f i
-- Init.Data.SInt.Lemmas
UInt8.toInt8_sub : ∀ (a b : UInt8), (a - b).toInt8 = a.toInt8 - b.toInt8
-- Init.Data.Nat.Basic
_private.Init.Data.Nat.Basic.0.Nat.repeat.match_1.eq_2 : ∀ {α : Type u_2} (motive : ℕ → α → Sort u_1) (n : ℕ) (a : α) (h_1 : (a : α) → motive 0 a)
  (h_2 : (n : ℕ) → (a : α) → motive n.succ a),
  (match n.succ, a with
    | 0, a => h_1 a
    | n.succ, a => h_2 n a) =
    h_2 n a
-- Mathlib.Algebra.Group.Prod
MulHom.coe_prodMap : ∀ {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul M']
  [inst_3 : Mul N'] (f : M →ₙ* M') (g : N →ₙ* N'), ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- If a sequence `g` converges to some `b`, then the sequence of constant functions
`fun n ↦ fun a ↦ g n` converges to the constant function `fun a ↦ b`.  -/
Filter.Tendsto.tendstoUniformly_const : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {p : Filter ι} {g : ι → β} {b : β},
  Filter.Tendsto g p (nhds b) → TendstoUniformly (fun n x => g n) (fun x => b) p
-- Lean.Meta.Canonicalizer
Lean.Meta.Canonicalizer.CanonM : Type → Type
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_sub : ∀ (x y : ℝ), ↑(x - y) = ↑x - ↑y
-- Lean.Parser.Extra
Lean.Parser.identWithPartialTrailingDot : Lean.Parser.Parser
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- Variant of `jacobiTheta₂'` which we introduce to simplify some formulae.  -/
HurwitzZeta.jacobiTheta₂'' : ℂ → ℂ → ℂ
-- Mathlib.Topology.MetricSpace.Gluing
Nat.leRecOn.congr_simp : ∀ {C : ℕ → Sort u_1} {n m : ℕ} (a : n ≤ m) (a_1 a_2 : {k : ℕ} → C k → C (k + 1)),
  a_1 = a_2 → ∀ (a_3 a_4 : C n), a_3 = a_4 → Nat.leRecOn a a_1 a_3 = Nat.leRecOn a a_2 a_4
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_idem_left : ∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) [inst : (j : ι) → Decidable (j ∈ s)] (f₁ f₂ g : (a : ι) → π a),
  s.piecewise (s.piecewise f₁ f₂) g = s.piecewise f₁ g
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.instNontrivial : ∀ {α : Type u} [Nontrivial α], Nontrivial (Additive α)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
DifferentiableOn.cos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E},
  DifferentiableOn ℝ f s → DifferentiableOn ℝ (fun x => Real.cos (f x)) s
-- Aesop.Forward.Match.Types
/-- Compare two queue entries by rule priority, rule name and the expressions
contained in the match. Higher-priority rules are considered less (since the
queues are min-queues). The ordering on expressions is arbitrary.  -/
Aesop.ForwardRuleMatch.ord : Ord Aesop.ForwardRuleMatch
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instIsScalarTower : ∀ (p : ENNReal) {K : Type u_1} (K' : Type u_2) {V : Type u_4} [inst : SMul K K'] [inst_1 : SMul K V]
  [inst_2 : SMul K' V] [IsScalarTower K K' V], IsScalarTower K K' (WithLp p V)
-- Mathlib.Order.Filter.NAry
Filter.map₂_assoc : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {ε' : Type u_10} {f : Filter α}
  {g : Filter β} {m : δ → γ → ε} {n : α → β → δ} {m' : α → ε' → ε} {n' : β → γ → ε'} {h : Filter γ},
  (∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)) →
    Filter.map₂ m (Filter.map₂ n f g) h = Filter.map₂ m' f (Filter.map₂ n' g h)
-- Mathlib.Data.Finsupp.Defs
Finsupp.mk.sizeOf_spec : ∀ {α : Type u_9} {M : Type u_10} [inst : Zero M] [inst_1 : SizeOf α] [inst_2 : SizeOf M] (support : Finset α)
  (toFun : α → M) (mem_support_toFun : ∀ (a : α), a ∈ support ↔ toFun a ≠ 0),
  sizeOf { support := support, toFun := toFun, mem_support_toFun := mem_support_toFun } = 1 + sizeOf support
-- Mathlib.Topology.ShrinkingLemma
ShrinkingLemma.PartialRefinement.mk : {ι : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {u : ι → Set X} →
        {s : Set X} →
          {p : Set X → Prop} →
            (toFun : ι → Set X) →
              (carrier : Set ι) →
                (∀ (i : ι), IsOpen (toFun i)) →
                  s ⊆ ⋃ i, toFun i →
                    (∀ {i : ι}, i ∈ carrier → closure (toFun i) ⊆ u i) →
                      (∀ {i : ι}, i ∈ carrier → p (toFun i)) →
                        (∀ {i : ι}, i ∉ carrier → toFun i = u i) → ShrinkingLemma.PartialRefinement u s p
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.mapDomainOfBialgHom_comp : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} {I : Type u_7} [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : Group G] [inst_3 : Group H] [inst_4 : Group I] (f : MonoidAlgebra R H →ₐc[R] MonoidAlgebra R I)
  (g : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H),
  MonoidAlgebra.mapDomainOfBialgHom (f.comp g) =
    (MonoidAlgebra.mapDomainOfBialgHom f).comp (MonoidAlgebra.mapDomainOfBialgHom g)
-- Lean.Level
Lean.instReprLevelMVarId.repr : Lean.LevelMVarId → ℕ → Std.Format
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.EssFiniteType.cond : ∀ {R : Type u_1} {S : Type u_2} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  [self : Algebra.EssFiniteType R S],
  ∃ s, IsLocalization (Submonoid.comap (algebraMap (↥(Algebra.adjoin R ↑s)) S) (IsUnit.submonoid S)) S
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.bisim' : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (R : P.M α → P.M α → Prop),
  (∀ (x y : P.M α),
      R x y →
        MvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P x) =
          MvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P y)) →
    ∀ (x y : P.M α), R x y → x = y
-- Mathlib.Algebra.Module.LinearMap.Polynomial
MvPolynomial.aeval.eq_1 : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (f : σ → S₁), MvPolynomial.aeval f = { toRingHom := MvPolynomial.eval₂Hom (algebraMap R S₁) f, commutes' := ⋯ }
-- Mathlib.Analysis.Normed.Group.Basic
/-- An injective group homomorphism from a `CommGroup` to a `NormedGroup` induces a
`NormedCommGroup` structure on the domain.  -/
NormedCommGroup.induced : {𝓕 : Type u_1} →
  (E : Type u_5) →
    (F : Type u_6) →
      [inst : FunLike 𝓕 E F] →
        [inst_1 : CommGroup E] →
          [inst_2 : NormedGroup F] → [MonoidHomClass 𝓕 E F] → (f : 𝓕) → Function.Injective ⇑f → NormedCommGroup E
-- Mathlib.NumberTheory.SmoothNumbers
Nat.smoothNumbersUpTo_card_add_roughNumbersUpTo_card : ∀ (N k : ℕ), (N.smoothNumbersUpTo k).card + (N.roughNumbersUpTo k).card = N
-- Mathlib.Topology.Separation.SeparatedNhds
HasSeparatingCover.mono : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s₁ s₂ t₁ t₂ : Set X},
  HasSeparatingCover s₂ t₂ → s₁ ⊆ s₂ → t₁ ⊆ t₂ → HasSeparatingCover s₁ t₁
-- Mathlib.Analysis.Convex.Topology
_private.Mathlib.Analysis.Convex.Topology.0.sdiff_singleton_eventually_mem_nhds_left : ∀ {𝕜 : Type u_4} [inst : LinearOrder 𝕜] [inst_1 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {s : Set 𝕜} {a : 𝕜},
  (∀ x ∈ closure s, Set.Ioo x a ⊆ s) → ∀ᶠ (x : 𝕜) in nhdsWithin a (s ∩ Set.Iio a), s \ {a} ∈ nhds x
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.coe_id : ∀ (α : Type u_2) [inst : Min α] [inst_1 : Top α], ⇑(InfTopHom.id α) = id
-- Mathlib.CategoryTheory.Conj
/-- `conj` defines a group isomorphism between groups of automorphisms  -/
CategoryTheory.Iso.conjAut : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ≅ Y) → CategoryTheory.Aut X ≃* CategoryTheory.Aut Y
-- Mathlib.CategoryTheory.Dialectica.Basic
_private.Mathlib.CategoryTheory.Dialectica.Basic.0.CategoryTheory.Dial.termπ₁ : Lean.ParserDescr
-- Mathlib.Algebra.Homology.Bifunctor
/-- The bifunctor on homological complexes that is induced by a bifunctor.  -/
CategoryTheory.Functor.map₂HomologicalComplex : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
              [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                [inst_5 : CategoryTheory.Preadditive D] →
                  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                    [inst_6 : F.PreservesZeroMorphisms] →
                      [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                        {I₁ : Type u_4} →
                          {I₂ : Type u_5} →
                            {J : Type u_6} →
                              (c₁ : ComplexShape I₁) →
                                (c₂ : ComplexShape I₂) →
                                  (c : ComplexShape J) →
                                    [DecidableEq J] →
                                      [inst_9 : TotalComplexShape c₁ c₂ c] →
                                        [∀ (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂),
                                              K₁.HasMapBifunctor K₂ F c] →
                                          CategoryTheory.Functor (HomologicalComplex C₁ c₁)
                                            (CategoryTheory.Functor (HomologicalComplex C₂ c₂) (HomologicalComplex D c))
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingField.instCharP : ∀ {K : Type v} [inst : Field K] (f : Polynomial K) (p : ℕ) [CharP K p], CharP f.SplittingField p
-- Mathlib.Data.Nat.Prime.Basic
Nat.not_prime_iff_exists_dvd_lt : ∀ {n : ℕ}, 2 ≤ n → (¬Nat.Prime n ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n)
-- Mathlib.AlgebraicGeometry.Limits
/-- The underlying topological space of the coproduct is homeomorphic to the disjoint union  -/
AlgebraicGeometry.coprodMk : (X Y : AlgebraicGeometry.Scheme) → ↥X ⊕ ↥Y ≃ₜ ↥(X ⨿ Y)
-- Mathlib.Analysis.Calculus.Deriv.ZPow
Differentiable.zpow : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {m : ℤ} {f : E → 𝕜},
  Differentiable 𝕜 f → (∀ (x : E), f x ≠ 0) ∨ 0 ≤ m → Differentiable 𝕜 fun x => f x ^ m
-- Std.Async.Select
/-- The continuation that is called on results from the event source.
 -/
Std.Async.Selectable.cont : {α : Type} → (self : Std.Async.Selectable α) → self.β → Std.Async.Async α
-- Lean.Elab.Tactic.Doc
/-- The tags that have been applied to the tactic  -/
Lean.Elab.Tactic.Doc.TacticDoc.tags : Lean.Elab.Tactic.Doc.TacticDoc → Lean.NameSet
-- Mathlib.Algebra.Group.Hom.Defs
Monoid.End.coe_mul : ∀ (M : Type u_4) [inst : MulOne M] (f g : Monoid.End M), ⇑(f * g) = ⇑f ∘ ⇑g
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.commaFromOver_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {X_1 Y : CategoryTheory.Functor J (CategoryTheory.Over X)} (f : X_1 ⟶ Y),
  (CategoryTheory.WithTerminal.commaFromOver.map f).right = CategoryTheory.CategoryStruct.id X
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.AlgebraTensorModule.ker_mapOfCompatibleSMul : ∀ {R : Type u_1} (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (M : Type u_4)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] {N : Type u_5}
  [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : Module A N] [inst_10 : IsScalarTower R A N],
  (TensorProduct.mapOfCompatibleSMul A R A M N).ker =
    Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_range_succ_comm : ∀ {M : Type u_4} [inst : AddCommMonoid M] (f : ℕ → M) (n : ℕ),
  ∑ x ∈ Finset.range (n + 1), f x = f n + ∑ x ∈ Finset.range n, f x
-- Lean.Linter.Init
Lean.Linter.instInhabitedLinterSets : Inhabited Lean.Linter.LinterSets
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- `leftSection` composed with `f` is `pi` composed with `rightSection`  -/
CategoryTheory.IsSplitCoequalizer.leftSection_top_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z}
  (self : CategoryTheory.IsSplitCoequalizer f g π) {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp self.leftSection (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp π (CategoryTheory.CategoryStruct.comp self.rightSection h)
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Set.natCard_smul_set : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (a : G) (s : Set α),
  Nat.card ↑(a • s) = Nat.card ↑s
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelIsoOfEq_inv_comp_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.Limits.HasCokernel g]
  (h : f = g) (e : Y ⟶ Z) (he : CategoryTheory.CategoryStruct.comp f e = 0),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelIsoOfEq h).inv
      (CategoryTheory.Limits.cokernel.desc f e he) =
    CategoryTheory.Limits.cokernel.desc g e ⋯
-- Mathlib.CategoryTheory.GradedObject.Single
CategoryTheory.GradedObject.singleObjApplyIso_inv_single_map_assoc : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Limits.HasInitial C] [inst_2 : DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) {Z : C}
  (h : (CategoryTheory.GradedObject.single j).obj Y j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIso j X).inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.single j).map f j) h) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIso j Y).inv h)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} {fallback : β k}, k ∉ m₁ → (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback
-- Mathlib.RingTheory.LocalProperties.Submodule
Submodule.mem_of_localization_maximal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5) [inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_4 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Module R (Mₚ P)]
  (f : (P : Ideal R) → [inst_5 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_5 : ∀ (P : Ideal R) [inst_5 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (m : M) (N : Submodule R M),
  (∀ (P : Ideal R) [inst_6 : P.IsMaximal], (f P) m ∈ Submodule.localized₀ P.primeCompl (f P) N) → m ∈ N
-- Mathlib.Order.Closure
/-- The identity function as a closure operator.  -/
ClosureOperator.id : (α : Type u_1) → [inst : Preorder α] → ClosureOperator α
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_comap_eq_self : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N} {S : AddSubsemigroup N},
  S ≤ f.srange → AddSubsemigroup.map f (AddSubsemigroup.comap f S) = S