mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.lift_conj_eq_mul_mul_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {X G : C}
  [inst_2 : CategoryTheory.GrpObj G] (f₁ f₂ : X ⟶ G) {Z : C} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrpObj.conj G) h) =
    CategoryTheory.CategoryStruct.comp (f₁ * f₂ * f₁⁻¹) h
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mahlerMeasure_def_of_ne_zero : ∀ {p : Polynomial ℂ},
  p ≠ 0 →
    p.mahlerMeasure =
      Real.exp ((2 * Real.pi)⁻¹ * ∫ (x : ℝ) in 0..2 * Real.pi, Real.log ‖Polynomial.eval (circleMap 0 1 x) p‖)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.im_smul_eq_div_normSq : ∀ (g : GL (Fin 2) ℝ) (z : UpperHalfPlane),
  (g • z).im = |↑(Matrix.GeneralLinearGroup.det g)| * z.im / Complex.normSq (UpperHalfPlane.denom g ↑z)
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.Result.no.sizeOf_spec : sizeOf Lean.Meta.Grind.Result.no✝ = 1
-- Mathlib.Topology.Separation.Hausdorff
IsIrreducible.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X), IsIrreducible s = (s.Nonempty ∧ IsPreirreducible s)
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_add_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W W₁ : E → E} {s : Set E} {x : E},
  DifferentiableWithinAt 𝕜 W s x →
    DifferentiableWithinAt 𝕜 W₁ s x →
      UniqueDiffWithinAt 𝕜 s x →
        VectorField.lieBracketWithin 𝕜 V (W + W₁) s x =
          VectorField.lieBracketWithin 𝕜 V W s x + VectorField.lieBracketWithin 𝕜 V W₁ s x
-- Mathlib.LinearAlgebra.Matrix.PosDef
/-- A matrix `M : Matrix n n R` is positive definite if it is Hermitian
and `xᴴMx` is greater than zero for all nonzero `x`.  -/
Matrix.PosDef.dotProduct_mulVec_pos : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [inst_3 : Fintype n]
  {M : Matrix n n R}, M.PosDef → ∀ {x : n → R}, x ≠ 0 → 0 < star x ⬝ᵥ M.mulVec x
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- Type-alias for modifications between strong transformations of oplax functors. This is the type
used for the 2-homomorphisms in the bicategory of oplax functors equipped with strong
transformations.  -/
CategoryTheory.Oplax.StrongTrans.Hom : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} → (F ⟶ G) → (F ⟶ G) → Type (max u₁ w₂)
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Construct a frame instance using the minimal amount of work needed.

This sets `a ⇨ b := sSup {c | c ⊓ a ≤ b}` and `aᶜ := a ⇨ ⊥`.  -/
Order.Frame.ofMinimalAxioms : {α : Type u} → [inst : CompleteLattice α] → Order.Frame.MinimalAxioms α → Order.Frame α
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeff_injective`. -/
SkewMonoidAlgebra.toFinsupp_injective : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k], Function.Injective SkewMonoidAlgebra.coeff
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologySequenceComposableArrows₅_exact : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [F.IsHomological] [inst_9 : F.ShiftSequence ℤ],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁), (F.homologySequenceComposableArrows₅ T n₀ n₁ h).Exact
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.isDenseInducing : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α), IsDenseInducing pkg.coe
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
/-- Coercion to a function as a `MonoidHom`. Similar to `MonoidHom.coeFn`.  -/
ContMDiffMap.coeFnMonoidHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {G : Type u_10} →
                                      [inst_9 : Monoid G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [inst_12 : ContMDiffMul I' n G] → ContMDiffMap I I' N G n →* N → G
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aeval_sumElim : ∀ {R : Type u} [inst : CommSemiring R] {S : Type u_2} {T : Type u_3} [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] {σ : Type u_4}
  {τ : Type u_5} (p : MvPolynomial (σ ⊕ τ) R) (f : τ → S) (g : σ → T),
  (MvPolynomial.aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p =
    (MvPolynomial.aeval g) ((MvPolynomial.aeval (Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ f))) p)
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.IsStrongLimit.mk : ∀ {c : Cardinal.{u_1}}, c ≠ 0 → c.IsStrongPrelimit → c.IsStrongLimit
-- Mathlib.Order.Irreducible
not_infIrred : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a : α}, ¬InfIrred a ↔ IsMax a ∨ ∃ b c, b ⊓ c = a ∧ a < b ∧ a < c
-- Mathlib.Data.List.Cycle
List.next.hcongr_5 : ∀ (α α' : Type u_1),
  α = α' →
    ∀ (inst : DecidableEq α) (inst' : DecidableEq α'),
      inst ≍ inst' →
        ∀ (l : List α) (l' : List α'),
          l ≍ l' → ∀ (x : α) (x' : α'), x ≍ x' → ∀ (h : x ∈ l) (h' : x' ∈ l'), h ≍ h' → l.next x h ≍ l'.next x' h'
-- Init.Data.UInt.Lemmas
UInt8.toUSize_add : ∀ (a b : UInt8), (a + b).toUSize = (a.toUSize + b.toUSize) % 256
-- Mathlib.FieldTheory.NormalizedTrace
/-- For a tower `K / E / F` of algebraic extensions, the normalized trace from `K` to `E` composed
with the normalized trace from `E` to `F` equals the normalized trace from `K` to `F`.  -/
Algebra.normalizedTrace_trans_apply : ∀ (F : Type u_3) (E : Type u_4) (K : Type u_5) [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra E K] [inst_5 : Algebra F K] [IsScalarTower F E K]
  [inst_7 : Algebra.IsIntegral F E] [inst_8 : Algebra.IsIntegral F K] [inst_9 : CharZero F]
  [inst_10 : Algebra.IsIntegral E K] [inst_11 : CharZero E] (a : K),
  (Algebra.normalizedTrace F E) ((Algebra.normalizedTrace E K) a) = (Algebra.normalizedTrace F K) a
-- Mathlib.Algebra.Module.LinearMap.Polynomial
Matrix.toMvPolynomial_constantCoeff : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : CommSemiring R] (M : Matrix m n R) (i : m),
  MvPolynomial.constantCoeff (M.toMvPolynomial i) = 0
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- If a short complex `S` is equipped with a splitting, then `S.X₃` is the cokernel of `S.f`.  -/
CategoryTheory.ShortComplex.Splitting.gIsCokernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} →
        [CategoryTheory.Limits.HasZeroObject C] →
          S.Splitting → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.unitHomEquiv_symm_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {M N : SheafOfModules R} (s : M.sections) (p : M ⟶ N),
  CategoryTheory.CategoryStruct.comp (M.unitHomEquiv.symm s) p = N.unitHomEquiv.symm (SheafOfModules.sectionsMap p s)
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.homologyι_opcyclesToCycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι)
  [inst_2 : K.HasHomology i] [inst_3 : K.HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.homologyι i) (K.opcyclesToCycles i j) = 0
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (i : X ⟶ Y) →
        (r : Y ⟶ X) →
          autoParam (CategoryTheory.CategoryStruct.comp i r = CategoryTheory.CategoryStruct.id X)
              CategoryTheory.Retract.retract._autoParam →
            CategoryTheory.Retract X Y
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- The `sSup` of a non-empty set is its least upper bound for a conditionally
complete lattice with a top.  -/
WithTop.isLUB_sSup' : ∀ {β : Type u_5} [inst : ConditionallyCompleteLattice β] {s : Set (WithTop β)}, s.Nonempty → IsLUB s (sSup s)
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_eq_lieBracketWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : (x : E) → TangentSpace (modelWithCornersSelf 𝕜 E) x} {s : Set E},
  VectorField.mlieBracketWithin (modelWithCornersSelf 𝕜 E) V W s = VectorField.lieBracketWithin 𝕜 V W s
-- Mathlib.LinearAlgebra.Dimension.Finite
exists_finset_linearIndependent_of_le_finrank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ},
  n ≤ Module.finrank R M → ∃ s, s.card = n ∧ LinearIndependent R Subtype.val
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.instInhabitedSimprocDecl : Inhabited Lean.Meta.Simp.SimprocDecl
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `FunLike.coe_mul`. -/
ContinuousLinearMap.coe_mul' : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : Mul β]
  [IsMulApply F α β] (f g : F), ⇑(f * g) = ⇑f * ⇑g
-- Init.Data.Vector.Find
Vector.findFinIdx?_singleton : ∀ {α : Type u_1} {a : α} {p : α → Bool}, Array.findFinIdx? p #[a] = if p a = true then some ⟨0, ⋯⟩ else none
-- Mathlib.Analysis.Convex.Topology
closure_subset_closedConvexHull : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] {s : Set E}, closure s ⊆ (closedConvexHull 𝕜) s
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_inv_naturality : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c₁ c₂ c₃ c₄ : C} {d₁ d₂ : D} (f : c₁ ⟶ c₂)
  (g : c₃ ⟶ c₄) (h : d₁ ⟶ d₂),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom g h))
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₂ c₄ d₂).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₁ c₃ d₁).inv
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
-- Mathlib.Order.Types.Defs
OrderType.liftOn_type : ∀ {δ : Sort v} (f : (α : Type u_1) → [LinearOrder α] → δ)
  (c :
    ∀ (α : Type u_1) [inst : LinearOrder α] (β : Type u_1) [inst_1 : LinearOrder β],
      OrderType.type α = OrderType.type β → f α = f β)
  {γ : Type u_1} [inst : LinearOrder γ], (OrderType.type γ).liftOn f c = f γ
-- Mathlib.Control.Fix
/-- `Fix α` provides a `fix` operator to define recursive computation
via the fixed point of function of type `α → α`.  -/
Fix : Type u_3 → Type u_3
-- Mathlib.Data.Multiset.Bind
Multiset.product_singleton : ∀ {α : Type u_1} {β : Type v} (a : α) (b : β), {a} ×ˢ {b} = {(a, b)}
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_eq_some_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.minKey? = some t.minKey!
-- Init.Prelude
/-- Returns the number of bytes in the byte array.

This is the number of bytes actually in the array, as distinct from its capacity, which is the
amount of memory presently allocated for the array.
 -/
ByteArray.size : ByteArray → ℕ
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- The type of `I`-adic Cauchy sequences is a submodule of the product `ℕ → M`.  -/
AdicCompletion.AdicCauchySequence.submodule : {R : Type u_1} →
  [inst : CommRing R] →
    Ideal R → (M : Type u_4) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Submodule R (ℕ → M)
-- Mathlib.Data.Num.Basic
/-- Division of `Num`s, where `x / 0 = 0`.  -/
Num.div : Num → Num → Num
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepFun.neg_right : ∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'}
  {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [inst_2 : Neg β'] [MeasurableNeg β'],
  ProbabilityTheory.CondIndepFun m' hm' f g μ → ProbabilityTheory.CondIndepFun m' hm' f (-g) μ
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.all₂.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (h_1 : Unit → motive [] [])
  (h_2 : (a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs))
  (h_3 : (x : List α) → (x_1 : List β) → motive x x_1),
  (match [], [] with
    | [], [] => h_1 ()
    | a :: as, b :: bs => h_2 a as b bs
    | x, x_1 => h_3 x x_1) =
    h_1 ()
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.id : ∀ {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α),
  MeasureTheory.Measure.QuasiMeasurePreserving id μ μ
-- Mathlib.Order.Booleanisation
/-- The bottom element of `Booleanisation α` is the bottom element of `α`.  -/
Booleanisation.instBot : {α : Type u_1} → [GeneralizedBooleanAlgebra α] → Bot (Booleanisation α)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instPartialOrder.eq_1 : ∀ {R : Type u} {M : Type v} [inst : SMul R M],
  SubMulAction.instPartialOrder = PartialOrder.ofSetLike (SubMulAction R M) M
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryProductIso_hom_comp_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.binaryProductIso F G).hom
      CategoryTheory.FunctorToTypes.prod.fst =
    CategoryTheory.Limits.prod.fst
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.typein.congr_simp : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r], Ordinal.typein r = Ordinal.typein r
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.dec.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (n : ℕ) (check persistent : Bool) (objs? : Option ℕ)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_13) (fvarId_1 : Lean.FVarId)
  (n_1 : ℕ) (check_1 persistent_1 : Bool) (objs?_1 : Option ℕ)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_13),
  (Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h =
      Lean.Compiler.LCNF.CodeDecl.dec fvarId_1 n_1 check_1 persistent_1 objs?_1 h_1) =
    (fvarId = fvarId_1 ∧ n = n_1 ∧ check = check_1 ∧ persistent = persistent_1 ∧ objs? = objs?_1)
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonnegative function and `x : R` is submultiplicative for `f`, then
`seminormFromBounded' f x = f x`.  -/
seminormFromBounded_of_mul_le : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ},
  0 ≤ f → ∀ {x : R}, (∀ (y : R), f (x * y) ≤ f x * f y) → f 1 ≤ 1 → seminormFromBounded' f x = f x
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPairEquiv_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (e : C ≌ C') (e' : D ≌ D'),
  (CategoryTheory.Join.mapPairEquiv e e').inverse = CategoryTheory.Join.mapPair e.inverse e'.inverse
-- Mathlib.Topology.Category.Profinite.AsLimit
/-- A bundled version of `X.asLimitCone` and `X.asLimit`.  -/
Profinite.lim : (X : Profinite) → CategoryTheory.Limits.LimitCone X.diagram
-- Init.Data.UInt.Lemmas
USize.ofInt_one : USize.ofInt 1 = 1
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instDivisionCommMonoid : {α : Type u_1} → [DivisionCommMonoid α] → DivisionCommMonoid (Lex α)
-- Mathlib.Algebra.Order.Group.Indicator
Set.mulIndicator_apply_le' : ∀ {α : Type u_2} {M : Type u_3} [inst : LE M] [inst_1 : One M] {s : Set α} {f : α → M} {a : α} {y : M},
  (a ∈ s → f a ≤ y) → (a ∉ s → 1 ≤ y) → s.mulIndicator f a ≤ y
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.T_gen.eq_1 : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  (F : Polynomial R) (a : ℤ_[p]),
  T_gen✝ p F a = ‖↑((Polynomial.aeval a) F) / ↑((Polynomial.aeval a) (Polynomial.derivative F) ^ 2)‖
-- Mathlib.CategoryTheory.Abelian.Basic
/-- The coimage-image comparison morphism is always an isomorphism in an abelian category.
See `CategoryTheory.Abelian.ofCoimageImageComparisonIsIso` for the converse.
 -/
CategoryTheory.Abelian.instIsIsoCoimageImageComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerRight_twice_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {H K : CategoryTheory.Functor B C} (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) (α : H ≅ K) {Z : CategoryTheory.Functor B E} (h : (K.comp F).comp G ≅ Z),
  CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Functor.isoWhiskerRight α F) G ≪≫ h =
    H.associator F G ≪≫ CategoryTheory.Functor.isoWhiskerRight α (F.comp G) ≪≫ (K.associator F G).symm ≪≫ h
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Construct an isomorphism of monoid objects by giving a monoid isomorphism between the underlying
objects.  -/
CategoryTheory.Mon.mkIso' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : C} →
        [inst_2 : CategoryTheory.MonObj M] →
          [inst_3 : CategoryTheory.MonObj N] →
            (e : M ≅ N) → [CategoryTheory.IsMonHom e.hom] → { X := M, mon := inst_2 } ≅ { X := N, mon := inst_3 }
-- Init.Grind.Module.Basic
Lean.Grind.NatModule.mul_nsmul : ∀ {M : Type u} [inst : Lean.Grind.NatModule M] (n m : ℕ) (a : M), (n * m) • a = n • m • a
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instRightCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : RightCancelMonoid α],
  Lex.instRightCancelMonoid = { toMonoid := Lex.instMonoid, toIsRightCancelMul := ⋯ }
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedPartialTermInfo : Inhabited Lean.Elab.PartialTermInfo
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM0.Cfg.map.match_1.splitter : {Γ : Type u_1} →
  [inst : Inhabited Γ] →
    {Λ : Type u_2} →
      (motive : Turing.TM0.Cfg Γ Λ → Sort u_3) →
        (x : Turing.TM0.Cfg Γ Λ) → ((q : Λ) → (T : Turing.Tape Γ) → motive { q := q, Tape := T }) → motive x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.cancelVar.eq_def : ∀ (m : Lean.Grind.CommRing.Mon) (x : Lean.Grind.CommRing.Var),
  m.cancelVar x =
    match m with
    | Lean.Grind.CommRing.Mon.unit => Lean.Grind.CommRing.Mon.unit
    | Lean.Grind.CommRing.Mon.mult pw m => bif pw.x == x then m else Lean.Grind.CommRing.Mon.mult pw (m.cancelVar x)
-- Mathlib.Geometry.Manifold.WhitneyEmbedding
_private.Mathlib.Geometry.Manifold.WhitneyEmbedding.0.SmoothBumpCovering.comp_embeddingPiTangent_mfderiv : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {H : Type uH} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_4 : TopologicalSpace M]
  [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I (↑⊤) M] [inst_7 : T2Space M] [inst_8 : Fintype ι] {s : Set M}
  (f : SmoothBumpCovering ι I M s) (x : M) (hx : x ∈ s),
  (ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (f.ind x hx)) ∘SL
      mfderiv% ⇑(SmoothBumpCovering.embeddingPiTangent✝ f) x =
    mfderiv% ↑(chartAt H (f.c (f.ind x hx))) x
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Balanced.below.blackR : ∀ {c₀ : RBTree.RBColor} {n₀ : ℕ} {α : Type u_1}
  {motive :
    (a : RBTree.RBNode.Path α) →
      (a_1 : RBTree.RBColor) → (a_2 : ℕ) → RBTree.RBNode.Path.Balanced c₀ n₀ a a_1 a_2 → Prop}
  {x : RBTree.RBNode α} {c₁ : RBTree.RBColor} {n : ℕ} {v : α} {parent : RBTree.RBNode.Path α} {c₂ : RBTree.RBColor}
  (a : x.Balanced c₁ n) (a_1 : RBTree.RBNode.Path.Balanced c₀ n₀ parent RBTree.RBColor.black (n + 1)),
  RBTree.RBNode.Path.Balanced.below a_1 →
    motive parent RBTree.RBColor.black (n + 1) a_1 → RBTree.RBNode.Path.Balanced.below ⋯
-- Mathlib.Data.Fin.Basic
Fin.coe_int_add_eq_mod : ∀ {n : ℕ} (u v : Fin n), ↑↑(u + v) = (↑↑u + ↑↑v) % ↑n
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.ext : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] {f g : StieltjesFunction R},
  (∀ (x : R), ↑f x = ↑g x) → f = g
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instFromJsonDiagnosticTag : Lean.FromJson Lean.Lsp.DiagnosticTag
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsCyclic.exists_monoid_generator : ∀ {α : Type u_1} [inst : Group α] [Finite α] [IsCyclic α], ∃ x, ∀ (y : α), y ∈ Submonoid.powers x
-- Init.Prelude
Nat.sub_lt : ∀ {n m : ℕ}, 0 < n → 0 < m → n - m < n
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.ext_iff : ∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] {f g : A →⋆ₙ+* B}, f = g ↔ ∀ (x : A), f x = g x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_f_2_comp_cochainsIso₂ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  CategoryTheory.CategoryStruct.comp ((groupCohomology.cochainsMap f φ).f 2) (groupCohomology.cochainsIso₂ B).hom =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₂ A).hom (groupCohomology.cochainsMap₂ f φ)
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
/-- `trailingCoeff p` gives the coefficient of the smallest power of `X` in `p`.  -/
Polynomial.trailingCoeff : {R : Type u} → [inst : Semiring R] → Polynomial R → R