mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsLinearSet.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] (s : Set M),
  IsLinearSet s = ∃ a t, t.Finite ∧ s = a +ᵥ ↑(AddSubmonoid.closure t)
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenCoend.map.eq_1 : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C] {G : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  (f : F ⟶ G),
  CategoryTheory.Limits.chosenCoend.map f =
    CategoryTheory.Limits.chosenCoend.desc
      (fun x =>
        CategoryTheory.CategoryStruct.comp ((f.app (Opposite.op x)).app x) (CategoryTheory.Limits.chosenCoend.ι G x))
      ⋯
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.instIsContinuousOverMapOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {X Y : C}
  (f : X ⟶ Y), (CategoryTheory.Over.map f).IsContinuous (J.over X) (J.over Y)
-- Mathlib.CategoryTheory.Sites.Equivalence
/-- The inverse in the equivalence of sheaf categories.  -/
CategoryTheory.Equivalence.sheafCongr.inverse : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (K : CategoryTheory.GrothendieckTopology D) →
            (e : C ≌ D) →
              (A : Type u₃) →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} A] →
                  [CategoryTheory.Functor.IsDenseSubsite K J e.inverse] →
                    CategoryTheory.Functor (CategoryTheory.Sheaf K A) (CategoryTheory.Sheaf J A)
-- Init.Data.String.FindPos
/-- Obtains the largest valid position that is less than or equal to the given byte position.
 -/
String.posLE : (s : String) → String.Pos.Raw → s.Pos
-- Mathlib.Data.Seq.Parallel
Computation.map_parallel : ∀ {α : Type u} {β : Type v} (f : α → β) (S : Stream'.WSeq (Computation α)),
  Computation.map f (Computation.parallel S) = Computation.parallel (Stream'.WSeq.map (Computation.map f) S)
-- Mathlib.Algebra.GroupWithZero.InjSurj
/-- Push forward a `CommMonoidWithZero` along a surjective function.
See note [reducible non-instances].  -/
Function.Surjective.commMonoidWithZero : {M₀ : Type u_1} →
  {M₀' : Type u_3} →
    [inst : Zero M₀'] →
      [inst_1 : Mul M₀'] →
        [inst_2 : One M₀'] →
          [inst_3 : Pow M₀' ℕ] →
            [inst_4 : CommMonoidWithZero M₀] →
              (f : M₀ → M₀') →
                Function.Surjective f →
                  f 0 = 0 →
                    f 1 = 1 →
                      (∀ (x y : M₀), f (x * y) = f x * f y) →
                        (∀ (x : M₀) (n : ℕ), f (x ^ n) = f x ^ n) → CommMonoidWithZero M₀'
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.mk.injEq : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  (inl : N →+ E) (rightHom : E →+ G) (inl_injective : Function.Injective ⇑inl)
  (range_inl_eq_ker_rightHom : inl.range = rightHom.ker) (rightHom_surjective : Function.Surjective ⇑rightHom)
  (inl_1 : N →+ E) (rightHom_1 : E →+ G) (inl_injective_1 : Function.Injective ⇑inl_1)
  (range_inl_eq_ker_rightHom_1 : inl_1.range = rightHom_1.ker)
  (rightHom_surjective_1 : Function.Surjective ⇑rightHom_1),
  ({ inl := inl, rightHom := rightHom, inl_injective := inl_injective,
        range_inl_eq_ker_rightHom := range_inl_eq_ker_rightHom, rightHom_surjective := rightHom_surjective } =
      { inl := inl_1, rightHom := rightHom_1, inl_injective := inl_injective_1,
        range_inl_eq_ker_rightHom := range_inl_eq_ker_rightHom_1, rightHom_surjective := rightHom_surjective_1 }) =
    (inl = inl_1 ∧ rightHom = rightHom_1)
-- Lean.Elab.InfoTree.Main
Lean.Elab.TermInfo.format : Lean.Elab.ContextInfo → Lean.Elab.TermInfo → IO Std.Format
-- Mathlib.Data.Num.ZNum
Num.gcdAux.eq_def : ∀ (x : ℕ) (x_1 x_2 : Num),
  Num.gcdAux x x_1 x_2 =
    match x, x_1, x_2 with
    | 0, x, b => b
    | n.succ, Num.zero, b => b
    | n.succ, a, b => Num.gcdAux n (b % a) a
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.coe_op : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {I : TwoSidedIdeal R}, ↑I.op = MulOpposite.unop ⁻¹' ↑I
-- Mathlib.LinearAlgebra.Dual.BaseChange
Module.Dual.baseChange_baseChange : ∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] (A : Type u_4)
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {B : Type u_5} [inst_5 : CommSemiring B] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : IsScalarTower R A B] (f : Module.Dual R V),
  (Module.Dual.baseChange B) ((Module.Dual.baseChange A) f) =
    (Module.Dual.congr (TensorProduct.AlgebraTensorModule.cancelBaseChange R A B B V)).symm
      ((Module.Dual.baseChange B) f)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_insert_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  [inst_1 : Inhabited (β a)] {b : β a}, (m.insert a b).get! a = b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.sin_eq_one_iff : ∀ {x : ℝ}, Real.sin x = 1 ↔ ∃ k, Real.pi / 2 + ↑k * (2 * Real.pi) = x
-- Mathlib.Algebra.Field.GeomSum
geom_sum_Ico : ∀ {K : Type u_2} [inst : DivisionRing K] {x : K},
  x ≠ 1 → ∀ {m n : ℕ}, m ≤ n → ∑ i ∈ Finset.Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Div-mul-mul version.  -/
Finset.ruzsa_triangle_inequality_div_mul_mul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] (A B C : Finset G),
  (A / C).card * B.card ≤ (A * B).card * (C * B).card
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- If a function has locally bounded variation, then the variation on
small closed intervals to the right of this point tends to the contribution of the point, i.e.,
the distance between the right limit and the value at the point  -/
LocallyBoundedVariationOn.tendsto_eVariationOn_Icc_right : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {s : Set α} {l : E},
  LocallyBoundedVariationOn f s →
    ∀ {x : α},
      Filter.Tendsto f (nhdsWithin x (s ∩ Set.Ioi x)) (nhds l) →
        x ∈ s →
          Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Icc x y)) (nhdsWithin x (s ∩ Set.Ioi x))
            (nhds (edist (f x) l))
-- Lean.Data.KVMap
Lean.instReprDataValue : Repr Lean.DataValue
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ShowDocumentClientCapabilities.support : Lean.Lsp.ShowDocumentClientCapabilities → Bool
-- Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
/-- The equivalence between `Finset.finsuppAntidiag s n` and `Sym s n`.  -/
Finset.finsuppAntidiagEquiv : {ι : Type u_1} → [inst : DecidableEq ι] → (s : Finset ι) → (n : ℕ) → ↥(s.finsuppAntidiag n) ≃ Sym (↥s) n
-- Mathlib.AlgebraicGeometry.Normalization
/-- This is the open cover of `f.normalization` by `Spec` of integral closures of `Γ(Y, U)`
in `Γ(X, f ⁻¹ U)` where `U` ranges over all affine opens.  -/
AlgebraicGeometry.Scheme.Hom.normalizationOpenCover : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.QuasiCompact f] →
      [inst_1 : AlgebraicGeometry.QuasiSeparated f] → (AlgebraicGeometry.Scheme.Hom.normalization f).OpenCover
-- Std.Data.DHashMap.Basic
Std.DHashMap.instRepr : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → [inst_1 : Hashable α] → [Repr α] → [(a : α) → Repr (β a)] → Repr (Std.DHashMap α β)
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.mk : {M : Type u_10} → {N : Type u_11} → [inst : One M] → [inst_1 : One N] → (toFun : M → N) → toFun 1 = 1 → OneHom M N
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
/-- Multiplication of the quaternion group.
 -/
_private.Mathlib.GroupTheory.SpecificGroups.Quaternion.0.QuaternionGroup.mul : {n : ℕ} → QuaternionGroup n → QuaternionGroup n → QuaternionGroup n
-- Mathlib.Analysis.Seminorm
Seminorm.ball_comp : ∀ {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedRing 𝕜₂] [inst_4 : AddCommGroup E₂] [inst_5 : Module 𝕜₂ E₂] {σ₁₂ : 𝕜 →+* 𝕜₂}
  [inst_6 : RingHomIsometric σ₁₂] (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (x : E) (r : ℝ),
  (p.comp f).ball x r = ⇑f ⁻¹' p.ball (f x) r
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.comap_inf_map_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
  Function.Injective ⇑f →
    ∀ (S T : AddSubmonoid M), AddSubmonoid.comap f (AddSubmonoid.map f S ⊓ AddSubmonoid.map f T) = S ⊓ T
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.M : Type → Type
-- Init.Data.List.Range
List.tail_range' : ∀ {s n step : ℕ}, (List.range' s n step).tail = List.range' (s + step) (n - 1) step
-- Mathlib.ModelTheory.Order
FirstOrder.Language.order.instUniqueSigmaNatRelations : Unique ((n : ℕ) × FirstOrder.Language.order.Relations n)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List α}, (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).isEmpty = ((↑m).isEmpty && l.isEmpty)
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
ZMod.instMeasurableSingletonClass : ∀ (n : ℕ), MeasurableSingletonClass (ZMod n)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v v_1 : IsDedekindDomain.HeightOneSpectrum R),
  v = v_1 →
    IsDedekindDomain.HeightOneSpectrum.adicCompletion K v = IsDedekindDomain.HeightOneSpectrum.adicCompletion K v_1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go.match_1.splitter : (motive : ℕ → Sort u_1) → (curr : ℕ) → (Unit → motive 0) → ((curr : ℕ) → motive curr.succ) → motive curr
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.coeff_hsum_mul : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : Semiring R] (s : HahnSeries.SummableFamily Γ R α)
  (t : HahnSeries.SummableFamily Γ R β) (g : Γ),
  (s.mul t).hsum.coeff g = ∑ gh ∈ Finset.antidiagonal ⋯ ⋯ g, s.hsum.coeff gh.1 * t.hsum.coeff gh.2
-- Mathlib.Tactic.ClickSuggestions.TryPremises
/-- Compute the library rearch suggestions. This uses `token` to incrementally update the output.  -/
Mathlib.Tactic.ClickSuggestions.librarySearchSuggestions : Lean.Expr →
  Lean.Expr →
    Lean.LocalContext →
      Mathlib.Tactic.ClickSuggestions.RwKind →
        Option Lean.Name → ProofWidgets.RefreshToken → Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM Unit
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α} [inst_3 : Inhabited β],
  (List.map Prod.fst l).contains k = false → (t.insertMany l)[k]! = t[k]!
-- Init.Data.Int.Order
Int.natAbs_natCast : ∀ (n : ℕ), (↑n).natAbs = n
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xn_modEq_x2n_add_lem : ∀ {a : ℕ} (a1 : 1 < a) (n j : ℕ),
  Pell.xn a1 n ∣ Pell.d✝ a1 * Pell.yn a1 n * (Pell.yn a1 n * Pell.xn a1 j) + Pell.xn a1 j
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- A face of a cone is a face of another if and only if they are contained in each other.  -/
PointedCone.IsFaceOf.isFaceOf_iff_le : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F₁ F₂ : PointedCone R M},
  F₁.IsFaceOf C → F₂.IsFaceOf C → (F₁.IsFaceOf F₂ ↔ F₁ ≤ F₂)
-- Init.Data.UInt.Lemmas
USize.zero_mul : ∀ {a : USize}, 0 * a = 0
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.mapDomainLinearEquiv_trans : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {O : Type u_5} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (e₁ : M ≃ N) (e₂ : N ≃ O),
  MonoidAlgebra.mapDomainLinearEquiv R S (e₁.trans e₂) =
    MonoidAlgebra.mapDomainLinearEquiv R S e₁ ≪≫ₗ MonoidAlgebra.mapDomainLinearEquiv R S e₂
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get?_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∩ t₂).get? k = none
-- Mathlib.Order.RelSeries
/-- In ℤ, the head and tail of an `LTSeries` differ at least by the length of the series  -/
LTSeries.head_add_length_le_int : ∀ (p : LTSeries ℤ), RelSeries.head p + ↑p.length ≤ RelSeries.last p
-- Mathlib.Topology.ContinuousMap.Ordered
ContinuousMap.sup'_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : SemilatticeSup β]
  [inst_3 : ContinuousSup β] {ι : Type u_3} {s : Finset ι} (H : s.Nonempty) (f : ι → C(α, β)) (a : α),
  (s.sup' H f) a = s.sup' H fun i => (f i) a
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Pre-composition by any function is uniformly continuous for the uniform structures of
uniform convergence.

More precisely, for any `f : γ → α`, the function `(· ∘ f) : (α →ᵤ β) → (γ →ᵤ β)` is uniformly
continuous.  -/
UniformFun.precomp_uniformContinuous : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {f : γ → α},
  UniformContinuous fun g => UniformFun.ofFun (UniformFun.toFun g ∘ f)
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.cylinder.eq_1 : ∀ {E : ℕ → Type u_1} (x : (n : ℕ) → E n) (n : ℕ), PiNat.cylinder x n = {y | ∀ i < n, y i = x i}
-- Mathlib.Algebra.Group.Commute.Units
isUnit_pow_iff_of_not_isUnit : ∀ {M : Type u_1} [inst : Monoid M] {a : M}, ¬IsUnit a → ∀ {n : ℕ}, IsUnit (a ^ n) ↔ n = 0
-- Lean.Elab.PreDefinition.TerminationHint
_private.Lean.Elab.PreDefinition.TerminationHint.0.Lean.Elab.TerminationBy.checkVars.parameters : ℕ → Lean.MessageData
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Morphisms for `WithInitial C`.  -/
CategoryTheory.WithInitial.Hom : {C : Type u} → [CategoryTheory.Category.{v, u} C] → CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → Type v
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.isPlausibleIndirectOutput_of_mem_toArray : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {it : Std.Iter β} {b : β},
  b ∈ it.toArray → it.IsPlausibleIndirectOutput b
-- Mathlib.Data.List.Basic
List.head!_append : ∀ {α : Type u} [inst : Inhabited α] (t : List α) {s : List α}, s ≠ [] → (s ++ t).head! = s.head!
-- Mathlib.LinearAlgebra.CliffordAlgebra.Prod
CliffordAlgebra.toProd.eq_1 : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] (Q₁ : QuadraticForm R M₁)
  (Q₂ : QuadraticForm R M₂),
  CliffordAlgebra.toProd Q₁ Q₂ =
    GradedTensorProduct.lift (CliffordAlgebra.evenOdd Q₁) (CliffordAlgebra.evenOdd Q₂)
      (CliffordAlgebra.map (QuadraticMap.Isometry.inl Q₁ Q₂)) (CliffordAlgebra.map (QuadraticMap.Isometry.inr Q₁ Q₂)) ⋯
-- Mathlib.CategoryTheory.Monad.Products
/-- The backward direction of the equivalence from coalgebras for the product comonad to the over
category.
 -/
CategoryTheory.overToCoalgebra : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) →
      [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] →
        CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.prodComonad X).Coalgebra
-- Mathlib.Algebra.Lie.Nilpotent
/-- The max nilpotent ideal of a Lie algebra. It is defined as the max nilpotent Lie submodule of
`L` under the adjoint action.  -/
LieAlgebra.maxNilpotentIdeal : (R : Type u) →
  (L : Type v) → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieSubmodule R L L
-- Std.Http.Data.Headers.Basic
Std.Http.Header.Host.mk.sizeOf_spec : ∀ (host : Std.Http.URI.Host) (port : Std.Http.URI.Port),
  sizeOf { host := host, port := port } = 1 + sizeOf host + sizeOf port
-- Mathlib.CategoryTheory.Adjunction.Additive
CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.Additive] (X : Cᵒᵖ) (Y : D)
  (a : ULift.{max v₁ v₂, v₂} (F.obj (Opposite.unop X) ⟶ Y)),
  (CategoryTheory.ConcreteCategory.hom ((adj.compPreadditiveYonedaIso.inv.app Y).app X)) a =
    { down := (adj.homEquiv (Opposite.unop X) Y) (AddEquiv.ulift a) }
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.TransitiveRelation.transitivity₂_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.TransitiveRelation p₁ p₂) {F : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_1 : CategoryTheory.ConcreteCategory C F]
  (x : carrier self.c.pt),
  (CategoryTheory.ConcreteCategory.hom p₂) ((CategoryTheory.ConcreteCategory.hom self.t) x) =
    (CategoryTheory.ConcreteCategory.hom p₂) ((CategoryTheory.ConcreteCategory.hom self.c.snd) x)
-- Mathlib.Data.Set.Basic
Subsingleton.set_cases : ∀ {α : Type u_1} [Subsingleton α] {p : Set α → Prop}, p ∅ → p Set.univ → ∀ (s : Set α), p s
-- Mathlib.Probability.Kernel.MeasurableIntegral
ProbabilityTheory.measurableSet_kernel_integrable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {E : Type u_4} [inst : NormedAddCommGroup E] [ProbabilityTheory.IsSFiniteKernel κ] ⦃f : α → β → E⦄,
  MeasureTheory.StronglyMeasurable (Function.uncurry f) → MeasurableSet {x | MeasureTheory.Integrable (f x) (κ x)}
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.pow_smul_le_pow_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  (F : I.Filtration M) (i j k : ℕ), I ^ (i + k) • F.N j ≤ I ^ k • F.N (i + j)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.comp_assoc : ∀ {R : Type u_1} [inst : CommSemiring R] (φ ψ χ : Polynomial R), (φ.comp ψ).comp χ = φ.comp (ψ.comp χ)
-- Init.Data.Array.Lemmas
Array.size_flatMap : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β},
  (Array.flatMap f xs).size = (Array.map (fun a => (f a).size) xs).sum
-- Mathlib.Data.List.Rotate
List.IsRotated.eqv : ∀ {α : Type u}, Equivalence List.IsRotated
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.coeff_mapRingEquiv`. -/
MonoidAlgebra.mapRingEquiv_apply : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (e : R ≃+* S) (x : MonoidAlgebra R M) (m : M), ((MonoidAlgebra.mapRingEquiv M e) x).coeff m = e (x.coeff m)
-- Mathlib.Tactic.Translate.GuessName
Mathlib.Tactic.GuessName.GuessNameData.mk.injEq : ∀ (nameDict : Std.HashMap String (List String)) (abbreviationDict : Std.HashMap String String)
  (nameDict_1 : Std.HashMap String (List String)) (abbreviationDict_1 : Std.HashMap String String),
  ({ nameDict := nameDict, abbreviationDict := abbreviationDict } =
      { nameDict := nameDict_1, abbreviationDict := abbreviationDict_1 }) =
    (nameDict = nameDict_1 ∧ abbreviationDict = abbreviationDict_1)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The cycles of a homological complex in degree `j` can be computed
by specifying a choice of `c.prev j` and `c.next j`.  -/
HomologicalComplex.cyclesIsoSc' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            (i j k : ι) →
              c.prev j = i →
                c.next j = k →
                  [inst_2 : K.HasHomology j] → [inst_3 : (K.sc' i j k).HasHomology] → K.cycles j ≅ (K.sc' i j k).cycles
-- Init.Data.Int.Linear
Int.Internal.Linear.mul_eq_zero_left : ∀ (a b : ℤ), a = 0 → a * b = 0
-- Init.Data.Nat.ToString
Nat.ofDigitChars_ten_toDigits : ∀ {n : ℕ}, Nat.ofDigitChars 10 (Nat.toDigits 10 n) 0 = n
-- Std.Data.Internal.List.Associative
Std.Internal.List.fst_mem_keys_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {a : (a : α) × β a} {l : List ((a : α) × β a)},
  a ∈ l → a.fst ∈ Std.Internal.List.keys l
-- Mathlib.Topology.Closure
Disjoint.frontier_right : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsOpen s → Disjoint s t → Disjoint s (frontier t)
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
HasOuterApproxClosed.apprSeq_apply_le_one : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F) (n : ℕ)
  (x : X), (hF.apprSeq n) x ≤ 1
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalClosure_idempotent : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G},
  AddSubgroup.normalClosure ↑(AddSubgroup.normalClosure s) = AddSubgroup.normalClosure s
-- Mathlib.Algebra.BigOperators.Fin
_private.Mathlib.Algebra.BigOperators.Fin.0.finSigmaFinEquiv.match_1.splitter : (motive : (m : ℕ) → {n : Fin m → ℕ} → Sort u_1) →
  (m : ℕ) → {n : Fin m → ℕ} → ((n : Fin 0 → ℕ) → motive 0) → ((m : ℕ) → (n : Fin m.succ → ℕ) → motive m.succ) → motive m
-- Mathlib.Algebra.Order.Interval.Set.Instances
/-- The coercion from `Set.Ioo 0 1` as a `MulHom`.  -/
Set.Ioo.coeMulHom : {R : Type u_1} →
  [inst : Semiring R] → [inst_1 : PartialOrder R] → [inst_2 : IsStrictOrderedRing R] → ↑(Set.Ioo 0 1) →ₙ* R
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.ofMulEquivOfDom.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {T : Submonoid P} {k : P ≃* M}
  (H : Submonoid.map k.toMonoidHom T = S),
  f.ofMulEquivOfDom H = (f.toMonoidHom.comp k.toMonoidHom).toLocalizationMap ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- A map from `X` to the equalizer  -/
CategoryTheory.IsSplitEqualizer.leftRetraction : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f g : X ⟶ Y} → {W : C} → {ι : W ⟶ X} → CategoryTheory.IsSplitEqualizer f g ι → (X ⟶ W)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.dFrom_comp_xNextIsoSelf_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i : ι}
  (h : ¬c.Rel i (c.next i)) {Z : V} (h_1 : C.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (C.dFrom i) (CategoryTheory.CategoryStruct.comp (C.xNextIsoSelf h).hom h_1) =
    CategoryTheory.CategoryStruct.comp 0 h_1
-- Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition
Echelon.Decomposition.rank_eq : ∀ {m : Type u_1} [inst : Fintype m] [inst_1 : LinearOrder m] {n : Type u_2} [inst_2 : Fintype n]
  [inst_3 : LinearOrder n] {R : Type u_3} [inst_4 : CommRing R] [IsDomain R] {A : Matrix m n R}
  (cert : Echelon.Decomposition A), A.rank = {i | cert.pivot i ≠ ⊤}.card