mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Congruence.Defs
RingCon.coe_neg : ∀ {R : Type u_1} [inst : AddGroup R] [inst_1 : Mul R] (c : RingCon R) (x : R), ↑(-x) = -↑x
-- Init.Data.UInt.Lemmas
BitVec.ofFin_uInt8ToFin : ∀ (n : UInt8), { toFin := n.toFin } = n.toBitVec
-- Mathlib.Analysis.ODE.Gronwall
gronwallBound_ε0_δ0 : ∀ (K x : ℝ), gronwallBound 0 K 0 x = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The category of bicones on a given diagram.  -/
CategoryTheory.Limits.Bicone.category : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} → CategoryTheory.Category.{uC', max (max uC uC') w} (CategoryTheory.Limits.Bicone F)
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- An additive functor `C ⥤ D` factors through its lift to `Mat_ C ⥤ D`.  -/
CategoryTheory.Mat_.embeddingLiftIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          [inst_3 : CategoryTheory.Preadditive D] →
            [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts D] →
              (F : CategoryTheory.Functor C D) →
                [inst_5 : F.Additive] → (CategoryTheory.Mat_.embedding C).comp (CategoryTheory.Mat_.lift F) ≅ F
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- Any transvection structure can be converted to a special linear matrix.  -/
Matrix.TransvectionStruct.toSpecialLinearGroup : {ι : Type u_1} →
  {F : Type u_2} →
    [inst : DecidableEq ι] →
      [inst_1 : Fintype ι] → [inst_2 : CommRing F] → Matrix.TransvectionStruct ι F → Matrix.SpecialLinearGroup ι F
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- A `CorepresentableBy` structure that characterizes maps out of `F ⊛ U` by
leveraging the fact that `F ⊠ U` is a left Kan extension of `F ⊠ (fromPUnit 𝟙_ V)`.  -/
CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (U : CategoryTheory.Functor C V) →
              [CategoryTheory.MonoidalCategory.DayConvolutionUnit U] →
                (F : CategoryTheory.Functor C V) →
                  [∀ (v : V) (d : C),
                        CategoryTheory.Limits.PreservesColimitsOfShape
                          (CategoryTheory.CostructuredArrow
                            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
                          (CategoryTheory.MonoidalCategory.tensorLeft v)] →
                    [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F U] →
                      (((CategoryTheory.Functor.whiskeringLeft (C × C) C V).obj
                                (CategoryTheory.MonoidalCategory.tensor C)).comp
                            (((CategoryTheory.Functor.whiskeringLeft (C × CategoryTheory.Discrete PUnit.{1}) (C × C)
                                      V).obj
                                  ((CategoryTheory.Functor.id C).prod
                                    (CategoryTheory.Functor.fromPUnit
                                      (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))).comp
                              (CategoryTheory.coyoneda.obj
                                (Opposite.op
                                  (CategoryTheory.MonoidalCategory.externalProduct F
                                    (CategoryTheory.Functor.fromPUnit
                                      (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))))))).CorepresentableBy
                        (CategoryTheory.MonoidalCategory.DayConvolution.convolution F U)
-- Lean.Declaration
Lean.TheoremVal.toConstantVal : Lean.TheoremVal → Lean.ConstantVal
-- Mathlib.CategoryTheory.ObjectProperty.Ind
CategoryTheory.ObjectProperty.ind_inverseImage_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{u_2, u_1} D]
  (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v, u_2, u, u_1} F],
  (P.inverseImage F).ind ≤ P.ind.inverseImage F
-- Mathlib.CategoryTheory.Abelian.Exact
imageToKernel'.congr_simp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) (g : B ⟶ C) [inst_2 : CategoryTheory.Limits.HasKernels V] [inst_3 : CategoryTheory.Limits.HasImages V]
  (w : CategoryTheory.CategoryStruct.comp f g = 0), imageToKernel' f g w = imageToKernel' f g w
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_eq_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ∪ t = s ↔ t ⊆ s
-- Mathlib.LinearAlgebra.Complex.Module
realPart.eq_1 : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A],
  realPart = selfAdjointPart ℝ
-- Mathlib.Topology.MetricSpace.Completion
Isometry.mapRingHom_coe : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : Ring α] [inst_2 : IsTopologicalRing α]
  [inst_3 : IsUniformAddGroup α] [inst_4 : Ring β] [inst_5 : PseudoMetricSpace β] [inst_6 : IsUniformAddGroup β]
  [inst_7 : IsTopologicalRing β] {f : α →+* β} (h : Isometry ⇑f) (x : α), h.mapRingHom ↑x = ↑(f x)
-- Mathlib.FieldTheory.KummerExtension
IntermediateField.adjoin_root_eq_top_of_isSplittingField : ∀ {K : Type u} [inst : Field K] {n : ℕ},
  (primitiveRoots n K).Nonempty →
    ∀ {a : K},
      Irreducible (Polynomial.X ^ n - Polynomial.C a) →
        ∀ {L : Type u_1} [inst_1 : Field L] [inst_2 : Algebra K L]
          [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L},
          α ^ n = (algebraMap K L) a → K⟮α⟯ = ⊤
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.integrableOn_rpowIntegrand₀₁_Ioi : ∀ {p x : ℝ},
  p ∈ Set.Ioo 0 1 →
    0 ≤ x → MeasureTheory.IntegrableOn (fun x_1 => p.rpowIntegrand₀₁ x_1 x) (Set.Ioi 0) MeasureTheory.volume
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.isLeast_l : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {a : α}, IsLeast {b | a ≤ u b} (l a)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
instIsAddCyclicInt : IsAddCyclic ℤ
-- Std.Data.DHashMap.IteratorLemmas
_private.Std.Data.DHashMap.IteratorLemmas.0.Std.DHashMap.Internal.toListModel.eq_1 : ∀ {α : Type u} {β : α → Type v} (buckets : Array (Std.DHashMap.Internal.AssocList α β)),
  Std.DHashMap.Internal.toListModel buckets = List.flatMap Std.DHashMap.Internal.AssocList.toList buckets.toList
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.mod.eq_1 : ∀ {R : Type u} [inst : Field R] (p q : Polynomial R), p.mod q = p %ₘ (q * Polynomial.C q.leadingCoeff⁻¹)
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- Projection on `WithLp p (α × β)` with range `α` and kernel `β`  -/
WithLp.idemFst : {α : Type u_2} →
  {β : Type u_3} →
    [inst : SeminormedAddCommGroup α] →
      [inst_1 : SeminormedAddCommGroup β] → {p : ENNReal} → AddMonoid.End (WithLp p (α × β))
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- If a function is `C^n` around each point in a set, then it is `C^n` on the set.  -/
contDiffOn_of_locally_contDiffOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞}, (∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)) → ContDiffOn 𝕜 n f s
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- The 2-morphisms underlying the oplax naturality constraint.  -/
CategoryTheory.Lax.OplaxTrans.naturality : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          (self : CategoryTheory.Lax.OplaxTrans F G) →
            {a b : B} →
              (f : a ⟶ b) →
                CategoryTheory.CategoryStruct.comp (F.map f) (self.app b) ⟶
                  CategoryTheory.CategoryStruct.comp (self.app a) (G.map f)
-- Aesop.BuiltinRules.Subst
Aesop.BuiltinRules.substEqs? : Lean.MVarId → Array Lean.FVarId → Aesop.ScriptM (Option Lean.MVarId)
-- Mathlib.Analysis.Normed.Module.RieszLemma
Metric.closedBall_infDist_compl_subset_closure : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [NormedSpace ℝ F] {x : F} {s : Set F},
  x ∈ s → Metric.closedBall x (Metric.infDist x sᶜ) ⊆ closure s
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
multipliable_iff_nat_tprod_vanishing : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : UniformSpace G] [IsUniformGroup G] [CompleteSpace G] {f : ℕ → G},
  Multipliable f ↔ ∀ e ∈ nhds 1, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
-- Mathlib.CategoryTheory.Category.PartialFun
partialFunEquivPointed_inverse_map_Dom : ∀ {X Y : Pointed} (f : X ⟶ Y) (a : PartialFun.of { x // x ≠ X.point }),
  (partialFunEquivPointed.inverse.map f a).Dom = ¬f.toFun ↑a = Y.point
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.coe_sup : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (f g : CauSeq α abs),
  ↑(f ⊔ g) = ↑f ⊔ ↑g
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.inr.eq_1 : ∀ (G₀ : Type u_1) (H₀ : Type u_2) [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0],
  MonoidWithZeroHom.inr G₀ H₀ =
    (WithZero.map' (MonoidHom.inr G₀ˣ H₀ˣ)).comp (MonoidWithZeroHom.ofClass WithZero.withZeroUnitsEquiv.symm)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
/-- A variant of `hasFDerivAt_finCons` where the derivative variables are free on the RHS
instead.  -/
hasFDerivAt_finCons' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] (i : Fin n) → F' i.succ},
  HasFDerivAt (fun x => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x ↔ HasFDerivAt φ φ' x ∧ HasFDerivAt φs φs' x
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.map_apply : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {G : Type u_7} [inst_4 : NormedAddCommGroup G]
  [inst_5 : InnerProductSpace 𝕜 G] (b : OrthonormalBasis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G) (i : ι), (b.map L) i = L (b i)
-- Mathlib.Data.Nat.Prime.Defs
Nat.instDecidablePredIrreducible : DecidablePred Irreducible
-- Mathlib.LinearAlgebra.Finsupp.LSum
/-- Given compatible `S` and `R`-module structures on `M` and a type `X`, the set of functions
`X → M` is `S`-linearly equivalent to the `R`-linear maps from the free `R`-module
on `X` to `M`.  -/
Finsupp.llift : (M : Type u_2) →
  (R : Type u_5) →
    (S : Type u_8) →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module R M] →
              (X : Type u_9) → [inst_4 : Module S M] → [inst_5 : SMulCommClass R S M] → (X → M) ≃ₗ[S] (X →₀ R) →ₗ[R] M
-- Lean.Meta.Basic
/-- Instantiate assigned universe metavariables in `u`, and then normalize it.  -/
Lean.Meta.normalizeLevel : Lean.Level → Lean.MetaM Lean.Level
-- Mathlib.Order.RelClasses
WellFounded.asymmetric : ∀ {α : Sort u_1} {r : α → α → Prop}, WellFounded r → ∀ (a b : α), r a b → ¬r b a
-- Mathlib.RingTheory.Extension.ExtendScalars
/-- The first homology of the naive cotangent complex of `P.extendScalars` is
linearly equivalent to that of `S` over `P.Ring`.  -/
Algebra.Extension.h1CotangentExtendScalarsEquiv : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (P : Algebra.Extension R S) → P.extendScalars.H1Cotangent ≃ₗ[S] Algebra.H1Cotangent P.Ring S
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- It's a named argument. Named arguments inhibit applying unexpanders.  -/
Lean.PrettyPrinter.Delaborator.AppImplicitArg.named : Lean.TSyntax `Lean.Parser.Term.namedArgument → Lean.PrettyPrinter.Delaborator.AppImplicitArg
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isLittleO_neg_right`. -/
Asymptotics.IsLittleO.of_neg_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, (f =o[l] fun x => -g' x) → f =o[l] g'
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.addUnits_surjective : ∀ {M : Type u_1} [inst : AddMonoid M], Function.Surjective AddSubmonoid.addUnits
-- Mathlib.NumberTheory.ModularForms.Identities
SlashInvariantForm.vAdd_width_periodic : ∀ (N : ℕ) (k n : ℤ)
  (f : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k)
  (z : UpperHalfPlane), f (↑N * ↑n +ᵥ z) = f z
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.edist_eq_pi_restrict : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : PseudoEMetricSpace β] [inst_1 : Fintype ↑𝔖]
  {f g : UniformOnFun α β 𝔖},
  edist f g =
    edist (fun s => UniformFun.ofFun ((↑s).domRestrict ((UniformOnFun.toFun 𝔖) f))) fun s =>
      UniformFun.ofFun ((↑s).domRestrict ((UniformOnFun.toFun 𝔖) g))
-- Mathlib.Computability.Primrec.List
/-- If `R a b` is decidable, then for any fixed `n` and `y`, `g n y ↔ ∃ x < n, R x y` is a
primitive recursive relation.  -/
PrimrecRel.exists_lt : ∀ {R : ℕ → ℕ → Prop}, PrimrecRel R → PrimrecRel fun n y => ∃ x < n, R x y
-- Init.Data.Range.Polymorphic.Basic
Std.Rcc.lower_le_of_mem : ∀ {α : Type u} {r : Std.Rcc α} {a : α} [inst : LE α], a ∈ r → r.lower ≤ a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] [inst_3 : Inhabited β] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false →
    Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.Const.insertMany t l) k = Std.ExtDTreeMap.Const.get! t k
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.reduce_toWord : ∀ {α : Type u_1} [inst : DecidableEq α] (x : FreeAddGroup α), FreeAddGroup.reduce x.toWord = x.toWord
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.neg_toEquiv : ∀ (G : Type v) [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd G G]
  [inst_3 : IsIsometricVAdd Gᵃᵒᵖ G], (IsometryEquiv.neg G).toEquiv = Equiv.neg G
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.boundedBy_top : ∀ {α : Type u_1}, MeasureTheory.OuterMeasure.boundedBy ⊤ = ⊤
-- Batteries.Lean.TagAttribute
/-- Implementation of `TagAttribute.getDecls`.  -/
Lean.TagAttribute.getDecls.core : Lean.PersistentEnvExtensionState Lean.Name Lean.NameSet → Array Lean.Name
-- Mathlib.GroupTheory.GroupAction.SubMulAction
Units.orbitRel_nonZero_iff : ∀ (R : Type u_1) (M : Type u_2) [inst : Monoid R] [inst_1 : AddCommMonoid M] [inst_2 : DistribMulAction R M]
  (x y : { v // v ≠ 0 }), (MulAction.orbitRel Rˣ { v // v ≠ 0 }) x y ↔ (MulAction.orbitRel Rˣ M) ↑x ↑y
-- Mathlib.Order.RelSeries
RelSeries.mk : {α : Type u_1} →
  {r : SetRel α α} →
    (length : ℕ) →
      (toFun : Fin (length + 1) → α) → (∀ (i : Fin length), (toFun i.castSucc, toFun i.succ) ∈ r) → RelSeries r
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- A 1-morphism in the other direction.  -/
CategoryTheory.Bicategory.Equivalence.inv : {B : Type u₁} → [inst : CategoryTheory.Bicategory B] → {a b : B} → CategoryTheory.Bicategory.Equivalence a b → (b ⟶ a)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.coe_preimage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens}, ↑((TopologicalSpace.Opens.map f.base).obj U) = ⇑f ⁻¹' ↑U
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.lift.congr_simp : ∀ {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] {L : CategoryTheory.Functor C D}
  {W : CategoryTheory.MorphismProperty C} {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (self self_1 : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W E),
  self = self_1 →
    ∀ (F F_1 : CategoryTheory.Functor C E) (e_F : F = F_1) (x : W.IsInvertedBy F), self.lift F x = self_1.lift F_1 ⋯
-- Init.Data.Bool
Bool.not_ite_eq_false_eq_false : ∀ {p : Prop} [h : Decidable p] {b c : Bool}, (¬if p then b = false else c = false) ↔ if p then b = true else c = true
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- The point of `X`.  -/
AlgebraicGeometry.Scheme.Pullback.Triplet.x : {X Y S : AlgebraicGeometry.Scheme} → {f : X ⟶ S} → {g : Y ⟶ S} → AlgebraicGeometry.Scheme.Pullback.Triplet f g → ↥X
-- Init.Data.Array.Attach
Array.attach_ne_empty_iff : ∀ {α : Type u_1} {xs : Array α}, xs.attach ≠ #[] ↔ xs ≠ #[]
-- Init.System.ST
ST.Out : Type → Type → Type
-- Mathlib.Analysis.Complex.Norm
Complex.nnnorm_natCast : ∀ (n : ℕ), ‖↑n‖₊ = ↑n
-- Mathlib.Order.JordanHolder
CompositionSeries.mem_eraseLast_of_ne_of_mem : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s : CompositionSeries X} {x : X},
  x ≠ RelSeries.last s → x ∈ s → x ∈ RelSeries.eraseLast s
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter_σ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (j : Fin (m + 1)) (hi : autoParam (n + i = m) CategoryTheory.SimplicialObject.σ₀Iter_σ._auto_1),
  autoParam (↑j ≤ i) CategoryTheory.SimplicialObject.σ₀Iter_σ._auto_3 →
    CategoryTheory.CategoryStruct.comp (X.σ₀Iter i hi) (X.σ j) = X.σ₀Iter (i + 1) ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.stdSimplex.ext₀_iff : ∀ {X : SSet} {f g : X ⟶ SSet.stdSimplex.obj { len := 0 }}, f = g ↔ True
-- Mathlib.Order.Defs.LinearOrder
ne_iff_gt_or_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≠ b ↔ b < a ∨ a < b
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.isoStrongEpiMono_inv_comp_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] {X Y : C} {f : X ⟶ Y} {I' : C} (e : X ⟶ I')
  (m : I' ⟶ Y) (comm : CategoryTheory.CategoryStruct.comp e m = f) [inst_2 : CategoryTheory.StrongEpi e]
  [inst_3 : CategoryTheory.Mono m],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.isoStrongEpiMono e m comm).inv m =
    CategoryTheory.Limits.image.ι f
-- Init.Coe
/-- `CoeTail α β` is for coercions that can only appear at the end of a
sequence of coercions. That is, `α` can be further coerced via `Coe σ α` and
`CoeHead τ σ` instances but `β` will only be the expected type of the expression.
 -/
CoeTail : semiOutParam (Sort u) → Sort v → Sort (max (max 1 u) v)
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- A normal monomorphism is a morphism which is the kernel of some morphism.  -/
CategoryTheory.NormalMono.g : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {X Y : C} →
      {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} →
        {f : X ⟶ Y} → [self : CategoryTheory.NormalMono f] → Y ⟶ CategoryTheory.NormalMono.Z f
-- Mathlib.Algebra.Group.Defs
CancelCommMonoid.mk : {M : Type u} → [toCommMonoid : CommMonoid M] → [toIsLeftCancelMul : IsLeftCancelMul M] → CancelCommMonoid M
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.gfpApprox_zero : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α}, OrdinalApprox.gfpApprox f x 0 = x
-- Mathlib.RingTheory.Spectrum.Prime.Module
Module.support_subset_preimage_comap : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Module A M] [IsScalarTower R A M],
  Module.support A M ⊆ PrimeSpectrum.comap (algebraMap R A) ⁻¹' Module.support R M
-- Mathlib.Data.Finset.Prod
Finset.instSProd : {α : Type u_1} → {β : Type u_2} → SProd (Finset α) (Finset β) (Finset (α × β))
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Build a `MulEquiv` from an isomorphism in the category `CommMonCat`.  -/
CategoryTheory.Iso.commMonCatIsoToMulEquiv : {X Y : CommMonCat} → (X ≅ Y) → ↑X ≃* ↑Y
-- Mathlib.LinearAlgebra.CliffordAlgebra.Prod
CliffordAlgebra.commute_map_mul_map_of_isOrtho_of_mem_evenOdd_zero_left : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Qₙ : QuadraticForm R N} (f₁ : Q₁ →qᵢ Qₙ)
  (f₂ : Q₂ →qᵢ Qₙ),
  (∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)) →
    ∀ (m₁ : CliffordAlgebra Q₁) (m₂ : CliffordAlgebra Q₂) {i₂ : ZMod 2},
      m₁ ∈ CliffordAlgebra.evenOdd Q₁ 0 →
        m₂ ∈ CliffordAlgebra.evenOdd Q₂ i₂ → Commute ((CliffordAlgebra.map f₁) m₁) ((CliffordAlgebra.map f₂) m₂)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_μ_unmop_unmop : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).inverse X Y).unmop.unmop =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Init.Data.SInt.Lemmas
Int64.neg_inj : ∀ {a b : Int64}, -a = -b ↔ a = b
-- Mathlib.Analysis.Complex.Isometry
LinearIsometry.im_apply_eq_im : ∀ {f : ℂ →ₗᵢ[ℝ] ℂ}, f 1 = 1 → ∀ (z : ℂ), z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
-- Mathlib.ModelTheory.ElementarySubstructures
/-- An elementary substructure, regarded as a subset of the ambient structure, meets definable
sets.  -/
FirstOrder.Language.ElementarySubstructure.meetsDefinable : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (S : L.ElementarySubstructure M),
  FirstOrder.Language.MeetsDefinable ↑S
-- Mathlib.Data.Nat.DvdSequence
IsDvdSequence.const : ∀ (α : Type u_1) {β : Type u_2} [inst : Dvd α] [inst_1 : Monoid β] (b : β), IsDvdSequence fun x => b
-- Mathlib.Algebra.Star.Unitary
/-- The star monoid homomorphism between unitary subgroups induced by a star monoid homomorphism of
the underlying star monoids.  -/
Unitary.map : {R : Type u_2} →
  {S : Type u_3} →
    [inst : Monoid R] →
      [inst_1 : StarMul R] → [inst_2 : Monoid S] → [inst_3 : StarMul S] → (R →⋆* S) → ↥(unitary R) →⋆* ↥(unitary S)
-- Lean.Parser.Do
Lean.Parser.Term.doDbgTrace.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.BitVec.Lemmas
BitVec.not_sshiftRight : ∀ {w n : ℕ} {b : BitVec w}, ~~~b.sshiftRight n = (~~~b).sshiftRight n
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivaryOn_neg_left`. -/
AntivaryOn.of_neg_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β}, AntivaryOn (-f) g s → MonovaryOn f g s
-- Mathlib.CategoryTheory.Monad.Products
/-- `X ⨯ -` has a comonad structure. This is sometimes called the writer comonad.  -/
CategoryTheory.prodComonad : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → C → [CategoryTheory.Limits.HasBinaryProducts C] → CategoryTheory.Comonad C