mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_inter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)], (m₁ ∩ m₂).get! k = if k ∈ m₂ then m₁.get! k else default
-- Init.Prelude
SeqRight.mk : {f : Type u → Type v} → ({α β : Type u} → f α → (Unit → f β) → f β) → SeqRight f
-- Mathlib.Data.Int.Order.Units
Int.units_sq : ∀ (u : ℤˣ), u ^ 2 = 1
-- Lean.Compiler.IR.Basic
Lean.IR.Decl.extern.sizeOf_spec : ∀ (f : Lean.IR.FunId) (xs : Array Lean.IR.Param) (type : Lean.IR.IRType) (ext : Lean.ExternAttrData),
  sizeOf (Lean.IR.Decl.extern f xs type ext) = 1 + sizeOf f + sizeOf xs + sizeOf type + sizeOf ext
-- Mathlib.Data.Finmap
Finmap.keys_ext : ∀ {α : Type u} {β : α → Type v} {s₁ s₂ : AList β}, s₁.toFinmap.keys = s₂.toFinmap.keys ↔ s₁.keys.Perm s₂.keys
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.map_smul : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E], IsQuotientCoveringMap f G → ∀ (g : G) {e : E}, f (g • e) = f e
-- Mathlib.Topology.Algebra.UniformMulAction
uniformContinuous_div_const' : ∀ {R : Type u_3} [inst : DivisionRing R] [inst_1 : UniformSpace R] [UniformContinuousConstSMul Rᵐᵒᵖ R] (a : R),
  UniformContinuous fun b => b / a
-- Mathlib.Algebra.Field.Defs
/-- The inverse of `0` in a group with zero is `0`.  -/
Semifield.inv_zero : ∀ {K : Type u_2} [self : Semifield K], 0⁻¹ = 0
-- Mathlib.NumberTheory.BernoulliPolynomials
Polynomial.coeff_bernoulli : ∀ (n i : ℕ), (Polynomial.bernoulli n).coeff i = if i ≤ n then bernoulli (n - i) * ↑(n.choose i) else 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.coe_add : ∀ (x y : ℝ), ↑(x + y) = ↑x + ↑y
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.localized₀_smul : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (p : Submonoid R) (f : M →ₗ[R] N)
  [inst_5 : IsLocalizedModule p f] (M' : Submodule R M) (I : Submodule R R),
  Submodule.localized₀ p f (I • M') = I • Submodule.localized₀ p f M'
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBiconeMorphism.ext_iff : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {c c' : CategoryTheory.Limits.BinaryBicone P Q} {f g : c ⟶ c'}, f = g ↔ f.hom = g.hom
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The continuous homomorphism given by inclusion of the second factor.  -/
ContinuousAddMonoidHom.inr : (A : Type u_2) →
  (B : Type u_3) →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → B →ₜ+ A × B
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.StructuredArrow.hasLimit : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {X : T} {G : CategoryTheory.Functor A T}
  (F : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X G))
  [i₁ : CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.StructuredArrow.proj X G))]
  [i₂ : CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.StructuredArrow.proj X G)) G],
  CategoryTheory.Limits.HasLimit F
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  DiffContOnCl 𝕜 f s → DiffContOnCl 𝕜 g s → DiffContOnCl 𝕜 (f - g) s
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- An injective presentation of an object `X` consists of a monomorphism `f : X ⟶ J`
to some injective object `J`.
 -/
CategoryTheory.InjectivePresentation.injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (self : CategoryTheory.InjectivePresentation X),
  CategoryTheory.Injective self.J
-- Init.Omega.Int
Lean.Omega.Fin.ne_iff_lt_or_gt : ∀ {n : ℕ} {i j : Fin n}, i ≠ j ↔ i < j ∨ i > j
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.revSkip?_eq_none_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice} {pos : s.Pos}, pos.revSkip? pat = none ↔ ¬String.Slice.Pattern.Model.RevMatchesAt pat pos
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionIdentifier.fvar.sizeOf_spec : ∀ (id : Lean.FVarId), sizeOf (Lean.Lsp.CompletionIdentifier.fvar id) = 1 + sizeOf id
-- Init.Data.Option.Basic
Option.min_none_left : ∀ {α : Type u_1} [inst : Min α] {o : Option α}, none ⊓ o = none
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- Two sets are at zero Hausdorff edistance if and only if they have the same closure.  -/
Metric.hausdorffEDist_zero_iff_closure_eq_closure : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α}, Metric.hausdorffEDist s t = 0 ↔ closure s = closure t
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.cons_vecMulVec : ∀ {α : Type u} {m : ℕ} {n' : Type uₙ} [inst : NonUnitalNonAssocSemiring α] (x : α) (v : Fin m → α) (w : n' → α),
  Matrix.vecMulVec (Matrix.vecCons x v) w = Matrix.vecCons (x • w) (Matrix.vecMulVec v w)
-- Mathlib.Probability.Decision.Risk.Basic
ProbabilityTheory.bayesRisk_discard : ∀ {Θ : Type u_1} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal},
  Measurable (Function.uncurry ℓ) →
    ∀ (π : MeasureTheory.Measure Θ) [MeasureTheory.SFinite π],
      ProbabilityTheory.bayesRisk ℓ (ProbabilityTheory.Kernel.discard Θ) π = ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂π
-- Mathlib.GroupTheory.Abelianization.Defs
Abelianization.map_id : ∀ {G : Type u} [inst : Group G], Abelianization.map (MonoidHom.id G) = MonoidHom.id (Abelianization G)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.IsTotallyReal.mult_eq : ∀ {K : Type u_2} [inst : Field K] [NumberField.IsTotallyReal K] (w : NumberField.InfinitePlace K), w.mult = 1
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.unop_bot : ∀ {M : Type u_2} [inst : MulOneClass M], ⊥.unop = ⊥
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_eq : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [inst_3 : X₁.HasTensor X₂]
  [inst_4 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j)
  (i₁₂ : I) (h' : i₁ + i₂ = i₁₂),
  CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ i₁₂ h') (X₃ i₃))
      (CategoryTheory.GradedObject.Monoidal.ιTensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ i₁₂ i₃
        j ⋯)
-- Init.Data.List.Lemmas
List.eq_getElem_of_length_eq_one : ∀ {α : Type u_1} (l : List α) (hl : l.length = 1), l = [l[0]]
-- Mathlib.Topology.Category.TopCat.OpenNhds
/-- An open map `f : X ⟶ Y` induces a functor `OpenNhds x ⥤ OpenNhds (f x)`.  -/
IsOpenMap.functorNhds : {X Y : TopCat} →
  {f : X ⟶ Y} →
    IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f) →
      (x : ↑X) →
        CategoryTheory.Functor (TopologicalSpace.OpenNhds x)
          (TopologicalSpace.OpenNhds ((CategoryTheory.ConcreteCategory.hom f) x))
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
/-- **Alias** of the reverse direction of `Complex.arg_mul_eq_add_arg_iff`. -/
Complex.arg_mul : ∀ {x y : ℂ}, x ≠ 0 → y ≠ 0 → x.arg + y.arg ∈ Set.Ioc (-Real.pi) Real.pi → (x * y).arg = x.arg + y.arg
-- Init.Data.BitVec.Lemmas
BitVec.sdiv_neg_one : ∀ {w : ℕ} {x : BitVec w}, x.toInt / -1 = -x.toInt
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_smul_le : ∀ {R : Type u} {S : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : DistribMulAction R S] (a : R) (f : MvPolynomial σ S), (a • f).totalDegree ≤ f.totalDegree
-- Mathlib.CategoryTheory.MorphismProperty.Concrete
/-- Bijectivity (in a concrete category) as a `MorphismProperty`  -/
CategoryTheory.MorphismProperty.bijective : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type u_2} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [CategoryTheory.ConcreteCategory C FC] → CategoryTheory.MorphismProperty C
-- Mathlib.Analysis.Calculus.AddTorsor.AffineMap
/-- `AffineMap.lineMap` is smooth as a function `𝕜 → V`.  -/
AffineMap.contDiff_lineMap : ∀ {𝕜 : Type u_1} {V : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] (p₀ p₁ : V) {n : WithTop ℕ∞}, ContDiff 𝕜 n ⇑(AffineMap.lineMap p₀ p₁)
-- Mathlib.Algebra.Order.Module.Defs
/-- Binary strict **rearrangement inequality**.  -/
smul_add_smul_lt_smul_add_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_7 : Module α β]
  [PosSMulStrictMono α β] {a₁ a₂ : α} {b₁ b₂ : β}, a₁ < a₂ → b₁ < b₂ → a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₁₀ArrowIso_inv_left : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupHomology.d₁₀ArrowIso A).inv.left = (groupHomology.chainsIso₁ A).inv
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_preimage_smul_null : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : SMul G α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.SMulInvariantMeasure G α μ] {s : Set α}, μ s = 0 → ∀ (c : G), μ ((fun x => c • x) ⁻¹' s) = 0
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.comp_id : ∀ {γ : Type w} {δ : Type u_2} [inst : TopologicalSpace γ] [inst_1 : TopologicalSpace δ] [inst_2 : Zero δ]
  (f : ZeroAtInftyContinuousMap γ δ), f.comp (CocompactMap.id γ) = f
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- Suppose `a : X → Set A` is continuous on `t : Set X` and `a x` satisfies the predicate `p` for
all `x ∈ t`. Suppose further that `s : X → Set 𝕜` is a family of sets with `s x` compact when
`x ∈ t` such that `s x₀` contains the spectrum of `a x` for all sufficiently close `x ∈ t`.
If `f : 𝕜 → 𝕜` is continuous on `s x` for each `x ∈ t`, and `f 0 = 0` then `fun x ↦ cfcₙ f (a x)`
is continuous on `t`.  -/
ContinuousOn.cfcₙ : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [ContinuousStar A] [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [inst_8 : TopologicalSpace X]
  {s : X → Set 𝕜} (f : 𝕜 → 𝕜) {a : X → A} {t : Set X},
  (∀ x ∈ t, IsCompact (s x)) →
    ContinuousOn a t →
      (∀ x₀ ∈ t, ∀ᶠ (x : X) in nhdsWithin x₀ t, quasispectrum 𝕜 (a x) ⊆ s x₀) →
        (∀ x ∈ t, p (a x)) →
          autoParam (∀ x ∈ t, ContinuousOn f (s x)) ContinuousOn.cfcₙ._auto_1 →
            autoParam (f 0 = 0) ContinuousOn.cfcₙ._auto_3 → ContinuousOn (fun x => cfcₙ f (a x)) t
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.withDensityᵥ_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : α → E},
  MeasureTheory.Integrable f μ → ∀ {s : Set α}, MeasurableSet s → (μ.withDensityᵥ f) s = ∫ (x : α) in s, f x ∂μ
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.linearEquivOfLeftInverse_symm_apply : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : Module.Invertible R M] [inst_6 : Module.Invertible R N]
  {f : M →ₗ[R] N} {g : N →ₗ[R] M} (hfg : Function.LeftInverse ⇑f ⇑g) (x : N),
  (Module.Invertible.linearEquivOfLeftInverse hfg).symm x = g x
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmuller₀_mapMonoidHom_idealQuotientMk : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R] {x : Perfection R p},
  (Perfection.teichmuller₀ p I) ((Perfection.mapMonoidHom p ↑(Ideal.Quotient.mk I)) x) =
    (Perfection.coeffMonoidHom R p 0) x
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.funCC.injEq : ∀ (declName declName_1 : Lean.Name),
  (Lean.Meta.Grind.Entry.funCC declName = Lean.Meta.Grind.Entry.funCC declName_1) = (declName = declName_1)
-- Mathlib.Combinatorics.Graph.Delete
Graph.edgeSet_deleteVerts : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α),
  (G.deleteVerts X).edgeSet = {e | ∃ x y, G.IsLink e x y ∧ x ∉ X ∧ y ∉ X}
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.det_toSquareBlock_id : ∀ {m : Type u_3} {R : Type v} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m] (M : Matrix m m R)
  (i : m), (M.toSquareBlock id i).det = M i i
-- Mathlib.Data.List.ToFinsupp
List.toFinsupp.congr_simp : ∀ {M : Type u_1} [inst : Zero M] (l l_1 : List M),
  l = l_1 →
    ∀ {inst_1 : DecidablePred fun x => l.getD x 0 ≠ 0} [inst_2 : DecidablePred fun x => l_1.getD x 0 ≠ 0],
      l.toFinsupp = l_1.toFinsupp
-- Mathlib.Order.OmegaCompletePartialOrder
/-- A monotone function on `ω`-continuous partial orders is said to be continuous
if for every chain `c : chain α`, `f (⊔ i, c i) = ⊔ i, f (c i)`.
This is just the bundled version of `OrderHom.continuous`.  -/
OmegaCompletePartialOrder.ContinuousHom : (α : Type u_2) → (β : Type u_3) → [OmegaCompletePartialOrder α] → [OmegaCompletePartialOrder β] → Type (max u_2 u_3)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
/-- The integral of the conditional expectation `condExpL1` over an `m`-measurable set is equal to
the integral of `f` on that set. See also `setIntegral_condExp`, the similar statement for
`condExp`.  -/
MeasureTheory.setIntegral_condExpL1 : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] {f : α → F'} {s : Set α}
  [CompleteSpace F'],
  MeasureTheory.Integrable f μ →
    MeasurableSet s → ∫ (x : α) in s, ↑↑(MeasureTheory.condExpL1 hm μ f) x ∂μ = ∫ (x : α) in s, f x ∂μ
-- Mathlib.GroupTheory.GroupAction.Defs
/-- Decomposition of a type `X` as a disjoint union of its orbits under an additive group action.

This version is expressed in terms of `AddAction.orbitRel.Quotient.orbit` instead of
`AddAction.orbit`, to avoid mentioning `Quotient.out`.  -/
AddAction.selfEquivSigmaOrbits' : (G : Type u_1) →
  (α : Type u_2) → [inst : AddGroup G] → [inst_1 : AddAction G α] → α ≃ (ω : AddAction.orbitRel.Quotient G α) × ↑ω.orbit
-- Mathlib.Tactic.Linter.OldObtain
/-- Whether a syntax element is an `obtain` tactic call without a provided proof.  -/
_private.Mathlib.Tactic.Linter.OldObtain.0.Mathlib.Linter.Style.isObtainWithoutProof : Lean.Syntax → Bool
-- Mathlib.Topology.MetricSpace.Bounded
/-- The distance between two points in a set is controlled by the diameter of the set.  -/
Metric.dist_le_diam_of_mem : ∀ {α : Type u} {s : Set α} {x y : α} [inst : PseudoMetricSpace α],
  Bornology.IsBounded s → x ∈ s → y ∈ s → dist x y ≤ Metric.diam s
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.coe_tensorObj : ∀ {R : Type u} [inst : CommRing R] (A B : CommAlgCat R),
  ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj A B) = TensorProduct R ↑A ↑B
-- Mathlib.Data.Nat.Factorization.Basic
/-- The only prime factor of prime `p` is `p` itself.  -/
Nat.Prime.eq_of_factorization_pos : ∀ {p q : ℕ}, Nat.Prime p → p.factorization q ≠ 0 → p = q
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.sInf_of_not_bddBelow : ∀ {α : Type u_1} [inst : LE α] [inst_1 : InfSet α] {s : Set (WithBot α)}, ¬BddBelow (WithBot.some ⁻¹' s) → sInf s = ⊥
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Int.Internal.Linear.Poly.pp : Int.Internal.Linear.Poly → Lean.Meta.Grind.GoalM Lean.MessageData
-- Init.Data.List.SplitOn.Basic
_private.Init.Data.List.SplitOn.Basic.0.List.splitOnPPrepend.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (x : List α), List.splitOnPPrepend p [] x = [x.reverse]
-- Mathlib.Algebra.Homology.SingleHomology
CochainComplex.exactAt_succ_single_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (A : C) (n : ℕ),
  HomologicalComplex.ExactAt ((CochainComplex.single₀ C).obj A) (n + 1)
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.addOppositeEquiv_symm_orderTop : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] (x : (HahnSeries Γ R)ᵃᵒᵖ),
  (HahnSeries.addOppositeEquiv.symm x).orderTop = (AddOpposite.unop x).orderTop
-- Mathlib.Data.Matrix.Reflection
Matrix.vecMulᵣ.eq_1 : ∀ {l m : ℕ} {α : Type u_1} [inst : Mul α] [inst_1 : Add α] [inst_2 : Zero α] (v : Fin l → α)
  (A : Matrix (Fin l) (Fin m) α), Matrix.vecMulᵣ v A = FinVec.map (fun a => Matrix.dotProductᵣ v a) A.transpose
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n). Map a function across a tree, without changing the structure. Only valid when
the function is strictly monotone, i.e. `x < y → f x < f y`.

```
partition (fun x ↦ x + 2) {1, 2, 4} = {2, 3, 6}
partition (fun x : ℕ ↦ x - 2) {1, 2, 4} = precondition violation
```  -/
Ordnode.map : {α : Type u_1} → {β : Type u_2} → (α → β) → Ordnode α → Ordnode β
-- Lean.Message
Lean.MessageData.nest.sizeOf_spec : ∀ (a : ℕ) (a_1 : Lean.MessageData), sizeOf (Lean.MessageData.nest a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TotallyBounded.inv : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {s : Set α},
  TotallyBounded s → TotallyBounded s⁻¹
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.coe_ofSubtype : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α) (k : ↥(alternatingGroup ↥s)),
  ↑((alternatingGroup.ofSubtype s) k) = Equiv.Perm.ofSubtype ↑k
-- Mathlib.LinearAlgebra.Matrix.Bilinear
/-- A version of `LinearMap.mulRight` for matrix multiplication.  -/
mulRightLinearMap : (l : Type u_1) →
  {m : Type u_2} →
    {n : Type u_3} →
      (R : Type u_5) →
        {A : Type u_6} →
          [Fintype m] →
            [inst : Semiring R] →
              [inst_1 : NonUnitalNonAssocSemiring A] →
                [inst_2 : Module R A] → [IsScalarTower R A A] → Matrix m n A → Matrix l m A →ₗ[R] Matrix l n A
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.map_mono : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b ⟶ g b)
  [∀ (i : β), CategoryTheory.Mono (p i)], CategoryTheory.Mono (CategoryTheory.Limits.Pi.map p)
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNegAssignment.eq_2 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg.addNegAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.map.congr_simp : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A : Type u_2)
  (B : Type u_3) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra A B]
  [inst_7 : Algebra S B] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : SMulCommClass S A B], KaehlerDifferential.map R S A B = KaehlerDifferential.map R S A B
-- Mathlib.RingTheory.RingHom.FinitePresentation
/-- Being finitely-presented is preserved by localizations.  -/
RingHom.finitePresentation_localizationPreserves : RingHom.LocalizationPreserves @RingHom.FinitePresentation
-- Init.Data.Sum.Basic
Sum.not_liftRel_inl_inr : ∀ {α : Type u_1} {γ : Type u_2} {r : α → γ → Prop} {β : Type u_3} {δ : Type u_4} {s : β → δ → Prop} {a : α} {d : δ},
  ¬Sum.LiftRel r s (Sum.inl a) (Sum.inr d)
-- Mathlib.Tactic.Simps.NotationClass
Simps.AutomaticProjectionData.mk.injEq : ∀ (className : Lean.Name) (isNotation : Bool) (findArgs className_1 : Lean.Name) (isNotation_1 : Bool)
  (findArgs_1 : Lean.Name),
  ({ className := className, isNotation := isNotation, findArgs := findArgs } =
      { className := className_1, isNotation := isNotation_1, findArgs := findArgs_1 }) =
    (className = className_1 ∧ isNotation = isNotation_1 ∧ findArgs = findArgs_1)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.norm.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr},
  Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.norm c = Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.norm c_1 → c = c_1
-- Mathlib.Topology.Instances.RatLemmas
Rat.instTotallyDisconnectedSpace : TotallyDisconnectedSpace ℚ
-- Mathlib.Order.WellFoundedSet
/-- **Alias** of the reverse direction of `Set.isPWO_iff_isWF`.

---

In a linear order, the predicates `Set.IsPWO` and `Set.IsWF` are equivalent.  -/
Set.IsWF.isPWO : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Set α}, s.IsWF → s.IsPWO
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.extendRestrictScalarsAdj_counit_app_apply_one_tmul : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (M : ModuleCat S) (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom ((ModuleCat.extendRestrictScalarsAdj f).counit.app M)) (1 ⊗ₜ[R] m) = m
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.mono_of_mem_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s t : Set α}
  {x : α}, ContinuousWithinAt f t x → t ∈ nhdsWithin x s → ContinuousWithinAt f s x
-- Mathlib.Probability.Process.PartitionFiltration
ProbabilityTheory.iSup_countableFiltration : ∀ (α : Type u_2) [m : MeasurableSpace α] [inst : MeasurableSpace.CountablyGenerated α],
  ⨆ n, ↑(ProbabilityTheory.countableFiltration α) n = m
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.measurableSet_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β) {s : Set β},
  MeasurableSet (⇑e ⁻¹' s) ↔ MeasurableSet s
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minKey?.eq_3 : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1)
  (l r r_1 : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).minKey? =
    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minKey?
-- Mathlib.Order.Filter.Basic
Filter.eventually_imp_distrib_right : ∀ {α : Type u} {f : Filter α} {p : α → Prop} {q : Prop}, (∀ᶠ (x : α) in f, p x → q) ↔ (∃ᶠ (x : α) in f, p x) → q
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleInvRotateIso.inv.app X).hom₂ = CategoryTheory.CategoryStruct.id (F.obj X.obj₁)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The morphism `⦋1⦌ ⟶ ⦋n⦌` that picks out the "diagonal composite" edge  -/
SimplexCategory.diag : (n : ℕ) → { len := 1 } ⟶ { len := n }