mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.foldrM_eq_foldrM_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ},
  Std.TreeMap.foldrM f init t = List.foldrM (fun a b => f a.1 a.2 b) init t.toList
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
MeasureTheory.eLpNorm_eq_eLpNorm' : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} [inst : ENorm ε] {μ : MeasureTheory.Measure α},
  p ≠ 0 → p ≠ ⊤ → ∀ {f : α → ε}, MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm' f p.toReal μ
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.sup_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β]
  (f g : SupBotHom α β) (a : α), (f ⊔ g) a = f a ⊔ g a
-- Mathlib.Geometry.Manifold.StructureGroupoid
ClosedUnderRestriction.mk : ∀ {H : Type u_1} [inst : TopologicalSpace H] {G : StructureGroupoid H},
  (∀ {e : OpenPartialHomeomorph H H}, e ∈ G → ∀ (s : Set H), IsOpen s → e.restr s ∈ G) → ClosedUnderRestriction G
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_le_rpow_iff_of_neg : ∀ {x : NNReal} {z : ℝ} {y : NNReal}, 0 < x → 0 < y → z < 0 → (x ^ z ≤ y ^ z ↔ y ≤ x)
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
Profinite.NobelingProof.e_mem_of_eq_true : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (s : Finset I)
  {x : ↑(Profinite.NobelingProof.π C fun x => x ∈ s)} {a : I},
  ↑x a = true →
    Profinite.NobelingProof.e (Profinite.NobelingProof.π C fun x => x ∈ s) a ∈ Profinite.NobelingProof.factors C s x
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- `N`-conjugacy is reflexive.  -/
GroupExtension.IsConj.refl : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  (S : GroupExtension N E G) (s : S.Splitting), S.IsConj s s
-- Init.Data.Rat.Lemmas
Rat.normalize.congr_simp : ∀ (num num_1 : ℤ),
  num = num_1 →
    ∀ (den den_1 : ℕ) (e_den : den = den_1) (den_nz : den ≠ 0),
      Rat.normalize num den den_nz = Rat.normalize num_1 den_1 ⋯
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
/-- Theorems for operators that have support for `i.wrap` over `i.wrap` simplification.
Currently only addition and multiplication have `wrap` cancellation theorems
 -/
Lean.Meta.Grind.Arith.Cutsat.ToIntThms : Type
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LetRecToLift.mk.inj : ∀ {ref : Lean.Syntax} {fvarId : Lean.FVarId} {attrs : Array Lean.Elab.Attribute} {shortDeclName declName : Lean.Name}
  {parentName? : Option Lean.Name} {lctx : Lean.LocalContext} {localInstances : Lean.LocalInstances}
  {type val : Lean.Expr} {mvarId : Lean.MVarId} {termination : Lean.Elab.TerminationHints} {binders : Lean.Syntax}
  {docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)} {ref_1 : Lean.Syntax} {fvarId_1 : Lean.FVarId}
  {attrs_1 : Array Lean.Elab.Attribute} {shortDeclName_1 declName_1 : Lean.Name} {parentName?_1 : Option Lean.Name}
  {lctx_1 : Lean.LocalContext} {localInstances_1 : Lean.LocalInstances} {type_1 val_1 : Lean.Expr}
  {mvarId_1 : Lean.MVarId} {termination_1 : Lean.Elab.TerminationHints} {binders_1 : Lean.Syntax}
  {docString?_1 : Option (Lean.TSyntax `Lean.Parser.Command.docComment)},
  { ref := ref, fvarId := fvarId, attrs := attrs, shortDeclName := shortDeclName, declName := declName,
        parentName? := parentName?, lctx := lctx, localInstances := localInstances, type := type, val := val,
        mvarId := mvarId, termination := termination, binders := binders, docString? := docString? } =
      { ref := ref_1, fvarId := fvarId_1, attrs := attrs_1, shortDeclName := shortDeclName_1, declName := declName_1,
        parentName? := parentName?_1, lctx := lctx_1, localInstances := localInstances_1, type := type_1, val := val_1,
        mvarId := mvarId_1, termination := termination_1, binders := binders_1, docString? := docString?_1 } →
    ref = ref_1 ∧
      fvarId = fvarId_1 ∧
        attrs = attrs_1 ∧
          shortDeclName = shortDeclName_1 ∧
            declName = declName_1 ∧
              parentName? = parentName?_1 ∧
                lctx = lctx_1 ∧
                  localInstances = localInstances_1 ∧
                    type = type_1 ∧
                      val = val_1 ∧
                        mvarId = mvarId_1 ∧
                          termination = termination_1 ∧ binders = binders_1 ∧ docString? = docString?_1
-- Mathlib.Order.Monotone.Union
/-- If `f` is strictly antitone both on `(-∞, a]` and `[a, ∞)`, then it is strictly antitone on the
whole line.  -/
StrictAntiOn.Iic_union_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {a : α} {f : α → β},
  StrictAntiOn f (Set.Iic a) → StrictAntiOn f (Set.Ici a) → StrictAnti f
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.fold_map : ∀ {α β γ δ : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {f : β → γ} {g : δ → γ → δ}
  {init : δ} {it : Std.IterM m β},
  Std.IterM.fold g init (Std.IterM.map f it) = Std.IterM.fold (fun d b => g d (f b)) init it
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.inr_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.coprod.desc f g) = g
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.leftInverseUnitor_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.prod.leftInverseUnitor C).obj X = ({ as := PUnit.unit }, X)
-- Mathlib.Analysis.Normed.Module.Basic
nnnorm_algebraMap_nnreal : ∀ (𝕜' : Type u_2) [inst : SeminormedRing 𝕜'] [NormOneClass 𝕜'] [inst_2 : NormedAlgebra ℝ 𝕜'] (x : NNReal),
  ‖(algebraMap NNReal 𝕜') x‖₊ = x
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tensorComm_symm : ∀ {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] [inst_5 : Invertible 2]
  (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂), (Q₁.tensorComm Q₂).symm = Q₂.tensorComm Q₁
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.mk : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : Finite σ] →
                (toPreSubmersivePresentation : Algebra.PreSubmersivePresentation R S ι σ) →
                  IsUnit toPreSubmersivePresentation.jacobian → Algebra.SubmersivePresentation R S ι σ
-- Mathlib.Topology.Hom.ContinuousEvalConst
/-- If a type `F'` of bundled morphisms admits a continuous projection
to a type satisfying `ContinuousEvalConst`,
then `F'` satisfies this predicate too.

The word "forget" in the name is motivated by the term "forgetful functor".  -/
ContinuousEvalConst.of_continuous_forget : ∀ {F : Type u_1} {α : Type u_2} {X : Type u_3} [inst : FunLike F α X] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [ContinuousEvalConst F α X] {F' : Type u_5} [inst_4 : FunLike F' α X]
  [inst_5 : TopologicalSpace F'] {f : F' → F},
  Continuous f →
    autoParam (∀ (g : F'), ⇑(f g) = ⇑g) ContinuousEvalConst.of_continuous_forget._auto_1 → ContinuousEvalConst F' α X
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_inter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      (m₁.inter m₂ ⋯).getKey? k = if Std.DTreeMap.Internal.Impl.contains k m₂ = true then m₁.getKey? k else none
-- Mathlib.Lean.Expr.Basic
/-- Get the projections that are projections to parent structures. Similar to `getParentStructures`,
except that this returns the (last component of the) projection names instead of the parent names.
 -/
Lean.getFieldsToParents : Lean.Environment → Lean.Name → Array Lean.Name
-- Mathlib.Topology.Category.TopCat.ULift
TopCat.uliftFunctorCompForgetIso_hom_app_hom_apply : ∀ (X : TopCat) (a : (TopCat.uliftFunctor.comp (CategoryTheory.forget TopCat)).obj X),
  (CategoryTheory.ConcreteCategory.hom (TopCat.uliftFunctorCompForgetIso.hom.app X)) a = a
-- Mathlib.Analysis.Calculus.FDeriv.Basic
hasStrictFDerivAt_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] (x : E), HasStrictFDerivAt id (ContinuousLinearMap.id 𝕜 E) x
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instNonAssocSemiring : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → [NonAssocSemiring Y] → NonAssocSemiring (LocallyConstant X Y)
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- If `G` acts on `X` properly, then the map `G × T → X × T, (g, t) ↦ (g • t, t)` is still
proper for *any* subset `T` of `X`.  -/
ProperSMul.isProperMap_smul_pair_set : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [ProperSMul G X] {t : Set X}, IsProperMap fun gx => (gx.1 • ↑gx.2, gx.2)
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.sup_sup : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x₁ x₂ : Filter α} {y₁ y₂ : Filter β},
  Filter.Tendsto f x₁ y₁ → Filter.Tendsto f x₂ y₂ → Filter.Tendsto f (x₁ ⊔ x₂) (y₁ ⊔ y₂)
-- Mathlib.Order.Interval.Finset.Defs
Finset.Iio.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : α),
  Finset.Iio a = LocallyFiniteOrderBot.finsetIio a
-- Mathlib.Combinatorics.Matroid.Loop
/-- **Alias** of `Matroid.closure_sdiff_eq_of_subset_coloops`. -/
Matroid.closure_diff_eq_of_subset_coloops : ∀ {α : Type u_1} {M : Matroid α} {K : Set α} (X : Set α), K ⊆ M.coloops → M.closure (X \ K) = M.closure X \ K
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
/-- Eta-expanded form of `ProbabilityTheory.BrownianReal.variance_projectiveFamily` -/
ProbabilityTheory.BrownianReal.variance_fun_projectiveFamily : ∀ (I : Finset NNReal) (f : (↥I → ℝ) → ℝ),
  ProbabilityTheory.variance f (ProbabilityTheory.BrownianReal.projectiveFamily I) =
    ProbabilityTheory.variance (fun x => f x.ofLp)
      (ProbabilityTheory.multivariateGaussian 0 (ProbabilityTheory.BrownianReal.covMatrix I))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit!_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [inst : BEq α] [Std.LawfulBEqOrd α]
  [Std.TransOrd α],
  t.WF →
    ∀ {l : List α} {k fallback : α},
      k ∉ t →
        l.contains k = false →
          (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).getKeyD k fallback = fallback
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.Polynomial.quotQuotEquivComm.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f : Polynomial R),
  AdjoinRoot.Polynomial.quotQuotEquivComm I f =
    (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f}).quotientEquiv
      (Ideal.span {(Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f}) I.polynomialQuotientEquivQuotientPolynomial ⋯
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.transvection_coe : ∀ {ι : Type u_1} {F : Type u_2} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommRing F] {i j : ι}
  (hij : i ≠ j) (b : F), ↑(Matrix.SpecialLinearGroup.transvection hij b) = 1 + Matrix.single i j b
-- Mathlib.Algebra.Group.Hom.Defs
/-- The underlying function  -/
AddHom.toFun : {M : Type u_10} → {N : Type u_11} → [inst : Add M] → [inst_1 : Add N] → (M →ₙ+ N) → M → N
-- Mathlib.Topology.Algebra.Algebra.Equiv
AlgEquiv.isUniformEmbedding : ∀ {R : Type u_1} [inst : CommSemiring R] {E₁ : Type u_5} {E₂ : Type u_6} [inst_1 : UniformSpace E₁]
  [inst_2 : UniformSpace E₂] [inst_3 : Ring E₁] [IsUniformAddGroup E₁] [inst_5 : Algebra R E₁] [inst_6 : Ring E₂]
  [IsUniformAddGroup E₂] [inst_8 : Algebra R E₂] (e : E₁ ≃ₐ[R] E₂),
  Continuous ⇑e → Continuous ⇑e.symm → IsUniformEmbedding ⇑e
-- Init.Data.ByteArray.Basic
/-- Moves the iterator's position several bytes forward.

The resulting iterator is only valid if the number of bytes to skip is less than or equal to
the number of bytes left in the iterator.
 -/
ByteArray.Iterator.nextn : ByteArray.Iterator → ℕ → ByteArray.Iterator
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- The `N`-conjugacy classes of splittings  -/
GroupExtension.ConjClasses : {N : Type u_1} →
  {G : Type u_2} →
    [inst : Group N] →
      [inst_1 : Group G] → {E : Type u_3} → [inst_2 : Group E] → GroupExtension N E G → Type (max u_2 u_3)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Fan.ext_inv_hom : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C} {c₁ c₂ : CategoryTheory.Limits.Fan f}
  (e : c₁.pt ≅ c₂.pt)
  (w :
    autoParam (∀ (b : β), c₁.proj b = CategoryTheory.CategoryStruct.comp e.hom (c₂.proj b))
      CategoryTheory.Limits.Fan.ext._auto_1),
  (CategoryTheory.Limits.Fan.ext e w).inv.hom = e.inv
-- Mathlib.Algebra.Order.Monoid.Lex
AddMonoidHom.inr_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoid α] [inst_1 : Preorder α] [inst_2 : AddMonoid β] [inst_3 : Preorder β],
  Monotone ⇑(AddMonoidHom.inr α β)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} {v : β k},
          (Std.DTreeMap.Internal.Impl.insertIfNew! k v t₁).Equiv (Std.DTreeMap.Internal.Impl.insertIfNew! k v t₂)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Assumes left covariance.  -/
Left.mul_nonneg : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : Preorder α] [PosMulMono α], 0 ≤ a → 0 ≤ b → 0 ≤ a * b
-- Mathlib.Algebra.Notation.Prod
Prod.snd_sub : ∀ {G : Type u_8} {H : Type u_9} [inst : Sub G] [inst_1 : Sub H] (a b : G × H), (a - b).2 = a.2 - b.2
-- Mathlib.Order.Antisymmetrization
instLinearOrderAntisymmetrizationLeOfDecidableLEOfDecidableLTOfTotal : {α : Type u_1} →
  [inst : Preorder α] →
    [DecidableLE α] →
      [DecidableLT α] → [Std.Total fun x1 x2 => x1 ≤ x2] → LinearOrder (Antisymmetrization α fun x1 x2 => x1 ≤ x2)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.ringEquivOfRingEquiv.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {M M_1 : Submonoid R} (e_M : M = M_1) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {T T_1 : Submonoid P}
  (e_T : T = T_1) (Q : Type u_4) [inst_5 : CommSemiring Q] [inst_6 : Algebra P Q] [inst_7 : IsLocalization T Q]
  (h h_1 : R ≃+* P) (e_h : h = h_1) (H : Submonoid.map h.toMonoidHom M = T),
  IsLocalization.ringEquivOfRingEquiv S Q h H = IsLocalization.ringEquivOfRingEquiv S Q h_1 ⋯
-- Mathlib.Algebra.Lie.Basic
LieEquiv.instEquivLike : {R : Type u} →
  {L₁ : Type v} →
    {L₂ : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] →
          [inst_2 : LieRing L₂] →
            [inst_3 : LieAlgebra R L₁] → [inst_4 : LieAlgebra R L₂] → EquivLike (L₁ ≃ₗ⁅R⁆ L₂) L₁ L₂
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.lt_log_of_exp_lt : ∀ {G : Type u_3} [inst : Preorder G] {a : G} [inst_1 : AddGroup G] {x : WithZero (Multiplicative G)},
  WithZero.exp a < x → a < x.log
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.snd_mapComp_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {a b c : B × C} (f : a ⟶ b) (g : b ⟶ c),
  ((CategoryTheory.Bicategory.Prod.snd B C).mapComp f g).hom =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f.2 g.2)
-- Mathlib.FieldTheory.Minpoly.Basic
minpoly.eq_1 : ∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B),
  minpoly A x =
    if hx : IsIntegral A x then ⋯.min (fun x_1 => x_1.Monic ∧ Polynomial.eval₂ (algebraMap A B) x x_1 = 0) hx else 0
-- Mathlib.Topology.UniformSpace.Defs
nhds_nhds_eq_uniformity_uniformity_prod : ∀ {α : Type ua} [inst : UniformSpace α] {a b : α},
  nhds a ×ˢ nhds b = (uniformity α).lift fun s => (uniformity α).lift' fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curryingEquiv_apply_map : ∀ {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]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X Y : C × D} (f : X ⟶ Y),
  (CategoryTheory.Functor.curryingEquiv F).map f =
    CategoryTheory.CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueMul.iff_existsUnique : ∀ {G : Type u_1} [inst : Mul G] {A B : Finset G} {a0 b0 : G},
  a0 ∈ A → b0 ∈ B → (UniqueMul A B a0 b0 ↔ ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.structureMapLM_zero_injective : ∀ (𝕜 : 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 : TopologicalSpace.Compacts E},
  Function.Injective ⇑(ContDiffMapSupportedIn.structureMapLM 𝕜 n 0)
-- Mathlib.Data.Set.Pairwise.Basic
/-- **Alias** of `subsingleton_setOfPred_mem_iff_pairwise_disjoint`. -/
subsingleton_setOf_mem_iff_pairwise_disjoint : ∀ {α : Type u_1} {ι : Type u_4} {f : ι → Set α},
  (∀ (a : α), {i | a ∈ f i}.Subsingleton) ↔ Pairwise (Function.onFun Disjoint f)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.card_eq_card_isUnramifiedIn : ∀ (k : Type u_1) [inst : Field k] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : NumberField K]
  [inst_4 : NumberField k] [IsGalois k K],
  Fintype.card (NumberField.InfinitePlace K) =
    {w | NumberField.InfinitePlace.IsUnramifiedIn K w}.card * Module.finrank k K +
      {w | NumberField.InfinitePlace.IsUnramifiedIn K w}ᶜ.card * (Module.finrank k K / 2)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.get!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} [inst_1 : Inhabited (β k)], t₁.Equiv t₂ → t₁.get! k = t₂.get! k
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `iteratedFDeriv_add_apply` -/
fun_iteratedFDeriv_add_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E} {i : ℕ}
  {f g : E → F},
  ContDiffAt 𝕜 (↑i) f x →
    ContDiffAt 𝕜 (↑i) g x → iteratedFDeriv 𝕜 i (fun i => f i + g i) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.sheafBotEquivalence_inverse_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (P : CategoryTheory.Functor Cᵒᵖ A), ((CategoryTheory.sheafBotEquivalence A).inverse.obj P).obj = P
-- Mathlib.GroupTheory.Coset.Basic
QuotientAddGroup.rightRel_prod : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {β : Type u_2} [inst_1 : AddGroup β] (s' : AddSubgroup β),
  QuotientAddGroup.rightRel (s.prod s') = (QuotientAddGroup.rightRel s).prod (QuotientAddGroup.rightRel s')
-- Mathlib.Topology.Order.Lattice
Continuous.finset_sup'_apply : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeSup L] [ContinuousSup L] {s : Finset ι} {f : ι → X → L} (hne : s.Nonempty),
  (∀ i ∈ s, Continuous (f i)) → Continuous fun a => s.sup' hne fun x => f x a
-- Mathlib.Data.NNRat.Defs
Rat.toNNRat_add : ∀ {p q : ℚ}, 0 ≤ q → 0 ≤ p → (q + p).toNNRat = q.toNNRat + p.toNNRat
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.lift' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [CategoryTheory.Balanced C],
  S.Exact →
    ∀ {A : C} (k : A ⟶ S.X₂),
      CategoryTheory.CategoryStruct.comp k S.g = 0 →
        ∀ [CategoryTheory.Mono S.f], ∃ l, CategoryTheory.CategoryStruct.comp l S.f = k
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.toCloseds_injective : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M], Function.Injective ClosedSubmodule.toCloseds
-- Mathlib.Analysis.Normed.Operator.NormedSpace
ContinuousLinearEquiv.one_le_norm_mul_norm_symm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂]
  [Nontrivial E] (e : E ≃SL[σ₁₂] F), 1 ≤ ‖↑e‖ * ‖↑e.symm‖
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Sized.node3L : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α},
  l.Sized → m.Sized → r.Sized → (l.node3L x m y r).Sized
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.sigma_ground_eq : ∀ {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)}, (Matroid.sigma M).E = Set.univ.sigma fun i => (M i).E
-- Mathlib.Order.Partition.Finpartition
Finpartition.part_subset : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) (a : α), P.part a ⊆ s
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.mem_aroots : ∀ {S : Type v} {T : Type w} [inst : CommRing T] [IsDomain T] [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : Algebra T S] [Module.IsTorsionFree T S] {p : Polynomial T} {a : S},
  a ∈ p.aroots S ↔ p ≠ 0 ∧ (Polynomial.aeval a) p = 0
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_eq : ∀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'}
  {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence₁ hF).counitIso =
    AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso hF
-- Mathlib.Algebra.Group.Basic
inv_unique : ∀ {M : Type u_4} [inst : CommMonoid M] {x y z : M}, x * y = 1 → x * z = 1 → y = z
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.addRecAux_extractAndExtend_eq_cpop : ∀ {w : ℕ} {x : BitVec w}, BitVec.addRecAux✝ (BitVec.extractAndExtend w x) w 0#w = x.cpop
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
/-- If the left cosets of `t` by elements of `s` are disjoint (but not necessarily
distinct!), then the size of `t` divides the size of `s + t`.  -/
Finset.card_dvd_card_add_right : ∀ {α : Type u_2} [inst : AddGroup α] [inst_1 : DecidableEq α] {s t : Finset α},
  ((fun x => x +ᵥ t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s + t).card
-- Std.Http.Data.Body.Any
/-- Non-blocking receive attempt. Returns `none` if no chunk is immediately available,
`some (some chunk)` when a chunk is ready, or `some none` at end-of-stream.
 -/
Std.Http.Body.Any.tryRecv : Std.Http.Body.Any → Std.Async.Async (Option (Option Std.Http.Chunk))
-- Init.Data.Array.Find
Array.get_find?_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α} {p : α → Bool} (h : (Array.find? p (Array.replicate n a)).isSome = true),
  (Array.find? p (Array.replicate n a)).get h = a