mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.FinValue.n : Lean.Meta.Sym.FinValue → ℕ
-- Mathlib.MeasureTheory.Measure.Stieltjes
Iotop_subset_Ioc : ∀ {R : Type u_1} [inst : LinearOrder R] {a b : R}, Iotop a b ⊆ Set.Ioc a b
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {f g : Equiv.Perm α},
  f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleType = g.cycleType - f.cycleType
-- Mathlib.Order.SuccPred.Limit
Order.not_isPredPrelimit_of_isPredArchimedean : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α] [NoMaxOrder α],
  ¬Order.IsPredPrelimit a
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_neg_le_of_le : ∀ {R : Type u} [inst : Ring R] {a : WithBot ℕ} {p : Polynomial R}, p.degree ≤ a → (-p).degree ≤ a
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.Subcomplex.ext`. -/
Topology.CWComplex.Subcomplex.ext : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  {E F : Topology.RelCWComplex.Subcomplex C}, (∀ (x : X), x ∈ E ↔ x ∈ F) → E = F
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAt.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [ContMDiffAdd I n G] {f g : M → G} {x : M},
  ContMDiffAt I' I n f x → ContMDiffAt I' I n g x → ContMDiffAt I' I n (f + g) x
-- Init.Data.List.Lex
List.nil_le : ∀ {α : Type u_1} [inst : LT α] (l : List α), [] ≤ l
-- Lean.Meta.Basic
Lean.Meta.withoutProofIrrelevance : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → n α → n α
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.move : {Γ : Type u_1} → {Λ : Type u_2} → {σ : Type u_3} → Turing.Dir → Turing.TM1.Stmt Γ Λ σ → Turing.TM1.Stmt Γ Λ σ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_le_size_insertIfNew : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {v : β k}, m.size ≤ (m.insertIfNew k v).size
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.map_id : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (z : S) (h : optParam (M ≤ Submonoid.comap (RingHom.id R) M) ⋯),
  (IsLocalization.map S (RingHom.id R) h) z = z
-- Mathlib.LinearAlgebra.TensorProduct.Pi
TensorProduct.piScalarRightHom_tmul : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module S N] [inst_6 : IsScalarTower R S N] (ι : Type u_4)
  (x : N) (f : ι → R), (TensorProduct.piScalarRightHom R S N ι) (x ⊗ₜ[R] f) = fun j => f j • x
-- Mathlib.RingTheory.Valuation.Integral
Valuation.Integers.integralClosure : ∀ {R : Type u} {Γ₀ : Type v} [inst : CommRing R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O R], v.Integers O → integralClosure O R = ⊥
-- Init.Notation
/-- `And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`. -/
«term_∧_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_id_fiber : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (X : F.Grothendieck),
  (CategoryTheory.CategoryStruct.id X).fiber = (F.mapId { as := X.base }).hom.toNatTrans.app X.fiber
-- Mathlib.Algebra.BigOperators.Finprod
finsum_curry₃ : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {γ : Type u_7} (f : α × β × γ → M),
  Function.HasFiniteSupport f → ∑ᶠ (abc : α × β × γ), f abc = ∑ᶠ (a : α) (b : β) (c : γ), f (a, b, c)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.maxKey!_alterKey_eq_self : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [inst_4 : Inhabited α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : Option β → Option β},
      (Std.Internal.List.Const.alterKey k f l).isEmpty = false →
        (Std.Internal.List.maxKey! (Std.Internal.List.Const.alterKey k f l) = k ↔
          (f (Std.Internal.List.getValue? k l)).isSome = true ∧
            ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k' k).isLE = true)
-- Init.Data.UInt.Bitwise
USize.ofBitVec_shiftLeft : ∀ (a : BitVec System.Platform.numBits),
  ∀ b < System.Platform.numBits, { toBitVec := a <<< b } = { toBitVec := a } <<< USize.ofNat b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {a : α} {h' : (Std.DTreeMap.Raw.Const.get? t a).isSome = true},
  (Std.DTreeMap.Raw.Const.get? t a).get h' = Std.DTreeMap.Raw.Const.get t a ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_obj_obj_snd_map : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  (U : CategoryTheory.Functor X Y) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) {X_1 Y_1 : X}
  (f : X_1 ⟶ Y_1),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).obj S).snd.map f =
    S.snd.map (U.map f)
-- Mathlib.Order.Interval.Finset.Basic
/-- A function from a locally finite preorder is monotone if and only if it is monotone when
restricted to pairs satisfying `a ⩿ b`.  -/
monotone_iff_forall_wcovBy : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [LocallyFiniteOrder α] [inst_2 : Preorder β] (f : α → β),
  Monotone f ↔ ∀ (a b : α), a ⩿ b → f a ≤ f b
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.coe_one : ∀ {M : Type u_2} {N : Type u_3} {X : Type u_4} {Y : Type u_5} {σ : M → N} [inst : SMul M X] [inst_1 : Monoid N]
  [inst_2 : Monoid Y] [inst_3 : MulDistribMulAction N Y], ⇑1 = 1
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtr.comp_continuousOn : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β}
  [inst_2 : TopologicalSpace δ] {s : Set δ} (g : δ → α) {b : δ},
  IsLocalExtr f (g b) → ContinuousOn g s → b ∈ s → IsLocalExtrOn (f ∘ g) s b
-- Mathlib.Tactic.Linter.FindDeprecations
/-- `removeRanges file rgs` removes from the string `file` the substrings whose ranges are in the array
`rgs`.

*Notes*.
* The command makes the assumption that `rgs` is *sorted*.
* The command removes all consecutive whitespace following the end of each range.
 -/
Mathlib.Tactic.removeRanges : String → Array Lean.Syntax.Range → String
-- Mathlib.Algebra.Homology.ShortComplex.Ab
/-- Given a short complex `S` of abelian groups, this is the isomorphism between
the abstract `S.homology` of the homology API and the more explicit
quotient of `AddMonoidHom.ker S.g` by the image of
`S.abToCycles : S.X₁ →+ AddMonoidHom.ker S.g`.  -/
CategoryTheory.ShortComplex.abHomologyIso : (S : CategoryTheory.ShortComplex Ab) →
  S.homology ≅ AddCommGrpCat.of (↥(AddCommGrpCat.Hom.hom S.g).ker ⧸ S.abToCycles.range)
-- Mathlib.Data.Real.Basic
/-- The type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  -/
termℝ : Lean.ParserDescr
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] {l : List α}
  {k k' fallback : α},
  cmp k k' = Ordering.eq →
    k ∉ t →
      List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
        k ∈ l → (Std.DTreeMap.Const.insertManyIfNewUnit t l).getKeyD k' fallback = k
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.equivalenceOfIsInitial_inverse_map : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) {X_1 Y : T}
  (f : X_1 ⟶ Y), (CategoryTheory.Under.equivalenceOfIsInitial hX).inverse.map f = CategoryTheory.Under.homMk f ⋯
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_ite_irrel : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (p : Prop) [inst_1 : Decidable p] (s : Finset ι) (f g : ι → M),
  (∏ x ∈ s, if p then f x else g x) = if p then ∏ x ∈ s, f x else ∏ x ∈ s, g x
-- Mathlib.Topology.Category.TopCat.Sphere
TopCat.disk.eq_1 : ∀ (n : ℕ), TopCat.disk n = TopCat.of (ULift.{u, 0} ↑(Metric.closedBall 0 1))
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.comp_homeomorph : ∀ {X : Type u_9} {Y : Type u_10} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {M : Type u_11}
  [inst_2 : Zero M] {f : Y → M}, HasCompactSupport f → ∀ (φ : X ≃ₜ Y), HasCompactSupport (f ∘ ⇑φ)
-- Init.Data.UInt.Bitwise
USize.not_neg_one : ~~~(-1) = 0
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivWithinAt.differentiableWithinAt : ∀ {𝕜 : 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 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x → DifferentiableWithinAt 𝕜 f s x
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoLocallyUniformly.inv : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F : ι → X → α} {f : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l → TendstoLocallyUniformly F⁻¹ f⁻¹ l
-- Mathlib.Order.Filter.AtTopBot.Basic
/-- **Alias** of `Filter.tendsto_atTop_atTop_iff_of_monotone`. -/
Monotone.tendsto_atTop_atTop_iff : ∀ {α : Type u_3} {β : Type u_4} [Nonempty α] [inst : Preorder α] [IsDirectedOrder α] {f : α → β} [inst_2 : Preorder β],
  Monotone f → (Filter.Tendsto f Filter.atTop Filter.atTop ↔ ∀ (b : β), ∃ a, b ≤ f a)
-- Mathlib.Order.Heyting.Basic
sdiff_le_sdiff_of_sup_le_sup_left : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, c ⊔ a ≤ c ⊔ b → a \ c ≤ b \ c
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.cases_mk : ∀ {F : PFunctor.{uA, uB}} {r : F.M → Sort u_2} (x : ↑F F.M) (f : (x : ↑F F.M) → r (PFunctor.M.mk x)),
  PFunctor.M.cases f (PFunctor.M.mk x) = f x
-- Mathlib.RingTheory.PowerSeries.Derivative
/-- The derivative of `g^n` equals `n * g^(n-1) * g'`.  -/
PowerSeries.derivative_pow : ∀ {R : Type u_1} [inst : CommSemiring R] (g : PowerSeries R) (n : ℕ),
  (PowerSeries.derivative R) (g ^ n) = ↑n * g ^ (n - 1) * (PowerSeries.derivative R) g
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.propQCPrecoverage_monotone : Monotone AlgebraicGeometry.Scheme.propQCPrecoverage
-- Mathlib.CategoryTheory.Sites.Point.Comap
CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso_hom_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} (Φ : K.Point)
  (F : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.RepresentablyFlat F]
  {J : CategoryTheory.GrothendieckTopology C} (hF : CategoryTheory.CoverPreserving J K F)
  [inst_3 : CategoryTheory.InitiallySmall (F.comp Φ.fiber).Elements] (A : Type u_3)
  [inst_4 : CategoryTheory.Category.{v, u_3} A] [inst_5 : CategoryTheory.Limits.HasProducts A]
  [inst_6 : F.IsContinuous J K] [inst_7 : (F.sheafPushforwardContinuous A J K).IsRightAdjoint]
  [inst_8 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u_3} A] (X : CategoryTheory.Sheaf J A),
  (Φ.sheafFiberComapIso F hF A).hom.app X =
    CategoryTheory.CategoryStruct.comp ((Φ.comap F hF).sheafFiber.map ((F.sheafAdjunctionContinuous A J K).unit.app X))
      (CategoryTheory.CategoryStruct.comp
        ((Φ.comap F hF).sheafFiber.map
          ((F.sheafPushforwardContinuous A J K).map
            (Φ.skyscraperSheafAdjunction.unit.app ((F.sheafPullback A J K).obj X))))
        (CategoryTheory.CategoryStruct.comp
          ((Φ.comap F hF).sheafFiber.map
            ((Φ.skyscraperSheafFunctorCompSheafPushforwardContinuous F hF A).hom.app
              (Φ.sheafFiber.obj ((F.sheafPullback A J K).obj X))))
          ((Φ.comap F hF).skyscraperSheafAdjunction.counit.app (Φ.sheafFiber.obj ((F.sheafPullback A J K).obj X)))))
-- Mathlib.Topology.Algebra.OpenSubgroup
/-- The product of two open subgroups as an open subgroup of the product group.  -/
OpenSubgroup.prod : {G : Type u_1} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] →
      {H : Type u_2} →
        [inst_2 : Group H] → [inst_3 : TopologicalSpace H] → OpenSubgroup G → OpenSubgroup H → OpenSubgroup (G × H)
-- Init.Data.List.Basic
/-- Lexicographic ordering for lists with respect to an ordering of elements.

`as` is lexicographically smaller than `bs` if
* `as` is empty and `bs` is non-empty, or
* both `as` and `bs` are non-empty, and the head of `as` is less than the head of `bs` according to
  `r`, or
* both `as` and `bs` are non-empty, their heads are equal, and the tail of `as` is less than the
  tail of `bs`.
 -/
List.Lex : {α : Type u} → (α → α → Prop) → List α → List α → Prop
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- A free additive group with a finite number of generators is finitely presented.  -/
AddGroup.IsFinitelyPresented.instFreeAddGroupOfFinite : ∀ {α : Type u_3} [Finite α], AddGroup.IsFinitelyPresented (FreeAddGroup α)
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
/-- Given a finite measure on a compact space, there exists another finite measure which
integrates in the same way bounded continuous functions, and is regular.  -/
MeasureTheory.Measure.exists_regular_eq_of_compactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [inst_2 : MeasurableSpace X] [BorelSpace X] [CompactSpace X]
  (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ],
  ∃ ν,
    ν.Regular ∧
      MeasureTheory.IsFiniteMeasure ν ∧ ∀ (g : BoundedContinuousFunction X ℝ), ∫ (x : X), g x ∂μ = ∫ (x : X), g x ∂ν
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.compl_mem' : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (self : BooleanSubalgebra α) {a : α}, a ∈ self.carrier → aᶜ ∈ self.carrier
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Ult
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Ult.0.Std.Tactic.BVDecide.BVPred.mkUlt.match_1.splitter : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          (motive : aig.BinaryRefVec w → Sort u_1) →
            (pair : aig.BinaryRefVec w) →
              ((lhsRefs rhsRefs : aig.RefVec w) → motive { lhs := lhsRefs, rhs := rhsRefs }) → motive pair
-- Lean.Util.ParamMinimizer
Lean.Util.ParamMinimizer.Result.mk.sizeOf_spec : ∀ (status : Lean.Util.ParamMinimizer.Status) (paramMask : Array Bool) (numCalls : ℕ),
  sizeOf { status := status, paramMask := paramMask, numCalls := numCalls } =
    1 + sizeOf status + sizeOf paramMask + sizeOf numCalls
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The cardinality of the ambient space is the product of the cardinality of a block
by the cardinality of the set of translates of that block  -/
MulAction.IsBlock.ncard_block_mul_ncard_orbit_eq : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] [MulAction.IsPretransitive G X] {B : Set X},
  MulAction.IsBlock G B → B.Nonempty → B.ncard * (MulAction.orbit G B).ncard = Nat.card X
-- Mathlib.Order.RelClasses
/-- Set notation form of `le_iff_lt_or_eq` -/
subset_iff_ssubset_or_eq : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ⊆ b ↔ a ⊂ b ∨ a = b
-- Mathlib.Data.Set.Pointwise.Support
/-- Note: to_additive also automatically translates `SMul` to `VAdd`, so we give the additive
version manually.  -/
support_comp_inv_smul₀ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : GroupWithZero α] [inst_1 : MulAction α β] [inst_2 : Zero γ]
  {c : α}, c ≠ 0 → ∀ (f : β → γ), (Function.support fun x => f (c⁻¹ • x)) = c • Function.support f
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueSet_one : ∀ {α : Type u_1} (G : SimpleGraph α), G.cliqueSet 1 = Set.range singleton
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.comp_apply : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] [inst_4 : NonUnitalNonAssocSemiring C] [inst_5 : Star C]
  (f : B →⋆ₙ+* C) (g : A →⋆ₙ+* B) (a : A), (f.comp g) a = f (g a)
-- Init.Data.BitVec.Lemmas
BitVec.toInt_neg_eq_ite : ∀ {w : ℕ} {x : BitVec w}, (-x).toInt = if x = BitVec.intMin w then x.toInt else -x.toInt
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.instHSubOffset_3 : HSub Std.Time.PlainDateTime Std.Time.Minute.Offset Std.Time.PlainDateTime
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
quasispectrum.mem_of_not_quasiregular : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A] (a : A)
  {r : Rˣ}, ¬IsQuasiregular (-(r⁻¹ • a)) → ↑r ∈ quasispectrum R a
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instIsScalarTowerComplex : ∀ {α : Type u_1} [inst : SMul α ℝ] [inst_1 : SMul α ℂ] [IsScalarTower α ℝ ℂ], IsScalarTower α ℂ ℂ
-- Mathlib.CategoryTheory.Whiskering
/-- The isomorphism between right-whiskering on the identity functor and the identity of the functor
between the resulting functor categories.  -/
CategoryTheory.Functor.whiskeringRightObjIdIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {E : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} E] →
        (CategoryTheory.Functor.whiskeringRight E C C).obj (CategoryTheory.Functor.id C) ≅
          CategoryTheory.Functor.id (CategoryTheory.Functor E C)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsEdgeConnected.preconnected : ∀ {V : Type u_1} {G : SimpleGraph V} {k : ℕ}, k ≠ 0 → G.IsEdgeConnected k → G.Preconnected
-- Mathlib.Order.Interval.Set.Basic
Set.eq_right_or_mem_Ioo_of_mem_Ioc : ∀ {α : Type u_1} [inst : PartialOrder α] {a b x : α}, x ∈ Set.Ioc b a → x = a ∨ x ∈ Set.Ioo b a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.addConj_eq_snd_of_isCommAddMonObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommAddMonObj G],
  CategoryTheory.AddGrpObj.addConj G = CategoryTheory.SemiCartesianMonoidalCategory.snd G G
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.instCategoryObjOppositeSimplexCategoryNerve : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Δ : SimplexCategoryᵒᵖ} → CategoryTheory.Category.{v_1, max u_1 v_1} ((CategoryTheory.nerve C).obj Δ)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.descItem.colonFn : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.Enriched.Basic
/-- To construct an isomorphism between enriched functors `F` and `G`, it suffices to construct
a natural isomorphism between `F.forget` and `G.forget`.  -/
CategoryTheory.EnrichedFunctor.isoMk : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₂} →
            [inst_3 : CategoryTheory.EnrichedCategory V D] →
              {F G : CategoryTheory.EnrichedFunctor V C D} → (F.forget ≅ G.forget) → (F ≅ G)
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.nnnorm_add_le_max : ∀ {S : Type u_1} [inst : SeminormedAddGroup S] [IsUltrametricDist S] (x y : S), ‖x + y‖₊ ≤ max ‖x‖₊ ‖y‖₊
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.TensorBimod.actRight.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T)
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)],
  Bimod.TensorBimod.actRight P Q = Bimod.TensorBimod.actRight P Q
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
/-- Restrict codomain of a continuous linear map.  -/
ContinuousLinearMap.codRestrict : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {M₁ : Type u_4} →
            {M₂ : Type u_5} →
              [inst_2 : TopologicalSpace M₁] →
                [inst_3 : AddCommMonoid M₁] →
                  [inst_4 : Module R₁ M₁] →
                    [inst_5 : TopologicalSpace M₂] →
                      [inst_6 : AddCommMonoid M₂] →
                        [inst_7 : Module R₂ M₂] →
                          (f : M₁ →SL[σ₁₂] M₂) → (p : Submodule R₂ M₂) → (∀ (x : M₁), f x ∈ p) → M₁ →SL[σ₁₂] ↥p
-- Mathlib.RingTheory.TotallySplit
Algebra.IsFiniteSplit.instTensorProduct : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u_4}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [Algebra.IsFiniteSplit R S],
  Algebra.IsFiniteSplit T (TensorProduct R T S)
-- Mathlib.Algebra.Lie.Basic
/-- The composition of Lie module morphisms is a morphism.  -/
LieModuleHom.comp : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        {P : Type w₂} →
          [inst : CommRing R] →
            [inst_1 : LieRing L] →
              [inst_2 : AddCommGroup M] →
                [inst_3 : AddCommGroup N] →
                  [inst_4 : AddCommGroup P] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module R N] →
                        [inst_7 : Module R P] →
                          [inst_8 : LieRingModule L M] →
                            [inst_9 : LieRingModule L N] →
                              [inst_10 : LieRingModule L P] → (N →ₗ⁅R,L⁆ P) → (M →ₗ⁅R,L⁆ N) → M →ₗ⁅R,L⁆ P
-- Mathlib.Order.CompleteLattice.Defs
CompleteSemilatticeSup.mk : {α : Type u_8} →
  [toPartialOrder : PartialOrder α] →
    [toSupSet : SupSet α] → (∀ (s : Set α), IsLUB s (sSup s)) → CompleteSemilatticeSup α
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiff_add_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G]
  {a : G}, ContMDiff I I n fun x => x + a