mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
CommMonCat.FilteredColimits.colimitCommMonoid : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J CommMonCat) → CommMonoid ↑(CommMonCat.FilteredColimits.M F)
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_add_right₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Add β]
  [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.Kernel.IndepFun (f i) (f j + f k) κ μ
-- Mathlib.Data.Prod.Basic
Prod.Lex.refl_left : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Refl r] (x : α × β), Prod.Lex r s x x
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.mem_sInf : ∀ {α : Type u_2} [inst : TopologicalSpace α] {S : Set (TopologicalSpace.Closeds α)} {x : α}, x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Group.covariant_iff_contravariant : ∀ {N : Type u_2} {r : N → N → Prop} [inst : Group N],
  Covariant N N (fun x1 x2 => x1 * x2) r ↔ Contravariant N N (fun x1 x2 => x1 * x2) r
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.unop_injective : ∀ {R : Type u_2} [inst : NonAssocSemiring R], Function.Injective Subsemiring.unop
-- Lean.PrettyPrinter.Formatter
/-- Stack of generated Format objects, analogous to the Syntax stack in the parser.
Note, however, that the stack is reversed because of the right-to-left traversal.  -/
Lean.PrettyPrinter.Formatter.State.stack : Lean.PrettyPrinter.Formatter.State → Array Std.Format
-- Mathlib.Algebra.Algebra.Subalgebra.Prod
Subalgebra.coe_prod : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (S : Subalgebra R A) (S₁ : Subalgebra R B), ↑(S.prod S₁) = ↑S ×ˢ ↑S₁
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instReprTransition : Repr Std.Time.TimeZone.Transition
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- We compute the absolute discriminant of a `p ^ (k + 1)`-th cyclotomic field.
Beware that in the case `p ^ k = 2` the formula uses `1 / 2 = 0`. See also the results below.  -/
IsCyclotomicExtension.Rat.discr_prime_pow_succ : ∀ (p k : ℕ) (K : Type u) [inst : Field K] [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K],
  NumberField.discr K = (-1) ^ (p ^ k * (p - 1) / 2) * ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
-- Mathlib.Topology.UniformSpace.Completion
/-- Automatic coercion from `α` to its completion. Not always injective.  -/
UniformSpace.Completion.instCoe : (α : Type u_1) → [inst : UniformSpace α] → Coe α (UniformSpace.Completion α)
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.commMagma.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : CommMagma M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (mul : ∀ (x y : M₁), f (x * y) = f x * f y), Function.Injective.commMagma f hf mul = { toMul := inst, mul_comm := ⋯ }
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given a family of sets `t : ι → Set α`, a finite set `I` in the index type such that
all sets `t i`, `i ∈ I`, are finite, if all `t i`, `i ∈ I`, are pairwise disjoint, then the
sum of `f a` over `a ∈ ⋃ i ∈ I, t i` is equal to the sum over `i ∈ I` of the sums of `f a`
over `a ∈ t i`.  -/
finsum_mem_biUnion : ∀ {α : Type u_1} {ι : Type u_3} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {I : Set ι} {t : ι → Set α},
  I.PairwiseDisjoint t →
    I.Finite →
      (∀ i ∈ I, (t i).Finite) →
        ∑ᶠ (a : α) (_ : a ∈ ⋃ x ∈ I, t x), f a = ∑ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j
-- Mathlib.Util.PrintSorries
/-- Collects all uses of `sorry` by the declaration `c`.
It finds all transitive uses as well.

This is a version of `Lean.CollectAxioms.collect` that keeps track of enough information to print
each use of `sorry`.
 -/
Mathlib.PrintSorries.collect : Lean.Name → StateT Mathlib.PrintSorries.State Lean.MetaM Unit
-- Mathlib.Data.Fintype.Sum
image_subtype_univ_ssubset_image_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] (k : β) (b : α → β),
  k ∈ Finset.image b Finset.univ →
    ∀ (p : β → Prop) [inst_2 : DecidablePred p],
      ¬p k → Finset.image (fun i => b ↑i) Finset.univ ⊂ Finset.image b Finset.univ
-- Mathlib.RingTheory.Unramified.LocalStructure
_private.Mathlib.RingTheory.Unramified.LocalStructure.0.Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn_of_finite : ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Q : Ideal S)
  [inst_3 : Q.IsPrime] [Module.Finite R S] [Algebra.IsUnramifiedAt R Q], ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
-- Lean.Environment
Lean.Kernel.Exception.exprTypeMismatch : Lean.Kernel.Environment → Lean.LocalContext → Lean.Expr → Lean.Expr → Lean.Kernel.Exception
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
tangentBundleCore.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] (I I_1 : ModelWithCorners 𝕜 E H)
  (e_I : I = I_1) (M : Type u_6) [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M],
  tangentBundleCore I M = tangentBundleCore I_1 M
-- Init.Data.Array.Erase
Array.eraseP_of_forall_getElem_not : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, (∀ (i : ℕ) (h : i < xs.size), ¬p xs[i] = true) → xs.eraseP p = xs
-- Std.Data.ExtDHashMap.Basic
/-- Internal implementation detail of the hash map.  -/
Std.ExtDHashMap.mk : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → Std.ExtDHashMap α β
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.subset_total : ∀ {x y : ZFSet.{u}}, x.IsOrdinal → y.IsOrdinal → x ⊆ y ∨ y ⊆ x
-- Mathlib.Tactic.ApplyWith
_private.Mathlib.Tactic.ApplyWith.0.Mathlib.Tactic.instEvalExprApplyConfig_mathlib : Lean.Elab.ConfigEval.EvalExpr Lean.Meta.ApplyConfig
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isUVar? : Lean.Name → Option ℕ
-- Mathlib.RingTheory.RamificationInertia.Inertia
Ideal.inertiaDeg_above_le : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.IsPrime] [r.LiesOver q] [Module.Finite R T], r.inertiaDeg S ≤ r.inertiaDeg R
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.IsDominant.of_comp_of_isOpenImmersion : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.IsDominant (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.IsOpenImmersion g],
  AlgebraicGeometry.IsDominant f
-- Mathlib.Topology.EMetricSpace.Defs
PseudoEMetricSpace.toUniformSpace : {α : Type u} → [self : PseudoEMetricSpace α] → UniformSpace α
-- Mathlib.Topology.Bornology.Real
Real.instIsOrderBornology : IsOrderBornology ℝ
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.π₃_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C), CategoryTheory.Pretriangulated.Triangle.π₃.obj T = T.obj₃
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `smul_apply`. -/
ContinuousLinearMap.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.simplicialCosimplicialEquiv_counitIso_hom_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor SimplexCategory Cᵒᵖ)
  (X_1 : SimplexCategory),
  ((CategoryTheory.simplicialCosimplicialEquiv C).counitIso.hom.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
TopRep.d_comp_d_assoc : ∀ {k : Type u_1} {G : Type u_2} [inst : Ring k] [inst_1 : Group G] [inst_2 : TopologicalSpace k]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) {Z : TopRep k G}
  (h : X.resolutionX (n + 1 + 1) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.d n) (CategoryTheory.CategoryStruct.comp (X.d (n + 1)) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.FunDecl.type : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.FunDecl pu → Lean.Expr
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.mapAlgHom_monomial : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (n : ℕ) (a : A),
  (Polynomial.mapAlgHom f) ((Polynomial.monomial n) a) = (Polynomial.monomial n) (f a)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.getLT_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {h' : ∃ a ∈ t₁, cmp a k = Ordering.lt} (h : t₁.Equiv t₂), t₁.getLT k h' = t₂.getLT k ⋯
-- Std.Http.Data.URI
/-- Attempts to parse a `RequestTarget` from the given string.
 -/
Std.Http.RequestTarget.parse? : String → Option Std.Http.RequestTarget
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_le_csSup_of_nonempty_inter : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s t : Set α},
  (s ∩ t).Nonempty →
    autoParam (BddBelow s) csInf_le_csSup_of_nonempty_inter._auto_1 →
      autoParam (BddAbove t) csInf_le_csSup_of_nonempty_inter._auto_3 → sInf s ≤ sSup t
-- Std.Data.DHashMap.Raw
/-- Two hash maps are equivalent in the sense of `Equiv` iff
all the keys and values are equal.
 -/
Std.DHashMap.Raw.Equiv : {α : Type u} → {β : α → Type v} → Std.DHashMap.Raw α β → Std.DHashMap.Raw α β → Prop
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.restrict₀_of_ne_zero : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : GroupWithZero B] {f : A →*₀ B} {a : A}
  (h : f a ≠ 0), (MonoidWithZeroHom.ValueGroup₀.restrict₀ f) a = ↑⟨Units.mk0 (f a) h, ⋯⟩
-- Lean.MonadEnv
Lean.withEnv : {m : Type → Type} → {α : Type} → [Monad m] → [MonadFinally m] → [Lean.MonadEnv m] → Lean.Environment → m α → m α
-- Mathlib.ModelTheory.Complexity
/-- An auxiliary operation to `FirstOrder.Language.BoundedFormula.toPrenex`.
If `φ` is quantifier-free and `ψ` is in prenex normal form, then `φ.toPrenexImpRight ψ`
is a prenex normal form for `φ.imp ψ`.  -/
FirstOrder.Language.BoundedFormula.toPrenexImpRight : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α n → L.BoundedFormula α n → L.BoundedFormula α n
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumLocallyUniformlyOn.tsum_eqOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β] [T2Space α],
  HasSumLocallyUniformlyOn f g s → Set.EqOn (fun x => ∑' (i : ι), f i x) g s
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.IsAffineMap.map_sum_weights : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} {I : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid N]
  [inst_6 : Module R N] {f : M → N} [inst_7 : Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M]
  [inst_9 : Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N],
  Convexity.IsAffineMap R f →
    ∀ (w : Convexity.StdSimplex R I) (g : I → M),
      f (w.weights.sum fun i r => r • g i) = w.weights.sum fun i r => r • f (g i)
-- Mathlib.Algebra.FreeAlgebra
/-- Coercion from `R` to `Pre R X`. Note: Used for notation only.  -/
FreeAlgebra.Pre.hasCoeSemiring : (R : Type u_1) → (X : Type u_2) → Coe R (FreeAlgebra.Pre R X)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Cofan.IsColimit.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type u_1} {F : I → C} {c : CategoryTheory.Limits.Cofan F}
  (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f g : c.pt ⟶ A),
  (∀ (i : I), CategoryTheory.CategoryStruct.comp (c.inj i) f = CategoryTheory.CategoryStruct.comp (c.inj i) g) → f = g
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instMulOneClass : {M : Type u_1} →
  [inst : TopologicalSpace M] → [inst_1 : MulOneClass M] → [ContinuousMul M] → MulOneClass (SeparationQuotient M)
-- Mathlib.Data.Seq.Defs
/-- Embed an infinite stream as a sequence  -/
Stream'.Seq.ofStream : {α : Type u} → Stream' α → Stream'.Seq α
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Multiplying by all the matrices either in `listTransvecCol M` and `listTransvecRow M` kills
all the coefficients in the last column but the last one.  -/
Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_row : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
  M (Sum.inr ()) (Sum.inr ()) ≠ 0 →
    ∀ (i : Fin r),
      ((Matrix.Pivot.listTransvecCol M).prod * M * (Matrix.Pivot.listTransvecRow M).prod) (Sum.inl i) (Sum.inr ()) = 0
-- Mathlib.Data.Int.Bitwise
Int.bodd_coe : ∀ (n : ℕ), (↑n).bodd = n.bodd
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereo_left_inv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1)
  {x : ↑(Metric.sphere 0 1)}, ↑x ≠ v → stereoInvFun hv (stereoToFun v ↑x) = x
-- Std.Time.Format.Modifier
/-- `Fraction` represents the fraction of a second, which can either be full nanoseconds
or a truncated form with fewer digits.
 -/
Std.Time.Fraction : Type
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.elabInductiveViewsPostprocessing : Array Lean.Elab.Command.InductiveView → Lean.Elab.Command.CommandElabM Unit
-- Lean.Parser.Types
Lean.Parser.ParserCacheEntry.newPos : Lean.Parser.ParserCacheEntry → String.Pos.Raw
-- Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
SSet.Homotopy.h₀_assoc : ∀ {X Y : SSet} {f g : X ⟶ Y} (H : SSet.Homotopy f g) {Z : SSet} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.ι₀ (CategoryTheory.CategoryStruct.comp H.h h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.MutuallySingular.add_left : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N]
  {v₁ v₂ : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} [T2Space N]
  [inst_5 : ContinuousAdd M], v₁.MutuallySingular w → v₂.MutuallySingular w → (v₁ + v₂).MutuallySingular w
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.mk : ∀ {S : Type u_3} {G : outParam (Type u_4)} [inst : DivInvMonoid G] [inst_1 : SetLike S G]
  [toSubmonoidClass : SubmonoidClass S G] [toInvMemClass : InvMemClass S G], SubgroupClass S G
-- Mathlib.Combinatorics.Matroid.Basic
/-- A `RankPos` matroid is one whose bases are nonempty.  -/
Matroid.RankPos : {α : Type u_1} → Matroid α → Prop
-- Mathlib.Topology.Order.Real
EReal.denseRange_ratCast : DenseRange fun r => ↑↑r
-- Mathlib.Data.UInt
UInt16.instCommMonoid : CommMonoid UInt16
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RocSlice.instToIterator : {α : Type u_1} →
  {β : α → Type v} →
    [inst : Ord α] →
      Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.RocSliceData α β)) Id (Std.DTreeMap.Internal.RxcIterator α β)
        ((a : α) × β a)
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.measure_stieltjesOfMeasurableRat_Iic : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : Measurable f) (a : α) (x : ℝ),
  (ProbabilityTheory.stieltjesOfMeasurableRat f hf a).measure (Set.Iic x) =
    ENNReal.ofReal (↑(ProbabilityTheory.stieltjesOfMeasurableRat f hf a) x)
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.toLp_sub : ∀ (p : ENNReal) {V : Type u_4} [inst : AddCommGroup V] (x y : V),
  WithLp.toLp p (x - y) = WithLp.toLp p x - WithLp.toLp p y
-- Mathlib.ModelTheory.LanguageMap
/-- A language map defined on two factors of a sum.  -/
FirstOrder.Language.LHom.sumElim : {L : FirstOrder.Language} →
  {L' : FirstOrder.Language} → (L →ᴸ L') → {L'' : FirstOrder.Language} → (L'' →ᴸ L') → (L.sum L'' →ᴸ L')
-- Mathlib.Algebra.Order.UpperLower
UpperSet.coe_div : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α] (s t : UpperSet α),
  ↑(s / t) = ↑s / ↑t
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_functor_obj_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) (X : CategoryTheory.MorphismProperty.Comma L₁ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).functor.obj X).left = X.left
-- Mathlib.Order.Hom.Lattice
SupHomClass.toOrderHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : SemilatticeSup α]
  [inst_2 : SemilatticeSup β] [SupHomClass F α β], OrderHomClass F α β
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.σ_comp_σ : ∀ {n : ℕ} {i j : Fin (n + 1)},
  i ≤ j →
    CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ i.castSucc) (SimplexCategoryGenRel.σ j) =
      CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ j.succ) (SimplexCategoryGenRel.σ i)
-- Mathlib.Algebra.Category.Grp.EpiMono
_private.Mathlib.Algebra.Category.Grp.EpiMono.0.GrpCat.SurjectiveOfEpiAuxs.termX : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Types
/-- State of the case-splitting module.  -/
Lean.Meta.Grind.GoalState.split : Lean.Meta.Grind.GoalState → Lean.Meta.Grind.Split.State
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α}, t.contains a = false → t.get? a = none
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonCompletionClientCapabilities : Lean.FromJson Lean.Lsp.CompletionClientCapabilities
-- Mathlib.Algebra.GradedMonoid
/-- Multiplication by `one` on the left is the identity  -/
GradedMonoid.GMonoid.one_mul : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : AddMonoid ι} [self : GradedMonoid.GMonoid A] (a : GradedMonoid A), 1 * a = a
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_of_continuousOn_differentiableOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : ℕ∞},
  (∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s) →
    (∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s) → ContDiffOn 𝕜 (↑n) f s
-- Mathlib.Analysis.Convex.Jensen
/-- Canonical form of the **equality case of Jensen's equality**.

For a strictly concave function `f` and nonnegative weights `w`, we have
`f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)` if and only if the points `p` with nonzero
weight are all equal (and in fact all equal to their center of mass w.r.t. `w`).  -/
StrictConcaveOn.map_sum_eq_iff' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConcaveOn 𝕜 s f →
    (∀ i ∈ t, 0 ≤ w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) →
          (f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, w j ≠ 0 → p j = ∑ i ∈ t, w i • p i)
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
/-- Evaluation at a point for left invariant derivations. Same thing as for generic global
derivations (`Derivation.evalAt`).  -/
LeftInvariantDerivation.evalAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] →
                        [inst_7 : ContMDiffMul I (↑⊤) G] →
                          (g : G) → LeftInvariantDerivation I G →ₗ[𝕜] PointDerivation I g
-- Mathlib.Algebra.Group.Defs
isLeftCancelAdd_iff : ∀ (G : Type u) [inst : Add G], IsLeftCancelAdd G ↔ ∀ (a : G), IsAddLeftRegular a
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.comp_assoc_of_second_degree_eq_neg_third_degree : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K L : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁)
  (z₂ : CochainComplex.HomComplex.Cochain G K (-n₂)) (z₃ : CochainComplex.HomComplex.Cochain K L n₂)
  (h₁₂ : n₁ + -n₂ = n₁₂), (z₁.comp z₂ h₁₂).comp z₃ ⋯ = z₁.comp (z₂.comp z₃ ⋯) ⋯
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.Transversal.mk : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            (∀ (i : ι), Function.Injective ⇑(φ i)) →
              (set : (i : ι) → Set (G i)) →
                (∀ (i : ι), 1 ∈ set i) →
                  (∀ (i : ι), Subgroup.IsComplement (↑(φ i).range) (set i)) → Monoid.PushoutI.NormalWord.Transversal φ
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.commute_of_mem_adjoin_self : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {a b : A},
  b ∈ NonUnitalAlgebra.adjoin R {a} → Commute a b
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.pow_of_dvd : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M},
  IsPrimitiveRoot ζ k → ∀ {p : ℕ}, p ≠ 0 → p ∣ k → IsPrimitiveRoot (ζ ^ p) (k / p)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max?_erase_le_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k km kme : α}
  (hkme : (t.erase k).max? = some kme), t.max?.get ⋯ = km → (cmp kme km).isLE = true
-- Init.Grind.Order
Lean.Grind.Order.int_lt : ∀ {x y k k' : ℤ}, k'.beq' (k - 1) = true → x < y + k → x ≤ y + k'
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.id_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.LaxMonoidalFunctor C D),
  (CategoryTheory.CategoryStruct.id F).hom = CategoryTheory.CategoryStruct.id F.toFunctor