mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Notation
/-- The standardized "high" priority `high = 10000`, for things that should be higher than default priority.  -/
prioHigh : Lean.ParserDescr
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.rightCont_def : ∀ {Ω : Type u_3} {ι : Type u_4} {m : MeasurableSpace Ω} [inst : PartialOrder ι] (𝓕 : MeasureTheory.Filtration ι m),
  𝓕.rightCont =
    { seq := fun i => if (nhdsWithin i (Set.Ioi i)).NeBot then ⨅ j, ⨅ (_ : j > i), ↑𝓕 j else ↑𝓕 i, mono' := ⋯,
      le' := ⋯ }
-- Mathlib.Data.Matrix.PEquiv
PEquiv.single_mul_single_of_ne : ∀ {k : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype n] [inst_1 : DecidableEq n]
  [inst_2 : DecidableEq k] [inst_3 : DecidableEq m] [inst_4 : NonAssocSemiring α] {b₁ b₂ : n},
  b₁ ≠ b₂ → ∀ (a : m) (c : k), (PEquiv.single a b₁).toMatrix * (PEquiv.single b₂ c).toMatrix = 0
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
/-- If `P` lies over `p`, `p` is a minimal prime over `I` and the image of `P` is
a minimal prime over the image of `J` in `S ⧸ p S`, then `P` is a minimal prime
over `I S ⊔ J`.  -/
Ideal.map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S] {I p : Ideal R}
  {P : Ideal S} [P.IsPrime] [P.LiesOver p],
  p ∈ I.minimalPrimes →
    ∀ {J : Ideal S},
      J ≤ P →
        Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) P ∈
            (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) J).minimalPrimes →
          P ∈ (Ideal.map (algebraMap R S) I ⊔ J).minimalPrimes
-- Mathlib.Order.PFilter
Order.IsPFilter.of_def : ∀ {P : Type u_1} [inst : Preorder P] {F : Set P},
  F.Nonempty → DirectedOn (fun x1 x2 => x1 ≥ x2) F → (∀ {x y : P}, x ≤ y → x ∈ F → y ∈ F) → Order.IsPFilter F
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.μ_natural_right_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.LaxMonoidal] {X Y : C} (X' : C) (f : X ⟶ Y) {Z : D}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X' Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X' Y) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X' X)
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f)) h)
-- Mathlib.Topology.Algebra.Algebra
Subalgebra.topologicalClosure_minimal : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsSemitopologicalSemiring A] {s t : Subalgebra R A},
  s ≤ t → IsClosed ↑t → s.topologicalClosure ≤ t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.keysArray_insertIfNew_perm : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : BEq α] [Std.TransOrd α]
  [Std.LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.keysArray.Perm
    (if Std.DTreeMap.Internal.Impl.contains k t = true then t.keysArray else t.keysArray.push k)
-- Mathlib.Algebra.Homology.Monoidal
HomologicalComplex.leftUnitor'_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive]
  [inst_5 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] {I : Type u_2}
  [inst_6 : AddMonoid I] {c : ComplexShape I} [inst_7 : c.TensorSigns] (K : HomologicalComplex C c)
  [inst_8 : DecidableEq I]
  [inst_9 :
    ∀ (X₂ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)]
  (i : I),
  K.leftUnitor'.inv i =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (K.X i)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (HomologicalComplex.singleObjXSelf c 0 (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (K.X i))
        ((HomologicalComplex.tensorUnit C c).ιTensorObj K 0 i i ⋯))
-- Mathlib.Util.Export
_private.Mathlib.Util.Export.0.Lean.Export.exportDef.indbody : Lean.Name → String → Lean.ExportM String
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
/-- A version of `WithBot.map` for `ZeroHom`s  -/
ZeroHom.withBotMap : {M : Type u_1} → {N : Type u_2} → [inst : Zero M] → [inst_1 : Zero N] → ZeroHom M N → ZeroHom (WithBot M) (WithBot N)
-- Mathlib.Order.BooleanSubalgebra
/-- The top Boolean subalgebra is isomorphic to the original Boolean algebra.

This is the Boolean subalgebra version of `Equiv.Set.univ α`.  -/
BooleanSubalgebra.topEquiv : {α : Type u_2} → [inst : BooleanAlgebra α] → ↥⊤ ≃o α
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of a quotient of `G` is less or equal the nilpotency class
of `G`.  -/
AddGroup.nilpotencyClass_quotient_le : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [inst_1 : H.Normal] [_h : AddGroup.IsNilpotent G],
  AddGroup.nilpotencyClass (G ⧸ H) ≤ AddGroup.nilpotencyClass G
-- Std.Http.Data.Headers.Basic
Std.Http.Header.instReprContentLength.repr : Std.Http.Header.ContentLength → ℕ → Std.Format
-- Mathlib.CategoryTheory.Types.Basic
/-- Any isomorphism between types gives an equivalence.  -/
CategoryTheory.Iso.toEquiv : {X Y : Type u} → (X ≅ Y) → X ≃ Y
-- Mathlib.CategoryTheory.Types.Basic
/-- A morphism in `Type u` is an isomorphism if and only if it is bijective.  -/
CategoryTheory.isIso_iff_bijective : ∀ {X Y : Type u} (f : X ⟶ Y), CategoryTheory.IsIso f ↔ Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.star_mul_self : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  (A : ↥(Matrix.unitaryGroup n α)), star ↑A * ↑A = 1
-- Init.Data.SInt.Lemmas
Int64.toBitVec_one : Int64.toBitVec 1 = 1#64
-- Mathlib.Topology.Order.IsNormal
Order.IsNormal.continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [WellFoundedLT α] [inst_2 : TopologicalSpace α] [OrderTopology α]
  [inst_4 : LinearOrder β] [WellFoundedLT β] [inst_6 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Order.IsNormal f → Continuous f
-- Mathlib.Data.ZMod.Aut
ZMod.AddAutEquivUnits_symm_apply : ∀ (n : ℕ) (x : Additive (ZMod n)ˣ), (ZMod.AddAutEquivUnits n).symm x = AddAut.mulLeft (Additive.toMul x)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.instIteratorIteratorIdOfUpwardEnumerableOfDecidableLT.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α],
  Std.Rxo.instIteratorIteratorIdOfUpwardEnumerableOfDecidableLT =
    { IsPlausibleStep := fun it step => step = Std.Rxo.Iterator.Monadic.step it,
      step := fun it => pure (Std.Shrink.deflate ⟨Std.Rxo.Iterator.Monadic.step it, ⋯⟩) }
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.monodromy_bijective : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) {x y : X} (γ : Path.Homotopic.Quotient x y), Function.Bijective (cov.monodromy γ)
-- Lean.Data.LBool
Lean.LBool.false : Lean.LBool
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.uniformContinuous_toCompacts : ∀ {α : Type u_1} [inst : UniformSpace α], UniformContinuous TopologicalSpace.NonemptyCompacts.toCompacts
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {D : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D] (L : CategoryTheory.Functor C₂ D) [inst_3 : L.IsLocalization W₂]
  {X₂ : C₂} {X₃ : D} (y : L.obj X₂ ⟶ X₃) (R : Φ.RightResolution X₂),
  (CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution Φ L y).obj R =
    CategoryTheory.CostructuredArrow.mk
      (CategoryTheory.StructuredArrow.homMk
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.isoOfHom L W₂ R.w ⋯).inv y) ⋯)
-- Mathlib.Order.SemiconjSup
/-- We say that `g : β → α` is an order right adjoint function for `f : α → β` if it sends each `y`
to a least upper bound for `{x | f x ≤ y}`. If `α` is a partial order, and `f : α → β` has
a right adjoint, then this right adjoint is unique.  -/
IsOrderRightAdjoint : {α : Type u_1} → {β : Type u_2} → [Preorder α] → [Preorder β] → (α → β) → (β → α) → Prop
-- Mathlib.CategoryTheory.Action.Concrete
Action.instMulAction : {V : Type (u + 1)} →
  [inst : CategoryTheory.LargeCategory V] →
    {FV : V → V → Type u_1} →
      {CV : V → Type u_2} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            {G : Type u_3} → [inst_3 : Monoid G] → (X : Action V G) → MulAction G (CategoryTheory.ToType X)
-- Std.Http.Protocol.H1.Message
Std.Http.Protocol.H1.Direction.receiving.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Direction.receiving = 1
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.pd_inv : ∀ (l : Type u_4) (R : Type u₂) [inst : DecidableEq l] [inst_1 : CommRing R] [inst_2 : Fintype l]
  [inst_3 : Invertible 2], LieAlgebra.Orthogonal.PD l R * ⅟2 • (LieAlgebra.Orthogonal.PD l R).transpose = 1
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.equalizerSieve_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] (J : CategoryTheory.GrothendieckTopology C)
  {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) [CategoryTheory.Presheaf.IsLocallyInjective J φ] {X : Cᵒᵖ}
  (x y : CategoryTheory.ToType (F₁.obj X)),
  (CategoryTheory.ConcreteCategory.hom (φ.app X)) x = (CategoryTheory.ConcreteCategory.hom (φ.app X)) y →
    CategoryTheory.Presheaf.equalizerSieve x y ∈ J (Opposite.unop X)
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.IsDynCoverOf.nonempty_inter : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F : Set X} {n : ℕ} [U.IsSymm] {s : Finset X},
  Dynamics.IsDynCoverOf T F U n ↑s →
    ∃ t,
      Dynamics.IsDynCoverOf T F U n ↑t ∧
        t.card ≤ s.card ∧ ∀ x ∈ t, (UniformSpace.ball x (Dynamics.dynEntourage T U n) ∩ F).Nonempty
-- Aesop.Forward.State
/-- Returns `true` if `h` is the hyp `fvarId` or is a pattern substitution
containing `fvarId`.  -/
Aesop.Hyp.containsHyp : Lean.FVarId → Aesop.Hyp → Bool
-- Mathlib.Logic.Equiv.Set
Equiv.Set.rangeInl_symm_apply_coe : ∀ (α : Type u_3) (β : Type u_4) (x : α), ↑((Equiv.Set.rangeInl α β).symm x) = Sum.inl x
-- Init.Ext
Thunk.ext : ∀ {α : Type u_1} {a b : Thunk α}, a.get = b.get → a = b
-- Mathlib.Algebra.Order.SuccPred
Order.pred_eq_sub_one : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Sub α] [inst_2 : One α] [inst_3 : PredSubOrder α] (x : α),
  Order.pred x = x - 1
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
isIntegral_one : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B], IsIntegral R 1
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.map_smul_left : ∀ {R : Type uR} {A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ}
  [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : IsScalarTower R A M]
  [inst_9 : AddCommMonoid N] [inst_10 : Module R N] [inst_11 : AddCommMonoid P] [inst_12 : Module R P]
  [inst_13 : Module A P] [inst_14 : IsScalarTower R A P] [inst_15 : AddCommMonoid Q] [inst_16 : Module R Q]
  [inst_17 : Module B P] [inst_18 : IsScalarTower R B P] [inst_19 : SMulCommClass A B P] (b : B) (f : M →ₗ[A] P)
  (g : N →ₗ[R] Q), TensorProduct.AlgebraTensorModule.map (b • f) g = b • TensorProduct.AlgebraTensorModule.map f g
-- Mathlib.Algebra.Group.ULift
ULift.div_down : ∀ {α : Type u} {x y : ULift.{w, u} α} [inst : Div α], (x / y).down = x.down / y.down
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.ite_else_not_ite' : ∀ {w : ℕ} (c0 c1 : Bool) {a b : BitVec w},
  (bif c0 then a else ~~~bif c1 then ~~~a else b) = bif !c0 && !c1 then ~~~b else a
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.map_eq_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E₂] [inst_3 : Module R₂ E₂] [inst_4 : NormedAddCommGroup F]
  [inst_5 : Module R F] (f₁ : F →ₛₗᵢ[σ₁₂] E₂) {x y : F}, f₁ x = f₁ y ↔ x = y
-- Mathlib.NumberTheory.ZetaValues
/-- The Fourier coefficients of `B₀(x) = 1`.  -/
bernoulli_zero_fourier_coeff : ∀ {n : ℤ}, n ≠ 0 → bernoulliFourierCoeff 0 n = 0
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.instSingletonProdOfEquivBEqOfLawfulHashable : {α : Type u} →
  {β : Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Singleton (α × β) (Std.ExtHashMap α β)
-- Mathlib.RingTheory.Polynomial.Basic
Ideal.mem_leadingCoeffNth : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal (Polynomial R)) (n : ℕ) (x : R),
  x ∈ I.leadingCoeffNth n ↔ ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.SimpCongrTheorem.theoremName : Lean.Meta.SimpCongrTheorem → Lean.Name
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableSMul₂_of_mul : ∀ (M : Type u_2) [inst : Mul M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M], MeasurableSMul₂ M M
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.Int8.toBitVec_cond : ∀ {c : Bool} {t e : Int8}, (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
-- Mathlib.Analysis.Normed.Operator.Basic
/-- `ContinuousLinearMap.restrictScalars` as a `LinearIsometry`.  -/
ContinuousLinearMap.restrictScalarsIsometry : (𝕜 : Type u_1) →
  (E : Type u_4) →
    (Fₗ : Type u_6) →
      [inst : SeminormedAddCommGroup E] →
        [inst_1 : SeminormedAddCommGroup Fₗ] →
          [inst_2 : NontriviallyNormedField 𝕜] →
            [inst_3 : NormedSpace 𝕜 E] →
              [inst_4 : NormedSpace 𝕜 Fₗ] →
                (𝕜' : Type u_9) →
                  [inst_5 : NontriviallyNormedField 𝕜'] →
                    [inst_6 : NormedAlgebra 𝕜' 𝕜] →
                      [inst_7 : NormedSpace 𝕜' E] →
                        [IsScalarTower 𝕜' 𝕜 E] →
                          [inst_9 : NormedSpace 𝕜' Fₗ] →
                            [IsScalarTower 𝕜' 𝕜 Fₗ] →
                              (𝕜'' : Type u_10) →
                                [inst_11 : Ring 𝕜''] →
                                  [inst_12 : Module 𝕜'' Fₗ] →
                                    [inst_13 : ContinuousConstSMul 𝕜'' Fₗ] →
                                      [inst_14 : SMulCommClass 𝕜 𝕜'' Fₗ] →
                                        [inst_15 : SMulCommClass 𝕜' 𝕜'' Fₗ] → (E →L[𝕜] Fₗ) →ₗᵢ[𝕜''] E →L[𝕜'] Fₗ
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
LineDifferentiableWithinAt.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {s : Set E}
  {x v : E}, LineDifferentiableWithinAt 𝕜 f s x v → ∀ (c : 𝕜), LineDifferentiableWithinAt 𝕜 f s x (c • v)
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IccExtend_of_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} (h : a ≤ b) {x : α} (f : ↑(Set.Icc a b) → β)
  (hx : x ∈ Set.Icc a b), Set.IccExtend h f x = f ⟨x, hx⟩
-- Mathlib.Algebra.Group.Pi.Basic
Pi.mulOneClass.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → MulOneClass (f i)],
  Pi.mulOneClass = { toOne := Pi.instOne, toMul := Pi.instMul, one_mul := ⋯, mul_one := ⋯ }
-- Mathlib.Topology.Sets.Opens
/-- A version of `Set.inclusion` not requiring definitional abuse  -/
TopologicalSpace.Opens.inclusion : {α : Type u_2} → [inst : TopologicalSpace α] → {U V : TopologicalSpace.Opens α} → U ≤ V → ↥U → ↥V
-- Init.Control.Lawful.Instances
Option.elimM.eq_1 : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] (x : m (Option α)) (y : m β) (z : α → m β),
  Option.elimM x y z = do
    let __do_lift ← x
    __do_lift.elim y z
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
/-- A normed additive commutative group structure on `C⋆ᵐᵒᵈ(A, E × F)` with the wrong topology,
uniformity and bornology. This is only used to build the instance with the correct forgetful
inheritance data.  -/
WithCStarModule.normedAddCommGroupProdAux : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      {E : Type u_2} →
        {F : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : Module ℂ E] →
              [inst_4 : SMul A E] →
                [inst_5 : NormedAddCommGroup F] →
                  [inst_6 : Module ℂ F] →
                    [inst_7 : SMul A F] →
                      [CStarModule A E] →
                        [CStarModule A F] → [StarOrderedRing A] → NormedAddCommGroup (WithCStarModule A (E × F))
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.equivNum_apply : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsDomain R] [inst_4 : Module.IsTorsionFree R P] [inst_5 : Nontrivial P] {I : FractionalIdeal S P}
  (h_nz : ↑I.den ≠ 0) (x : ↥I), (algebraMap R P) ↑((FractionalIdeal.equivNum h_nz) x) = I.den • ↑x
-- Lean.Elab.Tactic.LibrarySearch
Lean.Elab.LibrarySearch.evalExact : Lean.Elab.Tactic.Tactic
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.intCast_def' : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {B : Type u_3}
  [inst_3 : Ring B] [inst_4 : Algebra R B] (z : ℤ), ↑z = 1 ⊗ₜ[R] ↑z
-- Mathlib.Algebra.Group.Int.Defs
Int.instAddCommMonoid : AddCommMonoid ℤ
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- Suppose we have a square of 1-morphisms (where the top and bottom are adjunctions `l₁ ⊣ r₁`
and `l₂ ⊣ r₂` respectively).
```
      c ↔ d
    g ↓   ↓ h
      e ↔ f
```

Then we have a bijection between 2-morphisms `g ≫ l₂ ⟶ l₁ ≫ h` and
`r₁ ≫ g ⟶ h ≫ r₂`. This can be seen as a bijection of the 2-cells:

```
         l₁                  r₁
      c --→ d             c ←-- d
    g ↓  ↗  ↓ h         g ↓  ↘  ↓ h
      e --→ f             e ←-- f
         l₂                  r₂
```

Note that if one of the 2-morphisms is an iso, it does not imply the other is an iso.
 -/
CategoryTheory.Bicategory.mateEquiv : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {c d e f : B} →
      {g : c ⟶ e} →
        {h : d ⟶ f} →
          {l₁ : c ⟶ d} →
            {r₁ : d ⟶ c} →
              {l₂ : e ⟶ f} →
                {r₂ : f ⟶ e} →
                  CategoryTheory.Bicategory.Adjunction l₁ r₁ →
                    CategoryTheory.Bicategory.Adjunction l₂ r₂ →
                      (CategoryTheory.CategoryStruct.comp g l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ h) ≃
                        (CategoryTheory.CategoryStruct.comp r₁ g ⟶ CategoryTheory.CategoryStruct.comp h r₂)
-- Lean.Util.ReplaceLevel
Lean.Expr.ReplaceLevelImpl.State.keys : Lean.Expr.ReplaceLevelImpl.State → Array Lean.Expr
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.mem_support_normalize_iff : ∀ {α : Type u_1} {f : α → ENNReal} (hf0 : tsum f ≠ 0) (hf : tsum f ≠ ⊤) (a : α),
  a ∈ (PMF.normalize f hf0 hf).support ↔ f a ≠ 0
-- Mathlib.Computability.Reduce
/-- **Alias** of `stdRefl_manyOneReducible`. -/
reflexive_manyOneReducible : ∀ {α : Type u_1} [inst : Primcodable α], Std.Refl ManyOneReducible
-- Mathlib.Data.Vector.Defs
/-- Take `i` elements from a vector of length `n`; we can have `i > n`.  -/
List.Vector.take : {α : Type u_1} → {n : ℕ} → (i : ℕ) → List.Vector α n → List.Vector α (min i n)
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapₗ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapₗ F).app X =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom
-- Mathlib.Algebra.Lie.Loop
LieAlgebra.LoopAlgebra.toFinsupp.eq_1 : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieAlgebra.LoopAlgebra.toFinsupp R A L = TensorProduct.equivFinsuppOfBasisLeft (AddMonoidAlgebra.basis A R)
-- Mathlib.Algebra.Module.Torsion.Basic
/-- can't be an instance because `hM` can't be inferred  -/
Module.IsTorsionBySet.hasSMul : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {I : Ideal R} → Module.IsTorsionBySet R M ↑I → SMul (R ⧸ I) M
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.eval_eq_zero_of_eval₂_denom_eq_zero : ∀ {K : Type u} [inst : Field K] {L : Type u} [inst_1 : Field L] {f : K →+* L} {a : L} {x : RatFunc K},
  Polynomial.eval₂ f a x.denom = 0 → RatFunc.eval f a x = 0
-- Mathlib.Topology.MetricSpace.Algebra
instLipschitzAddAdditiveOfLipschitzMul : ∀ (α : Type u_1) [inst : PseudoMetricSpace α] [inst_1 : Monoid α] [LipschitzMul α], LipschitzAdd (Additive α)
-- Mathlib.Order.Defs.Unbundled
trichotomous_of : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Trichotomous r] (a b : α), r a b ∨ a = b ∨ r b a
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.measurableSet_image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β),
  MeasurableSet (⇑e '' s) ↔ MeasurableSet s
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Make a cofan `f` into a colimit cofan by providing `desc`, `fac`, and `uniq` --
just a convenience lemma to avoid having to go through `Discrete`  -/
CategoryTheory.Limits.Cofan.IsColimit.mk : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f : β → C} →
        (s : CategoryTheory.Limits.Cofan f) →
          (desc : (t : CategoryTheory.Limits.Cofan f) → s.pt ⟶ t.pt) →
            autoParam
                (∀ (t : CategoryTheory.Limits.Cofan f) (j : β),
                  CategoryTheory.CategoryStruct.comp (s.inj j) (desc t) = t.inj j)
                CategoryTheory.Limits.Cofan.IsColimit.mk._auto_1 →
              autoParam
                  (∀ (t : CategoryTheory.Limits.Cofan f) (m : s.pt ⟶ t.pt),
                    (∀ (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) m = t.inj j) → m = desc t)
                  CategoryTheory.Limits.Cofan.IsColimit.mk._auto_3 →
                CategoryTheory.Limits.IsColimit s
-- Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory
CategoryTheory.MorphismProperty.IsStableUnderComonoid.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {P : CategoryTheory.MorphismProperty C} {c : C} [inst_2 : CategoryTheory.ComonObj c],
  P CategoryTheory.ComonObj.counit → P CategoryTheory.ComonObj.comul → P.IsStableUnderComonoid c
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- Continuity is a "prelocal" predicate on functions to a fixed topological space `T`.
 -/
TopCat.continuousPrelocal : (X : TopCat) → (T : Type u_3) → [TopologicalSpace T] → TopCat.PrelocalPredicate fun x => T