mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Operations
Submodule.comap_unop_one : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) 1 = 1
-- Mathlib.CategoryTheory.EffectiveEpi.Comp
CategoryTheory.instEffectiveEpiFamilyCompOfIsSplitEpi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} {B : C} {X Y : α → C}
  (f : (a : α) → X a ⟶ B) (g : (a : α) → Y a ⟶ X a) [∀ (a : α), CategoryTheory.IsSplitEpi (g a)]
  [CategoryTheory.EffectiveEpiFamily X f],
  CategoryTheory.EffectiveEpiFamily Y fun a => CategoryTheory.CategoryStruct.comp (g a) (f a)
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasPosAssignment.eq_4 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned.hasPosAssignment = false
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- Evaluation of a `Γ` instance `I` for given solution `x`.  -/
ValuedCSP.Instance.evalSolution : {D : Type u_1} →
  {C : Type u_2} →
    [inst : AddCommMonoid C] →
      [inst_1 : PartialOrder C] →
        [inst_2 : IsOrderedAddMonoid C] → {Γ : ValuedCSP D C} → {ι : Type u_3} → Γ.Instance ι → (ι → D) → C
-- Mathlib.Topology.Algebra.Module.Star
starL_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : TopologicalSpace A]
  [inst_7 : ContinuousStar A] (a : A), (starL R) a = star a
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.toModuleEnd_bijective : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M], Function.Bijective ⇑(Module.toModuleEnd R M)
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
CategoryTheory.Sheaf.isConstant_of_forget : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {B : Type u_3} [inst_3 : CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B)
  [inst_4 : CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [inst_6 : J.HasSheafCompose U]
  (F : CategoryTheory.Sheaf J D) [(CategoryTheory.constantSheaf J D).Faithful] [(CategoryTheory.constantSheaf J D).Full]
  [(CategoryTheory.constantSheaf J B).Faithful] [(CategoryTheory.constantSheaf J B).Full]
  [(CategoryTheory.sheafCompose J U).ReflectsIsomorphisms]
  [CategoryTheory.Sheaf.IsConstant J ((CategoryTheory.sheafCompose J U).obj F)] {T : C}
  (hT : CategoryTheory.Limits.IsTerminal T), CategoryTheory.Sheaf.IsConstant J F
-- Mathlib.Order.Category.FinBoolAlg
/-- The powerset functor. `Set` as a functor.  -/
fintypeToFinBoolAlgOp : CategoryTheory.Functor FintypeCat FinBoolAlgᵒᵖ
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.hom_id : ∀ {X : CommGrpCat}, CommGrpCat.Hom.hom (CategoryTheory.CategoryStruct.id X) = MonoidHom.id ↑X
-- Init.Data.UInt.Lemmas
UInt32.neg_add_mul_eq_mul_not : ∀ {a b : UInt32}, -(a + a * b) = a * ~~~b
-- Mathlib.Tactic.ProxyType
/-- Returns a proxy type for a constructor and a pattern to use to match against it,
given a list of fvars for the constructor arguments and pattern names to use for the arguments.
The proxy type is expected to be a `Type*`.  -/
Mathlib.ProxyType.ProxyEquivConfig.mkCtorProxyType : Mathlib.ProxyType.ProxyEquivConfig → List (Lean.Expr × Lean.Name) → Lean.Elab.TermElabM (Lean.Expr × Lean.Term)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instSub : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        [inst : Ring R] →
          [inst_1 : (i : ι) → AddCommGroup (M₁ i)] →
            [inst_2 : AddCommGroup M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_6 : TopologicalSpace M₂] → [IsTopologicalAddGroup M₂] → Sub (ContinuousMultilinearMap R M₁ M₂)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.toHomeomorph_symm : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂),
  e.symm.toHomeomorph = e.toHomeomorph.symm
-- Init.Data.BEq
/-- `PartialEquivBEq α` says that the `BEq` implementation is a
partial equivalence relation, that is:
* it is symmetric: `a == b → b == a`
* it is transitive: `a == b → b == c → a == c`.
 -/
PartialEquivBEq : (α : Type u_1) → [BEq α] → Prop
-- Lean.Meta.TryThis
/-- Draws the color from a red-yellow-green color gradient with red at `0.0`, yellow at `0.5`, and
green at `1.0`. Values outside the range `[0.0, 1.0]` are clipped to lie within this range.

With `showValueInHoverText := true` (the default), the value `t` will be included in the `title` of
the HTML element (which appears on hover).  -/
Lean.Meta.Tactic.TryThis.SuggestionStyle.value : Float → optParam Bool true → Lean.Meta.Tactic.TryThis.SuggestionStyle
-- Mathlib.CategoryTheory.Subfunctor.OfSection
CategoryTheory.Subfunctor.mem_ofSection_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : Cᵒᵖ}
  (x : F.obj X), x ∈ (CategoryTheory.Subfunctor.ofSection x).obj X
-- Mathlib.CategoryTheory.Limits.Types.Equalizers
/-- Show the given fork in `Type u` is an equalizer given that any element in the "difference kernel"
comes from `X`.
The converse of `unique_of_type_equalizer`.
 -/
CategoryTheory.Limits.Types.typeEqualizerOfUnique : {X Y Z : Type u} →
  (f : X ⟶ Y) →
    {g h : Y ⟶ Z} →
      (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h) →
        (∀ (y : Y),
            (CategoryTheory.ConcreteCategory.hom g) y = (CategoryTheory.ConcreteCategory.hom h) y →
              ∃! x, (CategoryTheory.ConcreteCategory.hom f) x = y) →
          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.norm_projection_orthogonal_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (x : E), ‖(K.projection Kᗮ ⋯) x‖ ≤ ‖x‖
-- Mathlib.Order.Filter.Map
Function.LeftInverse.filter_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α},
  Function.LeftInverse g f → Function.LeftInverse (Filter.map g) (Filter.map f)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.mem_sdiv : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s t : Set β} {a : α}, a ∈ s /ₛ t ↔ ∃ x ∈ s, ∃ y ∈ t, x /ₛ y = a
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- `WithLp.fst` as a continuous linear map.  -/
WithLp.fstL : (p : ENNReal) →
  (𝕜 : Type u_1) →
    (α : Type u_2) →
      (β : Type u_3) →
        [inst : TopologicalSpace α] →
          [inst_1 : TopologicalSpace β] →
            [inst_2 : Semiring 𝕜] →
              [inst_3 : AddCommGroup α] →
                [inst_4 : AddCommGroup β] → [inst_5 : Module 𝕜 α] → [inst_6 : Module 𝕜 β] → WithLp p (α × β) →L[𝕜] α
-- Init.Data.Float.Model.Unpacked.Operations.Compare
/-- Determines whether `a` is equal to `b` according to IEEE rules.

This is not a reflexive relation.
 -/
Float.Model.UnpackedFloat.beq : Float.Model.UnpackedFloat → Float.Model.UnpackedFloat → Bool
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Predicate stating that the range between two positions of `s` can be covered by longest
reverse matches of the pattern within `s`.
 -/
String.Slice.Pattern.Model.IsLongestRevMatchAtChain : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.Model.PatternModel pat] → {s : String.Slice} → s.Pos → s.Pos → Prop
-- Mathlib.CategoryTheory.Action.Basic
Action.trivial_ρ : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G] (X : V),
  (Action.trivial G X).ρ = 1
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_lt_ediv_iff_of_dvd_of_pos_of_neg : ∀ {a b c d : ℤ}, 0 < b → d < 0 → b ∣ a → d ∣ c → (a / b < c / d ↔ c * b < d * a)
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.instHasSheafifyEtaleSmallEtaleTopology : ∀ {S : AlgebraicGeometry.Scheme} {A : Type u'} [inst : CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1}
  {CD : A → Type u} [inst_1 : (X Y : A) → FunLike (FA X Y) (CD X) (CD Y)]
  [inst_2 : CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
  [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A]
  [(CategoryTheory.forget A).ReflectsIsomorphisms]
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)],
  CategoryTheory.HasSheafify S.smallEtaleTopology A
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.bicategory_homCategory_id_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  (a b : CategoryTheory.Bicategory.InducedBicategory C F) (f : a ⟶ b),
  (CategoryTheory.CategoryStruct.id f).hom = CategoryTheory.CategoryStruct.id f.hom
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.instSemilatticeInf : {X : Type u_2} → [inst : TopologicalSpace X] → SemilatticeInf (DiscreteQuotient X)
-- Init.Grind.Config
/-- Minimum number of instantiations to trigger summary report in `#grind_lint`.
Remark: this option is only relevant for the `#grind_lint` command.
 -/
Lean.Grind.Config.min : Lean.Grind.Config → ℕ
-- Mathlib.CategoryTheory.Monoidal.Closed.Types
/-- This is not a good instance because of the universe levels. Below is the instance where the
target category is `Type (max u₁ v₁)`.  -/
CategoryTheory.cartesianClosedFunctorToTypes : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.MonoidalClosed (CategoryTheory.Functor C (Type (max u₁ v₁ u₂)))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensOptions : Type
-- Mathlib.Data.List.Sigma
List.lookupAll_eq_nil : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {l : List (Sigma β)},
  List.lookupAll a l = [] ↔ ∀ (b : β a), ⟨a, b⟩ ∉ l
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.add_empty : ∀ {α : Type u_2} [inst : Add α] {s : Set α}, s + ∅ = ∅
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor finset of `w` is the set of vertices
"below" `w` according to the adjacency relation of `G`.  -/
SimpleGraph.isBipartiteWith_bipartiteBelow : ∀ {V : Type u_1} {w : V} {G : SimpleGraph V} {s t : Finset V} [inst : Fintype ↑(G.neighborSet w)]
  [inst_1 : DecidableRel G.Adj], G.IsBipartiteWith ↑s ↑t → w ∈ t → G.neighborFinset w = Finset.bipartiteBelow G.Adj s w
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isUnramifiedIn : ∀ {k : Type u_1} [inst : Field k] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra k K]
  [IsUnramifiedAtInfinitePlaces k K] (w : NumberField.InfinitePlace k), NumberField.InfinitePlace.IsUnramifiedIn K w
-- Init.Data.SInt.Lemmas
Int16.ne_iff_toBitVec_ne : ∀ {a b : Int16}, a ≠ b ↔ a.toBitVec ≠ b.toBitVec
-- Mathlib.Data.DFinsupp.Defs
/-- `Π₀ i, β i` denotes the type of dependent functions with finite support `DFinsupp β`.  -/
«termΠ₀_,_» : Lean.ParserDescr
-- Mathlib.NumberTheory.ModularForms.LFunction
ModularForm.weakFEPair_g : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) [inst_2 : ModularFormClass F Γ k] (t : ℝ),
  (ModularForm.weakFEPair hk f).g t =
    (ModularForm.translate f
        (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)))
      (↑UpperHalfPlane.ofComplex (Complex.I * ↑t))
-- Mathlib.Analysis.BoxIntegral.Box.Basic
/-- The set of points in this box: this is the product of half-open intervals `(lower i, upper i]`,
where `lower` and `upper` are this box' corners.  -/
BoxIntegral.Box.toSet : {ι : Type u_1} → BoxIntegral.Box ι → Set (ι → ℝ)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) (x : Cᵒᵖ),
  (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F).app x =
    TypeCat.ofHom CategoryTheory.OverPresheafAux.YonedaCollection.yonedaEquivFst
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Polynomial.IsDistinguishedAt.isWeierstrassDivisorAt' : ∀ {A : Type u_1} [inst : CommRing A] {g : Polynomial A} {I : Ideal A},
  g.IsDistinguishedAt I → ∀ [IsHausdorff I A], (↑g).IsWeierstrassDivisorAt I
-- Mathlib.Algebra.Field.Subfield.Basic
/-- Product of elements of a subfield indexed by a `Finset` is in the subfield.  -/
Subfield.prod_mem : ∀ {K : Type u} [inst : Field K] (s : Subfield K) {ι : Type u_1} {t : Finset ι} {f : ι → K},
  (∀ c ∈ t, f c ∈ s) → ∏ i ∈ t, f i ∈ s
-- Mathlib.Logic.Equiv.Prod
Equiv.Perm.prodExtendRight.eq_1 : ∀ {α₁ : Type u_9} {β₁ : Type u_10} [inst : DecidableEq α₁] (a : α₁) (e : Equiv.Perm β₁),
  Equiv.Perm.prodExtendRight a e =
    { toFun := fun ab => if ab.1 = a then (a, e ab.2) else ab,
      invFun := fun ab => if ab.1 = a then (a, (Equiv.symm e) ab.2) else ab, left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instFinitenessRelation : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : LE α] →
      [inst_2 : DecidableLE α] →
        [Std.PRange.LawfulUpwardEnumerable α] →
          [Std.Rxc.IsAlwaysFinite α] → Std.Iterators.FinitenessRelation (Std.Rxc.Iterator α) Id
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.coe_mrange : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F), ↑(AddMonoidHom.mrange f) = Set.range ⇑f
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.leftUnitor_δ : ∀ {G : Type v} [inst : Monoid G] {k : Type u} [inst_1 : CommSemiring k] (X : Action (Type u) G),
  ↑(Representation.TensorProduct.lid k (Representation.linearize k G X)).symm =
    ((Representation.IntertwiningMap.rTensor (Representation.linearize k G X)
              (Representation.LinearizeMonoidal.η k G)).comp
          (Representation.LinearizeMonoidal.δ (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type u) G))
            X)).comp
      (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv)
-- Lean.Data.Lsp.Basic
Lean.Lsp.LocationLink.targetSelectionRange : Lean.Lsp.LocationLink → Lean.Lsp.Range
-- Mathlib.Order.Hom.PowersetCard
/-- The permutation of `Fin (m + n)` corresponding to adjoining a `Finset` of card `m`
to a `Finset` of card `n` and sorting the resulting set. In other words, given `s₁ < s₂ < ⋯ < sₘ`
and `t₁ < t₂ < ⋯ < tₙ` (disjoint) this is the permutation obtained by sorting
`s₁, s₂, …, sₘ, t₁, t₂, …, tₙ`.  -/
Set.powersetCard.permOfDisjoint : {m n : ℕ} →
  {I : Type u_2} →
    [LinearOrder I] →
      {s : ↑(Set.powersetCard I m)} → {t : ↑(Set.powersetCard I n)} → Disjoint ↑s ↑t → Equiv.Perm (Fin (m + n))
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.eq_zero_of_abs_lt_dvd : ∀ {m x : ℤ}, m ∣ x → |x| < m → x = 0
-- Mathlib.Topology.Algebra.StarSubalgebra
StarSubalgebra.topologicalClosure_mono : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A] [inst_6 : StarModule R A]
  [inst_7 : IsSemitopologicalSemiring A] [inst_8 : ContinuousStar A], Monotone StarSubalgebra.topologicalClosure
-- Mathlib.Algebra.Order.Round
round_add_one : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (a : α),
  round (a + 1) = round a + 1
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.equivEssImageOfReflective_functor : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {i : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective i],
  CategoryTheory.equivEssImageOfReflective.functor = i.toEssImage
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.instIsCorepresentableCompObjOppositeTypeCoyonedaOpObjLeftAdjointObjIsDefined : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D C) (X : F.PartialLeftAdjointSource),
  (F.comp (CategoryTheory.coyoneda.obj (Opposite.op X.obj))).IsCorepresentable
-- Mathlib.Algebra.Category.Ring.Limits
CommSemiRingCat.forget₂SemiRing_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndepOn.zero_notMem_image : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [Nontrivial R], LinearIndepOn R v s → 0 ∉ v '' s
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- The product of linear maps into an `R`-algebra is a quadratic map.  -/
QuadraticMap.linMulLin : {R : Type u_3} →
  {M : Type u_4} →
    {A : Type u_7} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module R M] →
              [inst_4 : Module R A] →
                [SMulCommClass R A A] → [IsScalarTower R A A] → (M →ₗ[R] A) → (M →ₗ[R] A) → QuadraticMap R M A
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
tangentBundleCore_localTriv_baseSet : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (i : ↑(atlas H M)),
  ((tangentBundleCore I M).localTriv i).baseSet = (↑i).source
-- Mathlib.GroupTheory.Coset.Basic
/-- A (non-canonical) bijection between an `AddGroup` `α` and the product `(α/s) × s`  -/
AddSubgroup.addGroupEquivQuotientProdAddSubgroup : {α : Type u_1} → [inst : AddGroup α] → {s : AddSubgroup α} → α ≃ (α ⧸ s) × ↥s
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- If `C` is a locally `w`-small category, this is a (colimit) cocone
expressing `F : C ⥤ Type w` as a colimit of corepresentable functors.  -/
CategoryTheory.Functor.Elements.coconeπOpCompShrinkYonedaFlip : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      (F : CategoryTheory.Functor C (Type w)) →
        CategoryTheory.Limits.Cocone
          ((CategoryTheory.CategoryOfElements.π F).op.comp CategoryTheory.shrinkYoneda.{w, v₁, u₁}.flip)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_roc : ∀ {m n i : ℕ}, (m<...=n).toArray[i]! = if i < n - m then m + 1 + i else 0
-- Mathlib.Algebra.Algebra.Epi
TensorProduct.lid'_symm_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : Algebra.IsEpi R A] (M : Type u_3) [inst_4 : AddCommMonoid M] [inst_5 : Module R M] [inst_6 : Module A M]
  [inst_7 : IsScalarTower R A M] (m : M), (TensorProduct.lid' R A M).symm m = 1 ⊗ₜ[R] m
-- Mathlib.Order.Filter.Basic
Filter.Frequently.of_forall : ∀ {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop}, (∀ (x : α), p x) → ∃ᶠ (x : α) in f, p x
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.rectVandermonde_apply_zero_right : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} {α : Type u_3} {v w : α → R} {i : α},
  w i = 0 → Matrix.rectVandermonde v w (n + 1) i = Pi.single (Fin.last n) (v i ^ n)
-- Init.Data.Nat.Basic
Nat.pow_le_pow_left : ∀ {n m : ℕ}, n ≤ m → ∀ (i : ℕ), n ^ i ≤ m ^ i
-- Mathlib.Topology.UniformSpace.Basic
le_iff_uniformContinuous_id : ∀ {α : Type ua} {u v : UniformSpace α}, u ≤ v ↔ UniformContinuous id
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.comp_preservesFiniteProducts : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFiniteProducts F]
  [CategoryTheory.Limits.PreservesFiniteProducts G], CategoryTheory.Limits.PreservesFiniteProducts (F.comp G)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.maxKeyD_modifyKey_eq_maxKeyD : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β} {fallback : α},
      Std.Internal.List.maxKeyD (Std.Internal.List.Const.modifyKey k f l) fallback =
        Std.Internal.List.maxKeyD l fallback
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiff.mk : Lean.SubExpr.PosMap Lean.Widget.ExprDiffTag✝ → Lean.SubExpr.PosMap Lean.Widget.ExprDiffTag✝ → Lean.Widget.ExprDiff✝
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.Hereditarily.self : ∀ {p : ZFSet.{u} → Prop} {x : ZFSet.{u}}, ZFSet.Hereditarily p x → p x
-- Init.Data.SInt.Bitwise
UInt64.toInt64_xor : ∀ (a b : UInt64), (a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64
-- Mathlib.MeasureTheory.Measure.Regular
/-- If `μ` is a weakly regular measure, then any open set can be approximated by a closed subset.  -/
IsOpen.exists_lt_isClosed : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.WeaklyRegular] ⦃U : Set α⦄, IsOpen U → ∀ {r : ENNReal}, r < μ U → ∃ F ⊆ U, IsClosed F ∧ r < μ F
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_le_withBotDegree_iff : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f g : MvPolynomial σ R),
  m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)
-- Mathlib.RingTheory.PowerSeries.Restricted
/-- Restricted power series as an additive subgroup of `PowerSeries R`.  -/
PowerSeries.IsRestricted.addSubgroup : {R : Type u_1} → [inst : NormedRing R] → ℝ → AddSubgroup (PowerSeries R)
-- Mathlib.Data.Set.Finite.Lemmas
Set.Finite.fin_param : ∀ {α : Type u} {s : Set α}, s.Finite → ∃ n f, Function.Injective f ∧ Set.range f = s
-- Mathlib.CategoryTheory.SingleObj
/-- The units in a monoid are (multiplicatively) equivalent to
the automorphisms of `star` when we think of the monoid as a single-object category.  -/
Units.toAut : (M : Type u) → [inst : Monoid M] → Mˣ ≃* CategoryTheory.Aut (CategoryTheory.SingleObj.star M)
-- Std.Tactic.Do.Syntax
/-- `mspecialize` is like `specialize`, but operating on a stateful `Std.Do.SPred` goal.
It specializes a hypothesis from the stateful context with hypotheses from either the pure
or stateful context or pure terms.
```lean
example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
  mintro HP HPQ
  mspecialize HPQ HP
  mexact HPQ

example (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) : ⊢ₛ Q → (∀ x, P → Q → Ψ x) → Ψ (y + 1) := by
  mintro HQ HΨ
  mspecialize HΨ (y + 1) hP HQ
  mexact HΨ
```
 -/
Lean.Parser.Tactic.mspecialize : Lean.ParserDescr
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.max!.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → (Unit → motive none) → ((x : α) → motive (some x)) → motive x
-- Std.Http.Protocol.H1.Reader
/-- Returns the current parse error if the reader has failed.
 -/
Std.Http.Protocol.H1.Reader.getError : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → Option Std.Http.Protocol.H1.Error