mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.universes : Lean.Option Bool
-- Init.Data.AC
Lean.Data.AC.Expr.op.inj : ∀ {lhs rhs lhs_1 rhs_1 : Lean.Data.AC.Expr}, lhs.op rhs = lhs_1.op rhs_1 → lhs = lhs_1 ∧ rhs = rhs_1
-- Init.Data.UInt.Basic
/-- Converts an `Int` to a `UInt16` by taking the (non-negative remainder of the division by `2 ^ 16`.  -/
UInt16.ofInt : ℤ → UInt16
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.C_mul' : ∀ {R : Type u} [inst : Semiring R] (a : R) (f : Polynomial R), Polynomial.C a * f = a • f
-- Init.Data.List.Scan.Basic
/-- Auxiliary for `scanAuxM`  -/
_private.Init.Data.List.Scan.Basic.0.List.scanAuxM.go : {m : Type u_1 → Type u_2} →
  {β : Type u_1} → {α : Type u_3} → [Monad m] → (β → α → m β) → List α → β → List β → m (List β)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.toFullSubcategory_I_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X : P.FullSubcategory}
  (Q : HomotopicalAlgebra.Precylinder X.obj) (hQ : P Q.I), (Q.toFullSubcategory hQ).I.obj = Q.I
-- Mathlib.Analysis.Calculus.Deriv.Comp
/-- The composition `l ∘ f` where `l : F → E` and `f : 𝕜 → F`, has a derivative within a set
equal to the Fréchet derivative of `l` applied to the derivative of `f`.  -/
HasFDerivWithinAt.comp_hasDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : 𝕜 → F}
  {f' : F} (x : 𝕜) {s : Set 𝕜} {l : F → E} {l' : F →L[𝕜] E} {t : Set F},
  HasFDerivWithinAt l l' t (f x) → HasDerivWithinAt f f' s x → Set.MapsTo f s t → HasDerivWithinAt (l ∘ f) (l' f') s x
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.coe_subset_coe : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι}, ↑I ⊆ ↑J ↔ I ≤ J
-- Mathlib.Data.List.Rotate
List.getElem_rotate : ∀ {α : Type u} (l : List α) (n k : ℕ) (h : k < (l.rotate n).length), (l.rotate n)[k] = l[(k + n) % l.length]
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.equivLike : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {σ₂₁ : R₂ →+* R₁} →
            [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
              [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                {M₁ : Type u_4} →
                  [inst_4 : TopologicalSpace M₁] →
                    [inst_5 : AddCommMonoid M₁] →
                      {M₂ : Type u_5} →
                        [inst_6 : TopologicalSpace M₂] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R₁ M₁] → [inst_9 : Module R₂ M₂] → EquivLike (M₁ ≃SL[σ₁₂] M₂) M₁ M₂
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ker_toAddSubmonoid : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddZeroClass M] (f : G →+ M),
  f.ker.toAddSubmonoid = AddMonoidHom.mker f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α} {v : β},
  a ∈ t.insert k v ↔ cmp k a = Ordering.eq ∨ a ∈ t
-- Mathlib.Tactic.Simps.Basic
Simps.Config.mk.sizeOf_spec : ∀ (isSimp : Bool) (attrs : Array Lean.Elab.Attribute) (simpRhs dsimpLhs : Bool)
  (typeMd rhsMd : Lean.Meta.TransparencyMode) (fullyApplied : Bool) (notRecursive : List Lean.Name) (debug : Bool)
  (nameStem : Option String),
  sizeOf
      { isSimp := isSimp, attrs := attrs, simpRhs := simpRhs, dsimpLhs := dsimpLhs, typeMd := typeMd, rhsMd := rhsMd,
        fullyApplied := fullyApplied, notRecursive := notRecursive, debug := debug, nameStem := nameStem } =
    1 + sizeOf isSimp + sizeOf attrs + sizeOf simpRhs + sizeOf dsimpLhs + sizeOf typeMd + sizeOf rhsMd +
            sizeOf fullyApplied +
          sizeOf notRecursive +
        sizeOf debug +
      sizeOf nameStem
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_minKey!_eq_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {hc : t.minKey! ∈ t}, t.getKey t.minKey! hc = t.minKey ⋯
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_ideal : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals I.ideal = I
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
/-- The limit cone for the product with a zero object is limiting.  -/
CategoryTheory.Limits.binaryFanZeroLeftIsLimit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (X : C) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.binaryFanZeroLeft X)
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.Exact.isIso_cokerToKer' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ)
  (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
  (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc)
  (hkf : CategoryTheory.Limits.IsLimit kf), CategoryTheory.IsIso (hS.cokerToKer' k hk cc kf hcc hkf)
-- Mathlib.RingTheory.RegularLocalRing.Defs
IsRegularLocalRing.mk : ∀ {R : Type u_1} [inst : CommRing R] [toIsLocalRing : IsLocalRing R] [toIsNoetherian : IsNoetherian R R],
  ↑(Submodule.spanFinrank (IsLocalRing.maximalIdeal R)) = ringKrullDim R → IsRegularLocalRing R
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
/-- The centralizer of a permutation is contained in the alternating group if and only if
its cycles have odd length, with at most one of each, and there is at most one fixed point.  -/
Equiv.Perm.centralizer_le_alternating_iff : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {g : Equiv.Perm α},
  Subgroup.centralizer {g} ≤ alternatingGroup α ↔
    (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
hasMFDerivAt_neg : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {z : M} {f : M → E'} {f' : TangentSpace I z →L[𝕜] E'},
  HasMFDerivAt% (-f) z (-f') ↔ HasMFDerivAt% f z f'
-- Mathlib.Algebra.Group.Defs
SubNegMonoid.toZSMul : {G : Type u} → [self : SubNegMonoid G] → ZSMul G
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_5} {G : Type u_6} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [inst_8 : ContinuousConstSMul 𝕜 F] [inst_9 : AddCommGroup G] [inst_10 : Module 𝕜 G]
  [inst_11 : TopologicalSpace G] [inst_12 : IsTopologicalAddGroup G] [inst_13 : ContinuousConstSMul 𝕜 G] (g : F ≃L[𝕜] G)
  (f : ContinuousMultilinearMap 𝕜 E F),
  (ContinuousLinearEquiv.continuousMultilinearMapCongrRight E g) f = (↑g).compContinuousMultilinearMap f
-- Mathlib.Order.Std
/-- < is decidable. This can always be automatically derived from `decidableLE`.  -/
LinearOrder.OfStdArgs.decidableLT : {α : Type u_1} →
  (self : LinearOrder.OfStdArgs α) →
    let this := self.toPreorderArgs;
    let this := self.decidableLE;
    DecidableLT α
-- Mathlib.Algebra.Algebra.Equiv
MulSemiringAction.toAlgEquiv_apply : ∀ {G : Type u_2} (R : Type u_3) (A : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G A] [inst_5 : SMulCommClass G R A] (g : G) (a : A),
  (MulSemiringAction.toAlgEquiv R A g) a = g • a
-- Init.Data.Option.Lemmas
Option.pfilter_pfilter : ∀ {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} {q : (a : α) → o.pfilter p = some a → Bool},
  (o.pfilter p).pfilter q = o.pfilter fun a h => if h' : p a h = true then q a ⋯ else false
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.mk.injEq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] (functor : A → CategoryTheory.Functor C D)
  (shiftIso : (n a a' : A) → n + a = a' → ((functor a').comp (CategoryTheory.shiftFunctor D n) ≅ functor a))
  (shiftIso_zero : ∀ (a : A), shiftIso 0 a a ⋯ = (functor a).isoWhiskerLeft (CategoryTheory.shiftFunctorZero D A))
  (shiftIso_add :
    ∀ (n m a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a''),
      shiftIso (m + n) a a'' ⋯ =
        (functor a'').isoWhiskerLeft (CategoryTheory.shiftFunctorAdd D m n) ≪≫
          ((functor a'').associator (CategoryTheory.shiftFunctor D m) (CategoryTheory.shiftFunctor D n)).symm ≪≫
            CategoryTheory.Functor.isoWhiskerRight (shiftIso m a' a'' ha'') (CategoryTheory.shiftFunctor D n) ≪≫
              shiftIso n a a' ha')
  (functor_1 : A → CategoryTheory.Functor C D)
  (shiftIso_1 : (n a a' : A) → n + a = a' → ((functor_1 a').comp (CategoryTheory.shiftFunctor D n) ≅ functor_1 a))
  (shiftIso_zero_1 : ∀ (a : A), shiftIso_1 0 a a ⋯ = (functor_1 a).isoWhiskerLeft (CategoryTheory.shiftFunctorZero D A))
  (shiftIso_add_1 :
    ∀ (n m a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a''),
      shiftIso_1 (m + n) a a'' ⋯ =
        (functor_1 a'').isoWhiskerLeft (CategoryTheory.shiftFunctorAdd D m n) ≪≫
          ((functor_1 a'').associator (CategoryTheory.shiftFunctor D m) (CategoryTheory.shiftFunctor D n)).symm ≪≫
            CategoryTheory.Functor.isoWhiskerRight (shiftIso_1 m a' a'' ha'') (CategoryTheory.shiftFunctor D n) ≪≫
              shiftIso_1 n a a' ha'),
  ({ functor := functor, shiftIso := shiftIso, shiftIso_zero := shiftIso_zero, shiftIso_add := shiftIso_add } =
      { functor := functor_1, shiftIso := shiftIso_1, shiftIso_zero := shiftIso_zero_1,
        shiftIso_add := shiftIso_add_1 }) =
    (functor = functor_1 ∧ shiftIso ≍ shiftIso_1)
-- Lean.Level
_private.Lean.Level.0.Lean.Level.geq.go.match_1.eq_5 : ∀ (motive : Lean.Level → Lean.Level → Sort u_1) (u v : Lean.Level) (h_1 : (x : Lean.Level) → motive x Lean.Level.zero)
  (h_2 : (u v₁ v₂ : Lean.Level) → motive u (v₁.max v₂)) (h_3 : (u₁ u₂ v : Lean.Level) → motive (u₁.max u₂) v)
  (h_4 : (a u₂ v : Lean.Level) → motive (a.imax u₂) v) (h_5 : (u v : Lean.Level) → motive u.succ v.succ)
  (h_6 : (x x_1 : Lean.Level) → motive x x_1),
  (match u.succ, v.succ with
    | x, Lean.Level.zero => h_1 x
    | u, v₁.max v₂ => h_2 u v₁ v₂
    | u₁.max u₂, v => h_3 u₁ u₂ v
    | a.imax u₂, v => h_4 a u₂ v
    | u.succ, v.succ => h_5 u v
    | x, x_1 => h_6 x x_1) =
    h_5 u v
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanPrepareModuleHierarchyParams.fromJson : Lean.Json → Except String Lean.Lsp.LeanPrepareModuleHierarchyParams
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
irreducible_iff_prime_of_existsUnique_irreducible_factors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α],
  (∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ Associated f.prod a) →
    (∀ (f g : Multiset α),
        (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → Associated f.prod g.prod → Multiset.Rel Associated f g) →
      ∀ (p : α), Irreducible p ↔ Prime p
-- Mathlib.LinearAlgebra.Prod
LinearMap.ker_prodMap : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄] (f : M →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄),
  (f.prodMap g).ker = f.ker.prod g.ker
-- Mathlib.GroupTheory.Congruence.Defs
/-- A coercion from an additive congruence relation to its underlying binary relation.  -/
AddCon.instFunLikeForallProp : {M : Type u_1} → [inst : Add M] → FunLike (AddCon M) M (M → Prop)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.hasColimit_equivalence_comp_iff : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} (e : K ≌ J),
  CategoryTheory.Limits.HasColimit (e.functor.comp F) ↔ CategoryTheory.Limits.HasColimit F
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
AlgebraicGeometry.Scheme.ord_eq_unzero_ordHom : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X] {x : ↥X} (hx : Order.coheight x = 1) {f : ↑X.functionField}
  (hf : f ≠ 0), AlgebraicGeometry.Scheme.ord f x = Multiplicative.toAdd (WithZero.unzero ⋯)
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.symm_g₀ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E), P.symm.g₀ = P.f₀
-- Init.Data.Range.Polymorphic.BitVec
BitVec.instLawfulUpwardEnumerableLE : ∀ {n : ℕ}, Std.PRange.LawfulUpwardEnumerableLE (BitVec n)
-- Mathlib.Data.Finset.Range
Finset.coe_range : ∀ (n : ℕ), ↑(Finset.range n) = Set.Iio n
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Atom₁.mk.sizeOf_spec : ∀ (e : Lean.Expr) (src tgt : Mathlib.Tactic.BicategoryLike.Obj),
  sizeOf { e := e, src := src, tgt := tgt } = 1 + sizeOf e + sizeOf src + sizeOf tgt
-- Mathlib.Condensed.Discrete.Colimit
/-- A finite set as a coproduct cocone in `LightProfinite` over itself.  -/
LightCondensed.fintypeCatAsCofan : (X : LightProfinite) → CategoryTheory.Limits.Cofan fun x => LightProfinite.of PUnit.{u + 1}
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffAt.neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [LieAddGroup I n G] {f : M → G} {x₀ : M}, ContMDiffAt I' I n f x₀ → ContMDiffAt I' I n (fun x => -f x) x₀
-- Mathlib.GroupTheory.Finiteness
Monoid.fg_iff_add_fg : ∀ {M : Type u_1} [inst : Monoid M], Monoid.FG M ↔ AddMonoid.FG (Additive M)
-- Mathlib.Data.Stream.Init
Stream'.drop_zip : ∀ {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (n : ℕ) (s₁ : Stream' α) (s₂ : Stream' β),
  Stream'.drop n (Stream'.zip f s₁ s₂) = Stream'.zip f (Stream'.drop n s₁) (Stream'.drop n s₂)
-- Init.Data.Float.Float
/-- Computes the hyperbolic tangent of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`tanh`.
 -/
Float.tanh : Float → Float
-- Mathlib.Algebra.Order.Hom.Basic
/-- The argument is zero if its image under the map is zero.  -/
MulRingNormClass.eq_zero_of_map_eq_zero : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : NonAssocRing α} {inst_1 : Semiring β}
  {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : MulRingNormClass F α β] (f : F) {a : α}, f a = 0 → a = 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_insert_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {v : β k}, (m.insert k v).contains k = true
-- Std.Http.Data.Body.Full
/-- Builds a response with an HTML body.
Sets `Content-Type: text/html; charset=utf-8`.
 -/
Std.Http.Response.Builder.html : Std.Http.Response.Builder → String → Std.Async.Async (Std.Http.Response Std.Http.Body.Full)
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
Real.smoothTransition.eq_one_iff_one_le : ∀ {x : ℝ}, x.smoothTransition = 1 ↔ 1 ≤ x
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.toEquiv_addLeft : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableAdd G] (g : G),
  (MeasurableEquiv.addLeft g).toEquiv = Equiv.addLeft g
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- Build an isomorphism in the category `AlgCat R` from an `AlgEquiv` between `Algebra`s.  -/
AlgEquiv.toAlgebraIso : {R : Type u} →
  [inst : CommRing R] →
    {X₁ X₂ : Type v} →
      {g₁ : Ring X₁} →
        {g₂ : Ring X₂} → {m₁ : Algebra R X₁} → {m₂ : Algebra R X₂} → (X₁ ≃ₐ[R] X₂) → (AlgCat.of R X₁ ≅ AlgCat.of R X₂)
-- Mathlib.Topology.UniformSpace.AbstractCompletion
_private.Mathlib.Topology.UniformSpace.AbstractCompletion.0.AbstractCompletion.termHatα : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.NatTrans.whiskerLeft_app_tensor_app : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.MonoidalCategory C]
  {F G F' G' : CategoryTheory.Functor J C} (α : F ⟶ F') (β : G ⟶ G') {X' Y' : J} (f : X' ⟶ Y') (X : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (G.map f))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app X) (β.app Y')) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app X) (β.app X'))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F'.obj X) (G'.map f))
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.OLeanEntry.kind.injEq : ∀ (val val_1 : Lean.SyntaxNodeKind),
  (Lean.Parser.ParserExtension.OLeanEntry.kind val = Lean.Parser.ParserExtension.OLeanEntry.kind val_1) = (val = val_1)
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_mul_right_nhdsNE : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {c a : G},
  Filter.map (fun x => x * c) (nhdsWithin a {a}ᶜ) = nhdsWithin (a * c) {a * c}ᶜ
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- The right injection into a product is a non-unital algebra homomorphism.  -/
NonUnitalAlgHom.inr : (R : Type u) →
  [inst : Monoid R] →
    (A : Type v) →
      (B : Type w) →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : DistribMulAction R A] →
            [inst_3 : NonUnitalNonAssocSemiring B] → [inst_4 : DistribMulAction R B] → B →ₙₐ[R] A × B
-- Mathlib.Order.Max
noMinOrder_iff' : ∀ (α : Type u_3) [inst : LT α], NoMinOrder α ↔ ∀ (a : α), ∃ b, b < a
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.toFun.eq_1 : ∀ (t : Tactic.ComputeAsymptotics.Monomial) (basis : Tactic.ComputeAsymptotics.Basis),
  t.toFun basis = t.coef • t.unit.toFun basis
-- Mathlib.Algebra.Opposites
MulOpposite.unop_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] (a : α) (b : βᵐᵒᵖ), MulOpposite.unop (a • b) = a • MulOpposite.unop b
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.singleton_nonempty : ∀ (u : ZFSet.{u_1}), {u}.Nonempty
-- Mathlib.Order.RelSeries
LTSeries.length_range : ∀ (n : ℕ), (LTSeries.range n).length = n
-- Init.Data.UInt.Lemmas
UInt64.add_eq_left : ∀ {a b : UInt64}, a + b = a ↔ b = 0
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arccos`, version subtracting vectors.  -/
Orientation.oangle_sub_left_eq_arccos_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  o.oangle x y = ↑(Real.pi / 2) → o.oangle (x - y) x = ↑(Real.arccos (‖x‖ / ‖x - y‖))
-- Mathlib.Data.Fintype.Inv
Function.Embedding.right_inv_of_invOfMemRange : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] (f : α ↪ β) (a : α),
  f.invOfMemRange ⟨f a, ⋯⟩ = a
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.stabilizerEquivStabilizer_inv : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {g : G} {a b : α} (hg : b = g⁻¹ • a),
  MulAction.stabilizerEquivStabilizer hg = (MulAction.stabilizerEquivStabilizer ⋯).symm
-- Lean.Parser.Do
Lean.Parser.Term.doSeq.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.instHasWeakLimitsOfShapeOfHasLimitsOfShape : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.HasWeakLimitsOfShape J C
-- Mathlib.Topology.Category.CompHaus.Basic
CompHaus.hasColimits : CategoryTheory.Limits.HasColimits CompHaus
-- Mathlib.Order.Filter.Prod
Filter.prod_neBot : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, (f ×ˢ g).NeBot ↔ f.NeBot ∧ g.NeBot
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.associator_hom_apply_2_1 : ∀ {X Y Z : TopCat}
  {x : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)},
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) x).2.1 = x.1.2
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.isChain_cons_of_lt : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  Profinite.NobelingProof.contained C (Order.succ o) →
    ∀ (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)),
      ∀ q < (↑l).Tail, List.IsChain (fun x x_1 => x > x_1) (Profinite.NobelingProof.term I ho :: ↑q)
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.RingTheory.Ideal.Over
Ideal.liesOver_iff : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B] (P : Ideal B)
  (p : Ideal A), P.LiesOver p ↔ p = Ideal.under A P
-- Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
HomotopicalAlgebra.isCofibrant_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (X : C),
  HomotopicalAlgebra.IsCofibrant X ↔ HomotopicalAlgebra.Cofibration (CategoryTheory.Limits.initial.to X)
-- Lean.Elab.Exception
Lean.Elab.throwAbortTerm : {α : Type u_1} → {m : Type u_1 → Type u_2} → [MonadExcept Lean.Exception m] → m α
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.parseRequestTarget.absoluteHttp : Std.Http.URI.Config → Std.Internal.Parsec.ByteArray.Parser Std.Http.RequestTarget
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepSets.iInter : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ι → Set (Set Ω)}
  {s' : Set (Set Ω)}, (∃ n, ProbabilityTheory.IndepSets (s n) s' μ) → ProbabilityTheory.IndepSets (⋂ n, s n) s' μ
-- Mathlib.GroupTheory.Commutator.Basic
addCommutator_def : ∀ (G : Type u_1) [inst : AddGroup G], addCommutator G = ⁅⊤, ⊤⁆
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.dual_dual : ∀ {α : Type u_1} (M : Matroid α), M✶✶ = M
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.optionalNoAntiquot.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Tactic.TacticAnalysis
/-- The declaration, of type `Config`, that defines this pass.  -/
Mathlib.TacticAnalysis.Entry.declName : Mathlib.TacticAnalysis.Entry → Lean.Name