mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- `GRewritePos` contains the ìnformation about a given subexpression position needed for
applying a  `grw` lemma.  -/
Mathlib.Tactic.ClickSuggestions.GrwPos : Type
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.coord_equivFun_symm : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Finite ι] (b : Module.Basis ι R M) (i : ι) (f : ι → R), (b.coord i) (b.equivFun.symm f) = f i
-- Mathlib.Probability.Density
MeasureTheory.pdf.eq_of_map_eq_withDensity : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure ℙ] {X : Ω → E} [MeasureTheory.HasPDF X ℙ μ]
  (f : E → ENNReal),
  AEMeasurable f μ → (MeasureTheory.Measure.map X ℙ = μ.withDensity f ↔ MeasureTheory.pdf X ℙ μ =ᵐ[μ] f)
-- Mathlib.Algebra.Jordan.Basic
/-- A commutative Jordan multiplication  -/
IsCommJordan : (A : Type u_1) → [CommMagma A] → Prop
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opcyclesOpIso_inv_naturality_assoc : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] {Z : Vᵒᵖ} (h : K.op.opcycles i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i).op
      (CategoryTheory.CategoryStruct.comp (K.opcyclesOpIso i).inv h) =
    CategoryTheory.CategoryStruct.comp (L.opcyclesOpIso i).inv
      (CategoryTheory.CategoryStruct.comp
        (HomologicalComplex.opcyclesMap ((HomologicalComplex.opFunctor V c).map φ.op) i) h)
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- Given a formal multilinear series `p` and a vector `x`, then `p.sum x` is the sum `Σ pₙ xⁿ`. A
priori, it only behaves well when `‖x‖ < p.radius`.  -/
FormalMultilinearSeries.sum : {𝕜 : Type u_1} →
  {E : Type u_3} →
    {F : Type u_4} →
      [inst : Semiring 𝕜] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : AddCommMonoid F] →
            [inst_3 : Module 𝕜 E] →
              [inst_4 : Module 𝕜 F] →
                [inst_5 : TopologicalSpace E] →
                  [inst_6 : TopologicalSpace F] →
                    [inst_7 : ContinuousAdd E] →
                      [inst_8 : ContinuousAdd F] →
                        [inst_9 : ContinuousConstSMul 𝕜 E] →
                          [inst_10 : ContinuousConstSMul 𝕜 F] → FormalMultilinearSeries 𝕜 E F → E → F
-- Mathlib.Algebra.Group.Basic
add_add_neg_cancel'_right : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b : G), a + (b + -a) = b
-- Init.Prelude
/-- Catches errors thrown in `body`, passing them to `handler`. Errors in `handler` are not caught.
 -/
MonadExceptOf.tryCatch : {ε : semiOutParam (Type u)} → {m : Type v → Type w} → [self : MonadExceptOf ε m] → {α : Type v} → m α → (ε → m α) → m α
-- Init.Data.UInt.Bitwise
UInt8.toUInt32_or : ∀ (a b : UInt8), (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32
-- Mathlib.Tactic.NormNum.Basic
_private.Mathlib.Tactic.NormNum.Basic.0.Mathlib.Meta.NormNum.Result.add.intArm : {u : Lean.Level} →
  {α : Q(Type u)} →
    {a b : Q(«$α»)} →
      Mathlib.Meta.NormNum.Result q(«$a») →
        Mathlib.Meta.NormNum.Result q(«$b») →
          (inst : Q(Add «$α»)) → Q(Ring «$α») → Lean.MetaM (Mathlib.Meta.NormNum.Result q(«$a» + «$b»))
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.rTensor_refl_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (y : TensorProduct R N M),
  (LinearEquiv.rTensor M (LinearEquiv.refl R N)) y = y
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.isHermitian_reindex_iff : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : Star α] {A : Matrix n n α} (f : n ≃ m),
  ((Matrix.reindex f f) A).IsHermitian ↔ A.IsHermitian
-- Mathlib.Probability.Independence.Integration
ProbabilityTheory.iIndepFun.integral_prod_comp : ∀ {Ω : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_3}
  [inst_1 : Fintype ι] {𝓧 : ι → Type u_4} {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i}
  {f : (i : ι) → 𝓧 i → 𝕜},
  ProbabilityTheory.iIndepFun X μ →
    (∀ (i : ι), AEMeasurable (X i) μ) →
      (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) (MeasureTheory.Measure.map (X i) μ)) →
        ∫ (x : Ω), (∏ i, f i ∘ X i) x ∂μ = ∏ i, ∫ (x : Ω), (f i ∘ X i) x ∂μ
-- Mathlib.MeasureTheory.Function.AEEqOfLIntegral
MeasureTheory.withDensity_eq_iff_of_sigmaFinite : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  {f g : α → ENNReal}, AEMeasurable f μ → AEMeasurable g μ → (μ.withDensity f = μ.withDensity g ↔ f =ᵐ[μ] g)
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- If `f` is a `K`-Lipschitz map, then it increases the Hausdorff `d`-measures of sets at most
by the factor of `K ^ d`.  -/
LipschitzWith.hausdorffMeasure_image_le : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
  [inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] {K : NNReal} {f : X → Y},
  LipschitzWith K f →
    ∀ {d : ℝ},
      0 ≤ d →
        ∀ (s : Set X),
          (MeasureTheory.Measure.hausdorffMeasure d) (f '' s) ≤ ↑K ^ d * (MeasureTheory.Measure.hausdorffMeasure d) s
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.documentation.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenModifier.documentation = 1
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.coroot'In_rootSpanMem_eq_pairingIn : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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) (i j : ι)
  (S : Type u_6) [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : Module S M] [inst_8 : IsScalarTower S R M]
  [inst_9 : FaithfulSMul S R] [inst_10 : P.IsValuedIn S], (P.coroot'In S i) (P.rootSpanMem S j) = P.pairingIn S j i
-- Mathlib.Topology.Constructions
nhds_toDual : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X), nhds (OrderDual.toDual x) = Filter.map (⇑OrderDual.toDual) (nhds x)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- Generalized eigenrange and generalized eigenspace for exponent `finrank K V` are disjoint.  -/
Module.End.generalized_eigenvec_disjoint_range_ker : ∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  (f : Module.End K V) (μ : K),
  Disjoint (f.genEigenrange μ ↑(Module.finrank K V)) ((f.genEigenspace μ) ↑(Module.finrank K V))
-- Init.Data.Option.Lemmas
Option.guard_false : ∀ {α : Type u_1}, (Option.guard fun x => false) = fun x => none
-- Mathlib.RingTheory.MvPowerSeries.LexOrder
MvPowerSeries.coeff_ne_zero_of_lexOrder : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder σ] [inst_2 : WellFoundedGT σ]
  {φ : MvPowerSeries σ R} {d : σ →₀ ℕ}, ↑(toLex d) = φ.lexOrder → (MvPowerSeries.coeff d) φ ≠ 0
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.Homotopy.rel_assoc : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : SSet.RelativeMorphism A B φ}
  (self : f.Homotopy g) {Z : SSet} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight A.ι (SSet.stdSimplex.obj { len := 1 }))
      (CategoryTheory.CategoryStruct.comp self.h h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.fst A.toSSet (SSet.stdSimplex.obj { len := 1 }))
      (CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp B.ι h))
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Function.Injective.hasProd_range_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α}
  {g : γ → β}, Function.Injective g → (HasProd (fun x => f ↑x) a ↔ HasProd (f ∘ g) a)
-- Std.Http.Data.Status
/-- 451 Unavailable For Legal Reasons
 -/
Std.Http.Status.unavailableForLegalReasons : Std.Http.Status
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
/-- If `d : MultispanIndex J C`, `c : Multicofork d` and `F : C ⥤ D`,
the cocone `F.mapCocone c` is colimit iff the multicofork `c.map F` is.  -/
CategoryTheory.Limits.Multicofork.isColimitMapEquiv : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {J : CategoryTheory.Limits.MultispanShape} →
          {d : CategoryTheory.Limits.MultispanIndex J C} →
            (c : CategoryTheory.Limits.Multicofork d) →
              (F : CategoryTheory.Functor C D) →
                CategoryTheory.Limits.IsColimit (F.mapCocone c) ≃ CategoryTheory.Limits.IsColimit (c.map F)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKeyGT!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} [inst : Inhabited α],
          Std.DTreeMap.Internal.Impl.getKeyGT! k t₁ = Std.DTreeMap.Internal.Impl.getKeyGT! k t₂
-- Init.Data.Vector.Lemmas
Vector.mem_or_eq_of_mem_push : ∀ {α : Type u_1} {n : ℕ} {a b : α} {xs : Vector α n}, a ∈ xs.push b → a ∈ xs ∨ a = b
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.liftP_iff' : ∀ {n : ℕ} {P : MvPFunctor.{u} n} {α : TypeVec.{u} n} (p : ⦃i : Fin2 n⦄ → α i → Prop) (a : P.A) (f : (P.B a).Arrow α),
  MvFunctor.LiftP p ⟨a, f⟩ ↔ ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
-- Init.Data.Array.Erase
Array.eraseIdx_append : ∀ {α : Type u_1} {k : ℕ} {xs ys : Array α} (h : k < (xs ++ ys).size),
  (xs ++ ys).eraseIdx k h = if h' : k < xs.size then xs.eraseIdx k h' ++ ys else xs ++ ys.eraseIdx (k - xs.size) ⋯
-- Mathlib.Data.Sum.Interval
Finset.sumLift₂.eq_3 : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  (f : α₁ → β₁ → Finset γ₁) (g : α₂ → β₂ → Finset γ₂) (val : α₂) (val_1 : β₁),
  Finset.sumLift₂ f g (Sum.inr val) (Sum.inl val_1) = ∅
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.tan_sub_int_mul_pi : ∀ (x : ℂ) (n : ℤ), Complex.tan (x - ↑n * ↑Real.pi) = Complex.tan x
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.evaln.match_1.eq_3 : ∀ (motive : ℕ → Nat.Partrec.Code → Sort u_1) (k : ℕ) (h_1 : (x : Nat.Partrec.Code) → motive 0 x)
  (h_2 : (k : ℕ) → motive k.succ Nat.Partrec.Code.zero) (h_3 : (k : ℕ) → motive k.succ Nat.Partrec.Code.succ)
  (h_4 : (k : ℕ) → motive k.succ Nat.Partrec.Code.left) (h_5 : (k : ℕ) → motive k.succ Nat.Partrec.Code.right)
  (h_6 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.pair cg))
  (h_7 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.comp cg))
  (h_8 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.prec cg))
  (h_9 : (k : ℕ) → (cf : Nat.Partrec.Code) → motive k.succ cf.rfind'),
  (match k.succ, Nat.Partrec.Code.succ with
    | 0, x => h_1 x
    | k.succ, Nat.Partrec.Code.zero => h_2 k
    | k.succ, Nat.Partrec.Code.succ => h_3 k
    | k.succ, Nat.Partrec.Code.left => h_4 k
    | k.succ, Nat.Partrec.Code.right => h_5 k
    | k.succ, cf.pair cg => h_6 k cf cg
    | k.succ, cf.comp cg => h_7 k cf cg
    | k.succ, cf.prec cg => h_8 k cf cg
    | k.succ, cf.rfind' => h_9 k cf) =
    h_3 k
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyFaithful.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  (∀ {X Y : C} {f g : X ⟶ Y}, (∀ (i : I), (F i).map f = (F i).map g) → f = g) → CategoryTheory.JointlyFaithful F
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The identity on `X` is an equalizer of `(f, g)`, if `f = g`.  -/
CategoryTheory.Limits.isLimitIdFork : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} → (h : f = g) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.idFork h)
-- Init.Data.Float.Model.Float32
/-- Converts a `Float32.Model` to a `UInt8`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float32.Model.toUInt8 : Float32.Model → UInt8
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- For finite intervals, see: `intervalIntegral.integral_deriv_mul_eq_sub`.  -/
MeasureTheory.integral_deriv_mul_eq_sub : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] {a' b' : A} {u v u' v' : ℝ → A} [CompleteSpace A],
  (∀ x ∈ tsupport v, HasDerivAt u (u' x) x) →
    (∀ x ∈ tsupport u, HasDerivAt v (v' x) x) →
      MeasureTheory.Integrable (u' * v + u * v') MeasureTheory.volume →
        Filter.Tendsto (u * v) Filter.atBot (nhds a') →
          Filter.Tendsto (u * v) Filter.atTop (nhds b') → ∫ (x : ℝ), u' x * v x + u x * v' x = b' - a'
-- Mathlib.Data.Matrix.Basic
Matrix.instFinite : ∀ {n : Type u_14} {m : Type u_15} [Finite m] [Finite n] (α : Type u_16) [Finite α], Finite (Matrix m n α)
-- Init.Data.String.Basic
String.decLE : (s₁ s₂ : String) → Decidable (s₁ ≤ s₂)
-- Mathlib.CategoryTheory.Action.Basic
/-- When a group acts, we can lift the action to the group of automorphisms.  -/
Action.ρAut : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} → [inst_1 : Group G] → (A : Action V G) → G →* CategoryTheory.Aut A.V
-- Mathlib.Algebra.GroupWithZero.InjSurj
/-- Pull back a `MulZeroOneClass` instance along an injective function.
See note [reducible non-instances].  -/
Function.Injective.mulZeroOneClass : {M₀ : Type u_1} →
  {M₀' : Type u_3} →
    [inst : MulZeroOneClass M₀] →
      [inst_1 : Mul M₀'] →
        [inst_2 : Zero M₀'] →
          [inst_3 : One M₀'] →
            (f : M₀' → M₀) →
              Function.Injective f → f 0 = 0 → f 1 = 1 → (∀ (a b : M₀'), f (a * b) = f a * f b) → MulZeroOneClass M₀'
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Convert an `rcases` pattern to an equivalent `intro` argument, if possible.  -/
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.introMergeArgOfRCasesPat? : Lean.TSyntax `rcasesPat → Option Lean.Term
-- Lean.Meta.GeneralizeTelescope
Lean.Meta.GeneralizeTelescope.Entry : Type
-- Mathlib.Topology.Subpath
Path.range_subpath_of_ge : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ : ↑unitInterval),
  t₁ ≤ t₀ → Set.range ⇑(γ.subpath t₀ t₁) = ⇑γ '' Set.Icc t₁ t₀
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_lt : ∀ {r : ENNReal} {n : ℕ∞}, n ≠ 0 → n ≠ ⊤ → (⌈r⌉ₑ < n ↔ r ≤ ↑n - 1)
-- Mathlib.Data.Set.Pairwise.Basic
Set.PairwiseDisjoint.eq_1 : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] (s : Set ι) (f : ι → α),
  s.PairwiseDisjoint f = s.Pairwise (Function.onFun Disjoint f)
-- Init.Grind.AC
Lean.Grind.AC.Seq.sort'.induct_unfolding : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Prop),
  (∀ (acc : Lean.Grind.AC.Seq) (x : Lean.Grind.AC.Var),
      motive (Lean.Grind.AC.Seq.var x) acc (Lean.Grind.AC.Seq.insert x acc)) →
    (∀ (acc : Lean.Grind.AC.Seq) (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
        motive s (Lean.Grind.AC.Seq.insert x acc) (s.sort' (Lean.Grind.AC.Seq.insert x acc)) →
          motive (Lean.Grind.AC.Seq.cons x s) acc (s.sort' (Lean.Grind.AC.Seq.insert x acc))) →
      ∀ (s acc : Lean.Grind.AC.Seq), motive s acc (s.sort' acc)
-- Mathlib.Topology.MetricSpace.Gluing
_private.Mathlib.Topology.MetricSpace.Gluing.0.Metric.glueDist.match_1.eq_4 : ∀ {X : Type u_1} {Y : Type u_2} (motive : X ⊕ Y → X ⊕ Y → Sort u_3) (x : Y) (y : X)
  (h_1 : (x y : X) → motive (Sum.inl x) (Sum.inl y)) (h_2 : (x y : Y) → motive (Sum.inr x) (Sum.inr y))
  (h_3 : (x : X) → (y : Y) → motive (Sum.inl x) (Sum.inr y)) (h_4 : (x : Y) → (y : X) → motive (Sum.inr x) (Sum.inl y)),
  (match Sum.inr x, Sum.inl y with
    | Sum.inl x, Sum.inl y => h_1 x y
    | Sum.inr x, Sum.inr y => h_2 x y
    | Sum.inl x, Sum.inr y => h_3 x y
    | Sum.inr x, Sum.inl y => h_4 x y) =
    h_4 x y
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.cramer_row_self : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
  (b : n → α) (i : n), (∀ (j : n), b j = A j i) → A.cramer b = Pi.single i A.det
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.strictLimitsOfShape_le_limitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], P.strictLimitsOfShape J ≤ P.limitsOfShape J
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.le_inf : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {a b c : CauSeq α abs},
  a ≤ b → a ≤ c → a ≤ b ⊓ c
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.map_const : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure α) {f : α → β},
  Measurable f →
    (ProbabilityTheory.Kernel.const γ μ).map f = ProbabilityTheory.Kernel.const γ (MeasureTheory.Measure.map f μ)
-- Mathlib.Util.FormatTable
Alignment.center.sizeOf_spec : sizeOf Alignment.center = 1
-- Mathlib.Data.Multiset.ZeroCons
Multiset.Rel.mono : ∀ {α : Type u_1} {β : Type v} {r p : α → β → Prop} {s : Multiset α} {t : Multiset β},
  Multiset.Rel r s t → (∀ a ∈ s, ∀ b ∈ t, r a b → p a b) → Multiset.Rel p s t
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.mem_fixedPoints : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] {a : α},
  a ∈ MulAction.fixedPoints M α ↔ ∀ (m : M), m • a = a
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.nat_odd_mul_antiperiodic : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : NonAssocSemiring α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c → ∀ (n : ℕ), Function.Antiperiodic f (↑n * (2 * c) + c)
-- Mathlib.Analysis.Seminorm
Seminorm.coe_comp : ∀ {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [inst : SeminormedRing 𝕜] [inst_1 : SeminormedRing 𝕜₂]
  {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup E₂]
  [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ E₂] (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂), ⇑(p.comp f) = ⇑p ∘ ⇑f
-- Mathlib.Algebra.Group.WithOne.Basic
MulEquiv.withOneCongr_apply : ∀ {α : Type u} {β : Type v} [inst : Mul α] [inst_1 : Mul β] (e : α ≃* β) (a : WithOne α),
  e.withOneCongr a = (WithOne.mapMulHom e.toMulHom) a
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_sub : ∀ {a b c : ENNReal}, (0 < c → c < b → a ≠ ⊤) → a * (b - c) = a * b - a * c
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.testAgainstNN_coe_eq : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω}
  {f : BoundedContinuousFunction Ω NNReal}, ↑(μ.testAgainstNN f) = ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ
-- Init.Data.Nat.Basic
Nat.le_of_add_right_le : ∀ {n m k : ℕ}, n + k ≤ m → n ≤ m
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_succ : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] [inst_1 : OrderBot ι] [inst_2 : InfSet ι] {a b : ℝ} {f : ι → Ω → ℝ}
  {N : ι} {n : ℕ} {ω : Ω},
  MeasureTheory.upperCrossingTime a b f N (n + 1) ω =
    MeasureTheory.hittingBtwn f (Set.Ici b)
      (MeasureTheory.lowerCrossingTimeAux a f (MeasureTheory.upperCrossingTime a b f N n ω) N ω) N ω
-- Init.Data.SInt.Lemmas
Int64.toInt_mul : ∀ (a b : Int64), (a * b).toInt = (a.toInt * b.toInt).bmod (2 ^ 64)
-- Mathlib.Tactic.Push
/-- A simproc variant of `pull fun _ ↦ _`, to be used as `simp [pullFun]`.  -/
pullFun : Lean.Meta.Simp.Simproc
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
/-- If `M` additively acts on `α`, then `DomAddAct M` acts on `α → β` as
well as some bundled maps from `α`. This is a type synonym for `AddOpposite M`, so this corresponds
to a right action of `M`.  -/
DomAddAct : Type u_1 → Type u_1
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.combineCones_π_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)) (j : J) (k : K),
  ((CategoryTheory.Limits.combineCones F c).π.app j).app k = (c k).cone.π.app j
-- Lean.Compiler.IR.CompilerM
_private.Lean.Compiler.IR.CompilerM.0.Lean.IR.exportIREntries.unsafe_impl_8 : Array (Option Lean.PkgId) → Array Lean.EnvExtensionEntry
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.comap_apply : ∀ {R : Type u} [inst : CommRing R] {S : Type u} [inst_1 : CommRing S] (f : R →+* S)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S))
  (hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier)
  (s : ↑((AlgebraicGeometry.Spec.structureSheaf R).obj.obj (Opposite.op U))) (p : ↥V),
  ↑((AlgebraicGeometry.StructureSheaf.comap f U V hUV) s) p =
    (Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯) (↑s ⟨PrimeSpectrum.comap f ↑p, ⋯⟩)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minEntry?_map : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (l : List ((a : α) × β a)) (f : (a : α) × β a → (a : α) × β a),
  (∀ (e₁ e₂ : (a : α) × β a), compare e₁.fst e₂.fst = compare (f e₁).fst (f e₂).fst) →
    Std.Internal.List.minEntry? (List.map f l) = Option.map f (Std.Internal.List.minEntry? l)
-- Mathlib.Tactic.NormNum.Irrational
/-- To prove that `m` is not `n`-power (and thus `m ^ (1/n)` is irrational), we find `k` such that
`k ^ n < m < (k + 1) ^ n`.  -/
Mathlib.Meta.NormNum.NotPowerCertificate : Q(ℕ) → Q(ℕ) → Type
-- Lean.Environment
/-- Evaluates the given declaration under the given environment to a value of the given type.
This function is only safe to use if the type matches the declaration's type in the environment
and if `enableInitializersExecution` has been used before importing any modules.

If `checkMeta` is true (the default), the function checks that all referenced imported constants are
marked or imported as `meta` or otherwise fails with an error. It should only be set to `false` in
cases where it is acceptable for code to work only in the language server, where more IR is loaded,
such as in `#eval`.
 -/
Lean.Environment.evalConst : (α : Type) → Lean.Environment → Lean.Options → Lean.Name → optParam Bool true → Except String α
-- Init.System.IOError
IO.Error.timeExpired.injEq : ∀ (osCode : UInt32) (details : String) (osCode_1 : UInt32) (details_1 : String),
  (IO.Error.timeExpired osCode details = IO.Error.timeExpired osCode_1 details_1) =
    (osCode = osCode_1 ∧ details = details_1)
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.closedEBall_prod_same`. -/
EMetric.closedBall_prod_same : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (x : α) (y : β) (r : ENNReal),
  Metric.closedEBall x r ×ˢ Metric.closedEBall y r = Metric.closedEBall (x, y) r
-- Lean.Linter.UnusedVariables
/-- Given `aliases` as a map from an alias to what it aliases, we get the original
term by recursion. This has no cycle detection, so if `aliases` contains a loop
then this function will recurse infinitely.  -/
Lean.Linter.UnusedVariables.followAliases : Std.HashMap Lean.FVarId Lean.FVarId → Lean.FVarId → Lean.FVarId
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.WorkspaceSymbolParams.mk.sizeOf_spec : ∀ (query : String), sizeOf { query := query } = 1 + sizeOf query
-- Mathlib.Topology.MetricSpace.Polish
TopologicalSpace.Opens.CompleteCopy.instSecondCountableTopology : ∀ {α : Type u_1} [inst : MetricSpace α] {s : TopologicalSpace.Opens α} [SecondCountableTopology α],
  SecondCountableTopology s.CompleteCopy