mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.isRoot : ∀ {R : Type u_4} [inst : CommRing R] {n : ℕ} {ζ : R}, IsPrimitiveRoot ζ n → (Polynomial.X ^ n - 1).IsRoot ζ
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.DominatedFinMeasAdditive.add_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {β : Type u_7} [inst : SeminormedAddCommGroup β] {T T' : Set α → β} {C C' : ℝ}
  (μ ν : MeasureTheory.Measure α),
  MeasureTheory.DominatedFinMeasAdditive μ T C →
    MeasureTheory.DominatedFinMeasAdditive ν T' C' → MeasureTheory.DominatedFinMeasAdditive (μ + ν) (T + T') (max C C')
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castAdd_uIoo : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.castAdd m '' Set.uIoo i j = Set.uIoo (Fin.castAdd m i) (Fin.castAdd m j)
-- Mathlib.Topology.Algebra.Group.Basic
Units.isEmbedding_val : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [ContinuousInv G], Topology.IsEmbedding Units.val
-- Init.Data.BitVec.Lemmas
BitVec.sub_zero : ∀ {n : ℕ} (x : BitVec n), x - 0#n = x
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coe_sup : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I J : FractionalIdeal S P), ↑(I ⊔ J) = ↑I ⊔ ↑J
-- Mathlib.Tactic.TermCongr
/-- Given a `pf` of an `Iff`, `Eq`, or `HEq`, return a proof of `HEq`.
If `pf` is not obviously any of these, weakly try making it be an `Eq` or an `Iff`,
and otherwise make it be a `HEq`.  -/
_private.Mathlib.Tactic.TermCongr.0.Mathlib.Tactic.TermCongr.CongrResult.mk'.toHEqPf : Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PrepathObject.RightHomotopy.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Y : C} {P : HomotopicalAlgebra.PrepathObject Y} {X : C}
  {f g : X ⟶ Y} (h : X ⟶ P.P)
  (h₀ :
    autoParam (CategoryTheory.CategoryStruct.comp h P.p₀ = f)
      HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀._autoParam)
  (h₁ :
    autoParam (CategoryTheory.CategoryStruct.comp h P.p₁ = g)
      HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁._autoParam)
  (h_1 : X ⟶ P.P)
  (h₀_1 :
    autoParam (CategoryTheory.CategoryStruct.comp h_1 P.p₀ = f)
      HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀._autoParam)
  (h₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp h_1 P.p₁ = g)
      HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁._autoParam),
  ({ h := h, h₀ := h₀, h₁ := h₁ } = { h := h_1, h₀ := h₀_1, h₁ := h₁_1 }) = (h = h_1)
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- The identity morphism on a bimodule object.  -/
Bimod.id' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → {A B : CategoryTheory.Mon C} → (M : Bimod A B) → M.Hom M
-- Std.Internal.UV.System
Std.Internal.UV.System.PasswdInfo.mk.inj : ∀ {username : String} {uid gid : Option UInt64} {shell homedir : Option String} {username_1 : String}
  {uid_1 gid_1 : Option UInt64} {shell_1 homedir_1 : Option String},
  { username := username, uid := uid, gid := gid, shell := shell, homedir := homedir } =
      { username := username_1, uid := uid_1, gid := gid_1, shell := shell_1, homedir := homedir_1 } →
    username = username_1 ∧ uid = uid_1 ∧ gid = gid_1 ∧ shell = shell_1 ∧ homedir = homedir_1
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of the reverse direction of `nontrivialTopology_iff_exists_norm_ne_zero'`. -/
NontrivialTopology.of_exists_norm_ne_zero' : ∀ {E : Type u_5} [inst : SeminormedGroup E], (∃ x, ‖x‖ ≠ 0) → NontrivialTopology E
-- Lean.Data.NameTrie
Lean.NamePart : Type
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.reverse_setBlack : ∀ {α : Type u_1} {t : RBTree.RBNode α}, t.setBlack.reverse = t.reverse.setBlack
-- Std.Time.Internal.Bounded
/-- Adds two `Bounded` and adjust the boundaries.
 -/
Std.Time.Internal.Bounded.LE.addBounds : {n m i j : ℤ} →
  Std.Time.Internal.Bounded.LE n m → Std.Time.Internal.Bounded.LE i j → Std.Time.Internal.Bounded.LE (n + i) (m + j)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.isCompact_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] {n : ℕ}
  {i : Topology.RelCWComplex.cell C n}, IsCompact (Topology.RelCWComplex.closedCell n i)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddCommMonoid : {α : Type u_1} → [AddCommMonoid α] → AddCommMonoid (Colex α)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift'_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} {c : C} (i : c ⟶ b) (h : c ⟶ a)
  (hi : CategoryTheory.CategoryStruct.comp (F.map i) f' = CategoryTheory.CategoryStruct.comp (F.map h) g)
  [inst_2 : F.Full] [F.Faithful], CategoryTheory.CategoryStruct.comp (hf'.lift' i h hi) (hf'.fst' g) = i
-- Mathlib.Algebra.Order.AbsoluteValue.Euclidean
/-- A well-founded relation on `R`, satisfying `r (a % b) b`.
This ensures that the GCD algorithm always terminates.  -/
_private.Mathlib.Algebra.Order.AbsoluteValue.Euclidean.0.«term_≺_» : Lean.TrailingParserDescr
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.encodingStepAux.go : Lean.Expr → List Lean.FVarId → Bool → Lean.Meta.RefinedDiscrTree.LazyM✝ Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.Analysis.Normed.Group.Pointwise
closedBall_sub_singleton : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x y : E),
  Metric.closedBall x δ - {y} = Metric.closedBall (x - y) δ
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.blocks_length : ∀ {n : ℕ} (c : CompositionAsSet n), c.blocks.length = c.length
-- Mathlib.Data.NNRat.Floor
Mathlib.Meta.NormNum.IsNNRat.natCeil : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (r : R) (n d : ℕ),
  Mathlib.Meta.NormNum.IsNNRat r n d → ∀ (res : ℕ), ⌈↑n / ↑d⌉₊ = res → Mathlib.Meta.NormNum.IsNat ⌈r⌉₊ res
-- Mathlib.Analysis.Normed.Group.Basic
inseparable_zero_iff_norm : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a : E}, Inseparable a 0 ↔ ‖a‖ = 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α},
  t.getKey? k = some k' → k' ∈ t
-- Mathlib.Topology.Algebra.Module.TransferInstance
/-- Given a continuous linear equivalence `e : α ≃L[R] β`, if scalar multiplication on `β` is
continuous, then so is it for `α`.  -/
ContinuousLinearEquiv.continuousSMul : ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring R] [inst_1 : TopologicalSpace β]
  [inst_2 : AddCommGroup β] [inst_3 : Module R β] [inst_4 : TopologicalSpace R] [ContinuousSMul R β]
  [inst_6 : TopologicalSpace α] [inst_7 : AddCommGroup α] [inst_8 : Module R α] (e : α ≃L[R] β), ContinuousSMul R α
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_inf : ∀ {V : Type u} (G₁ G₂ : SimpleGraph V), (G₁ ⊓ G₂).edgeSet = G₁.edgeSet ∩ G₂.edgeSet
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- Comonoid objects are contravariantly equivalent to monoid objects in the opposite category.
 -/
CategoryTheory.Comon.Comon_EquivMon_OpOp : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Comon C ≌ (CategoryTheory.Mon Cᵒᵖ)ᵒᵖ
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.isClosed`. -/
Topology.CWComplex.isClosed : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D], IsClosed C
-- Mathlib.RingTheory.SimpleModule.InjectiveProjective
Module.projective_of_isSemisimpleRing : ∀ (R : Type u_1) [inst : Ring R] [IsSemisimpleRing R] (M : Type u_2) [inst_2 : AddCommGroup M] [inst_3 : Module R M],
  Module.Projective R M
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- A single (unparenthesized) binder, or a list of parenthesized binders  -/
BigOperators.bigOpBinders : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.Instances.Real
Fact.Manifold.instLeReal : ∀ {x y : ℝ} [hxy : Fact (x < y)], Fact (x ≤ y)
-- Std.Data.DTreeMap.Internal.Balancing
/-- Constructor for an inner node with the correct size.  -/
Std.DTreeMap.Internal.Impl.bin : {α : Type u} →
  {β : α → Type v} →
    (k : α) → β k → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Lean.Meta.DiscrTree.Util
/-- Monadically fold the keys and values stored in a `Trie`.
 -/
Lean.Meta.DiscrTree.Trie.foldM : {m : Type u_1 → Type u_2} →
  {σ : Type u_1} →
    {α : Type} →
      [Monad m] →
        Array Lean.Meta.DiscrTree.Key →
          (σ → Array Lean.Meta.DiscrTree.Key → α → m σ) → σ → Lean.Meta.DiscrTree.Trie α → m σ
-- Mathlib.Analysis.Analytic.Constructions
Units.copy.congr_simp : ∀ {α : Type u} [inst : Monoid α] (u u_1 : αˣ) (e_u : u = u_1) (val val_1 : α) (e_val : val = val_1) (hv : val = ↑u)
  (inv inv_1 : α) (e_inv : inv = inv_1) (hi : inv = ↑u⁻¹), u.copy val hv inv hi = u_1.copy val_1 ⋯ inv_1 ⋯
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.ctor : Lean.Name → List Lean.Level → List Lean.Expr → List Lean.Meta.Match.Pattern → Lean.Meta.Match.Pattern
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.freeMonic.eq_1 : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
  Polynomial.freeMonic R n = Polynomial.X ^ n + ∑ i, Polynomial.C (MvPolynomial.X i) * Polynomial.X ^ ↑i
-- Mathlib.FieldTheory.Separable
/-- If `E / K / F` is a scalar tower and `algebraMap K E x` is separable over `F`, then `x` is
also separable over `F`.  -/
IsSeparable.tower_bot : ∀ {F : Type u_1} [inst : Field F] {K : Type u_2} {E : Type u_3} [inst_1 : Field K] [inst_2 : Ring E]
  [inst_3 : Algebra F K] [inst_4 : Algebra F E] [inst_5 : Algebra K E] [Nontrivial E] [IsScalarTower F K E] {x : K},
  IsSeparable F ((algebraMap K E) x) → IsSeparable F x
-- Mathlib.RingTheory.Ideal.Operations
Ideal.radical_pow : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R) {n : ℕ}, n ≠ 0 → (I ^ n).radical = I.radical
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.coreToInt : Lean.Expr →
  Lean.Expr →
    Lean.Expr → Int.Internal.Linear.Expr → Int.Internal.Linear.Expr → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.whiskeringRight₂_obj_map_app_app : ∀ (B : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (D : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E))
  {X_1 Y : CategoryTheory.Functor B C} (f : X_1 ⟶ Y) (Y_1 : CategoryTheory.Functor B D) (X_2 : B),
  ((((CategoryTheory.Functor.whiskeringRight₂ B C D E).obj X).map f).app Y_1).app X_2 =
    (X.map (f.app X_2)).app (Y_1.obj X_2)
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.inv_hom_iso_homₚ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (f : HP ⟶ HP') (i : ι)
  {Z : CategoryTheory.Functor TopCat C} (h : TopPair.incl.comp (HP'.Hₚ i) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HP.iso i).inv
      (CategoryTheory.CategoryStruct.comp (f.hom i) (CategoryTheory.CategoryStruct.comp (HP'.iso i).hom h)) =
    CategoryTheory.CategoryStruct.comp (TopPair.incl.whiskerLeft (f.homₚ i)) h
-- Mathlib.GroupTheory.IsSubnormal
Subgroup.toGroup.hcongr_3 : ∀ (G G' : Type u_3),
  G = G' →
    ∀ (inst : Group G) (inst' : Group G'),
      inst ≍ inst' → ∀ (H : Subgroup G) (H' : Subgroup G'), H ≍ H' → H.toGroup ≍ H'.toGroup
-- Batteries.Data.Array.Lemmas
Array.extract_eq_of_size_le_stop : ∀ {α : Type u_1} {j i : ℕ} {a : Array α}, a.size ≤ j → a.extract i j = a.extract i
-- Mathlib.Order.Heyting.Basic
/-- `⊤ \ a` is `￢a`  -/
CoheytingAlgebra.top_sdiff : ∀ {α : Type u_4} [self : CoheytingAlgebra α] (a : α), ⊤ \ a = ￢a
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Asymptotics.IsLittleO.sqrt : ∀ {α : Type u_1} {l : Filter α} {f g : α → ℝ}, f =o[l] g → 0 ≤ᶠ[l] g → (fun x => √(f x)) =o[l] fun x => √(g x)
-- Init.Control.Basic
/-- Same as `Bind.bind` but with arguments swapped. 

Conventions for notations in identifiers:

 * The recommended spelling of `=<<` in identifiers is `bindLeft`. -/
Bind.bindLeft : {α : Type u} → {m : Type u → Type u_1} → {β : Type u} → [Bind m] → (α → m β) → m α → m β
-- Mathlib.MeasureTheory.Group.FoelnerFilter
isAddFoelner_maxAddFoelner : ∀ (G : Type u_1) {X : Type u_2} [inst : MeasurableSpace X] (μ : MeasureTheory.Measure X) [inst_1 : AddGroup G]
  [inst_2 : AddAction G X], IsAddFoelner G μ (maxAddFoelner G μ) id
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.dist_eq_sInf : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.dist u v = sInf (Set.range SimpleGraph.Walk.length)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.mapsTo : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), Set.MapsTo (↑e) e.source e.target
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
ContinuousMap.toNNReal_neg_one : ∀ {X : Type u_1} [inst : TopologicalSpace X], (-1).toNNReal = 0
-- Mathlib.Algebra.GroupWithZero.Associated
/-- **Alias** of `dvdNotUnit_of_dvdNotUnit_associated`. -/
Associated.dvdNotUnit_right : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p q r : M}, DvdNotUnit p q → Associated q r → DvdNotUnit p r
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.instHashableFunInfoEnvCacheKey : Hashable Lean.Meta.FunInfoEnvCacheKey✝
-- Mathlib.Data.List.DropRight
_private.Mathlib.Data.List.DropRight.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.RingTheory.Bialgebra.Convolution
AlgHom.convMul_apply : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R C] [inst_4 : Algebra R A] (f g : WithConv (C →ₐ[R] A)) (c : C),
  (f * g).ofConv c = (Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯) (CoalgebraStruct.comul c)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ : ∀ {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U)
  (hx : x ∈ V),
  CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ V x hx) (X.restrictStalkIso h x).hom =
    X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.maxEntryD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {fallback : α × β}, t₁.Equiv t₂ → t₁.maxEntryD fallback = t₂.maxEntryD fallback
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.int.divByNat_self : ∀ (n : ℕ), (CharacterModule.int.divByNat n) ↑n = 0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
/-- A version of `Commute.cfc` or `IsSelfAdjoint.commute_cfc` which does not require any interaction
with `star` when the base ring is `ℝ`.  -/
Commute.cfc_real : ∀ {A : Type u_2} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : Algebra ℝ A] [inst_3 : TopologicalSpace A]
  [inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [IsTopologicalRing A] [T2Space A] {a b : A},
  Commute a b → ∀ (f : ℝ → ℝ), Commute (cfc f a) b
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.map_eq_zero_iff : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) {x : M₁}, e x = 0 ↔ x = 0
-- Init.Data.Nat.Lemmas
Nat.sub_le_sub_iff_left : ∀ {n m k : ℕ}, n ≤ k → (k - m ≤ k - n ↔ n ≤ m)
-- Mathlib.Algebra.Homology.ShortComplex.Limits
/-- `limitCone F` becomes limit after the application of `π₂ : ShortComplex C ⥤ C`.  -/
CategoryTheory.ShortComplex.isLimitπ₂MapConeLimitCone : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) →
            [inst_3 : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)] →
              [inst_4 : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)] →
                [inst_5 : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)] →
                  CategoryTheory.Limits.IsLimit
                    (CategoryTheory.ShortComplex.π₂.mapCone (CategoryTheory.ShortComplex.limitCone F))
-- Mathlib.Data.UInt
USize.toBitVec_intCast : ∀ (z : ℤ), (↑z).toBitVec = ↑z
-- Mathlib.Data.FunLike.Embedding
EmbeddingLike.comp_injective : ∀ {α : Sort u_2} {β : Sort u_3} {γ : Sort u_4} {F : Sort u_5} [inst : FunLike F β γ] [EmbeddingLike F β γ] (f : α → β)
  (e : F), Function.Injective (⇑e ∘ f) ↔ Function.Injective f
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.ofPowerSeries_powerSeriesPart : ∀ {R : Type u_1} [inst : Semiring R] (x : LaurentSeries R),
  (HahnSeries.ofPowerSeries ℤ R) x.powerSeriesPart = (HahnSeries.single (-HahnSeries.order x)) 1 * x
-- Lean.Meta.DiscrTree.Main
/-- A liberal version of `getMatch` which only takes the root symbol of `e` into account.
We use this method to simulate Lean 3's indexing.

The natural number in the result is the number of arguments in `e` after `reduceDT`.
 -/
Lean.Meta.DiscrTree.getMatchLiberal : {α : Type} → Lean.Meta.DiscrTree α → Lean.Expr → Lean.MetaM (Array α × ℕ)
-- Mathlib.Topology.Algebra.Valued.ValuedField
/-- The zero-preserving monoid homomorphism from the `ValueGroup₀` of the valuation on `K` to
that of the extension to its completion. TODO: Split out the definition of `(restrict₀_surjective
(.ofClass hv.v) x).choose` and prove a spec lemma of it. Remove tactic `set` in the proof.  -/
Valued.valueGroup₀_hom_extensionValuation : {K : Type u_1} →
  [inst : Field K] →
    {Γ₀ : Type u_2} →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
        [hv : Valued K Γ₀] →
          (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ →*₀
            (MonoidWithZeroHom.ofClass Valued.extensionValuation).ValueGroup₀
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.takeUntil : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} {p : G.Walk v w},
  p.IsPath → ∀ (h : u ∈ p.support), (p.takeUntil u h).IsPath
-- Mathlib.Order.Filter.Cofinite
Filter.cofinite_eq_bot_iff : ∀ {α : Type u_2}, Filter.cofinite = ⊥ ↔ Finite α
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  IsLocalizedModule x.asIdeal.primeCompl (AlgebraicGeometry.StructureSheaf.toStalkₗ R M x)
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.cof_le_one_iff : ∀ {α : Type u} [inst : Preorder α] [Nonempty α], Order.cof α ≤ 1 ↔ ∃ x, IsTop x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_eq_some_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.maxKey? = some t.maxKey!
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
/-- **Alias** of `LocallyCompactSpace.of_isCompactOperator_id`.

---

**Alias** of the forward direction of `isCompactOperator_id_iff_locallyCompactSpace`. -/
IsCompactOperator.locallyCompactSpace : ∀ {E : Type u_1} [inst : AddGroup E] [inst_1 : TopologicalSpace E] [IsTopologicalAddGroup E],
  IsCompactOperator id → LocallyCompactSpace E
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
/-- The postcomposition of an homotopy class by a relative morphism.  -/
SSet.RelativeMorphism.HomotopyClass.postcomp : {X Y Z : SSet} →
  {A : X.Subcomplex} →
    {B : Y.Subcomplex} →
      {φ : A.toSSet ⟶ B.toSSet} →
        {C : Z.Subcomplex} →
          {ψ : B.toSSet ⟶ C.toSSet} →
            SSet.RelativeMorphism.HomotopyClass A B φ →
              SSet.RelativeMorphism B C ψ →
                {φψ : A.toSSet ⟶ C.toSSet} →
                  CategoryTheory.CategoryStruct.comp φ ψ = φψ → SSet.RelativeMorphism.HomotopyClass A C φψ
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.CountableAB4Star.ofShape : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasCountableProducts C}
  [self : CategoryTheory.CountableAB4Star C] (α : Type) [inst_2 : Countable α],
  CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete α) C
-- Mathlib.Topology.Separation.Basic
/-- **Alias** of `t0Space_iff_exists_isOpen_xor_mem`. -/
t0Space_iff_exists_isOpen_xor'_mem : ∀ (X : Type u) [inst : TopologicalSpace X], T0Space X ↔ Pairwise fun x y => ∃ U, IsOpen U ∧ Xor (x ∈ U) (y ∈ U)
-- Init.Data.List.Attach
_private.Init.Data.List.Attach.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.limitAddMonoid : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddMonCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] →
        AddMonoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).pt
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_replaceₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β),
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ (a : α) (b : β a),
      (Std.DHashMap.Internal.toListModel (↑(m.replaceₘ a b)).buckets).Perm
        (Std.Internal.List.replaceEntry a b (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.Topology.MetricSpace.Lipschitz
Real.lipschitzWith_toNNReal : LipschitzWith 1 Real.toNNReal
-- Batteries.Data.Nat.Lemmas
Nat.strongRecOn_eq : ∀ {motive : ℕ → Sort u_1} (ind : (n : ℕ) → ((m : ℕ) → m < n → motive m) → motive n) (t : ℕ),
  Nat.strongRecOn t ind = ind t fun m x => Nat.strongRecOn m ind
-- Init.Data.String.Lemmas.Pattern.Char
_private.Init.Data.String.Lemmas.Pattern.Char.0.String.Slice.Pos.skipWhile.match_1.eq_1 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (nextCurr : s.Pos)
  (h_1 : (nextCurr : s.Pos) → motive (some nextCurr)) (h_2 : Unit → motive none),
  (match some nextCurr with
    | some nextCurr => h_1 nextCurr
    | none => h_2 ()) =
    h_1 nextCurr
-- Mathlib.FieldTheory.Separable
Polynomial.isUnit_or_eq_zero_of_separable_expand : ∀ {F : Type u} [inst : Field F] (p : ℕ) [HF : CharP F p] {f : Polynomial F} (n : ℕ),
  0 < p → ((Polynomial.expand F (p ^ n)) f).Separable → IsUnit f ∨ n = 0
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.coe_addMonoidHom_refl : ∀ {M : Type u_4} [inst : AddZeroClass M], ↑(AddEquiv.refl M) = AddMonoidHom.id M
-- Mathlib.Topology.Metrizable.Uniformity
PseudoEMetricSpace.pseudoMetrizableSpace : ∀ {α : Type u_2} [inst : PseudoEMetricSpace α], TopologicalSpace.PseudoMetrizableSpace α
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.instTypeNameLazyTraceChildren : TypeName Lean.Widget.LazyTraceChildren