mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.id_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} (X : CategoryTheory.CostructuredArrow S T),
  (CategoryTheory.CategoryStruct.id X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Topology.Neighborhoods
nhds_basis_closeds : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X), (nhds x).HasBasis (fun s => x ∉ s ∧ IsClosed s) compl
-- Mathlib.Order.Hom.Bounded
TopHom.instPartialOrder : {α : Type u_2} → {β : Type u_3} → [inst : Top α] → [PartialOrder β] → [inst_2 : Top β] → PartialOrder (TopHom α β)
-- Mathlib.InformationTheory.Coding.KraftMcMillan
_private.Mathlib.InformationTheory.Coding.KraftMcMillan.0.InformationTheory.concatFn : {α : Type u_1} → {S : Finset (List α)} → {r : ℕ} → (Fin r → ↥S) → List α
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.kernelIsoKer.eq_1 : ∀ {G H : AddCommGrpCat} (f : G ⟶ H),
  AddCommGrpCat.kernelIsoKer f =
    {
      hom :=
        AddCommGrpCat.ofHom
          { toFun := fun g => ⟨(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernel.ι f)) g, ⋯⟩,
            map_zero' := ⋯, map_add' := ⋯ },
      inv := CategoryTheory.Limits.kernel.lift f (AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom f).ker.subtype) ⋯,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedEMatchDiagNode : Inhabited Lean.Meta.Grind.EMatchDiagNode
-- Init.Data.Int.Linear
/-- Converts the given expression into a polynomial, and then normalizes it.  -/
Int.Internal.Linear.Expr.norm : Int.Internal.Linear.Expr → Int.Internal.Linear.Poly
-- Mathlib.Algebra.DualNumber
/-- Show DualNumber with values x and y as an `"x + y*ε"` string  -/
DualNumber.instRepr : {R : Type u_1} → [Repr R] → Repr (DualNumber R)
-- Init.MethodSpecsSimp
AndOp.andOp_hAnd : ∀ {α : Type u_1} [inst : AndOp α], AndOp.and = HAnd.hAnd
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.comp.match_1.eq_4 : ∀ {C : Type u_1}
  (motive : CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → Sort u_2)
  (_Y : C) (x : CategoryTheory.WithInitial C)
  (h_1 :
    (_X _Y _Z : C) →
      motive (CategoryTheory.WithInitial.of _X) (CategoryTheory.WithInitial.of _Y) (CategoryTheory.WithInitial.of _Z))
  (h_2 :
    (x : CategoryTheory.WithInitial C) →
      (_X : C) → motive CategoryTheory.WithInitial.star x (CategoryTheory.WithInitial.of _X))
  (h_3 :
    (x : CategoryTheory.WithInitial C) →
      (_X : C) → motive x (CategoryTheory.WithInitial.of _X) CategoryTheory.WithInitial.star)
  (h_4 :
    (_Y : C) →
      (x : CategoryTheory.WithInitial C) → motive (CategoryTheory.WithInitial.of _Y) CategoryTheory.WithInitial.star x)
  (h_5 : Unit → motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.of _Y, CategoryTheory.WithInitial.star, x with
    | CategoryTheory.WithInitial.of _X, CategoryTheory.WithInitial.of _Y, CategoryTheory.WithInitial.of _Z =>
      h_1 _X _Y _Z
    | CategoryTheory.WithInitial.star, x, CategoryTheory.WithInitial.of _X => h_2 x _X
    | x, CategoryTheory.WithInitial.of _X, CategoryTheory.WithInitial.star => h_3 x _X
    | CategoryTheory.WithInitial.of _Y, CategoryTheory.WithInitial.star, x => h_4 _Y x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star => h_5 ()) =
    h_4 _Y x
-- Mathlib.Algebra.MvPolynomial.Variables
/-- **Alias** of `MvPolynomial.mem_vars_iff_mem_support`. -/
MvPolynomial.mem_vars : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} (i : σ),
  i ∈ p.vars ↔ ∃ d ∈ p.support, i ∈ d.support
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.instReflectsIsomorphismsAddGrpCatForget₂AddMonoidHomCarrierCarrier : (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).ReflectsIsomorphisms
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.get_eq_getₘ : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α fun x => β)
  {h : Std.DTreeMap.Internal.Impl.contains k l = true}
  (h' : (Std.DTreeMap.Internal.Impl.Const.get?ₘ l k).isSome = true),
  Std.DTreeMap.Internal.Impl.Const.get l k h = Std.DTreeMap.Internal.Impl.Const.getₘ l k h'
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.tendsto_agmSequences_fst_agm : ∀ {x y : NNReal}, Filter.Tendsto (fun n => (x.agmSequences y n).1) Filter.atTop (nhds (x.agm y))
-- Mathlib.Order.SuccPred.Archimedean
Succ.rec_linear : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {p : α → Prop},
  (∀ (a : α), p a ↔ p (Order.succ a)) → ∀ (a b : α), p a ↔ p b
-- Lean.Environment
/-- Returns the environment just after importing. `none` if `finalizeImport` has never been called on
it.
 -/
Lean.Environment.importEnv? : Lean.Environment → Option Lean.Environment
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.LiftStruct.opEquiv_symm_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g) (l : ⋯.LiftStruct),
  (CategoryTheory.CommSq.LiftStruct.opEquiv sq).symm l = l.unop
-- Mathlib.Data.Finset.Image
Finset.disjoint_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {s t : Finset α} {f : α → β},
  Function.Injective f → (Disjoint (Finset.image f s) (Finset.image f t) ↔ Disjoint s t)
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.eq_zero_of_det_mem_nonZeroDivisors_of_mulVec_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}, M.mulVec v = 0 → v = 0
-- Lean.Parser.Types
Lean.Parser.Parser.mk.injEq : ∀ (info : Lean.Parser.ParserInfo) (fn : Lean.Parser.ParserFn) (info_1 : Lean.Parser.ParserInfo)
  (fn_1 : Lean.Parser.ParserFn),
  ({ info := info, fn := fn } = { info := info_1, fn := fn_1 }) = (info = info_1 ∧ fn = fn_1)
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `zero_eq_dist`.  -/
hamming_zero_eq_dist : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i},
  0 = hammingDist x y ↔ x = y
-- Mathlib.Algebra.Opposites
MulOpposite.op_comp_unop : ∀ {α : Type u_1}, MulOpposite.op ∘ MulOpposite.unop = id
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isValidRevSearchFrom_iff_isValidRevSearchFrom_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos}
  {l : List (String.Slice.Pattern.SearchStep s)},
  String.Slice.Pattern.Model.IsValidRevSearchFrom p pos l ↔
    String.Slice.Pattern.Model.IsValidRevSearchFrom (fun x => decide (p x)) pos l
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.imageSieve_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) [CategoryTheory.Presheaf.IsLocallySurjective J f] {U : Cᵒᵖ}
  (s : CategoryTheory.ToType (G.obj U)), CategoryTheory.Presheaf.imageSieve f s ∈ J (Opposite.unop U)
-- Mathlib.Probability.Kernel.Composition.CompProd
/-- Lebesgue integral against the composition-product of two kernels.  -/
ProbabilityTheory.Kernel.lintegral_compProd' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ]
  (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β → γ → ENNReal},
  Measurable (Function.uncurry f) →
    ∫⁻ (bc : β × γ), f bc.1 bc.2 ∂(κ.compProd η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f b c ∂η (a, b) ∂κ a
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.rePart : ∀ {α : Type u_1} {m : MeasurableSpace α} {c : MeasureTheory.ComplexMeasure α} {μ : MeasureTheory.Measure α}
  [self : c.HaveLebesgueDecomposition μ], (MeasureTheory.ComplexMeasure.re c).HaveLebesgueDecomposition μ
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
/-- `secondInter` is unchanged by multiplying the vector by a nonzero real.  -/
EuclideanGeometry.Sphere.secondInter_smul : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : EuclideanGeometry.Sphere P) (p : P) (v : V) {r : ℝ},
  r ≠ 0 → s.secondInter p (r • v) = s.secondInter p v
-- Mathlib.GroupTheory.OreLocalization.OreSet
AddOreLocalization.AddOreSet.mk : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} →
      (∀ (r₁ r₂ : R) (s : ↥S), r₁ + ↑s = r₂ + ↑s → ∃ s', ↑s' + r₁ = ↑s' + r₂) →
        (oreMin : R → ↥S → R) →
          (oreSubtra : R → ↥S → ↥S) →
            (∀ (r : R) (s : ↥S), ↑(oreSubtra r s) + r = oreMin r s + ↑s) → AddOreLocalization.AddOreSet S
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.mopEquiv_counitIso_inv_app_hom_unmop : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Mon Cᴹᵒᵖ),
  ((MonObj.mopEquiv C).counitIso.inv.app X).hom.unmop = CategoryTheory.CategoryStruct.id X.X.unmop
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.summable_norm_mul_pow : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal}, ↑r < p.radius → Summable fun n => ‖p n‖ * ↑r ^ n
-- Mathlib.Order.CompleteBooleanAlgebra
iSup_inf_of_monotone : ∀ {α : Type u} [inst : Order.Frame α] {ι : Type u_1} [inst_1 : Preorder ι] [IsDirectedOrder ι] {f g : ι → α},
  Monotone f → Monotone g → ⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.Hom.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} {x y : E.Hom F}, x = y ↔ x.s₀ = y.s₀ ∧ x.h₀ ≍ y.h₀
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtAllPlaces_eq_of_normAtComplexPlaces_eq : ∀ {K : Type u_1} [inst : Field K] {x y : NumberField.mixedEmbedding.mixedSpace K},
  NumberField.mixedEmbedding.normAtComplexPlaces x = NumberField.mixedEmbedding.normAtComplexPlaces y →
    NumberField.mixedEmbedding.normAtAllPlaces x = NumberField.mixedEmbedding.normAtAllPlaces y
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.ker_subtype : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.subtype.ker = ⊥
-- Mathlib.FieldTheory.Normal.Defs
/-- Restrict algebra isomorphism to a normal subfield  -/
AlgEquiv.restrictNormal : {F : Type u_1} →
  [inst : Field F] →
    {K₁ : Type u_3} →
      {K₂ : Type u_4} →
        [inst_1 : Field K₁] →
          [inst_2 : Field K₂] →
            [inst_3 : Algebra F K₁] →
              [inst_4 : Algebra F K₂] →
                (K₁ ≃ₐ[F] K₂) →
                  (E : Type u_6) →
                    [inst_5 : Field E] →
                      [inst_6 : Algebra F E] →
                        [inst_7 : Algebra E K₁] →
                          [inst_8 : Algebra E K₂] →
                            [IsScalarTower F E K₁] → [IsScalarTower F E K₂] → [Normal F E] → Gal(E/F)
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.uniqueGalC : {F : Type u_1} → [inst : Field F] → (x : F) → Unique (Polynomial.C x).Gal
-- Std.Time.DateTime.PlainDateTime
/-- Returns the week-based year for the given `PlainDateTime`, using `firstDay` as the start of the week
and `minDays` as the minimum number of days a week must have in the new year to count as week 1.
The week-based year may differ from the calendar year for dates near the start or end of the year.
 -/
Std.Time.PlainDateTime.weekYear : Std.Time.PlainDateTime →
  optParam Std.Time.Weekday Std.Time.Weekday.monday →
    optParam (Std.Time.Internal.Bounded.LE 0 6)
        (Std.Time.Internal.Bounded.LE.mk 4 Std.Time.PlainDateTime.weekOfYear._proof_1) →
      Std.Time.Year.Offset
-- Mathlib.FieldTheory.KrullTopology
/-- If `L/K` is an algebraic field extension, then the Krull topology on `Gal(L/K)` is
totally separated.  -/
krullTopology_isTotallySeparated : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsIntegral K L],
  IsTotallySeparated Set.univ
-- Aesop.Stats.Basic
Aesop.ForwardClusterStateStats.mk.injEq : ∀ (slots : ℕ) (instantiationStats : Array Aesop.ForwardInstantiationStats) (slots_1 : ℕ)
  (instantiationStats_1 : Array Aesop.ForwardInstantiationStats),
  ({ slots := slots, instantiationStats := instantiationStats } =
      { slots := slots_1, instantiationStats := instantiationStats_1 }) =
    (slots = slots_1 ∧ instantiationStats = instantiationStats_1)
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabRic : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- The set `0 : Set α` is defined as `{0}` in scope `Pointwise`.  -/
Set.zero : {α : Type u_2} → [Zero α] → Zero (Set α)
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.shouldPropagateExpectedTypeFor : Lean.Elab.Term.Arg → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicones.functoriality_obj_snd : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type uD} [inst_2 : CategoryTheory.Category.{uD', uD} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (P Q : C) (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms]
  (A : CategoryTheory.Limits.BinaryBicone P Q),
  ((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).obj A).snd = F.map A.snd
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.internalize : Lean.Expr → ℕ → optParam (Option Lean.Expr) none → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Geometry.Euclidean.Volume.Measure
Submodule.measurableEquivProd_symm_apply : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MetricSpace P]
  [inst_6 : MeasurableSpace P] [inst_7 : BorelSpace P] [inst_8 : NormedAddTorsor V P] (s : Submodule ℝ V) (p : P)
  (q : ↥s × ↥sᗮ), (s.measurableEquivProd p).symm q = (↑q.1 + ↑q.2) +ᵥ p
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeAddGroup.mk : ∀ {G : Type u} [inst : AddGroup G], (∃ ι, Nonempty (FreeAddGroupBasis ι G)) → IsFreeAddGroup G
-- Mathlib.Data.Set.Card
Set.ncard_le_one_iff_eq : ∀ {α : Type u_1} {s : Set α}, autoParam s.Finite Set.ncard_le_one_iff_eq._auto_1 → (s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a})
-- Mathlib.Algebra.Free
/-- The universal property of the free magma expressing its adjointness.  -/
FreeMagma.lift : {α : Type u} → {β : Type v} → [inst : Mul β] → (α → β) ≃ (FreeMagma α →ₙ* β)
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.coe_mk : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (f : X → Y) (h : IsLocallyConstant f),
  ⇑{ toFun := f, isLocallyConstant := h } = f
-- Mathlib.Data.Nat.Factorial.Basic
/-- `n.descFactorial k = n! / (n - k)!` but without ℕ-division. See `Nat.descFactorial_eq_div`
for the version using ℕ-division.  -/
Nat.factorial_mul_descFactorial : ∀ {n k : ℕ}, k ≤ n → (n - k).factorial * n.descFactorial k = n.factorial
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- `L₀` is the kernel of `v₁₂ : L₁ ⟶ L₂`.  -/
CategoryTheory.ShortComplex.SnakeInput.h₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (self : CategoryTheory.ShortComplex.SnakeInput C) →
        CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι self.v₀₁ ⋯)
-- Mathlib.Data.Set.Finite.Lattice
Set.toFinset_iUnion : ∀ {α : Type u} {β : Type v} [inst : Fintype β] [inst_1 : DecidableEq α] (f : β → Set α)
  [inst_2 : (w : β) → Fintype ↑(f w)], (⋃ x, f x).toFinset = Finset.univ.biUnion fun x => (f x).toFinset
-- Mathlib.Data.Holor
Holor.instZero : {α : Type} → {ds : List ℕ} → [Zero α] → Zero (Holor α ds)
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
ValuativeRel.isValuativeTopology : ∀ (R : Type u_1) [inst : Ring R] [inst_1 : ValuativeRel R], IsValuativeTopology R
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.hComp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C]
  {a b c d : CategoryTheory.CatEnrichedOrdinary C} {f f' : a ⟶ b} {g g' : b ⟶ c} {h h' : c ⟶ d} (η : f ⟶ f')
  (θ : g ⟶ g') (κ : h ⟶ h'),
  CategoryTheory.CatEnrichedOrdinary.hComp (CategoryTheory.CatEnrichedOrdinary.hComp η θ) κ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CatEnrichedOrdinary.hComp η (CategoryTheory.CatEnrichedOrdinary.hComp θ κ))
        (CategoryTheory.eqToHom ⋯))
-- Mathlib.Algebra.Group.Units.Equiv
/-- A version of `Equiv.mulLeft a b⁻¹` that is defeq to `a / b`.  -/
Equiv.divLeft : {G : Type u_5} → [Group G] → G → G ≃ G
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.innerDone_flatMap_pure : ∀ {α β α₂ γ : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterator α₂ Id γ] {f : β → Std.Iter γ}
  {it₁ : Std.Iter β} {it₂ : Std.Iter γ},
  it₂.IsPlausibleStep Std.IterStep.done →
    (Std.Iter.flatMapAfter f it₁ (some it₂)).IsPlausibleStep (Std.IterStep.skip (Std.Iter.flatMapAfter f it₁ none))
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.mk.sizeOf_spec : ∀ {σ : Type u_1} [inst : SizeOf σ] (syn : Type u_2)
  (addCommMonoidSyn : autoParam (AddCommMonoid syn) MonomialOrder.addCommMonoidSyn._autoParam)
  (linearOrderSyn : autoParam (LinearOrder syn) MonomialOrder.linearOrderSyn._autoParam)
  (isOrderedAddMonoid_syn : autoParam (IsOrderedAddMonoid syn) MonomialOrder.isOrderedAddMonoid_syn._autoParam)
  (toSyn : (σ →₀ ℕ) ≃+ syn) (toSyn_monotone : Monotone ⇑toSyn)
  (wellFoundedLT_syn : autoParam (WellFoundedLT syn) MonomialOrder.wellFoundedLT_syn._autoParam),
  sizeOf
      { syn := syn, addCommMonoidSyn := addCommMonoidSyn, linearOrderSyn := linearOrderSyn,
        isOrderedAddMonoid_syn := isOrderedAddMonoid_syn, toSyn := toSyn, toSyn_monotone := toSyn_monotone,
        wellFoundedLT_syn := wellFoundedLT_syn } =
    1 + sizeOf syn + sizeOf addCommMonoidSyn + sizeOf linearOrderSyn + sizeOf isOrderedAddMonoid_syn + sizeOf toSyn +
      sizeOf wellFoundedLT_syn
-- Mathlib.Order.Filter.Pi
Filter.coprodᵢ_neBot_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} [∀ (i : ι), Nonempty (α i)],
  (Filter.coprodᵢ f).NeBot ↔ ∃ d, (f d).NeBot
-- Mathlib.RingTheory.Coalgebra.Hom
Coalgebra.ext_to_ring : ∀ {R : Type u} (A : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (f g : A →ₗc[R] R), f = g
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.IsSeparated.empty : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : ENNReal}, Metric.IsSeparated ε ∅
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.map_monic_eq_zero_iff : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial R},
  p.Monic → (Polynomial.map f p = 0 ↔ ∀ (x : R), f x = 0)
-- Mathlib.Topology.Bornology.Absorbs
/-- **Alias** of the forward direction of `absorbs_neg_neg`. -/
Absorbs.of_neg_neg : ∀ {M : Type u_1} {E : Type u_2} [inst : Monoid M] [inst_1 : AddGroup E] [inst_2 : DistribMulAction M E]
  [inst_3 : Bornology M] {s t : Set E}, Absorbs M (-s) (-t) → Absorbs M s t
-- Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
ExteriorAlgebra.lhom_ext_iff : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {f g : ExteriorAlgebra R M →ₗ[R] N},
  f = g ↔
    ∀ (i : ℕ), f.compAlternatingMap (ExteriorAlgebra.ιMulti R i) = g.compAlternatingMap (ExteriorAlgebra.ιMulti R i)
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Subfunctor.to_sheafifyLift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.Subfunctor F) (f : G.toFunctor ⟶ F')
  (h : CategoryTheory.Presieve.IsSheaf J F'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.homOfLe ⋯) (G.sheafifyLift f h) = f
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instSemigroup.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Semigroup M],
  Filter.Germ.instSemigroup = { toMul := Filter.Germ.instMul, mul_assoc := ⋯ }
-- Mathlib.RepresentationTheory.Basic
Representation.ker_leftRegular_norm_eq : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Group G] [inst_2 : Fintype G],
  LinearMap.ker (Representation.leftRegular k G).norm =
    ((Finsupp.linearCombination k fun x => 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.mk : {A : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : LieRing L] →
        [inst_2 : Module A L] →
          (toSubmodule : Submodule A L) →
            (∀ {a b : L}, a ∈ toSubmodule.carrier → b ∈ toSubmodule.carrier → ⁅a, b⁆ ∈ toSubmodule.carrier) →
              LieRinehartSubalgebra A L
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.RightHomotopy.ofEq_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} (h : f = g), (CategoryTheory.Arrow.RightHomotopy.ofEq h).hom = 0
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedContext.errToSorry : Lean.Elab.Term.SavedContext → Bool
-- Lean.Parser.Types
Lean.Parser.ParserState.mkUnexpectedErrorAt : Lean.Parser.ParserState → String → String.Pos.Raw → Lean.Parser.ParserState
-- Init.Data.SInt.Lemmas
Int16.toInt64_lt : ∀ {a b : Int16}, a.toInt64 < b.toInt64 ↔ a < b
-- Mathlib.Analysis.Convex.Continuous
ConcaveOn.locallyLipschitzOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {C : Set E} {f : E → ℝ}
  [FiniteDimensional ℝ E], IsOpen C → ConcaveOn ℝ C f → LocallyLipschitzOn C f
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.Hom.mk.congr_simp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A}
  (hom hom_1 : (a : A) → F.functor a ⟶ G.functor a) (e_hom : hom = hom_1)
  (comm :
    ∀ (n a a' : A) (ha' : n + a = a'),
      CategoryTheory.CategoryStruct.comp (F.shiftIso n a a' ha').hom (hom a) =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (hom a') (CategoryTheory.shiftFunctor D n)) (G.shiftIso n a a' ha').hom),
  { hom := hom, comm := comm } = { hom := hom_1, comm := ⋯ }
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight_sumElim_zero_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} {ι' : Type u_3} [Finite ι]
  [Finite ι'] (x : ι → K), Height.logHeight (Sum.elim x 0) = Height.logHeight x
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.piCongrRight_apply : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : α → Sort u_3} (e : (a : α) → β a ↪ γ a) (f : (a : α) → β a) (a : α),
  (Function.Embedding.piCongrRight e) f a = (e a) (f a)
-- Mathlib.Algebra.Notation.Prod
Prod.instSub : {G : Type u_8} → {H : Type u_9} → [Sub G] → [Sub H] → Sub (G × H)