mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_union : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  Disjoint s t →
    MeasurableSet t →
      MeasureTheory.IntegrableOn f s μ →
        MeasureTheory.IntegrableOn f t μ → ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in t, f x ∂μ
-- Mathlib.Algebra.Group.Prod
Prod.SubtractionCommMonoid : {G : Type u_1} → {H : Type u_2} → [SubtractionCommMonoid G] → [SubtractionCommMonoid H] → SubtractionCommMonoid (G × H)
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.preservesEpimorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive],
  L.PreservesEpimorphisms
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.continue.inj : ∀ {dir : Std.Http.Protocol.H1.Direction} {a a_1 : Std.Http.Protocol.H1.Reader.State dir},
  a.continue = a_1.continue → a = a_1
-- Mathlib.CategoryTheory.PathCategory.Basic
/-- A path in a category can be composed to a single morphism.  -/
CategoryTheory.composePath : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → Quiver.Path X Y → (X ⟶ Y)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
/-- The `Y`-coordinate of `-((x₁, y₁) + (x₂, y₂))` for two nonsingular affine points `(x₁, y₁)` and
`(x₂, y₂)` on a Weierstrass curve `W`, where the line through them has a slope of `ℓ`.

This depends on `W`, and has argument order: `x₁`, `x₂`, `y₁`, `ℓ`.  -/
WeierstrassCurve.Affine.negAddY : {R : Type r} → [CommRing R] → WeierstrassCurve.Affine R → R → R → R → R → R
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.mk : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [inst_3 : CompleteSpace E] →
            {F : Type u_3} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : CompleteSpace F] →
                    {G : Type u_4} →
                      [inst_7 : NormedAddCommGroup G] →
                        [inst_8 : NormedSpace 𝕜 G] →
                          [inst_9 : CompleteSpace G] →
                            (leftFun : E → F) →
                              (leftDeriv : E →L[𝕜] F) →
                                (rightFun : E → G) →
                                  (rightDeriv : E →L[𝕜] G) →
                                    (pt : E) →
                                      HasStrictFDerivAt leftFun leftDeriv pt →
                                        HasStrictFDerivAt rightFun rightDeriv pt →
                                          (↑leftDeriv).range = ⊤ →
                                            (↑rightDeriv).range = ⊤ →
                                              IsCompl (↑leftDeriv).ker (↑rightDeriv).ker → ImplicitFunctionData 𝕜 E F G
-- Mathlib.CategoryTheory.Join.Opposites
_private.Mathlib.CategoryTheory.Join.Opposites.0.CategoryTheory.Join.opEquiv.match_5.eq_1 : ∀ (C : Type u_4) (D : Type u_3) [inst : CategoryTheory.Category.{u_2, u_4} C]
  [inst_1 : CategoryTheory.Category.{u_1, u_3} D] (motive : CategoryTheory.Join Dᵒᵖ Cᵒᵖ → Sort u_5) (a : Dᵒᵖ)
  (h_1 : (a : Dᵒᵖ) → motive (CategoryTheory.Join.left a)) (h_2 : (a : Cᵒᵖ) → motive (CategoryTheory.Join.right a)),
  (match CategoryTheory.Join.left a with
    | CategoryTheory.Join.left a => h_1 a
    | CategoryTheory.Join.right a => h_2 a) =
    h_1 a
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.ins.eq_1 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (x : α),
  RBTree.RBNode.ins cmp x RBTree.RBNode.nil =
    RBTree.RBNode.node RBTree.RBColor.red RBTree.RBNode.nil x RBTree.RBNode.nil
-- Mathlib.Order.Interval.Basic
Interval.inf_coe : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DecidableLE α] (s t : NonemptyInterval α),
  ↑s ⊓ ↑t =
    if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
      ↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ }
    else ⊥
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.instCategoryAffineEtale : (S : AlgebraicGeometry.Scheme) → CategoryTheory.Category.{u_1, u_1 + 1} S.AffineEtale
-- Init.Data.Int.Linear
Int.Internal.Linear.le_combine_coeff_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → Bool
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Iic_castSucc : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a : Fin n),
  ∑ i ≤ a.castSucc, f i = ∑ i ≤ a, f i.castSucc
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- auxiliary construction for `coconesIso`  -/
CategoryTheory.Adjunction.coconesIsoComponentHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              {J : Type u} →
                [inst_2 : CategoryTheory.Category.{v, u} J] →
                  {K : CategoryTheory.Functor J C} →
                    (Y : D) →
                      ((CategoryTheory.cocones J D).obj (Opposite.op (K.comp F))).obj Y →
                        (G.comp ((CategoryTheory.cocones J C).obj (Opposite.op K))).obj Y
-- Mathlib.Data.ULift
ULift.instNonempty_mathlib : ∀ {α : Type u} [Nonempty α], Nonempty (ULift.{u_1, u} α)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.instOrderTopOfCompactSpaceOfNonempty : {α : Type u_1} →
  [inst : TopologicalSpace α] → [CompactSpace α] → [Nonempty α] → OrderTop (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.Geometry.Diffeology.Basic
/-- The Galois insertion between `DiffeologicalSpace X` and
`Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))` whose lower part sends a collection of plots in `X`
to the diffeology they generate, and whose upper part sends a diffeology to its collection of plots.
 -/
DiffeologicalSpace.giGenerateFrom : (X : Type u_2) → GaloisInsertion DiffeologicalSpace.generateFrom DiffeologicalSpace.toPlots
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.indep_limsup_atTop_self : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [inst : SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι],
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iIndep s μ →
      ProbabilityTheory.Indep (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) μ
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.foldM_eq_foldlM_toArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashSet.Raw α} {δ : Type v} {m' : Type v → Type w}
  [inst_2 : Monad m'] [LawfulMonad m'] {f : δ → α → m' δ} {init : δ},
  m.WF → Std.HashSet.Raw.foldM (fun d a => f d a) init m = Array.foldlM f init m.toArray
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
HomologicalComplex.truncGE'.truncGE'_hasHomology : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (i : ι), (K.truncGE' e).HasHomology i
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.strictMono_valueGroupOrderIso₀ : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [inst_1 : Ring R] (v : Valuation R Γ₀),
  StrictMono ⇑(WithVal.valueGroupOrderIso₀ v)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.LaxTrans.naturality_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.LaxTrans F G) {a b : B} {f g : a ⟶ b} (η : f ⟶ g)
  {Z : F.obj a ⟶ G.obj b} (h : CategoryTheory.CategoryStruct.comp (F.map g) (self.app b) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.naturality f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))
      (CategoryTheory.CategoryStruct.comp (self.naturality g) h)
-- Mathlib.Algebra.Order.Module.Pointwise
upperBounds_smul_of_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : GroupWithZero α] [inst_3 : Zero β]
  [inst_4 : MulActionWithZero α β] [PosSMulMono α β] [PosSMulReflectLE α β] {s : Set β} {a : α},
  0 < a → upperBounds (a • s) = a • upperBounds s
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.ofTree.eq_2 : ∀ (value : Unit) (l r : BinaryTree Unit),
  DyckWord.ofTree (BinaryTree.node value l r) = (DyckWord.ofTree l).nest + DyckWord.ofTree r
-- Mathlib.Data.Matrix.Basic
/-- The `AddEquiv` between spaces of matrices induced by an `AddEquiv` between their
coefficients. This is `Matrix.map` as an `AddEquiv`.  -/
AddEquiv.mapMatrix : {m : Type u_2} →
  {n : Type u_3} →
    {α : Type u_11} → {β : Type u_12} → [inst : Add α] → [inst_1 : Add β] → α ≃+ β → Matrix m n α ≃+ Matrix m n β
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.get?ₘ.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α),
  Std.DHashMap.Internal.Raw₀.Const.get?ₘ m a =
    Std.DHashMap.Internal.AssocList.get? a (Std.DHashMap.Internal.bucket (↑m).buckets ⋯ a)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
CauchySeq.const_mul : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} [inst_3 : Preorder ι]
  {u : ι → α} {x : α}, CauchySeq u → CauchySeq fun n => x * u n
-- Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
/-- Given a measurable function `f` with values in `ℝ≥0`, there exists a lower semicontinuous
function `g ≥ f` with integral arbitrarily close to that of `f`. Formulation in terms of
`lintegral`.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`.  -/
MeasureTheory.exists_le_lowerSemicontinuous_lintegral_ge : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α)
  [μ.WeaklyRegular] (f : α → ENNReal),
  Measurable f →
    ∀ {ε : ENNReal},
      ε ≠ 0 → ∃ g, (∀ (x : α), f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
groupHomology.δ.congr_simp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) (i j : ℕ) (hij : j + 1 = i), groupHomology.δ hX i j hij = groupHomology.δ hX i j hij
-- Lean.Meta.CongrTheorems
/-- The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : a_i ≍ b_i`.
`a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their heterogeneous equality.  -/
Lean.Meta.CongrArgKind.heq : Lean.Meta.CongrArgKind
-- Std.Time.Duration
/-- Adds a `Millisecond.Offset` to a `Duration`
 -/
Std.Time.Duration.subMilliseconds : Std.Time.Duration → Std.Time.Millisecond.Offset → Std.Time.Duration
-- Mathlib.Data.ENNReal.Operations
/-- If `a ≤ b + c`, `b ≠ ∞`, and `c ≠ ∞`, then
`ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c`. This lemma is useful to transfer
triangle-like inequalities from `ENNReal`s to `Real`s.  -/
ENNReal.toReal_le_add : ∀ {a b c : ENNReal}, a ≤ b + c → b ≠ ⊤ → c ≠ ⊤ → a.toReal ≤ b.toReal + c.toReal
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.spectralRadius_pow_le' : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [Nontrivial A] (a : A)
  (n : ℕ), spectralRadius 𝕜 a ^ n ≤ spectralRadius 𝕜 (a ^ n)
-- Std.Async.Select
/-- Atomically checks whether the `Waiter` has already finished. Note that right after this function
call ends this might have already changed.
 -/
Std.Async.Waiter.checkFinished : {m : Type → Type} → {α : Type} → [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → Std.Async.Waiter α → m Bool
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.Ordinal.instLTOfDay : LT Std.Time.Nanosecond.Ordinal.OfDay
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` preserves limits of shape `Jᵒᵖ`, then `F.leftOp : Cᵒᵖ ⥤ D` preserves colimits
of shape `J`.  -/
CategoryTheory.Limits.preservesColimitsOfShape_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C Dᵒᵖ)
  [CategoryTheory.Limits.PreservesLimitsOfShape Jᵒᵖ F], CategoryTheory.Limits.PreservesColimitsOfShape J F.leftOp
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.p_descOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0)
  [inst_2 : S.HasRightHomology], CategoryTheory.CategoryStruct.comp S.pOpcycles (S.descOpcycles k hk) = k
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.veq_rfl`. -/
ValuativeRel.veq.rfl : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x : R}, x =ᵥ x
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_initial_object : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D]
  {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) F],
  F.PreservesZeroMorphisms
-- Mathlib.Order.Interval.Finset.Defs
Subtype.instLocallyFiniteOrderTop.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrderTop α],
  Subtype.instLocallyFiniteOrderTop p =
    { finsetIoi := fun a => Finset.subtype p (Finset.Ioi ↑a), finsetIci := fun a => Finset.subtype p (Finset.Ici ↑a),
      finset_mem_Ici := ⋯, finset_mem_Ioi := ⋯ }
-- Init.Data.Ord.Array
_private.Init.Data.Ord.Array.0.Array.compareLex.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_2 ()
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.instMaxSubtypeMem : {α : Type u_1} → [inst : CompleteLattice α] → {L : CompleteSublattice α} → Max ↥L
-- Mathlib.Order.Category.HeytAlg
HeytAlg.instConcreteCategoryHeytingHomCarrier : CategoryTheory.ConcreteCategory HeytAlg fun x1 x2 => HeytingHom ↑x1 ↑x2
-- Init.Data.BitVec.Basic
BitVec.instHShiftLeftNat : {w : ℕ} → HShiftLeft (BitVec w) ℕ (BitVec w)
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_eq_iff : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] {f : ι → M} {s : Set ι},
  Function.mulSupport f = s ↔ (∀ x ∈ s, f x ≠ 1) ∧ ∀ x ∉ s, f x = 1
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.mapRangeAlgHom_comp : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {C : Type u_6} {M : Type u_7} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B]
  [inst_6 : Algebra R C] [inst_7 : AddMonoid M] (f : A →ₐ[R] B) (g : B →ₐ[R] C),
  AddMonoidAlgebra.mapAlgHom M (g.comp f) = (AddMonoidAlgebra.mapAlgHom M g).comp (AddMonoidAlgebra.mapAlgHom M f)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.Monic.coeff_natDegree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → p.coeff p.natDegree = 1
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.cons_cons : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {p : α × Bool}, FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red (p :: L₁) (p :: L₂)
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.iteratedDeriv_two_cgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ},
  v ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    iteratedDeriv 2 (ProbabilityTheory.cgf X μ) v =
      (∫ (x : Ω), (fun ω => X ω ^ 2 * Real.exp (v * X ω)) x ∂μ) / ProbabilityTheory.mgf X μ v -
        deriv (ProbabilityTheory.cgf X μ) v ^ 2
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.eraseManyEntries!_impl_eq_foldl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β},
  ↑(t₁.eraseManyEntries! t₂) =
    Std.DTreeMap.Internal.Impl.foldl (fun acc k x_1 => Std.DTreeMap.Internal.Impl.erase! k acc) t₁ t₂
-- Std.Data.DHashMap.Raw
_private.Std.Data.DHashMap.Raw.0.Std.DHashMap.Raw.getThenInsertIfNew?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] (m : Std.DHashMap.Raw α β)
  (a : α) (b : β a),
  m.getThenInsertIfNew? a b =
    if h : 0 < m.buckets.size then
      match Std.DHashMap.Internal.Raw₀.getThenInsertIfNew? ⟨m, h⟩ a b with
      | (previous, ⟨r, property⟩) => (previous, r)
    else (none, m)
-- Mathlib.Order.Hom.Basic
OrderHom.apply_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (x : α),
  ⇑(OrderHom.apply x) = Function.eval x ∘ fun f => ⇑f
-- Init.Data.Vector.Lemmas
Vector.back?_append : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m}, (xs ++ ys).back? = ys.back?.or xs.back?
-- Mathlib.Order.Hom.Lex
OrderIso.sumLexIioIci_apply_inr : ∀ {α : Type u_1} [inst : LinearOrder α] {x : α} (a : ↑(Set.Ici x)), (OrderIso.sumLexIioIci x) (toLex (Sum.inr a)) = ↑a
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.toPresentation_val : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePresentation R S) (a : Fin 2),
  P.toPresentation.val a =
    (P.lift P.x ⋯)
      (P.equivMvPolynomialQuotient.symm
        ((Ideal.Quotient.mk
            (Ideal.span
              {(Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C P.f),
                (Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.X * Polynomial.C P.g - 1)}))
          (MvPolynomial.X a)))
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- A topological group that has a `ContinuousMulEquiv` to a profinite group is profinite.  -/
ProfiniteGrp.ofContinuousMulEquiv : {G : ProfiniteGrp.{u}} →
  {H : Type v} →
    [inst : TopologicalSpace H] →
      [inst_1 : Group H] → [IsTopologicalGroup H] → ↑G.toProfinite.toTop ≃ₜ* H → ProfiniteGrp.{v}
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAddMonoid : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [AddMonoid Y] → AddMonoid (LocallyConstant X Y)
-- Init.Data.BitVec.Lemmas
BitVec.msb_one : ∀ {w : ℕ}, (1#w).msb = decide (w = 1)
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.idRSS : Std.Internal.UV.System.RUsage → UInt64
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
integralClosure_eq_top_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  integralClosure R A = ⊤ ↔ Algebra.IsIntegral R A
-- Mathlib.Algebra.Lie.Basic
/-- The inverse of a bijective morphism of Lie modules is a morphism of Lie modules.  -/
LieModuleHom.inverse : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] →
                      [inst_7 : LieRingModule L N] →
                        (f : M →ₗ⁅R,L⁆ N) →
                          (g : N → M) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → N →ₗ⁅R,L⁆ M
-- Mathlib.Data.QPF.Multivariate.Constructions.Const
/-- `map` for constant functor  -/
MvQPF.Const.map : {n : ℕ} → {A : Type u} → {α β : TypeVec.{u} n} → MvQPF.Const n A α → MvQPF.Const n A β
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.RepresentablyCoflat.filtered : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.RepresentablyCoflat F] (X : D),
  CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow F X)
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- The standard resolution of `k` as a trivial representation, defined as the alternating
face map complex of a simplicial `k`-linear `G`-representation.  -/
Rep.standardComplex : (k G : Type u) → [inst : CommRing k] → [inst_1 : Monoid G] → ChainComplex (Rep.{u, u, u} k G) ℕ
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.instIsScalarTowerTensorProduct : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing A] [inst_4 : Algebra R A], IsScalarTower R A (TensorProduct R S Ω[A⁄R])
-- Std.Async.Select
/-- Registers a `Waiter` with the event source. Once data is available, the event source should
attempt to call `Waiter.race` and resolve the `Waiter`'s promise if it wins. It is crucial that
data is never actually consumed from the event source unless `Waiter.race` wins in order to
prevent data loss.
 -/
Std.Async.Selector.registerFn : {α : Type} → Std.Async.Selector α → Std.Async.Waiter α → Std.Async.Async Unit
-- Batteries.Data.List.Basic
/-- Left-biased version of `List.zip`. `zipLeft as bs` returns the list of pairs
`(aᵢ, bᵢ)` for `aᵢ ∈ as` and `bᵢ ∈ bs`. If `bs` is shorter than `as`, the
remaining `aᵢ` are paired with `none`.
```
zipLeft [1, 2] ['a'] = [(1, some 'a'), (2, none)]
zipLeft [1] ['a', 'b'] = [(1, some 'a')]
zipLeft = zipWithLeft prod.mk
```
 -/
List.zipLeft : {α : Type u_1} → {β : Type u_2} → List α → List β → List (α × Option β)
-- Mathlib.ModelTheory.Basic
/-- In an algebraic language, any injective homomorphism is an embedding.  -/
FirstOrder.Language.Embedding.ofInjective : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] → [L.IsAlgebraic] → {f : L.Hom M N} → Function.Injective ⇑f → L.Embedding M N
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_comm : ∀ {G : Type u_1} [inst : Group G] (H₁ H₂ : Subgroup G), ⁅H₁, H₂⁆ = ⁅H₂, H₁⁆
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
MeasureTheory.IntegrableOn.continuousOn_Iic_primitive_Iio : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {f : ℝ → E}
  [MeasureTheory.NullSingletonClass μ] {a₀ : ℝ},
  MeasureTheory.IntegrableOn f (Set.Iio a₀) μ → ContinuousOn (fun b => ∫ (x : ℝ) in Set.Iio b, f x ∂μ) (Set.Iic a₀)
-- Batteries.Lean.Meta.UnusedNames
/-- Exact match.  -/
Lean.Name.MatchUpToIndexSuffix.exactMatch : Lean.Name.MatchUpToIndexSuffix
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.of_smul_right : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter α} {g : Filter β}, (f • g).NeBot → g.NeBot
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.Nonempty.exists_prop : ∀ {C : Type u} {inst : CategoryTheory.CategoryStruct.{v, u} C} {P : CategoryTheory.ObjectProperty C}
  [self : P.Nonempty], ∃ X, P X