mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
HomogeneousSubmodule.mk.injEq : ∀ {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [inst : Semiring A]
  [inst_1 : AddCommMonoid M] [inst_2 : Module A M] {𝒜 : ιA → σA} {ℳ : ιM → σM} [inst_3 : DecidableEq ιA]
  [inst_4 : AddMonoid ιA] [inst_5 : SetLike σA A] [inst_6 : AddSubmonoidClass σA A] [inst_7 : GradedRing 𝒜]
  [inst_8 : DecidableEq ιM] [inst_9 : SetLike σM M] [inst_10 : AddSubmonoidClass σM M]
  [inst_11 : DirectSum.Decomposition ℳ] [inst_12 : VAdd ιA ιM] [inst_13 : SetLike.GradedSMul 𝒜 ℳ]
  (toSubmodule : Submodule A M) (is_homogeneous' : toSubmodule.IsHomogeneous ℳ) (toSubmodule_1 : Submodule A M)
  (is_homogeneous'_1 : toSubmodule_1.IsHomogeneous ℳ),
  ({ toSubmodule := toSubmodule, is_homogeneous' := is_homogeneous' } =
      { toSubmodule := toSubmodule_1, is_homogeneous' := is_homogeneous'_1 }) =
    (toSubmodule = toSubmodule_1)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C_one : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.C R 1 = Polynomial.X
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.le_trailingDegree_monomial : ∀ {R : Type u} {a : R} {n : ℕ} [inst : Semiring R], ↑n ≤ ((Polynomial.monomial n) a).trailingDegree
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The canonical morphism from `G` to its profinite completion.  -/
ProfiniteGrp.ProfiniteCompletion.eta : (G : GrpCat) → G ⟶ GrpCat.of ↑(ProfiniteGrp.ProfiniteCompletion.completion G).toProfinite.toTop
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α}, (k == k') = true → m.getKey? k = m.getKey? k'
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
HasSum.const_div : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : DivisionSemiring α] [inst_1 : TopologicalSpace α]
  [IsTopologicalSemiring α] {f : ι → α} {a : α},
  HasSum (fun x => 1 / f x) a L → ∀ (b : α), HasSum (fun i => b / f i) (b * a) L
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.ι_leftInverse : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Function.LeftInverse ⇑TensorAlgebra.ιInv ⇑(TensorAlgebra.ι R)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_add_iff_right : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LT α] [AddRightStrictMono α] [AddRightReflectLT α] (a : α) {b c : α},
  b + a < c + a ↔ b < c
-- Mathlib.Geometry.Manifold.Instances.Icc
contMDiffOn_comp_projIcc_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {x y : ℝ}
  [h : Fact (x < y)] {n : WithTop ℕ∞} {f : ↑(Set.Icc x y) → M},
  ContMDiffOn (modelWithCornersSelf ℝ ℝ) I n (f ∘ Set.projIcc x y ⋯) (Set.Icc x y) ↔
    ContMDiff (modelWithCornersEuclideanHalfSpace 1) I n f
-- Mathlib.Data.PFunctor.Univariate.Basic
/-- We prefer `PFunctor.map` to `Functor.map` because it is universe-polymorphic.  -/
PFunctor.map_eq_map : ∀ (P : PFunctor.{uA, uB}) {α β : Type v} (f : α → β) (x : ↑P α), f <$> x = P.map f x
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.valuation_surjective : ∀ (K : Type u_2) [inst : Field K], Function.Surjective ⇑Valued.v
-- Mathlib.Data.Sigma.Interval
Sigma.instLocallyFiniteOrderBot : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Preorder (α i)] → [(i : ι) → LocallyFiniteOrderBot (α i)] → LocallyFiniteOrderBot ((i : ι) × α i)
-- Init.Data.Int.DivMod.Basic
Int.negSucc_ediv_ofNat_succ : ∀ {a b : ℕ}, Int.negSucc a / ↑(b + 1) = Int.negSucc (a / b.succ)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- Change of variables. If `f` has continuous derivative `f'` on `[a, b]`,
and `g` is continuous on `f '' [a, b]`, then we can substitute `u = f x` to get
`∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u`.
Compared to `intervalIntegral.integral_deriv_smul_comp` we only require that `g` is continuous on
`f '' [a, b]`.

If the function `f` is monotone or antitone, see also `integral_deriv_smul_comp_of_deriv_nonneg`
and `integral_deriv_smul_comp_of_deriv_nonpos` dropping all assumptions on `g`.  -/
intervalIntegral.integral_deriv_smul_comp' : ∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E},
  (∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
    ContinuousOn f' (Set.uIcc a b) →
      ContinuousOn g (f '' Set.uIcc a b) → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (x : ℝ) in f a..f b, g x
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
CategoryTheory.Limits.instPreservesColimitsOfShapeOppositeDiscrete : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {I : Type w} (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F],
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I)ᵒᵖ F
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
/-- Two morphisms from a horn are equal if they are equal on all suitable faces.  -/
SSet.horn.hom_ext : ∀ {n : ℕ} {i : Fin (n + 2)} {S : SSet} (σ₁ σ₂ : (SSet.horn (n + 1) i).toSSet ⟶ S),
  (∀ (j : Fin (n + 2)) (h : j ≠ i),
      (CategoryTheory.ConcreteCategory.hom (σ₁.app (Opposite.op { len := n }))) (SSet.horn.face i j h) =
        (CategoryTheory.ConcreteCategory.hom (σ₂.app (Opposite.op { len := n }))) (SSet.horn.face i j h)) →
    σ₁ = σ₂
-- Mathlib.Algebra.BigOperators.ModEq
Nat.prod_modEq_single : ∀ {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Finset α} {a : α},
  (a ∉ s → f a ≡ 1 [MOD n]) → (∀ x ∈ s, x ≠ a → f x ≡ 1 [MOD n]) → ∏ x ∈ s, f x ≡ f a [MOD n]
-- Mathlib.CategoryTheory.Sites.Whiskering
/-- Composing a sheaf with a functor preserving the limit of `(S.index P).multicospan` yields a functor
between sheaf categories.
 -/
CategoryTheory.hasSheafCompose_of_preservesMulticospan : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C)
  (F : CategoryTheory.Functor A B)
  [∀ (X : C) (S : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ A),
      CategoryTheory.Limits.PreservesLimit (S.index P).multicospan F],
  J.HasSheafCompose F
-- Mathlib.CategoryTheory.Sites.CoverPreserving
/-- `CompatiblePreserving` functors indeed preserve compatible families.  -/
CategoryTheory.Presieve.FamilyOfElements.Compatible.functorPushforward : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D},
  CategoryTheory.CompatiblePreserving K G →
    ∀ (ℱ : CategoryTheory.Sheaf K (Type w)) {Z : C} {T : CategoryTheory.Presieve Z}
      {x : CategoryTheory.Presieve.FamilyOfElements (G.op.comp ℱ.obj) T},
      x.Compatible → (CategoryTheory.Presieve.FamilyOfElements.functorPushforward G x).Compatible
-- Lean.Meta.TryThis
/-- Suggestion edit as it will be applied to the editor document.  -/
Lean.Meta.Tactic.TryThis.TryThisInfo.edit : Lean.Meta.Tactic.TryThis.TryThisInfo → Lean.Lsp.TextEdit
-- Mathlib.Tactic.DepRewrite
/-- `rewrite!` is like `rewrite`,
but can also insert casts to adjust types that depend on the LHS of a rewrite.
It is available as an ordinary tactic and a `conv` tactic.

The sort of casts that are inserted is controlled by the `castMode` configuration option.
By default, only proof terms are casted;
by proof irrelevance, this adds no observable complexity.

With `rewrite! +letAbs (castMode := .all)`, casts are inserted whenever necessary.
This means that the 'motive is not type correct' error never occurs,
at the expense of creating potentially complicated terms.
 -/
Mathlib.Tactic.DepRewrite.Conv.evalDepRewriteSeq : Lean.Elab.Tactic.Tactic
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sqrtTwoAddSeries.eq_1 : ∀ (x : ℝ), x.sqrtTwoAddSeries 0 = x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffineLift_some : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {X Y : F} (h : W.NonsingularLift ⟦![X, Y, 1]⟧),
  { point := ⟦![X, Y, 1]⟧, nonsingular := h }.toAffineLift = WeierstrassCurve.Affine.Point.some X Y ⋯
-- Mathlib.Topology.Separation.Basic
/-- Removing a non-isolated point from a dense set, one still obtains a dense set.  -/
Dense.sdiff_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {s : Set X},
  Dense s → ∀ (x : X) [(nhdsWithin x {x}ᶜ).NeBot], Dense (s \ {x})
-- Init.Data.UInt.Lemmas
UInt16.mul_add : ∀ {a b c : UInt16}, a * (b + c) = a * b + a * c
-- Mathlib.Algebra.Lie.Nilpotent
LieRing.IsNilpotent.eq_1 : ∀ (L : Type v) [inst : LieRing L], LieRing.IsNilpotent L = LieModule.IsNilpotent L L
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.cocone_naturality_components : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) (j j' : J) (f : j ⟶ j')
  (x : ↑(F.obj j)),
  (CategoryTheory.ConcreteCategory.hom (RingCat.Colimits.coconeMorphism F j'))
      ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) =
    (CategoryTheory.ConcreteCategory.hom (RingCat.Colimits.coconeMorphism F j)) x
-- Mathlib.Order.Filter.Basic
Filter.mem_inf_principal' : ∀ {α : Type u} {f : Filter α} {s t : Set α}, s ∈ f ⊓ Filter.principal t ↔ tᶜ ∪ s ∈ f
-- Mathlib.LinearAlgebra.Eigenspace.Minpoly
/-- An endomorphism of a finite-dimensional vector space has finitely many eigenvalues.  -/
Module.End.instFintypeEigenvalues : {R : Type v} →
  {M : Type w} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (f : Module.End R M) → [IsDomain R] → [Module.Finite R M] → [Module.IsTorsionFree R M] → Fintype f.Eigenvalues
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.instIsOpenImmersionH₀ : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {𝒱 : X.OpenCover} (f : 𝒰 ⟶ 𝒱) (i : 𝒰.I₀),
  AlgebraicGeometry.IsOpenImmersion (f.h₀ i)
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.IndGroupInfo.numMotives : Lean.Elab.Structural.IndGroupInfo → ℕ
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.norm_sum_eq_sup'_of_pairwise_ne : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] {s : Finset ι} {f : ι → M}
  (hs' : s.Nonempty), ((↑s).Pairwise fun i j => ‖f i‖ ≠ ‖f j‖) → ‖∑ i ∈ s, f i‖ = s.sup' hs' fun i => ‖f i‖
-- Init.PropLemmas
forall_apply_eq_imp_iff : ∀ {α : Sort u_2} {β : Sort u_1} {f : α → β} {p : β → Prop}, (∀ (b : β) (a : α), f a = b → p b) ↔ ∀ (a : α), p (f a)
-- Std.Data.ExtTreeMap.Lemmas
/-- Simpler variant of `getElem_filterMap` when `LawfulEqCmp` is available.  -/
Std.ExtTreeMap.getElem_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : α → β → Option γ} {k : α} {h : k ∈ Std.ExtTreeMap.filterMap f t},
  (Std.ExtTreeMap.filterMap f t)[k] = (f k t[k]).get ⋯
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Complex.not_differentiableAt_Gamma_neg_nat : ∀ (n : ℕ), ¬DifferentiableAt ℂ Complex.Gamma (-↑n)
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.State.mk.inj : ∀ {share : Lean.Meta.Sym.AlphaShareCommon.State} {maxFVar : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.FVarId)}
  {proofInstInfo : Lean.PHashMap Lean.Name (Option Lean.Meta.Sym.ProofInstInfo)}
  {inferType : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr}
  {getLevel : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Level}
  {congrInfo : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Sym.CongrInfo}
  {defEqI : Lean.PHashMap (Lean.Meta.Sym.ExprPtr × Lean.Meta.Sym.ExprPtr) Bool}
  {extensions : Array Lean.Meta.Sym.SymExtensionState} {issues : List Lean.MessageData}
  {canon : Lean.Meta.Sym.Canon.State} {instanceOverrides : Lean.PHashMap Lean.Expr Lean.Expr} {debug : Bool}
  {share_1 : Lean.Meta.Sym.AlphaShareCommon.State}
  {maxFVar_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.FVarId)}
  {proofInstInfo_1 : Lean.PHashMap Lean.Name (Option Lean.Meta.Sym.ProofInstInfo)}
  {inferType_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr}
  {getLevel_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Level}
  {congrInfo_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Sym.CongrInfo}
  {defEqI_1 : Lean.PHashMap (Lean.Meta.Sym.ExprPtr × Lean.Meta.Sym.ExprPtr) Bool}
  {extensions_1 : Array Lean.Meta.Sym.SymExtensionState} {issues_1 : List Lean.MessageData}
  {canon_1 : Lean.Meta.Sym.Canon.State} {instanceOverrides_1 : Lean.PHashMap Lean.Expr Lean.Expr} {debug_1 : Bool},
  { share := share, maxFVar := maxFVar, proofInstInfo := proofInstInfo, inferType := inferType, getLevel := getLevel,
        congrInfo := congrInfo, defEqI := defEqI, extensions := extensions, issues := issues, canon := canon,
        instanceOverrides := instanceOverrides, debug := debug } =
      { share := share_1, maxFVar := maxFVar_1, proofInstInfo := proofInstInfo_1, inferType := inferType_1,
        getLevel := getLevel_1, congrInfo := congrInfo_1, defEqI := defEqI_1, extensions := extensions_1,
        issues := issues_1, canon := canon_1, instanceOverrides := instanceOverrides_1, debug := debug_1 } →
    share = share_1 ∧
      maxFVar = maxFVar_1 ∧
        proofInstInfo = proofInstInfo_1 ∧
          inferType = inferType_1 ∧
            getLevel = getLevel_1 ∧
              congrInfo = congrInfo_1 ∧
                defEqI = defEqI_1 ∧
                  extensions = extensions_1 ∧
                    issues = issues_1 ∧ canon = canon_1 ∧ instanceOverrides = instanceOverrides_1 ∧ debug = debug_1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
/-- A rank function for a pairing is a function from the type (II) simplices
to a partially ordered type which maps ancestrality relations to strict inequalities.  -/
SSet.Subcomplex.Pairing.RankFunction : {X : SSet} → {A : X.Subcomplex} → A.Pairing → (α : Type v) → [PartialOrder α] → Type (max u v)
-- Lean.Hygiene
Lean.getSanitizeNames : Lean.Options → Bool
-- Init.Data.Iterators.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Combinators.Monadic.Attach.0.Std.Iterators.Types.Attach.Monadic.modifyStep.match_1.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {P : β → Prop}
  (it : Std.IterM m { out // P out }) (motive : it.internalState.inner.Step → Sort u_3)
  (property : it.internalState.inner.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Mathlib.Algebra.Lie.Basic
LieHom.coe_one : ∀ {R : Type u} {L₁ : Type v} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁], ⇑1 = id
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.add : ∀ {R : Type u_1} [inst : AddMonoid R] [inst_1 : StarAddMonoid R] {x y : R},
  IsSelfAdjoint x → IsSelfAdjoint y → IsSelfAdjoint (x + y)
-- Mathlib.RingTheory.FinitePresentation
/-- [Stacks Tag 0561](https://stacks.math.columbia.edu/tag/0561) -/
Algebra.FinitePresentation.of_restrict_scalars_finitePresentation : ∀ (R : Type w₁) (A : Type w₂) (B : Type w₃) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B]
  [Algebra.FinitePresentation R B] [Algebra.FiniteType R A], Algebra.FinitePresentation A B
-- Init.Data.String.Basic
String.utf8encode_data : ∀ {b : String}, b.toList.utf8Encode = b.toByteArray
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Construct a `NormalExpr` expression from a `WhiskerLeft` expression.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.ofM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
      [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] →
        [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
          Mathlib.Tactic.BicategoryLike.WhiskerLeft → m Mathlib.Tactic.BicategoryLike.NormalExpr
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- If `f` is an open immersion `X ⟶ Y`, the global sections of `X`
are naturally isomorphic to the sections of `Y` over the image of `f`.  -/
AlgebraicGeometry.IsOpenImmersion.ΓIso : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.IsOpenImmersion f] →
      (U : Y.Opens) →
        X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)) ≅
          Y.presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.Hom.opensRange f ⊓ U))
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_Iio : ∀ (o : Ordinal.{u}), Order.cof ↑(Set.Iio o) = (Ordinal.lift.{u + 1, u} o).cof
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.sieveOfSubfunctor_functorInclusion : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X},
  CategoryTheory.Sieve.sieveOfSubfunctor S.functorInclusion = S
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedAddCommGroup.mk : {E : Type u_8} →
  [toNorm : Norm E] →
    [toAddCommGroup : AddCommGroup E] →
      [toPseudoMetricSpace : PseudoMetricSpace E] →
        autoParam (∀ (x y : E), dist x y = ‖-x + y‖) SeminormedAddCommGroup.dist_eq._autoParam →
          SeminormedAddCommGroup E
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
/-- The value of the Infimum of a nonempty set of outer measures on a set is not simply
the minimum value of a measure on that set: it is the infimum sum of measures of countable set of
sets that covers that set, where a different measure can be used for each set in the cover.  -/
MeasureTheory.OuterMeasure.sInf_apply : ∀ {α : Type u_1} {m : Set (MeasureTheory.OuterMeasure α)} {s : Set α},
  m.Nonempty → (sInf m) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, μ (t n)
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.Path.ext'_iff : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} {m : ℕ} {f g : X.Path (m + 1)},
  f = g ↔ ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
/-- Normal elements commute with their absolute value.  -/
CFC.commute_abs_self : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A),
  autoParam (IsStarNormal a) CFC.commute_abs_self._auto_1 → Commute (CFC.abs a) a
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- Twice the associated bilinear map of `Q` is the same as the polar of `Q`.  -/
QuadraticMap.two_nsmul_associated : ∀ (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : CommSemiring S] [inst_6 : Algebra S R]
  [inst_7 : Module S N] [inst_8 : IsScalarTower S R N] [inst_9 : Invertible 2] (Q : QuadraticMap R M N),
  2 • (QuadraticMap.associatedHom S) Q = Q.polarBilin
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.unop_whiskerRight_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {H : CategoryTheory.Functor Dᵒᵖ Eᵒᵖ} (α : F ⟶ G) {Z : CategoryTheory.Functor C E} (h : (F.comp H).unop ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.unop (CategoryTheory.Functor.whiskerRight α H)) h =
    CategoryTheory.CategoryStruct.comp (G.unopComp H).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.unop α) H.unop)
        (CategoryTheory.CategoryStruct.comp (F.unopComp H).inv h))
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- The presheaf of smooth functions from `M` to `G`, for `G` an additive Lie group,
as a presheaf of additive groups.  -/
smoothPresheafAddGroup : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              ModelWithCorners 𝕜 EM HM →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [ChartedSpace HM M] →
                                  (G : Type u) →
                                    [inst_9 : TopologicalSpace G] →
                                      [inst_10 : ChartedSpace H G] →
                                        [inst_11 : AddGroup G] →
                                          [LieAddGroup I (↑⊤) G] → TopCat.Presheaf AddGrpCat (TopCat.of M)
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.dual_div_dual : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] {I J : FractionalIdeal (nonZeroDivisors B) L},
  FractionalIdeal.dual A K J / FractionalIdeal.dual A K I = I / J
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.conj_apply_self : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (g : G) (φ : ρ.Equiv σ), φ.toLinearEquiv.conj (ρ g) = σ g
-- Std.Http.Protocol.H1.Reader
/-- Parse chunk data for the current chunk.
 -/
Std.Http.Protocol.H1.Reader.BodyState.chunkedBody : Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue) → ℕ → Std.Http.Protocol.H1.Reader.BodyState
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.instInhabited.eq_1 : AddMagmaCat.instInhabited = { default := AddMagmaCat.of PEmpty.{u_1 + 1} }
-- Mathlib.GroupTheory.FiniteAbelian.Basic
/-- **Alias** of `CommGroup.finite_of_fg_isMulTorsion`. -/
CommGroup.finite_of_fg_torsion : ∀ (G : Type u) [inst : CommGroup G] [Group.FG G], IsMulTorsion G → Finite G
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.basis_apply : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) (i : Fin f.natDegree), h.basis i = h.root ^ ↑i
-- Mathlib.Data.Seq.Basic
Stream'.Seq.join_append : ∀ {α : Type u} (S T : Stream'.Seq (Stream'.Seq1 α)), (S.append T).join = S.join.append T.join
-- Lean.Data.Lsp.Internal
/-- Start character of range.  -/
Lean.Lsp.DeclInfo.rangeStartPosCharacter : Lean.Lsp.DeclInfo → ℕ