mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the forward direction of `SimpleGraph.Walk.isCycle_mapLe`. -/
SimpleGraph.Walk.IsCycle.of_mapLe : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u : V} {p : G.Walk u u},
  (SimpleGraph.Walk.mapLe h p).IsCycle → p.IsCycle
-- Init.Data.Nat.Lcm
Nat.lcm_mul_right_right : ∀ (m n : ℕ), n.lcm (n * m) = n * m
-- Mathlib.Probability.Distributions.Gamma
ProbabilityTheory.cdf_gammaMeasure_eq_lintegral : ∀ {a r : ℝ},
  0 < a →
    0 < r →
      ∀ (x : ℝ),
        ↑(ProbabilityTheory.cdf (ProbabilityTheory.gammaMeasure a r)) x =
          (∫⁻ (x : ℝ) in Set.Iic x, ProbabilityTheory.gammaPDF a r x).toReal
-- Init.Data.Array.Basic
/-- Maps `f` over the array and collects the results with `<|>`. The result for the end of the array is
`failure`.

Examples:
 * `#[[], [1, 2], [], [2]].firstM List.head? = some 1`
 * `#[[], [], []].firstM List.head? = none`
 * `#[].firstM List.head? = none`
 -/
Array.firstM : {β : Type v} → {α : Type u} → {m : Type v → Type w} → [Alternative m] → (α → m β) → Array α → m β
-- Mathlib.NumberTheory.ModularForms.SlashActions
_private.Mathlib.NumberTheory.ModularForms.SlashActions.0.ModularForm.«term_∣[_]__1» : Lean.TrailingParserDescr
-- Mathlib.Order.Hom.Lattice
LatticeHom.id_apply : ∀ {α : Type u_2} [inst : Lattice α] (a : α), (LatticeHom.id α) a = a
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
/-- We call a `Multiseries` `Trimmed` if it is either `.nil` or `cons (exp, coef) tl` where `coef`
is trimmed and is not zero.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.Trimmed : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl → Prop
-- Lean.Data.LBool
Lean.instInhabitedLBool.default : Lean.LBool
-- Init.Data.SInt.Bitwise
Int8.neg_one_or : ∀ {a : Int8}, -1 ||| a = -1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_le_arcsin : ∀ {x y : ℝ}, x ≤ y → Real.arcsin x ≤ Real.arcsin y
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shift_shiftFunctorCompIsoId_add_neg_cancel_hom_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] (n : A) (X : C),
  (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C n (-n) ⋯).hom.app X) =
    (CategoryTheory.shiftFunctorCompIsoId C (-n) n ⋯).hom.app ((CategoryTheory.shiftFunctor C n).obj X)
-- Mathlib.LinearAlgebra.TensorProduct.Basis
TensorProduct.equivFinsuppOfBasisLeft_apply_tmul : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq ι]
  (ℬ : Module.Basis ι R M) (m : M) (n : N),
  (TensorProduct.equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ[R] n) = Finsupp.mapRange (fun x => x • n) ⋯ (ℬ.repr m)
-- Mathlib.Data.DFinsupp.Defs
/-- Given `Fintype ι`, `equivFunOnFintype` is the `Equiv` between `Π₀ i, β i` and `Π i, β i`.
(All dependent functions on a finite type are finitely supported.)  -/
DFinsupp.equivFunOnFintype : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → Zero (β i)] → [Fintype ι] → (Π₀ (i : ι), β i) ≃ ((i : ι) → β i)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Extract
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract.go_get : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w newWidth : ℕ} (aig : Std.Sat.AIG α) (input : aig.RefVec w)
  (lo curr : ℕ) (hcurr : curr ≤ newWidth) (s : aig.RefVec curr) (idx : ℕ) (hidx1 : idx < newWidth),
  curr ≤ idx →
    (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract.go input lo curr hcurr s).get idx hidx1 =
      input.getD (lo + idx) (aig.mkConstCached false)
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
String.Slice.Pattern.Model.ForwardStringSearcher.lawfulToForwardSearcherModel : ∀ {pat : String}, pat ≠ "" → String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biproduct.desc_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type}
  [inst_2 : Fintype J] {f : J → C} [inst_3 : CategoryTheory.Limits.HasBiproduct f] {T : C} {g : (j : J) → f j ⟶ T},
  CategoryTheory.Limits.biproduct.desc g =
    ∑ j, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) (g j)
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The bounded continuous map `x ↦ exp (L x * I)`, for a continuous linear form `L`.  -/
BoundedContinuousFunction.probCharDual : {F : Type u_2} →
  [inst : SeminormedAddCommGroup F] → [inst_1 : NormedSpace ℝ F] → StrongDual ℝ F → BoundedContinuousFunction F ℂ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
/-- The power series expansion of `Real.sinh`.  -/
Real.hasSum_sinh : ∀ (r : ℝ), HasSum (fun n => r ^ (2 * n + 1) / ↑(2 * n + 1).factorial) (Real.sinh r)
-- Mathlib.Data.Matrix.Basis
Matrix.mem_range_scalar_iff_commute_single : ∀ {n : Type u_3} {α : Type u_7} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : Semiring α] {M : Matrix n n α},
  M ∈ Set.range ⇑(Matrix.scalar n) ↔ ∀ (i j : n), i ≠ j → Commute (Matrix.single i j 1) M
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.IsIso.instUnmopOfMonoidalOpposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᴹᵒᵖ} (f : X ⟶ Y) [CategoryTheory.IsIso f],
  CategoryTheory.IsIso f.unmop
-- Batteries.Data.List.Lemmas
List.findIdxNth_eq_length_iff : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {xs : List α}, List.findIdxNth p xs n = xs.length ↔ List.countP p xs ≤ n
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_ge : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι],
  MeasureTheory.IsStoppingTime f τ → ∀ (i : ι), MeasurableSet {ω | ↑i ≤ τ ω}
-- Mathlib.Dynamics.Flow
Flow.ext_iff : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddZero τ]
  {ϕ₁ ϕ₂ : Flow τ α}, ϕ₁ = ϕ₂ ↔ ∀ (t : τ) (x : α), ϕ₁.toFun t x = ϕ₂.toFun t x
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u}),
  IsTopologicalAddGroup
    ↑(Profinite.limitCone (F.comp (CategoryTheory.forget₂ ProfiniteAddGrp.{max u v} Profinite))).pt.toTop
-- Mathlib.FieldTheory.Normal.Basic
AlgHom.fieldRange_of_normal : ∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] {E : IntermediateField F K}
  [Normal F ↥E] (f : ↥E →ₐ[F] K), f.fieldRange = E
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.eval₂_uniqueAlgEquiv_symm : ∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Unique σ]
  {f : Polynomial R} {φ : R →+* S} {a : σ → S},
  MvPolynomial.eval₂ φ a ((MvPolynomial.uniqueAlgEquiv R σ).symm f) = Polynomial.eval₂ φ (a default) f
-- Mathlib.RepresentationTheory.Intertwining
/-- Composition of intertwining maps.

A convenience variant of `IntertwiningMap.llcomp` for use in dot notation.  -/
Representation.IntertwiningMap.comp : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        {U : Type u_5} →
          [inst : Semiring A] →
            [inst_1 : Monoid G] →
              [inst_2 : AddCommMonoid V] →
                [inst_3 : AddCommMonoid W] →
                  [inst_4 : AddCommMonoid U] →
                    [inst_5 : Module A V] →
                      [inst_6 : Module A W] →
                        [inst_7 : Module A U] →
                          {ρ : Representation A G V} →
                            {σ : Representation A G W} →
                              {τ : Representation A G U} →
                                σ.IntertwiningMap τ → ρ.IntertwiningMap σ → ρ.IntertwiningMap τ
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.disjoint_closure_left : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, SeparatedNhds s t → Disjoint (closure s) t
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} {h : k' ∈ m.modify k f},
  (m.modify k f).getKey k' h = if (k == k') = true then k else m.getKey k' ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
/-- Given a `2`-truncated simplicial set `X` and a category `C`,
this is the morphism `X ⟶ (truncation 2).obj (nerve C)` corresponding
to a functor `X.HomotopyCategory ⥤ C`.  -/
SSet.Truncated.HomotopyCategory.homToNerveMk : {X : SSet.Truncated 2} →
  {C : Type u} →
    [inst : CategoryTheory.SmallCategory C] →
      CategoryTheory.Functor X.HomotopyCategory C → (X ⟶ (SSet.truncation 2).obj (CategoryTheory.nerve C))
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.opcyclesToCycles_iCycles_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι)
  [inst_2 : K.HasHomology i] [inst_3 : K.HasHomology j] {Z : C} (h : K.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (CategoryTheory.CategoryStruct.comp (K.iCycles j) h) =
    CategoryTheory.CategoryStruct.comp (K.fromOpcycles i j) h
-- ImportGraph.Lean.Environment
/-- Return the name of the module in which a declaration was defined.  -/
Lean.Environment.getModuleFor? : Lean.Environment → Lean.Name → Option Lean.Name
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_alter_of_beq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : Option (β k) → Option (β k)}, (k == k') = true → (k' ∈ m.alter k f ↔ (f (m.get? k)).isSome = true)
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- A topological space is Delta-generated if its topology is generated
by the continuous maps from topological spaces of the form `Fin n → ℝ`.  -/
DeltaGeneratedSpace : (Y : Type u_1) → [TopologicalSpace Y] → Prop
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  (S : CategoryTheory.ShortComplex C), (CategoryTheory.ShortComplex.leftHomologyFunctor C).obj S = S.leftHomology
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
AnalyticAt.hasStrictFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E}, AnalyticAt 𝕜 f x → HasStrictFDerivAt f (fderiv 𝕜 f x) x
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- A list with positive sum must have positive length.  -/
List.length_pos_of_sum_pos : ∀ {M : Type u_4} [inst : AddMonoid M] [inst_1 : Preorder M] (L : List M), 0 < L.sum → 0 < L.length
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addIndex.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (K V : Set G),
  MeasureTheory.Measure.haar.addIndex K V = sInf (Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g + h) ⁻¹' V})
-- Mathlib.MeasureTheory.Constructions.Projective
MeasureTheory.IsProjectiveMeasureFamily.eq_zero_of_isEmpty : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)]
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} [h : IsEmpty ((i : ι) → α i)],
  MeasureTheory.IsProjectiveMeasureFamily P → ∀ (I : Finset ι), P I = 0
-- Mathlib.Order.Interval.Finset.Defs
WithBot.Ioo_coe_coe : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : LocallyFiniteOrder α] (a b : α),
  Finset.Ioo ↑b ↑a = Finset.map Function.Embedding.some (Finset.Ioo b a)
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.mk.injEq : ∀ {E : Type u_1} {c : E} (rIn rOut : ℝ) (rIn_pos : 0 < rIn) (rIn_lt_rOut : rIn < rOut) (rIn_1 rOut_1 : ℝ)
  (rIn_pos_1 : 0 < rIn_1) (rIn_lt_rOut_1 : rIn_1 < rOut_1),
  ({ rIn := rIn, rOut := rOut, rIn_pos := rIn_pos, rIn_lt_rOut := rIn_lt_rOut } =
      { rIn := rIn_1, rOut := rOut_1, rIn_pos := rIn_pos_1, rIn_lt_rOut := rIn_lt_rOut_1 }) =
    (rIn = rIn_1 ∧ rOut = rOut_1)
-- Mathlib.Data.Rat.Cast.Order
Rat.intCast_lt_cast : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {m : ℤ} {n : ℚ}, ↑m < ↑n ↔ ↑m < n
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The functor sending `(X, n)` to the product of copies of `X` indexed by `n`.  -/
CategoryTheory.Limits.piConst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasProducts C] → CategoryTheory.Functor C (CategoryTheory.Functor Type wᵒᵖ C)
-- Mathlib.Probability.Kernel.RadonNikodym
/-- For two kernels `κ, η`, the singular part of `κ a` with respect to `η a` is a measurable
function of `a`.  -/
ProbabilityTheory.Kernel.measurable_singularPart : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η],
  Measurable fun a => (κ a).singularPart (η a)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.continuousOn_setToFun_of_dominated : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {X : Type u_7} [inst_4 : TopologicalSpace X] [FirstCountableTopology X]
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {fs : X → α → E} {bound : α → ℝ} {s : Set X},
  (∀ x ∈ s, MeasureTheory.AEStronglyMeasurable (fs x) μ) →
    (∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a) →
      MeasureTheory.Integrable bound μ →
        (∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s) →
          ContinuousOn (fun x => MeasureTheory.setToFun μ T hT (fs x)) s
-- Mathlib.RingTheory.WittVector.IsPoly
/-- A function `f : Π R, 𝕎 R → 𝕎 R` that maps Witt vectors to Witt vectors over arbitrary base rings
is said to be *polynomial* if there is a family of polynomials `φₙ` over `ℤ` such that the `n`th
coefficient of `f x` is given by evaluating `φₙ` at the coefficients of `x`.

See also `WittVector.IsPoly₂` for the binary variant.

The `ghost_calc` tactic makes use of the `IsPoly` and `IsPoly₂` typeclass and its instances.
(In Lean 3, there was an `@[is_poly]` attribute to manage these instances,
because typeclass resolution did not play well with function composition.
This no longer seems to be an issue, so that such instances can be defined directly.)
 -/
WittVector.IsPoly : (p : ℕ) → (⦃R : Type u_2⦄ → [CommRing R] → WittVector p R → WittVector p R) → Prop
-- Mathlib.CategoryTheory.Action.Continuous
CategoryTheory.Functor.mapContActionCongr_hom : ∀ {V : Type u_5} {W : Type u_6} [inst : CategoryTheory.Category.{v_2, u_5} V] {FV : V → V → Type u_7}
  {CV : V → Type u_8} [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
  [inst_2 : CategoryTheory.ConcreteCategory V FV] [inst_3 : CategoryTheory.HasForget₂ V TopCat]
  [inst_4 : CategoryTheory.Category.{v_3, u_6} W] {FW : W → W → Type u_9} {CW : W → Type u_10}
  [inst_5 : (X Y : W) → FunLike (FW X Y) (CW X) (CW Y)] [inst_6 : CategoryTheory.ConcreteCategory W FW]
  [inst_7 : CategoryTheory.HasForget₂ W TopCat] (G : Type u_11) [inst_8 : Monoid G] [inst_9 : TopologicalSpace G]
  {F F' : CategoryTheory.Functor V W} (e : F ≅ F')
  (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous)
  (H' : ∀ (X : ContAction V G), ((F'.mapAction G).obj X.obj).IsContinuous),
  (CategoryTheory.Functor.mapContActionCongr G e H H').hom =
    { app := fun X => CategoryTheory.ObjectProperty.homMk (Action.mkIso (e.app X.obj.V) ⋯).hom, naturality := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.isoForkOfι_hom_hom : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g),
  c.isoForkOfι.hom.hom = CategoryTheory.CategoryStruct.id c.pt
-- Mathlib.Data.Finset.Sym
Finset.not_isDiag_mk_of_mem_offDiag : ∀ {α : Type u_1} {s : Finset α} {a b : α}, (a, b) ∈ s.offDiag → ¬s(a, b).IsDiag
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_eq_head?_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.minKey? = t.keys.head?
-- Mathlib.Algebra.Group.Action.Faithful
faithfulVAdd_iff : ∀ {G : Type u_2} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α],
  FaithfulVAdd G α ↔ ∀ (g : G), (∀ (a : α), g +ᵥ a = a) → g = 0
-- Mathlib.Analysis.Distribution.TestFunction
/-- See note [custom simps projection].  -/
TestFunction.Simps.coe : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {Ω : TopologicalSpace.Opens E} →
        {F : Type u_4} →
          [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → {n : ℕ∞} → TestFunction Ω F n → E → F
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
zsmulRec.eq_2 : ∀ {G : Type u_1} [inst : Zero G] [inst_1 : Add G] [inst_2 : Neg G] (nsmul : ℕ → G → G) (x : G) (n : ℕ),
  zsmulRec nsmul (Int.negSucc n) x = -nsmul n.succ x
-- Init.Data.UInt.Lemmas
instLawfulCommIdentityUSizeHMulOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 * x2) 1
-- Mathlib.Algebra.Order.CompleteField
/-- Any conditionally complete linearly ordered field is archimedean.  -/
ConditionallyCompleteLinearOrderedField.to_archimedean : ∀ {α : Type u_2} [inst : Field α] [inst_1 : ConditionallyCompleteLinearOrder α] [IsStrictOrderedRing α], Archimedean α
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.coe_edge_down_toOrderHom : ∀ (n : ℕ) (a b : Fin (n + 1)) (hab : a ≤ b),
  ⇑(SimplexCategory.Hom.toOrderHom (SSet.stdSimplex.edge n a b hab).down) = ![a, b]
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.rel_id : ∀ {I : Type u} [inst : DecidableEq I] (R : Type v) [inst_1 : CommSemiring R] (A : I → Type w)
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)] (i : I),
  LinearAlgebra.FreeProduct.rel R A ((TensorAlgebra.ι R) ((DirectSum.lof R I A i) 1)) 1
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Closedness of `carrier`.  -/
SymbolicDynamics.FullShift.MulSubshift.isClosed : ∀ {A : Type u_1} [inst : TopologicalSpace A] {G : Type u_2} [inst_1 : Monoid G]
  (self : SymbolicDynamics.FullShift.MulSubshift A G), IsClosed self.carrier
-- Mathlib.Algebra.Ring.Associator
AddMonoidHom.associator_eq_zero : ∀ {R : Type u_1} [inst : NonUnitalRing R], AddMonoidHom.associator = 0
-- Mathlib.CategoryTheory.Generator.Basic
/-- We say that `P : ObjectProperty C` is codetecting if the functors `C(-, G)`
for `G : C` such that `P G` collectively reflect isomorphisms,
i.e., if any `h` with codomain `G` such that `P G` uniquely factors through `f`,
then `f` is an isomorphism.  -/
CategoryTheory.ObjectProperty.IsCodetecting : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
/-- If a real-valued function has bounded variation on a set, then it is a difference of monotone
functions there. Moreover, one can make sure that the two monotone functions add up to the
variation of `f`.  -/
LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn' : ∀ {α : Type u_1} [inst : LinearOrder α] {f : α → ℝ} {s : Set α},
  LocallyBoundedVariationOn f s →
    ∃ p q,
      MonotoneOn p s ∧
        MonotoneOn q s ∧ f = p - q ∧ ∀ x ∈ s, ∀ y ∈ s, p y - p x + (q y - q x) = variationOnFromTo f s x y
-- Mathlib.Data.Set.Finite.Basic
Set.finite_mem_finset : ∀ {α : Type u} (s : Finset α), {a | a ∈ s}.Finite
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.hom_zsmul : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} (n : ℤ) (f : M ⟶ N),
  ModuleCat.Hom.hom (n • f) = n • ModuleCat.Hom.hom f
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorRightUnitor_inv_naturality : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) {Y : C}
  (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
  (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X X' : CategoryTheory.GradedObject J D) (φ : X ⟶ X')
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
          ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
      p]
  [inst_7 :
    (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj
          ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
      p],
  CategoryTheory.CategoryStruct.comp φ (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X').inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).inv
      (CategoryTheory.GradedObject.mapBifunctorMapMap F p φ
        (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj Y)))
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- `achart H x` is the chart at `x`, considered as an element of the atlas.
Especially useful for working with `BasicContMDiffVectorBundleCore`.  -/
achart : (H : Type u) →
  {M : Type u_2} →
    [inst : TopologicalSpace H] → [inst_1 : TopologicalSpace M] → [inst_2 : ChartedSpace H M] → M → ↑(atlas H M)
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
_private.Mathlib.Data.QPF.Multivariate.Constructions.Sigma.0.MvQPF.Pi.abs.match_1.splitter : {n : ℕ} →
  {A : Type u_1} →
    (F : A → TypeVec.{u_1} n → Type u_1) →
      [inst : (α : A) → MvQPF (F α)] →
        ⦃α : TypeVec.{u_1} n⦄ →
          (motive : ↑(MvQPF.Pi.P F) α → Sort u_2) →
            (x : ↑(MvQPF.Pi.P F) α) →
              ((a : (MvQPF.Pi.P F).A) → (f : ((MvQPF.Pi.P F).B a).Arrow α) → motive ⟨a, f⟩) → motive x
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.prod.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (c : AddCon M) (d : AddCon N),
  c.prod d = { toSetoid := c.prod d.toSetoid, add' := ⋯ }
-- Init.Data.List.MinMax
List.min_mem : ∀ {α : Type u_1} [inst : Min α] [Std.MinEqOr α] {l : List α} (hl : l ≠ []), l.min hl ∈ l
-- Mathlib.Data.Set.Prod
Set.subset_fst_image_prod_snd_image : ∀ {α : Type u_1} {β : Type u_2} {s : Set (α × β)}, s ⊆ (Prod.fst '' s) ×ˢ (Prod.snd '' s)
-- Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem
CategoryTheory.MorphismProperty.IsWeakFactorizationSystem.rlp : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [self : W₁.IsWeakFactorizationSystem W₂], W₁.rlp = W₂
-- Mathlib.NumberTheory.Real.Irrational
irrational_div_intCast_iff : ∀ {m : ℤ} {x : ℝ}, Irrational (x / ↑m) ↔ m ≠ 0 ∧ Irrational x
-- Init.Data.Repr
Char.quoteCore : Char → optParam Bool false → String
-- Lean.Compiler.IR.Format
_private.Lean.Compiler.IR.Format.0.Lean.IR.formatFnBody.loop : ℕ → Lean.IR.FnBody → Std.Format
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get?_inter_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∩ m₂).get? k = none