mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.add_le_right : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.AddCommMonoid M] [Lean.Grind.OrderedAdd M]
  {a b : M} (c : M), a ≤ b → c + a ≤ c + b
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.face_map : ∀ {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup V₂] [inst_3 : Module k V] [inst_4 : Module k V₂] [inst_5 : AddTorsor V P]
  [inst_6 : AddTorsor V₂ P₂] {n : ℕ} (s : Affine.Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f)
  {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1), (s.map f hf).face h = (s.face h).map f hf
-- Mathlib.Topology.Algebra.Affine
/-- The line map is continuous.  -/
AffineMap.lineMap_continuous : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : AddCommGroup V] [inst_1 : TopologicalSpace V]
  [inst_2 : AddTorsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P] [inst_5 : Ring R]
  [inst_6 : Module R V] [inst_7 : TopologicalSpace R] [ContinuousSMul R V] {p q : P},
  Continuous ⇑(AffineMap.lineMap p q)
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.instMonoidHomClass : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B] [inst_3 : Star B],
  MonoidHomClass (A →⋆* B) A B
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.sub.injEq : ∀ (a b a_1 b_1 : Int.Internal.Linear.Expr), (a.sub b = a_1.sub b_1) = (a = a_1 ∧ b = b_1)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- This lemma exists for `aesop`, as `aesop` simplifies `-x * y` to `-(x * y)` before applying
unsafe rules like `mul_mem`, leading to a dead end in cases where `neg_mem` does not hold.  -/
neg_mul_mem : ∀ {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst_1 : HasDistribNeg R] [inst_2 : SetLike S R] [MulMemClass S R]
  {s : S} {x y : R}, -x ∈ s → y ∈ s → -(x * y) ∈ s
-- Lean.Meta.Match.Basic
Lean.Meta.Match.instInhabitedPattern : Inhabited Lean.Meta.Match.Pattern
-- Mathlib.Data.Seq.Computation
Computation.mem_of_get_eq : ∀ {α : Type u} (s : Computation α) [h : s.Terminates] {a : α}, s.get = a → a ∈ s
-- Mathlib.Order.Hom.Basic
/-- Transport an `OrderEmbedding` across a pair of `OrderIso`s, by pre- and post-composition.

This is `Equiv.embeddingCongr`/`RelIso.relEmbeddingCongr` for `OrderEmbedding`.  -/
OrderIso.orderEmbeddingCongr : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      {δ : Type u_5} →
        [inst : LE α] → [inst_1 : LE β] → [inst_2 : LE γ] → [inst_3 : LE δ] → α ≃o γ → β ≃o δ → α ↪o β ≃ (γ ↪o δ)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.Functor.Braided.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {D : Type u₂} {inst_3 : CategoryTheory.Category.{v₂, u₂} D}
  {inst_4 : CategoryTheory.MonoidalCategory D} {inst_5 : CategoryTheory.BraidedCategory D}
  {F : CategoryTheory.Functor C D} {x y : F.Braided},
  x = y ↔
    CategoryTheory.Functor.LaxMonoidal.ε F = CategoryTheory.Functor.LaxMonoidal.ε F ∧
      CategoryTheory.Functor.LaxMonoidal.μ F = CategoryTheory.Functor.LaxMonoidal.μ F ∧
        CategoryTheory.Functor.OplaxMonoidal.η F = CategoryTheory.Functor.OplaxMonoidal.η F ∧
          CategoryTheory.Functor.OplaxMonoidal.δ F = CategoryTheory.Functor.OplaxMonoidal.δ F
-- Std.Sat.AIG.CNF
/-- Add the CNF for a `Decl.false` to the state.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.addFalse : {aig : Std.Sat.AIG ℕ} →
  (state : Std.Sat.AIG.toCNF.State✝ aig) →
    (idx : ℕ) →
      (h : idx < aig.decls.size) →
        aig.decls[idx] = Std.Sat.AIG.Decl.false → { out // Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state out idx h }
-- Init.Data.Int.Gcd
Int.neg_gcd : ∀ {a b : ℤ}, (-a).gcd b = a.gcd b
-- Aesop.Tree.TreeM
Aesop.getAndIncrementNextRappId : Aesop.TreeM Aesop.RappId
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.box_injective : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n], Function.Injective fun ν => BoxIntegral.unitPartition.box n ν
-- Mathlib.Analysis.Convex.Function
/-- Left translation preserves strict convexity.  -/
StrictConvexOn.translate_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCancelCommMonoid E] [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E]
  [inst_6 : SMul 𝕜 β] {s : Set E} {f : E → β},
  StrictConvexOn 𝕜 s f → ∀ (c : E), StrictConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.uliftNatTransOfLe_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S T : CategoryTheory.Sieve X} (h : S ≤ T)
  (x : Cᵒᵖ), (CategoryTheory.Sieve.uliftNatTransOfLe h).app x = TypeCat.ofHom fun f => { down := ⟨↑f.down, ⋯⟩ }
-- Mathlib.Order.CompleteLattice.Defs
lt_iSup_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLinearOrder α] {a : α} {f : ι → α}, a < iSup f ↔ ∃ i, a < f i
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.omega_mul_algebraMap_mul_mk : ∀ {R : Type u_2} {a b : R} [inst : CommSemiring R] (n x y : R),
  QuadraticAlgebra.omega * (algebraMap R (QuadraticAlgebra R a b)) n * { re := x, im := y } =
    { re := a * n * y, im := n * x + n * b * y }
-- Mathlib.Algebra.DirectSum.Internal
SetLike.intCast_mem_graded : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : Zero ι] [inst_1 : AddGroupWithOne R] [inst_2 : SetLike σ R]
  [AddSubgroupClass σ R] (A : ι → σ) [SetLike.GradedOne A] (z : ℤ), ↑z ∈ A 0
-- Mathlib.Algebra.Group.Commute.Units
AddCommute.addUnits_neg_right_iff : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M}, AddCommute a ↑(-u) ↔ AddCommute a ↑u
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.instInhabited : (C : Type u) → [inst : CategoryTheory.CategoryStruct.{v, u} C] → Inhabited (CategoryTheory.MorphismProperty C)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isBoundary₂_of_mem_boundaries₂ : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A],
  ∀ x ∈ groupHomology.boundaries₂ (Rep.ofDistribMulAction k G A), groupHomology.IsBoundary₂ x
-- Mathlib.Probability.Notation
/-- `P⟦s | m⟧` is the conditional expectation of `s` with respect to `m` under measure `P`.  -/
ProbabilityTheory.«term_⟦_|_⟧» : Lean.TrailingParserDescr
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.prod_coe_symm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv γ δ),
  ↑(e.prod e').symm = fun p => (↑e.symm p.1, ↑e'.symm p.2)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Algebra.finite_of_essFiniteType_of_isAlgebraic : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.EssFiniteType F E]
  [Algebra.IsAlgebraic F E], Module.Finite F E
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.locallyRingedSpaceMap_id : ∀ (R : CommRingCat),
  AlgebraicGeometry.Spec.locallyRingedSpaceMap (CategoryTheory.CategoryStruct.id R) =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec.locallyRingedSpaceObj R)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.zero : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] → [inst_1 : SeminormedAddCommGroup V₂] → Zero (NormedAddGroupHom V₁ V₂)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.restrictAppIso_inv_map : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules)
  {U V : X.Opens} (hUV : Opposite.op V ⟶ Opposite.op U),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M V).inv
      ((M.restrict f).presheaf.map hUV) =
    CategoryTheory.CategoryStruct.comp (M.presheaf.map (CategoryTheory.homOfLE ⋯).op)
      (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).inv
-- Mathlib.Data.Nat.Factorial.Basic
Nat.zero_ascFactorial : ∀ (k : ℕ), Nat.ascFactorial 0 k.succ = 0
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.instFullExactFunctorWhiskeringLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] (E : Type u'') [inst_4 : CategoryTheory.Category.{v'', u''} E]
  [inst_5 : CategoryTheory.Abelian E] [inst_6 : L.IsLocalization P.isoModSerre] [inst_7 : CategoryTheory.Preadditive D]
  [inst_8 : L.Additive], (CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft L P E).Full
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
/-- If `ω` is a closed `1`-form on a convex set,
then `∫ᶜ x in Path.segment a b, ω x + ∫ᶜ x in Path.segment b c, ω x = ∫ᶜ x in Path.segment a c, ω x`
for all `a b c ∈ s`.

This is the key lemma used to establish that closed a `1`-form on  a convex set
has a primitive.
 -/
Convex.curveIntegral_segment_add_eq_of_hasFDerivWithinAt_symmetric : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedSpace ℝ E]
  [inst_6 : NormedSpace ℝ F] {a b c : E} {s : Set E} {ω : E → E →L[𝕜] F} {dω : E → E →L[ℝ] E →L[𝕜] F},
  Convex ℝ s →
    (∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x) →
      (∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x) →
        a ∈ s →
          b ∈ s →
            c ∈ s →
              ∫ᶜ (x : E) in Path.segment a b, ω x + ∫ᶜ (x : E) in Path.segment b c, ω x =
                ∫ᶜ (x : E) in Path.segment a c, ω x
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- The identity affine isometry.  -/
AffineIsometry.id : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {P : Type u_10} →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : NormedSpace 𝕜 V] → [inst_3 : PseudoMetricSpace P] → [inst_4 : NormedAddTorsor V P] → P →ᵃⁱ[𝕜] P
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.unit_rightAdjointUniq_hom : ∀ {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 : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F ⊣ G'),
  CategoryTheory.CategoryStruct.comp adj1.unit (F.whiskerLeft (adj1.rightAdjointUniq adj2).hom) = adj2.unit
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_of_contains_map : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α},
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.map f m).contains k = true → m.contains k = true
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- A morphism of monoid objects induces a "restriction" or "comap" functor
between the categories of module objects.
 -/
CategoryTheory.Mod.comap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A B : C} →
              [inst_4 : CategoryTheory.MonObj A] →
                [inst_5 : CategoryTheory.MonObj B] →
                  (f : A ⟶ B) →
                    [CategoryTheory.IsMonHom f] →
                      CategoryTheory.Functor (CategoryTheory.Mod D B) (CategoryTheory.Mod D A)
-- Mathlib.Order.RelIso.Basic
RelEmbedding.isWellOrder : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (x : r ↪r s) [IsWellOrder β s], IsWellOrder α r
-- Std.Async.Process
/-- Number of minor (soft) page faults (no disk I/O)
 -/
Std.IO.Process.ResourceUsageStats.minorPageFaults : Std.IO.Process.ResourceUsageStats → UInt64
-- Mathlib.Topology.Order.LeftRightNhds
/-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `(l, a)`
with `l < a`, provided `a` is not a bottom element.  -/
mem_nhdsLT_iff_exists_Ioo_subset' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a l' : α} {s : Set α},
  l' < a → (s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Iio a, Set.Ioo l a ⊆ s)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasStrictFDerivAt_pi'' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {ι : Type u_6} {F' : ι → Type u_7} [inst_3 : (i : ι) → NormedAddCommGroup (F' i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} {Φ' : E →L[𝕜] (i : ι) → F' i},
  (∀ (i : ι), HasStrictFDerivAt (fun x => Φ x i) (ContinuousLinearMap.proj i ∘SL Φ') x) → HasStrictFDerivAt Φ Φ' x
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
/-- A groupoid `G` is free when we have the following data:
- a quiver on `IsFreeGroupoid.Generators G` (a type synonym for `G`)
- a function `of` taking a generating arrow to a morphism in `G`
- such that a functor from `G` to any group `X` is uniquely determined
  by assigning labels in `X` to the generating arrows.

This definition is nonstandard. Normally one would require that functors `G ⥤ X`
to any _groupoid_ `X` are given by graph homomorphisms from `generators`.  -/
IsFreeGroupoid : (G : Type u_1) → [CategoryTheory.Groupoid G] → Type (max u_1 (v + 1))
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.bayesRisk_of_isEmpty' : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ}
  [Nonempty 𝓧] [IsEmpty 𝓨], ProbabilityTheory.bayesRisk ℓ P π = ⊤
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.contains_insertManyIfNewUnit_emptyWithCapacity_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).contains k =
    l.contains k
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.Nil.dropLast : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w}, p.Nil → p.dropLast.Nil
-- Lean.Environment
Lean.ImportM.Context : Type
-- Init.Data.ByteArray.Basic
ByteArray.instInhabitedIterator : Inhabited ByteArray.Iterator
-- Init.Data.List.Erase
_private.Init.Data.List.Erase.0.List.eraseP_filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → ((y : β) → motive (some y)) → (Unit → motive none) → motive x
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.zsmul_mem : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {x : R}, x ∈ s → ∀ (n : ℤ), n • x ∈ s
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.toSheafify_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q),
  CategoryTheory.CategoryStruct.comp η (J.toSheafify Q) =
    CategoryTheory.CategoryStruct.comp (J.toSheafify P) (J.sheafifyMap η)
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.moebius_eq_or : ∀ (n : ℕ), ArithmeticFunction.moebius n = 0 ∨ ArithmeticFunction.moebius n = 1 ∨ ArithmeticFunction.moebius n = -1
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W W_1 : CategoryTheory.MorphismProperty C),
  W = W_1 →
    ∀ (J : Type w) [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J]
      ⦃X Y : C⦄ (x x_1 : X ⟶ Y),
      x = x_1 → W.transfiniteCompositionsOfShape J x = W_1.transfiniteCompositionsOfShape J x_1
-- Init.Data.AC
Lean.Data.AC.eval.eq_def : ∀ {α : Sort u_1} (β : Sort u) [inst : Lean.Data.AC.EvalInformation α β] (ctx : α) (x : Lean.Data.AC.Expr),
  Lean.Data.AC.eval β ctx x =
    match x with
    | Lean.Data.AC.Expr.var idx => Lean.Data.AC.EvalInformation.evalVar ctx idx
    | l.op r => Lean.Data.AC.EvalInformation.evalOp ctx (Lean.Data.AC.eval β ctx l) (Lean.Data.AC.eval β ctx r)
-- Mathlib.Lean.Expr.Basic
Lean.Expr.modifyRevArg : (Lean.Expr → Lean.Expr) → ℕ → Lean.Expr → Lean.Expr
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instReprOrdinal : Repr Std.Time.Millisecond.Ordinal
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.symm_mem_dilatransvections_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {e : V ≃ₗ[R] V},
  e.symm ∈ LinearEquiv.dilatransvections R V ↔ e ∈ LinearEquiv.dilatransvections R V
-- Mathlib.Algebra.Order.Archimedean.Basic
exists_rat_btwn : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K},
  x < y → ∃ q, x < ↑q ∧ ↑q < y
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- additive version of `MeasureTheory.Measure.haar.prehaar`  -/
MeasureTheory.Measure.haar.addPrehaar : {G : Type u_1} → [AddGroup G] → [inst : TopologicalSpace G] → Set G → Set G → TopologicalSpace.Compacts G → ℝ
-- Init.Data.Nat.ToString
Nat.reprPrec_eq_repr : ∀ {n i : ℕ}, reprPrec n i = Std.Format.text n.repr
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGE?_eq_getEntryGE?ₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getEntryGE? k t = Std.DTreeMap.Internal.Impl.getEntryGE?ₘ k t
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- The same-universe version of `lift_rank_le_of_surjective_injective`.  -/
rank_le_of_surjective_injective : ∀ {R : Type u} {R' : Type u'} {M M₁ : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring R'] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R' M₁] (i : R → R') (j : M →+ M₁),
  Function.Surjective i →
    Function.Injective ⇑j → (∀ (r : R) (m : M), j (r • m) = i r • j m) → Module.rank R M ≤ Module.rank R' M₁
-- Mathlib.Algebra.Group.Finsupp
Finsupp.erase_neg : ∀ {ι : Type u_1} {G : Type u_6} [inst : AddGroup G] (a : ι) (f : ι →₀ G), Finsupp.erase a (-f) = -Finsupp.erase a f
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.functorToCore_comp_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : Type u₂} [inst_1 : CategoryTheory.Groupoid G]
  {G' : Type u₃} [inst_2 : CategoryTheory.Groupoid G'] (H : CategoryTheory.Functor G C)
  (F : CategoryTheory.Functor G' G),
  CategoryTheory.Core.functorToCore (F.comp H) = F.comp (CategoryTheory.Core.functorToCore H)
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasProd_of_isLUB_of_one_le : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommMonoid α] [inst_1 : LinearOrder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderTopology α] {f : ι → α} (i : α),
  (∀ (i : ι), 1 ≤ f i) → IsLUB (Set.range fun s => ∏ i ∈ s, f i) i → HasProd f i
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.zero_power : ∀ {a : Cardinal.{u_1}}, a ≠ 0 → 0 ^ a = 0
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.coprod.inr_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.coprod.fst X Y) = 0
-- Mathlib.Data.Real.Basic
Real.instSub : Sub ℝ
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- The quotient of a finitely presented group by a subgroup
which is finitely generated as a normal subgroup is finitely presented.  -/
Group.IsFinitelyPresented.quotient : ∀ {G : Type u_1} [inst : Group G] [hG : Group.IsFinitelyPresented G] (N : Subgroup G) [inst_1 : N.Normal],
  N.IsFinitelyNormallyGenerated → Group.IsFinitelyPresented (G ⧸ N)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeGroup.lift_of : ∀ {G : Type u_1} [inst : Group G] [inst_1 : IsFreeGroup G] {H : Type u_2} [inst_2 : Group H]
  (f : IsFreeGroup.Generators G → H) (a : IsFreeGroup.Generators G), (IsFreeGroup.lift f) (IsFreeGroup.of a) = f a
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.mkArrowIso_hom_hom_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (f : CategoryTheory.MonoOver X),
  f.mkArrowIso.hom.hom.left = CategoryTheory.CategoryStruct.id f.obj.left
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.toAddSubgroup_top : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R], ⊤.toAddSubgroup = ⊤
-- Mathlib.Algebra.Order.Floor.Div
/-- Flooring division. If `a > 0`, then `b ⌊/⌋ a` is the greatest `c` such that `a • c ≤ b`.  -/
«term_⌊/⌋_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Algebra.Order.Field
/-- In a linearly ordered field with the order topology, if `f` tends to `Filter.atBot` and `g`
tends to a positive constant `C` then `f * g` tends to `Filter.atBot`.  -/
Filter.Tendsto.atBot_mul_pos : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜},
  0 < C →
    Filter.Tendsto f l Filter.atBot → Filter.Tendsto g l (nhds C) → Filter.Tendsto (fun x => f x * g x) l Filter.atBot
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_Ixx : ∀ {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_4} [inst : LinearOrder α] {Ixx : α → α → Set α} {p : α → α → Prop},
  (∀ {a b : α}, (Ixx a b).Nonempty → p a b) →
    (∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)) →
      ∀ (f : ι → α) (g : ι' → α), IsPiSystem {S | ∃ i j, p (f i) (g j) ∧ Ixx (f i) (g j) = S}
-- Mathlib.Analysis.Normed.Field.Basic
/-- The norm on a normed division ring is strictly multiplicative.  -/
NormedDivisionRing.toNormMulClass : ∀ {α : Type u_2} [inst : NormedDivisionRing α], NormMulClass α
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.Gate.and.sizeOf_spec : sizeOf Std.Tactic.BVDecide.Gate.and = 1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.imp_keqC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.CommRing α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  [Lean.Grind.NoNatZeroDivisors α] (k : ℤ) (lhs rhs : Lean.Grind.CommRing.Expr) (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.imp_keq_certC lhs rhs k p₁ p₂ c = true →
    ↑k * Lean.Grind.CommRing.Poly.denote ctx p₁ = Lean.Grind.CommRing.Poly.denote ctx p₂ →
      Lean.Grind.CommRing.Expr.denote ctx lhs = Lean.Grind.CommRing.Expr.denote ctx rhs
-- Mathlib.Topology.Order.LeftRightNhds
/-- If `S` is order-connected and contains two points `x < y`,
then `S` is a right neighbourhood of `x`.  -/
Set.OrdConnected.mem_nhdsGE : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {S : Set α} {x y : α},
  S.OrdConnected → x ∈ S → y ∈ S → x < y → S ∈ nhdsWithin x (Set.Ici x)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.toCycles_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology] (φ : S₁ ⟶ S₂)
  {Z : C} (h : S₂.cycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp S₁.toCycles
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) h) =
    CategoryTheory.CategoryStruct.comp φ.τ₁ (CategoryTheory.CategoryStruct.comp S₂.toCycles h)