mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.AffineMonoid.Basic
/-- An affine monoid is a finitely generated cancellative torsion-free commutative monoid.  -/
IsAffineAddMonoid : (M : Type u_1) → [AddCommMonoid M] → Prop
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_atTop_zero_iff_lt_of_antitone : ∀ {β : Type u_4} [Nonempty β] [inst : SemilatticeSup β] {f : β → ENNReal},
  Antitone f → (Filter.Tendsto f Filter.atTop (nhds 0) ↔ ∀ (ε : ENNReal), 0 < ε → ∃ n, f n < ε)
-- Mathlib.Topology.Compactification.StoneCech
preStoneCechCompat : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type v} [inst_1 : TopologicalSpace β] [T2Space β] [CompactSpace β]
  {g : α → β},
  Continuous g →
    ∀ {F G : Ultrafilter α} {x : α}, ↑F ≤ nhds x → ↑G ≤ nhds x → Ultrafilter.extend g F = Ultrafilter.extend g G
-- Init.Data.UInt.Bitwise
UInt8.and_lt_add_one : ∀ {b c : UInt8}, c ≠ -1 → b &&& c < c + 1
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
/-- If `C` has an initial object and binary coproducts, then it has finite coproducts.  -/
CategoryTheory.hasFiniteCoproducts_of_has_binary_and_initial : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C]
  [CategoryTheory.Limits.HasInitial C], CategoryTheory.Limits.HasFiniteCoproducts C
-- Mathlib.Order.WithBot
WithTop.distribLattice : {α : Type u_1} → [DistribLattice α] → DistribLattice (WithTop α)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constMaxEntryD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {fallback : α × β}, t₁.Equiv t₂ → Std.DTreeMap.Const.maxEntryD t₁ fallback = Std.DTreeMap.Const.maxEntryD t₂ fallback
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.getLoogleQueryJson : String → optParam ℕ 6 → Lean.CoreM LeanSearchClient.LoogleResult
-- Init.Data.Int.Linear
Int.Internal.Linear.unsatEqDivCoeffCert.eq_1 : ∀ (lhs rhs : Int.Internal.Linear.Expr) (k : ℤ),
  Int.Internal.Linear.unsatEqDivCoeffCert lhs rhs k =
    (Int.Internal.Linear.Poly.divCoeffs k (lhs.sub rhs).norm).and'
      ((Int.blt' 0 k).and' (decide (Int.Internal.Linear.cmod (lhs.sub rhs).norm.getConst k < 0)))
-- Init.Data.Sum.Lemmas
Sum.lex_wf : ∀ {α : Type u_1} {r : α → α → Prop} {α_1 : Type u_2} {s : α_1 → α_1 → Prop},
  WellFounded r → WellFounded s → WellFounded (Sum.Lex r s)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- A morphism of presheaves of modules is locally surjective
if the underlying morphism of presheaves of abelian groups is.  -/
PresheafOfModules.IsLocallySurjective : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.GrothendieckTopology C →
      {R : CategoryTheory.Functor Cᵒᵖ RingCat} → {M₁ M₂ : PresheafOfModules R} → (M₁ ⟶ M₂) → Prop
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.Entry.mk.sizeOf_spec : ∀ (name : Lean.Name) (info : Lean.Meta.MatcherInfo),
  sizeOf { name := name, info := info } = 1 + sizeOf name + sizeOf info
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_dvd_iff_primeFactors_subset : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M},
  b ≠ 0 →
    (UniqueFactorizationMonoid.radical a ∣ b ↔
      UniqueFactorizationMonoid.primeFactors a ⊆ UniqueFactorizationMonoid.primeFactors b)
-- Mathlib.Algebra.Group.TransferInstance
Equiv.inv_def : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Inv β] (x : α), x⁻¹ = e.symm (e x)⁻¹
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionEqualizerProducts.res_π_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (i : ι) {F_1 : C → C → Type uF}
  {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F_1 X Y) (carrier X) (carrier Y)}
  [inst_2 : CategoryTheory.ConcreteCategory C F_1] (x : carrier (F.obj (Opposite.op (iSup U)))),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun i => F.obj (Opposite.op (U i)))
          { as := i }))
      ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.SheafConditionEqualizerProducts.res F U)) x) =
    (CategoryTheory.ConcreteCategory.hom (F.map (TopologicalSpace.Opens.leSupr U i).op)) x
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- Let `S` be an `S₀`-algebra. Then `S`-modules are modules over `S₀`.
 -/
ModuleCat.Algebra.instModuleCarrier : {S₀ : Type u₀} →
  [inst : CommSemiring S₀] → {S : Type u} → [inst_1 : Ring S] → [Algebra S₀ S] → {M : ModuleCat S} → Module S₀ ↑M
-- Mathlib.NumberTheory.Real.Irrational
irrational_add_natCast_iff : ∀ {n : ℕ} {x : ℝ}, Irrational (x + ↑n) ↔ Irrational x
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.centeredArc.eq_1 : ∀ (r : ℝ), Circle.centeredArc r = ⇑Circle.exp '' {x | |x| < r}
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_nhds_top : ∀ {α : Type u_1} {m : α → ENNReal} {f : Filter α}, (∀ (n : ℕ), ∀ᶠ (a : α) in f, ↑n < m a) → Filter.Tendsto m f (nhds ⊤)
-- Mathlib.FieldTheory.Galois.Profinite
/-- The homomorphism from `Gal(K/k)` to `lim Gal(L/k)` where `L` is a
`FiniteGaloisIntermediateField k K` ordered by inverse inclusion. It is induced by the
canonical projections from `Gal(K/k)` to `Gal(L/k)`.
 -/
InfiniteGalois.algEquivToLimit : (k : Type u_3) →
  (K : Type u_4) →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] →
          Gal(K/k) →* ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
-- Mathlib.Order.WithBot
WithTop.coe_bot : ∀ {α : Type u_1} [inst : Bot α], ↑⊥ = ⊥
-- Mathlib.Data.Part
Part.mem_assert : ∀ {α : Type u_1} {p : Prop} {f : p → Part α} {a : α} (h : p), a ∈ f h → a ∈ Part.assert p f
-- Mathlib.Computability.DFA
/-- A transition function from state to state labelled by the alphabet.  -/
DFA.step : {α : Type u} → {σ : Type v} → DFA α σ → σ → α → σ
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.rightOpWhiskerRight_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ D} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {H : CategoryTheory.Functor D E} (α : F ⟶ G) {Z : CategoryTheory.Functor C Eᵒᵖ} (h : (F.comp H).rightOp ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightOp (CategoryTheory.Functor.whiskerRight α H)) h =
    CategoryTheory.CategoryStruct.comp (G.rightOpComp H).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.rightOp α) H.op)
        (CategoryTheory.CategoryStruct.comp (F.rightOpComp H).inv h))
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_support_card_lt : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f ≠ 0 → f.eraseLead.support.card < f.support.card
-- Mathlib.FieldTheory.Finite.GaloisField
/-- Uniqueness of finite fields:
Any two finite fields of the same cardinality are (possibly noncanonically) isomorphic  -/
FiniteField.algEquivOfCardEq : {K : Type u_1} →
  {K' : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field K'] →
        [inst_2 : Fintype K] →
          [inst_3 : Fintype K'] →
            (p : ℕ) →
              [h_prime : Fact (Nat.Prime p)] →
                [inst_4 : Algebra (ZMod p) K] →
                  [inst_5 : Algebra (ZMod p) K'] → Fintype.card K = Fintype.card K' → K ≃ₐ[ZMod p] K'
-- Mathlib.Data.Set.Lattice
Set.iInter₂_congr : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s t : (i : ι) → κ i → Set α},
  (∀ (i : ι) (j : κ i), s i j = t i j) → ⋂ i, ⋂ j, s i j = ⋂ i, ⋂ j, t i j
-- Mathlib.CategoryTheory.Monad.Equalizer
/-- The top map in the equalizer diagram we will construct.  -/
CategoryTheory.Comonad.CofreeEqualizer.topMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Comonad C} → (X : T.Coalgebra) → T.cofree.obj X.A ⟶ T.cofree.obj (T.obj X.A)
-- Init.Data.Nat.Lemmas
Nat.lt_mul_self_iff : ∀ {n : ℕ}, n < n * n ↔ 1 < n
-- Init.Data.SInt.Float
/-- Obtains a `Float` whose value is near the given `Int64`.

It will be exactly the value of the given `Int64` if such a `Float` exists. If no such `Float`
exists, the returned value will either be the smallest `Float` that is larger than the given value,
or the largest `Float` that is smaller than the given value.


This function does not reduce in the kernel.
 -/
Int64.toFloat : Int64 → Float
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.congrLeftFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (E : Type u_3) [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (X : C ≌ D), (CategoryTheory.Equivalence.congrLeftFunctor C D E).obj X = Opposite.op X.congrLeft
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.id.eq_1 : ∀ (α : Type u_2) [inst : Max α] [inst_1 : Bot α], SupBotHom.id α = { toSupHom := SupHom.id α, map_bot' := ⋯ }
-- Init.Data.Range.Polymorphic.Basic
/-- Checks whether the range contains any value.

This function returns a meaningful value given `LawfulUpwardEnumerable` and
`LawfulUpwardEnumerableLT` instances.
 -/
Std.Rco.isEmpty : {α : Type u} → [inst : LT α] → [DecidableLT α] → [Std.PRange.UpwardEnumerable α] → Std.Rco α → Bool
-- Init.Data.UInt.Lemmas
UInt16.toUSize_neg : ∀ (a : UInt16), (-a).toUSize = -a.toUSize % 65536
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f g : X ⟶ Y)
  (U :
    TopologicalSpace.Opens
      ↑↑(CategoryTheory.Limits.coequalizer (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
              (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g)).toPresheafedSpace)
  (s :
    ↑((CategoryTheory.Limits.coequalizer (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
              (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g)).presheaf.obj
        (Opposite.op U))),
  IsOpen
    (⇑(CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.Limits.coequalizer.π (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
                (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g)).hom.base) ''
      (AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen f g U s).carrier)
-- Mathlib.AlgebraicGeometry.Birational.Composition
/-- Composition of partial maps. The domain of `f.comp g` is the preimage of `g.domain` under `f`,
viewed as an open subscheme of `X`. Requires `f.hom` to be dominant so that the domain is dense.  -/
AlgebraicGeometry.Scheme.PartialMap.comp : {X Y Z : AlgebraicGeometry.Scheme} →
  [PreirreducibleSpace ↥X] →
    [Nonempty ↥Y] → (f : X.PartialMap Y) → [AlgebraicGeometry.IsDominant f.hom] → Y.PartialMap Z → X.PartialMap Z
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- `AdicCompletion` is the submodule of compatible families in
`∀ n : ℕ, M ⧸ (I ^ n • ⊤)`.  -/
AdicCompletion.submodule : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Submodule R ((n : ℕ) → M ⧸ I ^ n • ⊤)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X Y).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom Y)
        h)
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The right inclusion `G ⟶ homotopyCofiber φ`.  -/
HomologicalComplex.homotopyCofiber.inr : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {F G : HomologicalComplex C c} →
            (φ : F ⟶ G) →
              [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
                [inst_3 : DecidableRel c.Rel] → G ⟶ HomologicalComplex.homotopyCofiber φ
-- Mathlib.GroupTheory.Focal
Subgroup.ker_restrict_transferFocal_eq_focalSubgroupOf : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G) [inst_2 : (↑P).FiniteIndex],
  ((↑P).transferFocal.domRestrict P).ker = (↑P).focalSubgroupOf
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
RightPreLieRing.ext : ∀ {L : Type u_1} {x y : RightPreLieRing L},
  Add.add = Add.add →
    Zero.zero = Zero.zero →
      NSMul.nsmul = NSMul.nsmul →
        Neg.neg = Neg.neg → Sub.sub = Sub.sub → ZSMul.zsmul = ZSMul.zsmul → Mul.mul = Mul.mul → x = y
-- Mathlib.RepresentationTheory.Homological.Resolution
Representation.linearizeTrivialIso.eq_1 : ∀ (k : Type u) (G : Type v) [inst : Monoid G] [inst_1 : Semiring k] (X : Type w),
  Representation.linearizeTrivialIso k G X =
    Representation.Equiv.mk (LinearEquiv.refl k (MonoidAlgebra k (Action.trivial G X).V)) ⋯
-- Std.Sync.Channel
/-- A multi-producer multi-consumer FIFO channel that offers both bounded and unbounded buffering
and an asynchronous API. To switch into synchronous mode use `Channel.sync`.

If a channel needs to be closed to indicate some sort of completion event use `Std.CloseableChannel`
instead. Note that `Std.CloseableChannel` introduces a need for error handling in some cases, thus
`Std.Channel` is usually easier to use if applicable.
 -/
Std.Channel : Type → Type
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_lt' : ∀ {x y : ℝ}, 0 < y → (√x < y ↔ x < y ^ 2)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.rescale.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (a : R),
  PowerSeries.rescale a =
    { toFun := fun f => PowerSeries.mk fun n => a ^ n * (PowerSeries.coeff n) f, map_one' := ⋯, map_mul' := ⋯,
      map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.map_zero : ∀ {R : CommRingCat} {M N : ModuleCat ↑R}, AlgebraicGeometry.tilde.map 0 = 0
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBSet.isEmpty.match_1.eq_2 : ∀ {α : Type u_1} {cmp : α → α → Ordering} (motive : RBTree.RBSet α cmp → Sort u_2) (x : RBTree.RBSet α cmp)
  (h_1 : (property : RBTree.RBNode.WF cmp RBTree.RBNode.nil) → motive ⟨RBTree.RBNode.nil, property⟩)
  (h_2 : (x : RBTree.RBSet α cmp) → motive x),
  (∀ (property : RBTree.RBNode.WF cmp RBTree.RBNode.nil), x = ⟨RBTree.RBNode.nil, property⟩ → False) →
    (match x with
      | ⟨RBTree.RBNode.nil, property⟩ => h_1 property
      | x => h_2 x) =
      h_2 x
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- A variant of `CategoryTheory.Limits.Cocone.ext` specialized to produce
isomorphisms of cowedges.  -/
CategoryTheory.Limits.Cowedge.ext : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
          {W₁ W₂ : CategoryTheory.Limits.Cowedge F} →
            (e : W₁.pt ≅ W₂.pt) →
              autoParam
                  (∀ (j : J),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π W₁ j) e.hom =
                      CategoryTheory.Limits.Multicofork.π W₂ j)
                  CategoryTheory.Limits.Cowedge.ext._auto_1 →
                (W₁ ≅ W₂)
-- Batteries.Data.List.Lemmas
List.disjoint_nil_left : ∀ {α : Type u_1} (l : List α), [].Disjoint l
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.monic_of_natDegree_le_of_coeff_eq_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} (n : ℕ), p.natDegree ≤ n → p.coeff n = 1 → p.Monic
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.eoi.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_keysArray : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.keysArray.size = m.size
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.relNorm_eq_pow_of_isMaximal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] (P : Ideal S)
  (p : Ideal R) [hPp : P.LiesOver p] [PerfectField (FractionRing R)] [P.IsMaximal] [p.IsMaximal],
  (Ideal.relNorm R) P = p ^ P.inertiaDeg R
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.instCompactSpace : ∀ {α : Type u_1} [inst : UniformSpace α] [CompactSpace α], CompactSpace (TopologicalSpace.Closeds α)
-- Init.Data.Fin.Lemmas
Fin.le_def : ∀ {n : ℕ} {a b : Fin n}, a ≤ b ↔ ↑a ≤ ↑b
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.restrictScalarsHom_injective : ∀ (R : Type u) {S : Type v} {A : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A],
  Function.Injective ⇑(AlgEquiv.restrictScalarsHom R)
-- Lean.Level
/-- Similar to `mkLevelMax`, but applies cheap simplifications  -/
Lean.mkLevelMax' : Lean.Level → Lean.Level → Lean.Level
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (R : CategoryTheory.Functor E D),
  (CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence L R).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Iso.refl
          ((CategoryTheory.Functor.id
                (CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L)))).obj
            x))
      ⋯
-- Lean.Message
Lean.BaseMessage.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (fileName : String) (pos : Lean.Position) (endPos : Option Lean.Position)
  (keepFullRange : Bool) (severity : Lean.MessageSeverity) (isSilent : Bool) (caption : String) (data : α),
  sizeOf
      { fileName := fileName, pos := pos, endPos := endPos, keepFullRange := keepFullRange, severity := severity,
        isSilent := isSilent, caption := caption, data := data } =
    1 + sizeOf fileName + sizeOf pos + sizeOf endPos + sizeOf keepFullRange + sizeOf severity + sizeOf isSilent +
        sizeOf caption +
      sizeOf data
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.comap_monotone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F : CategoryTheory.Functor C D}, Monotone (CategoryTheory.Precoverage.comap F)
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.ofPred_inter_eq_sep`. -/
Set.setOf_inter_eq_sep : ∀ {α : Type u} (p : α → Prop) (s : Set α), {a | p a} ∩ s = {a | a ∈ s ∧ p a}
-- Init.Data.Slice.Basic
Std.Slice.mk.injEq : ∀ {γ : Type u} (internalRepresentation internalRepresentation_1 : γ),
  ({ internalRepresentation := internalRepresentation } = { internalRepresentation := internalRepresentation_1 }) =
    (internalRepresentation = internalRepresentation_1)
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- The **Matrix determinant lemma**

TODO: show the more general version without `hA : IsUnit A.det` as
`(A + replicateCol u * replicateRow v).det = A.det + v ⬝ᵥ (adjugate A) *ᵥ u`.
 -/
Matrix.det_add_replicateCol_mul_replicateRow : ∀ {m : Type u_2} {α : Type u_4} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommRing α] {ι : Type u_5}
  [inst_3 : Unique ι] {A : Matrix m m α},
  IsUnit A.det →
    ∀ (u v : m → α),
      (A + Matrix.replicateCol ι u * Matrix.replicateRow ι v).det =
        A.det * (1 + Matrix.replicateRow ι v * A⁻¹ * Matrix.replicateCol ι u).det
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
TopCat.Presheaf.IsSheafPairwiseIntersections.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Presheaf C X),
  F.IsSheafPairwiseIntersections =
    ∀ ⦃ι : Type w⦄ (U : ι → TopologicalSpace.Opens ↑X),
      Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.mapCone F (CategoryTheory.Pairwise.cocone U).op))
-- Mathlib.Algebra.Order.Monoid.Lex
/-- Given ordered monoids M, N, the natural inclusion ordered homomorphism from N to M × N.  -/
OrderMonoidHom.inr : (α : Type u_1) →
  (β : Type u_2) →
    [inst : Monoid α] → [inst_1 : PartialOrder α] → [inst_2 : Monoid β] → [inst_3 : Preorder β] → β →*o α × β
-- Mathlib.Algebra.Symmetrized
/-- The symmetrized algebra (denoted as `αˢʸᵐ`)
has the same underlying space as the original algebra `α`.  -/
SymAlg : Type u_1 → Type u_1
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- As a simplicial set, `cechNerveTerminalFrom` of a monoid `G` is isomorphic to the universal
cover of the classifying space of `G` as a simplicial set.  -/
classifyingSpaceUniversalCover.cechNerveTerminalFromIsoCompForget : (G : Type u) →
  [inst : Monoid G] →
    CategoryTheory.cechNerveTerminalFrom G ≅
      CategoryTheory.Functor.comp (classifyingSpaceUniversalCover G) (CategoryTheory.forget (Action (Type u) G))
-- Mathlib.Data.Set.Finite.Monad
Set.fintypeBind' : {α β : Type u_1} →
  [DecidableEq β] → (s : Set α) → [Fintype ↑s] → (f : α → Set β) → [(a : α) → Fintype ↑(f a)] → Fintype ↑(s >>= f)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
/-- The composition of two pushforward functors on categories of presheaves of modules
identify to the pushforward for the composition.  -/
PresheafOfModules.pushforwardComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {F : CategoryTheory.Functor C D} →
              {R : CategoryTheory.Functor Dᵒᵖ RingCat} →
                {S : CategoryTheory.Functor Cᵒᵖ RingCat} →
                  (φ : S ⟶ F.op.comp R) →
                    {T : CategoryTheory.Functor Eᵒᵖ RingCat} →
                      {G : CategoryTheory.Functor D E} →
                        (ψ : R ⟶ G.op.comp T) →
                          (PresheafOfModules.pushforward ψ).comp (PresheafOfModules.pushforward φ) ≅
                            PresheafOfModules.pushforward (CategoryTheory.CategoryStruct.comp φ (F.op.whiskerLeft ψ))
-- Init.Data.SInt.Lemmas
ISize.sub_eq_add_neg : ∀ (a b : ISize), a - b = a + -b
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.trivial.congr_simp : ∀ {R : Type u_5} [inst : Semiring R] [inst_1 : DecidablePred fun x => x = 0] [inst_2 : NoZeroDivisors R] {S : Type u_6}
  [inst_3 : Semiring S] [inst_4 : PartialOrder S] [inst_5 : IsOrderedRing S] [inst_6 : Nontrivial S],
  AbsoluteValue.trivial = AbsoluteValue.trivial
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toArray.go_eq.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()