mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.Monotone
/-- An antitone function continuous at the indexed infimum over a nonempty `Sort` sends this indexed
infimum to the indexed supremum of the composition.  -/
Antitone.map_ciInf_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β]
  {ι : Sort u_3} [Nonempty ι] {f : α → β} {g : ι → α},
  ContinuousAt f (iInf g) →
    Antitone f →
      autoParam (BddBelow (Set.range g)) Antitone.map_ciInf_of_continuousAt._auto_1 → f (⨅ i, g i) = ⨆ i, f (g i)
-- Lean.Meta.Sym.Arith.Poly
_private.Lean.Meta.Sym.Arith.Poly.0.Lean.Grind.CommRing.Mon.lcm.eq_def : ∀ (x x_1 : Lean.Grind.CommRing.Mon),
  x.lcm x_1 =
    match x, x_1 with
    | Lean.Grind.CommRing.Mon.unit, m₂ => m₂
    | m₁, Lean.Grind.CommRing.Mon.unit => m₁
    | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ =>
      match compare pw₁.x pw₂.x with
      | Ordering.eq => Lean.Grind.CommRing.Mon.mult { x := pw₁.x, k := max pw₁.k pw₂.k } (m₁.lcm m₂)
      | Ordering.lt => Lean.Grind.CommRing.Mon.mult pw₁ (m₁.lcm (Lean.Grind.CommRing.Mon.mult pw₂ m₂))
      | Ordering.gt => Lean.Grind.CommRing.Mon.mult pw₂ ((Lean.Grind.CommRing.Mon.mult pw₁ m₁).lcm m₂)
-- Mathlib.Algebra.Module.GradedModule
_private.Mathlib.Algebra.Module.GradedModule.0.DirectSum.Gmodule.mul_smul' : ∀ {ιA : Type u_1} {ιB : Type u_2} (A : ιA → Type u_3) (M : ιB → Type u_4) [inst : AddMonoid ιA] [inst_1 : VAdd ιA ιB]
  [inst_2 : (i : ιA) → AddCommMonoid (A i)] [inst_3 : (i : ιB) → AddCommMonoid (M i)] [inst_4 : DecidableEq ιA]
  [inst_5 : DecidableEq ιB] [inst_6 : DirectSum.GSemiring A] [inst_7 : DirectSum.Gmodule A M]
  (a b : DirectSum ιA fun i => A i) (c : DirectSum ιB fun i => M i), (a * b) • c = a • b • c
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.coe_pow : ∀ {G : Type u_1} [inst : Add G] {a : G} (f : AddConstMap G G a a) (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
-- Mathlib.Data.List.Monad
List.instAlternativeMonad_mathlib : AlternativeMonad List
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- An auxiliary definition for `descHomotopyZero`.  -/
CategoryTheory.InjectiveResolution.descHomotopyZeroSucc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {Y Z : C} →
        {I : CategoryTheory.InjectiveResolution Y} →
          {J : CategoryTheory.InjectiveResolution Z} →
            (f : I.cocomplex ⟶ J.cocomplex) →
              (n : ℕ) →
                (g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) →
                  (g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) →
                    f.f (n + 1) =
                        CategoryTheory.CategoryStruct.comp (I.cocomplex.d (n + 1) (n + 2)) g' +
                          CategoryTheory.CategoryStruct.comp g (J.cocomplex.d n (n + 1)) →
                      (I.cocomplex.X (n + 3) ⟶ J.cocomplex.X (n + 2))
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- The global sections, notated Gamma.
 -/
AlgebraicGeometry.PresheafedSpace.Γ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.Functor (AlgebraicGeometry.PresheafedSpace C)ᵒᵖ C
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.coe_set_eq : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (L₁' L₂' : LieSubalgebra R L), ↑L₁' = ↑L₂' ↔ L₁' = L₂'
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.mem_homogeneousSubmodule : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (n : ℕ) (p : MvPolynomial σ R),
  p ∈ MvPolynomial.homogeneousSubmodule σ R n ↔ p.IsHomogeneous n
-- Mathlib.Condensed.Light.Functors
instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet : lightProfiniteToLightCondSet.Full
-- Mathlib.Order.SuccPred.CompleteLinearOrder
sSup_mem_of_not_isSuccPrelimit : ∀ {α : Type u_2} [inst : CompleteLinearOrder α] {s : Set α}, ¬Order.IsSuccPrelimit (sSup s) → sSup s ∈ s
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_add_right : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} (X : Ω → ENNReal) {Y : Ω → ENNReal},
  AEMeasurable Y P → P⁻[X + Y | mΩ] =ᵐ[P] P⁻[X | mΩ] + P⁻[Y | mΩ]
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOpId_inv_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖᵒᵖ),
  (CategoryTheory.Functor.leftOpId C).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.unop X))
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- If an invariant measure is inner regular, then it gives the same mass to measurable sets with
compact closure as any other invariant measure, up to the scalar `haarScalarFactor μ' μ`.

Auxiliary lemma in the proof of the more general
`measure_isMulInvariant_eq_smul_of_isCompact_closure`, which works for any set with
compact closure, and removes the inner regularity assumption.  -/
MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsMulLeftInvariant]
  [μ.InnerRegularCompactLTTop] {s : Set G}, MeasurableSet s → IsCompact (closure s) → μ' s = μ'.haarScalarFactor μ • μ s
-- Mathlib.Algebra.Order.GroupWithZero.Basic
lt_mul_iff_one_lt_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [PosMulStrictMono α]
  [PosMulReflectLT α], 0 < a → (a < a * b ↔ 1 < b)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.canonical_right_H : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.HomologyData.canonical S).right.H = S.homology
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.instCategoryAugmented : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Category.{v, max u v} (CategoryTheory.SimplicialObject.Augmented C)
-- Lean.Declaration
Lean.ConstantInfo.ctorInfo : Lean.ConstructorVal → Lean.ConstantInfo
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.edgeSet.ext_iff : ∀ {α : Type u_1} {e e' : Set α} {H : Hypergraph α},
  e ∈ H.edgeSet → e' ∈ H.edgeSet → (e = e' ↔ ∀ x ∈ H.vertexSet, x ∈ e ↔ x ∈ e')
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.get!_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α] {k : α}, m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.get! k = m₂.get! k
-- Mathlib.Algebra.CubicDiscriminant
/-- The degree-2 coefficient  -/
Cubic.b : {R : Type u_1} → Cubic R → R
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.instSemiring : {R : Type u_1} → [inst : Semiring R] → Semiring (ArithmeticFunction R)
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.getEntry? : {α : Type u} → {β : α → Type v} → [BEq α] → α → List ((a : α) × β a) → Option ((a : α) × β a)
-- Batteries.Data.AssocList
Batteries.AssocList.toList.eq_1 : ∀ {α : Type u_1} {β : Type u_2}, Batteries.AssocList.nil.toList = []
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.Total.Hom.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  {k l : CategoryTheory.Limits.ColimitPresentation.Total P} (base base_1 : k.fst ⟶ l.fst) (e_base : base = base_1)
  (hom hom_1 : (P k.fst).diag.obj k.snd ⟶ (P l.fst).diag.obj l.snd) (e_hom : hom = hom_1)
  (w :
    CategoryTheory.CategoryStruct.comp ((P k.fst).ι.app k.snd) (D.map base) =
      CategoryTheory.CategoryStruct.comp hom ((P l.fst).ι.app l.snd)),
  { base := base, hom := hom, w := w } = { base := base_1, hom := hom_1, w := ⋯ }
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.ins.eq_def : ∀ {α : Type u_1} (cmp : α → α → Ordering) (x : α) (x_1 : RBTree.RBNode α),
  RBTree.RBNode.ins cmp x x_1 =
    match x_1 with
    | RBTree.RBNode.nil => RBTree.RBNode.node RBTree.RBColor.red RBTree.RBNode.nil x RBTree.RBNode.nil
    | RBTree.RBNode.node RBTree.RBColor.red a y b =>
      match cmp x y with
      | Ordering.lt => RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.ins cmp x a) y b
      | Ordering.gt => RBTree.RBNode.node RBTree.RBColor.red a y (RBTree.RBNode.ins cmp x b)
      | Ordering.eq => RBTree.RBNode.node RBTree.RBColor.red a x b
    | RBTree.RBNode.node RBTree.RBColor.black a y b =>
      match cmp x y with
      | Ordering.lt => (RBTree.RBNode.ins cmp x a).balance1 y b
      | Ordering.gt => a.balance2 y (RBTree.RBNode.ins cmp x b)
      | Ordering.eq => RBTree.RBNode.node RBTree.RBColor.black a x b
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.minEntry.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.isEmpty = false → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : x.isEmpty = false) →
          ((size : ℕ) →
              (k : α) →
                (v : β k) →
                  (r : Std.DTreeMap.Internal.Impl α β) →
                    (x :
                        (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false) →
                      motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (size_1 : ℕ) →
                      (k_1 : α) →
                        (v_1 : β k_1) →
                          (l r r_1 : Std.DTreeMap.Internal.Impl α β) →
                            (h :
                                (Std.DTreeMap.Internal.Impl.inner size k v
                                      (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).isEmpty =
                                  false) →
                              motive
                                (Std.DTreeMap.Internal.Impl.inner size k v
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
                                h) →
              motive x x_1
-- Init.Data.SInt.Lemmas
Int8.toISize_div_of_ne_left : ∀ (a b : Int8), a ≠ Int8.minValue → (a / b).toISize = a.toISize / b.toISize
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.ShiftSequence.shiftIso.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] (n a a' : ℤ) (ha' : n + a = a'),
  CochainComplex.ShiftSequence.shiftIso C n a a' ha' =
    (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).isoWhiskerLeft
        (HomologicalComplex.homologyFunctorIso C (ComplexShape.up ℤ) a) ≪≫
      ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).associator
            (HomologicalComplex.shortComplexFunctor C (ComplexShape.up ℤ) a)
            (CategoryTheory.ShortComplex.homologyFunctor C)).symm ≪≫
        CategoryTheory.Functor.isoWhiskerRight (CochainComplex.shiftShortComplexFunctorIso C n a a' ha')
            (CategoryTheory.ShortComplex.homologyFunctor C) ≪≫
          (HomologicalComplex.homologyFunctorIso C (ComplexShape.up ℤ) a').symm
-- Lean.Meta.Tactic.Repeat
_private.Lean.Meta.Tactic.Repeat.0.Lean.Meta.repeat'Core.go.match_3.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive n
-- Init.Data.Array.Attach
/-- See also `pmap_eq_map_attach` for writing `pmap` in terms of `map` and `attach`.  -/
Array.map_attach_eq_pmap : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : { x // x ∈ xs } → β},
  Array.map f xs.attach = Array.pmap (fun a h => f ⟨a, h⟩) xs ⋯
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.id_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (U : CategoryTheory.Under X),
  CategoryTheory.Under.Hom.right (CategoryTheory.CategoryStruct.id U) = CategoryTheory.CategoryStruct.id U.right
-- Mathlib.Order.Max
/-- For each term `a`, there is some `b` which is either incomparable or strictly smaller.  -/
NoBotOrder.exists_not_ge : ∀ {α : Type u_3} {inst : LE α} [self : NoBotOrder α] (a : α), ∃ b, ¬a ≤ b
-- Lean.Data.Lsp.Basic
Lean.Lsp.LocationLink.mk.sizeOf_spec : ∀ (originSelectionRange? : Option Lean.Lsp.Range) (targetUri : Lean.Lsp.DocumentUri)
  (targetRange targetSelectionRange : Lean.Lsp.Range),
  sizeOf
      { originSelectionRange? := originSelectionRange?, targetUri := targetUri, targetRange := targetRange,
        targetSelectionRange := targetSelectionRange } =
    1 + sizeOf originSelectionRange? + sizeOf targetUri + sizeOf targetRange + sizeOf targetSelectionRange
-- Mathlib.Topology.UniformSpace.Ascoli
/-- Let `X` be a topological space, `𝔖` a covering of `X` by compact subsets, `α` a uniform space,
and `F : ι → (X → α)` a family which is equicontinuous on each `K ∈ 𝔖`. Then, the topologies
of uniform convergence on `𝔖` and pointwise convergence induce the same topology on `ι`.

This is a specialization of `EquicontinuousOn.inducing_uniformOnFun_iff_pi'` to
the case where `𝔖` covers `X`.  -/
EquicontinuousOn.isInducing_uniformOnFun_iff_pi : ∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  [inst_2 : TopologicalSpace ι] {𝔖 : Set (Set X)},
  ⋃₀ 𝔖 = Set.univ →
    (∀ K ∈ 𝔖, IsCompact K) →
      (∀ K ∈ 𝔖, EquicontinuousOn F K) → (Topology.IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ Topology.IsInducing F)
-- Mathlib.Algebra.Lie.SkewAdjoint
mem_skewAdjointMatricesLieSubalgebra_unit_smul : ∀ {R : Type u} {n : Type w} [inst : CommRing R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (u : Rˣ)
  (J A : Matrix n n R), A ∈ skewAdjointMatricesLieSubalgebra (u • J) ↔ A ∈ skewAdjointMatricesLieSubalgebra J
-- Batteries.Linter.UnnecessarySeqFocus
/-- The monad for collecting used tactic syntaxes.  -/
Batteries.Linter.UnnecessarySeqFocus.M : Type → Type → Type
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Bundle.mdifferentiableAt_zeroSection : ∀ (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {x : B},
  MDiffAt (Bundle.zeroSection F E) x
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.Integrable.finsetSum : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.VectorMeasure X F} {ι : Type u_8} (s : Finset ι) {f : ι → X → E},
  (∀ i ∈ s, μ.Integrable (f i)) → μ.Integrable (∑ i ∈ s, f i)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.coe_toAddSubmonoid : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R), ↑s.toAddSubmonoid = ↑s
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `E / F` is an algebraic extension, `F` is separably closed,
then `E / F` is purely inseparable.  -/
Algebra.IsAlgebraic.isPurelyInseparable_of_isSepClosed : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Ring E] [IsDomain E] [inst_3 : Algebra F E]
  [Algebra.IsAlgebraic F E] [IsSepClosed F], IsPurelyInseparable F E
-- Mathlib.Data.Rat.Cast.Order
NNRat.preimage_cast_Ici : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p : ℚ≥0),
  NNRat.cast ⁻¹' Set.Ici ↑p = Set.Ici p
-- Mathlib.Analysis.Calculus.TangentCone.Real
uniqueDiffOn_Icc : ∀ {a b : ℝ}, a < b → UniqueDiffOn ℝ (Set.Icc a b)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoidClass.subtype.eq_1 : ∀ {M : Type u_1} {A : Type u_3} [inst : AddZeroClass M] [inst_1 : SetLike A M] [hA : AddSubmonoidClass A M] (S' : A),
  AddSubmonoidClass.subtype S' = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
WeakBilin.instIsScalarTower : ∀ {𝕜 : Type u_2} {𝕝 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : CommSemiring 𝕜] [inst_1 : CommSemiring 𝕝]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F] [inst_6 : SMul 𝕝 𝕜]
  [inst_7 : Module 𝕝 E] [IsScalarTower 𝕝 𝕜 E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜), IsScalarTower 𝕝 𝕜 (WeakBilin B)
-- Lean.Compiler.InlineAttrs
_private.Lean.Compiler.InlineAttrs.0.Lean.Compiler.InlineAttributeKind.toAttrString : Lean.Compiler.InlineAttributeKind → String
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.toArray_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w}
  {f : (a : α) → β a → Option (γ a)},
  (Std.DTreeMap.filterMap f t).toArray =
    Array.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toArray
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegular.instSum_1 : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {ι : Type u_3}
  {μ : ι → MeasureTheory.Measure α} [∀ (i : ι), (μ i).InnerRegular], (MeasureTheory.Measure.sum μ).InnerRegular
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.cases : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Cases pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Option.getD.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : α) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match some x with
    | some x => h_1 x
    | none => h_2 ()) =
    h_1 x
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Real.hasDerivAt_rpow_const : ∀ {x p : ℝ}, x ≠ 0 ∨ 1 ≤ p → HasDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.IsModuleConvexSpace.sConvexComb_eq_sum : ∀ {R : Type u_2} {M : Type u_3} {inst : Semiring R} {inst_1 : PartialOrder R} {inst_2 : IsStrictOrderedRing R}
  {inst_3 : AddCommMonoid M} {inst_4 : Module R M} {inst_5 : Convexity.ConvexSpace R M}
  [self : Convexity.IsModuleConvexSpace R M] (w : Convexity.StdSimplex R M),
  Convexity.sConvexComb w = w.weights.sum fun m r => r • m
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedAtom.default : Mathlib.Tactic.BicategoryLike.Atom
-- Mathlib.Topology.ContinuousOn
continuousOn_open_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  IsOpen s → (ContinuousOn f s ↔ ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t))
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- Shorthand for the 1st group cohomology of a `k`-linear `G`-representation `A`, `H¹(G, A)`,
defined as the 1st cohomology of the complex of inhomogeneous cochains of `A`.  -/
groupCohomology.H1 : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → Rep.{u, u, u} k G → ModuleCat k
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.minEntry : {α : Type u} → {β : Type v} → (t : Std.DTreeMap.Internal.Impl α fun x => β) → t.isEmpty = false → α × β
-- Batteries.Tactic.Lint.Basic
/-- If `isFast` is false, this test will be omitted from `#lint-`.  -/
Batteries.Tactic.Lint.Linter.isFast : Batteries.Tactic.Lint.Linter → Bool
-- Mathlib.Combinatorics.Quiver.Schreier
/-- The labelling prefunctor is a covering for Schreier graphs with group actions.  -/
Quiver.SchreierGraph.labelling_isCovering : ∀ {V : Type u_1} {M : Type u_2} [inst : Group M] [inst_1 : MulAction M V] {S : Type u_3} (ι : S → M),
  (Quiver.SchreierGraph.labelling V ι).IsCovering
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.inv (CategoryTheory.CategoryStruct.comp S.iCycles h) =
    CategoryTheory.CategoryStruct.comp S.moduleCatLeftHomologyData.i h
-- Mathlib.RingTheory.Congruence.Hom
RingCon.range_mk' : ∀ {M : Type u_1} [inst : Ring M] {c : RingCon M}, c.mk'.range = ⊤
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- Project an element of the standard simplex to a lower-dimensional standard simplex,
assuming at least one non-zero weight subsists.  -/
Convexity.StdSimplex.restrict : {X : Type u_2} →
  {K : Type u_8} →
    [inst : Semifield K] →
      [inst_1 : LinearOrder K] →
        [IsStrictOrderedRing K] →
          (w : Convexity.StdSimplex K X) → (s : Set X) → (∃ x ∈ s, w.weights x ≠ 0) → Convexity.StdSimplex K X
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.specializingMap_isZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget (AlgebraicGeometry.topologically @SpecializingMap)
-- Mathlib.Tactic.FunProp.Decl
/-- Extension storing function properties tracked and used by the `fun_prop` attribute and tactic,
including, for example, `Continuous`, `Measurable`, `Differentiable`, etc.  -/
Mathlib.Meta.FunProp.funPropDeclsExt : Mathlib.Meta.FunProp.FunPropDeclsExt
-- Mathlib.Topology.Connected.PathConnected
/-- The product of a family of path-connected sets is path-connected.  -/
IsPathConnected.pi : ∀ {ι : Type u_3} {Z : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (Z i)] {s : (i : ι) → Set (Z i)},
  (∀ (i : ι), IsPathConnected (s i)) → IsPathConnected (Set.univ.pi s)
-- Mathlib.GroupTheory.Transfer
IsCyclic.normalizer_le_centralizer : ∀ {G : Type u_3} [inst : Group G] [Finite G] {p : ℕ},
  (Nat.card G).minFac = p → ∀ {P : Sylow p G}, IsCyclic ↥↑P → Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P
-- Mathlib.GroupTheory.Congruence.Basic
/-- Given a congruence relation `c` on a monoid and a homomorphism `f` constant on `c`'s
equivalence classes, `f` has the same image as the homomorphism that `f` induces on the
quotient.  -/
Con.lift_range : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} {f : M →* P}
  (H : c ≤ Con.ker f), MonoidHom.mrange (c.lift f H) = MonoidHom.mrange f
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
CategoryTheory.FunctorToTypes.rightAdj_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type (max w v u))) (X : C),
  ((CategoryTheory.FunctorToTypes.rightAdj F).obj G).obj X = F.HomObj G (CategoryTheory.coyoneda.obj (Opposite.op X))
-- Mathlib.Data.Ordmap.Ordset
/-- O(log n). Retrieve an element in the set that is equivalent to `x` in the order,
if it exists.  -/
Ordset.find : {α : Type u_1} → [inst : Preorder α] → [DecidableLE α] → α → Ordset α → Option α
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- **Alias** of `IsEllipticDvdSequence.smul`. -/
IsEllDivSequence.smul : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R}, IsEllipticDvdSequence W → ∀ (x : R), IsEllipticDvdSequence (x • W)