mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
/-- Each `projectiveFamily I` is the centered Gaussian measure with covariance matrix given
by `covMatrix I s t := min s t`.

Note that we build a measure over `I → ℝ` rather than `EuclideanSpace I ℝ`. This is because
we want to extend this family to a measure over `ℝ≥0 → ℝ` through the Kolmogorov's extension
theorem, which is phrased in this language.  -/
ProbabilityTheory.BrownianReal.projectiveFamily : (I : Finset NNReal) → MeasureTheory.Measure (↥I → ℝ)
-- Init.Data.ByteArray.Lemmas
ByteArray.getElem_set! : ∀ (data : ByteArray) (i j : ℕ) (v : UInt8),
  i < data.size → ∀ (hj : j < data.size), (data.set! i v)[j] = if i = j then v else data[j]
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.boundaryGE_embeddingUpIntGE_iff : ∀ (p : ℤ) (n : ℕ), (ComplexShape.embeddingUpIntGE p).BoundaryGE n ↔ n = 0
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.measureReal_fundamentalDomain : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Module.Basis ι ℝ E)
  [inst_2 : Fintype ι] [inst_3 : DecidableEq ι] [inst_4 : MeasurableSpace E] (μ : MeasureTheory.Measure E)
  [BorelSpace E] [μ.IsAddHaarMeasure] (b₀ : Module.Basis ι ℝ E),
  μ.real (ZSpan.fundamentalDomain b) = |b₀.det ⇑b| * μ.real (ZSpan.fundamentalDomain b₀)
-- Mathlib.Analysis.Convex.Continuous
ConvexOn.continuousOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {C : Set E} {f : E → ℝ}
  [FiniteDimensional ℝ E], IsOpen C → ConvexOn ℝ C f → ContinuousOn f C
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If a function `f` with a densely ordered codomain is monotone on a neighborhood of `a` and the
closure of the image of this neighborhood under `f` is a neighborhood of `f a`, then `f` is
continuous at `a`.  -/
continuousAt_of_monotoneOn_of_closure_image_mem_nhds : ∀ {α : 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 ∈ nhds a → closure (f '' s) ∈ nhds (f a) → ContinuousAt f a
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.IsWeakLimit.equivIsoWeakLimit_apply : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cone F}
  (i : r ≅ t) (P : CategoryTheory.Limits.IsWeakLimit r),
  (CategoryTheory.Limits.IsWeakLimit.equivIsoWeakLimit i) P = P.ofIsoWeakLimit i
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Constructing an equivalence `isColimit c ≃ isColimit d` from a natural isomorphism
between the underlying functors, and then an isomorphism between `c` transported along this and `d`.
 -/
CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} →
          (α : F ≅ G) →
            (c : CategoryTheory.Limits.Cocone F) →
              (d : CategoryTheory.Limits.Cocone G) →
                ((CategoryTheory.Limits.Cocone.precompose α.inv).obj c ≅ d) →
                  CategoryTheory.Limits.IsColimit c ≃ CategoryTheory.Limits.IsColimit d
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.IsRoot.eq_1 : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (a : R), p.IsRoot a = (Polynomial.eval a p = 0)
-- Lean.Environment
_private.Lean.Environment.0.Lean.looksLikeOldCodegenName : Lean.Name → Bool
-- Mathlib.CategoryTheory.Action.Basic
Action.inv_hom_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (f : M ≅ N), CategoryTheory.CategoryStruct.comp f.inv.hom f.hom.hom = CategoryTheory.CategoryStruct.id N.V
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (X : C) →
      (p : X ⟶ X) →
        autoParam (CategoryTheory.CategoryStruct.comp p p = p) CategoryTheory.Idempotents.Karoubi.idem._autoParam →
          CategoryTheory.Idempotents.Karoubi C
-- Mathlib.Data.TypeVec
TypeVec.dropFun_id : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)}, TypeVec.dropFun TypeVec.id = TypeVec.id
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
instSMulMemClassHomogeneousSubmodule : ∀ {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [inst : Semiring A]
  [inst_1 : AddCommMonoid M] [inst_2 : Module A M] (𝒜 : ιA → σA) (ℳ : ιM → σM) [inst_3 : DecidableEq ιA]
  [inst_4 : AddMonoid ιA] [inst_5 : SetLike σA A] [inst_6 : AddSubmonoidClass σA A] [inst_7 : GradedRing 𝒜]
  [inst_8 : DecidableEq ιM] [inst_9 : SetLike σM M] [inst_10 : AddSubmonoidClass σM M]
  [inst_11 : DirectSum.Decomposition ℳ] [inst_12 : VAdd ιA ιM] [inst_13 : SetLike.GradedSMul 𝒜 ℳ],
  SMulMemClass (HomogeneousSubmodule 𝒜 ℳ) A M
-- Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
associated_of_factorization_eq : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : NormalizationMonoid α]
  [inst_3 : DecidableEq α] (a b : α), a ≠ 0 → b ≠ 0 → factorization a = factorization b → Associated a b
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitDiagInfo.gen : Lean.Meta.Grind.SplitDiagInfo → ℕ
-- Lean.Meta.CoeAttr
Lean.Meta.CoeFnInfo.mk.injEq : ∀ (numArgs coercee : ℕ) (type : Lean.Meta.CoeFnType) (numArgs_1 coercee_1 : ℕ) (type_1 : Lean.Meta.CoeFnType),
  ({ numArgs := numArgs, coercee := coercee, type := type } =
      { numArgs := numArgs_1, coercee := coercee_1, type := type_1 }) =
    (numArgs = numArgs_1 ∧ coercee = coercee_1 ∧ type = type_1)
-- Init.Core
Lean.Name.num.injEq : ∀ (pre : Lean.Name) (i : ℕ) (pre_1 : Lean.Name) (i_1 : ℕ), (pre.num i = pre_1.num i_1) = (pre = pre_1 ∧ i = i_1)
-- Mathlib.Topology.Order.MonotoneConvergence
OrderDual.infConvergenceClass : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [SupConvergenceClass α], InfConvergenceClass αᵒᵈ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- `BinaryBiproduct.bicone P Q` is a limit bicone.  -/
CategoryTheory.Limits.BinaryBiproduct.isBilimit : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (P Q : C) →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q] →
          (CategoryTheory.Limits.BinaryBiproduct.bicone P Q).IsBilimit
-- Mathlib.RingTheory.Localization.Cardinality
/-- A localization always has cardinality less than or equal to the base ring.  -/
IsLocalization.cardinalMk_le : ∀ {R : Type u} [inst : CommSemiring R] {L : Type u} [inst_1 : CommSemiring L] [inst_2 : Algebra R L] (S : Submonoid R)
  [IsLocalization S L], Cardinal.mk L ≤ Cardinal.mk R
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
TensorAlgebra.toClifford.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M}, TensorAlgebra.toClifford = (TensorAlgebra.lift R) (CliffordAlgebra.ι Q)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_insert_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (cmp ((t.insert k v).minKey ⋯) k).isLE = true
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.coe_mk : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] (f : M → N) (h1 : f 1 = 1),
  ⇑{ toFun := f, map_one' := h1 } = f
-- Mathlib.Data.EReal.Basic
EReal.coe_nonpos : ∀ {x : ℝ}, ↑x ≤ 0 ↔ x ≤ 0
-- Mathlib.Data.Real.ConjExponents
NNReal.holderConjugate_iff_eq_conjExponent : ∀ {p q : NNReal}, 1 < p → (p.HolderConjugate q ↔ q = p / (p - 1))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_union_of_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → k ∈ t₁ ∪ t₂
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedDeclValue : {a : Lean.Compiler.LCNF.Purity} → Inhabited (Lean.Compiler.LCNF.DeclValue a)
-- Mathlib.Tactic.Observe
/-- `observe hp : p` asserts the proposition `p` as a hypothesis named `hp`, and tries to prove it
using `exact?`.
If no proof is found, the tactic fails.
In other words, this tactic is equivalent to `have hp : p := by exact?`.

* `observe : p` uses the name `this` for the new hypothesis.
* `observe? hp : p` will emit a trace message of the form `have hp : p := proof_term`.
  This may be particularly useful to speed up proofs.
 -/
Mathlib.Tactic.LibrarySearch.«tacticObserve?__:_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_hom_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [inst_1 : P.IsClosedUnderMapObj] {X Y Z : B} (f : X ⟶ Y) (g : Y ⟶ Z) (M : P.Obj X),
  (P.mapComp f g).hom.app M = CategoryTheory.ObjectProperty.homMk ((F.mapComp f g).hom.toNatTrans.app M.obj)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.map.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β), FreeGroup.map f = MonoidHom.mk' (Quot.map (List.map fun x => (f x.1, x.2)) ⋯) ⋯
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.instEffectiveEpiFamilyObjMapOfIsEquivalence : ∀ {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] {B : C} {α : Type u_3} (X : α → C) (π : (a : α) → X a ⟶ B)
  [CategoryTheory.EffectiveEpiFamily X π] (F : CategoryTheory.Functor C D) [F.IsEquivalence],
  CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)
-- Lean.Parser.Term
/-- `haveI` behaves like `have`, but inlines the value instead of producing a `have` term.  -/
Lean.Parser.Term.haveI : Lean.Parser.Parser
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.unitsWithZeroEquiv_symm_apply : ∀ {α : Type u_1} [inst : Group α] (a : α), WithZero.unitsWithZeroEquiv.symm a = Units.mk0 ↑a ⋯
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.ConjClasses.eq_1 : ∀ {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.ConjClasses = Quotient (GroupExtension.IsConj.setoid S)
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
VectorBundleCore.IsContMDiff.mk : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] {EB : Type u_7}
  [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_3 : TopologicalSpace HB]
  [inst_4 : TopologicalSpace B] [inst_5 : ChartedSpace HB B] [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F]
  {ι : Type u_11} {Z : VectorBundleCore 𝕜 B F ι} {IB : ModelWithCorners 𝕜 EB HB} {n : WithTop ℕ∞},
  (∀ (i j : ι), ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (Z.coordChange i j) (Z.baseSet i ∩ Z.baseSet j)) →
    Z.IsContMDiff IB n
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegrable_const : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
  [MeasureTheory.IsLocallyFiniteMeasure μ] {c : E}, IntervalIntegrable (fun x => c) μ a b
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
IsQuasiregular.isUnit_one_add : ∀ {R : Type u_1} [inst : Semiring R] {x : R}, IsQuasiregular x → IsUnit (1 + x)
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.instFGUnitsRingOfIntegers : ∀ (K : Type u_1) [inst : Field K] [NumberField K], Monoid.FG (NumberField.RingOfIntegers K)ˣ
-- Aesop.Tree.Data
Aesop.Goal.originalGoalId : Aesop.Goal → Aesop.GoalId
-- Std.Time.Notation
/-- Defines a syntax for datetime values without timezone. The input should be a string in an
ISO8601-like format.

Example:
`datetime("2024-10-13T15:00:00")`
 -/
Std.Time.«termDatetime(_)» : Lean.ParserDescr
-- Init.Data.UInt.Bitwise
USize.toUInt64_shiftLeft : ∀ (a b : USize),
  (a <<< b).toUInt64 = a.toUInt64 <<< (b % USize.ofNat System.Platform.numBits).toUInt64 % UInt64.ofNat USize.size
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.CofixA.instSubsingleton : ∀ {F : PFunctor.{uA, uB}}, Subsingleton (PFunctor.Approx.CofixA F 0)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_neg : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] (a : Aˣ) (x : ℝ),
  autoParam (0 ≤ ↑a) CFC.rpow_neg._auto_1 → ↑a ^ (-x) = ↑a⁻¹ ^ x
-- Mathlib.Order.Filter.Pointwise
/-- A multiplicative action of a monoid on a type `β` gives a multiplicative action on `Filter β`.
 -/
Filter.mulActionFilter : {α : Type u_2} → {β : Type u_3} → [inst : Monoid α] → [MulAction α β] → MulAction α (Filter β)
-- Mathlib.Topology.Instances.Shrink
/-- `equivShrink` as a homeomorphism.  -/
Shrink.homeomorph : (X : Type u) → [inst : TopologicalSpace X] → [inst_1 : Small.{v, u} X] → X ≃ₜ Shrink.{v, u} X
-- Mathlib.RingTheory.Spectrum.Prime.Noetherian
IsArtinianRing.finrank_eq_sum_primeSpectrum : ∀ (R : Type u_1) [inst : CommRing R] [IsArtinianRing R] (F : Type u_2) [inst_2 : Field F] [inst_3 : Algebra F R]
  [Module.Finite F R] [inst_5 : Fintype (PrimeSpectrum R)],
  Module.finrank F R = ∑ p, Module.finrank F (Localization.AtPrime p.asIdeal)
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsExtTangent.dist_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s₁ s₂ : EuclideanGeometry.Sphere P},
  s₁.IsExtTangent s₂ → dist s₁.center s₂.center = s₁.radius + s₂.radius
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
/-- The natural isomorphism `(K⟦n⟧).sc i ≅ K.sc i'` when `n + i = i'`.  -/
CochainComplex.shiftShortComplexFunctorIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (n i i' : ℤ) →
        n + i = i' →
          ((CochainComplex.shiftFunctor C n).comp (HomologicalComplex.shortComplexFunctor C (ComplexShape.up ℤ) i) ≅
            HomologicalComplex.shortComplexFunctor C (ComplexShape.up ℤ) i')
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.liftOfStrictSegal.hδ'₀ : ∀ {X Y : SSet.Truncated 2}
  (f₀ :
    X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) →
      Y.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }))
  (f₁ :
    X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) →
      Y.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }))
  (hδ₁ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hδ₀ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hY : Y.StrictSegal) (x : X.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ })),
  f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝ _proof_15✝).op)) x) =
    (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝ _proof_15✝).op))
      (SSet.Truncated.liftOfStrictSegal.f₂ f₀ f₁ hδ₁ hδ₀ hY x)
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeIdeal_inj' : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [loc : IsLocalization S P], S ≤ nonZeroDivisors R → ∀ {I J : Ideal R}, ↑I = ↑J ↔ I = J
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- a right homology map data  -/
CategoryTheory.ShortComplex.HomologyMapData.right : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.HomologyData} →
            {h₂ : S₂.HomologyData} →
              CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂ →
                CategoryTheory.ShortComplex.RightHomologyMapData φ h₁.right h₂.right
-- Mathlib.Data.SetLike.Basic
/-- The coercion from a `SetLike` type preserves the ordering.  -/
IsConcreteLE.coe_subset_coe' : ∀ {A : Type u_1} {B : outParam (Type u_2)} {inst : SetLike A B} {inst_1 : LE A} [self : IsConcreteLE A B] {S T : A},
  ↑S ⊆ ↑T ↔ S ≤ T
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k : α}, (List.map Sigma.fst l).contains k = false → (t.insertMany l).get? k = t.get? k
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
UniqueFactorizationMonoid.factors_unique : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] {f g : Multiset α},
  (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → Associated f.prod g.prod → Multiset.Rel Associated f g
-- Mathlib.Algebra.Order.Group.End
RelEmbedding.instMonoid : {α : Type u_1} → {r : α → α → Prop} → Monoid (r ↪r r)
-- Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
/-- The infinite product of strongly measurable functions is measurable.  -/
MeasureTheory.StronglyMeasurable.tprod : ∀ {X : Type u_4} {E : Type u_5} {ι : Type u_6} [inst : MeasurableSpace X] [inst_1 : CommMonoid E]
  [inst_2 : TopologicalSpace E] [ContinuousMul E] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace E] [Countable ι] {f : ι → X → E},
  (∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) → MeasureTheory.StronglyMeasurable fun x => ∏'[L] (i : ι), f i x
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.minEntryD : {α : Type u} → {β : Type v} → (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → α × β
-- Std.Sat.CNF.Literal
/-- Flip the polarity of `l`.
 -/
Std.Sat.Literal.negate : {α : Type u_1} → Std.Sat.Literal α → Std.Sat.Literal α
-- Mathlib.Probability.Moments.SubGaussian
/-- For `ν : Measure Ω'`, `κ : Kernel Ω' Ω` and `η : (Ω' × Ω) Ω''`, if a random variable `X : Ω → ℝ`
has a sub-Gaussian mgf with respect to `κ` and `ν` and another random variable `Y : Ω'' → ℝ` has
a sub-Gaussian mgf with respect to `η` and `ν ⊗ₘ κ : Measure (Ω' × Ω)`, then `X + Y` (random
variable on the measurable space `Ω × Ω''`) has a sub-Gaussian mgf with respect to
`κ ⊗ₖ η : Kernel Ω' (Ω × Ω'')` and `ν`.  -/
ProbabilityTheory.Kernel.HasSubgaussianMGF.add_compProd : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal} {Ω'' : Type u_3} {mΩ'' : MeasurableSpace Ω''}
  {Y : Ω'' → ℝ} {cY : NNReal} [MeasureTheory.SFinite ν] {η : ProbabilityTheory.Kernel (Ω' × Ω) Ω''}
  [ProbabilityTheory.IsZeroOrMarkovKernel η],
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν →
    ProbabilityTheory.Kernel.HasSubgaussianMGF Y cY η (ν.compProd κ) →
      ProbabilityTheory.Kernel.HasSubgaussianMGF (fun p => X p.1 + Y p.2) (c + cY) (κ.compProd η) ν
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_le_maxKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k : α} {v : β k} {km kmi : α},
  t.maxKey? = some km → (t.insert k v).maxKey?.get ⋯ = kmi → (cmp km kmi).isLE = true
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inlX_fstX_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel j i) {Z : C} (h : F.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hij)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ j i hij) h) =
    h
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.eq_of_toNormPoly_eq : ∀ (ctx : Nat.Internal.Linear.Context) (c d : Nat.Internal.Linear.ExprCnstr),
  (c.toNormPoly == d.toPoly) = true →
    Nat.Internal.Linear.ExprCnstr.denote ctx c = Nat.Internal.Linear.ExprCnstr.denote ctx d
-- Init.Data.List.Nat.Basic
List.length_filterMap_lt_length_iff_exists : ∀ {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → Option β},
  (List.filterMap f xs).length < xs.length ↔ ∃ x, ∃ (_ : x ∈ xs), f x = none
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.unitBallBall.congr_simp : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {P : Type u_2}
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor E P] (c c_1 : P),
  c = c_1 →
    ∀ (r r_1 : ℝ) (e_r : r = r_1) (hr : 0 < r),
      OpenPartialHomeomorph.unitBallBall c r hr = OpenPartialHomeomorph.unitBallBall c_1 r_1 ⋯
-- Lean.Elab.Command
Lean.Elab.Command.Context.fileName : Lean.Elab.Command.Context → String
-- Mathlib.Order.Nat
Nat.bot_eq_zero : ⊥ = 0
-- Lean.Server.InfoUtils
Lean.Elab.InfoWithCtx.info : Lean.Elab.InfoWithCtx → Lean.Elab.Info
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_inv_coe_angle : ∀ (x : ℂ), ↑x⁻¹.arg = -↑x.arg
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given two Localization maps `f : M →+ N, k : M →+ P` for a Submonoid `S ⊆ M`, the hom
from `P` to `N` induced by `f` is left inverse to the hom from `N` to `P` induced by `k`.  -/
AddSubmonoid.LocalizationMap.lift_left_inverse : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {k : S.LocalizationMap P} (z : N), (k.lift ⋯) ((f.lift ⋯) z) = z
-- Mathlib.Algebra.Group.Nat.Even
Nat.even_iff : ∀ {n : ℕ}, Even n ↔ n % 2 = 0
-- Mathlib.RingTheory.Ideal.Prod
Ideal.span_prod : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {s : Set R} {t : Set S},
  (s.Nonempty ↔ t.Nonempty) → Ideal.span (s ×ˢ t) = (Ideal.span s).prod (Ideal.span t)
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_arrow : ∀ (α : Type u) (β : Type v),
  Cardinal.mk (α → β) = Cardinal.lift.{u, v} (Cardinal.mk β) ^ Cardinal.lift.{v, u} (Cardinal.mk α)
-- Mathlib.Order.Interval.Set.ProjIcc
Set.range_projIci : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, Set.range (Set.projIci a) = Set.univ
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Fintype.piFinset_sub : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → Sub (α i)] (s t : (i : ι) → Finset (α i)),
  (Fintype.piFinset fun i => s i - t i) = Fintype.piFinset s - Fintype.piFinset t
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.IsThreeCycle.nodup_iff_mem_support : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {g : Equiv.Perm α} {a : α},
  g.IsThreeCycle → ([a, g a, g (g a)].Nodup ↔ a ∈ g.support)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_neg : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E],
  ⇑(LinearIsometryEquiv.neg R) = fun x => -x