mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- The counit for the equivalence `Comon (Mon C) ≌ Mon (Comon C)`.  -/
CategoryTheory.Bimon.equivMonComonCounitIsoApp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (M : CategoryTheory.Mon (CategoryTheory.Comon C)) →
          ((CategoryTheory.Bimon.ofMonComon C).comp (CategoryTheory.Bimon.toMonComon C)).obj M ≅ M
-- Mathlib.Topology.MetricSpace.Gluing
Metric.Sum.dist_eq_glueDist : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {p q : X ⊕ Y} (x : X) (y : Y),
  Metric.Sum.dist p q = Metric.glueDist (fun x_1 => ⋯.some) (fun x => ⋯.some) 1 p q
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RioSliceData.range : {α : Type u} → {β : Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Const.RioSliceData α β → Std.Rio α
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
/-- The base change map for endomorphisms of a free finite module.  -/
IsBaseChange.endHom : {R : Type u_1} →
  [inst : CommSemiring R] →
    {S : Type u_2} →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {M : Type u_3} →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] →
                {P : Type u_5} →
                  [inst_5 : AddCommMonoid P] →
                    [inst_6 : Module R P] →
                      [inst_7 : Module S P] →
                        [inst_8 : IsScalarTower R S P] →
                          {α : M →ₗ[R] P} → IsBaseChange S α → (M →ₗ[R] M) →ₗ[R] P →ₗ[S] P
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iInter_add_subset : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Add α] (s : ι → Set α) (t : Set α), (⋂ i, s i) + t ⊆ ⋂ i, s i + t
-- Mathlib.Topology.Algebra.Algebra
Subalgebra.valA_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A] (p : Subalgebra R A) (x : ↥p), p.valA x = ↑x
-- Mathlib.Order.Antisymmetrization
/-- Turn an element into its antisymmetrization.  -/
toAntisymmetrization : {α : Type u_1} → (r : α → α → Prop) → [inst : IsPreorder α r] → α → Antisymmetrization α r
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_inv_app_f_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))) (n : α),
  ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).unitIso.inv.app P).f.f n = P.p.f n
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement'.QuotientMulEquiv_apply : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [inst_1 : K.Normal] (h : H.IsComplement' K) (a : G ⧸ K),
  h.QuotientMulEquiv a = (Subgroup.IsComplement.leftQuotientEquiv h) a
-- Mathlib.CategoryTheory.Adjunction.Unique
/-- If `G` and `G'` are both right adjoint to `F`, then they are naturally isomorphic.  -/
CategoryTheory.Adjunction.rightAdjointUniq : {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] →
        {F : CategoryTheory.Functor C D} → {G G' : CategoryTheory.Functor D C} → (F ⊣ G) → (F ⊣ G') → (G ≅ G')
-- Mathlib.Order.Interval.Set.Monotone
Monotone.Ico : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β},
  Monotone f → Antitone g → Antitone fun x => Set.Ico (f x) (g x)
-- Mathlib.Algebra.Order.Antidiag.Finsupp
Finset.mapRange_finsuppAntidiag_eq : ∀ {ι : Type u_1} {μ : Type u_2} {μ' : Type u_3} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ]
  [inst_2 : Finset.HasAntidiagonal μ] [inst_3 : DecidableEq μ] [inst_4 : AddCommMonoid μ']
  [inst_5 : Finset.HasAntidiagonal μ'] [inst_6 : DecidableEq μ'] {e : μ ≃+ μ'} {s : Finset ι} {n : μ},
  Finset.map (Finsupp.mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) = s.finsuppAntidiag (e n)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` reflects finite limits, then `F.rightOp : C ⥤ Dᵒᵖ` reflects finite
colimits.  -/
CategoryTheory.Limits.reflectsFiniteColimits_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.ReflectsFiniteLimits F],
  CategoryTheory.Limits.ReflectsFiniteColimits F.rightOp
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.isEmptyAlgEquiv_symm_toRingHom : ∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] [inst_1 : IsEmpty σ],
  (MvPolynomial.isEmptyAlgEquiv R σ).symm.toRingEquiv.toRingHom = MvPolynomial.C
-- Mathlib.Algebra.Star.MonoidHom
/-- By definition, a star monoid equivalence preserves the `star` operation.  -/
StarMulEquiv.map_star' : ∀ {A : Type u_6} {B : Type u_7} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B] (self : A ≃⋆* B)
  (a : A), self.toFun (star a) = star (self.toFun a)
-- Mathlib.MeasureTheory.Measure.Haar.DistribChar
MeasureTheory.addHaarScalarFactor_smul_inv_eq_distribHaarChar : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  [inst_3 : TopologicalSpace A] [inst_4 : IsTopologicalAddGroup A] [inst_5 : LocallyCompactSpace A]
  [inst_6 : ContinuousConstSMul G A] [inst_7 : MeasurableSpace A] [inst_8 : BorelSpace A] (μ : MeasureTheory.Measure A)
  [inst_9 : μ.IsAddHaarMeasure] (g : G),
  μ.addHaarScalarFactor ((DomMulAct.mk g)⁻¹ • μ) = (MeasureTheory.distribHaarChar A) g
-- Mathlib.Order.ULift
ULift.down_beq : ∀ {α : Type u} [inst : BEq α] (a b : ULift.{u_1, u} α), (a.down == b.down) = (a == b)
-- Mathlib.RingTheory.Multiplicity
finiteMultiplicity_of_emultiplicity_eq_natCast : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {n : ℕ}, emultiplicity a b = ↑n → FiniteMultiplicity a b
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- Given two objects `a` and `b` in a bicategory,
this is the type of adjunctions between `a` and `b`.
 -/
CategoryTheory.Bicategory.Adj.Hom : {B : Type u} → [CategoryTheory.Bicategory B] → B → B → Type (max v w)
-- Mathlib.GroupTheory.OrderOfElement
/-- If a direct product has finite additive order then so does each component.  -/
IsOfFinAddOrder.apply : ∀ {η : Type u_6} {Gs : η → Type u_7} [inst : (i : η) → AddMonoid (Gs i)] {x : (i : η) → Gs i},
  IsOfFinAddOrder x → ∀ (i : η), IsOfFinAddOrder (x i)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.ConeMorphism.hom_inv_id_assoc : ∀ {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 d : CategoryTheory.Limits.Cone F} (f : c ≅ d) {Z : C} (h : c.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp f.hom.hom (CategoryTheory.CategoryStruct.comp f.inv.hom h) = h
-- Init.Data.Vector.Lemmas
Vector.exists_mem_iff_exists_getElem : ∀ {α : Type u_1} {n : ℕ} {P : α → Prop} {xs : Vector α n}, (∃ x ∈ xs, P x) ↔ ∃ i, ∃ (hi : i < n), P xs[i]
-- Mathlib.Analysis.Complex.RemovableSingularity
/-- **Removable singularity** theorem: if `s` is a neighborhood of `c : ℂ`, a function `f : ℂ → E`
is complex differentiable on `s \ {c}`, and $f(z) - f(c)=o((z-c)^{-1})$, then `f` redefined to be
equal to `limUnder (𝓝[≠] c) f` at `c` is complex differentiable on `s`.  -/
Complex.differentiableOn_update_limUnder_of_isLittleO : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {s : Set ℂ}
  {c : ℂ},
  s ∈ nhds c →
    DifferentiableOn ℂ f (s \ {c}) →
      ((fun z => f z - f c) =o[nhdsWithin c {c}ᶜ] fun z => (z - c)⁻¹) →
        DifferentiableOn ℂ (Function.update f c ((nhdsWithin c {c}ᶜ).limUnder f)) s
-- Aesop.Index.RulePattern
/-- Convert a rule pattern substitution map to a flat array of substitutions.  -/
Aesop.RulePatternSubstMap.toFlatArray : Aesop.RulePatternSubstMap → Array (Aesop.RuleName × Aesop.Substitution)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.comm₃₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂),
  CategoryTheory.CategoryStruct.comp sq₁.f₃₄ self.τ₄ = CategoryTheory.CategoryStruct.comp self.τ₃ sq₂.f₃₄
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.match_3.congr_eq_1 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1)
  (cOpt : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) (h_1 : Unit → motive none)
  (h_2 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some c)),
  cOpt = none →
    (match cOpt with
      | none => h_1 ()
      | some c => h_2 c) ≍
      h_1 ()
-- Mathlib.Algebra.Module.Torsion.Free
smul_ne_zero_iff_left : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R} {m : M}
  [Module.IsTorsionFree R M] [IsCancelMulZero R], m ≠ 0 → (r • m ≠ 0 ↔ r ≠ 0)
-- Mathlib.Analysis.Convolution
HasCompactSupport.continuous_convolution_left : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : AddCommGroup G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [inst_12 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [BorelSpace G],
  HasCompactSupport f →
    Continuous f → MeasureTheory.LocallyIntegrable g μ → Continuous (MeasureTheory.convolution f g L μ)
-- Mathlib.Order.UpperLower.Hom
UpperSet.coe_iciSupHom : ∀ {α : Type u_1} [inst : SemilatticeSup α], ⇑UpperSet.iciSupHom = UpperSet.Ici
-- Mathlib.Data.DFinsupp.Order
DFinsupp.single_tsub : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : ∀ (i : ι), CanonicallyOrderedAdd (α i)] [inst_3 : (i : ι) → Sub (α i)]
  [inst_4 : ∀ (i : ι), OrderedSub (α i)] {i : ι} {a b : α i} [inst_5 : DecidableEq ι],
  (fun₀ | i => a - b) = (fun₀ | i => a) - fun₀ | i => b
-- Mathlib.Algebra.Polynomial.Degree.Domain
Polynomial.natDegree_le_of_dvd : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {p q : Polynomial R}, p ∣ q → q ≠ 0 → p.natDegree ≤ q.natDegree
-- Std.Data.String.ToInt
Nat.isInt_repr : ∀ (n : ℕ), n.repr.isInt = true
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.Context.mk.injEq : ∀ (optionsPerPos : Lean.PrettyPrinter.Delaborator.OptionsPerPos) (currNamespace : Lean.Name)
  (openDecls : List Lean.OpenDecl) (inPattern : Bool) (subExpr : Lean.SubExpr) (depth lctxInitIndices : ℕ)
  (optionsPerPos_1 : Lean.PrettyPrinter.Delaborator.OptionsPerPos) (currNamespace_1 : Lean.Name)
  (openDecls_1 : List Lean.OpenDecl) (inPattern_1 : Bool) (subExpr_1 : Lean.SubExpr) (depth_1 lctxInitIndices_1 : ℕ),
  ({ optionsPerPos := optionsPerPos, currNamespace := currNamespace, openDecls := openDecls, inPattern := inPattern,
        subExpr := subExpr, depth := depth, lctxInitIndices := lctxInitIndices } =
      { optionsPerPos := optionsPerPos_1, currNamespace := currNamespace_1, openDecls := openDecls_1,
        inPattern := inPattern_1, subExpr := subExpr_1, depth := depth_1, lctxInitIndices := lctxInitIndices_1 }) =
    (optionsPerPos = optionsPerPos_1 ∧
      currNamespace = currNamespace_1 ∧
        openDecls = openDecls_1 ∧
          inPattern = inPattern_1 ∧ subExpr = subExpr_1 ∧ depth = depth_1 ∧ lctxInitIndices = lctxInitIndices_1)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.op_vadd_inter_nonempty_iff : ∀ {α : Type u_2} [inst : AddGroup α] {s t : Set α} {x : αᵃᵒᵖ},
  ((x +ᵥ s) ∩ t).Nonempty ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ -a + b = AddOpposite.unop x
-- Mathlib.Probability.Distributions.Geometric
ProbabilityTheory.geometricMeasure_real_singleton_pos : ∀ {p : ↑unitInterval}, p ≠ 0 → p ≠ 1 → ∀ (n : ℕ), 0 < (ProbabilityTheory.geometricMeasure p).real {n}
-- Init.Control.StateCps
StateCpsT.run'_eq : ∀ {α σ : Type u} {m : Type u → Type v} [inst : Monad m] (x : StateCpsT σ m α) (s : σ),
  x.run' s = x.runK s fun a x => pure a
-- Mathlib.Order.JordanHolder
JordanHolderLattice.iso_symm : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {x y : X × X},
  JordanHolderLattice.Iso x y → JordanHolderLattice.Iso y x
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.mk : {ι : Type u_1} →
  {I : BoxIntegral.Box ι} →
    BoxIntegral.Prepartition I →
      (tag : BoxIntegral.Box ι → ι → ℝ) →
        (∀ (J : BoxIntegral.Box ι), tag J ∈ BoxIntegral.Box.Icc I) → BoxIntegral.TaggedPrepartition I
-- Mathlib.Topology.Semicontinuity.Defs
/-- A relation `r : α → β → Prop` is semicontinuous within `s` at `x : α`, if whenever `r x y`
is true, it is also true for all `x'` sufficiently close to `x` within `s`.

This notion generalizes lower and upper semicontinuity of functions, as well as
lower and upper hemicontinuity of set-valued correspondences.  -/
SemicontinuousWithinAt : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → (α → β → Prop) → Set α → α → Prop
-- Mathlib.Data.Countable.Defs
Countable.mk : ∀ {α : Sort u}, (∃ f, Function.Injective f) → Countable α
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMap.match_1.splitter : {β' : Type u_1} →
  (motive : Option β' → Sort u_2) →
    (x : Option β') → (x = none → motive none) → ((out' : β') → x = some out' → motive (some out')) → motive x
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- `OneMemClass S M` says `S` is a type of subsets `s ≤ M`, such that `1 ∈ s` for all `s`.  -/
OneMemClass : (S : Type u_3) → (M : outParam (Type u_4)) → [One M] → [SetLike S M] → Prop
-- Batteries.Data.UInt
UInt16.toNat_min : ∀ (x y : UInt16), (x ⊓ y).toNat = min x.toNat y.toNat
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trCont.match_1.eq_3 : ∀ (motive : Turing.ToPartrec.Cont → Sort u_1) (a : List ℕ) (k : Turing.ToPartrec.Cont)
  (h_1 : Unit → motive Turing.ToPartrec.Cont.halt)
  (h_2 :
    (c : Turing.ToPartrec.Code) →
      (a : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₁ c a k))
  (h_3 : (a : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₂ a k))
  (h_4 : (c : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.comp c k))
  (h_5 : (c : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.fix c k)),
  (match Turing.ToPartrec.Cont.cons₂ a k with
    | Turing.ToPartrec.Cont.halt => h_1 ()
    | Turing.ToPartrec.Cont.cons₁ c a k => h_2 c a k
    | Turing.ToPartrec.Cont.cons₂ a k => h_3 a k
    | Turing.ToPartrec.Cont.comp c k => h_4 c k
    | Turing.ToPartrec.Cont.fix c k => h_5 c k) =
    h_3 a k
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map : ∀ (D : Type u₂) [inst : CategoryTheory.Category.{v₂, u₂} D] {X Y : CategoryTheory.Cat} (F : X ⟶ Y)
  {X_1 Y_1 : CategoryTheory.Join (↑X) D} (f : X_1 ⟶ Y_1),
  ((CategoryTheory.Join.pseudofunctorLeft D).map F).toFunctor.map f =
    CategoryTheory.Join.homInduction (fun x x_1 f => (CategoryTheory.Join.inclLeft (↑Y) D).map (F.toFunctor.map f))
      (fun x x_1 g => (CategoryTheory.Join.inclRight (↑Y) D).map g)
      (fun c d => CategoryTheory.Join.edge (F.toFunctor.obj c) d) f
-- Init.Data.Dyadic.Basic
Dyadic.ble.eq_1 : Dyadic.zero.ble Dyadic.zero = true
-- Mathlib.Data.Multiset.Antidiagonal
Multiset.antidiagonal_cons : ∀ {α : Type u_1} (a : α) (s : Multiset α),
  (a ::ₘ s).antidiagonal =
    Multiset.map (Prod.map id (Multiset.cons a)) s.antidiagonal +
      Multiset.map (Prod.map (Multiset.cons a) id) s.antidiagonal
-- Batteries.Lean.EStateM
EStateM.ext : ∀ {ε σ α : Type u_1} {x y : EStateM ε σ α}, (∀ (s : σ), x.run s = y.run s) → x = y
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The underlying profinite topological space.  -/
ProfiniteAddGrp.toProfinite : ProfiniteAddGrp.{u} → Profinite
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `setWidth`, `zeroExtend` and `signExtend` on `BitVec`s.  -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.reduceExtend : Lean.Name → ({n : ℕ} → (m : ℕ) → BitVec n → BitVec m) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.Topology.Separation.Basic
Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_3} {p : ι → Prop} {t : ι → Set X} {s : Set X},
  IsDiscrete s → ∀ {x : X}, (nhds x).HasBasis p t → x ∈ s → ∃ i, p i ∧ t i ∩ s = {x}
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_ne_of_natTrailingDegree_ne : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.natTrailingDegree ≠ n → p.trailingDegree ≠ ↑n
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.toLinearMap : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {N : Type u_7} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R N] →
                      {Q₁ : QuadraticMap R M₁ N} → {Q₂ : QuadraticMap R M₂ N} → (Q₁ →qᵢ Q₂) → M₁ →ₗ[R] M₂
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
/-- The center of `GL n R` consists of scalar matrices.  -/
Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] {g : GL n R},
  g ∈ Subgroup.center (GL n R) ↔ ↑g ∈ Set.range ⇑(Matrix.scalar n)
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.forallTelescopeImp : {α : Type} → Lean.Expr → (Array Lean.Expr → Lean.Expr → Lean.MetaM α) → Bool → Bool → Lean.MetaM α
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.RanIsSheafOfIsCocontinuous.lift.congr_simp : ∀ {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] {G : CategoryTheory.Functor C D} {A : Type w}
  [inst_2 : CategoryTheory.Category.{w', w} A] {J J_1 : CategoryTheory.GrothendieckTopology C} (e_J : J = J_1)
  {K : CategoryTheory.GrothendieckTopology D} [inst_3 : G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A}
  (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F}
  (hR hR_1 : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension),
  hR = hR_1 →
    ∀ {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)),
      CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s = CategoryTheory.RanIsSheafOfIsCocontinuous.lift ⋯ hR_1 s
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- Given a weight, `MvPolynomial` as a graded algebra  -/
MvPolynomial.weightedGradedAlgebra : (R : Type u_1) →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      {σ : Type u_3} →
        (w : σ → M) →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : DecidableEq M] → GradedAlgebra (MvPolynomial.weightedHomogeneousSubmodule R w)
-- Std.Http.Protocol.H1
/-- Processes a finished header block:
1. updates keep-alive policy from config and headers,
2. validates semantic message framing,
3. enforces configured body-size limits,
4. transitions into body/continue state and emits follow-up events.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.processHeaders : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.State.exprToSemiringId : Lean.Meta.Grind.Arith.CommRing.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ
-- Mathlib.Order.Hom.WithTopBot
SupHom.withTop_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β]
  [inst_2 : SemilatticeSup γ] (f : SupHom β γ) (g : SupHom α β), (f.comp g).withTop = f.withTop.comp g.withTop
-- Mathlib.Data.Nat.Cast.Order.Basic
/-- See also `Nat.ofNat_nonneg`, specialised to `IsOrderedRing`.  -/
Nat.ofNat_nonneg' : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] (n : ℕ)
  [inst_4 : n.AtLeastTwo], 0 ≤ OfNat.ofNat n
-- Mathlib.CategoryTheory.Subobject.Basic
/-- When `f : X ⟶ Y` is a monomorphism, `exists f` agrees with `map f`.
 -/
CategoryTheory.Subobject.exists_iso_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasImages C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Mono f], CategoryTheory.Subobject.exists f = CategoryTheory.Subobject.map f
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_le_algebraMap_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A]
  (f : R → R) (r : R) (a : A),
  autoParam (ContinuousOn f (spectrum R a)) cfc_le_algebraMap_iff._auto_1 →
    autoParam (p a) cfc_le_algebraMap_iff._auto_3 → (cfc f a ≤ (algebraMap R A) r ↔ ∀ x ∈ spectrum R a, f x ≤ r)
-- Mathlib.Algebra.Group.Action.TransferInstance
/-- Transfer `VAddAssocClass` across an `Equiv`  -/
Equiv.vaddAssocClass : ∀ (M : Type u_1) (N : Type u_2) {α : Type u_4} {β : Type u_5} [inst : VAdd M N] [inst_1 : VAdd M β] [inst_2 : VAdd N β]
  (e : α ≃ β) [VAddAssocClass M N β], VAddAssocClass M N α
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Mapping from types to its "ring id". We cache failures using `none`.
`nctypeIdOf[type]` is `some id`, then `id < ncRings.size`.  -/
Lean.Meta.Grind.Arith.CommRing.State.nctypeIdOf : Lean.Meta.Grind.Arith.CommRing.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_eq_zero_of_infinite : ∀ {α : Type u_1} [Infinite α], Nat.card α = 0
-- Init.Grind.Ring.Basic
/-- In every semiring there is a canonical map from the natural numbers to the semiring,
providing the values of `0` and `1`. Note that this function need not be injective.
 -/
Lean.Grind.Semiring.natCast : {α : Type u} → [self : Lean.Grind.Semiring α] → NatCast α
-- Init.Tactics
/-- The `*` location refers to all hypotheses and the goal.  -/
Lean.Parser.Tactic.locationWildcard : Lean.ParserDescr
-- Mathlib.Order.RelSeries
LTSeries.head_range : ∀ (n : ℕ), RelSeries.head (LTSeries.range n) = 0
-- Mathlib.Algebra.Lie.Nilpotent
/-- If the quotient of a Lie module `M` by a Lie submodule on which the Lie algebra acts trivially
is nilpotent then `M` is nilpotent.

This is essentially the Lie module equivalent of the fact that a central
extension of nilpotent Lie algebras is nilpotent. See `LieAlgebra.nilpotent_of_nilpotent_quotient`
below for the corresponding result for Lie algebras.  -/
LieModule.nilpotentOfNilpotentQuotient : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  {N : LieSubmodule R L M},
  N ≤ LieModule.maxTrivSubmodule R L M → LieModule.IsNilpotent L (M ⧸ N) → LieModule.IsNilpotent L M