mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.haarContent_outerMeasure_self_pos : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G), 0 < (MeasureTheory.Measure.haar.haarContent K₀).outerMeasure ↑K₀
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- If `f : Spec S → Spec R` is generalizing and surjective, the topology on `Spec R` is the
quotient topology induced by `f`.  -/
PrimeSpectrum.isQuotientMap_of_generalizingMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] {f : R →+* S},
  Function.Surjective (PrimeSpectrum.comap f) →
    GeneralizingMap (PrimeSpectrum.comap f) → Topology.IsQuotientMap (PrimeSpectrum.comap f)
-- Mathlib.Algebra.Group.Action.Defs
AddAction.ext_iff : ∀ {G : Type u_9} {P : Type u_10} {inst : AddMonoid G} {x y : AddAction G P}, x = y ↔ VAdd.vadd = VAdd.vadd
-- Lean.PrettyPrinter.Formatter
/-- If `pos?` has a position, run `x` and tag its results with that position,
if they are not already tagged. Otherwise just run `x`.  -/
Lean.PrettyPrinter.Formatter.withMaybeTag : Option String.Pos.Raw → Lean.PrettyPrinter.FormatterM Unit → Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_hom_rel : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {r : M → N → Prop}
  {f : ι → M} {g : ι → N} {s : Finset ι},
  r 0 0 → (∀ (a : ι) (b : M) (c : N), r b c → r (f a + b) (g a + c)) → r (∑ x ∈ s, f x) (∑ x ∈ s, g x)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.quot_lift_mk : ∀ {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool) → β)
  (H : ∀ (L₁ L₂ : List (α × Bool)), FreeAddGroup.Red.Step L₁ L₂ → f L₁ = f L₂), Quot.lift f H (FreeAddGroup.mk L) = f L
-- Mathlib.LinearAlgebra.QuadraticForm.Dual
LinearMap.separatingLeft_dualProd : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  LinearMap.SeparatingLeft (LinearMap.dualProd R M) ↔ Function.Injective ⇑(Module.Dual.eval R M)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.yonedaCollectionFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v))
  {X Y : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : X ⟶ Y),
  (CategoryTheory.OverPresheafAux.yonedaCollectionFunctor A).map η =
    CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁ η
-- Std.Internal.UV.Signal
/-- This function has different behavior depending on the state and configuration of the `Signal`:
- if `repeating` is `false` and:
  - it is initial, start listening and return a new `IO.Promise` that is set to resolve once
    the signal `signum` is received. After this `IO.Promise` is resolved the `Signal` is finished.
  - it is running or finished, return the same `IO.Promise` that the first call to `next` returned.
- if `repeating` is `true` and:
  - it is initial, start listening and return a new `IO.Promise` that resolves when the next
    signal `signum` is received.
  - it is running, check whether the last returned `IO.Promise` is already resolved:
     - If it is, return a new `IO.Promise` that resolves upon receiving the next signal
     - If it is not, return the last `IO.Promise`
     This ensures that the returned `IO.Promise` resolves at the next occurrence of the signal.
  - if it is finished, return the last `IO.Promise` created by `next`. Notably this could be one
    that never resolves if the signal handler was stopped before fulfilling the last one.

The resolved `IO.Promise` contains the signal number that was received.
 -/
Std.Internal.UV.Signal.next : Std.Internal.UV.Signal → IO (IO.Promise ℤ)
-- Mathlib.Data.List.Permutation
/-- The `ts` argument to `permutationsAux2` can be folded into the `f` argument.  -/
List.permutationsAux2_comp_append : ∀ {α : Type u_1} {β : Type u_2} {t : α} {ts ys : List α} {r : List β} (f : List α → β),
  (List.permutationsAux2 t [] r ys fun x => f (x ++ ts)).2 = (List.permutationsAux2 t ts r ys f).2
-- Mathlib.LinearAlgebra.Basis.Exact
_private.Mathlib.LinearAlgebra.Basis.Exact.0.top_le_span_of_aux : ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K] [inst_6 : Module R P]
  {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K},
  s ∘ₗ f = LinearMap.id →
    Function.Exact ⇑f ⇑g →
      ∀ {κ : Type u_6} {σ : Type u_7} (v : κ ⊕ σ → M),
        Function.Surjective ⇑g →
          (∀ (i : κ), s (v (Sum.inl i)) = 0) →
            LinearIndependent R (⇑s ∘ v ∘ Sum.inr) →
              ⊤ ≤ Submodule.span R (Set.range v) → ⊤ ≤ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))
-- Mathlib.Order.Filter.Extr
IsMaxFilter.isExtr : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMaxFilter f l a → IsExtrFilter f l a
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.mkConsts : List (Lean.Name × List String) →
  List Lean.Level → Lean.Elab.TermElabM (List (Lean.Expr × List String × List Lean.Level))
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.apply_eq_iff_eq : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) {x y : M}, e x = e y ↔ x = y
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.trace.sizeOf_spec : ∀ (cls : Lean.Name) (msg : Std.Format) (collapsed : Bool)
  (children : Lean.Widget.StrictOrLazy (Array Std.Format) (Array Lean.MessageData)),
  sizeOf (Lean.Widget.EmbedFmt.trace✝ cls msg collapsed children) =
    1 + sizeOf cls + sizeOf msg + sizeOf collapsed + sizeOf children
-- Mathlib.Analysis.Convex.Side
/-- If `x` and `y` lie off `s` and are displaced from points of `s` by multiples of a common
vector whose coefficients have nonpositive product, they are strictly on opposite sides of `s`.  -/
AffineSubspace.sOppSide_of_vsub_eq_smul : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y p₁ p₂ : P} {m : V} {c₁ c₂ : R},
  p₁ ∈ s → p₂ ∈ s → x -ᵥ p₁ = c₁ • m → y -ᵥ p₂ = c₂ • m → c₁ * c₂ ≤ 0 → x ∉ s → y ∉ s → s.SOppSide x y
-- Init.Data.List.Sublist
List.IsPrefix.filter : ∀ {α : Type u_1} (p : α → Bool) ⦃l₁ l₂ : List α⦄, l₁ <+: l₂ → List.filter p l₁ <+: List.filter p l₂
-- Mathlib.Algebra.Ring.Basic
/-- An `AddMonoidHom` preserves multiplication if pre- and post- composition with
`mul` are equivalent. By converting the statement into an equality of
`AddMonoidHom`s, this lemma allows various specialized `ext` lemmas about `→+` to then be applied.
 -/
AddMonoidHom.map_mul_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : R →+ S), (∀ (x y : R), f (x * y) = f x * f y) ↔ AddMonoidHom.mul.compr₂ f = (AddMonoidHom.mul.comp f).compl₂ f
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.eq_of_spanning_subset : ∀ {α : Type u_2} {M : Matroid α} {S I : Set α}, M.Indep I → M.Spanning S → S ⊆ I → S = I
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBit.mk.injEq : ∀ (var : ℕ) {w : ℕ} (idx : Fin w) (var_1 w_1 : ℕ) (idx_1 : Fin w_1),
  ({ var := var, w := w, idx := idx } = { var := var_1, w := w_1, idx := idx_1 }) =
    (var = var_1 ∧ w = w_1 ∧ idx ≍ idx_1)
-- Init.Data.List.Lemmas
List.length_dropLast : ∀ {α : Type u_1} {xs : List α}, xs.dropLast.length = xs.length - 1
-- Mathlib.Algebra.Order.Floor.Defs
Int.fract_int : Int.fract = 0
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.instHasZeroMorphisms : {R : Type u} → [inst : Semiring R] → CategoryTheory.Limits.HasZeroMorphisms (SemimoduleCat R)
-- Init.Data.Nat.Div.Basic
Nat.div_lt_iff_lt_mul : ∀ {k x y : ℕ}, 0 < k → (x / k < y ↔ x < y * k)
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.coe_span_apply : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : ι → M} (hli : LinearIndependent R v) (i : ι), ↑((Module.Basis.span hli) i) = v i
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.cancel_right : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] {g₁ g₂ : N →ₙ+ P}
  {f : M →ₙ+ N}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Lean.Expr
/-- Returns `true` if `e` is an application of one of the type annotation gadgets. This does not check that the application has the correct arity.  -/
Lean.Expr.isTypeAnnotation : Lean.Expr → Bool
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instSMulCommClass : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : SMul R A] [inst_1 : SMul S A]
  [SMulCommClass R S A], SMulCommClass R S (CStarMatrix m n A)
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_pos : ∀ {a : Ordinal.{u_1}} (b : Ordinal.{u_1}), 0 < a → 0 < a ^ b
-- Mathlib.ModelTheory.Definability
Set.Definable.preimage_comp : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {β : Type u_1} (f : α → β)
  {s : Set (α → M)}, A.Definable L s → A.Definable L ((fun g => g ∘ f) ⁻¹' s)
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.coe_comap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (K : Subgroup N) (f : G →* N),
  ↑(Subgroup.comap f K) = ⇑f ⁻¹' ↑K
-- Mathlib.Algebra.Homology.BifunctorShift
/-- The canonical isomorphism `mapBifunctor K₁ (K₂⟦y⟧) F ≅ (mapBifunctor K₁ K₂ F)⟦y⟧`.
This isomorphism involves signs: on the summand `(F.obj (K₁.X p)).obj (K₂.X q)`, it is given
by the multiplication by `(p * y).negOnePow`.  -/
CochainComplex.mapBifunctorShift₂Iso : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
              [inst_4 : CategoryTheory.Preadditive C₂] →
                [inst_5 : CategoryTheory.Preadditive D] →
                  (K₁ : CochainComplex C₁ ℤ) →
                    (K₂ : CochainComplex C₂ ℤ) →
                      (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                        [inst_6 : F.PreservesZeroMorphisms] →
                          [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] →
                            (y : ℤ) →
                              [inst_8 : K₁.HasMapBifunctor K₂ F] →
                                K₁.mapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F ≅
                                  (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).obj (K₁.mapBifunctor K₂ F)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels
/-- A limit kernel fork gives a colimit cokernel cofork in the opposite category  -/
CategoryTheory.Limits.KernelFork.IsLimit.ofιOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K X Y : C} →
        (i : K ⟶ X) →
          {f : X ⟶ Y} →
            (w : CategoryTheory.CategoryStruct.comp i f = 0) →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i w) →
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ i.op ⋯)
-- Lean.Linter.Init
Lean.Linter.getLinterAll : Lean.Linter.LinterOptions → optParam Bool Lean.Linter.linter.all.defValue → Bool
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousWithinAt_iff_le_liminf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_4} [inst_1 : CompleteLinearOrder γ]
  {f : α → γ}, LowerSemicontinuousWithinAt f s x ↔ f x ≤ Filter.liminf f (nhdsWithin x s)
-- Mathlib.Algebra.Category.AlgCat.TensorAlgebra
AlgCat.tensorAlgebra_obj_carrier : ∀ (R : Type u) [inst : CommRing R] (M : ModuleCat R), ↑((AlgCat.tensorAlgebra R).obj M) = TensorAlgebra R ↑M
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- See Note [custom simps projection]  -/
MeasurableEquiv.Simps.symm_apply : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [inst_1 : MeasurableSpace β] → α ≃ᵐ β → β → α
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.algEquivOfIso_symm_apply : ∀ {R : Type u} [inst : CommRing R] {A B : CommAlgCat R} (i : A ≅ B) (a : ↑B),
  (CommAlgCat.algEquivOfIso i).symm a = (CategoryTheory.ConcreteCategory.hom i.inv) a
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_iUnion_apply : ∀ {ι : Sort u_1} {α : Type u_2} {M : Type u_3} [inst : CompleteLattice M] [inst_1 : Zero M],
  ⊥ = 0 → ∀ (s : ι → Set α) (f : α → M) (x : α), (⋃ i, s i).indicator f x = ⨆ i, (s i).indicator f x
-- Mathlib.Data.FinEnum
FinEnum.card_UInt64 : FinEnum.card UInt64 = 2 ^ 64
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.exists_notMem : ∀ {α : Type u} {s : Set α} [Infinite α], s.Finite → ∃ a, a ∉ s
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β}, a ∈ t.insertIfNew k v ↔ cmp k a = Ordering.eq ∨ a ∈ t
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverEntropy_union : ∀ {X : Type u_1} {T : X → X} {F G : Set X} [inst : UniformSpace X],
  Dynamics.coverEntropy T (F ∪ G) = max (Dynamics.coverEntropy T F) (Dynamics.coverEntropy T G)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentContentChangeEvent.rangeChange.inj : ∀ {range : Lean.Lsp.Range} {text : String} {range_1 : Lean.Lsp.Range} {text_1 : String},
  Lean.Lsp.TextDocumentContentChangeEvent.rangeChange range text =
      Lean.Lsp.TextDocumentContentChangeEvent.rangeChange range_1 text_1 →
    range = range_1 ∧ text = text_1
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckAddGroup.instNeg.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M],
  Algebra.GrothendieckAddGroup.instNeg =
    { neg := fun x => AddLocalization.rec (fun m s => AddLocalization.mk ↑s ⟨m, ⋯⟩) ⋯ x }
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.castLE_comp_castLE : ∀ {L : FirstOrder.Language} {α : Type u'} {k m n : ℕ} (km : k ≤ m) (mn : m ≤ n),
  FirstOrder.Language.BoundedFormula.castLE mn ∘ FirstOrder.Language.BoundedFormula.castLE km =
    FirstOrder.Language.BoundedFormula.castLE ⋯
-- Init.Data.Hashable
instHashableOption : {α : Type u_1} → [Hashable α] → Hashable (Option α)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadHom.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C}
  (toNatTrans toNatTrans_1 : CategoryTheory.NatTrans T₁.toFunctor T₂.toFunctor)
  (e_toNatTrans : toNatTrans = toNatTrans_1)
  (app_η : ∀ (X : C), CategoryTheory.CategoryStruct.comp (T₁.η.app X) (toNatTrans.app X) = T₂.η.app X)
  (app_μ :
    ∀ (X : C),
      CategoryTheory.CategoryStruct.comp (T₁.μ.app X) (toNatTrans.app X) =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.CategoryStruct.comp (T₁.map (toNatTrans.app X)) (toNatTrans.app (T₂.obj X))) (T₂.μ.app X)),
  { toNatTrans := toNatTrans, app_η := app_η, app_μ := app_μ } = { toNatTrans := toNatTrans_1, app_η := ⋯, app_μ := ⋯ }
-- Init.Data.String.Lemmas.Slice
String.Slice.back.eq_1 : ∀ (s : String.Slice), s.back = s.back?.getD default
-- Mathlib.Topology.Order.WithTop
WithTop.untopA.congr_simp : ∀ {α : Type u_1} [inst : Nonempty α] (a a_1 : WithTop α), a = a_1 → a.untopA = a_1.untopA
-- Mathlib.Algebra.Category.Grp.FiniteGrp
/-- An additive group that is finite  -/
FiniteAddGrp.toAddGrp : FiniteAddGrp.{u} → AddGrpCat
-- Mathlib.Algebra.Order.Monoid.Basic
OrderEmbedding.mulRight_apply : ∀ {α : Type u_2} [inst : Mul α] [inst_1 : LinearOrder α] [inst_2 : MulRightStrictMono α] (m n : α),
  (OrderEmbedding.mulRight m) n = n * m
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- Helper function for constructing morphisms between wide equalizer tridents.
 -/
CategoryTheory.Limits.Trident.mkHom : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [Nonempty J] →
            {s t : CategoryTheory.Limits.Trident f} →
              (k : s.pt ⟶ t.pt) →
                autoParam (CategoryTheory.CategoryStruct.comp k t.ι = s.ι) CategoryTheory.Limits.Trident.mkHom._auto_1 →
                  (s ⟶ t)
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.SmallHom.mk_comp_mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {X Y Z : C}
  [inst_1 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y]
  [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W Y Z]
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W X Z] (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.Localization.SmallHom.mk W f).comp (CategoryTheory.Localization.SmallHom.mk W g) =
    CategoryTheory.Localization.SmallHom.mk W (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.RingTheory.Support
Module.mem_support_iff' : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {p : PrimeSpectrum R}, p ∈ Module.support R M ↔ ∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0
-- Lean.Meta.ReduceEval
Lean.Meta.reduceEval : {α : Type} → [Lean.Meta.ReduceEval α] → Lean.Expr → Lean.MetaM α
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
CategoryTheory.Limits.preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type w} [inst_2 : LinearOrder J] (G : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J G] (j : J),
  Order.IsSuccLimit j → CategoryTheory.Limits.PreservesColimitsOfShape (↑(Set.Iio j)) G
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRank_restrict : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), (M.restrict X).eRank = M.eRk X
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        CategoryTheory.Category.{max u₁ v, max (max (max (v + 1) u) u₁) v₁} (SheafOfModules R)
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.endofunctorMonoidalCategory_rightUnitor_inv_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C C) (X : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor F).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.RepresentationTheory.Equiv
Representation.leftRegularMapEquiv_symm_apply_toFun : ∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {k : Type u} [inst_2 : CommSemiring k]
  [inst_3 : Module k V] (σ : Representation k G V) (v : V) (x : MonoidAlgebra k G),
  (σ.leftRegularMapEquiv.symm v) x = x.coeff.sum fun x r => r • (σ x) v
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.isEmpty_diff_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.isEmpty = true → (m₁ \ m₂).isEmpty = true
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y Z : CategoryTheory.RingObjCat C} (f : X.Hom Y) (g : Y.Hom Z),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.Data.Set.Functor
instAlternativeMonadSetM : AlternativeMonad SetM
-- Mathlib.Analysis.Convex.Slope
/-- If `f : 𝕜 → 𝕜` is strictly concave, then for any three points `x < y < z` the slope of the
secant line of `f` on `[x, y]` is strictly greater than the slope of the secant line of `f` on
`[y, z]`.  -/
StrictConcaveOn.slope_anti_adjacent : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  StrictConcaveOn 𝕜 s f → ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.natTransPInfty_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (x : CategoryTheory.SimplicialObject C),
  (AlgebraicTopology.DoldKan.natTransPInfty C).app x = AlgebraicTopology.DoldKan.PInfty
-- Lean.Parser.Do
Lean.Parser.Term.do : Lean.Parser.Parser
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.Step.to_red : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.Red.Step L₁ L₂ → FreeGroup.Red L₁ L₂
-- Mathlib.Data.Matrix.Mul
Matrix.vecMulVec_sub : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocRing α] (w : m → α) (v₁ v₂ : n → α),
  Matrix.vecMulVec w (v₁ - v₂) = Matrix.vecMulVec w v₁ - Matrix.vecMulVec w v₂
-- Mathlib.Topology.Order
continuous_iInf_rng : ∀ {α : Type u} {β : Type v} {f : α → β} {ι : Sort u_2} {t₁ : TopologicalSpace α} {t₂ : ι → TopologicalSpace β},
  Continuous f ↔ ∀ (i : ι), Continuous f
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_restrict₀' : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet t μ → (μ.restrict t).restrict s = μ.restrict (s ∩ t)
-- Mathlib.Topology.Algebra.AsymptoticCone
AffineSpace.nhds_bind_asymptoticNhds : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [inst_6 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] (v : V),
  (nhds v).bind (AffineSpace.asymptoticNhds k P) = AffineSpace.asymptoticNhds k P v
-- Mathlib.Data.PFun
/-- First return map. Transforms a partial function `f : α →. β ⊕ α` into the partial function
`α →. β` which sends `a : α` to the first value in `β` it hits by iterating `f`, if such a value
exists. By abusing notation to illustrate, either `f a` is in the `β` part of `β ⊕ α` (in which
case `f.fix a` returns `f a`), or it is undefined (in which case `f.fix a` is undefined as well), or
it is in the `α` part of `β ⊕ α` (in which case we repeat the procedure, so `f.fix a` will return
`f.fix (f a)`).  -/
PFun.fix : {α : Type u_1} → {β : Type u_2} → (α →. β ⊕ α) → α →. β
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : CategoryTheory.PreZeroHypercover S} [self : AlgebraicGeometry.QuasiCompactCover 𝒰]
  {U : S.Opens}, AlgebraicGeometry.IsAffineOpen U → IsCompactOpenCovered (fun x => ⇑(𝒰.f x)) ↑U
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β},
  m₁.WF → m₂.WF → ∀ (f : α → β → Bool), m₁.Equiv m₂ → (Std.HashMap.Raw.filter f m₁).Equiv (Std.HashMap.Raw.filter f m₂)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_le_one : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] {a : α} [MulRightMono α], |a|ₘ ≤ 1 ↔ a = 1
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.id_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) (x : M),
  (QuadraticMap.Isometry.id Q) x = x