mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.asIsoHomologyπ_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [inst_2 : S.HasHomology], (S.asIsoHomologyπ hf).hom = S.homologyπ
-- Mathlib.Order.Category.PartOrd
/-- **Alias** of `CategoryTheory.ConcreteCategory.forget_map_eq_ofHom`. -/
PartOrd.forget_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.forget C).map f = TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_insertList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l toInsert : List ((a : α) × β a)},
  (Std.Internal.List.insertList l toInsert).isEmpty = (l.isEmpty && toInsert.isEmpty)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instSubtractionMonoid : {α : Type u_1} → [SubtractionMonoid α] → SubtractionMonoid (Lex α)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.congr_trans : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} {E : Type uE} {F : Type uF}
  [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A]
  [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B]
  [inst_9 : Semiring C] [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C]
  [inst_13 : Semiring D] [inst_14 : Algebra R D] [inst_15 : Semiring E] [inst_16 : Algebra R E] [inst_17 : Algebra S E]
  [inst_18 : IsScalarTower R S E] [inst_19 : Semiring F] [inst_20 : Algebra R F] (f₁ : A ≃ₐ[S] C) (f₂ : C ≃ₐ[S] E)
  (g₁ : B ≃ₐ[R] D) (g₂ : D ≃ₐ[R] F),
  Algebra.TensorProduct.congr (f₁.trans f₂) (g₁.trans g₂) =
    (Algebra.TensorProduct.congr f₁ g₁).trans (Algebra.TensorProduct.congr f₂ g₂)
-- Mathlib.Data.Set.Basic
Set.Nonempty.to_type : ∀ {α : Type u} {s : Set α}, s.Nonempty → Nonempty α
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_ker_self : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), Subgroup.map f f.ker = ⊥
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntry!ₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Inhabited ((a : α) × β a)] (l : Std.DTreeMap.Internal.Impl α β)
  (k : α), l.getEntry!ₘ k = (l.getEntry?ₘ k).get!
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_mk : ∀ {R : Type u} {M : Type v} (r : R) (m : M), TrivSqZeroExt.fst (r, m) = r
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_ι_assoc : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (U : ↑X.affineOpens)
  {Z : AlgebraicGeometry.Scheme} (h_1 : ↑↑U ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom h U)
      (CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) h_1) =
    CategoryTheory.CategoryStruct.comp (J.glueDataObjι U) h_1
-- Mathlib.Topology.Algebra.Group.Basic
mem_closure_iff_nhds_one : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {x : G} {s : Set G},
  x ∈ closure s ↔ ∀ U ∈ nhds 1, ∃ y ∈ s, y / x ∈ U
-- Lean.LocalContext
Lean.MonadLCtx.mk : {m : Type → Type} → m Lean.LocalContext → Lean.MonadLCtx m
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.tensorObj_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A B : C) [inst_3 : CategoryTheory.ComonObj A]
  [inst_4 : CategoryTheory.ComonObj B],
  CategoryTheory.ComonObj.counit =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.counit CategoryTheory.ComonObj.counit)
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
ContinuousAlternatingMap.constOfIsEmptyLIE.congr_simp : ∀ (𝕜 : Type u) (E : Type wE) (F : Type wF) (ι : Type v) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] [inst_6 : IsEmpty ι],
  ContinuousAlternatingMap.constOfIsEmptyLIE 𝕜 E F ι = ContinuousAlternatingMap.constOfIsEmptyLIE 𝕜 E F ι
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.id_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.Comonad.id C).map f = f
-- Std.Http.Protocol.H1
/-- Processes a fixed-size body when remaining size is zero.

Accepts completion only when producer has closed and no extra bytes are queued;
otherwise treats queued bytes as protocol error.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.processFixedZeroBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Data.Sign.Defs
_private.Mathlib.Data.Sign.Defs.0.SignType.fin3Equiv.match_1.eq_2 : ∀ (motive : SignType → Sort u_1) (h_1 : Unit → motive SignType.zero) (h_2 : Unit → motive SignType.pos)
  (h_3 : Unit → motive SignType.neg),
  (match SignType.pos with
    | SignType.zero => h_1 ()
    | SignType.pos => h_2 ()
    | SignType.neg => h_3 ()) =
    h_2 ()
-- Std.Data.DHashMap.RawLemmas
_private.Std.Data.DHashMap.RawLemmas.0.Std.DHashMap.Raw.insertIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β) (a : α) (b : β a),
  m.insertIfNew a b = if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.insertIfNew ⟨m, h⟩ a b) else m
-- Init.Data.Format.Basic
Std.Format.FlattenAllowability.allow.injEq : ∀ (fits fits_1 : Bool),
  (Std.Format.FlattenAllowability.allow fits = Std.Format.FlattenAllowability.allow fits_1) = (fits = fits_1)
-- Mathlib.Analysis.LConvolution
/-- Convolution is commutative when the group is commutative.  -/
MeasureTheory.mlconvolution_comm : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : CommGroup G] [MeasurableMul₂ G] [MeasurableInv G]
  {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] [μ.IsInvInvariant] {f g : G → ENNReal},
  MeasureTheory.mlconvolution f g μ = MeasureTheory.mlconvolution g f μ
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.instInhabitedInitResults : {α : Type} → Inhabited (Lean.Meta.LazyDiscrTree.InitResults α)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- If `G` preserves cokernels and `C` has them, then the cofork constructed of the mapped morphisms of
a cokernel cofork is a colimit.
 -/
CategoryTheory.Limits.isColimitOfHasCokernelOfPreservesColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (G : CategoryTheory.Functor C D) →
              [inst_4 : G.PreservesZeroMorphisms] →
                {X Y : C} →
                  (f : X ⟶ Y) →
                    [inst_5 : CategoryTheory.Limits.HasCokernel f] →
                      [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G] →
                        CategoryTheory.Limits.IsColimit
                          (CategoryTheory.Limits.Cofork.ofπ (G.map (CategoryTheory.Limits.cokernel.π f)) ⋯)
-- Init.Prelude
/-- Reader monads provide the ability to implicitly thread a value through a computation. The value can
be read, but not written. A `MonadWithReader ρ` instance additionally allows the value to be locally
overridden for a sub-computation.

In this class, `ρ` is an `outParam`, which means that it is inferred from `m`. `MonadReaderOf ρ`
provides the same operations, but allows `ρ` to influence instance synthesis.
 -/
MonadReader : outParam (Type u) → (Type u → Type v) → Type v
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mk_injective : ∀ {M : Type u_1} [inst : Monoid M] [Subsingleton Mˣ], Function.Injective Associates.mk
-- Mathlib.LinearAlgebra.Span.Basic
/-- The range of `toSpanSingleton x` is the span of `x`.  -/
LinearMap.range_toSpanSingleton : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  (LinearMap.toSpanSingleton R M x).range = R ∙ x
-- Init.Data.String.Lemmas.Slice
String.Slice.front?_eq : ∀ {s : String.Slice}, s.front? = s.copy.toList.head?
-- Init.Data.Slice.List.Lemmas
List.toArray_mkSlice_rii_eq_toArray_mkSlice_rco : ∀ {α : Type u_1} {xs : List α},
  Std.Slice.toArray (Std.Rii.Sliceable.mkSlice xs *...*) =
    Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs 0...xs.length)
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `add_apply`. -/
CuspForm.add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.inducing_coe : ∀ {K : Type u_2} [inst : Field K], IsUniformInducing ⇑(algebraMap (RatFunc K) (LaurentSeries K))
-- Mathlib.Data.PEquiv
PEquiv.inj : ∀ {α : Type u} {β : Type v} (f : α ≃. β) {a₁ a₂ : α} {b : β}, b ∈ f a₁ → b ∈ f a₂ → a₁ = a₂
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
Rat.HeightOneSpectrum.valuation_equiv_padicValuation : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : Algebra R ℚ] [inst_2 : IsIntegralClosure R ℤ ℚ]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R ℚ] (v : IsDedekindDomain.HeightOneSpectrum R),
  (IsDedekindDomain.HeightOneSpectrum.valuation ℚ v).IsEquiv (Rat.padicValuation ↑(Rat.HeightOneSpectrum.primesEquiv v))
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- If `μ` is σ-finite it has finite spanning sets in the collection of all measurable sets.  -/
MeasureTheory.Measure.toFiniteSpanningSetsIn : {α : Type u_1} →
  {m0 : MeasurableSpace α} →
    (μ : MeasureTheory.Measure α) → [h : MeasureTheory.SigmaFinite μ] → μ.FiniteSpanningSetsIn {s | MeasurableSet s}
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.deriv_add_eq_mul_omega0_add : ∀ (a b : Ordinal.{u}), Ordinal.deriv (fun x => a + x) b = a * Ordinal.omega0 + b
-- Mathlib.Algebra.Group.Defs
npowBinRec_zero : ∀ {M : Type u_2} [inst : Mul M] [inst_1 : One M] (m : M), npowBinRec 0 m = 1
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- The *structure map* of the restricted product is the obvious inclusion from `Π i, A i`
into `Πʳ i, [R i, A i]_[𝓕]`.  -/
RestrictedProduct.structureMap : {ι : Type u_1} →
  (R : ι → Type u_2) →
    (A : (i : ι) → Set (R i)) → (𝓕 : Filter ι) → ((i : ι) → ↑(A i)) → RestrictedProduct (fun i => R i) (fun i => A i) 𝓕
-- Mathlib.Data.FP.Basic
FP.emin : [C : FP.FloatCfg] → ℤ
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.instInhabitedSimpCongrTheorem : Inhabited Lean.Meta.SimpCongrTheorem
-- Init.Grind.ToInt
/-- The embedding into the integers takes `0` to `0`.
 -/
Lean.Grind.ToInt.Zero : (α : Type u) → [Zero α] → (I : outParam Lean.Grind.IntInterval) → [Lean.Grind.ToInt α I] → Prop
-- Init.GrindInstances.ToInt
Lean.Grind.instLEInt8SintOfNatNat : Lean.Grind.ToInt.LE Int8 (Lean.Grind.IntInterval.sint 8)
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.typeEquiv_inverse_obj : ∀ (X : CategoryTheory.Sheaf CategoryTheory.typesGrothendieckTopology (Type u)),
  CategoryTheory.typeEquiv.inverse.obj X = X.obj.obj (Opposite.op PUnit.{u + 1})
-- Mathlib.Algebra.Module.PointwisePi
smul_pi : ∀ {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [inst : Group K] [inst_1 : (i : ι) → MulAction K (R i)] (r : K)
  (S : Set ι) (t : (i : ι) → Set (R i)), r • S.pi t = S.pi (r • t)
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- **Alias** of `LinearOrderedCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete`. -/
LinearOrderedCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [Nontrivial G] {g : G},
  ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.instMulRightMono : ∀ {α : Type u_2} [inst : Mul α], MulRightMono (Set α)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- `Semiring` instance for `type`  -/
Lean.Meta.Grind.Arith.CommRing.Semiring.semiringInst : Lean.Meta.Grind.Arith.CommRing.Semiring → Lean.Expr
-- Mathlib.Order.WellFounded
WellFounded.min_mem : ∀ {α : Type u_1} {r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : s.Nonempty), H.min s h ∈ s
-- Std.Time.Format.Modifier
Std.Time.Year.extended.injEq : ∀ (num num_1 : ℕ), (Std.Time.Year.extended num = Std.Time.Year.extended num_1) = (num = num_1)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.toLinearMap_rTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E →L[𝕜] F),
  ↑(ContinuousLinearMap.rTensor G f) = LinearMap.rTensor G ↑f
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.unit_hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [hasDayConvolution :
    ∀ (F G : CategoryTheory.Functor C V),
      (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
        (CategoryTheory.MonoidalCategory.externalProduct F G)]
  [hasDayConvolutionUnit :
    (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
      (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))]
  [inst_4 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.Functor.id C).prod
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  {F : CategoryTheory.MonoidalCategory.DayFunctor C V}
  {α β : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.MonoidalCategory.DayFunctor C V) ⟶ F},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayFunctor.ν C V)
        (α.natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayFunctor.ν C V)
        (β.natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) →
    α = β
-- Init.Data.String.Lemmas.Order
String.Pos.sliceFrom_le_iff : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h : p₀ ≤ q},
  p₀.sliceFrom q h ≤ p ↔ q ≤ String.Pos.ofSliceFrom p
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocInfo.mk.injEq : ∀ (toElabInfo toElabInfo_1 : Lean.Elab.ElabInfo),
  ({ toElabInfo := toElabInfo } = { toElabInfo := toElabInfo_1 }) = (toElabInfo = toElabInfo_1)
-- Mathlib.Order.Defs.LinearOrder
not_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ¬a ≤ b ↔ b < a
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.top_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M), ⊤ ∈ f.invtSubmodule
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- If `α` is a natural transformation between left adjoints whose conjugate natural transformation
is an isomorphism, then `α` is an isomorphism. The converse is given in `conjugateEquiv_iso`.
 -/
CategoryTheory.conjugateEquiv_of_iso : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (α : L₂ ⟶ L₁) [CategoryTheory.IsIso ((CategoryTheory.conjugateEquiv adj₁ adj₂) α)], CategoryTheory.IsIso α
-- Init.Data.Rat.Lemmas
Rat.le_total : ∀ {a b : ℚ}, a ≤ b ∨ b ≤ a
-- Init.MetaTypes
Lean.Meta.instBEqOccurrences : BEq Lean.Meta.Occurrences
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.typed.injEq : ∀ (ref : Lean.Syntax) (a : Lean.Elab.Tactic.RCases.RCasesPatt) (a_1 : Lean.Term) (ref_1 : Lean.Syntax)
  (a_2 : Lean.Elab.Tactic.RCases.RCasesPatt) (a_3 : Lean.Term),
  (Lean.Elab.Tactic.RCases.RCasesPatt.typed ref a a_1 = Lean.Elab.Tactic.RCases.RCasesPatt.typed ref_1 a_2 a_3) =
    (ref = ref_1 ∧ a = a_2 ∧ a_1 = a_3)
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.EndpointIdent.mk : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜] {p a : 𝕜}
  [hp : Fact (0 < p)], AddCircle.EndpointIdent p a ⟨a, ⋯⟩ ⟨a + p, ⋯⟩
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.HoldsForLocalization.isLocalizationMap : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S]
  {P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop},
  (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P) →
      (RingHom.HoldsForLocalization fun {R S} [CommRing R] [CommRing S] => P) →
        ∀ {M : Submonoid R} {T : Submonoid S} {R' : Type u} [inst_2 : CommRing R'] [inst_3 : Algebra R R']
          [inst_4 : IsLocalization M R'] (S' : Type u) [inst_5 : CommRing S'] [inst_6 : Algebra S S']
          [inst_7 : IsLocalization T S'] {f : R →+* S} (hy : M ≤ Submonoid.comap f T),
          P f → P (IsLocalization.map S' f hy)
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.IsTrivial.eq_1 : ∀ {α : Type u_1} (H : Hypergraph α), H.IsTrivial = (H.vertexSet.Nonempty ∧ H.edgeSet = ∅)
-- Mathlib.Data.Nat.Factorization.Root
Nat.floorRoot_one_right : ∀ {n : ℕ}, n ≠ 0 → n.floorRoot 1 = 1
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.toThinSkeleton_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.toThinSkeleton C).map f = CategoryTheory.homOfLE ⋯
-- Mathlib.NumberTheory.ModularForms.Derivative
Derivative.normalizedDerivOfComplex_neg : ∀ (F : UpperHalfPlane → ℂ), MDiff F → Derivative.normalizedDerivOfComplex (-F) = -Derivative.normalizedDerivOfComplex F
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.instAlgebraAdicCauchySequence : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → Algebra R (AdicCompletion.AdicCauchySequence I R)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
/-- An arbitrary pair of subsets witnessing the non-uniformity of `(s, t)`. If `(s, t)` is uniform,
returns `(s, t)`. Witnesses for `(s, t)` and `(t, s)` don't necessarily match. See
`SimpleGraph.nonuniformWitness`.  -/
SimpleGraph.nonuniformWitnesses : {α : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : Field 𝕜] →
      [inst_1 : LinearOrder 𝕜] →
        [IsStrictOrderedRing 𝕜] →
          (G : SimpleGraph α) → [DecidableRel G.Adj] → 𝕜 → Finset α → Finset α → Finset α × Finset α
-- Init.Data.Ord.Basic
List.compare_nil_nil : ∀ {α : Type u_1} [inst : Ord α], compare [] [] = Ordering.eq
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndepOn.linearIndependent : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {s : Set ι}, LinearIndepOn R v s → LinearIndependent R fun (x : ↑s) => v ↑x
-- Mathlib.Algebra.Group.Pi.Basic
Function.extend_mul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Mul γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ),
  Function.extend f (g₁ * g₂) (e₁ * e₂) = Function.extend f g₁ e₁ * Function.extend f g₂ e₂
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {x y : S.Arrow}, x.Y = y.Y → x.f ≍ y.f → x = y
-- Init.Data.Option.Lemmas
Option.min_filter_left : ∀ {α : Type u_1} [inst : Min α] [Std.IdempotentOp min] {p : α → Bool} {o : Option α},
  Option.filter p o ⊓ o = Option.filter p o
-- Mathlib.RingTheory.Finiteness.Defs
Module.Finite.iff_addMonoid_fg : ∀ {M : Type u_6} [inst : AddCommMonoid M], Module.Finite ℕ M ↔ AddMonoid.FG M
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.mk : {α : Type u₁} → α → CategoryTheory.Discrete α
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extMk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (α : CategoryTheory.Abelian.Ext X Y n) (m : ℕ) (hm : n + 1 = m),
  ∃ f, ∃ (hf : CategoryTheory.CategoryStruct.comp f (R.cocomplex.d n m) = 0), R.extMk f m hm hf = α
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.nsmul_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C} (f : P ⟶ Q)
  (g : Q ⟶ R) (n : ℕ), CategoryTheory.CategoryStruct.comp (n • f) g = n • CategoryTheory.CategoryStruct.comp f g
-- Mathlib.Algebra.Jordan.Basic
IsCommJordan.mk : ∀ {A : Type u_1} [inst : CommMagma A], (∀ (a b : A), a * b * (a * a) = a * (b * (a * a))) → IsCommJordan A
-- Mathlib.Analysis.Complex.RealDeriv
HasDerivWithinAt.ofReal_comp : ∀ {z : ℝ} {f : ℝ → ℝ} {s : Set ℝ} {u : ℝ}, HasDerivWithinAt f u s z → HasDerivWithinAt (fun y => ↑(f y)) (↑u) s z
-- Mathlib.Analysis.Normed.Group.Uniform
AddMonoidHomClass.uniformContinuous_of_bound : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
  [inst_2 : FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ),
  (∀ (x : E), ‖f x‖ ≤ C * ‖x‖) → UniformContinuous ⇑f
-- Mathlib.Computability.TuringMachine.Tape
Turing.PointedMap.mk.sizeOf_spec : ∀ {Γ : Type u} {Γ' : Type v} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] [inst_2 : SizeOf Γ] [inst_3 : SizeOf Γ']
  (f : Γ → Γ') (map_pt' : f default = default), sizeOf { f := f, map_pt' := map_pt' } = 1 + sizeOf map_pt'