mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.instSMulCommClass : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {S : Type u_10} [inst_5 : Monoid S]
  [inst_6 : DistribMulAction S N] [inst_7 : SMulCommClass R S N] {T : Type u_11} [inst_8 : Monoid T]
  [inst_9 : DistribMulAction T N] [inst_10 : SMulCommClass R T N] [SMulCommClass S T N],
  SMulCommClass S T (M [⋀^ι]→ₗ[R] N)
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.prodFunctorToFunctorProdAssociator_inv_app_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.Category.{v₃, u₃} E] (A : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A]
  (X : (CategoryTheory.Functor A C × CategoryTheory.Functor A D) × CategoryTheory.Functor A E) (X_1 : A),
  ((CategoryTheory.prod.prodFunctorToFunctorProdAssociator C D E A).inv.app X).app X_1 =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (X.1.1.obj X_1))
      (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (X.1.2.obj X_1))
        (CategoryTheory.CategoryStruct.id (X.2.obj X_1)))
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjOpcyclesSelfIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C),
  (HomologicalComplex.singleObjOpcyclesSelfIso c j A).hom =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j A).inv
      (((HomologicalComplex.single C c j).obj A).pOpcycles j)
-- Mathlib.Algebra.Order.Module.Defs
PosSMulStrictMono.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α],
  (∀ ⦃a : α⦄, 0 < a → ∀ ⦃b₁ b₂ : β⦄, b₁ < b₂ → a • b₁ < a • b₂) → PosSMulStrictMono α β
-- Init.Data.UInt.Lemmas
UInt16.two_mul : ∀ {a : UInt16}, 2 * a = a + a
-- Mathlib.Topology.Order.AtTopBotIxx
map_coe_Ioo_atBot : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {a b : X},
  a < b →
    autoParam (Order.IsPredPrelimit a) map_coe_Ioo_atBot._auto_1 →
      Filter.map Subtype.val Filter.atBot = nhdsWithin a (Set.Ioi a)
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instFromJsonDidChangeWatchedFilesParams : Lean.FromJson Lean.Lsp.DidChangeWatchedFilesParams
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
/-- The diagram consisting of the `U i` and `U i ⊓ U j` is cofinal in the diagram
of all opens contained in some `U i`.
 -/
TopCat.Presheaf.SheafCondition.instFinalPairwiseOpensLeCoverPairwiseToOpensLeCover : ∀ {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X),
  (TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover U).Final
-- Mathlib.Analysis.Complex.AbelLimit
/-- **Abel's limit theorem**. Given a power series converging at 1, the corresponding function
is continuous at 1 when approaching 1 within a fixed Stolz set.  -/
Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzSet : ∀ {f : ℕ → ℂ} {l : ℂ},
  Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l) →
    ∀ {M : ℝ}, Filter.Tendsto (fun z => ∑' (n : ℕ), f n * z ^ n) (nhdsWithin 1 (Complex.stolzSet M)) (nhds l)
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.of.eq_1 : ∀ (M : Type u) [inst : CommMonoid M], CommMonCat.of M = { carrier := M, str := inst }
-- Mathlib.Data.Set.Image
Set.image_injective : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Injective (Set.image f) ↔ Function.Injective f
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insert!.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v : β k) (size : ℕ) (k' : α) (v' : β k')
  (l' r' : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.insert! k v (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.balanceL! k' v' (Std.DTreeMap.Internal.Impl.insert! k v l') r'
    | Ordering.gt => Std.DTreeMap.Internal.Impl.balanceR! k' v' l' (Std.DTreeMap.Internal.Impl.insert! k v r')
    | Ordering.eq => Std.DTreeMap.Internal.Impl.inner size k v l' r'
-- Batteries.Data.List.Perm
List.Perm.idxBij_rightInverse_idxBij_symm : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs ys : List α} (h : xs.Perm ys),
  Function.RightInverse h.idxBij ⋯.idxBij
-- Mathlib.Data.Nat.Multiplicity
Nat.Prime.emultiplicity_self : ∀ {p : ℕ}, Nat.Prime p → emultiplicity p p = 1
-- Mathlib.Algebra.Homology.HomologySequence
CategoryTheory.ShortComplex.ShortExact.comp_δ_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j) {Z : C} (h : S.X₁.homology j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap S.g i)
      (CategoryTheory.CategoryStruct.comp (hS.δ i j hij) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Data.List.Permutation
_private.Mathlib.Data.List.Permutation.0.Nat.factorial.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Algebra.Torsor.Defs
/-- Cancellation multiplying the results of two divisions.  -/
sdiv_mul_sdiv_cancel : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] (p₁ p₂ p₃ : P), (p₁ /ₛ p₂) * (p₂ /ₛ p₃) = p₁ /ₛ p₃
-- Mathlib.Topology.MetricSpace.Bounded
Metric.ediam_eq_top_iff_unbounded : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α], Metric.ediam s = ⊤ ↔ ¬Bornology.IsBounded s
-- Mathlib.Combinatorics.Additive.Energy
/-- The additive energy of two finsets `s` and `t` in a group is the number of quadruples
`(a₁, a₂, b₁, b₂) ∈ s × s × t × t` such that `a₁ + b₁ = a₂ + b₂`.  -/
Combinatorics.Additive.«termE[_,_]» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.image_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {t : Set β} {a : α}, (fun x => a +ᵥ x) '' t = a +ᵥ t
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.sub_const : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  DiffContOnCl 𝕜 f s → ∀ (c : F), DiffContOnCl 𝕜 (fun x => f x - c) s
-- Mathlib.Geometry.Manifold.Instances.Real
IccRightChart_symm_apply_of_le : ∀ {x y : ℝ} [hxy : Fact (x < y)] {z : EuclideanHalfSpace 1} (hz : (↑z).ofLp 0 ≤ y - x),
  ↑(IccRightChart x y).symm z = ⟨y - (↑z).ofLp 0, ⋯⟩
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
Float.Model.UnpackedFloat.packedInfinity.eq_1 : ∀ (spec : Float.Model.Format) (sign : Float.Model.UnpackedFloat.Sign),
  Float.Model.UnpackedFloat.packedInfinity spec sign =
    Float.Model.UnpackedFloat.packComponents spec sign (-1#spec.exponentBits) 0
-- Mathlib.Probability.Distributions.Fernique
ProbabilityTheory.Fernique.logRatio_mul_normThreshold_add_one_le : ∀ {a : ℝ} {c : ENNReal},
  2⁻¹ < c →
    c < 1 →
      ∀ (n : ℕ),
        ProbabilityTheory.Fernique.logRatio c * ProbabilityTheory.Fernique.normThreshold a (n + 1) ^ 2 * a⁻¹ ^ 2 ≤
          2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.instToString : {α : Type u_1} → [ToString α] → ToString (Ordnode α)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- Given `I ≤ J`, this is the map `Spec(Γ(X, U)/J(U)) ⟶ Spec(Γ(X, U)/I(U))`.  -/
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom : {X : AlgebraicGeometry.Scheme} →
  {I J : X.IdealSheafData} → I ≤ J → (U : ↑X.affineOpens) → J.glueDataObj U ⟶ I.glueDataObj U
-- Init.Data.String.Lemmas.Slice
String.Pos.get?_eq_dif : ∀ {s : String} {p : s.Pos}, p.get? = if h : p = s.endPos then none else some (p.get h)
-- Mathlib.GroupTheory.Archimedean
/-- If a nontrivial additive subgroup of a linear ordered additive commutative group
is disjoint with the interval `Set.Ioo 0 a` for some positive `a`, then the set of positive
elements of this group admits the least element.  -/
AddSubgroup.exists_isLeast_pos : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G]
  {H : AddSubgroup G}, H ≠ ⊥ → ∀ {a : G}, 0 < a → Disjoint (↑H) (Set.Ioo 0 a) → ∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.MonadicityInternal.counitCofork_ι_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (B : D)
  (X : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Monad.MonadicityInternal.counitCofork adj B).ι.app X =
    CategoryTheory.Limits.WalkingParallelPair.rec
      (CategoryTheory.CategoryStruct.comp (adj.counit.app (F.obj (G.obj B))) (adj.counit.app B)) (adj.counit.app B) X
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.incl_of_counitAppApp : ∀ {P : TopCat → Prop} [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  {S : CompHausLike P} {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))}
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}]
  (f : LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1}))))
  [inst_2 : CategoryTheory.Limits.PreservesFiniteProducts Y] [inst_3 : CompHausLike.HasExplicitFiniteCoproducts P]
  (a : Function.Fiber ⇑f),
  (CategoryTheory.ConcreteCategory.hom (Y.map (CompHausLike.LocallyConstant.sigmaIncl f a).op))
      ((CategoryTheory.ConcreteCategory.hom (CompHausLike.LocallyConstant.counitAppApp S Y)) f) =
    CompHausLike.LocallyConstant.counitAppAppImage f a
-- Std.Time.Format.Modifier
Std.Time.instInhabitedText.default : Std.Time.Text
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.closure_univ : ∀ {M : Type u_1} [inst : AddZeroClass M], AddSubmonoid.closure Set.univ = ⊤
-- Init.Data.Int.Order
Int.toNat_negSucc : ∀ (n : ℕ), (Int.negSucc n).toNat = 0
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂Aux_eq : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] {σ₁ σ₂ : R →+* R} [inst_7 : Fintype n]
  [inst_8 : Fintype m] [inst_9 : DecidableEq m] [inst_10 : DecidableEq n] (b₁ : Module.Basis n R M₁)
  (b₂ : Module.Basis m R M₂) (B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂),
  (LinearMap.toMatrix₂Aux R ⇑b₁ ⇑b₂) B = (LinearMap.toMatrix₂ b₁ b₂) B
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.ofRestrict : ∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)),
  AlgebraicGeometry.IsOpenImmersion (X.ofRestrict h)
-- Mathlib.Order.RelSeries
RelSeries.rel_of_lt : ∀ {α : Type u_1} {r : SetRel α α} [r.IsTrans] (x : RelSeries r) {i j : Fin (x.length + 1)},
  i < j → (x.toFun i, x.toFun j) ∈ r
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.continuous_aeval : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {a : S} [inst_2 : UniformSpace R]
  [inst_3 : UniformSpace S] [inst_4 : IsUniformAddGroup R] [inst_5 : IsTopologicalSemiring R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : T2Space S] [inst_8 : CompleteSpace S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S] (ha : PowerSeries.HasEval a),
  Continuous ⇑(PowerSeries.aeval ha)
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the largest element of the tree set, returning `fallback` if the tree set is empty.
 -/
Std.ExtTreeSet.maxD : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → α → α
-- Mathlib.Algebra.RingQuot
RingQuot.Rel.below : {R : Type uR} →
  [inst : Semiring R] →
    {r : R → R → Prop} →
      {motive : (a a_1 : R) → RingQuot.Rel r a a_1 → Prop} → {a a_1 : R} → RingQuot.Rel r a a_1 → Prop
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.eraseTR.go.eq_def : ∀ {α : Type u_1} [inst : BEq α] (l : List α) (a : α) (a_1 : List α) (a_2 : Array α),
  List.eraseTR.go✝ l a a_1 a_2 =
    match a_1, a_2 with
    | [], x => l
    | x :: xs, acc => bif x == a then acc.toListAppend xs else List.eraseTR.go✝ l a xs (acc.push x)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.mk : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : Add A] →
        [inst_1 : Add B] →
          [inst_2 : Mul A] →
            [inst_3 : Mul B] →
              [inst_4 : SMul R A] →
                [inst_5 : SMul R B] →
                  [inst_6 : Star A] →
                    [inst_7 : Star B] →
                      (toStarRingEquiv : A ≃⋆+* B) →
                        (∀ (r : R) (a : A), toStarRingEquiv.toFun (r • a) = r • toStarRingEquiv.toFun a) → A ≃⋆ₐ[R] B
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
USize.reduceToNat : Lean.Meta.Simp.Simproc
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.mem_ι_image_iff : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) {x : ↥U} {V : (↑U).Opens},
  ↑x ∈ (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V ↔ x ∈ V
-- Mathlib.Order.Bounds.Basic
/-- In a directed order, the union of bounded above sets is bounded above.  -/
BddAbove.union : ∀ {α : Type u_1} [inst : Preorder α] [IsDirectedOrder α] {s t : Set α}, BddAbove s → BddAbove t → BddAbove (s ∪ t)
-- Mathlib.AlgebraicTopology.SimplicialSet.Op
/-- The functor `opFunctor : SSet ⥤ SSet` is an involution.  -/
SSet.opFunctorCompOpFunctorIso : SSet.opFunctor.comp SSet.opFunctor ≅ CategoryTheory.Functor.id SSet
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.HasSubobjectClassifier.truthIsSplitMono`. -/
CategoryTheory.HasClassifier.truthIsSplitMono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasSubobjectClassifier C],
  CategoryTheory.IsSplitMono (CategoryTheory.HasSubobjectClassifier.truth C)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.affineSpan_range_medial : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [inst_5 : CharZero k] (s : Affine.Simplex k P n),
  affineSpan k (Set.range s.medial.points) = affineSpan k (Set.range s.points)
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_eq_Ioc_same_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioo a b = Set.Ioc a b ↔ ¬a < b
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKey!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.Equiv t₂ → t₁.getKey! k = t₂.getKey! k
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
/-- The unit associated to a representative of `2 • P` for a Jacobian point representative `P` on a
Weierstrass curve `W` that is `2`-torsion.

More specifically, the unit `u` such that `W.add P P = u • ![1, 1, 0]` where `P = W.neg P`.  -/
WeierstrassCurve.Jacobian.dblU : {R : Type r} → [CommRing R] → WeierstrassCurve.Jacobian R → (Fin 3 → R) → R
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.mk.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} (x : M) (y : ↥S), Localization.mk x y = x /ₒ y
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.isAcyclic_add_edge_iff_of_not_reachable : ∀ {V : Type u_1} {G : SimpleGraph V} (x y : V), ¬G.Reachable x y → ((G ⊔ SimpleGraph.edge x y).IsAcyclic ↔ G.IsAcyclic)
-- Mathlib.Logic.Pairwise
Std.Refl.set_pairwise_iff : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} [Std.Refl r], s.Pairwise r ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b
-- Std.Data.HashMap.Lemmas
Std.HashMap.insertMany_list_singleton : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {k : α} {v : β},
  m.insertMany [(k, v)] = m.insert k v
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_emptyWithCapacity : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {a fallback : α} {c : ℕ},
  (Std.HashSet.emptyWithCapacity c).getD a fallback = fallback
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_le_mul_iff_right : ∀ {a b c : ENNReal}, a ≠ 0 → a ≠ ⊤ → (a * b ≤ a * c ↔ b ≤ c)
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplexHomeomorphUnitInterval_one : stdSimplexHomeomorphUnitInterval ⟨Pi.single 1 1, ⋯⟩ = 1
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.lift_unique : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P]
  {f : M →+ P} {g : N →+ P} {fg : AddMonoid.Coprod M N →+ P},
  fg.comp AddMonoid.Coprod.inl = f → fg.comp AddMonoid.Coprod.inr = g → fg = AddMonoid.Coprod.lift f g
-- Mathlib.Algebra.Category.CommBialgCat
_private.Mathlib.Algebra.Category.CommBialgCat.0.CommBialgCat.Hom.mk : {R : Type u} → [inst : CommRing R] → {A B : CommBialgCat R} → (↑A →ₐc[R] ↑B) → A.Hom B
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (I : Ideal R)
  [hI : I.IsPrime] [inst_3 : IsLocalization.AtPrime S I] (a : ↑(Set.Iic { asIdeal := I, isPrime := hI })),
  ↑((RelIso.symm (IsLocalization.AtPrime.primeSpectrumOrderIso S I)) a).asIdeal =
    ⋂ s,
      ⋂ (_ :
        ↑↑((OrderIso.setCongr (fun p => p.IsPrime ∧ Disjoint ↑I.primeCompl ↑p) (fun p => p.IsPrime ∧ p ≤ I) ⋯).symm
                ⟨(↑a).asIdeal, ⋯⟩) ⊆
          ⇑(algebraMap R S) ⁻¹' ↑s),
        ↑s
-- Mathlib.Topology.FiberPartition
TopologicalSpace.Fiber.instCompactSpaceElemValSetMemRangeCoeLocallyConstantPreimageSingleton : ∀ {S : Type u_1} {Y : Type u_2} [inst : TopologicalSpace S] (l : LocallyConstant S Y) [CompactSpace S]
  (x : Function.Fiber ⇑l), CompactSpace ↑↑x
-- Lean.Meta.Tactic.Grind.Arith.Linear.PP
Lean.Meta.Grind.Arith.Linear.ppStruct? : Lean.Meta.Grind.Goal → Lean.Meta.Grind.Arith.Linear.Struct → Lean.MetaM (Option Lean.MessageData)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.isConstant_comp_tendsto : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f : α → β} {lc : Filter γ} {g : γ → α},
  (↑f).IsConstant → Filter.Tendsto g lc l → (↑(f ∘ g)).IsConstant
-- Mathlib.CategoryTheory.Abelian.Subobject
/-- A well-powered abelian category is also well-copowered.  -/
CategoryTheory.Abelian.wellPowered_opposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.WellPowered.{w, v, u} C],
  CategoryTheory.WellPowered.{w, v, u} Cᵒᵖ
-- Mathlib.Algebra.GroupWithZero.Basic
exists_right_inv_of_exists_left_inv : ∀ {α : Type u_3} [inst : MonoidWithZero α], (∀ (a : α), a ≠ 0 → ∃ b, b * a = 1) → ∀ {a : α}, a ≠ 0 → ∃ b, a * b = 1
-- Mathlib.Analysis.InnerProductSpace.PiL2
DirectSum.IsInternal.collectedOrthonormalBasis.eq_1 : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {A : ι → Submodule 𝕜 E}
  (hV : OrthogonalFamily 𝕜 (fun i => ↥(A i)) fun i => (A i).subtypeₗᵢ) [inst_4 : DecidableEq ι]
  (hV_sum : DirectSum.IsInternal fun i => A i) {α : ι → Type u_7} [inst_5 : (i : ι) → Fintype (α i)]
  (v_family : (i : ι) → OrthonormalBasis (α i) 𝕜 ↥(A i)),
  DirectSum.IsInternal.collectedOrthonormalBasis hV hV_sum v_family =
    (hV_sum.collectedBasis fun i => (v_family i).toBasis).toOrthonormalBasis ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- `Cofork.ofπ π w` is a colimit cocone in `Cᵒᵖ` if and only if `Fork.ofι π'.unop w'` in `C` is
a limit cone.  -/
CategoryTheory.Limits.Cofork.isColimitOfπEquivIsLimitUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y P : Cᵒᵖ} →
      {f g : X ⟶ Y} →
        (π π' : Y ⟶ P) →
          (w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π) →
            (w' :
                CategoryTheory.CategoryStruct.comp π'.unop f.unop = CategoryTheory.CategoryStruct.comp π'.unop g.unop) →
              π = π' →
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ π w) ≃
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι π'.unop w')
-- Mathlib.MeasureTheory.PiSystem
generatePiSystem.brecOn : ∀ {α : Type u_1} {S : Set (Set α)} {motive : (a : Set α) → generatePiSystem S a → Prop} {a : Set α}
  (t : generatePiSystem S a),
  (∀ (a : Set α) (t : generatePiSystem S a), generatePiSystem.below t → motive a t) → motive a t
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.eapproxDiff.eq_2 : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : α → ENNReal) (n : ℕ),
  MeasureTheory.SimpleFunc.eapproxDiff f n.succ =
    MeasureTheory.SimpleFunc.map ENNReal.toNNReal
      (MeasureTheory.SimpleFunc.eapprox f (n + 1) - MeasureTheory.SimpleFunc.eapprox f n)
-- Lean.Compiler.IR.Format
Lean.IR.instToFormatArg : Std.ToFormat Lean.IR.Arg
-- Lean.Environment
/-- Commits the kernel environment of the given environment back to the main branch.  -/
Lean.Environment.PromiseCheckedResult.commitChecked : Lean.Environment.PromiseCheckedResult → Lean.Environment → BaseIO Unit
-- Mathlib.Dynamics.Ergodic.Action.Basic
ErgodicSMul.toSMulInvariantMeasure : ∀ {G : Type u_1} {α : Type u_2} {inst : SMul G α} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [self : ErgodicSMul G α μ], MeasureTheory.SMulInvariantMeasure G α μ
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.paramsPos : Lean.Meta.RecursorInfo → List (Option ℕ)
-- Mathlib.CategoryTheory.Localization.Bifunctor
CategoryTheory.Localization.natTrans₂_ext : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] (L₁ : CategoryTheory.Functor C₁ D₁)
  (L₂ : CategoryTheory.Functor C₂ D₂) (W₁ : CategoryTheory.MorphismProperty C₁)
  (W₂ : CategoryTheory.MorphismProperty C₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [W₁.ContainsIdentities]
  [W₂.ContainsIdentities] {F₁' F₂' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)} {τ τ' : F₁' ⟶ F₂'},
  (∀ (X₁ : C₁) (X₂ : C₂), (τ.app (L₁.obj X₁)).app (L₂.obj X₂) = (τ'.app (L₁.obj X₁)).app (L₂.obj X₂)) → τ = τ'
-- Mathlib.Algebra.Lie.Basis.Base
LieAlgebra.Basis.h'.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) (i : ι), b.h' i = ⟨b.h i, ⋯⟩
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Given three points in strict order on the same line, and a fourth point, the angles at the
fourth point between the first and second or first and third points have the same sign.  -/
Sbtw.oangle_sign_eq_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P} (p₄ : P),
  Sbtw ℝ p₁ p₂ p₃ → (EuclideanGeometry.oangle p₁ p₄ p₂).sign = (EuclideanGeometry.oangle p₁ p₄ p₃).sign
-- Mathlib.Order.Filter.SmallSets
Filter.smallSets_bot : ∀ {α : Type u_1}, ⊥.smallSets = pure ∅