mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.OplaxTrans.leftUnitor_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Oplax.OplaxTrans.leftUnitor η).hom.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom
-- Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
ContinuousMap.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry : ∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : TopologicalSpace Y]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] {s : Set X} {t : Set Y} [CompactSpace ↑t] [inst_4 : TopologicalSpace X]
  [OpensMeasurableSpace X] [SecondCountableTopologyEither X C(↑t, E)],
  MeasurableSet s →
    ∀ (f : X → Y → E) (g : C(↑t, E)),
      ContinuousOn (Function.uncurry f) (s ×ˢ t) →
        MeasureTheory.AEStronglyMeasurable (fun x => ContinuousMap.mkD (t.domRestrict (f x)) g) (μ.restrict s)
-- Mathlib.Algebra.Module.Injective
Module.ulift_injective_of_injective : ∀ (R : Type u) [inst : Ring R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Small.{v, u} R],
  Module.Injective R M → Module.Injective R (ULift.{v', v} M)
-- Std.Time.Duration
Std.Time.Duration.instLE : LE Std.Time.Duration
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instIsSubApply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  (𝔖 : Set (Set E)), IsSubApply (UniformConvergenceCLM σ F 𝔖) E F
-- Mathlib.Order.Filter.Basic
/-- Eta-expanded form of `Filter.EventuallyEq.add` -/
Filter.EventuallyEq.fun_add : ∀ {α : Type u} {β : Type v} [inst : Add β] {f f' g g' : α → β} {l : Filter α},
  f =ᶠ[l] g → f' =ᶠ[l] g' → (fun i => f i + f' i) =ᶠ[l] fun i => g i + g' i
-- Mathlib.Order.Closure
LowerAdjoint.closure_iUnion_closure : ∀ {α : Type u_1} {ι : Sort u_2} {β : Type u_4} [inst : SetLike α β] [inst_1 : Preorder α] (l : LowerAdjoint SetLike.coe)
  (f : ι → α), l.toFun (⋃ i, ↑(l.toFun ↑(f i))) = l.toFun (⋃ i, ↑(f i))
-- Mathlib.Data.Nat.Digits.Defs
/-- Interpreting as a base `p` number and modulo `p^i` is the same as taking the first `i` digits.
 -/
Nat.ofDigits_mod_pow_eq_ofDigits_take : ∀ {p : ℕ} (i : ℕ),
  0 < p →
    ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → Nat.ofDigits p digits % p ^ i = Nat.ofDigits p (List.take i digits)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.ofObj_obj : ∀ {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} (M : ↑(F.obj { as := Opposite.op S })) (i : ι),
  (CategoryTheory.Pseudofunctor.DescentData.ofObj M).obj i = (F.map (f i).op.toLoc).toFunctor.obj M
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.counitApp_app : ∀ {P : TopCat → Prop} [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] [inst_2 : CompHausLike.HasExplicitFiniteCoproducts P]
  (Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w)))
  [inst_3 : CategoryTheory.Limits.PreservesFiniteProducts Y] (x : (CompHausLike P)ᵒᵖ),
  (CompHausLike.LocallyConstant.counitApp Y).app x = CompHausLike.LocallyConstant.counitAppApp (Opposite.unop x) Y
-- Mathlib.RingTheory.PowerSeries.Substitution
/-- A variant of `HasSubst.monomial` to avoid the expansion of `Unit`.  -/
PowerSeries.HasSubst.monomial' : ∀ {S : Type u_4} [inst : CommRing S] {n : ℕ}, n ≠ 0 → ∀ (s : S), PowerSeries.HasSubst ((PowerSeries.monomial n) s)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α}, a ∈ t.erase k ↔ cmp k a ≠ Ordering.eq ∧ a ∈ t
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.stronglyAdapted_predictablePart' : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0},
  MeasureTheory.StronglyAdapted ℱ fun n => MeasureTheory.predictablePart f ℱ μ n
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of the twist of the von Mangoldt function `Λ` by a Dirichlet character `χ`
converges at `s` when `re s > 1`.  -/
DirichletCharacter.LSeriesSummable_twist_vonMangoldt : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ},
  1 < s.re → LSeriesSummable ((fun n => χ ↑n) * fun n => ↑(ArithmeticFunction.vonMangoldt n)) s
-- Lean.LibrarySuggestions.Basic
/-- The tactic that is calling the premise selection, e.g. `simp`, `grind`, or `aesop`.
This may be used to adjust the score of the suggestions
 -/
Lean.LibrarySuggestions.Config.caller : Lean.LibrarySuggestions.Config → Option String
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.multicospanIndexEnd_snd : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) (f : (CategoryTheory.Limits.multicospanShapeEnd J).R),
  (CategoryTheory.Limits.multicospanIndexEnd F).snd f =
    (F.map (CategoryTheory.Arrow.hom f).op).app (CategoryTheory.Arrow.right f)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteEdges_le : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)), G'.deleteEdges s ≤ G'
-- Std.Data.ExtTreeMap.Basic
/-- Checks whether a key is present in a map and inserts a value for the key if it was not found.
If the returned `Bool` is `true`, then the returned map is unaltered. If the `Bool` is `false`,
then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `contains` followed by `insertIfNew`.
 -/
Std.ExtTreeMap.containsThenInsertIfNew : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → β → Bool × Std.ExtTreeMap α β cmp
-- Init.Data.Range.Polymorphic.Iterators
Std.Rii.Internal.isPlausibleIndirectOutput_iter_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.Least? α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLeast? α] {r : Std.Rii α} {a : α},
  (Std.Rii.Internal.iter r).IsPlausibleIndirectOutput a ↔ a ∈ r
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAtOfComplement.domChart.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I I_1 : ModelWithCorners 𝕜 E H}
  (e_I : I = I_1) {J J_1 : ModelWithCorners 𝕜 E'' G} (e_J : J = J_1) {M : Type u_11} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N]
  {n n_1 : WithTop ℕ∞} (e_n : n = n_1) {f f_1 : M → N} (e_f : f = f_1) {x x_1 : M} (e_x : x = x_1)
  (h : Manifold.IsImmersionAtOfComplement F I J n f x), h.domChart = ⋯.domChart
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.FG.of_finite : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] [Finite M], FirstOrder.Language.Structure.FG L M
-- Mathlib.Topology.Algebra.SeparationQuotient.Hom
SeparationQuotient.liftContinuousAddMonoidHom.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : AddCommMonoid M]
  [inst_3 : ContinuousAdd M] [inst_4 : AddCommMonoid N] (f : M →ₜ+ N) (hf : ∀ (x y : M), Inseparable x y → f x = f y),
  SeparationQuotient.liftContinuousAddMonoidHom f hf =
    { toFun := SeparationQuotient.lift (⇑f) hf, map_zero' := ⋯, map_add' := ⋯, continuous_toFun := ⋯ }
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.copy.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] [inst_1 : SupSet β] (f : sSupHom α β) (f' : α → β) (h : f' = ⇑f),
  f.copy f' h = { toFun := f', map_sSup' := ⋯ }
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ'.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℕ), W.preΨ' n = preNormEDS' (W.Ψ₂Sq ^ 2) W.Ψ₃ W.preΨ₄ n
-- Mathlib.Algebra.Algebra.Operations
Submodule.sup_smul : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  (I J : Submodule R A) (N : Submodule R M), (I ⊔ J) • N = I • N ⊔ J • N
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
isIntegral_intCast : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] (n : ℤ), IsIntegral R ↑n
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateEquiv_adjunction_id : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c : B} {l r : c ⟶ c}
  (adj : CategoryTheory.Bicategory.Adjunction l r) (α : CategoryTheory.CategoryStruct.id c ⟶ l),
  (CategoryTheory.Bicategory.conjugateEquiv adj (CategoryTheory.Bicategory.Adjunction.id c)) α =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor r).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft r α) adj.counit)
-- Mathlib.Order.Part
OrderHom.partBind_coe : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] (f : α →o Part β) (g : α →o β → Part γ) (x : α),
  (f.partBind g) x = (f x).bind (g x)
-- Lean.Elab.Tactic.Basic
/-- Add the given goal to the front of the current list of goals.  -/
Lean.Elab.Tactic.pushGoal : Lean.MVarId → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
ContDiffAt.csinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {n : WithTop ℕ∞},
  ContDiffAt ℂ n f x → ContDiffAt ℂ n (fun x => Complex.sinh (f x)) x
-- Mathlib.CategoryTheory.Shift.Quotient
CategoryTheory.Quotient.functor_obj_shift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (r : HomRel C) (A : Type w) [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] [inst_3 : r.IsCompatibleWithShift A] (X : C) (n : A),
  (CategoryTheory.shiftFunctor (CategoryTheory.Quotient r) n).obj ((CategoryTheory.Quotient.functor r).obj X) =
    (CategoryTheory.Quotient.functor r).obj ((CategoryTheory.shiftFunctor C n).obj X)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.equalizer.hom_ext_iff : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g] {W : C} {k l : W ⟶ CategoryTheory.Limits.equalizer f g},
  k = l ↔
    CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.equalizer.ι f g) =
      CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.equalizer.ι f g)
-- Batteries.Data.List.Perm
List.nil_subperm : ∀ {α : Type u_1} {l : List α}, [].Subperm l
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {a : α}, Std.DTreeMap.Internal.Impl.contains a t = false → t.getKey? a = none
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.isOpen_source : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E)
  (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj), IsOpen e.source
-- Mathlib.NumberTheory.Dioph
/-- The set of places where one Diophantine function is at most another is Diophantine.  -/
Dioph.le_dioph : ∀ {α : Type} {f g : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph.DiophFn g → Dioph {v | f v ≤ g v}
-- Init.Data.Option.List
Option.length_toList : ∀ {α : Type u_1} {o : Option α}, o.toList.length = if o.isSome = true then 1 else 0
-- Init.Data.Vector.Attach
Vector.toList_attachWith : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {P : α → Prop} {H : ∀ x ∈ xs, P x},
  (xs.attachWith P H).toList = xs.toList.attachWith P ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
/-- If there are two elliptic curves with the same `j`-invariants defined over a
separably closed field, then there exists a change of variables over that field which change
one curve into another.  -/
WeierstrassCurve.exists_variableChange_of_j_eq : ∀ {F : Type u_1} [inst : Field F] [IsSepClosed F] (E E' : WeierstrassCurve F) [inst_2 : E.IsElliptic]
  [inst_3 : E'.IsElliptic], E.j = E'.j → ∃ C, C • E = E'
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.overMapPullback_id_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {X Y : C} (f : X ⟶ Y)
  {Z : CategoryTheory.Functor (CategoryTheory.Sheaf (J.over Y) A) (CategoryTheory.Sheaf (J.over X) A)}
  (h : J.overMapPullback A f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (J.overMapPullbackComp A (CategoryTheory.CategoryStruct.id X) f).inv
      (CategoryTheory.CategoryStruct.comp ((J.overMapPullback A f).whiskerLeft (J.overMapPullbackId A X).hom)
        (CategoryTheory.CategoryStruct.comp (J.overMapPullback A f).rightUnitor.hom h)) =
    CategoryTheory.CategoryStruct.comp (J.overMapPullbackCongr A ⋯).hom h
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.coe_zsmul : ∀ {A : Type u_1} {G : Type u_2} [inst : Semiring A] [inst_1 : Monoid G] {V : Type u_6} {W : Type u_7}
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommGroup W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (z : ℤ), ⇑(z • f) = z • ⇑f
-- Lean.Parser.Extra
/-- The parser `ident` parses a single identifier, possibly with namespaces, such as `foo` or
`bar.baz`. The identifier must not be a declared token, so for example it will not match `"def"`
because `def` is a keyword token. Tokens are implicitly declared by using them in string literals
in parser declarations, so `syntax foo := "bla"` will make `bla` no longer legal as an identifier.

Identifiers can contain special characters or keywords if they are escaped using the `«»` characters:
`«def»` is an identifier named `def`, and `«x»` is treated the same as `x`. This is useful for
using disallowed characters in identifiers such as `«foo.bar».baz` or `«hello world»`.

This parser has arity 1: it produces a `Syntax.ident` node containing the parsed identifier.
You can use `TSyntax.getId` to extract the name from the resulting syntax object.  -/
Lean.Parser.ident : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_inv_app_right_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T}
  {R : CategoryTheory.Functor D T} {C' : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅}
  [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T']
  {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'}
  {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F)
  (β : R.comp F ⟶ F₂.comp R') [inst_6 : CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R')
  (X_1 :
    CategoryTheory.Comma (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α)
      (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β))),
  ((CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso α β X).inv.app X_1).right.right =
    CategoryTheory.CategoryStruct.id X_1.right.right
-- Mathlib.GroupTheory.Nilpotent
/-- n-ary products of nilpotent groups are nilpotent.  -/
AddGroup.isNilpotent_pi : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → AddGroup (Gs i)] [Finite η]
  [∀ (i : η), AddGroup.IsNilpotent (Gs i)], AddGroup.IsNilpotent ((i : η) → Gs i)
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
/-- The canonical map to the explicit equalizer.  -/
CategoryTheory.regularTopology.mapToEqualizer : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type u_4)) →
      {W X B : C} →
        (f : X ⟶ B) →
          (g₁ g₂ : W ⟶ X) →
            CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
              (P.obj (Opposite.op B) ⟶
                ↑{x |
                    (CategoryTheory.ConcreteCategory.hom (P.map g₁.op)) x =
                      (CategoryTheory.ConcreteCategory.hom (P.map g₂.op)) x})
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.pOpcycles_singleObjOpcyclesSelfIso_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c j).obj A).pOpcycles j)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjOpcyclesSelfIso c j A).inv h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j A).hom h
-- Lean.Meta.Basic
/-- Array of postponed universe level constraints  -/
Lean.Meta.State.postponed : Lean.Meta.State → Lean.PersistentArray Lean.Meta.PostponedEntry
-- Mathlib.RingTheory.PowerSeries.Binomial
PowerSeries.binomialSeries_add : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : BinomialRing R] [inst_2 : Ring A] [inst_3 : Algebra R A]
  (r s : R), PowerSeries.binomialSeries A (r + s) = PowerSeries.binomialSeries A r * PowerSeries.binomialSeries A s
-- Mathlib.RingTheory.LittleWedderburn
/-- A finite domain is a field. See also `littleWedderburn` and `Fintype.divisionRingOfIsDomain`.  -/
Finite.isDomain_to_isField : ∀ (D : Type u_1) [Finite D] [inst : Ring D] [IsDomain D], IsField D
-- Mathlib.RingTheory.KrullDimension.Module
Module.supportDim_eq_ringKrullDim_quotient_annihilator : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M],
  Module.supportDim R M = ringKrullDim (R ⧸ Module.annihilator R M)
-- Mathlib.Analysis.Convex.Basic
/-- The preimage of a convex set under an affine map is convex.  -/
Convex.affine_preimage : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] (f : E →ᵃ[𝕜] F) {s : Set F},
  Convex 𝕜 s → Convex 𝕜 (⇑f ⁻¹' s)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instVAddSubtypeMem.eq_1 : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] (p : SubAddAction R M),
  p.instVAddSubtypeMem = { vadd := fun c x => ⟨c +ᵥ ↑x, ⋯⟩ }
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
ModuleCat.shortComplex_exact : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom S.f) ⇑(CategoryTheory.ConcreteCategory.hom S.g) → S.Exact
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftHom.whiskerLeft : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : C) →
        [inst_2 : Mathlib.Tactic.Coherence.LiftObj X] →
          {Y Z : C} →
            [inst_3 : Mathlib.Tactic.Coherence.LiftObj Y] →
              [inst_4 : Mathlib.Tactic.Coherence.LiftObj Z] →
                (f : Y ⟶ Z) →
                  [Mathlib.Tactic.Coherence.LiftHom f] →
                    Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
-- Mathlib.Data.List.Rotate
List.rotate_injective : ∀ {α : Type u} (n : ℕ), Function.Injective fun l => l.rotate n
-- Aesop.Builder.Apply
Aesop.RuleBuilderOptions.applyTransparency : Aesop.RuleBuilderOptions → Lean.Meta.TransparencyMode
-- Mathlib.Data.Complex.Basic
Complex.addGroupWithOne : AddGroupWithOne ℂ
-- Lean.Data.Lsp.Basic
Lean.Lsp.ApplyWorkspaceEditParams.mk.injEq : ∀ (label? : Option String) (edit : Lean.Lsp.WorkspaceEdit) (label?_1 : Option String) (edit_1 : Lean.Lsp.WorkspaceEdit),
  ({ label? := label?, edit := edit } = { label? := label?_1, edit := edit_1 }) = (label? = label?_1 ∧ edit = edit_1)
-- Mathlib.Tactic.Ring.PNat
Mathlib.Tactic.Ring.instCSLiftValPNatNatHMul : ∀ {n : ℕ+} {n' : ℕ} {k : ℕ+} {k' : ℕ} [h1 : Mathlib.Tactic.Ring.CSLiftVal n n']
  [h2 : Mathlib.Tactic.Ring.CSLiftVal k k'], Mathlib.Tactic.Ring.CSLiftVal (n * k) (n' * k')
-- Mathlib.Order.Closure
/-- The type of elements closed under a closure operator.  -/
ClosureOperator.Closeds : {α : Type u_1} → [inst : Preorder α] → ClosureOperator α → Type (max 0 u_1)
-- Mathlib.Analysis.ConstantSpeed
/-- `f` has constant speed `l` on `s` if the variation of `f` on `s ∩ Icc x y` is equal to
`l * (y - x)` for any `x y` in `s`.
 -/
HasConstantSpeedOnWith : {E : Type u_2} → [PseudoEMetricSpace E] → (ℝ → E) → Set ℝ → NNReal → Prop
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.srange_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M → N) (hf : ∀ (x y : M), f (x * y) = f x * f y),
  { toFun := f, map_mul' := hf }.srange = { carrier := Set.range f, mul_mem' := ⋯ }
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.refl : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  (x : MonCat.Colimits.Prequotient F), MonCat.Colimits.Relation F x x
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Embedding.substructureEquivMap_apply : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Embedding M N) (p : L.Substructure M) (x : ↥p), ↑((f.substructureEquivMap p) x) = f ↑x
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.instMonoInr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y], CategoryTheory.Mono (CategoryTheory.Limits.prod.inr X Y)
-- Mathlib.SetTheory.Cardinal.Order
/-- A cardinal is a strong limit if it is not zero and it is closed under powersets.
Note that `ℵ₀` is a strong limit by this definition.

See `IsStrongPrelimit` for a version including `0`.  -/
Cardinal.IsStrongLimit : Cardinal.{u_1} → Prop
-- Mathlib.Algebra.Lie.UniversalEnveloping
/-- The universal enveloping algebra of a Lie algebra.  -/
UniversalEnvelopingAlgebra : (R : Type u₁) → (L : Type u₂) → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → Type (max u₁ u₂)
-- Init.Data.SInt.Lemmas
Int32.ofNat_lt_iff_lt : ∀ {a b : ℕ}, a < 2 ^ 31 → b < 2 ^ 31 → (Int32.ofNat a < Int32.ofNat b ↔ a < b)
-- Mathlib.Data.Complex.Basic
Complex.div_natCast_im : ∀ (z : ℂ) (n : ℕ), (z / ↑n).im = z.im / ↑n
-- Mathlib.Topology.Constructible
IsCompact.isRetrocompact : ∀ {X : Type u_2} [inst : TopologicalSpace X] {U : Set X} [QuasiSeparatedSpace X],
  IsCompact U → IsOpen U → IsRetrocompact U
-- Mathlib.Algebra.Module.Hom
AddMonoid.End.smulCommClass : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_4} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : AddCommMonoid A]
  [inst_3 : DistribMulAction R A] [inst_4 : DistribMulAction S A] [SMulCommClass R S A],
  SMulCommClass R S (AddMonoid.End A)