mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.mapDomainBialgHomEquiv_symm_apply : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Group G]
  [inst_3 : Group H] (f : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H),
  MonoidAlgebra.mapDomainBialgHomEquiv.symm f = MonoidAlgebra.mapDomainOfBialgHom f
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_eq_if : ∀ {m n : ℕ}, (m<...=n).toList = if m + 1 ≤ n then (m + 1) :: ((m + 1)<...=n).toList else []
-- Mathlib.Algebra.Polynomial.Splits
_private.Mathlib.Algebra.Polynomial.Splits.0.Polynomial.«term_~ᵤ_» : Lean.TrailingParserDescr
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
Finsupp.DegLex.single_strictAnti : ∀ {α : Type u_1} [inst : LinearOrder α], StrictAnti fun a => toDegLex fun₀ | a => 1
-- Init.Grind.Module.Basic
Lean.Grind.IntModule.toNatModule : {M : Type u} → [I : Lean.Grind.IntModule M] → Lean.Grind.NatModule M
-- Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
/-- The coefficient of a monomial in a product `f * g` that can be reached in at most one way
as a product of monomials in the supports of `f` and `g` is a product.  -/
MonoidAlgebra.coeff_mul_mul_of_uniqueMul : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : Mul A] {f g : MonoidAlgebra R A} {a0 b0 : A},
  UniqueMul f.coeff.support g.coeff.support a0 b0 → (f * g).coeff (a0 * b0) = f.coeff a0 * g.coeff b0
-- Init.Data.Slice.List.Lemmas
ListSlice.size_eq_length_toList : ∀ {α : Type u_1} {xs : ListSlice α}, Std.Slice.size xs = (Std.Slice.toList xs).length
-- Init.Data.List.Lemmas
List.ne_and_not_mem_of_not_mem_cons : ∀ {α : Type u_1} {a y : α} {l : List α}, a ∉ y :: l → a ≠ y ∧ a ∉ l
-- Mathlib.Analysis.Analytic.Constructions
hasFPowerSeriesOnBall_pi_iff : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {e : E} {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)] {f : (i : ι) → E → Fm i}
  {r : ENNReal} {p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)},
  0 < r →
    (HasFPowerSeriesOnBall (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) e r ↔
      ∀ (i : ι), HasFPowerSeriesOnBall (f i) (p i) e r)
-- Mathlib.RingTheory.Ideal.Maps
Module.comap_annihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {R₀ : Type u_4}
  [inst_3 : CommSemiring R₀] [inst_4 : Module R₀ M] [inst_5 : Algebra R₀ R] [IsScalarTower R₀ R M],
  Ideal.comap (algebraMap R₀ R) (Module.annihilator R M) = Module.annihilator R₀ M
-- Lean.Elab.Tactic.Doc
/-- The docstring for the tactic  -/
Lean.Elab.Tactic.Doc.TacticDoc.docString : Lean.Elab.Tactic.Doc.TacticDoc → Option String
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.mul_sInter_subset : ∀ {α : Type u_2} [inst : Mul α] (s : Set α) (T : Set (Set α)), s * ⋂₀ T ⊆ ⋂ t ∈ T, s * t
-- Mathlib.Analysis.Real.Cardinality
/-- The cardinality of the interval $(a, ∞)$.  -/
Cardinal.mk_Ioi_real : ∀ (a : ℝ), Cardinal.mk ↑(Set.Ioi a) = Cardinal.continuum
-- Mathlib.GroupTheory.IsSubnormal
Subgroup.IsSubnormal.brecOn : ∀ {G : Type u_1} [inst : Group G] {motive : (a : Subgroup G) → a.IsSubnormal → Prop} {a : Subgroup G}
  (t : a.IsSubnormal), (∀ (a : Subgroup G) (t : a.IsSubnormal), Subgroup.IsSubnormal.below t → motive a t) → motive a t
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation of `r : R` is less than `WithZero.exp (-n)` if and only if
`vⁿ` divides the ideal `(r)`.  -/
IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R)
  (n : ℕ), v.intValuation r ≤ WithZero.exp (-↑n) ↔ v.asIdeal ^ n ∣ Ideal.span {r}
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [inst : BEq α] [Std.LawfulBEqOrd α]
  [Std.TransOrd α] [inst_3 : Inhabited α] (h : t.WF) {l : List α} {k : α},
  k ∉ t → l.contains k = false → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)).getKey! k = default
-- Mathlib.Algebra.Opposites
MulOpposite.unop_inj : ∀ {α : Type u_1} {x y : αᵐᵒᵖ}, MulOpposite.unop x = MulOpposite.unop y ↔ x = y
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.compl_inv : ∀ {α : Type u_2} [inst : Inv α] {s : Set α}, sᶜ⁻¹ = s⁻¹ᶜ
-- Mathlib.Algebra.Category.Ring.FilteredColimits
CommRingCat.FilteredColimits.forget_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget CommRingCat)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.transfer : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {H : SimpleGraph V} {p : G.Walk u v} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet),
  p.IsPath → (p.transfer H hp).IsPath
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.neg_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H X : C} [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.AddGrpObj H] (f : X ⟶ G) (g : G ⟶ H)
  [CategoryTheory.IsAddMonHom g], CategoryTheory.CategoryStruct.comp (-f) g = -CategoryTheory.CategoryStruct.comp f g
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instNonUnitalCommSemiring : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] →
        [IsOrderedCancelAddMonoid Γ] → [inst : NonUnitalCommSemiring R] → NonUnitalCommSemiring (HahnSeries Γ R)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- The left adjoint mate `ᘁf : ᘁY ⟶ ᘁX` of a morphism `f : X ⟶ Y`.  -/
CategoryTheory.leftAdjointMate : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y : C} →
        [inst_2 : CategoryTheory.HasLeftDual X] → [inst_3 : CategoryTheory.HasLeftDual Y] → (X ⟶ Y) → (ᘁY ⟶ ᘁX)
-- Mathlib.Order.Filter.Lift
Filter.lift'_bot : ∀ {α : Type u_1} {β : Type u_2} {h : Set α → Set β}, Monotone h → ⊥.lift' h = Filter.principal (h ∅)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `≠` on `BitVec`s.  -/
BitVec.reduceNe : Lean.Meta.Simp.Simproc
-- Mathlib.Condensed.Discrete.Colimit
/-- `locallyConstantPresheaf` restricted to finite sets is isomorphic to `finYoneda F`.  -/
LightCondensed.locallyConstantIsoFinYoneda : (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) →
  FintypeCat.toLightProfinite.op.comp
      (LightCondensed.locallyConstantPresheaf
        (F.obj (FintypeCat.toLightProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1}))))) ≅
    LightCondensed.finYoneda F
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_mul_sphere : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x y : E), {x} * Metric.sphere y δ = Metric.sphere (x * y) δ
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.IsColimit.descCoconeMorphism_eq_isInitial_to : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c)
  (s : CategoryTheory.Limits.Cocone F), hc.descCoconeMorphism s = (c.isColimitEquivIsInitial hc).to s
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.substAlgHom_X : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} (ha : MvPowerSeries.HasSubst a) (s : σ),
  (MvPowerSeries.substAlgHom ha) (MvPowerSeries.X s) = a s
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientGroup.quotientQuotientIsometryEquivQuotient.eq_1 : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] {S T : Subgroup M} (h : S ≤ T),
  QuotientGroup.quotientQuotientIsometryEquivQuotient h =
    { toEquiv := (QuotientGroup.quotientQuotientEquivQuotient S T h).toEquiv, isometry_toFun := ⋯ }
-- Mathlib.Logic.Equiv.Fin.Basic
finAddFlip.eq_1 : ∀ {m n : ℕ}, finAddFlip = (finSumFinEquiv.symm.trans (Equiv.sumComm (Fin m) (Fin n))).trans finSumFinEquiv
-- Mathlib.Topology.Algebra.UniformMulAction
/-- The action of `Semiring.toOppositeModule` is uniformly continuous.  -/
Ring.uniformContinuousConstSMul_op : ∀ (R : Type u) [inst : Ring R] [inst_1 : UniformSpace R] [IsUniformAddGroup R] [ContinuousMul R],
  UniformContinuousConstSMul Rᵐᵒᵖ R
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.sizeLt.injEq : ∀ (lhs n lhs_1 n_1 : ℕ),
  (Lean.Meta.Grind.EMatchTheoremConstraint.sizeLt lhs n = Lean.Meta.Grind.EMatchTheoremConstraint.sizeLt lhs_1 n_1) =
    (lhs = lhs_1 ∧ n = n_1)
-- Mathlib.Algebra.Exact.Basic
LinearEquiv.conj_exact_iff_exact : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {P : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : AddCommMonoid P]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R N'] [inst_8 : Module R P] (f : M →ₗ[R] N)
  (g : N →ₗ[R] P) (e : N ≃ₗ[R] N'), Function.Exact ⇑(↑e ∘ₗ f) ⇑(g ∘ₗ ↑e.symm) ↔ Function.Exact ⇑f ⇑g
-- Std.Http.Data.URI.Encoding
/-- Appends a single encoded query character to an encoded query string.
 -/
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.EncodedQueryString.push : {r : UInt8 → Bool} →
  Std.Http.URI.EncodedQueryString r →
    (c : UInt8) → Std.Http.URI.isEncodedQueryChar r c = true → Std.Http.URI.EncodedQueryString r
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_eq_right_iff : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] [IsDomain k] [Module.IsTorsionFree k V1] {p₀ p₁ : P1} {c : k},
  (AffineMap.lineMap p₀ p₁) c = p₁ ↔ p₀ = p₁ ∨ c = 1
-- Mathlib.Topology.UniformSpace.Closeds
IsUniformEmbedding.nonemptyCompacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β}
  (hf : IsUniformEmbedding f), IsUniformEmbedding (TopologicalSpace.NonemptyCompacts.map f ⋯)
-- Mathlib.Topology.Path
Path.mul_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Mul X] [inst_2 : ContinuousMul X] {a₁ b₁ a₂ b₂ : X}
  (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) (a : ↑unitInterval), (γ₁.mul γ₂) a = γ₁ a * γ₂ a
-- Init.Data.Array.Lemmas
Array.getElem?_setIfInBounds_self_of_lt : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {a : α}, i < xs.size → (xs.setIfInBounds i a)[i]? = some a
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.natCard_powers_le_orderOf : ∀ {G : Type u_1} [inst : Monoid G] {a : G}, IsOfFinOrder a → Nat.card ↑↑(Submonoid.powers a) ≤ orderOf a
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.SpecTensorTo_SpecOfPoint : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↥(CategoryTheory.Limits.pullback f g)),
  (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).SpecTensorTo (AlgebraicGeometry.Scheme.Pullback.SpecOfPoint t) =
    t
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.Opposite.instAdditiveOppositeShiftFunctorInt : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (n : ℤ),
  (CategoryTheory.shiftFunctor Cᵒᵖ n).Additive
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {km fallback : α}, t.maxKey? = some km → t.getKeyD km fallback = km
-- Mathlib.Topology.Closure
interior_inter : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, interior (s ∩ t) = interior s ∩ interior t
-- Mathlib.NumberTheory.NumberField.CMField
/-- A totally complex field that has a unique complex conjugation is CM.
 -/
NumberField.IsCMField.of_forall_isConj : ∀ (K : Type u_2) [inst : Field K] [inst_1 : CharZero K] [Algebra.IsIntegral ℚ K] [NumberField.IsTotallyComplex K]
  [IsGalois ℚ K] {σ : Gal(K/ℚ)}, (∀ (φ : K →+* ℂ), NumberField.ComplexEmbedding.IsConj φ σ) → NumberField.IsCMField K
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.faithful_map₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L)
  (β : R.comp G ⟶ F.comp R') [F.Faithful], (CategoryTheory.StructuredArrow.map₂ α β).Faithful
-- Mathlib.CategoryTheory.Limits.Final
/-- Given a colimit cocone over `F ⋙ G` we can construct a colimit cocone over `G`.  -/
CategoryTheory.Functor.Final.colimitCoconeOfComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [F.Final] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                {G : CategoryTheory.Functor D E} →
                  CategoryTheory.Limits.ColimitCocone (F.comp G) → CategoryTheory.Limits.ColimitCocone G
-- Mathlib.Control.Random
/-- A monad transformer to generate random objects using the generic generator type `g`  -/
RandGT : Type → (Type u_1 → Type u_2) → Type u_1 → Type (max u_1 u_2)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Decomp.0.SimpleGraph.Walk.takeUntil.match_1.splitter : {V : Type u_1} →
  {G : SimpleGraph V} →
    {v : V} →
      (motive : (w : V) → (x : G.Walk v w) → (x_1 : V) → x_1 ∈ x.support → Sort u_2) →
        (w : V) →
          (x : G.Walk v w) →
            (x_1 : V) →
              (x_2 : x_1 ∈ x.support) →
                ((u : V) → (h : u ∈ SimpleGraph.Walk.nil.support) → motive v SimpleGraph.Walk.nil u h) →
                  ((w v_1 : V) →
                      (r : G.Adj v v_1) →
                        (p : G.Walk v_1 w) →
                          (u : V) →
                            (h : u ∈ (SimpleGraph.Walk.cons r p).support) → motive w (SimpleGraph.Walk.cons r p) u h) →
                    motive w x x_1 x_2
-- Mathlib.Order.Filter.Basic
/-- Eta-expanded form of `Filter.EventuallyEq.const_vadd` -/
Filter.EventuallyEq.fun_const_vadd : ∀ {α : Type u} {β : Type v} {γ : Type u_2} [inst : VAdd γ β] {f g : α → β} {l : Filter α},
  f =ᶠ[l] g → ∀ (c : γ), (fun i => c +ᵥ f i) =ᶠ[l] fun i => c +ᵥ g i
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.preimage_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (b : β),
  ⇑e ⁻¹' Set.Ici b = Set.Ici (e.symm b)
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.apply_eq_of_preconnectedSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [PreconnectedSpace X] {f : X → Y},
  IsLocallyConstant f → ∀ (x y : X), f x = f y
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.compl.congr_simp : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α] {m : ℕ} (hm : m + n = Fintype.card α),
  Set.powersetCard.compl hm = Set.powersetCard.compl hm
-- Lean.Elab.PreDefinition.FixedParams
/-- Are all fixed parameters a non-reordered prefix?
 -/
Lean.Elab.FixedParamPerms.fixedArePrefix : Lean.Elab.FixedParamPerms → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
CategoryTheory.hoFunctor.isIso_prodComparison : ∀ (X Y : SSet), CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison SSet.hoFunctor X Y)
-- Mathlib.Topology.Algebra.Module.IsWeak
LinearMap.isWeak_iff : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  [t : TopologicalSpace E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜),
  B.IsWeak ↔ t = TopologicalSpace.induced (fun x1 x2 => (B x1) x2) Pi.topologicalSpace
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.integer_valuation : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), A.valuation.integer = A.toSubring
-- Init.Data.ByteArray.Basic
ByteArray.Iterator.mk : ByteArray → ℕ → ByteArray.Iterator
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- There exists a colimit for `F`  -/
CategoryTheory.Limits.HasColimit.exists_colimit : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C}
  {F : CategoryTheory.Functor J C} [self : CategoryTheory.Limits.HasColimit F],
  Nonempty (CategoryTheory.Limits.ColimitCocone F)
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.PredTrans.pushExcept.match_1.eq_2 : ∀ {α ε : Type u_1} (motive : Except ε α → Sort u_2) (e : ε) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.error e with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_2 e
-- Lean.Meta.Structure
/-- Checks if the expression is of the form `S.mk x.1 ... x.n` with `n` nonzero
and `S.mk` a structure constructor with `S` one of the recorded structure parents.
Returns `x`.
Each projection `x.i` can be either a native projection or from a projection function.
 -/
Lean.Meta.etaStruct? : Lean.Expr → (Lean.Name → Bool) → Lean.MetaM (Option Lean.Expr)
-- Init.Data.Int.Basic
/-- `x < y` for kernel reduction.  -/
Int.blt' : ℤ → ℤ → Bool
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.h_comp_σ_succ_of_lt_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  (self : CategoryTheory.SimplicialObject.Homotopy f g) {n : ℕ} (i j : Fin (n + 1)),
  j ≤ i →
    ∀ {Z : C} (h : Y.obj (Opposite.op { len := n + 1 + 1 }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (self.h j) (CategoryTheory.CategoryStruct.comp (Y.σ i.succ) h) =
        CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (self.h j.castSucc) h)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.lt_map_of_int_lt_translationNumber : ∀ (f : CircleDeg1Lift) {n : ℤ}, ↑n < f.translationNumber → ∀ (x : ℝ), x + ↑n < f x
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.apply_one : ∀ {E : Type u_3} [inst : AddGroup E] [inst_1 : DecidableEq E] (x : E), 1 x = if x = 0 then 0 else 1
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.hom_comp : ∀ {X Y T : AddGrpCat} (f : X ⟶ Y) (g : Y ⟶ T),
  AddGrpCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (AddGrpCat.Hom.hom g).comp (AddGrpCat.Hom.hom f)
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurable_from_top : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace β] {f : α → β}, Measurable f
-- Init.Data.String.Lemmas.Splits
String.Pos.splits_append_rawEndPos : ∀ {s t : String}, ((s ++ t).pos s.rawEndPos ⋯).Splits s t
-- Mathlib.Lean.MessageData.ForExprs
/-- Iterate over the tags of a `Format` using `f`.  -/
_private.Mathlib.Lean.MessageData.ForExprs.0.Lean.MessageData.forExprsIn.goFmt : {m : Type → Type u} →
  [Monad m] →
    {σ : Type} →
      (Lean.PPContext × Lean.Expr → σ → m (ForInStep σ)) →
        Lean.PPContext → Lean.PrettyPrinter.InfoPerPos → σ → Std.Format → m (ForInStep σ)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The equalizer of an idempotent morphism and the identity is split mono.  -/
CategoryTheory.Limits.splitMonoOfIdempotentEqualizer : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {f : X ⟶ X} →
        CategoryTheory.CategoryStruct.comp f f = f →
          [inst_1 : CategoryTheory.Limits.HasEqualizer (CategoryTheory.CategoryStruct.id X) f] →
            CategoryTheory.SplitMono (CategoryTheory.Limits.equalizer.ι (CategoryTheory.CategoryStruct.id X) f)
-- Mathlib.Algebra.Module.PUnit
PUnit.instMulAction : {R : Type u_1} → MulAction PUnit.{u_3 + 1} R
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsIntegral.isAlgebraic_iff_top : ∀ (R : Type u_1) (S : Type u_2) {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S]
  [Algebra.IsIntegral R S] [FaithfulSMul R S], Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic S A
-- Mathlib.Logic.Equiv.Multiset
Denumerable.lower.eq_2 : ∀ (x m : ℕ) (l : List ℕ), Denumerable.lower (m :: l) x = (m - x) :: Denumerable.lower l m
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.le_iff_le : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {a : α} {b : β}, l a ≤ b ↔ a ≤ u b
-- Batteries.Data.String.Lemmas
String.revFind_of_valid : ∀ (p : Char → Bool) (s : String),
  String.Legacy.revFind s p =
    Option.map (fun x => { byteIdx := String.utf8Len x }) (List.dropWhile (fun x => !p x) s.toList.reverse).tail?
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.evaln.match_1.eq_8 : ∀ (motive : ℕ → Nat.Partrec.Code → Sort u_1) (k : ℕ) (cf cg : Nat.Partrec.Code)
  (h_1 : (x : Nat.Partrec.Code) → motive 0 x) (h_2 : (k : ℕ) → motive k.succ Nat.Partrec.Code.zero)
  (h_3 : (k : ℕ) → motive k.succ Nat.Partrec.Code.succ) (h_4 : (k : ℕ) → motive k.succ Nat.Partrec.Code.left)
  (h_5 : (k : ℕ) → motive k.succ Nat.Partrec.Code.right)
  (h_6 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.pair cg))
  (h_7 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.comp cg))
  (h_8 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.prec cg))
  (h_9 : (k : ℕ) → (cf : Nat.Partrec.Code) → motive k.succ cf.rfind'),
  (match k.succ, cf.prec cg with
    | 0, x => h_1 x
    | k.succ, Nat.Partrec.Code.zero => h_2 k
    | k.succ, Nat.Partrec.Code.succ => h_3 k
    | k.succ, Nat.Partrec.Code.left => h_4 k
    | k.succ, Nat.Partrec.Code.right => h_5 k
    | k.succ, cf.pair cg => h_6 k cf cg
    | k.succ, cf.comp cg => h_7 k cf cg
    | k.succ, cf.prec cg => h_8 k cf cg
    | k.succ, cf.rfind' => h_9 k cf) =
    h_8 k cf cg
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- The functor `Set.Iic i ⥤ C` obtained by "restriction" of `F : Set.Iic j ⥤ C`
when `i ≤ j`.  -/
CategoryTheory.SmallObject.restrictionLE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : PartialOrder J] →
        {j : J} → CategoryTheory.Functor (↑(Set.Iic j)) C → {i : J} → i ≤ j → CategoryTheory.Functor (↑(Set.Iic i)) C
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.range_swap : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H], (Monoid.Coprod.swap G H).range = ⊤
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHomFunctor_map_app : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] (C : Type u)
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X Y : Cᵒᵖ}
  (φ : X ⟶ Y) (Y_1 : C), ((CategoryTheory.eHomFunctor V C).map φ).app Y_1 = CategoryTheory.eHomWhiskerRight V φ.unop Y_1
-- Mathlib.Order.CompleteBooleanAlgebra
compl_sSup' : ∀ {α : Type u} [inst : CompleteBooleanAlgebra α] {s : Set α}, (sSup s)ᶜ = sInf (compl '' s)
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.map_eq_range_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M},
  Submodule.map f p = f.range ↔ Codisjoint p f.ker
-- Mathlib.Condensed.Light.Epi
LightCondMod.instReflectsEpimorphismsLightCondSetForget : ∀ (R : Type u) [inst : Ring R], (LightCondensed.forget R).ReflectsEpimorphisms
-- Mathlib.Data.Fin.VecNotation
Matrix.empty_eq : ∀ {α : Type u} (v : Fin 0 → α), v = ![]