mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The `r`th page of the spectral sequence.  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequence.page : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            CategoryTheory.Abelian.SpectralObject C ι →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀ →
                    (r : ℤ) → r₀ ≤ r → HomologicalComplex C (c r)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasSum_ite_eq' : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (b : β)
  [inst_2 : DecidablePred fun x => b = x] (a : α) (L : optParam (SummationFilter β) (SummationFilter.unconditional β))
  [L.LeAtTop], HasSum (fun b' => if b = b' then a else 0) a L
-- Init.Data.String.Substring
/-- Removes the specified number of characters (Unicode code points) from the end of a substring
by moving its end position towards its start position.

If the substring's start position is reached, the end position is not retracted past it.
 -/
Substring.Raw.dropRight : Substring.Raw → ℕ → Substring.Raw
-- Lean.PrettyPrinter.Formatter
/-- When the `leadWord` is nonempty, whether it is an identifier. Identifiers get space inserted between them.  -/
Lean.PrettyPrinter.Formatter.State.leadWordIdent : Lean.PrettyPrinter.Formatter.State → Bool
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobject_arrow_comp_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  {f : X ⟶ Y} {g : Y ⟶ Z} [inst_2 : CategoryTheory.Limits.HasImage f]
  [CategoryTheory.Epi (CategoryTheory.Limits.factorThruImageSubobject f)],
  CategoryTheory.CategoryStruct.comp f g = 0 →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow g = 0
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
AffineSubspace.pointwise_vadd_span : ∀ {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (v : V) (s : Set P), v +ᵥ affineSpan k s = affineSpan k (v +ᵥ s)
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
/-- The basis of `(g * X - 1) / (g * X - 1)²` given by the image of `g * X - 1`.

This is def-eq to `(SubmersivePresentation.localizationAway T g).basisCotangent`, but
```
(SubmersivePresentation.localizationAway T g).toExtension =
  (Generators.localizationAway T g).toExtension
```
is not reducibly def-eq. Hence using the general `SubmersivePresentation.basisCotangent` leads
to `erw` hell.
 -/
Algebra.Generators.basisCotangentAway : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (r : R) →
            [inst_3 : IsLocalization.Away r S] →
              Module.Basis Unit S (Algebra.Generators.localizationAway S r).toExtension.Cotangent
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.d₀₁_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G) (m : ↑A) (g : G),
  (ModuleCat.Hom.hom (groupCohomology.d₀₁ A)) m g = (A.ρ g) m - m
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.emptyWithCapacity_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {c : ℕ},
  Std.ExtHashMap.emptyWithCapacity c = ∅
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, panicking if no such pair exists.
 -/
Std.ExtDTreeMap.Const.getEntryLE! : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → [Std.TransCmp cmp] → [Inhabited (α × β)] → Std.ExtDTreeMap α (fun x => β) cmp → α → α × β
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.uniformity_eq_comap_totalLengthFilter : ∀ {X : Type u_1} [inst : PseudoMetricSpace X],
  uniformity X = Filter.comap (fun x => (1, fun x_1 => x)) AbsolutelyContinuousOnInterval.totalLengthFilter
-- Mathlib.Data.List.Defs
/-- Monadic variant of `foldlIdx`.  -/
List.foldlIdxM : {m : Type v → Type w} → [Monad m] → {α : Type u_7} → {β : Type v} → (ℕ → β → α → m β) → β → List α → m β
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.imp_mono_l : ∀ {σs : List (Type u)} {P P' Q : Std.Do.SPred σs}, (P' ⊢ₛ P) → (P → Q) ⊢ₛ P' → Q
-- Mathlib.Algebra.QuadraticAlgebra.Basic
/-- Every element of a quadratic algebra satisfies its characteristic equation.  -/
QuadraticAlgebra.sq_sub_trace_smul_add_norm_eq_zero : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (z : QuadraticAlgebra R a b),
  z ^ 2 - QuadraticAlgebra.trace z • z + (algebraMap R (QuadraticAlgebra R a b)) (QuadraticAlgebra.norm z) = 0
-- Mathlib.Analysis.Fourier.ZMod
/-- The discrete Fourier transform on `ℤ / N ℤ` (with the counting measure). This definition is
private because it is superseded by the bundled `LinearEquiv` version.
 -/
_private.Mathlib.Analysis.Fourier.ZMod.0.ZMod.auxDFT : {N : ℕ} → [NeZero N] → {E : Type u_1} → [inst : AddCommGroup E] → [Module ℂ E] → (ZMod N → E) → ZMod N → E
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.inl.eq_1 : ∀ {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂),
  CategoryTheory.Limits.Types.Pushout.inl f g =
    TypeCat.ofHom fun x => Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) (Sum.inl x)
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Profunctor.ulift_map_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (P : CategoryTheory.Profunctor.{w, v₁, v₂, u₁, u₂} C D) {X Y : C} (f : X ⟶ Y) (X_1 : Dᵒᵖ),
  ((CategoryTheory.Profunctor.ulift.{w', w, v₁, v₂, u₁, u₂} P).map f).app X_1 =
    TypeCat.ofHom fun x => { down := (CategoryTheory.ConcreteCategory.hom ((P.map f).app X_1)) x.down }
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.ofFun_inv : ∀ {α : Type u_1} {β : Type u_2} [inst : Inv β] (f : α → β), UniformFun.ofFun f⁻¹ = (UniformFun.ofFun f)⁻¹
-- Mathlib.Tactic.ITauto
/-- Reify an `Expr` into a `IProp`, allocating anything non-propositional as an atom in the
`AtomM` state.  -/
Mathlib.Tactic.ITauto.reify : Q(Prop) → Mathlib.Tactic.AtomM Mathlib.Tactic.ITauto.IProp
-- Mathlib.Analysis.Calculus.Darboux
/-- **Darboux's theorem**: the image of a convex set under `f'` is a convex set,
`HasDerivWithinAt` version.  -/
Convex.image_hasDerivWithinAt : ∀ {f f' : ℝ → ℝ} {s : Set ℝ}, Convex ℝ s → (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) → Convex ℝ (f' '' s)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.hom_eq : ∀ {α : Type u_1} {M : Type u_4} [inst : AddMonoid M] ⦃f g : FreeAddMonoid α →+ M⦄,
  (∀ (x : α), f (FreeAddMonoid.of x) = g (FreeAddMonoid.of x)) → f = g
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.eventuallyEq_one : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c), ↑f =ᶠ[nhds c] 1
-- Mathlib.Order.UpperLower.Basic
isLowerSet_preimage_ofDual_iff : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, IsLowerSet (⇑OrderDual.ofDual ⁻¹' s) ↔ IsUpperSet s
-- Mathlib.Probability.Notation
/-- `∂P/∂Q` is the Radon–Nikodym derivative of `P` with respect to `Q`.  -/
ProbabilityTheory.«term∂_/∂_» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Prod
/-- Subtraction as an additive monoid homomorphism.  -/
subAddMonoidHom : {α : Type u_6} → [inst : SubtractionCommMonoid α] → α × α →+ α
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_multiset_map_count : ∀ {ι : Type u_1} [inst : DecidableEq ι] (s : Multiset ι) {M : Type u_5} [inst_1 : CommMonoid M] (f : ι → M),
  (Multiset.map f s).prod = ∏ m ∈ s.toFinset, f m ^ Multiset.count m s
-- Mathlib.Analysis.Normed.Group.NullSubmodule
/-- The null space with respect to the norm.  -/
nullSubmodule : (𝕜 : Type u_2) →
  (E : Type u_3) →
    [inst : SeminormedAddCommGroup E] →
      [inst_1 : SeminormedRing 𝕜] → [inst_2 : Module 𝕜 E] → [IsBoundedSMul 𝕜 E] → Submodule 𝕜 E
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_comap_eq_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N},
  Function.Surjective ⇑f → ∀ (S : AddSubsemigroup N), AddSubsemigroup.map f (AddSubsemigroup.comap f S) = S
-- Mathlib.Tactic.Linter.Lint
/-- The `dupNamespace` linter produces a warning when a component of a declaration name is repeated
several times. The repetition does not have to be consecutive. Examples: `Nat.Nat.foo`,
`One.two.two`, `Nat.One.Nat`, `Nat.Prime.Nat.Prime.foo`, `Nat.Prime.Nat.bar`

The linter also warns about auto-generated declarations (such as, those generated by `to_additive`).
 -/
Mathlib.Linter.linter.dupNamespace : Lean.Option Bool
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.rightRel_eq_top : ∀ {G : Type u_1} [inst : AddGroup G] {N : AddSubgroup G}, QuotientAddGroup.rightRel N = ⊤ ↔ N = ⊤
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.dist_pseudoMetricSpaceToProd : ∀ (p : ENNReal) [hp : Fact (1 ≤ p)] (α : Type u_4) (β : Type u_5) [inst : PseudoMetricSpace α]
  [inst_1 : PseudoMetricSpace β] (x y : α × β), dist x y = dist (WithLp.toLp p x) (WithLp.toLp p y)
-- Mathlib.Topology.Category.Born
Born.of.injEq : ∀ (carrier : Type u_1) [str : Bornology carrier] (carrier_1 : Type u_1) (str_1 : Bornology carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The preimage of a `NonUnitalSubring` along a ring homomorphism is a `NonUnitalSubring`.  -/
NonUnitalSubring.comap : {F : Type w} →
  {R : Type u} →
    {S : Type v} →
      [inst : NonUnitalNonAssocRing R] →
        [inst_1 : NonUnitalNonAssocRing S] →
          [inst_2 : FunLike F R S] → [NonUnitalRingHomClass F R S] → F → NonUnitalSubring S → NonUnitalSubring R
-- Init.Data.Array.Lemmas
Array.filterMap_flatten : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xss : Array (Array α)} {stop : ℕ},
  stop = xss.flatten.size →
    Array.filterMap f xss.flatten 0 stop = (Array.map (fun as => Array.filterMap f as) xss).flatten
-- Mathlib.Order.FixedPoints
fixedPoints.gfp_eq_sInf_iterate : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α),
  OmegaCompletePartialOrder.ωScottContinuous ⇑(OrderHom.dual f) → OrderHom.gfp f = ⨅ n, (⇑f)^[n] ⊤
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.mem_toSubgroup : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {U : OpenSubgroup G} {g : G}, g ∈ ↑U ↔ g ∈ U
-- Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
HomotopicalAlgebra.rightHomotopyClassToHom_mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {H : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H)
  [inst_3 : L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] {X Y : C} (f : X ⟶ Y),
  HomotopicalAlgebra.rightHomotopyClassToHom L (HomotopicalAlgebra.RightHomotopyClass.mk f) = L.map f
-- Init.Data.Int.Lemmas
Int.ofNat_add_negSucc : ∀ (m n : ℕ), ↑m + Int.negSucc n = Int.subNatNat m n.succ
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.tendsto_iff_weakDual_tendsto : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω},
  Filter.Tendsto μs F (nhds μ) ↔ Filter.Tendsto (fun i => (μs i).toWeakDualBCNN) F (nhds μ.toWeakDualBCNN)
-- Mathlib.Topology.Instances.Rat
Rat.instOrderTopology : OrderTopology ℚ
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  DiscreteTopology ↥(NumberField.mixedEmbedding.euclidean.integerLattice K)
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.insert.match_1.eq_2 : ∀ (motive : RBTree.RBColor → Sort u_1) (h_1 : Unit → motive RBTree.RBColor.red)
  (h_2 : Unit → motive RBTree.RBColor.black),
  (match RBTree.RBColor.black with
    | RBTree.RBColor.red => h_1 ()
    | RBTree.RBColor.black => h_2 ()) =
    h_2 ()
-- Mathlib.LinearAlgebra.Prod
Submodule.comap_fst : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (p : Submodule R M), Submodule.comap (LinearMap.fst R M M₂) p = p.prod ⊤
-- Mathlib.Tactic.CategoryTheory.ToApp
/-- Simplify an expression in `Cat` using basic properties of `NatTrans.app`.  -/
Mathlib.Tactic.CategoryTheory.ToApp.catAppSimp : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Order.Defs.PartialOrder
ge_trans : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, b ≤ a → c ≤ b → c ≤ a
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instSMulIntHom : {k : Type u} → {G : Type v} → [inst : Semiring k] → [inst_1 : Monoid G] → {A B : Rep.{w, u, v} k G} → SMul ℤ (A ⟶ B)
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' : ∀ {M : Type u_1} [inst : CommGroupWithZero M] (n : ℤ) (e : M) {t t_n t_d : Mathlib.Tactic.FieldSimp.NF M},
  t.eval = t_n.eval / t_d.eval → ((-n, e) ::ᵣ t).eval = t_n.eval / ((n, e) ::ᵣ t_d).eval
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.hasColimitsOfSize_of_hasStrongEpiMonoFactorisations : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y : C} [CategoryTheory.Limits.HasCoproducts C]
  [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C],
  CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₁, max u₁ v₁} (CategoryTheory.MonoOver Y)
-- Mathlib.LinearAlgebra.Dimension.Localization
/-- Given `IsScalarTower R S N`, if `S` is the fraction ring of `R`, then the finrank `finrank S N`
of the right part of the tower equals the finrank `finrank R N` of the whole tower.

See `IsFractionRing.rank_right_eq` for the rank version.
See `IsFractionRing.finrank_left_eq` for the left version.
See `IsFractionRing.finrank_eq` for the simultaneous version.  -/
IsFractionRing.finrank_right_eq : ∀ (R : Type uR) (S : Type uS) (N : Type uN) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : AddCommGroup N]
  [inst_3 : Module R N] [inst_4 : Algebra R S] [inst_5 : Module S N] [IsScalarTower R S N] [IsFractionRing R S],
  Module.finrank S N = Module.finrank R N
-- Mathlib.LinearAlgebra.Pi
LinearMap.pi_ext'_iff : ∀ {R : Type u} {M : Type v} {ι : Type x} [inst : Semiring R] {φ : ι → Type i} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] [Finite ι] [inst_5 : AddCommMonoid M]
  [inst_6 : Module R M] {f g : ((i : ι) → φ i) →ₗ[R] M},
  f = g ↔ ∀ (i : ι), f ∘ₗ LinearMap.single R φ i = g ∘ₗ LinearMap.single R φ i
-- Lean.Data.Lsp.Diagnostics
/-- Represents a diagnostic, such as a compiler error or warning. Diagnostic objects are only valid in the scope of a resource.

LSP accepts a `Diagnostic := DiagnosticWith String`.
The infoview also accepts `InteractiveDiagnostic := DiagnosticWith InteractiveMessage`.

[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#diagnostic)  -/
Lean.Lsp.DiagnosticWith : Type → Type
-- Mathlib.Order.Compare
cmpLE_toDual : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (x y : α),
  cmpLE (OrderDual.toDual x) (OrderDual.toDual y) = cmpLE y x
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionResult.solved.sizeOf_spec : sizeOf Lean.Meta.InjectionResult.solved = 1
-- Mathlib.Order.UpperLower.Relative
IsRelUpperSet.union : ∀ {α : Type u_1} {s t : Set α} {P : α → Prop} [inst : LE α],
  IsRelUpperSet s P → IsRelUpperSet t P → IsRelUpperSet (s ∪ t) P
-- Mathlib.Order.Sublattice
/-- Arbitrary product of sublattices. Given an index set `s` and a family of sublattices
`L : Π i, Sublattice (α i)`, `pi s L` is the sublattice of dependent functions `f : Π i, α i` such
that `f i` belongs to `L i` whenever `i ∈ s`.  -/
Sublattice.pi : {κ : Type u_5} →
  {π : κ → Type u_6} →
    [inst : (i : κ) → Lattice (π i)] → Set κ → ((i : κ) → Sublattice (π i)) → Sublattice ((i : κ) → π i)
-- Mathlib.Order.Filter.AtTopBot.Ring
Filter.Tendsto.atBot_mul_atTop₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] {l : Filter β}
  {f g : β → α},
  Filter.Tendsto f l Filter.atBot → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x * g x) l Filter.atBot
-- Init.Data.String.PosRaw
String.instHSubRawChar : HSub String.Pos.Raw Char String.Pos.Raw
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.SDiff.adjDecidable : (V : Type u_2) → (G H : Digraph V) → [DecidableRel G.Adj] → [DecidableRel H.Adj] → DecidableRel (G \ H).Adj
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biproduct.lift_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type}
  [inst_2 : Fintype J] {f : J → C} [inst_3 : CategoryTheory.Limits.HasBiproduct f] {T : C} {g : (j : J) → T ⟶ f j},
  CategoryTheory.Limits.biproduct.lift g =
    ∑ j, CategoryTheory.CategoryStruct.comp (g j) (CategoryTheory.Limits.biproduct.ι f j)
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_ofNatClamp_of_le : ∀ {n : ℕ},
  UInt16.size ≤ n →
    (UInt16.ofNatClamp n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) UInt16.toUInt8_ofNatClamp_of_le._proof_1
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.IsStrictlySupported.mk : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : HomologicalComplex C c'} {e : c.Embedding c'},
  (∀ (i' : ι'), (∀ (i : ι), e.f i ≠ i') → CategoryTheory.Limits.IsZero (K.X i')) → K.IsStrictlySupported e
-- Mathlib.Algebra.Star.CentroidHom
CentroidHom.starCenterToCentroid_apply : ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] [inst_1 : StarRing α] (z : ↥(NonUnitalStarSubsemiring.center α))
  (a : α), (CentroidHom.starCenterToCentroid z) a = ↑z * a
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.mk_cardinal : Cardinal.mk Cardinal.{u} = Cardinal.univ.{u, u + 1}
-- Mathlib.Logic.Equiv.Fin.Basic
finSumNatEquiv_symm_apply_of_ge : ∀ {n i : ℕ}, n ≤ i → (finSumNatEquiv n).symm i = Sum.inr (i - n)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.trans_iff : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b c : ℝ}
  {μ : MeasureTheory.Measure ℝ} [TopologicalSpace.PseudoMetrizableSpace ε],
  b ∈ Set.uIcc a c → (IntervalIntegrable f μ a c ↔ IntervalIntegrable f μ a b ∧ IntervalIntegrable f μ b c)
-- Mathlib.Algebra.Group.Prod
/-- Multiplying by the trivial monoid doesn't change the
structure.

This is the `AddEquiv` version of `Equiv.uniqueProd`.  -/
AddEquiv.uniqueProd : {M : Type u_3} → {N : Type u_4} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [Unique N] → N × M ≃+ M
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAt.isBigOTVS_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} [ContinuousAdd F] [ContinuousSMul 𝕜 F],
  HasFDerivAt f f' x → (fun x_1 => f x_1 - f x) =O[𝕜; nhds x] fun x_1 => x_1 - x
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousWithinAt.fun_add : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f g : X → M} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (fun i => f i + g i) s x
-- Mathlib.Algebra.Group.Conj
IsAddConj.symm : ∀ {α : Type u} [inst : AddMonoid α] {a b : α}, IsAddConj a b → IsAddConj b a
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.«builder_option(Index:=[_])» : Lean.ParserDescr
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.hsum_sub : ∀ {Γ : Type u_1} {α : Type u_5} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [IsOrderedCancelAddMonoid Γ]
  {R : Type u_7} [inst : Ring R] {s t : HahnSeries.SummableFamily Γ R α}, (s - t).hsum = s.hsum - t.hsum
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GLPos.det_ne_zero : ∀ {n : Type u} {R : Type v} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R] [inst_3 : LinearOrder R]
  [inst_4 : IsStrictOrderedRing R] (A : ↥(Matrix.GLPos n R)), (↑↑A).det ≠ 0
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
/-- The centralizer of a subset of a semigroup `M`.  -/
Subsemigroup.centralizer : {M : Type u_1} → Set M → [inst : Semigroup M] → Subsemigroup M
-- Mathlib.CategoryTheory.Countable
CategoryTheory.CountableCategory.countableHom : ∀ {J : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} J} [self : CategoryTheory.CountableCategory J] (j j' : J),
  Countable (j ⟶ j')
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.Functor.mapExtLinearMap_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [inst_7 : CategoryTheory.HasExt C]
  [inst_8 : CategoryTheory.HasExt D] (X Y : C) (n : ℕ) (R : Type u_1) [inst_9 : Ring R]
  [inst_10 : CategoryTheory.Linear R C] [inst_11 : CategoryTheory.Linear R D]
  [inst_12 : CategoryTheory.Functor.Linear R F],
  ⇑(F.mapExtLinearMap R X Y n) = CategoryTheory.Abelian.Ext.mapExactFunctor F
-- Mathlib.Data.Set.Function
Set.EqOn.symm : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β}, Set.EqOn f₁ f₂ s → Set.EqOn f₂ f₁ s
-- Lean.Meta.LazyDiscrTree
/-- Creates reference for lazy discriminator tree that only contains this module's definitions.
If `droppedEntriesRef` is provided, dropped entries (e.g., star-indexed lemmas) are extracted
and appended to the array in the reference.
 -/
Lean.Meta.LazyDiscrTree.createModuleTreeRef : {α : Type} →
  (Lean.Name → Lean.AsyncConstantInfo → Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry α))) →
    List (List Lean.Meta.LazyDiscrTree.Key) →
      optParam (Option (IO.Ref (Option (Array α)))) none → Lean.MetaM (Lean.Meta.LazyDiscrTree.ModuleDiscrTreeRef α)
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.piecewise_apply' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β}
  {s : Set α} {hs : MeasurableSet s} [inst : DecidablePred fun x => x ∈ s] (a : α) (t : Set β),
  ((ProbabilityTheory.Kernel.piecewise hs κ η) a) t = if a ∈ s then (κ a) t else (η a) t
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_ε_unmop_unmop : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).inverse).unmop.unmop =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Algebra.Order.Monovary
monovary_inv_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semifield β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {f : ι → α} {g : ι → β}, StrongLT 0 g → (Monovary f g⁻¹ ↔ Antivary f g)
-- Mathlib.NumberTheory.ZetaValues
/-- The `n`-th Fourier coefficient of the `k`-th Bernoulli function on the interval `[0, 1]`.  -/
bernoulliFourierCoeff : ℕ → ℤ → ℂ