mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Rep.Res
Rep.res_id : ∀ {k : Type u} [inst : Semiring k] {G : Type v1} [inst_1 : Monoid G] (M : Rep.{u_1, u, v1} k G),
  Rep.res (MonoidHom.id G) M = M
-- Mathlib.Data.FunLike.Group
FunLike.invOneClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : One F] [inst_2 : Inv F]
  [inst_3 : InvOneClass β] [inst_4 : IsOneApply F α β] [inst_5 : IsInvApply F α β],
  FunLike.invOneClass = Function.Injective.invOneClass (fun f => ⇑f) ⋯ ⋯ ⋯
-- Mathlib.Data.ZMod.Basic
ZMod.lift_castAddHom : ∀ (n : ℕ) {A : Type u_2} [inst : AddGroup A] (f : { f // f ↑n = 0 }) (x : ℤ),
  ((ZMod.lift n) f) ((Int.castAddHom (ZMod n)) x) = ↑f x
-- Init.Data.UInt.Basic
instModUInt64 : Mod UInt64
-- Mathlib.Condensed.Functors
instFaithfulCompHausCondensedTypeCompHausToCondensed' : compHausToCondensed'.Faithful
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (y, y⁻¹x)` sends `μ × ν` to `ν × μ`.
This is the function `S⁻¹R` in [Halmos, §59],
where `S` is the map `(x, y) ↦ (x, xy)` and `R` is `Prod.swap`.  -/
MeasureTheory.measurePreserving_prod_inv_mul_swap : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.2, z.2⁻¹ * z.1)) (μ.prod ν) (ν.prod μ)
-- Mathlib.Order.Atoms
IsStronglyAtomic.of_wellFounded_lt : ∀ {α : Type u_2} [inst : PartialOrder α], (WellFounded fun x1 x2 => x1 < x2) → IsStronglyAtomic α
-- Mathlib.Order.UpperLower.Prod
UpperSet.prod_sup : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (s : UpperSet α) (t₁ t₂ : UpperSet β),
  s ×ˢ (t₁ ⊔ t₂) = s ×ˢ t₁ ⊔ s ×ˢ t₂
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- If a monomorphism out of `X` is zero, then `X ≅ 0`.  -/
CategoryTheory.Limits.isoZeroOfMonoEqZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {X Y : C} → {f : X ⟶ Y} → [CategoryTheory.Mono f] → f = 0 → (X ≅ 0)
-- Mathlib.Algebra.Category.Grp.Basic
/-- The forgetful functor from groups to monoids is fully faithful.  -/
GrpCat.fullyFaithfulForget₂ToMonCat : (CategoryTheory.forget₂ GrpCat MonCat).FullyFaithful
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.hsymmPart_zero : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : DecidableEq σ],
  MvPolynomial.hsymmPart σ R (Nat.Partition.indiscrete 0) = 1
-- Mathlib.Algebra.Order.Sub.Basic
tsub_lt_self_iff : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b : α} [AddLeftReflectLE α], a - b < a ↔ 0 < a ∧ 0 < b
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
ModelWithCorners.contDiffWithinAt_extendCoordChange' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {n : WithTop ℕ∞} {I : ModelWithCorners 𝕜 E H} {e e' : OpenPartialHomeomorph M H} [inst_5 : ChartedSpace H M],
  e ∈ IsManifold.maximalAtlas I n M →
    e' ∈ IsManifold.maximalAtlas I n M →
      ∀ {x : M},
        x ∈ e.source →
          x ∈ e'.source →
            ContDiffWithinAt 𝕜 n (↑(ModelWithCorners.extendCoordChange e e')) (Set.range ↑I) (↑(e.extend I) x)
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- The period of an additive action of `g` on `a` is the smallest positive `n`
such that `(n • g) +ᵥ a = a`, or `0` if such an `n` does not exist.  -/
AddAction.period : {α : Type v} → {M : Type u} → [inst : AddMonoid M] → [AddAction M α] → M → α → ℕ
-- Init.Data.List.Sort.Basic
_private.Init.Data.List.Sort.Basic.0.List.merge.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (ys : List α) (h_1 : (ys : List α) → motive [] ys)
  (h_2 : (xs : List α) → motive xs [])
  (h_3 : (x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)),
  (match [], ys with
    | [], ys => h_1 ys
    | xs, [] => h_2 xs
    | x :: xs, y :: ys => h_3 x xs y ys) =
    h_1 ys
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.imp_congr_l : ∀ {σs : List (Type u)} {P P' Q : Std.Do.SPred σs}, (P ⊣⊢ₛ P') → (P → Q) ⊣⊢ₛ P' → Q
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.floor_exp_one_eq_two : ⌊Real.exp 1⌋ = 2
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.inspectOutParams.inspectAux : Lean.Expr →
  Lean.Expr → ℕ → Array Lean.Expr → Array Lean.Expr → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f f₁ : E → F}
  {x : E} {n : WithTop ℕ∞}, ContDiffAt 𝕜 n f x → f₁ =ᶠ[nhds x] f → ContDiffAt 𝕜 n f₁ x
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
FractionalIdeal.le_inv_comm : ∀ {A : Type u_2} {K : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : IsDedekindDomain A]
  [inst_3 : Algebra A K] [inst_4 : IsFractionRing A K] {I J : FractionalIdeal (nonZeroDivisors A) K},
  I ≠ 0 → J ≠ 0 → (I ≤ J⁻¹ ↔ J ≤ I⁻¹)
-- Mathlib.Algebra.Homology.Single
ChainComplex.fromSingle₀Equiv.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] (C : ChainComplex V ℕ) (X : V),
  C.fromSingle₀Equiv X =
    { toFun := fun f => f.f 0, invFun := fun f => HomologicalComplex.mkHomFromSingle f ⋯, left_inv := ⋯,
      right_inv := ⋯ }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.le_maxKey?_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k km : α}
  (hc : t.contains k = true), t.maxKey?.get ⋯ = km → (cmp k km).isLE = true
-- Init.Data.Int.OfNat
Nat.ToInt.natCast_ofNat : ∀ (n : ℕ), ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Analysis.CStarAlgebra.Multiplier
starₗᵢ.congr_simp : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : StarRing 𝕜] [inst_2 : SeminormedAddCommGroup E]
  [inst_3 : StarAddMonoid E] [inst_4 : NormedStarGroup E] [inst_5 : Module 𝕜 E] [inst_6 : StarModule 𝕜 E],
  starₗᵢ 𝕜 = starₗᵢ 𝕜
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereoInvFunAux.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (v w : E),
  stereoInvFunAux v w = (‖w‖ ^ 2 + 4)⁻¹ • (4 • w + (‖w‖ ^ 2 - 4) • v)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.mk_one_eq_monoidOf_mk : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} (x : M), Localization.mk x 1 = (Localization.monoidOf S) x
-- Init.GetElem
Array.getInternal.congr_simp : ∀ {α : Type u} (a a_1 : Array α) (e_a : a = a_1) (i i_1 : ℕ) (e_i : i = i_1) (h : i < a.size),
  a.getInternal i h = a_1.getInternal i_1 ⋯
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.one_notMem_support : ∀ {R : Type u_1} [inst : CommRing R] (P : RingPreordering R) [inst_1 : P.HasIdealSupport], 1 ∉ P.support
-- Mathlib.Tactic.Widget.GCongr
/-- Rpc function for the gcongr widget.  -/
GCongrSelectionPanel.rpc : SelectInsertParams → Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- Given a row partitioned matrix extract the first row  -/
Matrix.toRows₁ : {R : Type u_1} → {m₁ : Type u_3} → {m₂ : Type u_4} → {n : Type u_5} → Matrix (m₁ ⊕ m₂) n R → Matrix m₁ n R
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_union_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, (m₁.union m₂).contains k = true ↔ m₁.contains k = true ∨ m₂.contains k = true
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.bijective : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
  Function.Bijective ⇑e
-- Init.Core
/-- Strict superset relation: `a ⊃ b`  

Conventions for notations in identifiers:

 * The recommended spelling of `⊃` in identifiers is `ssuperset` (prefer `⊂` over `⊃`). -/
SSuperset : {α : Type u_1} → [HasSSubset α] → α → α → Prop
-- Mathlib.NumberTheory.Height.NumberField
NumberField.sum_nonarchAbsVal_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {M : Type u_2} [inst_2 : AddCommMonoid M]
  (f : AbsoluteValue K ℝ → M),
  ∑ᶠ (v : ↑Height.AdmissibleAbsValues.nonarchAbsVal), f ↑v = ∑ᶠ (v : NumberField.FinitePlace K), f ↑v
-- Mathlib.NumberTheory.AbelSummation
_private.Mathlib.NumberTheory.AbelSummation.0.abelSummationProof.sumlocc : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {m : ℕ} (n : ℕ),
  ∀ᵐ (t : ℝ), t ∈ Set.Icc (↑n) (↑n + 1) → ∑ k ∈ Finset.Icc m ⌊t⌋₊, c k = ∑ k ∈ Finset.Icc m n, c k
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.alternatingCofaceMapComplex_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.CosimplicialObject C),
  (AlgebraicTopology.alternatingCofaceMapComplex C).obj X = AlgebraicTopology.AlternatingCofaceMapComplex.obj X
-- Mathlib.Order.Heyting.Hom
BiheytingHom.id_apply : ∀ {α : Type u_2} [inst : BiheytingAlgebra α] (a : α), (BiheytingHom.id α) a = a
-- Mathlib.Data.Set.Image
Set.image_mono : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set α}, s ⊆ t → f '' s ⊆ f '' t
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.instCoeFunHomForallCarrierToTopTotallyDisconnectedSpaceToProfinite.eq_1 : ∀ {M N : ProfiniteGrp.{u}},
  ProfiniteGrp.instCoeFunHomForallCarrierToTopTotallyDisconnectedSpaceToProfinite =
    { coe := fun f => ⇑(ProfiniteGrp.Hom.hom f) }
-- Init.Prelude
/-- The dependent conditional function, in which each branch is provided with a local assumption about
the condition's value. This allows the value to be used in proofs as well as for control flow.

`dcond c (fun h => x) (fun h => y)` is the same as `if h : c then x else y`, but optimized for a
Boolean condition rather than a decidable proposition. Unlike the non-dependent version `cond`,
there is no special notation for `dcond`.

Just like `ite`, `dite`, and `cond`, `dcond` is declared `@[macro_inline]`, which causes
applications of `dcond` to be unfolded. As a result, `x` and `y` are not evaluated at runtime until
one of them is selected, and only the selected branch is evaluated. `dcond` is intended for
metaprogramming use, rather than for use in verified programs, so behavioral lemmas are not
provided.
 -/
Bool.dcond : {α : Sort u} → (c : Bool) → (c = true → α) → (c = false → α) → α
-- Mathlib.Algebra.Azumaya.Defs
IsAzumaya.toFaithfulSMul : ∀ {R : Type u_1} {A : Type u_2} {inst : CommSemiring R} {inst_1 : Semiring A} {inst_2 : Algebra R A}
  [self : IsAzumaya R A], FaithfulSMul R A
-- Lean.Meta.LitValues
/-- Returns `true` if `e` is a literal value.
 -/
Lean.Meta.isLitValue : Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.sheafPushforwardContinuousNatTrans_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} (τ : F ⟶ F') (A : Type u) [inst_2 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [inst_3 : F.IsContinuous J K]
  [inst_4 : F'.IsContinuous J K] (M : CategoryTheory.Sheaf K A),
  ((CategoryTheory.Functor.sheafPushforwardContinuousNatTrans τ A J K).app M).hom =
    CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op τ) ((CategoryTheory.sheafToPresheaf K A).obj M)
-- Lean.Meta.SizeOf
Lean.Meta.SizeOfSpecNested.Context.mk.injEq : ∀ (indInfo : Lean.InductiveVal) (sizeOfFns : Array Lean.Name) (ctorName : Lean.Name)
  (params localInsts : Array Lean.Expr) (recMap : Lean.NameMap Lean.Name) (indInfo_1 : Lean.InductiveVal)
  (sizeOfFns_1 : Array Lean.Name) (ctorName_1 : Lean.Name) (params_1 localInsts_1 : Array Lean.Expr)
  (recMap_1 : Lean.NameMap Lean.Name),
  ({ indInfo := indInfo, sizeOfFns := sizeOfFns, ctorName := ctorName, params := params, localInsts := localInsts,
        recMap := recMap } =
      { indInfo := indInfo_1, sizeOfFns := sizeOfFns_1, ctorName := ctorName_1, params := params_1,
        localInsts := localInsts_1, recMap := recMap_1 }) =
    (indInfo = indInfo_1 ∧
      sizeOfFns = sizeOfFns_1 ∧
        ctorName = ctorName_1 ∧ params = params_1 ∧ localInsts = localInsts_1 ∧ recMap = recMap_1)
-- Plausible.Shrinkable
/-- `Int.shrinkable` operates like `Nat.shrinkable` but also includes the negative variants.  -/
Plausible.Int.shrinkable : Plausible.Shrinkable ℤ
-- Mathlib.RingTheory.Smooth.StandardSmoothOfFree
/-- `S` is an étale `R`-algebra if and only if it is standard smooth of relative dimension `0`.  -/
Algebra.Etale.iff_isStandardSmoothOfRelativeDimension_zero : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Algebra.Etale R S ↔ Algebra.IsStandardSmoothOfRelativeDimension 0 R S
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.transpose_conjTranspose : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Star α] (M : Matrix m n α), M.transpose.conjTranspose = M.map star
-- Mathlib.Data.Set.Sups
Set.forall_infs_iff : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s t : Set α} {p : α → Prop},
  (∀ c ∈ s ⊼ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a ⊓ b)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.equivHomsetLeftOfNatIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} (iso : F ≅ F') {X : C} {Y : D},
  CategoryTheory.Adjunction.equivHomsetLeftOfNatIso iso =
    { toFun := fun f => CategoryTheory.CategoryStruct.comp (iso.inv.app X) f,
      invFun := fun g => CategoryTheory.CategoryStruct.comp (iso.hom.app X) g, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Module.SpanRank
Submodule.lift_spanRank_map_le : ∀ {R : Type u_1} {S : Type u_2} {M : Type u} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S}
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] {L : Type v} [inst_4 : AddCommMonoid L] [inst_5 : Module S L]
  [inst_6 : RingHomSurjective σ] (f : M →ₛₗ[σ] L) (p : Submodule R M),
  Cardinal.lift.{u, v} (Submodule.map f p).spanRank ≤ Cardinal.lift.{v, u} p.spanRank
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.continuousWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞}, ContDiffWithinAt 𝕜 n f s x → ContinuousWithinAt f s x
-- Mathlib.Data.Finsupp.Defs
Finsupp.embDomain.match_1.congr_eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : Option α) (h_1 : (a : α) → motive (some a))
  (h_2 : Unit → motive none),
  x = none →
    (match x with
      | some a => h_1 a
      | none => h_2 ()) ≍
      h_2 ()
-- Mathlib.GroupTheory.ArchimedeanDensely
instLocallyFiniteOrderMultiplicative : {X : Type u_2} → [inst : Preorder X] → [LocallyFiniteOrder X] → LocallyFiniteOrder (Multiplicative X)
-- Batteries.Classes.Order
Std.TransCmp.gt_of_ge_of_gt : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] {x y z : α},
  cmp x y ≠ Ordering.lt → cmp y z = Ordering.gt → cmp x z = Ordering.gt
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.addRecAux_cpopTree : ∀ {len w : ℕ} {x : BitVec (len * w)}, BitVec.addRecAux✝ (BitVec.cast ⋯ x.cpopTree) 1 0#w = BitVec.addRecAux✝ x len 0#w
-- Mathlib.Analysis.Normed.Module.Bases
/-- The basis vectors are linearly independent.  -/
GeneralSchauderBasis.linearIndependent : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L),
  LinearIndependent 𝕜 ↑b
-- Mathlib.Probability.Kernel.Integral
ProbabilityTheory.Kernel.integral_deterministic : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_3}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : β → E} {a : α} [CompleteSpace E] {g : α → β}
  [MeasurableSingletonClass β] (hg : Measurable g),
  ∫ (x : β), f x ∂(ProbabilityTheory.Kernel.deterministic g hg) a = f (g a)
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coe_monomial : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (a : R), ↑((Polynomial.monomial n) a) = (PowerSeries.monomial n) a
-- Mathlib.Control.Fix
Fix.mk : {α : Type u_3} → ((α → α) → α) → Fix α
-- Std.Data.ExtTreeMap.Basic
/-- Returns the `n`-th smallest key.  -/
Std.ExtTreeMap.keyAtIdx : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → (t : Std.ExtTreeMap α β cmp) → (n : ℕ) → n < t.size → α
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
/-- Chooses entering and exiting variables using
[Bland's rule](https://en.wikipedia.org/wiki/Bland%27s_rule) that guarantees that the Simplex
Algorithm terminates.
 -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.choosePivots : {matType : ℕ → ℕ → Type} →
  [inst : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
    Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmM matType (ℕ × ℕ)
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.instNeBotSymmetricIoc : ∀ (G : Type u_1) [inst : Neg G] [inst_1 : Preorder G] [inst_2 : LocallyFiniteOrder G] [Filter.atTop.NeBot],
  (SummationFilter.symmetricIoc G).NeBot
-- Mathlib.NumberTheory.EulerProduct.Basic
Nat.equivProdNatFactoredNumbers.congr_simp : ∀ {s : Finset ℕ} {p : ℕ} (hp : Nat.Prime p) (hs : p ∉ s),
  Nat.equivProdNatFactoredNumbers hp hs = Nat.equivProdNatFactoredNumbers hp hs
-- Mathlib.Data.ENat.Basic
ENat.recTopCoe_zero : ∀ {C : ℕ∞ → Sort u_1} (d : C ⊤) (f : (a : ℕ) → C ↑a), ENat.recTopCoe d f 0 = f 0
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
/-- The composite `A ⟶ A ⨯ A ⟶ cokernel (Δ A)`, where the first map is `(𝟙 A, 0)` and the second map
is the canonical projection into the cokernel.  -/
CategoryTheory.NonPreadditiveAbelian.r : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.NonPreadditiveAbelian C] →
      (A : C) → A ⟶ CategoryTheory.Limits.cokernel (CategoryTheory.Limits.diag A)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The `faceOppositeCentroid` lines on the median through the corresponding vertex.  -/
Affine.Simplex.faceOppositeCentroid_mem_median : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.faceOppositeCentroid i ∈ s.median i
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.def' : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
  {l : Filter α}, f =o[l] g → 0 < c → Asymptotics.IsBigOWith c l f g
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.exists_pow_Uniformizer : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [inst_1 : Field K] {v : Valuation K Γ}
  [hv : v.IsRankOneDiscrete] {r : ↥v.valuationSubring}, r ≠ 0 → ∀ (π : v.Uniformizer), ∃ n u, ↑r = ↑(π.val ^ n) * ↑↑u
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_two_pi : Real.sin (2 * Real.pi) = 0
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- the backwards direction of a homotopy equivalence.  -/
CategoryTheory.ShortComplex.HomotopyEquiv.inv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → {S₁ S₂ : CategoryTheory.ShortComplex C} → S₁.HomotopyEquiv S₂ → (S₂ ⟶ S₁)
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.start : ∀ (pat s : String.Slice), pat.isEmpty = false → String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s 0 0
-- Init.Data.List.Monadic
List.mapM.loop.eq_2 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m β) (x : List β) (a : α) (as : List α),
  List.mapM.loop f (a :: as) x = do
    let __do_lift ← f a
    List.mapM.loop f as (__do_lift :: x)
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.continuous_comp : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : AddMonoid C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] [LocallyCompactSpace B],
  Continuous fun f => f.2.comp f.1
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.reduce_nil : ∀ {α : Type u_1} [inst : DecidableEq α], FreeAddGroup.reduce [] = []
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- The automorphism of the polynomial algebra given by `p(X) ↦ p(a * X + b)`,
with inverse `p(X) ↦ p(a⁻¹ * (X - b))`.  -/
Polynomial.algEquivCMulXAddC : {R : Type u_3} → [inst : CommRing R] → (a : R) → R → [Invertible a] → Polynomial R ≃ₐ[R] Polynomial R
-- Mathlib.Order.Sublattice
Sublattice.apply_mem_map_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {L : Sublattice α} {f : LatticeHom α β} {a : α},
  Function.Injective ⇑f → (f a ∈ Sublattice.map f L ↔ a ∈ L)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {km : α},
  t.maxKey? = some km → t.getKey? km = some km
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc : ∀ {Z : SSet} (h : SSet.stdSimplex.obj { len := 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonIso 0).hom
      (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.face {0}).ι h) =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) h
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.refl_toHom : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M],
  (FirstOrder.Language.Embedding.refl L M).toHom = FirstOrder.Language.Hom.id L M
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.toFilter_mono : ∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι) {l₁ l₂ : BoxIntegral.IntegrationParams},
  l₁ ≤ l₂ → l₁.toFilter I ≤ l₂.toFilter I
-- Mathlib.Data.Finset.Sups
Finset.sups_infs_subset_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DistribLattice α] (s t u : Finset α), t ⊼ u ⊻ s ⊆ (t ⊻ s) ⊼ (u ⊻ s)
-- Mathlib.Topology.Maps.Strict.Basic
/-- A closed continuous map is a strict map.  -/
IsClosedMap.isStrictMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsClosedMap f → Continuous f → Topology.IsStrictMap f
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_eq_pow : ∀ (x : NNReal) (y : ℝ), x.rpow y = x ^ y