mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Polynomial.Opposites
Polynomial.natDegree_opRingEquiv : ∀ {R : Type u_1} [inst : Semiring R] (p : (Polynomial R)ᵐᵒᵖ),
  ((Polynomial.opRingEquiv R) p).natDegree = (MulOpposite.unop p).natDegree
-- Mathlib.Algebra.Group.Hom.Instances
/-- Evaluation of a `MonoidHom` at a point as a monoid homomorphism. See also `MonoidHom.apply`
for the evaluation of any function at a point.  -/
MonoidHom.eval : {M : Type uM} → {N : Type uN} → [inst : MulOneClass M] → [inst_1 : CommMonoid N] → M →* (M →* N) →* N
-- Init.Data.List.Lemmas
List.filterMap_replicate_of_none : ∀ {α : Type u_1} {β : Type u_2} {a : α} {n : ℕ} {f : α → Option β},
  f a = none → List.filterMap f (List.replicate n a) = []
-- Mathlib.Data.ENNReal.Operations
ENNReal.le_of_add_le_add_right : ∀ {a b c : ENNReal}, a ≠ ⊤ → b + a ≤ c + a → b ≤ c
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_map_div : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield 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] [inst_9 : ContinuousFunctionalCalculus R A p] [ContinuousInv₀ R]
  (f g : R → R) (a : A),
  (∀ x ∈ spectrum R a, g x ≠ 0) →
    autoParam (ContinuousOn f (spectrum R a)) cfc_map_div._auto_1 →
      autoParam (ContinuousOn g (spectrum R a)) cfc_map_div._auto_3 →
        autoParam (p a) cfc_map_div._auto_5 → cfc (fun x => f x / g x) a = cfc f a * Ring.inverse (cfc g a)
-- Lean.Server.ServerTask
Lean.Server.ServerTask.EIO.bindTaskCheap : {α : Type u_1} →
  {ε β : Type} →
    Lean.Server.ServerTask α →
      (α → EIO ε (Lean.Server.ServerTask (Except ε β))) → BaseIO (Lean.Server.ServerTask (Except ε β))
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_union_congr_of_subset : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ t₁ t₂ : Set α},
  s₁ ⊆ s₂ → μ s₂ ≤ μ s₁ → t₁ ⊆ t₂ → μ t₂ ≤ μ t₁ → μ (s₁ ∪ t₁) = μ (s₂ ∪ t₂)
-- Init.Data.Array.Find
Array.getElem?_zero_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α}, (Array.filterMap f xs)[0]? = Array.findSome? f xs
-- Init.Data.Order.Ord
/-- A typeclass for functions `α → α → Ordering` which are oriented: flipping the arguments amounts
to applying `Ordering.swap` to the return value.
 -/
Std.OrientedCmp : {α : Type u} → (α → α → Ordering) → Prop
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.UniquePartitionZero : Unique (Nat.Partition 0)
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_le_map_of_inv_on : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  {G : Type u_2} [inst_3 : FunLike G S R] [inst_4 : RingHomClass F R S] (g : G) (I : Ideal S),
  Set.LeftInvOn (⇑g) (⇑f) (⇑f ⁻¹' ↑I) → Ideal.comap f I ≤ Ideal.map g I
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isSome_max?_of_isSome_max?_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.erase k).max?.isSome = true → t.max?.isSome = true
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.toSubgraph.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, SimpleGraph.Walk.nil.toSubgraph = G.singletonSubgraph u
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.var.injEq : ∀ (fvarId fvarId_1 : Lean.FVarId),
  (Lean.Meta.Match.Pattern.var fvarId = Lean.Meta.Match.Pattern.var fvarId_1) = (fvarId = fvarId_1)
-- Mathlib.Data.List.Basic
_private.Mathlib.Data.List.Basic.0.List.getLast?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
/-- The negation of a nonsingular Jacobian point on a Weierstrass curve `W`.

Given a nonsingular Jacobian point `P` on `W`, use `-P` instead of `neg P`.  -/
WeierstrassCurve.Jacobian.Point.neg : {F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Jacobian F} → W.Point → W.Point
-- Mathlib.Algebra.Ring.Divisibility.Basic
/-- An element `a` divides the difference `a - b` if and only if `a` divides `b`.  -/
dvd_sub_self_left : ∀ {α : Type u_1} [inst : Ring α] {a b : α}, a ∣ a - b ↔ a ∣ b
-- Mathlib.Algebra.Category.Ring.Adjunctions
/-- The adjunction `G ↦ R[G]` and `S ↦ Sˣ` between `CommGrpCat` and `R-Alg`.  -/
CommRingCat.monoidAlgebraAdj : (R : CommRingCat) →
  R.monoidAlgebra ⊣ (CategoryTheory.Under.forget R).comp (CategoryTheory.forget₂ CommRingCat CommMonCat)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.instEpiDescι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasCoproduct F.obj],
  CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.colimit.ι F))
-- Init.Data.UInt.Basic
instLTUInt64 : LT UInt64
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.forget₂CreatesLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections],
  CommMonCat.forget₂CreatesLimit F =
    CategoryTheory.createsLimitOfReflectsIso fun c' t =>
      {
        liftedCone :=
          {
            pt :=
              CommMonCat.of
                (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget CommMonCat))).pt,
            π :=
              {
                app := fun j =>
                  CommMonCat.ofHom (MonCat.limitπMonoidHom (F.comp (CategoryTheory.forget₂ CommMonCat MonCat)) j),
                naturality := ⋯ } },
        validLift :=
          (MonCat.HasLimits.limitConeIsLimit (F.comp (CategoryTheory.forget₂ CommMonCat MonCat))).uniqueUpToIso t,
        makesLimit :=
          CategoryTheory.Limits.IsLimit.ofFaithful (CategoryTheory.forget₂ CommMonCat MonCat)
            (MonCat.HasLimits.limitConeIsLimit (F.comp (CategoryTheory.forget₂ CommMonCat MonCat)))
            (fun x =>
              {
                hom' :=
                  {
                    toFun := fun v =>
                      EquivLike.coe
                        (equivShrink
                          ↑((F.comp (CategoryTheory.forget₂ CommMonCat MonCat)).comp
                                (CategoryTheory.forget MonCat)).sections)
                        ⟨fun j =>
                          (CategoryTheory.ConcreteCategory.hom
                              (((CategoryTheory.forget MonCat).mapCone
                                      ((CategoryTheory.forget₂ CommMonCat MonCat).mapCone x)).π.app
                                j))
                            v,
                          ⋯⟩,
                    map_one' := ⋯, map_mul' := ⋯ } })
            ⋯ }
-- Mathlib.RingTheory.Flat.Equalizer
/-- If `T` is `R`-flat, the canonical map
`T ⊗[R] eq(f, g) →ₐ[S] eq (𝟙 ⊗ f, 𝟙 ⊗ g)` is an isomorphism.  -/
AlgHom.tensorEqualizerEquiv : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (T : Type u_3) →
            [inst_3 : CommRing T] →
              [inst_4 : Algebra R T] →
                [inst_5 : Algebra S T] →
                  [inst_6 : IsScalarTower R S T] →
                    {A : Type u_4} →
                      {B : Type u_5} →
                        [inst_7 : CommRing A] →
                          [inst_8 : CommRing B] →
                            [inst_9 : Algebra R A] →
                              [inst_10 : Algebra R B] →
                                (f g : A →ₐ[R] B) →
                                  [Module.Flat R T] →
                                    TensorProduct R T ↥(f.equalizer g) ≃ₐ[S]
                                      ↥((Algebra.TensorProduct.map (AlgHom.id S T) f).equalizer
                                          (Algebra.TensorProduct.map (AlgHom.id S T) g))
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkInductiveAux₂.congr_simp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero zero_1 : P.X 0 ⟶ Q.X 1) (e_zero : zero = zero_1)
  (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0)) (one one_1 : P.X 1 ⟶ Q.X 2)
  (e_one : one = one_1)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1))
  (succ succ_1 :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X (n + 1)) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f +
                  CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst +
              CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))),
  succ = succ_1 →
    ∀ (n : ℕ),
      Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ n =
        Homotopy.mkInductiveAux₂ e zero_1 ⋯ one_1 ⋯ succ_1 n
-- Mathlib.Topology.Homotopy.Lifting
/-- The monodromy action of a quotient covering map commutes with the group action.  -/
IsQuotientCoveringMap.monodromy_toPermFiber : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hp : IsQuotientCoveringMap p G) {g : G} {x y : X}
  {γ : Path.Homotopic.Quotient x y} {e : ↑(p ⁻¹' {x})},
  ⋯.monodromy γ (((hp.toPermFiber x) g) e) = ((hp.toPermFiber y) g) (⋯.monodromy γ e)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_pi_div_two : Complex.sin (↑Real.pi / 2) = 1
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_two_pow_add_eq : ∀ (x i : ℕ), (2 ^ i + x).testBit i = !x.testBit i
-- Mathlib.Order.Category.BddOrd
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
BddOrd.Hom.Simps.hom : (X Y : BddOrd) → X.Hom Y → BoundedOrderHom ↑X.toPartOrd ↑Y.toPartOrd
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- Any category with finite coproducts and coequalizers has all finite colimits.  -/
CategoryTheory.Limits.hasFiniteColimits_of_hasCoequalizers_and_finite_coproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteCoproducts C]
  [CategoryTheory.Limits.HasCoequalizers C], CategoryTheory.Limits.HasFiniteColimits C
-- Mathlib.Algebra.Quandle
Rack.instDivInvMonoidEnvelGroup : (R : Type u_1) → [inst : Rack R] → DivInvMonoid (Rack.EnvelGroup R)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `(f ◁ η) ◫ θ`  -/
Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp.mkEvalHorizontalCompAux'Whisker : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp m] →
    Mathlib.Tactic.BicategoryLike.Atom₁ →
      Mathlib.Tactic.BicategoryLike.WhiskerLeft →
        Mathlib.Tactic.BicategoryLike.WhiskerLeft →
          Mathlib.Tactic.BicategoryLike.NormalExpr →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr →
                Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.comp.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {P : Type u_3} [inst_2 : Monoid P] {φ : M →* N}
  {ψ : N →* P} {χ : M →* P} {A : Type u_4} [inst_3 : Monoid A] [inst_4 : MulDistribMulAction M A] {B : Type u_5}
  [inst_5 : Monoid B] [inst_6 : MulDistribMulAction N B] {C : Type u_7} [inst_7 : Monoid C]
  [inst_8 : MulDistribMulAction P C] [κ : φ.CompTriple ψ χ] (g : B →ₑ*[ψ] C) (f : A →ₑ*[φ] B),
  g.comp f = { toMulActionHom := (↑g).comp ↑f, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.Convex.Between
sbtw_mul_sub_add_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [IsDomain R] {x y r : R},
  Sbtw R x (r * (y - x) + x) y ↔ x ≠ y ∧ r ∈ Set.Ioo 0 1
-- Mathlib.Analysis.Analytic.Constructions
/-- Finite products of analytic functions are analytic  -/
Finset.analyticOn_fun_prod : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_9} [inst_3 : NormedCommRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : α → E → A}
  {s : Set E} (N : Finset α), (∀ n ∈ N, AnalyticOn 𝕜 (f n) s) → AnalyticOn 𝕜 (fun z => ∏ n ∈ N, f n z) s
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.instDiscrete_unitLattice : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], DiscreteTopology ↥(NumberField.Units.unitLattice K)
-- Init.Data.SInt.Lemmas
Int32.not_lt : ∀ {a b : Int32}, ¬a < b ↔ b ≤ a
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.mapFunctor_map : ∀ (T : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y),
  (CategoryTheory.Over.mapFunctor T).map f = (CategoryTheory.Over.map f).toCatHom
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.mk : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] →
          [inst_3 : Star A] →
            (toNonUnitalSubalgebra : NonUnitalSubalgebra R A) →
              (∀ {a : A}, a ∈ toNonUnitalSubalgebra.carrier → star a ∈ toNonUnitalSubalgebra.carrier) →
                NonUnitalStarSubalgebra R A
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.eraseMax.match_1.eq_2 : ∀ {α : Type u_1} (motive : Ordnode α → Sort u_2) (size : ℕ) (l : Ordnode α) (x : α) (h_1 : Unit → motive Ordnode.nil)
  (h_2 : (size : ℕ) → (l : Ordnode α) → (x : α) → motive (Ordnode.node size l x Ordnode.nil))
  (h_3 :
    (size : ℕ) →
      (l : Ordnode α) →
        (x : α) →
          (sz : ℕ) →
            (l' : Ordnode α) → (y : α) → (r' : Ordnode α) → motive (Ordnode.node size l x (Ordnode.node sz l' y r'))),
  (match Ordnode.node size l x Ordnode.nil with
    | Ordnode.nil => h_1 ()
    | Ordnode.node size l x Ordnode.nil => h_2 size l x
    | Ordnode.node size l x (Ordnode.node sz l' y r') => h_3 size l x sz l' y r') =
    h_2 size l x
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- **Alias** of the forward direction of `MulAction.isBlock_iff_smul_eq_of_mem`. -/
MulAction.IsBlock.smul_eq_of_mem : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X},
  MulAction.IsBlock G B → ∀ ⦃g : G⦄ ⦃a : X⦄, a ∈ B → g • a ∈ B → g • B = B
-- Mathlib.Order.CompleteLattice.Basic
/-- When taking the supremum of `f : ι → α`, the elements of `ι` on which `f` gives `⊥` can be
dropped, without changing the result.  -/
iSup_ne_bot_subtype : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (f : ι → α), ⨆ i, f ↑i = ⨆ i, f i
-- Mathlib.Algebra.Polynomial.HasseDeriv
Polynomial.hasseDeriv_monomial : ∀ {R : Type u_1} [inst : Semiring R] (k n : ℕ) (r : R),
  (Polynomial.hasseDeriv k) ((Polynomial.monomial n) r) = (Polynomial.monomial (n - k)) (↑(n.choose k) * r)
-- Mathlib.Order.Defs.Prop
/-- Propositions form a complete Boolean algebra, where the `≤` relation is given by implication.  -/
Prop.le : LE Prop
-- Lean.Util.Diff
/-- Computes an edit script to transform `left` into `right`.
 -/
Lean.Diff.diff : {α : Type} → [BEq α] → [Hashable α] → [Inhabited α] → Array α → Array α → Array (Lean.Diff.Action × α)
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.convs'Aux_succ_none : ∀ {K : Type u_1} [inst : DivisionRing K] {s : Stream'.Seq (GenContFract.Pair K)},
  s.head = none → ∀ (n : ℕ), GenContFract.convs'Aux s (n + 1) = 0
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- Given a row partitioned matrix extract the second row  -/
Matrix.toRows₂ : {R : Type u_1} → {m₁ : Type u_3} → {m₂ : Type u_4} → {n : Type u_5} → Matrix (m₁ ⊕ m₂) n R → Matrix m₂ n R
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.instCoeOut : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → CoeOut (CategoryTheory.Subobject X) C
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.instIsFilteredTotalOfIsFinitelyPresentableObjDiag : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {I : J → Type w}
  [inst_1 : CategoryTheory.SmallCategory J] [inst_2 : (j : J) → CategoryTheory.SmallCategory (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  [CategoryTheory.IsFiltered J] [∀ (j : J), CategoryTheory.IsFiltered (I j)]
  [∀ (j : J) (i : I j), CategoryTheory.IsFinitelyPresentable ((P j).diag.obj i)],
  CategoryTheory.IsFiltered (CategoryTheory.Limits.ColimitPresentation.Total P)
-- Mathlib.Data.Set.Function
Set.mapsTo_range : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), Set.MapsTo f s (Set.range f)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.comp : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X Y Z : CategoryTheory.FreeMonoidalCategory C} {f f' : X.Hom Y} {g g' : Y.Hom Z}
  (a : CategoryTheory.FreeMonoidalCategory.HomEquiv f f') (a_1 : CategoryTheory.FreeMonoidalCategory.HomEquiv g g'),
  CategoryTheory.FreeMonoidalCategory.HomEquiv.below a →
    motive f f' a →
      CategoryTheory.FreeMonoidalCategory.HomEquiv.below a_1 →
        motive g g' a_1 → CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.Smooth.ofLocalizationSpanTarget : RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] => RingHom.Smooth
-- Lean.Meta.Tactic.Split
Lean.Meta.Split.simpMatchTarget : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Order.Interval.Basic
NonemptyInterval.coe_sup_interval : ∀ {α : Type u_1} [inst : Lattice α] (s t : NonemptyInterval α), ↑(s ⊔ t) = ↑s ⊔ ↑t
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_insertEntryIfNew_le_self : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k} {fallback : α},
      (compare (Std.Internal.List.minKeyD (Std.Internal.List.insertEntryIfNew k v l) fallback) k).isLE = true
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_toENat_eq_self : ∀ {a : Cardinal.{u_1}}, ↑(Cardinal.toENat a) = a ↔ a ≤ Cardinal.aleph0
-- Mathlib.Algebra.Order.Group.DenselyOrdered
mul_le_of_forall_lt : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : LinearOrder α] [MulLeftMono α] [DenselyOrdered α] {a b c : α},
  (∀ a' < a, ∀ b' < b, a' * b' ≤ c) → a * b ≤ c
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.ae_measure_preimage_mul_right_lt_top_of_ne_zero : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] {s : Set G} [MeasurableInv G]
  (μ' ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν']
  [μ'.IsMulLeftInvariant] [ν'.IsMulLeftInvariant], ν' s ≠ 0 → ν' s ≠ ⊤ → ∀ᵐ (x : G) ∂μ', ν' ((fun y => y * x) ⁻¹' s) < ⊤
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.Hom.ι_comp_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} {I : CategoryTheory.InjectiveResolution Z} {Z' : C}
  {I' : CategoryTheory.InjectiveResolution Z'} {f : Z ⟶ Z'} (φ : I.Hom I' f) {Z_1 : CochainComplex C ℕ}
  (h : I'.cocomplex ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp I.ι (CategoryTheory.CategoryStruct.comp φ.hom h) =
    CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) (CategoryTheory.CategoryStruct.comp I'.ι h)
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.getPos : {m : Type → Type} → [Monad m] → [MonadReaderOf Lean.SubExpr m] → m Lean.SubExpr.Pos
-- Init.Data.SInt.Bitwise
Int8.toISize_xor : ∀ (a b : Int8), (a ^^^ b).toISize = a.toISize ^^^ b.toISize
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.instHasHomologyTruncLE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] (i' : ι'), (K.truncLE e).HasHomology i'
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
cfcₙ_real_eq_complex : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [T2Space A]
  [inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] {a : A} (f : ℝ → ℝ),
  autoParam (IsSelfAdjoint a) cfcₙ_real_eq_complex._auto_1 → cfcₙ f a = cfcₙ (fun x => ↑(f x.re)) a
-- Mathlib.InformationTheory.Hamming
Hamming.instModule : {ι : Type u_2} →
  (α : Type u_5) →
    [inst : Semiring α] →
      (β : ι → Type u_4) → [inst_1 : (i : ι) → AddCommMonoid (β i)] → [(i : ι) → Module α (β i)] → Module α (Hamming β)
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.intCast : ∀ {R : Type u_1} [inst : CommRing R] {a b : ℤ}, IsCoprime a b → IsCoprime ↑a ↑b
-- Init.Data.Vector.Lemmas
Vector.map_mk : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Array α} (h : xs.size = n),
  Vector.map f (Vector.mk xs h) = Vector.mk (Array.map f xs) ⋯
-- Lean.DocString.Types
Lean.Doc.instBEqPart : {i : Type u_1} → {b : Type u_2} → {p : Type u_3} → [BEq i] → [BEq b] → [BEq p] → BEq (Lean.Doc.Part i b p)
-- Mathlib.Data.PEquiv
PEquiv.refl_apply : ∀ {α : Type u} (a : α), (PEquiv.refl α) a = some a
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If `s` is a colimit binary cofan over `X` and `Y`, then every pair of morphisms `f : X ⟶ W` and
`g : Y ⟶ W` induces a morphism `l : s.pt ⟶ W` satisfying `s.inl ≫ l = f` and `s.inr ≫ l = g`.
 -/
CategoryTheory.Limits.BinaryCofan.IsColimit.desc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y W : C} →
      {s : CategoryTheory.Limits.BinaryCofan X Y} → CategoryTheory.Limits.IsColimit s → (X ⟶ W) → (Y ⟶ W) → (s.pt ⟶ W)
-- Lean.Parser.Syntax
Lean.Parser.Command.elabArg.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.coweightEquiv_mul : ∀ {ι : 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} (x y : P.Equiv P),
  RootPairing.Equiv.coweightEquiv P P x * RootPairing.Equiv.coweightEquiv P P y =
    RootPairing.Equiv.coweightEquiv P P y ≪≫ₗ RootPairing.Equiv.coweightEquiv P P x
-- Mathlib.Analysis.Complex.Trigonometric
_private.Mathlib.Analysis.Complex.Trigonometric.0.Complex.cosh_add_aux : ∀ {a b c d : ℂ}, (a + b) * (c + d) + (a - b) * (c - d) = 2 * (a * c + b * d)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Notation for `actionHomLeft`, the action of `C` on morphisms in `D`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.«term_⊵ₗ_» : Lean.TrailingParserDescr
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile.mk.sizeOf_spec : ∀ (uri : Lean.Lsp.DocumentUri) (options? : Option Lean.Lsp.DeleteFile.Options) (annotationId? : Option String),
  sizeOf { uri := uri, options? := options?, annotationId? := annotationId? } =
    1 + sizeOf uri + sizeOf options? + sizeOf annotationId?
-- Init.System.FilePath
System.SearchPath : Type