mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- The constant functor returning a specific initial object is indeed initial.  -/
CategoryTheory.Functor.isInitialConst : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {X : D} →
          CategoryTheory.Limits.IsInitial X → CategoryTheory.Limits.IsInitial ((CategoryTheory.Functor.const C).obj X)
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.maxInsts.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.algEquivOfRing_apply : ∀ (R : Type u) {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Module.Invertible R A] (x : R), (Module.Invertible.algEquivOfRing R A) x = (algebraMap R A) x
-- Init.Data.SInt.Lemmas
Int8.toInt_bmod_two_pow_numBits : ∀ (x : Int8), x.toInt.bmod (2 ^ System.Platform.numBits) = x.toInt
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.coe_fn_coe' : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B]
  (f : A →ₑ+[φ] B), ⇑↑f = ⇑f
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- The canonical continuous multilinear map on `R^ι`, associating to `m` the product of all the
`m i` (multiplied by a fixed reference element `z` in the target module)  -/
ContinuousMultilinearMap.mkPiRing : (R : Type u) →
  (ι : Type v) →
    {M : Type u_1} →
      [Fintype ι] →
        [inst : CommRing R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace R] →
                [inst_4 : TopologicalSpace M] →
                  [ContinuousMul R] → [ContinuousSMul R M] → M → ContinuousMultilinearMap R (fun x => R) M
-- Mathlib.Order.SuccPred.InitialSeg
InitialSeg.map_pred : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : PredOrder α] [NoMinOrder α]
  [inst_4 : PredOrder β] (f : α ≤i β) (a : α), f (Order.pred a) = Order.pred (f a)
-- Mathlib.Order.Interval.Finset.Nat
Nat.mod_injOn_Ico : ∀ (n a : ℕ), Set.InjOn (fun x => x % a) ↑(Finset.Ico n (n + a))
-- Init.Data.Range.Polymorphic.Fin
Fin.instLawfulHasSize : ∀ {n : ℕ}, Std.Rxc.LawfulHasSize (Fin n)
-- Mathlib.InformationTheory.KullbackLeibler.ChainRule
InformationTheory.klDiv_compProd_left : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} (μ ν : MeasureTheory.Measure 𝓧)
  (κ : ProbabilityTheory.Kernel 𝓧 𝓨) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [ProbabilityTheory.IsMarkovKernel κ],
  InformationTheory.klDiv (μ.compProd κ) (ν.compProd κ) = InformationTheory.klDiv μ ν
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instUniformSpace.eq_1 : ∀ {𝕜₁ : 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 : UniformSpace F] [inst_8 : IsUniformAddGroup F]
  (𝔖 : Set (Set E)),
  UniformConvergenceCLM.instUniformSpace σ F 𝔖 =
    (UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.uniformSpace E F 𝔖)).replaceTopology ⋯
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def
ProbabilityTheory.HasGaussianLaw.mk : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} [inst : TopologicalSpace E] [inst_1 : AddCommMonoid E]
  [inst_2 : Module ℝ E] [mE : MeasurableSpace E] {X : Ω → E} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map X P) → ProbabilityTheory.HasGaussianLaw X P
-- Lean.Meta.Basic
Lean.Meta.isLevelDefEqAux : Lean.Level → Lean.Level → Lean.MetaM Bool
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_mabs_div_mabs_le : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a b : α), ||a|ₘ / |b|ₘ|ₘ ≤ |a / b|ₘ
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor.congr_simp : ∀ {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) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  (F : CategoryTheory.Functor C V)
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution U F],
  CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor U F =
    CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor U F
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
instLinearOrderedAddCommMonoidWithTopOrderDualAdditive : {α : Type u_1} → [LinearOrderedCommMonoidWithZero α] → LinearOrderedAddCommMonoidWithTop (Additive α)ᵒᵈ
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.exists_countable_is_age_of_iff : ∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} [Countable ((l : ℕ) × L.Functions l)],
  (∃ M, Countable ↑M ∧ L.age ↑M = K) ↔
    K.Nonempty ∧
      (∀ (M N : CategoryTheory.Bundled L.Structure), Nonempty (L.Equiv ↑M ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        (Quotient.mk' '' K).Countable ∧
          (∀ M ∈ K, FirstOrder.Language.Structure.FG L ↑M) ∧
            FirstOrder.Language.Hereditary K ∧ FirstOrder.Language.JointEmbedding K
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- The composition of `C^n` functions on domains is `C^n`.  -/
ContMDiffOn.comp : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] {E'' : Type u_8} [inst_9 : NormedAddCommGroup E''] [inst_10 : NormedSpace 𝕜 E'']
  {H'' : Type u_9} [inst_11 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10}
  [inst_12 : TopologicalSpace M''] [inst_13 : ChartedSpace H M] [inst_14 : ChartedSpace H' M']
  [inst_15 : ChartedSpace H'' M''] {f : M → M'} {s : Set M} {n : WithTop ℕ∞} {t : Set M'} {g : M' → M''},
  ContMDiffOn I' I'' n g t → ContMDiffOn I I' n f s → s ⊆ f ⁻¹' t → ContMDiffOn I I'' n (g ∘ f) s
-- Mathlib.Algebra.Category.MonCat.Colimits
/-- The bundled monoid giving the colimit of a diagram.  -/
MonCat.Colimits.colimit : {J : Type v} → [inst : CategoryTheory.Category.{u, v} J] → CategoryTheory.Functor J MonCat → MonCat
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
ZMod.injective_toCircle : ∀ {N : ℕ} [inst : NeZero N], Function.Injective ⇑ZMod.toCircle
-- Std.Async.Basic
/-- Converts a `Async` to a `AsyncTask`.
 -/
Std.Async.Async.toIO : {α : Type} → Std.Async.Async α → IO (Std.Async.AsyncTask α)
-- Mathlib.Topology.Constructions.SumProd
Continuous.prodMk_left : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (y : Y),
  Continuous fun x => (x, y)
-- Mathlib.LinearAlgebra.Orientation
Module.Basis.orientation.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_4} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  (e : Module.Basis ι R M), e.orientation = rayOfNeZero R e.det ⋯
-- Mathlib.Topology.Sheaves.Flasque
/-- If the target category has a zero object, then any skyscraper sheaf valued in this category is a
flasque sheaf.
 -/
isFlasque_skyscraperSheaf_of_hasZeroObject : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} C] (A : C) [inst_2 : CategoryTheory.Limits.HasZeroObject C],
  (skyscraperSheaf p₀ A).IsFlasque
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.symm_reindexRingEquiv : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : Mul R]
  [inst_3 : AddCommMonoid R] (e : m ≃ n), (Matrix.reindexRingEquiv R e).symm = Matrix.reindexRingEquiv R e.symm
-- Mathlib.RingTheory.Nilpotent.Basic
IsNilpotent.isUnit_add_right_of_commute : ∀ {R : Type u_1} [inst : Ring R] {r u : R}, IsNilpotent r → IsUnit u → Commute r u → IsUnit (r + u)
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- A category is called preadditive if `P ⟶ Q` is an abelian group such that composition is
linear in both variables.  -/
CategoryTheory.Preadditive.comp_add_assoc : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Preadditive C] (P Q R : C) (f : P ⟶ Q)
  (g g' : Q ⟶ R) {Z : C} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (g + g') h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f g') h
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.IsPreimmersion.SpecMap_iff : ∀ {R S : CommRingCat} (f : R ⟶ S),
  AlgebraicGeometry.IsPreimmersion (AlgebraicGeometry.Spec.map f) ↔
    Topology.IsEmbedding (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ (CommRingCat.Hom.hom f).SurjectiveOnStalks
-- Aesop.Tree.UnsafeQueue
Aesop.instInhabitedUnsafeQueueEntry : Inhabited Aesop.UnsafeQueueEntry
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.hasSum_int_evenKernel : ∀ (a : ℝ) {t : ℝ}, 0 < t → HasSum (fun n => Real.exp (-Real.pi * (↑n + a) ^ 2 * t)) (HurwitzZeta.evenKernel (↑a) t)
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
GaussianFourier.integrable_cexp_neg_mul_sum_add : ∀ {b : ℂ} {ι : Type u_2} [inst : Fintype ι],
  0 < b.re →
    ∀ (c : ι → ℂ),
      MeasureTheory.Integrable (fun v => Complex.exp (-b * ∑ i, ↑(v i) ^ 2 + ∑ i, c i * ↑(v i))) MeasureTheory.volume
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.mono_of_cancel_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {Q R : C} (f : Q ⟶ R),
  (∀ {P : C} (g : P ⟶ Q), CategoryTheory.CategoryStruct.comp g f = 0 → g = 0) → CategoryTheory.Mono f
-- Lean.Util.CollectLooseBVars
Lean.Expr.CollectLooseBVars.State.mk.sizeOf_spec : ∀ (visited : Std.HashSet (ℕ × Lean.Expr)) (bvars : Std.HashSet ℕ),
  sizeOf { visited := visited, bvars := bvars } = 1 + sizeOf visited + sizeOf bvars
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Comma.ext : ∀ {A : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} A} {B : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} B}
  {T : Type u₃} {inst_2 : CategoryTheory.Category.{v₃, u₃} T} {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {x y : CategoryTheory.Comma L R},
  x.left = y.left → x.right = y.right → x.hom ≍ y.hom → x = y
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.le_preimage : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (f : SSet.RelativeMorphism A B φ),
  A ≤ B.preimage f.map
-- Mathlib.Combinatorics.SimpleGraph.UniversalVerts
/-- The set of vertices that are connected to all other vertices.
 -/
SimpleGraph.universalVerts : {V : Type u_1} → SimpleGraph V → Set V
-- Mathlib.Order.Defs.Unbundled
/-- **Alias** of `Std.Asymm.antisymm`. -/
Std.Asymm.isAntisymm : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Asymm r], Std.Antisymm r
-- Std.Async.TCP
/-- Listens for incoming connections with the given backlog.
 -/
Std.Async.TCP.Socket.Server.listen : Std.Async.TCP.Socket.Server → UInt32 → IO Unit
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α]
  {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → (Std.DHashMap.ofList l).getKey! k' = k
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.card_support_extend_domain : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {β : Type u_2} [inst_2 : DecidableEq β]
  [inst_3 : Fintype β] {p : β → Prop} [inst_4 : DecidablePred p] (f : α ≃ Subtype p) {g : Equiv.Perm α},
  (g.extendDomain f).support.card = g.support.card
-- Mathlib.Algebra.Free
FreeAddSemigroup.recOnPure.eq_1 : ∀ {α : Type u} {C : FreeAddSemigroup α → Sort l} (x : FreeAddSemigroup α) (ih1 : (x : α) → C (pure x))
  (ih2 : (x : α) → (y : FreeAddSemigroup α) → C (pure x) → C y → C (pure x + y)),
  x.recOnPure ih1 ih2 = x.recOnAdd ih1 ih2
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueSums.of_addOpposite : ∀ {G : Type u} [inst : Add G], UniqueSums Gᵃᵒᵖ → UniqueSums G
-- Lean.Meta.Tactic.Grind.Arith.Util
/-- Returns `true` if `e` is a numeral and has type `Int`.  -/
Lean.Meta.Grind.Arith.isIntNum : Lean.Expr → Bool
-- Lean.Parser.Term
Lean.Parser.Term.explicitUnivSuffix.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.map_comp_map : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] {M'' : Type u_6} {N'' : Type u_7} [inst_4 : MulOneClass M'']
  [inst_5 : MulOneClass N''] (f' : M' →* M'') (g' : N' →* N'') (f : M →* M') (g : N →* N'),
  (Monoid.Coprod.map f' g').comp (Monoid.Coprod.map f g) = Monoid.Coprod.map (f'.comp f) (g'.comp g)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.insertMany_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List ((a : α) × β a)} {p : (a : α) × β a},
  m.insertMany (p :: l) = (m.insert p.fst p.snd).insertMany l
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curryHomEquiv'_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.Closed X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X ⟹ Y),
  CategoryTheory.MonoidalClosed.curryHomEquiv'.symm g = CategoryTheory.MonoidalClosed.uncurry' g
-- Mathlib.CategoryTheory.Bicategory.Coherence
/-- The normalization of the composition of `p : Path a b` and `f : Hom b c`.
`p` will eventually be taken to be `nil` and we then get the normalization
of `f` alone, but the auxiliary `p` is necessary for Lean to accept the definition of
`normalizeIso` and the `whisker_left` case of `normalizeAux_congr` and `normalize_naturality`.
 -/
CategoryTheory.FreeBicategory.normalizeAux : {B : Type u} →
  [inst : Quiver B] → {a b c : B} → Quiver.Path a b → CategoryTheory.FreeBicategory.Hom b c → Quiver.Path a c
-- Init.Data.SInt.Lemmas
ISize.right_eq_add : ∀ {a b : ISize}, b = a + b ↔ a = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A biproduct over an index type with exactly one term is just the object over that term.  -/
CategoryTheory.Limits.biproductUniqueIso : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_2 : Unique J] → (f : J → C) → ⨁ f ≅ f default
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The projection onto a summand of a biproduct.  -/
CategoryTheory.Limits.biproduct.π : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (f : J → C) → [inst_2 : CategoryTheory.Limits.HasBiproduct f] → (b : J) → ⨁ f ⟶ f b
-- Init.Data.Nat.Basic
Nat.mul_comm : ∀ (n m : ℕ), n * m = m * n
-- Std.Data.Iterators.Lemmas.Producers.Vector
Std.Iterators.Vector.isPlausibleStep_iter_of_not_pos : ∀ {β : Type w} {n : ℕ} {xs : Vector β n}, ¬0 < n → xs.iter.IsPlausibleStep Std.IterStep.done
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
LocallyFiniteOrder.addMonoidHom.congr_simp : ∀ (G : Type u_2) [inst : AddCommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedAddMonoid G]
  [inst_3 : LocallyFiniteOrder G], LocallyFiniteOrder.addMonoidHom G = LocallyFiniteOrder.addMonoidHom G
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.lsum_apply : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : Semiring R] (s : HahnSeries.SummableFamily Γ R α),
  HahnSeries.SummableFamily.lsum s = s.hsum
-- Init.Data.Array.Lemmas
/-- Flattening a reverse is the same as reversing all parts and reversing the flattened result.  -/
Array.flatten_reverse : ∀ {α : Type u_1} {xss : Array (Array α)}, xss.reverse.flatten = (Array.map Array.reverse xss).flatten.reverse
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.inclusion_injective : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {K K' : LieSubalgebra R L} (h : K ≤ K'), Function.Injective ⇑(LieSubalgebra.inclusion h)
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.carrier_eq_coe : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Submodule R M),
  s.carrier = ↑s
-- Mathlib.AlgebraicGeometry.Spec
/-- The stalk map of `Spec M⁻¹R ⟶ Spec R` is an iso for each `p : Spec M⁻¹R`.  -/
AlgebraicGeometry.isIso_SpecMap_stakMap_localization : ∀ (R : CommRingCat) (M : Submonoid ↑R) (x : PrimeSpectrum (Localization M)),
  CategoryTheory.IsIso
    (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap
      (AlgebraicGeometry.Spec.toPresheafedSpace.map (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op) x)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- Fixing a point in affine space, homothety about this point gives a group homomorphism from (the
centre of) the units of the scalars into the group of affine equivalences.  -/
AffineEquiv.homothetyUnitsMulHom : {R : Type u_10} →
  {V : Type u_11} →
    {P : Type u_12} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → [inst_3 : AddTorsor V P] → P → Rˣ →* P ≃ᵃ[R] P
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.isIso_fst_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
  CategoryTheory.IsIso (CategoryTheory.Limits.pullback.fst f f)
-- Mathlib.CategoryTheory.Limits.Preorder
/-- If a cone is a limit, its point is a glb.  -/
Preorder.isGLB_of_isLimit : ∀ {C : Type u} [inst : Preorder C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} J]
  (F : CategoryTheory.Functor J C) {c : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit c),
  IsGLB (Set.range F.obj) c.pt
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyQuasiFinite f] {s : Set ↥Y},
  IsDiscrete s → IsDiscrete (⇑f ⁻¹' s)
-- Mathlib.GroupTheory.OrderOfElement
orderOf_eq_prime_pow : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {n p : ℕ} [hp : Fact (Nat.Prime p)],
  ¬x ^ p ^ n = 1 → x ^ p ^ (n + 1) = 1 → orderOf x = p ^ (n + 1)
-- Mathlib.Topology.UniformSpace.CompactConvergence
ContinuousMap.range_toUniformOnFunIsCompact : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β],
  Set.range ContinuousMap.toUniformOnFunIsCompact = {f | Continuous f}
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.structuredArrowEquivalence_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)),
  (CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).functor =
    CategoryTheory.CategoryOfElements.toStructuredArrow F
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.tracePositiveLinearMap_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E →ₗ[𝕜] E), (LinearMap.tracePositiveLinearMap 𝕜 E) x = (LinearMap.trace 𝕜 E) x
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.instPreservesColimitsOfShapeTopCatForget : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  [∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
  [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C],
  CategoryTheory.Limits.PreservesColimitsOfShape J (AlgebraicGeometry.PresheafedSpace.forget C)
-- Lean.Elab.Tactic.LibrarySearch
_private.Lean.Elab.Tactic.LibrarySearch.0.Lean.Elab.LibrarySearch.instEvalExprLibrarySearchConfig : Lean.Elab.ConfigEval.EvalExpr Lean.Parser.Tactic.LibrarySearchConfig
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_map : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [LawfulBEq α] [inst_3 : Inhabited γ] {f : α → β → γ} {k : α},
  (↑m).WF →
    Std.DHashMap.Internal.Raw₀.Const.get! (Std.DHashMap.Internal.Raw₀.map f m) k =
      (Option.map (f k) (Std.DHashMap.Internal.Raw₀.Const.get? m k)).get!
-- Lean.Data.Lsp.Window
Lean.Lsp.instToJsonMessageActionItem.toJson : Lean.Lsp.MessageActionItem → Lean.Json
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.unopFunctor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : CategoryTheory.ShortComplex Cᵒᵖ} (φ : X ⟶ Y),
  (CategoryTheory.ShortComplex.unopFunctor C).map φ = (CategoryTheory.ShortComplex.unopMap φ).op
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.finrank_pos_iff_of_free : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Free R M] [Module.Finite R M], 0 < Module.finrank R M ↔ Nontrivial M
-- Mathlib.RingTheory.Polynomial.Content
/-- In a field, the notion of primitive polynomials is degenerate.  -/
Polynomial.isPrimitive_iff_ne_zero : ∀ {F : Type u_2} [inst : Field F] (p : Polynomial F), p.IsPrimitive ↔ p ≠ 0
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_inv_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat))
  (ι : Type u_1) [inst_1 : Unique ι] {X S : C} (f : X ⟶ S)
  (X_1 : (CategoryTheory.Adjunction.ofCat (F.map f.op.toLoc).adj).toComonad.Coalgebra),
  ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).counitIso.inv.app X_1).f =
    CategoryTheory.CategoryStruct.id X_1.A
-- Mathlib.Order.Antisymmetrization
/-- **Alias** of `not_gt_of_antisymmRel`. -/
AntisymmRel.not_gt : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → ¬b < a
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- If a simplicial set `X` is representable by `⦋m⦌` for some `m : ℕ`, then this is the
corresponding isomorphism `Δ[m] ≅ X`.  -/
SSet.stdSimplex.isoOfRepresentableBy : {X : SSet} → {m : ℕ} → CategoryTheory.Functor.RepresentableBy X { len := m } → (SSet.stdSimplex.obj { len := m } ≅ X)
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- `Fib S` is a category.  -/
HasFibers.category : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳} →
        {p : CategoryTheory.Functor 𝒳 𝒮} →
          [self : HasFibers p] → (S : 𝒮) → CategoryTheory.Category.{v₃, u₃} (HasFibers.Fib p S)