mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.mapAlgEquiv_apply : ∀ {R : Type u} (σ : Type u_1) [inst : CommSemiring R] {A₁ : Type u_2} {A₂ : Type u_3} [inst_1 : CommSemiring A₁]
  [inst_2 : CommSemiring A₂] [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : MvPolynomial σ A₁),
  (MvPolynomial.mapAlgEquiv σ e) x = (MvPolynomial.map ↑e) x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_inter_of_contains_eq_false_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₁.contains k = false → Std.DHashMap.Internal.Raw₀.Const.get? (m₁.inter m₂) k = none
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.SwapTrue.eq_1 : ∀ {I : Type u} [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (o : Ordinal.{u}) (f : I → Bool) (i : I),
  Profinite.NobelingProof.SwapTrue o f i = if Profinite.NobelingProof.ord I i = o then true else f i
-- Std.Data.Iterators.Combinators.StepSize
/-- Produces an iterator that emits one value of `it`, then drops `n - 1` elements, then emits another
value, and so on. In other words, it emits every `n`-th value of `it`, starting with the first one.

If `n = 0`, the iterator behaves like for `n = 1`: It emits all values of `it`.


**Marble diagram:**

```
it               ---1----2----3---4----5
it.stepSize 2    ---1---------3--------5
```

**Availability:**

This operation is currently only available for iterators implementing `IteratorAccess`,
such as `PRange.iter` range iterators.

**Termination properties:**

* `Finite` instance: only if the base iterator `it` is finite
* `Productive` instance: always
 -/
Std.Iter.stepSize : {α β : Type u_1} → [inst : Std.Iterator α Id β] → [Std.IteratorAccess α Id] → Std.Iter β → ℕ → Std.Iter β
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The `Functor.CoreMonoidal` structure given by a lax monoidal functor such
that `ε` and `μ` are isomorphisms.  -/
CategoryTheory.Functor.CoreMonoidal.ofLaxMonoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.LaxMonoidal] →
                [CategoryTheory.IsIso (CategoryTheory.Functor.LaxMonoidal.ε F)] →
                  [∀ (X Y : C), CategoryTheory.IsIso (CategoryTheory.Functor.LaxMonoidal.μ F X Y)] → F.CoreMonoidal
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.Nonnegg.eq_4 : ∀ (c d a a_1 : ℕ), Zsqrtd.Nonnegg c d (Int.negSucc a) (Int.negSucc a_1) = False
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.vcomp_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.StrongTrans F G)
  (θ : CategoryTheory.Oplax.StrongTrans G H) (a : B), (η.vcomp θ).app a = (η.toOplax.vcomp θ.toOplax).app a
-- Mathlib.Algebra.Group.UniqueProds.Basic
TwoUniqueSums.of_injective_addHom : ∀ {G : Type u} {H : Type v} [inst : Add G] [inst_1 : Add H] (f : H →ₙ+ G),
  Function.Injective ⇑f → TwoUniqueSums G → TwoUniqueSums H
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.r_w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}
  (h : CategoryTheory.RetractArrow f g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left h.r) f =
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.Arrow.Hom.right h.r)
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.hasVarPattern : Lean.Meta.Match.Problem → Bool
-- Lean.Parser.Term
Lean.Parser.Term.prop.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSemanticTokenModifier.fromJson : Lean.Json → Except String Lean.Lsp.SemanticTokenModifier
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Finpartition.nonuniformWitnesses.congr_simp : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] {A : Finset α} (P P_1 : Finpartition A),
  P = P_1 →
    ∀ (G G_1 : SimpleGraph α),
      G = G_1 →
        ∀ {inst_4 : DecidableRel G.Adj} [inst_5 : DecidableRel G_1.Adj] (ε ε_1 : 𝕜),
          ε = ε_1 → ∀ (s s_1 : Finset α), s = s_1 → P.nonuniformWitnesses G ε s = P_1.nonuniformWitnesses G_1 ε_1 s_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_erase_eq_of_not_compare_eq_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (∀ {km : α}, t.maxKey? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).maxKey? = t.maxKey?
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.CofanMapObjFun.hasMap : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  (X : CategoryTheory.GradedObject I C) (p : I → J) (c : (j : J) → X.CofanMapObjFun p j)
  (hc : (j : J) → CategoryTheory.Limits.IsColimit (c j)), X.HasMap p
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (t.alter k f).minKey? = some k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Clean.State.mk.injEq : ∀ (used : Lean.PHashSet Lean.Name) (next : Lean.PHashMap Lean.Name ℕ) (used_1 : Lean.PHashSet Lean.Name)
  (next_1 : Lean.PHashMap Lean.Name ℕ),
  ({ used := used, next := next } = { used := used_1, next := next_1 }) = (used = used_1 ∧ next = next_1)
-- Mathlib.Data.Nat.GCD.Basic
Nat.dvd_of_lcm_left_dvd : ∀ {a b c : ℕ}, a.lcm b ∣ c → b ∣ c
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instLaxMonoidalMonMapAddMon.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : CategoryTheory.BraidedCategory C]
  [inst_5 : CategoryTheory.BraidedCategory D] [inst_6 : F.LaxBraided],
  F.instLaxMonoidalMonMapAddMon =
    { ε := { hom := CategoryTheory.Functor.LaxMonoidal.ε F, isAddMonHom_hom := ⋯ },
      μ := fun M N => { hom := CategoryTheory.Functor.LaxMonoidal.μ F M.X N.X, isAddMonHom_hom := ⋯ },
      μ_natural_left := ⋯, μ_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯, right_unitality := ⋯ }
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_append : ∀ {as bs : ByteArray} {i j : ℕ}, (as ++ bs).extract i j = as.extract i j ++ bs.extract (i - as.size) (j - as.size)
-- Init.Data.Int.Lemmas
Int.subNatNat_of_sub_eq_zero : ∀ {m n : ℕ}, n - m = 0 → Int.subNatNat m n = ↑(m - n)
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.finite_left : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {S : Set G} [H.FiniteIndex], Subgroup.IsComplement S ↑H → S.Finite
-- Mathlib.LinearAlgebra.LinearIndependent.Algebra
LinearIndepOn.algebraMap_comp_iff : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [IsScalarTower R S A] [FaithfulSMul S A]
  {ι : Type u_4} {v : ι → S} {s : Set ι}, LinearIndepOn R (⇑(algebraMap S A) ∘ v) s ↔ LinearIndepOn R v s
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
/-- Every ordinal has a fundamental sequence.  -/
Ordinal.exists_fundamental_sequence : ∀ (a : Ordinal.{u}), ∃ f, a.IsFundamentalSequence a.cof.ord f
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.coe_tensorUnit : ∀ {R : Type u} [inst : CommRing R], ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (CommAlgCat R)) = R
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Cache for entry certificates, keyed by matrix indices.  -/
Mathlib.Tactic.Determinant.CertCache.entryCache : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} →
      Mathlib.Tactic.Determinant.CertCache rα → Std.HashMap (ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα)
-- Mathlib.Probability.HasLaw
ProbabilityTheory.hasLaw_smul_dirac_of_ae_eq : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {P : MeasureTheory.Measure Ω} {x : 𝓧},
  (X =ᵐ[P] fun x_1 => x) → ProbabilityTheory.HasLaw X (P Set.univ • MeasureTheory.Measure.dirac x) P
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CtorInfo.isRef : Lean.Compiler.LCNF.CtorInfo → Bool
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSignatureHelpParams : Lean.FromJson Lean.Lsp.SignatureHelpParams
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Delaborator for `Finset.prod`. The `pp.funBinderTypes` option controls whether
to show the domain type when the product is over `Finset.univ`.  -/
BigOperators.delabFinsetProd : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Data.Nat.Fib.Basic
Nat.fastFib_eq : ∀ (n : ℕ), n.fastFib = Nat.fib n
-- Init.Data.SInt.Lemmas
Int16.toInt_mul : ∀ (a b : Int16), (a * b).toInt = (a.toInt * b.toInt).bmod (2 ^ 16)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
/-- If `S` is nonempty such that there is `A` with `|S| ≤ |A|` such that `|A * S| ≤ (2 - ε) * |S|`
for some `0 < ε ≤ 1`, then there is a finite subgroup `H` of `G` of size `|H| ≤ (2 / ε - 1) * |S|`
such that `S` is covered by at most `2 / ε - 1` right cosets of `H`.  -/
Finset.card_mul_finset_lt_two : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {S : Finset G} {ε : ℝ},
  0 < ε →
    ε ≤ 1 →
      S.Nonempty →
        (∃ A, S.card ≤ A.card ∧ ↑(A * S).card ≤ (2 - ε) * ↑S.card) →
          ∃ H x Z, ↑(Fintype.card ↥H) ≤ (2 / ε - 1) * ↑S.card ∧ ↑Z.card ≤ 2 / ε - 1 ∧ ↑S ⊆ ↑H * ↑Z
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.comapStructureSheafFun.congr_simp : ∀ {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B] [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B]
  {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜] [inst_7 : GradedRing ℬ] (f f_1 : 𝒜 →+*ᵍ ℬ) (e_f : f = f_1)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜))
  (U : TopologicalSpace.Opens (ProjectiveSpectrum 𝒜)) (V : TopologicalSpace.Opens (ProjectiveSpectrum ℬ))
  (hUV : V.carrier ⊆ ⇑(AlgebraicGeometry.ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier)
  (s s_1 : (x : ↥U) → HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toSubmodule),
  s = s_1 →
    ∀ (y : ↥V),
      AlgebraicGeometry.Proj.comapStructureSheafFun f hf U V hUV s y =
        AlgebraicGeometry.Proj.comapStructureSheafFun f_1 ⋯ U V ⋯ s_1 y
-- Mathlib.Order.Fin.Basic
Fin.rev_bot : ∀ {n : ℕ} [inst : NeZero n], ⊥.rev = ⊤
-- Std.Data.TreeSet.Basic
Std.TreeSet.instSingleton : {α : Type u} → {cmp : α → α → Ordering} → Singleton α (Std.TreeSet α cmp)
-- Mathlib.Topology.Order
instDiscreteTopologyWithDiscreteTopology : ∀ {α : Type u}, DiscreteTopology (WithDiscreteTopology α)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- A commutative additive monoid object is a commutative additive monoid object in the
category of additive monoid objects.  -/
CategoryTheory.AddMon.instIsCommAddMonObj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M : CategoryTheory.AddMon C}
  [inst_3 : CategoryTheory.IsCommAddMonObj M.X], CategoryTheory.IsCommAddMonObj M
-- Lean.DocString.Parser
/-- Parses block opener prefixes. At the beginning of the line, if this parser succeeds, then a special
block is beginning.
 -/
Lean.Doc.Parser.blockOpener : Lean.Parser.ParserFn
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
/-- Conditionally complete partial orders (with suprema) are partial orders
where every nonempty, directed set which is bounded above has a least upper bound.  -/
ConditionallyCompletePartialOrderSup : Type u_3 → Type u_3
-- Mathlib.CategoryTheory.Monoidal.Hopf_
/-- A Hopf monoid in a braided category `C` is a bimonoid object in `C` equipped with an antipode.
 -/
CategoryTheory.HopfObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → [CategoryTheory.BraidedCategory C] → C → Type v₁
-- Mathlib.Analysis.InnerProductSpace.ExteriorPower
OrthonormalBasis.toBasis_exteriorPower : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {I : Type u_2} [inst_3 : Fintype I] [inst_4 : LinearOrder I] (b : OrthonormalBasis I ℝ E) (n : ℕ),
  (b.exteriorPower n).toBasis = Module.Basis.exteriorPower n b.toBasis
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- The endomorphism monoid of a root pairing.  -/
RootPairing.Hom.instMonoid : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (P : RootPairing ι R M N) → Monoid (P.Hom P)
-- Lean.DocString.Add
/-- Adds a Verso docstring to the environment.

`binders` should be the syntax of the parameters to the constant that is being documented, as a null
node that contains a sequence of bracketed binders. It is used to allow interactive features such as
document highlights and “find references” to work for documented parameters. If no parameter binders
are available, pass `Syntax.missing` or an empty null node.
 -/
Lean.addVersoModDocString : Lean.DeclarationRange → Lean.TSyntax `Lean.Doc.Parser.document → Lean.Elab.TermElabM Unit
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- The nonnegative part of a bounded continuous `ℝ`-valued function as a bounded
continuous `ℝ≥0`-valued function.  -/
BoundedContinuousFunction.nnrealPart : {α : Type u} → [inst : TopologicalSpace α] → BoundedContinuousFunction α ℝ → BoundedContinuousFunction α NNReal
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.lipschitz_eval_const : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] (x : α),
  LipschitzWith 1 fun f => f x
-- Std.Time.DateTime.WallTime
/-- Adds an `Hour.Offset` to the given `WallTime`.
 -/
Std.Time.WallTime.addHours : Std.Time.WallTime → Std.Time.Hour.Offset → Std.Time.WallTime
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
ciInf_subsingleton : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderInf α] [Subsingleton ι] (i : ι) (s : ι → α),
  ⨅ i, s i = s i
-- Std.Http.Data.URI.Basic
/-- A `:` port separator is present with no digits after it (for example, `example.com:`).
 -/
Std.Http.URI.Port.empty : Std.Http.URI.Port
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α} [inst_3 : Inhabited (β k)], m₁.contains k = false → (m₁.union m₂).get! k = m₂.get! k
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyInf_antitone : ∀ {X : Type u_1} (T : X → X) (F : Set X), Antitone fun u => Dynamics.coverEntropyInf T F
-- Mathlib.GroupTheory.Coxeter.Inversion
_private.Mathlib.GroupTheory.Coxeter.Inversion.0.CoxeterSystem.termRis_ : Lean.ParserDescr
-- Mathlib.Algebra.IsPrimePow
IsPrimePow.pos : ∀ {n : ℕ}, IsPrimePow n → 0 < n
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.length_eq_zero : ∀ {n : ℕ} (c : Composition n), c.length = 0 ↔ n = 0
-- Mathlib.Algebra.Group.Prod
MulHom.coprod_apply : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Mul M] [inst_1 : Mul N] [inst_2 : CommSemigroup P] (f : M →ₙ* P)
  (g : N →ₙ* P) (p : M × N), (f.coprod g) p = f p.1 * g p.2
-- Mathlib.Data.List.Infix
List.getElem_tails : ∀ {α : Type u_1} (l : List α) (n : ℕ) (h : n < l.tails.length), l.tails[n] = List.drop n l
-- Mathlib.Order.DirSupClosed
PartialOrder.dirSupClosed_singleton : ∀ {α : Type u_1} [inst : PartialOrder α] (a : α), DirSupClosed {a}
-- Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
/-- A convolution-type scalar multiplication of the additive
monoid algebra on the set of formal functions.  -/
AddMonoidAlgebra.instVAddForallOfIsLeftCancelVAddOfVAddWithZero : {G : Type u_1} →
  {P : Type u_2} →
    {R : Type u_3} →
      {V : Type u_4} →
        [inst : VAdd G P] →
          [IsLeftCancelVAdd G P] →
            [inst : Semiring R] → [inst_1 : AddCommMonoid V] → [SMulWithZero R V] → SMul (AddMonoidAlgebra R G) (P → V)
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
CategoryTheory.Pseudofunctor.DescentData.pullFunctor.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p p_1 : S' ⟶ S} (e_p : p = p_1) {ι' : Type t'} {X' : ι' → C}
  {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι} {p' p'_1 : (j : ι') → X' j ⟶ X (α j)} (e_p' : p' = p'_1)
  (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) p),
  CategoryTheory.Pseudofunctor.DescentData.pullFunctor F w = CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯
-- Mathlib.GroupTheory.PGroup
/-- **Alias** of the forward direction of `IsPGroup.iff_card`. -/
IsPGroup.exists_card_eq : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)] [Finite G], IsPGroup p G → ∃ n, Nat.card G = p ^ n
-- Mathlib.Algebra.Quaternion
Quaternion.imI_ofScientific : ∀ {R : Type u_1} [inst : Field R] (m : ℕ) (s : Bool) (e : ℕ),
  QuaternionAlgebra.imI (OfScientific.ofScientific m s e) = 0
-- Mathlib.Analysis.Fourier.Notation
/-- The Fourier transform as a continuous linear map.  -/
FourierTransform.fourierCLM : (R : Type u_2) →
  (E : Type u_3) →
    {F : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : AddCommMonoid F] →
            [inst_3 : Module R E] →
              [inst_4 : Module R F] →
                [inst_5 : FourierTransform E F] →
                  [FourierAdd E F] →
                    [FourierSMul R E F] →
                      [inst_8 : TopologicalSpace E] →
                        [inst_9 : TopologicalSpace F] → [ContinuousFourier E F] → E →L[R] F
-- Mathlib.RingTheory.Polynomial.Basic
MvPolynomial.ker_mapAlgHom : ∀ {R : Type u} [inst : CommRing R] {S₁ : Type u_2} {S₂ : Type u_3} {σ : Type u_4} [inst_1 : CommRing S₁]
  [inst_2 : CommRing S₂] [inst_3 : Algebra R S₁] [inst_4 : Algebra R S₂] (f : S₁ →ₐ[R] S₂),
  RingHom.ker (MvPolynomial.mapAlgHom f) = Ideal.map MvPolynomial.C (RingHom.ker f)
-- Init.Data.Int.Order
Int.min_self : ∀ (a : ℤ), min a a = a
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.isoMk_inv_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (hl : f.left ≅ g.left)
  (hw : autoParam (CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom) CategoryTheory.Over.isoMk._auto_1),
  (CategoryTheory.Over.isoMk hl hw).inv.left = hl.inv
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
/-- The main term in the infinite product for sine.  -/
sineTerm : ℂ → ℕ → ℂ
-- Mathlib.Algebra.GroupWithZero.Action.End
/-- `AddMonoid.End.applyDistribMulAction` is faithful.  -/
AddMonoid.End.applyFaithfulSMul : ∀ {α : Type u_4} [inst : AddMonoid α], FaithfulSMul (AddMonoid.End α) α
-- Mathlib.FieldTheory.CardinalEmb
/-- A bijection between `E →ₐ[F] Ē` and the product of `E⟮<i⁺⟯ →ₐ[E⟮<i⟯] Ē` over all `i : ι`.  -/
Field.Emb.Cardinal.embEquivPi : {F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] →
            [inst_3 : Algebra.IsAlgebraic F E] →
              Field.Emb F E ≃ ((i : (Module.rank F E).ord.ToType) → Field.Emb.Cardinal.factor ↑i)
-- Std.Async.TCP
Std.Async.TCP.Socket.Server.native : Std.Async.TCP.Socket.Server → Std.Internal.UV.TCP.Socket
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.minEntry?.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
      h_3 size k v l size_1 k_1 v_1 l_1 r h r_1) =
    h_1 ()
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.brecOn.eq : ∀ {motive : (a : Tactic.ComputeAsymptotics.Basis) → Tactic.ComputeAsymptotics.BasisExtension a → Sort u}
  {a : Tactic.ComputeAsymptotics.Basis} (t : Tactic.ComputeAsymptotics.BasisExtension a)
  (F_1 :
    (a : Tactic.ComputeAsymptotics.Basis) →
      (t : Tactic.ComputeAsymptotics.BasisExtension a) → Tactic.ComputeAsymptotics.BasisExtension.below t → motive a t),
  Tactic.ComputeAsymptotics.BasisExtension.brecOn t F_1 =
    F_1 a t (Tactic.ComputeAsymptotics.BasisExtension.brecOn.go t F_1).2
-- Mathlib.Data.FunLike.IsApply
IsZeroApply.mk : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} [inst : FunLike F α β] [inst_1 : Zero β]
  [inst_2 : Zero F], (∀ (x : α), 0 x = 0) → IsZeroApply F α β
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_right_inj_of_comparable : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [MulLeftStrictMono α] {a b c : α},
  b ≤ c ∨ c ≤ b → (a * c = a * b ↔ c = b)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.walkingSpanOpEquiv_inverse_map : ∀ {X₁ X₂ : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair} (a : X₁ ⟶ X₂),
  CategoryTheory.Limits.walkingSpanOpEquiv.inverse.map a =
    CategoryTheory.Limits.widePullbackShapeOpMap CategoryTheory.Limits.WalkingPair X₁ X₂ a
-- Lean.Meta.Tactic.TryThis
/-- Delaborate `e` into a suggestion suitable for use by `refine`.  -/
Lean.Meta.Tactic.TryThis.delabToRefinableSuggestion : Lean.Expr → Lean.MetaM Lean.Meta.Tactic.TryThis.Suggestion