mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.EMetricSpace.BoundedVariation
LipschitzWith.comp_locallyBoundedVariationOn : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {F : Type u_3}
  [inst_2 : PseudoEMetricSpace F] {f : E → F} {C : NNReal},
  LipschitzWith C f → ∀ {g : α → E} {s : Set α}, LocallyBoundedVariationOn g s → LocallyBoundedVariationOn (f ∘ g) s
-- Init.Data.Nat.Sqrt.Lemmas
_private.Init.Data.Nat.Sqrt.Lemmas.0.Nat.IsSqrt.eq_1 : ∀ (n q : ℕ), Nat.IsSqrt✝ n q = (q * q ≤ n ∧ n < (q + 1) * (q + 1))
-- Mathlib.Data.Prod.TProd
List.TProd.mk_elim : ∀ {ι : Type u} {α : ι → Type v} {l : List ι} [inst : DecidableEq ι],
  l.Nodup → ∀ (h : ∀ (i : ι), i ∈ l) (v : List.TProd α l), List.TProd.mk l (List.TProd.elim' h v) = v
-- Mathlib.Geometry.Euclidean.Projection
/-- Subtracting the `orthogonalProjection` from a point in the given
subspace produces a result in the direction of the given subspace.  -/
EuclideanGeometry.vsub_orthogonalProjection_mem_direction : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {p₁ : P} (p₂ : P) (hp₁ : p₁ ∈ s),
  ↑(⟨p₁, hp₁⟩ -ᵥ (EuclideanGeometry.orthogonalProjection s) p₂) ∈ s.direction
-- Lean.Meta.Match.Basic
/-- Returns `true` if `s` is of the form `congr_eq_<idx>`  -/
Lean.Meta.Match.isCongrEqnReservedNameSuffix : String → Bool
-- Mathlib.Topology.Algebra.Order.LiminfLimsup
limsup_mul_le : ∀ {ι : Type u_1} {f : Filter ι} {u v : ι → ℝ},
  (∃ᶠ (x : ι) in f, 0 ≤ u x) →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u →
      0 ≤ᶠ[f] v →
        Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v →
          Filter.limsup (u * v) f ≤ Filter.limsup u f * Filter.limsup v f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_filter_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k k' : α},
  (↑m).WF →
    m.getKey? k = some k' →
      Std.DHashMap.Internal.Raw₀.Const.get? (Std.DHashMap.Internal.Raw₀.filter f m) k =
        Option.filter (fun x => f k' x) (Std.DHashMap.Internal.Raw₀.Const.get? m k)
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_neg_left : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.covariance (-X) Y μ = -ProbabilityTheory.covariance X Y μ
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
/-- By construction, the section `cotangentCompAwaySec` sends `g * X - 1` to `x`.  -/
Algebra.Generators.cotangentCompAwaySec_apply : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι)
  (x : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent),
  (Algebra.Generators.cotangentCompAwaySec g P x) (Algebra.Generators.cMulXSubOneCotangent T g) = x
-- Mathlib.Algebra.Group.Action.Prod
/-- A `MulAction` by a product monoid is equivalent to commuting `MulAction`s by the factors.  -/
MulAction.prodEquiv : (M : Type u_1) →
  (N : Type u_2) →
    (α : Type u_5) →
      [inst : Monoid M] →
        [inst_1 : Monoid N] → MulAction (M × N) α ≃ (x : MulAction M α) ×' (x_1 : MulAction N α) ×' SMulCommClass M N α
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instWeakEquivalenceCompOfIsStableUnderCompositionWeakEquivalences : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [(HomotopicalAlgebra.weakEquivalences C).IsStableUnderComposition] [hf : HomotopicalAlgebra.WeakEquivalence f]
  [hg : HomotopicalAlgebra.WeakEquivalence g],
  HomotopicalAlgebra.WeakEquivalence (CategoryTheory.CategoryStruct.comp f g)
-- Init.Data.List.Impl
List.modify_eq_modifyTR : @List.modify = @List.modifyTR
-- Mathlib.Topology.Category.TopCat.Opens
/-- The natural isomorphism between taking preimages under `f ≫ g`, and the composite
of taking preimages under `g`, then preimages under `f`.
 -/
TopologicalSpace.Opens.mapComp : {X Y Z : TopCat} →
  (f : X ⟶ Y) →
    (g : Y ⟶ Z) →
      TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g) ≅
        (TopologicalSpace.Opens.map g).comp (TopologicalSpace.Opens.map f)
-- Init.Data.Float.Model.Unpacked.Basic
Float.Model.UnpackedFloat.infinity.sizeOf_spec : ∀ (sign : Float.Model.UnpackedFloat.Sign), sizeOf (Float.Model.UnpackedFloat.infinity sign) = 1 + sizeOf sign
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
MvPowerSeries.WithPiTopology.continuous_C : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Semiring R], Continuous ⇑MvPowerSeries.C
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.normalClosure_def'' : ∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] (K : IntermediateField F L)
  [Normal F L], IntermediateField.normalClosure F (↥K) L = ⨆ f, IntermediateField.map (↑f) K
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
/-- If `X` is geometrically connected over a point, then it is connected.  -/
AlgebraicGeometry.GeometricallyConnected.connectedSpace_of_subsingleton : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.GeometricallyConnected f] [Subsingleton ↥S]
  [Nonempty ↥S], ConnectedSpace ↥X
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.domain_mono : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F], StrictMono LinearPMap.domain
-- Mathlib.Algebra.CharP.LinearMaps
instExpCharLinearMapSubtypeMemSubringCenterId : ∀ {D : Type u_1} [inst : DivisionRing D] {p : ℕ} [ExpChar D p], ExpChar (D →ₗ[↥(Subring.center D)] D) p
-- Mathlib.Topology.Instances.Irrational
Irrational.instOrderTopologySubtypeReal : OrderTopology { x // Irrational x }
-- Mathlib.Algebra.Polynomial.Basic
/-- `X` commutes with everything, even when the coefficients are noncommutative.  -/
Polynomial.X_mul : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, Polynomial.X * p = p * Polynomial.X
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.mk_mem_cotangentIdeal : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} {x : R}, (Ideal.Quotient.mk (I ^ 2)) x ∈ I.cotangentIdeal ↔ x ∈ I
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.pow_toProd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (n : ℕ)
  (a : DoubleCentralizer 𝕜 A), (a ^ n).toProd = a.toProd ^ n
-- Mathlib.Topology.Covering.Quotient
IsAddQuotientCoveringMap.homeomorph_comp : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E],
  IsAddQuotientCoveringMap f G →
    ∀ {Y : Type u_4} [inst_4 : TopologicalSpace Y] (φ : X ≃ₜ Y), IsAddQuotientCoveringMap (⇑φ ∘ f) G
-- Mathlib.Computability.Reduce
ManyOneDegree.add_le : ∀ {d₁ d₂ d₃ : ManyOneDegree}, d₁ + d₂ ≤ d₃ ↔ d₁ ≤ d₃ ∧ d₂ ≤ d₃
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A functor between preadditive categories that preserves (zero morphisms and) binary coproducts
preserves binary biproducts.  -/
CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBinaryCoproduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {X Y : C}
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) F],
  CategoryTheory.Limits.PreservesBinaryBiproduct X Y F
-- Mathlib.CategoryTheory.Localization.Opposite
CategoryTheory.Functor.IsLocalization.op_iff : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C), L.op.IsLocalization W.op ↔ L.IsLocalization W
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_zero : ∀ {w i : ℕ}, (0#w).getMsbD i = false
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso'_inv_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  [inst_4 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C}
  (i : CategoryTheory.Limits.IsInitial I) {W : C},
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso' X i).inv.right =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj W X.right)
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.rightToLeft_app_adj₂_unit_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : G.Full] [inst_3 : G.Faithful]
  (X : C) {Z : D} (h : H.obj (G.obj (F.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.rightToLeft.app X)
      (CategoryTheory.CategoryStruct.comp (t.adj₂.unit.app (F.obj X)) h) =
    CategoryTheory.CategoryStruct.comp (H.map (t.adj₁.unit.app X)) h
-- Mathlib.Order.Filter.Pointwise
Filter.not_one_le_div_iff : ∀ {α : Type u_2} [inst : Group α] {f g : Filter α}, ¬1 ≤ f / g ↔ Disjoint f g
-- Mathlib.GroupTheory.EckmannHilton
EckmannHilton.commMonoid.eq_1 : ∀ {X : Type u} {m₁ : X → X → X} {e₁ : X} (h₁ : EckmannHilton.IsUnital m₁ e₁) [h : MulOneClass X]
  (distrib : ∀ (a b c d : X), m₁ (a * b) (c * d) = m₁ a c * m₁ b d),
  EckmannHilton.commMonoid h₁ distrib =
    { toMul := h.toMul, mul_assoc := ⋯, toOne := h.toOne, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto,
      npow_zero := ⋯, npow_succ := ⋯, mul_comm := ⋯ }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.length_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α], (Std.DHashMap.Const.toList m).length = m.size
-- Lean.Meta.Match.MatcherApp.Transform
/-- Given
- matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and
- a expression `B[discrs]` (which may not be a type, e.g. `n : Nat`),
returns the expressions `fun ys_1 ... ys_i => B[C_1[ys_1]] ... B[C_n[ys_n]]`,

This method assumes
- the `matcherApp.motive` is a lambda abstraction where `xs.size == discrs.size`
- each alternative is a lambda abstraction where `ys_i.size == matcherApp.altNumParams[i]`

This is similar to `MatcherApp.addArg` when you only have an expression to
refined, and not a type with a value.

This is used in `Lean.Elab.PreDefinition.WF.GuessFix` when constructing the context of recursive
calls to refine the functions' parameter, which may mention `major`.
See there for how to use this function.
 -/
Lean.Meta.MatcherApp.refineThrough : Lean.Meta.MatcherApp → Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelp.mk : Array Lean.Lsp.SignatureInformation → Option ℕ → Option ℕ → Lean.Lsp.SignatureHelp
-- Mathlib.Algebra.Homology.HomotopyCategory.KInjective
CochainComplex.isKInjective_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {L₁ L₂ : CochainComplex C ℤ} (e : L₁ ≅ L₂) [L₁.IsKInjective], L₂.IsKInjective
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- The forgetful functor from `LocallyRingedSpace` to `Top`.  -/
AlgebraicGeometry.LocallyRingedSpace.forgetToTop : CategoryTheory.Functor AlgebraicGeometry.LocallyRingedSpace TopCat
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- Structure which allows to construct a category whose types
of objects and morphisms are subtypes of a fixed type `Ω`.  -/
CategoryTheory.SmallCategoryOfSet : Type w → Type w
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage_add_measure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f : α → ENNReal},
  ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ Set.univ / (μ Set.univ + ν Set.univ) * ⨍⁻ (x : α), f x ∂μ +
      ν Set.univ / (μ Set.univ + ν Set.univ) * ⨍⁻ (x : α), f x ∂ν
-- Mathlib.Topology.Homotopy.Lifting
IsAddQuotientCoveringMap.monodromy_eq_id_iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hp : IsAddQuotientCoveringMap p G) {x : X} (e : ↑(p ⁻¹' {x}))
  {γ : FundamentalGroup X x}, ⋯.monodromy γ = id ↔ ⋯.monodromy γ e = e
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.algEquiv_map : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : Ring T] [inst_4 : Algebra R T] (h' : IsAdjoinRoot T f),
  (↑(h.algEquiv h')).comp h.map = h'.map
-- Mathlib.Topology.LocalAtTarget
TopologicalSpace.IsOpenCover.isInducing_iff_restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {ι : Type u_3}
  {U : ι → TopologicalSpace.Opens β},
  TopologicalSpace.IsOpenCover U →
    Continuous f → (Topology.IsInducing f ↔ ∀ (i : ι), Topology.IsInducing ((U i).carrier.restrictPreimage f))
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.continuous_setIntegral : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure X}
  [inst_1 : NormedSpace ℝ E] (s : Set X), Continuous fun f => ∫ (x : X) in s, ↑↑f x ∂μ
-- Mathlib.Algebra.Colimit.Ring
/-- Consider direct limits `lim G` and `lim G'` with direct system `f` and `f'` respectively, any
family of ring homomorphisms `gᵢ : Gᵢ ⟶ G'ᵢ` such that `g ∘ f = f' ∘ g` induces a ring
homomorphism `lim G ⟶ lim G'`.
 -/
Ring.DirectLimit.map : {ι : Type u_1} →
  [inst : Preorder ι] →
    {G : ι → Type u_2} →
      [inst_1 : (i : ι) → CommRing (G i)] →
        {f : (i j : ι) → i ≤ j → G i →+* G j} →
          {G' : ι → Type u_4} →
            [inst_2 : (i : ι) → CommRing (G' i)] →
              {f' : (i j : ι) → i ≤ j → G' i →+* G' j} →
                (g : (i : ι) → G i →+* G' i) →
                  (∀ (i j : ι) (h : i ≤ j), (g j).comp (f i j h) = (f' i j h).comp (g i)) →
                    (Ring.DirectLimit G fun x x_1 h => ⇑(f x x_1 h)) →+*
                      Ring.DirectLimit G' fun x x_1 h => ⇑(f' x x_1 h)
-- Mathlib.Data.Rat.Defs
Rat.divInt_neg : ∀ (n d : ℤ), Rat.divInt n (-d) = Rat.divInt (-n) d
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_zero_right_iff : ∀ {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [inst : SeminormedAddCommGroup F'] [inst_1 : NormedAddCommGroup E'']
  {f'' : α → E''} {l : Filter α}, (f'' =O[l] fun _x => 0) ↔ f'' =ᶠ[l] 0
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.resetSymbolPrioExt : Lean.CoreM Unit
-- Init.Data.Array.Lemmas
Array.sum_reverse : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Add α] [Std.Associative fun x1 x2 => x1 + x2]
  [Std.Commutative fun x1 x2 => x1 + x2] [Std.LawfulLeftIdentity (fun x1 x2 => x1 + x2) 0] (xs : Array α),
  xs.reverse.sum = xs.sum
-- Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
isLittleO_exp_neg_mul_sq_cocompact : ∀ {a : ℂ}, 0 < a.re → ∀ (s : ℝ), (fun x => Complex.exp (-a * ↑x ^ 2)) =o[Filter.cocompact ℝ] fun x => |x| ^ s
-- Mathlib.Order.SuccPred.Limit
IsMax.not_isPredLimit : ∀ {α : Type u_1} {a : α} [inst : Preorder α], IsMax a → ¬Order.IsPredLimit a
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.isFiniteMeasure_of_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure μ], ν ≤ μ → MeasureTheory.IsFiniteMeasure ν
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPolynomial.toMvPowerSeries_isUniformInducing : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R],
  IsUniformInducing MvPolynomial.toMvPowerSeries
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
BddAbove.range_add : ∀ {ι : Type u_1} {M : Type u_3} [inst : Add M] [inst_1 : Preorder M] [AddLeftMono M] [AddRightMono M] {f g : ι → M},
  BddAbove (Set.range f) → BddAbove (Set.range g) → BddAbove (Set.range fun i => f i + g i)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.isBasis_iff : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  autoParam (X ⊆ M.E) Matroid.isBasis_iff._auto_1 →
    (M.IsBasis I X ↔ M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J)
-- Mathlib.Control.Basic
/-- Takes a value `β` and `List α` and accumulates pairs according to a monadic function `f`.
Accumulation occurs from the right (i.e., starting from the tail of the list).  -/
List.mapAccumRM : {α : Type u} →
  {β' γ' : Type v} → {m' : Type v → Type w} → [Monad m'] → (α → β' → m' (β' × γ')) → β' → List α → m' (β' × List γ')
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_neg_coe_angle : ∀ {x : ℂ}, x ≠ 0 → ↑(-x).arg = ↑x.arg + ↑Real.pi
-- Mathlib.Algebra.Polynomial.HasseDeriv
Polynomial.hasseDeriv_zero : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.hasseDeriv 0 = LinearMap.id
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.inr_comp_pushoutComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] [inst_3 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (G.map f) (G.map g))
      (CategoryTheory.Limits.pushoutComparison G f g) =
    G.map (CategoryTheory.Limits.pushout.inr f g)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseWeekdayNarrow : Std.Time.DateFormatSymbols → Std.Internal.Parsec.String.Parser Std.Time.Weekday
-- Lean.Elab.Binders
Lean.Elab.Term.addLocalVarInfo : Lean.Syntax → Lean.Expr → Lean.Elab.TermElabM Unit
-- Batteries.Data.Fin.Fold
Fin.dfoldl_eq_foldl : ∀ {n : ℕ} {α : Type u_1} (f : Fin n → α → α) (x : α), Fin.dfoldl n (fun x => α) f x = Fin.foldl n (fun x i => f i x) x
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Metric.frontier_ball_subset_sphere : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, frontier (Metric.ball x ε) ⊆ Metric.sphere x ε
-- Mathlib.Algebra.CubicDiscriminant
Cubic.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : SizeOf R] (a b c d : R),
  sizeOf { a := a, b := b, c := c, d := d } = 1 + sizeOf a + sizeOf b + sizeOf c + sizeOf d
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.mk.sizeOf_spec : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [inst_2 : SizeOf C₁]
  [inst_3 : SizeOf C₂] [inst_4 : ⦃X Y : C₁⦄ → (x : X ⟶ Y) → SizeOf (W₁ x)]
  [inst_5 : ⦃X Y : C₂⦄ → (x : X ⟶ Y) → SizeOf (W₂ x)] {X₁ : C₁} (w : Φ.functor.obj X₁ ⟶ X₂) (hw : W₂ w),
  sizeOf { X₁ := X₁, w := w, hw := hw } = 1 + sizeOf X₁ + sizeOf w + sizeOf hw
-- Mathlib.CategoryTheory.Subobject.NoetherianObject
CategoryTheory.isNoetherianObject_iff_monotone_chain_condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.IsNoetherianObject X ↔ ∀ (f : ℕ →o CategoryTheory.Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
-- Batteries.Data.UInt
UInt64.toUInt8_toNat : ∀ (x : UInt64), x.toUInt8.toNat = x.toNat % 2 ^ 8
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.mul_const : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_7} [inst : NormedRing 𝕜] {f : α → 𝕜},
  MeasureTheory.HasFiniteIntegral f μ → ∀ (c : 𝕜), MeasureTheory.HasFiniteIntegral (fun x => f x * c) μ
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
FractionalIdeal.instMulPosReflectLENonZeroDivisors : ∀ {A : Type u_2} (K : Type u_3) [inst : CommRing A] [inst_1 : Field K] [IsDedekindDomain A] [inst_3 : Algebra A K]
  [IsFractionRing A K], MulPosReflectLE (FractionalIdeal (nonZeroDivisors A) K)
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.mk_coe : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) (h₁ : f 1 = 1)
  (h₂ :
    ∀ (x y : A),
      { toFun := ⇑f, map_one' := h₁ }.toFun (x * y) =
        { toFun := ⇑f, map_one' := h₁ }.toFun x * { toFun := ⇑f, map_one' := h₁ }.toFun y)
  (h₃ : (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0)
  (h₄ :
    ∀ (x y : A),
      (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) =
        (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun x +
          (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun y)
  (h₅ :
    ∀ {i : ι} {x : A},
      x ∈ 𝒜 i → { toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ } x ∈ ℬ i),
  { toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, map_mem := h₅ } = f
-- Init.Data.Vector.Algebra
Vector.instZero : {α : Type u_1} → {n : ℕ} → [Zero α] → Zero (Vector α n)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.BindStruct.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X : C} {S : CategoryTheory.Presieve X}
  {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y} {Z : C} {h : Z ⟶ X} {Y : C} {g : Z ⟶ Y} {f : Y ⟶ X}
  {hf : S f} {hg : R hf g} {fac : CategoryTheory.CategoryStruct.comp g f = h} {Y_1 : C} {g_1 : Z ⟶ Y_1} {f_1 : Y_1 ⟶ X}
  {hf_1 : S f_1} {hg_1 : R hf_1 g_1} {fac_1 : CategoryTheory.CategoryStruct.comp g_1 f_1 = h},
  { Y := Y, g := g, f := f, hf := hf, hg := hg, fac := fac } =
      { Y := Y_1, g := g_1, f := f_1, hf := hf_1, hg := hg_1, fac := fac_1 } →
    Y = Y_1 ∧ g ≍ g_1 ∧ f ≍ f_1
-- Lean.Compiler.LCNF.Basic
/-- The body of the declaration, usually changes as it progresses
through compiler passes.
 -/
Lean.Compiler.LCNF.Decl.value : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Decl pu → Lean.Compiler.LCNF.DeclValue pu
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.Spec.reflective : CategoryTheory.Reflective AlgebraicGeometry.Scheme.Spec
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_add : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x₁ x₂ : R) (y₁ y₂ : ↥M),
  IsLocalization.mk' S (x₁ * ↑y₂ + x₂ * ↑y₁) (y₁ * y₂) = IsLocalization.mk' S x₁ y₁ + IsLocalization.mk' S x₂ y₂
-- Lean.Util.MonadCache
Lean.MonadCache.findCached? : {α β : Type} → {m : Type → Type} → [self : Lean.MonadCache α β m] → α → m (Option β)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.centralizer_le : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : IsScalarTower R A A] [inst_5 : SMulCommClass R A A] (s t : Set A),
  s ⊆ t → NonUnitalStarSubalgebra.centralizer R t ≤ NonUnitalStarSubalgebra.centralizer R s