mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.prod_ε_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E] {C' : Type u₁'}
  [inst_6 : CategoryTheory.Category.{v₁', u₁'} C'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor E C')
  [inst_7 : CategoryTheory.MonoidalCategory C'] [inst_8 : F.LaxMonoidal] [inst_9 : G.LaxMonoidal],
  (CategoryTheory.Functor.LaxMonoidal.ε (F.prod G)).1 = CategoryTheory.Functor.LaxMonoidal.ε F
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_obj_fst_obj : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  (J : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) (X_1 : X),
  ((CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X).obj J).fst.obj X_1 = (J.obj X_1).fst
-- Mathlib.RingTheory.Ideal.Operations
Ideal.coprime_of_no_prime_ge : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, (∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime) → IsCoprime I J
-- Mathlib.Algebra.Group.Hom.Basic
AddMonoidHom.add_apply : ∀ {M : Type u_2} {N : Type u_3} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] (f g : M →+ N) (x : M),
  (f + g) x = f x + g x
-- Mathlib.Algebra.Group.Center
Set.addCentralizer_empty : ∀ {M : Type u_1} [inst : Add M], ∅.addCentralizer = ⊤
-- Init.Prelude
/-- The zero element of the type.  -/
Zero.zero : {α : Type u} → [self : Zero α] → α
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet_mono : ∀ {V : Type u} {G G' : SimpleGraph V}, G ≤ G' → ∀ (v : V), G.neighborSet v ⊆ G'.neighborSet v
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.opObjEquiv_symm_yonedaEquiv_const : ∀ {X : SSet} {n : SimplexCategory} (x : X.obj (Opposite.op { len := 0 })),
  SSet.opObjEquiv.symm (SSet.yonedaEquiv (SSet.const x)) = SSet.yonedaEquiv (SSet.const (SSet.opObjEquiv.symm x))
-- Std.Http.Data.Status
/-- 429 Too Many Requests
 -/
Std.Http.Status.tooManyRequests : Std.Http.Status
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
/-- Euler's infinite product formula for the real sine function.  -/
Real.tendsto_euler_sin_prod : ∀ (x : ℝ),
  Filter.Tendsto (fun n => Real.pi * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2)) Filter.atTop
    (nhds (Real.sin (Real.pi * x)))
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.ext : ∀ {X Y : AlgebraicGeometry.Scheme} (f g : X.PartialMap Y) (e : f.domain = g.domain),
  f.hom = CategoryTheory.CategoryStruct.comp (X.isoOfEq e).hom g.hom → f = g
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.toContIntertwiningMap_refl : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V] {ρ : ContRepresentation R G V},
  ↑(ContRepresentation.Equiv.refl ρ) = ContIntertwiningMap.id
-- Mathlib.CategoryTheory.Limits.Preserves.Lattice
CategoryTheory.Limits.CompleteLattice.preservesColimitsOfSize_toFunctor : ∀ {α : Type u} {β : Type v} {F : Type u_1} [inst : FunLike F α β] (f : F) [inst_1 : CompleteLattice α]
  [inst_2 : CompleteLattice β] [inst_3 : sSupHomClass F α β],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, u, v, u, v} (↑f).toFunctor
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Constants are `C^∞`.  -/
contDiff_const : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {c : F},
  ContDiff 𝕜 n fun x => c
-- Mathlib.Data.Multiset.Fold
Multiset.fold_singleton : ∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b a : α),
  Multiset.fold op b {a} = op a b
-- Mathlib.Probability.Kernel.Composition.RadonNikodym
/-- The Radon-Nikodym derivative `∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ κ)` (with the same kernel) equals `∂μ/∂ν`.  -/
ProbabilityTheory.rnDeriv_measure_compProd_left : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ ν : MeasureTheory.Measure α)
  (κ : ProbabilityTheory.Kernel α β) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [ProbabilityTheory.IsFiniteKernel κ], (μ.compProd κ).rnDeriv (ν.compProd κ) =ᵐ[ν.compProd κ] fun p => μ.rnDeriv ν p.1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_eq_maxKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered → ∀ {he : t.isEmpty = false}, t.maxKey he = Std.Internal.List.maxKey t.toListModel ⋯
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.mk.inj : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {f : ι → ι'}
  {injective_f : Function.Injective f} {rel : ∀ {i₁ i₂ : ι}, c.Rel i₁ i₂ → c'.Rel (f i₁) (f i₂)} {f_1 : ι → ι'}
  {injective_f_1 : Function.Injective f_1} {rel_1 : ∀ {i₁ i₂ : ι}, c.Rel i₁ i₂ → c'.Rel (f_1 i₁) (f_1 i₂)},
  { f := f, injective_f := injective_f, rel := rel } = { f := f_1, injective_f := injective_f_1, rel := rel_1 } →
    f = f_1
-- Mathlib.Order.BoundedOrder.Basic
lt_top_of_lt : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α] {a b : α}, a < b → a < ⊤
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableOn.sum : ∀ {𝕜 : 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'] {s : Set M} {ι : Type} {t : Finset ι} {f : ι → M → E'},
  (∀ i ∈ t, MDiff[s] (f i)) → MDiff[s] (∑ i ∈ t, f i)
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_add : ∀ (a b : UInt8), (a + b).toUInt32 = (a.toUInt32 + b.toUInt32) % 256
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.rupUnits_insert : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n), (f.insert c).rupUnits = f.rupUnits
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Poly.cancelAux.match_1.eq_1 : ∀ (motive : Nat.Internal.Linear.Poly → Nat.Internal.Linear.Poly → Sort u_1) (m₁ : Nat.Internal.Linear.Poly)
  (h_1 : (m₁ : Nat.Internal.Linear.Poly) → motive m₁ []) (h_2 : (m₂ : Nat.Internal.Linear.Poly) → motive [] m₂)
  (h_3 :
    (k₁ : ℕ) →
      (v₁ : Nat.Internal.Linear.Var) →
        (m₁ : List (ℕ × Nat.Internal.Linear.Var)) →
          (k₂ : ℕ) →
            (v₂ : Nat.Internal.Linear.Var) →
              (m₂ : List (ℕ × Nat.Internal.Linear.Var)) → motive ((k₁, v₁) :: m₁) ((k₂, v₂) :: m₂)),
  (match m₁, [] with
    | m₁, [] => h_1 m₁
    | [], m₂ => h_2 m₂
    | (k₁, v₁) :: m₁, (k₂, v₂) :: m₂ => h_3 k₁ v₁ m₁ k₂ v₂ m₂) =
    h_1 m₁
-- Mathlib.CategoryTheory.Abelian.LeftDerived
/-- The natural transformation `F.leftDerived 0 ⟶ F`.  -/
CategoryTheory.Functor.fromLeftDerivedZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.HasProjectiveResolutions C] →
            [inst_4 : CategoryTheory.Abelian D] →
              (F : CategoryTheory.Functor C D) → [inst_5 : F.Additive] → F.leftDerived 0 ⟶ F
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.instCommRingCore : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] → [inst_2 : Algebra R S] → {P : Algebra.Presentation R S ι σ} → CommRing P.Core
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.dual_ordSeparatingSet : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Set α},
  (⇑OrderDual.ofDual ⁻¹' s).ordSeparatingSet (⇑OrderDual.ofDual ⁻¹' t) = ⇑OrderDual.ofDual ⁻¹' s.ordSeparatingSet t
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The type of blocks for an additive group action containing a given element  -/
AddAction.BlockMem : (G : Type u_1) → [inst : AddGroup G] → {X : Type u_2} → [AddAction G X] → X → Type u_2
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β}, k ∉ m₁ → (m₁ ∩ m₂).getD k fallback = fallback
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- In a principal ideal ring, the order of vanishing of an irreducible element is `1`.
 -/
Ring.ord_of_irreducible : ∀ {R : Type u_1} [inst : CommRing R] [IsPrincipalIdealRing R] {ϖ : R}, Irreducible ϖ → Ring.ord R ϖ = 1
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The norm, relative to `ℤ`, of `ζ - 1` in a `p`-th cyclotomic extension of `ℚ` is `p` if
`p ≠ 2`.  -/
IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two' : ∀ {p : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p), p ≠ 2 → (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑p
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonWorkspaceSymbolParams.fromJson : Lean.Json → Except String Lean.Lsp.WorkspaceSymbolParams
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsOpenMap : (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsOpenMap).RespectsIso
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
HomotopyCategory.Plus.instIsLocalizationPlusCompQuotientQuasiIsoOfQuasiIso : ∀ {C : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor (HomotopyCategory.Plus C) H)
  [L.IsLocalization (HomotopyCategory.Plus.quasiIso C)],
  ((HomotopyCategory.Plus.quotient C).comp L).IsLocalization (CochainComplex.Plus.quasiIso C)
-- Init.Data.SInt.Lemmas
ISize.toBitVec_ofIntClamp : ∀ {n : ℤ},
  ISize.minValue.toInt ≤ n →
    n ≤ ISize.maxValue.toInt → (ISize.ofIntClamp n).toBitVec = BitVec.ofInt System.Platform.numBits n
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
/-- A `PMF` which assigns probability `p` to `true` and `1 - p` to `false`.  -/
PMF.bernoulli : (p : NNReal) → p ≤ 1 → PMF Bool
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → γ} {k : α}, (Std.ExtTreeMap.map f t).contains k = t.contains k
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
Fintype.not_linearIndependent_iffₒₛ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : LinearOrder R] [CanonicallyOrderedAdd R] [AddRightReflectLE R] [IsCancelAdd M]
  [inst_7 : DecidableEq ι] [inst_8 : Fintype ι],
  ¬LinearIndependent R v ↔ ∃ t f, ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i ∧ ∃ i ∈ t, 0 < f i
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Construct a natural isomorphism between `parallelPair f g` and `parallelPair f' g'` given
equalities `f = f'` and `g = g'`.  -/
CategoryTheory.Limits.parallelPair.eqOfHomEq : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g f' g' : X ⟶ Y} →
        f = f' → g = g' → (CategoryTheory.Limits.parallelPair f g ≅ CategoryTheory.Limits.parallelPair f' g')
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.snd_obj : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] (a : B × C),
  (CategoryTheory.Bicategory.Prod.snd B C).obj a = a.2
-- Mathlib.Algebra.Algebra.Equiv
/-- `ULift` is functorial for algebra homomorphisms.  -/
AlgHom.ulift : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : Semiring T] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra R T] → (S →ₐ[R] T) → ULift.{u₁, u_2} S →ₐ[ULift.{u₂, u_1} R] ULift.{u₃, u_3} T
-- Init.Data.Bool
Bool.exists_bool : ∀ {p : Bool → Prop}, (∃ b, p b) ↔ p false ∨ p true
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.instZSMul : {𝕜 : 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] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {n : WithTop ℕ∞} →
                              {V : M → Type u_6} →
                                [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                  [inst_9 : (x : M) → TopologicalSpace (V x)] →
                                    [inst_10 : FiberBundle F V] →
                                      [inst_11 : (x : M) → AddCommGroup (V x)] →
                                        [inst_12 : (x : M) → Module 𝕜 (V x)] →
                                          [VectorBundle 𝕜 F V] → SMul ℤ (ContMDiffSection I F n V)
-- Mathlib.GroupTheory.Perm.Fin
Fin.cons_apply_cycleRange : ∀ {n : ℕ} {α : Type u_1} (a : α) (x : Fin n → α) (p j : Fin (n + 1)), Fin.cons a x (p.cycleRange j) = p.insertNth a x j
-- Std.Async.Process
Std.IO.Process.ResourceUsageStats.mk.sizeOf_spec : ∀ (cpuUserTime cpuSystemTime : Std.Time.Millisecond.Offset)
  (peakResidentSetSizeKb sharedMemorySizeKb unsharedDataSizeKb unsharedStackSizeKb minorPageFaults majorPageFaults
    swapOperations blockInputOps blockOutputOps messagesSent messagesReceived signalsReceived voluntaryContextSwitches
    involuntaryContextSwitches : UInt64),
  sizeOf
      { cpuUserTime := cpuUserTime, cpuSystemTime := cpuSystemTime, peakResidentSetSizeKb := peakResidentSetSizeKb,
        sharedMemorySizeKb := sharedMemorySizeKb, unsharedDataSizeKb := unsharedDataSizeKb,
        unsharedStackSizeKb := unsharedStackSizeKb, minorPageFaults := minorPageFaults,
        majorPageFaults := majorPageFaults, swapOperations := swapOperations, blockInputOps := blockInputOps,
        blockOutputOps := blockOutputOps, messagesSent := messagesSent, messagesReceived := messagesReceived,
        signalsReceived := signalsReceived, voluntaryContextSwitches := voluntaryContextSwitches,
        involuntaryContextSwitches := involuntaryContextSwitches } =
    1 + sizeOf cpuUserTime + sizeOf cpuSystemTime + sizeOf peakResidentSetSizeKb + sizeOf sharedMemorySizeKb +
                            sizeOf unsharedDataSizeKb +
                          sizeOf unsharedStackSizeKb +
                        sizeOf minorPageFaults +
                      sizeOf majorPageFaults +
                    sizeOf swapOperations +
                  sizeOf blockInputOps +
                sizeOf blockOutputOps +
              sizeOf messagesSent +
            sizeOf messagesReceived +
          sizeOf signalsReceived +
        sizeOf voluntaryContextSwitches +
      sizeOf involuntaryContextSwitches
-- Batteries.Classes.Order
Std.TransCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm : ∀ {α : Type u_1} [inst : LT α] [inst_1 : LE α] [inst_2 : DecidableLT α] [inst_3 : DecidableEq α],
  (∀ (x : α), ¬x < x) →
    (∀ {x y z : α}, x < y → y < z → x < z) →
      (∀ {x y : α}, ¬x < y → y ≤ x) →
        (∀ {x y : α}, x ≤ y → y ≤ x → x = y) → Std.TransCmp fun x1 x2 => compareOfLessAndEq x1 x2
-- Mathlib.Algebra.Algebra.Basic
Module.End.instAlgebra : (R : Type u) →
  (S : Type v) →
    (M : Type w) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module R M] →
              [inst_4 : Module S M] →
                [SMulCommClass S R M] → [inst_6 : SMul R S] → [IsScalarTower R S M] → Algebra R (Module.End S M)
-- Mathlib.Topology.Algebra.Ring.Basic
Subsemiring.le_topologicalClosure : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Semiring R] [inst_2 : IsSemitopologicalSemiring R]
  (s : Subsemiring R), s ≤ s.topologicalClosure
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.colimitIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E) [inst_4 : CategoryTheory.Limits.HasColimit G],
  (CategoryTheory.Functor.Final.colimitIso F G).inv = CategoryTheory.inv (CategoryTheory.Limits.colimit.pre G F)
-- Mathlib.Analysis.Matrix.Order
/-- [**Schur product theorem**][schur1911] (positive semidefinite version): the Hadamard (entrywise)
product of positive semidefinite matrices is positive semidefinite.  -/
Matrix.PosSemidef.hadamard : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {ι : Type u_3} {A B : Matrix ι ι 𝕜},
  A.PosSemidef → B.PosSemidef → (A.hadamard B).PosSemidef
-- Mathlib.Order.Filter.Pointwise
Filter.vadd_filter_neBot_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter β} {a : α}, (a +ᵥ f).NeBot ↔ f.NeBot
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstr.p : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr → Lean.Grind.CommRing.Poly
-- Mathlib.Data.List.Defs
List.iterate.eq_def : ∀ {α : Type u_1} (f : α → α) (a : α) (x : ℕ),
  List.iterate f a x =
    match x with
    | 0 => []
    | n.succ => a :: List.iterate f (f a) n
-- Init.Omega.Constraint
_private.Init.Omega.Constraint.0.Option.merge.match_1.eq_4 : ∀ {α : Type u_1} (motive : Option α → Option α → Sort u_2) (x y : α) (h_1 : Unit → motive none none)
  (h_2 : (x : α) → motive (some x) none) (h_3 : (y : α) → motive none (some y))
  (h_4 : (x y : α) → motive (some x) (some y)),
  (match some x, some y with
    | none, none => h_1 ()
    | some x, none => h_2 x
    | none, some y => h_3 y
    | some x, some y => h_4 x y) =
    h_4 x y
-- Mathlib.LinearAlgebra.Matrix.RowCol
/-- `M *ᵥ v` is the vector whose entries are those of `M * replicateCol ι v`.  -/
Matrix.replicateCol_mulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_6} [inst : Fintype n] [inst_1 : NonUnitalNonAssocSemiring α]
  (M : Matrix m n α) (v : n → α), Matrix.replicateCol ι (M.mulVec v) = M * Matrix.replicateCol ι v
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.lt_of_stdPart_lt : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x : K} (f : ℝ →+*o K) {r : ℝ},
  0 ≤ ArchimedeanClass.mk x → ArchimedeanClass.stdPart x < r → x < f r
-- Mathlib.CategoryTheory.Quotient
Quot.liftOn.congr_simp : ∀ {α : Sort u} {β : Sort v} {r : α → α → Prop} (q q_1 : Quot r),
  q = q_1 → ∀ (f f_1 : α → β) (e_f : f = f_1) (c : ∀ (a b : α), r a b → f a = f b), q.liftOn f c = q_1.liftOn f_1 ⋯
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isColoop_iff_forall_mem_isBase : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.Hom.match_1.splitter : {C : Type u_1} →
  (motive : CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → Sort u_2) →
    (x x_1 : CategoryTheory.WithTerminal C) →
      ((X Y : C) → motive (CategoryTheory.WithTerminal.of X) (CategoryTheory.WithTerminal.of Y)) →
        ((a : C) → motive CategoryTheory.WithTerminal.star (CategoryTheory.WithTerminal.of a)) →
          ((x : CategoryTheory.WithTerminal C) → motive x CategoryTheory.WithTerminal.star) → motive x x_1
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- Definition of the `n`th exterior power of an `R`-module `M`. We introduce the notation
`⋀[R]^n M` for `exteriorPower R n M`.  -/
ExteriorAlgebra.exteriorPower : (R : Type u1) →
  [inst : CommRing R] →
    ℕ → (M : Type u2) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Submodule R (ExteriorAlgebra R M)
-- Mathlib.Analysis.Analytic.ChangeOrigin
/-- For any function `f` from a normed vector space to a Banach space, the set of points `x` such
that `f` is analytic at `x` is open.  -/
isOpen_analyticAt : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] (f : E → F),
  IsOpen {x | AnalyticAt 𝕜 f x}
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instContinuousMulOfLocallyCompactSpace : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [LocallyCompactSpace α]
  [inst_3 : Mul β] [inst_4 : ContinuousMul β], ContinuousMul C(α, β)
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.fromInducedMonoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategoryStruct D] →
            (F : CategoryTheory.Functor D C) →
              [inst_4 : F.Faithful] → (fData : CategoryTheory.Monoidal.InducingFunctorData F) → F.Monoidal
-- Mathlib.Topology.Homotopy.Basic
/-- Given a `HomotopyRel f₀ f₁ S`, we can define a `HomotopyRel f₁ f₀ S` by reversing the homotopy.
 -/
ContinuousMap.HomotopyRel.symm : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f₀ f₁ : C(X, Y)} → {S : Set X} → f₀.HomotopyRel f₁ S → f₁.HomotopyRel f₀ S
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_sum_single : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α],
  0 < p.toReal →
    ∀ (f : (i : α) → E i) (s : Finset α), ‖∑ i ∈ s, lp.single p i (f i)‖ ^ p.toReal = ∑ i ∈ s, ‖f i‖ ^ p.toReal
-- Aesop.Forward.RuleInfo
/-- The premises that appear in the rule's conclusion.  -/
Aesop.ForwardRuleInfo.conclusionDeps : Aesop.ForwardRuleInfo → Array Aesop.PremiseIndex
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Result.rfl.sizeOf_spec : ∀ (done contextDependent : optParam Bool false),
  sizeOf (Lean.Meta.Sym.Simp.Result.rfl done contextDependent) = 1 + sizeOf done + sizeOf contextDependent
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.monoidHomCongrLeft_apply : ∀ {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [inst : MulOneClass M₁] [inst_1 : MulOneClass M₂]
  [inst_2 : CommMonoid N] (e : M₁ ≃* M₂) (f : M₁ →* N), e.monoidHomCongrLeft f = f.comp ↑e.symm
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.Hom.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C C}
  {V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} {x y : V₀.Hom V₁}, x.f = y.f → x = y