mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.RegularEpi
CategoryTheory.Functor.instIsRegularEpiCategoryOfForallEpiHasPullbackOfHasPushouts : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_3, u_2} D]
  [∀ {F G : D} (f : F ⟶ G) [CategoryTheory.Epi f], CategoryTheory.Limits.HasPullback f f]
  [CategoryTheory.Limits.HasPushouts D] [CategoryTheory.IsRegularEpiCategory D],
  CategoryTheory.IsRegularEpiCategory (CategoryTheory.Functor C D)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_1.eq_2 : ∀ {n : ℕ}
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty)
  (h_3 :
    (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      (b : Bool) → motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b)))
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit),
  (match Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty with
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b) => h_3 l b
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit => h_4 ()) =
    h_2 ()
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `LinearMap.isIdempotentElem_iff_eq_projection_range_ker`.

---

A linear map is an idempotent if and only if it equals the projection
onto its range along its kernel.  -/
LinearMap.isIdempotentElem_iff_eq_isCompl_projection_range_ker : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {T : E →ₗ[R] E},
  IsIdempotentElem T ↔ ∃ (h : IsCompl T.range T.ker), T = T.range.projection T.ker h
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- `Res(f, g₁ * g₂) = Res(f, g₁) * Res(f, g₂)`.  -/
Polynomial.resultant_mul_right : ∀ {R : Type u_1} [inst : CommRing R] (f g₁ g₂ : Polynomial R) (m : ℕ),
  f.natDegree ≤ m → f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
IsSelfAdjoint.neg_algebraMap_norm_le_self : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a : A},
  autoParam (IsSelfAdjoint a) IsSelfAdjoint.neg_algebraMap_norm_le_self._auto_1 → -(algebraMap ℝ A) ‖a‖ ≤ a
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- This is a version of `radius_compContinuousLinearMap_linearIsometryEquiv_eq` with better
opportunity for unification, at the cost of manually supplying some hypotheses.  -/
FormalMultilinearSeries.radius_compContinuousLinearMap_eq : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [Nontrivial E] (p : FormalMultilinearSeries 𝕜 F G)
  (u : E →L[𝕜] F), Isometry ⇑u → Function.Surjective ⇑u → (p.compContinuousLinearMap u).radius = p.radius
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.derivative_nodal : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [inst_1 : DecidableEq ι],
  Polynomial.derivative (Lagrange.nodal s v) = ∑ i ∈ s, Lagrange.nodal (s.erase i) v
-- Init.Data.SInt.Lemmas
UInt8.toInt8_neg : ∀ (a : UInt8), (-a).toInt8 = -a.toInt8
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift
_private.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift.0.Affine.Simplex.closedInterior_inter_shift_aux : ∀ {k : Type u_1} [inst : Field k] [inst_1 : LinearOrder k] [IsOrderedRing k] {n : ℕ} (i : Fin n) {x : k},
  0 < x →
    x ≤ 1 →
      ∀ {w : Fin n → k},
        ∑ i, w i = 1 →
          ((∀ (j : Fin n), w j ∈ Set.Icc 0 1) ∧ w i = 1 - x ↔
            (∀ (j : Fin n), j ≠ i → x⁻¹ * w j ∈ Set.Icc 0 1) ∧ x⁻¹ * (w i - 1) + 1 = 0)
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.Measure.integral_comp_mul_right : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (g : ℝ → F) (a : ℝ),
  ∫ (x : ℝ), g (x * a) = |a⁻¹| • ∫ (y : ℝ), g y
-- Mathlib.MeasureTheory.Integral.TorusIntegral
torusIntegral_add : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : (Fin n → ℂ) → E}
  {c : Fin n → ℂ} {R : Fin n → ℝ},
  TorusIntegrable f c R →
    TorusIntegrable g c R →
      (∯ (x : Fin n → ℂ) in T(c, R), f x + g x) =
        (∯ (x : Fin n → ℂ) in T(c, R), f x) + ∯ (x : Fin n → ℂ) in T(c, R), g x
-- Mathlib.GroupTheory.Complement
Subgroup.exists_isComplement_right : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (g : G), ∃ T, Subgroup.IsComplement (↑H) T ∧ g ∈ T
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.opEquiv_functor_map_op_inclLeft : ∀ {C : Type u₁} (D : Type u₂) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {c c' : C} (f : c ⟶ c'),
  (CategoryTheory.Join.opEquiv C D).functor.map (Opposite.op ((CategoryTheory.Join.inclLeft C D).map f)) =
    (CategoryTheory.Join.inclRight Dᵒᵖ Cᵒᵖ).map (Opposite.op f)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The tangent of an angle in a right-angled triangle, where one side is a multiple of a
rotation of another by `π / 2`.  -/
Orientation.tan_oangle_add_right_smul_rotation_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x : V}, x ≠ 0 → ∀ (r : ℝ), (o.oangle x (x + r • (o.rotation ↑(Real.pi / 2)) x)).tan = r
-- Init.Data.BitVec.Lemmas
BitVec.toInt_ofFin : ∀ {w : ℕ} (x : Fin (2 ^ w)), { toFin := x }.toInt = (↑↑x).bmod (2 ^ w)
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.instFunLike : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} →
      [inst_1 : Semiring A] →
        [inst_2 : TopologicalSpace A] →
          {B : Type u_3} →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] → [inst_5 : Algebra R A] → [inst_6 : Algebra R B] → FunLike (A →A[R] B) A B
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instSMulCommClass : ∀ {α : Type u} {β : Type v} {𝕜 : Type u_2} [inst : PseudoMetricSpace 𝕜] [inst_1 : TopologicalSpace α]
  [inst_2 : PseudoMetricSpace β] [inst_3 : Zero 𝕜] [inst_4 : Zero β] [inst_5 : SMul 𝕜 β] [inst_6 : IsBoundedSMul 𝕜 β]
  {𝕜' : Type u_3} [inst_7 : PseudoMetricSpace 𝕜'] [inst_8 : Zero 𝕜'] [inst_9 : SMul 𝕜' β] [inst_10 : IsBoundedSMul 𝕜' β]
  [SMulCommClass 𝕜' 𝕜 β], SMulCommClass 𝕜' 𝕜 (BoundedContinuousFunction α β)
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
BoxIntegral.Prepartition.isSubordinate_toSubordinate : ∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  (r : (ι → ℝ) → ↑(Set.Ioi 0)), (π.toSubordinate r).IsSubordinate r
-- Init.Data.Subtype.Order
Subtype.instTransLE : {α : Type u} →
  [inst : LE α] →
    [i : Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2] →
      {P : α → Prop} → Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.image_rootSet : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : Field A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : IsDomain B] [inst_5 : Algebra R B] {f : Polynomial R},
  (Polynomial.map (algebraMap R A) f).Splits → ∀ (g : A →ₐ[R] B), ⇑g '' f.rootSet A = f.rootSet B
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The function from the colimit commutative ring to the cone point of any other cocone.  -/
CommRingCat.Colimits.descFun : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CommRingCat) →
      (s : CategoryTheory.Limits.Cocone F) → CommRingCat.Colimits.ColimitType F → ↑s.pt
-- Mathlib.Order.Monotone.Basic
StrictAnti.ite : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β},
  StrictAnti f →
    StrictAnti g →
      ∀ {p : α → Prop} [inst_2 : DecidablePred p],
        (∀ ⦃x y : α⦄, x < y → p y → p x) → (∀ (x : α), g x ≤ f x) → StrictAnti fun x => if p x then f x else g x
-- Mathlib.Algebra.Order.Group.Equiv
toEquiv_toLexMulEquiv : ∀ (α : Type u_1) [inst : Mul α], ↑(toLexMulEquiv α) = toLex
-- Mathlib.RingTheory.Perfectoid.Untilt
PreTilt.untilt.congr_simp : ∀ {O : Type u_1} [inst : CommRing O] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p]
  [inst_3 : IsAdicComplete (Ideal.span {↑p}) O], PreTilt.untilt = PreTilt.untilt
-- Mathlib.MeasureTheory.OuterMeasure.Induced
_private.Mathlib.MeasureTheory.OuterMeasure.Induced.0.Option.elim'.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.instUniqueOfNatNat : {R : Type u_1} → [inst : CommMonoidWithZero R] → Unique (DirichletCharacter R 1)
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Notation for the `leftUnitor`: `𝟙_C ⊗ X ≃ X`  -/
CategoryTheory.MonoidalCategory.«termλ_» : Lean.ParserDescr
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoLocallyUniformlyOn.neg` -/
TendstoLocallyUniformlyOn.fun_neg : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F : ι → X → α} {f : X → α} {s : Set X} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s → TendstoLocallyUniformlyOn (fun i i_1 => -F i i_1) (fun i => -f i) l s
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.symm_apply_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) {x : X} {y : Y},
  h.symm y = x ↔ y = h x
-- Mathlib.Algebra.Group.Invertible.Basic
invertiblePow : {α : Type u} → [inst : Monoid α] → (m : α) → [Invertible m] → (n : ℕ) → Invertible (m ^ n)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.map_comap : ∀ {α : Type u_1} {β : Type u_2} {N : Matroid β} {f : α → β},
  N.E ⊆ Set.range f → ∀ (hf : Set.InjOn f (f ⁻¹' N.E)), (N.comap f).map f hf = N
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.subset_closure_sdiff_iff_closure_eq : ∀ {α : Type u_2} {M : Matroid α} {X Y : Set α},
  Y ⊆ X →
    autoParam (Y ⊆ M.E) Matroid.subset_closure_sdiff_iff_closure_eq._auto_1 →
      (Y ⊆ M.closure (X \ Y) ↔ M.closure (X \ Y) = M.closure X)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.instInhabitedOfIsOrderedAddMonoid : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      {R : Type u_3} →
                        [inst_9 : AddCommGroup R] →
                          [inst_10 : LinearOrder R] →
                            [inst_11 : Module K R] →
                              {seed : HahnEmbedding.Seed K M R} →
                                [IsOrderedAddMonoid R] → Inhabited (HahnEmbedding.Partial seed)
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.mk.injEq : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} (toLinearMap : M₁ →ₗ[R] M₂)
  (map_app' : ∀ (m m' : M₁), (B₂ (toLinearMap.toFun m)) (toLinearMap.toFun m') = (B₁ m) m')
  (toLinearMap_1 : M₁ →ₗ[R] M₂)
  (map_app'_1 : ∀ (m m' : M₁), (B₂ (toLinearMap_1.toFun m)) (toLinearMap_1.toFun m') = (B₁ m) m'),
  ({ toLinearMap := toLinearMap, map_app' := map_app' } = { toLinearMap := toLinearMap_1, map_app' := map_app'_1 }) =
    (toLinearMap = toLinearMap_1)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_maxKey?_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t → t.maxKey?.isSome = true
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.srange_snd : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] [Nonempty M], (MulHom.snd M N).srange = ⊤
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mapL_smul_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (r : 𝕜) (f : E →L[𝕜] F) (g : G →L[𝕜] H),
  TensorProduct.mapL f (r • g) = r • TensorProduct.mapL f g
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.left : {α₁ : Type w} →
  {m : Type w → Type w'} →
    {β₁ : Type w} →
      [inst : Std.Iterator α₁ m β₁] → {α₂ β₂ : Type w} → Std.Iterators.Types.Zip α₁ m α₂ β₂ → Std.IterM m β₁
-- Mathlib.Data.Countable.Basic
WithTop.instCountable : ∀ {α : Type u} [Countable α], Countable (WithTop α)
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
SSet.instNonemptyπ₀OfIsConnected : ∀ (X : SSet) [X.IsConnected], Nonempty X.π₀
-- Mathlib.Probability.Kernel.Composition.Lemmas
MeasureTheory.Measure.prod_comp_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν]
  {κ : ProbabilityTheory.Kernel β γ} [ProbabilityTheory.IsSFiniteKernel κ],
  μ.prod (ν.bind ⇑κ) = (μ.prod ν).bind ⇑(ProbabilityTheory.Kernel.id.parallelComp κ)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.minDegree.congr_simp : ∀ {V : Type u_1} (G G_1 : SimpleGraph V),
  G = G_1 →
    ∀ [inst : Fintype V] {inst_1 : DecidableRel G.Adj} [inst_2 : DecidableRel G_1.Adj], G.minDegree = G_1.minDegree
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_pi_div_four : Real.sin (Real.pi / 4) = √2 / 2
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.toENNRealVectorMeasure_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (i : Set α),
  μ.toENNRealVectorMeasure i = if MeasurableSet i then μ i else 0
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.reverse_comp_involute : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M},
  CliffordAlgebra.reverse ∘ₗ CliffordAlgebra.involute.toLinearMap =
    CliffordAlgebra.involute.toLinearMap ∘ₗ CliffordAlgebra.reverse
-- Mathlib.Topology.MetricSpace.HausdorffDimension
Real.dimH_of_nonempty_interior : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E},
  (interior s).Nonempty → dimH s = ↑(Module.finrank ℝ E)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The coaugmented cosimplicial object that is deduced from a cosimplicial object and
an initial object.  -/
CategoryTheory.CosimplicialObject.augmentOfIsInitial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.CosimplicialObject C →
      {T : C} → CategoryTheory.Limits.IsInitial T → CategoryTheory.CosimplicialObject.Augmented C
-- Mathlib.Algebra.Ring.Subring.Defs
/-- Reinterpret a `Subring` as an `AddSubgroup`.  -/
Subring.toAddSubgroup : {R : Type u} → [inst : NonAssocRing R] → Subring R → AddSubgroup R
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.MorphismProperty.IsStableUnderBraiding.braiding_inv_mem : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (P : CategoryTheory.MorphismProperty C) [self : P.IsStableUnderBraiding]
  (c c' : C), P (β_ c c').inv
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.χ_comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {𝒞₁ 𝒞₂ : CategoryTheory.Subobject.Classifier C} {X Y : C}
  (m : X ⟶ Y) [inst_1 : CategoryTheory.Mono m], CategoryTheory.CategoryStruct.comp (𝒞₁.χ m) (𝒞₁.hom 𝒞₂) = 𝒞₂.χ m
-- Mathlib.RingTheory.Nilpotent.Lemmas
LinearMap.isNilpotent_toMatrix_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_3} {M : Type u_4} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (b : Module.Basis ι R M) (f : M →ₗ[R] M),
  IsNilpotent ((LinearMap.toMatrix b b) f) ↔ IsNilpotent f
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.instIsMarkovKernelPUnitDiscard : ∀ {α : Type u_1} {mα : MeasurableSpace α}, ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.discard α)
-- Lean.Data.Lsp.Basic
Lean.Lsp.MarkupKind.markdown.sizeOf_spec : sizeOf Lean.Lsp.MarkupKind.markdown = 1
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.apply : Lean.MVarId → Lean.Expr → Lean.Meta.TransparencyMode → Aesop.Script.TacticBuilder
-- Mathlib.Data.Set.Image
Set.subset_range_iff_exists_image_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, s ⊆ Set.range f ↔ ∃ t, f '' t = s
-- Mathlib.CategoryTheory.Comma.CardinalArrow
CategoryTheory.Arrow.finite_iff : ∀ (C : Type u) [inst : CategoryTheory.SmallCategory C],
  Finite (CategoryTheory.Arrow C) ↔ Nonempty (CategoryTheory.FinCategory C)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.coe_iUnion : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] (f : α → ZFSet.{u}), ↑(ZFSet.iUnion fun i => f i) = ⋃ i, ↑(f i)
-- Mathlib.Topology.Sheaves.Alexandrov
Alexandrov.principals.congr_simp : ∀ (X : Type v) [inst : TopologicalSpace X] [inst_1 : Preorder X] [inst_2 : Topology.IsUpperSet X],
  Alexandrov.principals X = Alexandrov.principals X
-- Init.Grind.Util
/-- A marker to indicate that a proposition has already been normalized and should not
be processed again.

This prevents issues when case-splitting on the condition `c` of an if-then-else
expression. Without this marker, the negated condition `¬c` might be rewritten into
an alternative form `c'`, which `grind` may not recognize as equivalent to `¬c`.
As a result, `grind` could fail to propagate that `if c then a else b` simplifies to `b`
in the `¬c` branch.
 -/
Lean.Grind.alreadyNorm : Prop → Prop
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_mul_left : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] (a : α), UniformContinuous fun b => a * b
-- Mathlib.Computability.Ackermann
_private.Mathlib.Computability.Ackermann.0.ack_strict_mono_left' : ∀ {m₁ m₂ : ℕ} (n : ℕ), m₁ < m₂ → ack m₁ n < ack m₂ n
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation.id : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation id
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageKind : Type
-- Mathlib.Data.EReal.Basic
EReal.coe_nnreal_lt_top : ∀ (x : NNReal), ↑↑x < ⊤
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.WithGeneratedByTopology.continuous_equiv : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y],
  Continuous ⇑Topology.WithGeneratedByTopology.equiv
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittAdd_zero : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], WittVector.wittAdd p 0 = MvPolynomial.X (0, 0) + MvPolynomial.X (1, 0)
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
/-- Given `i` and `j` in `Fin (n + 2)` such that `j ≠ i`, this is the inclusion
of `Δ[n]` in `horn (n + 1) i` given by `stdSimplex.δ j`.  -/
SSet.horn.ι : {n : ℕ} → (i j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ (SSet.horn (n + 1) i).toSSet)
-- Mathlib.Topology.Order.Basic
/-- For a function taking values in a second countable space, the set of points `x` for
which the image under `f` of `(-∞, x)` is separated above from `f x` is countable. We give
here a version relative to a set `t`.  -/
countable_image_gt_image_Iio_within : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [inst_3 : LinearOrder β] [SecondCountableTopology α] (t : Set β) (f : β → α),
  {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, y < x → z ≤ f y}.Countable
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.faithfulSMul : ∀ {M' : Type u_4} {α : Type u_5} [inst : MulOneClass M'] [inst_1 : SMul M' α] {S : Submonoid M'} [FaithfulSMul M' α],
  FaithfulSMul (↥S) α
-- Lean.Meta.Structure
Lean.Meta.StructProjDecl.ref : Lean.Meta.StructProjDecl → Lean.Syntax
-- Mathlib.Data.PNat.Prime
PNat.Prime.not_dvd_one : ∀ {p : ℕ+}, p.Prime → ¬p ∣ 1
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.pi_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_7}
  {ι' : Type u_10} {N : ι' → Type u_11} [inst_3 : (i : ι') → AddCommMonoid (N i)] [inst_4 : (i : ι') → Module R (N i)]
  (f : (i : ι') → M [⋀^ι]→ₗ[R] N i) (m : (i : ι) → (fun x => M) i) (i : ι'), (AlternatingMap.pi f) m i = (f i) m
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.insertEntry : {α : Type u} → {β : α → Type v} → [BEq α] → (k : α) → β k → List ((a : α) × β a) → List ((a : α) × β a)
-- Mathlib.RingTheory.LaurentSeries
RatFunc.coe_coe : ∀ {F : Type u} [inst : Field F] (P : Polynomial F),
  (HahnSeries.ofPowerSeries ℤ F) ↑P = (algebraMap (RatFunc F) (LaurentSeries F)) ↑P
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsKolmogorovProcess.mk : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {X : T → Ω → E} {P : MeasureTheory.Measure Ω} {p q : ℝ} {M : NNReal},
  (∀ (s t : T), Measurable fun ω => (X s ω, X t ω)) →
    (∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ ↑M * edist s t ^ q) →
      0 < p → 0 < q → ProbabilityTheory.IsKolmogorovProcess X P p q M
-- Mathlib.RingTheory.Coprime.Lemmas
IsCoprime.prod_right : ∀ {R : Type u} {I : Type v} [inst : CommSemiring R] {x : R} {s : I → R} {t : Finset I},
  (∀ i ∈ t, IsCoprime x (s i)) → IsCoprime x (∏ i ∈ t, s i)
-- Mathlib.Algebra.Polynomial.Basic
/-- Prefer putting constants to the left of `X`.

This lemma is the loop-avoiding `simp` version of `Polynomial.X_mul`.  -/
Polynomial.X_mul_C : ∀ {R : Type u} [inst : Semiring R] (r : R), Polynomial.X * Polynomial.C r = Polynomial.C r * Polynomial.X
-- Mathlib.Order.Disjoint
IsCompl.dual : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {x y : α},
  IsCompl x y → IsCompl (OrderDual.toDual x) (OrderDual.toDual y)
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.support_zero : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)], DFinsupp.support 0 = ∅
-- Mathlib.Algebra.Group.Units.Basic
eq_one_of_mul_left' : ∀ {α : Type u} [inst : CancelMonoid α] [Subsingleton αˣ] {a b : α}, a * b = 1 → b = 1
-- Mathlib.Algebra.Group.Prod
MulEquiv.prodUnique.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Unique N],
  MulEquiv.prodUnique = { toEquiv := Equiv.prodUnique M N, map_mul' := ⋯ }
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.summable_of_one : ∀ {α : Type u_3} {E : Type u_5} [inst : NormedAddCommGroup E] [CompleteSpace E] {x : α → E}, Memℓp x 1 → Summable x