mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- If `K : J ⥤ C` is a diagram with `C` thin, a cone for `K` is limiting
if and only if the cone point is the product of the components.  -/
CategoryTheory.Limits.isColimitEquivCofanOfIsThin : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [Quiver.IsThin C] →
      {J : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
          {K : CategoryTheory.Functor J C} →
            (c : CategoryTheory.Limits.Cocone K) →
              CategoryTheory.Limits.IsColimit c ≃
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk c.pt c.ι.app)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.contains_eq_isSome_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a : α},
  t.contains a = (Std.DTreeMap.Const.get? t a).isSome
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_truncLT_le : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : DecidableLT Γ] (x : HahnSeries Γ R)
  (c : Γ), ((HahnSeries.truncLT c) x).cardSupp ≤ x.cardSupp
-- Mathlib.Analysis.Calculus.Deriv.Star
HasDerivAt.star : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace 𝕜 F] [inst_4 : StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {f : 𝕜 → F} {f' : F} {x : 𝕜}
  [TrivialStar 𝕜], HasDerivAt f f' x → HasDerivAt (fun x => star (f x)) (star f') x
-- Aesop.Stats.Basic
Aesop.Stats.mk.inj : ∀ {total configParsing ruleSetConstruction search ruleSelection script forwardState : Aesop.Nanos}
  {scriptGenerated : Option Aesop.ScriptGenerated} {ruleStats : Array Aesop.RuleStats}
  {goalStats : Array Aesop.GoalStats}
  {total_1 configParsing_1 ruleSetConstruction_1 search_1 ruleSelection_1 script_1 forwardState_1 : Aesop.Nanos}
  {scriptGenerated_1 : Option Aesop.ScriptGenerated} {ruleStats_1 : Array Aesop.RuleStats}
  {goalStats_1 : Array Aesop.GoalStats},
  { total := total, configParsing := configParsing, ruleSetConstruction := ruleSetConstruction, search := search,
        ruleSelection := ruleSelection, script := script, forwardState := forwardState,
        scriptGenerated := scriptGenerated, ruleStats := ruleStats, goalStats := goalStats } =
      { total := total_1, configParsing := configParsing_1, ruleSetConstruction := ruleSetConstruction_1,
        search := search_1, ruleSelection := ruleSelection_1, script := script_1, forwardState := forwardState_1,
        scriptGenerated := scriptGenerated_1, ruleStats := ruleStats_1, goalStats := goalStats_1 } →
    total = total_1 ∧
      configParsing = configParsing_1 ∧
        ruleSetConstruction = ruleSetConstruction_1 ∧
          search = search_1 ∧
            ruleSelection = ruleSelection_1 ∧
              script = script_1 ∧
                forwardState = forwardState_1 ∧
                  scriptGenerated = scriptGenerated_1 ∧ ruleStats = ruleStats_1 ∧ goalStats = goalStats_1
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instAddCommGroup : {α : Type u_1} → [AddCommGroup α] → AddCommGroup αᵐᵒᵖ
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.fromOpcycles_op_cyclesOpIso_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] {Z : Cᵒᵖ} (h : S.op.cycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.fromOpcycles.op (CategoryTheory.CategoryStruct.comp S.cyclesOpIso.inv h) =
    CategoryTheory.CategoryStruct.comp S.op.toCycles h
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.toIsometry_id : ∀ {R : Type u} [inst : CommRing R] {M : QuadraticModuleCat R},
  QuadraticModuleCat.Hom.toIsometry (CategoryTheory.CategoryStruct.id M) = QuadraticMap.Isometry.id M.form
-- Std.Internal.Do.WP.Basic
/-- `Id`'s `WP` interpretation: `Prop` assertions and no exceptions.  -/
Std.Internal.Do.Id.wpInst : {α : Type u} → Std.Internal.Do.WP (Id α) α Prop EPost⟨⟩
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsupp'_symm_single_mul : ∀ (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R] (i : ι × κ) (r₁ r₂ : R),
  ((finsuppTensorFinsupp' R ι κ).symm fun₀ | i => r₁ * r₂) = (fun₀ | i.1 => r₁) ⊗ₜ[R] fun₀ | i.2 => r₂
-- Lean.Meta.Tactic.Apply
/-- If `synthAssignedInstances` is `true`, then `apply` will synthesize instance implicit arguments
even if they have assigned by `isDefEq`, and then check whether the synthesized value matches the
one inferred. The `congr` tactic sets this flag to false.
 -/
Lean.Meta.postprocessAppMVars : Lean.Name →
  Lean.MVarId → Array Lean.Expr → Array Lean.BinderInfo → optParam Bool true → optParam Bool false → Lean.MetaM Unit
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_dvd_gcd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b c d : α}, a ∣ b → c ∣ d → gcd a c ∣ gcd b d
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toSpanSingleton_pow : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalRing R] (c : R) (n : ℕ),
  ContinuousLinearMap.toSpanSingleton R c ^ n = ContinuousLinearMap.toSpanSingleton R (c ^ n)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.isUnit_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ_[p]}, IsUnit z ↔ ‖z‖ = 1
-- Mathlib.LinearAlgebra.Dual.Defs
Module.Dual.transpose_comp : ∀ {R : Type u_1} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_4}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] {M'' : Type u_5} [inst_5 : AddCommMonoid M'']
  [inst_6 : Module R M''] (u : M' →ₗ[R] M'') (v : M →ₗ[R] M'),
  Module.Dual.transpose (u ∘ₗ v) = Module.Dual.transpose v ∘ₗ Module.Dual.transpose u
-- Mathlib.Tactic.NormNum.LegendreSymbol
/-- This evaluates `r := jacobiSymNat a b` and produces a proof term for the equality
by removing powers of `2` from `b` and then calling `proveJacobiSymOdd`.  -/
Mathlib.Meta.NormNum.proveJacobiSymNat : (ea eb : Q(ℕ)) → (er : Q(ℤ)) × Q(Mathlib.Meta.NormNum.jacobiSymNat «$ea» «$eb» = «$er»)
-- Mathlib.Topology.Separation.Regular
/-- A T₂.₅ space, also known as a Urysohn space, is a topological space
where for every pair `x ≠ y`, there are two open sets, with the intersection of closures
empty, one containing `x` and the other `y` .  -/
T25Space : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.Order.SymmDiff
symmDiff_eq : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), symmDiff a b = a ⊓ bᶜ ⊔ b ⊓ aᶜ
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.topology_eq_top_of_isEmpty : ∀ (S : AlgebraicGeometry.Scheme) [IsEmpty ↥S], AlgebraicGeometry.Scheme.ProEt.topology S = ⊤
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_map : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} {fallback : γ k},
  (Std.DHashMap.map f m).getD k fallback = (Option.map (f k) (m.get? k)).getD fallback
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
MeasureTheory.integral_tsum : ∀ {α : Type u_1} {G : Type u_3} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {ι : Type u_4} [Countable ι] {f : ι → α → G},
  (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) →
    ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤ → ∫ (a : α), ∑' (i : ι), f i a ∂μ = ∑' (i : ι), ∫ (a : α), f i a ∂μ
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.cast_symm_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_5} {A : ι → Type u_6} [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] [inst_3 : (i : ι) → TopologicalSpace (A i)] {i j : ι} (h : i = j) (x : A j),
  (ContinuousAlgEquiv.cast h).symm x = (Equiv.cast ⋯) x
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_zpow : ∀ {ι : Type u_1} {G : Type u_5} [inst : DivisionCommMonoid G] (f : ι → G) (s : Finset ι) (n : ℤ),
  ∏ a ∈ s, f a ^ n = (∏ a ∈ s, f a) ^ n
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The obvious functor `(WidePushoutShape J)ᵒᵖ ⥤ WidePullbackShape J`  -/
CategoryTheory.Limits.widePushoutShapeUnop : (J : Type w) →
  CategoryTheory.Functor (CategoryTheory.Limits.WidePushoutShape J)ᵒᵖ (CategoryTheory.Limits.WidePullbackShape J)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_intro_l' : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (P ⊢ₛ Q) → P ⊢ₛ Q ∨ R
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.normalizationObjIso.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  AlgebraicGeometry.Scheme.Hom.normalizationObjIso f hU =
    CategoryTheory.Functor.mapIso (AlgebraicGeometry.Scheme.Hom.normalization f).presheaf
        (CategoryTheory.eqToIso ⋯).op ≪≫
      AlgebraicGeometry.Scheme.Hom.appIso ((AlgebraicGeometry.Scheme.Hom.normalizationOpenCover f).f ⟨U, hU⟩) ⊤ ≪≫
        AlgebraicGeometry.Scheme.ΓSpecIso
          (Opposite.unop
            (((AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor Y).op.comp
                    (AlgebraicGeometry.Scheme.Hom.normalizationDiagram f)).rightOp.obj
              ⟨U, hU⟩))
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Ici₀ : ∀ {G₀ : Type u_2} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {c : G₀} (a : G₀),
  0 < c → (fun x => c * x) ⁻¹' Set.Ici a = Set.Ici (a / c)
-- Init.Data.UInt.Lemmas
UInt32.toUSize_ofNatTruncate_of_le : ∀ {n : ℕ}, UInt32.size ≤ n → (UInt32.ofNatClamp n).toUSize = USize.ofNatLT (UInt32.size - 1) ⋯
-- Mathlib.CategoryTheory.Limits.EssentiallySmall
CategoryTheory.Limits.hasColimitsOfShape_of_essentiallySmall : ∀ (J : Type u₂) [inst : CategoryTheory.Category.{v₂, u₂} J] (C : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} C]
  [CategoryTheory.EssentiallySmall.{w₁, v₂, u₂} J] [CategoryTheory.Limits.HasColimitsOfSize.{w₁, w₁, v₁, u₁} C],
  CategoryTheory.Limits.HasColimitsOfShape J C
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.extractLsb'_if : ∀ {w : ℕ} {c : Bool} {x y : BitVec w} (s l : ℕ),
  BitVec.extractLsb' s l (bif c then x else y) = bif c then BitVec.extractLsb' s l x else BitVec.extractLsb' s l y
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.saturation_sup : ∀ {M : Type u_1} [inst : MulOneClass M] {s₁ s₂ : Submonoid M}, (s₁ ⊔ s₂).saturation = s₁.saturation ⊔ s₂.saturation
-- Mathlib.Algebra.QuadraticAlgebra.Defs
/-- Imaginary part of an element in quadratic algebra  -/
QuadraticAlgebra.im : {R : Type u} → {a b : R} → QuadraticAlgebra R a b → R
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.maxKeyD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {fallback : α},
  t₁.Equiv t₂ → t₁.maxKeyD fallback = t₂.maxKeyD fallback
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.comp_comparison_forget_hasColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J D)
  (R : CategoryTheory.Functor D C) [inst_3 : CategoryTheory.ComonadicLeftAdjoint R]
  [CategoryTheory.Limits.HasColimit (F.comp R)],
  CategoryTheory.Limits.HasColimit
    ((F.comp (CategoryTheory.Comonad.comparison (CategoryTheory.comonadicAdjunction R))).comp
      (CategoryTheory.comonadicAdjunction R).toComonad.forget)
-- Std.Data.Iterators.Lemmas.Producers.Slice
Std.Slice.foldlM_iter : ∀ {γ : Type u} {α β : Type v} {m : Type u_1 → Type u_2} {δ : Type u_1} [inst : Monad m]
  [inst_1 : Std.ToIterator (Std.Slice γ) Id α β] [inst_2 : Std.Iterator α Id β] [inst_3 : Std.IteratorLoop α Id m]
  {s : Std.Slice γ} {init : δ} {f : δ → β → m δ}, Std.Iter.foldM f init s.iter = Std.Slice.foldlM f init s
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.instCommRingObjForgetBialgHomX : {R : Type u} →
  [inst : CommRing R] → {A : CommHopfAlgCat R} → CommRing ((CategoryTheory.forget (CommHopfAlgCat R)).obj A)
-- Mathlib.Algebra.Star.Basic
/-- In a commutative ring, make `simp` prefer leaving the order unchanged.  -/
star_mul' : ∀ {R : Type u} [inst : CommMagma R] [inst_1 : StarMul R] (x y : R), star (x * y) = star x * star y
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.functor_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] {X Y : C}
  (f : X ⟶ Y) (T : C),
  (CategoryTheory.Limits.prod.functor.map f).app T =
    CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id T)
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- A variant of `DirectSum.induction_on` that uses `DirectSum.lof` instead of `.of`  -/
DirectSum.induction_lon : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : DecidableEq ι] {M : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module R (M i)]
  {motive : (DirectSum ι fun i => M i) → Prop} (x : DirectSum ι fun i => M i),
  motive 0 →
    (∀ (i : ι) (x : M i), motive ((DirectSum.lof R ι M i) x)) →
      (∀ (x y : DirectSum ι fun i => M i), motive x → motive y → motive (x + y)) → motive x
-- Std.Http.Protocol.H1.Writer
/-- Returns `true` when no more user body data will arrive: either the user called
`closeBody`, or the writer has already transitioned to `complete` or `closed`.

Note: this does **not** mean the wire is ready to accept new bytes — a `closed`
writer cannot send anything. Use this to decide whether to flush pending body
data rather than to check writability.
 -/
Std.Http.Protocol.H1.Writer.noMoreUserData : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Bool
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- The bundled commutative semiring giving the filtered colimit of a diagram.  -/
CommSemiRingCat.FilteredColimits.colimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J CommSemiRingCat → CommSemiRingCat
-- Mathlib.Topology.Order.Hom.Basic
/-- Copy of a `ContinuousOrderHom` with a new `ContinuousMap` equal to the old one. Useful to fix
definitional equalities.  -/
ContinuousOrderHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : Preorder α] →
        [inst_2 : TopologicalSpace β] → [inst_3 : Preorder β] → (f : α →Co β) → (f' : α → β) → f' = ⇑f → α →Co β
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → Bool},
  t.WF → ((Std.TreeMap.Raw.filter f t).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ t), f (t.getKey k h) t[k] = true)
-- Init.Data.String.Lemmas.Pattern.Pred
_private.Init.Data.String.Lemmas.Pattern.Pred.0.String.Slice.Pos.revSkipWhile.eq_1 : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  pos.revSkipWhile pat =
    match pos.revSkip? pat with
    | some nextCurr => if nextCurr < pos then nextCurr.revSkipWhile pat else pos
    | none => pos
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.Ψ_fromOpcycles : ∀ {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]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.Ψ_fromOpcycles._auto_1),
  CategoryTheory.CategoryStruct.comp (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁) (X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁) =
    CategoryTheory.CategoryStruct.comp (X.iCycles f₂ f₃ n₀) (X.δ f₁₂ f₃ n₀ n₁ hn₁)
-- Init.Data.Nat.Lemmas
Nat.dvd_add_right : ∀ {a b c : ℕ}, a ∣ b → (a ∣ b + c ↔ a ∣ c)
-- Mathlib.Data.ZMod.Basic
ZMod.eq_1 : ZMod 0 = ℤ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_eq_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k fallback : α}, k ∈ t → t.getKeyD k fallback = k
-- Mathlib.CategoryTheory.Abelian.Transfer
CategoryTheory.ShrinkHoms.hasFiniteLimits : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.LocallySmall.{w, v_1, u_1} C]
  [CategoryTheory.Limits.HasFiniteLimits C], CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.ShrinkHoms.{u_1} C)
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.mk : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₂} →
            [inst_3 : CategoryTheory.EnrichedCategory V D] →
              (obj : C → D) →
                (map : (X Y : C) → (X ⟶[V] Y) ⟶ obj X ⟶[V] obj Y) →
                  autoParam
                      (∀ (X : C),
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (map X X) =
                          CategoryTheory.eId V (obj X))
                      CategoryTheory.EnrichedFunctor.map_id._autoParam →
                    autoParam
                        (∀ (X Y Z : C),
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (map X Z) =
                            CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.tensorHom (map X Y) (map Y Z))
                              (CategoryTheory.eComp V (obj X) (obj Y) (obj Z)))
                        CategoryTheory.EnrichedFunctor.map_comp._autoParam →
                      CategoryTheory.EnrichedFunctor V C D
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrixIn_apply_same : ∀ {ι : 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) [FaithfulSMul S R]
  (i : ↥b.support), RootPairing.Base.cartanMatrixIn S b i i = 2
-- Mathlib.RingTheory.PowerSeries.Restricted
/-- Predicate for when `f` is a restricted power series.  -/
PowerSeries.IsRestricted : {R : Type u_1} → [NormedRing R] → ℝ → PowerSeries R → Prop
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
/-- The derivative of `log ∘ f` is the logarithmic derivative provided `f` is differentiable and
`f x  ≠ 0`.  -/
Real.deriv_log_comp_eq_logDeriv : ∀ {f : ℝ → ℝ} {x : ℝ}, DifferentiableAt ℝ f x → f x ≠ 0 → deriv (Real.log ∘ f) x = logDeriv f x
-- Init.Data.Vector.Find
Vector.findSomeRev?_push_of_isNone : ∀ {α : Type u_1} {n : ℕ} {α_1 : Type u_2} {f : α → Option α_1} {a : α} {xs : Vector α n} {h : (f a).isNone = true},
  Vector.findSomeRev? f (xs.push a) = Vector.findSomeRev? f xs
-- Init.Data.List.Lemmas
/-- We can prove that two folds over the same list are related (by some arbitrary relation)
if we know that the initial elements are related and the folding function, for each element of the list,
preserves the relation.
 -/
List.foldl_rel : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {f : β → α → β} {g : γ → α → γ} {a : β} {b : γ}
  {r : β → γ → Prop},
  r a b →
    (∀ a ∈ l, ∀ (c : β) (c' : γ), r c c' → r (f c a) (g c' a)) →
      r (List.foldl (fun acc a => f acc a) a l) (List.foldl (fun acc a => g acc a) b l)
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainTermGoal.mk.inj : ∀ {goal : String} {range : Lean.Lsp.Range} {goal_1 : String} {range_1 : Lean.Lsp.Range},
  { goal := goal, range := range } = { goal := goal_1, range := range_1 } → goal = goal_1 ∧ range = range_1
-- Aesop.Rule
Aesop.RegularRule.isUnsafe : Aesop.RegularRule → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct
SSet.instQuasicategoryObjIhomTerminal : ∀ (A : SSet), (A ⟹ ⊤_ SSet).Quasicategory
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
/-- A section over a compact open of a scheme is nilpotent if and only if its associated
basic open is empty.  -/
AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  IsCompact ↑U → ∀ (f : ↑(X.presheaf.obj (Opposite.op U))), IsNilpotent f ↔ X.basicOpen f = ⊥
-- Mathlib.Algebra.Module.SpanRank
Ideal.spanRank_map_le : ∀ {R S : Type u} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (I : Ideal R),
  Submodule.spanRank (Ideal.map f I) ≤ Submodule.spanRank I
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.lt_log_of_zpow_lt : ∀ {x y : ℝ} {n : ℤ}, 0 < x → x ^ n < y → ↑n * Real.log x < Real.log y
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- This propositional typeclass ensures that `UpwardEnumerable.succ?` is injective.
 -/
Std.PRange.LinearlyUpwardEnumerable : (α : Type u) → [Std.PRange.UpwardEnumerable α] → Prop
-- Mathlib.Order.Basic
/-- monotonicity of `<` with respect to `→`  -/
lt_imp_lt_of_le_of_le : ∀ {α : Type u_2} [inst : Preorder α] {a b c d : α}, c ≤ a → b ≤ d → a < b → c < d
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- Construct the adjunction to the comparison functor.
 -/
CategoryTheory.Monad.MonadicityInternal.leftAdjointComparison : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {G : CategoryTheory.Functor D C} →
          {F : CategoryTheory.Functor C D} →
            (adj : F ⊣ G) →
              [∀ (A : adj.toMonad.Algebra),
                    CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] →
                CategoryTheory.Functor adj.toMonad.Algebra D
-- Mathlib.Order.Defs.PartialOrder
instTransGE : {α : Type u_1} → [inst : Preorder α] → Trans GE.ge GE.ge GE.ge
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality : ∀ {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] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X)
  (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex),
  CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f →
    ∀ (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ),
      CategoryTheory.CategoryStruct.comp ((F.leftDerived n).map f) (Q.isoLeftDerivedObj F n).hom =
        CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom
          (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp
                (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map
            φ)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_minKey?_eq_not_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.minKey?.isSome = !t.isEmpty
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Algebra.isIntegral_sup : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {S T : Subalgebra R A},
  Algebra.IsIntegral R ↥(S ⊔ T) ↔ Algebra.IsIntegral R ↥S ∧ Algebra.IsIntegral R ↥T
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.filterMap_eq_filter : ∀ {α : Type u} {β : α → Type v} {f : (a : α) → β a → Bool} {l : Std.DHashMap.Internal.AssocList α β},
  Std.DHashMap.Internal.AssocList.filterMap (fun k => Option.guard fun v => f k v) l =
    Std.DHashMap.Internal.AssocList.filter f l