mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- `Sheaf.homEquiv` as a natural isomorphism.  -/
CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          (CategoryTheory.sheafToPresheaf J A).comp
              (CategoryTheory.yoneda.comp
                ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Sheaf J A)ᵒᵖ (CategoryTheory.Functor Cᵒᵖ A)ᵒᵖ
                      (Type (max u₁ v₂))).obj
                  (CategoryTheory.sheafToPresheaf J A).op)) ≅
            CategoryTheory.yoneda
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instPreservesLimitTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitOfModuleCatCompLinearMapForget : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] {J : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_1, u_2} J] {F : CategoryTheory.Functor J (TopModuleCat R)}
  [CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)))]
  [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)))
      (CategoryTheory.forget (ModuleCat R))],
  CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget₂ (TopModuleCat R) TopCat)
-- Aesop.Tree.Data
Aesop.GoalUnsafe.brecOn_8.eq : ∀ {motive_1 : Aesop.GoalUnsafe → Sort u} {motive_2 : Aesop.MVarClusterUnsafe → Sort u}
  {motive_3 : Aesop.RappUnsafe → Sort u} {motive_4 : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_5 : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Sort u}
  {motive_6 : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_7 : Array (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_8 : Option (IO.Ref Aesop.RappUnsafe) → Sort u}
  {motive_9 : Array (IO.Ref Aesop.GoalUnsafe) → Sort u} {motive_10 : Array (IO.Ref Aesop.MVarClusterUnsafe) → Sort u}
  {motive_11 : List (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_12 : List (IO.Ref Aesop.GoalUnsafe) → Sort u}
  {motive_13 : List (IO.Ref Aesop.MVarClusterUnsafe) → Sort u} (t : List (IO.Ref Aesop.RappUnsafe))
  (F_1 : (t : Aesop.GoalUnsafe) → t.below → motive_1 t) (F_2 : (t : Aesop.MVarClusterUnsafe) → t.below → motive_2 t)
  (F_3 : (t : Aesop.RappUnsafe) → t.below → motive_3 t)
  (F_4 : (t : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_1 t → motive_4 t)
  (F_5 : (t : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) → Aesop.GoalUnsafe.below_2 t → motive_5 t)
  (F_6 : (t : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_3 t → motive_6 t)
  (F_7 : (t : Array (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_4 t → motive_7 t)
  (F_8 : (t : Option (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_5 t → motive_8 t)
  (F_9 : (t : Array (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_6 t → motive_9 t)
  (F_10 : (t : Array (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_7 t → motive_10 t)
  (F_11 : (t : List (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_8 t → motive_11 t)
  (F_12 : (t : List (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_9 t → motive_12 t)
  (F_13 : (t : List (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_10 t → motive_13 t),
  Aesop.GoalUnsafe.brecOn_8 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13 =
    F_11 t (Aesop.GoalUnsafe.brecOn_8.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13).2
-- Mathlib.Analysis.SpecialFunctions.Arsinh
DifferentiableAt.arsinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E},
  DifferentiableAt ℝ f a → DifferentiableAt ℝ (fun x => Real.arsinh (f x)) a
-- Init.Data.Repr
instReprUSize : Repr USize
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceCastLE : Lean.Meta.Simp.DSimproc
-- Mathlib.Order.CompleteLattice.Basic
iSup₂_mono' : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {κ : ι → Sort u_6} {κ' : ι' → Sort u_7} [inst : CompleteLattice α]
  {f : (i : ι) → κ i → α} {g : (i' : ι') → κ' i' → α},
  (∀ (i : ι) (j : κ i), ∃ i' j', f i j ≤ g i' j') → ⨆ i, ⨆ j, f i j ≤ ⨆ i, ⨆ j, g i j
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
CompactConvergenceCLM.hasBasis_nhds_zero : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F],
  (nhds 0).HasBasis (fun SV => IsCompact SV.1 ∧ SV.2 ∈ nhds 0) fun SV => {f | ∀ x ∈ SV.1, f x ∈ SV.2}
-- Mathlib.Analysis.InnerProductSpace.Calculus
DifferentiableAt.dist : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f g : G → E}
  {x : G},
  DifferentiableAt ℝ f x → DifferentiableAt ℝ g x → f x ≠ g x → DifferentiableAt ℝ (fun y => dist (f y) (g y)) x
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.extend_function : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} (f : ↑s ↪ β),
  Nonempty (↑sᶜ ≃ ↑(Set.range ⇑f)ᶜ) → ∃ g, ∀ (x : ↑s), g ↑x = f x
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.changeForm_ι : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q) (m : M),
  (CliffordAlgebra.changeForm h) ((CliffordAlgebra.ι Q) m) = (CliffordAlgebra.ι Q') m
-- Mathlib.Algebra.Algebra.Pi
/-- Transport dependent functions through an equivalence of the base space, expressed as
"simplification".

This is `Equiv.piCongrLeft` as an `AlgEquiv`.
 -/
AlgEquiv.piCongrLeft : (R : Type u_3) →
  {ι : Type u_4} →
    (A₁ : ι → Type u_5) →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → Semiring (A₁ i)] →
          [inst_2 : (i : ι) → Algebra R (A₁ i)] →
            {ι' : Type u_8} → (e : ι' ≃ ι) → ((i : ι') → A₁ (e i)) ≃ₐ[R] (i : ι) → A₁ i
-- Init.Grind.ToInt
Lean.Grind.IntInterval.isFinite.eq_2 : ∀ (lo : ℤ), (Lean.Grind.IntInterval.ci lo).isFinite = false
-- Mathlib.MeasureTheory.Group.AddCircle
/-- Let `G` be the subgroup of `AddCircle T` generated by a point `u` of finite order `n : ℕ`. Then
any set `I` that is almost equal to a ball of radius `T / 2n` is a fundamental domain for the action
of `G` on `AddCircle T` by left addition.  -/
AddCircle.isAddFundamentalDomain_of_ae_ball : ∀ {T : ℝ} [hT : Fact (0 < T)] (I : Set (AddCircle T)) (u x : AddCircle T),
  IsOfFinAddOrder u →
    I =ᵐ[MeasureTheory.volume] Metric.ball x (T / (2 * ↑(addOrderOf u))) →
      MeasureTheory.IsAddFundamentalDomain (↥(AddSubgroup.zmultiples u)) I MeasureTheory.volume
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y) (s : Set X)
  (x : X), ContinuousWithinAt f s x = Filter.Tendsto f (nhdsWithin x s) (nhds (f x))
-- Mathlib.CategoryTheory.Monad.Algebra
/-- Given an algebra morphism whose carrier part is an isomorphism, we get an algebra isomorphism.
 -/
CategoryTheory.Monad.algebra_iso_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {A B : T.Algebra} (f : A ⟶ B)
  [CategoryTheory.IsIso f.f], CategoryTheory.IsIso f
-- Mathlib.Order.ModularLattice
covBy_sup_of_inf_covBy_left : ∀ {α : Type u_1} [inst : Lattice α] [IsUpperModularLattice α] {a b : α}, a ⊓ b ⋖ a → b ⋖ a ⊔ b
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.negMulLog.eq_1 : ∀ (x : ℝ), x.negMulLog = -x * Real.log x
-- Init.Data.String.Lemmas.Pattern.Split.Pred
_private.Init.Data.String.Lemmas.Pattern.Split.Pred.0.String.Slice.Pattern.Model.split.eq_1 : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} (firstRejected curr : s.Pos)
  (hle : firstRejected ≤ curr),
  String.Slice.Pattern.Model.split pat firstRejected curr hle =
    if h : curr = s.endPos then [s.subslice firstRejected curr hle]
    else
      match hd : String.Slice.Pattern.Model.matchAt? pat curr with
      | some pos =>
        have this := ⋯;
        s.subslice firstRejected curr hle :: String.Slice.Pattern.Model.split pat pos pos ⋯
      | none => String.Slice.Pattern.Model.split pat firstRejected (curr.next h) ⋯
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
/-- The characteristic function of a finite measure with a moment of order `n` is `C^n`.
See `contDiff_charFun'` for the version proving `C^∞` by assuming all moments exist.  -/
MeasureTheory.contDiff_charFun : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [BorelSpace E] [SecondCountableTopology E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] {n : ℕ},
  MeasureTheory.MemLp id (↑n) μ → ContDiff ℝ (↑n) (MeasureTheory.charFun μ)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.hasBiproduct_of_preserves : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁}
  (F : CategoryTheory.Functor C D) (f : J → C) [CategoryTheory.Limits.HasBiproduct f]
  [inst_5 : F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesBiproduct f F],
  CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_sub_index : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddGroup (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommGroup γ] {f g : Π₀ (i : ι), β i}
  {h : (i : ι) → β i → γ},
  (∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂) → (f - g).sum h = f.sum h - g.sum h
-- Mathlib.Algebra.Order.UpperLower
upperClosure_mul_distrib : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α] (s t : Set α),
  upperClosure (s * t) = upperClosure s * upperClosure t
-- Mathlib.Order.CompactlyGenerated.Basic
DirectedOn.disjoint_sSup_left : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsCompactlyGenerated α] {a : α} {s : Set α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → (Disjoint (sSup s) a ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint b a)
-- Mathlib.Algebra.Group.Action.End
Equiv.Perm.smul_def : ∀ {α : Type u_6} (f : Equiv.Perm α) (a : α), f • a = f a
-- Mathlib.Algebra.Module.Equiv.Basic
/-- A linear isomorphism between the domains and codomains of two spaces of linear maps gives a
linear isomorphism with respect to an action on the domains.  -/
LinearEquiv.domMulActCongrRight : {S : Type u_4} →
  {R₁ : Type u_9} →
    {R₁' : Type u_11} →
      {R₂' : Type u_12} →
        {M₁ : Type u_13} →
          {M₁' : Type u_15} →
            {M₂' : Type u_16} →
              [inst : Semiring R₁] →
                [inst_1 : Semiring R₁'] →
                  [inst_2 : Semiring R₂'] →
                    [inst_3 : AddCommMonoid M₁] →
                      [inst_4 : AddCommMonoid M₁'] →
                        [inst_5 : AddCommMonoid M₂'] →
                          [inst_6 : Module R₁ M₁] →
                            [inst_7 : Module R₁' M₁'] →
                              [inst_8 : Module R₂' M₂'] →
                                {σ₁'₂' : R₁' →+* R₂'} →
                                  {σ₂'₁' : R₂' →+* R₁'} →
                                    {σ₁₁' : R₁ →+* R₁'} →
                                      {σ₁₂' : R₁ →+* R₂'} →
                                        [inst_9 : RingHomInvPair σ₁'₂' σ₂'₁'] →
                                          [inst_10 : RingHomInvPair σ₂'₁' σ₁'₂'] →
                                            [RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] →
                                              [inst_12 : Semiring S] →
                                                [inst_13 : Module S M₁] →
                                                  [inst_14 : SMulCommClass R₁ S M₁] →
                                                    [RingHomCompTriple σ₁₂' σ₂'₁' σ₁₁'] →
                                                      (M₁' ≃ₛₗ[σ₁'₂'] M₂') →
                                                        (M₁ →ₛₗ[σ₁₁'] M₁') ≃ₗ[Sᵈᵐᵃ] M₁ →ₛₗ[σ₁₂'] M₂'
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.integral_mul_upcrossingsBefore_le_integral : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {a b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ}
  {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    (∀ (ω : Ω), a ≤ f N ω) →
      0 ≤ f 0 → a < b → (b - a) * ∫ (x : Ω), ↑(MeasureTheory.upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), f N x ∂μ
-- Mathlib.Analysis.Analytic.Order
/-- The order is additive when scalar multiplying analytic functions.  -/
analyticOrderAt_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {g : 𝕜 → E} {z₀ : 𝕜} {f : 𝕜 → 𝕜},
  AnalyticAt 𝕜 f z₀ → AnalyticAt 𝕜 g z₀ → analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀
-- Lean.Meta.Basic
/-- When `cacheInferType := true`, the `inferType` results are cached if the input term does not contain
metavariables
 -/
Lean.Meta.Context.cacheInferType : Lean.Meta.Context → Bool
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdUniformlyOn.multipliableUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α], HasProdUniformlyOn f g s → MultipliableUniformlyOn f s
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Icc₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {c : G₀} (a b : G₀),
  0 < c → (fun x => x * c) ⁻¹' Set.Icc a b = Set.Icc (a / c) (b / c)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.mkOfCompact_add : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : CompactSpace α]
  [inst_3 : Add β] [inst_4 : BoundedAdd β] [inst_5 : ContinuousAdd β] (f g : C(α, β)),
  BoundedContinuousFunction.mkOfCompact (f + g) =
    BoundedContinuousFunction.mkOfCompact f + BoundedContinuousFunction.mkOfCompact g
-- Mathlib.Analysis.Convex.Cone.Basic
/-- The positive cone is the proper cone formed by the set of nonnegative elements in an ordered
module.  -/
ProperCone.positive : (R : Type u_2) →
  (E : Type u_3) →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] →
          [inst_3 : AddCommMonoid E] →
            [inst_4 : TopologicalSpace E] →
              [inst_5 : Module R E] →
                [inst_6 : PartialOrder E] →
                  [IsOrderedAddMonoid E] → [PosSMulMono R E] → [OrderClosedTopology E] → ProperCone R E
-- Mathlib.CategoryTheory.Subobject.Basic
/-- An adjunction between `MonoOver A` and `MonoOver B` gives an adjunction
between `Subobject A` and `Subobject B`.  -/
CategoryTheory.Subobject.lowerAdjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {A : C} →
          {B : D} →
            {L : CategoryTheory.Functor (CategoryTheory.MonoOver A) (CategoryTheory.MonoOver B)} →
              {R : CategoryTheory.Functor (CategoryTheory.MonoOver B) (CategoryTheory.MonoOver A)} →
                (L ⊣ R) → (CategoryTheory.Subobject.lower L ⊣ CategoryTheory.Subobject.lower R)
-- Mathlib.CategoryTheory.Localization.HasLocalization
CategoryTheory.MorphismProperty.HasLocalization.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {D : Type u} →
        [hD : CategoryTheory.Category.{w, u} D] →
          (L : CategoryTheory.Functor C D) → [hL : L.IsLocalization W] → W.HasLocalization
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.ofInv_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (s : Y ⟶ X) (hs : W s),
  (CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).f = CategoryTheory.CategoryStruct.id Y
-- Mathlib.Logic.Equiv.Fintype
Equiv.subtypeCongr.eq_1 : ∀ {α : Type u_9} {p q : α → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q] (e : { x // p x } ≃ { x // q x })
  (f : { x // ¬p x } ≃ { x // ¬q x }),
  e.subtypeCongr f = (Equiv.sumCompl p).symm.trans ((e.sumCongr f).trans (Equiv.sumCompl q))
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.natural_eq_comap : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {β : ι → Type u_3} [inst : (i : ι) → TopologicalSpace (β i)]
  [inst_1 : ∀ (i : ι), TopologicalSpace.MetrizableSpace (β i)] [mβ : (i : ι) → MeasurableSpace (β i)]
  [inst_2 : ∀ (i : ι), BorelSpace (β i)] [inst_3 : Preorder ι] (u : (i : ι) → Ω → β i)
  (hum : ∀ (i : ι), MeasureTheory.StronglyMeasurable (u i)) (i : ι),
  ↑(MeasureTheory.Filtration.natural u hum) i = MeasurableSpace.comap (fun ω j => u (↑j) ω) inferInstance
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Fin.accumulate_invAccumulate : ∀ {n m : ℕ}, m ≤ n → ∀ {s : Fin m → ℕ}, Antitone s → (Fin.accumulate n m) (Fin.invAccumulate n m s) = s
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.comap_map_eq : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (H : Subgroup G),
  Subgroup.comap f (Subgroup.map f H) = H ⊔ f.ker
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_hom : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantFrom i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (i₀ ⟶ i)), (h.isoMap φ hφ).hom = F.map φ
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.boundariesOfIsBoundary₁_coe : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A] (x : G →₀ A) (hx : groupHomology.IsBoundary₁ x),
  ↑(groupHomology.boundariesOfIsBoundary₁ x hx) = x
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.HeapNode.toHeap.go.match_1.splitter : {α : Type u_1} →
  (motive : Batteries.BinomialHeap.Imp.HeapNode α → ℕ → Batteries.BinomialHeap.Imp.Heap α → Sort u_2) →
    (x : Batteries.BinomialHeap.Imp.HeapNode α) →
      (x_1 : ℕ) →
        (x_2 : Batteries.BinomialHeap.Imp.Heap α) →
          ((x : ℕ) → (res : Batteries.BinomialHeap.Imp.Heap α) → motive Batteries.BinomialHeap.Imp.HeapNode.nil x res) →
            ((a : α) →
                (c s : Batteries.BinomialHeap.Imp.HeapNode α) →
                  (n : ℕ) →
                    (res : Batteries.BinomialHeap.Imp.Heap α) →
                      motive (Batteries.BinomialHeap.Imp.HeapNode.node a c s) n res) →
              motive x x_1 x_2
-- Init.Data.SInt.Lemmas
Int64.not_lt : ∀ {a b : Int64}, ¬a < b ↔ b ≤ a
-- Init.Data.SInt.Lemmas
Int64.minValue_le : ∀ (a : Int64), Int64.minValue ≤ a
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.essentiallySmall_unop_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ),
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P.unop ↔
    CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P
-- Mathlib.Algebra.Lie.Quotient
/-- Given a Lie module `M` over a Lie algebra `L`, together with a Lie submodule `N ⊆ M`, there is
a natural bracket action of `L` on the quotient `M/N`.  -/
LieSubmodule.Quotient.actionAsEndoMapBracket : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [inst_4 : LieRingModule L M] →
                (N : LieSubmodule R L M) → [inst_5 : LieAlgebra R L] → [LieModule R L M] → Bracket L (M ⧸ N)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.subtype_comp_d₀₁_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G) (x : ↥A.ρ.invariants),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.d₀₁ A)) ↑x = 0
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
isLocalHom_of_comp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Semiring T]
  (f : R →+* S) (g : S →+* T) [IsLocalHom (g.comp f)], IsLocalHom f
-- Mathlib.Data.List.Cycle
Cycle.next_reverse_eq_prev : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (hs : s.Nodup) (x : α) (hx : x ∈ s),
  s.reverse.next ⋯ x ⋯ = s.prev hs x hx
-- Std.Http.Data.Method
Std.Http.Method.connect.sizeOf_spec : sizeOf Std.Http.Method.connect = 1
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- If two vector fields are `C^n` with `n ≥ m + 1`, then their Lie bracket is `C^m`.  -/
ContDiff.mlieBracket_vectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I (minSmoothness 𝕜 2) M]
  [CompleteSpace E] {m n : ℕ∞} [IsManifold I (↑n + 1) M] {U V : (x : M) → TangentSpace I x},
  (ContMDiff I I.tangent ↑n fun x => ⟨x, U x⟩) →
    (ContMDiff I I.tangent ↑n fun x => ⟨x, V x⟩) →
      minSmoothness 𝕜 (↑m + 1) ≤ ↑n → ContMDiff I I.tangent ↑m fun x₀ => ⟨x₀, VectorField.mlieBracket I U V x₀⟩
-- Mathlib.Order.CompleteLattice.Finset
Finset.iSup_insert_update : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] [inst_1 : DecidableEq α] {x : α} {t : Finset α} (f : α → β)
  {s : β}, x ∉ t → ⨆ i ∈ insert x t, Function.update f x s i = s ⊔ ⨆ i ∈ t, f i
-- Mathlib.Algebra.Order.Monovary
Monovary.pow_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, 0 ≤ f → Monovary f g → ∀ (n : ℕ), Monovary (f ^ n) g
-- Mathlib.Analysis.Calculus.ContDiff.RCLike
/-- If `f` is `C^1` at `x` and `K > ‖fderiv 𝕂 f x‖`, then `f` is `K`-Lipschitz in a neighborhood of
`x`.  -/
ContDiffAt.exists_lipschitzOnWith_of_nnnorm_lt : ∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {E' : Type u_2} [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedSpace 𝕂 E']
  {F' : Type u_3} [inst_3 : NormedAddCommGroup F'] [inst_4 : NormedSpace 𝕂 F'] {f : E' → F'} {x : E'},
  ContDiffAt 𝕂 1 f x → ∀ (K : NNReal), ‖fderiv 𝕂 f x‖₊ < K → ∃ t ∈ nhds x, LipschitzOnWith K f t
-- Mathlib.Algebra.Category.ModuleCat.Products
ModuleCat.ι_coprodIsoDirectSum_hom_apply : ∀ {R : Type u} [inst : Ring R] {ι : Type v} (Z : ι → ModuleCat R) [inst_1 : DecidableEq ι]
  [inst_2 : CategoryTheory.Limits.HasCoproduct Z] (i : ι) (x : ↑(Z i)),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.coprodIsoDirectSum Z).hom)
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι Z i)) x) =
    (DirectSum.lof R ι (fun i => ↑(Z i)) i) x
-- Lean.Elab.AutoBound
/-- Pushes a new variable onto the autoImplicit context, indicating that it needs
to be bound as an implicit parameter.
 -/
Lean.Elab.AutoBoundImplicitContext.push : Lean.Elab.AutoBoundImplicitContext → Lean.Expr → Lean.Elab.AutoBoundImplicitContext
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.hom_hom_leftUnitor : ∀ {R : Type u} [inst : CommRing R] {M : ModuleCat R},
  ModuleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom = ↑(TensorProduct.lid R ↑M)