mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.Away.Basic
selfZPow_sub_natCast : ∀ {R : Type u_1} [inst : CommSemiring R] (x : R) (B : Type u_2) [inst_1 : CommSemiring B] [inst_2 : Algebra R B]
  [inst_3 : IsLocalization.Away x B] {n m : ℕ},
  selfZPow x B (↑n - ↑m) = IsLocalization.mk' B (x ^ n) (Submonoid.pow x m)
-- Mathlib.Algebra.Notation.Prod
Prod.fst_zero : ∀ {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst_1 : Zero N], 0.1 = 0
-- Init.Data.Rat.Lemmas
/-- Define a (dependent) function or prove `∀ r : Rat, p r` by dealing with rational
numbers of the form `n /. d` with `0 < d` and coprime `n`, `d`.  -/
Rat.numDenCasesOn : {C : ℚ → Sort u} → (a : ℚ) → ((n : ℤ) → (d : ℕ) → 0 < d → n.natAbs.Coprime d → C (Rat.divInt n ↑d)) → C a
-- Mathlib.Order.CompactlyGenerated.Basic
/-- If each family `f i` is `iSupIndep`, then the family of pointwise infima
`k ↦ ⨅ i, f i (k i)` is also `iSupIndep`.
 -/
iSupIndep.iInf : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] {ι : Type u_3}
  {κ : ι → Type u_4} (f : (i : ι) → κ i → α), (∀ (i : ι), iSupIndep (f i)) → iSupIndep fun k => ⨅ i, f i (k i)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.apply_ne_one_iff : ∀ {α : Type u_1} {V : Type u_2} {A : Matrix V V α} [inst : MulZeroOneClass α] [Nontrivial α],
  A.IsAdjMatrix → ∀ (i j : V), ¬A i j = 1 ↔ A i j = 0
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.HomologyMapData.smul_left : ∀ {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).left = γ.left.smul a
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAtFilter.isEquivalent_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {L : Filter (E × E)},
  HasFDerivAtFilter f f' L →
    Topology.IsInducing ⇑f' → Asymptotics.IsEquivalent L (fun p => f p.1 - f p.2) fun p => f' (p.1 - p.2)
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIcc_eq_left : ∀ {α : Type u_1} [inst : LinearOrder α] {a b x : α} (h : a < b), Set.projIcc a b ⋯ x = ⟨a, ⋯⟩ ↔ x ≤ a
-- Mathlib.Topology.Category.Compactum
/-- The forgetful functors of `Compactum` and `CompHaus` are compatible via
`compactumToCompHaus`.  -/
compactumToCompHausCompForget : compactumToCompHaus.comp (CategoryTheory.forget CompHaus) ≅ Compactum.forget
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.den_mem : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} {x : Submonoid A}
  (self : HomogeneousLocalization.NumDenSameDeg 𝒜 x), ↑self.den ∈ x
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Goal.mvarId : Lean.Meta.Grind.Goal → Lean.MVarId
-- Mathlib.Algebra.Order.Floor.Extended
ENat.preimage_toENNReal_Ioi : ∀ (a : ENNReal), ENat.toENNReal ⁻¹' Set.Ioi a = Set.Ioi ⌊a⌋ₑ
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- If `{Uᵢ}` covers `Y`, the pre-`0`-hypercover `{X ×[Z] Uᵢ}` of `X ×[Z] Y` is isomorphic
to the pullback of `{Uᵢ}` along the second projection.  -/
CategoryTheory.PreZeroHypercover.pullbackCoverOfRightIsoPullback₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {Y : C} →
      (E : CategoryTheory.PreZeroHypercover Y) →
        {X Z : C} →
          (f : X ⟶ Z) →
            (g : Y ⟶ Z) →
              [inst_1 : CategoryTheory.Limits.HasPullback f g] →
                [inst_2 :
                    ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.snd f g)] →
                  [inst_3 :
                      ∀ (i : E.I₀),
                        CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f g) (E.f i)] →
                    E.pullbackCoverOfRight f g ≅
                      CategoryTheory.PreZeroHypercover.pullback₂ (CategoryTheory.Limits.pullback.snd f g) E
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.liftOfIsRightKanExtension_fac_app_assoc : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [inst_3 : F'.IsRightKanExtension α] (G : CategoryTheory.Functor D H) (β : L.comp G ⟶ F) (X : C)
  {Z : H} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F'.liftOfIsRightKanExtension α G β).app (L.obj X))
      (CategoryTheory.CategoryStruct.comp (α.app X) h) =
    CategoryTheory.CategoryStruct.comp (β.app X) h
-- Init.Data.List.Sort.Impl
/-- Split a list in two equal parts, reversing the first part.
If the length is odd, the first part will be one element longer.
 -/
List.MergeSort.Internal.splitRevInTwo : {α : Type u_1} → {n : ℕ} → { l // l.length = n } → { l // l.length = (n + 1) / 2 } × { l // l.length = n / 2 }
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.algEquivOfAlgEquiv_algebraMap : ∀ {R : Type u_8} {A : Type u_9} {K : Type u_10} {B : Type u_11} {L : Type u_12} [inst : CommSemiring R]
  [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : CommRing K] [inst_4 : CommRing L] [inst_5 : Algebra R A]
  [inst_6 : Algebra R K] [inst_7 : Algebra A K] [inst_8 : IsFractionRing A K] [inst_9 : IsScalarTower R A K]
  [inst_10 : Algebra R B] [inst_11 : Algebra R L] [inst_12 : Algebra B L] [inst_13 : IsFractionRing B L]
  [inst_14 : IsScalarTower R B L] (h : A ≃ₐ[R] B) (a : A),
  (IsFractionRing.algEquivOfAlgEquiv h) ((algebraMap A K) a) = (algebraMap B L) (h a)
-- Mathlib.Data.Set.Restrict
/-- **Alias** of the forward direction of `Set.injOn_iff_injective`. -/
Set.InjOn.injective : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.InjOn f s → Function.Injective (s.domRestrict f)
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A normed ring is a non-unital normed ring.  -/
NormedRing.toNonUnitalNormedRing : {α : Type u_2} → [β : NormedRing α] → NonUnitalNormedRing α
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.inv_inv : ∀ {a b : ℝ}, 0 < a → 0 < b → a + b = 1 → a⁻¹.HolderConjugate b⁻¹
-- Lean.Syntax
/-- Monad class that gives read/write access to a `Traverser`.  -/
Lean.Syntax.MonadTraverser : (Type → Type) → Type 1
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.mapEquiv_trans : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {P : Type u_6} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  (g : M ≃ₗ[R] N) (h : N ≃ₗ[R] P),
  (DividedPowerAlgebra.mapEquiv g).trans (DividedPowerAlgebra.mapEquiv h) = DividedPowerAlgebra.mapEquiv (g ≪≫ₗ h)
-- Mathlib.Analysis.InnerProductSpace.Basic
_private.Mathlib.Analysis.InnerProductSpace.Basic.0.«term⟪_,_⟫_4» : Lean.ParserDescr
-- Mathlib.RingTheory.Ideal.Prime
Ideal.IsPrime.mul_notMem : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, I.IsPrime → ∀ {x y : α}, x ∉ I → y ∉ I → x * y ∉ I
-- Mathlib.FieldTheory.Separable
Polynomial.Separable.mul_unit : ∀ {R : Type u} [inst : CommSemiring R] {f g : Polynomial R}, f.Separable → IsUnit g → (f * g).Separable
-- Mathlib.Data.Set.Image
Set.image_inter : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set α}, Function.Injective f → f '' (s ∩ t) = f '' s ∩ f '' t
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rcc_add_right_eq_map : ∀ {m n : ℕ}, (m...=m + n).toArray = Array.map (fun x => x + m) (0...=n).toArray
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyIncomingCall.mk.inj : ∀ {«from» : Lean.Lsp.CallHierarchyItem} {fromRanges : Array Lean.Lsp.Range} {from_1 : Lean.Lsp.CallHierarchyItem}
  {fromRanges_1 : Array Lean.Lsp.Range},
  { «from» := «from», fromRanges := fromRanges } = { «from» := from_1, fromRanges := fromRanges_1 } →
    «from» = from_1 ∧ fromRanges = fromRanges_1
-- Batteries.Recycling.MonadSatisfying.List
List.satisfiesM_foldrM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {motive : β → Prop} {l : List α} {b : β} [inst : Monad m]
  [LawfulMonad m] {f : α → β → m β},
  motive b → (∀ a ∈ l, ∀ (b : β), motive b → SatisfiesM motive (f a b)) → SatisfiesM motive (List.foldrM f b l)
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- The functor `(X ⊗ Y).HomotopyCategory ⥤ X.HomotopyCategory × Y.HomotopyCategory`
when `X` and `Y` are `2`-truncated simplicial sets.  -/
SSet.Truncated.HomotopyCategory.BinaryProduct.functor : (X Y : SSet.Truncated 2) →
  CategoryTheory.Functor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategory
    (X.HomotopyCategory × Y.HomotopyCategory)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.foldM_filterMapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [inst_5 : MonadAttach n]
  [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_8 : Monad o] [LawfulMonad o] [inst_10 : Std.IteratorLoop α m n]
  [inst_11 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m n] [Std.LawfulIteratorLoop α m o]
  [inst_14 : MonadLiftT m n] [inst_15 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
  {f : β → n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Std.IterM m β},
  Std.IterM.foldM g init (Std.IterM.filterMapM f it) =
    Std.IterM.foldM
      (fun d b => do
        let __x ← liftM (f b)
        match __x with
          | some c => g d c
          | x => pure d)
      init it
-- Plausible.Gen
Plausible.instReprGenError : Repr Plausible.GenError
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.sum'_map_inr : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A C)
  (G : CategoryTheory.Functor B C) {b b' : B} (f : b ⟶ b'),
  (F.sum' G).map ((CategoryTheory.Sum.inr_ A B).map f) = G.map f
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min_le_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α} (hc : k ∈ t),
  (cmp (t.min ⋯) k).isLE = true
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.toMulActionHom_injective : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  {f g : A →ₑ*[φ] B}, ↑f = ↑g → f = g
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategory} (i : Δ' ⟶ Δ)
  [inst_3 : CategoryTheory.Mono i],
  CategoryTheory.CategoryStruct.comp
      (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ)).inj
        (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op Δ)))
      ((AlgebraicTopology.DoldKan.Γ₀.obj K).map i.op) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i)
      (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ')).inj
        (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op Δ')))
-- Lean.Expr
Lean.Expr.hasFVarEx : Lean.Expr → Bool
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the sign of the oriented angle between two vectors is zero, either one of the vectors is
zero or the unoriented angle is 0 or π.  -/
Orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  (o.oangle x y).sign = 0 →
    x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = Real.pi
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.instOrderBot : {R : Type u_1} →
  {M : Type u_3} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → OrderBot (Submodule R M)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.evaluation_preservesColimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasColimitsOfShape J C] (k : K),
  CategoryTheory.Limits.PreservesColimitsOfShape J ((CategoryTheory.evaluation K C).obj k)
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.chainComplexMap_id : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) (X : A) [inst_2 : ι.Full] [inst_3 : ι.Faithful]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Abelian A],
  Λ.chainComplexMap (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (Λ.chainComplex X)
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
/-- `ofTensorProduct` packaged as linear equiv if `M` is a finite `R`-module and `R` is
Noetherian.  -/
AdicCompletion.ofTensorProductEquivOfFiniteNoetherian : {R : Type u} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u) →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [IsNoetherianRing R] →
              [Module.Finite R M] → TensorProduct R (AdicCompletion I R) M ≃ₗ[AdicCompletion I R] AdicCompletion I M
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.mem_sInf : ∀ {M : Type u_1} [inst : AddZeroClass M] {S : Set (AddSubmonoid M)} {x : M}, x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.empty_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] (t : Finset β), ∅ -ᵥ t = ∅
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.SubobjectRepresentableBy.iso_inv_hom_left_comp`. -/
CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_hom_left_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω) {U X : C} (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (h.iso m).inv.hom) m =
    ((CategoryTheory.Subobject.pullback (h.χ m)).obj h.Ω₀).arrow
-- Mathlib.Algebra.Order.Group.Indicator
Set.iSup_mulIndicator : ∀ {α : Type u_2} {M : Type u_3} [inst : CompleteLattice M] [inst_1 : One M] {ι : Type u_4} [inst_2 : Preorder ι]
  [IsDirectedOrder ι] {f : ι → α → M} {s : ι → Set α},
  ⊥ = 1 → Monotone f → Monotone s → ⨆ i, (s i).mulIndicator (f i) = (⋃ i, s i).mulIndicator (⨆ i, f i)
-- Mathlib.GroupTheory.GroupAction.CardCommute
/-- **Class formula** for a finite group acting on a finite type. See
`AddAction.card_eq_sum_card_addGroup_div_card_stabilizer` for a specialized version using
`Quotient.out`.  -/
AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer' : ∀ (α : Type u_1) (β : Type u_2) [inst : AddGroup α] [inst_1 : AddAction α β] [inst_2 : Fintype α] [inst_3 : Fintype β]
  [inst_4 : Fintype (Quotient (AddAction.orbitRel α β))] [inst_5 : (b : β) → Fintype ↥(AddAction.stabilizer α b)]
  {φ : Quotient (AddAction.orbitRel α β) → β},
  Function.LeftInverse Quotient.mk'' φ →
    Fintype.card β = ∑ ω, Fintype.card α / Fintype.card ↥(AddAction.stabilizer α (φ ω))
-- Mathlib.Order.Hom.Basic
/-- Inverse of an order isomorphism.  -/
OrderIso.symm : {α : Type u_2} → {β : Type u_3} → [inst : LE α] → [inst_1 : LE β] → α ≃o β → β ≃o α
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovary_iff_forall_smul_nonneg`. -/
Monovary.sub_smul_sub_nonneg : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [IsStrictOrderedModule α β] {f : ι → α} {g : ι → β}, Monovary f g → ∀ (i j : ι), 0 ≤ (f j - f i) • (g j - g i)
-- Std.Async.UDP
/-- Sends multiple data buffers through an UDP socket. The `addr` parameter specifies the destination
address. If `addr` is `none`, the data is sent to the default peer address set by `connect`.
 -/
Std.Async.UDP.Socket.sendAll : Std.Async.UDP.Socket → Array ByteArray → optParam (Option Std.Net.SocketAddress) none → Std.Async.Async Unit
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.projectiveDimension_eq_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (e : X ≅ Y),
  CategoryTheory.projectiveDimension X = CategoryTheory.projectiveDimension Y
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.waitForILeans : optParam Lean.JsonRpc.RequestID 0 → Lean.Lsp.DocumentUri → ℕ → Lean.Lsp.Ipc.IpcM Unit
-- Mathlib.Order.Minimal
minimalFor_id : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : LE α], MinimalFor P id x ↔ Minimal P x
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.mapCompLift_hom_app : ∀ {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.Groupoid E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E)
  (X : CategoryTheory.FreeGroupoid C),
  (CategoryTheory.FreeGroupoid.mapCompLift F G).hom.app X =
    CategoryTheory.CategoryStruct.id
      (((CategoryTheory.FreeGroupoid.map F).comp (CategoryTheory.FreeGroupoid.lift G)).obj X)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_iff_homology_iso_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] [inst_3 : CategoryTheory.Limits.HasZeroObject C],
  S.Exact ↔ Nonempty (S.homology ≅ 0)
-- Mathlib.Topology.Sheaves.Skyscraper
StalkSkyscraperPresheafAdjunctionAuxs.fromStalk_to_skyscraper : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [inst_3 : CategoryTheory.Limits.HasColimits C] {𝓕 : TopCat.Presheaf C X} {c : C} (f : 𝓕.stalk p₀ ⟶ c),
  StalkSkyscraperPresheafAdjunctionAuxs.fromStalk p₀ (StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf p₀ f) =
    f
-- Mathlib.Order.BooleanAlgebra.Basic
compl_himp_compl : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], xᶜ ⇨ yᶜ = y ⇨ x
-- Mathlib.Algebra.Category.AlgCat.TensorAlgebra
AlgCat.instIsRightAdjointAddCommGrpCatRingCatForget₂RingHomCarrierAddMonoidHomCarrier : (CategoryTheory.forget₂ RingCat AddCommGrpCat).IsRightAdjoint
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.WF.containsThenInsert₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size}
  {a : α} {b : β a}, m.WF → (↑(Std.DHashMap.Internal.Raw₀.containsThenInsert ⟨m, h⟩ a b).2).WF
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorial_le_factorial_mul_pow : ∀ (n k : ℕ), n.ascFactorial k ≤ k.factorial * n ^ k
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.instMulLeftMono : ∀ {α : Type u_2} [inst : Mul α], MulLeftMono (Set α)
-- Mathlib.Tactic.Sat.FromLRAT
/-- A literal is a positive or negative occurrence of an atomic propositional variable.
Note that unlike DIMACS, 0 is a valid variable index.  -/
Sat.Literal : Type
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mem_toSubalgebra : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] {S : StarSubalgebra R A} {x : A},
  x ∈ S.toSubalgebra ↔ x ∈ S
-- Std.Data.HashSet.Basic
/-- Returns `true` if the given key is present in the set. There is also a `Prop`-valued version of
this: `a ∈ m` is equivalent to `m.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` use
`==` for comparisons, while for hash sets, both use `==`.
 -/
Std.HashSet.contains : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → α → Bool
-- Mathlib.Analysis.Complex.Trigonometric
Real.sin_neg : ∀ (x : ℝ), Real.sin (-x) = -Real.sin x
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- An orbit is a block.  -/
AddAction.IsBlock.orbit : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] (a : X),
  AddAction.IsBlock G (AddAction.orbit G a)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- If `p ≠ 0` and `p ≠ 1`, then `padicValInt p p` is `1`.  -/
padicValInt.self : ∀ {p : ℕ}, 1 < p → padicValInt p ↑p = 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option (β k) → Option (β k)},
  m.WF →
    (m.alter k f).size =
      if k ∈ m ∧ (f (m.get? k)).isNone = true then m.size - 1
      else if k ∉ m ∧ (f (m.get? k)).isSome = true then m.size + 1 else m.size
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.forget_grp_preserves_epi : (CategoryTheory.forget GrpCat).PreservesEpimorphisms
-- Mathlib.Data.Multiset.UnionInter
Multiset.eq_union_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, t ≤ s → s ∪ t = s
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.Balanced.insert : ∀ {α : Type u_1} {c₀ : RBTree.RBColor} {n₀ : ℕ} {c : RBTree.RBColor} {n : ℕ} {t : RBTree.RBNode α} {v : α}
  {path : RBTree.RBNode.Path α},
  RBTree.RBNode.Path.Balanced c₀ n₀ path c n → t.Balanced c n → ∃ c n, (path.insert t v).Balanced c n
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.proj_isLocallyConstant : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X), IsLocallyConstant S.proj
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.filterMap.eq_1 : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} (f : (a : α) → β a → Option (γ a)) (m : Std.DHashMap.Raw α β),
  Std.DHashMap.Raw.filterMap f m =
    if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.filterMap f ⟨m, h⟩) else ∅
-- Mathlib.Algebra.Order.UpperLower
UpperSet.Ici_one : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α], UpperSet.Ici 1 = 1
-- Mathlib.Geometry.Manifold.Immersion
/-- Prefer using `IsImmersionAt.contMDiffAt` instead  -/
Manifold.IsImmersionAt.contMDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAt I J n f x), ContMDiffOn I J n f h.domChart.source
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
GenContFract.IntFractPair.coe_to_intFractPair : ∀ {K : Type u_1} {β : Type u_2} [inst : Coe K β] {b : ℤ} {fr : K}, ↑{ b := b, fr := fr } = { b := b, fr := Coe.coe fr }