mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Colimit.Module
/-- Consider direct limits `lim G` and `lim G'` with direct system `f` and `f'` respectively, any
family of linear maps `gᵢ : Gᵢ ⟶ G'ᵢ` such that `g ∘ f = f' ∘ g` induces a linear map
`lim G ⟶ lim G'`.
 -/
Module.DirectLimit.map : {R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_2} →
      [inst_1 : Preorder ι] →
        {G : ι → Type u_3} →
          [inst_2 : (i : ι) → AddCommMonoid (G i)] →
            [inst_3 : (i : ι) → Module R (G i)] →
              {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j} →
                [inst_4 : DecidableEq ι] →
                  {G' : ι → Type u_5} →
                    [inst_5 : (i : ι) → AddCommMonoid (G' i)] →
                      [inst_6 : (i : ι) → Module R (G' i)] →
                        {f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j} →
                          (g : (i : ι) → G i →ₗ[R] G' i) →
                            (∀ (i j : ι) (h : i ≤ j), g j ∘ₗ f i j h = f' i j h ∘ₗ g i) →
                              Module.DirectLimit G f →ₗ[R] Module.DirectLimit G' f'
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.toENNRealVectorMeasure_add : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α),
  (μ + ν).toENNRealVectorMeasure = μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- `NormedSpace.exp x` has explicit two-sided inverse `NormedSpace.exp (-x)`.  -/
NormedSpace.invertibleExp : {𝔸 : Type u_1} →
  [inst : NormedRing 𝔸] → [NormedAlgebra ℚ 𝔸] → [CompleteSpace 𝔸] → (x : 𝔸) → Invertible (NormedSpace.exp x)
-- Init.Data.SInt.Lemmas
Int64.toInt.eq_1 : ∀ (i : Int64), i.toInt = i.toBitVec.toInt
-- Mathlib.Order.MinMax
min_lt_min_left_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, min a c < min b c ↔ a < b ∧ a < c
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.δ.eq_1 : ∀ {G : Type v} [inst : Monoid G] (X Y : Action (Type w) G) {k : Type u} [inst_1 : CommSemiring k],
  Representation.LinearizeMonoidal.δ X Y = { toLinearMap := ↑(MonoidAlgebra.tensorEquiv k).symm, isIntertwining' := ⋯ }
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  {f : α → ε}, 0 < q → MeasureTheory.eLpNorm' f q μ < ⊤ → ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ < ⊤
-- Mathlib.Order.Bounds.Basic
bbdBelow_range_inf_iff : ∀ {ι : Sort u_4} {α : Type u_5} [inst : SemilatticeInf α] {f g : ι → α},
  BddBelow (Set.range fun x => f x ⊓ g x) ↔ BddBelow (Set.range f) ∧ BddBelow (Set.range g)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_le_card_div_self : ∀ {α : Type u_2} [inst : Group α] [inst_1 : DecidableEq α] {s : Finset α}, s.card ≤ (s / s).card
-- Init.Meta.Defs
Lean.instQuoteRawMkStr1 : Lean.Quote Substring.Raw
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Retrieve the underlying value from a `ArchimedeanOrder` element.  -/
ArchimedeanOrder.val : {M : Type u_1} → ArchimedeanOrder M ≃ M
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- The cocone over the proposed colimit semiring.  -/
SemiRingCat.FilteredColimits.colimitCocone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J SemiRingCat) → [CategoryTheory.IsFiltered J] → CategoryTheory.Limits.Cocone F
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t_id : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀),
  AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i i =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g i i)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.SymbolPriorityEntry.prio : Lean.Meta.Grind.SymbolPriorityEntry → ℕ
-- Lean.Meta.SynthInstance
Lean.Meta.backward.synthInstance.canonInstances : Lean.Option Bool
-- Lean.LoadDynlib
_private.Lean.LoadDynlib.0.Lean.loadPlugin.unsafe_7 : (dynlib : Lean.Dynlib) → dynlib.Symbol → IO Unit
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.unitBallBall_symm_apply : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {P : Type u_2}
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor E P] (c : P) (r : ℝ) (hr : 0 < r) (a : P),
  ↑(OpenPartialHomeomorph.unitBallBall c r hr).symm a = r⁻¹ • (a -ᵥ c)
-- Mathlib.Data.Fin.Embedding
Fin.equiv_iff_eq : ∀ {n m : ℕ}, Nonempty (Fin m ≃ Fin n) ↔ m = n
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.iInf_ker_truncate : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)], ⨅ i, RingHom.ker (WittVector.truncate i) = ⊥
-- Mathlib.Algebra.Homology.Embedding.Basic
/-- The embedding from `down ℕ` to `up ℤ` which sends `n : ℕ` to `p - n`.  -/
ComplexShape.embeddingUpIntLE : ℤ → (ComplexShape.down ℕ).Embedding (ComplexShape.up ℤ)
-- Lean.Elab.Syntax
Lean.Elab.Term.checkLeftRec : Lean.Syntax → Lean.Elab.Term.ToParserDescrM Bool
-- Mathlib.LinearAlgebra.Transvection.Generation
LinearEquiv.fixedSubmodule_transvection_mul : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.Finite K V] (e : V ≃ₗ[K] V) {f : Module.Dual K V} {v : V},
  v ∉ (↑e).fixedSubmodule →
    Submodule.map f (↑e).fixedSubmodule = ⊥ →
      ∀ (hfv : f (v - e v) = 0),
        f (e v) = 1 → (↑(LinearEquiv.transvection hfv * e)).fixedSubmodule = (↑e).fixedSubmodule ⊔ K ∙ v
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.ofMonComonObjX_one : ∀ {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.MonObj.one =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      CategoryTheory.MonObj.one.hom
-- Lean.Elab.Match
/-- `true` when performing dependent elimination. We use this to decide whether we optimize the "match unit" case.
See `isMatchUnit?`.  -/
Lean.Elab.Term.ElabMatchTypeAndDiscrsResult.isDep : Lean.Elab.Term.ElabMatchTypeAndDiscrsResult → Bool
-- Mathlib.Topology.PartialHomeomorph.Defs
Homeomorph.toPartialHomeomorph_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y),
  e.toPartialHomeomorph.target = Set.univ
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Presieve.CoverByImageStructure.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {G : CategoryTheory.Functor C D} →
          {V U : D} → {f : V ⟶ U} → (self : CategoryTheory.Presieve.CoverByImageStructure G f) → G.obj self.obj ⟶ U
-- Mathlib.Data.List.Permutation
List.length_permutations'Aux : ∀ {α : Type u_1} (s : List α) (x : α), (List.permutations'Aux x s).length = s.length + 1
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_sub : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocRing α] [inst_1 : Fintype m] (A B : Matrix m n α)
  (x : m → α), Matrix.vecMul x (A - B) = Matrix.vecMul x A - Matrix.vecMul x B
-- Mathlib.Order.Interval.Finset.Defs
Finset.mem_Ioo : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b x : α}, x ∈ Finset.Ioo a b ↔ a < x ∧ x < b
-- Mathlib.Data.Fin.SuccPred
Fin.cast_inj : ∀ {n m : ℕ} (eq : n = m) {a b : Fin n}, Fin.cast eq a = Fin.cast eq b ↔ a = b
-- Mathlib.Order.Fin.Basic
Fin.range_succAboveOrderEmb : ∀ {n : ℕ} (i : Fin (n + 1)), Set.range ⇑i.succAboveOrderEmb = {i}ᶜ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_eq_minKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {he : t.isEmpty = false} {fallback : α}, t.minKey he = t.minKeyD fallback
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.supOfBasis.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.house.supOfBasis✝ K = NumberField.house.supOfBasis✝ K
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSet.tProd : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (i : δ) → MeasurableSpace (X i)] (l : List δ) {s : (i : δ) → Set (X i)},
  (∀ (i : δ), MeasurableSet (s i)) → MeasurableSet (Set.tprod l s)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
isZero_groupHomology_succ_of_subsingleton : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [Subsingleton G] (n : ℕ),
  CategoryTheory.Limits.IsZero (groupHomology A (n + 1))
-- Mathlib.RingTheory.Finiteness.Cardinality
Submodule.fg_iff_exists_fin_linearMap : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M}, N.FG ↔ ∃ n f, f.range = N
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.mem_one : ∀ {R : Type u_2} [inst : AddMonoidWithOne R] {x : R}, x ∈ 1 ↔ ∃ n, ↑n = x
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.ComonObj.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X : C} →
        (counit : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) →
          (comul : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X X) →
            autoParam
                (CategoryTheory.CategoryStruct.comp comul
                    (CategoryTheory.MonoidalCategoryStruct.whiskerRight counit X) =
                  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv)
                CategoryTheory.ComonObj.counit_comul._autoParam →
              autoParam
                  (CategoryTheory.CategoryStruct.comp comul
                      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X counit) =
                    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv)
                  CategoryTheory.ComonObj.comul_counit._autoParam →
                autoParam
                    (CategoryTheory.CategoryStruct.comp comul
                        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X comul) =
                      CategoryTheory.CategoryStruct.comp comul
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight comul X)
                          (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom))
                    CategoryTheory.ComonObj.comul_assoc._autoParam →
                  CategoryTheory.ComonObj X
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.HoldsForLocalizationAway.of_bijective : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S)
  (P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop),
  (RingHom.HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P) → Function.Bijective ⇑f → P f
-- Mathlib.CategoryTheory.Subobject.Basic
/-- To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with
the arrows.  -/
CategoryTheory.Subobject.mk_eq_of_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} {X : CategoryTheory.Subobject B} (f : A ⟶ B)
  [inst_1 : CategoryTheory.Mono f] (i : A ≅ CategoryTheory.Subobject.underlying.obj X),
  CategoryTheory.CategoryStruct.comp i.hom X.arrow = f → CategoryTheory.Subobject.mk f = X
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.desc.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Balanced C] (hS : S.Exact) {A : C} (k k_1 : S.X₂ ⟶ A)
  (e_k : k = k_1) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0) [inst_3 : CategoryTheory.Epi S.g],
  hS.desc k hk = hS.desc k_1 ⋯
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
/-- The morphism `K.restriction e ⟶ L` induced by a morphism `K ⟶ L.extend e`.  -/
ComplexShape.Embedding.homRestrict : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          {C : Type u_3} →
            [inst : CategoryTheory.Category.{v_1, u_3} C] →
              [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
                [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                  {K : HomologicalComplex C c'} →
                    {L : HomologicalComplex C c} → [inst_3 : e.IsRelIff] → (K ⟶ L.extend e) → (K.restriction e ⟶ L)
-- Mathlib.Analysis.Calculus.UniformLimitsDeriv
/-- If our derivatives converge uniformly, then the Fréchet derivatives converge uniformly  -/
UniformCauchySeqOnFilter.one_smulRight : ∀ {ι : Type u_1} {l : Filter ι} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {G : Type u_3}
  [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f' : ι → 𝕜 → G} {l' : Filter 𝕜},
  UniformCauchySeqOnFilter f' l l' → UniformCauchySeqOnFilter (fun n z => ContinuousLinearMap.smulRight 1 (f' n z)) l l'
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.id_mapId_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (a : B),
  ((CategoryTheory.StrictlyUnitaryPseudofunctor.id B).mapId a).hom =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateAddAct.ext_iff : ∀ {α : Type u_1} {f : α → α} {x y : IterateAddAct f}, x = y ↔ x.val = y.val
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.toSubgraph.eq_def : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (x : G.Walk u v),
  x.toSubgraph =
    match v, x with
    | .(u), SimpleGraph.Walk.nil => G.singletonSubgraph u
    | v, SimpleGraph.Walk.cons h p => G.subgraphOfAdj h ⊔ p.toSubgraph
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_set_iInter : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {ι : Sort u_5} (a : α) (t : ι → Set β),
  a • ⋂ i, t i = ⋂ i, a • t i
-- Mathlib.Order.Category.BoolAlg
BoolAlg.forget_map : ∀ {X Y : BoolAlg} (f : X ⟶ Y),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget BoolAlg).map f)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_val_Iio : ∀ {n : ℕ} (b : Fin n), Finset.image Fin.val (Finset.Iio b) = Finset.Iio ↑b
-- Mathlib.GroupTheory.RegularWreathProduct
/-- The function of Q → D  -/
RegularWreathProduct.left : {D : Type u_1} → {Q : Type u_2} → D ≀ᵣ Q → Q → D
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian of a constant function is zero.
 -/
InnerProductSpace.laplacian_const : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {c : F},
  (Laplacian.laplacian fun x => c) = 0
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.State.mk.inj : ∀ {status : Std.HashMap String ℕ} {progress : Bool} {solvedSuggestions : Array ProofWidgets.Html}
  {status_1 : Std.HashMap String ℕ} {progress_1 : Bool} {solvedSuggestions_1 : Array ProofWidgets.Html},
  { status := status, progress := progress, solvedSuggestions := solvedSuggestions } =
      { status := status_1, progress := progress_1, solvedSuggestions := solvedSuggestions_1 } →
    status = status_1 ∧ progress = progress_1 ∧ solvedSuggestions = solvedSuggestions_1
-- ProofWidgets.Component.MakeEditLink
/-- Replace `range` with `newText`.
If `newSelection?` is absent, place the cursor at the end of the new text.
If `newSelection?` is present, make the specified selection instead.
See also `MakeEditLinkProps.ofReplaceRange`.
 -/
ProofWidgets.MakeEditLinkProps.ofReplaceRange' : Lean.Server.DocumentMeta →
  Lean.Lsp.Range → String → optParam (Option Lean.Lsp.Range) none → ProofWidgets.MakeEditLinkProps
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.IsHamiltonian.connected : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} [inst_1 : Fintype α], G.IsHamiltonian → G.Connected
-- Lean.Level
_private.Lean.Level.0.Lean.Level.isIMax.match_1.eq_2 : ∀ (motive : Lean.Level → Sort u_1) (x : Lean.Level) (h_1 : (a a_1 : Lean.Level) → motive (a.imax a_1))
  (h_2 : (x : Lean.Level) → motive x),
  (∀ (a a_1 : Lean.Level), x = a.imax a_1 → False) →
    (match x with
      | a.imax a_1 => h_1 a a_1
      | x => h_2 x) =
      h_2 x
-- Mathlib.Analysis.Convex.Extreme
IsExtreme.refl : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] (A : Set E), IsExtreme 𝕜 A A
-- Std.Data.ExtTreeMap.Lemmas
/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the
proof obligation in the statement of `get_insertIfNew`.  -/
Std.ExtTreeMap.mem_of_mem_insertIfNew' : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β}, a ∈ t.insertIfNew k v → ¬(cmp k a = Ordering.eq ∧ k ∉ t) → a ∈ t
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.SmallHom.mk.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {X Y : C}
  [inst_1 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y] (f : X ⟶ Y),
  CategoryTheory.Localization.SmallHom.mk W f = (CategoryTheory.Localization.SmallHom.equiv W W.Q).symm (W.Q.map f)
-- Mathlib.MeasureTheory.Group.Convolution
/-- Additive convolution of measures.  -/
MeasureTheory.Measure.conv : {M : Type u_1} →
  [AddMonoid M] →
    [inst : MeasurableSpace M] → MeasureTheory.Measure M → MeasureTheory.Measure M → MeasureTheory.Measure M
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
/-- Linear upper bound for `f (x + n)` on unit interval  -/
Real.BohrMollerup.f_add_nat_le : ∀ {f : ℝ → ℝ} {x : ℝ} {n : ℕ},
  ConvexOn ℝ (Set.Ioi 0) f →
    (∀ {y : ℝ}, 0 < y → f (y + 1) = f y + Real.log y) → n ≠ 0 → 0 < x → x ≤ 1 → f (↑n + x) ≤ f ↑n + x * Real.log ↑n
-- Mathlib.CategoryTheory.Square
/-- The functor `Arrow (Arrow C) ⥤ Square C` which sends
a morphism `Arrow.mk f ⟶ Arrow.mk g` to the commutative square
with `f` on the top side and `g` on the bottom side.  -/
CategoryTheory.Square.fromArrowArrowFunctor' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.Arrow (CategoryTheory.Arrow C)) (CategoryTheory.Square C)
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.Intersecting.notMem : ∀ {α : Type u_1} [inst : BooleanAlgebra α] {s : Set α}, s.Intersecting → ∀ {a : α}, aᶜ ∈ s → a ∉ s
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.FinMeasAdditive.sub : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} {T T' : Set α → β}
  [inst : AddCommGroup β],
  MeasureTheory.FinMeasAdditive μ T → MeasureTheory.FinMeasAdditive μ T' → MeasureTheory.FinMeasAdditive μ (T - T')
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.priority.injEq : ∀ (p p_1 : Aesop.Frontend.Priority),
  (Aesop.Frontend.Feature.priority p = Aesop.Frontend.Feature.priority p_1) = (p = p_1)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- The cokernel of a zero map is preserved by any functor which preserves zero morphisms.  -/
CategoryTheory.Limits.preservesCokernel_zero' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  {X Y : C} (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] (f : X ⟶ Y),
  f = 0 → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.instReprKey : Repr Lean.Meta.DiscrTree.Key
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.eval.match_1.eq_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {K : CategoryTheory.Precoverage C}
  (ι : C → Type (max u_1 u_2))
  (motive : (x : C) → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι x → Sort u_3) (x Y : C) (f : x ⟶ Y)
  (i : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι Y)
  (h_1 : (X : C) → (i : ι X) → motive X (CategoryTheory.Precoverage.SmallConstruction.Witness.base✝ X i))
  (h_2 :
    (x Y : C) →
      (f : x ⟶ Y) →
        (i : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι Y) →
          motive x (CategoryTheory.Precoverage.SmallConstruction.Witness.restrict✝ f i))
  (h_3 :
    (x : C) →
      (R : CategoryTheory.Presieve x) →
        (hR : R ∈ K.coverings x) →
          (h : ⦃W : C⦄ → (r : W ⟶ x) → R r → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι W) →
            motive x (CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate✝ hR h)),
  (match x, CategoryTheory.Precoverage.SmallConstruction.Witness.restrict✝ f i with
    | X, CategoryTheory.Precoverage.SmallConstruction.Witness.base✝ .(X) i => h_1 X i
    | x, CategoryTheory.Precoverage.SmallConstruction.Witness.restrict✝ f i => h_2 x Y f i
    | x, CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate✝ hR h => h_3 x R hR h) =
    h_2 x Y f i
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.id.eq_1 : ∀ (M : Type u_10) [inst : Add M], AddHom.id M = { toFun := fun x => x, map_add' := ⋯ }
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegral.tower_bot_of_field : ∀ {R : Type u_6} {A : Type u_7} {B : Type u_8} [inst : CommRing R] [inst_1 : Field A] [inst_2 : Ring B] [Nontrivial B]
  [inst_4 : Algebra R A] [inst_5 : Algebra A B] [inst_6 : Algebra R B] [IsScalarTower R A B] {x : A},
  IsIntegral R ((algebraMap A B) x) → IsIntegral R x
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- The identity modification.  -/
CategoryTheory.Oplax.LaxTrans.Modification.id : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} → (η : F ⟶ G) → CategoryTheory.Oplax.LaxTrans.Modification η η
-- Batteries.Data.List.Lemmas
List.swap_self : ∀ {α : Type u_1} {xs : List α} {i : ℕ}, xs.swap i i = xs
-- Mathlib.Algebra.Order.Module.Defs
lt_smul_iff_one_lt_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Monoid α] [inst_1 : Zero β] [inst_2 : MulAction α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosStrictMono α β] [SMulPosReflectLT α β],
  0 < b → (b < a • b ↔ 1 < a)
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.toProd_pow : ∀ {α : Type u_2} [inst : Monoid α] [inst_1 : Preorder α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α]
  (s : NonemptyInterval α) (n : ℕ), (s ^ n).toProd = s.toProd ^ n
-- Lean.Expr
Lean.Expr.lit.inj : ∀ {a a_1 : Lean.Literal}, Lean.Expr.lit a = Lean.Expr.lit a_1 → a = a_1
-- Mathlib.Order.Fin.Basic
Fin.coe_succOrderEmb : ∀ {n : ℕ}, ⇑(Fin.succOrderEmb n) = Fin.succ
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.Measure.integrable_integral_norm_of_integrable_comp : ∀ {α : Type u_5} {β : Type u_6} {E : Type u_7} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : NormedAddCommGroup E] {κ : ProbabilityTheory.Kernel α β} {μ : MeasureTheory.Measure α} {f : β → E},
  MeasureTheory.Integrable f (μ.bind ⇑κ) → MeasureTheory.Integrable (fun x => ∫ (y : β), ‖f y‖ ∂κ x) μ
-- Init.Data.Int.Order
Int.mul_le_mul_of_nonpos_left : ∀ {a b c : ℤ}, a ≤ 0 → c ≤ b → a * b ≤ a * c