mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Async.System
Std.Async.System.instReprSystemUser.repr : Std.Async.System.SystemUser → ℕ → Std.Format
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSignatureHelpContext.toJson : Lean.Lsp.SignatureHelpContext → Lean.Json
-- Mathlib.Order.RelClasses
/-- All values are accessible under the well-founded `>`.  -/
WellFoundedGT.apply : ∀ {α : Type u} [inst : LT α] [WellFoundedGT α] (a : α), Acc (fun x1 x2 => x2 < x1) a
-- Mathlib.Data.Finset.Card
Finset.card_le_one : ∀ {α : Type u_1} {s : Finset α}, s.card ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addXYZ_of_X_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → W.addXYZ P Q = WeierstrassCurve.Jacobian.addU P Q • ![1, 1, 0]
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.instInfSet : {Ω : Type u_1} → {ι : Type u_2} → {m : MeasurableSpace Ω} → [inst : Preorder ι] → InfSet (MeasureTheory.Filtration ι m)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- The quotient `q` in Weierstrass division, denoted by `f /ʷ g`. Note that when the image of
`g` in the residue field is zero, this is defined to be zero.  -/
PowerSeries.weierstrassDiv : {A : Type u_1} →
  [inst : CommRing A] →
    [inst_1 : IsLocalRing A] →
      PowerSeries A → PowerSeries A → [IsPrecomplete (IsLocalRing.maximalIdeal A) A] → PowerSeries A
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
ContMDiff.coordChange : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6}
  [inst : NontriviallyNormedField 𝕜] {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB]
  {HB : Type u_8} [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] {EM : Type u_9} [inst_6 : NormedAddCommGroup EM] [inst_7 : NormedSpace 𝕜 EM]
  {HM : Type u_10} [inst_8 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace HM M] [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)]
  [inst_13 : NormedAddCommGroup F] [inst_14 : NormedSpace 𝕜 F] [inst_15 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_16 : (x : B) → TopologicalSpace (E x)] [inst_17 : FiberBundle F E] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e]
  [MemTrivializationAtlas e'] {f : M → B} {g : M → F},
  ContMDiff IM IB n f →
    ContMDiff IM (modelWithCornersSelf 𝕜 F) n g →
      (∀ (x : M), f x ∈ e.baseSet) →
        (∀ (x : M), f x ∈ e'.baseSet) → ContMDiff IM (modelWithCornersSelf 𝕜 F) n fun y => e.coordChange e' (f y) (g y)
-- Mathlib.RingTheory.IsTensorProduct
/-- Given an `R`-algebra `S` and an `R`-module `M`, an `S`-module `N` together with a map
`f : M →ₗ[R] N` is the base change of `M` to `S` if the map `S × M → N, (s, m) ↦ s • f m` is the
tensor product.  -/
IsBaseChange : {R : Type u_1} →
  {M : Type v₁} →
    {N : Type v₂} →
      (S : Type v₃) →
        [inst : AddCommMonoid M] →
          [inst_1 : AddCommMonoid N] →
            [inst_2 : CommSemiring R] →
              [inst_3 : CommSemiring S] →
                [inst_4 : Algebra R S] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] → [inst_7 : Module S N] → [IsScalarTower R S N] → (M →ₗ[R] N) → Prop
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.smul_apply : ∀ {𝕜 : Type u} {𝕜' : Type u'} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F]
  [inst_10 : ContinuousConstSMul 𝕜 F] [inst_11 : Semiring 𝕜'] [inst_12 : Module 𝕜' F]
  [inst_13 : ContinuousConstSMul 𝕜' F] [inst_14 : SMulCommClass 𝕜 𝕜' F] (f : FormalMultilinearSeries 𝕜 E F) (n : ℕ)
  (a : 𝕜'), (a • f) n = a • f n
-- Init.Omega.IntList
/-- The difference between the balanced mod of a dot product,
and the dot product with balanced mod applied to each entry of the left factor.
 -/
Lean.Omega.IntList.bmod_dot_sub_dot_bmod : ℕ → Lean.Omega.IntList → Lean.Omega.IntList → ℤ
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.inl_toNormalization_normalizationCoprodIso_inv : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U V : AlgebraicGeometry.Scheme} {iU : U ⟶ X} {iV : V ⟶ X}
  (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV))
  [inst_2 : AlgebraicGeometry.QuasiCompact iU] [inst_3 : AlgebraicGeometry.QuasiSeparated iU]
  [inst_4 : AlgebraicGeometry.QuasiCompact iV] [inst_5 : AlgebraicGeometry.QuasiSeparated iV],
  CategoryTheory.CategoryStruct.comp iU
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f)
        (AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso f e).inv) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.CategoryStruct.comp iU f))
      CategoryTheory.Limits.coprod.inl
-- Mathlib.Algebra.Group.TypeTags.Basic
/-- If `α` has some additive structure and coerces to a function,
then `Multiplicative α` should also coerce to the same function.

This allows `Multiplicative` to be used on bundled function types with an additive structure, which
is often used for composition, without affecting the behavior of the function itself.
 -/
Multiplicative.coeToFun : {α : Type u_1} → {β : α → Sort u_2} → [CoeFun α β] → CoeFun (Multiplicative α) fun a => β (Multiplicative.toAdd a)
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.toSubtype'.match_1.eq_2 : ∀
  (motive :
    (n : ℕ) →
      (α : TypeVec.{u_1} n) →
        (p : (α.prod α).Arrow (TypeVec.repeat n Prop)) →
          (x : Fin2 n) → { x_1 // TypeVec.ofRepeat (p x (TypeVec.prod.mk x x_1.1 x_1.2)) } → Sort u_2)
  (n : ℕ) (α : TypeVec.{u_1} (n + 1)) (p : (α.prod α).Arrow (TypeVec.repeat (n + 1) Prop))
  (x : { x // TypeVec.ofRepeat (p Fin2.fz (TypeVec.prod.mk Fin2.fz x.1 x.2)) })
  (h_1 :
    (n : ℕ) →
      (α : TypeVec.{u_1} (n + 1)) →
        (p : (α.prod α).Arrow (TypeVec.repeat (n + 1) Prop)) →
          (i : Fin2 n) →
            (x : { x // TypeVec.ofRepeat (p i.fs (TypeVec.prod.mk i.fs x.1 x.2)) }) → motive (n + 1) α p i.fs x)
  (h_2 :
    (n : ℕ) →
      (α : TypeVec.{u_1} (n + 1)) →
        (p : (α.prod α).Arrow (TypeVec.repeat (n + 1) Prop)) →
          (x : { x // TypeVec.ofRepeat (p Fin2.fz (TypeVec.prod.mk Fin2.fz x.1 x.2)) }) → motive (n + 1) α p Fin2.fz x),
  (match n + 1, α, p, Fin2.fz, x with
    | .(n + 1), α, p, i.fs, x => h_1 n α p i x
    | .(n + 1), α, p, Fin2.fz, x => h_2 n α p x) =
    h_2 n α p x
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.of_bound : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {s : Set α}
  {μ : MeasureTheory.Measure α},
  μ s < ⊤ →
    ∀ {f : α → E},
      MeasureTheory.AEStronglyMeasurable f (μ.restrict s) →
        ∀ (C : ℝ), (∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ C) → MeasureTheory.IntegrableOn f s μ
-- Mathlib.Data.Nat.SuccPred
Nat.succ_eq_succ : Order.succ = Nat.succ
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ioo_pred_left_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [NoMinOrder α] (a b : α),
  Set.Ioo (Order.pred a) b = Set.Ico a b
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.nhdsNE_infty_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  nhdsWithin OnePoint.infty {OnePoint.infty}ᶜ = Filter.map OnePoint.some (Filter.coclosedCompact X)
-- Mathlib.RingTheory.Norm.Transitivity
Algebra.Norm.Transitivity.cornerAddX.congr_simp : ∀ {S : Type u_2} {m : Type u_5} [inst : CommRing S] (M M_1 : Matrix m m S),
  M = M_1 →
    ∀ {inst_1 : DecidableEq m} [inst_2 : DecidableEq m] (k k_1 : m),
      k = k_1 →
        ∀ (a a_1 : m),
          a = a_1 →
            ∀ (a_2 a_3 : m),
              a_2 = a_3 →
                Algebra.Norm.Transitivity.cornerAddX M k a a_2 = Algebra.Norm.Transitivity.cornerAddX M_1 k_1 a_1 a_3
-- Mathlib.Topology.Algebra.Monoid
Continuous.fun_nsmul : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : AddMonoid M]
  [ContinuousAdd M] {f : X → M}, Continuous f → ∀ (n : ℕ), Continuous fun i => n • f i
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {fallback : β k},
  Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.union m₂ ⋯ ⋯).getD k fallback = m₂.getD k fallback
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin.fst.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (a : α) (i : Fin (k + 1)),
  Finset.intervalGapsWithin.fst F h a i = if hi : i = 0 then a else ((F.orderEmbOfFin h) (i.pred hi)).2
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instIsUniformAddGroup : ∀ {A : Type u_3} {E : Type u_4} [inst : AddCommGroup E] [inst_1 : UniformSpace E] [IsUniformAddGroup E],
  IsUniformAddGroup (WithCStarModule A E)
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentationProps.mk.injEq : ∀ (expr expr_1 : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx),
  ({ expr := expr } = { expr := expr_1 }) = (expr = expr_1)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.lintegral_smul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {R : Type u_5} [inst : SMul R ENNReal]
  [inst_1 : IsScalarTower R ENNReal ENNReal] (f : MeasureTheory.SimpleFunc α ENNReal) (c : R),
  f.lintegral (c • μ) = c • f.lintegral μ
-- Init.Data.UInt.Lemmas
UInt8.ofNatLT.congr_simp : ∀ (n n_1 : ℕ) (e_n : n = n_1) (h : n < UInt8.size), UInt8.ofNatLT n h = UInt8.ofNatLT n_1 ⋯
-- Mathlib.LinearAlgebra.Charpoly.BaseChange
LinearMap.det_baseChange : ∀ {R : Type u_3} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M] (f : M →ₗ[R] M) {A : Type u_1} [inst_5 : CommRing A] [inst_6 : Algebra R A],
  LinearMap.det (LinearMap.baseChange A f) = (algebraMap R A) (LinearMap.det f)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.forIn_mapM : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {n : Type w → Type w''} {o : Type w → Type u_1} {β₂ : Type w}
  [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [LawfulMonad o] [inst_5 : MonadAttach n]
  [WeaklyLawfulMonadAttach n] [inst_7 : MonadLiftT n o] [LawfulMonadLiftT n o] [Std.Iterators.Finite α Id]
  [inst_10 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o] {it : Std.Iter β} {f : β → n β₂} {init : γ}
  {g : β₂ → γ → o (ForInStep γ)},
  forIn (Std.Iter.mapM f it) init g =
    forIn it init fun out acc => do
      let __do_lift ← liftM (f out)
      g __do_lift acc
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.truncate.eq_1 : ∀ {F : PFunctor.{uA, uB}} (a : F.A) (a_1 : F.B a → PFunctor.Approx.CofixA F 0),
  PFunctor.Approx.truncate (PFunctor.Approx.CofixA.intro a a_1) = PFunctor.Approx.CofixA.continue
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.Gate.xor.sizeOf_spec : sizeOf Std.Tactic.BVDecide.Gate.xor = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_filterMap! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α},
  t.WF →
    Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filterMap! f t) =
      Option.any (fun x => (f k x).isSome) (t.get? k)
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.cast_toNat : ∀ {a : ℤ}, a ≥ 0 → ↑a.toNat = a
-- Mathlib.GroupTheory.EckmannHilton
EckmannHilton.IsUnital.mk : ∀ {X : Type u} {m : X → X → X} {e : X}, Std.LawfulIdentity m e → EckmannHilton.IsUnital m e
-- Mathlib.Data.TypeVec
TypeVec.drop_append1' : ∀ {n : ℕ} {α : TypeVec.{u_1} n} {β : Type u_1}, (α ::: β).drop = α
-- Mathlib.Algebra.Homology.Embedding.Restriction
HomologicalComplex.restrictionMap_f : ∀ {ι : 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 L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsRelIff] (i : ι),
  (HomologicalComplex.restrictionMap φ e).f i = φ.f (e.f i)
-- Mathlib.Order.TransfiniteIteration
SuccOrder.limitRecOn.congr_simp : ∀ {α : Type u_1} (b : α) {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : SuccOrder α]
  [inst_2 : WellFoundedLT α] (isMin isMin_1 : (a : α) → IsMin a → motive a),
  isMin = isMin_1 →
    ∀ (succ succ_1 : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)),
      succ = succ_1 →
        ∀ (isSuccLimit isSuccLimit_1 : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a),
          isSuccLimit = isSuccLimit_1 →
            SuccOrder.limitRecOn b isMin succ isSuccLimit = SuccOrder.limitRecOn b isMin_1 succ_1 isSuccLimit_1
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.restrict_nonzero_iff : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω), μ.restrict A ≠ 0 ↔ μ A ≠ 0
-- Mathlib.Algebra.Group.Opposite
Commute.unop : ∀ {α : Type u_1} [inst : Mul α] {x y : αᵐᵒᵖ}, Commute x y → Commute (MulOpposite.unop x) (MulOpposite.unop y)
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- The isomorphism `f⁺ (g ≫ h) ≅ f⁺ g ≫ h` at the level of structured arrows.  -/
CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : a ⟶ b) →
        (g : a ⟶ c) →
          [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] →
            {x : B} →
              (h : c ⟶ x) →
                [inst_2 : CategoryTheory.Bicategory.Lan.CommuteWith f g h] →
                  CategoryTheory.Bicategory.lanLeftExtension f (CategoryTheory.CategoryStruct.comp g h) ≅
                    (CategoryTheory.Bicategory.lanLeftExtension f g).whisker h
-- Mathlib.Analysis.LocallyConvex.Montel
MontelSpace.mk : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : SeminormedRing 𝕜] [inst_1 : Zero E] [inst_2 : SMul 𝕜 E]
  [inst_3 : TopologicalSpace E],
  (∀ (s : Set E), IsClosed s → Bornology.IsVonNBounded 𝕜 s → IsCompact s) → MontelSpace 𝕜 E
-- Mathlib.RingTheory.Ideal.Span
Ideal.mem_span : ∀ {α : Type u} [inst : Semiring α] {s : Set α} (x : α), x ∈ Ideal.span s ↔ ∀ (p : Ideal α), s ⊆ ↑p → x ∈ p
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen.eq_1 : Ordinal.veblen = Ordinal.veblenWith fun x => Ordinal.omega0 ^ x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.map_fst_toArray_eq_keysArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α], Array.map Prod.fst (Std.DHashMap.Raw.Const.toArray ↑m) = (↑m).keysArray
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
IsSemisimpleRing.moduleEnd : ∀ (R : Type u) [inst : Ring R] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  [Module.Finite R M], IsSemisimpleRing (Module.End R M)
-- Mathlib.Algebra.Order.IsBotOne
one_le : ∀ {α : Type u_1} [inst : LE α] [inst_1 : One α] [IsBotOneClass α] {a : α}, 1 ≤ a
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.enriched_comp_id_assoc : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₂] {Z : V}
  (h : CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor
          (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂)
          (CategoryTheory.Enriched.FunctorCategory.enrichedId V F₂))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₂ F₂) h)) =
    h
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_mono : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} ⦃f g : α → ENNReal⦄,
  f ≤ g → ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ
-- Mathlib.Logic.Relation
Relation.TransGen.tail'_iff : ∀ {α : Type u_1} {r : α → α → Prop} {a c : α}, Relation.TransGen r a c ↔ ∃ b, Relation.ReflTransGen r a b ∧ r b c
-- Mathlib.CategoryTheory.Category.TwoP
/-- The category of two-pointed types.  -/
TwoP : Type (u + 1)
-- Mathlib.LinearAlgebra.Dimension.Free
/-- The rank of a free module `M` over an infinite scalar ring `R` is the cardinality of `M`
whenever `#R < #M`.  -/
Module.Free.rank_eq_mk_of_infinite_lt : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [StrongRankCondition R] [Infinite R],
  Cardinal.lift.{v, u} (Cardinal.mk R) < Cardinal.lift.{u, v} (Cardinal.mk M) → Module.rank R M = Cardinal.mk M
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atom_even : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) (a b : ℤ), IsEllipticNet.atom W (2 * a) (2 * b) = W (a + b) * W (a - b)
-- Mathlib.RingTheory.LaurentSeries
PowerSeries.coe_X : ∀ {R : Type u_1} [inst : Semiring R], (HahnSeries.ofPowerSeries ℤ R) PowerSeries.X = (HahnSeries.single 1) 1
-- Init.Data.SInt.Bitwise
Int8.zero_and : ∀ {a : Int8}, 0 &&& a = 0
-- Init.Data.SInt.Bitwise
Int32.not_neg_one : ~~~(-1) = 0
-- Mathlib.Order.UpperLower.Principal
UpperSet.Ioi_eq_top : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, UpperSet.Ioi a = ⊤ ↔ a = ⊤
-- Mathlib.Data.Fintype.EquivFin
not_surjective_finite_infinite : ∀ {α : Sort u_4} {β : Sort u_5} [Finite α] [Infinite β] (f : α → β), ¬Function.Surjective f
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_mul_iff_one_le_left' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LE α] [MulRightMono α] [MulRightReflectLE α] (a : α) {b : α},
  a ≤ b * a ↔ 1 ≤ b
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
DifferentiableOn.continuousAlternatingMap_apply_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {ι : Type u_5} {c : E → F [⋀^ι]→L[𝕜] G}
  [Finite ι], DifferentiableOn 𝕜 c s → ∀ (u : ι → F), DifferentiableOn 𝕜 (fun y => (c y) u) s
-- Mathlib.Data.List.Defs
/-- A variant of `mapIdxM` specialised to applicative actions which
return `Unit`.  -/
List.mapIdxM' : {m : Type v → Type w} → [Monad m] → {α : Type u_7} → (ℕ → α → m PUnit.{v + 1}) → List α → m PUnit.{v + 1}
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.skipSuffixWhile_eq_endPos_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String},
  s.skipSuffixWhile pat = s.endPos ↔ s.endsWith pat = false
-- Mathlib.CategoryTheory.Sites.CartesianMonoidal
CategoryTheory.sheafToPresheaf_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) [inst_2 : CategoryTheory.CartesianMonoidalCategory A],
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.sheafToPresheaf J A) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.sheafToPresheaf J A).obj
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Sheaf J A)))
-- Mathlib.Algebra.Homology.ModelCategory.Injective
CochainComplex.Plus.modelCategoryQuillen.instMonoOfCofibration : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {A B : CochainComplex.Plus C} (i : A ⟶ B) [HomotopicalAlgebra.Cofibration i], CategoryTheory.Mono i
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.imp : ∀ {α : Type u_1} {m : MeasurableSpace α} {p q : α → Prop},
  MeasurableSet {x | p x} → MeasurableSet {x | q x} → MeasurableSet {x | p x → q x}
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.surjective_π_iff_span_eq_top : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (solution : relations.Solution M),
  Function.Surjective ⇑solution.π ↔ Submodule.span A (Set.range solution.var) = ⊤
-- Mathlib.FieldTheory.IsRealClosed.Basic
IsSquare.of_not_isSquare_neg : ∀ {R : Type u} [inst : Field R] [IsRealClosed R] {x : R}, ¬IsSquare (-x) → IsSquare x
-- Mathlib.Data.Set.Monotone
Set.domRestrict.eq_1 : ∀ {α : Type u_1} {π : α → Type u_6} (s : Set α) (f : (a : α) → π a) (x : ↑s), s.domRestrict f x = f ↑x
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.tail_add : ∀ {α : Type u_1} {n : ℕ} [inst : Add α] (a b : Fin n.succ → α),
  Matrix.vecTail (a + b) = Matrix.vecTail a + Matrix.vecTail b
-- Mathlib.Data.Int.Cast.Lemmas
zpowersMulHom_apply : ∀ {α : Type u_3} [inst : CommGroup α] (x : α) (n : Multiplicative ℤ),
  ((zpowersMulHom α) x) n = x ^ Multiplicative.toAdd n
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_vsub_left : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1) (c : k), (AffineMap.lineMap p₀ p₁) c -ᵥ p₀ = c • (p₁ -ᵥ p₀)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_eq_top_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.eRk X = ⊤ ↔ ¬M.IsRkFinite X
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a non-degenerate right-angled triangle is positive.  -/
EuclideanGeometry.angle_pos_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 → p₁ ≠ p₂ ∨ p₃ = p₂ → 0 < EuclideanGeometry.angle p₂ p₃ p₁
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- We say that a 1-morphism `h` commutes with the left Kan extension `f⁺ g` if the whiskered
left extension for `f⁺ g` by `h` is a Kan extension of `g ≫ h` along `f`.  -/
CategoryTheory.Bicategory.Lan.CommuteWith : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : a ⟶ b) → (g : a ⟶ c) → [CategoryTheory.Bicategory.HasLeftKanExtension f g] → {x : B} → (c ⟶ x) → Prop
-- Mathlib.Dynamics.Ergodic.Action.Basic
MeasureTheory.aeconst_of_forall_preimage_smul_ae_eq : ∀ (G : Type u_1) {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : SMul G α]
  [ErgodicSMul G α μ] {s : Set α},
  MeasureTheory.NullMeasurableSet s μ →
    (∀ (g : G), (fun x => g • x) ⁻¹' s =ᵐ[μ] s) → Filter.EventuallyConst s (MeasureTheory.ae μ)