mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
CategoryTheory.Limits.instHasColimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesColimit₂ : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [CategoryTheory.Limits.HasColimit K₁] [CategoryTheory.Limits.HasColimit K₂]
  [CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G],
  CategoryTheory.Limits.HasColimit
    (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
-- Lean.CoreM
/-- Run a `CoreM` monad in IO.
Note that the value of `ctx.initHeartbeats` is ignored and replaced with `IO.getNumHeartbeats`.
 -/
Lean.Core.CoreM.toIO : {α : Type} → Lean.CoreM α → Lean.Core.Context → Lean.Core.State → IO (α × Lean.Core.State)
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.refl_toCoalgEquiv : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CoalgebraStruct R A], ↑(BialgEquiv.refl R A) = CoalgEquiv.refl R A
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
notMem_of_lt_csInf' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {x : α} {s : Set α}, x < sInf s → x ∉ s
-- Mathlib.Tactic.LinearCombination
/-- The handling in `linear_combination` of left- and right-multiplication and scalar-multiplication
and of division all five proceed according to the same logic, specified here: given a proof `p` of
an (in)equality and a constant `c`,
* if `p` is a proof of an equation, multiply/divide through by `c`;
* if `p` is a proof of a non-strict inequality, run `positivity` to find a proof that `c` is
  nonnegative, then multiply/divide through by `c`, invoking the nonnegativity of `c` where needed;
* if `p` is a proof of a strict inequality, run `positivity` to find a proof that `c` is positive
  (if possible) or nonnegative (if not), then multiply/divide through by `c`, invoking the
  positivity or nonnegativity of `c` where needed.

This generic logic takes as a parameter the object `lems`: the four lemmas corresponding to the four
cases.  -/
Mathlib.Tactic.LinearCombination.rescale : (Mathlib.Ineq.WithStrictness → Lean.Name) →
  Option Lean.Expr →
    Lean.Term → Lean.Term → Mathlib.Ineq → Lean.Elab.TermElabM Mathlib.Tactic.LinearCombination.Expanded
-- Mathlib.Order.WithBot
WithBot.lt_toDual_iff : ∀ {α : Type u_1} [inst : LT α] {x : WithTop αᵒᵈ} {y : WithBot α}, x < WithBot.toDual y ↔ y < WithTop.ofDual x
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift'_snd_assoc : ∀ {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] {Z : C} (h_1 : a ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hf'.lift' i h hi) (CategoryTheory.CategoryStruct.comp (hf'.snd g) h_1) =
    CategoryTheory.CategoryStruct.comp h h_1
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.mem_spectrum_iff_resolvent_zero : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Nontrivial A] {r : R}
  {a : A}, r ∈ spectrum R a ↔ resolvent a r = 0
-- Mathlib.RingTheory.Idempotents
OrthogonalIdempotents.mk : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} {e : I → R},
  (∀ (i : I), IsIdempotentElem (e i)) → (Pairwise fun x1 x2 => e x1 * e x2 = 0) → OrthogonalIdempotents e
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.tendsto_logb_comp_add_sub_logb : ∀ {b : ℝ} (y : ℝ), Filter.Tendsto (fun x => Real.logb b (x + y) - Real.logb b x) Filter.atTop (nhds 0)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (M : X.Modules)
  (U : X.Opens),
  AlgebraicGeometry.Scheme.Modules.Hom.app ((AlgebraicGeometry.Scheme.Modules.restrictAdjunction f).counit.app M) U =
    M.presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Init.Data.List.Count
_private.Init.Data.List.Count.0.List.filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Batteries.Data.String.Lemmas
String.revPosOf_eq : ∀ (s : String) (c : Char), String.Legacy.revPosOf s c = String.Legacy.revFind s fun x => x == c
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.HasPushoutsAgainst.hasPushoutsAlong : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P P' : CategoryTheory.MorphismProperty C}
  [self : P.HasPushoutsAgainst P'] ⦃X Y : C⦄ (f : X ⟶ Y), P' f → P.HasPushoutsAlong f
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.Measure.IsAddLeftInvariant.mk : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] {μ : MeasureTheory.Measure G},
  (∀ (g : G), MeasureTheory.Measure.map (fun x => g + x) μ = μ) → μ.IsAddLeftInvariant
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.ofNat_smul : ∀ {n : ℕ} {R : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : n.AtLeastTwo] {a : A}, OfNat.ofNat n • a = OfNat.ofNat n * a
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.coe_mapRingHom : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S),
  ⇑(Polynomial.mapRingHom f) = Polynomial.map f
-- Mathlib.LinearAlgebra.TensorProduct.Tower
Algebra.lsmul.congr_simp : ∀ (R : Type u) {A : Type w} (B : Type u₁) (M : Type v₁) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddCommMonoid M] [inst_6 : Module R M]
  [inst_7 : Module A M] [inst_8 : Module B M] [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M]
  [inst_11 : SMulCommClass A B M], Algebra.lsmul R B M = Algebra.lsmul R B M
-- Mathlib.Logic.Equiv.Basic
/-- If `α` is equivalent to `β` and the predicates `p : α → Prop` and `q : β → Prop` are equivalent
at corresponding points, then `{a // p a}` is equivalent to `{b // q b}`.
For the statement where `α = β`, that is, `e : perm α`, see `Perm.subtypePerm`.  -/
Equiv.subtypeEquiv : {α : Sort u_1} →
  {β : Sort u_4} →
    {p : α → Prop} → {q : β → Prop} → (e : α ≃ β) → (∀ (a : α), p a ↔ q (e a)) → { a // p a } ≃ { b // q b }
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.LimitOfShape.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {X : C}
  (toLimitPresentation : CategoryTheory.Limits.LimitPresentation J X)
  (prop_diag_obj : ∀ (j : J), P (toLimitPresentation.diag.obj j))
  (toLimitPresentation_1 : CategoryTheory.Limits.LimitPresentation J X)
  (prop_diag_obj_1 : ∀ (j : J), P (toLimitPresentation_1.diag.obj j)),
  ({ toLimitPresentation := toLimitPresentation, prop_diag_obj := prop_diag_obj } =
      { toLimitPresentation := toLimitPresentation_1, prop_diag_obj := prop_diag_obj_1 }) =
    (toLimitPresentation = toLimitPresentation_1)
-- Lean.Elab.Tactic.Config
Lean.Elab.Tactic.ConfigItemView : Type
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- To prove something for an arbitrary simple function, it suffices to show
that the property holds for (multiples of) characteristic functions and is closed under
addition (of functions with disjoint support).

It is possible to make the hypotheses in `h_add` a bit stronger, and such conditions can be added
once we need them (for example it is only necessary to consider the case where `g` is a multiple
of a characteristic function, and that this multiple doesn't appear in the image of `f`).

To use in an induction proof, the syntax is `induction f using SimpleFunc.induction with`.  -/
MeasureTheory.SimpleFunc.induction : ∀ {α : Type u_5} {γ : Type u_6} [inst : MeasurableSpace α] [inst_1 : AddZeroClass γ]
  {motive : MeasureTheory.SimpleFunc α γ → Prop},
  (∀ (c : γ) {s : Set α} (hs : MeasurableSet s),
      motive
        (MeasureTheory.SimpleFunc.piecewise s hs (MeasureTheory.SimpleFunc.const α c)
          (MeasureTheory.SimpleFunc.const α 0))) →
    (∀ ⦃f g : MeasureTheory.SimpleFunc α γ⦄,
        Disjoint (Function.support ⇑f) (Function.support ⇑g) → motive f → motive g → motive (f + g)) →
      ∀ (f : MeasureTheory.SimpleFunc α γ), motive f
-- Mathlib.Data.QPF.Multivariate.Constructions.Prj
MvQPF.Prj.mvqpf : {n : ℕ} → (i : Fin2 n) → MvQPF (MvQPF.Prj i)
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.cramer_transpose_apply : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
  (b : n → α) (i : n), A.transpose.cramer b i = (A.updateRow i b).det
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_one : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (m : M), IsLocalizedModule.mk' f m 1 = f m
-- Mathlib.Control.EquivFunctor
EquivFunctor.mapEquiv.injective : ∀ (f : Type u₀ → Type u₁) [inst : Applicative f] [inst_1 : LawfulApplicative f] {α β : Type u₀},
  (∀ (γ : Type u₀), Function.Injective pure) → Function.Injective (EquivFunctor.mapEquiv f)
-- Mathlib.Order.Filter.Prod
Filter.top_prod : ∀ {α : Type u_1} {β : Type u_2} {g : Filter β}, ⊤ ×ˢ g = Filter.comap Prod.snd g
-- Mathlib.Data.Finset.Insert
Finset.pairwise_cons : ∀ {α : Type u_1} {s : Finset α} {a : α} (ha : a ∉ s) (r : α → α → Prop),
  Pairwise (Function.onFun r fun a_1 => ↑a_1) ↔ Pairwise (Function.onFun r fun a => ↑a) ∧ ∀ b ∈ s, r a b ∧ r b a
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.instL1NormedSpace : (𝕜 : Type u_1) →
  {R : Type u_3} →
    {M : Type u_4} →
      [inst : NormedField 𝕜] →
        [inst_1 : NormedRing R] →
          [inst_2 : NormedAddCommGroup M] → [NormedAlgebra 𝕜 R] → [NormedSpace 𝕜 M] → NormedSpace 𝕜 (TrivSqZeroExt R M)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.comp_base : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
/-- If `P` holds for `f` over affine opens `U₂` of `Y` and `V₂` of `X` and `U₁` (resp. `V₁`) are
open neighborhoods of `x` (resp. `f.base x`), then `P` also holds for `f` over some affine open
`U'` of `Y` (resp. `V'` of `X`) that is contained in `U₁` (resp. `V₁`).  -/
AlgebraicGeometry.exists_affineOpens_le_appLE_of_appLE : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {X Y : AlgebraicGeometry.Scheme}
  {f : X ⟶ Y},
  (RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P) →
      ∀ (x : ↥X) (U₁ : Y.Opens) (U₂ : ↑Y.affineOpens) (V₁ : X.Opens) (V₂ : ↑X.affineOpens),
        x ∈ V₁ →
          x ∈ ↑V₂ →
            ∀ (e₂ : ↑V₂ ≤ (TopologicalSpace.Opens.map f.base).obj ↑U₂),
              P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) →
                f x ∈ U₁.carrier →
                  ∃ U' V',
                    ∃ (_ : ↑U' ≤ U₁) (_ : ↑V' ≤ V₁) (_ : x ∈ ↑V') (e :
                      ↑V' ≤ (TopologicalSpace.Opens.map f.base).obj ↑U'),
                      P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f (↑U') (↑V') e))
-- Init.Data.List.MapIdx
List.mapFinIdx_reverse : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : ℕ) → α → i < l.reverse.length → β},
  l.reverse.mapFinIdx f = (l.mapFinIdx fun i a h => f (l.length - 1 - i) a ⋯).reverse
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- Any two projective resolutions are homotopy equivalent.  -/
CategoryTheory.ProjectiveResolution.homotopyEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X : C} → (P Q : CategoryTheory.ProjectiveResolution X) → HomotopyEquiv P.complex Q.complex
-- Init.GrindInstances.Ring.Int
Lean.Grind.instIsCharPIntOfNatNat : Lean.Grind.IsCharP ℤ 0
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y : CategoryTheory.Dial C} (f : X.src ⟶ Y.src)
  (F : X.src ⨯ Y.tgt ⟶ X.tgt)
  (le :
    (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst F)).obj X.rel ≤
      (CategoryTheory.Subobject.pullback
            (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id Y.tgt))).obj
        Y.rel)
  (f_1 : X.src ⟶ Y.src) (F_1 : X.src ⨯ Y.tgt ⟶ X.tgt)
  (le_1 :
    (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst F_1)).obj X.rel ≤
      (CategoryTheory.Subobject.pullback
            (CategoryTheory.Limits.prod.map f_1 (CategoryTheory.CategoryStruct.id Y.tgt))).obj
        Y.rel),
  ({ f := f, F := F, le := le } = { f := f_1, F := F_1, le := le_1 }) = (f = f_1 ∧ F = F_1)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_add_right_singleton : ∀ {α : Type u_2} [inst : AddGroup α] {a b : α}, (fun x => x + a) ⁻¹' {b} = {b + -a}
-- Mathlib.RingTheory.Regular.IsSMulRegular
isSMulRegular_quotient_iff_mem_of_smul_mem : ∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  (r : R), IsSMulRegular (M ⧸ N) r ↔ ∀ (x : M), r • x ∈ N → x ∈ N
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.not_bddAbove_isInitial : ¬BddAbove {x | x.IsInitial}
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv_symm_apply_as : ∀ {C : Type u} (as : C), (CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv.symm as).as = as
-- Std.Do.PostCond
/-- Conjunction of exception assertions is defined as pointwise conjunction of the assertions for each
potential exception.
 -/
Std.Do.ExceptConds.and : {ps : Std.Do.PostShape} → Std.Do.ExceptConds ps → Std.Do.ExceptConds ps → Std.Do.ExceptConds ps
-- Mathlib.Algebra.Group.Action.Sum
Sum.vadd_inr : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst_1 : VAdd M β] (a : M) (c : β),
  a +ᵥ Sum.inr c = Sum.inr (a +ᵥ c)
-- Mathlib.Order.WellFoundedSet
Set.partiallyWellOrderedOn_insert : ∀ {α : Type u_2} {r : α → α → Prop} {s : Set α} {a : α} [Std.Refl r],
  (insert a s).PartiallyWellOrderedOn r ↔ s.PartiallyWellOrderedOn r
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.HomologyMapData.smul_right : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)
  (a : R), (γ.smul a).right = γ.right.smul a
-- Mathlib.Algebra.Order.Monoid.Basic
/-- The order embedding sending `b` to `a * b`, for some fixed `a`.
See also `OrderIso.mulLeft` when working in an ordered group.  -/
OrderEmbedding.mulLeft : {α : Type u_2} → [inst : Mul α] → [inst_1 : LinearOrder α] → [MulLeftStrictMono α] → α → α ↪o α
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : β k → β k}, (m.modify k f).get? k' = if h : (k == k') = true then cast ⋯ (Option.map f (m.get? k)) else m.get? k'
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.sectionOfCone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  (c : CategoryTheory.Limits.Cone F) (x : c.pt),
  CategoryTheory.Limits.Types.sectionOfCone c x = ⟨fun j => (CategoryTheory.ConcreteCategory.hom (c.π.app j)) x, ⋯⟩
-- Mathlib.Computability.Primrec.Basic
Primrec.sumCasesOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β]
  [inst_2 : Primcodable γ] [inst_3 : Primcodable σ] {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ → σ},
  Primrec f → Primrec₂ g → Primrec₂ h → Primrec fun a => Sum.casesOn (f a) (g a) (h a)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonClientCapabilities : Lean.ToJson Lean.Lsp.ClientCapabilities
-- Mathlib.Topology.Compactness.Compact
Topology.IsClosedEmbedding.compactSpace : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [h : CompactSpace Y] {f : X → Y},
  Topology.IsClosedEmbedding f → CompactSpace X
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.instFunLike.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] [inst_1 : SupSet β],
  sSupHom.instFunLike = { coe := sSupHom.toFun, coe_injective := ⋯ }
-- Mathlib.Analysis.Normed.Field.UnitBall
/-- Closed unit ball in a seminormed ring as a bundled `Submonoid`.  -/
Submonoid.unitClosedBall : (𝕜 : Type u_2) → [inst : SeminormedRing 𝕜] → [NormOneClass 𝕜] → Submonoid 𝕜
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.toRange_ι : ∀ {X Y : SSet} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.toRange f) (SSet.Subcomplex.range f).ι = f
-- Mathlib.NumberTheory.Bernoulli
bernoulli'_spec' : ∀ (n : ℕ), ∑ k ∈ Finset.HasAntidiagonal.antidiagonal n, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli' k.1 = 1
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Formula for `cosZeta` as a Dirichlet series in the convergence range, with sum over `ℕ`.  -/
HurwitzZeta.hasSum_nat_cosZeta : ∀ (a : ℝ) {s : ℂ}, 1 < s.re → HasSum (fun n => ↑(Real.cos (2 * Real.pi * a * ↑n)) / ↑n ^ s) (HurwitzZeta.cosZeta (↑a) s)
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_right_split_dvd_cert.eq_1 : ∀ (p₂ p' : Int.Internal.Linear.Poly) (b k : ℤ),
  Int.Internal.Linear.cooper_right_split_dvd_cert p₂ p' b k =
    (b.beq' p₂.leadCoeff).and' (p'.beq' (p₂.tail.addConst_k k))
-- Mathlib.Algebra.Homology.QuasiIso
HomologicalComplex.instRespectsIsoQuasiIso : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.CategoryWithHomology C], (HomologicalComplex.quasiIso C c).RespectsIso
-- Mathlib.SetTheory.Ordinal.Basic
/-- A "canonical" type order-isomorphic to the ordinal `o`, living in the same universe. This is
defined through the axiom of choice; in particular, it has no useful def-eqs, and it is not exposed.

Use this over `Iio o` only when it is paramount to have a `Type u` rather than a `Type (u + 1)`,
and convert using

```
Ordinal.ToType.mk : Iio o → o.ToType
Ordinal.ToType.toOrd : o.ToType → Iio o
```
 -/
Ordinal.ToType : Ordinal.{u} → Type u
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.S.eq_1 : ∀ (l : Type u_4) (R : Type u₂) [inst : DecidableEq l] [inst_1 : CommRing R],
  LieAlgebra.Orthogonal.S l R = LieAlgebra.Orthogonal.indefiniteDiagonal l l R
-- Mathlib.Data.Set.Lattice.Image
Set.bijective_iff_bijective_of_iUnion_eq_univ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β} {U : ι → Set β},
  Set.iUnion U = Set.univ → (Function.Bijective f ↔ ∀ (i : ι), Function.Bijective ((U i).restrictPreimage f))
-- Std.Time.Time.PlainTime
/-- Creates a `PlainTime` value representing midnight (00:00:00.000000000).
 -/
Std.Time.PlainTime.midnight : Std.Time.PlainTime
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.infty_coeFn_pow : ∀ {I : Type u_5} {B : I → Type u_6} [inst : (i : I) → NormedRing (B i)] [inst_1 : ∀ (i : I), NormOneClass (B i)]
  (f : ↥(lp B ⊤)) (n : ℕ), ↑(f ^ n) = ↑f ^ n
-- Mathlib.SetTheory.Cardinal.Finite
Nat.cast_card : ∀ {α : Type u_1} [Finite α], ↑(Nat.card α) = Cardinal.mk α
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
Algebra.cast.eq_1 : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Algebra.cast = ⇑(algebraMap R A)
-- Mathlib.Analysis.Normed.Module.Basic
/-- The product of finitely many normed algebras is a normed algebra, with the sup norm.  -/
Pi.normedAlgebra : (𝕜 : Type u_1) →
  [inst : NormedField 𝕜] →
    {ι : Type u_6} →
      {E : ι → Type u_7} →
        [inst_1 : Fintype ι] →
          [inst_2 : (i : ι) → SeminormedRing (E i)] →
            [(i : ι) → NormedAlgebra 𝕜 (E i)] → NormedAlgebra 𝕜 ((i : ι) → E i)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.getRatClauseIndices.eq_1 : ∀ {n : ℕ} (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)))
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.getRatClauseIndices clauses l =
    Array.filter
      (fun i =>
        match clauses[i]! with
        | none => false
        | some c => c.contains l.negate)
      (Array.range clauses.size)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_sum_eq_of_lt : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {ι : Type u_7} [inst_2 : DecidableEq ι] {s : Finset ι} {f : ι → R} {j : ι},
  j ∈ s → (∀ i ∈ s \ {j}, v (f i) < v (f j)) → v (∑ i ∈ s, f i) = v (f j)
-- Mathlib.CategoryTheory.Limits.Creates
/-- `F` creates limits of shape `J` if `F` creates the limit of any diagram
`K : J ⥤ C`.
 -/
CategoryTheory.CreatesLimitsOfShape : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) →
          [CategoryTheory.Category.{w', w} J] →
            CategoryTheory.Functor C D → Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')
-- Mathlib.LinearAlgebra.Determinant
LinearMap.isUnit_iff_isUnit_det : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  [Module.Free R M] (f : M →ₗ[R] M), IsUnit f ↔ IsUnit (LinearMap.det f)
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.hasCokernel_of_admissibleMorphism : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [inst_6 : CategoryTheory.Category.{v_2, u_2} A]
  {ι : CategoryTheory.Functor A C},
  (∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (CategoryTheory.shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) →
    ∀ [inst_7 : CategoryTheory.Preadditive A] [ι.Full] [ι.Faithful] {X₁ X₂ : A} (f₁ : X₁ ⟶ X₂),
      CategoryTheory.Triangulated.AbelianSubcategory.admissibleMorphism ι f₁ → CategoryTheory.Limits.HasCokernel f₁
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.eval₂_C_X_eq_coe : ∀ {R : Type u_1} [inst : Semiring R] {φ : Polynomial R}, Polynomial.eval₂ PowerSeries.C PowerSeries.X φ = ↑φ
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.sndL_comp_coe_orthogonalDecomposition : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection],
  WithLp.sndL 2 𝕜 ↥K ↥Kᗮ ∘SL ↑↑K.orthogonalDecomposition = Kᗮ.orthogonalProjectionOnto