mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- The projection of the counit.  -/
CompHausLike.LocallyConstant.counitAppAppImage : {P : TopCat → Prop} →
  [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] →
    {S : CompHausLike P} →
      {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))} →
        [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] →
          (f : LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))) →
            (a : Function.Fiber ⇑f) → Y.obj (Opposite.op (CompHausLike.LocallyConstant.fiber f a))
-- Mathlib.Data.Finsupp.Option
/-- Extend a finitely supported function on `α` to a finitely supported function on `Option α`,
provided a default value for `none`.
 -/
Finsupp.optionElim : {α : Type u_1} → {M : Type u_2} → [inst : Zero M] → M → (α →₀ M) → Option α →₀ M
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.isUnit_iff : ∀ {α : Type u_2} [inst : DivisionMonoid α] {s : Set α}, IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a
-- Lean.Level
Lean.Level.imax.injEq : ∀ (a a_1 a_2 a_3 : Lean.Level), (a.imax a_1 = a_2.imax a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.RingTheory.Morita.Matrix
fromModuleCatToModuleCatLinearEquivtoModuleCatObj.eq_1 : ∀ (R : Type u) {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (M : Type u_1)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (i : ι),
  fromModuleCatToModuleCatLinearEquivtoModuleCatObj R M i =
    {
      toFun :=
        (AddEquiv.refl
            ↑(((ModuleCat.toMatrixModCat R ι).comp (MatrixModCat.toModuleCat R i)).obj (ModuleCat.of R M))).toFun,
      map_add' := ⋯, map_smul' := ⋯,
      invFun :=
        (AddEquiv.refl
            ↑(((ModuleCat.toMatrixModCat R ι).comp (MatrixModCat.toModuleCat R i)).obj (ModuleCat.of R M))).invFun,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.NumberTheory.Height.NumberField
_private.Mathlib.NumberTheory.Height.NumberField.0.NumberField.one_le_pow_totalWeight_mul_finprod : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {n : ℕ},
  n ≠ 0 →
    ∀ (a : NumberField.RingOfIntegers K),
      1 ≤ ↑n ^ Height.totalWeight K * ∏ᶠ (v : NumberField.FinitePlace K), ⨆ i, v (![↑a, ↑n] i)
-- Mathlib.RingTheory.Coalgebra.Basic
Pi.counit_comp_finsuppLcoeFun : ∀ {R : Type u_1} {n : Type u_2} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M : Type u_4}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : CoalgebraStruct R M],
  CoalgebraStruct.counit ∘ₗ Finsupp.lcoeFun = CoalgebraStruct.counit
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.Hom.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} (f f_1 : A₀.a ⟶ A₁.a) (e_f : f = f_1)
  (h : CategoryTheory.CategoryStruct.comp (F.map f) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str f),
  { f := f, h := h } = { f := f_1, h := ⋯ }
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.lift_restrict : ∀ {α : Type u_1} {M : Type u_4} [inst : AddMonoid M] (f : FreeAddMonoid α →+ M),
  FreeAddMonoid.lift (⇑f ∘ FreeAddMonoid.of) = f
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.singleMapHomologicalComplex_inv_app_ne : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] [inst_4 : CategoryTheory.Limits.HasZeroObject W₁]
  [inst_5 : CategoryTheory.Limits.HasZeroObject W₂] (F : CategoryTheory.Functor W₁ W₂)
  [inst_6 : F.PreservesZeroMorphisms] (c : ComplexShape ι) [inst_7 : DecidableEq ι] {i j : ι},
  i ≠ j → ∀ (X : W₁), ((HomologicalComplex.singleMapHomologicalComplex F c j).inv.app X).f i = 0
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_one_mul_cancel_right_iff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R} {m : σ →₀ ℕ},
  p * (MvPolynomial.monomial m) 1 = q * (MvPolynomial.monomial m) 1 ↔ p = q
-- Mathlib.Logic.Encodable.Basic
Encodable.decodeSum.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Encodable β] (n : ℕ),
  Encodable.decodeSum n =
    match n.bodd, n.div2 with
    | false, m => Option.map Sum.inl (Encodable.decode m)
    | x, m => Option.map Sum.inr (Encodable.decode m)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toList_ric : ∀ {n k : ℕ}, List.map (fun x => x + k) (*...=n).toList = (k...=n + k).toList
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.Hereditarily.eq_1 : ∀ (p : ZFSet.{u_1} → Prop) (x : ZFSet.{u_1}), ZFSet.Hereditarily p x = (p x ∧ ∀ y ∈ x, ZFSet.Hereditarily p y)
-- Mathlib.Topology.UniformSpace.Ultra.Completion
IsUniformInducing.isUltraUniformity : ∀ {X : Type u_1} {Y : Type u_2} [inst : UniformSpace X] [inst_1 : UniformSpace Y] [IsUltraUniformity Y] {f : X → Y},
  IsUniformInducing f → IsUltraUniformity X
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.measurable_cylinderEvents_iff : ∀ {α : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {mα : MeasurableSpace α} [m : (i : ι) → MeasurableSpace (X i)]
  {Δ : Set ι} {g : α → (i : ι) → X i}, Measurable g ↔ ∀ ⦃i : ι⦄, i ∈ Δ → Measurable fun a => g a i
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} {I : CategoryTheory.InjectiveResolution Z} {Z' : C}
  {I' : CategoryTheory.InjectiveResolution Z'} {f : Z ⟶ Z'} (hom : I.cocomplex ⟶ I'.cocomplex)
  (ι_f_zero_comp_hom_f_zero :
    CategoryTheory.CategoryStruct.comp (I.ι.f 0) (hom.f 0) =
      CategoryTheory.CategoryStruct.comp (((CochainComplex.single₀ C).map f).f 0) (I'.ι.f 0))
  (hom_1 : I.cocomplex ⟶ I'.cocomplex)
  (ι_f_zero_comp_hom_f_zero_1 :
    CategoryTheory.CategoryStruct.comp (I.ι.f 0) (hom_1.f 0) =
      CategoryTheory.CategoryStruct.comp (((CochainComplex.single₀ C).map f).f 0) (I'.ι.f 0)),
  ({ hom := hom, ι_f_zero_comp_hom_f_zero := ι_f_zero_comp_hom_f_zero } =
      { hom := hom_1, ι_f_zero_comp_hom_f_zero := ι_f_zero_comp_hom_f_zero_1 }) =
    (hom = hom_1)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.natIsoSc'_inv_app_τ₂ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c),
  ((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₂ = CategoryTheory.CategoryStruct.id (X.X j)
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.instIsModularLattice : ∀ {R : Type u_10} {M : Type u_11} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsModularLattice (Submodule R M)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- An operator is a star projection if and only if it is an orthogonal projection.  -/
isStarProjection_iff_eq_starProjection_range : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {p : E →L[𝕜] E},
  IsStarProjection p ↔ ∃ (x : (↑p).range.HasOrthogonalProjection), p = (↑p).range.starProjection
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.toOrderHom : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [inst_2 : BoundedOrder α] → [inst_3 : BoundedOrder β] → BoundedOrderHom α β → α →o β
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.totalFlipIso_hom_f_D₁ : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c]
  [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c]
  [inst_6 : DecidableEq J] (j j' : J),
  CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).hom.f j) (K.D₁ c j j') =
    CategoryTheory.CategoryStruct.comp (K.flip.D₂ c j j') ((K.totalFlipIso c).hom.f j')
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- `HasImage f` means that there exists an image factorisation of `f`.  -/
CategoryTheory.Limits.HasImage.exists_image : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y}
  [self : CategoryTheory.Limits.HasImage f], Nonempty (CategoryTheory.Limits.ImageFactorisation f)
-- Mathlib.Order.Std
/-- ≤ forms a linear order.  -/
LinearOrder.OfStdArgs.isLinearOrder : ∀ {α : Type u_1} (self : LinearOrder.OfStdArgs α),
  let this := self.le;
  Std.IsLinearOrder α
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.IsPositive.isSelfAdjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {T : E →L[𝕜] E}, T.IsPositive → IsSelfAdjoint T
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.constCompSigmaIsoConst_hom_app : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape α C] {I : α → Type u_1}
  [inst_2 : (i : α) → CategoryTheory.Category.{v_1, u_1} (I i)] (X : α → C) (X_1 : (i : α) → I i),
  (CategoryTheory.Limits.Sigma.constCompSigmaIsoConst X).hom.app X_1 = CategoryTheory.CategoryStruct.id (∐ fun i => X i)
-- Mathlib.Algebra.Group.End
Equiv.permCongrHom_symm : ∀ {α : Type u_4} {β : Type u_5} (e : α ≃ β), e.permCongrHom.symm = e.symm.permCongrHom
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.prime_ne_zero : ∀ (p q : ℕ) [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)], p ≠ q → ↑q ≠ 0
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The map which sends `0 : Fin 2` to `X₀` and `1` to `X₁`.  -/
CategoryTheory.ComposableArrows.Mk₁.obj : {C : Type u_1} → C → C → Fin 2 → C
-- Init.Data.String.Slice
/-- Splits a slice at each subslice that matches the pattern `pat`. Unlike `split` the
matched subslices are included at the end of each subslice.

This function is generic over all currently supported patterns.

Examples:

* `("coffee tea water".toSlice.splitInclusive Char.isWhitespace).toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`

* `("coffee tea water".toSlice.splitInclusive ' ').toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`

* `("coffee tea water".toSlice.splitInclusive " tea ").toList == ["coffee tea ".toSlice, "water".toSlice]`

* `("baaab".toSlice.splitInclusive "aa").toList == ["baa".toSlice, "ab".toSlice]`
 -/
String.Slice.splitInclusive : {ρ : Type} →
  {σ : String.Slice → Type} →
    (s : String.Slice) → (pat : ρ) → [inst : String.Slice.Pattern.ToForwardSearcher pat σ] → Std.Iter String.Slice
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.mk.inj : ∀ {α α₂ β : Type w} {m : Type w → Type u_1} {it₁ : Std.IterM m (Std.IterM m β)} {it₂ : Option (Std.IterM m β)}
  {it₁_1 : Std.IterM m (Std.IterM m β)} {it₂_1 : Option (Std.IterM m β)},
  { it₁ := it₁, it₂ := it₂ } = { it₁ := it₁_1, it₂ := it₂_1 } → it₁ = it₁_1 ∧ it₂ = it₂_1
-- Mathlib.Order.SuccPred.Tree
/-- The unique atom less than an element in an `OrderBot` with archimedean predecessor.
 -/
IsPredArchimedean.findAtom : {α : Type u_1} →
  [inst : PartialOrder α] → [inst_1 : PredOrder α] → [IsPredArchimedean α] → [OrderBot α] → [DecidableEq α] → α → α
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.fix.sizeOf_spec : ∀ (a : Turing.ToPartrec.Code), sizeOf a.fix = 1 + sizeOf a
-- Mathlib.Topology.ContinuousMap.Basic
/-- Deprecated. Use `map_continuousAt` instead.  -/
ContinuousMap.continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : C(α, β)) (x : α),
  ContinuousAt (⇑f) x
-- Mathlib.Data.Matrix.Basic
LinearMap.mapMatrix_neg : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [inst : Semiring R]
  [inst_1 : Semiring S] {σᵣₛ : R →+* S} [inst_2 : AddCommMonoid α] [inst_3 : AddCommGroup β] [inst_4 : Module R α]
  [inst_5 : Module S β] (f : α →ₛₗ[σᵣₛ] β), (-f).mapMatrix = -f.mapMatrix
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.Rel'.inr_inl : ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (s : S),
  CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inr ((CategoryTheory.ConcreteCategory.hom g) s))
    (Sum.inl ((CategoryTheory.ConcreteCategory.hom f) s))
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
/-- Constructor for maps from the type of connected components of a simplicial set.  -/
SSet.π₀.lift : {X : SSet} →
  {T : Type u_1} →
    (f : X.obj (Opposite.op { len := 0 }) → T) →
      (∀ ⦃x₀ x₁ : X.obj (Opposite.op { len := 0 })⦄ (x : SSet.Edge x₀ x₁), f x₀ = f x₁) → X.π₀ → T
-- Mathlib.Algebra.Polynomial.Degree.Operations
/-- `Polynomial.leadingCoeff` bundled as a `MonoidHom` when `R` has `NoZeroDivisors`, and thus
`leadingCoeff` is multiplicative  -/
Polynomial.leadingCoeffHom : {R : Type u} → [inst : Semiring R] → [NoZeroDivisors R] → Polynomial R →* R
-- Mathlib.Order.RelSeries
RelSeries.last_map : ∀ {α : Type u_1} {r : SetRel α α} {β : Type u_2} {s : SetRel β β} (p : RelSeries r) (f : r.Hom s),
  (p.map f).last = f p.last
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.IsBase.compl_isBase_of_dual : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M✶.IsBase B → M.IsBase (M.E \ B)
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_union_lt_top_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α},
  μ (s ∪ t) < ⊤ ↔ μ s < ⊤ ∧ μ t < ⊤
-- Lean.Log
/-- Log a new information message using the given message data. The position is provided by `getRef`.  -/
Lean.logInfo : {m : Type → Type} →
  [Monad m] → [Lean.MonadLog m] → [Lean.AddMessageContext m] → [Lean.MonadOptions m] → Lean.MessageData → m Unit
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_inj : ∀ {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 e' : M₁ ≃SL[σ₁₂] M₂}, ↑e = ↑e' ↔ e = e'
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp}, t.keys.isEmpty = t.isEmpty
-- Mathlib.Algebra.CharP.Lemmas
list_sum_pow_char : ∀ {R : Type u_3} [inst : CommSemiring R] (p : ℕ) [ExpChar R p] (l : List R),
  l.sum ^ p = (List.map (fun x => x ^ p) l).sum
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- Predicate for adjacency. Two vertices `x` and `y` are adjacent if there is some edge `e ∈ E(H)`
where `x` and `y` are both incident to `e`.

Note that we do not need to explicitly check that `x, y ∈ V(H)` here because a vertex that is not in
the vertex set cannot be incident to any edge.
 -/
Hypergraph.Adj : {α : Type u_1} → Hypergraph α → α → α → Prop
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_g : ∀ (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)),
  ((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).obj F).g =
    F.whiskerLeft CategoryTheory.ShortComplex.π₂Toπ₃
-- Mathlib.RingTheory.Ideal.Maps
Submodule.annihilator_mono : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N P : Submodule R M}, N ≤ P → P.annihilator ≤ N.annihilator
-- Mathlib.Data.Finset.Basic
Finset.sdiff_eq_filter : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), s₁ \ s₂ = {x ∈ s₁ | x ∉ s₂}
-- Mathlib.Data.Nat.Init
/-- Induction principle deriving the next case from the two previous ones.  -/
Nat.twoStepInduction : {motive : ℕ → Sort u_1} →
  motive 0 → motive 1 → ((n : ℕ) → motive n → motive (n + 1) → motive (n + 2)) → (a : ℕ) → motive a
-- Batteries.Data.Fin.Lemmas
Fin.coe_divNat : ∀ {m n : ℕ} (i : Fin (m * n)), ↑i.divNat = ↑i / n
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {fallback : α},
  (t.insertIfNew k v).maxKeyD fallback = t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.Equalizer.lift.congr_simp : ∀ {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  [inst_2 : SeminormedAddCommGroup V₁] {f g : NormedAddGroupHom V W} (φ φ_1 : NormedAddGroupHom V₁ V) (e_φ : φ = φ_1)
  (h : f.comp φ = g.comp φ), NormedAddGroupHom.Equalizer.lift φ h = NormedAddGroupHom.Equalizer.lift φ_1 ⋯
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- If two sets are nonempty and bounded in a metric space, they are at finite Hausdorff
edistance.  -/
Metric.hausdorffEDist_ne_top_of_nonempty_of_bounded : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α},
  s.Nonempty → t.Nonempty → Bornology.IsBounded s → Bornology.IsBounded t → Metric.hausdorffEDist s t ≠ ⊤
-- Mathlib.Order.Disjoint
codisjoint_subtype_iff : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {pr : α → Prop},
  (∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊔ t)) → ∀ (htop : pr ⊤) {a b : Subtype pr}, Codisjoint a b ↔ Codisjoint ↑a ↑b
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.FiniteRangeSetoid.equiv_iff_isNoetherian_quotient_eqLocus : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {u v : V →ₗ[K] V₂}, u ≈ v ↔ IsNoetherian K (V ⧸ u.eqLocus v)
-- Mathlib.Topology.Instances.Sign
continuousAt_sign_of_neg : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : TopologicalSpace α] [inst_2 : PartialOrder α] [inst_3 : DecidableLT α]
  [OrderTopology α] {a : α}, a < 0 → ContinuousAt (⇑SignType.sign) a
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.equivOfIso_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F)
  (i : F.I₀), (CategoryTheory.PreZeroHypercover.equivOfIso e).symm i = e.inv.s₀ i
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.cases.sizeOf_spec : ∀ (eager : Bool), sizeOf (Lean.Meta.Grind.AttrKind.cases eager) = 1 + sizeOf eager
-- Mathlib.Data.PNat.Xgcd
/-- A term of `XgcdType` is a system of six naturals.  They should
be thought of as representing the matrix
`[[w, x], [y, z]] = [[wp + 1, x], [y, zp + 1]]`
together with the vector `[a, b] = [ap + 1, bp + 1]`.
 -/
PNat.XgcdType : Type
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- **Alias** of `Valuation.mem_nhds_zero_iff`. -/
Valuation.is_topological_valuation : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_3 : TopologicalSpace R] (v : Valuation R Γ₀) [v.Compatible] [IsValuativeTopology R] (s : Set R),
  s ∈ nhds 0 ↔ ∃ γ, {x | v.restrict x < ↑γ} ⊆ s
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateAddSubgroup.addSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_2} [inst_1 : SetLike S G] [AddSubgroupClass S G] {H : S},
  IsApproximateAddSubgroup 1 ↑H
-- Mathlib.Algebra.Category.CommBialgCat
/-- Build an isomorphism in the category `CommBialgCat R` from a `BialgEquiv` between
`Bialgebra`s.  -/
CommBialgCat.isoMk : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      {x : CommRing X} →
        {x_1 : CommRing Y} →
          {x_2 : Bialgebra R X} → {x_3 : Bialgebra R Y} → (X ≃ₐc[R] Y) → (CommBialgCat.of R X ≅ CommBialgCat.of R Y)
-- Mathlib.Analysis.Convex.Gauge
Convex.uniformContinuous_gauge : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E},
  Convex ℝ s → s ∈ nhds 0 → UniformContinuous (gauge s)
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.continuous_eval : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [inst : (i : ι) → TopologicalSpace (R i)]
  (i : ι), Continuous fun x => x i
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_le_size_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, t.size ≤ (t.insertIfNew k v).size
-- Std.Data.HashMap.Basic
/-- Returns a list of all values present in the hash map in some order.  -/
Std.HashMap.values : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → List β
-- Mathlib.Data.DFinsupp.Order
DFinsupp.subset_support_tsub : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : ∀ (i : ι), CanonicallyOrderedAdd (α i)] [inst_3 : (i : ι) → Sub (α i)]
  [inst_4 : ∀ (i : ι), OrderedSub (α i)] {f g : Π₀ (i : ι), α i} [inst_5 : DecidableEq ι]
  [inst_6 : (i : ι) → (x : α i) → Decidable (x ≠ 0)], f.support \ g.support ⊆ (f - g).support
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_filter_key : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → Bool} {k : α},
  m.WF → (Std.HashMap.Raw.filter (fun k x => f k) m).getKey? k = Option.filter f (m.getKey? k)
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.iff_is_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [PreconnectedSpace X] {f : X → Y},
  IsLocallyConstant f ↔ ∀ (x y : X), f x = f y
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.const.eq_2 : ∀ (c : ℝ) (basis_hd : ℝ → ℝ) (basis_tl : List (ℝ → ℝ)),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.const (basis_hd :: basis_tl) c =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
      (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.const basis_hd basis_tl c) fun x => c
-- Init.Data.Iterators.Basic
Std.IterM.mk.injEq : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} (internalState internalState_1 : α),
  ({ internalState := internalState } = { internalState := internalState_1 }) = (internalState = internalState_1)
-- Lean.Server.Completion.CompletionInfoSelection
_private.Lean.Server.Completion.CompletionInfoSelection.0.Lean.Server.Completion.findCompletionInfosAt.containsHoverPos : String.Pos.Raw → Lean.Elab.CompletionInfo → Bool
-- Mathlib.Logic.Equiv.Prod
Equiv.funSplitAt_apply : ∀ {α : Type u_9} [inst : DecidableEq α] (i : α) (β : Type u_10) (f : (j : α) → (fun a => β) j),
  (Equiv.funSplitAt i β) f = (f i, fun j => f ↑j)
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- A natural isomorphism between the functor `map (𝟭 C)` and `𝟭 (WithInitial C)`.  -/
CategoryTheory.WithInitial.mapId : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.WithInitial.map (CategoryTheory.Functor.id C) ≅
      CategoryTheory.Functor.id (CategoryTheory.WithInitial C)
-- Mathlib.NumberTheory.LSeries.RiemannZeta
HurwitzZeta.completedHurwitzZetaEven_zero : ∀ (s : ℂ), HurwitzZeta.completedHurwitzZetaEven 0 s = completedRiemannZeta s
-- Init.Grind.Ring.Basic
/-- Scalar multiplication by the negation of an integer is the negation of scalar multiplication by that integer.  -/
Lean.Grind.Ring.neg_zsmul : ∀ {α : Type u} [self : Lean.Grind.Ring α] (i : ℤ) (a : α), -i • a = -(i • a)