mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.ModObj.assoc_flip : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {M : C} [inst_4 : CategoryTheory.MonObj M] (X : D) [inst_5 : CategoryTheory.ModObj M X],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M CategoryTheory.ModObj.smul)
      CategoryTheory.ModObj.smul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonObj.mul X)
        CategoryTheory.ModObj.smul)
-- Mathlib.Topology.Compactness.Compact
Filter.Tendsto.isCompact_insert_range : ∀ {X : Type u} [inst : TopologicalSpace X] {f : ℕ → X} {x : X},
  Filter.Tendsto f Filter.atTop (nhds x) → IsCompact (insert x (Set.range f))
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.restrictFunctorId_inv_app_app : ∀ {X : AlgebraicGeometry.Scheme} {M : X.Modules} {U : X.Opens},
  AlgebraicGeometry.Scheme.Modules.Hom.app (AlgebraicGeometry.Scheme.Modules.restrictFunctorId.inv.app M) U =
    M.presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Mathlib.Data.Rel
/-- The graph of a function as a relation.  -/
Function.graph : {α : Type u_1} → {β : Type u_2} → (α → β) → SetRel α β
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
/-- Detecting vanishing of a morphism factoring through a connected limit by pushing out along the
projections of the limit.  -/
CategoryTheory.Limits.IsLimit.pushout_zero_ext : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] [CategoryTheory.IsConnected J] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_4 : CategoryTheory.Limits.HasPushouts C] [inst_5 : CategoryTheory.Limits.HasLimitsOfShape J C]
  [CategoryTheory.HasExactLimitsOfShape J C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone F}
  (hc : CategoryTheory.Limits.IsLimit c) {X Y : C} {g : Y ⟶ c.pt} {f : c.pt ⟶ X},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp g
          (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.pushout.inr (c.π.app j) f)) =
        0) →
    CategoryTheory.CategoryStruct.comp g f = 0
-- Mathlib.Algebra.Homology.Embedding.Connect
/-- Auxiliary definition for `ConnectData.cochainComplex`.  -/
CochainComplex.ConnectData.X : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → ChainComplex C ℕ → CochainComplex C ℕ → ℤ → C
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.MonadicityInternal.instHasColimitWalkingParallelPairParallelPairMapAppCounitObjOfHasCoequalizerAA : ∀ {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))] (B : D),
  CategoryTheory.Limits.HasColimit
    (CategoryTheory.Limits.parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B))))
-- Mathlib.Combinatorics.Quiver.Basic
Quiver.homOfEq_trans : ∀ {V : Type u_1} [inst : Quiver V] {X Y X' Y' : V} (f : X ⟶ Y) (hX : X = X') (hY : Y = Y') {X'' Y'' : V}
  (hX' : X' = X'') (hY' : Y' = Y''), Quiver.homOfEq (Quiver.homOfEq f hX hY) hX' hY' = Quiver.homOfEq f ⋯ ⋯
-- Mathlib.Analysis.Calculus.Monotone
/-- A monotone real function is differentiable Lebesgue-almost everywhere.  -/
Monotone.ae_differentiableAt : ∀ {f : ℝ → ℝ}, Monotone f → ∀ᵐ (x : ℝ), DifferentiableAt ℝ f x
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.monoidObj.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) (j : J),
  MonCat.monoidObj F j = (F.obj j).str
-- Mathlib.Data.List.AList
AList.lookup.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s : AList β),
  AList.lookup a s = List.dlookup a s.entries
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited α],
  t.WF → ∀ {l : List α} {k : α}, k ∉ t → l.contains k = false → (t.insertMany l).get! k = default
-- Init.Data.String.Basic
String.Pos.Raw.isValidForSlice_iff_exists_append : ∀ {s : String.Slice} {p : String.Pos.Raw},
  String.Pos.Raw.IsValidForSlice s p ↔ ∃ t₁ t₂, s.copy = t₁ ++ t₂ ∧ p = t₁.rawEndPos
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidSaveTextDocumentParams : Type
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_sub_nat_mul_two_pi : ∀ (x : ℂ) (n : ℕ), Complex.sin (x - ↑n * (2 * ↑Real.pi)) = Complex.sin x
-- Mathlib.LinearAlgebra.Charpoly.BaseChange
LinearEquiv.det_baseChange : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M] (A : Type u_3) [inst_5 : CommRing A] [inst_6 : Algebra R A] (f : M ≃ₗ[R] M),
  LinearEquiv.det (LinearEquiv.baseChange R A M M f) = (Units.map ↑(algebraMap R A)) (LinearEquiv.det f)
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
_private.Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit.0.CategoryTheory.coherentTopology.preimage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preregular C] →
      [inst_2 : CategoryTheory.FinitaryExtensive C] →
        {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))} →
          (∀ (n : ℕ), CategoryTheory.Sheaf.IsLocallySurjective (F.map (CategoryTheory.homOfLE ⋯).op)) →
            (X : C) →
              (F.obj (Opposite.op 0)).obj.obj (Opposite.op X) →
                (n : ℕ) → (Y : C) × (F.obj (Opposite.op n)).obj.obj (Opposite.op Y)
-- Mathlib.Data.Nat.Digits.Defs
/-- an n-digit number in base b + 2 is less than (b + 2)^n  -/
Nat.ofDigits_lt_base_pow_length' : ∀ {b : ℕ} {l : List ℕ}, (∀ x ∈ l, x < b + 2) → Nat.ofDigits (b + 2) l < (b + 2) ^ l.length
-- Init.Data.String.Basic
String.Pos.next.eq_1 : ∀ {s : String} (pos : s.Pos) (h : pos ≠ s.endPos), pos.next h = String.Pos.ofToSlice (pos.toSlice.next ⋯)
-- Mathlib.Order.Filter.CardinalInter
Filter.CardinalGenerateSets.below : {α : Type u} →
  {c : Cardinal.{u}} →
    {g : Set (Set α)} →
      {motive : (a : Set α) → Filter.CardinalGenerateSets g a → Prop} →
        {a : Set α} → Filter.CardinalGenerateSets g a → Prop
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {f : (a : α) → β a → Bool}
  {l : List ((a : α) × β a)} {k : α} [inst_2 : Inhabited (β k)],
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCast! k (List.filter (fun p => f p.fst p.snd) l) =
      (Option.filter (f k) (Std.Internal.List.getValueCast? k l)).get!
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.RingId.0.Lean.Meta.Grind.Arith.CommRing.getCommRingId?.goCore? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.GroupTheory.Torsion
CommGroup.torsion.eq_1 : ∀ (G : Type u_1) [inst : CommGroup G], CommGroup.torsion G = { toSubmonoid := CommMonoid.torsion G, inv_mem' := ⋯ }
-- Mathlib.Algebra.Homology.Bifunctor
/-- Constructor for morphisms from `(mapBifunctor K₁ K₂ F c).X j`.  -/
HomologicalComplex.mapBifunctorDesc : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            {I₁ : Type u_4} →
              {I₂ : Type u_5} →
                {J : Type u_6} →
                  {c₁ : ComplexShape I₁} →
                    {c₂ : ComplexShape I₂} →
                      [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
                        [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                          [inst_5 : CategoryTheory.Preadditive D] →
                            {K₁ : HomologicalComplex C₁ c₁} →
                              {K₂ : HomologicalComplex C₂ c₂} →
                                {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} →
                                  [inst_6 : F.PreservesZeroMorphisms] →
                                    [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                                      {c : ComplexShape J} →
                                        [inst_8 : TotalComplexShape c₁ c₂ c] →
                                          [inst_9 : K₁.HasMapBifunctor K₂ F c] →
                                            [inst_10 : DecidableEq J] →
                                              {A : D} →
                                                {j : J} →
                                                  ((i₁ : I₁) →
                                                      (i₂ : I₂) →
                                                        c₁.π c₂ c (i₁, i₂) = j →
                                                          ((F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ A)) →
                                                    ((K₁.mapBifunctor K₂ F c).X j ⟶ A)
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.dropPrefix_char_eq_dropPrefix_beq : ∀ {c : Char} {s : String.Slice}, s.dropPrefix c = s.dropPrefix fun x => x == c
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            {F G : CategoryTheory.Functor C V} →
              (convolution : CategoryTheory.Functor C V) →
                (unit :
                    CategoryTheory.MonoidalCategory.externalProduct F G ⟶
                      (CategoryTheory.MonoidalCategory.tensor C).comp convolution) →
                  (CategoryTheory.Functor.LeftExtension.mk convolution unit).IsPointwiseLeftKanExtension →
                    CategoryTheory.MonoidalCategory.DayConvolution F G
-- Mathlib.Analysis.Convex.Segment
midpoint_mem_segment : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [inst_5 : Invertible 2] (x y : E), midpoint 𝕜 x y ∈ segment 𝕜 x y
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.Hom.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A B : T.Algebra}
  (f f_1 : A.A ⟶ B.A) (e_f : f = f_1)
  (h : CategoryTheory.CategoryStruct.comp (T.map f) B.a = CategoryTheory.CategoryStruct.comp A.a f),
  { f := f, h := h } = { f := f_1, h := ⋯ }
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
AlternatingMap.mkContinuousLinear_norm_le_max : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  (f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G) (C : ℝ) (H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖),
  ‖AlternatingMap.mkContinuousLinear f C H‖ ≤ max C 0
-- Mathlib.Order.Bounds.Basic
upperBounds_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {t : Set β},
  s.Nonempty → t.Nonempty → upperBounds (s ×ˢ t) = upperBounds s ×ˢ upperBounds t
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.KernelFork.mapIsoOfIsLimit_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {kf : CategoryTheory.Limits.KernelFork f}
  {kf' : CategoryTheory.Limits.KernelFork f'} (hf : CategoryTheory.Limits.IsLimit kf)
  (hf' : CategoryTheory.Limits.IsLimit kf') (φ : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'),
  (CategoryTheory.Limits.KernelFork.mapIsoOfIsLimit hf hf' φ).inv = kf'.mapOfIsLimit hf φ.inv
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.mk.sizeOf_spec : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] {P' : Algebra.Generators R' S' ι'} [inst_6 : Algebra S S']
  [inst_7 : SizeOf R] [inst_8 : SizeOf S] [inst_9 : SizeOf ι] [inst_10 : SizeOf R'] [inst_11 : SizeOf S']
  [inst_12 : SizeOf ι'] (val : ι → P'.Ring)
  (aeval_val : ∀ (i : ι), (MvPolynomial.aeval P'.val) (val i) = (algebraMap S S') (P.val i)),
  sizeOf { val := val, aeval_val := aeval_val } = 1
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₂_monomial : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* MvPolynomial σ S) (d : σ →₀ ℕ) (r : R),
  (MvPolynomial.bind₂ f) ((MvPolynomial.monomial d) r) = f r * (MvPolynomial.monomial d) 1
-- Mathlib.Order.BoundedOrder.Basic
isMin_bot : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderBot α], IsMin ⊥
-- Mathlib.Analysis.InnerProductSpace.Spectrum
/-- *Diagonalization theorem*, *spectral theorem*; version 1: A self-adjoint operator `T` on a
finite-dimensional inner product space `E` acts diagonally on the decomposition of `E` into the
direct sum of the eigenspaces of `T`.  -/
LinearMap.IsSymmetric.diagonalization_apply_self_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] (hT : T.IsSymmetric) (v : E) (μ : Module.End.Eigenvalues T),
  (hT.diagonalization (T v)).ofLp μ = ↑T 1 μ • (hT.diagonalization v).ofLp μ
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst_assoc : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [inst_2 : P.HasPullbacksAlong f] {g : X ⟶ Y}
  [inst_3 : P.IsStableUnderBaseChangeAlong f] [inst_4 : Q.IsStableUnderBaseChange] (h : f = g) (A : P.Over Q Y) {Z : T}
  (h_1 : A.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.Over.pullbackCongr h).hom.app A).left
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst A.hom g) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst A.hom f) h_1
-- Init.Data.Fin.Lemmas
_private.Init.Data.Fin.Lemmas.0.Fin.reverseInduction_castSucc_aux : ∀ {n : ℕ} {motive : Fin (n + 1) → Sort u_1} {succ : (i : Fin n) → motive i.succ → motive i.castSucc} (i : Fin n) (j : ℕ)
  (h : j < n + 1) (h2 : ↑i < j) (zero : motive ⟨j, h⟩),
  Fin.reverseInduction.go succ i.castSucc j h ⋯ zero = succ i (Fin.reverseInduction.go succ i.succ j h h2 zero)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.smul_coroot_eq_of_root_eq_smul : ∀ {ι : 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] {P : RootPairing ι R M N} [Finite ι]
  [IsAddTorsionFree N] (i j : ι) (t : R), P.root j = t • P.root i → t • P.coroot j = P.coroot i
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α}, k ∈ t.insert k
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.instOrderTop : {ι : Type u_1} → {I : BoxIntegral.Box ι} → OrderTop (BoxIntegral.Prepartition I)
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- The localizer morphism from `W₁.arrow` to `W₂.arrow` that is induced by
`Φ : LocalizerMorphism W₁ W₂`.  -/
CategoryTheory.LocalizerMorphism.arrow : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            CategoryTheory.LocalizerMorphism W₁ W₂ → CategoryTheory.LocalizerMorphism W₁.arrow W₂.arrow
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instToJsonRange : Lean.ToJson Lean.Lsp.Range
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- The face of a simplex with all but one point.  -/
Affine.Simplex.faceOpposite : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_5} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] →
            [inst_3 : AddTorsor V P] →
              {n : ℕ} → [NeZero n] → Affine.Simplex k P n → Fin (n + 1) → Affine.Simplex k P (n - 1)
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.decomposeAlgEquiv_apply : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : CommSemiring R]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (𝒜 : ι → Submodule R A) [inst_5 : GradedAlgebra 𝒜] (a : A),
  (DirectSum.decomposeAlgEquiv 𝒜) a = (DirectSum.decompose 𝒜) a
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.δ_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) {m n : M}
  {X Y : C} (f : X ⟶ Y) [inst_3 : F.OplaxMonoidal] {Z : C} (h : (F.obj n).obj ((F.obj m).obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F m n).app X)
      (CategoryTheory.CategoryStruct.comp ((F.obj n).map ((F.obj m).map f)) h) =
    CategoryTheory.CategoryStruct.comp ((F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj m n)).map f)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F m n).app Y) h)
-- Mathlib.Order.SymmDiff
symmDiff_symmDiff_cancel_left : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b : α), symmDiff a (symmDiff a b) = b
-- Mathlib.Probability.ProbabilityMassFunction.Binomial
PMF.binomial_apply_zero : ∀ (p : NNReal) (h : p ≤ 1) (n : ℕ), (PMF.binomial p h n) 0 = (1 - ↑p) ^ n
-- Mathlib.Logic.Basic
Ne.dite_ne_right_iff : ∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {b : α} {A : P → α},
  (∀ (h : P), A h ≠ b) → ((dite P A fun x => b) ≠ b ↔ P)
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.eval_eq_rfindOpt : ∀ (c : Nat.Partrec.Code) (n : ℕ), c.eval n = Nat.rfindOpt fun k => Nat.Partrec.Code.evaln k c n
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- The morphism `Λ[3, 1] ⟶ X` which is obtained by gluing three
morphisms `Δ[2] ⟶ X`.  -/
SSet.horn₃₁.desc : {X : SSet} →
  (f₀ f₂ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X) →
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
        CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃ →
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
          CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂ →
        CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
            CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃ →
          ((SSet.horn 3 1).toSSet ⟶ X)
-- Mathlib.Topology.Homeomorph.Defs
IsHomeomorph.surjective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → Function.Surjective f
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
SSet.stdSimplex.objMk₁_of_castSucc_lt : ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)), j.castSucc < i → (SSet.stdSimplex.objMk₁ i) j = 0
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.inv_ext' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ≅ Y} {g : Y ⟶ X},
  CategoryTheory.CategoryStruct.comp f.hom g = CategoryTheory.CategoryStruct.id X → g = f.inv
-- Mathlib.Analysis.Matrix.Normed
/-- Normed group instance (using sup norm of sup norm) for matrices over a normed group.  Not
declared as an instance because there are several natural choices for defining the norm of a
matrix.  -/
Matrix.normedAddCommGroup : {m : Type u_3} →
  {n : Type u_4} →
    {α : Type u_5} → [Fintype m] → [Fintype n] → [NormedAddCommGroup α] → NormedAddCommGroup (Matrix m n α)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_subset_Ici_self : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : LocallyFiniteOrder α],
  Finset.Ico a b ⊆ Finset.Ici a
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_Icc_of_antitoneOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ},
  a ≤ b → ContinuousOn f (Set.Icc a b) → AntitoneOn f (Set.Icc a b) → f '' Set.Icc a b = Set.Icc (f b) (f a)
-- Mathlib.Algebra.Order.Archimedean.Class
/-- A closed ball defined by `FiniteMulArchimedeanClass.subgroup` of `UpperSet.Ici c`.  -/
FiniteMulArchimedeanClass.closedBallSubgroup : {M : Type u_1} →
  [inst : CommGroup M] →
    [inst_1 : LinearOrder M] → [inst_2 : IsOrderedMonoid M] → FiniteMulArchimedeanClass M → Subgroup M
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.ErrorContext.mk.sizeOf_spec : ∀ (error : Mathlib.Linter.TextBased.StyleError✝) (lineNumber : ℕ) (path : System.FilePath),
  sizeOf { error := error, lineNumber := lineNumber, path := path } = 1 + sizeOf error + sizeOf lineNumber + sizeOf path
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcHom_predicate : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  (f : C(↑(spectrum R a), R)), p ((cfcHom ha) f)
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.findSomeRevM?_find_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] (f : α → m (Option β))
  (l : List α) (i : ℕ) (h : i ≤ l.toArray.size),
  Array.findSomeRevM?.find✝ f l.toArray i h = List.findSomeM? f (List.take i l).reverse
-- Mathlib.NumberTheory.RamificationInertia.Unramified
Ideal.ramificationIdx_eq_one_of_isUnramifiedAt : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal S}
  [inst_3 : p.IsPrime] [Algebra.IsUnramifiedAt R p] [Algebra.EssFiniteType R S], p.ramificationIdx R = 1