mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Slice.List.Lemmas
List.size_mkSlice_rii : ∀ {α : Type u_1} {xs : List α}, Std.Slice.size (Std.Rii.Sliceable.mkSlice xs *...*) = xs.length
-- Init.Data.UInt.Lemmas
USize.neg_mul_not_eq_add_mul : ∀ {a b : USize}, -(a * ~~~b) = a + a * b
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_powC_nc : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.Ring α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (p : Lean.Grind.CommRing.Poly) (k : ℕ),
  Lean.Grind.CommRing.Poly.denote ctx (p.powC_nc k c) = Lean.Grind.CommRing.Poly.denote ctx p ^ k
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
cfc_real_eq_nnreal : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : PartialOrder A] [inst_3 : StarRing A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [IsSemitopologicalRing A] [T2Space A]
  [inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] {f : ℝ → ℝ} (a : A),
  (∀ x ∈ spectrum ℝ a, 0 ≤ f x) →
    autoParam (0 ≤ a) cfc_real_eq_nnreal._auto_1 → cfc f a = cfc (fun x => (f ↑x).toNNReal) a
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.top : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator → ℕ
-- Mathlib.RingTheory.Valuation.Quotient
AddValuation.supp_quot_supp : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : CommRing R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀]
  (v : AddValuation R Γ₀), AddValuation.supp (Valuation.onQuot v ⋯) = 0
-- Mathlib.Topology.Algebra.Order.UpperLower
IsOpen.upperClosure : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] [HasUpperLowerClosure α] {s : Set α},
  IsOpen s → IsOpen ↑(upperClosure s)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k a : α} {fallback : β a} {v : β k},
      (t.insertIfNew k v).getD a fallback = if h : cmp k a = Ordering.eq ∧ k ∉ t then cast ⋯ v else t.getD a fallback
-- Mathlib.Algebra.Order.Floor.Div
Nat.floorDiv_eq_div : ∀ (a b : ℕ), a ⌊/⌋ b = a / b
-- Mathlib.Analysis.Matrix.Normed
/-- Note this is safe as an instance as it carries no data.  -/
Matrix.instNormOneClassOfNonempty : ∀ {n : Type u_4} {α : Type u_5} [inst : Fintype n] [inst_1 : SeminormedAddCommGroup α] [Nonempty n]
  [inst_3 : DecidableEq n] [inst_4 : One α] [NormOneClass α], NormOneClass (Matrix n n α)
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Computation.BisimO.match_1.eq_2 : ∀ {α : Type u_1} (motive : α ⊕ Computation α → α ⊕ Computation α → Sort u_2) (s s' : Computation α)
  (h_1 : (a a' : α) → motive (Sum.inl a) (Sum.inl a')) (h_2 : (s s' : Computation α) → motive (Sum.inr s) (Sum.inr s'))
  (h_3 : (x x_1 : α ⊕ Computation α) → motive x x_1),
  (match Sum.inr s, Sum.inr s' with
    | Sum.inl a, Sum.inl a' => h_1 a a'
    | Sum.inr s, Sum.inr s' => h_2 s s'
    | x, x_1 => h_3 x x_1) =
    h_2 s s'
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.attachCodeDecls.go.match_1.splitter : {pu : Lean.Compiler.LCNF.Purity} →
  (motive : Lean.Compiler.LCNF.CodeDecl pu → Sort u_1) →
    (x : Lean.Compiler.LCNF.CodeDecl pu) →
      ((decl : Lean.Compiler.LCNF.LetDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.let decl)) →
        ((decl : Lean.Compiler.LCNF.FunDecl pu) →
            (h : pu = Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.CodeDecl.fun decl h)) →
          ((decl : Lean.Compiler.LCNF.FunDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.jp decl)) →
            ((fvarId : Lean.FVarId) →
                (idx : ℕ) →
                  (y : Lean.Compiler.LCNF.Arg pu) →
                    (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                      motive (Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h)) →
              ((fvarId : Lean.FVarId) →
                  (idx : ℕ) →
                    (y : Lean.FVarId) →
                      (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                        motive (Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h)) →
                ((fvarId : Lean.FVarId) →
                    (idx offset : ℕ) →
                      (y : Lean.FVarId) →
                        (ty : Lean.Expr) →
                          (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                            motive (Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h)) →
                  ((fvarId : Lean.FVarId) →
                      (cidx : ℕ) →
                        (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                          motive (Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h)) →
                    ((fvarId : Lean.FVarId) →
                        (n : ℕ) →
                          (check persistent : Bool) →
                            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                              motive (Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h)) →
                      ((fvarId : Lean.FVarId) →
                          (n : ℕ) →
                            (check persistent : Bool) →
                              (objs? : Option ℕ) →
                                (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                  motive (Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h)) →
                        ((fvarId : Lean.FVarId) →
                            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                              motive (Lean.Compiler.LCNF.CodeDecl.del fvarId h)) →
                          motive x
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrixIn.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (S : Type u_5) [inst_5 : CommRing S]
  [inst_6 : Algebra S R] {P : RootPairing ι R M N} [inst_7 : P.IsValuedIn S] (b : P.Base) (a a_1 : ↥b.support),
  a = a_1 →
    ∀ (a_2 a_3 : ↥b.support),
      a_2 = a_3 → RootPairing.Base.cartanMatrixIn S b a a_2 = RootPairing.Base.cartanMatrixIn S b a_1 a_3
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.filter_equiv_self_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.Equiv t ↔
    ∀ (a : α) (h : Std.DTreeMap.Internal.Impl.contains a t = true), f a (t.get a h) = true
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.uliftFunctorInclusion_top_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C}, CategoryTheory.IsIso ⊤.uliftFunctorInclusion
-- Lean.Meta.WHNF
/-- Auxiliary function for reducing recursor applications.  -/
_private.Lean.Meta.WHNF.0.Lean.Meta.reduceRec : {α : Type} →
  Lean.RecursorVal →
    List Lean.Level → Array Lean.Expr → (Unit → Lean.MetaM α) → (Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_def : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (p : MvPolynomial σ R),
  p.vars = p.degrees.toFinset
-- Init.Control.Basic
/-- Overloaded monadic iteration over some container type.

An instance of `ForM m γ α` describes how to iterate a monadic operator over a container of type `γ`
with elements of type `α` in the monad `m`. The element type should be uniquely determined by the
monad and the container.

Use `ForM.forIn` to construct a `ForIn` instance from a `ForM` instance, thus enabling the use of
the `for` operator in `do`-notation.
 -/
ForM : (Type u → Type v) → Type w₁ → outParam (Type w₂) → Type (max (max v w₁) w₂)
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.mapBifunctorMap_obj_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : 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} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6}
  (p : I × J → K)
  [inst_3 :
    ∀ (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂),
      (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p]
  (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂),
  ((CategoryTheory.GradedObject.mapBifunctorMap F p).obj X).obj Y =
    CategoryTheory.GradedObject.mapBifunctorMapObj F p X Y
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.equivQuotientZSMulOfEquiv_trans : ∀ {A B C : Type u} [inst : AddCommGroup A] [inst_1 : AddCommGroup B] [inst_2 : AddCommGroup C] (e : A ≃+ B) (d : B ≃+ C)
  (n : ℤ),
  (QuotientAddGroup.equivQuotientZSMulOfEquiv e n).trans (QuotientAddGroup.equivQuotientZSMulOfEquiv d n) =
    QuotientAddGroup.equivQuotientZSMulOfEquiv (e.trans d) n
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
DifferentiableAt.continuousAlternatingMapCompContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H] {f : E → G [⋀^ι]→L[𝕜] H} {g : E → F →L[𝕜] G} {x : E}
  [Finite ι],
  DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 g x → DifferentiableAt 𝕜 (fun x => (f x).compContinuousLinearMap (g x)) x
-- Mathlib.Analysis.Convex.Function
/-- Right translation preserves convexity.  -/
ConvexOn.translate_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E] [inst_6 : SMul 𝕜 β] {s : Set E}
  {f : E → β}, ConvexOn 𝕜 s f → ∀ (c : E), ConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z)
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.IsClosedUnderCokernels.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P : CategoryTheory.ObjectProperty C},
  (CategoryTheory.MorphismProperty.ofObjectProperty P P).cokernels ≤ P → P.IsClosedUnderCokernels
-- Mathlib.ModelTheory.Substructures
/-- Copy a substructure replacing `carrier` with a set that is equal to it.  -/
FirstOrder.Language.Substructure.copy : {L : FirstOrder.Language} →
  {M : Type w} → [inst : L.Structure M] → (S : L.Substructure M) → (s : Set M) → s = ↑S → L.Substructure M
-- Init.Data.UInt.Bitwise
UInt16.ofBitVec_xor : ∀ (a b : BitVec 16), { toBitVec := a ^^^ b } = { toBitVec := a } ^^^ { toBitVec := b }
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetAux'_nil : ∀ {α : Type u_1}, Multiset.powersetAux' [] = [0]
-- Lean.Elab.App
Lean.Elab.Term.LValResolution.const.injEq : ∀ (baseStructName structName constName : Lean.Name) (levels : List Lean.Level)
  (baseStructName_1 structName_1 constName_1 : Lean.Name) (levels_1 : List Lean.Level),
  (Lean.Elab.Term.LValResolution.const baseStructName structName constName levels =
      Lean.Elab.Term.LValResolution.const baseStructName_1 structName_1 constName_1 levels_1) =
    (baseStructName = baseStructName_1 ∧ structName = structName_1 ∧ constName = constName_1 ∧ levels = levels_1)
-- Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
/-- Preliminary lemma for compactness of the orbit map.  -/
_private.Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction.0.UpperHalfPlane.absq_le : ∀ {K : Set UpperHalfPlane},
  IsCompact K → ∃ A, ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℝ), g • UpperHalfPlane.I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
-- Mathlib.CategoryTheory.EffectiveEpi.Comp
/-- An effective epi family precomposed with a family of split epis is effective epimorphic.
 -/
CategoryTheory.effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {α : Type u_2} →
      {B : C} →
        {X Y : α → C} →
          (f : (a : α) → X a ⟶ B) →
            (g : (a : α) → Y a ⟶ X a) →
              [∀ (a : α), CategoryTheory.IsSplitEpi (g a)] →
                [CategoryTheory.EffectiveEpiFamily X f] →
                  CategoryTheory.EffectiveEpiFamilyStruct Y fun a => CategoryTheory.CategoryStruct.comp (g a) (f a)
-- Mathlib.Topology.Homotopy.Contractible
contractible_iff_id_nullhomotopic : ∀ (Y : Type u_1) [inst : TopologicalSpace Y], ContractibleSpace Y ↔ (ContinuousMap.id Y).Nullhomotopic
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_mul_leadingTerm : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
  (p q : MvPolynomial σ R), m.degree (p * m.leadingTerm q) = m.degree (p * q)
-- Mathlib.Analysis.Convex.EGauge
egauge_add_add_le : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {U V : Set E}, Balanced 𝕜 U → Balanced 𝕜 V → ∀ (a b : E), egauge 𝕜 (U + V) (a + b) ≤ max (egauge 𝕜 U a) (egauge 𝕜 V b)
-- Init.Data.Array.Lemmas
Array.instDecidableForallForallMemOfDecidablePred : {α : Type u_1} → {xs : Array α} → {p : α → Prop} → [DecidablePred p] → Decidable (∀ x ∈ xs, p x)
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.mul_assoc : ∀ {n : ℕ} (a b c : Fin n), a * b * c = a * (b * c)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.pruneLE.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_2 ()
-- Mathlib.Order.WellFounded
exists_not_acc_lt_of_not_acc : ∀ {α : Sort u_1} {a : α} {r : α → α → Prop}, ¬Acc r a → ∃ b, ¬Acc r b ∧ r b a
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.Limits.cocone_pt_coe : ∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  {F : CategoryTheory.Functor J PartOrdEmb}
  {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))}
  (hc : CategoryTheory.Limits.IsColimit c), ↑(PartOrdEmb.Limits.cocone hc).pt = PartOrdEmb.Limits.CoconePt hc
-- Lean.Environment
Lean.Kernel.Exception.typeExpected.inj : ∀ {env : Lean.Kernel.Environment} {lctx : Lean.LocalContext} {expr : Lean.Expr} {env_1 : Lean.Kernel.Environment}
  {lctx_1 : Lean.LocalContext} {expr_1 : Lean.Expr},
  Lean.Kernel.Exception.typeExpected env lctx expr = Lean.Kernel.Exception.typeExpected env_1 lctx_1 expr_1 →
    env = env_1 ∧ lctx = lctx_1 ∧ expr = expr_1
-- Init.MetaTypes
/-- When `true` (default: `true`), performs beta reduction of applications of `fun` expressions.
That is, `(fun x => e[x]) v` reduces to `e[v]`.
 -/
Lean.Meta.Simp.Config.beta : Lean.Meta.Simp.Config → Bool
-- Mathlib.Algebra.Lie.Prod
LieHom.range_inl : ∀ (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂],
  (LieHom.inl R L₁ L₂).range = LieIdeal.toLieSubalgebra R (L₁ × L₂) (LieHom.snd R L₁ L₂).ker
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.proj.inj : ∀ {i : ℕ} {x : Lean.IR.VarId} {i_1 : ℕ} {x_1 : Lean.IR.VarId},
  Lean.IR.Expr.proj i x = Lean.IR.Expr.proj i_1 x_1 → i = i_1 ∧ x = x_1
-- Init.Data.UInt.Bitwise
UInt32.neg_eq_not_add : ∀ (a : UInt32), -a = ~~~a + 1
-- Mathlib.Combinatorics.SimpleGraph.Hasse
SimpleGraph.pathGraph_connected : ∀ (n : ℕ), (SimpleGraph.pathGraph (n + 1)).Connected
-- Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
Std.Tactic.BVDecide.LRAT.Internal.Result.success : Std.Tactic.BVDecide.LRAT.Internal.Result
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.touchpointWeights_empty_pos : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) {i j : Fin (n + 1)},
  i ≠ j → 0 < s.touchpointWeights ∅ i j
-- Mathlib.Data.Matrix.DMatrix
DMatrix.ext_iff : ∀ {m : Type u_1} {n : Type u_2} {α : m → n → Type v} {M N : DMatrix m n α}, (∀ (i : m) (j : n), M i j = N i j) ↔ M = N
-- Mathlib.Topology.Order.Monotone
/-- An antitone function continuous at the infimum of a nonempty set sends this infimum to
the supremum of the image of this set.  -/
Antitone.map_csInf_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β]
  {f : α → β} {A : Set α},
  ContinuousAt f (sInf A) →
    Antitone f →
      A.Nonempty → autoParam (BddBelow A) Antitone.map_csInf_of_continuousAt._auto_1 → f (sInf A) = sSup (f '' A)
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The (exact) sequence `H^{n-1}(f₃) ⟶ Z^n(f₁, f₂) ⟶ E^n(f₁, f₂, f₃) ⟶ 0`.  -/
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i j k l : ι} →
              (i ⟶ j) →
                (j ⟶ k) →
                  (k ⟶ l) →
                    (n₀ n₁ n₂ : ℤ) →
                      autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE._auto_1 →
                        autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE._auto_3 →
                          CategoryTheory.ShortComplex C
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
/-- The Radon-Nikodym derivative `∂(μ.trim hm)/∂(ν.trim hm)` of the trimmed measures
(for `hm : m ≤ m0` stating that `m` is a sub-sigma-algebra of `m0`) is a.e.-equal to the
conditional expectation of `∂μ/∂ν` with respect to the sigma-algebra `m`.  -/
MeasureTheory.toReal_rnDeriv_trim : ∀ {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} (hm : m ≤ m𝓧)
  [MeasureTheory.IsFiniteMeasure μ] [hsf : MeasureTheory.SigmaFinite (ν.trim hm)],
  μ.AbsolutelyContinuous ν →
    (fun x => ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal) =ᵐ[ν.trim hm] ν[fun x => (μ.rnDeriv ν x).toReal | m]
-- Mathlib.Algebra.DualNumber
DualNumber.ringHom_ext_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {R' : Type u_5} [inst_1 : CommSemiring R'] {f g : DualNumber R →+* R'},
  f = g ↔
    f.comp (algebraMap R (DualNumber R)) = g.comp (algebraMap R (DualNumber R)) ∧ f DualNumber.eps = g DualNumber.eps
-- Mathlib.Algebra.Group.AddChar
/-- The natural equivalence to `(Multiplicative A →* M)` is a monoid isomorphism.  -/
AddChar.toMonoidHomMulEquiv : {A : Type u_2} →
  {M : Type u_3} → [inst : AddMonoid A] → [inst_1 : CommMonoid M] → AddChar A M ≃* (Multiplicative A →* M)
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.factor_dvd_of_degree_ne_zero : ∀ {K : Type v} [inst : Field K] {f : Polynomial K}, f.degree ≠ 0 → f.factor ∣ f
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- Two group isomorphisms `G ≃* G'` are equal if and only if they agree on a generator of `G`.  -/
MulEquiv.eq_iff_eq_on_generator : ∀ {G : Type u_2} {G' : Type u_3} [inst : Group G] [inst_1 : Group G'] {g : G},
  (∀ (x : G), x ∈ Subgroup.zpowers g) → ∀ (f₁ f₂ : G ≃* G'), f₁ = f₂ ↔ f₁ g = f₂ g
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instMax : {R : Type u_2} →
  {N : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid N] →
        [inst_2 : TopologicalSpace N] →
          [inst_3 : Module R N] → [ContinuousAdd N] → [ContinuousConstSMul R N] → Max (ClosedSubmodule R N)
-- Mathlib.CategoryTheory.Adjunction.Opposites
CategoryTheory.Functor.IsRightAdjoint.op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [F.IsRightAdjoint], F.op.IsLeftAdjoint
-- Mathlib.Algebra.Lie.Subalgebra
/-- A Lie subalgebra forms a new Lie algebra.  -/
LieSubalgebra.lieAlgebra : (R : Type u) →
  (L : Type v) →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (L' : LieSubalgebra R L) → LieAlgebra R ↥L'
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialRightAdjointHomEquiv_symm_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} {Y Y' : F.PartialRightAdjointSource} (f : F.obj X ⟶ Y.obj) (g : Y ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (F.partialRightAdjointHomEquiv.symm f) (F.partialRightAdjointMap g) =
    F.partialRightAdjointHomEquiv.symm (CategoryTheory.CategoryStruct.comp f g.hom)
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_le_ord : ∀ {c₁ c₂ : Cardinal.{u_1}}, c₁.ord ≤ c₂.ord ↔ c₁ ≤ c₂
-- Mathlib.Probability.Process.HittingTime
/-- `hittingBtwn` is monotone with respect to the minimal time.  -/
MeasureTheory.hittingBtwn_mono_left : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] (u : ι → Ω → β) (s : Set β)
  (m : ι), Monotone fun x => MeasureTheory.hittingBtwn u s x m
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars.eq_1 : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c : ℕ → 𝕜) (n : ℕ),
  FormalMultilinearSeries.ofScalars E c n = c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E
-- Mathlib.Data.Finset.Insert
Finset.eq_of_mem_singleton : ∀ {α : Type u_1} {x y : α}, x ∈ {y} → x = y
-- Mathlib.Algebra.Group.Invertible.Defs
mul_invOf_cancel_right' : ∀ {α : Type u} [inst : Monoid α] (a b : α) {x : Invertible b}, a * b * ⅟b = a
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β}, k ∉ t₂ → (t₁ ∩ t₂).getD k fallback = fallback
-- Mathlib.Data.Erased
Erased.out_inj_iff : ∀ {α : Sort u_1} {a b : Erased α}, a = b ↔ a.out = b.out
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.filter_equiv_self_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {f : α → Bool},
  (Std.TreeSet.filter f t).Equiv t ↔ ∀ (k : α) (h : k ∈ t), f (t.get k h) = true
-- Mathlib.Data.Complex.Basic
Complex.div_ofNat_im : ∀ (z : ℂ) (n : ℕ) [inst : n.AtLeastTwo], (z / OfNat.ofNat n).im = z.im / OfNat.ofNat n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.integralModel_Δ_eq : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] (W : WeierstrassCurve K)
  [hW : WeierstrassCurve.IsIntegral R W], (algebraMap R K) (WeierstrassCurve.integralModel R W).Δ = W.Δ
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.hasSum_derivWeierstrassPExcept : ∀ (L : PeriodPair) (l₀ z : ℂ),
  HasSum (fun l => if ↑l = l₀ then 0 else -2 / (z - ↑l) ^ 3) (L.derivWeierstrassPExcept l₀ z)
-- Mathlib.Algebra.Group.Hom.Defs
/-- `M →* N` denotes the type of monoid homomorphisms from `M` to `N`.  -/
«term_→*_» : Lean.TrailingParserDescr
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.ringHomCompHom_apply : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {R'' : Type u_3} [inst_2 : CommRing R'']
  (f : R' →+* R'') (χ : MulChar R R'), (MulChar.ringHomCompHom f) χ = χ.ringHomComp f
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.commute_of_mul_eq_isSelfAdjoint : ∀ {R : Type u_3} [inst : Mul R] [inst_1 : StarMul R] (x y z : R),
  IsSelfAdjoint x → IsSelfAdjoint y → IsSelfAdjoint z → x * y = z → Commute x y