mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RiiSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : SizeOf α] [inst_1 : SizeOf β] (treeMap : Std.DTreeMap.Internal.Impl α fun x => β)
  (range : Std.Rii α), sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.ConnectionState.expectData : {β : Type} → Std.Http.Server.Connection.ConnectionState✝ β → Option ℕ
-- Mathlib.Tactic.DuplicateDecls
/-- The duplicate declarations linter. It tells you which duplicate declarations there are
in the current environment.  -/
Mathlib.Tactic.DuplicateDecls.lintDuplicateDeclarations : Mathlib.Tactic.DuplicateDecls.Target → Lean.CoreM Lean.MessageData
-- Mathlib.Order.WellFounded
Function.Injective.isWellOrder : ∀ {α : Type u_1} {β : Type u_2} (r : β → β → Prop) {f : α → β},
  Function.Injective f → ∀ [IsWellOrder β r], IsWellOrder α (Function.onFun r f)
-- Init.Data.Sum.Lemmas
_private.Init.Data.Sum.Lemmas.0.Sum.isLeft.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (val : α) (h_1 : (val : α) → motive (Sum.inl val))
  (h_2 : (val : β) → motive (Sum.inr val)),
  (match Sum.inl val with
    | Sum.inl val => h_1 val
    | Sum.inr val => h_2 val) =
    h_1 val
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The ring equiv between the top element of `Subring R` and `R`.  -/
Subring.topEquiv : {R : Type u} → [inst : NonAssocRing R] → ↥⊤ ≃+* R
-- Mathlib.Data.Multiset.ZeroCons
Multiset.cons_inj_left : ∀ {α : Type u_1} {a b : α} (s : Multiset α), a ::ₘ s = b ::ₘ s ↔ a = b
-- Mathlib.RingTheory.IsTensorProduct
/-- If `M` is the tensor product of `M₁` and `M₂`, it is linearly equivalent to `M₁ ⊗[R] M₂`.  -/
IsTensorProduct.equiv : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M₁ : Type u_2} →
      {M₂ : Type u_3} →
        {M : Type u_4} →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R M] →
                      {f : M₁ →ₗ[R] M₂ →ₗ[R] M} → IsTensorProduct f → TensorProduct R M₁ M₂ ≃ₗ[R] M
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Preserves multiplication.  -/
MulEquivClass.map_mul : ∀ {F : Type u_9} {A : outParam (Type u_10)} {B : outParam (Type u_11)} {inst : Mul A} {inst_1 : Mul B}
  {inst_2 : EquivLike F A B} [self : MulEquivClass F A B] (f : F) (a b : A), f (a * b) = f a * f b
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
QuasispectrumRestricts.comp : ∀ {R₁ : Type u_6} {R₂ : Type u_7} {R₃ : Type u_8} {A : Type u_9} [inst : Semifield R₁] [inst_1 : Field R₂]
  [inst_2 : Field R₃] [inst_3 : NonUnitalRing A] [inst_4 : Module R₁ A] [inst_5 : Module R₂ A] [inst_6 : Module R₃ A]
  [inst_7 : Algebra R₁ R₂] [inst_8 : Algebra R₂ R₃] [inst_9 : Algebra R₁ R₃] [IsScalarTower R₁ R₂ R₃]
  [IsScalarTower R₂ R₃ A] [IsScalarTower R₃ A A] [SMulCommClass R₃ A A] {a : A} {f : R₃ → R₂} {g : R₂ → R₁}
  {e : R₃ → R₁}, g ∘ f = e → QuasispectrumRestricts a f → QuasispectrumRestricts a g → QuasispectrumRestricts a e
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScottHausdorff.isOpen_iff_dirSupInaccOn : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α] [t : TopologicalSpace α]
  [Topology.IsScottHausdorff α D], IsLowerSet D → (IsOpen s ↔ DirSupInaccOn D s)
-- Mathlib.Order.Filter.Pointwise
Filter.div_bot : ∀ {α : Type u_2} [inst : Div α] {f : Filter α}, f / ⊥ = ⊥
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- Given `W : MorphismProperty C`, this is class of morphisms that are
isomorphic to a coproduct of a family (indexed by some `J : Type w`) of maps in `W`.  -/
CategoryTheory.MorphismProperty.coproducts : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.funInvIdAssoc_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (F : CategoryTheory.Functor C E) (X : C),
  (e.funInvIdAssoc F).inv.app X = F.map (e.unit.app X)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.toSubring.congr_simp : ∀ {R : Type u_1} [inst : Ring R] (p p_1 : PowerSeries R) (e_p : p = p_1) (T : Subring R)
  (hp : ∀ (n : ℕ), (PowerSeries.coeff n) p ∈ T) (a a_1 : Unit →₀ ℕ),
  a = a_1 → p.toSubring T hp a = p_1.toSubring T ⋯ a_1
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instDistribMulAction : {α : Type u_1} →
  {R : Type u_6} →
    [inst : Monoid R] →
      [inst_1 : DistribMulAction R ENNReal] →
        [IsScalarTower R ENNReal ENNReal] → {x : MeasurableSpace α} → DistribMulAction R (MeasureTheory.Measure α)
-- Lean.Meta.Tactic.Grind.EMatch
/-- Matches a pattern argument. See `matchArgs?`.  -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.matchArg? : Lean.Meta.Grind.EMatch.Choice → Lean.Expr → Lean.Expr → OptionT Lean.Meta.Grind.GoalM Lean.Meta.Grind.EMatch.Choice
-- Lean.Meta.Sorry
Lean.Meta.SorryLabelView.mk.injEq : ∀ (module? module?_1 : Option Lean.DeclarationLocation),
  ({ module? := module? } = { module? := module?_1 }) = (module? = module?_1)
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.sq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : Pow γ ℕ] [MeasurablePow γ ℕ],
  ProbabilityTheory.IdentDistrib f g μ ν → ProbabilityTheory.IdentDistrib (fun x => f x ^ 2) (fun x => g x ^ 2) μ ν
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.WF.getThenInsertIfNew?₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {m : Std.DHashMap.Raw α β}
  {h : 0 < m.buckets.size} {a : α} {b : β a}, m.WF → (↑(Std.DHashMap.Internal.Raw₀.getThenInsertIfNew? ⟨m, h⟩ a b).2).WF
-- Batteries.Data.Stream
Std.Stream.snd_take_eq_drop : ∀ {σ : Type u_1} {α : Type u_2} [inst : Std.Stream σ α] (s : σ) (n : ℕ), (Std.Stream.take s n).2 = Std.Stream.drop s n
-- Std.Data.TreeMap.Basic
/-- Checks whether a key is present in a map, returning the associated value, and inserts a value for
the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.TreeMap.getThenInsertIfNew? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → β → Option β × Std.TreeMap α β cmp
-- Mathlib.RingTheory.Binomial
Ring.choose_zero_right : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] [NatPowAssoc R] (r : R),
  Ring.choose r 0 = 1
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fundamentalSequence.eq_2 : ∀ (e : ONote) (n : ℕ+) (a : ONote),
  (e.oadd n a).fundamentalSequence =
    match a.fundamentalSequence with
    | Sum.inr f => Sum.inr fun i => e.oadd n (f i)
    | Sum.inl (some b') => Sum.inl (some (e.oadd n b'))
    | Sum.inl none =>
      match e.fundamentalSequence, n.natPred with
      | Sum.inl none, 0 => Sum.inl (some ONote.zero)
      | Sum.inl none, m.succ => Sum.inl (some (ONote.zero.oadd m.succPNat ONote.zero))
      | Sum.inl (some a'), 0 => Sum.inr fun i => a'.oadd i.succPNat ONote.zero
      | Sum.inl (some a'), m.succ => Sum.inr fun i => e.oadd m.succPNat (a'.oadd i.succPNat ONote.zero)
      | Sum.inr f, 0 => Sum.inr fun i => (f i).oadd 1 ONote.zero
      | Sum.inr f, m.succ => Sum.inr fun i => e.oadd m.succPNat ((f i).oadd 1 ONote.zero)
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.int_add_iff : ∀ {p x : ℝ} {m : ℤ}, LiouvilleWith p (↑m + x) ↔ LiouvilleWith p x
-- Mathlib.Analysis.Real.Sqrt
/-- The real square root is at most the natural square root plus one  -/
Real.real_sqrt_le_nat_sqrt_succ : ∀ {a : ℕ}, √↑a ≤ ↑a.sqrt + 1
-- Mathlib.Algebra.Category.ModuleCat.Simple
/-- A simple object in the category of modules is a simple module.  -/
isSimpleModule_of_simple : ∀ {R : Type u_1} [inst : Ring R] (M : ModuleCat R) [CategoryTheory.Simple M], IsSimpleModule R ↑M
-- Lean.Meta.Basic
Lean.Meta.instantiateMVarsProfiling : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.Nat.Dist
/-- Distance (absolute value of difference) between natural numbers.  -/
Nat.dist : ℕ → ℕ → ℕ
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ψ₂.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.ψ₂ = W.toAffine.polynomialY
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get!.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α) [inst_2 : Inhabited (β k)]
  (size : ℕ) (k' : α) (v : β k') (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k' v l r).get! k =
    match h : compare k k' with
    | Ordering.lt => l.get! k
    | Ordering.gt => r.get! k
    | Ordering.eq => cast ⋯ v
-- Mathlib.CategoryTheory.Sites.LocallyBijective
CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_2} {CD : D → Type (max u v)}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD]
  [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose (CategoryTheory.forget D)]
  [J.PreservesSheafification (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms],
  J.WEqualsLocallyBijective D
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- A fork on a pair of morphisms `f` and `g` is the same as a multifork on the
single point index defined by `f` and `g`.  -/
CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.Limits.MulticospanShape) →
      [Unique J.L] →
        [Unique J.R] →
          {X Y : C} →
            (f g : X ⟶ Y) →
              CategoryTheory.Limits.Multifork (CategoryTheory.Limits.MulticospanIndex.ofParallelHoms J f g) ≌
                CategoryTheory.Limits.Fork f g
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.coe_ne_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {x : ↑(Set.Ioc 0 1)},
  ↑x ≠ 1 ↔ x ≠ 1
-- Init.Data.Int.DivMod.Basic
_private.Init.Data.Int.DivMod.Basic.0.Int.fdiv.match_1.eq_5 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (a : ℕ) → motive (Int.negSucc a) 0) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ))
  (h_6 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc m, Int.ofNat n.succ with
    | 0, x => h_1 x
    | Int.ofNat m, Int.ofNat n => h_2 m n
    | Int.ofNat m.succ, Int.negSucc n => h_3 m n
    | Int.negSucc a, 0 => h_4 a
    | Int.negSucc m, Int.ofNat n.succ => h_5 m n
    | Int.negSucc m, Int.negSucc n => h_6 m n) =
    h_5 m n
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If a function `f` with a densely ordered codomain is monotone on a right neighborhood of `a` and
the closure of the image of this neighborhood under `f` is a right neighborhood of `f a`, then `f`
is continuous at `a` from the right.  -/
continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α}
  {a : α},
  MonotoneOn f s →
    s ∈ nhdsWithin a (Set.Ici a) →
      closure (f '' s) ∈ nhdsWithin (f a) (Set.Ici (f a)) → ContinuousWithinAt f (Set.Ici a) a
-- Mathlib.Order.SupClosed
LinearOrder.infClosed : ∀ {α : Type u_3} [inst : LinearOrder α] (s : Set α), InfClosed s
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsAddHaarMeasure.nnreal_smul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] {c : NNReal}, c ≠ 0 → (c • μ).IsAddHaarMeasure
-- Lean.Elab.DefView
Lean.Elab.instTypeNameDefsParsedSnapshot : TypeName Lean.Elab.DefsParsedSnapshot
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The function from the free ring on the diagram to the cone point of any other
cocone.  -/
RingCat.Colimits.descFunLift : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J RingCat) →
      (s : CategoryTheory.Limits.Cocone F) → RingCat.Colimits.Prequotient F → ↑s.pt
-- Std.Http.Data.Request
/-- Creates a new HTTP GET Request with the specified URI.
 -/
Std.Http.Request.get : Std.Http.RequestTarget → Std.Http.Request.Builder
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.coeff_sum : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_7} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R] {s : Finset α}
  {x : α → HahnSeries Γ R} (g : Γ), (∑ i ∈ s, x i).coeff g = ∑ i ∈ s, (x i).coeff g
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_eq_emptyset : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {x : E} {r : ℝ}, r < 0 → p.closedBall x r = ∅
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.instHashableKey : Hashable Std.Tactic.BVDecide.BVExpr.Cache.Key
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
BoundedVariationOn.continuousWithinAt_variationOnFromTo_rightLim_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E}
  [inst_2 : TopologicalSpace α] [OrderTopology α] [T3Space E] [CompleteSpace E],
  BoundedVariationOn f Set.univ →
    ∀ {a x : α}, ContinuousWithinAt (variationOnFromTo (Function.rightLim f) Set.univ a) (Set.Ici x) x
-- Init.Data.Nat.Gcd
Nat.gcd_eq_left : ∀ {m n : ℕ}, m ∣ n → m.gcd n = m
-- Init.Data.SInt.Lemmas
Int32.toNatClampNeg_one : Int32.toNatClampNeg 1 = 1
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.mul_smul' : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f g : ArithmeticFunction R) (h : ArithmeticFunction M), (f * g) • h = f • g • h
-- Mathlib.Data.Finset.Sups
/-- The finset of elements of the form `a ⊔ b` where `a ∈ s`, `b ∈ t` and `a` and `b` are disjoint.
 -/
FinsetFamily.«term_○_» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffineLift_some : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {X Y : F} (h : W.NonsingularLift ⟦![X, Y, 1]⟧),
  { point := ⟦![X, Y, 1]⟧, nonsingular := h }.toAffineLift = WeierstrassCurve.Affine.Point.some X Y ⋯
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.map_modEq_iff : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a b p : M} {N : Type u_2} {F : Type u_3} [inst_1 : AddCommMonoid N]
  [inst_2 : FunLike F M N] [AddMonoidHomClass F M N] (f : F),
  Function.Injective ⇑f → (f a ≡ f b [PMOD f p] ↔ a ≡ b [PMOD p])
-- Mathlib.Algebra.Group.Subgroup.Basic
MonoidHom.liftOfRightInverseAux_comp_apply : ∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : Group G₁] [inst_1 : Group G₂] [inst_2 : Group G₃]
  (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) (x : G₁),
  (f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.mk_mul_mk : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x y : ℕ × K),
  PerfectClosure.mk K p x * PerfectClosure.mk K p y =
    PerfectClosure.mk K p (x.1 + y.1, (⇑(frobenius K p))^[y.1] x.2 * (⇑(frobenius K p))^[x.1] y.2)
-- Mathlib.Order.RelClasses
/-- **Alias** of `LT.lt.asymm`. -/
HasSSubset.SSubset.asymm : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → ¬b < a
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.instToString : ToString Lean.Omega.LinearCombo
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
/-- By using the axiom of choice, a dependent pair `(V, f)` where `f : V ⟶ iSup U` is a member of
`presieveOfCovering U f` can be turned into an index `i : ι`, such that `V = U i`.
 -/
TopCat.Presheaf.presieveOfCovering.indexOfHom : {X : TopCat} →
  {ι : Type v} →
    (U : ι → TopologicalSpace.Opens ↑X) →
      (V : TopologicalSpace.Opens ↑X) × { f // TopCat.Presheaf.presieveOfCovering U f } → ι
-- Mathlib.Algebra.Group.Subgroup.Even
/-- In a commutative monoid `M`, `Submonoid.square M` is the submonoid of squares in `M`.
 -/
Submonoid.square : (M : Type u_1) → [inst : CommMonoid M] → Submonoid M
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.Hom.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {X Y : CategoryTheory.Center C} {x y : X.Hom Y}, x.f = y.f → x = y
-- Mathlib.FieldTheory.NormalizedTrace
_private.Mathlib.FieldTheory.NormalizedTrace.0.Algebra.normalizedTraceAux_intermediateField : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] {E : IntermediateField F K}
  (a : ↥E), Algebra.normalizedTraceAux✝ F K ↑a = Algebra.normalizedTraceAux✝ F (↥E) a
-- Mathlib.Logic.Relation
/-- **Alias** of `Relation.Join.symm`. -/
Relation.symmetric_join : ∀ {α : Type u_1} {r : α → α → Prop}, Std.Symm (Relation.Join r)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
contDiffAt_prod_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {n : WithTop ℕ∞} (f : E → F × G),
  ContDiffAt 𝕜 n f x ↔ ContDiffAt 𝕜 n (Prod.fst ∘ f) x ∧ ContDiffAt 𝕜 n (Prod.snd ∘ f) x
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.toQuadraticForm'.eq_1 : ∀ {R : Type u_3} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] (M : Matrix n n R),
  M.toQuadraticForm' = LinearMap.BilinMap.toQuadraticMap ((Matrix.toLinearMap₂' R) M)
-- Mathlib.Order.Heyting.Hom
CoheytingHom.instFunLike : {α : Type u_2} →
  {β : Type u_3} → [inst : CoheytingAlgebra α] → [inst_1 : CoheytingAlgebra β] → FunLike (CoheytingHom α β) α β
-- Mathlib.Data.Nat.SuccPred
Nat.instIsSuccArchimedean : IsSuccArchimedean ℕ
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.range_smulRight_apply : ∀ {M₁ : Type u_4} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁] {M₂ : Type u_6}
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] {R : Type u_9} [inst_4 : DivisionSemiring R]
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] [inst_7 : TopologicalSpace R] [inst_8 : ContinuousSMul R M₂]
  {f : M₁ →L[R] R}, f ≠ 0 → ∀ (x : M₂), (↑(f.smulRight x)).range = R ∙ x
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.congr : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ → s =ᵐ[μ] t → MeasureTheory.NullMeasurableSet t μ
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.toSubspace_isMono : ∀ {η : Type u_1} {α : Type u_2} {ι : Type u_3} {κ : Type u_4} {l : Combinatorics.Line (η → α) ι} {C : (ι × η → α) → κ},
  Combinatorics.Subspace.IsMono C l.toSubspace ↔
    Combinatorics.Line.IsMono
      (fun x =>
        C fun x_1 =>
          match x_1 with
          | (i, e) => x i e)
      l
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.preservesFiniteCoproductsOfAdditive : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [F.Additive], CategoryTheory.Limits.PreservesFiniteCoproducts F
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.self_le_maxKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α} {v : β}
  {kmi : α}, (t.insertIfNew k v).maxKey?.get ⋯ = kmi → (cmp k kmi).isLE = true
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
/-- A two-sided ideal is simply a left ideal that is two-sided.  -/
TwoSidedIdeal.orderIsoIsTwoSided : {R : Type u_1} → [inst : Ring R] → TwoSidedIdeal R ≃o { I // I.IsTwoSided }
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.le_max!_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k : α}, t.contains k = true → (cmp k t.max!).isLE = true
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.bddAbove : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
  Memℓp f ⊤ → BddAbove (Set.range fun i => ‖f i‖)
-- Std.Internal.Do.ExceptPost
/-- The tail exception postconditions.  -/
Std.Internal.Do.EPost.Cons.tail : {eh : Type u} → {et : Type v} → EPost.Cons✝ eh et → et
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_monomial_ne : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {m n : σ →₀ ℕ},
  m ≠ n → ∀ (a : R), (MvPowerSeries.coeff m) ((MvPowerSeries.monomial n) a) = 0
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- A typeclass registering that a smoothness exponent is smaller than `∞`. Used to deduce that
some manifolds are `C^n` when they are `C^∞`.  -/
ENat.LEInfty : WithTop ℕ∞ → Prop
-- Mathlib.GroupTheory.Sylow
Sylow.normal_of_subsingleton : ∀ {G : Type u} [inst : Group G] {p : ℕ} [Subsingleton (Sylow p G)] (P : Sylow p G), (↑P).Normal
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterWeights_restrict : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (S : AffineSubspace ℝ P)
  (hS : affineSpan ℝ (Set.range s.points) ≤ S), (s.restrict S hS).excenterWeights = s.excenterWeights
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.sheafComposeNatTrans_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1}
  {B : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_1} A] [inst_2 : CategoryTheory.Category.{v_2, u_2} B]
  (F : CategoryTheory.Functor A B)
  {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)}
  (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A)
  {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)}
  (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [inst_3 : J.HasSheafCompose F] (P : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.CategoryStruct.comp (adj₂.unit.app (P.comp F))
      ((CategoryTheory.sheafToPresheaf J B).map ((CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂).app P)) =
    CategoryTheory.Functor.whiskerRight (adj₁.unit.app P) F
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_mono : ∀ {σs : List (Type u)} {P P' Q Q' : Std.Do.SPred σs}, (P ⊢ₛ P') → (Q ⊢ₛ Q') → P ∨ Q ⊢ₛ P' ∨ Q'
-- Mathlib.Order.SuccPred.Basic
Order.pred_le_pred_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α],
  Order.pred b ≤ Order.pred a ↔ b ≤ a
-- Mathlib.Computability.NFA
NFA.acceptsFrom_iUnion₂ : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) {ι : Sort u_1} {κ : ι → Sort u_2} (f : (i : ι) → κ i → Set σ),
  M.acceptsFrom (⋃ i, ⋃ j, f i j) = ⋃ i, ⋃ j, M.acceptsFrom (f i j)