mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian
SheafOfModules.instAbelian : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (R : CategoryTheory.Sheaf J RingCat) →
        [CategoryTheory.HasSheafify J AddCommGrpCat] →
          [J.WEqualsLocallyBijective AddCommGrpCat] → CategoryTheory.Abelian (SheafOfModules R)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.ofProp_and : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {φ₁ φ₂ : Prop},
  Lean.Order.meet (Lean.Order.CompleteLattice.ofProp φ₁) (Lean.Order.CompleteLattice.ofProp φ₂) =
    Lean.Order.CompleteLattice.ofProp (φ₁ ∧ φ₂)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.mk.injEq : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (carrier : Ideal A)
  (isSubideal : carrier ≤ I) (dpow_mem : ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier, hI.dpow n j ∈ carrier) (carrier_1 : Ideal A)
  (isSubideal_1 : carrier_1 ≤ I) (dpow_mem_1 : ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier_1, hI.dpow n j ∈ carrier_1),
  ({ carrier := carrier, isSubideal := isSubideal, dpow_mem := dpow_mem } =
      { carrier := carrier_1, isSubideal := isSubideal_1, dpow_mem := dpow_mem_1 }) =
    (carrier = carrier_1)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.comap_bot : ∀ {V : Type u_1} {W : Type u_2} (f : V → W), SimpleGraph.comap f (SimpleGraph.emptyGraph W) = SimpleGraph.emptyGraph V
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- A non-unital star subalgebra over a ring is also a `Subring`.  -/
NonUnitalStarSubalgebra.toNonUnitalSubring : {R : Type u} →
  {A : Type v} →
    [inst : CommRing R] →
      [inst_1 : NonUnitalRing A] →
        [inst_2 : Module R A] → [inst_3 : Star A] → NonUnitalStarSubalgebra R A → NonUnitalSubring A
-- Mathlib.Data.Int.Bitwise
Int.bodd_bit : ∀ (b : Bool) (n : ℤ), (Int.bit b n).bodd = b
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.uliftYonedaCompSheafToPresheaf_hom_app_app_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : C) (X_1 : Cᵒᵖ)
  (a :
    (((CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).comp
              (CategoryTheory.sheafToPresheaf J (Type (max v w)))).obj
          X).obj
      X_1),
  (CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaCompSheafToPresheaf.hom.app X).app X_1)) a = a
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of the reverse direction of `Finset.Icc_eq_empty_iff`. -/
Finset.Icc_eq_empty : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], ¬a ≤ b → Finset.Icc a b = ∅
-- Mathlib.Algebra.Order.Group.Abs
/-- `|a - b| < n` if `0 ≤ a < n` and `0 ≤ b < n`.  -/
abs_sub_lt_of_nonneg_of_lt : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b n : G},
  0 ≤ a → a < n → 0 ≤ b → b < n → |a - b| < n
-- Mathlib.Analysis.InnerProductSpace.Positive
InnerProductSpace.isPositive_rankOne_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), (((InnerProductSpace.rankOne 𝕜) x) x).IsPositive
-- Mathlib.Topology.Instances.CantorSet
ofDigits_cantorToTernary : ∀ {x : ℝ}, x ∈ cantorSet → Real.ofDigits (cantorToTernary x).get = x
-- Mathlib.Order.CompleteLattice.Basic
Antitone.iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : Preorder α] [inst_1 : CompleteLattice β] {f : ι → α → β},
  (∀ (i : ι), Antitone (f i)) → Antitone (⨆ i, f i)
-- Std.Sync.Semaphore
/-- Requests one permit.
Returns a promise that resolves once the permit is acquired.
 -/
Std.Semaphore.acquire : Std.Semaphore → BaseIO (IO.Promise Unit)
-- Mathlib.MeasureTheory.Measure.Real
/-- **Alias** of `MeasureTheory.measureReal_sdiff_le_iff_le_add`. -/
MeasureTheory.measureReal_diff_le_iff_le_add : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s →
    s ⊆ t →
      ∀ (ε : ℝ),
        autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_sdiff_le_iff_le_add._auto_1 →
          (μ.real (t \ s) ≤ ε ↔ μ.real t ≤ μ.real s + ε)
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.copy.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (f : ZeroHom M N) (f' : M → N) (h : f' = ⇑f),
  f.copy f' h = { toFun := f', map_zero' := ⋯ }
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instInhabitedPublishDiagnosticsParams : Inhabited Lean.Lsp.PublishDiagnosticsParams
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.toAffineMap : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      {P : Type u_10} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V] →
              [inst_2 : NormedSpace 𝕜 V] →
                [inst_3 : PseudoMetricSpace P] →
                  [inst_4 : NormedAddTorsor V P] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] → [inst_8 : NormedAddTorsor V₂ P₂] → (P →ᵃⁱ[𝕜] P₂) → P →ᵃ[𝕜] P₂
-- Init.Data.SInt.Lemmas
Int32.add_left_neg : ∀ (a : Int32), -a + a = 0
-- Mathlib.Order.RelIso.Basic
/-- **Alias** of `RelEmbedding.trichotomous`. -/
RelEmbedding.isTrichotomous : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (x : r ↪r s) [Std.Trichotomous s],
  Std.Trichotomous r
-- Lean.Environment
Lean.Kernel.Diagnostics.mk : Lean.PHashMap Lean.Name ℕ → Bool → Lean.Kernel.Diagnostics
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.flipEquivalenceCounitIso_hom_app_f_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : HomologicalComplex₂ C c₂ c₁)
  (i : I₂) (i_1 : I₁),
  (((HomologicalComplex₂.flipEquivalenceCounitIso C c₁ c₂).hom.app X).f i).f i_1 =
    CategoryTheory.CategoryStruct.id ((X.X i).X i_1)
-- Init.Data.UInt.Lemmas
UInt32.toNat_ofNatClamp_of_lt : ∀ {n : ℕ}, n < UInt32.size → (UInt32.ofNatClamp n).toNat = n
-- Mathlib.NumberTheory.Ostrowski
_private.Mathlib.NumberTheory.Ostrowski.0.Rat.AbsoluteValue.param_upperbound : ∀ {f : AbsoluteValue ℚ ℝ} {m n : ℕ},
  1 < m →
    1 < n →
      (¬∀ (n : ℕ), f ↑n ≤ 1) → ∀ {k : ℕ}, k ≠ 0 → f ↑n ≤ (↑m * f ↑m / (f ↑m - 1)) ^ (↑k)⁻¹ * f ↑m ^ Real.logb ↑m ↑n
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.iteratedFDerivLM_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n k : ℕ∞} {K : TopologicalSpace.Compacts E} {i : ℕ}
  (f : ContDiffMapSupportedIn E F n K),
  ⇑((ContDiffMapSupportedIn.iteratedFDerivLM 𝕜 n k i) f) = if k + ↑i ≤ n then iteratedFDeriv ℝ i ⇑f else 0
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitHomIsoLimitYoneda'_hom_comp_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor Iᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I (Type u₂)] (A : C) (i : I),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda' F A).hom
      (CategoryTheory.Limits.limit.π (F.rightOp.comp (CategoryTheory.yoneda.obj A)) i) =
    (CategoryTheory.yoneda.obj A).map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The construction `CatCommSqOver.transform` respects vertical composition
of `CatCospanTransform`s.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {A₁ : Type u₄} →
                  {B₁ : Type u₅} →
                    {C₁ : Type u₆} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] →
                            {F₁ : CategoryTheory.Functor A₁ B₁} →
                              {G₁ : CategoryTheory.Functor C₁ B₁} →
                                {A₂ : Type u₇} →
                                  {B₂ : Type u₈} →
                                    {C₂ : Type u₉} →
                                      [inst_6 : CategoryTheory.Category.{v₇, u₇} A₂] →
                                        [inst_7 : CategoryTheory.Category.{v₈, u₈} B₂] →
                                          [inst_8 : CategoryTheory.Category.{v₉, u₉} C₂] →
                                            {F₂ : CategoryTheory.Functor A₂ B₂} →
                                              {G₂ : CategoryTheory.Functor C₂ B₂} →
                                                (X : Type u₁₀) →
                                                  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} X] →
                                                    (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) →
                                                      (ψ' : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂) →
                                                        (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform
                                                                X).obj
                                                            (ψ.comp ψ') ≅
                                                          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform
                                                                    X).obj
                                                                ψ).comp
                                                            ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform
                                                                  X).obj
                                                              ψ')
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} SemiRingCat
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.responseBody.sizeOf_spec : ∀ {β : Type} [inst : SizeOf β] (x : Option Std.Http.Chunk),
  sizeOf (Std.Http.Server.Connection.Recv.responseBody✝ x) = 1 + sizeOf x
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.instAddAction : {ι : Type u_1} →
  {M : Type u_2} → {α : ι → Type u_4} → {m : AddMonoid M} → [(i : ι) → AddAction M (α i)] → AddAction M ((i : ι) × α i)
-- Mathlib.Analysis.RCLike.Basic
RCLike.mul_re_ax : ∀ {K : semiOutParam (Type u_1)} [self : RCLike K] (z w : K),
  RCLike.re (z * w) = RCLike.re z * RCLike.re w - RCLike.im z * RCLike.im w
-- Init.Data.String.Lemmas.Pattern.Pred
_private.Init.Data.String.Slice.0.String.Slice.Pos.skipWhile.match_1.congr_eq_1 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (x : Option s.Pos)
  (h_1 : (nextCurr : s.Pos) → motive (some nextCurr)) (h_2 : Unit → motive none) (nextCurr : s.Pos),
  x = some nextCurr →
    (match x with
      | some nextCurr => h_1 nextCurr
      | none => h_2 ()) ≍
      h_1 nextCurr
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsBlock.preimage : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X} {H : Type u_3} {Y : Type u_4}
  [inst_2 : Group H] [inst_3 : MulAction H Y] {φ : H → G} (j : Y →ₑ[φ] X),
  MulAction.IsBlock G B → MulAction.IsBlock H (⇑j ⁻¹' B)
-- Mathlib.Analysis.Calculus.Deriv.ZPow
hasDerivAt_zpow : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (m : ℤ) (x : 𝕜),
  x ≠ 0 ∨ 0 ≤ m → HasDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
-- Mathlib.CategoryTheory.Sites.Subsheaf
/-- The mono factorization given by `image_sheaf` for a morphism.  -/
CategoryTheory.imageMonoFactorization : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {F F' : CategoryTheory.Sheaf J (Type w)} → (f : F ⟶ F') → CategoryTheory.Limits.MonoFactorisation f
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- The vector given in `PiLp` by being `a : β i` at coordinate `i : ι` and `0 : β j` at
all other coordinates `j`.  -/
PiLp.single : (p : ENNReal) →
  {ι : Type u_2} → {β : ι → Type u_4} → [DecidableEq ι] → [(i : ι) → Zero (β i)] → (i : ι) → β i → PiLp p β
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.toLinearEquiv_inj : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (φ ψ : σ.Equiv ρ), φ.toLinearEquiv = ψ.toLinearEquiv ↔ φ = ψ
-- Mathlib.Computability.TuringMachine.Config
/-- The semantics of the `Code` primitives, as partial functions `List ℕ →. List ℕ`.
By convention, functions that return a single result return a singleton `[n]`,
or in some cases `n :: v` where `v` will be ignored by a subsequent function.

* `zero'` appends a `0` to the input. That is, `zero' v = 0 :: v`.
* `succ` returns the successor of the head of the input, defaulting to zero if there is no head:
  * `succ [] = [1]`
  * `succ (n :: v) = [n + 1]`
* `tail` returns the tail of the input
  * `tail [] = []`
  * `tail (n :: v) = v`
* `cons f fs` calls `f` and `fs` on the input and conses the results:
  * `cons f fs v = (f v).head :: fs v`
* `comp f g` calls `f` on the output of `g`:
  * `comp f g v = f (g v)`
* `case f g` cases on the head of the input, calling `f` or `g` depending on whether it is zero or
  a successor (similar to `Nat.casesOn`).
  * `case f g [] = f []`
  * `case f g (0 :: v) = f v`
  * `case f g (n+1 :: v) = g (n :: v)`
* `fix f` calls `f` repeatedly, using the head of the result of `f` to decide whether to call `f`
  again or finish:
  * `fix f v = []` if `f v = []`
  * `fix f v = w` if `f v = 0 :: w`
  * `fix f v = fix f w` if `f v = n+1 :: w` (the exact value of `n` is discarded)
 -/
Turing.ToPartrec.Code.eval : Turing.ToPartrec.Code → List ℕ →. List ℕ
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.Event.continue.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction}, sizeOf Std.Http.Protocol.H1.Event.continue = 1
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- Extend the inverse operation on `α` to `WithZero α` by sending `0` to `0`.  -/
WithZero.inv : {α : Type u_1} → [Inv α] → Inv (WithZero α)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.revAll_prop_eq : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice}, s.revAll P = s.copy.toList.all fun x => decide (P x)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
/-- A family of elements in the `realSpace K` formed of the image of the fundamental units
and the vector `(mult w)_w`. This family is in fact a basis of `realSpace K`, see `completeBasis`.
 -/
NumberField.mixedEmbedding.fundamentalCone.completeFamily : (K : Type u_1) →
  [inst : Field K] → [NumberField K] → NumberField.InfinitePlace K → NumberField.mixedEmbedding.realSpace K
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.leftUnitorEquivalence_inverse : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.prod.leftUnitorEquivalence C).inverse = CategoryTheory.prod.leftInverseUnitor C
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_inter_eq_size_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  (∀ a ∈ t₂, a ∈ t₁) → (t₁ ∩ t₂).size = t₂.size
-- Lean.LibrarySuggestions.SymbolFrequency
/-- A cached version of the local symbol frequency map.

Note that the local symbol frequency map changes during elaboration of a file,
so if this is called at different times it may give the wrong result.
The intended use case is that it is only called by environment extension export functions,
i.e. after all declarations have been elaborated.
 -/
_private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.LibrarySuggestions.cachedLocalSymbolFrequencyMap : Lean.MetaM (Lean.NameMap ℕ)
-- Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
/-- The canonical isomorphism
`DerivedCategory.singleFunctor C n ⋙ DerivedCategory.homologyFunctor C n ≅ 𝟭 C`  -/
DerivedCategory.singleFunctorCompHomologyFunctorIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        (n : ℤ) →
          (DerivedCategory.singleFunctor C n).comp (DerivedCategory.homologyFunctor C n) ≅ CategoryTheory.Functor.id C
-- Init.Data.SInt.Lemmas
Int32.ofInt_int64ToInt : ∀ (x : Int64), Int32.ofInt x.toInt = x.toInt32
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.generateFrom_insert_empty : ∀ {α : Type u_1} (S : Set (Set α)), MeasurableSpace.generateFrom (insert ∅ S) = MeasurableSpace.generateFrom S
-- Mathlib.Topology.Algebra.MulAction
Filter.Tendsto.smul_const : ∀ {M : Type u_1} {X : Type u_2} {α : Type u_4} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : SMul M X] [ContinuousSMul M X] {f : α → M} {l : Filter α} {c : M},
  Filter.Tendsto f l (nhds c) → ∀ (a : X), Filter.Tendsto (fun x => f x • a) l (nhds (c • a))
-- Lean.Level
Lean.Level.hasParam : Lean.Level → Bool
-- Init.Data.List.SplitOn.Lemmas
List.splitOnPPrepend_eq_modifyHead : ∀ {α : Type u_1} {p : α → Bool} {xs acc : List α},
  List.splitOnPPrepend p xs acc = List.modifyHead (fun x => acc.reverse ++ x) (List.splitOnP p xs)
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.ofUnits_injective : ∀ {M : Type u_1} [inst : Monoid M], Function.Injective Subgroup.ofUnits
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.coe_unop : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Subring Rᵐᵒᵖ), ↑S.unop = MulOpposite.op ⁻¹' ↑S
-- Mathlib.MeasureTheory.Measure.NullMeasurable
/-- A function `f : α → β` is null measurable if the preimage of a measurable set is a null
measurable set.

A similar notion is `AEMeasurable`. That notion is equivalent to `NullMeasurable` if
the σ-algebra on the codomain is countably generated, but stronger in general.  -/
MeasureTheory.NullMeasurable : {α : Type u_2} →
  {β : Type u_3} →
    [m : MeasurableSpace α] →
      [MeasurableSpace β] → (α → β) → autoParam (MeasureTheory.Measure α) MeasureTheory.NullMeasurable._auto_1 → Prop
-- Lean.Elab.PreDefinition.Structural.Eqns
_private.Lean.Elab.PreDefinition.Structural.Eqns.0.Lean.Elab.Structural.deltaRHS? : Lean.MVarId → Lean.Name → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the sign of the angle between three points is positive, the last two points are not
equal.  -/
EuclideanGeometry.right_ne_of_oangle_sign_eq_one : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign = 1 → p₃ ≠ p₂
-- Init.Data.Ord.Vector
Vector.compareLex : {α : Type u_1} → {n : ℕ} → (α → α → Ordering) → Vector α n → Vector α n → Ordering
-- Mathlib.Algebra.Group.Center
Set.add_mem_addCentralizer : ∀ {M : Type u_1} {S : Set M} [inst : AddSemigroup M] {a b : M},
  a ∈ S.addCentralizer → b ∈ S.addCentralizer → a + b ∈ S.addCentralizer
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getEntryLT_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} {h' : ∃ a ∈ t₁, cmp a k = Ordering.lt} (h : t₁.Equiv t₂), t₁.getEntryLT k h' = t₂.getEntryLT k ⋯
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestMatchAt_of_ofSliceTo : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {p : s.Pos}
  {startPos endPos : (s.sliceTo p).Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt pat (String.Slice.Pos.ofSliceTo startPos)
      (String.Slice.Pos.ofSliceTo endPos) →
    String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans_target : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ),
  (e.trans e').target = e'.target ∩ ↑e'.symm ⁻¹' e.target
-- Mathlib.LinearAlgebra.Charpoly.Basic
LinearMap.charpoly.eq_1 : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] (f : M →ₗ[R] M),
  f.charpoly = ((LinearMap.toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M)) f).charpoly
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_eq_of_brange_eq : ∀ {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}}
  {g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}},
  {o_1 | ∃ i, ∃ (hi : i < o), f i hi = o_1} = {o | ∃ i, ∃ (hi : i < o'), g i hi = o} → o.blsub f = o'.blsub g
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.coe_mkHomeomorph : ∀ {M : Type u_1} [inst : TopologicalSpace M], ⇑DomMulAct.mkHomeomorph = ⇑DomMulAct.mk
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.commRing : {d : ℤ} → CommRing (ℤ√d)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_mem : k ∈ m₁ \ m₂}, (m₁ \ m₂).get k h_mem = m₁.get k ⋯
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.lie_e_f_mul_ω : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : Fintype ι] (i j : ↥b.support),
  ⁅RootPairing.GeckConstruction.e i, RootPairing.GeckConstruction.f j⁆ * RootPairing.GeckConstruction.ω b =
    -RootPairing.GeckConstruction.ω b * ⁅RootPairing.GeckConstruction.e j, RootPairing.GeckConstruction.f i⁆
-- Init.Data.SInt.Bitwise
ISize.shiftLeft_or : ∀ {a b c : ISize}, (a ||| b) <<< c = a <<< c ||| b <<< c
-- Mathlib.Logic.Equiv.Prod
Equiv.piSplitAt_symm_apply : ∀ {α : Type u_9} [inst : DecidableEq α] (i : α) (β : α → Type u_10) (f : β i × ((j : { j // j ≠ i }) → β ↑j)) (j : α),
  (Equiv.piSplitAt i β).symm f j = if h : j = i then ⋯ ▸ f.1 else f.2 ⟨j, h⟩
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.Iterators.Types.DropWhile.instIterator.match_1.eq_1 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (P out).Property → Sort u_3) (h'' : (P out).Property { down := true })
  (h_1 : (h'' : (P out).Property { down := true }) → motive ⟨{ down := true }, h''⟩)
  (h_2 : (h'' : (P out).Property { down := false }) → motive ⟨{ down := false }, h''⟩),
  (match ⟨{ down := true }, h''⟩ with
    | ⟨{ down := true }, h''⟩ => h_1 h''
    | ⟨{ down := false }, h''⟩ => h_2 h'') =
    h_1 h''
-- Mathlib.NumberTheory.LSeries.Injectivity
_private.Mathlib.NumberTheory.LSeries.Injectivity.0.cpow_mul_div_cpow_eq_div_div_cpow : ∀ (m n : ℕ) (z : ℂ) (x : ℝ), (↑n + 1) ^ ↑x * (z / ↑m ^ ↑x) = z / (↑m / (↑n + 1)) ^ ↑x
-- Mathlib.GroupTheory.NoncommPiCoprod
Subgroup.injective_noncommPiCoprod_of_iSupIndep : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} [inst_1 : Fintype ι]
  {hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y},
  iSupIndep H → Function.Injective ⇑(Subgroup.noncommPiCoprod hcomm)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.re_ofNat : ∀ {d : ℤ} (n : ℕ) [inst : n.AtLeastTwo], (OfNat.ofNat n).re = ↑n