mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.cokernelCoforkOfCofork_ofπ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y}
  {P : C} (π : Y ⟶ P) (w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π),
  CategoryTheory.Preadditive.cokernelCoforkOfCofork (CategoryTheory.Limits.Cofork.ofπ π w) =
    CategoryTheory.Limits.CokernelCofork.ofπ π ⋯
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.eval_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type w} (b : β) {X Y : CategoryTheory.GradedObject β C}
  (f : X ⟶ Y), (CategoryTheory.GradedObject.eval b).map f = f b
-- Mathlib.Order.Filter.Finite
Filter.EventuallyLE.iInter : ∀ {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s t : ι → Set α},
  (∀ (i : ι), s i ≤ᶠ[l] t i) → ⋂ i, s i ≤ᶠ[l] ⋂ i, t i
-- Mathlib.Algebra.Group.Graph
/-- **Vertical line test** for monoid homomorphisms.

Let `G ≤ H × I` be a submonoid of a product of monoids. Assume that `G` maps bijectively to the
first factor. Then `G` is the graph of some monoid homomorphism `f : H → I`.  -/
Submonoid.exists_eq_mgraph : ∀ {H : Type u_2} {I : Type u_3} [inst : Monoid H] [inst_1 : Monoid I] {G : Submonoid (H × I)},
  Function.Bijective (Prod.fst ∘ ⇑G.subtype) → ∃ f, G = f.mgraph
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
/-- Vertices of a closed trail are 2-edge reachable.  -/
SimpleGraph.Walk.IsTrail.isEdgeReachable_two : ∀ {V : Type u_1} {G : SimpleGraph V} {u x y : V} {w : G.Walk u u},
  w.IsTrail → x ∈ w.support → y ∈ w.support → G.IsEdgeReachable 2 x y
-- Std.Http.Data.Extensions
/-- Retrieves a value of type `α` from the extensions, if present.
 -/
Std.Http.Extensions.get : Std.Http.Extensions → (α : Type) → [TypeName α] → Option α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.Color.mk.sizeOf_spec : ∀ (red green blue alpha : Float),
  sizeOf { red := red, green := green, blue := blue, alpha := alpha } =
    1 + sizeOf red + sizeOf green + sizeOf blue + sizeOf alpha
-- Std.Http.Data.URI.Encoding
Std.Http.URI.instHashableEncodedQueryString : {r : UInt8 → Bool} → Hashable (Std.Http.URI.EncodedQueryString r)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.tensorUnit_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C},
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X)).left = X
-- Batteries.Data.String.Lemmas
String.utf8GetAux_of_valid : ∀ (cs cs' : List Char) {i p : ℕ},
  i + String.utf8Len cs = p →
    String.Pos.Raw.utf8GetAux (cs ++ cs') { byteIdx := i } { byteIdx := p } = cs'.headD default
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.isClosedEmbedding_mk : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsClosedEmbedding ⇑DomAddAct.mk
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.cancelVar.eq_1 : ∀ (c : ℤ) (x : Lean.Grind.CommRing.Var) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.cancelVar c x p = Lean.Grind.CommRing.Poly.cancelVar' c x p (Lean.Grind.CommRing.Poly.num 0)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, Std.DTreeMap.Raw.Const.get? (t.insert k v) k = some v
-- Mathlib.Analysis.Complex.Circle
Circle.coe_zpow : ∀ (z : Circle) (n : ℤ), ↑(z ^ n) = ↑z ^ n
-- Lean.Meta.MkIffOfInductiveProp
/-- `compactRelation bs as_ps`: Produce a relation of the form:
```lean
R := fun as ↦ ∃ bs, ⋀_i a_i = p_i[bs]
```
This relation is user-visible, so we compact it by removing each `b_j` where a `p_i = b_j`, and
hence `a_i = b_j`. We need to take care when there are `p_i` and `p_j` with `p_i = p_j = b_k`.
 -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.compactRelation : List Lean.Expr →
  List (Lean.Expr × Lean.Expr) → List (Option Lean.Expr) × List (Lean.Expr × Lean.Expr) × (Lean.Expr → Lean.Expr)
-- Mathlib.Algebra.Polynomial.Laurent
/-- Evaluate a Laurent polynomial at a unit, using scalar multiplication.  -/
LaurentPolynomial.smeval : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid S] → [SMulWithZero R S] → [inst_3 : Monoid S] → LaurentPolynomial R → Sˣ → S
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.leftAdjointUniq_trans_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F F' F'' : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (adj3 : F'' ⊣ G) (x : C) {Z : D} (h : F''.obj x ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((adj1.leftAdjointUniq adj2).hom.app x)
      (CategoryTheory.CategoryStruct.comp ((adj2.leftAdjointUniq adj3).hom.app x) h) =
    CategoryTheory.CategoryStruct.comp ((adj1.leftAdjointUniq adj3).hom.app x) h
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_list_sum_map : ∀ {R : Type u} [inst : Semiring R] {ι : Type u_1} (l : List ι) (f : ι → Polynomial R) (n : ℕ),
  (List.map f l).sum.coeff n = (List.map (fun a => (f a).coeff n) l).sum
-- Mathlib.Analysis.Normed.Affine.AddTorsor
nndist_self_homothety : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜),
  nndist p₂ ((AffineMap.homothety p₁ c) p₂) = ‖1 - c‖₊ * nndist p₁ p₂
-- Init.Internal.Order.While
_private.Init.Internal.Order.While.0.Lean.Loop.forIn.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b' : β) (h_1 : (b' : β) → motive (ForInStep.done b'))
  (h_2 : (b' : β) → motive (ForInStep.yield b')),
  (match ForInStep.yield b' with
    | ForInStep.done b' => h_1 b'
    | ForInStep.yield b' => h_2 b') =
    h_2 b'
-- Mathlib.GroupTheory.IsSubnormal
AddSubgroup.IsSubnormal.addSubgroupOf : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.IsSubnormal → (H.addSubgroupOf K).IsSubnormal
-- Mathlib.Algebra.Module.PUnit
PUnit.mulAction : {R : Type u_1} → [inst : Monoid R] → MulAction R PUnit.{u_3 + 1}
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.ofHom_id : ∀ {M : Type u} [inst : SeminormedAddCommGroup M],
  SemiNormedGrp.ofHom (NormedAddGroupHom.id M) = CategoryTheory.CategoryStruct.id { carrier := M, str := inst }
-- Mathlib.RingTheory.Flat.Basic
/-- If p and q are submodules of M and N respectively, and M and q are flat,
then `p ⊗ q → M ⊗ N` is injective.  -/
Module.Flat.tensorProduct_mapIncl_injective_of_right : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (p : Submodule R M) (q : Submodule R N)
  [Module.Flat R M] [Module.Flat R ↥q], Function.Injective ⇑(TensorProduct.mapIncl p q)
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.neg_op_vadd_finset_distrib : ∀ {α : Type u_2} [inst : AddGroup α] [inst_1 : DecidableEq α] (a : α) (s : Finset α),
  -(AddOpposite.op a +ᵥ s) = -a +ᵥ -s
-- Mathlib.Topology.Constructions
ContinuousAt.finTail : ∀ {X : Type u} [inst : TopologicalSpace X] {n : ℕ} {A : Fin (n + 1) → Type u_9}
  [inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)] {f : X → (j : Fin (n + 1)) → A j} {x : X},
  ContinuousAt f x → ContinuousAt (fun a => Fin.tail (f a)) x
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.instCountablyGeneratedProd : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [MeasurableSpace.CountablyGenerated α]
  [inst_2 : MeasurableSpace β] [MeasurableSpace.CountablyGenerated β], MeasurableSpace.CountablyGenerated (α × β)
-- Lean.Parser.Basic
Lean.Parser.indexed : {α : Type} →
  Lean.Parser.TokenMap α →
    Lean.Parser.ParserContext →
      Lean.Parser.ParserState → Lean.Parser.LeadingIdentBehavior → Lean.Parser.ParserState × List α
-- Lean.Elab.Command
Lean.Elab.Command.instAddMessageContextCommandElabM : Lean.AddMessageContext Lean.Elab.Command.CommandElabM
-- Mathlib.LinearAlgebra.Orientation
/-- Negating a single basis vector (represented using `units_smul`) negates the corresponding
orientation.  -/
Module.Basis.orientation_neg_single : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  (e : Module.Basis ι R M) (i : ι), (e.unitsSMul (Function.update 1 i (-1))).orientation = -e.orientation
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The ring equiv between the top element of `Subsemiring R` and `R`.  -/
Subsemiring.topEquiv : {R : Type u} → [inst : NonAssocSemiring R] → ↥⊤ ≃+* R
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_neg_of_neg_of_pi_div_two_lt : ∀ {x : ℝ}, x < 0 → -(Real.pi / 2) < x → Real.tan x < 0
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs.0.EisensteinSeries.termφ : Lean.ParserDescr
-- Mathlib.Order.Filter.Germ.OrderedMonoid
Filter.Germ.instIsOrderedAddCancelMonoid : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : AddCommMonoid β] [inst_1 : Preorder β]
  [IsOrderedCancelAddMonoid β], IsOrderedCancelAddMonoid (l.Germ β)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryLT?.go.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (x : Ordering) (h_1 : Unit → motive Ordering.gt) (h_2 : (x : Ordering) → motive x),
  (x = Ordering.gt → False) →
    (match x with
      | Ordering.gt => h_1 ()
      | x => h_2 x) =
      h_2 x
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.Monic.prime_of_degree_eq_one : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] {p : Polynomial R}, p.degree = 1 → p.Monic → Prime p
-- Lean.Meta.Sym.SymM
/-- Incremental variant of `shareCommon` for expressions constructed from already-shared subterms.

Use this when an expression `e` was produced by a Lean API (e.g., `inferType`, `mkApp4`) that
does not preserve maximal sharing, but the inputs to that API were already maximally shared.

Unlike `shareCommon`, this function does not use a local `Std.HashMap ExprPtr Expr` to
track visited nodes. This is more efficient when the number of new (unshared) nodes is small,
which is the common case when wrapping API calls that build a few constructor nodes around
shared inputs.

Example:
```
-- `a` and `b` are already maximally shared
let result := mkApp2 f a b  -- result is not maximally shared
let result ← shareCommonInc result -- efficiently restore sharing
```
 -/
Lean.Meta.Sym.share : Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.ofParallelHoms_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Limits.MulticospanShape) {X Y : C}
  (f g : X ⟶ Y) (x : J.L), (CategoryTheory.Limits.MulticospanIndex.ofParallelHoms J f g).left x = X
-- Init.Data.Int.Lemmas
Int.add_right_neg : ∀ (a : ℤ), a + -a = 0
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.whiskerLeftFunctor_map_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n m : ℕ}
  (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) {X Y : CategoryTheory.ComposableArrows C m} (f : X ⟶ Y)
  (X_1 : Fin (n + 1)), ((CategoryTheory.ComposableArrows.whiskerLeftFunctor Φ).map f).app X_1 = f.app (Φ.obj X_1)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryLE.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.gt = Ordering.gt → motive Ordering.gt)
  (h_2 : Ordering.gt = Ordering.eq → motive Ordering.eq) (h_3 : Ordering.gt = Ordering.lt → motive Ordering.lt),
  (match hkky : Ordering.gt with
    | Ordering.gt => h_1 hkky
    | Ordering.eq => h_2 hkky
    | Ordering.lt => h_3 hkky) =
    h_1 ⋯
-- Init.Data.BitVec.Lemmas
BitVec.setWidth'_eq : ∀ {w v : ℕ} {x : BitVec w} (h : w ≤ v), BitVec.setWidth' h x = BitVec.setWidth v x
-- Mathlib.FieldTheory.Galois.Infinite
ClosedSubgroup.mk.congr_simp : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G] (toSubgroup toSubgroup_1 : Subgroup G)
  (e_toSubgroup : toSubgroup = toSubgroup_1) (isClosed' : IsClosed toSubgroup.carrier),
  { toSubgroup := toSubgroup, isClosed' := isClosed' } = { toSubgroup := toSubgroup_1, isClosed' := ⋯ }
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassFactorizationAt.isUnit : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A},
  g.IsWeierstrassFactorizationAt f h I → IsUnit h
-- Mathlib.Order.CompactlyGenerated.Basic
/-- This property is equivalent to `α` being upper continuous.  -/
inf_sSup_eq_iSup_inf_sup_finset : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsCompactlyGenerated α] {a : α} {s : Set α},
  a ⊓ sSup s = ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id
-- Mathlib.Analysis.Normed.Group.Bounded
/-- A helper lemma used to prove that the (scalar or usual) product of a function that
tends to zero and a bounded function tends to zero. This lemma is formulated for any binary
operation `op : E → F → G` with an estimate `‖op x y‖ ≤ A * ‖x‖ * ‖y‖` for some constant A instead
of multiplication so that it can be applied to `(*)`, `flip (*)`, `(•)`, and `flip (•)`.  -/
Filter.Tendsto.op_zero_isBoundedUnder_le' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : SeminormedAddGroup E]
  [inst_1 : SeminormedAddGroup F] [inst_2 : SeminormedAddGroup G] {f : α → E} {g : α → F} {l : Filter α},
  Filter.Tendsto f l (nhds 0) →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ g) →
      ∀ (op : E → F → G),
        (∃ A, ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖) → Filter.Tendsto (fun x => op (f x) (g x)) l (nhds 0)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.ofEpi.eq_1 : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N)
  [inst_3 : CategoryTheory.Epi p],
  σ.ofEpi p = { I := σ.I, s := fun i => SheafOfModules.sectionsMap p (σ.s i), epi := ⋯ }
-- Mathlib.Order.Hom.Basic
OrderIso.isMax_apply : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {x : α}, IsMax (f x) ↔ IsMax x
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.singleton_inj : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : T1Space α] {x y : α}, {x} = {y} ↔ x = y
-- Mathlib.Algebra.Category.ModuleCat.Localization
/-- The `R` module structure on `M.localizedModule S` given by the
`R` module structure on `Shrink.{v} (LocalizedModule S M)`  -/
ModuleCat.instModuleCarrierLocalizationLocalizedModule : {R : Type u} →
  [inst : CommRing R] →
    [inst_1 : Small.{v, u} R] → (M : ModuleCat R) → (S : Submonoid R) → Module R ↑(M.localizedModule S)
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.restrictScalarsId'_inv_app_hom_apply : ∀ {R : Type u_1} [inst : CommRing R] (f : R →+* R) (hf : f = RingHom.id R) (X : AlgCat R) (a : ↑X),
  (AlgCat.Hom.hom ((AlgCat.restrictScalarsId' f hf).inv.app X)) a = a
-- Mathlib.Algebra.Star.StarRingHom
/-- Reinterpret a non-unital star ring homomorphism as a non-unital ring homomorphism
by forgetting the interaction with the star operation.

Users should not make use of this, but instead utilize the coercion obtained through
the `NonUnitalRingHomClass` instance.  -/
NonUnitalStarRingHom.toNonUnitalRingHom : {A : Type u_1} →
  {B : Type u_2} →
    [inst : NonUnitalNonAssocSemiring A] →
      [inst_1 : Star A] → [inst_2 : NonUnitalNonAssocSemiring B] → [inst_3 : Star B] → (A →⋆ₙ+* B) → A →ₙ+* B
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.isDiscrete_comap_preimage_singleton : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.QuasiFinite R S] (P : PrimeSpectrum R), IsDiscrete (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {P})
-- Mathlib.Algebra.Group.Prod
Prod.instAddMonoid.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  Prod.instAddMonoid =
    { toAddSemigroup := Prod.instAddSemigroup, toZero := Prod.instAddZeroClass.toZero, zero_add := ⋯, add_zero := ⋯,
      nsmul := fun z a => (NSMul.nsmul z a.1, NSMul.nsmul z a.2), nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.whiskerLeft_id_bimod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {X Y Z : CategoryTheory.Mon C} {M : Bimod X Y} {N : Bimod Y Z},
  M.whiskerLeft (CategoryTheory.CategoryStruct.id N) = CategoryTheory.CategoryStruct.id (M.tensorBimod N)
-- Mathlib.Algebra.Module.Equiv.Basic
Module.compHom.toLinearEquiv_symm_apply : ∀ {R : Type u_9} {S : Type u_10} [inst : Semiring R] [inst_1 : Semiring S] (g : R ≃+* S) (a : S),
  (Module.compHom.toLinearEquiv g).symm a = g.symm a
-- Init.Data.Array.GetLit
List.drop.eq_def : ∀ {α : Type u} (x : ℕ) (x_1 : List α),
  List.drop x x_1 =
    match x, x_1 with
    | 0, as => as
    | n.succ, [] => []
    | n.succ, head :: as => List.drop n as
-- Mathlib.Algebra.Order.Round
round_zero : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α], round 0 = 0
-- Mathlib.Analysis.LConvolution
MeasureTheory.lconvolution.eq_1 : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : Add G] [inst_1 : Neg G] (f g : G → ENNReal)
  (μ : MeasureTheory.Measure G) (x : G), MeasureTheory.lconvolution f g μ x = ∫⁻ (y : G), f y * g (-y + x) ∂μ
-- Mathlib.Order.Hom.Basic
OrderIso.prodComm_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β], OrderIso.prodComm.symm = OrderIso.prodComm
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.instPreservesMonomorphismsObjFunctorTypeSigmaConst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A : C) [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [CategoryTheory.Limits.MonoCoprod C], (CategoryTheory.Limits.sigmaConst.obj A).PreservesMonomorphisms
-- Mathlib.Algebra.Group.Equiv.Opposite
AddEquiv.neg'.eq_1 : ∀ (G : Type u_3) [inst : SubtractionMonoid G],
  AddEquiv.neg' G = { toEquiv := Equiv.trans (Equiv.neg G) AddOpposite.opEquiv, map_add' := ⋯ }
-- Mathlib.Analysis.Normed.Group.Defs
coe_le_enorm : ∀ {E : Type u_8} [inst : NNNorm E] {x : E} {r : NNReal}, ↑r ≤ ‖x‖ₑ ↔ r ≤ ‖x‖₊
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_finsetSum' : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Finset β)
  {f : β → α → ENNReal}, (∀ b ∈ s, AEMeasurable (f b) μ) → ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom_map : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] {X Y : J} (f : X ⟶ Y),
  (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂).map f =
    CategoryTheory.Enriched.FunctorCategory.precompEnrichedHom' V (CategoryTheory.Under.map f)
      (CategoryTheory.Iso.refl ((CategoryTheory.Under.map f).comp ((CategoryTheory.Under.forget X).comp F₁)))
      (CategoryTheory.Iso.refl ((CategoryTheory.Under.map f).comp ((CategoryTheory.Under.forget X).comp F₂)))
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- **Uniqueness of additive Haar measures**:
Two additive Haar measures which are probability measures coincide.  -/
MeasureTheory.Measure.isAddHaarMeasure_eq_of_isProbabilityMeasure : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] [μ.IsAddHaarMeasure]
  [μ'.IsAddHaarMeasure], μ' = μ
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.restrictVarLeft.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] {γ : Type u_2} (x : L.Term (α ⊕ γ))
  (x_1 : ↥x.varFinsetLeft → β),
  x.restrictVarLeft x_1 =
    match x, x_1 with
    | FirstOrder.Language.var (Sum.inl a), f => FirstOrder.Language.var (Sum.inl (f ⟨a, ⋯⟩))
    | FirstOrder.Language.var (Sum.inr a), _f => FirstOrder.Language.var (Sum.inr a)
    | FirstOrder.Language.func F ts, f =>
      FirstOrder.Language.func F fun i => (ts i).restrictVarLeft (f ∘ Set.inclusion ⋯)
-- Std.Data.HashMap.Basic
/-- Checks whether a key is present in a map, and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
Std.HashMap.containsThenInsert : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → β → Bool × Std.HashMap α β
-- Mathlib.Data.List.Forall2
List.forall₂_nil_right_iff : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l : List α}, List.Forall₂ R l [] ↔ l = []
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.AEEqFun.Integrable.smul : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {𝕜 : Type u_5} [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 β] [inst_3 : IsBoundedSMul 𝕜 β] {c : 𝕜} {f : α →ₘ[μ] β},
  f.Integrable → (c • f).Integrable
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.finite_quotient_of_finite_quotient_of_finite_quotient : ∀ {G : Type u} {X : Type v} [inst : AddGroup G] [inst_1 : AddAction G X] {H : AddSubgroup G}
  [Finite (AddAction.orbitRel.Quotient G X)] [Finite (G ⧸ H)], Finite (AddAction.orbitRel.Quotient (↥H) X)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.Scheme.Hom.quasiFiniteAt : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyQuasiFinite f] (x : ↥X),
  AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt f x
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
MonoidAlgebra.instIsPushout : ∀ {R : Type u_1} {M : Type u_2} {S : Type u_4} {A : Type u_5} {B : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring A] [inst_3 : CommSemiring B] [inst_4 : Algebra R S]
  [inst_5 : Algebra R A] [inst_6 : Algebra R B] [inst_7 : CommMonoid M] [inst_8 : Algebra S B] [inst_9 : Algebra A B]
  [inst_10 : IsScalarTower R A B] [inst_11 : IsScalarTower R S B] [Algebra.IsPushout R S A B],
  Algebra.IsPushout R S (MonoidAlgebra A M) (MonoidAlgebra B M)
-- Mathlib.CategoryTheory.Category.Preorder
/-- An `OrderHom` as a functor `X ⥤ Y` between preorder categories.  -/
OrderHom.toFunctor : {X : Type u} → {Y : Type v} → [inst : Preorder X] → [inst_1 : Preorder Y] → (X →o Y) → CategoryTheory.Functor X Y
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.FilterMap.PlausibleStep.skip : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α}
  {f : β → Std.Iterators.PostconditionT n (Option γ)} [inst : Std.Iterator α m β] {it : Std.IterM n γ}
  {it' : Std.IterM m β},
  it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it') →
    Std.Iterators.Types.FilterMap.PlausibleStep it
      (Std.IterStep.skip (Std.IterM.InternalCombinators.filterMap lift f it'))