mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.inverts : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  [inst_1 : W.HasLeftCalculusOfFractions],
  W.IsInvertedBy (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W)
-- Mathlib.Util.FormatTable
Alignment.right.sizeOf_spec : sizeOf Alignment.right = 1
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'}
  [inst_3 : CategoryTheory.Limits.HasKernel f'] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).hom
      (CategoryTheory.Limits.kernel.map f f' sq.left sq.right ⋯) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap sq)
      (CategoryTheory.Limits.kernelSubobjectIso f').hom
-- Std.Data.ExtDTreeMap.Basic
/-- Implementation detail of the tree map  -/
Std.ExtDTreeMap.lift : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {γ : Sort w} →
        (f : Std.DTreeMap α β cmp → γ) →
          (∀ (a b : Std.DTreeMap α β cmp), a.Equiv b → f a = f b) → Std.ExtDTreeMap α β cmp → γ
-- Mathlib.AlgebraicGeometry.Artinian
/-- Spec of a field is artinian.  -/
AlgebraicGeometry.instIsArtinianSchemeOfSubsingletonCarrierCarrierCommRingCatOfIsReduced : ∀ {X : AlgebraicGeometry.Scheme} [Subsingleton ↥X] [AlgebraicGeometry.IsReduced X], AlgebraicGeometry.IsArtinianScheme X
-- Mathlib.Util.CompileInductive
/-- `compile_inductive% Foo` creates compiled code for the recursor `Foo.rec`,
so that `Foo.rec` can be used in a definition
without having to mark the definition as `noncomputable`.
 -/
Mathlib.Util.«commandCompile_inductive%_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
/-- `ToType X` converts the object `X` of the concrete category `C` to a type.

This is an `abbrev` so that instances on `X` (e.g. `Ring`) do not need to be redeclared.
 -/
CategoryTheory.ToType : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] → [CategoryTheory.ConcreteCategory C FC] → C → Type w
-- Lean.Setup
Lean.instToJsonPlugin : Lean.ToJson Lean.Plugin
-- Mathlib.Data.List.Sort
List.insertionSort.congr_simp : ∀ {α : Type u_1} (r r_1 : α → α → Prop),
  r = r_1 →
    ∀ {inst : DecidableRel r} [inst_1 : DecidableRel r_1] (a a_1 : List α),
      a = a_1 → List.insertionSort r a = List.insertionSort r_1 a_1
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry_natural_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X Y Y' : C}
  [inst_2 : CategoryTheory.Closed A] (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A X ⟶ Y) (g : Y ⟶ Y'),
  CategoryTheory.MonoidalClosed.curry (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.curry f) ((CategoryTheory.ihom A).map g)
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Finset.prod_comm : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β},
  ∏ x ∈ s, ∏ y ∈ t, f x y = ∏ y ∈ t, ∏ x ∈ s, f x y
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolAlg_sup : ∀ {α : Type u_1} [inst : BooleanRing α] (a b : AsBoolAlg α),
  ofBoolAlg (a ⊔ b) = ofBoolAlg a + ofBoolAlg b + ofBoolAlg a * ofBoolAlg b
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.toTopologicalSpace_top : ∀ {α : Type ua}, ⊤.toTopologicalSpace = ⊤
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {J : Type w} {inst_2 : CategoryTheory.Category.{w', w} J} {F : CategoryTheory.Functor C D}
  [self : CategoryTheory.Limits.PreservesColimitsOfShape J F] {K : CategoryTheory.Functor J C},
  CategoryTheory.Limits.PreservesColimit K F
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.mk_neg : ∀ {R : Type u_1} {M : Type u_2} {x : M} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (p : Submodule R M), Submodule.Quotient.mk (-x) = -Submodule.Quotient.mk x
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedAddMonoid.ext : ∀ {α : Type u_2} {M : Type u_3} [inst : AddMonoid M] (rels : FreeAddMonoid α → FreeAddMonoid α → Prop)
  {φ ψ : PresentedAddMonoid rels →+ M},
  (∀ (x : α), φ (PresentedAddMonoid.of rels x) = ψ (PresentedAddMonoid.of rels x)) → φ = ψ
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.IsTriangularizable.mk : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  (∀ (x : L), ⨆ φ, ((LieModule.toEnd R L M) x).maxGenEigenspace φ = ⊤) → LieModule.IsTriangularizable R L M
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter' : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g : M → M'} {s t : Set M} {x : M},
  G.LocalInvariantProp G' P →
    t ∈ nhdsWithin x s → (ChartedSpace.LiftPropWithinAt P g (s ∩ t) x ↔ ChartedSpace.LiftPropWithinAt P g s x)
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- Outside the usual range of `binEntropy`, it is negative. This is due to `log p = log |p|`  -/
Real.binEntropy_nonpos_of_one_le : ∀ {p : ℝ}, 1 ≤ p → Real.binEntropy p ≤ 0
-- Mathlib.Algebra.Ring.Defs
NonAssocCommSemiring.mk : {α : Type u} → [toNonAssocSemiring : NonAssocSemiring α] → (∀ (a b : α), a * b = b * a) → NonAssocCommSemiring α
-- Mathlib.RingTheory.FreeCommRing
FreeRing.coe_mul : ∀ {α : Type u} (x y : FreeRing α), ↑(x * y) = ↑x * ↑y
-- Std.Data.ExtHashSet.Lemmas
/-- This is a restatement of `mem_insert` that is written to exactly match the proof obligation
in the statement of `get_insert`.  -/
Std.ExtHashSet.mem_of_mem_insert' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a : α}, a ∈ m.insert k → ¬((k == a) = true ∧ k ∉ m) → a ∈ m
-- Std.Data.ExtDTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key.  -/
Std.ExtDTreeMap.entryAtIdx : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → (t : Std.ExtDTreeMap α β cmp) → (n : ℕ) → n < t.size → (a : α) × β a
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.eq.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr},
  Lean.Meta.Grind.Arith.Cutsat.UnsatProof.eq c = Lean.Meta.Grind.Arith.Cutsat.UnsatProof.eq c_1 → c = c_1
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
map_preNormEDS' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {F : Type u_3} [inst_2 : FunLike F R S]
  [RingHomClass F R S] (f : F) (b c d : R) (n : ℕ), f (preNormEDS' b c d n) = preNormEDS' (f b) (f c) (f d) n
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.IsNontrivial.exists_abv_lt_one : ∀ {R : Type u_3} {S : Type u_4} [inst : Field R] [inst_1 : Semifield S] [inst_2 : LinearOrder S] [IsStrictOrderedRing S]
  [ExistsAddOfLE S] {v : AbsoluteValue R S}, v.IsNontrivial → ∃ x, x ≠ 0 ∧ v x < 1
-- Init.Data.String.Lemmas.Order
String.Pos.offset_le_rawEndPos : ∀ {s : String} {p : s.Pos}, p.offset ≤ s.rawEndPos
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimit_map_colimitObjIsoColimitCompEvaluation_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) {i j : K} (f : i ⟶ j) {Z : C}
  (h : CategoryTheory.Limits.colimit (F.comp ((CategoryTheory.evaluation K C).obj j)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit F).map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F j).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F i).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.colimMap (F.whiskerLeft ((CategoryTheory.evaluation K C).map f))) h)
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.addMonoidHomCongrLeftEquiv_apply : ∀ {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [inst : AddZeroClass M₁] [inst_1 : AddZeroClass M₂]
  [inst_2 : AddMonoid N] (e : M₁ ≃+ M₂) (f : M₁ →+ N), e.addMonoidHomCongrLeftEquiv f = f.comp e.symm.toAddMonoidHom
-- Mathlib.CategoryTheory.Monad.Algebra
/-- A morphism of Eilenberg-Moore coalgebras for the comonad `G`.  -/
CategoryTheory.Comonad.Coalgebra.Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {G : CategoryTheory.Comonad C} → G.Coalgebra → G.Coalgebra → Type v₁
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
_private.Mathlib.Combinatorics.SimpleGraph.CycleGraph.0.SimpleGraph.cycleGraph.cycleCons : (n : ℕ) → (m : Fin (n + 3)) → (SimpleGraph.cycleGraph (n + 3)).Walk m 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.length_toList : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.toList.length = m.size
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_eq_iff_sup_ker_eq_of_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {I J : Ideal R} (f : R →+* S),
  Function.Surjective ⇑f → (Ideal.map f I = Ideal.map f J ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f)
-- Mathlib.NumberTheory.Cyclotomic.Gal
/-- Maps `μ` to the `AlgEquiv` that sends `IsCyclotomicExtension.zeta` to `μ`.  -/
IsCyclotomicExtension.fromZetaAut : {n : ℕ} →
  [NeZero n] →
    {K : Type u_1} →
      [inst : Field K] →
        {L : Type u_2} →
          {μ : L} →
            [inst_1 : CommRing L] →
              [IsDomain L] →
                IsPrimitiveRoot μ n →
                  [inst_3 : Algebra K L] →
                    [IsCyclotomicExtension {n} K L] → Irreducible (Polynomial.cyclotomic n K) → L ≃ₐ[K] L
-- Mathlib.Algebra.Group.Equiv.Basic
/-- Negation on an `AddGroup` is a permutation of the underlying type.  -/
Equiv.neg : (G : Type u_14) → [InvolutiveNeg G] → Equiv.Perm G
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.LocalizerMorphism.commShift_iso_hom_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {M : Type u_3}
  [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C₁ M] [inst_4 : CategoryTheory.HasShift C₂ M]
  [inst_5 : Φ.functor.CommShift M] {D₁ : Type u_4} {D₂ : Type u_5} [inst_6 : CategoryTheory.Category.{v_3, u_4} D₁]
  [inst_7 : CategoryTheory.Category.{v_4, u_5} D₂] (L₁ : CategoryTheory.Functor C₁ D₁) [inst_8 : L₁.IsLocalization W₁]
  (L₂ : CategoryTheory.Functor C₂ D₂) [inst_9 : CategoryTheory.HasShift D₁ M] [inst_10 : CategoryTheory.HasShift D₂ M]
  [inst_11 : L₁.CommShift M] [inst_12 : L₂.CommShift M] (G : CategoryTheory.Functor D₁ D₂)
  (e : Φ.functor.comp L₂ ≅ L₁.comp G) (m : M) (X : C₁),
  (CategoryTheory.Functor.commShiftIso G m).hom.app (L₁.obj X) =
    CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.Functor.commShiftIso L₁ m).inv.app X))
      (CategoryTheory.CategoryStruct.comp (e.inv.app ((CategoryTheory.shiftFunctor C₁ m).obj X))
        (CategoryTheory.CategoryStruct.comp (L₂.map ((CategoryTheory.Functor.commShiftIso Φ.functor m).hom.app X))
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso L₂ m).hom.app (Φ.functor.obj X))
            ((CategoryTheory.shiftFunctor D₂ m).map (e.hom.app X)))))
-- Mathlib.Order.Bounds.Basic
upperBounds_mono : ∀ {α : Type u_1} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → ∀ ⦃a b : α⦄, a ≤ b → a ∈ upperBounds t → b ∈ upperBounds s
-- Mathlib.FieldTheory.Relrank
IntermediateField.lift_rank_comap : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type w} [inst_3 : Field L]
  [inst_4 : Algebra F L] (A : IntermediateField F E) (f : L →ₐ[F] E),
  Cardinal.lift.{v, w} (Module.rank (↥(IntermediateField.comap f A)) L) = Cardinal.lift.{w, v} (A.relrank f.fieldRange)
-- Mathlib.Data.Multiset.Lattice
Multiset.sup_ndinsert : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] (a : α) (s : Multiset α),
  (Multiset.ndinsert a s).sup = a ⊔ s.sup
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
/-- If `N` is in perfect pairing with `M`, then it is reflexive.  -/
LinearEquiv.isReflexive_of_equiv_dual_of_isReflexive : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M),
  Module.IsReflexive R N
-- Lean.Elab.Tactic.BuiltinTactic
_private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.getCaseGoals.commaList : List Lean.MessageData → Lean.MessageData
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.π_descTruncGT : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁)
  [inst_6 : t.IsGE Y n₁], CategoryTheory.CategoryStruct.comp ((t.truncGTπ n₀).app X) (t.descTruncGT f n₀ n₁ h) = f
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.bind_apply : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] {β γ : Type v} (f : α →𝒄 Part β) (g : α →𝒄 β → Part γ) (x : α),
  (f.bind g) x = (f x).bind (g x)
-- Lean.Data.Lsp.Utf16
/-- Computes an UTF-8 offset into `text.source`
from an LSP-style 0-indexed (ln, col) position.  -/
Lean.FileMap.lspPosToUtf8Pos : Lean.FileMap → Lean.Lsp.Position → String.Pos.Raw
-- Mathlib.Analysis.Calculus.Deriv.Inv
HasDerivAt.div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'} {c' d' : 𝕜'},
  HasDerivAt c c' x → HasDerivAt d d' x → d x ≠ 0 → HasDerivAt (c / d) ((c' * d x - c x * d') / d x ^ 2) x
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.id_map_iff : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal},
  Measurable X →
    (ProbabilityTheory.Kernel.HasSubgaussianMGF id c (κ.map X) ν ↔ ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν)
-- Mathlib.Data.Finset.Basic
Finset.disjoint_of_erase_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∉ s → Disjoint s (t.erase a) → Disjoint s t
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentBundle.continuousLinearMapAt_model_space : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_8} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (b b' : F),
  Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt F (TangentSpace (modelWithCornersSelf 𝕜 F)) b) b' = 1
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_of_not_integrable : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  ¬MeasureTheory.Integrable (fun x => Real.exp (f x)) μ → μ.tilted f = 0
-- Mathlib.Topology.NhdsWithin
mem_nhdsSetWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t u : Set α}, u ∈ nhdsSetWithin s t ↔ ∃ v, IsOpen v ∧ s ⊆ v ∧ v ∩ t ⊆ u
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.regOfFamily.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ),
  NumberField.Units.regOfFamily u =
    if hu : NumberField.Units.IsMaxRank u then
      ZLattice.covolume (Submodule.span ℤ (Set.range ⇑(NumberField.Units.basisOfIsMaxRank hu))) MeasureTheory.volume
    else 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_pi : Real.cos Real.pi = -1
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
EisensteinSeries.e2Summand_zero_eq_two_riemannZeta_two : ∀ (z : UpperHalfPlane), EisensteinSeries.e2Summand 0 z = 2 * riemannZeta 2
-- Init.System.IO
IO.FS.instReprFileType : Repr IO.FS.FileType
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Node.atom.sizeOf_spec : ∀ (a : Mathlib.Tactic.Widget.StringDiagram.AtomNode),
  sizeOf (Mathlib.Tactic.Widget.StringDiagram.Node.atom a) = 1 + sizeOf a
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddAction.eq_1 : ∀ {M : Type u_1} {X : Type u_2} [inst : AddMonoid M] [inst_1 : AddAction M X] [inst_2 : TopologicalSpace X]
  [inst_3 : ContinuousConstVAdd M X],
  SeparationQuotient.instAddAction = Function.Surjective.addAction SeparationQuotient.mk ⋯ ⋯
-- Mathlib.Algebra.GCDMonoid.Basic
extract_gcd : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (x y : α),
  ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')
-- Mathlib.Topology.Separation.Basic
Continuous.isOpen_support : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [T1Space X] [inst_2 : Zero X] [inst_3 : TopologicalSpace Y]
  {f : Y → X}, Continuous f → IsOpen (Function.support f)
-- Mathlib.NumberTheory.LSeries.PrimesInAP
ArithmeticFunction.vonMangoldt.residueClass_le : ∀ {q : ℕ} (a : ZMod q) (n : ℕ), ArithmeticFunction.vonMangoldt.residueClass a n ≤ ArithmeticFunction.vonMangoldt n
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sSameSide_smul_vsub_vadd_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x p₁ p₂ : P},
  x ∉ s → p₁ ∈ s → p₂ ∈ s → ∀ {t : R}, 0 < t → s.SSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.map.eq_1 : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] (f : α → β),
  SeparationQuotient.map f = SeparationQuotient.lift' (SeparationQuotient.mk ∘ f)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.mkPiAlgebra_apply : ∀ (R : Type u) (ι : Type v) (A : Type u_1) [inst : Fintype ι] [inst_1 : CommSemiring R] [inst_2 : CommSemiring A]
  [inst_3 : Algebra R A] [inst_4 : TopologicalSpace A] [inst_5 : ContinuousMul A] (m : ι → A),
  (ContinuousMultilinearMap.mkPiAlgebra R ι A) m = ∏ i, m i
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.countPBefore.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → ℕ → Sort u_2) (head : α) (tail : List α) (s : ℕ)
  (h_1 : (head : α) → (tail : List α) → (s : ℕ) → motive (head :: tail) 0 s)
  (h_2 : (a : α) → (xs : List α) → (i s : ℕ) → motive (a :: xs) i.succ s) (h_3 : (x s : ℕ) → motive [] x s),
  (match head :: tail, 0, s with
    | head :: tail, 0, s => h_1 head tail s
    | a :: xs, i.succ, s => h_2 a xs i s
    | [], x, s => h_3 x s) =
    h_1 head tail s
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.ConeMorphism.mk : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {A B : CategoryTheory.Limits.Cone F} →
            (hom : A.pt ⟶ B.pt) →
              autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp hom (B.π.app j) = A.π.app j)
                  CategoryTheory.Limits.ConeMorphism.w._autoParam →
                CategoryTheory.Limits.ConeMorphism A B
-- Mathlib.Order.KrullDimension
Order.coheight_eq_of_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  StrictMono f →
    (∀ (a : α) (b : β), f a < b → ∃ a', a < a' ∧ f a' = b) → ∀ (a : α), Order.coheight a = Order.coheight (f a)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.assoc : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b : B} {f g h i : CategoryTheory.FreeBicategory.Hom a b} (η : CategoryTheory.FreeBicategory.Hom₂ f g)
  (θ : CategoryTheory.FreeBicategory.Hom₂ g h) (ι : CategoryTheory.FreeBicategory.Hom₂ h i),
  CategoryTheory.FreeBicategory.Rel.below ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_insertMany_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α},
  k ∈ ↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯) ↔ k ∈ t ∨ (List.map Prod.fst l).contains k = true
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.mk : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] →
                        [inst_7 : ContMDiffMul I (↑⊤) G] →
                          (toDerivation :
                              Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)
                                (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)) →
                            (∀ (g : G),
                                (hfdifferential ⋯) ((Derivation.evalAt 1) toDerivation) =
                                  (Derivation.evalAt g) toDerivation) →
                              LeftInvariantDerivation I G
-- Mathlib.Topology.Category.UniformSpace
/-- Construct a bundled `UniformSpace` from the underlying type and the appropriate typeclasses.  -/
CpltSepUniformSpace.of : (X : Type u) → [inst : UniformSpace X] → [CompleteSpace X] → [T0Space X] → CpltSepUniformSpace
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticWith.mk : {α : Type} →
  Lean.Lsp.Range →
    Option Lean.Lsp.Range →
      Option Lean.Lsp.DiagnosticSeverity →
        Option Bool →
          Option Lean.Lsp.DiagnosticCode →
            Option String →
              α →
                Option (Array Lean.Lsp.DiagnosticTag) →
                  Option (Array Lean.Lsp.LeanDiagnosticTag) →
                    Option (Array Lean.Lsp.DiagnosticRelatedInformation) → Option Lean.Json → Lean.Lsp.DiagnosticWith α
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeriesAux.eq_2 : ∀ (G : Type u_2) [inst : AddGroup G] (n : ℕ),
  AddSubgroup.upperCentralSeriesAux G n.succ = ⟨(AddSubgroup.upperCentralSeriesAux G n).fst.upperCentralSeriesStep, ⋯⟩
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.mk_neg : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G), ↑(-a) = -↑a