mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.merge.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Option α → Sort u_2) (x : α) (h_1 : Unit → motive none none)
  (h_2 : (x : α) → motive (some x) none) (h_3 : (y : α) → motive none (some y))
  (h_4 : (x y : α) → motive (some x) (some y)),
  (match some x, none with
    | none, none => h_1 ()
    | some x, none => h_2 x
    | none, some y => h_3 y
    | some x, some y => h_4 x y) =
    h_2 x
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- The property that a morphism property `W` is stable under coproducts indexed by a type `J`.  -/
CategoryTheory.MorphismProperty.IsStableUnderCoproductsOfShape : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Type u_1 → Prop
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.op_X : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V c) (i : ι),
  X.op.X i = Opposite.op (X.X i)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey?_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β},
  (Std.DTreeMap.Const.alter t k f).getKey? k' =
    if cmp k k' = Ordering.eq then if (f (Std.DTreeMap.Const.get? t k)).isSome = true then some k else none
    else t.getKey? k'
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulRightStrictMono.toMulPosStrictMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [MulRightStrictMono α], MulPosStrictMono α
-- Mathlib.Order.SupClosed
SupClosed.sSup_mem_of_nonempty : ∀ {α : Type u_3} [inst : ConditionallyCompleteLattice α] {s t : Set α},
  SupClosed s → t.Finite → t.Nonempty → t ⊆ s → sSup t ∈ s
-- Init.Data.SInt.Bitwise
Int32.toISize_or : ∀ (a b : Int32), (a ||| b).toISize = a.toISize ||| b.toISize
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.map_eq_lift : ∀ {α : Type u} {β : Type v} {f : α → β}, FreeAddGroup.map f = FreeAddGroup.lift (FreeAddGroup.of ∘ f)
-- Mathlib.Data.Set.Prod
Set.singleton_prod : ∀ {α : Type u_1} {β : Type u_2} {t : Set β} {a : α}, {a} ×ˢ t = Prod.mk a '' t
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.monoidalOpOp_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.opOp C) X Y =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.opOp C).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
-- Init.Data.Nat.Lemmas
Nat.mul_div_cancel_left' : ∀ {a b : ℕ}, a ∣ b → a * (b / a) = b
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
CategoryTheory.InjectiveResolution.ι'_f_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.InjectiveResolution X),
  R.ι'.f 0 =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).hom
      (CategoryTheory.CategoryStruct.comp (R.ι.f 0)
        (R.cochainComplexXIso 0 0 CategoryTheory.InjectiveResolution.ι'_f_zero._proof_1).inv)
-- Mathlib.Topology.Algebra.ConstMulAction
Homeomorph.vadd_symm_apply : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [inst_3 : ContinuousConstVAdd G α] (γ : G) (x : α), (Homeomorph.vadd γ).symm x = -γ +ᵥ x
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.merge.eq_def : ∀ {α : Type u_1} (xs ys : List α) (le : α → α → Bool),
  xs.merge ys le =
    match xs, ys with
    | [], ys => ys
    | xs, [] => xs
    | x :: xs, y :: ys => if le x y = true then x :: xs.merge (y :: ys) le else y :: (x :: xs).merge ys le
-- Mathlib.Topology.Instances.Matrix
HasSum.matrix_blockDiagonal : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [inst : AddCommMonoid R]
  [inst_1 : TopologicalSpace R] {L : SummationFilter X} [inst_2 : DecidableEq p] {f : X → p → Matrix m n R}
  {a : p → Matrix m n R}, HasSum f a L → HasSum (fun x => Matrix.blockDiagonal (f x)) (Matrix.blockDiagonal a) L
-- Mathlib.MeasureTheory.Group.Arithmetic
Pi.measurableSMul : ∀ {M : Type u_2} [inst : MeasurableSpace M] {ι : Type u_6} {α : ι → Type u_7} [inst_1 : (i : ι) → SMul M (α i)]
  [inst_2 : (i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableSMul M (α i)], MeasurableSMul M ((i : ι) → α i)
-- Init.Data.List.Find
List.find?_eq_none : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.find? p l = none ↔ ∀ x ∈ l, ¬p x = true
-- Init.Data.Range.Polymorphic.PRange
Std.Roo.mk : {α : Type u} → α → α → Std.Roo α
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.linearEquiv.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] (G : ι → Type u_3)
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
  [inst_4 : DecidableEq ι] [inst_5 : Nonempty ι] [inst_6 : IsDirectedOrder ι]
  [inst_7 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)],
  Module.DirectLimit.linearEquiv G f =
    LinearEquiv.ofLinearMap (Module.DirectLimit.lift R ι G f (DirectLimit.Module.of R ι G f) ⋯)
      (DirectLimit.Module.lift R ι G f (Module.DirectLimit.of R ι G f) ⋯) ⋯ ⋯
-- Mathlib.InformationTheory.Hamming
Hamming.nnnorm_eq_hammingNorm : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
  [inst_2 : (i : ι) → AddGroup (β i)] (x : Hamming β), ‖x‖₊ = ↑(hammingNorm (Hamming.ofHamming x))
-- Mathlib.RingTheory.MvPolynomial.Localization
/-- The canonical algebra map from `MvPolynomial Unit R` quotiented by
`C r * X () - 1` to the localization of `R` away from `r`.  -/
_private.Mathlib.RingTheory.MvPolynomial.Localization.0.IsLocalization.Away.auxHom : {R : Type u_2} →
  [inst : CommRing R] →
    (S : Type u_3) →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (r : R) →
            [IsLocalization.Away r S] →
              MvPolynomial Unit R ⧸ Ideal.span {MvPolynomial.C r * MvPolynomial.X () - 1} →ₐ[R] S
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousWithinAt.inf : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {x : α} {s : Set α} {r' : α → β → Prop},
  SemicontinuousWithinAt r s x → SemicontinuousWithinAt r' s x → SemicontinuousWithinAt (r ⊓ r') s x
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.id_mem_unitary : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E], ContinuousLinearMap.id 𝕜 E ∈ unitary (E →L[𝕜] E)
-- Mathlib.Algebra.GroupWithZero.Equiv
/-- An isomorphism of monoids with zero can be treated as a homomorphism preserving zero.
This is a helper projection that utilizes the `MonoidWithZeroHomClass` instance.  -/
MulEquiv.toMonoidWithZeroHom : {G : Type u_1} → {H : Type u_2} → [inst : MulZeroOneClass G] → [inst_1 : MulZeroOneClass H] → G ≃* H → G →*₀ H
-- Lean.Elab.Tactic.Induction
Lean.tactic.customEliminators : Lean.Option Bool
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
/-- In a category with weak equivalences, this is the quotient of the type
of morphisms `X ⟶ Y` by the equivalence relation generated by left homotopies.  -/
HomotopicalAlgebra.LeftHomotopyClass : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → C → C → [HomotopicalAlgebra.CategoryWithWeakEquivalences C] → Type v
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `lt_neg`. -/
lt_neg_of_lt_neg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α],
  a < -b → b < -a
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_map_sectL : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : PartialOrder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : DecidableLE (α × β)] (a b : α) (c : β),
  Finset.map (Function.Embedding.sectL α c) (Finset.Ico a b) = Finset.Ico (a, c) (b, c)
-- Mathlib.Data.Num.Lemmas
Num.ppred_to_nat : ∀ (n : Num), castNum <$> n.ppred = (↑n).ppred
-- Init.Data.Vector.Zip
Vector.zip_unzip : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (xs : Vector (α × β) n), xs.unzip.1.zip xs.unzip.2 = xs
-- Mathlib.Analysis.Complex.Polynomial.GaussLucas
/-- Given a polynomial `P` of positive degree and a root `z` of its derivative,
`derivRootWeight P z w` gives the weight of a root `w` of `P` in a convex combination
that is equal to `z`.  -/
Polynomial.derivRootWeight : Polynomial ℂ → ℂ → ℂ → ℝ
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_op_addSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] (s : AddSubgroup G), AddAction.stabilizer Gᵃᵒᵖ ↑s = s.op
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- Let `M` be an `A`-module. Every `A`-linear map `Mⁿ → Mⁿ` corresponds to a `n×n`-matrix whose entries
are `R`-linear maps `M → M`. In another word, we have `End(Mⁿ) ≅ Matₙₓₙ(End(M))` defined by:
`(f : Mⁿ → Mⁿ) ↦ (x ↦ f (0, ..., x at j-th position, ..., 0) i)ᵢⱼ` and
`m : Matₙₓₙ(End(M)) ↦ (v ↦ ∑ⱼ mᵢⱼ(vⱼ))`.

See also `LinearMap.toMatrix'`
 -/
endVecAlgEquivMatrixEnd : (ι : Type u_1) →
  [inst : Fintype ι] →
    [inst_1 : DecidableEq ι] →
      (R : Type u_2) →
        [inst_2 : CommSemiring R] →
          (A : Type u_3) →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] →
                (M : Type u_4) →
                  [inst_5 : AddCommMonoid M] →
                    [inst_6 : Module R M] →
                      [inst_7 : Module A M] →
                        [inst_8 : IsScalarTower R A M] → Module.End A (ι → M) ≃ₐ[R] Matrix ι ι (Module.End A M)
-- Mathlib.Order.Filter.Lift
Filter.HasBasis.lift' : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β} {ι : Sort u_5} {p : ι → Prop} {s : ι → Set α},
  f.HasBasis p s → Monotone h → (f.lift' h).HasBasis p (h ∘ s)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
/-- The coequalizer of `f g : X ⟶ Y` is the pushout of the diagonal map `X ⨿ X ⟶ X`
along the map `(f, g) : X ⨿ X ⟶ Y`.  -/
CategoryTheory.Limits.isPushout_coequalizer_coprod : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasCoequalizer f g] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X X],
  CategoryTheory.IsPushout (CategoryTheory.Limits.coprod.desc f g)
    (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))
    (CategoryTheory.Limits.coequalizer.π f g)
    (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.coequalizer.π f g))
-- Mathlib.CategoryTheory.Limits.Preserves.Lattice
CategoryTheory.Limits.CompleteLattice.instPreservesFiniteColimitsToFunctorToOrderHom : ∀ {α : Type u} {β : Type v} {F : Type u_1} [inst : FunLike F α β] (f : F) [inst_1 : SemilatticeSup α]
  [inst_2 : OrderBot α] [inst_3 : SemilatticeSup β] [inst_4 : OrderBot β] [inst_5 : SupBotHomClass F α β],
  CategoryTheory.Limits.PreservesFiniteColimits (↑f).toFunctor
-- Init.Data.List.TakeDrop
List.drop_left : ∀ {α : Type u_1} {l₁ l₂ : List α}, List.drop l₁.length (l₁ ++ l₂) = l₂
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.getLast!.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.Algebra.Order.Floor.Div
gc_floorDiv_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : FloorDiv α β] {a : α},
  0 < a → GaloisConnection (fun x => a • x) fun x => x ⌊/⌋ a
-- Batteries.Data.List.Basic
List.replaceFTR.go.eq_1 : ∀ {α : Type u_1} (f : α → Option α) (a : Array α), List.replaceFTR.go f [] a = a.toList
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_finsetInf' : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SemilatticeInf β] [inst_2 : Zero β]
  [inst_3 : TopologicalSpace β] [inst_4 : ContinuousInf β] {ι : Type u_5} {s : Finset ι} (H : s.Nonempty)
  (f : ι → CompactlySupportedContinuousMap α β), ⇑(s.inf' H f) = s.inf' H fun i => ⇑(f i)
-- Mathlib.Order.SetNotation
/-- Supremum of a set  -/
SupSet.sSup : {α : Type u_1} → [self : SupSet α] → Set α → α
-- Mathlib.Algebra.CharP.Algebra
/-- If `R` has characteristic `p`, then so does Frac(R).  -/
IsFractionRing.charP_of_isFractionRing : ∀ (R : Type u_3) {K : Type u_4} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  (p : ℕ) [CharP R p], CharP K p
-- Mathlib.Data.Tree.Traversable
BinaryTree.instLawfulTraversable : LawfulTraversable BinaryTree
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
/-- Formulation of reflection formula tailored to functional equations of L-functions of odd
Dirichlet characters.  -/
Complex.inv_Gammaℝ_two_sub : ∀ {s : ℂ}, (∀ (n : ℕ), s ≠ -↑n) → (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin (↑Real.pi * s / 2) * (s + 1).Gammaℝ⁻¹
-- Mathlib.CategoryTheory.Action.Limits
Action.instPreservesFiniteColimitsForgetOfHasFiniteColimits : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [CategoryTheory.Limits.HasFiniteColimits V], CategoryTheory.Limits.PreservesFiniteColimits (Action.forget V G)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_of_aestronglyMeasurable' : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (hm : m ≤ m₀) [hμm : MeasureTheory.SigmaFinite (μ.trim hm)] {f : α → E},
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.Integrable f μ → μ[f | m] =ᵐ[μ] f
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.PolyCnstr.toExpr : Nat.Internal.Linear.PolyCnstr → Nat.Internal.Linear.ExprCnstr
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.cyclesOpIso_hom_naturality_assoc : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] {Z : Vᵒᵖ} (h : Opposite.op (K.opcycles i) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap ((HomologicalComplex.opFunctor V c).map φ.op) i)
      (CategoryTheory.CategoryStruct.comp (K.cyclesOpIso i).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (L.cyclesOpIso i).hom (HomologicalComplex.opcyclesMap φ i).op) h
-- Mathlib.Algebra.Group.Action.Prod
/-- Scalar multiplication as a monoid homomorphism.  -/
smulMonoidHom : {α : Type u_5} →
  {β : Type u_6} →
    [inst : Monoid α] →
      [inst_1 : MulOneClass β] → [inst_2 : MulAction α β] → [IsScalarTower α β β] → [SMulCommClass α β β] → α × β →* β
-- Mathlib.Analysis.Matrix.Order
/-- The pre-inner product space structure implementation. Only an auxiliary for
`Matrix.toMatrixSeminormedAddCommGroup`, `Matrix.toMatrixNormedAddCommGroup`,
and `Matrix.toMatrixInnerProductSpace`.  -/
_private.Mathlib.Analysis.Matrix.Order.0.Matrix.PosSemidef.matrixPreInnerProductSpace : {𝕜 : Type u_1} →
  {n : Type u_2} →
    [inst : RCLike 𝕜] → [Fintype n] → {M : Matrix n n 𝕜} → M.PosSemidef → PreInnerProductSpace.Core 𝕜 (Matrix n n 𝕜)
-- Mathlib.Data.Finset.NatAntidiagonal
Finset.Nat.antidiagonal_eq_map : ∀ (n : ℕ),
  Finset.HasAntidiagonal.antidiagonal n = Finset.map { toFun := fun i => (i, n - i), inj' := ⋯ } (Finset.range (n + 1))
-- Mathlib.Algebra.Category.MonCat.Adjunctions
MonCat.adj.eq_1 : MonCat.adj =
  CategoryTheory.Adjunction.mkOfHomEquiv
    {
      homEquiv := fun X Y =>
        CategoryTheory.ConcreteCategory.homEquiv.trans (FreeMonoid.lift.symm.trans TypeCat.homEquiv.symm),
      homEquiv_naturality_left_symm := @MonCat.adj._proof_3, homEquiv_naturality_right := @MonCat.adj._proof_2 }
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.IsFiveWheelLike.isNClique_left : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {r k : ℕ} {v w₁ w₂ : α} {s t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → G.IsNClique (r + 1) (insert v s)
-- Init.Data.Array.OfFn
_private.Init.Data.Array.OfFn.0.Array.ofFn.go.match_1.eq_2 : ∀ {n : ℕ} (motive : (x : ℕ) → x ≤ n → Sort u_1) (x : 0 ≤ n) (h_1 : (i : ℕ) → (h : i + 1 ≤ n) → motive i.succ h)
  (h_2 : (x : 0 ≤ n) → motive 0 x),
  (match 0, x with
    | i.succ, h => h_1 i h
    | 0, x => h_2 x) =
    h_2 x
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.op_monotone : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty C},
  P ≤ Q → P.op ≤ Q.op
-- Lean.Elab.Term.TermElabM
/-- Return the list of nested `let rec` declarations that need to be lifted.  -/
Lean.Elab.Term.getLetRecsToLift : Lean.Elab.TermElabM (List Lean.Elab.Term.LetRecToLift)
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.instSmallD₁OfIsSmallOfLocallySmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [CategoryTheory.MorphismProperty.IsSmall.{w, v, u} W] [CategoryTheory.LocallySmall.{w, v, u} C],
  Small.{w, max u v} (CategoryTheory.OrthogonalReflection.D₁ W Z)
-- Mathlib.Algebra.GroupWithZero.Action.Pi
Pi.smulZeroClass' : {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      {n : (i : I) → Zero (g i)} → [(i : I) → SMulZeroClass (f i) (g i)] → SMulZeroClass ((i : I) → f i) ((i : I) → g i)
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- Compatibility of the monoid and comonoid structures, in terms of morphisms in `C`.  -/
CategoryTheory.Bimon.compatibility : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : C) [inst_3 : CategoryTheory.BimonObj M],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul CategoryTheory.ComonObj.comul)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator M M (CategoryTheory.MonoidalCategoryStruct.tensorObj M M)).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M
            (CategoryTheory.MonoidalCategoryStruct.associator M M M).inv)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M
              (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ M M).hom M))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M
                (CategoryTheory.MonoidalCategoryStruct.associator M M M).hom)
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.MonoidalCategoryStruct.associator M M
                    (CategoryTheory.MonoidalCategoryStruct.tensorObj M M)).inv
                (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul
                  CategoryTheory.MonObj.mul)))))) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul CategoryTheory.ComonObj.comul
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.node.sizeOf_spec : ∀ (i : Lean.Elab.Info) (children : Lean.PersistentArray Lean.Elab.InfoTree),
  sizeOf (Lean.Elab.InfoTree.node i children) = 1 + sizeOf i + sizeOf children
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.id.injEq : ∀ (stx : Lean.Syntax) (id : Lean.Name) (danglingDot : Bool) (lctx : Lean.LocalContext)
  (expectedType? : Option Lean.Expr) (stx_1 : Lean.Syntax) (id_1 : Lean.Name) (danglingDot_1 : Bool)
  (lctx_1 : Lean.LocalContext) (expectedType?_1 : Option Lean.Expr),
  (Lean.Elab.CompletionInfo.id stx id danglingDot lctx expectedType? =
      Lean.Elab.CompletionInfo.id stx_1 id_1 danglingDot_1 lctx_1 expectedType?_1) =
    (stx = stx_1 ∧ id = id_1 ∧ danglingDot = danglingDot_1 ∧ lctx = lctx_1 ∧ expectedType? = expectedType?_1)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.functor_map : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) {X : T} (Y : CategoryTheory.Over X)
  {X_1 Y_1 : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.toOver F X) Y} (f : X_1 ⟶ Y_1),
  (CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.functor F Y).map f =
    CategoryTheory.CostructuredArrow.homMk f.left.left ⋯
-- Lean.Parser.Types
Lean.Parser.Error.unexpected : Lean.Parser.Error → String
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.instNonemptyDiagonal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X S : C} {f : X ⟶ S}
  (h : CategoryTheory.Limits.ChosenPullback f f), Nonempty h.Diagonal
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∈ t₂ → (t₁ ∩ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- `Spec` is faithful on `R`-Hopf algebras.  -/
AlgebraicGeometry.hopfSpec.instFaithful : ∀ {R : CommRingCat}, (AlgebraicGeometry.hopfSpec R).Faithful
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?.eq_2 : ∀ {α : Type u} {β : Type v} [inst : BEq α] (a k : α) (v : β) (l : List ((_ : α) × β)),
  Std.Internal.List.getValue? a (⟨k, v⟩ :: l) = bif k == a then some v else Std.Internal.List.getValue? a l
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.category_id_τ₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.CategoryStruct.id sq).τ₁ = CategoryTheory.CategoryStruct.id sq.X₁
-- Mathlib.Algebra.Star.MonoidHom
/-- See Note [custom simps projection]  -/
StarMonoidHom.Simps.coe : {A : Type u_2} →
  {B : Type u_3} → [inst : Monoid A] → [inst_1 : Star A] → [inst_2 : Monoid B] → [inst_3 : Star B] → (A →⋆* B) → A → B
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
/-- The inclusion map of the Moore complex in the alternating face map complex  -/
AlgebraicTopology.inclusionOfMooreComplexMap : {A : Type u_2} →
  [inst : CategoryTheory.Category.{v_2, u_2} A] →
    [inst_1 : CategoryTheory.Abelian A] →
      (X : CategoryTheory.SimplicialObject A) →
        (AlgebraicTopology.normalizedMooreComplex A).obj X ⟶ (AlgebraicTopology.alternatingFaceMapComplex A).obj X
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
/-- See `eLpNorm_smul_measure_of_ne_zero` for a version with scalar multiplication by `ℝ≥0∞`.  -/
MeasureTheory.eLpNorm_smul_measure_of_ne_zero' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {ε : Type u_7} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε]
  {c : NNReal},
  c ≠ 0 →
    ∀ (f : α → ε) (p : ENNReal) (μ : MeasureTheory.Measure α),
      MeasureTheory.eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • MeasureTheory.eLpNorm f p μ
-- Std.Time.Zoned.Database.TzIf
/-- The correction applied during the leap second event in seconds.
 -/
Std.Time.TimeZone.TZif.LeapSecond.correction : Std.Time.TimeZone.TZif.LeapSecond → ℤ
-- Mathlib.Tactic.Abel
/-- Determine whether `e` will be handled as an atom by the `abel` tactic. The `match` in this
function should be preserved to be parallel in case-matching to that in the
`Mathlib.Tactic.Abel.eval` metaprogram.  -/
Mathlib.Tactic.Abel.isAtom : Lean.Expr → Bool
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.ofHom_hom : ∀ {M N : AddMagmaCat} (f : M ⟶ N), AddMagmaCat.ofHom (AddMagmaCat.Hom.hom f) = f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_maxKeyD_eq_maxKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {fallback : α} {hc : Std.DTreeMap.Internal.Impl.contains (t.maxKeyD fallback) t = true},
  t.getKey (t.maxKeyD fallback) hc = t.maxKey ⋯