mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.instInhabitedSubtypeMem : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] → [inst_2 : Module R A] → (S : NonUnitalSubalgebra R A) → Inhabited ↥S
-- Mathlib.CategoryTheory.Bicategory.SingleObj
CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_functor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence C).functor =
    CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.registerMVarErrorImplicitArgInfo : Lean.MVarId → Lean.Syntax → Lean.Expr → Lean.Elab.TermElabM Unit
-- Std.Sync.Notify
Std.Notify.Consumer : Type → Type
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.FinMeasAdditive.neg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} {T : Set α → β}
  [inst : AddGroup β], MeasureTheory.FinMeasAdditive μ T → MeasureTheory.FinMeasAdditive μ (-T)
-- Mathlib.Algebra.BigOperators.Finsupp.Fin
Finsupp.sum_cons' : ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : AddCommMonoid N] (n : ℕ) (σ : Fin n →₀ M) (i : M)
  (f : Fin (n + 1) → M → N), (∀ (x : Fin (n + 1)), f x 0 = 0) → (Finsupp.cons i σ).sum f = f 0 i + σ.sum (Fin.tail f)
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsStronglyCartesian.map.congr_simp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p p_1 : CategoryTheory.Functor 𝒳 𝒮) (e_p : p = p_1) {R S : 𝒮} {a b : 𝒳} (f f_1 : R ⟶ S) (e_f : f = f_1)
  (φ φ_1 : a ⟶ b) (e_φ : φ = φ_1) [inst_2 : p.IsStronglyCartesian f φ] {R' : 𝒮} {a' : 𝒳} {g g_1 : R' ⟶ R}
  (e_g : g = g_1) {f' f'_1 : R' ⟶ S} (e_f' : f' = f'_1) (hf' : f' = CategoryTheory.CategoryStruct.comp g f)
  (φ' φ'_1 : a' ⟶ b) (e_φ' : φ' = φ'_1) [inst_3 : p.IsHomLift f' φ'],
  CategoryTheory.Functor.IsStronglyCartesian.map p f φ hf' φ' =
    CategoryTheory.Functor.IsStronglyCartesian.map p_1 f_1 φ_1 ⋯ φ'_1
-- Init.Data.UInt.BasicAux
/-- Converts a natural number to a 16-bit unsigned integer, returning the largest representable value if
the number is too large.

Returns `2^16 - 1` for natural numbers greater than or equal to `2^16`.
 -/
UInt16.ofNatClamp : ℕ → UInt16
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
/-- A direct sum of faithfully flat `R`-modules is faithfully flat.  -/
Module.FaithfullyFlat.directSum : ∀ (R : Type u) [inst : CommRing R] {ι : Type u_1} [Nonempty ι] (M : ι → Type u_2)
  [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module R (M i)]
  [∀ (i : ι), Module.FaithfullyFlat R (M i)], Module.FaithfullyFlat R (DirectSum ι fun i => M i)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.norm_le_norm_of_mem : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] [NormOneClass A] {a : A} {k : 𝕜}, k ∈ spectrum 𝕜 a → ‖k‖ ≤ ‖a‖
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
/-- A commutative Noetherian total ring of fractions is semilocal.  -/
instFiniteMaximalSpectrumOfIsFractionRing : ∀ (A : Type u) [inst : CommRing A] [IsNoetherianRing A] [IsFractionRing A A], Finite (MaximalSpectrum A)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSet_iff : ∀ {Ω : Type u_1} {ι : Type u_2} {x : MeasurableSpace Ω} (s : ι → Set Ω) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.iIndepSet s μ ↔
    ∀ (s' : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s', MeasurableSet (f i)) → μ (⋂ i ∈ s', f i) = ∏ i ∈ s', μ (f i)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.flatten_think : ∀ {α : Type u} (c : Computation (Stream'.WSeq α)), Stream'.WSeq.flatten c.think = (Stream'.WSeq.flatten c).think
-- Mathlib.Data.EReal.Basic
EReal.image_coe_Icc : ∀ (x y : ℝ), Real.toEReal '' Set.Icc x y = Set.Icc ↑x ↑y
-- Mathlib.GroupTheory.Index
/-- A finite index subgroup has finite quotient  -/
AddSubgroup.fintypeQuotientOfFiniteIndex : {G : Type u_1} → [inst : AddGroup G] → {H : AddSubgroup G} → [H.FiniteIndex] → Fintype (G ⧸ H)
-- Mathlib.Order.Monotone.Defs
StrictMono.iterate : ∀ {α : Type u} [inst : Preorder α] {f : α → α}, StrictMono f → ∀ (n : ℕ), StrictMono f^[n]
-- Mathlib.Topology.VectorBundle.Hom
Bundle.Pretrivialization.continuousLinearMapCoordChange.eq_1 : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] (e₁ e₁' : Bundle.Trivialization F₁ Bundle.TotalSpace.proj)
  (e₂ e₂' : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) [inst_13 : Bundle.Trivialization.IsLinear 𝕜₁ e₁]
  [inst_14 : Bundle.Trivialization.IsLinear 𝕜₁ e₁'] [inst_15 : Bundle.Trivialization.IsLinear 𝕜₂ e₂]
  [inst_16 : Bundle.Trivialization.IsLinear 𝕜₂ e₂'] (b : B),
  Bundle.Pretrivialization.continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂' b =
    ↑((Bundle.Trivialization.coordChangeL 𝕜₁ e₁' e₁ b).symm.arrowCongrSL
        (Bundle.Trivialization.coordChangeL 𝕜₂ e₂ e₂' b))
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.coe_mk : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N] (f : ZeroHom M N)
  (hadd : ∀ (x y : M), f.toFun (x + y) = f.toFun x + f.toFun y), ⇑{ toZeroHom := f, map_add' := hadd } = ⇑f
-- Lean.Meta.AppBuilder
/-- Returns `of_eq_false h`  -/
Lean.Meta.mkOfEqFalse : Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_right_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℕ → Bool
-- Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
/-- Shows the correctness of `compExactValue` in case the continued fraction
`GenContFract.of v` did not terminate at position `n`. That is, we obtain the
value `v` if we pass the two successive (auxiliary) continuants at positions `n` and `n + 1` as well
as the fractional part at `IntFractPair.stream n` to `compExactValue`.

The correctness might be seen more readily if one uses `convs'` to evaluate the continued
fraction. Here is an example to illustrate the idea:

Let `(v : ℚ) := 3.4`. We have
- `GenContFract.IntFractPair.stream v 0 = some ⟨3, 0.4⟩`, and
- `GenContFract.IntFractPair.stream v 1 = some ⟨2, 0.5⟩`.

Now `(GenContFract.of v).convs' 1 = 3 + 1/2`, and our fractional term at position `2` is `0.5`.
We hence have `v = 3 + 1/(2 + 0.5) = 3 + 1/2.5 = 3.4`.
This computation corresponds exactly to the one using the recurrence equation in `compExactValue`.
 -/
GenContFract.compExactValue_correctness_of_stream_eq_some : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] {v : K} {n : ℕ} [inst_2 : FloorRing K]
  {ifp_n : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v n = some ifp_n →
    v = GenContFract.compExactValue ((GenContFract.of v).contsAux n) ((GenContFract.of v).contsAux (n + 1)) ifp_n.fr
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
/-- The homology functor `DerivedCategory C ⥤ C` in degree `n : ℤ`.  -/
DerivedCategory.homologyFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → ℤ → CategoryTheory.Functor (DerivedCategory C) C
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isEmpty_empty : ∀ {α : Type u} {cmp : α → α → Ordering}, ∅.isEmpty = true
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_filterMap_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)},
  (Std.DHashMap.filterMap f m).isEmpty = true ↔ ∀ (k : α) (h : k ∈ m), f k (m.get k h) = none
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
/-- A $C^{k+(α)}$ map satisfies $D^kf(x)-D^kf(a) = O(‖x - a‖ ^ α)$ as `x → a`.  -/
ContDiffPointwiseHolderAt.isBigO : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E → F} {a : E},
  ContDiffPointwiseHolderAt k α f a →
    (fun x => iteratedFDeriv ℝ k f x - iteratedFDeriv ℝ k f a) =O[nhds a] fun x => ‖x - a‖ ^ ↑α
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.USquash.inflate : {α : Type v} → [small : Std.Internal.Small α] → Std.Internal.USquash α → α
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- If `f : G → H` is a multiplicative homomorphism between two monoids, then
`MonoidAlgebra.mapDomain f` is a ring homomorphism between their monoid algebras.  -/
MonoidAlgebra.mapDomainNonUnitalRingHom : (R : Type u_3) →
  {M : Type u_6} →
    {N : Type u_7} →
      [inst : Semiring R] → [inst_1 : Mul M] → [inst_2 : Mul N] → (M →ₙ* N) → MonoidAlgebra R M →ₙ+* MonoidAlgebra R N
-- Mathlib.Combinatorics.Matroid.Map
/-- Given a function `f` that is injective on `M.E`, the copy of `M` in `β` whose independent sets
are the images of those in `M`. If `β` is a nonempty type, then `N : Matroid β` is a map of `M`
if and only if `M` and `N` are isomorphic.  -/
Matroid.map : {α : Type u_1} → {β : Type u_2} → (M : Matroid α) → (f : α → β) → Set.InjOn f M.E → Matroid β
-- Batteries.Lean.LawfulMonadLift
instLawfulMonadLiftIOCoreM_batteries : LawfulMonadLift IO Lean.CoreM
-- Mathlib.Analysis.Normed.Module.Convex
/-- Convex hull of `s` is bounded if and only if `s` is bounded.  -/
isBounded_convexHull : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E},
  Bornology.IsBounded ((convexHull ℝ) s) ↔ Bornology.IsBounded s
-- Mathlib.Analysis.Complex.Exponential
Real.quadratic_le_exp_of_nonneg : ∀ {x : ℝ}, 0 ≤ x → 1 + x + x ^ 2 / 2 ≤ Real.exp x
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ReturnCont.mk : Lean.Expr → (Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr) → Lean.Elab.Do.ReturnCont
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.length_alterKey_eq_sub_one : ∀ {α : Type u} [inst : BEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)},
  Std.Internal.List.containsKey k l = true →
    (f (Std.Internal.List.getValue? k l)).isNone = true → (Std.Internal.List.Const.alterKey k f l).length = l.length - 1
-- Mathlib.Data.Fin.SuccPred
Fin.coe_of_injective_castSucc_symm : ∀ {n : ℕ} (i : Fin n.succ) (hi : i ∈ Set.range Fin.castSucc), ↑((Equiv.ofInjective Fin.castSucc ⋯).symm ⟨i, hi⟩) = ↑i
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.even_nsmul_periodic : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddMonoid α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c → ∀ (n : ℕ), Function.Periodic f ((2 * n) • c)
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.mul : ∀ {R : Type u_1} [inst : Semiring R] {f g : Polynomial R}, f.Splits → g.Splits → (f * g).Splits
-- Lean.DocString.Syntax
/-- A code block that contains literal code.

Code blocks have the following syntax:
````
```(NAME ARGS*)?
CONTENT
```
````

`CONTENT` is a literal string. If the `CONTENT` contains a sequence of three or more backticks, then
the opening and closing ` ``` ` (called _fences_) should have more backticks than the longest
sequence in `CONTENT`. Additionally, the opening and closing fences should have the same number of
backticks.

If `NAME` and `ARGS` are not provided, then the code block represents literal text. If provided, the
`NAME` is an identifier that selects an interpretation of the block. Unlike Markdown, this name is
not necessarily the language in which the code is written, though many custom code blocks are, in
practice, named after the language that they contain. `NAME` is more akin to a function name. Each
of the `ARGS` may have the following forms:
* A value, which is a string literal, natural number, or identifier
* A named argument, of the form `(NAME := VALUE)`
* A flag, of the form `+NAME` or `-NAME`

The `CONTENT` is interpreted according to the indentation of the fences. If the fences are indented
`n` spaces, then `n` spaces are removed from the start of each line of `CONTENT`.
 -/
Lean.Doc.Syntax.codeblock : Lean.ParserDescr
-- Mathlib.Data.Finset.Sum
Finset.mem_disjSum : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {x : α ⊕ β},
  x ∈ s.disjSum t ↔ (∃ a ∈ s, Sum.inl a = x) ∨ ∃ b ∈ t, Sum.inr b = x
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.top_mem : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α}, ⊤ ∈ L
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.mem_sInf : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  {S : Set (IntermediateField F E)} {x : E}, x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
-- Mathlib.Logic.Equiv.Fin.Rotate
finRotate_one : finRotate 1 = Equiv.refl (Fin 1)
-- Mathlib.Order.Heyting.Hom
HeytingHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β] (f : HeytingHom α β),
  (HeytingHom.id β).comp f = f
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.le_of_opENorm_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f : E →SL[σ₁₂] F) {c : ENNReal}, ‖f‖ₑ ≤ c → ∀ (x : E), ‖f x‖ₑ ≤ c * ‖x‖ₑ
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.coe_orderHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] (f : α →*o β), ⇑↑f = ⇑f
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.instFiniteSubtypeMemSubmodule : ∀ {R : Type u_1} [inst : Semiring R] {n : ℕ}, Module.Finite R ↥(Polynomial.degreeLT R n)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_subset_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s₁ s₂ : Set α} {t₁ t₂ : Set β},
  s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ +ᵥ t₁ ⊆ s₂ +ᵥ t₂
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
/-- This holds true for all `x : ℂ` because of the junk values `0 / 0 = 0` and `log 0 = 0`.  -/
Complex.log_div_self : ∀ (x : ℂ), Complex.log (x / x) = 0
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
/-- If `f` is an antitone function with bounded range
and `g` tends to `atBot` along a nontrivial filter,
then the indexed supremum of `f ∘ g` is equal to the indexed supremum of `f`.

The assumption `BddAbove (range f)` can be omitted,
if the codomain of `f` is a conditionally complete linear order or a complete lattice, see below.
 -/
Antitone.ciSup_comp_tendsto_atBot : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : ConditionallyCompleteLattice γ]
  {l : Filter α} [l.NeBot] {f : β → γ},
  Antitone f → BddAbove (Set.range f) → ∀ {g : α → β}, Filter.Tendsto g l Filter.atBot → ⨆ a, f (g a) = ⨆ b, f b
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.ext_iff : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  {f g : A →ₑ*[φ] B}, f = g ↔ ∀ (x : A), f x = g x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.finset.eq_1 : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d), SSet.prodStdSimplex.pairingCore.finset x hd = {l | (x.cast hd).simplex.1 l = k.succ}
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- A short complex in a category `C` with zero morphisms is the datum
of two composable morphisms `f : X₁ ⟶ X₂` and `g : X₂ ⟶ X₃` such that
`f ≫ g = 0`.  -/
CategoryTheory.ShortComplex : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → Type (max u_1 v_1)
-- Mathlib.Data.Finset.Union
Finset.biUnion_image : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq β] [inst_1 : DecidableEq γ] {s : Finset α}
  {t : α → Finset β} {f : β → γ}, Finset.image f (s.biUnion t) = s.biUnion fun a => Finset.image f (t a)
-- Mathlib.Data.List.Triplewise
List.Triplewise.below.nil : ∀ {α : Type u_1} {p : α → α → α → Prop} {motive : (a : List α) → List.Triplewise p a → Prop}, List.Triplewise.below ⋯
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.comp_one : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : MulOneClass α] [inst_4 : MulOneClass β] [inst_5 : MulOneClass γ] (f : β →*o γ), f.comp 1 = 1
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.LevyProkhorov.dist_probabilityMeasure_def : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  (μ ν : MeasureTheory.LevyProkhorov (MeasureTheory.ProbabilityMeasure Ω)),
  dist μ ν = MeasureTheory.levyProkhorovDist ↑μ.toMeasure ↑ν.toMeasure
-- Init.Data.List.Erase
List.Pairwise.erase : ∀ {α : Type u_1} [inst : BEq α] {p : α → α → Prop} [LawfulBEq α] {l : List α} (a : α),
  List.Pairwise p l → List.Pairwise p (l.erase a)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.smul_mem : ∀ {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) {x : M} (r : R), x ∈ p → r • x ∈ p
-- Mathlib.Order.Interval.Set.InitialSeg
PrincipalSeg.orderIsoIio_apply_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α <i β) (a : α),
  ↑(f.orderIsoIio a) = f.toRelEmbedding a
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryGE! : {α : Type u} →
  {β : α → Type v} → [Ord α] → [Inhabited ((a : α) × β a)] → α → Std.DTreeMap.Internal.Impl α β → (a : α) × β a
-- Batteries.Data.AssocList
Batteries.AssocList.contains_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] (a : α) (l : Batteries.AssocList α β),
  Batteries.AssocList.contains a l = l.toList.any fun x => x.1 == a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- Given a bifunctor `F : C₁ ⥤ C₂ ⥤ C₃`, and morphisms `f₁ : X₁ ⟶ Y₁` in `C₁`
and `f₂ : X₂ ⟶ Y₂` in `C₂`, this structure contains the data of
a pushout of `(F.obj Y₁).obj X₂` and `(F.obj X₁).obj Y₂`
along `(F.obj X₁).obj X₂`.  -/
CategoryTheory.Functor.PushoutObjObj : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃) →
              {X₁ Y₁ : C₁} → (X₁ ⟶ Y₁) → {X₂ Y₂ : C₂} → (X₂ ⟶ Y₂) → Type (max u₃ v₃)
-- Init.Data.Nat.Basic
Nat.add_eq : ∀ {x y : ℕ}, x.add y = x + y
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- Given `x : X` and `y : Y` such that `f x = s = g y`, this is the
canonical map `κ(y) ⟶ κ(x) ⊗[κ(s)] κ(y)`.  -/
AlgebraicGeometry.Scheme.Pullback.Triplet.tensorInr : {X Y S : AlgebraicGeometry.Scheme} →
  {f : X ⟶ S} → {g : Y ⟶ S} → (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) → Y.residueField T.y ⟶ T.tensor
-- Std.Time.Format
/-- Converts a date in the SQL format (`uuuu-MM-dd`) into a `String`.
 -/
Std.Time.PlainDate.toSQLDateString : Std.Time.PlainDate → String
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
Module.Basis.addHaar.congr_simp : ∀ {ι : Type u_5} {E : Type u_6} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (b b_1 : Module.Basis ι ℝ E), b = b_1 → b.addHaar = b_1.addHaar
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (z : CategoryTheory.CatCenter C) {X Y : C} (f : X ⟶ Y) {Z : C}
  (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (z.app Y) h) =
    CategoryTheory.CategoryStruct.comp (z.app X) (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Order.Zorn
IsChain.exists_subset_flag : ∀ {α : Type u_1} [inst : Preorder α] {c : Set α}, IsChain (fun x1 x2 => x1 ≤ x2) c → ∃ s, c ⊆ ↑s
-- Mathlib.MeasureTheory.Measure.Prokhorov
/-- In a compact space, the set of finite measures with mass `C` is compact.  -/
isCompact_setOfPred_finiteMeasure_eq_of_compactSpace : ∀ (E : Type u_1) [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [T2Space E] [inst_3 : BorelSpace E]
  [CompactSpace E] (C : NNReal), IsCompact {μ | μ.mass = C}
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
Matrix.ofArray.congr_simp : ∀ {R : Type u_7} {m n : ℕ} (A A_1 : Array R) (e_A : A = A_1) (hA : A.size = m * n) (a a_1 : Fin m),
  a = a_1 → ∀ (a_2 a_3 : Fin n), a_2 = a_3 → Matrix.ofArray A hA a a_2 = Matrix.ofArray A_1 ⋯ a_1 a_3
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
/-- A reflexive module has a perfect pairing with its dual.  -/
LinearMap.IsPerfPair.id : ∀ {R : Type u_1} {M : Type u_3} [inst : AddCommGroup M] [inst_1 : CommRing R] [inst_2 : Module R M]
  [Module.IsReflexive R M], LinearMap.id.IsPerfPair
-- Init.Data.ToString.Basic
instToStringFin : (n : ℕ) → ToString (Fin n)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.norm_eq_cert : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Bool
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Polynomial.contentIdeal_map_eq_map_contentIdeal : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (p : Polynomial R) (f : R →+* S),
  (Polynomial.map f p).contentIdeal = Ideal.map f p.contentIdeal
-- Mathlib.CategoryTheory.EssentialImage
/-- Being in the essential image is a "hygienic" property: it is preserved under isomorphism.  -/
CategoryTheory.Functor.essImage.ofIso : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y Y' : D} (h : Y ≅ Y'), F.essImage Y → F.essImage Y'
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.sup_vanishingIdeal_le : ∀ {R : Type u} [inst : CommSemiring R] (t t' : Set (PrimeSpectrum R)),
  PrimeSpectrum.vanishingIdeal t ⊔ PrimeSpectrum.vanishingIdeal t' ≤ PrimeSpectrum.vanishingIdeal (t ∩ t')
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.swap_obj_X : ∀ (X : TwoP), (TwoP.swap.obj X).X = X.X
-- Mathlib.Tactic.Abel
/-- The normalization style.  -/
Mathlib.Tactic.Abel.AbelNF.Config.mode : Mathlib.Tactic.Abel.AbelNF.Config → Mathlib.Tactic.Abel.AbelMode
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.toProd_apply : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : K ⋊⁅ψ⁆ L),
  LieAlgebra.SemiDirectSum.toProd x = (x.left, x.right)
-- Init.Data.Array.Find
Array.back?_filter : ∀ {α : Type} {p : α → Bool} {xs : Array α}, (Array.filter p xs).back? = Array.findRev? p xs
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.mk_eq_mk : ∀ {K : Type u_1} [inst : Field K] (x y : K) (hx : x ∈ integralClosure ℤ K) (hy : y ∈ integralClosure ℤ K),
  ⟨x, hx⟩ = ⟨y, hy⟩ ↔ x = y
-- Mathlib.Algebra.Free
/-- `FreeSemigroup` is traversable.  -/
FreeSemigroup.traverse : {m : Type u → Type u} → [Applicative m] → {α β : Type u} → (α → m β) → FreeSemigroup α → m (FreeSemigroup β)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_pow_eq_zero : ∀ {R : Type u} [inst : CommSemiring R] [NoZeroDivisors R] {n : ℕ},
  ↑n ≠ 0 → ∀ {a : Polynomial R}, Polynomial.derivative (a ^ n) = 0 ↔ Polynomial.derivative a = 0
-- Mathlib.RingTheory.PowerSeries.Substitution
/-- A variant of `HasSubst.zero` to avoid the expansion of `Unit`.  -/
PowerSeries.HasSubst.zero' : ∀ {R : Type u_2} [inst : CommRing R], PowerSeries.HasSubst 0