mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Functor.IsLocalization.instCompOfIsEquivalence : ∀ {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) (E : Type u_3) [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor D E) [F.IsEquivalence] [L.IsLocalization W], (L.comp F).IsLocalization W
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.fibrations_over_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C) [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C],
  HomotopicalAlgebra.fibrations (CategoryTheory.Over S) = (HomotopicalAlgebra.fibrations C).over
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider differentiable maps `v : M → E₁` and `w : M → E₂` to vector bundles, over a base map
`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
One can apply `ψ  m` to `v m` and `w m`, and the resulting map is differentiable.

We give here a version of this statement at a point.  -/
MDifferentiableAt.clm_bundle_apply₂ : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {F₃ : Type u_5} {M : Type u_6}
  [inst : NontriviallyNormedField 𝕜] {E₁ : B → Type u_7} [inst_1 : (x : B) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_8}
  [inst_7 : (x : B) → AddCommGroup (E₂ x)] [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂]
  [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {E₃ : B → Type u_9} [inst_13 : (x : B) → AddCommGroup (E₃ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₃ x)] [inst_15 : NormedAddCommGroup F₃] [inst_16 : NormedSpace 𝕜 F₃]
  [inst_17 : TopologicalSpace (Bundle.TotalSpace F₃ E₃)] [inst_18 : (x : B) → TopologicalSpace (E₃ x)] {EB : Type u_10}
  [inst_19 : NormedAddCommGroup EB] [inst_20 : NormedSpace 𝕜 EB] {HB : Type u_11} [inst_21 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_22 : TopologicalSpace B] [inst_23 : ChartedSpace HB B] {EM : Type u_12}
  [inst_24 : NormedAddCommGroup EM] [inst_25 : NormedSpace 𝕜 EM] {HM : Type u_13} [inst_26 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_27 : TopologicalSpace M] [inst_28 : ChartedSpace HM M]
  [inst_29 : FiberBundle F₁ E₁] [inst_30 : VectorBundle 𝕜 F₁ E₁] [inst_31 : FiberBundle F₂ E₂]
  [inst_32 : VectorBundle 𝕜 F₂ E₂] [inst_33 : FiberBundle F₃ E₃] [inst_34 : VectorBundle 𝕜 F₃ E₃] {b : M → B}, ⋯
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `insertManyIfNew` which can be used in absence of balance information but still
assumes the preconditions of `insertManyIfNew`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.insertManyIfNew! : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      {ρ : Type w} →
        [ForIn Id ρ ((a : α) × β a)] → (t : Std.DTreeMap.Internal.Impl α β) → ρ → t.IteratedSlowNewInsertionInto
-- Mathlib.Logic.Relator
Relator.rel_not : Relator.LiftFun Iff Iff Not Not
-- Mathlib.LinearAlgebra.Matrix.IsDiag
Matrix.IsDiag.neg : ∀ {α : Type u_1} {n : Type u_4} [inst : SubtractionMonoid α] {A : Matrix n n α}, A.IsDiag → (-A).IsDiag
-- Init.Grind.AC
Lean.Grind.AC.Seq.eraseDup_k_eq_eraseDup : ∀ (s : Lean.Grind.AC.Seq), s.eraseDup_k = s.eraseDup
-- Mathlib.Algebra.Group.Int.Defs
Int.instAddCommSemigroup : AddCommSemigroup ℤ
-- Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
/-- If `A` is a family of enough low-degree polynomials over a finite semiring, there is a
pair of equal elements in `A`.  -/
Polynomial.exists_eq_polynomial : ∀ {Fq : Type u_1} [inst : Fintype Fq] [inst_1 : Semiring Fq] {d m : ℕ},
  Fintype.card Fq ^ d ≤ m →
    ∀ (b : Polynomial Fq),
      b.natDegree ≤ d →
        ∀ (A : Fin m.succ → Polynomial Fq),
          (∀ (i : Fin m.succ), (A i).degree < b.degree) → ∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ModuleDocstringState.mk.injEq : ∀ (toState : Lean.Doc.State)
  (scopedExts : Array (Lean.ScopedEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState))
  (toState_1 : Lean.Doc.State)
  (scopedExts_1 : Array (Lean.ScopedEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState)),
  ({ toState := toState, scopedExts := scopedExts } = { toState := toState_1, scopedExts := scopedExts_1 }) =
    (toState = toState_1 ∧ scopedExts = scopedExts_1)
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.diagramMap.eq_1 : ∀ {ι : Type v} {α : Type u} (U : ι → α) [inst : SemilatticeInf α] (i : ι),
  CategoryTheory.Pairwise.diagramMap U (CategoryTheory.Pairwise.Hom.id_single i) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Pairwise.diagramObj U (CategoryTheory.Pairwise.single i))
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.saturation_top : ∀ {M : Type u_1} [inst : AddZeroClass M], ⊤.saturation = ⊤
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.ofAddUnits_sSup : ∀ {M : Type u_1} [inst : AddMonoid M] (s : Set (AddSubgroup (AddUnits M))), (sSup s).ofAddUnits = ⨆ S ∈ s, S.ofAddUnits
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_eq_max'_orderOf : ∀ {G : Type u} [inst : CancelCommMonoid G] [inst_1 : Fintype G],
  Monoid.exponent G = (Finset.image orderOf Finset.univ).max' ⋯
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.widthInfty_nonneg : ∀ (𝒢 : Subgroup (GL (Fin 2) ℝ)), 0 ≤ 𝒢.widthInfty
-- ProofWidgets.Component.Panel.Basic
/-- The current tactic-mode goals.  -/
ProofWidgets.PanelWidgetProps.goals : ProofWidgets.PanelWidgetProps → Array Lean.Widget.InteractiveGoal
-- Mathlib.Algebra.Lie.Subalgebra
/-- An equivalence of Lie algebras restricts to an equivalence from any Lie subalgebra onto its
image.  -/
LieEquiv.ofSubalgebras : {R : Type u} →
  {L₁ : Type v} →
    {L₂ : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] →
          [inst_2 : LieRing L₂] →
            [inst_3 : LieAlgebra R L₁] →
              [inst_4 : LieAlgebra R L₂] →
                (L₁' : LieSubalgebra R L₁) →
                  (L₂' : LieSubalgebra R L₂) →
                    (e : L₁ ≃ₗ⁅R⁆ L₂) → LieSubalgebra.map e.toLieHom L₁' = L₂' → ↥L₁' ≃ₗ⁅R⁆ ↥L₂'
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.not_isCyclic : ∀ {n : ℕ}, n ≠ 1 → ¬IsCyclic (DihedralGroup n)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.uniformContinuous_iff_le : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃a b : α⦄, dist a b ≤ δ → dist (f a) (f b) ≤ ε
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateRow_inj : ∀ {n : Type u_3} {α : Type v} {ι : Type u_6} [Nonempty ι] {v w : n → α},
  Matrix.replicateRow ι v = Matrix.replicateRow ι w ↔ v = w
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
addMonoidAlgebraEquivDirectSum_symm_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring M] [inst_2 : (m : M) → Decidable (m ≠ 0)],
  ⇑addMonoidAlgebraEquivDirectSum.symm = DirectSum.toAddMonoidAlgebra
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.ι_biproductComparison' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁}
  (F : CategoryTheory.Functor C D) (f : J → C) [inst_4 : CategoryTheory.Limits.HasBiproduct f]
  [inst_5 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (F.obj ∘ f) j) (F.biproductComparison' f) =
    F.map (CategoryTheory.Limits.biproduct.ι f j)
-- Mathlib.Order.Filter.Bases.Basic
Filter.Tendsto.basis_both : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {ι' : Sort u_5} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α}
  {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β} {f : α → β},
  Filter.Tendsto f la lb →
    la.HasBasis pa sa → lb.HasBasis pb sb → ∀ (ib : ι'), pb ib → ∃ ia, pa ia ∧ Set.MapsTo f (sa ia) (sb ib)
-- Qq.MatchImpl
Qq.Impl.mkIsDefEqResult : Bool →
  (decls : List Qq.Impl.PatVarDecl) →
    have a := Qq.Impl.mkIsDefEqType decls;
    Q(«$a»)
-- Mathlib.Order.Defs.Unbundled
/-- The carrier of a `LowerSet`.  -/
LowerSet.carrier : {α : Type u_1} → [inst : LE α] → LowerSet α → Set α
-- Mathlib.Analysis.Seminorm
/-- **Alias** of `smul_apply`. -/
Seminorm.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.map_map : ∀ {V : Type u} {V' : Type v} {V'' : Type w} {G : SimpleGraph V} {G' : SimpleGraph V'} {G'' : SimpleGraph V''}
  (f : G →g G') (f' : G' →g G'') {u v : V} (p : G.Walk u v),
  SimpleGraph.Walk.map f' (SimpleGraph.Walk.map f p) = SimpleGraph.Walk.map (f'.comp f) p
-- Mathlib.SetTheory.Cardinal.Aleph
/-- The `omega` function gives the infinite initial ordinals listed by their ordinal index.
`omega 0 = ω`, `omega 1 = ω₁` is the first uncountable ordinal, and so on.

This is not to be confused with the first infinite ordinal `Ordinal.omega0`.

For a version including finite ordinals, see `Ordinal.preOmega`. 

Conventions for notations in identifiers:

 * The recommended spelling of `ω_` in identifiers is `omega`. -/
Ordinal.termω_ : Lean.ParserDescr
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.CompletionClientCapabilities : Type
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.mem_map_of_mem : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) {S : Subsemigroup M} {x : M},
  x ∈ S → f x ∈ Subsemigroup.map f S
-- Mathlib.Tactic.FunProp.Elab
_private.Mathlib.Tactic.FunProp.Elab.0.Mathlib.Meta.FunProp.instEvalExprConfig : Lean.Elab.ConfigEval.EvalExpr Mathlib.Meta.FunProp.Config
-- Mathlib.RingTheory.Norm.Basic
/-- Given `pb : PowerBasis K S`, then the norm of `pb.gen` is
`(-1) ^ pb.dim * coeff (minpoly K pb.gen) 0`.  -/
Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (pb : PowerBasis R S),
  (Algebra.norm R) pb.gen = (-1) ^ pb.dim * (minpoly R pb.gen).coeff 0
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDeriv_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {x v : E}
  {c : 𝕜}, lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v
-- Mathlib.Data.Set.Finite.Lattice
iSup_iInf_of_monotone : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [inst : Preorder ι'] [Nonempty ι'] [IsDirectedOrder ι']
  [inst_3 : Order.Frame α] {f : ι → ι' → α}, (∀ (i : ι), Monotone (f i)) → ⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.prod_mul_prod : ∀ {𝕜 : Type u_2} {α : Type u_5} {β : Type u_6} [inst : CommRing 𝕜] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : LocallyFiniteOrder β] [inst_5 : DecidableLE (α × β)]
  (f₁ f₂ : IncidenceAlgebra 𝕜 α) (g₁ g₂ : IncidenceAlgebra 𝕜 β), f₁.prod g₁ * f₂.prod g₂ = (f₁ * f₂).prod (g₁ * g₂)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- Composition as a semigroup homomorphism.  -/
CompactlySupportedContinuousMap.compMulHom : {β : Type u_3} →
  {γ : Type u_4} →
    {δ : Type u_5} →
      [inst : TopologicalSpace β] →
        [inst_1 : TopologicalSpace γ] →
          [inst_2 : TopologicalSpace δ] →
            [inst_3 : MulZeroClass δ] →
              [inst_4 : ContinuousMul δ] →
                CocompactMap β γ → CompactlySupportedContinuousMap γ δ →ₙ* CompactlySupportedContinuousMap β δ
-- Mathlib.RingTheory.PowerSeries.Order
/-- If the order of a formal power series is finite,
then the coefficient indexed by the order is nonzero.  -/
PowerSeries.coeff_order : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R}, φ ≠ 0 → (PowerSeries.coeff φ.order.toNat) φ ≠ 0
-- Mathlib.RingTheory.GradedAlgebra.TensorProduct
GradedAlgHom.liftEquiv_symm_apply : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} [inst : DecidableEq ι]
  [inst_1 : AddMonoid ι] [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Semiring A] [inst_5 : Semiring B]
  [inst_6 : Algebra R A] [inst_7 : Algebra S B] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule S B}
  [inst_8 : GradedAlgebra 𝒜] [inst_9 : GradedAlgebra ℬ] [inst_10 : Algebra R S] [inst_11 : Algebra R B]
  [inst_12 : IsScalarTower R S B] (f : (fun x => Submodule.baseChange S (𝒜 x)) →ₐᵍ[S] ℬ) (x : A),
  ((GradedAlgHom.liftEquiv 𝒜 ℬ).symm f) x = f (1 ⊗ₜ[R] x)
-- Init.Data.SInt.Lemmas
ISize.le_maxValue : ∀ (a : ISize), a ≤ ISize.maxValue
-- Std.Data.DTreeMap.Internal.Def
Std.DTreeMap.Internal.Impl.brecOn.go : {α : Type u} →
  {β : α → Type v} →
    {motive : Std.DTreeMap.Internal.Impl α β → Sort u_1} →
      (t : Std.DTreeMap.Internal.Impl α β) →
        ((t : Std.DTreeMap.Internal.Impl α β) → Std.DTreeMap.Internal.Impl.below t → motive t) →
          motive t ×' Std.DTreeMap.Internal.Impl.below t
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- A pointed cone `C` is a face of itself.  -/
PointedCone.IsFaceOf.refl : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (C : PointedCone R M), C.IsFaceOf C
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.minKeyD_modify_eq_minKeyD : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k : α} {f : β → β} {fallback : α}, (Std.DTreeMap.Raw.Const.modify t k f).minKeyD fallback = t.minKeyD fallback
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctorZero_eq : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ = CochainComplex.shiftFunctorZero' C 0 ⋯
-- Mathlib.Algebra.Order.Sub.Basic
AddLECancellable.tsub_lt_self : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b : α}, AddLECancellable a → 0 < a → 0 < b → a - b < a
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.cancelBaseChangeAux.eq_1 : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (A : Type u_8)
  (B : Type u_9) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B] (M : Type u_10) [inst_12 : AddCommGroup M] [inst_13 : Module R M]
  [inst_14 : Module A M] [inst_15 : IsScalarTower R A M],
  Algebra.IsPushout.cancelBaseChangeAux R S A B M =
    (((LinearEquiv.restrictScalars R
                  (TensorProduct.AlgebraTensorModule.congr (↑(Algebra.IsPushout.equiv R A S B)).symm
                    (LinearEquiv.refl A M))).trans
              (LinearEquiv.restrictScalars R (TensorProduct.comm A (TensorProduct R A S) M))).trans
          (LinearEquiv.restrictScalars R (TensorProduct.AlgebraTensorModule.cancelBaseChange R A A M S))).trans
      (LinearEquiv.restrictScalars R (TensorProduct.comm R M S))
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.coe_toSubsemiring : ∀ {R : Type v} [inst : NonAssocSemiring R] [inst_1 : StarRing R] (S : StarSubsemiring R), ↑S.toSubsemiring = ↑S
-- Mathlib.Algebra.BigOperators.Group.Finset.Preimage
Finset.prod_preimage : ∀ {ι : Type u_1} {κ : Type u_2} {β : Type u_3} [inst : CommMonoid β] (f : ι → κ) (s : Finset κ)
  (hf : Set.InjOn f (f ⁻¹' ↑s)) (g : κ → β),
  (∀ x ∈ s, x ∉ Set.range f → g x = 1) → ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s, g x
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of a non-trivial group is one more than its quotient by the center  -/
Group.nilpotencyClass_eq_quotient_center_plus_one : ∀ {G : Type u_1} [inst : Group G] [hH : Group.IsNilpotent G] [Nontrivial G],
  Group.nilpotencyClass G = Group.nilpotencyClass (G ⧸ Subgroup.center G) + 1
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.constVAdd_nsmul : ∀ (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (n : ℕ) (v : V₁), AffineEquiv.constVAdd k P₁ (n • v) = AffineEquiv.constVAdd k P₁ v ^ n
-- Std.Sync.SharedMutex
/-- Unlocks a `BaseSharedMutex` read lock.

The current thread must have already locked the mutex for read access.
Unlocking an unlocked mutex is undefined behavior (inherited from the C++ implementation).
 -/
Std.BaseSharedMutex.unlockRead : Std.BaseSharedMutex → BaseIO Unit
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.embDomain_coeff : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : PartialOrder Γ']
  {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {a : Γ}, (HahnSeries.embDomain f x).coeff (f a) = x.coeff a
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.instMkEvalWhiskerRightBicategoryM : Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight Mathlib.Tactic.Bicategory.BicategoryM
-- Mathlib.Topology.Algebra.FilterBasis
RingFilterBasis.mul' : ∀ {R : Type u} {inst : Ring R} [self : RingFilterBasis R] {U : Set R}, U ∈ self.sets → ∃ V ∈ self.sets, V * V ⊆ U
-- Mathlib.Tactic.Determinant.Bird.Meta
/-- Parse an array literal into an array of element expressions.

Compared to `getArrayLit?`, this also performs `whnf`.
 -/
Mathlib.Tactic.Determinant.arrayLiteral? : Lean.Expr → Lean.MetaM (Option (Array Lean.Expr))
-- Mathlib.Order.Heyting.Basic
sup_hnot_self : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), a ⊔ ￢a = ⊤
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.map_counit_comp_comul_right : ∀ {R : Type u_1} {M : Type u_3} {M' : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] [inst_5 : Coalgebra R M] (f : M →ₗ[R] M'),
  TensorProduct.map f CoalgebraStruct.counit ∘ₗ CoalgebraStruct.comul =
    TensorProduct.map f LinearMap.id ∘ₗ ↑(TensorProduct.rid R M).symm
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.of.eq_1 : ∀ {M : Type u_1}, ArchimedeanOrder.of = Equiv.refl M
-- Init.Data.SInt.Lemmas
Int64.toBitVec_toISize : ∀ (x : Int64), x.toISize.toBitVec = BitVec.signExtend System.Platform.numBits x.toBitVec
-- Mathlib.Data.Finset.Sups
Set.Sized.compls : ∀ {α : Type u_4} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {n : ℕ},
  Set.Sized n ↑𝒜 → Set.Sized (Fintype.card α - n) ↑𝒜.compls
-- Mathlib.FieldTheory.NormalizedTrace
/-- The normalized trace transfers via (injective) maps.  -/
Algebra.normalizedTrace_map : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] [inst_3 : CharZero F]
  [inst_4 : Algebra.IsIntegral F K] {E : Type u_3} [inst_5 : Field E] [inst_6 : Algebra F E]
  [inst_7 : Algebra.IsIntegral F E] (f : E →ₐ[F] K) (a : E),
  (Algebra.normalizedTrace F K) (f a) = (Algebra.normalizedTrace F E) a
-- Init.Data.String.Subslice
String.Slice.Subslice.mk : {s : String.Slice} → (startInclusive endExclusive : s.Pos) → startInclusive ≤ endExclusive → s.Subslice
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- If `f` is a regular epi, then every morphism `k : X ⟶ W` coequalizing `RegularEpi.left` and
`RegularEpi.right` induces `l : Y ⟶ W` such that `f ≫ l = k`.  -/
CategoryTheory.RegularEpi.desc' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y W : C} →
      {f : X ⟶ Y} →
        (hf : CategoryTheory.RegularEpi f) →
          (k : X ⟶ W) →
            CategoryTheory.CategoryStruct.comp hf.left k = CategoryTheory.CategoryStruct.comp hf.right k →
              { l // CategoryTheory.CategoryStruct.comp f l = k }
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.head : ∀ {n : ℕ}, Nat.Primrec' List.Vector.head
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.WithTop.completeLattice.eq_1 : ∀ {α : Type u_5} [inst : ConditionallyCompleteLattice α],
  WithBot.WithTop.completeLattice =
    { toLattice := WithBot.lattice, toSupSet := WithBot.instSupSet, isLUB_sSup := ⋯, toInfSet := WithBot.instInfSet,
      isGLB_sInf := ⋯, toBoundedOrder := WithBot.instBoundedOrder }
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
/-- The `𝕜`-incidence algebra over `α`.  -/
IncidenceAlgebra : (𝕜 : Type u_7) → (α : Type u_8) → [Zero 𝕜] → [LE α] → Type (max u_7 u_8)
-- Std.Internal.Do.ExceptPost
/-- A cons cell pairing a head exception postcondition type `eh` with a tail `et`.

For a monad with exception type `ε` over lattice `l`, the head `eh` is typically `ε → l`
and the tail `et` tracks remaining exception layers.  -/
Std.Internal.Do.EPost.Cons : Type u → Type v → Type (max u v)
-- Mathlib.RingTheory.DividedPowers.Padic
PadicInt.coe_dpow_eq : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (x : ℤ_[p]),
  ↑((PadicInt.dividedPowers p).dpow n x) = if x_1 : x ∈ Ideal.span {↑p} then Ring.inverse ↑n.factorial * ↑x ^ n else 0
-- Init.Data.Range.Polymorphic.SInt
Int64.instRxcLawfulHasSize : Std.Rxc.LawfulHasSize Int64
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.comp_continuous_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {γ : Type u_3}
  [inst_2 : TopologicalSpace γ] (h : α ≃ᵢ β) {f : γ → α}, Continuous (⇑h ∘ f) ↔ Continuous f
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a : α}, m.contains a = false → m.get? a = none
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.instInhabited : {q : ℕ} → Inhabited (LucasLehmer.X q)
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.prime_X_sub_C : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] (r : R), Prime (Polynomial.X - Polynomial.C r)
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedRequestID.default : Lean.JsonRpc.RequestID
-- Init.Data.Option.Lemmas
Option.pmap_eq_some_iff : ∀ {α : Type u_1} {β : Type u_2} {b : β} {p : α → Prop} {f : (a : α) → p a → β} {o : Option α}
  {h : ∀ (a : α), o = some a → p a}, Option.pmap f o h = some b ↔ ∃ a, ∃ (h : p a), o = some a ∧ b = f a h
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.const.match_1.eq_1 : ∀ (motive : (x : ℕ) → TypeVec.{u_1} x → Fin2 x → Sort u_2) (n : ℕ) (α : TypeVec.{u_1} n.succ) (a : Fin2 n)
  (h_1 : (n : ℕ) → (α : TypeVec.{u_1} n.succ) → (a : Fin2 n) → motive n.succ α a.fs)
  (h_2 : (n : ℕ) → (x : TypeVec.{u_1} n.succ) → motive n.succ x Fin2.fz),
  (match n.succ, α, a.fs with
    | n.succ, α, a.fs => h_1 n α a
    | n.succ, x, Fin2.fz => h_2 n x) =
    h_1 n α a
-- Mathlib.RingTheory.Norm.Defs
Algebra.norm_apply : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (x : S),
  (Algebra.norm R) x = LinearMap.det ((Algebra.lmul R S) x)
-- Init.Data.String.Basic
String.Pos.le_trans : ∀ {s : String} {p q r : s.Pos}, p ≤ q → q ≤ r → p ≤ r
-- Init.Data.Iterators.Basic
Std.Iter.IsPlausibleIndirectSuccessorOf.below : {α β : Type w} →
  [inst : Std.Iterator α Id β] →
    {a : Std.Iter β} →
      {motive : (a_1 : Std.Iter β) → a.IsPlausibleIndirectSuccessorOf a_1 → Prop} →
        {a_1 : Std.Iter β} → a.IsPlausibleIndirectSuccessorOf a_1 → Prop
-- Mathlib.Algebra.Algebra.Opposite
MulOpposite.instAlgebra : {R : Type u_1} → {A : Type u_3} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Algebra R Aᵐᵒᵖ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.equiv_some_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {P : Fin 3 → F}, P 2 ≠ 0 → P ≈ ![P 0 / P 2, P 1 / P 2, 1]