mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.empty' : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommMonoid G] {C : Set (Set α)} (self : MeasureTheory.AddContent G C),
  self.toFun ∅ = 0
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.match_1.congr_eq_4 : ∀ (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1) (x : ByteArray.utf8DecodeChar?.FirstByte)
  (h_1 : x = ByteArray.utf8DecodeChar?.FirstByte.invalid → motive ByteArray.utf8DecodeChar?.FirstByte.invalid)
  (h_2 : x = ByteArray.utf8DecodeChar?.FirstByte.done → motive ByteArray.utf8DecodeChar?.FirstByte.done)
  (h_3 : x = ByteArray.utf8DecodeChar?.FirstByte.oneMore → motive ByteArray.utf8DecodeChar?.FirstByte.oneMore)
  (h_4 : x = ByteArray.utf8DecodeChar?.FirstByte.twoMore → motive ByteArray.utf8DecodeChar?.FirstByte.twoMore)
  (h_5 : x = ByteArray.utf8DecodeChar?.FirstByte.threeMore → motive ByteArray.utf8DecodeChar?.FirstByte.threeMore)
  (heq_1 : x = ByteArray.utf8DecodeChar?.FirstByte.twoMore),
  (match h : x with
    | ByteArray.utf8DecodeChar?.FirstByte.invalid => h_1 h
    | ByteArray.utf8DecodeChar?.FirstByte.done => h_2 h
    | ByteArray.utf8DecodeChar?.FirstByte.oneMore => h_3 h
    | ByteArray.utf8DecodeChar?.FirstByte.twoMore => h_4 h
    | ByteArray.utf8DecodeChar?.FirstByte.threeMore => h_5 h) ≍
    h_4 heq_1
-- Lean.SubExpr
Lean.SubExpr.GoalLocation.hypValue.inj : ∀ {a : Lean.FVarId} {a_1 : Lean.SubExpr.Pos} {a_2 : Lean.FVarId} {a_3 : Lean.SubExpr.Pos},
  Lean.SubExpr.GoalLocation.hypValue a a_1 = Lean.SubExpr.GoalLocation.hypValue a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- Given a diagram of `StructuredArrow X F`s, we may obtain a cone with cone point `X`.  -/
CategoryTheory.Limits.Cone.fromStructuredArrow : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (F : CategoryTheory.Functor C D) →
              {X : D} →
                (G : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X F)) →
                  CategoryTheory.Limits.Cone (G.comp ((CategoryTheory.StructuredArrow.proj X F).comp F))
-- Mathlib.Algebra.Algebra.Basic
NoZeroDivisors.of_faithfulSMul : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A]
  [NoZeroDivisors A], NoZeroDivisors R
-- Mathlib.Algebra.Homology.Embedding.Extend
/-- The canonical isomorphism `K.op.extend e.op ≅ (K.extend e).op`.  -/
HomologicalComplex.extendOpIso : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
              [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
                (K : HomologicalComplex C c) → (e : c.Embedding c') → K.op.extend e.op ≅ (K.extend e).op
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instIsDomain : ∀ {R : Type u_1} [inst : Ring R] [IsDomain R], IsDomain Rᵒᵈ
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- If `f` is a local homeomorphism and the point `a` is in its target,
and if `f` is `n` times continuously differentiable at `f.symm a`,
and if the derivative at `f.symm a` is a continuous linear equivalence,
then `f.symm` is `n` times continuously differentiable at the point `a`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function.  -/
OpenPartialHomeomorph.contDiffAt_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  [CompleteSpace E] (f : OpenPartialHomeomorph E F) {f₀' : E ≃L[𝕜] F} {a : F},
  a ∈ f.target → HasFDerivAt (↑f) (↑f₀') (↑f.symm a) → ContDiffAt 𝕜 n (↑f) (↑f.symm a) → ContDiffAt 𝕜 n (↑f.symm) a
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.finite_multiples : ∀ {G : Type u_1} [inst : AddMonoid G] {a : G}, IsOfFinAddOrder a → (↑(AddSubmonoid.multiples a)).Finite
-- Lean.Meta.Match.Match
Lean.Meta.Match.MkMatcherInput.matchType : Lean.Meta.Match.MkMatcherInput → Lean.Expr
-- Init.Data.String.Basic
/-- Given a position in `s.sliceFrom p₀`, obtain the corresponding position in `s`.  -/
String.Slice.Pos.ofSliceFrom : {s : String.Slice} → {p₀ : s.Pos} → (s.sliceFrom p₀).Pos → s.Pos
-- Mathlib.Data.List.Infix
List.inits_eq_tails : ∀ {α : Type u_1} (l : List α), l.inits = (List.map List.reverse l.reverse.tails).reverse
-- Mathlib.Topology.Separation.Regular
RegularSpace.of_lift'_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X], (∀ (x : X), (nhds x).lift' closure = nhds x) → RegularSpace X
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instAdditiveTruncLT : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ), (t.truncLT n).Additive
-- Mathlib.CategoryTheory.Filtered.Basic
/-- For every cospan `j ⟶ i ⟵ j'`,
there exists a cone `j ⟵ k ⟶ j'` such that the square commutes.  -/
CategoryTheory.IsCofiltered.cospan : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {i j j' : C} (f : j ⟶ i)
  (f' : j' ⟶ i), ∃ k g g', CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp g' f'
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.range_eq_map_coprodSubtypeLEquivOfIsCompl : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_5} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] (f : E →L[𝕜] F) {G : Submodule 𝕜 F} (h : IsCompl (↑f).range G)
  [inst_7 : CompleteSpace ↥G] (hker : (↑f).ker = ⊥),
  (↑f).range = Submodule.map (↑↑(f.coprodSubtypeLEquivOfIsCompl h hker)) (⊤.prod ⊥)
-- Std.Data.TreeMap.Raw.Basic
/-- Given a proof that a mapping for the given key is present, retrieves the mapping for the given key.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.TreeMap.Raw.get : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → (t : Std.TreeMap.Raw α β cmp) → (a : α) → a ∈ t → β
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.isIso₁_truncLE_map_of_isGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ n₁ : ℤ), n₀ + 1 = n₁ → t.IsGE T.obj₃ n₁ → CategoryTheory.IsIso ((t.truncLE n₀).map T.mor₁)
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.trim_comap_apply : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β} (hf : Measurable f) {s : Set β},
  MeasurableSet s → (μ.trim ⋯) (f ⁻¹' s) = (MeasureTheory.Measure.map f μ) s
-- Mathlib.Algebra.Order.Ring.Cone
/-- `RingConeClass S R` says that `S` is a type of cones in `R`.  -/
RingConeClass : (S : Type u_1) → (R : outParam (Type u_2)) → [Ring R] → [SetLike S R] → Prop
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.isIso_actionHomLeft : ∀ {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.MonoidalRightAction C D] {x y : D} (f : x ⟶ y) [CategoryTheory.IsIso f]
  (z : C), CategoryTheory.IsIso (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f z)
-- Init.Data.ToString.Basic
instToStringULift : {α : Type u} → [ToString α] → ToString (ULift.{v, u} α)
-- Mathlib.LinearAlgebra.Matrix.Block
/-- Let `b` map rows and columns of a square matrix `M` to blocks indexed by `α`s. Then
`BlockTriangular M n b` says the matrix is block triangular.  -/
Matrix.BlockTriangular : {α : Type u_1} → {m : Type u_3} → {R : Type v} → [LT α] → [Zero R] → Matrix m m R → (m → α) → Prop
-- Mathlib.Topology.Instances.ENNReal.Lemmas
Real.ediam_Ioo : ∀ (a b : ℝ), Metric.ediam (Set.Ioo a b) = ENNReal.ofReal (b - a)
-- Mathlib.Data.Fin.SuccPred
Fin.castSucc_pred_eq_pred_castSucc : ∀ {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ 0), (a.pred ha).castSucc = a.castSucc.pred ⋯
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.le_self_mul_inv : ∀ {K : Type u_3} [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K}, I ≤ 1 → I ≤ I * I⁻¹
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_vecMulVec : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [Nontrivial n]
  (u v : n → R), (Matrix.vecMulVec u v).det = 0
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOpRightOpEquiv_functor_map_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ} (η : X ⟶ Y) (x : C),
  ((CategoryTheory.Functor.leftOpRightOpEquiv C D).functor.map η).app x = (η.unop.app (Opposite.op x)).op
-- Mathlib.Logic.Equiv.List
Encodable.decodeList.eq_1 : ∀ {α : Type u_1} [inst : Encodable α], Encodable.decodeList 0 = some []
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Multipliable.even_mul_odd : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M] {f : ℕ → M},
  (Multipliable fun k => f (2 * k)) → (Multipliable fun k => f (2 * k + 1)) → Multipliable f
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_union_of_subset : ∀ {α : Type u_1} {s t : Set α}, t ⊆ s → s \ t ∪ t = s
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_eq_getKey! : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {a : α} {h : a ∈ m}, m.getKey a h = m.getKey! a
-- Mathlib.Analysis.Convex.BetweenList
List.Sbtw.wbtw : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {l : List P}, List.Sbtw R l → List.Wbtw R l
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
_private.Mathlib.Analysis.SpecificLimits.ArithmeticGeometric.0.arithGeom.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- Nested monoid algebras can be taken in an arbitrary order.  -/
MonoidAlgebra.commRingEquiv : {R : Type u_3} →
  {M : Type u_6} →
    {N : Type u_7} →
      [inst : Semiring R] →
        [inst_1 : Monoid M] →
          [inst_2 : Monoid N] → MonoidAlgebra (MonoidAlgebra R M) N ≃+* MonoidAlgebra (MonoidAlgebra R N) M
-- Mathlib.Algebra.Homology.Bifunctor
CategoryTheory.Functor.mapBifunctorHomologicalComplex.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] (F F_1 : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  (e_F : F = F_1) {I₁ : Type u_4} {I₂ : Type u_5} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂)
  [inst_6 : F.PreservesZeroMorphisms] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms],
  F.mapBifunctorHomologicalComplex c₁ c₂ = F_1.mapBifunctorHomologicalComplex c₁ c₂
-- Batteries.Data.Array.Basic
/-- Fold a function `f` over the array from the left, returning the array of partial results.
```
scanl (· + ·) 0 #[1, 2, 3] = #[0, 1, 3, 6]
```
 -/
Array.scanl : {β : Type u_1} → {α : Type u_2} → (β → α → β) → β → (as : Array α) → optParam ℕ 0 → optParam ℕ as.size → Array β
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.instIsOverToRationalMapOfIsOver : ∀ {X Y S : AlgebraicGeometry.Scheme} [inst : X.Over S] [inst_1 : Y.Over S] (f : X.PartialMap Y)
  [AlgebraicGeometry.Scheme.PartialMap.IsOver S f], AlgebraicGeometry.Scheme.RationalMap.IsOver S f.toRationalMap
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_union_of_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → k ∈ m₁ ∪ m₂
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.one_of_isUnit' : ∀ {R : Type u} {Γ₀ : Type v} [inst : CommRing R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O R] {x : O},
  IsUnit x → (∀ (x : O), v ((algebraMap O R) x) ≤ 1) → v ((algebraMap O R) x) = 1
-- Mathlib.Order.GaloisConnection.Basic
/-- Lift the suprema along a Galois insertion  -/
GaloisInsertion.liftSemilatticeSup : {α : Type u} →
  {β : Type v} →
    {l : α → β} →
      {u : β → α} → [inst : PartialOrder β] → [inst_1 : SemilatticeSup α] → GaloisInsertion l u → SemilatticeSup β
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braidedCategory_braiding : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C]
  (X₁ X₂ : CategoryTheory.Arrow C), β_ X₁ X₂ = CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding X₁ X₂
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.exists_lt_of_tendsto_atBot : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsDirectedOrder α] {u : α → β} [inst_2 : Preorder β]
  [NoMinOrder β], Filter.Tendsto u Filter.atTop Filter.atBot → ∀ (a : α) (b : β), ∃ a', a ≤ a' ∧ u a' < b
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
HomotopyCategory.distinguished_iff_iso_trianglehOfDegreewiseSplit : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasBinaryBiproducts C]
  (T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))),
  T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔
    ∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.complexEmbedding_complexConj : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K] (φ : K →+* ℂ) (x : K),
  φ ((NumberField.IsCMField.complexConj K) x) = (starRingEnd ℂ) (φ x)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.le_comap : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : H →g G), H ≤ SimpleGraph.comap (⇑f) G
-- Init.Data.Order.LemmasExtra
Std.instLawfulEqOrdOfLawfulOrderOrdOfIsPartialOrder : ∀ {α : Type u} [inst : Ord α] [inst_1 : LE α] [Std.LawfulOrderOrd α] [Std.IsPartialOrder α], Std.LawfulEqOrd α
-- Mathlib.Topology.KrullDimension
/-- The Krull dimension of a topological space is the supremum of lengths of chains of
closed irreducible sets.
 -/
topologicalKrullDim : (T : Type u_1) → [TopologicalSpace T] → WithBot ℕ∞
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instSemiring : {α : Type u_5} → [inst : NonUnitalNonAssocSemiring α] → Semiring (CentroidHom α)
-- Mathlib.Data.Set.Insert
Set.eq_empty_of_ssubset_singleton : ∀ {α : Type u_1} {s : Set α} {x : α}, s ⊂ {x} → s = ∅
-- Std.Data.HashMap.Raw
/-- Monadically computes a value by folding the given function over the mappings in the hash
map in some order.
 -/
Std.HashMap.Raw.foldM : {α : Type u} →
  {β : Type v} → {m : Type w → Type w'} → [Monad m] → {γ : Type w} → (γ → α → β → m γ) → γ → Std.HashMap.Raw α β → m γ
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (j : C), ((t.triangleLTGE n).obj j).mor₂ = (t.truncGEπ n).app j
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- Algebra equivalences between `Algebra`s are the same as (isomorphic to) isomorphisms in
`AlgCat`.  -/
algEquivIsoAlgebraIso : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      [inst_1 : Ring X] →
        [inst_2 : Ring Y] →
          [inst_3 : Algebra R X] → [inst_4 : Algebra R Y] → (X ≃ₐ[R] Y) ≅ AlgCat.of R X ≅ AlgCat.of R Y
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- Determinant of 2x2 matrix  -/
Matrix.det_fin_two : ∀ {R : Type v} [inst : CommRing R] (A : Matrix (Fin 2) (Fin 2) R), A.det = A 0 0 * A 1 1 - A 0 1 * A 1 0
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
/-- An arbitrary choice of factors of `x : M` is exactly the (unique) normalized set of factors,
if `M` has a trivial group of units.  -/
UniqueFactorizationMonoid.factors_eq_normalizedFactors : ∀ {M : Type u_2} [inst : CommMonoidWithZero M] [inst_1 : UniqueFactorizationMonoid M] [inst_2 : Subsingleton Mˣ]
  (x : M), UniqueFactorizationMonoid.factors x = UniqueFactorizationMonoid.normalizedFactors x
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.mapsTo_symm : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), Set.MapsTo (↑e.symm) e.target e.source
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Expr.updateLambdaS! : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.hull_le_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {C : ConvexCone R M} {s : Set M}, ConvexCone.hull R s ≤ C ↔ s ⊆ ↑C
-- Mathlib.RingTheory.Jacobson.Semiprimary
IsSemiprimaryRing.isNilpotent : ∀ {R : Type u_1} {inst : Ring R} [self : IsSemiprimaryRing R], IsNilpotent (Ring.jacobson R)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instCompleteSemilatticeInf : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : TopologicalSpace M] → [inst_3 : Module R M] → CompleteSemilatticeInf (ClosedSubmodule R M)
-- Mathlib.SetTheory.Lists
Lists'.mem_cons : ∀ {α : Type u_1} {a y : Lists α} {l : Lists' α true}, a ∈ Lists'.cons y l ↔ a.Equiv y ∨ a ∈ l
-- Mathlib.RingTheory.Multiplicity
not_pow_dvd_of_emultiplicity_lt : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {m : ℕ}, emultiplicity a b < ↑m → ¬a ^ m ∣ b
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.tactic.sizeOf_spec : ∀ (stx : Lean.Syntax), sizeOf (Lean.Elab.CompletionInfo.tactic stx) = 1 + sizeOf stx
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.leftUnitor_inv_left_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (Y : CategoryTheory.Over X) {Z : C} (h : Y.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.id X) Y.hom) h) =
    h
-- Mathlib.Algebra.Quaternion
Quaternion.coe_smul : ∀ {S : Type u_1} {R : Type u_3} [inst : CommRing R] [inst_1 : SMulZeroClass S R] (s : S) (r : R), ↑(s • r) = s • ↑r
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.forget₂AddCommGroup_reflectsLimitOfShape : ∀ {R : Type u} [inst : Ring R] {J : Type v} [inst_1 : CategoryTheory.Category.{t, v} J],
  CategoryTheory.Limits.ReflectsLimitsOfShape J (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.instCoeSortType : CoeSort AddMagmaCat (Type u)
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.fderiv_aeval : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {R : Type u_1} [inst_1 : CommSemiring R]
  [inst_2 : Algebra R 𝕜] (q : Polynomial R),
  fderiv 𝕜 (fun x => (Polynomial.aeval x) q) x =
    ContinuousLinearMap.smulRight 1 ((Polynomial.aeval x) (Polynomial.derivative q))
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- A lax monoidal functor takes monoid objects to monoid objects.

That is, a lax monoidal functor `F : C ⥤ D` induces a functor `Mon C ⥤ Mon D`.
 -/
CategoryTheory.Functor.mapMon : {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] →
            (F : CategoryTheory.Functor C D) →
              [F.LaxMonoidal] → CategoryTheory.Functor (CategoryTheory.Mon C) (CategoryTheory.Mon D)
-- Init.Data.BitVec.Lemmas
BitVec.msb_eq_getMsbD : ∀ {w : ℕ} (x : BitVec w), x.msb = x.getMsbD 0
-- Mathlib.Algebra.BigOperators.Fin
/-- `finSigmaFinEquiv` on `Fin 1 × f` is just `f`  -/
finSigmaFinEquiv_one : ∀ {n : Fin 1 → ℕ} (ij : (i : Fin 1) × Fin (n i)), ↑(finSigmaFinEquiv ij) = ↑ij.snd
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Express `dist` in terms of `nndist`  -/
dist_nndist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), dist x y = ↑(nndist x y)
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- The motive, with the pi type version delaborated and the original expression version.
Once `AppMatchState` is complete, this is not `none`.  -/
Lean.PrettyPrinter.Delaborator.AppMatchState.motive : Lean.PrettyPrinter.Delaborator.AppMatchState → Option (Lean.Term × Lean.Expr)
-- Std.Time.DateTime
_private.Std.Time.DateTime.0.Std.Time.DateTime.mk.sizeOf_spec : ∀ (date : Thunk Std.Time.PlainDateTime) (timestamp : Std.Time.Timestamp) (rules : Std.Time.TimeZone.ZoneRules)
  (timezone : Std.Time.TimeZone),
  sizeOf { date := date, timestamp := timestamp, rules := rules, timezone := timezone } =
    1 + sizeOf date + sizeOf timestamp + sizeOf rules + sizeOf timezone
-- Mathlib.RingTheory.Congruence.Hom
/-- Homomorphisms on the quotient of a ring by a ring congruence relation are
equal if they are equal on elements that are coercions from the ring.  -/
RingCon.Quotient.hom_ext : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] {c : RingCon M}
  {f g : c.Quotient →+* P}, f.comp c.mk' = g.comp c.mk' → f = g
-- Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Subalgebra.coe_pointwise_smul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {R' : Type u_3}
  [inst_3 : Semiring R'] [inst_4 : MulSemiringAction R' A] [inst_5 : SMulCommClass R' R A] (m : R')
  (S : Subalgebra R A), ↑(m • S) = m • ↑S
-- Mathlib.Analysis.Convex.Body
ConvexBody.instSetLike : {V : Type u_1} →
  [inst : TopologicalSpace V] → [inst_1 : AddCommGroup V] → [inst_2 : Module ℝ V] → SetLike (ConvexBody V) V