mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Basic
real_inner_comm : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), inner ℝ y x = inner ℝ x y
-- Mathlib.Topology.Category.Profinite.Basic
Profinite.of.congr_simp : ∀ (X : Type u_1) [inst : TopologicalSpace X] [inst_1 : CompactSpace X] [inst_2 : T2Space X]
  [inst_3 : TotallyDisconnectedSpace X], Profinite.of X = Profinite.of X
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtrOn.comp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α → β} {s : Set α} {a : α}, IsLocalExtrOn f s a → ∀ {g : β → γ}, Monotone g → IsLocalExtrOn (g ∘ f) s a
-- Mathlib.Data.Countable.Basic
instUncountableProdOfNonempty_1 : ∀ {α : Type u} {β : Type v} [Nonempty α] [Uncountable β], Uncountable (α × β)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.verts_sInf : ∀ {V : Type u} {G : SimpleGraph V} (s : Set G.Subgraph), (sInf s).verts = ⋂ G' ∈ s, G'.verts
-- Mathlib.Data.Finsupp.Single
/-- **Alias** of `Finsupp.support_single`. -/
Finsupp.support_single_ne_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {b : M} (a : α), b ≠ 0 → (fun₀ | a => b).support = {a}
-- Mathlib.Condensed.Solid
/-- The natural transformation `R[S] ⟶ R[S]^\solid`.  -/
Condensed.profiniteSolidification : (R : Type (u + 1)) → [inst : Ring R] → Condensed.profiniteFree R ⟶ Condensed.profiniteSolid R
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.ext_iff : ∀ {x y : Std.Time.PlainDateTime}, x = y ↔ x.date = y.date ∧ x.time = y.time
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
CategoryTheory.additive_coyonedaObj' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (X : Cᵒᵖ),
  (CategoryTheory.preadditiveCoyoneda.obj X).Additive
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.codeBlock.deIndent : ℕ → String → String
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.LocalizationAwayPreserves.respectsIso : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P) →
    RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
-- Mathlib.SetTheory.ZFC.Basic
/-- A nonempty set is one that contains some element.  -/
ZFSet.Nonempty : ZFSet.{u} → Prop
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_one_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α), lcm a 1 = normalize a
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.embFunctor.congr_simp : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E]
  ⦃i j : WithTop (Module.rank F E).ord.ToType⦄ (h : i ≤ j)
  (f f_1 : ↥(Field.Emb.Cardinal.filtration j) →ₐ[F] AlgebraicClosure E),
  f = f_1 → Field.Emb.Cardinal.embFunctor F E h f = Field.Emb.Cardinal.embFunctor F E h f_1
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.copy.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N] (f : M →* N) (f' : M → N) (h : f' = ⇑f),
  f.copy f' h = { toOneHom := (↑f).copy f' h, map_mul' := ⋯ }
-- Init.Data.Ord.Basic
Ordering.lt.sizeOf_spec : sizeOf Ordering.lt = 1
-- Mathlib.Analysis.Convex.Jensen
/-- **Maximum principle** for convex functions on a segment. If a function `f` is convex on the
segment `[x, y]`, then the eventual maximum of `f` on `[x, y]` is at `x` or `y`.  -/
ConvexOn.le_max_of_mem_segment : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : LinearOrder β] [IsOrderedAddMonoid β]
  [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β} {x y z : E},
  ConvexOn 𝕜 s f → x ∈ s → y ∈ s → z ∈ segment 𝕜 x y → f z ≤ max (f x) (f y)
-- Mathlib.Data.Finsupp.Single
Finsupp.single_eq_same : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α} {b : M}, (fun₀ | a => b) a = b
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ArbitraryShiftTarget.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {m : ℕ} → (n : ℕ) → aig.RefVec m → aig.RefVec n → aig.ArbitraryShiftTarget m
-- Mathlib.Analysis.LocallyConvex.WeakDual
/-- Construct a seminorm from a linear form `f : E →ₗ[𝕜] 𝕜` over a normed field `𝕜` by
`fun x => ‖f x‖`  -/
LinearMap.toSeminorm : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NormedField 𝕜] → [inst_1 : AddCommGroup E] → [inst_2 : Module 𝕜 E] → (E →ₗ[𝕜] 𝕜) → Seminorm 𝕜 E
-- Plausible.Testable
/-- A counter-example to `p`; the strings specify values for the relevant variables.
`failure h vs n` also carries a proof that `p` does not hold. This way, we can
guarantee that there will be no false positive. The last component, `n`,
is the number of times that the counter-example was shrunk.
 -/
Plausible.TestResult.failure : {p : Prop} → ¬p → List String → ℕ → Plausible.TestResult p
-- Mathlib.Analysis.SpecialFunctions.Log.Base
/-- Induction principle for intervals of real numbers: if a proposition `P` is true
on `[x₀, r * x₀)` and if `P` for `[x₀, r^n * x₀)` implies `P` for `[r^n * x₀, r^(n+1) * x₀)`,
then `P` is true for all `x ≥ x₀`.  -/
Real.induction_Ico_mul : ∀ {P : ℝ → Prop} (x₀ r : ℝ),
  1 < r →
    0 < x₀ →
      (∀ x ∈ Set.Ico x₀ (r * x₀), P x) →
        (∀ n ≥ 1, (∀ z ∈ Set.Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Set.Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z) →
          ∀ x ≥ x₀, P x
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.smul_of_tower_mem : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SMul S R]
  [inst_3 : SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) (s : S) {x : M}, x ∈ p → s • x ∈ p
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_int_mod : ∀ (l : List ℤ) (n : ℤ), l.sum % n = (List.map (fun x => x % n) l).sum % n
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.ιOfLE_δ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsMonoidal] {P' : CategoryTheory.ObjectProperty C}
  [inst_3 : P'.IsMonoidal] (h : P ≤ P') (X Y : P.FullSubcategory),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.ObjectProperty.ιOfLE h) X Y =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.ObjectProperty.ιOfLE h).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.addSubgroup_vadd_def : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {H : AddSubgroup G} (a : ↥H) (b : α),
  a +ᵥ b = ↑a +ᵥ b
-- Init.Prelude
Pi.instNonempty : ∀ {α : Sort u} {β : α → Sort v} [∀ (a : α), Nonempty (β a)], Nonempty ((a : α) → β a)
-- Mathlib.Analysis.Convolution
/-- If `‖f‖ *[μ] ‖g‖` exists, then `f *[L, μ] g` exists.  -/
MeasureTheory.ConvolutionExistsAt.of_norm : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : AddGroup G]
  [MeasurableAdd₂ G] [MeasurableNeg G] [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant] {x₀ : G},
  MeasureTheory.ConvolutionExistsAt (fun x => ‖f x‖) (fun x => ‖g x‖) x₀ (ContinuousLinearMap.mul ℝ ℝ) μ →
    MeasureTheory.AEStronglyMeasurable f μ →
      MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.ConvolutionExistsAt f g x₀ L μ
-- Mathlib.RingTheory.Ideal.Basis
Ideal.constr_basisSpanSingleton : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] {N : Type u_4} [inst_4 : Semiring N] [inst_5 : Module N S] [inst_6 : SMulCommClass R N S]
  (b : Module.Basis ι R S) {x : S} (hx : x ≠ 0),
  (↑(b.constr N)).toFun (Subtype.val ∘ ⇑(Ideal.basisSpanSingleton b hx)) = (Algebra.lmul R S) x
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.triangle_aux₂ : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X Y : CategoryTheory.LocalizedMonoidal L W ε} {X' Y' : C}
  (e₁ : (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X' ≅ X)
  (e₂ : (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y' ≅ Y),
  CategoryTheory.MonoidalCategoryStruct.tensorHom e₁.hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ε.hom e₂.hom)
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X')
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Localization.Monoidal.ε' L W ε).hom
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y'))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
              (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.LocalizedMonoidal L W ε)) e₂.hom)
            (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom)))
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight e₁.hom Y)
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.localized'_smul : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R)
  [inst_9 : IsLocalization p S] (f : M →ₗ[R] N) [inst_10 : IsLocalizedModule p f] (M' : Submodule R M)
  (I : Submodule R R),
  Submodule.localized' S p f (I • M') =
    Submodule.localized' S p (Algebra.linearMap R S) I • Submodule.localized' S p f M'
-- Mathlib.Algebra.Group.AddChar
AddChar.mulShift_one : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : CommMonoid M] (ψ : AddChar R M), ψ.mulShift 1 = ψ
-- Mathlib.Topology.Homotopy.HSpaces
Path.delayReflRight_zero : ∀ {X : Type u} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), Path.delayReflRight 0 γ = γ.trans (Path.refl y)
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
/-- `exp ∘ f` is analytic  -/
AnalyticAt.rexp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  AnalyticAt ℝ f x → AnalyticAt ℝ (Real.exp ∘ f) x
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Ordered.reverse : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β}, t.Ordered → t.reverse.Ordered
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.centralizer_le : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] (s t : Set R),
  s ⊆ t → NonUnitalSubsemiring.centralizer t ≤ NonUnitalSubsemiring.centralizer s
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  (f : CategoryTheory.Arrow C) (j : κ.ord.ToType),
  CategoryTheory.Arrow.Hom.left (CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso I κ f j).hom =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.Arrow.mk
          (((CategoryTheory.SmallObject.iterationFunctor I κ).map (CategoryTheory.homOfLE ⋯)).app f)).left
-- Mathlib.Algebra.Field.Rat
NNRat.div_def : ∀ (p q : ℚ≥0), p / q = NNRat.divNat (p.num * q.den) (p.den * q.num)
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableVAdd_iterateAddAct : ∀ {α : Type u_2} {x : MeasurableSpace α} {f : α → α}, MeasurableVAdd (IterateAddAct f) α ↔ Measurable f
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `Topology.WithGeneratedByTopology.isOpen_iff`. -/
isOpen_deltaGenerated_iff : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  {U : Set (Topology.WithGeneratedByTopology X Y)},
  IsOpen U ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsOpen (⇑f ⁻¹' ⇑Topology.WithGeneratedByTopology.equiv.symm ⁻¹' U)
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.functorialityEquivalence`.

---

If `e : C ≌ D` is an equivalence of categories, then `functoriality F e.functor` induces an
equivalence between cocones over `F` and cocones over `F ⋙ e.functor`.
 -/
CategoryTheory.Limits.Cocones.functorialityEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (F : CategoryTheory.Functor J C) →
              (e : C ≌ D) → CategoryTheory.Limits.Cocone F ≌ CategoryTheory.Limits.Cocone (F.comp e.functor)
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.μ_δ_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (i j : M)
  (X : C) [inst_3 : F.Monoidal] {Z : C}
  (h : (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj i) (F.obj j)).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F i j).app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F i j).app X) h) =
    h
-- Lean.Elab.Open
Lean.Elab.OpenDecl.State.mk.sizeOf_spec : ∀ (openDecls : List Lean.OpenDecl) (currNamespace : Lean.Name),
  sizeOf { openDecls := openDecls, currNamespace := currNamespace } = 1 + sizeOf openDecls + sizeOf currNamespace
-- Mathlib.Algebra.Order.Star.Basic
IsStarProjection.instTrivialStarOfStarOrderedRing : ∀ {R : Type u_3} [inst : NonUnitalRing R] [inst_1 : LinearOrder R] [inst_2 : StarRing R] [StarOrderedRing R],
  TrivialStar R
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The natural ring homomorphism mapping `R[X][Y]` to `R[W]`.  -/
WeierstrassCurve.Affine.CoordinateRing.mk : {R : Type r} → [inst : CommRing R] → (W' : WeierstrassCurve.Affine R) → Polynomial (Polynomial R) →+* W'.CoordinateRing
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.equivalenceOfReindexing.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : e.functor.comp F ≅ G),
  CategoryTheory.Limits.Cocone.equivalenceOfReindexing e α =
    (CategoryTheory.Limits.Cocone.whiskeringEquivalence e).trans (CategoryTheory.Limits.Cocone.precomposeEquivalence α)
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  (s : (Finset (CategoryTheory.Discrete α))ᵒᵖ),
  (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj F).obj s = ∏ᶜ fun x => F.obj ↑x
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.instDecidableEq : {R : Type u_1} →
  {M : Type u_4} → [inst : Semiring R] → [DecidableEq R] → [DecidableEq M] → DecidableEq (AddMonoidAlgebra R M)
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.norm_ofSubsingleton : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] [inst_6 : Subsingleton ι] (i : ι) (f : E →L[𝕜] F),
  ‖(ContinuousAlternatingMap.ofSubsingleton 𝕜 E F i) f‖ = ‖f‖
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStronglyProgressive.stronglyMeasurable_stoppedProcess : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {u : ι → Ω → β}
  {τ : Ω → WithTop ι} [inst_1 : LinearOrder ι] [inst_2 : MeasurableSpace ι] [inst_3 : TopologicalSpace ι]
  [OrderTopology ι] [SecondCountableTopology ι] [BorelSpace ι] [inst_7 : TopologicalSpace β]
  {f : MeasureTheory.Filtration ι m} [TopologicalSpace.PseudoMetrizableSpace ι],
  MeasureTheory.IsStronglyProgressive f u →
    MeasureTheory.IsStoppingTime f τ → ∀ (i : ι), MeasureTheory.StronglyMeasurable (MeasureTheory.stoppedProcess u τ i)
-- Mathlib.RingTheory.Multiplicity
emultiplicity_of_one_right : ∀ {α : Type u_1} [inst : CommMonoid α] {a : α}, ¬IsUnit a → emultiplicity a 1 = 0
-- Mathlib.Algebra.Order.SuccPred
SuccAddOrder.succ_eq_add_one : ∀ {α : Type u_1} {inst : Preorder α} {inst_1 : Add α} {inst_2 : One α} [self : SuccAddOrder α] (x : α),
  SuccOrder.succ x = x + 1
-- Mathlib.Topology.ClusterPt
mem_closure_iff_clusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, x ∈ closure s ↔ ClusterPt x (Filter.principal s)
-- Mathlib.RingTheory.FreeRing
FreeRing.of_injective : ∀ {α : Type u}, Function.Injective FreeRing.of
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_hom_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {r s : CategoryTheory.Limits.Cone F} {t : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) (w : F ≅ G) {Z : C} (h : t.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.lift r)
      (CategoryTheory.CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.IsLimit.map r Q w.hom) h
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.closure_sdiff_eq_closure : ∀ {M : Type u_1} [inst : AddZeroClass M] {s t : Set M},
  t ⊆ ↑(AddSubmonoid.closure (s \ t)) → AddSubmonoid.closure (s \ t) = AddSubmonoid.closure s
-- Mathlib.LinearAlgebra.Dimension.Constructions
rank_span_of_finset : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  (s : Finset M), Module.rank R ↥(Submodule.span R ↑s) < Cardinal.aleph0
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEq_congrFun : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {u₀ v₀ : E.I₀ → F.I₀} {u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)}
  {v₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (v₀ i) (v₀ j)} (h₀ : u₀ = v₀),
  (∀ (i j : E.I₀) (k : E.I₁ i j), u₁ k = (CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) (v₁ k)) →
    ∀ {i j : E.I₀} (k : E.I₁ i j), (CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) (v₁ k) = u₁ k
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.fun.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {decl : Lean.Compiler.LCNF.FunDecl pu}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.CodeDecl._auto_1}
  {decl_1 : Lean.Compiler.LCNF.FunDecl pu}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.CodeDecl._auto_1},
  Lean.Compiler.LCNF.CodeDecl.fun decl h = Lean.Compiler.LCNF.CodeDecl.fun decl_1 h_1 → decl = decl_1
-- Init.Data.SInt.Float
/-- Truncates a floating-point number to the nearest 16-bit signed integer, rounding towards zero.

If the `Float` is larger than the maximum value for `Int16` (including `Inf`), returns the maximum
value of `Int16` (i.e. `Int16.maxValue`). If it is smaller than the minimum value for `Int16`
(including `-Inf`), returns the minimum value of `Int16` (i.e. `Int16.minValue`). If it is `NaN`,
returns `0`.

This function does not reduce in the kernel.
 -/
Float.toInt16 : Float → Int16
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofMacroExpansionInfo.inj : ∀ {i i_1 : Lean.Elab.MacroExpansionInfo},
  Lean.Elab.Info.ofMacroExpansionInfo i = Lean.Elab.Info.ofMacroExpansionInfo i_1 → i = i_1
-- Std.Time.Time.Unit.Nanosecond
/-- Creates an `Ordinal` from an integer, ensuring the value is within bounds.
 -/
Std.Time.Nanosecond.Ordinal.ofInt : (data : ℤ) → 0 ≤ data ∧ data ≤ 999999999 → Std.Time.Nanosecond.Ordinal
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isAlt_iff_eq_neg_flip : ∀ {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [inst : CommRing R] [inst_1 : CommSemiring R₁]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module R₁ M₁] {I : R₁ →+* R} [NoZeroDivisors R] [CharZero R]
  {B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R}, B.IsAlt ↔ B = -B.flip
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.Error.timeout.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Error.timeout = 1
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.prodCongr_apply : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  {M₂ : Type u_5} [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M₂] {M₃ : Type u_6}
  [inst_5 : TopologicalSpace M₃] [inst_6 : AddCommMonoid M₃] {M₄ : Type u_7} [inst_7 : TopologicalSpace M₄]
  [inst_8 : AddCommMonoid M₄] [inst_9 : Module R₁ M₁] [inst_10 : Module R₁ M₂] [inst_11 : Module R₁ M₃]
  [inst_12 : Module R₁ M₄] (e : M₁ ≃L[R₁] M₂) (e' : M₃ ≃L[R₁] M₄) (x : M₁ × M₃), (e.prodCongr e') x = (e x.1, e' x.2)
-- Mathlib.CategoryTheory.Opposites
/-- Compatibility of `Functor.rightOp` with respect to functor composition.  -/
CategoryTheory.Functor.rightOpComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} E] →
            (F : CategoryTheory.Functor Cᵒᵖ D) →
              (G : CategoryTheory.Functor D E) → (F.comp G).rightOp ≅ F.rightOp.comp G.op
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.inv' : ℝ → ℝ
-- Mathlib.Order.Filter.IndicatorFunction
Filter.EventuallyEq.indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero β] {l : Filter α} {f g : α → β} {s : Set α},
  f =ᶠ[l] g → s.indicator f =ᶠ[l] s.indicator g
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.findAux.eq_def : ∀ (self : Batteries.UnionFind) (x : Fin self.size),
  self.findAux x =
    let y := self.arr[↑x].parent;
    if h : y = ↑x then { s := self.arr, root := x, size_eq := ⋯ }
    else
      have this := ⋯;
      match self.findAux ⟨y, ⋯⟩ with
      | { s := arr₁, root := root, size_eq := H } =>
        { s := arr₁.modify ↑x fun s => { parent := ↑root, rank := s.rank }, root := root, size_eq := ⋯ }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {k k' : α}
  {f : β → β},
  Std.DTreeMap.Const.get? (Std.DTreeMap.Const.modify t k f) k' =
    if cmp k k' = Ordering.eq then Option.map f (Std.DTreeMap.Const.get? t k) else Std.DTreeMap.Const.get? t k'
-- Lean.Parser.Basic
Lean.Parser.mergeOrElseErrors : Lean.Parser.ParserState → Lean.Parser.Error → String.Pos.Raw → Bool → Lean.Parser.ParserState
-- Mathlib.Data.Multiset.Bind
Multiset.sigma.eq_1 : ∀ {α : Type u_1} {σ : α → Type u_4} (s : Multiset α) (t : (a : α) → Multiset (σ a)),
  s.sigma t = s.bind fun a => Multiset.map (Sigma.mk a) (t a)