mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Module.RCLike.Extend
/-- **Alias** of `StrongDual.norm_extendRCLike`. -/
ContinuousLinearMap.norm_extendTo𝕜 : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F), ‖fr.extendRCLike‖ = ‖fr‖
-- Init.Tactics
/-- The tactic `nomatch h` is shorthand for `exact nomatch h`.
 -/
Lean.Parser.Tactic.«tacticNomatch_,,» : Lean.ParserDescr
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_subset_Ico_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioo a b ⊆ Set.Ico a b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∪ t₂).getKey! k = t₂.getKey! k
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.lieSpan_mono : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {s t : Set M},
  s ⊆ t → LieSubmodule.lieSpan R L s ≤ LieSubmodule.lieSpan R L t
-- Mathlib.Analysis.ODE.Basic
/-- `IsIntegralCurve γ v` means `γ : ℝ → E` is a global integral curve of `v`. That is, `γ t` is
tangent to `v t (γ t)` for all `t : ℝ`.  -/
IsIntegralCurve : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → (ℝ → E) → (ℝ → E → E) → Prop
-- Mathlib.Algebra.Homology.CochainComplexOpposite
CochainComplex.homotopyOp_hom_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {f g : K ⟶ L} (h : Homotopy f g) (p q p' q' : ℤ)
  (hp : autoParam (p + p' = 0) CochainComplex.homotopyOp_hom_eq._auto_1)
  (hq : autoParam (q + q' = 0) CochainComplex.homotopyOp_hom_eq._auto_3),
  (CochainComplex.homotopyOp h).hom p q =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq L ⋯).hom.op
      (CategoryTheory.CategoryStruct.comp (h.hom q' p').op (HomologicalComplex.XIsoOfEq K ⋯).hom.op)
-- Init.Data.SInt.Lemmas
Int16.toBitVec_ofNat' : ∀ {n : ℕ}, (Int16.ofNat n).toBitVec = BitVec.ofNat 16 n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits.0.CategoryTheory.WithTerminal.map.match_1.eq_3 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithTerminal C) → (X ⟶ Y) → Sort u_3)
  (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star)
  (h_1 :
    (a a_1 : C) →
      (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_1) →
        motive (CategoryTheory.WithTerminal.of a) (CategoryTheory.WithTerminal.of a_1) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of a) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f => h_1 a a_1 f
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x => h_2 a x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_3 x
-- Mathlib.Data.Fintype.EquivFin
Sum.infinite_of_left : ∀ {α : Type u_1} {β : Type u_2} [Infinite α], Infinite (α ⊕ β)
-- Mathlib.Control.Monad.Basic
/-- run a `StateT` program and discard the final state  -/
StateT.eval : {α σ : Type u} → {m : Type u → Type v} → [Functor m] → StateT σ m α → σ → m α
-- Mathlib.Data.Nat.Dist
Nat.dist.eq_1 : ∀ (n m : ℕ), n.dist m = n - m + (m - n)
-- Mathlib.Algebra.Order.Floor.Ring
Int.map_ceil : ∀ {F : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : Ring S]
  [inst_3 : LinearOrder S] [inst_4 : FloorRing R] [inst_5 : FloorRing S] [inst_6 : FunLike F R S] [RingHomClass F R S]
  (f : F), StrictMono ⇑f → ∀ (a : R), ⌈f a⌉ = ⌈a⌉
-- Mathlib.Order.GaloisConnection.Basic
GaloisCoinsertion.u_inf_l : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β]
  (gi : GaloisCoinsertion l u) (a b : β), u (l a ⊓ l b) = a ⊓ b
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.maxEntry?_eq_minEntry? : ∀ {α : Type u} {β : α → Type v} [o : Ord α] [«to» : Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered → t.maxEntry? = Std.Internal.List.minEntry? t.toListModel
-- Mathlib.Logic.Equiv.Prod
/-- Any `Unique` type is a left identity for type product up to equivalence.  -/
Equiv.uniqueProd : (α : Type u_9) → (β : Type u_10) → [Unique β] → β × α ≃ α
-- Mathlib.CategoryTheory.Shift.Twist
CategoryTheory.TwistShiftData.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] [inst_3 : SizeOf C] [inst_4 : SizeOf A]
  (z : A → A → (CategoryTheory.CatCenter C)ˣ)
  (z_zero_zero : autoParam (z 0 0 = 1) CategoryTheory.TwistShiftData.z_zero_zero._autoParam)
  (assoc :
    autoParam (∀ (a b c : A), z (a + b) c * z a b = z a (b + c) * z b c) CategoryTheory.TwistShiftData.assoc._autoParam)
  (commShift :
    autoParam (∀ (a b : A), CategoryTheory.NatTrans.CommShift (↑(z a b)) A)
      CategoryTheory.TwistShiftData.commShift._autoParam),
  sizeOf { z := z, z_zero_zero := z_zero_zero, assoc := assoc, commShift := commShift } = 1 + sizeOf z_zero_zero
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Composition on the left by a (continuous) homomorphism of topological `R`-algebras, as an
`AlgHom`. Similar to `AlgHom.compLeft`.  -/
AlgHom.compLeftContinuous : (R : Type u_2) →
  [inst : CommSemiring R] →
    {A : Type u_3} →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : Semiring A] →
          [inst_3 : Algebra R A] →
            [inst_4 : IsTopologicalSemiring A] →
              {A₂ : Type u_4} →
                [inst_5 : TopologicalSpace A₂] →
                  [inst_6 : Semiring A₂] →
                    [inst_7 : Algebra R A₂] →
                      [inst_8 : IsTopologicalSemiring A₂] →
                        {α : Type u_5} →
                          [inst_9 : TopologicalSpace α] → (g : A →ₐ[R] A₂) → Continuous ⇑g → C(α, A) →ₐ[R] C(α, A₂)
-- Lean.Meta.ArgsPacker
/-- Given unary expressions `e₁`, `e₂` with types `(x : A) → R₁[x]`
and `(z : C) → R₂[z]`, returns an expression of type
```
(x : A ⊕' C) → (match x with | .inl x => R₁[x] | .inr R₂[z])
```
 -/
Lean.Meta.ArgsPacker.Mutual.uncurryWithType : Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.semigroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : Semigroup M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (mul : ∀ (x y : M₁), f (x * y) = f x * f y), Function.Injective.semigroup f hf mul = { toMul := inst, mul_assoc := ⋯ }
-- Init.Prelude
Inhabited.mk : {α : Sort u} → α → Inhabited α
-- Mathlib.Order.PiLex
Pi.instLTColexForall : {ι : Type u_1} → {β : ι → Type u_2} → [LT ι] → [(a : ι) → LT (β a)] → LT (Colex ((i : ι) → β i))
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalClosure_subset_iff : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G} {N : AddSubgroup G} [N.Normal],
  s ⊆ ↑N ↔ AddSubgroup.normalClosure s ≤ N
-- Lean.Expr
Lean.mkConstEx : Lean.Name → List Lean.Level → Lean.Expr
-- Mathlib.Algebra.Group.Fin.Basic
Fin.coe_sub_one : ∀ {n : ℕ} (a : Fin (n + 1)), ↑(a - 1) = if a = 0 then n else ↑a - 1
-- Mathlib.Data.Finset.Empty
Finset.Nonempty.mono : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → s.Nonempty → t.Nonempty
-- Lean.Elab.Tactic.Location
Lean.Elab.Tactic.Location.targets.injEq : ∀ (hypotheses : Array Lean.Syntax) (type : Bool) (hypotheses_1 : Array Lean.Syntax) (type_1 : Bool),
  (Lean.Elab.Tactic.Location.targets hypotheses type = Lean.Elab.Tactic.Location.targets hypotheses_1 type_1) =
    (hypotheses = hypotheses_1 ∧ type = type_1)
-- Mathlib.CategoryTheory.Galois.Basic
/-- Coproduct inclusions are monic in Galois categories.  -/
CategoryTheory.PreGaloisCategory.instMonoCoprod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C],
  CategoryTheory.Limits.MonoCoprod C
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instSemilatticeSupFiniteIndexNormalSubgroup.eq_1 : ∀ {G : Type u_1} [inst : Group G],
  FiniteIndexNormalSubgroup.instSemilatticeSupFiniteIndexNormalSubgroup =
    Function.Injective.semilatticeSup (fun H => H.toSubgroup) ⋯ ⋯ ⋯ ⋯
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.instAdditiveModuleCatCarrierObjOppositeRingCatEvaluation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (X : Cᵒᵖ),
  (PresheafOfModules.evaluation R X).Additive
-- Init.Data.UInt.Bitwise
UInt8.ofBitVec_shiftLeft : ∀ (a : BitVec 8), ∀ b < 8, { toBitVec := a <<< b } = { toBitVec := a } <<< UInt8.ofNat b
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.forall_coe_one_iff_one : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : One β]
  (f : BoundedContinuousFunction α β), (∀ (x : α), f x = 1) ↔ f = 1
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₂Unchecked : UInt8 → UInt8 → UInt32
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.integral_eq_tsum_of_ac : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α]
  [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} [inst_7 : NormedSpace ℝ E],
  MeasureTheory.IsFundamentalDomain G s μ →
    ν.AbsolutelyContinuous μ →
      ∀ (f : α → E), MeasureTheory.Integrable f ν → ∫ (x : α), f x ∂ν = ∑' (g : G), ∫ (x : α) in g • s, f x ∂ν
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanImportKind : Lean.FromJson Lean.Lsp.LeanImportKind
-- Mathlib.InformationTheory.Hamming
hammingDist.eq_1 : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] (x y : (i : ι) → β i),
  hammingDist x y = {i | x i ≠ y i}.card
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.derivedSeries_of_derivedLength_succ : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  (k : ℕ),
  LieAlgebra.derivedLengthOfIdeal R L I = k + 1 ↔
    IsLieAbelian ↥(LieAlgebra.derivedSeriesOfIdeal R L k I) ∧ LieAlgebra.derivedSeriesOfIdeal R L k I ≠ ⊥
-- Mathlib.Algebra.WithConv
WithConv.ofConv_smul : ∀ {R : Type u_1} {A : Type u_2} [inst : Monoid R] [inst_1 : MulAction R A] (c : R) (x : WithConv A),
  (c • x).ofConv = c • x.ofConv
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.comap_strictMono_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N},
  Function.Surjective ⇑f → StrictMono (Subsemigroup.comap f)
-- Mathlib.Geometry.Manifold.ChartedSpace
achart_val : ∀ (H : Type u) {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (x : M), ↑(achart H x) = chartAt H x
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- `charFun` is a Fourier integral for the inner product and the character `fourierChar`.  -/
MeasureTheory.charFun_eq_fourierIntegral' : ∀ {E : Type u_2} {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [inst : SeminormedAddCommGroup E]
  [inst_1 : InnerProductSpace ℝ E] (t : E),
  MeasureTheory.charFun μ t = VectorFourier.fourierIntegral Real.fourierChar μ (innerₗ E) 1 (-(2 * Real.pi)⁻¹ • t)
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.equalizerSieve_mem_of_equalizerSieve_app_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] (J : CategoryTheory.GrothendieckTopology C)
  {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) {X : Cᵒᵖ} (x y : CategoryTheory.ToType (F₁.obj X)),
  CategoryTheory.Presheaf.equalizerSieve ((CategoryTheory.ConcreteCategory.hom (φ.app X)) x)
        ((CategoryTheory.ConcreteCategory.hom (φ.app X)) y) ∈
      J (Opposite.unop X) →
    ∀ [CategoryTheory.Presheaf.IsLocallyInjective J φ], CategoryTheory.Presheaf.equalizerSieve x y ∈ J (Opposite.unop X)
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.instLineDerivLeftSMulReal : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F], LineDerivLeftSMul ℝ E (TemperedDistribution E F) (TemperedDistribution E F)
-- Mathlib.RepresentationTheory.Basic
/-- Given representations of `G` on a family `V i` indexed by `i`, there is a
natural representation of `G` on their direct sum `⨁ i, V i`.
 -/
Representation.directSum : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Semiring k] →
      [inst_1 : Monoid G] →
        {ι : Type u_3} →
          {V : ι → Type u_4} →
            [inst_2 : (i : ι) → AddCommMonoid (V i)] →
              [inst_3 : (i : ι) → Module k (V i)] →
                ((i : ι) → Representation k G (V i)) → Representation k G (DirectSum ι fun i => V i)
-- Mathlib.Analysis.LocallyConvex.WeakDual
/-- Construct a family of seminorms from a bilinear form.  -/
LinearMap.toSeminormFamily : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NormedField 𝕜] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : AddCommGroup F] → [inst_4 : Module 𝕜 F] → (E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) → SeminormFamily 𝕜 E F
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconePrecompose_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F G : CategoryTheory.Functor J C} {α : G ⟶ F} {c : CategoryTheory.Limits.Cocone F},
  H.mapCoconePrecompose.inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
-- Lean.Message
Lean.MessageLog.hasUnreported : Lean.MessageLog → Bool
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_apply_univ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel (α × β) γ}
  [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsMarkovKernel η] {a : α},
  ((κ.compProd η) a) Set.univ = (κ a) Set.univ
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instSubtractionMonoidOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : SubtractionMonoid Mᵃᵒᵖ], DomAddAct.instSubtractionMonoidOfAddOpposite = inst
-- Std.Data.ExtTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the largest key that is
less than the given key.
 -/
Std.ExtTreeMap.getKeyLT : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [inst : Std.TransCmp cmp] → (t : Std.ExtTreeMap α β cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.lt) → α
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
MeasureTheory.lintegral_strict_mono_of_ae_le_of_ae_lt_on : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  AEMeasurable g μ →
    ∫⁻ (x : α), f x ∂μ ≠ ⊤ →
      f ≤ᵐ[μ] g → ∀ {s : Set α}, μ s ≠ 0 → (∀ᵐ (x : α) ∂μ, x ∈ s → f x < g x) → ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ
-- Mathlib.Combinatorics.Graph.Basic
/-- `G.IsLoopAt e x` means that both ends of the edge `e` are equal to the vertex `x`.  -/
Graph.IsLoopAt : {α : Type u_1} → {β : Type u_2} → Graph α β → β → α → Prop
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.MIntl.inhabited : (F : PFunctor.{uA, uB}) → [Inhabited F.A] → Inhabited F.MIntl
-- Mathlib.Tactic.Simps.Basic
/-- will simp lemmas be generated for with (without specifically naming this?)  -/
Simps.ParsedProjectionData.isDefault : Simps.ParsedProjectionData → Bool
-- Lean.CoreM
/-- Name generator for creating persistent auxiliary declarations. Separate from `ngen` to keep
numbers smaller and create user-accessible names.
 -/
Lean.Core.State.auxDeclNGen : Lean.Core.State → Lean.DeclNameGenerator
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime : ∀ {p : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [hcycl : IsCyclotomicExtension {p} ℚ K], IsPrimitiveRoot ζ p → IsIntegralClosure ↥ℤ[ζ] ℤ K
-- Mathlib.Topology.Spectral.Hom
SpectralMap.instInhabited : (α : Type u_2) → [inst : TopologicalSpace α] → Inhabited (SpectralMap α α)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
/-- The ancestrality relation on the index type of `h : A.PairingCore`.  -/
SSet.Subcomplex.PairingCore.AncestralRel : {X : SSet} → {A : X.Subcomplex} → (h : A.PairingCore) → h.ι → h.ι → Prop
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry!_cons_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k}
  [inst_2 : Inhabited ((a : α) × β a)], Std.Internal.List.getEntry! k (⟨k, v⟩ :: l) = ⟨k, v⟩
-- Mathlib.Topology.Algebra.RestrictedProduct.Units
RestrictedProduct.eventually_isUnit_of_isUnit : ∀ {ι : Type u_1} {R : ι → Type u_2} [inst : (i : ι) → Monoid (R i)] {S : ι → Type u_3}
  [inst_1 : (i : ι) → SetLike (S i) (R i)] [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i}
  {𝓕 : Filter ι} {x : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕},
  IsUnit x → (∀ (i : ι), IsUnit (x i)) ∧ ∀ᶠ (i : ι) in 𝓕, ∃ (h : x i ∈ B i), IsUnit ⟨x i, h⟩
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_counitIso_inv_app : ∀ (X : CategoryTheory.Limits.WalkingParallelPair),
  CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.counitIso.inv.app X = CategoryTheory.eqToHom ⋯
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableOn.sub_iff_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {s : Set E}, DifferentiableOn 𝕜 f s → (DifferentiableOn 𝕜 (f - g) s ↔ DifferentiableOn 𝕜 g s)
-- Mathlib.Analysis.Normed.Module.Basic
/-- Produces a `PseudoMetricSpace E` instance from a `SeminormedSpace.Core`. Note that
if this is used to define an instance on a type, it also provides a new uniformity and
topology on the type. See note [reducible non-instances].  -/
PseudoMetricSpace.ofSeminormedSpaceCore : {𝕜 : Type u_6} →
  {E : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Norm E] → [inst_3 : Module 𝕜 E] → SeminormedSpace.Core 𝕜 E → PseudoMetricSpace E
-- Lean.Level
Lean.LevelSet : Type
-- Init.Data.Array.Lemmas
Array.getElem?_setIfInBounds_ne : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ}, i ≠ j → ∀ {a : α}, (xs.setIfInBounds i a)[j]? = xs[j]?
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsKolmogorovProcess.edist_eq_zero : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E},
  ProbabilityTheory.IsKolmogorovProcess X P p q M →
    ∀ {s t : T}, edist s t = 0 → ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.changeInverse_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G), (e.changeInverse iso).functor = e.functor
-- Init.Data.Array.MapIdx
Array.mapIdx_eq_append_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : ℕ → α → β} {ys zs : Array β},
  Array.mapIdx f xs = ys ++ zs ↔
    ∃ xs' zs', xs = xs' ++ zs' ∧ Array.mapIdx f xs' = ys ∧ Array.mapIdx (fun i => f (i + xs'.size)) zs' = zs
-- Mathlib.Order.Basic
/-- **Alias** of `lt_trans`. -/
gt_trans' : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a < b → b < c → a < c
-- Mathlib.Topology.UniformSpace.Cauchy
cauchySeq_iff_tendsto : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Nonempty β] [inst : SemilatticeSup β] {u : β → α},
  CauchySeq u ↔ Filter.Tendsto (Prod.map u u) Filter.atTop (uniformity α)
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.HD_bound_aux1 : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] [Nonempty Y] (f : GromovHausdorff.Cb✝ X Y)
  (C : ℝ), BddAbove (Set.range fun x => ⨅ y, f (Sum.inl x, Sum.inr y) + C)