mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.sc₃_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.sc₃._auto_1),
  (X.sc₃ f g fg h n₀ n₁ hn₁).X₁ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ fg)
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.lt_irrefl : ∀ {α : Type u} [inst : Preorder α] {a : α}, ¬a < a
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.numLitNoAntiquot.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.w_mk_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f : CategoryTheory.Arrow T} {X Y : T} {g : X ⟶ Y}
  (sq : f ⟶ CategoryTheory.Arrow.mk g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) g =
    CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.Arrow.Hom.right sq)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_inv_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ),
  X.leftOpRightOpIso.inv.left = CategoryTheory.CategoryStruct.id X.left
-- Init.Data.UInt.Bitwise
UInt64.right_le_or : ∀ {a b : UInt64}, b ≤ a ||| b
-- Init.Data.Vector.Lemmas
Vector.getElem?_flatMap : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {m : ℕ} {xs : Vector α n} {f : α → Vector β m} {i : ℕ},
  (xs.flatMap f)[i]? = if hi : i < n * m then some (f xs[i / m])[i % m] else none
-- Mathlib.Analysis.MeanInequalitiesPow
Real.arith_mean_le_rpow_mean : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
  (∀ i ∈ s, 0 ≤ w i) →
    ∑ i ∈ s, w i = 1 → (∀ i ∈ s, 0 ≤ z i) → ∀ {p : ℝ}, 1 ≤ p → ∑ i ∈ s, w i * z i ≤ (∑ i ∈ s, w i * z i ^ p) ^ (1 / p)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.commandExpandersFor : Lean.Ident →
  Lean.Elab.TermElabM
    (Array
      (Lean.Name ×
        StateT (Array (Lean.TSyntax `doc_arg)) Lean.Doc.DocM (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)))
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
SSet.stdSimplex.δ_zero_toSSetObjI : CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) SSet.stdSimplex.toSSetObjI =
  SSet.const (TopCat.toSSetObj₀Equiv.symm 1)
-- Init.Data.Int.Order
Int.mul_le_mul_of_nonneg_left : ∀ {a b c : ℤ}, a ≤ b → 0 ≤ c → c * a ≤ c * b
-- Mathlib.LinearAlgebra.TensorProduct.Pi
TensorProduct.piRight.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module S N] [inst_6 : IsScalarTower R S N] {ι : Type u_4}
  (M : ι → Type u_5) [inst_7 : (i : ι) → AddCommMonoid (M i)] [inst_8 : (i : ι) → Module R (M i)] [inst_9 : Fintype ι]
  [inst_10 : DecidableEq ι],
  TensorProduct.piRight R S N M =
    LinearEquiv.ofLinearMap (TensorProduct.piRightHom R S N M) (TensorProduct.piRightInv R S N M) ⋯ ⋯
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Γ_obj_op : ∀ (X : AlgebraicGeometry.Scheme), AlgebraicGeometry.Scheme.Γ.obj (Opposite.op X) = X.presheaf.obj (Opposite.op ⊤)
-- Lean.Meta.Tactic.Grind.EqResolution
/-- Similar to `forallMetaTelescopeReducing`, but if `prop` resulting type is of the form `¬ p`, it will "convert" it so `p → False`, and
will return a hypothesis for it and return `False` as the resulting type.
 -/
_private.Lean.Meta.Tactic.Grind.EqResolution.0.Lean.Meta.Grind.forallMetaTelescopeReducingAndUnfoldingNot : Lean.Expr → Lean.MetaM (Array Lean.Expr × Lean.Expr)
-- Mathlib.Topology.ClusterPt
clusterPt_iff_forall_mem_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F : Filter X}, ClusterPt x F ↔ ∀ s ∈ F, x ∈ closure s
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval_sum : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {ι : Type u_2} (s : Finset ι) (f : ι → MvPolynomial σ R)
  (g : σ → R), (MvPolynomial.eval g) (∑ i ∈ s, f i) = ∑ i ∈ s, (MvPolynomial.eval g) (f i)
-- Mathlib.Data.Num.Basic
/-- The successor of a `ZNum`.  -/
ZNum.succ : ZNum → ZNum
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.insert_Ioc_right_eq_Ioc_succ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] {a b : α} [NoMaxOrder α],
  a ≤ b → insert (Order.succ b) (Finset.Ioc a b) = Finset.Ioc a (Order.succ b)
-- Mathlib.Topology.UniformSpace.UniformConvergence
UniformContinuousOn.tendstoUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {x : α} [inst_1 : UniformSpace α]
  [inst_2 : UniformSpace γ] {U : Set α} {V : Set β} {F : α → β → γ},
  UniformContinuousOn (↿F) (U ×ˢ V) → x ∈ U → TendstoUniformlyOn F (F x) (nhdsWithin x U) V
-- Mathlib.Data.EReal.Inv
SignType.sign.eq_1 : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : DecidableLT α],
  SignType.sign = { toFun := fun a => if 0 < a then 1 else if a < 0 then -1 else 0, monotone' := ⋯ }
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.insert_Icc_pred_right_eq_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : PredOrder α] {a b : α},
  a ≤ b → insert b (Finset.Icc a (Order.pred b)) = Finset.Icc a b
-- Mathlib.CategoryTheory.Enriched.HomCongr
CategoryTheory.Iso.eHomCongr_symm : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X Y X₁ Y₁ : C}
  (α : X ≅ X₁) (β : Y ≅ Y₁), (CategoryTheory.Iso.eHomCongr V α β).symm = CategoryTheory.Iso.eHomCongr V α.symm β.symm
-- Mathlib.Topology.Semicontinuity.Defs
HasOpenLowerSections.comp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {γ : Type u_4} [inst_1 : TopologicalSpace γ]
  {g : γ → α}, HasOpenLowerSections f → Continuous g → HasOpenLowerSections (f ∘ g)
-- Lean.Structure
_private.Lean.Structure.0.Lean.structureExt : Lean.PersistentEnvExtension Lean.StructureInfo Lean.StructureInfo (Unit × Lean.StructureState✝)
-- Mathlib.Computability.RegularExpressions
RegularExpression.matches'.eq_1 : ∀ {α : Type u_1}, RegularExpression.zero.matches' = 0
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.BalancedTree.mk.congr_simp : ∀ {α : Type u} {β : α → Type v} (impl impl_1 : Std.DTreeMap.Internal.Impl α β) (e_impl : impl = impl_1)
  (balanced_impl : impl.Balanced),
  { impl := impl, balanced_impl := balanced_impl } = { impl := impl_1, balanced_impl := ⋯ }
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.sup_lie : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  (I J : LieIdeal R L), ⁅I ⊔ J, N⁆ = ⁅I, N⁆ ⊔ ⁅J, N⁆
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.conj : ∀ {α : Type u_2} {f g : Equiv.Perm α}, f.IsCycle → (g * f * g⁻¹).IsCycle
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.map_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' X'' Y'' Z'' : C} {f : X ⟶ Y} {g : X ⟶ Z}
  {f' : X' ⟶ Y'} {g' : X' ⟶ Z'} {f'' : X'' ⟶ Y''} {g'' : X'' ⟶ Z''} (i₁ : X ⟶ X') (j₁ : X' ⟶ X'') (i₂ : Y ⟶ Y')
  (j₂ : Y' ⟶ Y'') (i₃ : Z ⟶ Z') (j₃ : Z' ⟶ Z'') [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout f' g'] [inst_3 : CategoryTheory.Limits.HasPushout f'' g'']
  (e₁ : CategoryTheory.CategoryStruct.comp f i₂ = CategoryTheory.CategoryStruct.comp i₁ f')
  (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₁ g')
  (e₃ : CategoryTheory.CategoryStruct.comp f' j₂ = CategoryTheory.CategoryStruct.comp j₁ f'')
  (e₄ : CategoryTheory.CategoryStruct.comp g' j₃ = CategoryTheory.CategoryStruct.comp j₁ g''),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.map f g f' g' i₂ i₃ i₁ e₁ e₂)
      (CategoryTheory.Limits.pushout.map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄) =
    CategoryTheory.Limits.pushout.map f g f'' g'' (CategoryTheory.CategoryStruct.comp i₂ j₂)
      (CategoryTheory.CategoryStruct.comp i₃ j₃) (CategoryTheory.CategoryStruct.comp i₁ j₁) ⋯ ⋯
-- Mathlib.Tactic.Translate.Reorder
/-- Elaborate the argument of a `(reorder := ...)` option.  -/
Mathlib.Tactic.Translate.elabReorder : Lean.TSyntax `translateReorder →
  Array Lean.Name → Array Lean.Expr → Lean.MessageData → Lean.MetaM Mathlib.Tactic.Translate.ArgReorder
-- Mathlib.FieldTheory.SeparableClosure
Field.finInsepDegree_def' : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  Field.finInsepDegree F E = Cardinal.toNat (Field.insepDegree F E)
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- If `M` is boundaryless, `∂(M×N) = M × ∂N`.  -/
ModelWithCorners.boundary_of_boundaryless_left : ∀ {𝕜 : 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'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {N : Type u_7}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {J : ModelWithCorners 𝕜 E' H'} [BoundarylessManifold I M],
  ModelWithCorners.boundary (M × N) = Set.univ.prod (ModelWithCorners.boundary N)
-- Mathlib.LinearAlgebra.AnnihilatingPolynomial
/-- The generator of the annihilating ideal is the minimal polynomial.  -/
Polynomial.annIdealGenerator_eq_minpoly : ∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A),
  Polynomial.annIdealGenerator 𝕜 a = minpoly 𝕜 a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.function : Lean.Lsp.SemanticTokenType
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonWaitForILeans.fromJson : Lean.Json → Except String Lean.Lsp.WaitForILeans
-- Mathlib.Algebra.Group.Prod
Prod.instAddRightCancelMonoid.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddRightCancelMonoid M] [inst_1 : AddRightCancelMonoid N],
  Prod.instAddRightCancelMonoid = { toAddMonoid := Prod.instAddMonoid, toIsRightCancelAdd := ⋯ }
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
_private.Init.Data.String.Lemmas.Pattern.TakeDrop.Basic.0.String.Slice.Pos.skipWhile.match_1.eq_1 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (nextCurr : s.Pos)
  (h_1 : (nextCurr : s.Pos) → motive (some nextCurr)) (h_2 : Unit → motive none),
  (match some nextCurr with
    | some nextCurr => h_1 nextCurr
    | none => h_2 ()) =
    h_1 nextCurr
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The underlying object in the ambient monoidal category  -/
CategoryTheory.AddMon.X : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.AddMon C → C
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.multiplicity_lt_iff_not_dvd : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {k : ℕ}, FiniteMultiplicity a b → (multiplicity a b < k ↔ ¬a ^ k ∣ b)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] {f : α → β → Bool} {k : α} {h' : k ∈ Std.HashMap.Raw.filter f m} (h : m.WF),
  (Std.HashMap.Raw.filter f m)[k] = m[k]
-- Mathlib.Order.Category.NonemptyFinLinOrd
/-- Constructs an equivalence between nonempty finite linear orders from an order isomorphism
between them.  -/
NonemptyFinLinOrd.Iso.mk : {α β : NonemptyFinLinOrd} → ↑α.toLinOrd ≃o ↑β.toLinOrd → (α ≅ β)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.ShiftMkCore.shiftFunctorZero_eq : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  (h : CategoryTheory.ShiftMkCore C A), CategoryTheory.shiftFunctorZero C A = h.zero
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_self_sub_emod : ∀ {x m : ℤ}, m ∣ x - x % m
-- Lean.Environment
/-- Direct and transitive imports. Modules are given with their effective import modifiers, not their
original ones. Each module is listed at most once. The index of a module in the array equals the
`ModuleIdx` for the same module.
 -/
Lean.EnvironmentHeader.modules : Lean.EnvironmentHeader → Array Lean.EffectiveImport
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanILeanHeaderSetupInfoParams.toJson : Lean.Lsp.LeanILeanHeaderSetupInfoParams → Lean.Json
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile.mk.injEq : ∀ (uri : Lean.Lsp.DocumentUri) (options? : Option Lean.Lsp.DeleteFile.Options) (annotationId? : Option String)
  (uri_1 : Lean.Lsp.DocumentUri) (options?_1 : Option Lean.Lsp.DeleteFile.Options) (annotationId?_1 : Option String),
  ({ uri := uri, options? := options?, annotationId? := annotationId? } =
      { uri := uri_1, options? := options?_1, annotationId? := annotationId?_1 }) =
    (uri = uri_1 ∧ options? = options?_1 ∧ annotationId? = annotationId?_1)
-- Mathlib.Data.Nat.Prime.Nth
Nat.nth_prime_four_eq_eleven : Nat.nth Nat.Prime 4 = 11
-- Mathlib.Data.Set.Lattice
Set.sUnion_sdiff_singleton_empty : ∀ {α : Type u_1} (s : Set (Set α)), ⋃₀ (s \ {∅}) = ⋃₀ s
-- Mathlib.Computability.DFA
DFA.acceptsFrom_inter : ∀ {α : Type u} {σ1 σ2 : Type v} (M1 : DFA α σ1) (M2 : DFA α σ2) (s1 : σ1) (s2 : σ2),
  (M1.inter M2).acceptsFrom (s1, s2) = M1.acceptsFrom s1 ⊓ M2.acceptsFrom s2
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_subsingleton : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] [Subsingleton n]
  (A : Matrix n n α), A.adjugate = 1
-- Batteries.Recycling.MonadSatisfying.Basic
/-- `SatisfiesM p (x : m α)` lifts propositions over a monad. It asserts that `x` may as well
have the type `x : m {a // p a}`, because there exists some `m {a // p a}` whose image is `x`.
So `p` is the postcondition of the monadic value.
 -/
SatisfiesM : {α : Type u} → {m : Type u → Type v} → [Functor m] → (α → Prop) → m α → Prop
-- Mathlib.Analysis.Distribution.FourierMultiplier
SchwartzMap.fourierMultiplierCLM_apply : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace ℝ E] [inst_4 : NormedSpace ℂ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℂ 𝕜 F] [inst_7 : FiniteDimensional ℝ E] [inst_8 : MeasurableSpace E] [inst_9 : BorelSpace E]
  (g : E → 𝕜) (f : SchwartzMap E F),
  (SchwartzMap.fourierMultiplierCLM F g) f =
    FourierTransformInv.fourierInv ((SchwartzMap.smulLeftCLM F g) (FourierTransform.fourier f))
-- ProofWidgets.Component.MakeEditLink
ProofWidgets.instFromJsonMakeEditLinkProps : Lean.FromJson ProofWidgets.MakeEditLinkProps
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.mk.injEq : ∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePair R) (x : S) (hasMap : P.HasMap x) (lift_bijective : Function.Bijective ⇑(P.lift x hasMap))
  (P_1 : StandardEtalePair R) (x_1 : S) (hasMap_1 : P_1.HasMap x_1)
  (lift_bijective_1 : Function.Bijective ⇑(P_1.lift x_1 hasMap_1)),
  ({ P := P, x := x, hasMap := hasMap, lift_bijective := lift_bijective } =
      { P := P_1, x := x_1, hasMap := hasMap_1, lift_bijective := lift_bijective_1 }) =
    (P = P_1 ∧ x = x_1)
-- Mathlib.Data.ENNReal.Inv
ENNReal.coe_div_le : ∀ {r p : NNReal}, ↑(p / r) ≤ ↑p / ↑r
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α], (↑m₁).WF → (↑m₂).WF → (↑(m₁.diff m₂)).size + (↑(m₁.inter m₂)).size = (↑m₁).size
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.refl_apply : ∀ (M : Type u_1) [inst : TopologicalSpace M] [inst_1 : Add M] (m : M), (ContinuousAddEquiv.refl M) m = m
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Adjunction.toComonad_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R), h.toComonad.ε = h.counit
-- Mathlib.Topology.Order.LeftRightLim
/-- Let `f : α → β` be a function from a linear order `α` to a topological space `β`, and
let `a : α`. The limit strictly to the left of `f` at `a`, denoted with `leftLim f a`, is defined
by using the order topology on `α`. If `a` is isolated to its left or the function has no left
limit, we use `f a` instead to guarantee a good behavior in most cases.  -/
Function.leftLim : {α : Type u_1} → {β : Type u_2} → [LinearOrder α] → [TopologicalSpace β] → (α → β) → α → β
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientInfEquivQuotientProd_fst : ∀ {R : Type u_2} [inst : CommRing R] (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I ⊓ J),
  ((I.quotientInfEquivQuotientProd J coprime) x).1 = (Ideal.Quotient.factor ⋯) x
-- Init.Data.Vector.Attach
Vector.pmap_eq_attachWith : ∀ {α : Type u_1} {n : ℕ} {p q : α → Prop} {f : ∀ (a : α), p a → q a} {xs : Vector α n} (H : ∀ a ∈ xs, p a),
  Vector.pmap (fun a h => ⟨a, ⋯⟩) xs H = xs.attachWith q ⋯
-- Init.Data.UInt.Lemmas
USize.le_zero_iff : ∀ {a : USize}, a ≤ 0 ↔ a = 0
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.instDecidableEq : DecidableEq BoxIntegral.IntegrationParams
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.instSub : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π₁ : ContRepresentation R G V} →
                              {π₂ : ContRepresentation R G W} → Sub (ContIntertwiningMap π₁ π₂)
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
/-- When `C` has enough projectives, the object `Projective.syzygies f` is
an arbitrarily chosen projective object over `kernel f`.
 -/
CategoryTheory.Projective.syzygies : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.EnoughProjectives C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Limits.HasKernel f] → C
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- The union of the kernels of `(f - μ • id) ^ k` over all `k`.  -/
Module.End.maxGenEigenspace : {R : Type v} →
  {M : Type w} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → Submodule R M
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanced_balanceR! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  l.Balanced →
    r.Balanced →
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size →
        (Std.DTreeMap.Internal.Impl.balanceR! k v l r).Balanced
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Matrix.minpoly_toLin : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {N : Type w}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (b : Module.Basis n R N) (M : Matrix n n R),
  minpoly R ((Matrix.toLin b b) M) = minpoly R M
-- Mathlib.Order.Hom.Bounded
instCoeTCBotHomOfBotHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] → [inst_1 : Bot α] → [inst_2 : Bot β] → [BotHomClass F α β] → CoeTC F (BotHom α β)
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addCommMagma.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → AddCommMagma (f i)],
  Pi.addCommMagma = { toAdd := Pi.instAdd, add_comm := ⋯ }
-- Mathlib.Analysis.RCLike.Basic
IsRCLikeNormedField.mk : ∀ {𝕜 : Type u_3} [hk : NormedField 𝕜], (∃ h, hk = h.toNormedField) → IsRCLikeNormedField 𝕜
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : β}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getD k fallback = t₂.getD k fallback
-- Mathlib.Topology.Order.OrderClosed
interior_Ioi : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a : α},
  interior (Set.Ioi a) = Set.Ioi a
-- Mathlib.LinearAlgebra.Reflection
Module.preReflection_apply_self : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x : M}
  {f : Module.Dual R M}, f x = 2 → (Module.preReflection x f) x = -x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.isSubwalk_nil_iff : ∀ {V : Type u_1} {G : SimpleGraph V} {u v u' : V} (p : G.Walk u v),
  p.IsSubwalk SimpleGraph.Walk.nil ↔ ∃ (hu : u' = u) (hv : u' = v), p = SimpleGraph.Walk.nil.copy hu hv
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
SheafOfModules.ιFree.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {I : Type u} (i : I),
  SheafOfModules.ιFree i = CategoryTheory.Limits.Sigma.ι (fun x => SheafOfModules.unit R) i
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.instPowReal : Pow ENNReal ℝ
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.instNonUnitalNonAssocSemiring : {ι : Type u_1} →
  {R : Type u_3} →
    {A : ι → Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)] →
          [inst_2 : (i : ι) → Module R (A i)] →
            [∀ (i : ι), SMulCommClass R (A i) (A i)] →
              [∀ (i : ι), IsScalarTower R (A i) (A i)] → NonUnitalNonAssocSemiring (PiTensorProduct R fun i => A i)
-- Mathlib.RingTheory.ClassGroup.Basic
toPrincipalIdeal_eq_iff : ∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] {I : (FractionalIdeal (nonZeroDivisors R) K)ˣ} {x : Kˣ},
  (toPrincipalIdeal R K) x = I ↔ FractionalIdeal.spanSingleton (nonZeroDivisors R) ↑x = ↑I
-- Lean.Elab.DeclModifiers
/-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `protected`, `unsafe`, `meta`, `noncomputable`, doc string) -/
Lean.Elab.elabModifiers : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadResolveName m] →
        [Lean.MonadError m] →
          [MonadFinally m] →
            [Lean.Elab.MonadMacroAdapter m] →
              [Lean.MonadRecDepth m] →
                [Lean.MonadTrace m] →
                  [Lean.MonadOptions m] →
                    [Lean.AddMessageContext m] →
                      [Lean.MonadLog m] →
                        [MonadLiftT IO m] → Lean.TSyntax `Lean.Parser.Command.declModifiers → m Lean.Elab.Modifiers
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
/-- Induction following the recursive structure of `sumFrom`.  -/
BirdDet.sumFrom_induct : ∀ (n : ℕ) (motive : ℕ → Prop),
  (∀ lo < n, motive (lo + 1) → motive lo) → (∀ (lo : ℕ), ¬lo < n → motive lo) → ∀ (lo : ℕ), motive lo
-- Init.Data.BitVec.Basic
/-- The bitvector of width `w` that has the largest value when interpreted as an integer.  -/
BitVec.intMax : (w : ℕ) → BitVec w