mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Config
/-- A minimal configuration, with ematching and splitting disabled, and all solver modules turned off.
`grind` will not do anything in this configuration,
which can be used a starting point for minimal configurations.
 -/
Lean.Grind.NoopConfig : Type
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.instInhabitedState.default : Lean.Meta.Grind.Arith.Linear.State
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instMul : {α : Type u_5} → [inst : NonUnitalNonAssocSemiring α] → Mul (CentroidHom α)
-- Mathlib.Data.List.Basic
List.setOfPred_mem_cons : ∀ {α : Type u} (l : List α) (a : α), {x | x ∈ a :: l} = insert a {x | x ∈ l}
-- Lean.Elab.Tactic.Basic
_private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.throwExs : Lean.Syntax → Array Lean.Elab.Tactic.EvalTacticFailure → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.colorable_chromaticNumber_of_fintype : ∀ {V : Type u} (G : SimpleGraph V) [Finite V], G.Colorable G.chromaticNumber.toNat
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.RatAlgebra.dpow_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (I : Ideal R) [inst_1 : DecidablePred fun x => x ∈ I] [inst_2 : Algebra ℚ R]
  {n : ℕ} {x : R},
  (DividedPowers.RatAlgebra.dividedPowers I).dpow n x = if x ∈ I then Ring.inverse ↑n.factorial * x ^ n else 0
-- Mathlib.CategoryTheory.Localization.Resolution
/-- A localizer morphism has left resolutions when any object has a left resolution.  -/
CategoryTheory.LocalizerMorphism.HasLeftResolutions : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} → CategoryTheory.LocalizerMorphism W₁ W₂ → Prop
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Poly.add_denote.go : ∀ (ctx : Nat.Internal.Linear.Context) (fuel : ℕ) (p₁ p₂ : Nat.Internal.SOM.Poly),
  Nat.Internal.SOM.Poly.denote ctx (Nat.Internal.SOM.Poly.add.go✝ fuel p₁ p₂) =
    Nat.Internal.SOM.Poly.denote ctx p₁ + Nat.Internal.SOM.Poly.denote ctx p₂
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.map_preimage_basicOpen : ∀ {A B σ τ : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B]
  [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜]
  [inst_7 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) (s : A),
  (TopologicalSpace.Opens.map (AlgebraicGeometry.Proj.map f hf).base).obj (AlgebraicGeometry.Proj.basicOpen 𝒜 s) =
    AlgebraicGeometry.Proj.basicOpen ℬ (f s)
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.pointwise_smul_def : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M}
  (S : Subsemiring R), a • S = Subsemiring.map (MulSemiringAction.toRingHom M R a) S
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.firstM.go.eq_def : ∀ {β : Type v} {α : Type u} {m : Type v → Type w} [inst : Alternative m] (f : α → m β) (as : Array α) (i : ℕ),
  Array.firstM.go✝ f as i = if hlt : i < as.size then f as[i] <|> Array.firstM.go✝ f as (i + 1) else failure
-- Init.Data.String.Lemmas.Iterate
String.Slice.toList_positionsFrom : ∀ {s : String.Slice} {p : s.Pos}, (String.Slice.positionsFrom p).toList = String.Slice.Model.positionsFrom p
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min!_erase_eq_of_not_compare_min!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k : α}, (t.erase k).isEmpty = false → ¬cmp k t.min! = Ordering.eq → (t.erase k).min! = t.min!
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.toStructuredArrowCompProj_inv_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (X : J),
  c.toStructuredArrowCompProj.inv.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.loops_eq_empty : ∀ {α : Type u_1} (M : Matroid α) [M.Loopless], M.loops = ∅
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.addSimprocAttrCore : Lean.Meta.Simp.SimprocExtension → Lean.Name → Lean.AttributeKind → Bool → Lean.CoreM Unit
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.quotientToQuotientRangePowQuotSucc_mk : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [hfp : NeZero (p.ramificationIdx' P)] {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) (x : S),
  (p.quotientToQuotientRangePowQuotSucc P a_mem) (Submodule.Quotient.mk x) =
    Submodule.Quotient.mk ⟨(Ideal.Quotient.mk (P ^ p.ramificationIdx' P)) (a * x), ⋯⟩
-- Mathlib.Data.Fintype.Card
Set.toFinset_card : ∀ {α : Type u_4} (s : Set α) [inst : Fintype ↑s], s.toFinset.card = Fintype.card ↑s
-- Mathlib.Data.List.AList
/-- The empty association list.  -/
AList.instEmptyCollection : {α : Type u} → {β : α → Type v} → EmptyCollection (AList β)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (n : ℤ)
  {X Y : Cᵒᵖ} (f : X ⟶ Y) {Z : Cᵒᵖ}
  (h :
    (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).inverse.obj
        ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).functor.obj Y) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app Y) h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f).unop).op h)
-- Mathlib.Order.Bounds.Basic
isGreatest_union_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {s t : Set α},
  IsGreatest (s ∪ t) a ↔ IsGreatest s a ∧ a ∈ upperBounds t ∨ a ∈ upperBounds s ∧ IsGreatest t a
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_interval_add_Ioi : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  MeasureTheory.IntegrableOn f (Set.Ioi a) μ →
    MeasureTheory.IntegrableOn f (Set.Ioi b) μ →
      ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in Set.Ioi b, f x ∂μ = ∫ (x : ℝ) in Set.Ioi a, f x ∂μ
-- Mathlib.NumberTheory.RamificationInertia.Galois
Ideal.coe_smul_primesOver_mk : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {p : Ideal A}
  {G : Type u_3} [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [inst_5 : SMulCommClass G A B] (σ : G)
  (P : Ideal B) [inst_6 : P.IsPrime] [inst_7 : P.LiesOver p], ↑(σ • Ideal.primesOver.mk p P) = σ • P
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.limitCone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections],
  CommMonCat.limitCone F =
    CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ CommMonCat MonCat)))
-- Mathlib.Topology.Semicontinuity.Basic
ContinuousAt.comp_lowerSemicontinuousWithinAt : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {δ : Type u_5} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
  [OrderTopology δ] {g : γ → δ} {f : α → γ},
  ContinuousAt g (f x) → LowerSemicontinuousWithinAt f s x → Monotone g → LowerSemicontinuousWithinAt (g ∘ f) s x
-- Mathlib.Order.LiminfLimsup
Filter.limsSup_principal_eq_sSup : ∀ {α : Type u_1} [inst : CompleteLattice α] (s : Set α), (Filter.principal s).limsSup = sSup s
-- Mathlib.Logic.Equiv.Prod
Equiv.prodCongr_refl_left : ∀ {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : β₁ ≃ β₂),
  (Equiv.refl α₁).prodCongr e = Equiv.prodCongrRight fun x => e
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isBigOWith_abs_left`. -/
Asymptotics.IsBigOWith.of_abs_left : ∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {c : ℝ} {g : α → F} {l : Filter α} {u : α → ℝ},
  Asymptotics.IsBigOWith c l (fun x => |u x|) g → Asymptotics.IsBigOWith c l u g
-- Init.Data.SInt.Lemmas
ISize.toInt_eq_toNatClampNeg : ∀ {a : ISize}, 0 ≤ a → a.toInt = ↑a.toNatClampNeg
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_ofMultiset : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (s : Multiset R), (Polynomial.ofMultiset s).roots = s
-- Std.Http.Protocol.H1.Config
/-- Maximum number of requests (server) or responses (client) per connection.
 -/
Std.Http.Protocol.H1.Config.maxMessages : Std.Http.Protocol.H1.Config → ℕ
-- Mathlib.RingTheory.Derivation.Lie
Derivation.Compatible.mk_right : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {A' : Type u_3}
  [inst_3 : CommRing A'] [inst_4 : Algebra R A'] [inst_5 : Algebra A A'] [inst_6 : IsScalarTower R A A']
  (x : Derivation R A' A') (y : Derivation R A A) (h : ⇑x ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑y),
  (↑(Derivation.Compatible.mk x y h)).2 = y
-- Mathlib.Order.Partition.Finpartition
Finpartition.indiscrete.congr_simp : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (ha : a ≠ ⊥),
  Finpartition.indiscrete ha = Finpartition.indiscrete ha
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.eq_zero_of_det_mem_nonZeroDivisors_of_vecMul_eq_zero : ∀ {m : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : Fintype m] [inst_2 : DecidableEq m] {M : Matrix m m R},
  M.det ∈ nonZeroDivisors R → ∀ {v : m → R}, Matrix.vecMul v M = 0 → v = 0
-- Init.Data.SInt.Lemmas
Int16.toInt64_ne_minValue : ∀ (a : Int16), a.toInt64 ≠ Int64.minValue
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.forall_apply_eq_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] {a : α} [Finite α], (∀ (ψ : AddChar α ℂ), ψ a = 1) ↔ a = 0
-- Mathlib.RingTheory.Extension.Generators
/-- Given families of generators `X ⊆ T` over `S` and `Y ⊆ S` over `R`,
there is a map of generators `R[X, Y] → S[X]`.  -/
Algebra.Generators.ofComp : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            {ι' : Type u_3} →
              {T : Type u_7} →
                [inst_3 : CommRing T] →
                  [inst_4 : Algebra R T] →
                    [inst_5 : Algebra S T] →
                      [inst_6 : IsScalarTower R S T] →
                        (Q : Algebra.Generators S T ι') → (P : Algebra.Generators R S ι) → (Q.comp P).Hom Q
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.lowerCentralSeries_eq_bot_iff_nilpotencyClass_le`. -/
lowerCentralSeries_eq_bot_iff_nilpotencyClass_le : ∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G] {n : ℕ},
  ⊤.lowerCentralSeries n = ⊥ ↔ Group.nilpotencyClass G ≤ n
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.symm_preimage_preimage : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₂), ⇑e.symm ⁻¹' ⇑e ⁻¹' s = s
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
ContMDiffWithinAt.coordChange : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6}
  [inst : NontriviallyNormedField 𝕜] {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB]
  {HB : Type u_8} [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] {EM : Type u_9} [inst_6 : NormedAddCommGroup EM] [inst_7 : NormedSpace 𝕜 EM]
  {HM : Type u_10} [inst_8 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace HM M] [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)]
  [inst_13 : NormedAddCommGroup F] [inst_14 : NormedSpace 𝕜 F] [inst_15 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_16 : (x : B) → TopologicalSpace (E x)] [inst_17 : FiberBundle F E] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e]
  [MemTrivializationAtlas e'] {s : Set M} {f : M → B} {g : M → F} {x : M},
  ContMDiffWithinAt IM IB n f s x →
    ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n g s x →
      f x ∈ e.baseSet →
        f x ∈ e'.baseSet → ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun y => e.coordChange e' (f y) (g y)) s x
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_toSubmodule_le : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A}
  {t : Submodule R A}, Subalgebra.toSubmodule (Algebra.adjoin R s) ≤ t ↔ ↑(Submonoid.closure s) ⊆ ↑t
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_union : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s₁ s₂ : Finset β} {f : β → α}
  [inst_2 : DecidableEq β], (s₁ ∪ s₂).inf f = s₁.inf f ⊓ s₂.inf f
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Constructor for morphisms to the point of a limit multifork.  -/
CategoryTheory.Limits.Multifork.IsLimit.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      {I : CategoryTheory.Limits.MulticospanIndex J C} →
        {K : CategoryTheory.Limits.Multifork I} →
          CategoryTheory.Limits.IsLimit K →
            {T : C} →
              (k : (a : J.L) → T ⟶ I.left a) →
                (∀ (b : J.R),
                    CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) =
                      CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b)) →
                  (T ⟶ K.pt)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instInhabited : {R : Type u} → {M : Type v} → [inst : VAdd R M] → Inhabited (SubAddAction R M)
-- Mathlib.Algebra.Group.Units.Basic
eq_one_of_mul_right' : ∀ {α : Type u} [inst : CancelMonoid α] [Subsingleton αˣ] {a b : α}, a * b = 1 → a = 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_alter_eq_self_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  k ∈ t → (f (t.get? k)).isSome = true → (t.alter k f).size = t.size
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsLower.isTopologicalBasis : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLower α],
  TopologicalSpace.IsTopologicalBasis (Topology.IsLower.lowerBasis α)
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.coe_algebraMap : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M], ⇑(algebraMap R (MonoidAlgebra A M)) = MonoidAlgebra.single 1 ∘ ⇑(algebraMap R A)
-- Init.Data.AC
Lean.Data.AC.removeNeutrals.loop.eq_2 : ∀ {α : Sort u_1} [info : Lean.Data.AC.ContextInformation α] (ctx : α), Lean.Data.AC.removeNeutrals.loop ctx [] = []
-- Mathlib.Order.Hom.Lattice
LatticeHomClass.mk : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : FunLike F α β]
  [toSupHomClass : SupHomClass F α β] [toInfHomClass : InfHomClass F α β], LatticeHomClass F α β
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.one_le_exp_iff : ∀ {a : EReal}, 1 ≤ a.exp ↔ 0 ≤ a
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Equality of the composition of the unit and counit with the identity `F ⟶ FGF ⟶ F = 𝟙`  -/
CategoryTheory.Adjunction.left_triangle_components_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (self : F ⊣ G) (X : C) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (self.unit.app X))
      (CategoryTheory.CategoryStruct.comp (self.counit.app (F.obj X)) h) =
    h
-- Mathlib.CategoryTheory.ConcreteCategory.Bundled
/-- A generic function for lifting a type equipped with an instance to a bundled object.  -/
CategoryTheory.Bundled.of : {c : Type u → Type v} → (α : Type u) → [str : c α] → CategoryTheory.Bundled c
-- Mathlib.Data.List.Sort
List.mem_insertionSort : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] {l : List α} {x : α}, x ∈ List.insertionSort r l ↔ x ∈ l
-- Mathlib.Algebra.Group.Action.Opposite
AddCommSemigroup.isCentralVAdd : ∀ {α : Type u_3} [inst : AddCommSemigroup α], IsCentralVAdd α α
-- Lean.Log
Lean.instMonadLogOfMonadLift : (m n : Type → Type) → [MonadLift m n] → [Lean.MonadLog m] → Lean.MonadLog n
-- Mathlib.Topology.MetricSpace.Algebra
LipschitzAdd.lipschitz_add : ∀ {β : Type u_2} {inst : PseudoMetricSpace β} {inst_1 : AddMonoid β} [self : LipschitzAdd β],
  ∃ C, LipschitzWith C fun p => p.1 + p.2
-- Mathlib.Order.KrullDimension
Order.LTSeries.length_le_krullDim : ∀ {α : Type u_1} [inst : Preorder α] (p : LTSeries α), ↑p.length ≤ Order.krullDim α
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.instQuotientInnerProductSpace : {𝕜 : Type u_1} →
  {E : Type u_4} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          (K : Submodule 𝕜 E) → [K.HasOrthogonalProjection] → InnerProductSpace 𝕜 (E ⧸ K)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.lift_K_comp_cyclesIso_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {A : C} (k : A ⟶ S.X₂)
  (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [inst_2 : S.HasLeftHomology] {Z : C} (h_1 : S.cycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (h.liftK k hk) (CategoryTheory.CategoryStruct.comp h.cyclesIso.inv h_1) =
    CategoryTheory.CategoryStruct.comp (S.liftCycles k hk) h_1
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.neg : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (j : J)
  (x : ↑(F.obj j)),
  CommRingCat.Colimits.Relation F (CommRingCat.Colimits.Prequotient.of j (-x))
    (CommRingCat.Colimits.Prequotient.of j x).neg
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- We say that a measurable space separates points if for any two distinct points,
there is a measurable set containing one but not the other.  -/
MeasurableSpace.SeparatesPoints : (α : Type u_3) → [m : MeasurableSpace α] → Prop
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.uniqueHomFromTrivial_default_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C), default.hom = CategoryTheory.MonObj.one
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.coe_prod : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N),
  ↑(s.prod t) = ↑s ×ˢ ↑t
-- Mathlib.Order.Hom.Bounded
/-- Reinterpret a bounded order homomorphism as a bounded order homomorphism between the dual
orders.  -/
BoundedOrderHom.dual : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : BoundedOrder α] →
        [inst_2 : Preorder β] → [inst_3 : BoundedOrder β] → BoundedOrderHom α β ≃ BoundedOrderHom αᵒᵈ βᵒᵈ
-- Mathlib.Topology.UniformSpace.Separation
/-- The separation quotient functor acting on functions.  -/
SeparationQuotient.map : {α : Type u} →
  {β : Type v} →
    [inst : UniformSpace α] → [inst_1 : UniformSpace β] → (α → β) → SeparationQuotient α → SeparationQuotient β
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.finset_logSizeBallSeq_add_one : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T] (hJ : J.Nonempty)
  (i : ℕ),
  (PairReduction.logSizeBallSeq J hJ a c (i + 1)).finset =
    (PairReduction.logSizeBallSeq J hJ a c i).finset \ (PairReduction.logSizeBallSeq J hJ a c i).smallBall c
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
AEMeasurable.min : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [SecondCountableTopology α] [OrderClosedTopology α] {f g : δ → α}
  {μ : MeasureTheory.Measure δ}, AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun a => min (f a) (g a)) μ
-- Init.Data.List.MinMax
List.max?_eq_some_iff : ∀ {α : Type u_1} {a : α} [inst : Max α] [inst_1 : LE α] {xs : List α} [Std.IsLinearOrder α] [Std.LawfulOrderMax α],
  xs.max? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a
-- Mathlib.Analysis.Convex.Gauge
/-- If `s` is balanced, then the Minkowski functional is ℂ-homogeneous.  -/
gauge_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : RCLike 𝕜]
  [inst_3 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E], Balanced 𝕜 s → ∀ (r : 𝕜) (x : E), gauge s (r • x) = ‖r‖ * gauge s x
-- Mathlib.Algebra.Lie.LieTheorem
/-- The weight space of `V` with respect to `χ : A → R`, a priori a Lie submodule for `A`, is also a
Lie submodule for `L`.  -/
LieModule.weightSpaceOfIsLieTower : (R : Type u_1) →
  {L : Type u_2} →
    {A : Type u_3} →
      (V : Type u_4) →
        [inst : CommRing R] →
          [IsPrincipalIdealRing R] →
            [IsDomain R] →
              [CharZero R] →
                [inst_4 : LieRing L] →
                  [inst_5 : LieAlgebra R L] →
                    [inst_6 : LieRing A] →
                      [inst_7 : LieAlgebra R A] →
                        [inst_8 : Bracket L A] →
                          [inst_9 : Bracket A L] →
                            [inst_10 : AddCommGroup V] →
                              [inst_11 : Module R V] →
                                [Module.Free R V] →
                                  [Module.Finite R V] →
                                    [inst_14 : LieRingModule L V] →
                                      [LieModule R L V] →
                                        [inst_16 : LieRingModule A V] →
                                          [LieModule R A V] →
                                            [IsLieTower L A V] → [IsLieTower A L V] → (A → R) → LieSubmodule R L V
-- Lean.Server.Requests
Lean.Language.SnapshotTree.foldSnaps.Control.proceed.sizeOf_spec : ∀ (foldChildren : Bool),
  sizeOf (Lean.Language.SnapshotTree.foldSnaps.Control.proceed foldChildren) = 1 + sizeOf foldChildren
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- The constant multiseries approximates the constant function.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.const_approximates : ∀ {c : ℝ} {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis basis →
    (Tactic.ComputeAsymptotics.MultiseriesExpansion.const basis c).Approximates
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.full_empty : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C], CategoryTheory.Subgroupoid.full ∅ = ⊥
-- Mathlib.Algebra.Group.UniqueProds.Basic
MulHom.mk.congr_simp : ∀ {M : Type u_10} {N : Type u_11} [inst : Mul M] [inst_1 : Mul N] (toFun toFun_1 : M → N) (e_toFun : toFun = toFun_1)
  (map_mul' : ∀ (x y : M), toFun (x * y) = toFun x * toFun y),
  { toFun := toFun, map_mul' := map_mul' } = { toFun := toFun_1, map_mul' := ⋯ }